% problem-set/algebra/category.theory/p2.ver1.out % created : 07/07/89 % revised : 07/07/89 --------- OTTER 1.03+, 1989 --------- Job run on Fri Jul 7 17:12:51 1989 set(sos_queue). set(ur_res). set(dynamic_demod). set(order_eq). assign(max_seconds,1800). assign(max_mem,10000). list(axioms). 1 [] -DEF(x,y) | P(x,y,star(x,y)). 2 [] -P(x,y,z) | DEF(x,y). 3 [] -P(x,y,xy) | -DEF(xy,z) | DEF(y,z). 4 [] -P(x,y,xy) | -P(y,z,yz) | -DEF(xy,z) | DEF(x,yz). 5 [] -P(x,y,xy) | -P(xy,z,xyz) | -P(y,z,yz) | P(x,yz,xyz). 6 [] -P(y,z,yz) | -DEF(x,yz) | DEF(x,y). 7 [] -P(y,z,yz) | -P(x,y,xy) | -DEF(x,yz) | DEF(xy,z). 8 [] -P(y,z,yz) | -P(x,yz,xyz) | -P(x,y,xy) | P(xy,z,xyz). 9 [] -DEF(x,y) | -DEF(y,z) | -IDENT(y) | DEF(x,z). 10 [] IDENT(dom(x)). 11 [] IDENT(cod(x)). 12 [] DEF(x,dom(x)). 13 [] DEF(cod(x),x). 14 [] P(x,dom(x),x). 15 [] P(cod(x),x,x). 16 [] -DEF(x,y) | -IDENT(x) | P(x,y,y). 17 [] -DEF(x,y) | -IDENT(y) | P(x,y,x). 18 [] EQUAL(x,x). 19 [] -EQUAL(x,y) | -P(x,z,w) | P(y,z,w). 20 [] -EQUAL(x,y) | -P(z,x,w) | P(z,y,w). 21 [] -EQUAL(x,y) | -P(z,w,x) | P(z,w,y). 22 [] -EQUAL(x,y) | EQUAL(star(z,x),star(z,y)). 23 [] -EQUAL(x,y) | EQUAL(star(x,z),star(y,z)). 24 [] -P(x,y,z) | -P(x,y,w) | EQUAL(z,w). end_of_list. list(sos). 25 [] -P(a,x,w) | -P(a,y,w) | EQUAL(x,y). 26 [] -P(b,x,w) | -P(b,y,w) | EQUAL(x,y). 27 [] P(a,b,c). 28 [] P(c,h,d). 29 [] P(c,g,d). 30 [] -EQUAL(h,g). end_of_list. weight_list(pick_and_purge). weight(dom(1),5). weight(cod(1),5). weight(x,5). weight(c,0). weight(g,0). weight(h,0). end_of_list. list(demodulators). 31 [] EQUAL(dom(dom(x)),dom(x)). 32 [] EQUAL(cod(dom(x)),dom(x)). 33 [] EQUAL(dom(cod(x)),cod(x)). 34 [] EQUAL(cod(cod(x)),cod(x)). 35 [] EQUAL(star(cod(x),x),x). 36 [] EQUAL(star(x,dom(x)),x). 37 [] EQUAL(star(cod(x),cod(x)),cod(x)). 38 [] EQUAL(star(dom(x),dom(x)),dom(x)). 39 [] EQUAL(dom(star(x,y)),dom(y)). 40 [] EQUAL(cod(star(x,y)),cod(x)). end_of_list. ----> UNIT CONFLICT at 163.73 sec ----> 492 [binary,491,431] . ---------------- PROOF ---------------- 1 [] -DEF(x,y) | P(x,y,star(x,y)). 2 [] -P(x,y,z) | DEF(x,y). 3 [] -P(x,y,xy) | -DEF(xy,z) | DEF(y,z). 5 [] -P(x,y,xy) | -P(xy,z,xyz) | -P(y,z,yz) | P(x,yz,xyz). 15 [] P(cod(x),x,x). 21 [] -EQUAL(x,y) | -P(z,w,x) | P(z,w,y). 24 [] -P(x,y,z) | -P(x,y,w) | EQUAL(z,w). 25 [] -P(a,x,w) | -P(a,y,w) | EQUAL(x,y). 26 [] -P(b,x,w) | -P(b,y,w) | EQUAL(x,y). 27 [] P(a,b,c). 28 [] P(c,h,d). 29 [] P(c,g,d). 30 [] -EQUAL(h,g). 50 [ur,28,2] DEF(c,h). 53 [ur,29,2] DEF(c,g). 54 [ur,30,24,15] -P(cod(g),g,h). 83 [ur,50,3,27] DEF(b,h). 85 [ur,50,1] P(c,h,star(c,h)). 92 [ur,53,3,27] DEF(b,g). 94 [ur,53,1] P(c,g,star(c,g)). 95 [ur,54,21,15] -EQUAL(g,h). 156 [ur,83,1] P(b,h,star(b,h)). 159 [ur,85,24,28] EQUAL(star(c,h),d). 160 [new_demod,159] EQUAL(star(c,h),d). 179 [ur,92,1] P(b,g,star(b,g)). 182 [ur,94,24,29] EQUAL(star(c,g),d). 183 [new_demod,182] EQUAL(star(c,g),d). 282 [ur,156,26,95] -P(b,g,star(b,h)). 288 [ur,156,5,27,85,demod,160] P(a,star(b,h),d). 337 [ur,179,5,27,94,demod,183] P(a,star(b,g),d). 431 [ur,282,21,179] -EQUAL(star(b,g),star(b,h)). 491 [ur,337,25,288] EQUAL(star(b,g),star(b,h)). 492 [binary,491,431] . ------------ end of proof ------------- ------------- memory usage ------------ 6 mallocs of 32700 bytes each (191.6+ K) -------------- statistics ------------- clauses input 40 clauses given 275 clauses generated 12445 demod & eval rewrites 6266 tautologies deleted 0 clauses forward subsumed 12040 (subsumed by sos) 1468 clauses kept 406 new demodulators 46 empty clauses 1 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 163.93 (run time 0 hr, 2 min, 43 sec) input time 0.57 clausify time 0.00 UR_res time 105.19 pre_process time 52.79 demod time 13.27 for_sub time 25.38 renumber time 4.10 cl integrate 0.31 print_cl time 1.27 post_process time 2.23 conflict time 1.22 back_sub time 0.42 FPA build time 0.64 IS build time 0.19 weigh cl time 0.38 window time 0.00