%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX223+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n012.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 : Wed Apr 29 02:38:07 PM UTC 2026 % Result : Theorem 10.82s 11.14s % Output : Refutation 10.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SWX223+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : tptp2X_and_run_prover9 %d %s % 0.07/0.25 % Computer : n012.cluster.edu % 0.07/0.25 % Model : x86_64 x86_64 % 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.25 % Memory : 8042.1875MB % 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.25 % CPULimit : 300 % 0.07/0.25 % WCLimit : 300 % 0.07/0.25 % DateTime : Wed Apr 29 02:11:15 EDT 2026 % 0.07/0.25 % CPUTime : % 0.39/0.71 ============================== Prover9 =============================== % 0.39/0.71 Prover9 (32) version 2009-11A, November 2009. % 0.39/0.71 Process 6857 was started by sandbox2 on n012.cluster.edu, % 0.39/0.71 Wed Apr 29 02:11:16 2026 % 0.39/0.71 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_6703_n012.cluster.edu". % 0.39/0.71 ============================== end of head =========================== % 0.39/0.71 % 0.39/0.71 ============================== INPUT ================================= % 0.39/0.71 % 0.39/0.71 % Reading from file /tmp/Prover9_6703_n012.cluster.edu % 0.39/0.71 % 0.39/0.71 set(prolog_style_variables). % 0.39/0.71 set(auto2). % 0.39/0.71 % set(auto2) -> set(auto). % 0.39/0.71 % set(auto) -> set(auto_inference). % 0.39/0.71 % set(auto) -> set(auto_setup). % 0.39/0.71 % set(auto_setup) -> set(predicate_elim). % 0.39/0.71 % set(auto_setup) -> assign(eq_defs, unfold). % 0.39/0.71 % set(auto) -> set(auto_limits). % 0.39/0.71 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.39/0.71 % set(auto_limits) -> assign(sos_limit, 20000). % 0.39/0.71 % set(auto) -> set(auto_denials). % 0.39/0.71 % set(auto) -> set(auto_process). % 0.39/0.71 % set(auto2) -> assign(new_constants, 1). % 0.39/0.71 % set(auto2) -> assign(fold_denial_max, 3). % 0.39/0.71 % set(auto2) -> assign(max_weight, "200.000"). % 0.39/0.71 % set(auto2) -> assign(max_hours, 1). % 0.39/0.71 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.39/0.71 % set(auto2) -> assign(max_seconds, 0). % 0.39/0.71 % set(auto2) -> assign(max_minutes, 5). % 0.39/0.71 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.39/0.71 % set(auto2) -> set(sort_initial_sos). % 0.39/0.71 % set(auto2) -> assign(sos_limit, -1). % 0.39/0.71 % set(auto2) -> assign(lrs_ticks, 3000). % 0.39/0.71 % set(auto2) -> assign(max_megs, 400). % 0.39/0.71 % set(auto2) -> assign(stats, some). % 0.39/0.71 % set(auto2) -> clear(echo_input). % 0.39/0.71 % set(auto2) -> set(quiet). % 0.39/0.71 % set(auto2) -> clear(print_initial_clauses). % 0.39/0.71 % set(auto2) -> clear(print_given). % 0.39/0.71 assign(lrs_ticks,-1). % 0.39/0.71 assign(sos_limit,10000). % 0.39/0.71 assign(order,kbo). % 0.39/0.71 set(lex_order_vars). % 0.39/0.71 clear(print_given). % 0.39/0.71 % 0.39/0.71 % formulas(sos). % not echoed (36 formulas) % 0.39/0.71 % 0.39/0.71 ============================== end of input ========================== % 0.39/0.71 % 0.39/0.71 % From the command line: assign(max_seconds, 300). % 0.39/0.71 % 0.39/0.71 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.39/0.71 % 0.39/0.71 % Formulas that are not ordinary clauses: % 0.39/0.71 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 4 (all X all X2 proj1Arr(arr(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 5 (all X all X2 proj2Arr(arr(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 6 (all X all X2 arr(X,X2) != a) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 7 (all X all X2 arr(X,X2) != b) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 8 (all X all X2 arr(X,X2) != c) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 9 (all X proj1Suc(suc(X)) = X) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 10 (all X zero != suc(X)) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 11 (all X proj1Just(just(X)) = X) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 12 (all X nothing != just(X)) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 13 (all X all X2 all X3 proj1App(app(X,X2,X3)) = X) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 14 (all X all X2 all X3 proj2App(app(X,X2,X3)) = X2) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 16 (all X proj1Lam(lam(X)) = X) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 17 (all X proj1Var(var(X)) = X) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 18 (all X all X2 all X3 all X4 app(X,X2,X3) != lam(X4)) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.39/0.71 19 (all X all X2 all X3 all X4 app(X,X2,X3) != var(X4)) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 20 (all X all X2 lam(X) != var(X2)) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 21 (all Y all Z all X2 (Y != lam(proj1Lam(Y)) -> (nf(app(Y,Z,X2)) <-> nf(Y) & nf(Z)))) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 22 (all Z all X2 all X3 -nf(app(lam(X3),Z,X2))) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 23 (all E (nf(lam(E)) <-> nf(E))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 24 (all X4 nf(var(X4))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 25 (all Y index(nil,Y) = nothing) # label(axiom_028) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 26 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 27 (all Z all Xs all N index(cons(Z,Xs),suc(N)) = index(Xs,N)) # label(axiom_030) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 28 (all X all Z all F all X2 all Tx (tc(X,app(F,X2,Tx),Z) <-> tc(X,F,arr(Tx,Z)) & tc(X,X2,Tx))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 29 (all X all Z all E (Z != arr(proj1Arr(Z),proj2Arr(Z)) -> -tc(X,lam(E),Z))) # label(axiom_032) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 30 (all X all E all Tx2 all T1 (tc(X,lam(E),arr(Tx2,T1)) <-> tc(cons(Tx2,X),E,T1))) # label(axiom_033) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 31 (all X all Z all X3 (index(X,X3) = nothing -> -tc(X,var(X3),Z))) # label(axiom_034) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 32 (all X all Z all X3 all Tx3 (index(X,X3) = just(Tx3) -> (tc(X,var(X3),Z) <-> Tx3 = Z))) # label(axiom_035) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 33 -(exists E (nf(E) & tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))))) # label(goal_036) # label(negated_conjecture) # label(non_clause). [assumption]. % 10.82/11.14 % 10.82/11.14 ============================== end of process non-clausal formulas === % 10.82/11.14 % 10.82/11.14 ============================== PROCESS INITIAL CLAUSES =============== % 10.82/11.14 % 10.82/11.14 ============================== PREDICATE ELIMINATION ================= % 10.82/11.14 % 10.82/11.14 ============================== end predicate elimination ============= % 10.82/11.14 % 10.82/11.14 Auto_denials: (non-Horn, no changes). % 10.82/11.14 % 10.82/11.14 Term ordering decisions: % 10.82/11.14 Function symbol KB weights: nil=1. nothing=1. zero=1. a=1. b=1. c=1. arr=1. cons=1. index=1. lam=1. just=1. proj1Lam=1. var=1. proj1Arr=1. proj2Arr=1. suc=1. head=1. proj1App=1. proj1Just=1. proj1Suc=1. proj1Var=1. proj2App=1. proj3App=1. tail=1. app=1. % 10.82/11.14 % 10.82/11.14 ============================== end of process initial clauses ======== % 10.82/11.14 % 10.82/11.14 ============================== CLAUSES FOR SEARCH ==================== % 10.82/11.14 % 10.82/11.14 ============================== end of clauses for search ============= % 10.82/11.14 % 10.82/11.14 ============================== SEARCH ================================ % 10.82/11.14 % 10.82/11.14 % Starting search at 0.01 seconds. % 10.82/11.14 % 10.82/11.14 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 147 (0.00 of 0.21 sec). % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=28.000, iters=3339 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=27.000, iters=3336 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=26.000, iters=3345 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=25.000, iters=3333 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=24.000, iters=3333 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=23.000, iters=3336 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=22.000, iters=3348 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=21.000, iters=3350 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=20.000, iters=3336 % 10.82/11.14 % 10.82/11.14 Low Water (keep): wt=19.000, iters=3333 % 10.82/11.14 % 10.82/11.14 ============================== PROOF ================================= % 10.82/11.14 % SZS status Theorem % 10.82/11.14 % SZS output start Refutation % 10.82/11.14 % 10.82/11.14 % Proof 1 at 9.93 (+ 0.50) seconds. % 10.82/11.14 % Length of proof is 42. % 10.82/11.14 % Level of proof is 9. % 10.82/11.14 % Maximum clause weight is 23.000. % 10.82/11.14 % Given clauses 5469. % 10.82/11.14 % 10.82/11.14 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 18 (all X all X2 all X3 all X4 app(X,X2,X3) != lam(X4)) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 20 (all X all X2 lam(X) != var(X2)) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 21 (all Y all Z all X2 (Y != lam(proj1Lam(Y)) -> (nf(app(Y,Z,X2)) <-> nf(Y) & nf(Z)))) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 23 (all E (nf(lam(E)) <-> nf(E))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 24 (all X4 nf(var(X4))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 26 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 27 (all Z all Xs all N index(cons(Z,Xs),suc(N)) = index(Xs,N)) # label(axiom_030) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 28 (all X all Z all F all X2 all Tx (tc(X,app(F,X2,Tx),Z) <-> tc(X,F,arr(Tx,Z)) & tc(X,X2,Tx))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 30 (all X all E all Tx2 all T1 (tc(X,lam(E),arr(Tx2,T1)) <-> tc(cons(Tx2,X),E,T1))) # label(axiom_033) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 32 (all X all Z all X3 all Tx3 (index(X,X3) = just(Tx3) -> (tc(X,var(X3),Z) <-> Tx3 = Z))) # label(axiom_035) # label(axiom) # label(non_clause). [assumption]. % 10.82/11.14 33 -(exists E (nf(E) & tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))))) # label(goal_036) # label(negated_conjecture) # label(non_clause). [assumption]. % 10.82/11.14 34 nf(var(A)) # label(axiom_027) # label(axiom). [clausify(24)]. % 10.82/11.14 46 proj3App(app(A,B,C)) = C # label(axiom_018) # label(axiom). [clausify(15)]. % 10.82/11.14 47 index(cons(A,B),zero) = just(A) # label(axiom_029) # label(axiom). [clausify(26)]. % 10.82/11.14 48 index(cons(A,B),suc(C)) = index(B,C) # label(axiom_030) # label(axiom). [clausify(27)]. % 10.82/11.14 61 var(A) != lam(B) # label(axiom_023) # label(axiom). [clausify(20)]. % 10.82/11.14 63 lam(A) != app(B,C,D) # label(axiom_021) # label(axiom). [clausify(18)]. % 10.82/11.14 66 -nf(A) | -tc(nil,A,arr(arr(a,arr(a,b)),arr(a,b))) # label(goal_036) # label(negated_conjecture). [clausify(33)]. % 10.82/11.14 68 nf(lam(A)) | -nf(A) # label(axiom_026) # label(axiom). [clausify(23)]. % 10.82/11.14 75 tc(A,lam(B),arr(C,D)) | -tc(cons(C,A),B,D) # label(axiom_033) # label(axiom). [clausify(30)]. % 10.82/11.14 76 lam(proj1Lam(A)) = A | nf(app(A,B,C)) | -nf(A) | -nf(B) # label(axiom_024) # label(axiom). [clausify(21)]. % 10.82/11.14 78 index(A,B) != just(C) | tc(A,var(B),D) | C != D # label(axiom_035) # label(axiom). [clausify(32)]. % 10.82/11.14 79 tc(A,app(B,C,D),E) | -tc(A,B,arr(D,E)) | -tc(A,C,D) # label(axiom_031) # label(axiom). [clausify(28)]. % 10.82/11.14 91 nf(app(var(A),B,C)) | -nf(B). [resolve(76,c,34,a),unit_del(a(flip),61)]. % 10.82/11.14 92 lam(proj1Lam(A)) = A | nf(app(A,var(B),C)) | -nf(A). [resolve(76,d,34,a)]. % 10.82/11.14 117 tc(cons(A,B),var(zero),C) | A != C. [resolve(78,a,47,a)]. % 10.82/11.14 122 index(A,B) != just(C) | tc(cons(D,A),var(suc(B)),E) | C != E. [para(48(a,1),78(a,1))]. % 10.82/11.14 172 nf(app(var(A),var(B),C)). [resolve(91,b,34,a)]. % 10.82/11.14 237 tc(cons(A,B),var(zero),A). [resolve(117,b,46,a),rewrite([46(2)])]. % 10.82/11.14 238 tc(cons(A,B),app(C,var(zero),A),D) | -tc(cons(A,B),C,arr(A,D)). [resolve(237,a,79,c)]. % 10.82/11.14 253 nf(app(app(var(A),var(B),C),var(D),E)). [resolve(92,c,172,a),unit_del(a,63)]. % 10.82/11.14 337 nf(lam(app(app(var(A),var(B),C),var(D),E))). [resolve(253,a,68,b)]. % 10.82/11.14 479 nf(lam(lam(app(app(var(A),var(B),C),var(D),E)))). [resolve(337,a,68,b)]. % 10.82/11.14 663 tc(cons(A,cons(B,C)),var(suc(zero)),D) | B != D. [resolve(122,a,47,a)]. % 10.82/11.14 721 -tc(nil,lam(lam(app(app(var(A),var(B),C),var(D),E))),arr(arr(a,arr(a,b)),arr(a,b))). [ur(66,a,479,a)]. % 10.82/11.14 789 tc(cons(A,cons(B,C)),var(suc(zero)),B). [resolve(663,b,46,a),rewrite([46(2)])]. % 10.82/11.14 3220 tc(cons(A,cons(arr(A,B),C)),app(var(suc(zero)),var(zero),A),B). [resolve(238,b,789,a)]. % 10.82/11.14 4559 tc(cons(A,cons(arr(A,arr(A,B)),C)),app(app(var(suc(zero)),var(zero),A),var(zero),A),B). [resolve(3220,a,238,b)]. % 10.82/11.14 8929 -tc(cons(arr(a,arr(a,b)),nil),lam(app(app(var(A),var(B),C),var(D),E)),arr(a,b)). [ur(75,a,721,a)]. % 10.82/11.14 14063 tc(cons(arr(A,arr(A,B)),C),lam(app(app(var(suc(zero)),var(zero),A),var(zero),A)),arr(A,B)). [resolve(4559,a,75,b)]. % 10.82/11.14 14064 $F. [resolve(14063,a,8929,a)]. % 10.82/11.14 % 10.82/11.14 % SZS output end Refutation % 10.82/11.14 ============================== end of proof ========================== % 10.82/11.14 % 10.82/11.14 ============================== STATISTICS ============================ % 10.82/11.14 % 10.82/11.14 Given=5469. Generated=812372. Kept=14027. proofs=1. % 10.82/11.14 Usable=5468. Sos=8533. Demods=14. Limbo=0, Disabled=68. Hints=0. % 10.82/11.14 Megabytes=13.31. % 10.82/11.14 User_CPU=9.93, System_CPU=0.50, Wall_clock=10. % 10.82/11.14 % 10.82/11.14 ============================== end of statistics ===================== % 10.82/11.14 % 10.82/11.14 ============================== end of search ========================= % 10.82/11.14 % 10.82/11.14 THEOREM PROVED % 10.82/11.14 % SZS status Theorem % 10.82/11.14 % 10.82/11.14 Exiting with 1 proof. % 10.82/11.14 % 10.82/11.14 Process 6857 exit (max_proofs) Wed Apr 29 02:11:26 2026 % 10.82/11.14 Prover9 interrupted %------------------------------------------------------------------------------