Parsing... Instantiating... Starting instantiation [8 rules]... Completing instantiation... [0.010s CPU, 0.016s wall-clock] Instantiating: [0.040s CPU, 0.045s wall-clock] Computing fact groups... Finding invariants... 5 initial candidates [0.010s CPU, 0.002s wall-clock] Checking invariant weight... [0.000s CPU, 0.000s wall-clock] Instantiating groups... [0.000s CPU, 0.000s wall-clock] Collecting mutex groups... [0.000s CPU, 0.000s wall-clock] Choosing groups... 112 uncovered facts Choosing groups: [0.000s CPU, 0.000s wall-clock] Building translation key... [0.000s CPU, 0.000s wall-clock] Computing fact groups: [0.010s CPU, 0.003s wall-clock] Building STRIPS to SAS dictionary... [0.000s CPU, 0.000s wall-clock] Building dictionary for full mutex groups... [0.000s CPU, 0.000s wall-clock] Translating task... Processing axioms... Processing axioms... Processing axioms: [0.000s CPU, 0.001s wall-clock] Translating task: [0.010s CPU, 0.013s wall-clock] 0 implied effects removed 0 effect conditions simplified 0 implied preconditions added Building mutex information... Building mutex information: [0.000s CPU, 0.001s wall-clock] Detecting unreachable propositions... 0 operators removed 2 propositions removed Detecting unreachable propositions: [0.010s CPU, 0.006s wall-clock] Writing translation key... [0.000s CPU, 0.001s wall-clock] Writing mutex key... [0.000s CPU, 0.002s wall-clock] c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.628656 c found header 'p cnf 595 1734' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 8 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 1734 539 0 56 0 0 0 0.0 0 0 @c: 0 0.0 1734 320 238 37 0 1 0 0.0 0 0 c s UNSATISFIABLE c c 1 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 0 simplifications, 0 reductions c c vars: 238 fixed, 37 equiv, 0 elim, 56 merged c elim: 0 resolutions, 0 phases, 0 rounds c sbst: 0% substituted, 0.0% nots, 0.0% ands, 0.0% xors, 0.0% ites c arty: 0.00 and 0.00 xor average arity c prbe: 16 probed, 1 phases, 0 rounds c prbe: 16 failed, 0 lifted, 0 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 56 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 0 doms c strs: 0 forward, 0 backward c doms: 0 dominators, 0 high, 0 low c prps: 438 propagations, 0.00 megaprops c c 0.0 seconds, 0 MB max, 0 MB recycled c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.667632 c found header 'p cnf 1188 3968' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 0 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 3968 1132 0 56 0 0 0 0.0 0 1 @c: 0 0.0 4134 745 399 44 0 1 0 0.0 0 1 c s UNSATISFIABLE c c 1 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 0 simplifications, 0 reductions c c vars: 399 fixed, 44 equiv, 0 elim, 61 merged c elim: 0 resolutions, 0 phases, 0 rounds c sbst: 0% substituted, 0.0% nots, 0.0% ands, 0.0% xors, 0.0% ites c arty: 0.00 and 0.00 xor average arity c prbe: 53 probed, 1 phases, 0 rounds c prbe: 17 failed, 233 lifted, 4 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 57 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 42 doms c strs: 0 forward, 0 backward c doms: 131 dominators, 0 high, 0 low c prps: 1531 propagations, 0.00 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.730196 c found header 'p cnf 1781 6202' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 0 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 6202 1725 0 56 0 0 0 0.0 0 1 @c: 0 0.0 6412 457 1307 17 0 1 0 0.0 0 1 c s UNSATISFIABLE c c 1 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 0 simplifications, 0 reductions c c vars: 1307 fixed, 17 equiv, 0 elim, 66 merged c elim: 0 resolutions, 0 phases, 0 rounds c sbst: 0% substituted, 0.0% nots, 0.0% ands, 0.0% xors, 0.0% ites c arty: 0.00 and 0.00 xor average arity c prbe: 153 probed, 1 phases, 0 rounds c prbe: 29 failed, 229 lifted, 1 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 65 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 68 doms c strs: 0 forward, 0 backward c doms: 149 dominators, 0 high, 0 low c prps: 3094 propagations, 0.00 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.816924 c found header 'p cnf 2374 8436' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 8 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 8436 2318 0 56 0 0 0 0.0 0 1 @c: 0 0.0 9316 404 1954 16 0 1 0 0.0 0 1 c s UNSATISFIABLE c c 1 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 0 simplifications, 0 reductions c c vars: 1954 fixed, 16 equiv, 0 elim, 142 merged c elim: 0 resolutions, 0 phases, 0 rounds c sbst: 0% substituted, 0.0% nots, 0.0% ands, 0.0% xors, 0.0% ites c arty: 0.00 and 0.00 xor average arity c prbe: 318 probed, 1 phases, 0 rounds c prbe: 55 failed, 279 lifted, 33 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 109 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 165 doms c strs: 0 forward, 0 backward c doms: 485 dominators, 0 high, 0 low c prps: 9404 propagations, 0.94 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled Original parser has 170 operators. Start parsing planning graph info... Implication Set: 165/389 Total Subsumed Trans # 165 useful for saving op mutex Equivalent Set cnt: 55 out of 389 Basic reducible op analysis... Simple Reducible Trans 0 out of total 222 Simple Reducible Op 0 out of total 170 More advanced reducible op analysis... 0 Single Diff, 167 Easy, out of total 222, SinDiff Covered Actions 0/170 Reasonable Reducible covered actions %d 0 # of shared Preconditions 167 Number of Transitions: 222 Number of Transitions (with prevail ones) : 389 Number of Actions: 170 Encoding-Constants Initilized! Encoding layer 0 Total Number of Trans Variables 1; Op Variables 1 reduced by 0 I.a (Trans Mutex) 0 I.b Transitions's progression 0 I.b Transitions's progression (Backward) 0 I.c Inital state 111 Encoding layer 1 Total Number of Trans Variables 390; Op Variables 560 reduced by 0 I.a (Trans Mutex) 390 I.b Transitions's progression 390 I.b Transitions's progression (Backward) 390 I.c Inital state 501 I.d Goal 557 II.b Trans => Opers 724 II.c Opers => Trans 1398 II.d Opers' mutex 1624 SASE Encoding finished. #Var: 594 III.b Implied Transitions 1734 ulimit -t 2400; ../precosat CNF_2931.628656 precosat.result2931.628656 Encoding layer 2 Total Number of Trans Variables 779; Op Variables 1119 reduced by 0 I.a (Trans Mutex) 780 I.b Transitions's progression 1169 I.b Transitions's progression (Backward) 1447 I.c Inital state 1558 I.d Goal 1614 II.b Trans => Opers 1948 II.c Opers => Trans 3296 II.d Opers' mutex 3748 SASE Encoding finished. #Var: 1187 III.b Implied Transitions 3968 ulimit -t 2399; ../precosat CNF_2931.667632 precosat.result2931.667632 Encoding layer 3 Total Number of Trans Variables 1168; Op Variables 1678 reduced by 0 I.a (Trans Mutex) 1170 I.b Transitions's progression 1948 I.b Transitions's progression (Backward) 2504 I.c Inital state 2615 I.d Goal 2671 II.b Trans => Opers 3172 II.c Opers => Trans 5194 II.d Opers' mutex 5872 SASE Encoding finished. #Var: 1780 III.b Implied Transitions 6202 ulimit -t 2399; ../precosat CNF_2931.730196 precosat.result2931.730196 Encoding layer 4 Total Number of Trans Variables 1557; Op Variables 2237 reduced by 0 I.a (Trans Mutex) 1560 I.b Transitions's progression 2727 I.b Transitions's progression (Backward) 3561 I.c Inital state 3672 I.d Goal 3728 II.b Trans => Opers 4396 II.c Opers => Trans 7092 II.d Opers' mutex 7996 SASE Encoding finished. #Var: 2373 III.b Implied Transitions 8436 ulimit -t 2399; ../precosat CNF_2931.816924 precosat.result2931.816924 Encoding layer 5 Total Number of Trans Variables 1946; Op Variables 2796 reduced by 0 I.a (Trans Mutex) 1950 I.b Transitions's progression 3506 I.b Transitions's proc PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.928702 c found header 'p cnf 2967 10670' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 16 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 10670 2911 0 56 0 0 0 0.0 0 1 @c: 0 0.0 12217 482 2468 17 0 1 0 0.0 0 2 c s UNSATISFIABLE c c 1 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 0 simplifications, 0 reductions c c vars: 2468 fixed, 17 equiv, 0 elim, 140 merged c elim: 0 resolutions, 0 phases, 0 rounds c sbst: 0% substituted, 0.0% nots, 0.0% ands, 0.0% xors, 0.0% ites c arty: 0.00 and 0.00 xor average arity c prbe: 476 probed, 1 phases, 0 rounds c prbe: 62 failed, 232 lifted, 5 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 135 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 256 doms c strs: 0 forward, 0 backward c doms: 627 dominators, 0 high, 0 low c prps: 13503 propagations, 0.68 megaprops c c 0.0 seconds, 2 MB max, 0 MB recycled c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.66261 c found header 'p cnf 3560 12904' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 0 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 12904 3504 0 56 0 0 0 0.0 0 2 @c: 0 0.0 14867 782 2715 63 0 1 0 0.0 0 2 c s UNSATISFIABLE c c 1 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 0 simplifications, 0 reductions c c vars: 2715 fixed, 63 equiv, 0 elim, 185 merged c elim: 0 resolutions, 0 phases, 0 rounds c sbst: 0% substituted, 0.0% nots, 0.0% ands, 0.0% xors, 0.0% ites c arty: 0.00 and 0.00 xor average arity c prbe: 651 probed, 1 phases, 0 rounds c prbe: 61 failed, 233 lifted, 23 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 162 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 367 doms c strs: 0 forward, 0 backward c doms: 736 dominators, 0 high, 0 low c prps: 18496 propagations, 0.92 megaprops c c 0.0 seconds, 2 MB max, 0 MB recycled c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.229659 c found header 'p cnf 4153 15138' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 0 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 15138 4097 0 56 0 0 0 0.0 0 2 @c: 0 0.0 17449 1250 2824 79 0 1 0 0.0 0 2 c s UNSATISFIABLE c c 1 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 0 simplifications, 0 reductions c c vars: 2824 fixed, 79 equiv, 0 elim, 186 merged c elim: 0 resolutions, 0 phases, 0 rounds c sbst: 0% substituted, 0.0% nots, 0.0% ands, 0.0% xors, 0.0% ites c arty: 0.00 and 0.00 xor average arity c prbe: 815 probed, 1 phases, 0 rounds c prbe: 63 failed, 232 lifted, 6 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 180 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 420 doms c strs: 0 forward, 0 backward c doms: 825 dominators, 0 high, 0 low c prps: 20352 propagations, 1.02 megaprops c c 0.0 seconds, 2 MB max, 0 MB recycled c PicoSATLight Version 236 3e7a3f8825c0b9e241f38a63fee5517540b2feca c Copyright (C) 2009, Armin Biere, JKU, Linz, Austria. All rights reserved. c Released on Thu Jul 9 17:46:36 CEST 2009 c Compiled on Tue Apr 26 15:52:00 CDT 2011 c g++ (GCC) 4.1.2 20080704 (Red Hat 4.1.2-48) c -O3 -static -Wall -Wextra -DNDEBUG -DNLOGPRECO -DNSTATSPRECO c -finline-limit=10000000 -fomit-frame-pointer -fno-exceptions c Linux moss.cse.wustl.edu 2.6.18-194.32.1.el5 x86_64 c c reading CNF_2931.424003 c found header 'p cnf 4746 17372' c finished parsing c c --check=0 --verbose=0 --order=3 --simprd=40 --merge=1 --hash=1 c --dominate=1 --restart=1 --restartint=100 --rebias=1 --rebiasint=1000 c --probe=1 --probeint=100000 --probeprd=10 --decompose=1 --minimize=3 c --maxdepth=1000 --strength=10 --elim=1 --elimint=300000 --elimprd=20 c --subst=1 --ands=1 --xors=1 --ites=1 --minlimit=1000 --maxlimit=10000000 c --random=1 --spread=2000 --seed=0 --skip=25 c c sizeof vars[0] = 24 alignment = 16 0 MB c sizeof orgs[0] = 16 alignment = 0 0 MB c sizeof occs[0] = 16 alignment = 0 0 MB c sizeof iirfs[0..1] = 8 alignment = 0 0 MB c c starting search after 0.0 seconds c no decision limit c c original/binary fixed eliminated learned agility c seconds variables equivalent conflicts height MB c @c: * 0.0 17372 4690 0 56 0 0 0 0.0 0 2 @c: s 0.0 0 0 4305 154 287 0 0 0.0 0 1 @c: l 0.0 0 0 4305 154 287 0 1000 0.0 0 1 @c: 1 0.0 0 0 4305 154 287 0 0 0.0 0 1 c s SATISFIABLE v v 0 c c 0 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 23 shrunken, 0 rescored, 0 rebiased c 1 simplifications, 0 reductions c c vars: 4305 fixed, 154 equiv, 287 elim, 568 merged c elim: 64 resolutions, 1 phases, 1 rounds c sbst: 1% substituted, 0.0% nots, 100.0% ands, 0.0% xors, 0.0% ites c arty: 2.00 and 0.00 xor average arity c prbe: 2200 probed, 1 phases, 2 rounds c prbe: 78 failed, 240 lifted, 158 merged c sccs: 39 non trivial, 0 fixed, 124 merged c hash: 0 units, 286 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 26 forward, 24 backward, 582 doms c strs: 1 forward, 1 backward c doms: 1213 dominators, 0 high, 0 low c prps: 32622 propagations, 1.09 megaprops c c 0.0 seconds, 3 MB max, 1 MB recycled gression (Backward) 4618 I.c Inital state 4729 I.d Goal 4785 II.b Trans => Opers 5620 II.c Opers => Trans 8990 II.d Opers' mutex 10120 SASE Encoding finished. #Var: 2966 III.b Implied Transitions 10670 ulimit -t 2399; ../precosat CNF_2931.928702 precosat.result2931.928702 Encoding layer 6 Total Number of Trans Variables 2335; Op Variables 3355 reduced by 0 I.a (Trans Mutex) 2340 I.b Transitions's progression 4285 I.b Transitions's progression (Backward) 5675 I.c Inital state 5786 I.d Goal 5842 II.b Trans => Opers 6844 II.c Opers => Trans 10888 II.d Opers' mutex 12244 SASE Encoding finished. #Var: 3559 III.b Implied Transitions 12904 ulimit -t 2399; ../precosat CNF_2931.66261 precosat.result2931.66261 Encoding layer 7 Total Number of Trans Variables 2724; Op Variables 3914 reduced by 0 I.a (Trans Mutex) 2730 I.b Transitions's progression 5064 I.b Transitions's progression (Backward) 6732 I.c Inital state 6843 I.d Goal 6899 II.b Trans => Opers 8068 II.c Opers => Trans 12786 II.d Opers' mutex 14368 SASE Encoding finished. #Var: 4152 III.b Implied Transitions 15138 ulimit -t 2399; ../precosat CNF_2931.229659 precosat.result2931.229659 Encoding layer 8 Total Number of Trans Variables 3113; Op Variables 4473 reduced by 0 I.a (Trans Mutex) 3120 I.b Transitions's progression 5843 I.b Transitions's progression (Backward) 7789 I.c Inital state 7900 I.d Goal 7956 II.b Trans => Opers 9292 II.c Opers => Trans 14684 II.d Opers' mutex 16492 SASE Encoding finished. #Var: 4745 III.b Implied Transitions 17372 ulimit -t 2399; ../precosat CNF_2931.424003 precosat.result2931.424003 Decoding for total time layer 8 [1] [6] [15] [24] [32] [38] [44] [59] @Steps: 8 Time Span: 8 ; Time 1.02 0:(move r1 v54 v53) 1:(move r1 v53 v46) 2:(move r1 v46 v39) 3:(move r1 v39 v34) 4:(move r1 v34 v33) 5:(move r1 v33 v25) 6:(move r1 v25 v19) 7:(move r1 v19 v18) @All Time: 1.02 @SAT Time: 0.18 @Largest SAT Time: 0.05 @Last Encoding VAR: 4746 @Last Encoding CLAUSE: 17372