--------- OTTER 1.03+, 1989 --------- Job run on Tue Aug 8 09:48:51 1989 set(print_weight). set(hyper_res). assign(max_seconds,200). list(axioms). 1 [] -SUM(x,y,v3) | SUM(y,x,v3). 2 [] -PROD(x,y,v3) | PROD(y,x,v3). 3 [] -PROD(x,y,v1) | -PROD(x,z,v2) | -SUM(y,z,v3) | -PROD(x,v3,v4) | SUM(v1,v2,v4). 4 [] -PROD(x,y,v1) | -PROD(x,z,v2) | -SUM(y,z,v3) | -SUM(v1,v2,v4) | PROD(x,v3,v4). 5 [] -PROD(y,x,v1) | -PROD(z,x,v2) | -SUM(y,z,v3) | -PROD(v3,x,v4) | SUM(v1,v2,v4). 6 [] -PROD(y,x,v1) | -PROD(z,x,v2) | -SUM(y,z,v3) | -SUM(v1,v2,v4) | PROD(v3,x,v4). 7 [] -SUM(x,y,v1) | -SUM(x,z,v2) | -PROD(y,z,v3) | -SUM(x,v3,v4) | PROD(v1,v2,v4). 8 [] -SUM(x,y,v1) | -SUM(x,z,v2) | -PROD(y,z,v3) | -PROD(v1,v2,v4) | SUM(x,v3,v4). 9 [] -SUM(y,x,v1) | -SUM(z,x,v2) | -PROD(y,z,v3) | -SUM(v3,x,v4) | PROD(v1,v2,v4). 10 [] -SUM(y,x,v1) | -SUM(z,x,v2) | -PROD(y,z,v3) | -PROD(v1,v2,v4) | SUM(v3,x,v4). 11 [] -SUM(x,y,u) | -SUM(x,y,v) | EQUAL(u,v). 12 [] -PROD(x,y,u) | -PROD(x,y,v) | EQUAL(u,v). 13 [] EQUAL(x,x). 14 [] -EQUAL(x,y) | EQUAL(y,x). 15 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 16 [] -EQUAL(x,y) | -SUM(x,v1,v2) | SUM(y,v1,v2). 17 [] -EQUAL(x,y) | -SUM(v1,x,v2) | SUM(v1,y,v2). 18 [] -EQUAL(x,y) | -SUM(v1,v2,x) | SUM(v1,v2,y). 19 [] -EQUAL(x,y) | -PROD(x,v1,v2) | PROD(y,v1,v2). 20 [] -EQUAL(x,y) | -PROD(v1,x,v2) | PROD(v1,y,v2). 21 [] -EQUAL(x,y) | -PROD(v1,v2,x) | PROD(v1,v2,y). 22 [] -EQUAL(x,y) | EQUAL(f1(x,v1),f1(y,v1)). 23 [] -EQUAL(x,y) | EQUAL(f1(v1,x),f1(v1,y)). 24 [] -EQUAL(x,y) | EQUAL(f2(x,v1),f2(y,v1)). 25 [] -EQUAL(x,y) | EQUAL(f2(v1,x),f2(v1,y)). 26 [] -EQUAL(x,y) | EQUAL(comp(x),comp(y)). end_of_list. list(sos). 27 [] SUM(x,y,f1(x,y)). 28 [] PROD(x,y,f2(x,y)). 29 [] SUM(x,comp(x),1). 30 [] SUM(comp(x),x,1). 31 [] PROD(x,comp(x),0). 32 [] PROD(comp(x),x,0). 33 [] SUM(x,0,x). 34 [] SUM(0,x,x). 35 [] PROD(x,1,x). 36 [] PROD(1,x,x). 37 [] -PROD(a,a,a). end_of_list. weight_list(pick_given). weight(f1(x,y),4). weight(f2(x,y),2). weight(x,1). end_of_list. ----> UNIT CONFLICT at 73.25 sec ----> 1340 [binary,1325,37] . ---------------- PROOF ---------------- 2 [] -PROD(x,y,v3) | PROD(y,x,v3). 4 [] -PROD(x,y,v1) | -PROD(x,z,v2) | -SUM(y,z,v3) | -SUM(v1,v2,v4) | PROD(x,v3,v4). 12 [] -PROD(x,y,u) | -PROD(x,y,v) | EQUAL(u,v). 21 [] -EQUAL(x,y) | -PROD(v1,v2,x) | PROD(v1,v2,y). 28 [] PROD(x,y,f2(x,y)). 29 [] SUM(x,comp(x),1). 31 [] PROD(x,comp(x),0). 33 [] SUM(x,0,x). 35 [] PROD(x,1,x). 37 [] -PROD(a,a,a). 88 [hyper,28,2] PROD(x,y,f2(y,x)). 260 [hyper,31,4,28,29,33] PROD(x,1,f2(x,x)). 948 [hyper,260,12,35] EQUAL(f2(x,x),x). 1325 [hyper,948,21,88] PROD(x,x,x). 1340 [binary,1325,37] . ------------ end of proof ------------- ------------- memory usage ------------ 14 mallocs of 32700 bytes each (447.1+ K) type (bytes each) gets frees in use avail bytes -------------- statistics ------------- clauses input 37 clauses given 28 clauses generated 7762 demod & eval rewrites 0 tautologies deleted 0 clauses forward subsumed 6460 (subsumed by sos) 4760 clauses kept 1303 empty clauses 1 clauses back subsumed 97 clauses not processed 21 ----------- times (seconds) ----------- run time 73.41 (run time 0 hr, 1 min, 13 sec) input time 0.71 clausify time 0.00 hyper_res time 22.21 pre_process time 35.84 demod time 0.00 lex_rpo time 0.00 for_sub time 21.09 renumber time 0.54 cl integrate 1.30 print_cl time 5.75 post_process time 13.08 conflict time 5.15 back_sub time 5.16 FPA build time 1.64 IS build time 0.89 weigh cl time 1.41 window time 0.00