Parsing... Instantiating... Starting instantiation [8 rules]... Completing instantiation... [0.020s CPU, 0.019s wall-clock] Instantiating: [0.050s CPU, 0.053s wall-clock] Computing fact groups... Finding invariants... 5 initial candidates [0.000s CPU, 0.002s wall-clock] Checking invariant weight... [0.000s CPU, 0.001s wall-clock] Instantiating groups... [0.000s CPU, 0.000s wall-clock] Collecting mutex groups... [0.000s CPU, 0.000s wall-clock] Choosing groups... 122 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.000s 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.010s CPU, 0.001s wall-clock] Translating task: [0.020s CPU, 0.016s 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.007s wall-clock] Writing translation key... [0.010s 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_2910.370982 c found header 'p cnf 692 2047' 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 2043 630 0 62 0 0 0 0.0 0 0 @c: 0 0.0 2043 126 557 9 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: 557 fixed, 9 equiv, 0 elim, 62 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: 41 probed, 1 phases, 0 rounds c prbe: 41 failed, 0 lifted, 0 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 62 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: 1005 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_2910.419737 c found header 'p cnf 1382 4639' 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 4631 1319 0 63 0 0 0 0.0 0 1 @c: 0 0.0 4850 179 1199 4 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: 1199 fixed, 4 equiv, 0 elim, 73 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: 89 probed, 1 phases, 0 rounds c prbe: 37 failed, 236 lifted, 0 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 73 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 78 doms c strs: 0 forward, 0 backward c doms: 189 dominators, 0 high, 0 low c prps: 2872 propagations, 0.29 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_2910.496170 c found header 'p cnf 2072 7231' 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 7219 2008 0 64 0 0 0 0.0 0 1 @c: 0 0.0 7545 281 1784 7 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: 1784 fixed, 7 equiv, 0 elim, 80 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: 214 probed, 1 phases, 0 rounds c prbe: 54 failed, 215 lifted, 0 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 80 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 90 doms c strs: 0 forward, 0 backward c doms: 222 dominators, 0 high, 0 low c prps: 4476 propagations, 0.45 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_2910.599062 c found header 'p cnf 2762 9823' 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 9807 2697 0 65 0 0 0 0.0 0 1 @c: 0 0.0 10388 447 2305 10 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: 2305 fixed, 10 equiv, 0 elim, 102 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: 360 probed, 1 phases, 0 rounds c prbe: 64 failed, 241 lifted, 8 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 94 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 113 doms c strs: 0 forward, 0 backward c doms: 290 dominators, 0 high, 0 low c prps: 6523 propagations, 0.65 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled Original parser has 204 operators. Start parsing planning graph info... Implication Set: 180/424 Total Subsumed Trans # 181 useful for saving op mutex Equivalent Set cnt: 60 out of 424 Basic reducible op analysis... Simple Reducible Trans 3 out of total 242 Simple Reducible Op 2 out of total 204 More advanced reducible op analysis... 0 Single Diff, 179 Easy, out of total 242, SinDiff Covered Actions 0/204 Reasonable Reducible covered actions %d 0 # of shared Preconditions 179 Number of Transitions: 242 Number of Transitions (with prevail ones) : 424 Number of Actions: 204 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 121 Encoding layer 1 Total Number of Trans Variables 425; Op Variables 627 reduced by 2 I.a (Trans Mutex) 425 I.b Transitions's progression 425 I.b Transitions's progression (Backward) 425 I.c Inital state 546 I.d Goal 607 II.b Trans => Opers 789 II.c Opers => Trans 1597 II.d Opers' mutex 1924 SASE Encoding finished. #Var: 691 III.b Implied Transitions 2047 ulimit -t 2400; ../precosat CNF_2910.370982 precosat.result2910.370982 Encoding layer 2 Total Number of Trans Variables 849; Op Variables 1253 reduced by 4 I.a (Trans Mutex) 850 I.b Transitions's progression 1274 I.b Transitions's progression (Backward) 1577 I.c Inital state 1698 I.d Goal 1759 II.b Trans => Opers 2123 II.c Opers => Trans 3739 II.d Opers' mutex 4393 SASE Encoding finished. #Var: 1381 III.b Implied Transitions 4639 ulimit -t 2399; ../precosat CNF_2910.419737 precosat.result2910.419737 Encoding layer 3 Total Number of Trans Variables 1273; Op Variables 1879 reduced by 6 I.a (Trans Mutex) 1275 I.b Transitions's progression 2123 I.b Transitions's progression (Backward) 2729 I.c Inital state 2850 I.d Goal 2911 II.b Trans => Opers 3457 II.c Opers => Trans 5881 II.d Opers' mutex 6862 SASE Encoding finished. #Var: 2071 III.b Implied Transitions 7231 ulimit -t 2399; ../precosat CNF_2910.496170 precosat.result2910.496170 Encoding layer 4 Total Number of Trans Variables 1697; Op Variables 2505 reduced by 8 I.a (Trans Mutex) 1700 I.b Transitions's progression 2972 I.b Transitions's progression (Backward) 3881 I.c Inital state 4002 I.d Goal 4063 II.b Trans => Opers 4791 II.c Opers => Trans 8023 II.d Opers' mutex 9331 SASE Encoding finished. #Var: 2761 III.b Implied Transitions 9823 ulimit -t 2399; ../precosat CNF_2910.599062 precosat.result2910.599062 Encoding layer 5 Total Number of Trans Variables 2121; Op Variables 3131 reduced by 10 I.a (Trans Mutex) 2125 I.b Transitions's progression 3821 I.b Transitions's prc 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_2910.730926 c found header 'p cnf 3452 12415' 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 12395 3386 0 66 0 0 0 0.0 0 2 @c: 0 0.0 13338 762 2636 54 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: 2636 fixed, 54 equiv, 0 elim, 150 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: 527 probed, 1 phases, 0 rounds c prbe: 67 failed, 238 lifted, 23 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 127 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 183 doms c strs: 0 forward, 0 backward c doms: 447 dominators, 0 high, 0 low c prps: 9647 propagations, 0.96 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_2910.892388 c found header 'p cnf 4142 15007' 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 14983 4075 0 67 0 0 0 0.0 0 2 @c: 0 0.0 16222 1107 2984 51 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: 2984 fixed, 51 equiv, 0 elim, 161 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: 712 probed, 1 phases, 0 rounds c prbe: 68 failed, 252 lifted, 9 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 152 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 206 doms c strs: 0 forward, 0 backward c doms: 491 dominators, 0 high, 0 low c prps: 11333 propagations, 0.57 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_2910.96138 c found header 'p cnf 4832 17599' 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 17571 4764 0 68 0 0 0 0.0 0 2 @c: 0 0.0 19261 1556 3168 108 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: 3168 fixed, 108 equiv, 0 elim, 247 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: 914 probed, 1 phases, 0 rounds c prbe: 76 failed, 247 lifted, 47 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 200 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 271 doms c strs: 0 forward, 0 backward c doms: 662 dominators, 0 high, 0 low c prps: 15736 propagations, 0.79 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_2910.320269 c found header 'p cnf 5522 20191' 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 20159 5453 0 69 0 0 0 0.0 0 2 @c: s 0.0 0 0 4690 281 551 0 0 0.0 0 1 @c: l 0.0 0 0 4690 281 551 0 1000 0.0 0 1 @c: 1 0.0 0 0 4690 281 551 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, 62 shrunken, 0 rescored, 0 rebiased c 1 simplifications, 0 reductions c c vars: 4690 fixed, 281 equiv, 551 elim, 623 merged c elim: 302 resolutions, 1 phases, 1 rounds c sbst: 3% 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: 3428 probed, 1 phases, 2 rounds c prbe: 99 failed, 248 lifted, 241 merged c sccs: 27 non trivial, 0 fixed, 69 merged c hash: 0 units, 313 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 82 forward, 62 backward, 475 doms c strs: 7 forward, 2 backward c doms: 1189 dominators, 0 high, 0 low c prps: 41813 propagations, 1.05 megaprops c c 0.0 seconds, 3 MB max, 1 MB recycled ogression (Backward) 5033 I.c Inital state 5154 I.d Goal 5215 II.b Trans => Opers 6125 II.c Opers => Trans 10165 II.d Opers' mutex 11800 SASE Encoding finished. #Var: 3451 III.b Implied Transitions 12415 ulimit -t 2399; ../precosat CNF_2910.730926 precosat.result2910.730926 Encoding layer 6 Total Number of Trans Variables 2545; Op Variables 3757 reduced by 12 I.a (Trans Mutex) 2550 I.b Transitions's progression 4670 I.b Transitions's progression (Backward) 6185 I.c Inital state 6306 I.d Goal 6367 II.b Trans => Opers 7459 II.c Opers => Trans 12307 II.d Opers' mutex 14269 SASE Encoding finished. #Var: 4141 III.b Implied Transitions 15007 ulimit -t 2399; ../precosat CNF_2910.892388 precosat.result2910.892388 Encoding layer 7 Total Number of Trans Variables 2969; Op Variables 4383 reduced by 14 I.a (Trans Mutex) 2975 I.b Transitions's progression 5519 I.b Transitions's progression (Backward) 7337 I.c Inital state 7458 I.d Goal 7519 II.b Trans => Opers 8793 II.c Opers => Trans 14449 II.d Opers' mutex 16738 SASE Encoding finished. #Var: 4831 III.b Implied Transitions 17599 ulimit -t 2399; ../precosat CNF_2910.96138 precosat.result2910.96138 Encoding layer 8 Total Number of Trans Variables 3393; Op Variables 5009 reduced by 16 I.a (Trans Mutex) 3400 I.b Transitions's progression 6368 I.b Transitions's progression (Backward) 8489 I.c Inital state 8610 I.d Goal 8671 II.b Trans => Opers 10127 II.c Opers => Trans 16591 II.d Opers' mutex 19207 SASE Encoding finished. #Var: 5521 III.b Implied Transitions 20191 ulimit -t 2399; ../precosat CNF_2910.320269 precosat.result2910.320269 Decoding for total time layer 8 [2] [7] [21] [44] [70] [98] [128] [153] @Steps: 8 Time Span: 8 ; Time 1.21 0:(move r1 v39 v40) 1:(move r1 v40 v32) 2:(move r1 v32 v25) 3:(move r1 v25 v17) 4:(move r1 v17 v18) 5:(move r1 v18 v19) 6:(move r1 v19 v11) 7:(move r1 v11 v4) @All Time: 1.21 @SAT Time: 0.2 @Largest SAT Time: 0.06 @Last Encoding VAR: 5522 @Last Encoding CLAUSE: 20191