%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX199+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:16:18 AM UTC 2026
% Result : Theorem 0.13s 0.47s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 11
% Syntax : Number of formulae : 64 ( 47 unt; 0 def)
% Number of atoms : 87 ( 73 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 46 ( 23 ~; 16 |; 0 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 148 ( 7 sgn 20 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X,X2] : head(cons(X,X2)) = X,
file('theBenchmark.p',axiom_001) ).
fof(axiom_002,axiom,
! [X,X2] : tail(cons(X,X2)) = X2,
file('theBenchmark.p',axiom_002) ).
fof(axiom_005,axiom,
! [X] : z != s(X),
file('theBenchmark.p',axiom_005) ).
fof(axiom_006,axiom,
! [Y] : leqNat(z,Y),
file('theBenchmark.p',axiom_006) ).
fof(axiom_007,axiom,
! [Z] : ~ leqNat(s(Z),z),
file('theBenchmark.p',axiom_007) ).
fof(axiom_008,axiom,
! [Z,M] :
( leqNat(s(Z),s(M))
<=> leqNat(Z,M) ),
file('theBenchmark.p',axiom_008) ).
fof(axiom_009,axiom,
! [Y] : merge(nil,Y) = Y,
file('theBenchmark.p',axiom_009) ).
fof(axiom_010,axiom,
! [Z,Xs] : merge(cons(Z,Xs),nil) = cons(Z,Xs),
file('theBenchmark.p',axiom_010) ).
fof(axiom_011,axiom,
! [Z,Xs,Y2,Ys] :
( leqNat(Z,Y2)
=> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Z,merge(Xs,cons(Y2,Ys))) ),
file('theBenchmark.p',axiom_011) ).
fof(axiom_012,axiom,
! [Z,Xs,Y2,Ys] :
( ~ leqNat(Z,Y2)
=> merge(cons(Z,Xs),cons(Y2,Ys)) = cons(Y2,merge(cons(Z,Xs),Ys)) ),
file('theBenchmark.p',axiom_012) ).
fof(goal_013,conjecture,
? [Xs,Ys,Zs] :
~ ( merge(Xs,Ys) = merge(Ys,Xs)
=> ( merge(Xs,Zs) = merge(Zs,Xs)
=> merge(Ys,Zs) = merge(Zs,Ys) ) ),
file('theBenchmark.p',goal_013) ).
fof(goal_013_neg,negated_conjecture,
~ ? [Xs,Ys,Zs] :
~ ( merge(Xs,Ys) = merge(Ys,Xs)
=> ( merge(Xs,Zs) = merge(Zs,Xs)
=> merge(Ys,Zs) = merge(Zs,Ys) ) ),
inference(assume_negation,[status(cth)],[goal_013]) ).
cnf(c_14,plain,
head(cons(A,B)) = A,
inference(clausify,[status(thm)],[axiom_001]) ).
cnf(c_15,plain,
tail(cons(A,B)) = B,
inference(clausify,[status(thm)],[axiom_002]) ).
cnf(c_18,plain,
s(A) != z,
inference(clausify,[status(thm)],[axiom_005]) ).
cnf(c_19,plain,
leqNat(z,A),
inference(clausify,[status(thm)],[axiom_006]) ).
cnf(c_20,plain,
~ leqNat(s(A),z),
inference(clausify,[status(thm)],[axiom_007]) ).
cnf(c_22,plain,
( ~ leqNat(A,B)
| leqNat(s(A),s(B)) ),
inference(clausify,[status(thm)],[axiom_008]) ).
cnf(c_23,plain,
merge(nil,A) = A,
inference(clausify,[status(thm)],[axiom_009]) ).
cnf(c_24,plain,
merge(cons(A,B),nil) = cons(A,B),
inference(clausify,[status(thm)],[axiom_010]) ).
cnf(c_25,plain,
( merge(cons(A,C),cons(B,D)) = cons(A,merge(C,cons(B,D)))
| ~ leqNat(A,B) ),
inference(clausify,[status(thm)],[axiom_011]) ).
cnf(c_26,plain,
( merge(cons(A,C),cons(B,D)) = cons(B,merge(cons(A,C),D))
| leqNat(A,B) ),
inference(clausify,[status(thm)],[axiom_012]) ).
cnf(c_27,negated_conjecture,
( merge(C,A) = merge(A,C)
| merge(C,B) != merge(B,C)
| merge(A,B) != merge(B,A) ),
inference(clausify,[status(thm)],[goal_013_neg]) ).
cnf(c_29,plain,
leqNat(s(z),s(A)),
inference(resolve,[status(thm)],[c_22,c_19]) ).
cnf(c_30,plain,
merge(cons(z,A),cons(B,C)) = cons(z,merge(A,cons(B,C))),
inference(resolve,[status(thm)],[c_25,c_19]) ).
cnf(c_34,plain,
merge(cons(s(A),B),cons(z,C)) = cons(z,merge(cons(s(A),B),C)),
inference(resolve,[status(thm)],[c_26,c_20]) ).
cnf(c_294,plain,
( merge(B,A) = merge(A,B)
| merge(B,nil) != merge(nil,B)
| merge(A,nil) != A ),
inference(paramod,[status(thm)],[c_23,c_27]) ).
cnf(c_37,plain,
( merge(B,A) = merge(A,B)
| merge(B,nil) != B
| merge(A,nil) != A ),
inference(paramod,[status(thm)],[c_23,c_294]) ).
cnf(c_46,plain,
merge(cons(s(z),A),cons(s(B),C)) = cons(s(z),merge(A,cons(s(B),C))),
inference(resolve,[status(thm)],[c_29,c_25]) ).
cnf(c_295,plain,
( merge(A,cons(B,C)) = merge(cons(B,C),A)
| merge(A,nil) != A ),
inference(resolve,[status(thm)],[c_37,c_24]) ).
cnf(c_48,plain,
merge(cons(A,B),cons(C,D)) = merge(cons(C,D),cons(A,B)),
inference(resolve,[status(thm)],[c_295,c_24]) ).
cnf(c_296,negated_conjecture,
( merge(cons(D,E),A) = merge(A,cons(D,E))
| merge(A,cons(B,C)) != merge(cons(B,C),A) ),
inference(resolve,[status(thm)],[c_48,c_27]) ).
cnf(c_49,negated_conjecture,
( merge(cons(D,E),C) = merge(C,cons(D,E))
| merge(cons(A,B),C) != merge(C,cons(A,B)) ),
inference(copy,[status(thm)],[c_296]) ).
cnf(c_297,plain,
cons(z,merge(A,cons(B,C))) = merge(cons(B,C),cons(z,A)),
inference(paramod,[status(thm)],[c_30,c_48]) ).
cnf(c_50,plain,
merge(cons(A,B),cons(z,C)) = cons(z,merge(C,cons(A,B))),
inference(copy,[status(thm)],[c_297]) ).
cnf(c_298,plain,
cons(z,merge(C,cons(s(A),B))) = cons(z,merge(cons(s(A),B),C)),
inference(paramod,[status(thm)],[c_50,c_34]) ).
cnf(c_52,plain,
cons(z,merge(cons(s(A),B),C)) = cons(z,merge(C,cons(s(A),B))),
inference(copy,[status(thm)],[c_298]) ).
cnf(c_55,plain,
cons(z,merge(A,cons(z,B))) = cons(z,merge(B,cons(z,A))),
inference(paramod,[status(thm)],[c_50,c_30]) ).
cnf(c_299,plain,
tail(cons(z,merge(A,cons(z,B)))) = merge(B,cons(z,A)),
inference(paramod,[status(thm)],[c_55,c_15]) ).
cnf(c_57,plain,
merge(A,cons(z,B)) = merge(B,cons(z,A)),
inference(paramod,[status(thm)],[c_15,c_299]) ).
cnf(c_300,plain,
merge(A,cons(z,cons(B,C))) = merge(cons(z,A),cons(B,C)),
inference(paramod,[status(thm)],[c_57,c_48]) ).
cnf(c_70,plain,
merge(A,cons(z,cons(B,C))) = cons(z,merge(A,cons(B,C))),
inference(paramod,[status(thm)],[c_30,c_300]) ).
cnf(c_301,plain,
tail(cons(z,merge(A,cons(s(B),C)))) = merge(cons(s(B),C),A),
inference(paramod,[status(thm)],[c_52,c_15]) ).
cnf(c_302,plain,
merge(A,cons(s(B),C)) = merge(cons(s(B),C),A),
inference(paramod,[status(thm)],[c_15,c_301]) ).
cnf(c_166,plain,
merge(cons(s(A),B),C) = merge(C,cons(s(A),B)),
inference(copy,[status(thm)],[c_302]) ).
cnf(c_205,plain,
merge(cons(A,B),C) = merge(C,cons(A,B)),
inference(resolve,[status(thm)],[c_166,c_49]) ).
cnf(c_303,negated_conjecture,
( merge(C,A) = merge(A,C)
| merge(B,C) != merge(C,B)
| merge(A,B) != merge(B,A) ),
inference(copy,[status(thm)],[c_27]) ).
cnf(c_304,negated_conjecture,
( merge(D,A) = merge(A,D)
| merge(A,cons(s(B),C)) != merge(cons(s(B),C),A) ),
inference(resolve,[status(thm)],[c_166,c_303]) ).
cnf(c_305,negated_conjecture,
( merge(D,A) = merge(A,D)
| merge(cons(s(B),C),A) != merge(A,cons(s(B),C)) ),
inference(copy,[status(thm)],[c_304]) ).
cnf(c_207,negated_conjecture,
merge(A,B) = merge(B,A),
inference(resolve,[status(thm)],[c_205,c_305]) ).
cnf(c_213,plain,
merge(cons(z,A),B) = merge(A,cons(z,B)),
inference(paramod,[status(thm)],[c_207,c_57]) ).
cnf(c_306,plain,
cons(s(z),merge(A,cons(s(B),C))) = merge(cons(s(B),C),cons(s(z),A)),
inference(paramod,[status(thm)],[c_46,c_207]) ).
cnf(c_231,plain,
merge(cons(s(A),B),cons(s(z),C)) = cons(s(z),merge(C,cons(s(A),B))),
inference(copy,[status(thm)],[c_306]) ).
cnf(c_237,plain,
cons(s(z),merge(A,cons(s(z),B))) = cons(s(z),merge(B,cons(s(z),A))),
inference(paramod,[status(thm)],[c_231,c_46]) ).
cnf(c_307,plain,
tail(cons(s(z),merge(A,cons(s(z),B)))) = merge(B,cons(s(z),A)),
inference(paramod,[status(thm)],[c_237,c_15]) ).
cnf(c_239,plain,
merge(A,cons(s(z),B)) = merge(B,cons(s(z),A)),
inference(paramod,[status(thm)],[c_15,c_307]) ).
cnf(c_257,plain,
merge(A,cons(s(z),nil)) = cons(s(z),A),
inference(paramod,[status(thm)],[c_239,c_23]) ).
cnf(c_308,plain,
cons(s(z),cons(z,A)) = merge(A,cons(z,cons(s(z),nil))),
inference(paramod,[status(thm)],[c_257,c_213]) ).
cnf(c_309,plain,
cons(s(z),cons(z,A)) = cons(z,merge(A,cons(s(z),nil))),
inference(paramod,[status(thm)],[c_70,c_308]) ).
cnf(c_274,plain,
cons(s(z),cons(z,A)) = cons(z,cons(s(z),A)),
inference(paramod,[status(thm)],[c_257,c_309]) ).
cnf(c_310,plain,
head(cons(z,cons(s(z),A))) = s(z),
inference(paramod,[status(thm)],[c_274,c_14]) ).
cnf(c_311,plain,
z = s(z),
inference(paramod,[status(thm)],[c_14,c_310]) ).
cnf(c_312,plain,
s(z) = z,
inference(copy,[status(thm)],[c_311]) ).
cnf(c_293,plain,
$false,
inference(resolve,[status(thm)],[c_18,c_312]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX199+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 16:54:45 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 3752949 was started by sandbox2 on n010,
% 0.08/0.36 % Sat Sep 26 16:54:45 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.36
% 0.13/0.36 % From the command line: assign(max_seconds, 300).
% 0.13/0.47
% 0.13/0.47 % SZS status Theorem for theBenchmark
% 0.13/0.47
% 0.13/0.47 % Proof 1 at 0.08 (+ 0.02) seconds.
% 0.13/0.47 % Length of proof is 44.
% 0.13/0.47 % Level of proof is 14.
% 0.13/0.47 % Maximum clause weight is 44.000.
% 0.13/0.47 % Given clauses 64.
% 0.13/0.47
% 0.13/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------