%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX197-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n017.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:24 PM UTC 2026 % Result : Unknown 2.22s 2.46s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX197-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.16/0.34 % Computer : n017.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 11:04:57 EDT 2026 % 0.16/0.34 % CPUTime : % 2.22/2.44 ----- Otter 3.3f, August 2004 ----- % 2.22/2.44 The process was started by sandbox2 on n017.cluster.edu, % 2.22/2.44 Tue May 5 11:04:57 2026 % 2.22/2.44 The command was "./otter". The process ID is 16505. % 2.22/2.44 % 2.22/2.44 set(prolog_style_variables). % 2.22/2.44 set(auto). % 2.22/2.44 dependent: set(auto1). % 2.22/2.44 dependent: set(process_input). % 2.22/2.44 dependent: clear(print_kept). % 2.22/2.44 dependent: clear(print_new_demod). % 2.22/2.44 dependent: clear(print_back_demod). % 2.22/2.44 dependent: clear(print_back_sub). % 2.22/2.44 dependent: set(control_memory). % 2.22/2.44 dependent: assign(max_mem, 12000). % 2.22/2.44 dependent: assign(pick_given_ratio, 4). % 2.22/2.44 dependent: assign(stats_level, 1). % 2.22/2.44 dependent: assign(max_seconds, 10800). % 2.22/2.44 clear(print_given). % 2.22/2.44 % 2.22/2.44 list(usable). % 2.22/2.44 0 [] A=A. % 2.22/2.44 0 [] aux(X,A2,B3,btrue)=suc(zero). % 2.22/2.44 0 [] aux(X,A2,B3,bfalse)=zero. % 2.22/2.44 0 [] aux2(X,R,E4,Q,Q2,btrue)=run(X,append(Q2,R)). % 2.22/2.44 0 [] aux2(X,R,E4,Q,Q2,bfalse)=run(X,append(Q,R)). % 2.22/2.44 0 [] store(nil,zero,Z)=cons(Z,nil). % 2.22/2.44 0 [] store(nil,suc(X2),Z)=cons(zero,store(nil,X2,Z)). % 2.22/2.44 0 [] store(cons(N,St),zero,Z)=cons(Z,St). % 2.22/2.44 0 [] store(cons(N,St),suc(X3),Z)=cons(N,store(St,X3,Z)). % 2.22/2.44 0 [] opti2(while(E,P))=while(E,map(lam,P)). % 2.22/2.44 0 [] opti2(if(C,Q,R))=if(add(n(suc(zero)),C),R,Q). % 2.22/2.44 0 [] opti2(print(X))=print(X). % 2.22/2.44 0 [] opti2(x(X,X2))=x(X,X2). % 2.22/2.44 0 [] fetch(nil,Y)=zero. % 2.22/2.44 0 [] fetch(cons(N,St),zero)=N. % 2.22/2.44 0 [] fetch(cons(N,St),suc(Z))=fetch(St,Z). % 2.22/2.44 0 [] addNat(zero,Y)=Y. % 2.22/2.44 0 [] addNat(suc(Z),zero)=suc(Z). % 2.22/2.44 0 [] addNat(suc(Z),suc(X2))=suc(addNat(Z,suc(X2))). % 2.22/2.44 0 [] mulNat(zero,Y)=zero. % 2.22/2.44 0 [] mulNat(suc(Z),zero)=zero. % 2.22/2.44 0 [] mulNat(suc(Z),suc(X2))=addNat(mulNat(Z,suc(X2)),suc(X2)). % 2.22/2.44 0 [] eval(X,n(N))=N. % 2.22/2.44 0 [] eval(X,add(A,B))=addNat(eval(X,A),eval(X,B)). % 2.22/2.44 0 [] eval(X,mul(C,B2))=mulNat(eval(X,C),eval(X,B2)). % 2.22/2.44 0 [] eval(X,e_q(A2,B3))=aux(X,A2,B3,e_q4(eval(X,A2),eval(X,B3))). % 2.22/2.44 0 [] eval(X,v(Z))=fetch(X,Z). % 2.22/2.44 0 [] run(X,nil2)=nil. % 2.22/2.44 0 [] run(X,cons2(print(E),R))=cons(eval(X,E),run(X,R)). % 2.22/2.44 0 [] run(X,cons2(x(X2,E2),R))=run(store(X,X2,eval(X,E2)),R). % 2.22/2.44 0 [] run(X,cons2(while(E3,P),R))=run(X,cons2(if(E3,append(P,cons2(while(E3,P),nil2)),nil2),R)). % 2.22/2.44 0 [] run(X,cons2(if(E4,Q,Q2),R))=aux2(X,R,E4,Q,Q2,e_q4(eval(X,E4),zero)). % 2.22/2.44 0 [] prop_Opti2(X)=e_q2(run(nil,cons2(X,nil2)),run(nil,cons2(opti2(X),nil2))). % 2.22/2.44 0 [] map(F,nil2)=nil2. % 2.22/2.44 0 [] map(F,cons2(Y,Xs))=cons2(apply1(F,Y),map(F,Xs)). % 2.22/2.44 0 [] append(nil2,Y)=Y. % 2.22/2.44 0 [] append(cons2(Z,Xs),Y)=cons2(Z,append(Xs,Y)). % 2.22/2.44 0 [] e_q7(bfalse,btrue)=bfalse. % 2.22/2.44 0 [] e_q7(btrue,bfalse)=bfalse. % 2.22/2.44 0 [] e_q4(X,X)=btrue. % 2.22/2.44 0 [] e_q5(X,X)=btrue. % 2.22/2.44 0 [] e_q6(X,X)=btrue. % 2.22/2.44 0 [] e_q7(X,X)=btrue. % 2.22/2.44 0 [] e_q2(X,X)=btrue. % 2.22/2.44 0 [] e_q3(X,X)=btrue. % 2.22/2.44 0 [] e_q4(X,Z)!=bfalse|e_q2(cons(X,Y),cons(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q6(X,Z)!=bfalse|e_q3(cons2(X,Y),cons2(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q4(X,Z)!=btrue|e_q2(cons(X,Y),cons(Z,X2))=e_q2(Y,X2). % 2.22/2.44 0 [] e_q6(X,Z)!=btrue|e_q3(cons2(X,Y),cons2(Z,X2))=e_q3(Y,X2). % 2.22/2.44 0 [] e_q2(nil,cons(X,Y))=bfalse. % 2.22/2.44 0 [] e_q3(nil2,cons2(X,Y))=bfalse. % 2.22/2.44 0 [] e_q2(cons(X,Y),nil)=bfalse. % 2.22/2.44 0 [] e_q3(cons2(X,Y),nil2)=bfalse. % 2.22/2.44 0 [] e_q5(n(X),n(Y))=e_q4(X,Y). % 2.22/2.44 0 [] e_q5(X,Z)!=bfalse|e_q5(add(X,Y),add(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(X,Z)!=btrue|e_q5(add(X,Y),add(Z,X2))=e_q5(Y,X2). % 2.22/2.44 0 [] e_q5(X,Z)!=bfalse|e_q5(mul(X,Y),mul(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(X,Z)!=btrue|e_q5(mul(X,Y),mul(Z,X2))=e_q5(Y,X2). % 2.22/2.44 0 [] e_q5(X,Z)!=bfalse|e_q5(e_q(X,Y),e_q(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(X,Z)!=btrue|e_q5(e_q(X,Y),e_q(Z,X2))=e_q5(Y,X2). % 2.22/2.44 0 [] e_q5(v(X),v(Y))=e_q4(X,Y). % 2.22/2.44 0 [] e_q5(n(X),add(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q5(n(X),mul(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q5(n(X),e_q(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q5(n(X),v(Y))=bfalse. % 2.22/2.44 0 [] e_q5(add(X,Y),n(Z))=bfalse. % 2.22/2.44 0 [] e_q5(add(X,Y),mul(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(add(X,Y),e_q(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(add(X,Y),v(Z))=bfalse. % 2.22/2.44 0 [] e_q5(mul(X,Y),n(Z))=bfalse. % 2.22/2.44 0 [] e_q5(mul(X,Y),add(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(mul(X,Y),e_q(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(mul(X,Y),v(Z))=bfalse. % 2.22/2.44 0 [] e_q5(e_q(X,Y),n(Z))=bfalse. % 2.22/2.44 0 [] e_q5(e_q(X,Y),add(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(e_q(X,Y),mul(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(e_q(X,Y),v(Z))=bfalse. % 2.22/2.44 0 [] e_q5(v(X),n(Y))=bfalse. % 2.22/2.44 0 [] e_q5(v(X),add(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q5(v(X),mul(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q5(v(X),e_q(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q4(suc(X),suc(Y))=e_q4(X,Y). % 2.22/2.44 0 [] e_q4(zero,suc(X))=bfalse. % 2.22/2.44 0 [] e_q4(suc(X),zero)=bfalse. % 2.22/2.44 0 [] e_q6(print(X),print(Y))=e_q5(X,Y). % 2.22/2.44 0 [] e_q4(X,Z)!=bfalse|e_q6(x(X,Y),x(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q4(X,Z)!=btrue|e_q6(x(X,Y),x(Z,X2))=e_q5(Y,X2). % 2.22/2.44 0 [] e_q5(X,Z)!=bfalse|e_q6(while(X,Y),while(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q5(X,Z)!=btrue|e_q6(while(X,Y),while(Z,X2))=e_q3(Y,X2). % 2.22/2.44 0 [] e_q5(X,X2)!=bfalse|e_q6(if(X,Y,Z),if(X2,X3,X4))=bfalse. % 2.22/2.44 0 [] e_q5(X,X2)!=btrue|e_q3(Y,X3)!=bfalse|e_q6(if(X,Y,Z),if(X2,X3,X4))=bfalse. % 2.22/2.44 0 [] e_q5(X,X2)!=btrue|e_q3(Y,X3)!=btrue|e_q6(if(X,Y,Z),if(X2,X3,X4))=e_q3(Z,X4). % 2.22/2.44 0 [] e_q6(print(X),x(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q6(print(X),while(Y,Z))=bfalse. % 2.22/2.44 0 [] e_q6(print(X),if(Y,Z,X2))=bfalse. % 2.22/2.44 0 [] e_q6(x(X,Y),print(Z))=bfalse. % 2.22/2.44 0 [] e_q6(x(X,Y),while(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q6(x(X,Y),if(Z,X2,X3))=bfalse. % 2.22/2.44 0 [] e_q6(while(X,Y),print(Z))=bfalse. % 2.22/2.44 0 [] e_q6(while(X,Y),x(Z,X2))=bfalse. % 2.22/2.44 0 [] e_q6(while(X,Y),if(Z,X2,X3))=bfalse. % 2.22/2.44 0 [] e_q6(if(X,Y,Z),print(X2))=bfalse. % 2.22/2.44 0 [] e_q6(if(X,Y,Z),x(X2,X3))=bfalse. % 2.22/2.44 0 [] e_q6(if(X,Y,Z),while(X2,X3))=bfalse. % 2.22/2.44 0 [] apply1(lam,Y)=opti2(Y). % 2.22/2.44 0 [] e_q7(prop_Opti2(X),bfalse)!=btrue. % 2.22/2.44 end_of_list. % 2.22/2.44 % 2.22/2.44 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=3. % 2.22/2.44 % 2.22/2.44 This is a Horn set with equality. The strategy will be % 2.22/2.44 Knuth-Bendix and hyper_res, with positive clauses in % 2.22/2.44 sos and nonpositive clauses in usable. % 2.22/2.44 % 2.22/2.44 dependent: set(knuth_bendix). % 2.22/2.44 dependent: set(anl_eq). % 2.22/2.44 dependent: set(para_from). % 2.22/2.44 dependent: set(para_into). % 2.22/2.44 dependent: clear(para_from_right). % 2.22/2.44 dependent: clear(para_into_right). % 2.22/2.44 dependent: set(para_from_vars). % 2.22/2.44 dependent: set(eq_units_both_ways). % 2.22/2.44 dependent: set(dynamic_demod_all). % 2.22/2.44 dependent: set(dynamic_demod). % 2.22/2.44 dependent: set(order_eq). % 2.22/2.44 dependent: set(back_demod). % 2.22/2.44 dependent: set(lrpo). % 2.22/2.44 dependent: set(hyper_res). % 2.22/2.44 dependent: clear(order_hyper). % 2.22/2.44 % 2.22/2.44 ------------> process usable: % 2.22/2.44 ** KEPT (pick-wt=14): 1 [] e_q4(A,B)!=bfalse|e_q2(cons(A,C),cons(B,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=14): 2 [] e_q6(A,B)!=bfalse|e_q3(cons2(A,C),cons2(B,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=16): 3 [] e_q4(A,B)!=btrue|e_q2(cons(A,C),cons(B,D))=e_q2(C,D). % 2.22/2.44 ** KEPT (pick-wt=16): 4 [] e_q6(A,B)!=btrue|e_q3(cons2(A,C),cons2(B,D))=e_q3(C,D). % 2.22/2.44 ** KEPT (pick-wt=14): 5 [] e_q5(A,B)!=bfalse|e_q5(add(A,C),add(B,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=16): 6 [] e_q5(A,B)!=btrue|e_q5(add(A,C),add(B,D))=e_q5(C,D). % 2.22/2.44 ** KEPT (pick-wt=14): 7 [] e_q5(A,B)!=bfalse|e_q5(mul(A,C),mul(B,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=16): 8 [] e_q5(A,B)!=btrue|e_q5(mul(A,C),mul(B,D))=e_q5(C,D). % 2.22/2.44 ** KEPT (pick-wt=14): 9 [] e_q5(A,B)!=bfalse|e_q5(e_q(A,C),e_q(B,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=16): 10 [] e_q5(A,B)!=btrue|e_q5(e_q(A,C),e_q(B,D))=e_q5(C,D). % 2.22/2.44 ** KEPT (pick-wt=14): 11 [] e_q4(A,B)!=bfalse|e_q6(x(A,C),x(B,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=16): 12 [] e_q4(A,B)!=btrue|e_q6(x(A,C),x(B,D))=e_q5(C,D). % 2.22/2.44 ** KEPT (pick-wt=14): 13 [] e_q5(A,B)!=bfalse|e_q6(while(A,C),while(B,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=16): 14 [] e_q5(A,B)!=btrue|e_q6(while(A,C),while(B,D))=e_q3(C,D). % 2.22/2.44 ** KEPT (pick-wt=16): 15 [] e_q5(A,B)!=bfalse|e_q6(if(A,C,D),if(B,E,F))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=21): 16 [] e_q5(A,B)!=btrue|e_q3(C,D)!=bfalse|e_q6(if(A,C,E),if(B,D,F))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=23): 17 [] e_q5(A,B)!=btrue|e_q3(C,D)!=btrue|e_q6(if(A,C,E),if(B,D,F))=e_q3(E,F). % 2.22/2.44 ** KEPT (pick-wt=6): 18 [] e_q7(prop_Opti2(A),bfalse)!=btrue. % 2.22/2.44 % 2.22/2.44 ------------> process sos: % 2.22/2.44 ** KEPT (pick-wt=3): 19 [] A=A. % 2.22/2.44 ** KEPT (pick-wt=8): 20 [] aux(A,B,C,btrue)=suc(zero). % 2.22/2.44 ** KEPT (pick-wt=7): 21 [] aux(A,B,C,bfalse)=zero. % 2.22/2.44 ---> New Demodulator: 22 [new_demod,21] aux(A,B,C,bfalse)=zero. % 2.22/2.44 ** KEPT (pick-wt=13): 23 [] aux2(A,B,C,D,E,btrue)=run(A,append(E,B)). % 2.22/2.44 ** KEPT (pick-wt=13): 24 [] aux2(A,B,C,D,E,bfalse)=run(A,append(D,B)). % 2.22/2.44 ** KEPT (pick-wt=8): 26 [copy,25,flip.1] cons(A,nil)=store(nil,zero,A). % 2.22/2.44 ---> New Demodulator: 27 [new_demod,26] cons(A,nil)=store(nil,zero,A). % 2.22/2.44 ** KEPT (pick-wt=12): 28 [] store(nil,suc(A),B)=cons(zero,store(nil,A,B)). % 2.22/2.44 ** KEPT (pick-wt=10): 29 [] store(cons(A,B),zero,C)=cons(C,B). % 2.22/2.44 ** KEPT (pick-wt=14): 30 [] store(cons(A,B),suc(C),D)=cons(A,store(B,C,D)). % 2.22/2.44 ** KEPT (pick-wt=10): 31 [] opti2(while(A,B))=while(A,map(lam,B)). % 2.22/2.44 ---> New Demodulator: 32 [new_demod,31] opti2(while(A,B))=while(A,map(lam,B)). % 2.22/2.44 ** KEPT (pick-wt=14): 33 [] opti2(if(A,B,C))=if(add(n(suc(zero)),A),C,B). % 2.22/2.44 ** KEPT (pick-wt=6): 34 [] opti2(print(A))=print(A). % 2.22/2.44 ---> New Demodulator: 35 [new_demod,34] opti2(print(A))=print(A). % 2.22/2.44 ** KEPT (pick-wt=8): 36 [] opti2(x(A,B))=x(A,B). % 2.22/2.44 ---> New Demodulator: 37 [new_demod,36] opti2(x(A,B))=x(A,B). % 2.22/2.44 ** KEPT (pick-wt=5): 38 [] fetch(nil,A)=zero. % 2.22/2.44 ---> New Demodulator: 39 [new_demod,38] fetch(nil,A)=zero. % 2.22/2.44 ** KEPT (pick-wt=7): 40 [] fetch(cons(A,B),zero)=A. % 2.22/2.44 ---> New Demodulator: 41 [new_demod,40] fetch(cons(A,B),zero)=A. % 2.22/2.44 ** KEPT (pick-wt=10): 42 [] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.22/2.44 ---> New Demodulator: 43 [new_demod,42] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.22/2.44 ** KEPT (pick-wt=5): 44 [] addNat(zero,A)=A. % 2.22/2.44 ---> New Demodulator: 45 [new_demod,44] addNat(zero,A)=A. % 2.22/2.44 ** KEPT (pick-wt=7): 46 [] addNat(suc(A),zero)=suc(A). % 2.22/2.44 ---> New Demodulator: 47 [new_demod,46] addNat(suc(A),zero)=suc(A). % 2.22/2.44 ** KEPT (pick-wt=11): 49 [copy,48,flip.1] suc(addNat(A,suc(B)))=addNat(suc(A),suc(B)). % 2.22/2.44 ---> New Demodulator: 50 [new_demod,49] suc(addNat(A,suc(B)))=addNat(suc(A),suc(B)). % 2.22/2.44 ** KEPT (pick-wt=5): 51 [] mulNat(zero,A)=zero. % 2.22/2.44 ---> New Demodulator: 52 [new_demod,51] mulNat(zero,A)=zero. % 2.22/2.44 ** KEPT (pick-wt=6): 53 [] mulNat(suc(A),zero)=zero. % 2.22/2.44 ---> New Demodulator: 54 [new_demod,53] mulNat(suc(A),zero)=zero. % 2.22/2.44 ** KEPT (pick-wt=13): 55 [] mulNat(suc(A),suc(B))=addNat(mulNat(A,suc(B)),suc(B)). % 2.22/2.44 ---> New Demodulator: 56 [new_demod,55] mulNat(suc(A),suc(B))=addNat(mulNat(A,suc(B)),suc(B)). % 2.22/2.44 ** KEPT (pick-wt=6): 57 [] eval(A,n(B))=B. % 2.22/2.44 ---> New Demodulator: 58 [new_demod,57] eval(A,n(B))=B. % 2.22/2.44 ** KEPT (pick-wt=13): 59 [] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.22/2.44 ---> New Demodulator: 60 [new_demod,59] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.22/2.44 ** KEPT (pick-wt=13): 62 [copy,61,flip.1] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.22/2.44 ---> New Demodulator: 63 [new_demod,62] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.22/2.44 ** KEPT (pick-wt=17): 64 [] eval(A,e_q(B,C))=aux(A,B,C,e_q4(eval(A,B),eval(A,C))). % 2.22/2.44 ---> New Demodulator: 65 [new_demod,64] eval(A,e_q(B,C))=aux(A,B,C,e_q4(eval(A,B),eval(A,C))). % 2.22/2.44 ** KEPT (pick-wt=8): 66 [] eval(A,v(B))=fetch(A,B). % 2.22/2.44 ** KEPT (pick-wt=5): 67 [] run(A,nil2)=nil. % 2.22/2.44 ---> New Demodulator: 68 [new_demod,67] run(A,nil2)=nil. % 2.22/2.44 ** KEPT (pick-wt=14): 69 [] run(A,cons2(print(B),C))=cons(eval(A,B),run(A,C)). % 2.22/2.44 ---> New Demodulator: 70 [new_demod,69] run(A,cons2(print(B),C))=cons(eval(A,B),run(A,C)). % 2.22/2.44 ** KEPT (pick-wt=16): 71 [] run(A,cons2(x(B,C),D))=run(store(A,B,eval(A,C)),D). % 2.22/2.44 ** KEPT (pick-wt=22): 73 [copy,72,flip.1] run(A,cons2(if(B,append(C,cons2(while(B,C),nil2)),nil2),D))=run(A,cons2(while(B,C),D)). % 2.22/2.44 ---> New Demodulator: 74 [new_demod,73] run(A,cons2(if(B,append(C,cons2(while(B,C),nil2)),nil2),D))=run(A,cons2(while(B,C),D)). % 2.22/2.44 ** KEPT (pick-wt=20): 75 [] run(A,cons2(if(B,C,D),E))=aux2(A,E,B,C,D,e_q4(eval(A,B),zero)). % 2.22/2.44 ---> New Demodulator: 76 [new_demod,75] run(A,cons2(if(B,C,D),E))=aux2(A,E,B,C,D,e_q4(eval(A,B),zero)). % 2.22/2.44 ** KEPT (pick-wt=15): 77 [] prop_Opti2(A)=e_q2(run(nil,cons2(A,nil2)),run(nil,cons2(opti2(A),nil2))). % 2.22/2.44 ---> New Demodulator: 78 [new_demod,77] prop_Opti2(A)=e_q2(run(nil,cons2(A,nil2)),run(nil,cons2(opti2(A),nil2))). % 2.22/2.44 ** KEPT (pick-wt=5): 79 [] map(A,nil2)=nil2. % 2.22/2.44 ---> New Demodulator: 80 [new_demod,79] map(A,nil2)=nil2. % 2.22/2.44 ** KEPT (pick-wt=13): 81 [] map(A,cons2(B,C))=cons2(apply1(A,B),map(A,C)). % 2.22/2.44 ---> New Demodulator: 82 [new_demod,81] map(A,cons2(B,C))=cons2(apply1(A,B),map(A,C)). % 2.22/2.44 ** KEPT (pick-wt=5): 83 [] append(nil2,A)=A. % 2.22/2.44 ---> New Demodulator: 84 [new_demod,83] append(nil2,A)=A. % 2.22/2.44 ** KEPT (pick-wt=11): 86 [copy,85,flip.1] cons2(A,append(B,C))=append(cons2(A,B),C). % 2.22/2.44 ---> New Demodulator: 87 [new_demod,86] cons2(A,append(B,C))=append(cons2(A,B),C). % 2.22/2.44 ** KEPT (pick-wt=5): 88 [] e_q7(bfalse,btrue)=bfalse. % 2.22/2.44 ---> New Demodulator: 89 [new_demod,88] e_q7(bfalse,btrue)=bfalse. % 2.22/2.44 ** KEPT (pick-wt=5): 90 [] e_q7(btrue,bfalse)=bfalse. % 2.22/2.44 ---> New Demodulator: 91 [new_demod,90] e_q7(btrue,bfalse)=bfalse. % 2.22/2.44 ** KEPT (pick-wt=5): 92 [] e_q4(A,A)=btrue. % 2.22/2.44 ---> New Demodulator: 93 [new_demod,92] e_q4(A,A)=btrue. % 2.22/2.44 ** KEPT (pick-wt=5): 94 [] e_q5(A,A)=btrue. % 2.22/2.44 ---> New Demodulator: 95 [new_demod,94] e_q5(A,A)=btrue. % 2.22/2.44 ** KEPT (pick-wt=5): 96 [] e_q6(A,A)=btrue. % 2.22/2.44 ---> New Demodulator: 97 [new_demod,96] e_q6(A,A)=btrue. % 2.22/2.44 ** KEPT (pick-wt=5): 98 [] e_q7(A,A)=btrue. % 2.22/2.44 ---> New Demodulator: 99 [new_demod,98] e_q7(A,A)=btrue. % 2.22/2.44 ** KEPT (pick-wt=5): 100 [] e_q2(A,A)=btrue. % 2.22/2.44 ---> New Demodulator: 101 [new_demod,100] e_q2(A,A)=btrue. % 2.22/2.44 ** KEPT (pick-wt=5): 102 [] e_q3(A,A)=btrue. % 2.22/2.44 ---> New Demodulator: 103 [new_demod,102] e_q3(A,A)=btrue. % 2.22/2.44 ** KEPT (pick-wt=7): 104 [] e_q2(nil,cons(A,B))=bfalse. % 2.22/2.44 ---> New Demodulator: 105 [new_demod,104] e_q2(nil,cons(A,B))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=7): 106 [] e_q3(nil2,cons2(A,B))=bfalse. % 2.22/2.44 ---> New Demodulator: 107 [new_demod,106] e_q3(nil2,cons2(A,B))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=7): 108 [] e_q2(cons(A,B),nil)=bfalse. % 2.22/2.44 ---> New Demodulator: 109 [new_demod,108] e_q2(cons(A,B),nil)=bfalse. % 2.22/2.44 ** KEPT (pick-wt=7): 110 [] e_q3(cons2(A,B),nil2)=bfalse. % 2.22/2.44 ---> New Demodulator: 111 [new_demod,110] e_q3(cons2(A,B),nil2)=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 112 [] e_q5(n(A),n(B))=e_q4(A,B). % 2.22/2.44 ---> New Demodulator: 113 [new_demod,112] e_q5(n(A),n(B))=e_q4(A,B). % 2.22/2.44 ** KEPT (pick-wt=9): 114 [] e_q5(v(A),v(B))=e_q4(A,B). % 2.22/2.44 ---> New Demodulator: 115 [new_demod,114] e_q5(v(A),v(B))=e_q4(A,B). % 2.22/2.44 ** KEPT (pick-wt=8): 116 [] e_q5(n(A),add(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 117 [new_demod,116] e_q5(n(A),add(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 118 [] e_q5(n(A),mul(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 119 [new_demod,118] e_q5(n(A),mul(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 120 [] e_q5(n(A),e_q(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 121 [new_demod,120] e_q5(n(A),e_q(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=7): 122 [] e_q5(n(A),v(B))=bfalse. % 2.22/2.44 ---> New Demodulator: 123 [new_demod,122] e_q5(n(A),v(B))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 124 [] e_q5(add(A,B),n(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 125 [new_demod,124] e_q5(add(A,B),n(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 126 [] e_q5(add(A,B),mul(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 127 [new_demod,126] e_q5(add(A,B),mul(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 128 [] e_q5(add(A,B),e_q(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 129 [new_demod,128] e_q5(add(A,B),e_q(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 130 [] e_q5(add(A,B),v(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 131 [new_demod,130] e_q5(add(A,B),v(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 132 [] e_q5(mul(A,B),n(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 133 [new_demod,132] e_q5(mul(A,B),n(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 134 [] e_q5(mul(A,B),add(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 135 [new_demod,134] e_q5(mul(A,B),add(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 136 [] e_q5(mul(A,B),e_q(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 137 [new_demod,136] e_q5(mul(A,B),e_q(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 138 [] e_q5(mul(A,B),v(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 139 [new_demod,138] e_q5(mul(A,B),v(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 140 [] e_q5(e_q(A,B),n(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 141 [new_demod,140] e_q5(e_q(A,B),n(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 142 [] e_q5(e_q(A,B),add(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 143 [new_demod,142] e_q5(e_q(A,B),add(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 144 [] e_q5(e_q(A,B),mul(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 145 [new_demod,144] e_q5(e_q(A,B),mul(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 146 [] e_q5(e_q(A,B),v(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 147 [new_demod,146] e_q5(e_q(A,B),v(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=7): 148 [] e_q5(v(A),n(B))=bfalse. % 2.22/2.44 ---> New Demodulator: 149 [new_demod,148] e_q5(v(A),n(B))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 150 [] e_q5(v(A),add(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 151 [new_demod,150] e_q5(v(A),add(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 152 [] e_q5(v(A),mul(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 153 [new_demod,152] e_q5(v(A),mul(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 154 [] e_q5(v(A),e_q(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 155 [new_demod,154] e_q5(v(A),e_q(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 156 [] e_q4(suc(A),suc(B))=e_q4(A,B). % 2.22/2.44 ---> New Demodulator: 157 [new_demod,156] e_q4(suc(A),suc(B))=e_q4(A,B). % 2.22/2.44 ** KEPT (pick-wt=6): 158 [] e_q4(zero,suc(A))=bfalse. % 2.22/2.44 ---> New Demodulator: 159 [new_demod,158] e_q4(zero,suc(A))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=6): 160 [] e_q4(suc(A),zero)=bfalse. % 2.22/2.44 ---> New Demodulator: 161 [new_demod,160] e_q4(suc(A),zero)=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 162 [] e_q6(print(A),print(B))=e_q5(A,B). % 2.22/2.44 ---> New Demodulator: 163 [new_demod,162] e_q6(print(A),print(B))=e_q5(A,B). % 2.22/2.44 ** KEPT (pick-wt=8): 164 [] e_q6(print(A),x(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 165 [new_demod,164] e_q6(print(A),x(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 166 [] e_q6(print(A),while(B,C))=bfalse. % 2.22/2.44 ---> New Demodulator: 167 [new_demod,166] e_q6(print(A),while(B,C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 168 [] e_q6(print(A),if(B,C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 169 [new_demod,168] e_q6(print(A),if(B,C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 170 [] e_q6(x(A,B),print(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 171 [new_demod,170] e_q6(x(A,B),print(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 172 [] e_q6(x(A,B),while(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 173 [new_demod,172] e_q6(x(A,B),while(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=10): 174 [] e_q6(x(A,B),if(C,D,E))=bfalse. % 2.22/2.44 ---> New Demodulator: 175 [new_demod,174] e_q6(x(A,B),if(C,D,E))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=8): 176 [] e_q6(while(A,B),print(C))=bfalse. % 2.22/2.44 ---> New Demodulator: 177 [new_demod,176] e_q6(while(A,B),print(C))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 178 [] e_q6(while(A,B),x(C,D))=bfalse. % 2.22/2.44 ---> New Demodulator: 179 [new_demod,178] e_q6(while(A,B),x(C,D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=10): 180 [] e_q6(while(A,B),if(C,D,E))=bfalse. % 2.22/2.44 ---> New Demodulator: 181 [new_demod,180] e_q6(while(A,B),if(C,D,E))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=9): 182 [] e_q6(if(A,B,C),print(D))=bfalse. % 2.22/2.44 ---> New Demodulator: 183 [new_demod,182] e_q6(if(A,B,C),print(D))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=10): 184 [] e_q6(if(A,B,C),x(D,E))=bfalse. % 2.22/2.44 ---> New Demodulator: 185 [new_demod,184] e_q6(if(A,B,C),x(D,E))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=10): 186 [] e_q6(if(A,B,C),while(D,E))=bfalse. % 2.22/2.44 ---> New Demodulator: 187 [new_demod,186] e_q6(if(A,B,C),while(D,E))=bfalse. % 2.22/2.44 ** KEPT (pick-wt=6): 189 [copy,188,flip.1] opti2(A)=apply1(lam,A). % 2.22/2.44 ---> New Demodulator: 190 [new_demod,189] opti2(A)=apply1(lam,A). % 2.22/2.44 Following clause subsumed by 19 during input processing: 0 [copy,19,flip.1] A=A. % 2.22/2.44 ** KEPT (pick-wt=8): 191 [copy,20,flip.1] suc(zero)=aux(A,B,C,btrue). % 2.22/2.44 >>>> Starting back demodulation with 22. % 2.22/2.44 ** KEPT (pick-wt=13): 192 [copy,23,flip.1] run(A,append(B,C))=aux2(A,C,D,E,B,btrue). % 2.22/2.44 ** KEPT (pick-wt=13): 193 [copy,24,flip.1] run(A,append(B,C))=aux2(A,C,D,B,E,bfalse). % 2.22/2.44 >>>> Starting back demodulation with 27. % 2.22/2.44 ** KEPT (pick-wt=12): 194 [copy,28,flip.1] cons(zero,store(nil,A,B))=store(nil,suc(A),B). % 2.22/2.44 ** KEPT (pick-wt=10): 195 [copy,29,flip.1] cons(A,B)=store(cons(C,B),zero,A). % 2.22/2.44 ** KEPT (pick-wt=14): 196 [copy,30,flip.1] cons(A,store(B,C,D))=store(cons(A,B),suc(C),D). % 2.22/2.44 >>>> Starting back demodulation with 32. % 2.22/2.44 ** KEPT (pick-wt=15): 197 [copy,33,flip.1,demod,190] if(add(n(suc(zero)),A),B,C)=apply1(lam,if(A,C,B)). % 2.22/2.44 >>>> Starting back demodulation with 35. % 2.22/2.44 >>>> Starting back demodulation with 37. % 2.22/2.44 >>>> Starting back demodulation with 39. % 2.22/2.44 >>>> Starting back demodulation with 41. % 2.22/2.44 >>>> Starting back demodulation with 43. % 2.22/2.44 >>>> Starting back demodulation with 45. % 2.22/2.44 >>>> Starting back demodulation with 47. % 2.22/2.44 >>>> Starting back demodulation with 50. % 2.22/2.44 >>>> Starting back demodulation with 52. % 2.22/2.44 >>>> Starting back demodulation with 54. % 2.22/2.44 >>>> Starting back demodulation with 56. % 2.22/2.44 >>>> Starting back demodulation with 58. % 2.22/2.44 >>>> Starting back demodulation with 60. % 2.22/2.44 >>>> Starting back demodulation with 63. % 2.22/2.44 >>>> Starting back demodulation with 65. % 2.22/2.44 ** KEPT (pick-wt=8): 198 [copy,66,flip.1] fetch(A,B)=eval(A,v(B)). % 2.22/2.44 >>>> Starting back demodulation with 68. % 2.22/2.44 >>>> Starting back demodulation with 70. % 2.22/2.44 ** KEPT (pick-wt=16): 199 [copy,71,flip.1] run(store(A,B,eval(A,C)),D)=run(A,cons2(x(B,C),D)). % 2.22/2.44 >>>> Starting back demodulation with 74. % 2.22/2.44 >>>> Starting back demodulation with 76. % 2.22/2.44 >> back demodulating 73 with 76. % 2.22/2.44 >>>> Starting back demodulation with 78. % 2.22/2.44 >> back demodulating 18 with 78. % 2.22/2.44 >>>> Starting back demodulation with 80. % 2.22/2.44 >>>> Starting back demodulation with 82. % 2.22/2.44 >>>> Starting back demodulation with 84. % 2.22/2.44 >>>> Starting back demodulation with 87. % 2.22/2.44 >>>> Starting back demodulation with 89. % 2.22/2.44 >>>> Starting back demodulation with 91. % 2.22/2.44 >>>> Starting back demodulation with 93. % 2.22/2.44 >>>> Starting back demodulation with 95. % 2.22/2.44 >>>> Starting back demodulation with 97. % 2.22/2.44 >>>> Starting back demodulation with 99. % 2.22/2.46 >>>> Starting back demodulation with 101. % 2.22/2.46 >>>> Starting back demodulation with 103. % 2.22/2.46 >>>> Starting back demodulation with 105. % 2.22/2.46 >>>> Starting back demodulation with 107. % 2.22/2.46 >>>> Starting back demodulation with 109. % 2.22/2.46 >>>> Starting back demodulation with 111. % 2.22/2.46 >>>> Starting back demodulation with 113. % 2.22/2.46 >>>> Starting back demodulation with 115. % 2.22/2.46 >>>> Starting back demodulation with 117. % 2.22/2.46 >>>> Starting back demodulation with 119. % 2.22/2.46 >>>> Starting back demodulation with 121. % 2.22/2.46 >>>> Starting back demodulation with 123. % 2.22/2.46 >>>> Starting back demodulation with 125. % 2.22/2.46 >>>> Starting back demodulation with 127. % 2.22/2.46 >>>> Starting back demodulation with 129. % 2.22/2.46 >>>> Starting back demodulation with 131. % 2.22/2.46 >>>> Starting back demodulation with 133. % 2.22/2.46 >>>> Starting back demodulation with 135. % 2.22/2.46 >>>> Starting back demodulation with 137. % 2.22/2.46 >>>> Starting back demodulation with 139. % 2.22/2.46 >>>> Starting back demodulation with 141. % 2.22/2.46 >>>> Starting back demodulation with 143. % 2.22/2.46 >>>> Starting back demodulation with 145. % 2.22/2.46 >>>> Starting back demodulation with 147. % 2.22/2.46 >>>> Starting back demodulation with 149. % 2.22/2.46 >>>> Starting back demodulation with 151. % 2.22/2.46 >>>> Starting back demodulation with 153. % 2.22/2.46 >>>> Starting back demodulation with 155. % 2.22/2.46 >>>> Starting back demodulation with 157. % 2.22/2.46 >>>> Starting back demodulation with 159. % 2.22/2.46 >>>> Starting back demodulation with 161. % 2.22/2.46 >>>> Starting back demodulation with 163. % 2.22/2.46 >>>> Starting back demodulation with 165. % 2.22/2.46 >>>> Starting back demodulation with 167. % 2.22/2.46 >>>> Starting back demodulation with 169. % 2.22/2.46 >>>> Starting back demodulation with 171. % 2.22/2.46 >>>> Starting back demodulation with 173. % 2.22/2.46 >>>> Starting back demodulation with 175. % 2.22/2.46 >>>> Starting back demodulation with 177. % 2.22/2.46 >>>> Starting back demodulation with 179. % 2.22/2.46 >>>> Starting back demodulation with 181. % 2.22/2.46 >>>> Starting back demodulation with 183. % 2.22/2.46 >>>> Starting back demodulation with 185. % 2.22/2.46 >>>> Starting back demodulation with 187. % 2.22/2.46 >>>> Starting back demodulation with 190. % 2.22/2.46 >> back demodulating 77 with 190. % 2.22/2.46 >> back demodulating 36 with 190. % 2.22/2.46 >> back demodulating 34 with 190. % 2.22/2.46 >> back demodulating 33 with 190. % 2.22/2.46 >> back demodulating 31 with 190. % 2.22/2.46 Following clause subsumed by 20 during input processing: 0 [copy,191,flip.1] aux(A,B,C,btrue)=suc(zero). % 2.22/2.46 Following clause subsumed by 23 during input processing: 0 [copy,192,flip.1] aux2(A,B,C,D,E,btrue)=run(A,append(E,B)). % 2.22/2.46 Following clause subsumed by 24 during input processing: 0 [copy,193,flip.1] aux2(A,B,C,D,E,bfalse)=run(A,append(D,B)). % 2.22/2.46 Following clause subsumed by 28 during input processing: 0 [copy,194,flip.1] store(nil,suc(A),B)=cons(zero,store(nil,A,B)). % 2.22/2.46 Following clause subsumed by 29 during input processing: 0 [copy,195,flip.1] store(cons(A,B),zero,C)=cons(C,B). % 2.22/2.46 Following clause subsumed by 30 during input processing: 0 [copy,196,flip.1] store(cons(A,B),suc(C),D)=cons(A,store(B,C,D)). % 2.22/2.46 Following clause subsumed by 209 during input processing: 0 [copy,197,flip.1] apply1(lam,if(A,B,C))=if(add(n(suc(zero)),A),C,B). % 2.22/2.46 Following clause subsumed by 66 during input processing: 0 [copy,198,flip.1] eval(A,v(B))=fetch(A,B). % 2.22/2.46 Following clause subsumed by 71 during input processing: 0 [copy,199,flip.1] run(A,cons2(x(B,C),D))=run(store(A,B,eval(A,C)),D). % 2.22/2.46 >>>> Starting back demodulation with 201. % 2.22/2.46 >>>> Starting back demodulation with 204. % 2.22/2.46 >>>> Starting back demodulation with 206. % 2.22/2.46 >>>> Starting back demodulation with 208. % 2.22/2.46 Following clause subsumed by 197 during input processing: 0 [copy,209,flip.1] if(add(n(suc(zero)),A),B,C)=apply1(lam,if(A,C,B)). % 2.22/2.46 >>>> Starting back demodulation with 211. % 2.22/2.46 % 2.22/2.46 ======= end of input processing ======= % 2.22/2.46 % 2.22/2.46 =========== start of search =========== % 2.22/2.46 % 2.22/2.46 % 2.22/2.46 Resetting weight limit to 9. % 2.22/2.46 % 2.22/2.46 % 2.22/2.46 Resetting weight limit to 9. % 2.22/2.46 % 2.22/2.46 sos_size=178 % 2.22/2.46 % 2.22/2.46 Search stopped because sos empty. % 2.22/2.46 % 2.22/2.46 % 2.22/2.46 Search stopped because sos empty. % 2.22/2.46 % 2.22/2.46 ============ end of search ============ % 2.22/2.46 % 2.22/2.46 -------------- statistics ------------- % 2.22/2.46 clauses given 248 % 2.22/2.46 clauses generated 3691 % 2.22/2.46 clauses kept 276 % 2.22/2.46 clauses forward subsumed 846 % 2.22/2.46 clauses back subsumed 8 % 2.22/2.46 Kbytes malloced 6835 % 2.22/2.46 % 2.22/2.46 ----------- times (seconds) ----------- % 2.22/2.46 user CPU time 0.02 (0 hr, 0 min, 0 sec) % 2.22/2.46 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.22/2.46 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.22/2.46 % 2.22/2.46 Process 16505 finished Tue May 5 11:04:59 2026 % 2.22/2.46 Otter interrupted % 2.22/2.46 PROOF NOT FOUND %------------------------------------------------------------------------------