%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX194-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n013.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 2.18s 2.89s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX194-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.17/0.34 % Computer : n013.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue May 5 10:53:25 EDT 2026 % 0.17/0.35 % CPUTime : % 2.18/2.85 ----- Otter 3.3f, August 2004 ----- % 2.18/2.85 The process was started by sandbox2 on n013.cluster.edu, % 2.18/2.85 Tue May 5 10:53:26 2026 % 2.18/2.85 The command was "./otter". The process ID is 16827. % 2.18/2.85 % 2.18/2.85 set(prolog_style_variables). % 2.18/2.85 set(auto). % 2.18/2.85 dependent: set(auto1). % 2.18/2.85 dependent: set(process_input). % 2.18/2.85 dependent: clear(print_kept). % 2.18/2.85 dependent: clear(print_new_demod). % 2.18/2.85 dependent: clear(print_back_demod). % 2.18/2.85 dependent: clear(print_back_sub). % 2.18/2.85 dependent: set(control_memory). % 2.18/2.85 dependent: assign(max_mem, 12000). % 2.18/2.85 dependent: assign(pick_given_ratio, 4). % 2.18/2.85 dependent: assign(stats_level, 1). % 2.18/2.85 dependent: assign(max_seconds, 10800). % 2.18/2.85 clear(print_given). % 2.18/2.85 % 2.18/2.85 list(usable). % 2.18/2.85 0 [] A=A. % 2.18/2.85 0 [] aux(Z,Y2,btrue)=mul(n(suc(suc(zero))),v(Z)). % 2.18/2.85 0 [] aux(Z,Y2,bfalse)=add(v(Z),v(Y2)). % 2.18/2.85 0 [] aux2(Y,B,btrue)=mul(n(suc(suc(zero))),Y). % 2.18/2.85 0 [] aux2(add(C,B1),B,bfalse)=add(C,add(B1,B)). % 2.18/2.85 0 [] aux2(v(Z),v(Y2),bfalse)=aux(Z,Y2,e_q2(Z,Z)). % 2.18/2.85 0 [] aux2(v(Z),n(X),bfalse)=add(v(Z),n(X)). % 2.18/2.85 0 [] aux2(v(Z),add(X,X2),bfalse)=add(v(Z),add(X,X2)). % 2.18/2.85 0 [] aux2(v(Z),mul(X,X2),bfalse)=add(v(Z),mul(X,X2)). % 2.18/2.85 0 [] aux2(v(Z),e_q(X,X2),bfalse)=add(v(Z),e_q(X,X2)). % 2.18/2.85 0 [] aux2(n(X),B,bfalse)=add(n(X),B). % 2.18/2.85 0 [] aux2(mul(X,X2),B,bfalse)=add(mul(X,X2),B). % 2.18/2.85 0 [] aux2(e_q(X,X2),B,bfalse)=add(e_q(X,X2),B). % 2.18/2.85 0 [] aux3(Z,Y2,btrue)=mul(n(suc(suc(zero))),v(Z)). % 2.18/2.85 0 [] aux3(Z,Y2,bfalse)=add(v(Z),v(Y2)). % 2.18/2.85 0 [] aux4(Y,B,btrue)=mul(n(suc(suc(zero))),Y). % 2.18/2.85 0 [] aux4(add(C,B1),B,bfalse)=add(C,add(B1,B)). % 2.18/2.85 0 [] aux4(v(Z),v(Y2),bfalse)=aux3(Z,Y2,e_q2(Z,Z)). % 2.18/2.85 0 [] aux4(v(Z),n(X),bfalse)=add(v(Z),n(X)). % 2.18/2.85 0 [] aux4(v(Z),add(X,X2),bfalse)=add(v(Z),add(X,X2)). % 2.18/2.85 0 [] aux4(v(Z),mul(X,X2),bfalse)=add(v(Z),mul(X,X2)). % 2.18/2.85 0 [] aux4(v(Z),e_q(X,X2),bfalse)=add(v(Z),e_q(X,X2)). % 2.18/2.85 0 [] aux4(n(X),B,bfalse)=add(n(X),B). % 2.18/2.85 0 [] aux4(mul(X,X2),B,bfalse)=add(mul(X,X2),B). % 2.18/2.85 0 [] aux4(e_q(X,X2),B,bfalse)=add(e_q(X,X2),B). % 2.18/2.85 0 [] aux5(A3,B3,btrue)=n(suc(zero)). % 2.18/2.85 0 [] aux5(A3,B3,bfalse)=e_q(A3,B3). % 2.18/2.85 0 [] aux6(A,B,n(zero))=b(B). % 2.18/2.85 0 [] aux6(A,B,n(suc(X5)))=fail4(y(A),b(B)). % 2.18/2.85 0 [] aux6(A,B,add(X,X2))=fail4(y(A),b(B)). % 2.18/2.85 0 [] aux6(A,B,mul(X,X2))=fail4(y(A),b(B)). % 2.18/2.85 0 [] aux6(A,B,e_q(X,X2))=fail4(y(A),b(B)). % 2.18/2.85 0 [] aux6(A,B,v(X))=fail4(y(A),b(B)). % 2.18/2.85 0 [] aux7(C,B2,n(zero))=n(zero). % 2.18/2.85 0 [] aux7(C,B2,n(suc(X16)))=fail23(x6(C),b2(B2)). % 2.18/2.85 0 [] aux7(C,B2,add(X,X2))=fail23(x6(C),b2(B2)). % 2.18/2.85 0 [] aux7(C,B2,mul(X,X2))=fail23(x6(C),b2(B2)). % 2.18/2.85 0 [] aux7(C,B2,e_q(X,X2))=fail23(x6(C),b2(B2)). % 2.18/2.85 0 [] aux7(C,B2,v(X))=fail23(x6(C),b2(B2)). % 2.18/2.85 0 [] aux8(A2,B3,btrue)=n(suc(zero)). % 2.18/2.85 0 [] aux8(A2,B3,bfalse)=e_q(a3(A2),b3(B3)). % 2.18/2.85 0 [] aux9(X,A2,B3,btrue)=suc(zero). % 2.18/2.85 0 [] aux9(X,A2,B3,bfalse)=zero. % 2.18/2.85 0 [] fail1(Y,B)=aux2(Y,B,e_q3(Y,B)). % 2.18/2.85 0 [] fail(Y,n(zero))=Y. % 2.18/2.85 0 [] fail(Y,n(suc(X3)))=fail1(Y,n(suc(X3))). % 2.18/2.85 0 [] fail(Y,add(X,X2))=fail1(Y,add(X,X2)). % 2.18/2.85 0 [] fail(Y,mul(X,X2))=fail1(Y,mul(X,X2)). % 2.18/2.85 0 [] fail(Y,e_q(X,X2))=fail1(Y,e_q(X,X2)). % 2.18/2.85 0 [] fail(Y,v(X))=fail1(Y,v(X)). % 2.18/2.85 0 [] fail3(mul(A2,B12),B2)=mul(A2,mul(B12,B2)). % 2.18/2.85 0 [] fail3(n(X),B2)=mul(n(X),B2). % 2.18/2.85 0 [] fail3(add(X,X2),B2)=mul(add(X,X2),B2). % 2.18/2.85 0 [] fail3(e_q(X,X2),B2)=mul(e_q(X,X2),B2). % 2.18/2.85 0 [] fail3(v(X),B2)=mul(v(X),B2). % 2.18/2.85 0 [] fail22(X6,n(zero))=fail3(X6,n(zero)). % 2.18/2.85 0 [] fail22(X6,n(suc(zero)))=X6. % 2.18/2.85 0 [] fail22(X6,n(suc(suc(X9))))=fail3(X6,n(suc(suc(X9)))). % 2.18/2.85 0 [] fail22(X6,add(X,X2))=fail3(X6,add(X,X2)). % 2.18/2.85 0 [] fail22(X6,mul(X,X2))=fail3(X6,mul(X,X2)). % 2.18/2.85 0 [] fail22(X6,e_q(X,X2))=fail3(X6,e_q(X,X2)). % 2.18/2.85 0 [] fail22(X6,v(X))=fail3(X6,v(X)). % 2.18/2.85 0 [] fail12(n(zero),B2)=fail22(n(zero),B2). % 2.18/2.85 0 [] fail12(n(suc(zero)),B2)=B2. % 2.18/2.85 0 [] fail12(n(suc(suc(X12))),B2)=fail22(n(suc(suc(X12))),B2). % 2.18/2.85 0 [] fail12(add(X,X2),B2)=fail22(add(X,X2),B2). % 2.18/2.85 0 [] fail12(mul(X,X2),B2)=fail22(mul(X,X2),B2). % 2.18/2.85 0 [] fail12(e_q(X,X2),B2)=fail22(e_q(X,X2),B2). % 2.18/2.85 0 [] fail12(v(X),B2)=fail22(v(X),B2). % 2.18/2.85 0 [] fail2(X6,n(zero))=n(zero). % 2.18/2.85 0 [] fail2(X6,n(suc(X14)))=fail12(X6,n(suc(X14))). % 2.18/2.85 0 [] fail2(X6,add(X,X2))=fail12(X6,add(X,X2)). % 2.18/2.85 0 [] fail2(X6,mul(X,X2))=fail12(X6,mul(X,X2)). % 2.18/2.85 0 [] fail2(X6,e_q(X,X2))=fail12(X6,e_q(X,X2)). % 2.18/2.85 0 [] fail2(X6,v(X))=fail12(X6,v(X)). % 2.18/2.85 0 [] fail13(Y,B)=aux4(Y,B,e_q3(Y,B)). % 2.18/2.85 0 [] fail4(Y,n(zero))=Y. % 2.18/2.85 0 [] fail4(Y,n(suc(X3)))=fail13(Y,n(suc(X3))). % 2.18/2.85 0 [] fail4(Y,add(X,X2))=fail13(Y,add(X,X2)). % 2.18/2.85 0 [] fail4(Y,mul(X,X2))=fail13(Y,mul(X,X2)). % 2.18/2.85 0 [] fail4(Y,e_q(X,X2))=fail13(Y,e_q(X,X2)). % 2.18/2.85 0 [] fail4(Y,v(X))=fail13(Y,v(X)). % 2.18/2.85 0 [] b(B)=simp1(B). % 2.18/2.85 0 [] y(A)=simp1(A). % 2.18/2.85 0 [] fail32(mul(A2,B12),B2)=mul(A2,mul(B12,B2)). % 2.18/2.85 0 [] fail32(n(X),B2)=mul(n(X),B2). % 2.18/2.85 0 [] fail32(add(X,X2),B2)=mul(add(X,X2),B2). % 2.18/2.85 0 [] fail32(e_q(X,X2),B2)=mul(e_q(X,X2),B2). % 2.18/2.85 0 [] fail32(v(X),B2)=mul(v(X),B2). % 2.18/2.85 0 [] fail222(X6,n(zero))=fail32(X6,n(zero)). % 2.18/2.85 0 [] fail222(X6,n(suc(zero)))=X6. % 2.18/2.85 0 [] fail222(X6,n(suc(suc(X9))))=fail32(X6,n(suc(suc(X9)))). % 2.18/2.85 0 [] fail222(X6,add(X,X2))=fail32(X6,add(X,X2)). % 2.18/2.85 0 [] fail222(X6,mul(X,X2))=fail32(X6,mul(X,X2)). % 2.18/2.85 0 [] fail222(X6,e_q(X,X2))=fail32(X6,e_q(X,X2)). % 2.18/2.85 0 [] fail222(X6,v(X))=fail32(X6,v(X)). % 2.18/2.85 0 [] fail122(n(zero),B2)=fail222(n(zero),B2). % 2.18/2.85 0 [] fail122(n(suc(zero)),B2)=B2. % 2.18/2.85 0 [] fail122(n(suc(suc(X12))),B2)=fail222(n(suc(suc(X12))),B2). % 2.18/2.85 0 [] fail122(add(X,X2),B2)=fail222(add(X,X2),B2). % 2.18/2.85 0 [] fail122(mul(X,X2),B2)=fail222(mul(X,X2),B2). % 2.18/2.85 0 [] fail122(e_q(X,X2),B2)=fail222(e_q(X,X2),B2). % 2.18/2.85 0 [] fail122(v(X),B2)=fail222(v(X),B2). % 2.18/2.85 0 [] fail23(X6,n(zero))=n(zero). % 2.18/2.85 0 [] fail23(X6,n(suc(X14)))=fail122(X6,n(suc(X14))). % 2.18/2.85 0 [] fail23(X6,add(X,X2))=fail122(X6,add(X,X2)). % 2.18/2.85 0 [] fail23(X6,mul(X,X2))=fail122(X6,mul(X,X2)). % 2.18/2.85 0 [] fail23(X6,e_q(X,X2))=fail122(X6,e_q(X,X2)). % 2.18/2.85 0 [] fail23(X6,v(X))=fail122(X6,v(X)). % 2.18/2.85 0 [] b2(B2)=simp1(B2). % 2.18/2.85 0 [] x6(C)=simp1(C). % 2.18/2.85 0 [] b3(B3)=simp1(B3). % 2.18/2.85 0 [] a3(A2)=simp1(A2). % 2.18/2.85 0 [] step1(add(n(zero),B))=B. % 2.18/2.85 0 [] step1(add(n(suc(X5)),B))=fail(n(suc(X5)),B). % 2.18/2.85 0 [] step1(add(add(X,X2),B))=fail(add(X,X2),B). % 2.18/2.85 0 [] step1(add(mul(X,X2),B))=fail(mul(X,X2),B). % 2.18/2.85 0 [] step1(add(e_q(X,X2),B))=fail(e_q(X,X2),B). % 2.18/2.85 0 [] step1(add(v(X),B))=fail(v(X),B). % 2.18/2.85 0 [] step1(mul(n(zero),B2))=n(zero). % 2.18/2.85 0 [] step1(mul(n(suc(X16)),B2))=fail2(n(suc(X16)),B2). % 2.18/2.85 0 [] step1(mul(add(X,X2),B2))=fail2(add(X,X2),B2). % 2.18/2.85 0 [] step1(mul(mul(X,X2),B2))=fail2(mul(X,X2),B2). % 2.18/2.85 0 [] step1(mul(e_q(X,X2),B2))=fail2(e_q(X,X2),B2). % 2.18/2.85 0 [] step1(mul(v(X),B2))=fail2(v(X),B2). % 2.18/2.85 0 [] step1(e_q(A3,B3))=aux5(A3,B3,e_q3(A3,B3)). % 2.18/2.85 0 [] step1(n(X))=n(X). % 2.18/2.85 0 [] step1(v(X))=v(X). % 2.18/2.85 0 [] simp1(add(A,B))=aux6(A,B,y(A)). % 2.18/2.85 0 [] simp1(mul(C,B2))=aux7(C,B2,x6(C)). % 2.18/2.85 0 [] simp1(e_q(A2,B3))=aux8(A2,B3,e_q3(a3(A2),b3(B3))). % 2.18/2.85 0 [] simp1(n(X))=n(X). % 2.18/2.85 0 [] simp1(v(X))=v(X). % 2.18/2.85 0 [] fetch(nil,Y)=zero. % 2.18/2.85 0 [] fetch(cons(N,St),zero)=N. % 2.18/2.85 0 [] fetch(cons(N,St),suc(Z))=fetch(St,Z). % 2.18/2.85 0 [] addNat(zero,Y)=Y. % 2.18/2.85 0 [] addNat(suc(Z),Y)=suc(addNat(Z,Y)). % 2.18/2.85 0 [] mulNat(zero,Y)=zero. % 2.18/2.85 0 [] mulNat(suc(Z),Y)=addNat(Y,mulNat(Z,Y)). % 2.18/2.85 0 [] eval(X,n(N))=N. % 2.18/2.85 0 [] eval(X,add(A,B))=addNat(eval(X,A),eval(X,B)). % 2.18/2.85 0 [] eval(X,mul(C,B2))=mulNat(eval(X,C),eval(X,B2)). % 2.18/2.85 0 [] eval(X,e_q(A2,B3))=aux9(X,A2,B3,e_q2(eval(X,A2),eval(X,B3))). % 2.18/2.85 0 [] eval(X,v(Z))=fetch(X,Z). % 2.18/2.85 0 [] prop1(X,Y)=e_q4(e_q2(eval(X,Y),eval(X,simp1(Y))),btrue). % 2.18/2.85 0 [] e_q4(bfalse,btrue)=bfalse. % 2.18/2.85 0 [] e_q4(btrue,bfalse)=bfalse. % 2.18/2.85 0 [] e_q3(n(X),n(Y))=e_q2(X,Y). % 2.18/2.85 0 [] e_q3(X,Z)!=bfalse|e_q3(add(X,Y),add(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(X,Z)!=btrue|e_q3(add(X,Y),add(Z,X2))=e_q3(Y,X2). % 2.18/2.85 0 [] e_q3(X,Z)!=bfalse|e_q3(mul(X,Y),mul(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(X,Z)!=btrue|e_q3(mul(X,Y),mul(Z,X2))=e_q3(Y,X2). % 2.18/2.85 0 [] e_q3(X,Z)!=bfalse|e_q3(e_q(X,Y),e_q(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(X,Z)!=btrue|e_q3(e_q(X,Y),e_q(Z,X2))=e_q3(Y,X2). % 2.18/2.85 0 [] e_q3(v(X),v(Y))=e_q2(X,Y). % 2.18/2.85 0 [] e_q3(n(X),add(Y,Z))=bfalse. % 2.18/2.85 0 [] e_q3(n(X),mul(Y,Z))=bfalse. % 2.18/2.85 0 [] e_q3(n(X),e_q(Y,Z))=bfalse. % 2.18/2.85 0 [] e_q3(n(X),v(Y))=bfalse. % 2.18/2.85 0 [] e_q3(add(X,Y),n(Z))=bfalse. % 2.18/2.85 0 [] e_q3(add(X,Y),mul(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(add(X,Y),e_q(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(add(X,Y),v(Z))=bfalse. % 2.18/2.85 0 [] e_q3(mul(X,Y),n(Z))=bfalse. % 2.18/2.85 0 [] e_q3(mul(X,Y),add(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(mul(X,Y),e_q(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(mul(X,Y),v(Z))=bfalse. % 2.18/2.85 0 [] e_q3(e_q(X,Y),n(Z))=bfalse. % 2.18/2.85 0 [] e_q3(e_q(X,Y),add(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(e_q(X,Y),mul(Z,X2))=bfalse. % 2.18/2.85 0 [] e_q3(e_q(X,Y),v(Z))=bfalse. % 2.18/2.85 0 [] e_q3(v(X),n(Y))=bfalse. % 2.18/2.85 0 [] e_q3(v(X),add(Y,Z))=bfalse. % 2.18/2.85 0 [] e_q3(v(X),mul(Y,Z))=bfalse. % 2.18/2.85 0 [] e_q3(v(X),e_q(Y,Z))=bfalse. % 2.18/2.85 0 [] e_q2(suc(X),suc(Y))=e_q2(X,Y). % 2.18/2.85 0 [] e_q2(zero,suc(X))=bfalse. % 2.18/2.85 0 [] e_q2(suc(X),zero)=bfalse. % 2.18/2.85 0 [] e_q2(X,X)=btrue. % 2.18/2.85 0 [] e_q3(X,X)=btrue. % 2.18/2.85 0 [] e_q4(X,X)=btrue. % 2.18/2.85 0 [] e_q4(prop1(X,Y),bfalse)!=btrue. % 2.18/2.85 end_of_list. % 2.18/2.85 % 2.18/2.85 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 2.18/2.85 % 2.18/2.85 This is a Horn set with equality. The strategy will be % 2.18/2.85 Knuth-Bendix and hyper_res, with positive clauses in % 2.18/2.85 sos and nonpositive clauses in usable. % 2.18/2.85 % 2.18/2.85 dependent: set(knuth_bendix). % 2.18/2.85 dependent: set(anl_eq). % 2.18/2.85 dependent: set(para_from). % 2.18/2.85 dependent: set(para_into). % 2.18/2.85 dependent: clear(para_from_right). % 2.18/2.85 dependent: clear(para_into_right). % 2.18/2.85 dependent: set(para_from_vars). % 2.18/2.85 dependent: set(eq_units_both_ways). % 2.18/2.85 dependent: set(dynamic_demod_all). % 2.18/2.85 dependent: set(dynamic_demod). % 2.18/2.85 dependent: set(order_eq). % 2.18/2.85 dependent: set(back_demod). % 2.18/2.85 dependent: set(lrpo). % 2.18/2.85 dependent: set(hyper_res). % 2.18/2.85 dependent: clear(order_hyper). % 2.18/2.85 % 2.18/2.85 ------------> process usable: % 2.18/2.85 ** KEPT (pick-wt=14): 1 [] e_q3(A,B)!=bfalse|e_q3(add(A,C),add(B,D))=bfalse. % 2.18/2.85 ** KEPT (pick-wt=16): 2 [] e_q3(A,B)!=btrue|e_q3(add(A,C),add(B,D))=e_q3(C,D). % 2.18/2.85 ** KEPT (pick-wt=14): 3 [] e_q3(A,B)!=bfalse|e_q3(mul(A,C),mul(B,D))=bfalse. % 2.18/2.85 ** KEPT (pick-wt=16): 4 [] e_q3(A,B)!=btrue|e_q3(mul(A,C),mul(B,D))=e_q3(C,D). % 2.18/2.85 ** KEPT (pick-wt=14): 5 [] e_q3(A,B)!=bfalse|e_q3(e_q(A,C),e_q(B,D))=bfalse. % 2.18/2.85 ** KEPT (pick-wt=16): 6 [] e_q3(A,B)!=btrue|e_q3(e_q(A,C),e_q(B,D))=e_q3(C,D). % 2.18/2.85 ** KEPT (pick-wt=7): 7 [] e_q4(prop1(A,B),bfalse)!=btrue. % 2.18/2.85 % 2.18/2.85 ------------> process sos: % 2.18/2.85 ** KEPT (pick-wt=3): 8 [] A=A. % 2.18/2.85 ** KEPT (pick-wt=12): 9 [] aux(A,B,btrue)=mul(n(suc(suc(zero))),v(A)). % 2.18/2.85 ** KEPT (pick-wt=10): 11 [copy,10,flip.1] add(v(A),v(B))=aux(A,B,bfalse). % 2.18/2.85 ---> New Demodulator: 12 [new_demod,11] add(v(A),v(B))=aux(A,B,bfalse). % 2.18/2.85 ** KEPT (pick-wt=11): 13 [] aux2(A,B,btrue)=mul(n(suc(suc(zero))),A). % 2.18/2.85 ** KEPT (pick-wt=12): 15 [copy,14,flip.1] add(A,add(B,C))=aux2(add(A,B),C,bfalse). % 2.18/2.85 ---> New Demodulator: 16 [new_demod,15] add(A,add(B,C))=aux2(add(A,B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=13): 17 [] aux2(v(A),v(B),bfalse)=aux(A,B,e_q2(A,A)). % 2.18/2.85 ---> New Demodulator: 18 [new_demod,17] aux2(v(A),v(B),bfalse)=aux(A,B,e_q2(A,A)). % 2.18/2.85 ** KEPT (pick-wt=12): 20 [copy,19,flip.1] add(v(A),n(B))=aux2(v(A),n(B),bfalse). % 2.18/2.85 ---> New Demodulator: 21 [new_demod,20] add(v(A),n(B))=aux2(v(A),n(B),bfalse). % 2.18/2.85 ** KEPT (pick-wt=15): 23 [copy,22,demod,16] aux2(v(A),add(B,C),bfalse)=aux2(add(v(A),B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=14): 25 [copy,24,flip.1] add(v(A),mul(B,C))=aux2(v(A),mul(B,C),bfalse). % 2.18/2.85 ---> New Demodulator: 26 [new_demod,25] add(v(A),mul(B,C))=aux2(v(A),mul(B,C),bfalse). % 2.18/2.85 ** KEPT (pick-wt=14): 28 [copy,27,flip.1] add(v(A),e_q(B,C))=aux2(v(A),e_q(B,C),bfalse). % 2.18/2.85 ---> New Demodulator: 29 [new_demod,28] add(v(A),e_q(B,C))=aux2(v(A),e_q(B,C),bfalse). % 2.18/2.85 ** KEPT (pick-wt=10): 31 [copy,30,flip.1] add(n(A),B)=aux2(n(A),B,bfalse). % 2.18/2.85 ---> New Demodulator: 32 [new_demod,31] add(n(A),B)=aux2(n(A),B,bfalse). % 2.18/2.85 ** KEPT (pick-wt=12): 34 [copy,33,flip.1] add(mul(A,B),C)=aux2(mul(A,B),C,bfalse). % 2.18/2.85 ---> New Demodulator: 35 [new_demod,34] add(mul(A,B),C)=aux2(mul(A,B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=12): 37 [copy,36,flip.1] add(e_q(A,B),C)=aux2(e_q(A,B),C,bfalse). % 2.18/2.85 ---> New Demodulator: 38 [new_demod,37] add(e_q(A,B),C)=aux2(e_q(A,B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=12): 39 [] aux3(A,B,btrue)=mul(n(suc(suc(zero))),v(A)). % 2.18/2.85 ** KEPT (pick-wt=9): 41 [copy,40,demod,12] aux3(A,B,bfalse)=aux(A,B,bfalse). % 2.18/2.85 ---> New Demodulator: 42 [new_demod,41] aux3(A,B,bfalse)=aux(A,B,bfalse). % 2.18/2.85 ** KEPT (pick-wt=11): 43 [] aux4(A,B,btrue)=mul(n(suc(suc(zero))),A). % 2.18/2.85 ** KEPT (pick-wt=13): 45 [copy,44,demod,16] aux4(add(A,B),C,bfalse)=aux2(add(A,B),C,bfalse). % 2.18/2.85 ---> New Demodulator: 46 [new_demod,45] aux4(add(A,B),C,bfalse)=aux2(add(A,B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=13): 47 [] aux4(v(A),v(B),bfalse)=aux3(A,B,e_q2(A,A)). % 2.18/2.85 ---> New Demodulator: 48 [new_demod,47] aux4(v(A),v(B),bfalse)=aux3(A,B,e_q2(A,A)). % 2.18/2.85 ** KEPT (pick-wt=13): 50 [copy,49,demod,21] aux4(v(A),n(B),bfalse)=aux2(v(A),n(B),bfalse). % 2.18/2.85 ---> New Demodulator: 51 [new_demod,50] aux4(v(A),n(B),bfalse)=aux2(v(A),n(B),bfalse). % 2.18/2.85 ** KEPT (pick-wt=15): 53 [copy,52,demod,16] aux4(v(A),add(B,C),bfalse)=aux2(add(v(A),B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=15): 55 [copy,54,demod,26] aux4(v(A),mul(B,C),bfalse)=aux2(v(A),mul(B,C),bfalse). % 2.18/2.85 ---> New Demodulator: 56 [new_demod,55] aux4(v(A),mul(B,C),bfalse)=aux2(v(A),mul(B,C),bfalse). % 2.18/2.85 ** KEPT (pick-wt=15): 58 [copy,57,demod,29] aux4(v(A),e_q(B,C),bfalse)=aux2(v(A),e_q(B,C),bfalse). % 2.18/2.85 ---> New Demodulator: 59 [new_demod,58] aux4(v(A),e_q(B,C),bfalse)=aux2(v(A),e_q(B,C),bfalse). % 2.18/2.85 ** KEPT (pick-wt=11): 61 [copy,60,demod,32] aux4(n(A),B,bfalse)=aux2(n(A),B,bfalse). % 2.18/2.85 ---> New Demodulator: 62 [new_demod,61] aux4(n(A),B,bfalse)=aux2(n(A),B,bfalse). % 2.18/2.85 ** KEPT (pick-wt=13): 64 [copy,63,demod,35] aux4(mul(A,B),C,bfalse)=aux2(mul(A,B),C,bfalse). % 2.18/2.85 ---> New Demodulator: 65 [new_demod,64] aux4(mul(A,B),C,bfalse)=aux2(mul(A,B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=13): 67 [copy,66,demod,38] aux4(e_q(A,B),C,bfalse)=aux2(e_q(A,B),C,bfalse). % 2.18/2.85 ---> New Demodulator: 68 [new_demod,67] aux4(e_q(A,B),C,bfalse)=aux2(e_q(A,B),C,bfalse). % 2.18/2.85 ** KEPT (pick-wt=8): 69 [] aux5(A,B,btrue)=n(suc(zero)). % 2.18/2.85 ** KEPT (pick-wt=8): 71 [copy,70,flip.1] e_q(A,B)=aux5(A,B,bfalse). % 2.18/2.85 ---> New Demodulator: 72 [new_demod,71] e_q(A,B)=aux5(A,B,bfalse). % 2.18/2.85 ** KEPT (pick-wt=8): 73 [] aux6(A,B,n(zero))=b(B). % 2.18/2.85 ** KEPT (pick-wt=12): 74 [] aux6(A,B,n(suc(C)))=fail4(y(A),b(B)). % 2.18/2.85 ** KEPT (pick-wt=12): 75 [] aux6(A,B,add(C,D))=fail4(y(A),b(B)). % 2.18/2.85 ** KEPT (pick-wt=12): 76 [] aux6(A,B,mul(C,D))=fail4(y(A),b(B)). % 2.18/2.85 ** KEPT (pick-wt=13): 78 [copy,77,demod,72] aux6(A,B,aux5(C,D,bfalse))=fail4(y(A),b(B)). % 2.18/2.85 ** KEPT (pick-wt=11): 79 [] aux6(A,B,v(C))=fail4(y(A),b(B)). % 2.18/2.85 ** KEPT (pick-wt=8): 80 [] aux7(A,B,n(zero))=n(zero). % 2.18/2.85 ---> New Demodulator: 81 [new_demod,80] aux7(A,B,n(zero))=n(zero). % 2.18/2.85 ** KEPT (pick-wt=12): 82 [] aux7(A,B,n(suc(C)))=fail23(x6(A),b2(B)). % 2.18/2.85 ** KEPT (pick-wt=12): 83 [] aux7(A,B,add(C,D))=fail23(x6(A),b2(B)). % 2.18/2.85 ** KEPT (pick-wt=12): 84 [] aux7(A,B,mul(C,D))=fail23(x6(A),b2(B)). % 2.18/2.85 ** KEPT (pick-wt=13): 86 [copy,85,demod,72] aux7(A,B,aux5(C,D,bfalse))=fail23(x6(A),b2(B)). % 2.18/2.85 ** KEPT (pick-wt=11): 87 [] aux7(A,B,v(C))=fail23(x6(A),b2(B)). % 2.18/2.85 ** KEPT (pick-wt=8): 88 [] aux8(A,B,btrue)=n(suc(zero)). % 2.18/2.85 ** KEPT (pick-wt=11): 90 [copy,89,demod,72] aux8(A,B,bfalse)=aux5(a3(A),b3(B),bfalse). % 2.18/2.85 ** KEPT (pick-wt=8): 91 [] aux9(A,B,C,btrue)=suc(zero). % 2.18/2.85 ** KEPT (pick-wt=7): 92 [] aux9(A,B,C,bfalse)=zero. % 2.18/2.85 ---> New Demodulator: 93 [new_demod,92] aux9(A,B,C,bfalse)=zero. % 2.18/2.85 ** KEPT (pick-wt=10): 94 [] fail1(A,B)=aux2(A,B,e_q3(A,B)). % 2.18/2.85 ---> New Demodulator: 95 [new_demod,94] fail1(A,B)=aux2(A,B,e_q3(A,B)). % 2.18/2.85 ** KEPT (pick-wt=6): 96 [] fail(A,n(zero))=A. % 2.18/2.85 ---> New Demodulator: 97 [new_demod,96] fail(A,n(zero))=A. % 2.18/2.85 ** KEPT (pick-wt=16): 99 [copy,98,demod,95] fail(A,n(suc(B)))=aux2(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.18/2.85 ---> New Demodulator: 100 [new_demod,99] fail(A,n(suc(B)))=aux2(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.18/2.85 ** KEPT (pick-wt=16): 102 [copy,101,demod,95] fail(A,add(B,C))=aux2(A,add(B,C),e_q3(A,add(B,C))). % 2.18/2.85 ---> New Demodulator: 103 [new_demod,102] fail(A,add(B,C))=aux2(A,add(B,C),e_q3(A,add(B,C))). % 2.18/2.85 ** KEPT (pick-wt=16): 105 [copy,104,demod,95] fail(A,mul(B,C))=aux2(A,mul(B,C),e_q3(A,mul(B,C))). % 2.18/2.85 ---> New Demodulator: 106 [new_demod,105] fail(A,mul(B,C))=aux2(A,mul(B,C),e_q3(A,mul(B,C))). % 2.18/2.85 ** KEPT (pick-wt=19): 108 [copy,107,demod,72,72,95] fail(A,aux5(B,C,bfalse))=aux2(A,aux5(B,C,bfalse),e_q3(A,aux5(B,C,bfalse))). % 2.18/2.85 ---> New Demodulator: 109 [new_demod,108] fail(A,aux5(B,C,bfalse))=aux2(A,aux5(B,C,bfalse),e_q3(A,aux5(B,C,bfalse))). % 2.18/2.85 ** KEPT (pick-wt=13): 111 [copy,110,demod,95] fail(A,v(B))=aux2(A,v(B),e_q3(A,v(B))). % 2.18/2.85 ---> New Demodulator: 112 [new_demod,111] fail(A,v(B))=aux2(A,v(B),e_q3(A,v(B))). % 2.18/2.85 ** KEPT (pick-wt=11): 114 [copy,113,flip.1] mul(A,mul(B,C))=fail3(mul(A,B),C). % 2.18/2.85 ---> New Demodulator: 115 [new_demod,114] mul(A,mul(B,C))=fail3(mul(A,B),C). % 2.18/2.85 ** KEPT (pick-wt=9): 117 [copy,116,flip.1] mul(n(A),B)=fail3(n(A),B). % 2.18/2.85 ---> New Demodulator: 118 [new_demod,117] mul(n(A),B)=fail3(n(A),B). % 2.18/2.85 ** KEPT (pick-wt=11): 120 [copy,119,flip.1] mul(add(A,B),C)=fail3(add(A,B),C). % 2.18/2.85 ---> New Demodulator: 121 [new_demod,120] mul(add(A,B),C)=fail3(add(A,B),C). % 2.18/2.85 ** KEPT (pick-wt=13): 123 [copy,122,demod,72,72,flip.1] mul(aux5(A,B,bfalse),C)=fail3(aux5(A,B,bfalse),C). % 2.18/2.85 ---> New Demodulator: 124 [new_demod,123] mul(aux5(A,B,bfalse),C)=fail3(aux5(A,B,bfalse),C). % 2.18/2.85 ** KEPT (pick-wt=9): 126 [copy,125,flip.1] mul(v(A),B)=fail3(v(A),B). % 2.18/2.85 ---> New Demodulator: 127 [new_demod,126] mul(v(A),B)=fail3(v(A),B). % 2.18/2.86 ** KEPT (pick-wt=9): 129 [copy,128,flip.1] fail3(A,n(zero))=fail22(A,n(zero)). % 2.18/2.86 ---> New Demodulator: 130 [new_demod,129] fail3(A,n(zero))=fail22(A,n(zero)). % 2.18/2.86 ** KEPT (pick-wt=7): 131 [] fail22(A,n(suc(zero)))=A. % 2.18/2.86 ---> New Demodulator: 132 [new_demod,131] fail22(A,n(suc(zero)))=A. % 2.18/2.86 ** KEPT (pick-wt=13): 134 [copy,133,flip.1] fail3(A,n(suc(suc(B))))=fail22(A,n(suc(suc(B)))). % 2.18/2.86 ---> New Demodulator: 135 [new_demod,134] fail3(A,n(suc(suc(B))))=fail22(A,n(suc(suc(B)))). % 2.18/2.86 ** KEPT (pick-wt=11): 137 [copy,136,flip.1] fail3(A,add(B,C))=fail22(A,add(B,C)). % 2.18/2.86 ---> New Demodulator: 138 [new_demod,137] fail3(A,add(B,C))=fail22(A,add(B,C)). % 2.18/2.86 ** KEPT (pick-wt=11): 140 [copy,139,flip.1] fail3(A,mul(B,C))=fail22(A,mul(B,C)). % 2.18/2.86 ---> New Demodulator: 141 [new_demod,140] fail3(A,mul(B,C))=fail22(A,mul(B,C)). % 2.18/2.86 ** KEPT (pick-wt=13): 143 [copy,142,demod,72,72,flip.1] fail3(A,aux5(B,C,bfalse))=fail22(A,aux5(B,C,bfalse)). % 2.18/2.86 ---> New Demodulator: 144 [new_demod,143] fail3(A,aux5(B,C,bfalse))=fail22(A,aux5(B,C,bfalse)). % 2.18/2.86 ** KEPT (pick-wt=9): 146 [copy,145,flip.1] fail3(A,v(B))=fail22(A,v(B)). % 2.18/2.86 ---> New Demodulator: 147 [new_demod,146] fail3(A,v(B))=fail22(A,v(B)). % 2.18/2.86 ** KEPT (pick-wt=9): 149 [copy,148,flip.1] fail22(n(zero),A)=fail12(n(zero),A). % 2.18/2.86 ---> New Demodulator: 150 [new_demod,149] fail22(n(zero),A)=fail12(n(zero),A). % 2.18/2.86 ** KEPT (pick-wt=7): 151 [] fail12(n(suc(zero)),A)=A. % 2.18/2.86 ---> New Demodulator: 152 [new_demod,151] fail12(n(suc(zero)),A)=A. % 2.18/2.86 ** KEPT (pick-wt=13): 154 [copy,153,flip.1] fail22(n(suc(suc(A))),B)=fail12(n(suc(suc(A))),B). % 2.18/2.86 ---> New Demodulator: 155 [new_demod,154] fail22(n(suc(suc(A))),B)=fail12(n(suc(suc(A))),B). % 2.18/2.86 ** KEPT (pick-wt=11): 157 [copy,156,flip.1] fail22(add(A,B),C)=fail12(add(A,B),C). % 2.18/2.86 ---> New Demodulator: 158 [new_demod,157] fail22(add(A,B),C)=fail12(add(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=11): 160 [copy,159,flip.1] fail22(mul(A,B),C)=fail12(mul(A,B),C). % 2.18/2.86 ---> New Demodulator: 161 [new_demod,160] fail22(mul(A,B),C)=fail12(mul(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=13): 163 [copy,162,demod,72,72,flip.1] fail22(aux5(A,B,bfalse),C)=fail12(aux5(A,B,bfalse),C). % 2.18/2.86 ---> New Demodulator: 164 [new_demod,163] fail22(aux5(A,B,bfalse),C)=fail12(aux5(A,B,bfalse),C). % 2.18/2.86 ** KEPT (pick-wt=9): 166 [copy,165,flip.1] fail22(v(A),B)=fail12(v(A),B). % 2.18/2.86 ---> New Demodulator: 167 [new_demod,166] fail22(v(A),B)=fail12(v(A),B). % 2.18/2.86 ** KEPT (pick-wt=7): 168 [] fail2(A,n(zero))=n(zero). % 2.18/2.86 ---> New Demodulator: 169 [new_demod,168] fail2(A,n(zero))=n(zero). % 2.18/2.86 ** KEPT (pick-wt=11): 170 [] fail2(A,n(suc(B)))=fail12(A,n(suc(B))). % 2.18/2.86 ---> New Demodulator: 171 [new_demod,170] fail2(A,n(suc(B)))=fail12(A,n(suc(B))). % 2.18/2.86 ** KEPT (pick-wt=11): 172 [] fail2(A,add(B,C))=fail12(A,add(B,C)). % 2.18/2.86 ---> New Demodulator: 173 [new_demod,172] fail2(A,add(B,C))=fail12(A,add(B,C)). % 2.18/2.86 ** KEPT (pick-wt=11): 174 [] fail2(A,mul(B,C))=fail12(A,mul(B,C)). % 2.18/2.86 ---> New Demodulator: 175 [new_demod,174] fail2(A,mul(B,C))=fail12(A,mul(B,C)). % 2.18/2.86 ** KEPT (pick-wt=13): 177 [copy,176,demod,72,72] fail2(A,aux5(B,C,bfalse))=fail12(A,aux5(B,C,bfalse)). % 2.18/2.86 ---> New Demodulator: 178 [new_demod,177] fail2(A,aux5(B,C,bfalse))=fail12(A,aux5(B,C,bfalse)). % 2.18/2.86 ** KEPT (pick-wt=9): 179 [] fail2(A,v(B))=fail12(A,v(B)). % 2.18/2.86 ---> New Demodulator: 180 [new_demod,179] fail2(A,v(B))=fail12(A,v(B)). % 2.18/2.86 ** KEPT (pick-wt=10): 181 [] fail13(A,B)=aux4(A,B,e_q3(A,B)). % 2.18/2.86 ---> New Demodulator: 182 [new_demod,181] fail13(A,B)=aux4(A,B,e_q3(A,B)). % 2.18/2.86 ** KEPT (pick-wt=6): 183 [] fail4(A,n(zero))=A. % 2.18/2.86 ---> New Demodulator: 184 [new_demod,183] fail4(A,n(zero))=A. % 2.18/2.86 ** KEPT (pick-wt=16): 186 [copy,185,demod,182] fail4(A,n(suc(B)))=aux4(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.18/2.86 ---> New Demodulator: 187 [new_demod,186] fail4(A,n(suc(B)))=aux4(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.18/2.86 ** KEPT (pick-wt=16): 189 [copy,188,demod,182] fail4(A,add(B,C))=aux4(A,add(B,C),e_q3(A,add(B,C))). % 2.18/2.86 ---> New Demodulator: 190 [new_demod,189] fail4(A,add(B,C))=aux4(A,add(B,C),e_q3(A,add(B,C))). % 2.18/2.86 ** KEPT (pick-wt=16): 192 [copy,191,demod,182] fail4(A,mul(B,C))=aux4(A,mul(B,C),e_q3(A,mul(B,C))). % 2.18/2.86 ---> New Demodulator: 193 [new_demod,192] fail4(A,mul(B,C))=aux4(A,mul(B,C),e_q3(A,mul(B,C))). % 2.18/2.86 ** KEPT (pick-wt=19): 195 [copy,194,demod,72,72,182] fail4(A,aux5(B,C,bfalse))=aux4(A,aux5(B,C,bfalse),e_q3(A,aux5(B,C,bfalse))). % 2.18/2.86 ---> New Demodulator: 196 [new_demod,195] fail4(A,aux5(B,C,bfalse))=aux4(A,aux5(B,C,bfalse),e_q3(A,aux5(B,C,bfalse))). % 2.18/2.86 ** KEPT (pick-wt=13): 198 [copy,197,demod,182] fail4(A,v(B))=aux4(A,v(B),e_q3(A,v(B))). % 2.18/2.86 ---> New Demodulator: 199 [new_demod,198] fail4(A,v(B))=aux4(A,v(B),e_q3(A,v(B))). % 2.18/2.86 ** KEPT (pick-wt=5): 201 [copy,200,flip.1] simp1(A)=b(A). % 2.18/2.86 ---> New Demodulator: 202 [new_demod,201] simp1(A)=b(A). % 2.18/2.86 ** KEPT (pick-wt=5): 204 [copy,203,demod,202] y(A)=b(A). % 2.18/2.86 ---> New Demodulator: 205 [new_demod,204] y(A)=b(A). % 2.18/2.86 ** KEPT (pick-wt=11): 207 [copy,206,demod,115] fail32(mul(A,B),C)=fail3(mul(A,B),C). % 2.18/2.86 ---> New Demodulator: 208 [new_demod,207] fail32(mul(A,B),C)=fail3(mul(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=9): 210 [copy,209,demod,118] fail32(n(A),B)=fail3(n(A),B). % 2.18/2.86 ---> New Demodulator: 211 [new_demod,210] fail32(n(A),B)=fail3(n(A),B). % 2.18/2.86 ** KEPT (pick-wt=11): 213 [copy,212,demod,121] fail32(add(A,B),C)=fail3(add(A,B),C). % 2.18/2.86 ---> New Demodulator: 214 [new_demod,213] fail32(add(A,B),C)=fail3(add(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=13): 216 [copy,215,demod,72,72,124] fail32(aux5(A,B,bfalse),C)=fail3(aux5(A,B,bfalse),C). % 2.18/2.86 ---> New Demodulator: 217 [new_demod,216] fail32(aux5(A,B,bfalse),C)=fail3(aux5(A,B,bfalse),C). % 2.18/2.86 ** KEPT (pick-wt=9): 219 [copy,218,demod,127] fail32(v(A),B)=fail3(v(A),B). % 2.18/2.86 ---> New Demodulator: 220 [new_demod,219] fail32(v(A),B)=fail3(v(A),B). % 2.18/2.86 ** KEPT (pick-wt=9): 222 [copy,221,flip.1] fail32(A,n(zero))=fail222(A,n(zero)). % 2.18/2.86 ---> New Demodulator: 223 [new_demod,222] fail32(A,n(zero))=fail222(A,n(zero)). % 2.18/2.86 ** KEPT (pick-wt=7): 224 [] fail222(A,n(suc(zero)))=A. % 2.18/2.86 ---> New Demodulator: 225 [new_demod,224] fail222(A,n(suc(zero)))=A. % 2.18/2.86 ** KEPT (pick-wt=13): 227 [copy,226,flip.1] fail32(A,n(suc(suc(B))))=fail222(A,n(suc(suc(B)))). % 2.18/2.86 ---> New Demodulator: 228 [new_demod,227] fail32(A,n(suc(suc(B))))=fail222(A,n(suc(suc(B)))). % 2.18/2.86 ** KEPT (pick-wt=11): 230 [copy,229,flip.1] fail32(A,add(B,C))=fail222(A,add(B,C)). % 2.18/2.86 ---> New Demodulator: 231 [new_demod,230] fail32(A,add(B,C))=fail222(A,add(B,C)). % 2.18/2.86 ** KEPT (pick-wt=11): 233 [copy,232,flip.1] fail32(A,mul(B,C))=fail222(A,mul(B,C)). % 2.18/2.86 ---> New Demodulator: 234 [new_demod,233] fail32(A,mul(B,C))=fail222(A,mul(B,C)). % 2.18/2.86 ** KEPT (pick-wt=13): 236 [copy,235,demod,72,72,flip.1] fail32(A,aux5(B,C,bfalse))=fail222(A,aux5(B,C,bfalse)). % 2.18/2.86 ---> New Demodulator: 237 [new_demod,236] fail32(A,aux5(B,C,bfalse))=fail222(A,aux5(B,C,bfalse)). % 2.18/2.86 ** KEPT (pick-wt=9): 239 [copy,238,flip.1] fail32(A,v(B))=fail222(A,v(B)). % 2.18/2.86 ---> New Demodulator: 240 [new_demod,239] fail32(A,v(B))=fail222(A,v(B)). % 2.18/2.86 ** KEPT (pick-wt=9): 242 [copy,241,flip.1] fail222(n(zero),A)=fail122(n(zero),A). % 2.18/2.86 ---> New Demodulator: 243 [new_demod,242] fail222(n(zero),A)=fail122(n(zero),A). % 2.18/2.86 ** KEPT (pick-wt=7): 244 [] fail122(n(suc(zero)),A)=A. % 2.18/2.86 ---> New Demodulator: 245 [new_demod,244] fail122(n(suc(zero)),A)=A. % 2.18/2.86 ** KEPT (pick-wt=13): 247 [copy,246,flip.1] fail222(n(suc(suc(A))),B)=fail122(n(suc(suc(A))),B). % 2.18/2.86 ---> New Demodulator: 248 [new_demod,247] fail222(n(suc(suc(A))),B)=fail122(n(suc(suc(A))),B). % 2.18/2.86 ** KEPT (pick-wt=11): 250 [copy,249,flip.1] fail222(add(A,B),C)=fail122(add(A,B),C). % 2.18/2.86 ---> New Demodulator: 251 [new_demod,250] fail222(add(A,B),C)=fail122(add(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=11): 253 [copy,252,flip.1] fail222(mul(A,B),C)=fail122(mul(A,B),C). % 2.18/2.86 ---> New Demodulator: 254 [new_demod,253] fail222(mul(A,B),C)=fail122(mul(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=13): 256 [copy,255,demod,72,72,flip.1] fail222(aux5(A,B,bfalse),C)=fail122(aux5(A,B,bfalse),C). % 2.18/2.86 ---> New Demodulator: 257 [new_demod,256] fail222(aux5(A,B,bfalse),C)=fail122(aux5(A,B,bfalse),C). % 2.18/2.86 ** KEPT (pick-wt=9): 259 [copy,258,flip.1] fail222(v(A),B)=fail122(v(A),B). % 2.18/2.86 ---> New Demodulator: 260 [new_demod,259] fail222(v(A),B)=fail122(v(A),B). % 2.18/2.86 ** KEPT (pick-wt=7): 261 [] fail23(A,n(zero))=n(zero). % 2.18/2.86 ---> New Demodulator: 262 [new_demod,261] fail23(A,n(zero))=n(zero). % 2.18/2.86 ** KEPT (pick-wt=11): 263 [] fail23(A,n(suc(B)))=fail122(A,n(suc(B))). % 2.18/2.86 ---> New Demodulator: 264 [new_demod,263] fail23(A,n(suc(B)))=fail122(A,n(suc(B))). % 2.18/2.86 ** KEPT (pick-wt=11): 265 [] fail23(A,add(B,C))=fail122(A,add(B,C)). % 2.18/2.86 ---> New Demodulator: 266 [new_demod,265] fail23(A,add(B,C))=fail122(A,add(B,C)). % 2.18/2.86 ** KEPT (pick-wt=11): 267 [] fail23(A,mul(B,C))=fail122(A,mul(B,C)). % 2.18/2.86 ---> New Demodulator: 268 [new_demod,267] fail23(A,mul(B,C))=fail122(A,mul(B,C)). % 2.18/2.86 ** KEPT (pick-wt=13): 270 [copy,269,demod,72,72] fail23(A,aux5(B,C,bfalse))=fail122(A,aux5(B,C,bfalse)). % 2.18/2.86 ---> New Demodulator: 271 [new_demod,270] fail23(A,aux5(B,C,bfalse))=fail122(A,aux5(B,C,bfalse)). % 2.18/2.86 ** KEPT (pick-wt=9): 272 [] fail23(A,v(B))=fail122(A,v(B)). % 2.18/2.86 ---> New Demodulator: 273 [new_demod,272] fail23(A,v(B))=fail122(A,v(B)). % 2.18/2.86 ** KEPT (pick-wt=5): 275 [copy,274,demod,202] b2(A)=b(A). % 2.18/2.86 ---> New Demodulator: 276 [new_demod,275] b2(A)=b(A). % 2.18/2.86 ** KEPT (pick-wt=5): 278 [copy,277,demod,202] x6(A)=b(A). % 2.18/2.86 ---> New Demodulator: 279 [new_demod,278] x6(A)=b(A). % 2.18/2.86 ** KEPT (pick-wt=5): 281 [copy,280,demod,202] b3(A)=b(A). % 2.18/2.86 ---> New Demodulator: 282 [new_demod,281] b3(A)=b(A). % 2.18/2.86 ** KEPT (pick-wt=5): 284 [copy,283,demod,202,flip.1] b(A)=a3(A). % 2.18/2.86 ---> New Demodulator: 285 [new_demod,284] b(A)=a3(A). % 2.18/2.86 ** KEPT (pick-wt=8): 287 [copy,286,demod,32] step1(aux2(n(zero),A,bfalse))=A. % 2.18/2.86 ---> New Demodulator: 288 [new_demod,287] step1(aux2(n(zero),A,bfalse))=A. % 2.18/2.86 ** KEPT (pick-wt=13): 290 [copy,289,demod,32] step1(aux2(n(suc(A)),B,bfalse))=fail(n(suc(A)),B). % 2.18/2.86 ---> New Demodulator: 291 [new_demod,290] step1(aux2(n(suc(A)),B,bfalse))=fail(n(suc(A)),B). % 2.18/2.86 ** KEPT (pick-wt=12): 292 [] step1(add(add(A,B),C))=fail(add(A,B),C). % 2.18/2.86 ---> New Demodulator: 293 [new_demod,292] step1(add(add(A,B),C))=fail(add(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=13): 295 [copy,294,demod,35] step1(aux2(mul(A,B),C,bfalse))=fail(mul(A,B),C). % 2.18/2.86 ---> New Demodulator: 296 [new_demod,295] step1(aux2(mul(A,B),C,bfalse))=fail(mul(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=14): 298 [copy,297,demod,72,72] step1(add(aux5(A,B,bfalse),C))=fail(aux5(A,B,bfalse),C). % 2.18/2.86 ---> New Demodulator: 299 [new_demod,298] step1(add(aux5(A,B,bfalse),C))=fail(aux5(A,B,bfalse),C). % 2.18/2.86 ** KEPT (pick-wt=10): 300 [] step1(add(v(A),B))=fail(v(A),B). % 2.18/2.86 ---> New Demodulator: 301 [new_demod,300] step1(add(v(A),B))=fail(v(A),B). % 2.18/2.86 ** KEPT (pick-wt=8): 303 [copy,302,demod,118] step1(fail3(n(zero),A))=n(zero). % 2.18/2.86 ---> New Demodulator: 304 [new_demod,303] step1(fail3(n(zero),A))=n(zero). % 2.18/2.86 ** KEPT (pick-wt=12): 306 [copy,305,demod,118] step1(fail3(n(suc(A)),B))=fail2(n(suc(A)),B). % 2.18/2.86 ---> New Demodulator: 307 [new_demod,306] step1(fail3(n(suc(A)),B))=fail2(n(suc(A)),B). % 2.18/2.86 ** KEPT (pick-wt=12): 309 [copy,308,demod,121] step1(fail3(add(A,B),C))=fail2(add(A,B),C). % 2.18/2.86 ---> New Demodulator: 310 [new_demod,309] step1(fail3(add(A,B),C))=fail2(add(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=12): 311 [] step1(mul(mul(A,B),C))=fail2(mul(A,B),C). % 2.18/2.86 ---> New Demodulator: 312 [new_demod,311] step1(mul(mul(A,B),C))=fail2(mul(A,B),C). % 2.18/2.86 ** KEPT (pick-wt=14): 314 [copy,313,demod,72,124,72] step1(fail3(aux5(A,B,bfalse),C))=fail2(aux5(A,B,bfalse),C). % 2.18/2.86 ---> New Demodulator: 315 [new_demod,314] step1(fail3(aux5(A,B,bfalse),C))=fail2(aux5(A,B,bfalse),C). % 2.18/2.86 ** KEPT (pick-wt=10): 317 [copy,316,demod,127] step1(fail3(v(A),B))=fail2(v(A),B). % 2.18/2.86 ---> New Demodulator: 318 [new_demod,317] step1(fail3(v(A),B))=fail2(v(A),B). % 2.18/2.86 ** KEPT (pick-wt=12): 320 [copy,319,demod,72] step1(aux5(A,B,bfalse))=aux5(A,B,e_q3(A,B)). % 2.18/2.86 ---> New Demodulator: 321 [new_demod,320] step1(aux5(A,B,bfalse))=aux5(A,B,e_q3(A,B)). % 2.18/2.86 ** KEPT (pick-wt=6): 322 [] step1(n(A))=n(A). % 2.18/2.86 ---> New Demodulator: 323 [new_demod,322] step1(n(A))=n(A). % 2.18/2.86 ** KEPT (pick-wt=6): 324 [] step1(v(A))=v(A). % 2.18/2.86 ---> New Demodulator: 325 [new_demod,324] step1(v(A))=v(A). % 2.18/2.86 ** KEPT (pick-wt=10): 327 [copy,326,demod,202,285,205,285] a3(add(A,B))=aux6(A,B,a3(A)). % 2.18/2.86 ---> New Demodulator: 328 [new_demod,327] a3(add(A,B))=aux6(A,B,a3(A)). % 2.18/2.86 ** KEPT (pick-wt=10): 330 [copy,329,demod,202,285,279,285] a3(mul(A,B))=aux7(A,B,a3(A)). % 2.18/2.86 ---> New Demodulator: 331 [new_demod,330] a3(mul(A,B))=aux7(A,B,a3(A)). % 2.18/2.86 ** KEPT (pick-wt=14): 333 [copy,332,demod,72,202,285,282,285] a3(aux5(A,B,bfalse))=aux8(A,B,e_q3(a3(A),a3(B))). % 2.18/2.86 ---> New Demodulator: 334 [new_demod,333] a3(aux5(A,B,bfalse))=aux8(A,B,e_q3(a3(A),a3(B))). % 2.18/2.86 ** KEPT (pick-wt=6): 336 [copy,335,demod,202,285] a3(n(A))=n(A). % 2.18/2.86 ---> New Demodulator: 337 [new_demod,336] a3(n(A))=n(A). % 2.18/2.86 ** KEPT (pick-wt=6): 339 [copy,338,demod,202,285] a3(v(A))=v(A). % 2.18/2.86 ---> New Demodulator: 340 [new_demod,339] a3(v(A))=v(A). % 2.18/2.86 ** KEPT (pick-wt=5): 341 [] fetch(nil,A)=zero. % 2.18/2.86 ---> New Demodulator: 342 [new_demod,341] fetch(nil,A)=zero. % 2.18/2.86 ** KEPT (pick-wt=7): 343 [] fetch(cons(A,B),zero)=A. % 2.18/2.86 ---> New Demodulator: 344 [new_demod,343] fetch(cons(A,B),zero)=A. % 2.18/2.86 ** KEPT (pick-wt=10): 345 [] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.18/2.86 ---> New Demodulator: 346 [new_demod,345] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.18/2.86 ** KEPT (pick-wt=5): 347 [] addNat(zero,A)=A. % 2.18/2.86 ---> New Demodulator: 348 [new_demod,347] addNat(zero,A)=A. % 2.18/2.86 ** KEPT (pick-wt=9): 350 [copy,349,flip.1] suc(addNat(A,B))=addNat(suc(A),B). % 2.18/2.86 ---> New Demodulator: 351 [new_demod,350] suc(addNat(A,B))=addNat(suc(A),B). % 2.18/2.86 ** KEPT (pick-wt=5): 352 [] mulNat(zero,A)=zero. % 2.18/2.86 ---> New Demodulator: 353 [new_demod,352] mulNat(zero,A)=zero. % 2.18/2.86 ** KEPT (pick-wt=10): 354 [] mulNat(suc(A),B)=addNat(B,mulNat(A,B)). % 2.18/2.86 ---> New Demodulator: 355 [new_demod,354] mulNat(suc(A),B)=addNat(B,mulNat(A,B)). % 2.18/2.86 ** KEPT (pick-wt=6): 356 [] eval(A,n(B))=B. % 2.18/2.86 ---> New Demodulator: 357 [new_demod,356] eval(A,n(B))=B. % 2.18/2.86 ** KEPT (pick-wt=13): 358 [] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.18/2.86 ---> New Demodulator: 359 [new_demod,358] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.18/2.86 ** KEPT (pick-wt=13): 361 [copy,360,flip.1] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.18/2.86 ---> New Demodulator: 362 [new_demod,361] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.18/2.86 ** KEPT (pick-wt=18): 364 [copy,363,demod,72] eval(A,aux5(B,C,bfalse))=aux9(A,B,C,e_q2(eval(A,B),eval(A,C))). % 2.18/2.86 ---> New Demodulator: 365 [new_demod,364] eval(A,aux5(B,C,bfalse))=aux9(A,B,C,e_q2(eval(A,B),eval(A,C))). % 2.18/2.86 ** KEPT (pick-wt=8): 366 [] eval(A,v(B))=fetch(A,B). % 2.18/2.86 ** KEPT (pick-wt=14): 368 [copy,367,demod,202,285] prop1(A,B)=e_q4(e_q2(eval(A,B),eval(A,a3(B))),btrue). % 2.18/2.86 ** KEPT (pick-wt=5): 369 [] e_q4(bfalse,btrue)=bfalse. % 2.18/2.86 ---> New Demodulator: 370 [new_demod,369] e_q4(bfalse,btrue)=bfalse. % 2.18/2.86 ** KEPT (pick-wt=5): 371 [] e_q4(btrue,bfalse)=bfalse. % 2.18/2.86 ---> New Demodulator: 372 [new_demod,371] e_q4(btrue,bfalse)=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 373 [] e_q3(n(A),n(B))=e_q2(A,B). % 2.18/2.86 ---> New Demodulator: 374 [new_demod,373] e_q3(n(A),n(B))=e_q2(A,B). % 2.18/2.86 ** KEPT (pick-wt=9): 375 [] e_q3(v(A),v(B))=e_q2(A,B). % 2.18/2.86 ---> New Demodulator: 376 [new_demod,375] e_q3(v(A),v(B))=e_q2(A,B). % 2.18/2.86 ** KEPT (pick-wt=8): 377 [] e_q3(n(A),add(B,C))=bfalse. % 2.18/2.86 ---> New Demodulator: 378 [new_demod,377] e_q3(n(A),add(B,C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=8): 379 [] e_q3(n(A),mul(B,C))=bfalse. % 2.18/2.86 ---> New Demodulator: 380 [new_demod,379] e_q3(n(A),mul(B,C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 382 [copy,381,demod,72] e_q3(n(A),aux5(B,C,bfalse))=bfalse. % 2.18/2.86 ---> New Demodulator: 383 [new_demod,382] e_q3(n(A),aux5(B,C,bfalse))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=7): 384 [] e_q3(n(A),v(B))=bfalse. % 2.18/2.86 ---> New Demodulator: 385 [new_demod,384] e_q3(n(A),v(B))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=8): 386 [] e_q3(add(A,B),n(C))=bfalse. % 2.18/2.86 ---> New Demodulator: 387 [new_demod,386] e_q3(add(A,B),n(C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 388 [] e_q3(add(A,B),mul(C,D))=bfalse. % 2.18/2.86 ---> New Demodulator: 389 [new_demod,388] e_q3(add(A,B),mul(C,D))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=10): 391 [copy,390,demod,72] e_q3(add(A,B),aux5(C,D,bfalse))=bfalse. % 2.18/2.86 ---> New Demodulator: 392 [new_demod,391] e_q3(add(A,B),aux5(C,D,bfalse))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=8): 393 [] e_q3(add(A,B),v(C))=bfalse. % 2.18/2.86 ---> New Demodulator: 394 [new_demod,393] e_q3(add(A,B),v(C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=8): 395 [] e_q3(mul(A,B),n(C))=bfalse. % 2.18/2.86 ---> New Demodulator: 396 [new_demod,395] e_q3(mul(A,B),n(C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 397 [] e_q3(mul(A,B),add(C,D))=bfalse. % 2.18/2.86 ---> New Demodulator: 398 [new_demod,397] e_q3(mul(A,B),add(C,D))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=10): 400 [copy,399,demod,72] e_q3(mul(A,B),aux5(C,D,bfalse))=bfalse. % 2.18/2.86 ---> New Demodulator: 401 [new_demod,400] e_q3(mul(A,B),aux5(C,D,bfalse))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=8): 402 [] e_q3(mul(A,B),v(C))=bfalse. % 2.18/2.86 ---> New Demodulator: 403 [new_demod,402] e_q3(mul(A,B),v(C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 405 [copy,404,demod,72] e_q3(aux5(A,B,bfalse),n(C))=bfalse. % 2.18/2.86 ---> New Demodulator: 406 [new_demod,405] e_q3(aux5(A,B,bfalse),n(C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=10): 408 [copy,407,demod,72] e_q3(aux5(A,B,bfalse),add(C,D))=bfalse. % 2.18/2.86 ---> New Demodulator: 409 [new_demod,408] e_q3(aux5(A,B,bfalse),add(C,D))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=10): 411 [copy,410,demod,72] e_q3(aux5(A,B,bfalse),mul(C,D))=bfalse. % 2.18/2.86 ---> New Demodulator: 412 [new_demod,411] e_q3(aux5(A,B,bfalse),mul(C,D))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 414 [copy,413,demod,72] e_q3(aux5(A,B,bfalse),v(C))=bfalse. % 2.18/2.86 ---> New Demodulator: 415 [new_demod,414] e_q3(aux5(A,B,bfalse),v(C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=7): 416 [] e_q3(v(A),n(B))=bfalse. % 2.18/2.86 ---> New Demodulator: 417 [new_demod,416] e_q3(v(A),n(B))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=8): 418 [] e_q3(v(A),add(B,C))=bfalse. % 2.18/2.86 ---> New Demodulator: 419 [new_demod,418] e_q3(v(A),add(B,C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=8): 420 [] e_q3(v(A),mul(B,C))=bfalse. % 2.18/2.86 ---> New Demodulator: 421 [new_demod,420] e_q3(v(A),mul(B,C))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 423 [copy,422,demod,72] e_q3(v(A),aux5(B,C,bfalse))=bfalse. % 2.18/2.86 ---> New Demodulator: 424 [new_demod,423] e_q3(v(A),aux5(B,C,bfalse))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=9): 425 [] e_q2(suc(A),suc(B))=e_q2(A,B). % 2.18/2.86 ---> New Demodulator: 426 [new_demod,425] e_q2(suc(A),suc(B))=e_q2(A,B). % 2.18/2.86 ** KEPT (pick-wt=6): 427 [] e_q2(zero,suc(A))=bfalse. % 2.18/2.86 ---> New Demodulator: 428 [new_demod,427] e_q2(zero,suc(A))=bfalse. % 2.18/2.86 ** KEPT (pick-wt=6): 429 [] e_q2(suc(A),zero)=bfalse. % 2.18/2.86 ---> New Demodulator: 430 [new_demod,429] e_q2(suc(A),zero)=bfalse. % 2.18/2.86 ** KEPT (pick-wt=5): 431 [] e_q2(A,A)=btrue. % 2.18/2.86 ---> New Demodulator: 432 [new_demod,431] e_q2(A,A)=btrue. % 2.18/2.86 ** KEPT (pick-wt=5): 433 [] e_q3(A,A)=btrue. % 2.18/2.86 ---> New Demodulator: 434 [new_demod,433] e_q3(A,A)=btrue. % 2.18/2.86 ** KEPT (pick-wt=5): 435 [] e_q4(A,A)=btrue. % 2.18/2.86 ---> New Demodulator: 436 [new_demod,435] e_q4(A,A)=btrue. % 2.18/2.86 Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] A=A. % 2.18/2.86 ** KEPT (pick-wt=12): 437 [copy,9,flip.1,demod,118,147,155] fail12(n(suc(suc(zero))),v(A))=aux(A,B,btrue). % 2.18/2.86 >>>> Starting back demodulation with 12. % 2.18/2.86 ** KEPT (pick-wt=11): 438 [copy,13,flip.1,demod,118] fail3(n(suc(suc(zero))),A)=aux2(A,B,btrue). % 2.18/2.86 >>>> Starting back demodulation with 16. % 2.18/2.86 >>>> Starting back demodulation with 18. % 2.18/2.86 >>>> Starting back demodulation with 21. % 2.18/2.86 ** KEPT (pick-wt=15): 439 [copy,23,flip.1] aux2(add(v(A),B),C,bfalse)=aux2(v(A),add(B,C),bfalse). % 2.18/2.86 >>>> Starting back demodulation with 26. % 2.18/2.86 >>>> Starting back demodulation with 29. % 2.18/2.86 >>>> Starting back demodulation with 32. % 2.18/2.86 >>>> Starting back demodulation with 35. % 2.18/2.86 >>>> Starting back demodulation with 38. % 2.18/2.86 ** KEPT (pick-wt=12): 440 [copy,39,flip.1,demod,118,147,155] fail12(n(suc(suc(zero))),v(A))=aux3(A,B,btrue). % 2.18/2.86 >>>> Starting back demodulation with 42. % 2.18/2.86 ** KEPT (pick-wt=11): 441 [copy,43,flip.1,demod,118] fail3(n(suc(suc(zero))),A)=aux4(A,B,btrue). % 2.18/2.86 >>>> Starting back demodulation with 46. % 2.18/2.86 >>>> Starting back demodulation with 48. % 2.18/2.86 >>>> Starting back demodulation with 51. % 2.18/2.86 ** KEPT (pick-wt=15): 442 [copy,53,flip.1] aux2(add(v(A),B),C,bfalse)=aux4(v(A),add(B,C),bfalse). % 2.18/2.86 >>>> Starting back demodulation with 56. % 2.18/2.86 >>>> Starting back demodulation with 59. % 2.18/2.86 >>>> Starting back demodulation with 62. % 2.18/2.86 >>>> Starting back demodulation with 65. % 2.18/2.86 >>>> Starting back demodulation with 68. % 2.18/2.86 ** KEPT (pick-wt=8): 443 [copy,69,flip.1] n(suc(zero))=aux5(A,B,btrue). % 2.18/2.86 >>>> Starting back demodulation with 72. % 2.18/2.86 >> back demodulating 67 with 72. % 2.18/2.86 >> back demodulating 58 with 72. % 2.18/2.86 >> back demodulating 37 with 72. % 2.18/2.86 >> back demodulating 28 with 72. % 2.18/2.86 >> back demodulating 6 with 72. % 2.18/2.86 >> back demodulating 5 with 72. % 2.18/2.86 ** KEPT (pick-wt=8): 454 [copy,73,flip.1,demod,285] a3(A)=aux6(B,A,n(zero)). % 2.18/2.86 ** KEPT (pick-wt=12): 455 [copy,74,flip.1,demod,205,285,285] fail4(a3(A),a3(B))=aux6(A,B,n(suc(C))). % 2.18/2.86 ** KEPT (pick-wt=12): 456 [copy,75,flip.1,demod,205,285,285] fail4(a3(A),a3(B))=aux6(A,B,add(C,D)). % 2.18/2.86 ** KEPT (pick-wt=12): 457 [copy,76,flip.1,demod,205,285,285] fail4(a3(A),a3(B))=aux6(A,B,mul(C,D)). % 2.18/2.86 ** KEPT (pick-wt=13): 458 [copy,78,flip.1,demod,205,285,285] fail4(a3(A),a3(B))=aux6(A,B,aux5(C,D,bfalse)). % 2.18/2.86 ** KEPT (pick-wt=11): 459 [copy,79,flip.1,demod,205,285,285] fail4(a3(A),a3(B))=aux6(A,B,v(C)). % 2.18/2.86 >>>> Starting back demodulation with 81. % 2.18/2.86 ** KEPT (pick-wt=12): 460 [copy,82,flip.1,demod,279,285,276,285] fail23(a3(A),a3(B))=aux7(A,B,n(suc(C))). % 2.18/2.86 ** KEPT (pick-wt=12): 461 [copy,83,flip.1,demod,279,285,276,285] fail23(a3(A),a3(B))=aux7(A,B,add(C,D)). % 2.18/2.86 ** KEPT (pick-wt=12): 462 [copy,84,flip.1,demod,279,285,276,285] fail23(a3(A),a3(B))=aux7(A,B,mul(C,D)). % 2.18/2.86 ** KEPT (pick-wt=13): 463 [copy,86,flip.1,demod,279,285,276,285] fail23(a3(A),a3(B))=aux7(A,B,aux5(C,D,bfalse)). % 2.18/2.86 ** KEPT (pick-wt=11): 464 [copy,87,flip.1,demod,279,285,276,285] fail23(a3(A),a3(B))=aux7(A,B,v(C)). % 2.18/2.86 ** KEPT (pick-wt=8): 465 [copy,88,flip.1] n(suc(zero))=aux8(A,B,btrue). % 2.18/2.86 ** KEPT (pick-wt=11): 466 [copy,90,flip.1,demod,282,285] aux5(a3(A),a3(B),bfalse)=aux8(A,B,bfalse). % 2.18/2.86 ** KEPT (pick-wt=8): 467 [copy,91,flip.1] suc(zero)=aux9(A,B,C,btrue). % 2.18/2.86 >>>> Starting back demodulation with 93. % 2.18/2.86 >>>> Starting back demodulation with 95. % 2.18/2.86 >>>> Starting back demodulation with 97. % 2.18/2.86 >>>> Starting back demodulation with 100. % 2.18/2.86 >>>> Starting back demodulation with 103. % 2.18/2.86 >>>> Starting back demodulation with 106. % 2.18/2.86 >>>> Starting back demodulation with 109. % 2.18/2.86 >>>> Starting back demodulation with 112. % 2.18/2.86 >>>> Starting back demodulation with 115. % 2.18/2.86 >>>> Starting back demodulation with 118. % 2.18/2.86 >> back demodulating 43 with 118. % 2.18/2.86 >> back demodulating 39 with 118. % 2.18/2.86 >> back demodulating 13 with 118. % 2.18/2.86 >> back demodulating 9 with 118. % 2.18/2.86 >>>> Starting back demodulation with 121. % 2.18/2.86 >>>> Starting back demodulation with 124. % 2.18/2.86 >>>> Starting back demodulation with 127. % 2.18/2.86 >>>> Starting back demodulation with 130. % 2.18/2.86 >>>> Starting back demodulation with 132. % 2.18/2.86 >>>> Starting back demodulation with 135. % 2.18/2.86 >>>> Starting back demodulation with 138. % 2.18/2.86 >>>> Starting back demodulation with 141. % 2.18/2.86 >>>> Starting back demodulation with 144. % 2.18/2.86 >>>> Starting back demodulation with 147. % 2.18/2.86 >>>> Starting back demodulation with 150. % 2.18/2.86 >>>> Starting back demodulation with 152. % 2.18/2.86 >>>> Starting back demodulation with 155. % 2.18/2.86 >>>> Starting back demodulation with 158. % 2.18/2.86 >>>> Starting back demodulation with 161. % 2.18/2.86 >>>> Starting back demodulation with 164. % 2.18/2.86 >>>> Starting back demodulation with 167. % 2.18/2.86 >>>> Starting back demodulation with 169. % 2.18/2.86 >>>> Starting back demodulation with 171. % 2.18/2.86 >>>> Starting back demodulation with 173. % 2.18/2.86 >>>> Starting back demodulation with 175. % 2.18/2.86 >>>> Starting back demodulation with 178. % 2.18/2.86 >>>> Starting back demodulation with 180. % 2.18/2.86 >>>> Starting back demodulation with 182. % 2.18/2.86 >>>> Starting back demodulation with 184. % 2.18/2.86 >>>> Starting back demodulation with 187. % 2.18/2.86 >>>> Starting back demodulation with 190. % 2.18/2.86 >>>> Starting back demodulation with 193. % 2.18/2.86 >>>> Starting back demodulation with 196. % 2.18/2.86 >>>> Starting back demodulation with 199. % 2.18/2.86 >>>> Starting back demodulation with 202. % 2.18/2.86 >>>> Starting back demodulation with 205. % 2.18/2.86 >> back demodulating 79 with 205. % 2.18/2.86 >> back demodulating 78 with 205. % 2.18/2.86 >> back demodulating 76 with 205. % 2.18/2.86 >> back demodulating 75 with 205. % 2.18/2.86 >> back demodulating 74 with 205. % 2.18/2.86 >>>> Starting back demodulation with 208. % 2.18/2.86 >>>> Starting back demodulation with 211. % 2.18/2.86 >>>> Starting back demodulation with 214. % 2.18/2.86 >>>> Starting back demodulation with 217. % 2.18/2.86 >>>> Starting back demodulation with 220. % 2.18/2.86 >>>> Starting back demodulation with 223. % 2.18/2.86 >>>> Starting back demodulation with 225. % 2.18/2.86 >>>> Starting back demodulation with 228. % 2.18/2.86 >>>> Starting back demodulation with 231. % 2.18/2.86 >>>> Starting back demodulation with 234. % 2.18/2.86 >>>> Starting back demodulation with 237. % 2.18/2.86 >>>> Starting back demodulation with 240. % 2.18/2.86 >>>> Starting back demodulation with 243. % 2.18/2.86 >>>> Starting back demodulation with 245. % 2.18/2.86 >>>> Starting back demodulation with 248. % 2.18/2.86 >>>> Starting back demodulation with 251. % 2.18/2.86 >>>> Starting back demodulation with 254. % 2.18/2.86 >>>> Starting back demodulation with 257. % 2.18/2.86 >>>> Starting back demodulation with 260. % 2.18/2.86 >>>> Starting back demodulation with 262. % 2.18/2.86 >>>> Starting back demodulation with 264. % 2.18/2.86 >>>> Starting back demodulation with 266. % 2.18/2.86 >>>> Starting back demodulation with 268. % 2.18/2.86 >>>> Starting back demodulation with 271. % 2.18/2.86 >>>> Starting back demodulation with 273. % 2.18/2.86 >>>> Starting back demodulation with 276. % 2.18/2.86 >> back demodulating 87 with 276. % 2.18/2.86 >> back demodulating 86 with 276. % 2.18/2.86 >> back demodulating 84 with 276. % 2.18/2.86 >> back demodulating 83 with 276. % 2.18/2.86 >> back demodulating 82 with 276. % 2.18/2.86 >>>> Starting back demodulation with 279. % 2.18/2.86 >>>> Starting back demodulation with 282. % 2.18/2.86 >> back demodulating 90 with 282. % 2.18/2.86 >>>> Starting back demodulation with 285. % 2.18/2.86 >> back demodulating 281 with 285. % 2.18/2.86 >> back demodulating 278 with 285. % 2.18/2.86 >> back demodulating 275 with 285. % 2.18/2.86 >> back demodulating 204 with 285. % 2.18/2.86 >> back demodulating 201 with 285. % 2.18/2.86 >> back demodulating 73 with 285. % 2.18/2.86 >>>> Starting back demodulation with 288. % 2.18/2.86 >>>> Starting back demodulation with 291. % 2.18/2.86 >>>> Starting back demodulation with 293. % 2.18/2.86 >>>> Starting back demodulation with 296. % 2.18/2.86 >>>> Starting back demodulation with 299. % 2.18/2.86 >>>> Starting back demodulation with 301. % 2.18/2.86 >>>> Starting back demodulation with 304. % 2.18/2.86 >>>> Starting back demodulation with 307. % 2.18/2.86 >>>> Starting back demodulation with 310. % 2.18/2.86 >>>> Starting back demodulation with 312. % 2.18/2.86 >>>> Starting back demodulation with 315. % 2.18/2.86 >>>> Starting back demodulation with 318. % 2.18/2.86 >>>> Starting back demodulation with 321. % 2.18/2.86 >>>> Starting back demodulation with 323. % 2.18/2.86 >>>> Starting back demodulation with 325. % 2.18/2.86 >>>> Starting back demodulation with 328. % 2.18/2.86 >>>> Starting back demodulation with 331. % 2.18/2.86 >>>> Starting back demodulation with 334. % 2.18/2.86 >>>> Starting back demodulation with 337. % 2.18/2.86 >>>> Starting back demodulation with 340. % 2.18/2.86 >>>> Starting back demodulation with 342. % 2.18/2.86 >>>> Starting back demodulation with 344. % 2.18/2.86 >>>> Starting back demodulation with 346. % 2.18/2.86 >>>> Starting back demodulation with 348. % 2.18/2.86 >>>> Starting back demodulation with 351. % 2.18/2.86 >>>> Starting back demodulation with 353. % 2.18/2.86 >>>> Starting back demodulation with 355. % 2.18/2.86 >>>> Starting back demodulation with 357. % 2.18/2.86 >>>> Starting back demodulation with 359. % 2.18/2.86 >>>> Starting back demodulation with 362. % 2.18/2.86 >>>> Starting back demodulation with 365. % 2.18/2.86 ** KEPT (pick-wt=8): 494 [copy,366,flip.1] fetch(A,B)=eval(A,v(B)). % 2.18/2.86 ** KEPT (pick-wt=14): 495 [copy,368,flip.1] e_q4(e_q2(eval(A,B),eval(A,a3(B))),btrue)=prop1(A,B). % 2.18/2.86 >>>> Starting back demodulation with 370. % 2.18/2.86 >>>> Starting back demodulation with 372. % 2.18/2.86 >>>> Starting back demodulation with 374. % 2.18/2.86 >>>> Starting back demodulation with 376. % 2.18/2.86 >>>> Starting back demodulation with 378. % 2.18/2.86 >>>> Starting back demodulation with 380. % 2.18/2.86 >>>> Starting back demodulation with 383. % 2.18/2.86 >>>> Starting back demodulation with 385. % 2.18/2.86 >>>> Starting back demodulation with 387. % 2.18/2.86 >>>> Starting back demodulation with 389. % 2.18/2.86 >>>> Starting back demodulation with 392. % 2.18/2.86 >>>> Starting back demodulation with 394. % 2.18/2.86 >>>> Starting back demodulation with 396. % 2.18/2.86 >>>> Starting back demodulation with 398. % 2.18/2.86 >>>> Starting back demodulation with 401. % 2.18/2.86 >>>> Starting back demodulation with 403. % 2.18/2.86 >>>> Starting back demodulation with 406. % 2.18/2.86 >>>> Starting back demodulation with 409. % 2.18/2.86 >>>> Starting back demodulation with 412. % 2.18/2.86 >>>> Starting back demodulation with 415. % 2.18/2.86 >>>> Starting back demodulation with 417. % 2.18/2.86 >>>> Starting back demodulation with 419. % 2.18/2.86 >>>> Starting back demodulation with 421. % 2.18/2.86 >>>> Starting back demodulation with 424. % 2.18/2.86 >>>> Starting back demodulation with 426. % 2.18/2.86 >>>> Starting back demodulation with 428. % 2.18/2.86 >>>> Starting back demodulation with 430. % 2.18/2.86 >>>> Starting back demodulation with 432. % 2.18/2.86 >> back demodulating 47 with 432. % 2.18/2.86 >> back demodulating 17 with 432. % 2.18/2.86 >>>> Starting back demodulation with 434. % 2.18/2.86 >>>> Starting back demodulation with 436. % 2.18/2.86 Following clause subsumed by 471 during input processing: 0 [copy,437,flip.1] aux(A,B,btrue)=fail12(n(suc(suc(zero))),v(A)). % 2.18/2.86 Following clause subsumed by 470 during input processing: 0 [copy,438,flip.1] aux2(A,B,btrue)=fail3(n(suc(suc(zero))),A). % 2.18/2.86 Following clause subsumed by 23 during input processing: 0 [copy,439,flip.1] aux2(v(A),add(B,C),bfalse)=aux2(add(v(A),B),C,bfalse). % 2.18/2.86 Following clause subsumed by 469 during input processing: 0 [copy,440,flip.1] aux3(A,B,btrue)=fail12(n(suc(suc(zero))),v(A)). % 2.18/2.86 Following clause subsumed by 468 during input processing: 0 [copy,441,flip.1] aux4(A,B,btrue)=fail3(n(suc(suc(zero))),A). % 2.18/2.86 Following clause subsumed by 53 during input processing: 0 [copy,442,flip.1] aux4(v(A),add(B,C),bfalse)=aux2(add(v(A),B),C,bfalse). % 2.18/2.86 Following clause subsumed by 69 during input processing: 0 [copy,443,flip.1] aux5(A,B,btrue)=n(suc(zero)). % 2.18/2.86 >>>> Starting back demodulation with 445. % 2.18/2.86 >>>> Starting back demodulation with 447. % 2.18/2.86 >>>> Starting back demodulation with 449. % 2.18/2.86 >> back demodulating 298 with 449. % 2.18/2.86 >>>> Starting back demodulation with 451. % 2.18/2.86 Following clause subsumed by 493 during input processing: 0 [copy,454,flip.1] aux6(A,B,n(zero))=a3(B). % 2.18/2.86 Following clause subsumed by 476 during input processing: 0 [copy,455,flip.1] aux6(A,B,n(suc(C)))=fail4(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 475 during input processing: 0 [copy,456,flip.1] aux6(A,B,add(C,D))=fail4(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 474 during input processing: 0 [copy,457,flip.1] aux6(A,B,mul(C,D))=fail4(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 473 during input processing: 0 [copy,458,flip.1] aux6(A,B,aux5(C,D,bfalse))=fail4(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 472 during input processing: 0 [copy,459,flip.1] aux6(A,B,v(C))=fail4(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 481 during input processing: 0 [copy,460,flip.1] aux7(A,B,n(suc(C)))=fail23(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 480 during input processing: 0 [copy,461,flip.1] aux7(A,B,add(C,D))=fail23(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 479 during input processing: 0 [copy,462,flip.1] aux7(A,B,mul(C,D))=fail23(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 478 during input processing: 0 [copy,463,flip.1] aux7(A,B,aux5(C,D,bfalse))=fail23(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 477 during input processing: 0 [copy,464,flip.1] aux7(A,B,v(C))=fail23(a3(A),a3(B)). % 2.18/2.86 Following clause subsumed by 88 during input processing: 0 [copy,465,flip.1] aux8(A,B,btrue)=n(suc(zero)). % 2.18/2.86 Following clause subsumed by 482 during input processing: 0 [copy,466,flip.1] aux8(A,B,bfalse)=aux5(a3(A),a3(B),bfalse). % 2.18/2.86 Following clause subsumed by 91 during input processing: 0 [copy,467,flip.1] aux9(A,B,C,btrue)=suc(zero). % 2.18/2.86 Following clause subsumed by 441 during input processing: 0 [copy,468,flip.1] fail3(n(suc(suc(zero))),A)=aux4(A,B,btrue). % 2.18/2.86 Following clause subsumed by 440 during input processing: 0 [copy,469,flip.1] fail12(n(suc(suc(zero))),v(A))=aux3(A,B,btrue). % 2.18/2.86 Following clause subsumed by 438 during input processing: 0 [copy,470,flip.1] fail3(n(suc(suc(zero))),A)=aux2(A,B,btrue). % 2.18/2.86 Following clause subsumed by 437 during input processing: 0 [copy,471,flip.1] fail12(n(suc(suc(zero))),v(A))=aux(A,B,btrue). % 2.18/2.86 Following clause subsumed by 459 during input processing: 0 [copy,472,flip.1] fail4(a3(A),a3(B))=aux6(A,B,v(C)). % 2.18/2.86 Following clause subsumed by 458 during input processing: 0 [copy,473,flip.1] fail4(a3(A),a3(B))=aux6(A,B,aux5(C,D,bfalse)). % 2.18/2.86 Following clause subsumed by 457 during input processing: 0 [copy,474,flip.1] fail4(a3(A),a3(B))=aux6(A,B,mul(C,D)). % 2.18/2.86 Following clause subsumed by 456 during input processing: 0 [copy,475,flip.1] fail4(a3(A),a3(B))=aux6(A,B,add(C,D)). % 2.18/2.86 Following clause subsumed by 455 during input processing: 0 [copy,476,flip.1] fail4(a3(A),a3(B))=aux6(A,B,n(suc(C))). % 2.18/2.86 Following clause subsumed by 464 during input processing: 0 [copy,477,flip.1] fail23(a3(A),a3(B))=aux7(A,B,v(C)). % 2.18/2.86 Following clause subsumed by 463 during input processing: 0 [copy,478,flip.1] fail23(a3(A),a3(B))=aux7(A,B,aux5(C,D,bfalse)). % 2.18/2.86 Following clause subsumed by 462 during input processing: 0 [copy,479,flip.1] fail23(a3(A),a3(B))=aux7(A,B,mul(C,D)). % 2.18/2.86 Following clause subsumed by 461 during input processing: 0 [copy,480,flip.1] fail23(a3(A),a3(B))=aux7(A,B,add(C,D)). % 2.18/2.86 Following clause subsumed by 460 during input processing: 0 [copy,481,flip.1] fail23(a3(A),a3(B))=aux7(A,B,n(suc(C))). % 2.18/2.86 Following clause subsumed by 466 during input processing: 0 [copy,482,flip.1] aux5(a3(A),a3(B),bfalse)=aux8(A,B,bfalse). % 2.18/2.86 >>>> Starting back demodulation with 484. % 2.18/2.86 >>>> Starting back demodulation with 486. % 2.18/2.86 >>>> Starting back demodulation with 488. % 2.18/2.86 >>>> Starting back demodulation with 490. % 2.18/2.86 >>>> Starting back demodulation with 492. % 2.18/2.86 Following clause subsumed by 454 during input processing: 0 [copy,493,flip.1] a3(A)=aux6(B,A,n(zero)). % 2.18/2.88 Following clause subsumed by 366 during input processing: 0 [copy,494,flip.1] eval(A,v(B))=fetch(A,B). % 2.18/2.88 Following clause subsumed by 368 during input processing: 0 [copy,495,flip.1] prop1(A,B)=e_q4(e_q2(eval(A,B),eval(A,a3(B))),btrue). % 2.18/2.88 >>>> Starting back demodulation with 497. % 2.18/2.88 >>>> Starting back demodulation with 499. % 2.18/2.88 >>>> Starting back demodulation with 501. % 2.18/2.88 % 2.18/2.88 ======= end of input processing ======= % 2.18/2.88 % 2.18/2.88 =========== start of search =========== % 2.18/2.88 % 2.18/2.88 % 2.18/2.88 Resetting weight limit to 6. % 2.18/2.88 % 2.18/2.88 % 2.18/2.88 Resetting weight limit to 6. % 2.18/2.88 % 2.18/2.88 sos_size=204 % 2.18/2.88 % 2.18/2.88 Search stopped because sos empty. % 2.18/2.88 % 2.18/2.88 % 2.18/2.88 Search stopped because sos empty. % 2.18/2.88 % 2.18/2.88 ============ end of search ============ % 2.18/2.88 % 2.18/2.88 -------------- statistics ------------- % 2.18/2.88 clauses given 220 % 2.18/2.88 clauses generated 2308 % 2.18/2.88 clauses kept 256 % 2.18/2.88 clauses forward subsumed 230 % 2.18/2.88 clauses back subsumed 1 % 2.18/2.88 Kbytes malloced 7812 % 2.18/2.88 % 2.18/2.88 ----------- times (seconds) ----------- % 2.18/2.88 user CPU time 0.03 (0 hr, 0 min, 0 sec) % 2.18/2.88 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.18/2.88 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.18/2.88 % 2.18/2.88 Process 16827 finished Tue May 5 10:53:28 2026 % 2.18/2.88 Otter interrupted % 2.18/2.88 PROOF NOT FOUND %------------------------------------------------------------------------------