Parsing... Instantiating... Starting instantiation [8 rules]... Completing instantiation... [0.020s CPU, 0.016s wall-clock] Instantiating: [0.050s 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... 110 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.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.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_2896.838280 c found header 'p cnf 578 1689' 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 1689 523 0 55 0 0 0 0.0 0 0 @c: 0 0.0 1689 268 280 30 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: 280 fixed, 30 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: 20 probed, 1 phases, 0 rounds c prbe: 20 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: 508 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_2896.878319 c found header 'p cnf 1154 3869' 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 3869 1099 0 55 0 0 0 0.0 0 1 @c: 0 0.0 4000 692 422 40 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: 422 fixed, 40 equiv, 0 elim, 59 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: 48 probed, 1 phases, 0 rounds c prbe: 16 failed, 197 lifted, 0 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 59 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 38 doms c strs: 0 forward, 0 backward c doms: 100 dominators, 0 high, 0 low c prps: 1366 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_2896.941717 c found header 'p cnf 1730 6049' 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 6049 1675 0 55 0 0 0 0.0 0 1 @c: 0 0.0 6343 153 1574 3 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: 1574 fixed, 3 equiv, 0 elim, 74 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: 164 probed, 1 phases, 0 rounds c prbe: 34 failed, 258 lifted, 3 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, 81 doms c strs: 0 forward, 0 backward c doms: 195 dominators, 0 high, 0 low c prps: 3692 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_2896.29931 c found header 'p cnf 2306 8229' 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 8229 2251 0 55 0 0 0 0.0 0 1 @c: 0 0.0 8659 193 2104 9 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: 2104 fixed, 9 equiv, 0 elim, 86 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: 270 probed, 1 phases, 0 rounds c prbe: 36 failed, 297 lifted, 10 merged c sccs: 0 non trivial, 0 fixed, 0 merged c hash: 0 units, 76 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 0 forward, 0 backward, 106 doms c strs: 0 forward, 0 backward c doms: 242 dominators, 0 high, 0 low c prps: 5166 propagations, 0.52 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled Original parser has 166 operators. Start parsing planning graph info... Implication Set: 162/382 Total Subsumed Trans # 162 useful for saving op mutex Equivalent Set cnt: 54 out of 382 Basic reducible op analysis... Simple Reducible Trans 0 out of total 218 Simple Reducible Op 0 out of total 166 More advanced reducible op analysis... 0 Single Diff, 164 Easy, out of total 218, SinDiff Covered Actions 0/166 Reasonable Reducible covered actions %d 0 # of shared Preconditions 164 Number of Transitions: 218 Number of Transitions (with prevail ones) : 382 Number of Actions: 166 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 109 Encoding layer 1 Total Number of Trans Variables 383; Op Variables 549 reduced by 0 I.a (Trans Mutex) 383 I.b Transitions's progression 383 I.b Transitions's progression (Backward) 383 I.c Inital state 492 I.d Goal 547 II.b Trans => Opers 711 II.c Opers => Trans 1369 II.d Opers' mutex 1581 SASE Encoding finished. #Var: 577 III.b Implied Transitions 1689 ulimit -t 2400; ../precosat CNF_2896.838280 precosat.result2896.838280 Encoding layer 2 Total Number of Trans Variables 765; Op Variables 1097 reduced by 0 I.a (Trans Mutex) 766 I.b Transitions's progression 1148 I.b Transitions's progression (Backward) 1421 I.c Inital state 1530 I.d Goal 1585 II.b Trans => Opers 1913 II.c Opers => Trans 3229 II.d Opers' mutex 3653 SASE Encoding finished. #Var: 1153 III.b Implied Transitions 3869 ulimit -t 2399; ../precosat CNF_2896.878319 precosat.result2896.878319 Encoding layer 3 Total Number of Trans Variables 1147; Op Variables 1645 reduced by 0 I.a (Trans Mutex) 1149 I.b Transitions's progression 1913 I.b Transitions's progression (Backward) 2459 I.c Inital state 2568 I.d Goal 2623 II.b Trans => Opers 3115 II.c Opers => Trans 5089 II.d Opers' mutex 5725 SASE Encoding finished. #Var: 1729 III.b Implied Transitions 6049 ulimit -t 2399; ../precosat CNF_2896.941717 precosat.result2896.941717 Encoding layer 4 Total Number of Trans Variables 1529; Op Variables 2193 reduced by 0 I.a (Trans Mutex) 1532 I.b Transitions's progression 2678 I.b Transitions's progression (Backward) 3497 I.c Inital state 3606 I.d Goal 3661 II.b Trans => Opers 4317 II.c Opers => Trans 6949 II.d Opers' mutex 7797 SASE Encoding finished. #Var: 2305 III.b Implied Transitions 8229 ulimit -t 2399; ../precosat CNF_2896.29931 precosat.result2896.29931 Encoding layer 5 Total Number of Trans Variables 1911; Op Variables 2741 reduced by 0 I.a (Trans Mutex) 1915 I.b Transitions's progression 3443 I.b Transitions's progrc 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_2896.143366 c found header 'p cnf 2882 10409' 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 10409 2827 0 55 0 0 0 0.0 0 1 @c: s 0.0 0 0 2636 94 152 0 0 0.0 0 0 @c: l 0.0 0 0 2636 94 152 0 1000 0.0 0 0 @c: 1 0.0 0 0 2636 94 152 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, 20 shrunken, 0 rescored, 0 rebiased c 1 simplifications, 0 reductions c c vars: 2636 fixed, 94 equiv, 152 elim, 204 merged c elim: 16 resolutions, 1 phases, 1 rounds c sbst: 2% 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: 1001 probed, 1 phases, 2 rounds c prbe: 39 failed, 283 lifted, 80 merged c sccs: 7 non trivial, 0 fixed, 18 merged c hash: 0 units, 106 merged c mins: 0 learned, 0% deleted, 0 strong, 0 depth c subs: 20 forward, 25 backward, 141 doms c strs: 0 forward, 0 backward c doms: 341 dominators, 0 high, 0 low c prps: 10401 propagations, 1.04 megaprops c c 0.0 seconds, 1 MB max, 0 MB recycled ession (Backward) 4535 I.c Inital state 4644 I.d Goal 4699 II.b Trans => Opers 5519 II.c Opers => Trans 8809 II.d Opers' mutex 9869 SASE Encoding finished. #Var: 2881 III.b Implied Transitions 10409 ulimit -t 2399; ../precosat CNF_2896.143366 precosat.result2896.143366 Decoding for total time layer 5 [2] [10] [33] [59] [87] @Steps: 5 Time Span: 5 ; Time 0.48 0:(move r1 v34 v38) 1:(move r1 v38 v46) 2:(move r1 v46 v54) 3:(move r1 v54 v53) 4:(move r1 v53 v52) @All Time: 0.48 @SAT Time: 0.06 @Largest SAT Time: 0.02 @Last Encoding VAR: 2882 @Last Encoding CLAUSE: 10409