%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n017.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:02 PM UTC 2026 % Result : Theorem 0.76s 1.05s % Output : Refutation 0.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX190+1 : TPTP v9.3.0. Released v9.3.0. % 0.13/0.13 % Command : tptp2X_and_run_prover9 %d %s % 0.17/0.34 % Computer : n017.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Apr 28 23:46:57 EDT 2026 % 0.17/0.34 % CPUTime : % 0.76/1.03 ============================== Prover9 =============================== % 0.76/1.03 Prover9 (32) version 2009-11A, November 2009. % 0.76/1.03 Process 26675 was started by sandbox2 on n017.cluster.edu, % 0.76/1.03 Tue Apr 28 23:46:58 2026 % 0.76/1.03 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_26522_n017.cluster.edu". % 0.76/1.03 ============================== end of head =========================== % 0.76/1.03 % 0.76/1.03 ============================== INPUT ================================= % 0.76/1.03 % 0.76/1.03 % Reading from file /tmp/Prover9_26522_n017.cluster.edu % 0.76/1.03 % 0.76/1.03 set(prolog_style_variables). % 0.76/1.03 set(auto2). % 0.76/1.03 % set(auto2) -> set(auto). % 0.76/1.03 % set(auto) -> set(auto_inference). % 0.76/1.03 % set(auto) -> set(auto_setup). % 0.76/1.03 % set(auto_setup) -> set(predicate_elim). % 0.76/1.03 % set(auto_setup) -> assign(eq_defs, unfold). % 0.76/1.03 % set(auto) -> set(auto_limits). % 0.76/1.03 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.76/1.03 % set(auto_limits) -> assign(sos_limit, 20000). % 0.76/1.03 % set(auto) -> set(auto_denials). % 0.76/1.03 % set(auto) -> set(auto_process). % 0.76/1.03 % set(auto2) -> assign(new_constants, 1). % 0.76/1.03 % set(auto2) -> assign(fold_denial_max, 3). % 0.76/1.03 % set(auto2) -> assign(max_weight, "200.000"). % 0.76/1.03 % set(auto2) -> assign(max_hours, 1). % 0.76/1.03 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.76/1.03 % set(auto2) -> assign(max_seconds, 0). % 0.76/1.03 % set(auto2) -> assign(max_minutes, 5). % 0.76/1.03 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.76/1.03 % set(auto2) -> set(sort_initial_sos). % 0.76/1.03 % set(auto2) -> assign(sos_limit, -1). % 0.76/1.03 % set(auto2) -> assign(lrs_ticks, 3000). % 0.76/1.03 % set(auto2) -> assign(max_megs, 400). % 0.76/1.03 % set(auto2) -> assign(stats, some). % 0.76/1.03 % set(auto2) -> clear(echo_input). % 0.76/1.03 % set(auto2) -> set(quiet). % 0.76/1.03 % set(auto2) -> clear(print_initial_clauses). % 0.76/1.03 % set(auto2) -> clear(print_given). % 0.76/1.03 assign(lrs_ticks,-1). % 0.76/1.03 assign(sos_limit,10000). % 0.76/1.03 assign(order,kbo). % 0.76/1.03 set(lex_order_vars). % 0.76/1.03 clear(print_given). % 0.76/1.03 % 0.76/1.03 % formulas(sos). % not echoed (54 formulas) % 0.76/1.03 % 0.76/1.03 ============================== end of input ========================== % 0.76/1.03 % 0.76/1.03 % From the command line: assign(max_seconds, 300). % 0.76/1.03 % 0.76/1.03 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.76/1.03 % 0.76/1.03 % Formulas that are not ordinary clauses: % 0.76/1.03 1 (all X proj1S(s(X)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 2 (all X s(X) != z) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 3 (all X proj1N(n(X)) = X) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 4 (all X all X2 proj1(x(X,X2)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 5 (all X all X2 proj2(x(X,X2)) = X2) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 6 (all X all X2 proj12(y(X,X2)) = X) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 7 (all X all X2 proj22(y(X,X2)) = X2) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 8 (all X all X2 all X3 n(X) != x(X2,X3)) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 9 (all X all X2 all X3 n(X) != y(X2,X3)) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 10 (all X n(X) != x2) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 11 (all X all X2 all X3 all X4 x(X,X2) != y(X3,X4)) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 12 (all X all X2 x(X,X2) != x2) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 13 (all X all X2 y(X,X2) != x2) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 14 (all Y all E (Y = E -> fail2(Y,E) = y(n(s(s(z))),opt(Y)))) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 15 (all Y all E (Y != E -> (Y != x(proj1(Y),proj2(Y)) -> fail2(Y,E) = x(opt(Y),opt(E))))) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 16 (all E all A all B (x(A,B) != E -> fail2(x(A,B),E) = opt(x(A,x(B,E))))) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 17 (all Y all E (Y != n(proj1N(Y)) -> fail1(Y,E) = fail2(Y,E))) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 18 (all E all C (E != n(proj1N(E)) -> fail1(n(C),E) = fail2(n(C),E))) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 19 (all C all B2 fail1(n(C),n(B2)) = n(addNat(C,B2))) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 20 (all Y all E (E != n(proj1N(E)) -> fail(Y,E) = fail1(Y,E))) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 21 (all Y all X2 fail(Y,n(s(X2))) = fail1(Y,n(s(X2)))) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 22 (all Y fail(Y,n(z)) = Y) # label(axiom_022) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 23 (all X5 all E2 fail4(X5,E2) = y(opt(X5),opt(E2))) # label(axiom_023) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 24 (all X5 all E2 (X5 != n(proj1N(X5)) -> (X5 != y(proj12(X5),proj22(X5)) -> fail32(X5,E2) = fail4(X5,E2)))) # label(axiom_024) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 25 (all E2 all A2 (E2 != n(proj1N(E2)) -> fail32(n(A2),E2) = fail4(n(A2),E2))) # label(axiom_025) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 26 (all A2 all B3 fail32(n(A2),n(B3)) = n(mulNat(A2,B3))) # label(axiom_026) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 27 (all E2 all A3 all B4 fail32(y(A3,B4),E2) = opt(y(A3,y(B4,E2)))) # label(axiom_027) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 28 (all X5 all E2 (E2 != n(proj1N(E2)) -> fail22(X5,E2) = fail32(X5,E2))) # label(axiom_028) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 29 (all X5 all X8 fail22(X5,n(s(s(X8)))) = fail32(X5,n(s(s(X8))))) # label(axiom_029) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 30 (all X5 fail22(X5,n(s(z))) = X5) # label(axiom_030) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 31 (all X5 fail22(X5,n(z)) = fail32(X5,n(z))) # label(axiom_031) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 32 (all X5 all E2 (X5 != n(proj1N(X5)) -> fail12(X5,E2) = fail22(X5,E2))) # label(axiom_032) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 33 (all E2 all X11 fail12(n(s(s(X11))),E2) = fail22(n(s(s(X11))),E2)) # label(axiom_033) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 34 (all E2 fail12(n(s(z)),E2) = E2) # label(axiom_034) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 35 (all E2 fail12(n(z),E2) = fail22(n(z),E2)) # label(axiom_035) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 36 (all X5 all E2 (E2 != n(proj1N(E2)) -> fail3(X5,E2) = fail12(X5,E2))) # label(axiom_036) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 37 (all X5 all X13 fail3(X5,n(s(X13))) = fail12(X5,n(s(X13)))) # label(axiom_037) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 38 (all X5 fail3(X5,n(z)) = n(z)) # label(axiom_038) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 39 (all Y d(n(Y)) = n(z)) # label(axiom_039) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 40 (all F all G d(x(F,G)) = x(d(F),d(G))) # label(axiom_040) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 41 (all H all G2 d(y(H,G2)) = x(y(d(H),G2),y(H,d(G2)))) # label(axiom_041) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 42 (all Y all Z addNat(s(Z),Y) = s(addNat(Z,Y))) # label(axiom_043) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 43 (all Y addNat(z,Y) = Y) # label(axiom_044) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 44 (all Y all Z mulNat(s(Z),Y) = addNat(Y,mulNat(Z,Y))) # label(axiom_045) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 45 (all Y mulNat(z,Y) = z) # label(axiom_046) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 46 (all X (X != x(proj1(X),proj2(X)) -> (X != y(proj12(X),proj22(X)) -> opt(X) = X))) # label(axiom_047) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 47 (all Y all E (Y != n(proj1N(Y)) -> opt(x(Y,E)) = fail(Y,E))) # label(axiom_048) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 48 (all E all X4 opt(x(n(s(X4)),E)) = fail(n(s(X4)),E)) # label(axiom_049) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 49 (all E opt(x(n(z),E)) = E) # label(axiom_050) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.03 50 (all X5 all E2 (X5 != n(proj1N(X5)) -> opt(y(X5,E2)) = fail3(X5,E2))) # label(axiom_051) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 51 (all E2 all X15 opt(y(n(s(X15)),E2)) = fail3(n(s(X15)),E2)) # label(axiom_052) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 52 (all E2 opt(y(n(z),E2)) = n(z)) # label(axiom_053) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 53 -(exists E opt(d(E)) != opt(d(opt(E)))) # label(goal_054) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.76/1.05 % 0.76/1.05 ============================== end of process non-clausal formulas === % 0.76/1.05 % 0.76/1.05 ============================== PROCESS INITIAL CLAUSES =============== % 0.76/1.05 % 0.76/1.05 ============================== PREDICATE ELIMINATION ================= % 0.76/1.05 % 0.76/1.05 ============================== end predicate elimination ============= % 0.76/1.05 % 0.76/1.05 Auto_denials: (non-Horn, no changes). % 0.76/1.05 % 0.76/1.05 Term ordering decisions: % 0.76/1.05 Function symbol KB weights: z=1. x2=1. x=1. y=1. fail22=1. fail32=1. fail12=1. addNat=1. fail=1. fail1=1. fail2=1. fail3=1. mulNat=1. fail4=1. n=1. s=1. opt=1. proj1N=1. d=1. proj1=1. proj12=1. proj2=1. proj22=1. proj1S=1. % 0.76/1.05 % 0.76/1.05 ============================== end of process initial clauses ======== % 0.76/1.05 % 0.76/1.05 ============================== CLAUSES FOR SEARCH ==================== % 0.76/1.05 % 0.76/1.05 ============================== end of clauses for search ============= % 0.76/1.05 % 0.76/1.05 ============================== SEARCH ================================ % 0.76/1.05 % 0.76/1.05 % Starting search at 0.01 seconds. % 0.76/1.05 % 0.76/1.05 ============================== PROOF ================================= % 0.76/1.05 % SZS status Theorem % 0.76/1.05 % SZS output start Refutation % 0.76/1.05 % 0.76/1.05 % Proof 1 at 0.03 (+ 0.00) seconds. % 0.76/1.05 % Length of proof is 28. % 0.76/1.05 % Level of proof is 6. % 0.76/1.05 % Maximum clause weight is 18.000. % 0.76/1.05 % Given clauses 52. % 0.76/1.05 % 0.76/1.05 8 (all X all X2 all X3 n(X) != x(X2,X3)) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 9 (all X all X2 all X3 n(X) != y(X2,X3)) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 39 (all Y d(n(Y)) = n(z)) # label(axiom_039) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 40 (all F all G d(x(F,G)) = x(d(F),d(G))) # label(axiom_040) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 41 (all H all G2 d(y(H,G2)) = x(y(d(H),G2),y(H,d(G2)))) # label(axiom_041) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 46 (all X (X != x(proj1(X),proj2(X)) -> (X != y(proj12(X),proj22(X)) -> opt(X) = X))) # label(axiom_047) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 49 (all E opt(x(n(z),E)) = E) # label(axiom_050) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 52 (all E2 opt(y(n(z),E2)) = n(z)) # label(axiom_053) # label(axiom) # label(non_clause). [assumption]. % 0.76/1.05 53 -(exists E opt(d(E)) != opt(d(opt(E)))) # label(goal_054) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.76/1.05 63 d(n(A)) = n(z) # label(axiom_039) # label(axiom). [clausify(39)]. % 0.76/1.05 71 opt(x(n(z),A)) = A # label(axiom_050) # label(axiom). [clausify(49)]. % 0.76/1.05 72 opt(y(n(z),A)) = n(z) # label(axiom_053) # label(axiom). [clausify(52)]. % 0.76/1.05 73 opt(d(opt(A))) = opt(d(A)) # label(goal_054) # label(negated_conjecture). [clausify(53)]. % 0.76/1.05 82 d(x(A,B)) = x(d(A),d(B)) # label(axiom_040) # label(axiom). [clausify(40)]. % 0.76/1.05 83 x(d(A),d(B)) = d(x(A,B)). [copy(82),flip(a)]. % 0.76/1.05 114 d(y(A,B)) = x(y(d(A),B),y(A,d(B))) # label(axiom_041) # label(axiom). [clausify(41)]. % 0.76/1.05 115 x(y(d(A),B),y(A,d(B))) = d(y(A,B)). [copy(114),flip(a)]. % 0.76/1.05 118 x(proj1(A),proj2(A)) = A | y(proj12(A),proj22(A)) = A | opt(A) = A # label(axiom_047) # label(axiom). [clausify(46)]. % 0.76/1.05 127 x(A,B) != n(C) # label(axiom_008) # label(axiom). [clausify(8)]. % 0.76/1.05 128 y(A,B) != n(C) # label(axiom_009) # label(axiom). [clausify(9)]. % 0.76/1.05 134 opt(d(x(n(z),A))) = opt(d(A)). [para(71(a,1),73(a,1,1,1)),flip(a)]. % 0.76/1.05 135 opt(d(y(n(z),A))) = opt(n(z)). [para(72(a,1),73(a,1,1,1)),rewrite([63(3)]),flip(a)]. % 0.76/1.05 146 d(x(n(A),B)) = x(n(z),d(B)). [para(63(a,1),83(a,1,1)),flip(a)]. % 0.76/1.05 148 opt(d(A)) = d(A). [back_rewrite(134),rewrite([146(4),71(5)]),flip(a)]. % 0.76/1.05 150 d(y(n(z),A)) = opt(n(z)). [back_rewrite(135),rewrite([148(5)])]. % 0.76/1.05 376 d(y(A,B)) != n(C). [para(115(a,1),127(a,1))]. % 0.76/1.05 403 opt(n(A)) = n(A). [resolve(128,a,118,b),unit_del(a,127)]. % 0.76/1.05 443 $F. [back_rewrite(150),rewrite([403(7)]),unit_del(a,376)]. % 0.76/1.05 % 0.76/1.05 % SZS output end Refutation % 0.76/1.05 ============================== end of proof ========================== % 0.76/1.05 % 0.76/1.05 ============================== STATISTICS ============================ % 0.76/1.05 % 0.76/1.05 Given=52. Generated=548. Kept=366. proofs=1. % 0.76/1.05 Usable=50. Sos=216. Demods=95. Limbo=40, Disabled=114. Hints=0. % 0.76/1.05 Megabytes=0.58. % 0.76/1.05 User_CPU=0.03, System_CPU=0.00, Wall_clock=0. % 0.76/1.05 % 0.76/1.05 ============================== end of statistics ===================== % 0.76/1.05 % 0.76/1.05 ============================== end of search ========================= % 0.76/1.05 % 0.76/1.05 THEOREM PROVED % 0.76/1.05 % SZS status Theorem % 0.76/1.05 % 0.76/1.05 Exiting with 1 proof. % 0.76/1.05 % 0.76/1.05 Process 26675 exit (max_proofs) Tue Apr 28 23:46:58 2026 % 0.76/1.05 Prover9 interrupted %------------------------------------------------------------------------------