--------- OTTER 1.03+, 1989 --------- Job run on Fri Aug 18 12:56:44 1989 set(hyper_res). assign(max_seconds,100). 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,comp(x),1). 12 [] SUM(comp(x),x,1). 13 [] PROD(x,comp(x),0). 14 [] PROD(comp(x),x,0). 15 [] -SUM(x,y,u) | -SUM(x,y,v) | EQUAL(u,v). 16 [] -PROD(x,y,u) | -PROD(x,y,v) | EQUAL(u,v). 17 [] EQUAL(x,x). 18 [] -EQUAL(x,y) | EQUAL(y,x). 19 [] -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). 20 [] -EQUAL(x,y) | -SUM(x,v1,v2) | SUM(y,v1,v2). 21 [] -EQUAL(x,y) | -SUM(v1,x,v2) | SUM(v1,y,v2). 22 [] -EQUAL(x,y) | -SUM(v1,v2,x) | SUM(v1,v2,y). 23 [] -EQUAL(x,y) | -PROD(x,v1,v2) | PROD(y,v1,v2). 24 [] -EQUAL(x,y) | -PROD(v1,x,v2) | PROD(v1,y,v2). 25 [] -EQUAL(x,y) | -PROD(v1,v2,x) | PROD(v1,v2,y). 26 [] -EQUAL(x,y) | EQUAL(f1(x,v1),f1(y,v1)). 27 [] -EQUAL(x,y) | EQUAL(f1(v1,x),f1(v1,y)). 28 [] -EQUAL(x,y) | EQUAL(f2(x,v1),f2(y,v1)). 29 [] -EQUAL(x,y) | EQUAL(f2(v1,x),f2(v1,y)). 30 [] -EQUAL(x,y) | EQUAL(comp(x),comp(y)). end_of_list. list(sos). 31 [] SUM(x,0,x). 32 [] SUM(0,x,x). 33 [] PROD(x,1,x). 34 [] PROD(1,x,x). 35 [] SUM(x,y,f1(x,y)). 36 [] PROD(x,y,f2(x,y)). 37 [] -PROD(a,0,0). end_of_list. weight_list(pick_given). weight(f1(x,y),2). weight(f2(x,y),4). weight(x,1). end_of_list. ------------ END OF SEARCH ------------ search stopped by max_seconds option. ------------- memory usage ------------ 9 mallocs of 32700 bytes each (287.4+ K) type (bytes each) gets frees in use avail bytes -------------- statistics ------------- clauses given 19 clauses generated 5695 clauses forward subsumed 4883 clauses kept 812 clauses back subsumed 116 ----------- times (seconds) ----------- run time 118.13 (run time 0 hr, 1 min, 58 sec) hyper_res time 42.35 for_sub time 38.71 back_sub time 4.13