%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX221+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n006.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:27 PM UTC 2026 % Result : Unknown 15.62s 15.85s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX221+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.16/0.33 % Computer : n006.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 12:29:45 EDT 2026 % 0.16/0.33 % CPUTime : % 1.94/2.15 ----- Otter 3.3f, August 2004 ----- % 1.94/2.15 The process was started by sandbox on n006.cluster.edu, % 1.94/2.15 Tue May 5 12:29:46 2026 % 1.94/2.15 The command was "./otter". The process ID is 23353. % 1.94/2.15 % 1.94/2.15 set(prolog_style_variables). % 1.94/2.15 set(auto). % 1.94/2.15 dependent: set(auto1). % 1.94/2.15 dependent: set(process_input). % 1.94/2.15 dependent: clear(print_kept). % 1.94/2.15 dependent: clear(print_new_demod). % 1.94/2.15 dependent: clear(print_back_demod). % 1.94/2.15 dependent: clear(print_back_sub). % 1.94/2.15 dependent: set(control_memory). % 1.94/2.15 dependent: assign(max_mem, 12000). % 1.94/2.15 dependent: assign(pick_given_ratio, 4). % 1.94/2.15 dependent: assign(stats_level, 1). % 1.94/2.15 dependent: assign(max_seconds, 10800). % 1.94/2.15 clear(print_given). % 1.94/2.15 % 1.94/2.15 formula_list(usable). % 1.94/2.15 all A (A=A). % 1.94/2.15 all X X2 (head(cons(X,X2))=X). % 1.94/2.15 all X X2 (tail(cons(X,X2))=X2). % 1.94/2.15 all X X2 (nil!=cons(X,X2)). % 1.94/2.15 all X X2 (proj1Arr(arr(X,X2))=X). % 1.94/2.15 all X X2 (proj2Arr(arr(X,X2))=X2). % 1.94/2.15 all X X2 (arr(X,X2)!=a). % 1.94/2.15 all X X2 (arr(X,X2)!=b). % 1.94/2.15 all X X2 (arr(X,X2)!=c). % 1.94/2.15 a!=b. % 1.94/2.15 a!=c. % 1.94/2.15 b!=c. % 1.94/2.15 all X (proj1Suc(suc(X))=X). % 1.94/2.15 all X (zero!=suc(X)). % 1.94/2.15 all X (proj1Just(just(X))=X). % 1.94/2.15 all X (nothing!=just(X)). % 1.94/2.15 all X X2 X3 (proj1App(app(X,X2,X3))=X). % 1.94/2.15 all X X2 X3 (proj2App(app(X,X2,X3))=X2). % 1.94/2.15 all X X2 X3 (proj3App(app(X,X2,X3))=X3). % 1.94/2.15 all X (proj1Lam(lam(X))=X). % 1.94/2.15 all X (proj1Var(var(X))=X). % 1.94/2.15 all X X2 X3 X4 (app(X,X2,X3)!=lam(X4)). % 1.94/2.15 all X X2 X3 X4 (app(X,X2,X3)!=var(X4)). % 1.94/2.15 all X X2 (lam(X)!=var(X2)). % 1.94/2.15 all Y Z X2 (Y!=lam(proj1Lam(Y))-> (nf(app(Y,Z,X2))<->nf(Y)&nf(Z))). % 1.94/2.15 all Z X2 X3 (-nf(app(lam(X3),Z,X2))). % 1.94/2.15 all E (nf(lam(E))<->nf(E)). % 1.94/2.15 all X4 nf(var(X4)). % 1.94/2.15 all Y (index(nil,Y)=nothing). % 1.94/2.15 all Z Xs (index(cons(Z,Xs),zero)=just(Z)). % 1.94/2.15 all Z Xs N (index(cons(Z,Xs),suc(N))=index(Xs,N)). % 1.94/2.15 all X Z F X2 Tx (tc(X,app(F,X2,Tx),Z)<->tc(X,F,arr(Tx,Z))&tc(X,X2,Tx)). % 1.94/2.15 all X Z E (Z!=arr(proj1Arr(Z),proj2Arr(Z))-> -tc(X,lam(E),Z)). % 1.94/2.15 all X E Tx2 T1 (tc(X,lam(E),arr(Tx2,T1))<->tc(cons(Tx2,X),E,T1)). % 1.94/2.15 all X Z X3 (index(X,X3)=nothing-> -tc(X,var(X3),Z)). % 1.94/2.15 all X Z X3 Tx3 (index(X,X3)=just(Tx3)-> (tc(X,var(X3),Z)<->Tx3=Z)). % 1.94/2.15 -(exists E (nf(E)&tc(nil,E,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))))). % 1.94/2.15 end_of_list. % 1.94/2.15 % 1.94/2.15 -------> usable clausifies to: % 1.94/2.15 % 1.94/2.15 list(usable). % 1.94/2.15 0 [] A=A. % 1.94/2.15 0 [] head(cons(X,X2))=X. % 1.94/2.15 0 [] tail(cons(X,X2))=X2. % 1.94/2.15 0 [] nil!=cons(X,X2). % 1.94/2.15 0 [] proj1Arr(arr(X,X2))=X. % 1.94/2.15 0 [] proj2Arr(arr(X,X2))=X2. % 1.94/2.15 0 [] arr(X,X2)!=a. % 1.94/2.15 0 [] arr(X,X2)!=b. % 1.94/2.15 0 [] arr(X,X2)!=c. % 1.94/2.15 0 [] a!=b. % 1.94/2.15 0 [] a!=c. % 1.94/2.15 0 [] b!=c. % 1.94/2.15 0 [] proj1Suc(suc(X))=X. % 1.94/2.15 0 [] zero!=suc(X). % 1.94/2.15 0 [] proj1Just(just(X))=X. % 1.94/2.15 0 [] nothing!=just(X). % 1.94/2.15 0 [] proj1App(app(X,X2,X3))=X. % 1.94/2.15 0 [] proj2App(app(X,X2,X3))=X2. % 1.94/2.15 0 [] proj3App(app(X,X2,X3))=X3. % 1.94/2.15 0 [] proj1Lam(lam(X))=X. % 1.94/2.15 0 [] proj1Var(var(X))=X. % 1.94/2.15 0 [] app(X,X2,X3)!=lam(X4). % 1.94/2.15 0 [] app(X,X2,X3)!=var(X4). % 1.94/2.15 0 [] lam(X)!=var(X2). % 1.94/2.15 0 [] Y=lam(proj1Lam(Y))| -nf(app(Y,Z,X2))|nf(Y). % 1.94/2.15 0 [] Y=lam(proj1Lam(Y))| -nf(app(Y,Z,X2))|nf(Z). % 1.94/2.15 0 [] Y=lam(proj1Lam(Y))|nf(app(Y,Z,X2))| -nf(Y)| -nf(Z). % 1.94/2.15 0 [] -nf(app(lam(X3),Z,X2)). % 1.94/2.15 0 [] -nf(lam(E))|nf(E). % 1.94/2.15 0 [] nf(lam(E))| -nf(E). % 1.94/2.15 0 [] nf(var(X4)). % 1.94/2.15 0 [] index(nil,Y)=nothing. % 1.94/2.15 0 [] index(cons(Z,Xs),zero)=just(Z). % 1.94/2.15 0 [] index(cons(Z,Xs),suc(N))=index(Xs,N). % 1.94/2.15 0 [] -tc(X,app(F,X2,Tx),Z)|tc(X,F,arr(Tx,Z)). % 1.94/2.15 0 [] -tc(X,app(F,X2,Tx),Z)|tc(X,X2,Tx). % 1.94/2.15 0 [] tc(X,app(F,X2,Tx),Z)| -tc(X,F,arr(Tx,Z))| -tc(X,X2,Tx). % 1.94/2.15 0 [] Z=arr(proj1Arr(Z),proj2Arr(Z))| -tc(X,lam(E),Z). % 1.94/2.15 0 [] -tc(X,lam(E),arr(Tx2,T1))|tc(cons(Tx2,X),E,T1). % 1.94/2.15 0 [] tc(X,lam(E),arr(Tx2,T1))| -tc(cons(Tx2,X),E,T1). % 1.94/2.15 0 [] index(X,X3)!=nothing| -tc(X,var(X3),Z). % 1.94/2.15 0 [] index(X,X3)!=just(Tx3)| -tc(X,var(X3),Z)|Tx3=Z. % 1.94/2.15 0 [] index(X,X3)!=just(Tx3)|tc(X,var(X3),Z)|Tx3!=Z. % 1.94/2.15 0 [] -nf(E)| -tc(nil,E,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))). % 1.94/2.15 end_of_list. % 1.94/2.15 % 1.94/2.15 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4. % 1.94/2.15 % 1.94/2.15 This ia a non-Horn set with equality. The strategy will be % 1.94/2.15 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.94/2.15 deletion, with positive clauses in sos and nonpositive % 1.94/2.15 clauses in usable. % 1.94/2.15 % 1.94/2.15 dependent: set(knuth_bendix). % 1.94/2.15 dependent: set(anl_eq). % 1.94/2.15 dependent: set(para_from). % 1.94/2.15 dependent: set(para_into). % 1.94/2.15 dependent: clear(para_from_right). % 1.94/2.15 dependent: clear(para_into_right). % 1.94/2.15 dependent: set(para_from_vars). % 1.94/2.15 dependent: set(eq_units_both_ways). % 1.94/2.15 dependent: set(dynamic_demod_all). % 1.94/2.15 dependent: set(dynamic_demod). % 1.94/2.15 dependent: set(order_eq). % 1.94/2.15 dependent: set(back_demod). % 1.94/2.15 dependent: set(lrpo). % 1.94/2.15 dependent: set(hyper_res). % 1.94/2.15 dependent: set(unit_deletion). % 1.94/2.15 dependent: set(factor). % 1.94/2.15 % 1.94/2.15 ------------> process usable: % 1.94/2.15 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil. % 1.94/2.15 ** KEPT (pick-wt=5): 3 [] arr(A,B)!=a. % 1.94/2.15 ** KEPT (pick-wt=5): 4 [] arr(A,B)!=b. % 1.94/2.15 ** KEPT (pick-wt=5): 5 [] arr(A,B)!=c. % 1.94/2.15 ** KEPT (pick-wt=3): 7 [copy,6,flip.1] b!=a. % 1.94/2.15 ** KEPT (pick-wt=3): 9 [copy,8,flip.1] c!=a. % 1.94/2.15 ** KEPT (pick-wt=3): 11 [copy,10,flip.1] c!=b. % 1.94/2.15 ** KEPT (pick-wt=4): 13 [copy,12,flip.1] suc(A)!=zero. % 1.94/2.15 ** KEPT (pick-wt=4): 15 [copy,14,flip.1] just(A)!=nothing. % 1.94/2.15 ** KEPT (pick-wt=7): 16 [] app(A,B,C)!=lam(D). % 1.94/2.15 ** KEPT (pick-wt=7): 17 [] app(A,B,C)!=var(D). % 1.94/2.15 ** KEPT (pick-wt=5): 18 [] lam(A)!=var(B). % 1.94/2.15 ** KEPT (pick-wt=12): 20 [copy,19,flip.1] lam(proj1Lam(A))=A| -nf(app(A,B,C))|nf(A). % 1.94/2.15 ** KEPT (pick-wt=12): 22 [copy,21,flip.1] lam(proj1Lam(A))=A| -nf(app(A,B,C))|nf(B). % 1.94/2.15 ** KEPT (pick-wt=14): 24 [copy,23,flip.1] lam(proj1Lam(A))=A|nf(app(A,B,C))| -nf(A)| -nf(B). % 1.94/2.15 ** KEPT (pick-wt=6): 25 [] -nf(app(lam(A),B,C)). % 1.94/2.15 ** KEPT (pick-wt=5): 26 [] -nf(lam(A))|nf(A). % 1.94/2.15 ** KEPT (pick-wt=5): 27 [] nf(lam(A))| -nf(A). % 1.94/2.15 ** KEPT (pick-wt=13): 28 [] -tc(A,app(B,C,D),E)|tc(A,B,arr(D,E)). % 1.94/2.15 ** KEPT (pick-wt=11): 29 [] -tc(A,app(B,C,D),E)|tc(A,C,D). % 1.94/2.15 ** KEPT (pick-wt=17): 30 [] tc(A,app(B,C,D),E)| -tc(A,B,arr(D,E))| -tc(A,C,D). % 1.94/2.15 ** KEPT (pick-wt=12): 32 [copy,31,flip.1] arr(proj1Arr(A),proj2Arr(A))=A| -tc(B,lam(C),A). % 1.94/2.15 ** KEPT (pick-wt=13): 33 [] -tc(A,lam(B),arr(C,D))|tc(cons(C,A),B,D). % 1.94/2.15 ** KEPT (pick-wt=13): 34 [] tc(A,lam(B),arr(C,D))| -tc(cons(C,A),B,D). % 1.94/2.15 ** KEPT (pick-wt=10): 35 [] index(A,B)!=nothing| -tc(A,var(B),C). % 1.94/2.15 ** KEPT (pick-wt=14): 36 [] index(A,B)!=just(C)| -tc(A,var(B),D)|C=D. % 1.94/2.15 ** KEPT (pick-wt=14): 37 [] index(A,B)!=just(C)|tc(A,var(B),D)|C!=D. % 1.94/2.15 ** KEPT (pick-wt=16): 38 [] -nf(A)| -tc(nil,A,arr(arr(a,arr(b,c)),arr(b,arr(a,c)))). % 1.94/2.15 ** KEPT (pick-wt=7): 39 [copy,16,flip.1] lam(A)!=app(B,C,D). % 1.94/2.15 ** KEPT (pick-wt=7): 40 [copy,17,flip.1] var(A)!=app(B,C,D). % 1.94/2.15 ** KEPT (pick-wt=5): 41 [copy,18,flip.1] var(A)!=lam(B). % 1.94/2.15 Following clause subsumed by 16 during input processing: 0 [copy,39,flip.1] app(A,B,C)!=lam(D). % 1.94/2.15 Following clause subsumed by 17 during input processing: 0 [copy,40,flip.1] app(A,B,C)!=var(D). % 1.94/2.15 Following clause subsumed by 18 during input processing: 0 [copy,41,flip.1] lam(A)!=var(B). % 1.94/2.15 % 1.94/2.15 ------------> process sos: % 1.94/2.15 ** KEPT (pick-wt=3): 44 [] A=A. % 1.94/2.15 ** KEPT (pick-wt=6): 45 [] head(cons(A,B))=A. % 1.94/2.15 ---> New Demodulator: 46 [new_demod,45] head(cons(A,B))=A. % 1.94/2.15 ** KEPT (pick-wt=6): 47 [] tail(cons(A,B))=B. % 1.94/2.15 ---> New Demodulator: 48 [new_demod,47] tail(cons(A,B))=B. % 1.94/2.15 ** KEPT (pick-wt=6): 49 [] proj1Arr(arr(A,B))=A. % 1.94/2.15 ---> New Demodulator: 50 [new_demod,49] proj1Arr(arr(A,B))=A. % 1.94/2.15 ** KEPT (pick-wt=6): 51 [] proj2Arr(arr(A,B))=B. % 1.94/2.15 ---> New Demodulator: 52 [new_demod,51] proj2Arr(arr(A,B))=B. % 1.94/2.15 ** KEPT (pick-wt=5): 53 [] proj1Suc(suc(A))=A. % 1.94/2.15 ---> New Demodulator: 54 [new_demod,53] proj1Suc(suc(A))=A. % 1.94/2.15 ** KEPT (pick-wt=5): 55 [] proj1Just(just(A))=A. % 1.94/2.15 ---> New Demodulator: 56 [new_demod,55] proj1Just(just(A))=A. % 1.94/2.15 ** KEPT (pick-wt=7): 57 [] proj1App(app(A,B,C))=A. % 1.94/2.15 ---> New Demodulator: 58 [new_demod,57] proj1App(app(A,B,C))=A. % 1.94/2.15 ** KEPT (pick-wt=7): 59 [] proj2App(app(A,B,C))=B. % 1.94/2.15 ---> New Demodulator: 60 [new_demod,59] proj2App(app(A,B,C))=B. % 1.94/2.15 ** KEPT (pick-wt=7): 61 [] proj3App(app(A,B,C))=C. % 1.94/2.15 ---> New Demodulator: 62 [new_demod,61] proj3App(app(A,B,C))=C. % 1.94/2.15 ** KEPT (pick-wt=5): 63 [] proj1Lam(lam(A))=A. % 1.94/2.15 ---> New Demodulator: 64 [new_demod,63] proj1Lam(lam(A))=A. % 1.94/2.15 ** KEPT (pick-wt=5): 65 [] proj1Var(var(A))=A. % 1.94/2.15 ---> New Demodulator: 66 [new_demod,65] proj1Var(var(A))=A. % 1.94/2.15 ** KEPT (pick-wt=3): 67 [] nf(var(A)). % 1.94/2.15 ** KEPT (pick-wt=5): 68 [] index(nil,A)=nothing. % 1.94/2.15 ---> New Demodulator: 69 [new_demod,68] index(nil,A)=nothing. % 1.94/2.15 ** KEPT (pick-wt=8): 70 [] index(cons(A,B),zero)=just(A). % 1.94/2.15 ** KEPT (pick-wt=10): 71 [] index(cons(A,B),suc(C))=index(B,C). % 1.94/2.15 ---> New Demodulator: 72 [new_demod,71] index(cons(A,B),suc(C))=index(B,C). % 1.94/2.15 Following clause subsumed by 44 during input processing: 0 [copy,44,flip.1] A=A. % 1.94/2.15 >>>> Starting back demodulation with 46. % 1.94/2.15 >>>> Starting back demodulation with 48. % 15.62/15.85 >>>> Starting back demodulation with 50. % 15.62/15.85 >>>> Starting back demodulation with 52. % 15.62/15.85 >>>> Starting back demodulation with 54. % 15.62/15.85 >>>> Starting back demodulation with 56. % 15.62/15.85 >>>> Starting back demodulation with 58. % 15.62/15.85 >>>> Starting back demodulation with 60. % 15.62/15.85 >>>> Starting back demodulation with 62. % 15.62/15.85 >>>> Starting back demodulation with 64. % 15.62/15.85 >>>> Starting back demodulation with 66. % 15.62/15.85 >>>> Starting back demodulation with 69. % 15.62/15.85 ** KEPT (pick-wt=8): 73 [copy,70,flip.1] just(A)=index(cons(A,B),zero). % 15.62/15.85 >>>> Starting back demodulation with 72. % 15.62/15.85 Following clause subsumed by 70 during input processing: 0 [copy,73,flip.1] index(cons(A,B),zero)=just(A). % 15.62/15.85 % 15.62/15.85 ======= end of input processing ======= % 15.62/15.85 % 15.62/15.85 =========== start of search =========== % 15.62/15.85 % 15.62/15.85 % 15.62/15.85 Resetting weight limit to 15. % 15.62/15.85 % 15.62/15.85 % 15.62/15.85 Resetting weight limit to 15. % 15.62/15.85 % 15.62/15.85 sos_size=847 % 15.62/15.85 % 15.62/15.85 Search stopped because sos empty. % 15.62/15.85 % 15.62/15.85 % 15.62/15.85 Search stopped because sos empty. % 15.62/15.85 % 15.62/15.85 ============ end of search ============ % 15.62/15.85 % 15.62/15.85 -------------- statistics ------------- % 15.62/15.85 clauses given 1001 % 15.62/15.85 clauses generated 835563 % 15.62/15.85 clauses kept 1046 % 15.62/15.85 clauses forward subsumed 11923 % 15.62/15.85 clauses back subsumed 12 % 15.62/15.85 Kbytes malloced 6835 % 15.62/15.85 % 15.62/15.85 ----------- times (seconds) ----------- % 15.62/15.85 user CPU time 13.69 (0 hr, 0 min, 13 sec) % 15.62/15.85 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 15.62/15.85 wall-clock time 15 (0 hr, 0 min, 15 sec) % 15.62/15.85 % 15.62/15.85 Process 23353 finished Tue May 5 12:30:01 2026 % 15.62/15.85 Otter interrupted % 15.62/15.85 PROOF NOT FOUND %------------------------------------------------------------------------------