[1] 18903 ----- MACE 1.3, September 1996 ----- The job began on gyro.isdn.mcs.anl.gov, Wed Sep 10 17:29:26 1997 The command was "/home/mccune/bin/anldp -n10 -m1 -p -k96000". Symbol id=0, type=relation, name==, arity=2, univ/10, univ/10, props=equality, base=1. Symbol id=1, type=function, name=^, arity=3, univ/10, univ/10, univ/10, props=-----, base=101. Symbol id=2, type=function, name=v, arity=3, univ/10, univ/10, univ/10, props=-----, base=1101. Symbol id=3, type=function, name=c, arity=2, univ/10, univ/10, props=-----, base=2101. Symbol id=4, type=function, name=A, arity=1, univ/10, props=-----, base=2201. Symbol id=5, type=function, name=B, arity=1, univ/10, props=-----, base=2211. Symbol id=6, type=function, name=D1, arity=1, univ/10, props=-----, base=2221. Symbol id=7, type=function, name=D2, arity=1, univ/10, props=-----, base=2231. Symbol id=8, type=function, name=D3, arity=1, univ/10, props=-----, base=2241. Symbol id=9, type=function, name=D4, arity=1, univ/10, props=-----, base=2251. Symbol id=10, type=function, name=D5, arity=1, univ/10, props=-----, base=2261. Symbol id=11, type=function, name=D6, arity=1, univ/10, props=-----, base=2271. Symbol id=12, type=function, name=D7, arity=1, univ/10, props=-----, base=2281. Symbol id=13, type=function, name=D8, arity=1, univ/10, props=-----, base=2291. Adding units for equality relation =. Processing clause: -^(v0,v1,v2) ^(v1,v0,v2) Processing clause: -v(v0,v1,v2) v(v1,v0,v2) Processing clause: -c(v0,v1) c(v1,v0) Processing clause: -^(v0,v1,v2) v(v0,v2,v0) Processing clause: ^(v0,v0,v0) Processing clause: v(v0,v0,v0) Processing clause: -v(1,v0,v1) =(v1,1) Processing clause: -v(v0,1,v1) =(v1,1) Processing clause: ^(1,v0,v0) Processing clause: ^(v0,1,v0) Processing clause: -^(0,v0,v1) =(v1,0) Processing clause: -^(v0,0,v1) =(v1,0) Processing clause: v(0,v0,v0) Processing clause: v(v0,0,v0) function ^, arity 3, well-defined and closed. function v, arity 3, well-defined and closed. function c, arity 2, well-defined and closed. function A, arity 1, well-defined and closed. function B, arity 1, well-defined and closed. function D1, arity 1, well-defined and closed. function D2, arity 1, well-defined and closed. function D3, arity 1, well-defined and closed. function D4, arity 1, well-defined and closed. function D5, arity 1, well-defined and closed. function D6, arity 1, well-defined and closed. function D7, arity 1, well-defined and closed. function D8, arity 1, well-defined and closed. Processing clause: -^(v0,v1,v2) -^(v3,v2,v4) -^(v3,v0,v5) ^(v5,v1,v4) Processing clause: -^(v0,v1,v2) ^(v3,v2,v4) -^(v3,v0,v5) -^(v5,v1,v4) [1] Done ( sleep 3; /bin/rm $TEMP ) Processing clause: -v(v0,v1,v2) -v(v3,v2,v4) -v(v3,v0,v5) v(v5,v1,v4) Processing clause: -v(v0,v1,v2) v(v3,v2,v4) -v(v3,v0,v5) -v(v5,v1,v4) Processing clause: -c(v0,v1) -v(v0,v1,v2) -v(v3,v2,v4) =(v4,v2) Processing clause: -c(v0,v1) -c(v2,v3) -v(v3,v1,v4) -c(v4,v5) ^(v2,v0,v5) Processing clause: -c(v0,v1) -c(v2,v3) -v(v3,v1,v4) c(v4,v5) -^(v2,v0,v5) Processing clause: -c(v0,v1) -v(v1,v0,v2) =(v2,1) Processing clause: -c(v0,v1) -^(v1,v0,v2) =(v2,0) Processing clause: -D1(v0) -B(v1) -c(v1,v2) -A(v3) ^(v3,v2,v0) Processing clause: D1(v0) -B(v1) -c(v1,v2) -A(v3) -^(v3,v2,v0) Processing clause: -D2(v0) -B(v1) -c(v1,v2) -A(v3) v(v3,v2,v0) Processing clause: D2(v0) -B(v1) -c(v1,v2) -A(v3) -v(v3,v2,v0) Processing clause: -D3(v0) -B(v1) -A(v2) v(v2,v1,v0) Processing clause: D3(v0) -B(v1) -A(v2) -v(v2,v1,v0) Processing clause: -D4(v0) -A(v1) c(v1,v0) Processing clause: D4(v0) -A(v1) -c(v1,v0) Processing clause: -D5(v0) -D3(v1) -D2(v2) ^(v2,v1,v0) Processing clause: D5(v0) -D3(v1) -D2(v2) -^(v2,v1,v0) Processing clause: -D6(v0) -D5(v1) -c(v1,v2) -D4(v3) ^(v3,v2,v0) Processing clause: D6(v0) -D5(v1) -c(v1,v2) -D4(v3) -^(v3,v2,v0) Processing clause: -D7(v0) -D5(v1) -D4(v2) ^(v2,v1,v0) Processing clause: D7(v0) -D5(v1) -D4(v2) -^(v2,v1,v0) Processing clause: -D8(v0) -D6(v1) -D7(v2) v(v2,v1,v0) Processing clause: D8(v0) -D6(v1) -D7(v2) -v(v2,v1,v0) Processing clause: -D8(v0) -v(v1,v0,v2) -D4(v3) -D1(v1) -v(v1,v3,v4) -c(v4,v5) -v(v5,v2,1) 7183980 clauses were generated; 1713433 of those survived the first stage of unit preprocessing; there are 2300 atoms. After all unit preprocessing, 1164 atoms are still unassigned; 1520087 clauses remain; 130 of those are selectable; 83852 K allocated; the current user CPU time is 32.06 seconds. ======================= Model #1 at 876.37 seconds: ^ : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 9 2 | 0 2 2 0 0 2 0 7 0 7 3 | 0 3 0 3 4 0 3 0 0 4 4 | 0 4 0 4 4 0 4 0 0 4 5 | 0 5 2 0 0 5 8 7 8 7 6 | 0 6 0 3 4 8 6 0 8 4 7 | 0 7 7 0 0 7 0 7 0 7 8 | 0 8 0 0 0 8 8 0 8 0 9 | 0 9 7 4 4 7 4 7 0 9 v : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 1 2 3 4 5 6 7 8 9 1 | 1 1 1 1 1 1 1 1 1 1 2 | 2 1 2 1 1 5 1 2 5 1 3 | 3 1 1 3 3 1 6 1 6 1 4 | 4 1 1 3 4 1 6 9 6 9 5 | 5 1 5 1 1 5 1 5 5 1 6 | 6 1 1 6 6 1 6 1 6 1 7 | 7 1 2 1 9 5 1 7 5 9 8 | 8 1 5 6 6 5 6 5 8 1 9 | 9 1 1 1 9 1 1 9 1 9 c : 0 1 2 3 4 5 6 7 8 9 ----------------------- 1 0 3 2 5 4 7 6 9 8 A: 2 B: 8 D1: 7 D2: 1 D3: 5 D4: 3 D5: 5 D6: 4 D7: 0 D8: 4 end_of_model -------------- statistics ------------- Input: Clauses input 1713433 Literal occurrences input 7318386 Greatest atom 2300 Unit preprocess: Preprocess unit assignments 1136 Clauses after subsumption 1520087 Literal occ. after subsump. 6591286 Selectable clauses 130 Decide: Splits 30455 Unit assignments 1842891 Failed paths 30443 Models found 1 Memory: Memory malloced 63 K Memory tp_alloced 83789 K ----------- times (seconds) ----------- Wed Sep 10 17:44:19 1997 user CPU time 876.37 (0 hr, 14 min, 36 sec) system CPU time 1.23 (0 hr, 0 min, 1 sec) wall-clock time 893 (0 hr, 14 min, 53 sec) input time 28.15 preprocess units 3.90 decide time (incl. preprocess) 848.21 Exit due to max_models parameter. 876.3u 1.2s 14:53.53 98.2% 0+0k 0+0io 279pf+0w