[1] 5515 ----- MACE 1.3, September 1996 ----- The job began on gyro.isdn.mcs.anl.gov, Thu Sep 25 15:44:16 1997 The command was "/home/mccune/bin/anldp -m1 -p -k96000 -n10". Symbol id=0, type=relation, name==, arity=2, univ/10, univ/10, props=equality, base=1. Symbol id=1, type=function, name=c, arity=2, univ/10, univ/10, props=-----, base=101. Symbol id=2, type=function, name=A, arity=1, univ/10, props=-----, base=201. Symbol id=3, type=function, name=d2, arity=1, univ/10, props=-----, base=211. Symbol id=4, type=function, name=v, arity=3, univ/10, univ/10, univ/10, props=-----, base=221. Symbol id=5, type=function, name=B, arity=1, univ/10, props=-----, base=1221. Symbol id=6, type=function, name=d3, arity=1, univ/10, props=-----, base=1231. Symbol id=7, type=function, name=^, arity=3, univ/10, univ/10, univ/10, props=-----, base=1241. Symbol id=8, type=function, name=d4, arity=1, univ/10, props=-----, base=2241. Symbol id=9, type=function, name=d5, arity=1, univ/10, props=-----, base=2251. Symbol id=10, type=function, name=d8, arity=1, univ/10, props=-----, base=2261. Symbol id=11, type=function, name=d9, arity=1, univ/10, props=-----, base=2271. Symbol id=12, type=function, name=d10, arity=1, univ/10, props=-----, base=2281. Symbol id=13, type=function, name=d11, arity=1, univ/10, props=-----, base=2291. Symbol id=14, type=function, name=d12, arity=1, univ/10, props=-----, base=2301. Symbol id=15, type=function, name=d13, arity=1, univ/10, props=-----, base=2311. Symbol id=16, type=function, name=d14, arity=1, univ/10, props=-----, base=2321. Symbol id=17, type=function, name=d16, arity=1, univ/10, props=-----, base=2331. Symbol id=18, type=function, name=d17, arity=1, univ/10, props=-----, base=2341. Symbol id=19, type=function, name=d18, arity=1, univ/10, props=-----, base=2351. Symbol id=20, type=function, name=d19, arity=1, univ/10, props=-----, base=2361. Symbol id=21, type=function, name=d20, arity=1, univ/10, props=-----, base=2371. Symbol id=22, type=function, name=d21, arity=1, univ/10, props=-----, base=2381. Symbol id=23, type=function, name=d22, arity=1, univ/10, props=-----, base=2391. Symbol id=24, type=function, name=d23, arity=1, univ/10, props=-----, base=2401. 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 c, arity 2, well-defined and closed. function A, arity 1, well-defined and closed. function d2, arity 1, well-defined and closed. function v, arity 3, well-defined and closed. function B, arity 1, well-defined and closed. function d3, arity 1, well-defined and closed. function ^, arity 3, well-defined and closed. function d4, arity 1, well-defined and closed. function d5, arity 1, well-defined and closed. function d8, arity 1, well-defined and closed. function d9, arity 1, well-defined and closed. function d10, arity 1, well-defined and closed. function d11, arity 1, well-defined and closed. function d12, arity 1, well-defined and closed. function d13, arity 1, well-defined and closed. function d14, arity 1, well-defined and closed. function d16, arity 1, well-defined and closed. function d17, arity 1, well-defined and closed. function d18, arity 1, well-defined and closed. function d19, arity 1, well-defined and closed. function d20, arity 1, well-defined and closed. function d21, arity 1, well-defined and closed. function d22, arity 1, well-defined and closed. function d23, arity 1, well-defined and closed. Processing clause: -d2(v0) -A(v1) c(v1,v0) Processing clause: d2(v0) -A(v1) -c(v1,v0) Processing clause: -d3(v0) -d2(v1) -B(v2) v(v2,v1,v0) Processing clause: d3(v0) -d2(v1) -B(v2) -v(v2,v1,v0) Processing clause: -d4(v0) -d2(v1) -B(v2) ^(v2,v1,v0) Processing clause: d4(v0) -d2(v1) -B(v2) -^(v2,v1,v0) Processing clause: -d5(v0) -d3(v1) c(v1,v0) Processing clause: d5(v0) -d3(v1) -c(v1,v0) Processing clause: -d8(v0) -B(v1) -c(v1,v2) -d2(v3) ^(v3,v2,v0) Processing clause: d8(v0) -B(v1) -c(v1,v2) -d2(v3) -^(v3,v2,v0) Processing clause: -d9(v0) -A(v1) -d3(v2) ^(v2,v1,v0) Processing clause: d9(v0) -A(v1) -d3(v2) -^(v2,v1,v0) Processing clause: -d10(v0) -d4(v1) -d8(v2) v(v2,v1,v0) Processing clause: d10(v0) -d4(v1) -d8(v2) -v(v2,v1,v0) Processing clause: -d11(v0) -d9(v1) -d10(v2) v(v2,v1,v0) Processing clause: d11(v0) -d9(v1) -d10(v2) -v(v2,v1,v0) Processing clause: -d12(v0) -d2(v1) -d11(v2) ^(v2,v1,v0) Processing clause: d12(v0) -d2(v1) -d11(v2) -^(v2,v1,v0) Processing clause: -d13(v0) -d2(v1) -d11(v2) v(v2,v1,v0) Processing clause: d13(v0) -d2(v1) -d11(v2) -v(v2,v1,v0) Processing clause: -d14(v0) -d2(v1) -d11(v2) -c(v2,v3) ^(v3,v1,v0) Processing clause: d14(v0) -d2(v1) -d11(v2) -c(v2,v3) -^(v3,v1,v0) Processing clause: -d16(v0) -A(v1) -d13(v2) ^(v2,v1,v0) Processing clause: d16(v0) -A(v1) -d13(v2) -^(v2,v1,v0) Processing clause: -d17(v0) -d12(v1) -d14(v2) v(v2,v1,v0) Processing clause: d17(v0) -d12(v1) -d14(v2) -v(v2,v1,v0) Processing clause: -d18(v0) -d16(v1) -d17(v2) v(v2,v1,v0) Processing clause: d18(v0) -d16(v1) -d17(v2) -v(v2,v1,v0) Processing clause: -d19(v0) -d18(v1) -d5(v2) ^(v2,v1,v0) Processing clause: d19(v0) -d18(v1) -d5(v2) -^(v2,v1,v0) Processing clause: -d20(v0) -d5(v1) -d18(v2) -c(v2,v3) ^(v3,v1,v0) Processing clause: d20(v0) -d5(v1) -d18(v2) -c(v2,v3) -^(v3,v1,v0) Processing clause: -d21(v0) -d5(v1) -d18(v2) v(v2,v1,v0) Processing clause: d21(v0) -d5(v1) -d18(v2) -v(v2,v1,v0) Processing clause: -d22(v0) -d3(v1) -d21(v2) ^(v2,v1,v0) Processing clause: d22(v0) -d3(v1) -d21(v2) -^(v2,v1,v0) Processing clause: -d23(v0) -d22(v1) -d19(v2) v(v2,v1,v0) Processing clause: d23(v0) -d22(v1) -d19(v2) -v(v2,v1,v0) Processing clause: -d20(v0) -d23(v1) -v(v1,v0,1) Processing clause: -v(v0,v1,v2) -v(v3,v2,v4) -v(v3,v0,v5) v(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: -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) 4104786 clauses were generated; 1411077 of those survived the first stage of unit preprocessing; there are 2410 atoms. After all unit preprocessing, 1274 atoms are still unassigned; 863465 clauses remain; 141 of those are selectable; 68327 K allocated; the current user CPU time is 19.79 seconds. ======================= Model #1 at 720.86 seconds: c : 0 1 2 3 4 5 6 7 8 9 ----------------------- 1 0 3 2 5 4 7 6 9 8 A: 2 d2: 3 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 2 1 7 1 7 3 | 3 1 1 3 4 1 3 1 1 4 4 | 4 1 1 4 4 1 4 1 1 4 5 | 5 1 2 1 1 5 8 7 8 7 6 | 6 1 1 3 4 8 6 1 8 4 7 | 7 1 7 1 1 7 1 7 1 7 8 | 8 1 1 1 1 8 8 1 8 1 9 | 9 1 7 4 4 7 4 7 1 9 B: 9 d3: 4 ^ : | 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 5 0 2 5 0 3 | 0 3 0 3 3 0 6 0 6 0 4 | 0 4 0 3 4 0 6 9 6 9 5 | 0 5 5 0 0 5 0 5 5 0 6 | 0 6 0 6 6 0 6 0 6 0 7 | 0 7 2 0 9 5 0 7 5 9 8 | 0 8 5 6 6 5 6 5 8 0 9 | 0 9 0 0 9 0 0 9 0 9 d4: 0 d5: 5 d8: 6 d9: 0 d10: 6 d11: 6 d12: 6 d13: 3 d14: 0 d16: 0 d17: 6 d18: 6 d19: 0 d20: 5 d21: 8 d22: 6 d23: 6 end_of_model -------------- statistics ------------- Input: Clauses input 1411077 Literal occurrences input 6012880 Greatest atom 2410 Unit preprocess: Preprocess unit assignments 1136 Clauses after subsumption 863465 Literal occ. after subsump. 3635306 Selectable clauses 141 Decide: Splits 30455 Unit assignments 5141760 Failed paths 30444 Models found 1 Memory: Memory malloced 66 K Memory tp_alloced 68261 K ----------- times (seconds) ----------- Thu Sep 25 15:56:18 1997 user CPU time 720.87 (0 hr, 12 min, 0 sec) system CPU time 1.14 (0 hr, 0 min, 1 sec) wall-clock time 722 (0 hr, 12 min, 2 sec) input time 16.33 preprocess units 3.46 decide time (incl. preprocess) 704.54 Exit due to max_models parameter. 720.8u 1.1s 12:02.36 99.9% 0+0k 0+0io 277pf+0w