%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX199+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n029.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:04 PM UTC 2026 % Result : Theorem 0.86s 1.17s % Output : Refutation 0.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX199+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.16/0.33 % Computer : n029.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Wed Apr 29 00:31:44 EDT 2026 % 0.16/0.33 % CPUTime : % 0.42/1.00 ============================== Prover9 =============================== % 0.42/1.00 Prover9 (32) version 2009-11A, November 2009. % 0.42/1.00 Process 11946 was started by sandbox on n029.cluster.edu, % 0.42/1.00 Wed Apr 29 00:31:44 2026 % 0.42/1.00 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_11793_n029.cluster.edu". % 0.42/1.00 ============================== end of head =========================== % 0.42/1.00 % 0.42/1.00 ============================== INPUT ================================= % 0.42/1.00 % 0.42/1.00 % Reading from file /tmp/Prover9_11793_n029.cluster.edu % 0.42/1.00 % 0.42/1.00 set(prolog_style_variables). % 0.42/1.00 set(auto2). % 0.42/1.00 % set(auto2) -> set(auto). % 0.42/1.00 % set(auto) -> set(auto_inference). % 0.42/1.00 % set(auto) -> set(auto_setup). % 0.42/1.00 % set(auto_setup) -> set(predicate_elim). % 0.42/1.00 % set(auto_setup) -> assign(eq_defs, unfold). % 0.42/1.00 % set(auto) -> set(auto_limits). % 0.42/1.00 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.42/1.00 % set(auto_limits) -> assign(sos_limit, 20000). % 0.42/1.00 % set(auto) -> set(auto_denials). % 0.42/1.00 % set(auto) -> set(auto_process). % 0.42/1.00 % set(auto2) -> assign(new_constants, 1). % 0.42/1.00 % set(auto2) -> assign(fold_denial_max, 3). % 0.42/1.00 % set(auto2) -> assign(max_weight, "200.000"). % 0.42/1.00 % set(auto2) -> assign(max_hours, 1). % 0.42/1.00 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.42/1.00 % set(auto2) -> assign(max_seconds, 0). % 0.42/1.00 % set(auto2) -> assign(max_minutes, 5). % 0.42/1.00 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.42/1.00 % set(auto2) -> set(sort_initial_sos). % 0.42/1.00 % set(auto2) -> assign(sos_limit, -1). % 0.42/1.00 % set(auto2) -> assign(lrs_ticks, 3000). % 0.42/1.00 % set(auto2) -> assign(max_megs, 400). % 0.42/1.00 % set(auto2) -> assign(stats, some). % 0.42/1.00 % set(auto2) -> clear(echo_input). % 0.42/1.00 % set(auto2) -> set(quiet). % 0.42/1.00 % set(auto2) -> clear(print_initial_clauses). % 0.42/1.00 % set(auto2) -> clear(print_given). % 0.42/1.00 assign(lrs_ticks,-1). % 0.42/1.00 assign(sos_limit,10000). % 0.42/1.00 assign(order,kbo). % 0.42/1.00 set(lex_order_vars). % 0.42/1.00 clear(print_given). % 0.42/1.00 % 0.42/1.00 % formulas(sos). % not echoed (13 formulas) % 0.42/1.00 % 0.42/1.00 ============================== end of input ========================== % 0.42/1.00 % 0.42/1.00 % From the command line: assign(max_seconds, 300). % 0.42/1.00 % 0.42/1.00 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.42/1.00 % 0.42/1.00 % Formulas that are not ordinary clauses: % 0.42/1.00 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 3 (all X all X2 nil != cons(X,X2)) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 4 (all X proj1S(s(X)) = X) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 5 (all X z != s(X)) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 6 (all Y leqNat(z,Y)) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 7 (all Z -leqNat(s(Z),z)) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 8 (all Z all M (leqNat(s(Z),s(M)) <-> leqNat(Z,M))) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 9 (all Y merge(nil,Y) = Y) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 10 (all Z all Xs merge(cons(Z,Xs),nil) = cons(Z,Xs)) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 11 (all Z all Xs all Y2 all Ys (leqNat(Z,Y2) -> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))))) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 12 (all Z all Xs all Y2 all Ys (-leqNat(Z,Y2) -> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Y2,merge(cons(Z,Xs),Ys)))) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.42/1.00 13 -(exists Xs exists Ys exists Zs -(merge(Xs,Ys) = merge(Ys,Xs) -> (merge(Xs,Zs) = merge(Zs,Xs) -> merge(Ys,Zs) = merge(Zs,Ys)))) # label(goal_013) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.42/1.00 % 0.42/1.00 ============================== end of process non-clausal formulas === % 0.42/1.00 % 0.42/1.00 ============================== PROCESS INITIAL CLAUSES =============== % 0.42/1.00 % 0.42/1.00 ============================== PREDICATE ELIMINATION ================= % 0.42/1.00 % 0.42/1.00 ============================== end predicate elimination ============= % 0.42/1.00 % 0.42/1.00 Auto_denials: (non-Horn, no changes). % 0.42/1.00 % 0.42/1.00 Term ordering decisions: % 0.86/1.17 Function symbol KB weights: nil=1. z=1. cons=1. merge=1. s=1. head=1. proj1S=1. tail=1. % 0.86/1.17 % 0.86/1.17 ============================== end of process initial clauses ======== % 0.86/1.17 % 0.86/1.17 ============================== CLAUSES FOR SEARCH ==================== % 0.86/1.17 % 0.86/1.17 ============================== end of clauses for search ============= % 0.86/1.17 % 0.86/1.17 ============================== SEARCH ================================ % 0.86/1.17 % 0.86/1.17 % Starting search at 0.01 seconds. % 0.86/1.17 % back CAC tautology: 180 cons(z,cons(z,merge(cons(s(A),B),cons(C,D)))) = cons(z,cons(z,merge(cons(C,D),cons(s(A),B)))). [para(95(a,1),87(a,1,2)),rewrite([34(15)])]. % 0.86/1.17 % back CAC tautology: 174 cons(z,merge(A,cons(B,C))) = cons(B,merge(C,cons(z,A))) | cons(z,merge(merge(D,cons(s(E),F)),cons(B,V6))) = cons(z,merge(cons(B,V6),merge(D,cons(s(E),F)))). [para(87(a,2),33(b,1,2)),rewrite([93(4),95(4),171(16)])]. % 0.86/1.17 % back CAC tautology: 89 cons(z,merge(cons(A,B),cons(C,D))) = cons(z,merge(cons(C,D),cons(A,B))). [para(85(a,1),34(a,2,2)),rewrite([34(5)])]. % 0.86/1.17 % 0.86/1.17 ============================== PROOF ================================= % 0.86/1.17 % SZS status Theorem % 0.86/1.17 % SZS output start Refutation % 0.86/1.17 % 0.86/1.17 % Proof 1 at 0.18 (+ 0.01) seconds. % 0.86/1.17 % Length of proof is 48. % 0.86/1.17 % Level of proof is 17. % 0.86/1.17 % Maximum clause weight is 30.000. % 0.86/1.17 % Given clauses 131. % 0.86/1.17 % 0.86/1.17 1 (all X all X2 head(cons(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 2 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 5 (all X z != s(X)) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 6 (all Y leqNat(z,Y)) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 7 (all Z -leqNat(s(Z),z)) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 9 (all Y merge(nil,Y) = Y) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 10 (all Z all Xs merge(cons(Z,Xs),nil) = cons(Z,Xs)) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 11 (all Z all Xs all Y2 all Ys (leqNat(Z,Y2) -> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))))) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 12 (all Z all Xs all Y2 all Ys (-leqNat(Z,Y2) -> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Y2,merge(cons(Z,Xs),Ys)))) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.86/1.17 13 -(exists Xs exists Ys exists Zs -(merge(Xs,Ys) = merge(Ys,Xs) -> (merge(Xs,Zs) = merge(Zs,Xs) -> merge(Ys,Zs) = merge(Zs,Ys)))) # label(goal_013) # label(negated_conjecture) # label(non_clause). [assumption]. % 0.86/1.17 14 leqNat(z,A) # label(axiom_006) # label(axiom). [clausify(6)]. % 0.86/1.17 16 merge(nil,A) = A # label(axiom_009) # label(axiom). [clausify(9)]. % 0.86/1.17 17 head(cons(A,B)) = A # label(axiom_001) # label(axiom). [clausify(1)]. % 0.86/1.17 18 tail(cons(A,B)) = B # label(axiom_002) # label(axiom). [clausify(2)]. % 0.86/1.17 19 merge(cons(A,B),nil) = cons(A,B) # label(axiom_010) # label(axiom). [clausify(10)]. % 0.86/1.17 20 leqNat(A,B) | merge(cons(A,C),cons(B,D)) = cons(B,merge(cons(A,C),D)) # label(axiom_012) # label(axiom). [clausify(12)]. % 0.86/1.17 21 s(A) != z # label(axiom_005) # label(axiom). [clausify(5)]. % 0.86/1.17 22 -leqNat(s(A),z) # label(axiom_007) # label(axiom). [clausify(7)]. % 0.86/1.17 26 -leqNat(A,B) | merge(cons(A,C),cons(B,D)) = cons(A,merge(C,cons(B,D))) # label(axiom_011) # label(axiom). [clausify(11)]. % 0.86/1.17 27 merge(A,B) != merge(B,A) | merge(C,B) != merge(B,C) | merge(C,A) = merge(A,C) # label(goal_013) # label(negated_conjecture). [clausify(13)]. % 0.86/1.17 28 merge(cons(s(A),B),cons(z,C)) = cons(z,merge(cons(s(A),B),C)). [resolve(22,a,20,a)]. % 0.86/1.17 33 merge(cons(A,B),cons(C,D)) = cons(A,merge(B,cons(C,D))) | merge(cons(A,E),cons(C,F)) = cons(C,merge(cons(A,E),F)). [resolve(26,a,20,a)]. % 0.86/1.17 34 merge(cons(z,A),cons(B,C)) = cons(z,merge(A,cons(B,C))). [resolve(26,a,14,a)]. % 0.86/1.17 38 merge(A,nil) != A | merge(cons(B,C),A) = merge(A,cons(B,C)). [para(19(a,1),27(a,1)),rewrite([16(4),16(7)]),flip(c),xx(a)]. % 0.86/1.17 85 merge(cons(A,B),cons(C,D)) = merge(cons(C,D),cons(A,B)). [resolve(38,a,19,a)]. % 0.86/1.17 87 cons(z,merge(cons(s(A),B),C)) = cons(z,merge(C,cons(s(A),B))). [para(85(a,1),28(a,1)),rewrite([34(5)]),flip(a)]. % 0.86/1.17 88 merge(cons(A,B),cons(z,C)) = cons(z,merge(C,cons(A,B))). [para(85(a,1),34(a,1))]. % 0.86/1.17 90 cons(z,merge(A,cons(z,B))) = cons(z,merge(B,cons(z,A))). [para(88(a,1),34(a,1))]. % 0.86/1.17 93 merge(A,cons(z,B)) = merge(B,cons(z,A)). [para(90(a,1),18(a,1,1)),rewrite([18(6)])]. % 0.86/1.17 95 merge(A,cons(z,cons(B,C))) = cons(z,merge(A,cons(B,C))). [back_rewrite(88),rewrite([93(4)])]. % 0.86/1.17 101 merge(cons(A,B),cons(C,D)) = cons(C,merge(cons(A,B),D)) | merge(cons(C,E),cons(A,F)) = cons(A,merge(F,cons(C,E))). [para(33(a,1),85(a,1)),flip(b)]. % 0.86/1.17 102 merge(cons(A,B),cons(C,D)) = cons(A,merge(B,cons(C,D))) | merge(cons(C,E),cons(A,F)) = cons(C,merge(cons(A,F),E)). [para(33(b,1),85(a,1)),flip(b)]. % 0.86/1.17 124 merge(A,cons(z,nil)) = cons(z,A). [para(93(a,1),16(a,1))]. % 0.86/1.17 168 merge(cons(s(A),B),C) = merge(C,cons(s(A),B)). [para(87(a,1),18(a,1,1)),rewrite([18(6)]),flip(a)]. % 0.86/1.17 189 merge(A,B) = merge(B,A). [resolve(168,a,27,b(flip)),flip(a),unit_del(a,168)]. % 0.86/1.17 223 merge(cons(A,B),cons(C,D)) = cons(A,merge(B,cons(C,D))) | merge(cons(C,E),cons(A,F)) = cons(C,merge(E,cons(A,F))). [back_rewrite(102),rewrite([189(12)])]. % 0.86/1.17 224 merge(cons(A,B),cons(C,D)) = cons(C,merge(D,cons(A,B))) | merge(cons(C,E),cons(A,F)) = cons(A,merge(F,cons(C,E))). [back_rewrite(101),rewrite([189(5)])]. % 0.86/1.17 252 merge(cons(A,B),cons(A,C)) = cons(A,merge(B,cons(A,C))). [factor(223,a,b)]. % 0.86/1.17 253 cons(A,merge(B,cons(A,C))) = cons(A,merge(C,cons(A,B))). [factor(224,a,b),rewrite([252(3)])]. % 0.86/1.17 260 merge(A,cons(B,C)) = merge(C,cons(B,A)). [para(253(a,1),18(a,1,1)),rewrite([18(4)])]. % 0.86/1.17 263 merge(cons(z,nil),merge(A,cons(z,B))) = cons(z,merge(A,cons(z,B))). [para(253(a,1),124(a,2)),rewrite([189(7),260(11)])]. % 0.86/1.17 268 merge(A,cons(B,cons(B,C))) = cons(B,merge(C,cons(B,A))). [para(253(a,1),252(a,2)),rewrite([260(3),260(5)])]. % 0.86/1.17 347 merge(cons(z,nil),cons(z,merge(A,cons(B,C)))) = cons(z,cons(z,merge(A,cons(B,C)))). [para(95(a,1),263(a,1,2)),rewrite([95(13)])]. % 0.86/1.17 383 cons(z,merge(cons(z,nil),cons(A,merge(B,cons(A,C))))) = cons(z,cons(z,cons(A,merge(B,cons(A,C))))). [para(268(a,1),347(a,1,2,2)),rewrite([95(9),268(14)])]. % 0.86/1.17 483 merge(cons(z,nil),cons(A,merge(B,cons(A,C)))) = cons(z,cons(A,merge(B,cons(A,C)))). [para(383(a,1),18(a,1,1)),rewrite([18(8)]),flip(a)]. % 0.86/1.17 497 cons(z,cons(A,cons(A,merge(B,cons(A,C))))) = cons(A,cons(z,cons(A,merge(B,cons(A,C))))). [para(268(a,1),483(a,1,2,2)),rewrite([268(8),260(7),483(7),268(10)]),flip(a)]. % 0.86/1.17 511 z = A. [para(497(a,1),17(a,1,1)),rewrite([17(7)]),flip(a)]. % 0.86/1.17 512 $F. [resolve(511,a,21,a(flip))]. % 0.86/1.17 % 0.86/1.17 % SZS output end Refutation % 0.86/1.17 ============================== end of proof ========================== % 0.86/1.17 % 0.86/1.17 ============================== STATISTICS ============================ % 0.86/1.17 % 0.86/1.17 Given=131. Generated=2115. Kept=498. proofs=1. % 0.86/1.17 Usable=102. Sos=175. Demods=97. Limbo=0, Disabled=234. Hints=0. % 0.86/1.17 Megabytes=0.93. % 0.86/1.17 User_CPU=0.18, System_CPU=0.01, Wall_clock=1. % 0.86/1.17 % 0.86/1.17 ============================== end of statistics ===================== % 0.86/1.17 % 0.86/1.17 ============================== end of search ========================= % 0.86/1.17 % 0.86/1.17 THEOREM PROVED % 0.86/1.17 % SZS status Theorem % 0.86/1.17 % 0.86/1.17 Exiting with 1 proof. % 0.86/1.17 % 0.86/1.17 Process 11946 exit (max_proofs) Wed Apr 29 00:31:45 2026 % 0.86/1.17 Prover9 interrupted %------------------------------------------------------------------------------