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.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... 114 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.010s 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.000s CPU, 0.006s 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_2982.744171 c found header 'p cnf 596 1746' 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 1746 539 0 57 0 0 0 0.0 0 0 @c: 0 0.0 1746 105 481 10 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: 481 fixed, 10 equiv, 0 elim, 57 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, 57 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: 831 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_2982.782678 c found header 'p cnf 1190 4001' 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 4001 1133 0 57 0 0 0 0.0 0 1 @c: 0 0.0 4176 274 901 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: 901 fixed, 15 equiv, 0 elim, 63 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: 61 probed, 1 phases, 0 rounds c prbe: 27 failed, 167 lifted, 0 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 63 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: 143 dominators, 0 high, 0 low c prps: 2151 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_2982.844750 c found header 'p cnf 1784 6256' 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 6256 1727 0 57 0 0 0 0.0 0 1 @c: s 0.0 0 0 1685 20 79 0 0 0.0 0 0 @c: l 0.0 0 0 1685 20 79 0 1000 0.0 0 0 @c: 1 0.0 0 0 1685 20 79 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: 1685 fixed, 20 equiv, 79 elim, 110 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: 493 probed, 1 phases, 2 rounds c prbe: 40 failed, 277 lifted, 18 merged c sccs: 7 non trivial, 0 fixed, 19 merged c hash: 0 units, 73 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 89 doms c strs: 0 forward, 0 backward c doms: 229 dominators, 0 high, 0 low c prps: 4741 propagations, 0.47 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled Original parser has 172 operators. Start parsing planning graph info... Implication Set: 168/396 Total Subsumed Trans # 168 useful for saving op mutex Equivalent Set cnt: 56 out of 396 Basic reducible op analysis... Simple Reducible Trans 0 out of total 226 Simple Reducible Op 0 out of total 172 More advanced reducible op analysis... 0 Single Diff, 170 Easy, out of total 226, SinDiff Covered Actions 0/172 Reasonable Reducible covered actions %d 0 # of shared Preconditions 170 Number of Transitions: 226 Number of Transitions (with prevail ones) : 396 Number of Actions: 172 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 113 Encoding layer 1 Total Number of Trans Variables 397; Op Variables 569 reduced by 0 I.a (Trans Mutex) 397 I.b Transitions's progression 397 I.b Transitions's progression (Backward) 397 I.c Inital state 510 I.d Goal 567 II.b Trans => Opers 737 II.c Opers => Trans 1419 II.d Opers' mutex 1634 SASE Encoding finished. #Var: 595 III.b Implied Transitions 1746 ulimit -t 2400; ../precosat CNF_2982.744171 precosat.result2982.744171 Encoding layer 2 Total Number of Trans Variables 793; Op Variables 1137 reduced by 0 I.a (Trans Mutex) 794 I.b Transitions's progression 1190 I.b Transitions's progression (Backward) 1473 I.c Inital state 1586 I.d Goal 1643 II.b Trans => Opers 1983 II.c Opers => Trans 3347 II.d Opers' mutex 3777 SASE Encoding finished. #Var: 1189 III.b Implied Transitions 4001 ulimit -t 2399; ../precosat CNF_2982.782678 precosat.result2982.782678 Encoding layer 3 Total Number of Trans Variables 1189; Op Variables 1705 reduced by 0 I.a (Trans Mutex) 1191 I.b Transitions's progression 1983 I.b Transitions's progression (Backward) 2549 I.c Inital state 2662 I.d Goal 2719 II.b Trans => Opers 3229 II.c Opers => Trans 5275 II.d Opers' mutex 5920 SASE Encoding finished. #Var: 1783 III.b Implied Transitions 6256 ulimit -t 2399; ../precosat CNF_2982.844750 precosat.result2982.844750 Decoding for total time layer 3 [2] [8] [28] @Steps: 3 Time Span: 3 ; Time 0.23 0:(move r1 v35 v40) 1:(move r1 v40 v39) 2:(move r1 v39 v46) @All Time: 0.23 @SAT Time: 0.02 @Largest SAT Time: 0.01 @Last Encoding VAR: 1784 @Last Encoding CLAUSE: 6256