----- Otter 3.0.3d, Feb 1995 ----- The job was started by mccune on gyro, Tue Feb 28 14:53:38 1995 The command was "otter3". op(400,xfx,^). op(400,xfx,v). set(knuth_bendix). dependent: set(para_from). dependent: set(para_into). dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). dependent: set(order_eq). dependent: set(back_demod). dependent: set(process_input). dependent: set(lrpo). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(pick_given_ratio,4). assign(max_weight,15). assign(max_mem,12000). set(output_sequent). set(hyper_res). set(order_history). set(para_from_units_only). set(para_into_units_only). list(usable). 0 [] -> x=x. end_of_list. list(sos). 0 [] -> (x^y) v (x^ (x v y))=x. 0 [] -> (x^x) v (y^ (x v x))=x. 0 [] -> (x^y) v (y^ (x v y))=y. end_of_list. list(usable). 0 [] A^A=A, A^B=B^A, A v A=A, A v B=B v A -> . end_of_list. list(sos). 0 [] -> ((x v y)^ (z v x))^x=x. 0 [] -> ((x^y) v (z^x)) v x=x. end_of_list. weight_list(pick_and_purge). weight(A,-1). weight(B,-1). weight(C,-1). end_of_list. ------------> process usable: ** KEPT (wt=3): 1 [] -> x=x. ** KEPT (wt=-4): 3 [copy,2,flip.2,flip.4] A^A=A, B^A=A^B, A v A=A, B v A=A v B -> . Following clause subsumed by 1 during input processing: 0 [copy,1,flip.1] -> x=x. ------------> process sos: ** KEPT (wt=11): 4 [] -> (x^y) v (x^ (x v y))=x. ---> New Demodulator: 5 [new_demod,4] -> (x^y) v (x^ (x v y))=x. ** KEPT (wt=11): 6 [] -> (x^x) v (y^ (x v x))=x. ---> New Demodulator: 7 [new_demod,6] -> (x^x) v (y^ (x v x))=x. ** KEPT (wt=11): 8 [] -> (x^y) v (y^ (x v y))=y. ---> New Demodulator: 9 [new_demod,8] -> (x^y) v (y^ (x v y))=y. ** KEPT (wt=11): 10 [] -> ((x v y)^ (z v x))^x=x. ---> New Demodulator: 11 [new_demod,10] -> ((x v y)^ (z v x))^x=x. ** KEPT (wt=11): 12 [] -> ((x^y) v (z^x)) v x=x. ---> New Demodulator: 13 [new_demod,12] -> ((x^y) v (z^x)) v x=x. >>>> Starting back demodulation with 5. >>>> Starting back demodulation with 7. >>>> Starting back demodulation with 9. >>>> Starting back demodulation with 11. >>>> Starting back demodulation with 13. ======= end of input processing ======= =========== start of search =========== given clause #1: (wt=11) 4 [] -> (x^y) v (x^ (x v y))=x. given clause #2: (wt=11) 6 [] -> (x^x) v (y^ (x v x))=x. given clause #3: (wt=11) 8 [] -> (x^y) v (y^ (x v y))=y. given clause #4: (wt=11) 10 [] -> ((x v y)^ (z v x))^x=x. given clause #5: (wt=9) 18 [para_from,10.1.1,6.1.1.2] -> (x^x) v (x v x)=x. given clause #6: (wt=11) 12 [] -> ((x^y) v (z^x)) v x=x. given clause #7: (wt=9) 24 [para_into,12.1.1.1.2,10.1.1] -> ((x^y) v x) v x=x. given clause #8: (wt=9) 26 [para_from,12.1.1,10.1.1.1.2] -> ((x v y)^x)^x=x. given clause #9: (wt=13) 30 [para_from,24.1.1,8.1.1.2.2] -> (((x^y) v x)^x) v (x^x)=x. given clause #10: (wt=13) 34 [para_into,26.1.1.1.1,8.1.1] -> (x^ (y^x))^ (y^x)=y^x. given clause #11: (wt=15) 14 [para_into,10.1.1.1.1,8.1.1] -> (x^ (y v (z^x)))^ (z^x)=z^x. given clause #12: (wt=7) 44 [para_into,34.1.1.1.2,26.1.1,demod,27,27] -> (x^x)^x=x. given clause #13: (wt=9) 46 [para_into,14.1.1.1.2.2,26.1.1,demod,27,27] -> (x^ (y v x))^x=x. given clause #14: (wt=9) 58 [para_into,46.1.1.1.2,30.1.1,demod,45] -> x^ (x^x)=x^x. given clause #15: (wt=11) 48 [para_into,14.1.1.1.2,30.1.1] -> (x^x)^ (x^x)=x^x. given clause #16: (wt=15) 16 [para_into,10.1.1.1.1,4.1.1] -> (x^ (y v (x^z)))^ (x^z)=x^z. given clause #17: (wt=11) 54 [para_from,44.1.1,8.1.1.1] -> x v (x^ ((x^x) v x))=x. given clause #18: (wt=11) 74 [para_into,16.1.1.1.2.2,44.1.1,demod,45,45] -> ((x^x)^ (y v x))^x=x. given clause #19: (wt=-4) 108 [back_demod,3,demod,89] A=A, B^A=A^B, A v A=A, B v A=A v B -> . given clause #20: (wt=5) 88 [para_into,74.1.1.1.2,24.1.1,demod,45] -> x^x=x. given clause #21: (wt=15) 20 [para_from,10.1.1,8.1.1.1] -> x v (x^ (((x v y)^ (z v x)) v x))=x. given clause #22: (wt=-3) 115 [back_demod,108,demod,114] A=A, B^A=A^B, B v A=A v B -> . given clause #23: (wt=5) 113 [para_into,20.1.1.2.2.1,88.1.1,demod,95,89] -> x v x=x. given clause #24: (wt=7) 116 [back_demod,106,demod,114] -> x v (y^x)=x. given clause #25: (wt=7) 128 [para_from,116.1.1,4.1.1.2.2,demod,123,89] -> (x^y) v y=y. given clause #26: (wt=13) 64 [para_from,46.1.1,8.1.1.1] -> x v (x^ ((x^ (y v x)) v x))=x. given clause #27: (wt=7) 134 [back_demod,26,demod,131] -> (x v y)^x=x. given clause #28: (wt=9) 122 [para_from,116.1.1,14.1.1.1.2,demod,89] -> x^ (y^x)=y^x. given clause #29: (wt=9) 130 [para_from,128.1.1,4.1.1.2.2,demod,114] -> (x^y)^y=x^y. given clause #30: (wt=9) 132 [back_demod,36,demod,131] -> x^ (x^y)=x^y. given clause #31: (wt=13) 72 [para_into,16.1.1.1.2.2,46.1.1,demod,47,47] -> ((x^ (y v x))^ (z v x))^x=x. given clause #32: (wt=11) 142 [back_demod,64,demod,141] -> x v ((x^ (y v x)) v x)=x. given clause #33: (wt=11) 148 [para_from,134.1.1,8.1.1.1] -> x v (x^ ((x v y) v x))=x. given clause #34: (wt=11) 152 [para_from,122.1.1,12.1.1.1.1] -> ((x^y) v (z^y)) v y=y. given clause #35: (wt=11) 156 [para_from,148.1.1,4.1.1.2.2,demod,133,89] -> (x^ ((x v y) v x)) v x=x. given clause #36: (wt=15) 78 [para_into,16.1.1.1.2.2,10.1.1,demod,11,11] -> (((x v y)^ (z v x))^ (u v x))^x=x. given clause #37: (wt=9) 158 [para_into,156.1.1.1.2.1,156.1.1,demod,149,47,149,flip.1] -> x^ ((x v y) v x)=x. given clause #38: (wt=9) 162 [para_from,158.1.1,122.1.1.2,demod,159] -> ((x v y) v x)^x=x. given clause #39: (wt=13) 136 [para_into,64.1.1.2.2.1.2,20.1.1,demod,47,21,47,119,flip.1] -> x^ (((x v y)^ (z v x)) v x)=x. given clause #40: (wt=9) 172 [para_into,136.1.1.2.1.1,142.1.1,demod,141] -> (x^ (y v x)) v x=x. given clause #41: (wt=15) 124 [para_from,116.1.1,10.1.1.1.2] -> (((x^y) v z)^y)^ (x^y)=x^y. given clause #42: (wt=7) 178 [para_from,172.1.1,4.1.1.2.2,demod,47,47,114,flip.1] -> x^ (y v x)=x. given clause #43: (wt=7) 180 [back_demod,140,demod,179,flip.1] -> (x^y) v x=x. given clause #44: (wt=7) 186 [para_from,178.1.1,122.1.1.2,demod,179] -> (x v y)^y=y. given clause #45: (wt=9) 188 [para_from,178.1.1,116.1.1.2] -> (x v y) v y=x v y. given clause #46: (wt=15) 146 [para_from,134.1.1,12.1.1.1.1] -> (x v (y^ (x v z))) v (x v z)=x v z. given clause #47: (wt=9) 196 [para_from,178.1.1,128.1.1.1] -> x v (y v x)=y v x. given clause #48: (wt=9) 198 [back_demod,144,demod,189] -> x v (x v y)=x v y. given clause #49: (wt=7) 212 [para_from,198.1.1,4.1.1.2.2,demod,114] -> x^ (x v y)=x. given clause #50: (wt=9) 200 [para_from,180.1.1,4.1.1.2.2,demod,114] -> (x^y)^x=x^y. given clause #51: (wt=15) 184 [para_from,178.1.1,152.1.1.1.2] -> ((x^ (y v z)) v z) v (y v z)=y v z. given clause #52: (wt=7) 236 [para_from,200.1.1,116.1.1.2] -> x v (x^y)=x. given clause #53: (wt=9) 216 [para_from,212.1.1,116.1.1.2] -> (x v y) v x=x v y. given clause #54: (wt=11) 190 [para_from,178.1.1,14.1.1.2,demod,179,179] -> ((x v y)^ (z v y))^y=y. given clause #55: (wt=11) 220 [para_from,212.1.1,124.1.1.2,demod,213,213] -> ((x v y)^ (x v z))^x=x. given clause #56: (wt=15) 192 [para_from,178.1.1,12.1.1.1.2] -> (((x v y)^z) v y) v (x v y)=x v y. given clause #57: (wt=11) 230 [para_into,200.1.1.1,10.1.1,demod,11] -> x^ ((x v y)^ (z v x))=x. given clause #58: (wt=11) 232 [para_from,200.1.1,152.1.1.1.2] -> ((x^y) v (y^z)) v y=y. given clause #59: (wt=11) 238 [para_from,200.1.1,12.1.1.1.2] -> ((x^y) v (x^z)) v x=x. given clause #60: (wt=11) 242 [para_from,236.1.1,14.1.1.1.2] -> (x^y)^ (y^x)=y^x. given clause #61: (wt=15) 194 [para_from,178.1.1,152.1.1.1.1] -> (x v (y^ (z v x))) v (z v x)=z v x. given clause #62: (wt=7) 286 [para_from,242.1.1,200.1.1.1,demod,243,243] -> x^y=y^x. given clause #63: (wt=11) 246 [para_into,216.1.1.1,152.1.1,demod,153] -> x v ((y^x) v (z^x))=x. given clause #64: (wt=11) 250 [para_into,216.1.1.1,12.1.1,demod,13] -> x v ((x^y) v (z^x))=x. given clause #65: (wt=11) 262 [para_into,190.1.1.1.2,216.1.1] -> ((x v y)^ (y v z))^y=y. given clause #66: (wt=15) 204 [para_into,146.1.1.1.2.2,152.1.1,demod,153,153] -> (((x^y) v (z^y)) v (u^y)) v y=y. given clause #67: (wt=11) 264 [para_from,190.1.1,200.1.1.1,demod,191] -> x^ ((y v x)^ (z v x))=x. given clause #68: (wt=11) 266 [para_from,220.1.1,200.1.1.1,demod,221] -> x^ ((x v y)^ (x v z))=x. given clause #69: (wt=11) 278 [para_from,232.1.1,216.1.1.1,demod,233] -> x v ((y^x) v (x^z))=x. given clause #70: (wt=11) 282 [para_from,238.1.1,216.1.1.1,demod,239] -> x v ((x^y) v (x^z))=x. given clause #71: (wt=15) 206 [para_into,146.1.1.1.2.2,12.1.1,demod,13,13] -> (((x^y) v (z^x)) v (u^x)) v x=x. given clause #72: (wt=11) 284 [para_from,242.1.1,236.1.1.2] -> (x^y) v (y^x)=x^y. given clause #73: (wt=11) 287 [para_into,194.1.1.1.2,212.1.1] -> (x v y) v (y v x)=y v x. given clause #74: (wt=7) 349 [para_from,287.1.1,216.1.1.1,demod,288,288] -> x v y=y v x. -----> EMPTY CLAUSE at 2.51 sec ----> 352 [hyper,115,1,286,349] -> . Length of proof is 46. Level of proof is 21. ---------------- PROOF ---------------- 1 [] -> x=x. 2 [] A^A=A, A^B=B^A, A v A=A, A v B=B v A -> . 3 [copy,2,flip.2,flip.4] A^A=A, B^A=A^B, A v A=A, B v A=A v B -> . 4 [] -> (x^y) v (x^ (x v y))=x. 6 [] -> (x^x) v (y^ (x v x))=x. 8 [] -> (x^y) v (y^ (x v y))=y. 10 [] -> ((x v y)^ (z v x))^x=x. 12 [] -> ((x^y) v (z^x)) v x=x. 14 [para_into,10.1.1.1.1,8.1.1] -> (x^ (y v (z^x)))^ (z^x)=z^x. 16 [para_into,10.1.1.1.1,4.1.1] -> (x^ (y v (x^z)))^ (x^z)=x^z. 21,20 [para_from,10.1.1,8.1.1.1] -> x v (x^ (((x v y)^ (z v x)) v x))=x. 24 [para_into,12.1.1.1.2,10.1.1] -> ((x^y) v x) v x=x. 27,26 [para_from,12.1.1,10.1.1.1.2] -> ((x v y)^x)^x=x. 30 [para_from,24.1.1,8.1.1.2.2] -> (((x^y) v x)^x) v (x^x)=x. 34 [para_into,26.1.1.1.1,8.1.1] -> (x^ (y^x))^ (y^x)=y^x. 45,44 [para_into,34.1.1.1.2,26.1.1,demod,27,27] -> (x^x)^x=x. 47,46 [para_into,14.1.1.1.2.2,26.1.1,demod,27,27] -> (x^ (y v x))^x=x. 48 [para_into,14.1.1.1.2,30.1.1] -> (x^x)^ (x^x)=x^x. 63,62 [para_into,46.1.1.1.2,8.1.1,demod,47] -> x^ (x^ (y v x))=x^ (y v x). 64 [para_from,46.1.1,8.1.1.1] -> x v (x^ ((x^ (y v x)) v x))=x. 70 [para_from,48.1.1,24.1.1.1.1] -> ((x^x) v (x^x)) v (x^x)=x^x. 74 [para_into,16.1.1.1.2.2,44.1.1,demod,45,45] -> ((x^x)^ (y v x))^x=x. 89,88 [para_into,74.1.1.1.2,24.1.1,demod,45] -> x^x=x. 95,94 [back_demod,70,demod,89,89,89,89] -> (x v x) v x=x. 106 [back_demod,6,demod,89] -> x v (y^ (x v x))=x. 108 [back_demod,3,demod,89] A=A, B^A=A^B, A v A=A, B v A=A v B -> . 114,113 [para_into,20.1.1.2.2.1,88.1.1,demod,95,89] -> x v x=x. 115 [back_demod,108,demod,114] A=A, B^A=A^B, B v A=A v B -> . 116 [back_demod,106,demod,114] -> x v (y^x)=x. 119,118 [para_from,20.1.1,4.1.1.2.2,demod,63,89] -> (x^ (((x v y)^ (z v x)) v x)) v x=x. 123,122 [para_from,116.1.1,14.1.1.1.2,demod,89] -> x^ (y^x)=y^x. 128 [para_from,116.1.1,4.1.1.2.2,demod,123,89] -> (x^y) v y=y. 131,130 [para_from,128.1.1,4.1.1.2.2,demod,114] -> (x^y)^y=x^y. 134 [back_demod,26,demod,131] -> (x v y)^x=x. 136 [para_into,64.1.1.2.2.1.2,20.1.1,demod,47,21,47,119,flip.1] -> x^ (((x v y)^ (z v x)) v x)=x. 141,140 [para_into,134.1.1.1,24.1.1] -> x^ ((x^y) v x)= (x^y) v x. 142 [back_demod,64,demod,141] -> x v ((x^ (y v x)) v x)=x. 144 [para_from,134.1.1,24.1.1.1.1] -> (x v (x v y)) v (x v y)=x v y. 152 [para_from,122.1.1,12.1.1.1.1] -> ((x^y) v (z^y)) v y=y. 172 [para_into,136.1.1.2.1.1,142.1.1,demod,141] -> (x^ (y v x)) v x=x. 179,178 [para_from,172.1.1,4.1.1.2.2,demod,47,47,114,flip.1] -> x^ (y v x)=x. 180 [back_demod,140,demod,179,flip.1] -> (x^y) v x=x. 189,188 [para_from,178.1.1,116.1.1.2] -> (x v y) v y=x v y. 194 [para_from,178.1.1,152.1.1.1.1] -> (x v (y^ (z v x))) v (z v x)=z v x. 198 [back_demod,144,demod,189] -> x v (x v y)=x v y. 200 [para_from,180.1.1,4.1.1.2.2,demod,114] -> (x^y)^x=x^y. 212 [para_from,198.1.1,4.1.1.2.2,demod,114] -> x^ (x v y)=x. 216 [para_from,212.1.1,116.1.1.2] -> (x v y) v x=x v y. 236 [para_from,200.1.1,116.1.1.2] -> x v (x^y)=x. 243,242 [para_from,236.1.1,14.1.1.1.2] -> (x^y)^ (y^x)=y^x. 286 [para_from,242.1.1,200.1.1.1,demod,243,243] -> x^y=y^x. 288,287 [para_into,194.1.1.1.2,212.1.1] -> (x v y) v (y v x)=y v x. 349 [para_from,287.1.1,216.1.1.1,demod,288,288] -> x v y=y v x. 352 [hyper,115,1,286,349] -> . ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 74 clauses generated 2734 hyper_res generated 1 para_from generated 1304 para_into generated 1429 demod & eval rewrites 4363 clauses wt,lit,sk delete 525 tautologies deleted 0 clauses forward subsumed 2114 (subsumed by sos) 4 unit deletions 0 factor simplifications 0 clauses kept 178 new demodulators 172 empty clauses 1 clauses back demodulated 74 clauses back subsumed 0 usable size 50 sos size 54 demodulators size 100 passive size 0 hot size 0 Kbytes malloced 319 ----------- times (seconds) ----------- user CPU time 2.53 (0 hr, 0 min, 2 sec) system CPU time 0.89 (0 hr, 0 min, 0 sec) wall-clock time 4 (0 hr, 0 min, 4 sec) input time 0.05 clausify time 0.00 process input 0.02 hyper_res time 0.01 para_into time 0.30 para_from time 0.30 pre_process time 1.65 renumber time 0.13 demod time 0.74 order equalities 0.11 unit deleletion 0.00 factor simplify 0.00 weigh cl time 0.11 sort lits time 0.00 forward subsume 0.18 delete cl time 0.14 keep cl time 0.07 print_cl time 0.01 conflict time 0.02 new demod time 0.06 post_process time 0.10 back demod time 0.07 back subsume 0.03 factor time 0.00 unindex time 0.02 The job finished Tue Feb 28 14:53:42 1995