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