Parsing... Instantiating... Starting instantiation [8 rules]... Completing instantiation... [0.020s CPU, 0.016s wall-clock] Instantiating: [0.040s CPU, 0.043s wall-clock] Computing fact groups... Finding invariants... 5 initial candidates [0.000s 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... 106 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.012s 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.000s CPU, 0.006s wall-clock] Writing translation key... [0.000s CPU, 0.001s wall-clock] Writing mutex key... [0.010s 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_2882.182916 c found header 'p cnf 550 1607' 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 1599 495 0 55 0 0 0 0.0 0 0 @c: 0 0.0 1599 112 427 11 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: 427 fixed, 11 equiv, 0 elim, 55 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: 32 probed, 1 phases, 0 rounds c prbe: 32 failed, 0 lifted, 0 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 55 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: 779 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_2882.226614 c found header 'p cnf 1098 3687' 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 3671 1041 0 57 0 0 0 0.0 0 0 @c: 0 0.0 3813 281 802 15 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: 802 fixed, 15 equiv, 0 elim, 71 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: 65 probed, 1 phases, 0 rounds c prbe: 29 failed, 140 lifted, 4 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 67 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 48 doms c strs: 0 forward, 0 backward c doms: 117 dominators, 0 high, 0 low c prps: 1947 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_2882.291272 c found header 'p cnf 1646 5767' 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 5743 1587 0 59 0 0 0 0.0 0 1 @c: 0 0.0 5921 565 1058 23 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: 1058 fixed, 23 equiv, 0 elim, 72 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: 140 probed, 1 phases, 0 rounds c prbe: 32 failed, 133 lifted, 1 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 71 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 55 doms c strs: 0 forward, 0 backward c doms: 115 dominators, 0 high, 0 low c prps: 2670 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_2882.377105 c found header 'p cnf 2194 7847' 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 7815 2133 0 61 0 0 0 0.0 0 1 @c: 0 0.0 8117 1137 1012 45 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: 1012 fixed, 45 equiv, 0 elim, 76 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: 218 probed, 1 phases, 0 rounds c prbe: 34 failed, 139 lifted, 1 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 75 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 60 doms c strs: 0 forward, 0 backward c doms: 132 dominators, 0 high, 0 low c prps: 3405 propagations, 0.00 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled Original parser has 154 operators. Start parsing planning graph info... Implication Set: 156/368 Total Subsumed Trans # 158 useful for saving op mutex Equivalent Set cnt: 52 out of 368 Basic reducible op analysis... Simple Reducible Trans 6 out of total 210 Simple Reducible Op 4 out of total 154 More advanced reducible op analysis... 0 Single Diff, 152 Easy, out of total 210, SinDiff Covered Actions 0/154 Reasonable Reducible covered actions %d 0 # of shared Preconditions 152 Number of Transitions: 210 Number of Transitions (with prevail ones) : 368 Number of Actions: 154 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 105 Encoding layer 1 Total Number of Trans Variables 369; Op Variables 519 reduced by 4 I.a (Trans Mutex) 369 I.b Transitions's progression 369 I.b Transitions's progression (Backward) 369 I.c Inital state 474 I.d Goal 527 II.b Trans => Opers 685 II.c Opers => Trans 1295 II.d Opers' mutex 1497 SASE Encoding finished. #Var: 549 III.b Implied Transitions 1607 ulimit -t 2400; ../precosat CNF_2882.182916 precosat.result2882.182916 Encoding layer 2 Total Number of Trans Variables 737; Op Variables 1037 reduced by 8 I.a (Trans Mutex) 738 I.b Transitions's progression 1106 I.b Transitions's progression (Backward) 1369 I.c Inital state 1474 I.d Goal 1527 II.b Trans => Opers 1843 II.c Opers => Trans 3063 II.d Opers' mutex 3467 SASE Encoding finished. #Var: 1097 III.b Implied Transitions 3687 ulimit -t 2399; ../precosat CNF_2882.226614 precosat.result2882.226614 Encoding layer 3 Total Number of Trans Variables 1105; Op Variables 1555 reduced by 12 I.a (Trans Mutex) 1107 I.b Transitions's progression 1843 I.b Transitions's progression (Backward) 2369 I.c Inital state 2474 I.d Goal 2527 II.b Trans => Opers 3001 II.c Opers => Trans 4831 II.d Opers' mutex 5437 SASE Encoding finished. #Var: 1645 III.b Implied Transitions 5767 ulimit -t 2399; ../precosat CNF_2882.291272 precosat.result2882.291272 Encoding layer 4 Total Number of Trans Variables 1473; Op Variables 2073 reduced by 16 I.a (Trans Mutex) 1476 I.b Transitions's progression 2580 I.b Transitions's progression (Backward) 3369 I.c Inital state 3474 I.d Goal 3527 II.b Trans => Opers 4159 II.c Opers => Trans 6599 II.d Opers' mutex 7407 SASE Encoding finished. #Var: 2193 III.b Implied Transitions 7847 ulimit -t 2399; ../precosat CNF_2882.377105 precosat.result2882.377105 Encoding layer 5 Total Number of Trans Variables 1841; Op Variables 2591 reduced by 20 I.a (Trans Mutex) 1845 I.b Transitions's progression 3317 I.b Transitions's 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_2882.484807 c found header 'p cnf 2742 9927' 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 9887 2679 0 63 0 0 0 0.0 0 1 @c: 0 0.0 10256 1320 1386 36 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: 1386 fixed, 36 equiv, 0 elim, 78 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: 38 failed, 139 lifted, 1 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 77 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 63 doms c strs: 0 forward, 0 backward c doms: 137 dominators, 0 high, 0 low c prps: 4564 propagations, 0.46 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_2882.617391 c found header 'p cnf 3290 12007' 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 11959 3225 0 65 0 0 0 0.0 0 1 @c: s 0.0 0 0 3080 27 183 0 0 0.0 0 0 @c: l 0.0 0 0 3080 27 183 0 1000 0.0 0 0 @c: 1 0.0 0 0 3080 27 183 0 0 0.0 0 0 c s SATISFIABLE v v 0 c c 0 conflicts, 0 decisions, 0 random c 0 iterations, 0 restarts, 0 skipped c 0 enlarged, 0 shrunken, 0 rescored, 0 rebiased c 1 simplifications, 0 reductions c c vars: 3080 fixed, 27 equiv, 183 elim, 242 merged c elim: 0 resolutions, 1 phases, 1 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: 1328 probed, 1 phases, 2 rounds c prbe: 65 failed, 252 lifted, 41 merged c sccs: 16 non trivial, 0 fixed, 43 merged c hash: 0 units, 158 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: 543 dominators, 0 high, 0 low c prps: 11518 propagations, 0.58 megaprops c c 0.0 seconds, 2 MB max, 1 MB recycled progression (Backward) 4369 I.c Inital state 4474 I.d Goal 4527 II.b Trans => Opers 5317 II.c Opers => Trans 8367 II.d Opers' mutex 9377 SASE Encoding finished. #Var: 2741 III.b Implied Transitions 9927 ulimit -t 2399; ../precosat CNF_2882.484807 precosat.result2882.484807 Encoding layer 6 Total Number of Trans Variables 2209; Op Variables 3109 reduced by 24 I.a (Trans Mutex) 2214 I.b Transitions's progression 4054 I.b Transitions's progression (Backward) 5369 I.c Inital state 5474 I.d Goal 5527 II.b Trans => Opers 6475 II.c Opers => Trans 10135 II.d Opers' mutex 11347 SASE Encoding finished. #Var: 3289 III.b Implied Transitions 12007 ulimit -t 2399; ../precosat CNF_2882.617391 precosat.result2882.617391 Decoding for total time layer 6 [0] [3] [15] [42] [70] [104] @Steps: 6 Time Span: 6 ; Time 0.64 0:(move r1 v28 v24) 1:(move r1 v24 v17) 2:(move r1 v17 v18) 3:(move r1 v18 v11) 4:(move r1 v11 v3) 5:(move r1 v3 v4) @All Time: 0.64 @SAT Time: 0.13 @Largest SAT Time: 0.04 @Last Encoding VAR: 3290 @Last Encoding CLAUSE: 12007