%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : NUM374+2 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n004.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.35s 2.56s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : NUM374+2 : TPTP v8.1.0. Released v3.2.0. % 0.09/0.13 % Command : otter-tptp-script %s % 0.14/0.34 % Computer : n004.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Jul 27 09:38:06 EDT 2022 % 0.14/0.35 % CPUTime : % 1.83/2.03 ----- Otter 3.3f, August 2004 ----- % 1.83/2.03 The process was started by sandbox2 on n004.cluster.edu, % 1.83/2.03 Wed Jul 27 09:38:06 2022 % 1.83/2.03 The command was "./otter". The process ID is 2420. % 1.83/2.03 % 1.83/2.03 set(prolog_style_variables). % 1.83/2.03 set(auto). % 1.83/2.03 dependent: set(auto1). % 1.83/2.03 dependent: set(process_input). % 1.83/2.03 dependent: clear(print_kept). % 1.83/2.03 dependent: clear(print_new_demod). % 1.83/2.03 dependent: clear(print_back_demod). % 1.83/2.03 dependent: clear(print_back_sub). % 1.83/2.03 dependent: set(control_memory). % 1.83/2.03 dependent: assign(max_mem, 12000). % 1.83/2.03 dependent: assign(pick_given_ratio, 4). % 1.83/2.03 dependent: assign(stats_level, 1). % 1.83/2.03 dependent: assign(max_seconds, 10800). % 1.83/2.03 clear(print_given). % 1.83/2.03 % 1.83/2.03 formula_list(usable). % 1.83/2.03 all A (A=A). % 1.83/2.03 all X Y (sum(X,Y)=sum(Y,X)). % 1.83/2.03 all X Y Z (sum(X,sum(Y,Z))=sum(sum(X,Y),Z)). % 1.83/2.03 all X (product(X,n1)=X). % 1.83/2.03 all X Y (product(X,Y)=product(Y,X)). % 1.83/2.03 all X Y Z (product(X,product(Y,Z))=product(product(X,Y),Z)). % 1.83/2.03 all X Y Z (product(X,sum(Y,Z))=sum(product(X,Y),product(X,Z))). % 1.83/2.03 all X (exponent(n1,X)=n1). % 1.83/2.03 all X (exponent(X,n1)=X). % 1.83/2.03 all X Y Z (exponent(X,sum(Y,Z))=product(exponent(X,Y),exponent(X,Z))). % 1.83/2.03 all X Y Z (exponent(product(X,Y),Z)=product(exponent(X,Z),exponent(Y,Z))). % 1.83/2.03 all X Y Z (exponent(exponent(X,Y),Z)=exponent(X,product(Y,Z))). % 1.83/2.03 all C P Q R S B (lemmas(C,P,Q,R,S,B)<->n2=sum(n1,n1)&B!=n0&B!=n1&B!=n2& (all X (B!=product(n0,X)))& (all X (P!=product(Q,X)))& (all X (Q!=product(P,X)))& (all X (R!=product(S,X)))& (all X (S!=product(R,X)))&sum(n1,n0)!=n1&sum(n2,n0)!=n1&sum(n0,n0)!=n1&C!=n1&sum(n1,C)!=n1&product(C,n0)!=n1&sum(n1,n0)!=n0&sum(n2,n0)!=n0&sum(n0,n0)!=n0&C!=n0&sum(n1,C)!=n0&sum(n2,n0)!=sum(n1,n0)&C!=sum(n1,n0)&product(C,n0)!=sum(n1,n0)&C!=sum(n2,n0)&C!=sum(n0,n0)&sum(n1,C)!=C). % 1.83/2.03 n0!=n1. % 1.83/2.03 n0!=n2. % 1.83/2.03 n1!=n2. % 1.83/2.03 -(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))&lemmas(C,P,Q,R,S,B)->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.83/2.03 end_of_list. % 1.83/2.03 % 1.83/2.03 -------> usable clausifies to: % 1.83/2.03 % 1.83/2.03 list(usable). % 1.83/2.03 0 [] A=A. % 1.83/2.03 0 [] sum(X,Y)=sum(Y,X). % 1.83/2.03 0 [] sum(X,sum(Y,Z))=sum(sum(X,Y),Z). % 1.83/2.03 0 [] product(X,n1)=X. % 1.83/2.03 0 [] product(X,Y)=product(Y,X). % 1.83/2.03 0 [] product(X,product(Y,Z))=product(product(X,Y),Z). % 1.83/2.03 0 [] product(X,sum(Y,Z))=sum(product(X,Y),product(X,Z)). % 1.83/2.03 0 [] exponent(n1,X)=n1. % 1.83/2.03 0 [] exponent(X,n1)=X. % 1.83/2.03 0 [] exponent(X,sum(Y,Z))=product(exponent(X,Y),exponent(X,Z)). % 1.83/2.03 0 [] exponent(product(X,Y),Z)=product(exponent(X,Z),exponent(Y,Z)). % 1.83/2.03 0 [] exponent(exponent(X,Y),Z)=exponent(X,product(Y,Z)). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|n2=sum(n1,n1). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|B!=n0. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|B!=n1. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|B!=n2. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|B!=product(n0,X). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|P!=product(Q,X1). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|Q!=product(P,X2). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|R!=product(S,X3). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|S!=product(R,X4). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n1,n0)!=n1. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n2,n0)!=n1. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n0,n0)!=n1. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|C!=n1. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n1,C)!=n1. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|product(C,n0)!=n1. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n1,n0)!=n0. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n2,n0)!=n0. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n0,n0)!=n0. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|C!=n0. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n1,C)!=n0. % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n2,n0)!=sum(n1,n0). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|C!=sum(n1,n0). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|product(C,n0)!=sum(n1,n0). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|C!=sum(n2,n0). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|C!=sum(n0,n0). % 1.83/2.03 0 [] -lemmas(C,P,Q,R,S,B)|sum(n1,C)!=C. % 1.83/2.03 0 [] lemmas(C,P,Q,R,S,B)|n2!=sum(n1,n1)|B=n0|B=n1|B=n2|B=product(n0,$f1(C,P,Q,R,S,B))|P=product(Q,$f2(C,P,Q,R,S,B))|Q=product(P,$f3(C,P,Q,R,S,B))|R=product(S,$f4(C,P,Q,R,S,B))|S=product(R,$f5(C,P,Q,R,S,B))|sum(n1,n0)=n1|sum(n2,n0)=n1|sum(n0,n0)=n1|C=n1|sum(n1,C)=n1|product(C,n0)=n1|sum(n1,n0)=n0|sum(n2,n0)=n0|sum(n0,n0)=n0|C=n0|sum(n1,C)=n0|sum(n2,n0)=sum(n1,n0)|C=sum(n1,n0)|product(C,n0)=sum(n1,n0)|C=sum(n2,n0)|C=sum(n0,n0)|sum(n1,C)=C. % 1.83/2.03 0 [] n0!=n1. % 1.83/2.03 0 [] n0!=n2. % 1.83/2.03 0 [] n1!=n2. % 1.83/2.04 0 [] $c7=product($c2,$c2). % 1.83/2.04 0 [] $c6=sum(n1,$c2). % 1.83/2.04 0 [] $c5=sum($c6,$c7). % 1.83/2.04 0 [] $c4=sum(n1,product($c2,$c7)). % 1.83/2.04 0 [] $c3=sum(sum(n1,$c7),product($c7,$c7)). % 1.83/2.04 0 [] lemmas($c7,$c6,$c5,$c4,$c3,$c1). % 1.83/2.04 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.83/2.04 end_of_list. % 1.83/2.04 % 1.83/2.04 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=27. % 1.83/2.04 % 1.83/2.04 This ia a non-Horn set with equality. The strategy will be % 1.83/2.04 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.83/2.04 deletion, with positive clauses in sos and nonpositive % 1.83/2.04 clauses in usable. % 1.83/2.04 % 1.83/2.04 dependent: set(knuth_bendix). % 1.83/2.04 dependent: set(anl_eq). % 1.83/2.04 dependent: set(para_from). % 1.83/2.04 dependent: set(para_into). % 1.83/2.04 dependent: clear(para_from_right). % 1.83/2.04 dependent: clear(para_into_right). % 1.83/2.04 dependent: set(para_from_vars). % 1.83/2.04 dependent: set(eq_units_both_ways). % 1.83/2.04 dependent: set(dynamic_demod_all). % 1.83/2.04 dependent: set(dynamic_demod). % 1.83/2.04 dependent: set(order_eq). % 1.83/2.04 dependent: set(back_demod). % 1.83/2.04 dependent: set(lrpo). % 1.83/2.04 dependent: set(hyper_res). % 1.83/2.04 dependent: set(unit_deletion). % 1.83/2.04 dependent: set(factor). % 1.83/2.04 % 1.83/2.04 ------------> process usable: % 1.83/2.04 ** KEPT (pick-wt=12): 2 [copy,1,flip.2] -lemmas(A,B,C,D,E,F)|sum(n1,n1)=n2. % 1.83/2.04 ** KEPT (pick-wt=10): 3 [] -lemmas(A,B,C,D,E,F)|F!=n0. % 1.83/2.04 ** KEPT (pick-wt=10): 4 [] -lemmas(A,B,C,D,E,F)|F!=n1. % 1.83/2.04 ** KEPT (pick-wt=10): 5 [] -lemmas(A,B,C,D,E,F)|F!=n2. % 1.83/2.04 ** KEPT (pick-wt=12): 6 [] -lemmas(A,B,C,D,E,F)|F!=product(n0,G). % 1.83/2.04 ** KEPT (pick-wt=12): 7 [] -lemmas(A,B,C,D,E,F)|B!=product(C,G). % 1.83/2.04 ** KEPT (pick-wt=12): 8 [] -lemmas(A,B,C,D,E,F)|C!=product(B,G). % 1.83/2.04 ** KEPT (pick-wt=12): 9 [] -lemmas(A,B,C,D,E,F)|D!=product(E,G). % 1.83/2.04 ** KEPT (pick-wt=12): 10 [] -lemmas(A,B,C,D,E,F)|E!=product(D,G). % 1.83/2.04 ** KEPT (pick-wt=12): 11 [] -lemmas(A,B,C,D,E,F)|sum(n1,n0)!=n1. % 1.83/2.04 ** KEPT (pick-wt=12): 12 [] -lemmas(A,B,C,D,E,F)|sum(n2,n0)!=n1. % 1.83/2.04 ** KEPT (pick-wt=12): 13 [] -lemmas(A,B,C,D,E,F)|sum(n0,n0)!=n1. % 1.83/2.04 ** KEPT (pick-wt=10): 14 [] -lemmas(A,B,C,D,E,F)|A!=n1. % 1.83/2.04 ** KEPT (pick-wt=12): 15 [] -lemmas(A,B,C,D,E,F)|sum(n1,A)!=n1. % 1.83/2.04 ** KEPT (pick-wt=12): 16 [] -lemmas(A,B,C,D,E,F)|product(A,n0)!=n1. % 1.83/2.04 ** KEPT (pick-wt=12): 17 [] -lemmas(A,B,C,D,E,F)|sum(n1,n0)!=n0. % 1.83/2.04 ** KEPT (pick-wt=12): 18 [] -lemmas(A,B,C,D,E,F)|sum(n2,n0)!=n0. % 1.83/2.04 ** KEPT (pick-wt=12): 19 [] -lemmas(A,B,C,D,E,F)|sum(n0,n0)!=n0. % 1.83/2.04 ** KEPT (pick-wt=10): 20 [] -lemmas(A,B,C,D,E,F)|A!=n0. % 1.83/2.04 ** KEPT (pick-wt=12): 21 [] -lemmas(A,B,C,D,E,F)|sum(n1,A)!=n0. % 1.83/2.04 ** KEPT (pick-wt=14): 22 [] -lemmas(A,B,C,D,E,F)|sum(n2,n0)!=sum(n1,n0). % 1.83/2.04 ** KEPT (pick-wt=12): 23 [] -lemmas(A,B,C,D,E,F)|A!=sum(n1,n0). % 1.83/2.04 ** KEPT (pick-wt=14): 24 [] -lemmas(A,B,C,D,E,F)|product(A,n0)!=sum(n1,n0). % 1.83/2.04 ** KEPT (pick-wt=12): 25 [] -lemmas(A,B,C,D,E,F)|A!=sum(n2,n0). % 1.83/2.04 ** KEPT (pick-wt=12): 26 [] -lemmas(A,B,C,D,E,F)|A!=sum(n0,n0). % 1.83/2.04 ** KEPT (pick-wt=12): 27 [] -lemmas(A,B,C,D,E,F)|sum(n1,A)!=A. % 1.83/2.04 ** KEPT (pick-wt=161): 29 [copy,28,flip.2,flip.6,flip.7,flip.8,flip.9,flip.10] lemmas(A,B,C,D,E,F)|sum(n1,n1)!=n2|F=n0|F=n1|F=n2|product(n0,$f1(A,B,C,D,E,F))=F|product(C,$f2(A,B,C,D,E,F))=B|product(B,$f3(A,B,C,D,E,F))=C|product(E,$f4(A,B,C,D,E,F))=D|product(D,$f5(A,B,C,D,E,F))=E|sum(n1,n0)=n1|sum(n2,n0)=n1|sum(n0,n0)=n1|A=n1|sum(n1,A)=n1|product(A,n0)=n1|sum(n1,n0)=n0|sum(n2,n0)=n0|sum(n0,n0)=n0|A=n0|sum(n1,A)=n0|sum(n2,n0)=sum(n1,n0)|A=sum(n1,n0)|product(A,n0)=sum(n1,n0)|A=sum(n2,n0)|A=sum(n0,n0)|sum(n1,A)=A. % 1.83/2.04 ** KEPT (pick-wt=3): 31 [copy,30,flip.1] n1!=n0. % 1.83/2.04 ** KEPT (pick-wt=3): 33 [copy,32,flip.1] n2!=n0. % 1.83/2.04 ** KEPT (pick-wt=3): 35 [copy,34,flip.1] n2!=n1. % 1.83/2.04 ** KEPT (pick-wt=39): 36 [] 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.83/2.04 % 1.83/2.04 ------------> process sos: % 1.83/2.04 ** KEPT (pick-wt=3): 74 [] A=A. % 1.83/2.04 ** KEPT (pick-wt=7): 75 [] sum(A,B)=sum(B,A). % 1.83/2.04 ** KEPT (pick-wt=11): 77 [copy,76,flip.1] sum(sum(A,B),C)=sum(A,sum(B,C)). % 1.83/2.04 ---> New Demodulator: 78 [new_demod,77] sum(sum(A,B),C)=sum(A,sum(B,C)). % 2.35/2.56 ** KEPT (pick-wt=5): 79 [] product(A,n1)=A. % 2.35/2.56 ---> New Demodulator: 80 [new_demod,79] product(A,n1)=A. % 2.35/2.56 ** KEPT (pick-wt=7): 81 [] product(A,B)=product(B,A). % 2.35/2.56 ** KEPT (pick-wt=11): 83 [copy,82,flip.1] product(product(A,B),C)=product(A,product(B,C)). % 2.35/2.56 ---> New Demodulator: 84 [new_demod,83] product(product(A,B),C)=product(A,product(B,C)). % 2.35/2.56 ** KEPT (pick-wt=13): 86 [copy,85,flip.1] sum(product(A,B),product(A,C))=product(A,sum(B,C)). % 2.35/2.56 ---> New Demodulator: 87 [new_demod,86] sum(product(A,B),product(A,C))=product(A,sum(B,C)). % 2.35/2.56 ** KEPT (pick-wt=5): 88 [] exponent(n1,A)=n1. % 2.35/2.56 ---> New Demodulator: 89 [new_demod,88] exponent(n1,A)=n1. % 2.35/2.56 ** KEPT (pick-wt=5): 90 [] exponent(A,n1)=A. % 2.35/2.56 ---> New Demodulator: 91 [new_demod,90] exponent(A,n1)=A. % 2.35/2.56 ** KEPT (pick-wt=13): 92 [] exponent(A,sum(B,C))=product(exponent(A,B),exponent(A,C)). % 2.35/2.56 ** KEPT (pick-wt=13): 94 [copy,93,flip.1] product(exponent(A,B),exponent(C,B))=exponent(product(A,C),B). % 2.35/2.56 ---> New Demodulator: 95 [new_demod,94] product(exponent(A,B),exponent(C,B))=exponent(product(A,C),B). % 2.35/2.56 ** KEPT (pick-wt=11): 96 [] exponent(exponent(A,B),C)=exponent(A,product(B,C)). % 2.35/2.56 ** KEPT (pick-wt=5): 98 [copy,97,flip.1] product($c2,$c2)=$c7. % 2.35/2.56 ---> New Demodulator: 99 [new_demod,98] product($c2,$c2)=$c7. % 2.35/2.56 ** KEPT (pick-wt=5): 101 [copy,100,flip.1] sum(n1,$c2)=$c6. % 2.35/2.56 ---> New Demodulator: 102 [new_demod,101] sum(n1,$c2)=$c6. % 2.35/2.56 ** KEPT (pick-wt=5): 104 [copy,103,flip.1] sum($c6,$c7)=$c5. % 2.35/2.56 ---> New Demodulator: 105 [new_demod,104] sum($c6,$c7)=$c5. % 2.35/2.56 ** KEPT (pick-wt=7): 107 [copy,106,flip.1] sum(n1,product($c2,$c7))=$c4. % 2.35/2.56 ---> New Demodulator: 108 [new_demod,107] sum(n1,product($c2,$c7))=$c4. % 2.35/2.56 ** KEPT (pick-wt=9): 110 [copy,109,demod,78,flip.1] sum(n1,sum($c7,product($c7,$c7)))=$c3. % 2.35/2.56 ---> New Demodulator: 111 [new_demod,110] sum(n1,sum($c7,product($c7,$c7)))=$c3. % 2.35/2.56 ** KEPT (pick-wt=7): 112 [] lemmas($c7,$c6,$c5,$c4,$c3,$c1). % 2.35/2.56 Following clause subsumed by 74 during input processing: 0 [copy,74,flip.1] A=A. % 2.35/2.56 74 back subsumes 73. % 2.35/2.56 74 back subsumes 72. % 2.35/2.56 74 back subsumes 71. % 2.35/2.56 74 back subsumes 70. % 2.35/2.56 74 back subsumes 69. % 2.35/2.56 74 back subsumes 68. % 2.35/2.56 74 back subsumes 67. % 2.35/2.56 74 back subsumes 66. % 2.35/2.56 74 back subsumes 65. % 2.35/2.56 74 back subsumes 64. % 2.35/2.56 74 back subsumes 63. % 2.35/2.56 74 back subsumes 62. % 2.35/2.56 74 back subsumes 61. % 2.35/2.56 74 back subsumes 60. % 2.35/2.56 74 back subsumes 59. % 2.35/2.56 74 back subsumes 58. % 2.35/2.56 74 back subsumes 57. % 2.35/2.56 74 back subsumes 56. % 2.35/2.56 74 back subsumes 55. % 2.35/2.56 74 back subsumes 54. % 2.35/2.56 74 back subsumes 53. % 2.35/2.56 74 back subsumes 52. % 2.35/2.56 74 back subsumes 51. % 2.35/2.56 74 back subsumes 50. % 2.35/2.56 74 back subsumes 49. % 2.35/2.56 74 back subsumes 48. % 2.35/2.56 74 back subsumes 47. % 2.35/2.56 74 back subsumes 46. % 2.35/2.56 74 back subsumes 45. % 2.35/2.56 74 back subsumes 42. % 2.35/2.56 Following clause subsumed by 75 during input processing: 0 [copy,75,flip.1] sum(A,B)=sum(B,A). % 2.35/2.56 >>>> Starting back demodulation with 78. % 2.35/2.56 >>>> Starting back demodulation with 80. % 2.35/2.56 Following clause subsumed by 81 during input processing: 0 [copy,81,flip.1] product(A,B)=product(B,A). % 2.35/2.56 >>>> Starting back demodulation with 84. % 2.35/2.56 >>>> Starting back demodulation with 87. % 2.35/2.56 >>>> Starting back demodulation with 89. % 2.35/2.56 >>>> Starting back demodulation with 91. % 2.35/2.56 ** KEPT (pick-wt=13): 113 [copy,92,flip.1] product(exponent(A,B),exponent(A,C))=exponent(A,sum(B,C)). % 2.35/2.56 >>>> Starting back demodulation with 95. % 2.35/2.56 ** KEPT (pick-wt=11): 114 [copy,96,flip.1] exponent(A,product(B,C))=exponent(exponent(A,B),C). % 2.35/2.56 >>>> Starting back demodulation with 99. % 2.35/2.56 >>>> Starting back demodulation with 102. % 2.35/2.56 >>>> Starting back demodulation with 105. % 2.35/2.56 >>>> Starting back demodulation with 108. % 2.35/2.56 >>>> Starting back demodulation with 111. % 2.35/2.56 Following clause subsumed by 92 during input processing: 0 [copy,113,flip.1] exponent(A,sum(B,C))=product(exponent(A,B),exponent(A,C)). % 2.35/2.56 Following clause subsumed by 96 during input processing: 0 [copy,114,flip.1] exponent(exponent(A,B),C)=exponent(A,product(B,C)). % 2.35/2.56 % 2.35/2.56 ======= end of input processing ======= % 2.35/2.56 % 2.35/2.56 =========== start of search =========== % 2.35/2.56 % 2.35/2.56 % 2.35/2.56 Resetting weight limit to 11. % 2.35/2.56 % 2.35/2.56 % 2.35/2.56 Resetting weight limit to 11. % 2.35/2.56 % 2.35/2.56 sos_size=142 % 2.35/2.56 % 2.35/2.56 % 2.35/2.56 Resetting weight limit to 9. % 2.35/2.56 % 2.35/2.56 % 2.35/2.56 Resetting weight limit to 9. % 2.35/2.56 % 2.35/2.56 sos_size=32 % 2.35/2.56 % 2.35/2.56 Search stopped because sos empty. % 2.35/2.56 % 2.35/2.56 % 2.35/2.56 Search stopped because sos empty. % 2.35/2.56 % 2.35/2.56 ============ end of search ============ % 2.35/2.56 % 2.35/2.56 -------------- statistics ------------- % 2.35/2.56 clauses given 111 % 2.35/2.56 clauses generated 4782 % 2.35/2.56 clauses kept 315 % 2.35/2.56 clauses forward subsumed 1831 % 2.35/2.56 clauses back subsumed 30 % 2.35/2.56 Kbytes malloced 4882 % 2.35/2.56 % 2.35/2.56 ----------- times (seconds) ----------- % 2.35/2.56 user CPU time 0.56 (0 hr, 0 min, 0 sec) % 2.35/2.56 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 2.35/2.56 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.35/2.56 % 2.35/2.56 Process 2420 finished Wed Jul 27 09:38:08 2022 % 2.35/2.56 Otter interrupted % 2.35/2.56 PROOF NOT FOUND %------------------------------------------------------------------------------