%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n026.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:06 PM UTC 2026 % Result : Theorem 0.77s 1.03s % Output : Refutation 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.16/0.34 % Computer : n026.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Wed Apr 29 01:46:23 EDT 2026 % 0.16/0.34 % CPUTime : % 0.45/1.00 ============================== Prover9 =============================== % 0.45/1.00 Prover9 (32) version 2009-11A, November 2009. % 0.45/1.00 Process 31758 was started by sandbox on n026.cluster.edu, % 0.45/1.00 Wed Apr 29 01:46:24 2026 % 0.45/1.00 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_31605_n026.cluster.edu". % 0.45/1.00 ============================== end of head =========================== % 0.45/1.00 % 0.45/1.00 ============================== INPUT ================================= % 0.45/1.00 % 0.45/1.00 % Reading from file /tmp/Prover9_31605_n026.cluster.edu % 0.45/1.00 % 0.45/1.00 set(prolog_style_variables). % 0.45/1.00 set(auto2). % 0.45/1.00 % set(auto2) -> set(auto). % 0.45/1.00 % set(auto) -> set(auto_inference). % 0.45/1.00 % set(auto) -> set(auto_setup). % 0.45/1.00 % set(auto_setup) -> set(predicate_elim). % 0.45/1.00 % set(auto_setup) -> assign(eq_defs, unfold). % 0.45/1.00 % set(auto) -> set(auto_limits). % 0.45/1.00 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.45/1.00 % set(auto_limits) -> assign(sos_limit, 20000). % 0.45/1.00 % set(auto) -> set(auto_denials). % 0.45/1.00 % set(auto) -> set(auto_process). % 0.45/1.00 % set(auto2) -> assign(new_constants, 1). % 0.45/1.00 % set(auto2) -> assign(fold_denial_max, 3). % 0.45/1.00 % set(auto2) -> assign(max_weight, "200.000"). % 0.45/1.00 % set(auto2) -> assign(max_hours, 1). % 0.45/1.00 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.45/1.00 % set(auto2) -> assign(max_seconds, 0). % 0.45/1.00 % set(auto2) -> assign(max_minutes, 5). % 0.45/1.00 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.45/1.00 % set(auto2) -> set(sort_initial_sos). % 0.45/1.00 % set(auto2) -> assign(sos_limit, -1). % 0.45/1.00 % set(auto2) -> assign(lrs_ticks, 3000). % 0.45/1.00 % set(auto2) -> assign(max_megs, 400). % 0.45/1.00 % set(auto2) -> assign(stats, some). % 0.45/1.00 % set(auto2) -> clear(echo_input). % 0.45/1.00 % set(auto2) -> set(quiet). % 0.45/1.00 % set(auto2) -> clear(print_initial_clauses). % 0.45/1.00 % set(auto2) -> clear(print_given). % 0.45/1.00 assign(lrs_ticks,-1). % 0.45/1.00 assign(sos_limit,10000). % 0.45/1.00 assign(order,kbo). % 0.45/1.00 set(lex_order_vars). % 0.45/1.00 clear(print_given). % 0.45/1.00 % 0.45/1.00 % formulas(sos). % not echoed (24 formulas) % 0.45/1.00 % 0.45/1.00 ============================== end of input ========================== % 0.45/1.00 % 0.45/1.00 % From the command line: assign(max_seconds, 300). % 0.45/1.00 % 0.45/1.00 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.45/1.00 % 0.45/1.00 % Formulas that are not ordinary clauses: % 0.45/1.00 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 4 (all X proj1Suc(suc(X)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 5 (all X zero != suc(X)) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 6 (all N half(suc(suc(N))) = suc(half(N))) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 7 (all N (evenNat(suc(N)) <-> -evenNat(N))) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 8 (all Y (evenNat(suc(Y)) -> shw(suc(Y)) = cons(o,shw(half(suc(Y)))))) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 9 (all Y (-evenNat(suc(Y)) -> shw(suc(Y)) = cons(i,shw(half(suc(Y)))))) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 10 (all Y append(nil,Y) = Y) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 11 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 12 (all Y addNat(zero,Y) = Y) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 13 (all Y all Z addNat(suc(Z),Y) = suc(addNat(Z,Y))) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 14 (all X double(X) = addNat(X,X)) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 15 (all Xs rd(cons(i,Xs)) = suc(double(rd(Xs)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 16 (all Xs rd(cons(o,Xs)) = double(rd(Xs))) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 17 (all X all Y x(X,Y) = rd(append(shw(X),shw(Y)))) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.45/1.00 18 -(exists X exists Y x(X,Y) != x(Y,X)) # label(goal_024) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.77/1.03 % 0.77/1.03 ============================== end of process non-clausal formulas === % 0.77/1.03 % 0.77/1.03 ============================== PROCESS INITIAL CLAUSES =============== % 0.77/1.03 % 0.77/1.03 ============================== PREDICATE ELIMINATION ================= % 0.77/1.03 % 0.77/1.03 ============================== end predicate elimination ============= % 0.77/1.03 % 0.77/1.03 Auto_denials: (non-Horn, no changes). % 0.77/1.03 % 0.77/1.03 Term ordering decisions: % 0.77/1.03 Function symbol KB weights: zero=1. nil=1. i=1. o=1. cons=1. addNat=1. append=1. x=1. suc=1. shw=1. half=1. rd=1. double=1. head=1. proj1Suc=1. tail=1. % 0.77/1.03 % 0.77/1.03 ============================== end of process initial clauses ======== % 0.77/1.03 % 0.77/1.03 ============================== CLAUSES FOR SEARCH ==================== % 0.77/1.03 % 0.77/1.03 ============================== end of clauses for search ============= % 0.77/1.03 % 0.77/1.03 ============================== SEARCH ================================ % 0.77/1.03 % 0.77/1.03 % Starting search at 0.01 seconds. % 0.77/1.03 % 0.77/1.03 ============================== PROOF ================================= % 0.77/1.03 % SZS status Theorem % 0.77/1.03 % SZS output start Refutation % 0.77/1.03 % 0.77/1.03 % Proof 1 at 0.04 (+ 0.00) seconds. % 0.77/1.03 % Length of proof is 67. % 0.77/1.03 % Level of proof is 14. % 0.77/1.03 % Maximum clause weight is 16.000. % 0.77/1.03 % Given clauses 105. % 0.77/1.03 % 0.77/1.03 4 (all X proj1Suc(suc(X)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 6 (all N half(suc(suc(N))) = suc(half(N))) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 7 (all N (evenNat(suc(N)) <-> -evenNat(N))) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 8 (all Y (evenNat(suc(Y)) -> shw(suc(Y)) = cons(o,shw(half(suc(Y)))))) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 9 (all Y (-evenNat(suc(Y)) -> shw(suc(Y)) = cons(i,shw(half(suc(Y)))))) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 10 (all Y append(nil,Y) = Y) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 11 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 12 (all Y addNat(zero,Y) = Y) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 13 (all Y all Z addNat(suc(Z),Y) = suc(addNat(Z,Y))) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 14 (all X double(X) = addNat(X,X)) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 15 (all Xs rd(cons(i,Xs)) = suc(double(rd(Xs)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 16 (all Xs rd(cons(o,Xs)) = double(rd(Xs))) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 17 (all X all Y x(X,Y) = rd(append(shw(X),shw(Y)))) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.77/1.03 18 -(exists X exists Y x(X,Y) != x(Y,X)) # label(goal_024) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.77/1.03 19 evenNat(zero) # label(axiom_010) # label(axiom). [assumption]. % 0.77/1.03 20 half(zero) = zero # label(axiom_007) # label(axiom). [assumption]. % 0.77/1.03 21 shw(zero) = nil # label(axiom_012) # label(axiom). [assumption]. % 0.77/1.03 22 rd(nil) = zero # label(axiom_020) # label(axiom). [assumption]. % 0.77/1.03 23 proj1Suc(suc(A)) = A # label(axiom_004) # label(axiom). [clausify(4)]. % 0.77/1.03 24 half(suc(zero)) = zero # label(axiom_008) # label(axiom). [assumption]. % 0.77/1.03 25 evenNat(suc(A)) | evenNat(A) # label(axiom_011) # label(axiom). [clausify(7)]. % 0.77/1.03 26 append(nil,A) = A # label(axiom_015) # label(axiom). [clausify(10)]. % 0.77/1.03 27 addNat(zero,A) = A # label(axiom_017) # label(axiom). [clausify(12)]. % 0.77/1.03 30 double(A) = addNat(A,A) # label(axiom_019) # label(axiom). [clausify(14)]. % 0.77/1.03 31 x(A,B) = x(B,A) # label(goal_024) # label(negated_conjecture). [clausify(18)]. % 0.77/1.03 32 half(suc(suc(A))) = suc(half(A)) # label(axiom_009) # label(axiom). [clausify(6)]. % 0.77/1.03 33 rd(cons(o,A)) = double(rd(A)) # label(axiom_022) # label(axiom). [clausify(16)]. % 0.77/1.03 34 addNat(rd(A),rd(A)) = rd(cons(o,A)). [copy(33),rewrite([30(5)]),flip(a)]. % 0.77/1.03 35 addNat(suc(A),B) = suc(addNat(A,B)) # label(axiom_018) # label(axiom). [clausify(13)]. % 0.77/1.03 36 suc(addNat(A,B)) = addNat(suc(A),B). [copy(35),flip(a)]. % 0.77/1.03 37 rd(cons(i,A)) = suc(double(rd(A))) # label(axiom_021) # label(axiom). [clausify(15)]. % 0.77/1.03 38 suc(rd(cons(o,A))) = rd(cons(i,A)). [copy(37),rewrite([30(5),34(6)]),flip(a)]. % 0.77/1.03 39 x(A,B) = rd(append(shw(A),shw(B))) # label(axiom_023) # label(axiom). [clausify(17)]. % 0.77/1.03 40 append(cons(A,B),C) = cons(A,append(B,C)) # label(axiom_016) # label(axiom). [clausify(11)]. % 0.77/1.03 41 evenNat(suc(A)) | shw(suc(A)) = cons(i,shw(half(suc(A)))) # label(axiom_014) # label(axiom). [clausify(9)]. % 0.77/1.03 42 evenNat(suc(A)) | cons(i,shw(half(suc(A)))) = shw(suc(A)). [copy(41),flip(b)]. % 0.77/1.03 47 -evenNat(suc(A)) | -evenNat(A) # label(axiom_011) # label(axiom). [clausify(7)]. % 0.77/1.03 48 -evenNat(suc(A)) | shw(suc(A)) = cons(o,shw(half(suc(A)))) # label(axiom_013) # label(axiom). [clausify(8)]. % 0.77/1.03 49 -evenNat(suc(A)) | cons(o,shw(half(suc(A)))) = shw(suc(A)). [copy(48),flip(b)]. % 0.77/1.03 50 rd(append(shw(A),shw(B))) = rd(append(shw(B),shw(A))). [back_rewrite(31),rewrite([39(1),39(5)])]. % 0.77/1.03 51 rd(cons(o,nil)) = zero. [para(22(a,1),34(a,1,1)),rewrite([22(3),27(3)]),flip(a)]. % 0.77/1.03 54 addNat(suc(zero),A) = suc(A). [para(27(a,1),36(a,1,1)),flip(a)]. % 0.77/1.03 55 half(addNat(suc(suc(A)),B)) = suc(half(addNat(A,B))). [para(36(a,1),32(a,1,1,1)),rewrite([36(3)])]. % 0.77/1.03 56 addNat(suc(rd(A)),rd(A)) = rd(cons(i,A)). [para(34(a,1),36(a,1,1)),rewrite([38(4)]),flip(a)]. % 0.77/1.03 65 -evenNat(suc(zero)). [ur(47,b,19,a)]. % 0.77/1.03 69 cons(o,shw(half(suc(A)))) = shw(suc(A)) | evenNat(A). [resolve(49,a,25,a)]. % 0.77/1.03 76 rd(cons(i,nil)) = suc(zero). [para(51(a,1),38(a,1,1)),flip(a)]. % 0.77/1.03 77 shw(suc(zero)) = cons(i,nil). [resolve(65,a,42,a),rewrite([24(4),21(3)]),flip(a)]. % 0.77/1.03 82 addNat(suc(suc(zero)),A) = suc(suc(A)). [para(54(a,1),36(a,1,1)),flip(a)]. % 0.77/1.03 83 rd(cons(o,cons(i,nil))) = suc(suc(zero)). [para(76(a,1),34(a,1,1)),rewrite([76(6),54(5)]),flip(a)]. % 0.77/1.03 84 rd(append(shw(A),cons(i,nil))) = rd(cons(i,shw(A))). [para(77(a,1),50(a,1,1,1)),rewrite([40(5),26(4),77(8)]),flip(a)]. % 0.77/1.03 95 addNat(suc(suc(suc(zero))),A) = suc(suc(suc(A))). [para(82(a,1),36(a,1,1)),flip(a)]. % 0.77/1.03 104 rd(cons(i,cons(i,nil))) = suc(suc(suc(zero))). [para(83(a,1),38(a,1,1)),flip(a)]. % 0.77/1.03 113 rd(cons(i,cons(o,cons(i,nil)))) = suc(suc(suc(suc(suc(zero))))). [para(83(a,1),56(a,1,1,1)),rewrite([83(10),95(8)]),flip(a)]. % 0.77/1.03 120 addNat(suc(suc(suc(suc(zero)))),A) = suc(suc(suc(suc(A)))). [para(95(a,1),36(a,1,1)),flip(a)]. % 0.77/1.03 121 rd(cons(o,cons(i,cons(i,nil)))) = suc(suc(suc(suc(suc(suc(zero)))))). [para(104(a,1),34(a,1,1)),rewrite([104(10),95(9)]),flip(a)]. % 0.77/1.03 135 cons(o,cons(i,nil)) = shw(suc(suc(zero))). [resolve(69,b,65,a),rewrite([32(5),20(3),77(4)])]. % 0.77/1.03 138 rd(cons(i,shw(suc(suc(zero))))) = suc(suc(suc(suc(suc(zero))))). [back_rewrite(113),rewrite([135(6)])]. % 0.77/1.03 143 append(shw(suc(suc(zero))),A) = cons(o,cons(i,A)). [para(135(a,1),40(a,1,1)),rewrite([40(10),26(9)])]. % 0.77/1.03 166 suc(suc(suc(suc(suc(suc(zero)))))) = suc(suc(suc(suc(suc(zero))))). [para(143(a,1),84(a,1,1)),rewrite([121(8),138(14)])]. % 0.77/1.03 216 addNat(suc(suc(suc(suc(suc(zero))))),A) = suc(suc(suc(suc(suc(A))))). [para(120(a,1),36(a,1,1)),flip(a)]. % 0.77/1.03 217 suc(suc(half(suc(A)))) = suc(suc(suc(half(A)))). [para(120(a,1),55(a,2,1,1)),rewrite([166(7),216(7),32(6),32(4),32(9),32(7)])]. % 0.77/1.03 220 suc(suc(suc(zero))) = suc(suc(zero)). [para(20(a,1),217(a,2,1,1,1)),rewrite([24(3)]),flip(a)]. % 0.77/1.03 249 suc(suc(suc(A))) = suc(suc(A)). [back_rewrite(95),rewrite([220(4),82(4)]),flip(a)]. % 0.77/1.03 258 suc(suc(A)) = suc(A). [para(249(a,1),23(a,1,1)),rewrite([23(3)]),flip(a)]. % 0.77/1.03 259 evenNat(suc(A)). [para(249(a,1),25(a,1)),rewrite([258(2),258(4)]),merge(b)]. % 0.77/1.03 260 $F. [resolve(259,a,65,a)]. % 0.77/1.03 % 0.77/1.03 % SZS output end Refutation % 0.77/1.03 ============================== end of proof ========================== % 0.77/1.03 % 0.77/1.03 ============================== STATISTICS ============================ % 0.77/1.03 % 0.77/1.03 Given=105. Generated=751. Kept=235. proofs=1. % 0.77/1.03 Usable=99. Sos=94. Demods=86. Limbo=1, Disabled=65. Hints=0. % 0.77/1.03 Megabytes=0.35. % 0.77/1.03 User_CPU=0.04, System_CPU=0.00, Wall_clock=0. % 0.77/1.03 % 0.77/1.03 ============================== end of statistics ===================== % 0.77/1.03 % 0.77/1.03 ============================== end of search ========================= % 0.77/1.03 % 0.77/1.03 THEOREM PROVED % 0.77/1.03 % SZS status Theorem % 0.77/1.03 % 0.77/1.03 Exiting with 1 proof. % 0.77/1.03 % 0.77/1.03 Process 31758 exit (max_proofs) Wed Apr 29 01:46:24 2026 % 0.77/1.03 Prover9 interrupted %------------------------------------------------------------------------------