%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.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 : Tue May 5 07:05:23 PM UTC 2026 % Result : Unknown 3.33s 3.55s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.16/0.33 % Computer : n011.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 09:54:02 EDT 2026 % 0.16/0.33 % CPUTime : % 2.08/2.28 ----- Otter 3.3f, August 2004 ----- % 2.08/2.28 The process was started by sandbox on n011.cluster.edu, % 2.08/2.28 Tue May 5 09:54:02 2026 % 2.08/2.28 The command was "./otter". The process ID is 30050. % 2.08/2.28 % 2.08/2.28 set(prolog_style_variables). % 2.08/2.28 set(auto). % 2.08/2.28 dependent: set(auto1). % 2.08/2.28 dependent: set(process_input). % 2.08/2.28 dependent: clear(print_kept). % 2.08/2.28 dependent: clear(print_new_demod). % 2.08/2.28 dependent: clear(print_back_demod). % 2.08/2.28 dependent: clear(print_back_sub). % 2.08/2.28 dependent: set(control_memory). % 2.08/2.28 dependent: assign(max_mem, 12000). % 2.08/2.28 dependent: assign(pick_given_ratio, 4). % 2.08/2.28 dependent: assign(stats_level, 1). % 2.08/2.28 dependent: assign(max_seconds, 10800). % 2.08/2.28 clear(print_given). % 2.08/2.28 % 2.08/2.28 formula_list(usable). % 2.08/2.28 all A (A=A). % 2.08/2.28 all X (proj1S(s(X))=X). % 2.08/2.28 all X (s(X)!=z). % 2.08/2.28 all X (proj1N(n(X))=X). % 2.08/2.28 all X X2 (proj1(x(X,X2))=X). % 2.08/2.28 all X X2 (proj2(x(X,X2))=X2). % 2.08/2.28 all X X2 (proj12(y(X,X2))=X). % 2.08/2.28 all X X2 (proj22(y(X,X2))=X2). % 2.08/2.28 all X X2 X3 (n(X)!=x(X2,X3)). % 2.08/2.28 all X X2 X3 (n(X)!=y(X2,X3)). % 2.08/2.28 all X (n(X)!=x2). % 2.08/2.28 all X X2 X3 X4 (x(X,X2)!=y(X3,X4)). % 2.08/2.28 all X X2 (x(X,X2)!=x2). % 2.08/2.28 all X X2 (y(X,X2)!=x2). % 2.08/2.28 all Y E (Y=E->fail2(Y,E)=y(n(s(s(z))),opt(Y))). % 2.08/2.28 all Y E (Y!=E-> (Y!=x(proj1(Y),proj2(Y))->fail2(Y,E)=x(opt(Y),opt(E)))). % 2.08/2.28 all E A B (x(A,B)!=E->fail2(x(A,B),E)=opt(x(A,x(B,E)))). % 2.08/2.28 all Y E (Y!=n(proj1N(Y))->fail1(Y,E)=fail2(Y,E)). % 2.08/2.28 all E C (E!=n(proj1N(E))->fail1(n(C),E)=fail2(n(C),E)). % 2.08/2.28 all C B2 (fail1(n(C),n(B2))=n(addNat(C,B2))). % 2.08/2.28 all Y E (E!=n(proj1N(E))->fail(Y,E)=fail1(Y,E)). % 2.08/2.28 all Y X2 (fail(Y,n(s(X2)))=fail1(Y,n(s(X2)))). % 2.08/2.28 all Y (fail(Y,n(z))=Y). % 2.08/2.28 all X5 E2 (fail4(X5,E2)=y(opt(X5),opt(E2))). % 2.08/2.28 all X5 E2 (X5!=n(proj1N(X5))-> (X5!=y(proj12(X5),proj22(X5))->fail32(X5,E2)=fail4(X5,E2))). % 2.08/2.28 all E2 A2 (E2!=n(proj1N(E2))->fail32(n(A2),E2)=fail4(n(A2),E2)). % 2.08/2.28 all A2 B3 (fail32(n(A2),n(B3))=n(mulNat(A2,B3))). % 2.08/2.28 all E2 A3 B4 (fail32(y(A3,B4),E2)=opt(y(A3,y(B4,E2)))). % 2.08/2.28 all X5 E2 (E2!=n(proj1N(E2))->fail22(X5,E2)=fail32(X5,E2)). % 2.08/2.28 all X5 X8 (fail22(X5,n(s(s(X8))))=fail32(X5,n(s(s(X8))))). % 2.08/2.28 all X5 (fail22(X5,n(s(z)))=X5). % 2.08/2.28 all X5 (fail22(X5,n(z))=fail32(X5,n(z))). % 2.08/2.28 all X5 E2 (X5!=n(proj1N(X5))->fail12(X5,E2)=fail22(X5,E2)). % 2.08/2.28 all E2 X11 (fail12(n(s(s(X11))),E2)=fail22(n(s(s(X11))),E2)). % 2.08/2.28 all E2 (fail12(n(s(z)),E2)=E2). % 2.08/2.28 all E2 (fail12(n(z),E2)=fail22(n(z),E2)). % 2.08/2.28 all X5 E2 (E2!=n(proj1N(E2))->fail3(X5,E2)=fail12(X5,E2)). % 2.08/2.28 all X5 X13 (fail3(X5,n(s(X13)))=fail12(X5,n(s(X13)))). % 2.08/2.28 all X5 (fail3(X5,n(z))=n(z)). % 2.08/2.28 all Y (d(n(Y))=n(z)). % 2.08/2.28 all F G (d(x(F,G))=x(d(F),d(G))). % 2.08/2.28 all H G2 (d(y(H,G2))=x(y(d(H),G2),y(H,d(G2)))). % 2.08/2.28 d(x2)=n(s(z)). % 2.08/2.28 all Y Z (addNat(s(Z),Y)=s(addNat(Z,Y))). % 2.08/2.28 all Y (addNat(z,Y)=Y). % 2.08/2.28 all Y Z (mulNat(s(Z),Y)=addNat(Y,mulNat(Z,Y))). % 2.08/2.28 all Y (mulNat(z,Y)=z). % 2.08/2.28 all X (X!=x(proj1(X),proj2(X))-> (X!=y(proj12(X),proj22(X))->opt(X)=X)). % 2.08/2.28 all Y E (Y!=n(proj1N(Y))->opt(x(Y,E))=fail(Y,E)). % 2.08/2.28 all E X4 (opt(x(n(s(X4)),E))=fail(n(s(X4)),E)). % 2.08/2.28 all E (opt(x(n(z),E))=E). % 2.08/2.28 all X5 E2 (X5!=n(proj1N(X5))->opt(y(X5,E2))=fail3(X5,E2)). % 2.08/2.28 all E2 X15 (opt(y(n(s(X15)),E2))=fail3(n(s(X15)),E2)). % 2.08/2.28 all E2 (opt(y(n(z),E2))=n(z)). % 2.08/2.28 -(exists E (opt(d(E))!=opt(d(opt(E))))). % 2.08/2.28 end_of_list. % 2.08/2.28 % 2.08/2.28 -------> usable clausifies to: % 2.08/2.28 % 2.08/2.28 list(usable). % 2.08/2.28 0 [] A=A. % 2.08/2.28 0 [] proj1S(s(X))=X. % 2.08/2.28 0 [] s(X)!=z. % 2.08/2.28 0 [] proj1N(n(X))=X. % 2.08/2.28 0 [] proj1(x(X,X2))=X. % 2.08/2.28 0 [] proj2(x(X,X2))=X2. % 2.08/2.28 0 [] proj12(y(X,X2))=X. % 2.08/2.28 0 [] proj22(y(X,X2))=X2. % 2.08/2.28 0 [] n(X)!=x(X2,X3). % 2.08/2.28 0 [] n(X)!=y(X2,X3). % 2.08/2.28 0 [] n(X)!=x2. % 2.08/2.28 0 [] x(X,X2)!=y(X3,X4). % 2.08/2.28 0 [] x(X,X2)!=x2. % 2.08/2.28 0 [] y(X,X2)!=x2. % 2.08/2.28 0 [] Y!=E|fail2(Y,E)=y(n(s(s(z))),opt(Y)). % 2.08/2.28 0 [] Y=E|Y=x(proj1(Y),proj2(Y))|fail2(Y,E)=x(opt(Y),opt(E)). % 2.08/2.28 0 [] x(A,B)=E|fail2(x(A,B),E)=opt(x(A,x(B,E))). % 2.08/2.28 0 [] Y=n(proj1N(Y))|fail1(Y,E)=fail2(Y,E). % 2.08/2.28 0 [] E=n(proj1N(E))|fail1(n(C),E)=fail2(n(C),E). % 2.08/2.28 0 [] fail1(n(C),n(B2))=n(addNat(C,B2)). % 2.08/2.28 0 [] E=n(proj1N(E))|fail(Y,E)=fail1(Y,E). % 2.08/2.28 0 [] fail(Y,n(s(X2)))=fail1(Y,n(s(X2))). % 2.08/2.28 0 [] fail(Y,n(z))=Y. % 2.08/2.28 0 [] fail4(X5,E2)=y(opt(X5),opt(E2)). % 2.08/2.28 0 [] X5=n(proj1N(X5))|X5=y(proj12(X5),proj22(X5))|fail32(X5,E2)=fail4(X5,E2). % 2.08/2.28 0 [] E2=n(proj1N(E2))|fail32(n(A2),E2)=fail4(n(A2),E2). % 2.08/2.28 0 [] fail32(n(A2),n(B3))=n(mulNat(A2,B3)). % 2.08/2.28 0 [] fail32(y(A3,B4),E2)=opt(y(A3,y(B4,E2))). % 2.08/2.28 0 [] E2=n(proj1N(E2))|fail22(X5,E2)=fail32(X5,E2). % 2.08/2.28 0 [] fail22(X5,n(s(s(X8))))=fail32(X5,n(s(s(X8)))). % 2.08/2.28 0 [] fail22(X5,n(s(z)))=X5. % 2.08/2.28 0 [] fail22(X5,n(z))=fail32(X5,n(z)). % 2.08/2.28 0 [] X5=n(proj1N(X5))|fail12(X5,E2)=fail22(X5,E2). % 2.08/2.28 0 [] fail12(n(s(s(X11))),E2)=fail22(n(s(s(X11))),E2). % 2.08/2.28 0 [] fail12(n(s(z)),E2)=E2. % 2.08/2.28 0 [] fail12(n(z),E2)=fail22(n(z),E2). % 2.08/2.28 0 [] E2=n(proj1N(E2))|fail3(X5,E2)=fail12(X5,E2). % 2.08/2.28 0 [] fail3(X5,n(s(X13)))=fail12(X5,n(s(X13))). % 2.08/2.28 0 [] fail3(X5,n(z))=n(z). % 2.08/2.28 0 [] d(n(Y))=n(z). % 2.08/2.28 0 [] d(x(F,G))=x(d(F),d(G)). % 2.08/2.28 0 [] d(y(H,G2))=x(y(d(H),G2),y(H,d(G2))). % 2.08/2.28 0 [] d(x2)=n(s(z)). % 2.08/2.28 0 [] addNat(s(Z),Y)=s(addNat(Z,Y)). % 2.08/2.28 0 [] addNat(z,Y)=Y. % 2.08/2.28 0 [] mulNat(s(Z),Y)=addNat(Y,mulNat(Z,Y)). % 2.08/2.28 0 [] mulNat(z,Y)=z. % 2.08/2.28 0 [] X=x(proj1(X),proj2(X))|X=y(proj12(X),proj22(X))|opt(X)=X. % 2.08/2.28 0 [] Y=n(proj1N(Y))|opt(x(Y,E))=fail(Y,E). % 2.08/2.28 0 [] opt(x(n(s(X4)),E))=fail(n(s(X4)),E). % 2.08/2.28 0 [] opt(x(n(z),E))=E. % 2.08/2.28 0 [] X5=n(proj1N(X5))|opt(y(X5,E2))=fail3(X5,E2). % 2.08/2.28 0 [] opt(y(n(s(X15)),E2))=fail3(n(s(X15)),E2). % 2.08/2.28 0 [] opt(y(n(z),E2))=n(z). % 2.08/2.28 0 [] opt(d(E))=opt(d(opt(E))). % 2.08/2.28 end_of_list. % 2.08/2.28 % 2.08/2.28 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. % 2.08/2.28 % 2.08/2.28 This ia a non-Horn set with equality. The strategy will be % 2.08/2.28 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.08/2.28 deletion, with positive clauses in sos and nonpositive % 2.08/2.28 clauses in usable. % 2.08/2.28 % 2.08/2.28 dependent: set(knuth_bendix). % 2.08/2.28 dependent: set(anl_eq). % 2.08/2.28 dependent: set(para_from). % 2.08/2.28 dependent: set(para_into). % 2.08/2.28 dependent: clear(para_from_right). % 2.08/2.28 dependent: clear(para_into_right). % 2.08/2.28 dependent: set(para_from_vars). % 2.08/2.28 dependent: set(eq_units_both_ways). % 2.08/2.28 dependent: set(dynamic_demod_all). % 2.08/2.28 dependent: set(dynamic_demod). % 2.08/2.28 dependent: set(order_eq). % 2.08/2.28 dependent: set(back_demod). % 2.08/2.28 dependent: set(lrpo). % 2.08/2.28 dependent: set(hyper_res). % 2.08/2.28 dependent: set(unit_deletion). % 2.08/2.28 dependent: set(factor). % 2.08/2.28 % 2.08/2.28 ------------> process usable: % 2.08/2.28 ** KEPT (pick-wt=4): 1 [] s(A)!=z. % 2.08/2.28 ** KEPT (pick-wt=6): 2 [] n(A)!=x(B,C). % 2.08/2.28 ** KEPT (pick-wt=6): 3 [] n(A)!=y(B,C). % 2.08/2.28 ** KEPT (pick-wt=4): 4 [] n(A)!=x2. % 2.08/2.28 ** KEPT (pick-wt=7): 5 [] x(A,B)!=y(C,D). % 2.08/2.28 ** KEPT (pick-wt=5): 6 [] x(A,B)!=x2. % 2.08/2.28 ** KEPT (pick-wt=5): 7 [] y(A,B)!=x2. % 2.08/2.28 ** KEPT (pick-wt=14): 8 [] A!=B|fail2(A,B)=y(n(s(s(z))),opt(A)). % 2.08/2.28 ** KEPT (pick-wt=6): 9 [copy,2,flip.1] x(A,B)!=n(C). % 2.08/2.28 ** KEPT (pick-wt=6): 10 [copy,3,flip.1] y(A,B)!=n(C). % 2.08/2.28 ** KEPT (pick-wt=7): 11 [copy,5,flip.1] y(A,B)!=x(C,D). % 2.08/2.28 Following clause subsumed by 2 during input processing: 0 [copy,9,flip.1] n(A)!=x(B,C). % 2.08/2.28 Following clause subsumed by 3 during input processing: 0 [copy,10,flip.1] n(A)!=y(B,C). % 2.08/2.28 Following clause subsumed by 5 during input processing: 0 [copy,11,flip.1] x(A,B)!=y(C,D). % 2.08/2.28 % 2.08/2.28 ------------> process sos: % 2.08/2.28 ** KEPT (pick-wt=3): 12 [] A=A. % 2.08/2.28 ** KEPT (pick-wt=5): 13 [] proj1S(s(A))=A. % 2.08/2.28 ---> New Demodulator: 14 [new_demod,13] proj1S(s(A))=A. % 2.08/2.28 ** KEPT (pick-wt=5): 15 [] proj1N(n(A))=A. % 2.08/2.28 ---> New Demodulator: 16 [new_demod,15] proj1N(n(A))=A. % 2.08/2.28 ** KEPT (pick-wt=6): 17 [] proj1(x(A,B))=A. % 2.08/2.28 ---> New Demodulator: 18 [new_demod,17] proj1(x(A,B))=A. % 2.08/2.28 ** KEPT (pick-wt=6): 19 [] proj2(x(A,B))=B. % 2.08/2.28 ---> New Demodulator: 20 [new_demod,19] proj2(x(A,B))=B. % 2.08/2.28 ** KEPT (pick-wt=6): 21 [] proj12(y(A,B))=A. % 2.08/2.28 ---> New Demodulator: 22 [new_demod,21] proj12(y(A,B))=A. % 2.08/2.28 ** KEPT (pick-wt=6): 23 [] proj22(y(A,B))=B. % 2.08/2.28 ---> New Demodulator: 24 [new_demod,23] proj22(y(A,B))=B. % 2.08/2.28 ** KEPT (pick-wt=19): 26 [copy,25,flip.2,flip.3] A=B|x(proj1(A),proj2(A))=A|x(opt(A),opt(B))=fail2(A,B). % 2.08/2.28 ** KEPT (pick-wt=17): 28 [copy,27,flip.2] x(A,B)=C|opt(x(A,x(B,C)))=fail2(x(A,B),C). % 2.08/2.28 ** KEPT (pick-wt=12): 30 [copy,29,flip.1,flip.2] n(proj1N(A))=A|fail2(A,B)=fail1(A,B). % 2.08/2.28 ** KEPT (pick-wt=14): 32 [copy,31,flip.1,flip.2] n(proj1N(A))=A|fail2(n(B),A)=fail1(n(B),A). % 2.08/2.28 ** KEPT (pick-wt=10): 34 [copy,33,flip.1] n(addNat(A,B))=fail1(n(A),n(B)). % 2.08/2.28 ---> New Demodulator: 35 [new_demod,34] n(addNat(A,B))=fail1(n(A),n(B)). % 2.08/2.28 ** KEPT (pick-wt=12): 37 [copy,36,flip.1,flip.2] n(proj1N(A))=A|fail1(B,A)=fail(B,A). % 2.08/2.28 ** KEPT (pick-wt=11): 39 [copy,38,flip.1] fail1(A,n(s(B)))=fail(A,n(s(B))). % 2.08/2.28 ---> New Demodulator: 40 [new_demod,39] fail1(A,n(s(B)))=fail(A,n(s(B))). % 2.08/2.28 ** KEPT (pick-wt=6): 41 [] fail(A,n(z))=A. % 2.08/2.28 ---> New Demodulator: 42 [new_demod,41] fail(A,n(z))=A. % 2.08/2.28 ** KEPT (pick-wt=9): 44 [copy,43,flip.1] y(opt(A),opt(B))=fail4(A,B). % 2.08/2.28 ---> New Demodulator: 45 [new_demod,44] y(opt(A),opt(B))=fail4(A,B). % 2.08/2.28 ** KEPT (pick-wt=19): 47 [copy,46,flip.1,flip.2,flip.3] n(proj1N(A))=A|y(proj12(A),proj22(A))=A|fail4(A,B)=fail32(A,B). % 2.08/2.28 ** KEPT (pick-wt=14): 49 [copy,48,flip.1,flip.2] n(proj1N(A))=A|fail4(n(B),A)=fail32(n(B),A). % 2.08/2.28 ** KEPT (pick-wt=10): 51 [copy,50,flip.1] n(mulNat(A,B))=fail32(n(A),n(B)). % 2.08/2.28 ---> New Demodulator: 52 [new_demod,51] n(mulNat(A,B))=fail32(n(A),n(B)). % 2.08/2.28 ** KEPT (pick-wt=12): 54 [copy,53,flip.1] opt(y(A,y(B,C)))=fail32(y(A,B),C). % 2.08/2.28 ---> New Demodulator: 55 [new_demod,54] opt(y(A,y(B,C)))=fail32(y(A,B),C). % 2.08/2.28 ** KEPT (pick-wt=12): 57 [copy,56,flip.1,flip.2] n(proj1N(A))=A|fail32(B,A)=fail22(B,A). % 2.08/2.28 ** KEPT (pick-wt=13): 59 [copy,58,flip.1] fail32(A,n(s(s(B))))=fail22(A,n(s(s(B)))). % 2.08/2.28 ---> New Demodulator: 60 [new_demod,59] fail32(A,n(s(s(B))))=fail22(A,n(s(s(B)))). % 2.08/2.28 ** KEPT (pick-wt=7): 61 [] fail22(A,n(s(z)))=A. % 2.08/2.28 ---> New Demodulator: 62 [new_demod,61] fail22(A,n(s(z)))=A. % 2.08/2.28 ** KEPT (pick-wt=9): 64 [copy,63,flip.1] fail32(A,n(z))=fail22(A,n(z)). % 2.08/2.28 ---> New Demodulator: 65 [new_demod,64] fail32(A,n(z))=fail22(A,n(z)). % 2.08/2.28 ** KEPT (pick-wt=12): 67 [copy,66,flip.1,flip.2] n(proj1N(A))=A|fail22(A,B)=fail12(A,B). % 2.08/2.28 ** KEPT (pick-wt=13): 69 [copy,68,flip.1] fail22(n(s(s(A))),B)=fail12(n(s(s(A))),B). % 2.08/2.28 ---> New Demodulator: 70 [new_demod,69] fail22(n(s(s(A))),B)=fail12(n(s(s(A))),B). % 2.08/2.28 ** KEPT (pick-wt=7): 71 [] fail12(n(s(z)),A)=A. % 2.08/2.28 ---> New Demodulator: 72 [new_demod,71] fail12(n(s(z)),A)=A. % 2.08/2.28 ** KEPT (pick-wt=9): 74 [copy,73,flip.1] fail22(n(z),A)=fail12(n(z),A). % 2.08/2.28 ---> New Demodulator: 75 [new_demod,74] fail22(n(z),A)=fail12(n(z),A). % 2.08/2.28 ** KEPT (pick-wt=12): 77 [copy,76,flip.1] n(proj1N(A))=A|fail3(B,A)=fail12(B,A). % 2.08/2.28 ** KEPT (pick-wt=11): 78 [] fail3(A,n(s(B)))=fail12(A,n(s(B))). % 2.08/2.28 ---> New Demodulator: 79 [new_demod,78] fail3(A,n(s(B)))=fail12(A,n(s(B))). % 2.08/2.28 ** KEPT (pick-wt=7): 80 [] fail3(A,n(z))=n(z). % 2.08/2.28 ---> New Demodulator: 81 [new_demod,80] fail3(A,n(z))=n(z). % 2.08/2.28 ** KEPT (pick-wt=6): 82 [] d(n(A))=n(z). % 2.08/2.28 ** KEPT (pick-wt=10): 83 [] d(x(A,B))=x(d(A),d(B)). % 2.08/2.28 ---> New Demodulator: 84 [new_demod,83] d(x(A,B))=x(d(A),d(B)). % 2.08/2.28 ** KEPT (pick-wt=14): 85 [] d(y(A,B))=x(y(d(A),B),y(A,d(B))). % 2.08/2.28 ---> New Demodulator: 86 [new_demod,85] d(y(A,B))=x(y(d(A),B),y(A,d(B))). % 2.08/2.28 ** KEPT (pick-wt=6): 88 [copy,87,flip.1] n(s(z))=d(x2). % 2.08/2.28 ---> New Demodulator: 89 [new_demod,88] n(s(z))=d(x2). % 2.08/2.28 ** KEPT (pick-wt=9): 91 [copy,90,flip.1] s(addNat(A,B))=addNat(s(A),B). % 2.08/2.28 ---> New Demodulator: 92 [new_demod,91] s(addNat(A,B))=addNat(s(A),B). % 2.08/2.28 ** KEPT (pick-wt=5): 93 [] addNat(z,A)=A. % 2.08/2.28 ---> New Demodulator: 94 [new_demod,93] addNat(z,A)=A. % 2.08/2.28 ** KEPT (pick-wt=10): 95 [] mulNat(s(A),B)=addNat(B,mulNat(A,B)). % 2.08/2.28 ---> New Demodulator: 96 [new_demod,95] mulNat(s(A),B)=addNat(B,mulNat(A,B)). % 2.08/2.28 ** KEPT (pick-wt=5): 97 [] mulNat(z,A)=z. % 2.08/2.28 ---> New Demodulator: 98 [new_demod,97] mulNat(z,A)=z. % 2.08/2.28 ** KEPT (pick-wt=18): 100 [copy,99,flip.1,flip.2] x(proj1(A),proj2(A))=A|y(proj12(A),proj22(A))=A|opt(A)=A. % 2.08/2.28 ** KEPT (pick-wt=13): 102 [copy,101,flip.1] n(proj1N(A))=A|opt(x(A,B))=fail(A,B). % 2.08/2.28 ** KEPT (pick-wt=12): 103 [] opt(x(n(s(A)),B))=fail(n(s(A)),B). % 2.08/2.28 ---> New Demodulator: 104 [new_demod,103] opt(x(n(s(A)),B))=fail(n(s(A)),B). % 2.08/2.28 ** KEPT (pick-wt=7): 105 [] opt(x(n(z),A))=A. % 2.08/2.28 ---> New Demodulator: 106 [new_demod,105] opt(x(n(z),A))=A. % 2.08/2.28 ** KEPT (pick-wt=13): 108 [copy,107,flip.1] n(proj1N(A))=A|opt(y(A,B))=fail3(A,B). % 2.08/2.28 ** KEPT (pick-wt=12): 109 [] opt(y(n(s(A)),B))=fail3(n(s(A)),B). % 2.08/2.28 ---> New Demodulator: 110 [new_demod,109] opt(y(n(s(A)),B))=fail3(n(s(A)),B). % 2.08/2.28 ** KEPT (pick-wt=8): 111 [] opt(y(n(z),A))=n(z). % 2.08/2.28 ---> New Demodulator: 112 [new_demod,111] opt(y(n(z),A))=n(z). % 2.08/2.28 ** KEPT (pick-wt=8): 114 [copy,113,flip.1] opt(d(opt(A)))=opt(d(A)). % 2.08/2.28 ---> New Demodulator: 115 [new_demod,114] opt(d(opt(A)))=opt(d(A)). % 2.08/2.28 Following clause subsumed by 12 during input processing: 0 [copy,12,flip.1] A=A. % 2.08/2.28 >>>> Starting back demodulation with 14. % 2.08/2.28 >>>> Starting back demodulation with 16. % 2.08/2.28 >>>> Starting back demodulation with 18. % 2.08/2.28 >>>> Starting back demodulation with 20. % 2.08/2.28 >>>> Starting back demodulation with 22. % 2.08/2.28 >>>> Starting back demodulation with 24. % 2.08/2.28 >>>> Starting back demodulation with 35. % 2.08/2.28 >>>> Starting back demodulation with 40. % 2.08/2.28 >>>> Starting back demodulation with 42. % 3.33/3.54 >>>> Starting back demodulation with 45. % 3.33/3.54 >>>> Starting back demodulation with 52. % 3.33/3.54 >>>> Starting back demodulation with 55. % 3.33/3.54 >>>> Starting back demodulation with 60. % 3.33/3.54 >>>> Starting back demodulation with 62. % 3.33/3.54 >>>> Starting back demodulation with 65. % 3.33/3.54 >>>> Starting back demodulation with 70. % 3.33/3.54 >>>> Starting back demodulation with 72. % 3.33/3.54 >>>> Starting back demodulation with 75. % 3.33/3.54 >>>> Starting back demodulation with 79. % 3.33/3.54 >>>> Starting back demodulation with 81. % 3.33/3.54 ** KEPT (pick-wt=6): 116 [copy,82,flip.1] n(z)=d(n(A)). % 3.33/3.54 >>>> Starting back demodulation with 84. % 3.33/3.54 >>>> Starting back demodulation with 86. % 3.33/3.54 >>>> Starting back demodulation with 89. % 3.33/3.54 >> back demodulating 71 with 89. % 3.33/3.54 >> back demodulating 61 with 89. % 3.33/3.54 >>>> Starting back demodulation with 92. % 3.33/3.54 >>>> Starting back demodulation with 94. % 3.33/3.54 >>>> Starting back demodulation with 96. % 3.33/3.54 >>>> Starting back demodulation with 98. % 3.33/3.54 >>>> Starting back demodulation with 104. % 3.33/3.54 >>>> Starting back demodulation with 106. % 3.33/3.54 >>>> Starting back demodulation with 110. % 3.33/3.54 >>>> Starting back demodulation with 112. % 3.33/3.54 >>>> Starting back demodulation with 115. % 3.33/3.54 Following clause subsumed by 82 during input processing: 0 [copy,116,flip.1] d(n(A))=n(z). % 3.33/3.54 >>>> Starting back demodulation with 118. % 3.33/3.54 >>>> Starting back demodulation with 120. % 3.33/3.54 % 3.33/3.54 ======= end of input processing ======= % 3.33/3.54 % 3.33/3.54 =========== start of search =========== % 3.33/3.54 % 3.33/3.54 % 3.33/3.54 Resetting weight limit to 8. % 3.33/3.54 % 3.33/3.54 % 3.33/3.54 Resetting weight limit to 8. % 3.33/3.54 % 3.33/3.54 sos_size=276 % 3.33/3.54 % 3.33/3.54 Search stopped because sos empty. % 3.33/3.54 % 3.33/3.54 % 3.33/3.54 Search stopped because sos empty. % 3.33/3.54 % 3.33/3.54 ============ end of search ============ % 3.33/3.54 % 3.33/3.54 -------------- statistics ------------- % 3.33/3.54 clauses given 371 % 3.33/3.54 clauses generated 95087 % 3.33/3.54 clauses kept 557 % 3.33/3.54 clauses forward subsumed 789 % 3.33/3.54 clauses back subsumed 10 % 3.33/3.54 Kbytes malloced 7812 % 3.33/3.54 % 3.33/3.54 ----------- times (seconds) ----------- % 3.33/3.54 user CPU time 1.26 (0 hr, 0 min, 1 sec) % 3.33/3.54 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 3.33/3.54 wall-clock time 3 (0 hr, 0 min, 3 sec) % 3.33/3.54 % 3.33/3.54 Process 30050 finished Tue May 5 09:54:05 2026 % 3.33/3.54 Otter interrupted % 3.33/3.54 PROOF NOT FOUND %------------------------------------------------------------------------------