---SatPlan Version: 1.1 bb: parsing domain file domain 'MULTIROBOT' defined ... done. bb: parsing problem file problem 'MULTIROBOT_INSTANCE' defined ... done. time: 0, 52 facts and 0 exclusive pairs 55 ops and 3 exclusive pairs time: 1, 56 facts and 3 exclusive pairs creating thin gp-based encoding... plan graph layer 0... plan graph layer 1... goal constraints... goal fact not coded - level too low?? bb: parsing domain file domain 'MULTIROBOT' defined ... done. bb: parsing problem file problem 'MULTIROBOT_INSTANCE' defined ... done. time: 0, 52 facts and 0 exclusive pairs 55 ops and 3 exclusive pairs time: 1, 56 facts and 3 exclusive pairs 69 ops and 49 exclusive pairs time: 2, 62 facts and 6 exclusive pairs creating thin gp-based encoding... plan graph layer 0... plan graph layer 1... plan graph layer 2... goal constraints... goal fact not coded - level too low?? bb: parsing domain file domain 'MULTIROBOT' defined ... done. bb: parsing problem file problem 'MULTIROBOT_INSTANCE' defined ... done. time: 0, 52 facts and 0 exclusive pairs 55 ops and 3 exclusive pairs time: 1, 56 facts and 3 exclusive pairs 69 ops and 49 exclusive pairs time: 2, 62 facts and 6 exclusive pairs 97 ops and 149 exclusive pairs time: 3, 73 facts and 11 exclusive pairs creating thin gp-based encoding... plan graph layer 0... plan graph layer 1... plan graph layer 2... plan graph layer 3... goal constraints... goal fact not coded - level too low?? bb: parsing domain file domain 'MULTIROBOT' defined ... done. bb: parsing problem file problem 'MULTIROBOT_INSTANCE' defined ... done. time: 0, 52 facts and 0 exclusive pairs 55 ops and 3 exclusive pairs time: 1, 56 facts and 3 exclusive pairs 69 ops and 49 exclusive pairs time: 2, 62 facts and 6 exclusive pairs 97 ops and 149 exclusive pairs time: 3, 73 facts and 11 exclusive pairs 139 ops and 324 exclusive pairs time: 4, 82 facts and 9 exclusive pairs creating thin gp-based encoding... plan graph layer 0... plan graph layer 1... plan graph layer 2... plan graph layer 3... plan graph layer 4... goal constraints... goal fact not coded - level too low?? bb: parsing domain file domain 'MULTIROBOT' defined ... done. bb: parsing problem file problem 'MULTIROBOT_INSTANCE' defined ... done. time: 0, 52 facts and 0 exclusive pairs 55 ops and 3 exclusive pairs time: 1, 56 facts and 3 exclusive pairs 69 ops and 49 exclusive pairs time: 2, 62 facts and 6 exclusive pairs 97 ops and 149 exclusive pairs time: 3, 73 facts and 11 exclusive pairs 139 ops and 324 exclusive pairs time: 4, 82 facts and 9 exclusive pairs 180 ops and 480 exclusive pairs time: 5, 93 facts and 11 exclusive pairs creating thin gp-based encoding... plan graph layer 0... plan graph layer 1... plan graph layer 2... plan graph layer 3... plan graph layer 4... plan graph layer 5... goal constraints... exclusion constraints layer 0... exclusion constraints layer 1... exclusion constraints layer 2... exclusion constraints layer 3... exclusion constraints layer 4... exclusion constraints layer 5... DECISION LAYER 5, WRITING THIN GP-BASED ENCODING WITH 958 VARS, 2039 CLAUSES. time spent: 0.00 seconds instantiating 8316 action templates 0.00 seconds reachability analysis, yielding 106 facts and 154 actions 0.00 seconds collecting 105 relevant facts 0.00 seconds building connectivity graph 0.00 seconds building (std) graph 0.01 seconds CNF output time 0.01 seconds total planner time (solving not included) ***Solving*** [ filemap ] [ extract ] variables : 958 pure lits : 92 1-clauses : 53 2-clauses : 1842 3-clauses : 37 n-clauses : 107 discarded : 0 [ solve ] satisfiable [ stats ] decisions : 1107 conflicts : 47 time : ~0.01 bb: parsing domain file domain 'MULTIROBOT' defined ... done. bb: parsing problem file problem 'MULTIROBOT_INSTANCE' defined ... done. time: 0, 52 facts and 0 exclusive pairs 55 ops and 3 exclusive pairs time: 1, 56 facts and 3 exclusive pairs 69 ops and 49 exclusive pairs time: 2, 62 facts and 6 exclusive pairs 97 ops and 149 exclusive pairs time: 3, 73 facts and 11 exclusive pairs 139 ops and 324 exclusive pairs time: 4, 82 facts and 9 exclusive pairs 180 ops and 480 exclusive pairs time: 5, 93 facts and 11 exclusive pairs creating thin gp-based encoding... plan graph layer 0... plan graph layer 1... plan graph layer 2... plan graph layer 3... plan graph layer 4... plan graph layer 5... goal constraints... exclusion constraints layer 0... exclusion constraints layer 1... exclusion constraints layer 2... exclusion constraints layer 3... exclusion constraints layer 4... exclusion constraints layer 5... DECISION LAYER 5, WRITING THIN GP-BASED ENCODING WITH 958 VARS, 2039 CLAUSES. time spent: 0.01 seconds instantiating 8316 action templates 0.00 seconds reachability analysis, yielding 106 facts and 154 actions 0.00 seconds collecting 105 relevant facts 0.00 seconds building connectivity graph 0.00 seconds building (std) graph 0.00 seconds CNF output time 0.01 seconds total planner time (solving not included) Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] Pruned: 0: (MOVE R1 V52 V51) [1] ---SatPlan Version: 1.1 ***SAT!*** Solved in 5 layers Real Time: = 0.05 User Time: = 0.09 Syst Time: = 0