%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n002.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 0.74s 1.04s % Output : Refutation 0.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX222+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.14/0.32 % Computer : n002.cluster.edu % 0.14/0.32 % Model : x86_64 x86_64 % 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.32 % Memory : 8042.1875MB % 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.32 % CPULimit : 300 % 0.14/0.32 % WCLimit : 300 % 0.14/0.32 % DateTime : Wed Apr 29 02:08:31 EDT 2026 % 0.14/0.32 % CPUTime : % 0.41/1.01 ============================== Prover9 =============================== % 0.41/1.01 Prover9 (32) version 2009-11A, November 2009. % 0.41/1.01 Process 12003 was started by sandbox on n002.cluster.edu, % 0.41/1.01 Wed Apr 29 02:08:32 2026 % 0.41/1.01 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_11850_n002.cluster.edu". % 0.41/1.01 ============================== end of head =========================== % 0.41/1.01 % 0.41/1.01 ============================== INPUT ================================= % 0.41/1.01 % 0.41/1.01 % Reading from file /tmp/Prover9_11850_n002.cluster.edu % 0.41/1.01 % 0.41/1.01 set(prolog_style_variables). % 0.41/1.01 set(auto2). % 0.41/1.01 % set(auto2) -> set(auto). % 0.41/1.01 % set(auto) -> set(auto_inference). % 0.41/1.01 % set(auto) -> set(auto_setup). % 0.41/1.01 % set(auto_setup) -> set(predicate_elim). % 0.41/1.01 % set(auto_setup) -> assign(eq_defs, unfold). % 0.41/1.01 % set(auto) -> set(auto_limits). % 0.41/1.01 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.41/1.01 % set(auto_limits) -> assign(sos_limit, 20000). % 0.41/1.01 % set(auto) -> set(auto_denials). % 0.41/1.01 % set(auto) -> set(auto_process). % 0.41/1.01 % set(auto2) -> assign(new_constants, 1). % 0.41/1.01 % set(auto2) -> assign(fold_denial_max, 3). % 0.41/1.01 % set(auto2) -> assign(max_weight, "200.000"). % 0.41/1.01 % set(auto2) -> assign(max_hours, 1). % 0.41/1.01 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.41/1.01 % set(auto2) -> assign(max_seconds, 0). % 0.41/1.01 % set(auto2) -> assign(max_minutes, 5). % 0.41/1.01 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.41/1.01 % set(auto2) -> set(sort_initial_sos). % 0.41/1.01 % set(auto2) -> assign(sos_limit, -1). % 0.41/1.01 % set(auto2) -> assign(lrs_ticks, 3000). % 0.41/1.01 % set(auto2) -> assign(max_megs, 400). % 0.41/1.01 % set(auto2) -> assign(stats, some). % 0.41/1.01 % set(auto2) -> clear(echo_input). % 0.41/1.01 % set(auto2) -> set(quiet). % 0.41/1.01 % set(auto2) -> clear(print_initial_clauses). % 0.41/1.01 % set(auto2) -> clear(print_given). % 0.41/1.01 assign(lrs_ticks,-1). % 0.41/1.01 assign(sos_limit,10000). % 0.41/1.01 assign(order,kbo). % 0.41/1.01 set(lex_order_vars). % 0.41/1.01 clear(print_given). % 0.41/1.01 % 0.41/1.01 % formulas(sos). % not echoed (36 formulas) % 0.41/1.01 % 0.41/1.01 ============================== end of input ========================== % 0.41/1.01 % 0.41/1.01 % From the command line: assign(max_seconds, 300). % 0.41/1.01 % 0.41/1.01 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.41/1.02 % 0.41/1.02 % Formulas that are not ordinary clauses: % 0.41/1.02 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 4 (all X all X2 proj1Arr(arr(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 5 (all X all X2 proj2Arr(arr(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 6 (all X all X2 arr(X,X2) != a) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 7 (all X all X2 arr(X,X2) != b) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 8 (all X all X2 arr(X,X2) != c) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 9 (all X proj1Suc(suc(X)) = X) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 10 (all X zero != suc(X)) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 11 (all X proj1Just(just(X)) = X) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 12 (all X nothing != just(X)) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 13 (all X all X2 all X3 proj1App(app(X,X2,X3)) = X) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 14 (all X all X2 all X3 proj2App(app(X,X2,X3)) = X2) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 16 (all X proj1Lam(lam(X)) = X) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 17 (all X proj1Var(var(X)) = X) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.41/1.02 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.41/1.02 19 (all X all X2 all X3 all X4 app(X,X2,X3) != var(X4)) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 20 (all X all X2 lam(X) != var(X2)) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 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]. % 0.74/1.04 22 (all Z all X2 all X3 -nf(app(lam(X3),Z,X2))) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 23 (all E (nf(lam(E)) <-> nf(E))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 24 (all X4 nf(var(X4))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 25 (all Y index(nil,Y) = nothing) # label(axiom_028) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 26 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 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]. % 0.74/1.04 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]. % 0.74/1.04 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]. % 0.74/1.04 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]. % 0.74/1.04 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]. % 0.74/1.04 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]. % 0.74/1.04 33 -(exists E (nf(E) & tc(nil,E,arr(a,arr(b,b))))) # label(goal_036) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.74/1.04 % 0.74/1.04 ============================== end of process non-clausal formulas === % 0.74/1.04 % 0.74/1.04 ============================== PROCESS INITIAL CLAUSES =============== % 0.74/1.04 % 0.74/1.04 ============================== PREDICATE ELIMINATION ================= % 0.74/1.04 % 0.74/1.04 ============================== end predicate elimination ============= % 0.74/1.04 % 0.74/1.04 Auto_denials: (non-Horn, no changes). % 0.74/1.04 % 0.74/1.04 Term ordering decisions: % 0.74/1.04 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. % 0.74/1.04 % 0.74/1.04 ============================== end of process initial clauses ======== % 0.74/1.04 % 0.74/1.04 ============================== CLAUSES FOR SEARCH ==================== % 0.74/1.04 % 0.74/1.04 ============================== end of clauses for search ============= % 0.74/1.04 % 0.74/1.04 ============================== SEARCH ================================ % 0.74/1.04 % 0.74/1.04 % Starting search at 0.02 seconds. % 0.74/1.04 % 0.74/1.04 ============================== PROOF ================================= % 0.74/1.04 % SZS status Theorem % 0.74/1.04 % SZS output start Refutation % 0.74/1.04 % 0.74/1.04 % Proof 1 at 0.03 (+ 0.00) seconds. % 0.74/1.04 % Length of proof is 22. % 0.74/1.04 % Level of proof is 6. % 0.74/1.04 % Maximum clause weight is 14.000. % 0.74/1.04 % Given clauses 88. % 0.74/1.04 % 0.74/1.04 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 23 (all E (nf(lam(E)) <-> nf(E))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 24 (all X4 nf(var(X4))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 26 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 0.74/1.04 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]. % 0.74/1.04 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]. % 0.74/1.04 33 -(exists E (nf(E) & tc(nil,E,arr(a,arr(b,b))))) # label(goal_036) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.74/1.04 34 nf(var(A)) # label(axiom_027) # label(axiom). [clausify(24)]. % 0.74/1.04 46 proj3App(app(A,B,C)) = C # label(axiom_018) # label(axiom). [clausify(15)]. % 0.74/1.04 47 index(cons(A,B),zero) = just(A) # label(axiom_029) # label(axiom). [clausify(26)]. % 0.74/1.04 66 -nf(A) | -tc(nil,A,arr(a,arr(b,b))) # label(goal_036) # label(negated_conjecture). [clausify(33)]. % 0.74/1.04 68 nf(lam(A)) | -nf(A) # label(axiom_026) # label(axiom). [clausify(23)]. % 0.74/1.04 75 tc(A,lam(B),arr(C,D)) | -tc(cons(C,A),B,D) # label(axiom_033) # label(axiom). [clausify(30)]. % 0.74/1.04 78 index(A,B) != just(C) | tc(A,var(B),D) | C != D # label(axiom_035) # label(axiom). [clausify(32)]. % 0.74/1.04 84 nf(lam(var(A))). [resolve(68,b,34,a)]. % 0.74/1.04 117 tc(cons(A,B),var(zero),C) | A != C. [resolve(78,a,47,a)]. % 0.74/1.04 138 nf(lam(lam(var(A)))). [resolve(84,a,68,b)]. % 0.74/1.04 142 -tc(nil,lam(lam(var(A))),arr(a,arr(b,b))). [ur(66,a,138,a)]. % 0.74/1.04 237 tc(cons(A,B),var(zero),A). [resolve(117,b,46,a),rewrite([46(2)])]. % 0.74/1.04 241 tc(A,lam(var(zero)),arr(B,B)). [resolve(237,a,75,b)]. % 0.74/1.04 270 tc(A,lam(lam(var(zero))),arr(B,arr(C,C))). [resolve(241,a,75,b)]. % 0.74/1.04 271 $F. [resolve(270,a,142,a)]. % 0.74/1.04 % 0.74/1.04 % SZS output end Refutation % 0.74/1.04 ============================== end of proof ========================== % 0.74/1.04 % 0.74/1.04 ============================== STATISTICS ============================ % 0.74/1.04 % 0.74/1.04 Given=88. Generated=590. Kept=234. proofs=1. % 0.74/1.04 Usable=87. Sos=134. Demods=14. Limbo=2, Disabled=53. Hints=0. % 0.74/1.04 Megabytes=0.29. % 0.74/1.04 User_CPU=0.03, System_CPU=0.00, Wall_clock=0. % 0.74/1.04 % 0.74/1.04 ============================== end of statistics ===================== % 0.74/1.04 % 0.74/1.04 ============================== end of search ========================= % 0.74/1.04 % 0.74/1.04 THEOREM PROVED % 0.74/1.04 % SZS status Theorem % 0.74/1.04 % 0.74/1.04 Exiting with 1 proof. % 0.74/1.04 % 0.74/1.04 Process 12003 exit (max_proofs) Wed Apr 29 02:08:32 2026 % 0.74/1.04 Prover9 interrupted %------------------------------------------------------------------------------