%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX241_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n020.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:29 PM UTC 2026 % Result : Timeout 299.78s 300.02s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX241_1 : TPTP v9.3.0. Released v9.3.0. % 0.14/0.13 % Command : otter-tptp-script %s % 0.18/0.35 % Computer : n020.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Tue May 5 13:27:34 EDT 2026 % 0.18/0.35 % CPUTime : % 2.07/2.27 ----- Otter 3.3f, August 2004 ----- % 2.07/2.27 The process was started by sandbox2 on n020.cluster.edu, % 2.07/2.27 Tue May 5 13:27:34 2026 % 2.07/2.27 The command was "./otter". The process ID is 21501. % 2.07/2.27 % 2.07/2.27 set(prolog_style_variables). % 2.07/2.27 set(auto). % 2.07/2.27 dependent: set(auto1). % 2.07/2.27 dependent: set(process_input). % 2.07/2.27 dependent: clear(print_kept). % 2.07/2.27 dependent: clear(print_new_demod). % 2.07/2.27 dependent: clear(print_back_demod). % 2.07/2.27 dependent: clear(print_back_sub). % 2.07/2.27 dependent: set(control_memory). % 2.07/2.27 dependent: assign(max_mem, 12000). % 2.07/2.27 dependent: assign(pick_given_ratio, 4). % 2.07/2.27 dependent: assign(stats_level, 1). % 2.07/2.27 dependent: assign(max_seconds, 10800). % 2.07/2.27 clear(print_given). % 2.07/2.27 % 2.07/2.27 formula_list(usable). % 2.07/2.27 all A (A=A). % 2.07/2.27 all X X2 (head(cons(X,X2))=X). % 2.07/2.27 all X X2 (tail(cons(X,X2))=X2). % 2.07/2.27 all X X2 (nil!=cons(X,X2)). % 2.07/2.27 all X (proj1Suc(suc(X))=X). % 2.07/2.27 all X (zero!=suc(X)). % 2.07/2.27 all X (proj1High(high(X))=X). % 2.07/2.27 all X (proj1Low(low(X))=X). % 2.07/2.27 all X X2 (high(X)!=low(X2)). % 2.07/2.27 all X X2 (proj1Nand(nand(X,X2))=X). % 2.07/2.27 all X X2 (proj2Nand(nand(X,X2))=X2). % 2.07/2.27 all X (proj1Var(var(X))=X). % 2.07/2.27 all X X2 (nand(X,X2)!=tT). % 2.07/2.27 all X X2 (nand(X,X2)!=fF). % 2.07/2.27 all X X2 X3 (nand(X,X2)!=var(X3)). % 2.07/2.27 tT!=fF. % 2.07/2.27 all X (tT!=var(X)). % 2.07/2.27 all X (fF!=var(X)). % 2.07/2.27 all X X2 (proj1Assign(assign(X,X2))=X). % 2.07/2.27 all X X2 (proj2Assign(assign(X,X2))=X2). % 2.07/2.27 all X X2 (proj1Se_q(se_q(X,X2))=X). % 2.07/2.27 all X X2 (proj2Se_q(se_q(X,X2))=X2). % 2.07/2.27 all X X2 X3 (proj1IfThenElse(ifThenElse(X,X2,X3))=X). % 2.07/2.27 all X X2 X3 (proj2IfThenElse(ifThenElse(X,X2,X3))=X2). % 2.07/2.27 all X X2 X3 (proj3IfThenElse(ifThenElse(X,X2,X3))=X3). % 2.07/2.27 all X X2 (proj1While(while(X,X2))=X). % 2.07/2.27 all X X2 (proj2While(while(X,X2))=X2). % 2.07/2.27 all X X2 (skip!=assign(X,X2)). % 2.07/2.27 all X X2 (skip!=se_q(X,X2)). % 2.07/2.27 all X X2 X3 (skip!=ifThenElse(X,X2,X3)). % 2.07/2.27 all X X2 (skip!=while(X,X2)). % 2.07/2.27 all X X2 X3 X4 (assign(X,X2)!=se_q(X3,X4)). % 2.07/2.27 all X X2 X3 X4 X5 (assign(X,X2)!=ifThenElse(X3,X4,X5)). % 2.07/2.27 all X X2 X3 X4 (assign(X,X2)!=while(X3,X4)). % 2.07/2.27 all X X2 X3 X4 X5 (se_q(X,X2)!=ifThenElse(X3,X4,X5)). % 2.07/2.27 all X X2 X3 X4 (se_q(X,X2)!=while(X3,X4)). % 2.07/2.27 all X X2 X3 X4 X5 (ifThenElse(X,X2,X3)!=while(X4,X5)). % 2.07/2.27 all X (X!=nand(proj1Nand(X),proj2Nand(X))-> (X!=var(proj1Var(X))-> -secret(X))). % 2.07/2.27 all A B (secret(nand(A,B))<->secret(A)|secret(B)). % 2.07/2.27 all Z secret(var(high(Z))). % 2.07/2.27 all X2 (-secret(var(low(X2)))). % 2.07/2.27 typeCorrect(skip). % 2.07/2.27 all E Z typeCorrect(assign(high(Z),E)). % 2.07/2.27 all E X2 (typeCorrect(assign(low(X2),E))<-> -secret(E)). % 2.07/2.27 all P Q (typeCorrect(se_q(P,Q))<->typeCorrect(P)&typeCorrect(Q)). % 2.07/2.27 all C R Q2 (typeCorrect(ifThenElse(C,R,Q2))<->typeCorrect(R)&typeCorrect(Q2)). % 2.07/2.27 all E2 P2 (typeCorrect(while(E2,P2))<->typeCorrect(P2)). % 2.07/2.27 l=low(zero). % 2.07/2.27 h=high(zero). % 2.07/2.27 all X (-elem(X,nil)). % 2.07/2.27 all X Z Xs (elem(X,cons(Z,Xs))<->Z=X|elem(X,Xs)). % 2.07/2.27 all X A B (eval(X,nand(A,B))<-> -eval(X,A)| -eval(X,B)). % 2.07/2.27 all X eval(X,tT). % 2.07/2.27 all X (-eval(X,fF)). % 2.07/2.27 all X Z (eval(X,var(Z))<->elem(Z,X)). % 2.07/2.27 all X (del(X,nil)=nil). % 2.07/2.27 all X Z Ys (X=Z->del(X,cons(Z,Ys))=del(X,Ys)). % 2.07/2.27 all X Z Ys (X!=Z->del(X,cons(Z,Ys))=cons(Z,del(X,Ys))). % 2.07/2.27 all X (run(X,skip)=X). % 2.07/2.27 all X Z E (eval(X,E)->run(X,assign(Z,E))=cons(Z,X)). % 2.07/2.27 all X Z E (-eval(X,E)->run(X,assign(Z,E))=del(Z,X)). % 2.07/2.27 all X P Q (run(X,se_q(P,Q))=run(run(X,P),Q)). % 2.07/2.27 all X E2 R Q2 (eval(X,E2)->run(X,ifThenElse(E2,R,Q2))=run(X,R)). % 2.07/2.27 all X E2 R Q2 (-eval(X,E2)->run(X,ifThenElse(E2,R,Q2))=run(X,Q2)). % 2.07/2.27 all X E3 P2 (run(X,while(E3,P2))=run(X,ifThenElse(E3,se_q(P2,while(E3,P2)),skip))). % 2.07/2.27 -(exists P S (-(typeCorrect(P)-> (elem(l,run(S,P))<->elem(l,run(cons(h,S),P)))))). % 2.07/2.27 end_of_list. % 2.07/2.27 % 2.07/2.27 -------> usable clausifies to: % 2.07/2.27 % 2.07/2.27 list(usable). % 2.07/2.27 0 [] A=A. % 2.07/2.27 0 [] head(cons(X,X2))=X. % 2.07/2.27 0 [] tail(cons(X,X2))=X2. % 2.07/2.27 0 [] nil!=cons(X,X2). % 2.07/2.27 0 [] proj1Suc(suc(X))=X. % 2.07/2.27 0 [] zero!=suc(X). % 2.07/2.27 0 [] proj1High(high(X))=X. % 2.07/2.27 0 [] proj1Low(low(X))=X. % 2.07/2.27 0 [] high(X)!=low(X2). % 2.07/2.27 0 [] proj1Nand(nand(X,X2))=X. % 2.07/2.27 0 [] proj2Nand(nand(X,X2))=X2. % 2.07/2.27 0 [] proj1Var(var(X))=X. % 2.07/2.27 0 [] nand(X,X2)!=tT. % 2.07/2.27 0 [] nand(X,X2)!=fF. % 2.07/2.27 0 [] nand(X,X2)!=var(X3). % 2.07/2.27 0 [] tT!=fF. % 2.07/2.27 0 [] tT!=var(X). % 2.07/2.27 0 [] fF!=var(X). % 2.07/2.27 0 [] proj1Assign(assign(X,X2))=X. % 2.07/2.27 0 [] proj2Assign(assign(X,X2))=X2. % 2.07/2.27 0 [] proj1Se_q(se_q(X,X2))=X. % 2.07/2.27 0 [] proj2Se_q(se_q(X,X2))=X2. % 2.07/2.27 0 [] proj1IfThenElse(ifThenElse(X,X2,X3))=X. % 2.07/2.27 0 [] proj2IfThenElse(ifThenElse(X,X2,X3))=X2. % 2.07/2.27 0 [] proj3IfThenElse(ifThenElse(X,X2,X3))=X3. % 2.07/2.27 0 [] proj1While(while(X,X2))=X. % 2.07/2.27 0 [] proj2While(while(X,X2))=X2. % 2.07/2.27 0 [] skip!=assign(X,X2). % 2.07/2.27 0 [] skip!=se_q(X,X2). % 2.07/2.27 0 [] skip!=ifThenElse(X,X2,X3). % 2.07/2.27 0 [] skip!=while(X,X2). % 2.07/2.27 0 [] assign(X,X2)!=se_q(X3,X4). % 2.07/2.27 0 [] assign(X,X2)!=ifThenElse(X3,X4,X5). % 2.07/2.27 0 [] assign(X,X2)!=while(X3,X4). % 2.07/2.27 0 [] se_q(X,X2)!=ifThenElse(X3,X4,X5). % 2.07/2.27 0 [] se_q(X,X2)!=while(X3,X4). % 2.07/2.27 0 [] ifThenElse(X,X2,X3)!=while(X4,X5). % 2.07/2.27 0 [] X=nand(proj1Nand(X),proj2Nand(X))|X=var(proj1Var(X))| -secret(X). % 2.07/2.27 0 [] -secret(nand(A,B))|secret(A)|secret(B). % 2.07/2.27 0 [] secret(nand(A,B))| -secret(A). % 2.07/2.27 0 [] secret(nand(A,B))| -secret(B). % 2.07/2.27 0 [] secret(var(high(Z))). % 2.07/2.27 0 [] -secret(var(low(X2))). % 2.07/2.27 0 [] typeCorrect(skip). % 2.07/2.27 0 [] typeCorrect(assign(high(Z),E)). % 2.07/2.27 0 [] -typeCorrect(assign(low(X2),E))| -secret(E). % 2.07/2.27 0 [] typeCorrect(assign(low(X2),E))|secret(E). % 2.07/2.27 0 [] -typeCorrect(se_q(P,Q))|typeCorrect(P). % 2.07/2.27 0 [] -typeCorrect(se_q(P,Q))|typeCorrect(Q). % 2.07/2.27 0 [] typeCorrect(se_q(P,Q))| -typeCorrect(P)| -typeCorrect(Q). % 2.07/2.27 0 [] -typeCorrect(ifThenElse(C,R,Q2))|typeCorrect(R). % 2.07/2.27 0 [] -typeCorrect(ifThenElse(C,R,Q2))|typeCorrect(Q2). % 2.07/2.27 0 [] typeCorrect(ifThenElse(C,R,Q2))| -typeCorrect(R)| -typeCorrect(Q2). % 2.07/2.27 0 [] -typeCorrect(while(E2,P2))|typeCorrect(P2). % 2.07/2.27 0 [] typeCorrect(while(E2,P2))| -typeCorrect(P2). % 2.07/2.27 0 [] l=low(zero). % 2.07/2.27 0 [] h=high(zero). % 2.07/2.27 0 [] -elem(X,nil). % 2.07/2.27 0 [] -elem(X,cons(Z,Xs))|Z=X|elem(X,Xs). % 2.07/2.27 0 [] elem(X,cons(Z,Xs))|Z!=X. % 2.07/2.27 0 [] elem(X,cons(Z,Xs))| -elem(X,Xs). % 2.07/2.27 0 [] -eval(X,nand(A,B))| -eval(X,A)| -eval(X,B). % 2.07/2.27 0 [] eval(X,nand(A,B))|eval(X,A). % 2.07/2.27 0 [] eval(X,nand(A,B))|eval(X,B). % 2.07/2.27 0 [] eval(X,tT). % 2.07/2.27 0 [] -eval(X,fF). % 2.07/2.27 0 [] -eval(X,var(Z))|elem(Z,X). % 2.07/2.27 0 [] eval(X,var(Z))| -elem(Z,X). % 2.07/2.27 0 [] del(X,nil)=nil. % 2.07/2.27 0 [] X!=Z|del(X,cons(Z,Ys))=del(X,Ys). % 2.07/2.27 0 [] X=Z|del(X,cons(Z,Ys))=cons(Z,del(X,Ys)). % 2.07/2.27 0 [] run(X,skip)=X. % 2.07/2.27 0 [] -eval(X,E)|run(X,assign(Z,E))=cons(Z,X). % 2.07/2.27 0 [] eval(X,E)|run(X,assign(Z,E))=del(Z,X). % 2.07/2.27 0 [] run(X,se_q(P,Q))=run(run(X,P),Q). % 2.07/2.27 0 [] -eval(X,E2)|run(X,ifThenElse(E2,R,Q2))=run(X,R). % 2.07/2.27 0 [] eval(X,E2)|run(X,ifThenElse(E2,R,Q2))=run(X,Q2). % 2.07/2.27 0 [] run(X,while(E3,P2))=run(X,ifThenElse(E3,se_q(P2,while(E3,P2)),skip)). % 2.07/2.27 0 [] -typeCorrect(P)| -elem(l,run(S,P))|elem(l,run(cons(h,S),P)). % 2.07/2.27 0 [] -typeCorrect(P)|elem(l,run(S,P))| -elem(l,run(cons(h,S),P)). % 2.07/2.27 end_of_list. % 2.07/2.27 % 2.07/2.27 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. % 2.07/2.27 % 2.07/2.27 This ia a non-Horn set with equality. The strategy will be % 2.07/2.27 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.07/2.27 deletion, with positive clauses in sos and nonpositive % 2.07/2.27 clauses in usable. % 2.07/2.27 % 2.07/2.27 dependent: set(knuth_bendix). % 2.07/2.27 dependent: set(anl_eq). % 2.07/2.27 dependent: set(para_from). % 2.07/2.27 dependent: set(para_into). % 2.07/2.27 dependent: clear(para_from_right). % 2.07/2.27 dependent: clear(para_into_right). % 2.07/2.27 dependent: set(para_from_vars). % 2.07/2.27 dependent: set(eq_units_both_ways). % 2.07/2.27 dependent: set(dynamic_demod_all). % 2.07/2.27 dependent: set(dynamic_demod). % 2.07/2.27 dependent: set(order_eq). % 2.07/2.27 dependent: set(back_demod). % 2.07/2.27 dependent: set(lrpo). % 2.07/2.27 dependent: set(hyper_res). % 2.07/2.27 dependent: set(unit_deletion). % 2.07/2.27 dependent: set(factor). % 2.07/2.27 % 2.07/2.27 ------------> process usable: % 2.07/2.27 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil. % 2.07/2.27 ** KEPT (pick-wt=4): 4 [copy,3,flip.1] suc(A)!=zero. % 2.07/2.27 ** KEPT (pick-wt=5): 5 [] high(A)!=low(B). % 2.07/2.27 ** KEPT (pick-wt=5): 6 [] nand(A,B)!=tT. % 2.07/2.27 ** KEPT (pick-wt=5): 7 [] nand(A,B)!=fF. % 2.07/2.27 ** KEPT (pick-wt=6): 8 [] nand(A,B)!=var(C). % 2.07/2.27 ** KEPT (pick-wt=3): 9 [] tT!=fF. % 2.07/2.27 ** KEPT (pick-wt=4): 11 [copy,10,flip.1] var(A)!=tT. % 2.07/2.27 ** KEPT (pick-wt=4): 13 [copy,12,flip.1] var(A)!=fF. % 2.07/2.27 ** KEPT (pick-wt=5): 15 [copy,14,flip.1] assign(A,B)!=skip. % 2.07/2.27 ** KEPT (pick-wt=5): 17 [copy,16,flip.1] se_q(A,B)!=skip. % 2.07/2.27 ** KEPT (pick-wt=6): 19 [copy,18,flip.1] ifThenElse(A,B,C)!=skip. % 2.07/2.27 ** KEPT (pick-wt=5): 21 [copy,20,flip.1] while(A,B)!=skip. % 2.07/2.27 ** KEPT (pick-wt=7): 22 [] assign(A,B)!=se_q(C,D). % 2.07/2.27 ** KEPT (pick-wt=8): 23 [] assign(A,B)!=ifThenElse(C,D,E). % 2.07/2.27 ** KEPT (pick-wt=7): 24 [] assign(A,B)!=while(C,D). % 2.07/2.27 ** KEPT (pick-wt=8): 25 [] se_q(A,B)!=ifThenElse(C,D,E). % 2.07/2.27 ** KEPT (pick-wt=7): 26 [] se_q(A,B)!=while(C,D). % 2.07/2.27 ** KEPT (pick-wt=8): 27 [] ifThenElse(A,B,C)!=while(D,E). % 2.07/2.27 ** KEPT (pick-wt=14): 29 [copy,28,flip.1,flip.2] nand(proj1Nand(A),proj2Nand(A))=A|var(proj1Var(A))=A| -secret(A). % 2.07/2.27 ** KEPT (pick-wt=8): 30 [] -secret(nand(A,B))|secret(A)|secret(B). % 2.07/2.27 ** KEPT (pick-wt=6): 31 [] secret(nand(A,B))| -secret(A). % 2.07/2.27 ** KEPT (pick-wt=6): 32 [] secret(nand(A,B))| -secret(B). % 2.07/2.27 ** KEPT (pick-wt=4): 33 [] -secret(var(low(A))). % 2.07/2.27 ** KEPT (pick-wt=7): 34 [] -typeCorrect(assign(low(A),B))| -secret(B). % 2.07/2.27 ** KEPT (pick-wt=6): 35 [] -typeCorrect(se_q(A,B))|typeCorrect(A). % 2.07/2.27 ** KEPT (pick-wt=6): 36 [] -typeCorrect(se_q(A,B))|typeCorrect(B). % 2.07/2.27 ** KEPT (pick-wt=8): 37 [] typeCorrect(se_q(A,B))| -typeCorrect(A)| -typeCorrect(B). % 2.07/2.27 ** KEPT (pick-wt=7): 38 [] -typeCorrect(ifThenElse(A,B,C))|typeCorrect(B). % 2.07/2.27 ** KEPT (pick-wt=7): 39 [] -typeCorrect(ifThenElse(A,B,C))|typeCorrect(C). % 2.07/2.27 ** KEPT (pick-wt=9): 40 [] typeCorrect(ifThenElse(A,B,C))| -typeCorrect(B)| -typeCorrect(C). % 2.07/2.27 ** KEPT (pick-wt=6): 41 [] -typeCorrect(while(A,B))|typeCorrect(B). % 2.07/2.27 ** KEPT (pick-wt=6): 42 [] typeCorrect(while(A,B))| -typeCorrect(B). % 2.07/2.27 ** KEPT (pick-wt=3): 43 [] -elem(A,nil). % 2.07/2.27 ** KEPT (pick-wt=11): 44 [] -elem(A,cons(B,C))|B=A|elem(A,C). % 2.07/2.27 ** KEPT (pick-wt=8): 45 [] elem(A,cons(B,C))|B!=A. % 2.07/2.27 ** KEPT (pick-wt=8): 46 [] elem(A,cons(B,C))| -elem(A,C). % 2.07/2.27 ** KEPT (pick-wt=11): 47 [] -eval(A,nand(B,C))| -eval(A,B)| -eval(A,C). % 2.07/2.27 ** KEPT (pick-wt=3): 48 [] -eval(A,fF). % 2.07/2.27 ** KEPT (pick-wt=7): 49 [] -eval(A,var(B))|elem(B,A). % 2.07/2.27 ** KEPT (pick-wt=7): 50 [] eval(A,var(B))| -elem(B,A). % 2.07/2.27 ** KEPT (pick-wt=12): 51 [] A!=B|del(A,cons(B,C))=del(A,C). % 2.07/2.27 ** KEPT (pick-wt=12): 52 [] -eval(A,B)|run(A,assign(C,B))=cons(C,A). % 2.07/2.27 ** KEPT (pick-wt=13): 53 [] -eval(A,B)|run(A,ifThenElse(B,C,D))=run(A,C). % 2.07/2.27 ** KEPT (pick-wt=14): 54 [] -typeCorrect(A)| -elem(l,run(B,A))|elem(l,run(cons(h,B),A)). % 2.07/2.27 ** KEPT (pick-wt=14): 55 [] -typeCorrect(A)|elem(l,run(B,A))| -elem(l,run(cons(h,B),A)). % 2.07/2.27 ** KEPT (pick-wt=5): 56 [copy,5,flip.1] low(A)!=high(B). % 2.07/2.27 ** KEPT (pick-wt=6): 57 [copy,8,flip.1] var(A)!=nand(B,C). % 2.07/2.27 ** KEPT (pick-wt=7): 58 [copy,22,flip.1] se_q(A,B)!=assign(C,D). % 2.07/2.27 ** KEPT (pick-wt=8): 59 [copy,23,flip.1] ifThenElse(A,B,C)!=assign(D,E). % 2.07/2.27 ** KEPT (pick-wt=7): 60 [copy,24,flip.1] while(A,B)!=assign(C,D). % 2.07/2.27 ** KEPT (pick-wt=8): 61 [copy,25,flip.1] ifThenElse(A,B,C)!=se_q(D,E). % 2.07/2.27 ** KEPT (pick-wt=7): 62 [copy,26,flip.1] while(A,B)!=se_q(C,D). % 2.07/2.27 ** KEPT (pick-wt=8): 63 [copy,27,flip.1] while(A,B)!=ifThenElse(C,D,E). % 2.07/2.27 Following clause subsumed by 5 during input processing: 0 [copy,56,flip.1] high(A)!=low(B). % 2.07/2.27 Following clause subsumed by 8 during input processing: 0 [copy,57,flip.1] nand(A,B)!=var(C). % 2.07/2.27 Following clause subsumed by 22 during input processing: 0 [copy,58,flip.1] assign(A,B)!=se_q(C,D). % 2.07/2.27 Following clause subsumed by 23 during input processing: 0 [copy,59,flip.1] assign(A,B)!=ifThenElse(C,D,E). % 2.07/2.27 Following clause subsumed by 24 during input processing: 0 [copy,60,flip.1] assign(A,B)!=while(C,D). % 2.07/2.27 Following clause subsumed by 25 during input processing: 0 [copy,61,flip.1] se_q(A,B)!=ifThenElse(C,D,E). % 2.07/2.27 Following clause subsumed by 26 during input processing: 0 [copy,62,flip.1] se_q(A,B)!=while(C,D). % 2.07/2.27 Following clause subsumed by 27 during input processing: 0 [copy,63,flip.1] ifThenElse(A,B,C)!=while(D,E). % 2.07/2.27 % 2.07/2.27 ------------> process sos: % 2.07/2.27 ** KEPT (pick-wt=3): 68 [] A=A. % 2.07/2.27 ** KEPT (pick-wt=6): 69 [] head(cons(A,B))=A. % 2.07/2.27 ---> New Demodulator: 70 [new_demod,69] head(cons(A,B))=A. % 2.07/2.27 ** KEPT (pick-wt=6): 71 [] tail(cons(A,B))=B. % 2.07/2.27 ---> New Demodulator: 72 [new_demod,71] tail(cons(A,B))=B. % 2.07/2.27 ** KEPT (pick-wt=5): 73 [] proj1Suc(suc(A))=A. % 2.07/2.27 ---> New Demodulator: 74 [new_demod,73] proj1Suc(suc(A))=A. % 2.07/2.27 ** KEPT (pick-wt=5): 75 [] proj1High(high(A))=A. % 2.07/2.27 ---> New Demodulator: 76 [new_demod,75] proj1High(high(A))=A. % 2.07/2.27 ** KEPT (pick-wt=5): 77 [] proj1Low(low(A))=A. % 2.07/2.27 ---> New Demodulator: 78 [new_demod,77] proj1Low(low(A))=A. % 2.07/2.27 ** KEPT (pick-wt=6): 79 [] proj1Nand(nand(A,B))=A. % 2.07/2.27 ---> New Demodulator: 80 [new_demod,79] proj1Nand(nand(A,B))=A. % 2.07/2.27 ** KEPT (pick-wt=6): 81 [] proj2Nand(nand(A,B))=B. % 2.07/2.27 ---> New Demodulator: 82 [new_demod,81] proj2Nand(nand(A,B))=B. % 2.07/2.27 ** KEPT (pick-wt=5): 83 [] proj1Var(var(A))=A. % 2.07/2.27 ---> New Demodulator: 84 [new_demod,83] proj1Var(var(A))=A. % 2.07/2.27 ** KEPT (pick-wt=6): 85 [] proj1Assign(assign(A,B))=A. % 2.07/2.27 ---> New Demodulator: 86 [new_demod,85] proj1Assign(assign(A,B))=A. % 2.07/2.27 ** KEPT (pick-wt=6): 87 [] proj2Assign(assTerminated % 299.78/300.02 Otter interrupted % 299.78/300.02 PROOF NOT FOUND %------------------------------------------------------------------------------