%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n019.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:08 PM UTC 2026 % Result : Theorem 0.77s 1.09s % Output : Refutation 248.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.33 % Computer : n019.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Wed Apr 29 02:16:43 EDT 2026 % 0.17/0.34 % CPUTime : % 0.77/1.02 ============================== Prover9 =============================== % 0.77/1.02 Prover9 (32) version 2009-11A, November 2009. % 0.77/1.02 Process 31193 was started by sandbox2 on n019.cluster.edu, % 0.77/1.02 Wed Apr 29 02:16:44 2026 % 0.77/1.02 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_30856_n019.cluster.edu". % 0.77/1.02 ============================== end of head =========================== % 0.77/1.02 % 0.77/1.02 ============================== INPUT ================================= % 0.77/1.02 % 0.77/1.02 % Reading from file /tmp/Prover9_30856_n019.cluster.edu % 0.77/1.02 % 0.77/1.02 set(prolog_style_variables). % 0.77/1.02 set(auto2). % 0.77/1.02 % set(auto2) -> set(auto). % 0.77/1.02 % set(auto) -> set(auto_inference). % 0.77/1.02 % set(auto) -> set(auto_setup). % 0.77/1.02 % set(auto_setup) -> set(predicate_elim). % 0.77/1.02 % set(auto_setup) -> assign(eq_defs, unfold). % 0.77/1.02 % set(auto) -> set(auto_limits). % 0.77/1.02 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.77/1.02 % set(auto_limits) -> assign(sos_limit, 20000). % 0.77/1.02 % set(auto) -> set(auto_denials). % 0.77/1.02 % set(auto) -> set(auto_process). % 0.77/1.02 % set(auto2) -> assign(new_constants, 1). % 0.77/1.02 % set(auto2) -> assign(fold_denial_max, 3). % 0.77/1.02 % set(auto2) -> assign(max_weight, "200.000"). % 0.77/1.02 % set(auto2) -> assign(max_hours, 1). % 0.77/1.02 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.77/1.02 % set(auto2) -> assign(max_seconds, 0). % 0.77/1.02 % set(auto2) -> assign(max_minutes, 5). % 0.77/1.02 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.77/1.02 % set(auto2) -> set(sort_initial_sos). % 0.77/1.02 % set(auto2) -> assign(sos_limit, -1). % 0.77/1.02 % set(auto2) -> assign(lrs_ticks, 3000). % 0.77/1.02 % set(auto2) -> assign(max_megs, 400). % 0.77/1.02 % set(auto2) -> assign(stats, some). % 0.77/1.02 % set(auto2) -> clear(echo_input). % 0.77/1.02 % set(auto2) -> set(quiet). % 0.77/1.02 % set(auto2) -> clear(print_initial_clauses). % 0.77/1.02 % set(auto2) -> clear(print_given). % 0.77/1.02 assign(lrs_ticks,-1). % 0.77/1.02 assign(sos_limit,10000). % 0.77/1.02 assign(order,kbo). % 0.77/1.02 set(lex_order_vars). % 0.77/1.02 clear(print_given). % 0.77/1.02 % 0.77/1.02 % formulas(sos). % not echoed (32 formulas) % 0.77/1.02 % 0.77/1.02 ============================== end of input ========================== % 0.77/1.02 % 0.77/1.02 % From the command line: assign(max_seconds, 300). % 0.77/1.02 % 0.77/1.02 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.77/1.02 % 0.77/1.02 % Formulas that are not ordinary clauses: % 0.77/1.02 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 4 (all X all X2 proj1Arr(arr(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 5 (all X all X2 proj2Arr(arr(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 6 (all X all X2 arr(X,X2) != a) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 7 (all X all X2 arr(X,X2) != b) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 8 (all X all X2 arr(X,X2) != c) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 9 (all X proj1Suc(suc(X)) = X) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 10 (all X zero != suc(X)) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 11 (all X proj1Just(just(X)) = X) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 12 (all X nothing != just(X)) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.77/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.77/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.77/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.77/1.02 16 (all X proj1Lam(lam(X)) = X) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.02 17 (all X proj1Var(var(X)) = X) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.77/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.77/1.02 19 (all X % 0.77/1.03 WARNING: denials share constants (see output). % 0.77/1.03 % 0.77/1.09 all X2 all X3 all X4 app(X,X2,X3) != var(X4)) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 20 (all X all X2 lam(X) != var(X2)) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 21 (all Y index(nil,Y) = nothing) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 22 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 23 (all Z all Xs all N index(cons(Z,Xs),suc(N)) = index(Xs,N)) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 24 (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_027) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 25 (all X all Z all E (Z != arr(proj1Arr(Z),proj2Arr(Z)) -> -tc(X,lam(E),Z))) # label(axiom_028) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 26 (all X all E all Tx2 all T1 (tc(X,lam(E),arr(Tx2,T1)) <-> tc(cons(Tx2,X),E,T1))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 27 (all X all Z all X3 (index(X,X3) = nothing -> -tc(X,var(X3),Z))) # label(axiom_030) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 28 (all X all Z all X3 all Tx3 (index(X,X3) = just(Tx3) -> (tc(X,var(X3),Z) <-> Tx3 = Z))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 29 -(exists E tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b)))) # label(goal_032) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.77/1.09 % 0.77/1.09 ============================== end of process non-clausal formulas === % 0.77/1.09 % 0.77/1.09 ============================== PROCESS INITIAL CLAUSES =============== % 0.77/1.09 % 0.77/1.09 ============================== PREDICATE ELIMINATION ================= % 0.77/1.09 % 0.77/1.09 ============================== end predicate elimination ============= % 0.77/1.09 % 0.77/1.09 Auto_denials: % 0.77/1.09 % copying label axiom_009 to answer in negative clause % 0.77/1.09 % copying label axiom_010 to answer in negative clause % 0.77/1.09 % copying label axiom_011 to answer in negative clause % 0.77/1.09 % copying label axiom_013 to answer in negative clause % 0.77/1.09 % copying label axiom_015 to answer in negative clause % 0.77/1.09 % copying label axiom_003 to answer in negative clause % 0.77/1.09 % copying label axiom_006 to answer in negative clause % 0.77/1.09 % copying label axiom_007 to answer in negative clause % 0.77/1.09 % copying label axiom_008 to answer in negative clause % 0.77/1.09 % copying label axiom_023 to answer in negative clause % 0.77/1.09 % copying label axiom_021 to answer in negative clause % 0.77/1.09 % copying label axiom_022 to answer in negative clause % 0.77/1.09 % copying label axiom_030 to answer in negative clause % 0.77/1.09 % copying label goal_032 to answer in negative clause % 0.77/1.09 % assign(max_proofs, 14). % (Horn set with more than one neg. clause) % 0.77/1.09 % 0.77/1.09 WARNING, because some of the denials share constants, % 0.77/1.09 some of the denials or their descendents may be subsumed, % 0.77/1.09 preventing the target number of proofs from being found. % 0.77/1.09 The shared constants are: nil, nothing, c, b, a. % 0.77/1.09 % 0.77/1.09 Term ordering decisions: % 0.77/1.09 Function symbol KB weights: nil=1. nothing=1. zero=1. a=1. b=1. c=1. arr=1. cons=1. index=1. just=1. lam=1. var=1. proj1Arr=1. proj2Arr=1. suc=1. head=1. proj1App=1. proj1Just=1. proj1Lam=1. proj1Suc=1. proj1Var=1. proj2App=1. proj3App=1. tail=1. app=1. % 0.77/1.09 % 0.77/1.09 ============================== end of process initial clauses ======== % 0.77/1.09 % 0.77/1.09 ============================== CLAUSES FOR SEARCH ==================== % 0.77/1.09 % 0.77/1.09 ============================== end of clauses for search ============= % 0.77/1.09 % 0.77/1.09 ============================== SEARCH ================================ % 0.77/1.09 % 0.77/1.09 % Starting search at 0.01 seconds. % 0.77/1.09 % 0.77/1.09 ============================== PROOF ================================= % 0.77/1.09 % SZS status Theorem % 0.77/1.09 % SZS output start Refutation % 0.77/1.09 % 0.77/1.09 % Proof 1 at 0.07 (+ 0.00) seconds: goal_032. % 0.77/1.09 % Length of proof is 24. % 0.77/1.09 % Level of proof is 7. % 0.77/1.09 % Maximum clause weight is 28.000. % 0.77/1.09 % Given clauses 88. % 0.77/1.09 % 0.77/1.09 15 (all X all X2 all X3 proj3App(app(X,X2,X3)) = X3) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 22 (all Z all Xs index(cons(Z,Xs),zero) = just(Z)) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.09 23 (all Z all Xs all N index(cons(Z,Xs),suc(N)) = index(Xs,N)) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 248.65/248.97 24 (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_027) # label(axiom) # label(non_clause). [assumption]. % 248.65/248.97 26 (all X all E all Tx2 all T1 (tc(X,lam(E),arr(Tx2,T1)) <-> tc(cons(Tx2,X),E,T1))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 248.65/248.97 28 (all X all Z all X3 all Tx3 (index(X,X3) = just(Tx3) -> (tc(X,var(X3),Z) <-> Tx3 = Z))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 248.65/248.97 29 -(exists E tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b)))) # label(goal_032) # label(negated_conjecture) # label(non_clause). [assumption]. % 248.65/248.97 41 proj3App(app(A,B,C)) = C # label(axiom_018) # label(axiom). [clausify(15)]. % 248.65/248.97 42 index(cons(A,B),zero) = just(A) # label(axiom_025) # label(axiom). [clausify(22)]. % 248.65/248.97 43 index(cons(A,B),suc(C)) = index(B,C) # label(axiom_026) # label(axiom). [clausify(23)]. % 248.65/248.97 60 -tc(nil,A,arr(arr(a,arr(a,b)),arr(a,b))) # label(goal_032) # label(negated_conjecture) # answer(goal_032). [clausify(29)]. % 248.65/248.97 65 tc(A,lam(B),arr(C,D)) | -tc(cons(C,A),B,D) # label(axiom_029) # label(axiom). [clausify(26)]. % 248.65/248.97 67 index(A,B) != just(C) | tc(A,var(B),D) | C != D # label(axiom_031) # label(axiom). [clausify(28)]. % 248.65/248.97 68 tc(A,app(B,C,D),E) | -tc(A,B,arr(D,E)) | -tc(A,C,D) # label(axiom_027) # label(axiom). [clausify(24)]. % 248.65/248.97 75 -tc(cons(arr(a,arr(a,b)),nil),A,arr(a,b)) # answer(goal_032). [ur(65,a,60,a)]. % 248.65/248.97 102 tc(cons(A,B),var(zero),A). [hyper(67,a,42,a,c,41,a),rewrite([41(2)])]. % 248.65/248.97 104 index(A,B) != just(C) | tc(cons(D,A),var(suc(B)),E) | C != E. [para(43(a,1),67(a,1))]. % 248.65/248.97 291 -tc(cons(a,cons(arr(a,arr(a,b)),nil)),A,b) # answer(goal_032). [ur(65,a,75,a)]. % 248.65/248.97 306 tc(cons(A,cons(B,C)),var(suc(zero)),B). [hyper(104,a,42,a,c,41,a),rewrite([41(2)])]. % 248.65/248.97 330 tc(cons(A,cons(arr(A,B),C)),app(var(suc(zero)),var(zero),A),B). [hyper(68,b,306,a,c,102,a)]. % 248.65/248.97 331 tc(cons(A,B),lam(var(suc(zero))),arr(C,A)). [hyper(65,b,306,a)]. % 248.65/248.97 354 tc(cons(A,B),app(lam(var(suc(zero))),var(zero),A),A). [hyper(68,b,331,a,c,102,a)]. % 248.65/248.97 610 tc(cons(A,cons(arr(A,arr(A,B)),C)),app(app(var(suc(zero)),var(zero),A),app(lam(var(suc(zero))),var(zero),A),A),B). [hyper(68,b,330,a,c,354,a)]. % 248.65/248.97 611 $F # answer(goal_032). [resolve(610,a,291,a)]. % 248.65/248.97 % 248.65/248.97 % SZS output end Refutation % 248.65/248.97 ============================== end of proof ========================== % 248.65/248.97 % Redundant proof: 621 $F # answer(goal_032). [resolve(620,a,291,a)]. % 248.65/248.97 % Redundant proof: 625 $F # answer(goal_032). [resolve(624,a,291,a)]. % 248.65/248.97 % 248.65/248.97 % Disable descendants (x means already disabled): % 248.65/248.97 60 70 74x 75 132 139 145 146 181 196x % 248.65/248.97 197x 283 284 285 286 287 288 289 290 291 % 248.65/248.97 292x 293 356 385 386 387 388 391 392 393 % 248.65/248.97 394 395 396 397 398 399 400 401 402 403 % 248.65/248.97 404 405 406 407 408 409 410 537 538 539 % 248.65/248.97 540 541 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=52.000, iters=3444 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=51.000, iters=3412 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=49.000, iters=3357 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=46.000, iters=3387 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=44.000, iters=3399 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=43.000, iters=3348 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=42.000, iters=3387 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=41.000, iters=3371 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=40.000, iters=3412 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=38.000, iters=3346 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=37.000, iters=3409 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=36.000, iters=3339 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=35.000, iters=3367 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=34.000, iters=3355 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=33.000, iters=3381 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=32.000, iters=3337 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=31.000, iters=3351 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=30.000, iters=3343 % 248.65/248.97 % 248.65/248.97 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 784 (0.00 of 0.98 sec). % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=29.000, iters=3334 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=28.000, iters=3333 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=3214, wt=76.000 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=3226, wt=75.000 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=3527, wt=69.000 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=3205, wt=68.000 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=3217, wt=65.000 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=3231, wt=64.000 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=12284, wt=19.000 % 248.65/248.97 % 248.65/248.97 Low Water (displace): id=12393, wt=18.000 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=25.000, iters=3333 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=23.000, iters=3333 % 248.65/248.97 % 248.65/248.97 Low Water (keep): wt=21.Terminated % 299.77/300.03 Prover9 interrupted %------------------------------------------------------------------------------