%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NUM374+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jul 27 13:08:10 EDT 2022 % Result : Unknown 2.90s 3.15s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : NUM374+1 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.13 % Command : otter-tptp-script %s % 0.13/0.35 % Computer : n024.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Jul 27 09:37:25 EDT 2022 % 0.13/0.35 % CPUTime : % 1.66/1.85 ----- Otter 3.3f, August 2004 ----- % 1.66/1.85 The process was started by sandbox on n024.cluster.edu, % 1.66/1.85 Wed Jul 27 09:37:25 2022 % 1.66/1.85 The command was "./otter". The process ID is 3858. % 1.66/1.85 % 1.66/1.85 set(prolog_style_variables). % 1.66/1.85 set(auto). % 1.66/1.85 dependent: set(auto1). % 1.66/1.85 dependent: set(process_input). % 1.66/1.85 dependent: clear(print_kept). % 1.66/1.85 dependent: clear(print_new_demod). % 1.66/1.85 dependent: clear(print_back_demod). % 1.66/1.85 dependent: clear(print_back_sub). % 1.66/1.85 dependent: set(control_memory). % 1.66/1.85 dependent: assign(max_mem, 12000). % 1.66/1.85 dependent: assign(pick_given_ratio, 4). % 1.66/1.85 dependent: assign(stats_level, 1). % 1.66/1.85 dependent: assign(max_seconds, 10800). % 1.66/1.85 clear(print_given). % 1.66/1.85 % 1.66/1.85 formula_list(usable). % 1.66/1.85 all A (A=A). % 1.66/1.85 all X Y (sum(X,Y)=sum(Y,X)). % 1.66/1.85 all X Y Z (sum(X,sum(Y,Z))=sum(sum(X,Y),Z)). % 1.66/1.85 all X (product(X,n1)=X). % 1.66/1.85 all X Y (product(X,Y)=product(Y,X)). % 1.66/1.85 all X Y Z (product(X,product(Y,Z))=product(product(X,Y),Z)). % 1.66/1.85 all X Y Z (product(X,sum(Y,Z))=sum(product(X,Y),product(X,Z))). % 1.66/1.85 all X (exponent(n1,X)=n1). % 1.66/1.85 all X (exponent(X,n1)=X). % 1.66/1.85 all X Y Z (exponent(X,sum(Y,Z))=product(exponent(X,Y),exponent(X,Z))). % 1.66/1.85 all X Y Z (exponent(product(X,Y),Z)=product(exponent(X,Z),exponent(Y,Z))). % 1.66/1.85 all X Y Z (exponent(exponent(X,Y),Z)=exponent(X,product(Y,Z))). % 1.66/1.85 -(all C P Q R S A B (C=product(A,A)&P=sum(n1,A)&Q=sum(P,C)&R=sum(n1,product(A,C))&S=sum(sum(n1,C),product(C,C))->product(exponent(sum(exponent(P,A),exponent(Q,A)),B),exponent(sum(exponent(R,B),exponent(S,B)),A))=product(exponent(sum(exponent(P,B),exponent(Q,B)),A),exponent(sum(exponent(R,A),exponent(S,A)),B)))). % 1.66/1.85 end_of_list. % 1.66/1.85 % 1.66/1.85 -------> usable clausifies to: % 1.66/1.85 % 1.66/1.85 list(usable). % 1.66/1.85 0 [] A=A. % 1.66/1.85 0 [] sum(X,Y)=sum(Y,X). % 1.66/1.85 0 [] sum(X,sum(Y,Z))=sum(sum(X,Y),Z). % 1.66/1.85 0 [] product(X,n1)=X. % 1.66/1.85 0 [] product(X,Y)=product(Y,X). % 1.66/1.85 0 [] product(X,product(Y,Z))=product(product(X,Y),Z). % 1.66/1.85 0 [] product(X,sum(Y,Z))=sum(product(X,Y),product(X,Z)). % 1.66/1.85 0 [] exponent(n1,X)=n1. % 1.66/1.85 0 [] exponent(X,n1)=X. % 1.66/1.85 0 [] exponent(X,sum(Y,Z))=product(exponent(X,Y),exponent(X,Z)). % 1.66/1.85 0 [] exponent(product(X,Y),Z)=product(exponent(X,Z),exponent(Y,Z)). % 1.66/1.85 0 [] exponent(exponent(X,Y),Z)=exponent(X,product(Y,Z)). % 1.66/1.85 0 [] $c7=product($c2,$c2). % 1.66/1.85 0 [] $c6=sum(n1,$c2). % 1.66/1.85 0 [] $c5=sum($c6,$c7). % 1.66/1.85 0 [] $c4=sum(n1,product($c2,$c7)). % 1.66/1.85 0 [] $c3=sum(sum(n1,$c7),product($c7,$c7)). % 1.66/1.85 0 [] product(exponent(sum(exponent($c6,$c2),exponent($c5,$c2)),$c1),exponent(sum(exponent($c4,$c1),exponent($c3,$c1)),$c2))!=product(exponent(sum(exponent($c6,$c1),exponent($c5,$c1)),$c2),exponent(sum(exponent($c4,$c2),exponent($c3,$c2)),$c1)). % 1.66/1.85 end_of_list. % 1.66/1.85 % 1.66/1.85 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 1.66/1.85 % 1.66/1.85 All clauses are units, and equality is present; the % 1.66/1.85 strategy will be Knuth-Bendix with positive clauses in sos. % 1.66/1.85 % 1.66/1.85 dependent: set(knuth_bendix). % 1.66/1.85 dependent: set(anl_eq). % 1.66/1.85 dependent: set(para_from). % 1.66/1.85 dependent: set(para_into). % 1.66/1.85 dependent: clear(para_from_right). % 1.66/1.85 dependent: clear(para_into_right). % 1.66/1.85 dependent: set(para_from_vars). % 1.66/1.85 dependent: set(eq_units_both_ways). % 1.66/1.85 dependent: set(dynamic_demod_all). % 1.66/1.85 dependent: set(dynamic_demod). % 1.66/1.85 dependent: set(order_eq). % 1.66/1.85 dependent: set(back_demod). % 1.66/1.85 dependent: set(lrpo). % 1.66/1.85 % 1.66/1.85 ------------> process usable: % 1.66/1.85 ** KEPT (pick-wt=39): 1 [] product(exponent(sum(exponent($c6,$c2),exponent($c5,$c2)),$c1),exponent(sum(exponent($c4,$c1),exponent($c3,$c1)),$c2))!=product(exponent(sum(exponent($c6,$c1),exponent($c5,$c1)),$c2),exponent(sum(exponent($c4,$c2),exponent($c3,$c2)),$c1)). % 1.66/1.85 % 1.66/1.85 ------------> process sos: % 1.66/1.85 ** KEPT (pick-wt=3): 2 [] A=A. % 1.66/1.85 ** KEPT (pick-wt=7): 3 [] sum(A,B)=sum(B,A). % 1.66/1.85 ** KEPT (pick-wt=11): 5 [copy,4,flip.1] sum(sum(A,B),C)=sum(A,sum(B,C)). % 1.66/1.85 ---> New Demodulator: 6 [new_demod,5] sum(sum(A,B),C)=sum(A,sum(B,C)). % 1.66/1.85 ** KEPT (pick-wt=5): 7 [] product(A,n1)=A. % 1.66/1.85 ---> New Demodulator: 8 [new_demod,7] product(A,n1)=A. % 1.66/1.85 ** KEPT (pick-wt=7): 9 [] product(A,B)=product(B,A). % 1.66/1.85 ** KEPT (pick-wt=11): 11 [copy,10,flip.1] product(product(A,B),C)=product(A,product(B,C)). % 1.66/1.85 ---> New Demodulator: 12 [new_demod,11] product(product(A,B),C)=product(A,product(B,C)). % 1.66/1.85 ** KEPT (pick-wt=13): 14 [copy,13,flip.1] sum(product(A,B),product(A,C))=product(A,sum(B,C)). % 1.66/1.85 ---> New Demodulator: 15 [new_demod,14] sum(product(A,B),product(A,C))=product(A,sum(B,C)). % 2.90/3.15 ** KEPT (pick-wt=5): 16 [] exponent(n1,A)=n1. % 2.90/3.15 ---> New Demodulator: 17 [new_demod,16] exponent(n1,A)=n1. % 2.90/3.15 ** KEPT (pick-wt=5): 18 [] exponent(A,n1)=A. % 2.90/3.15 ---> New Demodulator: 19 [new_demod,18] exponent(A,n1)=A. % 2.90/3.15 ** KEPT (pick-wt=13): 20 [] exponent(A,sum(B,C))=product(exponent(A,B),exponent(A,C)). % 2.90/3.15 ** KEPT (pick-wt=13): 22 [copy,21,flip.1] product(exponent(A,B),exponent(C,B))=exponent(product(A,C),B). % 2.90/3.15 ---> New Demodulator: 23 [new_demod,22] product(exponent(A,B),exponent(C,B))=exponent(product(A,C),B). % 2.90/3.15 ** KEPT (pick-wt=11): 24 [] exponent(exponent(A,B),C)=exponent(A,product(B,C)). % 2.90/3.15 ** KEPT (pick-wt=5): 26 [copy,25,flip.1] product($c2,$c2)=$c7. % 2.90/3.15 ---> New Demodulator: 27 [new_demod,26] product($c2,$c2)=$c7. % 2.90/3.15 ** KEPT (pick-wt=5): 29 [copy,28,flip.1] sum(n1,$c2)=$c6. % 2.90/3.15 ---> New Demodulator: 30 [new_demod,29] sum(n1,$c2)=$c6. % 2.90/3.15 ** KEPT (pick-wt=5): 32 [copy,31,flip.1] sum($c6,$c7)=$c5. % 2.90/3.15 ---> New Demodulator: 33 [new_demod,32] sum($c6,$c7)=$c5. % 2.90/3.15 ** KEPT (pick-wt=7): 35 [copy,34,flip.1] sum(n1,product($c2,$c7))=$c4. % 2.90/3.15 ---> New Demodulator: 36 [new_demod,35] sum(n1,product($c2,$c7))=$c4. % 2.90/3.15 ** KEPT (pick-wt=9): 38 [copy,37,demod,6,flip.1] sum(n1,sum($c7,product($c7,$c7)))=$c3. % 2.90/3.15 ---> New Demodulator: 39 [new_demod,38] sum(n1,sum($c7,product($c7,$c7)))=$c3. % 2.90/3.15 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A. % 2.90/3.15 Following clause subsumed by 3 during input processing: 0 [copy,3,flip.1] sum(A,B)=sum(B,A). % 2.90/3.15 >>>> Starting back demodulation with 6. % 2.90/3.15 >>>> Starting back demodulation with 8. % 2.90/3.15 Following clause subsumed by 9 during input processing: 0 [copy,9,flip.1] product(A,B)=product(B,A). % 2.90/3.15 >>>> Starting back demodulation with 12. % 2.90/3.15 >>>> Starting back demodulation with 15. % 2.90/3.15 >>>> Starting back demodulation with 17. % 2.90/3.15 >>>> Starting back demodulation with 19. % 2.90/3.15 ** KEPT (pick-wt=13): 40 [copy,20,flip.1] product(exponent(A,B),exponent(A,C))=exponent(A,sum(B,C)). % 2.90/3.15 >>>> Starting back demodulation with 23. % 2.90/3.15 ** KEPT (pick-wt=11): 41 [copy,24,flip.1] exponent(A,product(B,C))=exponent(exponent(A,B),C). % 2.90/3.15 >>>> Starting back demodulation with 27. % 2.90/3.15 >>>> Starting back demodulation with 30. % 2.90/3.15 >>>> Starting back demodulation with 33. % 2.90/3.15 >>>> Starting back demodulation with 36. % 2.90/3.15 >>>> Starting back demodulation with 39. % 2.90/3.15 Following clause subsumed by 20 during input processing: 0 [copy,40,flip.1] exponent(A,sum(B,C))=product(exponent(A,B),exponent(A,C)). % 2.90/3.15 Following clause subsumed by 24 during input processing: 0 [copy,41,flip.1] exponent(exponent(A,B),C)=exponent(A,product(B,C)). % 2.90/3.15 % 2.90/3.15 ======= end of input processing ======= % 2.90/3.15 % 2.90/3.15 =========== start of search =========== % 2.90/3.15 % 2.90/3.15 % 2.90/3.15 Resetting weight limit to 11. % 2.90/3.15 % 2.90/3.15 % 2.90/3.15 Resetting weight limit to 11. % 2.90/3.15 % 2.90/3.15 sos_size=589 % 2.90/3.15 % 2.90/3.15 Search stopped because sos empty. % 2.90/3.15 % 2.90/3.15 % 2.90/3.15 Search stopped because sos empty. % 2.90/3.15 % 2.90/3.15 ============ end of search ============ % 2.90/3.15 % 2.90/3.15 -------------- statistics ------------- % 2.90/3.15 clauses given 821 % 2.90/3.15 clauses generated 233275 % 2.90/3.15 clauses kept 937 % 2.90/3.15 clauses forward subsumed 18074 % 2.90/3.15 clauses back subsumed 62 % 2.90/3.15 Kbytes malloced 7812 % 2.90/3.15 % 2.90/3.15 ----------- times (seconds) ----------- % 2.90/3.15 user CPU time 1.29 (0 hr, 0 min, 1 sec) % 2.90/3.15 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.90/3.15 wall-clock time 3 (0 hr, 0 min, 3 sec) % 2.90/3.15 % 2.90/3.15 Process 3858 finished Wed Jul 27 09:37:28 2022 % 2.90/3.15 Otter interrupted % 2.90/3.15 PROOF NOT FOUND %------------------------------------------------------------------------------