%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX201-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:19 AM UTC 2026
% Result : Unsatisfiable 4.31s 1.35s
% Output : CNFRefutation 4.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 29
% Syntax : Number of formulae : 172 ( 172 unt; 0 def)
% Number of atoms : 172 ( 171 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 52 ( 52 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 4 con; 0-5 aty)
% Number of variables : 407 ( 41 sgn 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : aux(VAR_0,VAR_1,VAR_2,pair2(VAR_3,VAR_4)) = pair2(cons(VAR_1,VAR_3),VAR_4),
file('theBenchmark.p',axiom) ).
cnf(c_1,plain,
aux(A,B,C,pair2(D,E)) = pair2(cons(B,D),E),
inference(clausify,[status(thm)],[axiom]) ).
fof(axiom_001,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : aux2(VAR_0,VAR_1,VAR_2,VAR_3,btrue) = cons(VAR_0,merge(VAR_1,cons(VAR_2,VAR_3))),
file('theBenchmark.p',axiom_001) ).
cnf(c_2,plain,
aux2(A,B,C,D,btrue) = cons(A,merge(B,cons(C,D))),
inference(clausify,[status(thm)],[axiom_001]) ).
fof(axiom_003,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : aux3(VAR_0,VAR_1,VAR_2,pair2(VAR_3,VAR_4)) = merge(msort(VAR_3),msort(VAR_4)),
file('theBenchmark.p',axiom_003) ).
cnf(c_4,plain,
aux3(A,B,C,pair2(D,E)) = merge(msort(D),msort(E)),
inference(clausify,[status(thm)],[axiom_003]) ).
fof(axiom_004,axiom,
! [VAR_0,VAR_1,VAR_2] : aux4(VAR_0,VAR_1,VAR_2,btrue) = s(count(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_004) ).
cnf(c_5,plain,
aux4(A,B,C,btrue) = s(count(A,C)),
inference(clausify,[status(thm)],[axiom_004]) ).
fof(axiom_005,axiom,
! [VAR_0,VAR_1,VAR_2] : aux4(VAR_0,VAR_1,VAR_2,bfalse) = count(VAR_0,VAR_2),
file('theBenchmark.p',axiom_005) ).
cnf(c_6,plain,
aux4(A,B,C,bfalse) = count(A,C),
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_006,axiom,
! [VAR_0] : splitAtNat(z,VAR_0) = pair2(nil,VAR_0),
file('theBenchmark.p',axiom_006) ).
cnf(c_7,plain,
splitAtNat(z,A) = pair2(nil,A),
inference(clausify,[status(thm)],[axiom_006]) ).
fof(axiom_008,axiom,
! [VAR_0,VAR_1,VAR_2] : splitAtNat(s(VAR_0),cons(VAR_1,VAR_2)) = aux(VAR_0,VAR_1,VAR_2,splitAtNat(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_008) ).
cnf(c_9,plain,
splitAtNat(s(A),cons(B,C)) = aux(A,B,C,splitAtNat(A,C)),
inference(clausify,[status(thm)],[axiom_008]) ).
cnf(c_10,plain,
aux(A,B,C,splitAtNat(A,C)) = splitAtNat(s(A),cons(B,C)),
inference(copy,[status(thm)],[c_9]) ).
fof(axiom_009,axiom,
! [VAR_0] : leqNat(z,VAR_0) = btrue,
file('theBenchmark.p',axiom_009) ).
cnf(c_11,plain,
leqNat(z,A) = btrue,
inference(clausify,[status(thm)],[axiom_009]) ).
fof(axiom_010,axiom,
! [VAR_0] : leqNat(s(VAR_0),z) = bfalse,
file('theBenchmark.p',axiom_010) ).
cnf(c_12,plain,
leqNat(s(A),z) = bfalse,
inference(clausify,[status(thm)],[axiom_010]) ).
fof(axiom_011,axiom,
! [VAR_0,VAR_1] : leqNat(s(VAR_0),s(VAR_1)) = leqNat(VAR_0,VAR_1),
file('theBenchmark.p',axiom_011) ).
cnf(c_13,plain,
leqNat(s(A),s(B)) = leqNat(A,B),
inference(clausify,[status(thm)],[axiom_011]) ).
fof(axiom_012,axiom,
! [VAR_0] : merge(nil,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_012) ).
cnf(c_14,plain,
merge(nil,A) = A,
inference(clausify,[status(thm)],[axiom_012]) ).
fof(axiom_014,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : merge(cons(VAR_0,VAR_1),cons(VAR_2,VAR_3)) = aux2(VAR_0,VAR_1,VAR_2,VAR_3,leqNat(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_014) ).
cnf(c_16,plain,
merge(cons(A,B),cons(C,D)) = aux2(A,B,C,D,leqNat(A,C)),
inference(clausify,[status(thm)],[axiom_014]) ).
cnf(c_17,plain,
aux2(A,B,C,D,leqNat(A,C)) = merge(cons(A,B),cons(C,D)),
inference(copy,[status(thm)],[c_16]) ).
fof(axiom_015,axiom,
lengthNat(nil) = z,
file('theBenchmark.p',axiom_015) ).
cnf(c_18,plain,
lengthNat(nil) = z,
inference(clausify,[status(thm)],[axiom_015]) ).
fof(axiom_016,axiom,
! [VAR_0,VAR_1] : lengthNat(cons(VAR_0,VAR_1)) = s(lengthNat(VAR_1)),
file('theBenchmark.p',axiom_016) ).
cnf(c_19,plain,
lengthNat(cons(A,B)) = s(lengthNat(B)),
inference(clausify,[status(thm)],[axiom_016]) ).
fof(axiom_017,axiom,
! [VAR_0] : impl(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_017) ).
cnf(c_20,plain,
impl(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_017]) ).
fof(axiom_019,axiom,
div2(z) = z,
file('theBenchmark.p',axiom_019) ).
cnf(c_22,plain,
div2(z) = z,
inference(clausify,[status(thm)],[axiom_019]) ).
fof(axiom_020,axiom,
div2(s(z)) = z,
file('theBenchmark.p',axiom_020) ).
cnf(c_23,plain,
div2(s(z)) = z,
inference(clausify,[status(thm)],[axiom_020]) ).
fof(axiom_021,axiom,
! [VAR_0] : div2(s(s(VAR_0))) = s(div2(VAR_0)),
file('theBenchmark.p',axiom_021) ).
cnf(c_24,plain,
div2(s(s(A))) = s(div2(A)),
inference(clausify,[status(thm)],[axiom_021]) ).
fof(axiom_023,axiom,
! [VAR_0] : msort(cons(VAR_0,nil)) = cons(VAR_0,nil),
file('theBenchmark.p',axiom_023) ).
cnf(c_26,plain,
msort(cons(A,nil)) = cons(A,nil),
inference(clausify,[status(thm)],[axiom_023]) ).
fof(axiom_024,axiom,
! [VAR_0,VAR_1,VAR_2] : msort(cons(VAR_0,cons(VAR_1,VAR_2))) = aux3(VAR_0,VAR_1,VAR_2,splitAtNat(div2(lengthNat(cons(VAR_0,cons(VAR_1,VAR_2)))),cons(VAR_0,cons(VAR_1,VAR_2)))),
file('theBenchmark.p',axiom_024) ).
cnf(c_27,plain,
msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(div2(lengthNat(cons(A,cons(B,C)))),cons(A,cons(B,C)))),
inference(clausify,[status(thm)],[axiom_024]) ).
cnf(c_1191,plain,
msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(div2(s(lengthNat(cons(B,C)))),cons(A,cons(B,C)))),
inference(paramod,[status(thm)],[c_19,c_27]) ).
cnf(c_1192,plain,
msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(div2(s(s(lengthNat(C)))),cons(A,cons(B,C)))),
inference(paramod,[status(thm)],[c_19,c_1191]) ).
cnf(c_1193,plain,
msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(s(div2(lengthNat(C))),cons(A,cons(B,C)))),
inference(paramod,[status(thm)],[c_24,c_1192]) ).
cnf(c_28,plain,
aux3(A,B,C,splitAtNat(s(div2(lengthNat(C))),cons(A,cons(B,C)))) = msort(cons(A,cons(B,C))),
inference(copy,[status(thm)],[c_1193]) ).
fof(axiom_025,axiom,
! [VAR_0] : count(VAR_0,nil) = z,
file('theBenchmark.p',axiom_025) ).
cnf(c_29,plain,
count(A,nil) = z,
inference(clausify,[status(thm)],[axiom_025]) ).
fof(axiom_026,axiom,
! [VAR_0,VAR_1,VAR_2] : count(VAR_0,cons(VAR_1,VAR_2)) = aux4(VAR_0,VAR_1,VAR_2,eq(VAR_1,VAR_0)),
file('theBenchmark.p',axiom_026) ).
cnf(c_30,plain,
count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)),
inference(clausify,[status(thm)],[axiom_026]) ).
cnf(c_31,plain,
aux4(A,B,C,eq(B,A)) = count(A,cons(B,C)),
inference(copy,[status(thm)],[c_30]) ).
fof(axiom_027,axiom,
! [VAR_0,VAR_1] : prop_msort_permutation_wrong1(VAR_0,VAR_1) = impl(eq2(leqNat(count(VAR_1,VAR_0),s(s(s(s(s(z)))))),bfalse),eq(count(VAR_1,VAR_0),count(s(VAR_1),msort(VAR_0)))),
file('theBenchmark.p',axiom_027) ).
cnf(c_32,plain,
prop_msort_permutation_wrong1(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(B,A),count(s(B),msort(A)))),
inference(clausify,[status(thm)],[axiom_027]) ).
fof(axiom_030,axiom,
! [VAR_0,VAR_1] : eq(s(VAR_0),s(VAR_1)) = eq(VAR_0,VAR_1),
file('theBenchmark.p',axiom_030) ).
cnf(c_35,plain,
eq(s(A),s(B)) = eq(A,B),
inference(clausify,[status(thm)],[axiom_030]) ).
fof(axiom_031,axiom,
! [VAR_0] : eq(z,s(VAR_0)) = bfalse,
file('theBenchmark.p',axiom_031) ).
cnf(c_36,plain,
eq(z,s(A)) = bfalse,
inference(clausify,[status(thm)],[axiom_031]) ).
fof(axiom_032,axiom,
! [VAR_0] : eq(s(VAR_0),z) = bfalse,
file('theBenchmark.p',axiom_032) ).
cnf(c_37,plain,
eq(s(A),z) = bfalse,
inference(clausify,[status(thm)],[axiom_032]) ).
fof(axiom_033,axiom,
! [VAR_0] : eq(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_033) ).
cnf(c_38,plain,
eq(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_033]) ).
fof(axiom_034,axiom,
! [VAR_0] : eq2(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_034) ).
cnf(c_39,plain,
eq2(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_034]) ).
fof(goal,axiom,
! [VAR_0,VAR_1] : eq2(prop_msort_permutation_wrong1(VAR_0,VAR_1),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_40,plain,
eq2(prop_msort_permutation_wrong1(A,B),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_41,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(s(s(s(z)))))),bfalse),eq(count(A,B),count(s(A),msort(B)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_32,c_40]) ).
cnf(c_1194,plain,
aux(z,A,B,pair2(nil,B)) = splitAtNat(s(z),cons(A,B)),
inference(paramod,[status(thm)],[c_7,c_10]) ).
cnf(c_1195,plain,
pair2(cons(A,nil),B) = splitAtNat(s(z),cons(A,B)),
inference(paramod,[status(thm)],[c_1,c_1194]) ).
cnf(c_42,plain,
splitAtNat(s(z),cons(A,B)) = pair2(cons(A,nil),B),
inference(copy,[status(thm)],[c_1195]) ).
cnf(c_1196,plain,
aux2(z,A,B,C,btrue) = merge(cons(z,A),cons(B,C)),
inference(paramod,[status(thm)],[c_11,c_17]) ).
cnf(c_1197,plain,
cons(z,merge(A,cons(B,C))) = merge(cons(z,A),cons(B,C)),
inference(paramod,[status(thm)],[c_2,c_1196]) ).
cnf(c_44,plain,
merge(cons(z,A),cons(B,C)) = cons(z,merge(A,cons(B,C))),
inference(copy,[status(thm)],[c_1197]) ).
cnf(c_1198,plain,
aux3(A,B,nil,splitAtNat(s(div2(z)),cons(A,cons(B,nil)))) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_18,c_28]) ).
cnf(c_1199,plain,
aux3(A,B,nil,splitAtNat(s(z),cons(A,cons(B,nil)))) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_22,c_1198]) ).
cnf(c_1200,plain,
aux3(A,B,nil,pair2(cons(A,nil),cons(B,nil))) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_42,c_1199]) ).
cnf(c_1201,plain,
merge(msort(cons(A,nil)),msort(cons(B,nil))) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_4,c_1200]) ).
cnf(c_1202,plain,
merge(cons(A,nil),msort(cons(B,nil))) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_26,c_1201]) ).
cnf(c_1203,plain,
merge(cons(A,nil),cons(B,nil)) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_26,c_1202]) ).
cnf(c_47,plain,
msort(cons(A,cons(B,nil))) = merge(cons(A,nil),cons(B,nil)),
inference(copy,[status(thm)],[c_1203]) ).
cnf(c_48,plain,
aux3(A,B,cons(C,D),splitAtNat(s(div2(s(lengthNat(D)))),cons(A,cons(B,cons(C,D))))) = msort(cons(A,cons(B,cons(C,D)))),
inference(paramod,[status(thm)],[c_19,c_28]) ).
cnf(c_1204,plain,
aux4(s(A),z,B,bfalse) = count(s(A),cons(z,B)),
inference(paramod,[status(thm)],[c_36,c_31]) ).
cnf(c_1205,plain,
count(s(A),B) = count(s(A),cons(z,B)),
inference(paramod,[status(thm)],[c_6,c_1204]) ).
cnf(c_50,plain,
count(s(A),cons(z,B)) = count(s(A),B),
inference(copy,[status(thm)],[c_1205]) ).
cnf(c_1206,plain,
aux4(z,s(A),B,bfalse) = count(z,cons(s(A),B)),
inference(paramod,[status(thm)],[c_37,c_31]) ).
cnf(c_1207,plain,
count(z,B) = count(z,cons(s(A),B)),
inference(paramod,[status(thm)],[c_6,c_1206]) ).
cnf(c_51,plain,
count(z,cons(s(A),B)) = count(z,B),
inference(copy,[status(thm)],[c_1207]) ).
cnf(c_1208,plain,
aux4(A,A,B,btrue) = count(A,cons(A,B)),
inference(paramod,[status(thm)],[c_38,c_31]) ).
cnf(c_1209,plain,
s(count(A,B)) = count(A,cons(A,B)),
inference(paramod,[status(thm)],[c_5,c_1208]) ).
cnf(c_52,plain,
count(A,cons(A,B)) = s(count(A,B)),
inference(copy,[status(thm)],[c_1209]) ).
cnf(c_1210,plain,
aux(s(z),A,cons(B,C),pair2(cons(B,nil),C)) = splitAtNat(s(s(z)),cons(A,cons(B,C))),
inference(paramod,[status(thm)],[c_42,c_10]) ).
cnf(c_1211,plain,
pair2(cons(A,cons(B,nil)),C) = splitAtNat(s(s(z)),cons(A,cons(B,C))),
inference(paramod,[status(thm)],[c_1,c_1210]) ).
cnf(c_55,plain,
splitAtNat(s(s(z)),cons(A,cons(B,C))) = pair2(cons(A,cons(B,nil)),C),
inference(copy,[status(thm)],[c_1211]) ).
cnf(c_1212,plain,
eq2(impl(eq2(leqNat(s(count(A,B)),s(s(s(s(s(z)))))),bfalse),eq(count(A,cons(A,B)),count(s(A),msort(cons(A,B))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_41]) ).
cnf(c_1213,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(s(s(z))))),bfalse),eq(count(A,cons(A,B)),count(s(A),msort(cons(A,B))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_1212]) ).
cnf(c_57,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(s(s(z))))),bfalse),eq(s(count(A,B)),count(s(A),msort(cons(A,B))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_1213]) ).
cnf(c_1214,plain,
eq2(impl(eq2(leqNat(s(count(A,B)),s(s(s(s(z))))),bfalse),eq(s(count(A,cons(A,B))),count(s(A),msort(cons(A,cons(A,B)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_57]) ).
cnf(c_1215,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(s(z)))),bfalse),eq(s(count(A,cons(A,B))),count(s(A),msort(cons(A,cons(A,B)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_1214]) ).
cnf(c_63,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(s(z)))),bfalse),eq(s(s(count(A,B))),count(s(A),msort(cons(A,cons(A,B)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_1215]) ).
cnf(c_1216,plain,
eq2(impl(eq2(leqNat(s(count(A,B)),s(s(s(z)))),bfalse),eq(s(s(count(A,cons(A,B)))),count(s(A),msort(cons(A,cons(A,cons(A,B))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_63]) ).
cnf(c_1217,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(z))),bfalse),eq(s(s(count(A,cons(A,B)))),count(s(A),msort(cons(A,cons(A,cons(A,B))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_1216]) ).
cnf(c_79,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(z))),bfalse),eq(s(s(s(count(A,B)))),count(s(A),msort(cons(A,cons(A,cons(A,B))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_1217]) ).
cnf(c_1218,plain,
aux(s(s(z)),A,cons(B,cons(C,D)),pair2(cons(B,cons(C,nil)),D)) = splitAtNat(s(s(s(z))),cons(A,cons(B,cons(C,D)))),
inference(paramod,[status(thm)],[c_55,c_10]) ).
cnf(c_1219,plain,
pair2(cons(A,cons(B,cons(C,nil))),D) = splitAtNat(s(s(s(z))),cons(A,cons(B,cons(C,D)))),
inference(paramod,[status(thm)],[c_1,c_1218]) ).
cnf(c_94,plain,
splitAtNat(s(s(s(z))),cons(A,cons(B,cons(C,D)))) = pair2(cons(A,cons(B,cons(C,nil))),D),
inference(copy,[status(thm)],[c_1219]) ).
cnf(c_1220,plain,
aux3(A,B,cons(C,nil),splitAtNat(s(div2(s(z))),cons(A,cons(B,cons(C,nil))))) = msort(cons(A,cons(B,cons(C,nil)))),
inference(paramod,[status(thm)],[c_18,c_48]) ).
cnf(c_1221,plain,
aux3(A,B,cons(C,nil),splitAtNat(s(z),cons(A,cons(B,cons(C,nil))))) = msort(cons(A,cons(B,cons(C,nil)))),
inference(paramod,[status(thm)],[c_23,c_1220]) ).
cnf(c_1222,plain,
aux3(A,B,cons(C,nil),pair2(cons(A,nil),cons(B,cons(C,nil)))) = msort(cons(A,cons(B,cons(C,nil)))),
inference(paramod,[status(thm)],[c_42,c_1221]) ).
cnf(c_1223,plain,
merge(msort(cons(A,nil)),msort(cons(B,cons(C,nil)))) = msort(cons(A,cons(B,cons(C,nil)))),
inference(paramod,[status(thm)],[c_4,c_1222]) ).
cnf(c_1224,plain,
merge(cons(A,nil),msort(cons(B,cons(C,nil)))) = msort(cons(A,cons(B,cons(C,nil)))),
inference(paramod,[status(thm)],[c_26,c_1223]) ).
cnf(c_1225,plain,
merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))) = msort(cons(A,cons(B,cons(C,nil)))),
inference(paramod,[status(thm)],[c_47,c_1224]) ).
cnf(c_96,plain,
msort(cons(A,cons(B,cons(C,nil)))) = merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))),
inference(copy,[status(thm)],[c_1225]) ).
cnf(c_1226,plain,
aux3(A,B,cons(C,cons(D,E)),splitAtNat(s(div2(s(s(lengthNat(E))))),cons(A,cons(B,cons(C,cons(D,E)))))) = msort(cons(A,cons(B,cons(C,cons(D,E))))),
inference(paramod,[status(thm)],[c_19,c_48]) ).
cnf(c_97,plain,
aux3(A,B,cons(C,cons(D,E)),splitAtNat(s(s(div2(lengthNat(E)))),cons(A,cons(B,cons(C,cons(D,E)))))) = msort(cons(A,cons(B,cons(C,cons(D,E))))),
inference(paramod,[status(thm)],[c_24,c_1226]) ).
cnf(c_1227,plain,
eq2(impl(eq2(leqNat(s(count(A,B)),s(s(z))),bfalse),eq(s(s(s(count(A,cons(A,B))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,B)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_79]) ).
cnf(c_1228,plain,
eq2(impl(eq2(leqNat(count(A,B),s(z)),bfalse),eq(s(s(s(count(A,cons(A,B))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,B)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_1227]) ).
cnf(c_101,plain,
eq2(impl(eq2(leqNat(count(A,B),s(z)),bfalse),eq(s(s(s(s(count(A,B))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,B)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_1228]) ).
cnf(c_1229,plain,
eq2(impl(eq2(leqNat(s(count(A,B)),s(z)),bfalse),eq(s(s(s(s(count(A,cons(A,B)))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,B))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_101]) ).
cnf(c_1230,plain,
eq2(impl(eq2(leqNat(count(A,B),z),bfalse),eq(s(s(s(s(count(A,cons(A,B)))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,B))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_1229]) ).
cnf(c_202,plain,
eq2(impl(eq2(leqNat(count(A,B),z),bfalse),eq(s(s(s(s(s(count(A,B)))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,B))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_1230]) ).
cnf(c_1231,plain,
aux3(A,B,cons(C,cons(D,nil)),splitAtNat(s(s(div2(z))),cons(A,cons(B,cons(C,cons(D,nil)))))) = msort(cons(A,cons(B,cons(C,cons(D,nil))))),
inference(paramod,[status(thm)],[c_18,c_97]) ).
cnf(c_1232,plain,
aux3(A,B,cons(C,cons(D,nil)),splitAtNat(s(s(z)),cons(A,cons(B,cons(C,cons(D,nil)))))) = msort(cons(A,cons(B,cons(C,cons(D,nil))))),
inference(paramod,[status(thm)],[c_22,c_1231]) ).
cnf(c_1233,plain,
aux3(A,B,cons(C,cons(D,nil)),pair2(cons(A,cons(B,nil)),cons(C,cons(D,nil)))) = msort(cons(A,cons(B,cons(C,cons(D,nil))))),
inference(paramod,[status(thm)],[c_55,c_1232]) ).
cnf(c_1234,plain,
merge(msort(cons(A,cons(B,nil))),msort(cons(C,cons(D,nil)))) = msort(cons(A,cons(B,cons(C,cons(D,nil))))),
inference(paramod,[status(thm)],[c_4,c_1233]) ).
cnf(c_1235,plain,
merge(merge(cons(A,nil),cons(B,nil)),msort(cons(C,cons(D,nil)))) = msort(cons(A,cons(B,cons(C,cons(D,nil))))),
inference(paramod,[status(thm)],[c_47,c_1234]) ).
cnf(c_1236,plain,
merge(merge(cons(A,nil),cons(B,nil)),merge(cons(C,nil),cons(D,nil))) = msort(cons(A,cons(B,cons(C,cons(D,nil))))),
inference(paramod,[status(thm)],[c_47,c_1235]) ).
cnf(c_367,plain,
msort(cons(A,cons(B,cons(C,cons(D,nil))))) = merge(merge(cons(A,nil),cons(B,nil)),merge(cons(C,nil),cons(D,nil))),
inference(copy,[status(thm)],[c_1236]) ).
cnf(c_368,plain,
aux3(A,B,cons(C,cons(D,cons(E,F))),splitAtNat(s(s(div2(s(lengthNat(F))))),cons(A,cons(B,cons(C,cons(D,cons(E,F))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,F)))))),
inference(paramod,[status(thm)],[c_19,c_97]) ).
cnf(c_1237,plain,
eq2(impl(eq2(leqNat(s(count(A,B)),z),bfalse),eq(s(s(s(s(s(count(A,cons(A,B))))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,cons(A,B)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_202]) ).
cnf(c_1238,plain,
eq2(impl(eq2(bfalse,bfalse),eq(s(s(s(s(s(count(A,cons(A,B))))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,cons(A,B)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_12,c_1237]) ).
cnf(c_1239,plain,
eq2(impl(btrue,eq(s(s(s(s(s(count(A,cons(A,B))))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,cons(A,B)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_39,c_1238]) ).
cnf(c_1240,plain,
eq2(impl(btrue,eq(s(s(s(s(s(s(count(A,B))))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,cons(A,B)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_1239]) ).
cnf(c_466,plain,
eq2(eq(s(s(s(s(s(s(count(A,B))))))),count(s(A),msort(cons(A,cons(A,cons(A,cons(A,cons(A,cons(A,B))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_20,c_1240]) ).
cnf(c_480,plain,
eq2(eq(s(s(s(s(s(s(count(z,A))))))),count(s(z),msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,cons(s(B),A)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_51,c_466]) ).
cnf(c_535,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,cons(s(A),nil)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_29,c_480]) ).
cnf(c_1241,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,V6)))),splitAtNat(s(s(div2(s(s(lengthNat(V6)))))),cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,V6)))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,V6))))))),
inference(paramod,[status(thm)],[c_19,c_368]) ).
cnf(c_556,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,V6)))),splitAtNat(s(s(s(div2(lengthNat(V6))))),cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,V6)))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,V6))))))),
inference(paramod,[status(thm)],[c_24,c_1241]) ).
cnf(c_789,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,cons(V6,V7))))),splitAtNat(s(s(s(div2(s(lengthNat(V7)))))),cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,V7))))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,V7)))))))),
inference(paramod,[status(thm)],[c_19,c_556]) ).
cnf(c_1242,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil))))),splitAtNat(s(s(s(div2(s(z))))),cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil))))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil)))))))),
inference(paramod,[status(thm)],[c_18,c_789]) ).
cnf(c_1243,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil))))),splitAtNat(s(s(s(z))),cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil))))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil)))))))),
inference(paramod,[status(thm)],[c_23,c_1242]) ).
cnf(c_1244,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil))))),pair2(cons(A,cons(B,cons(C,nil))),cons(D,cons(E,cons(F,cons(V6,nil)))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil)))))))),
inference(paramod,[status(thm)],[c_94,c_1243]) ).
cnf(c_1245,plain,
merge(msort(cons(A,cons(B,cons(C,nil)))),msort(cons(D,cons(E,cons(F,cons(V6,nil)))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil)))))))),
inference(paramod,[status(thm)],[c_4,c_1244]) ).
cnf(c_1246,plain,
merge(merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))),msort(cons(D,cons(E,cons(F,cons(V6,nil)))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil)))))))),
inference(paramod,[status(thm)],[c_96,c_1245]) ).
cnf(c_1247,plain,
merge(merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))),merge(merge(cons(D,nil),cons(E,nil)),merge(cons(F,nil),cons(V6,nil)))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil)))))))),
inference(paramod,[status(thm)],[c_367,c_1246]) ).
cnf(c_1112,plain,
msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,cons(V6,nil)))))))) = merge(merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))),merge(merge(cons(D,nil),cons(E,nil)),merge(cons(F,nil),cons(V6,nil)))),
inference(copy,[status(thm)],[c_1247]) ).
cnf(c_1248,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(merge(cons(z,nil),merge(cons(z,nil),cons(z,nil))),merge(merge(cons(z,nil),cons(z,nil)),merge(cons(z,nil),cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1112,c_535]) ).
cnf(c_1249,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(merge(cons(z,nil),cons(z,merge(nil,cons(z,nil)))),merge(merge(cons(z,nil),cons(z,nil)),merge(cons(z,nil),cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1248]) ).
cnf(c_1250,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(merge(cons(z,nil),cons(z,cons(z,nil))),merge(merge(cons(z,nil),cons(z,nil)),merge(cons(z,nil),cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_1249]) ).
cnf(c_1251,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,merge(nil,cons(z,cons(z,nil)))),merge(merge(cons(z,nil),cons(z,nil)),merge(cons(z,nil),cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1250]) ).
cnf(c_1252,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),merge(merge(cons(z,nil),cons(z,nil)),merge(cons(z,nil),cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_1251]) ).
cnf(c_1253,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),merge(cons(z,merge(nil,cons(z,nil))),merge(cons(z,nil),cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1252]) ).
cnf(c_1254,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),merge(cons(z,cons(z,nil)),merge(cons(z,nil),cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_1253]) ).
cnf(c_1255,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),merge(cons(z,cons(z,nil)),cons(z,merge(nil,cons(s(A),nil))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1254]) ).
cnf(c_1256,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),merge(cons(z,cons(z,nil)),cons(z,cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_1255]) ).
cnf(c_1257,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),cons(z,merge(cons(z,nil),cons(z,cons(s(A),nil))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1256]) ).
cnf(c_1258,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),cons(z,cons(z,merge(nil,cons(z,cons(s(A),nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1257]) ).
cnf(c_1259,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),merge(cons(z,cons(z,cons(z,nil))),cons(z,cons(z,cons(z,cons(s(A),nil))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_1258]) ).
cnf(c_1260,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,merge(cons(z,cons(z,nil)),cons(z,cons(z,cons(z,cons(s(A),nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1259]) ).
cnf(c_1261,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(z,merge(cons(z,nil),cons(z,cons(z,cons(z,cons(s(A),nil))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1260]) ).
cnf(c_1262,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(z,cons(z,merge(nil,cons(z,cons(z,cons(z,cons(s(A),nil)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_1261]) ).
cnf(c_1263,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,cons(s(A),nil))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_1262]) ).
cnf(c_1264,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(z,cons(z,cons(z,cons(z,cons(s(A),nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_1263]) ).
cnf(c_1265,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(z,cons(z,cons(z,cons(s(A),nil))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_1264]) ).
cnf(c_1266,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(z,cons(z,cons(s(A),nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_1265]) ).
cnf(c_1267,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(z,cons(s(A),nil))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_1266]) ).
cnf(c_1268,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(z,cons(s(A),nil)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_1267]) ).
cnf(c_1115,plain,
eq2(eq(s(s(s(s(s(s(z)))))),count(s(z),cons(s(A),nil))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_1268]) ).
cnf(c_1269,plain,
eq2(eq(s(s(s(s(s(s(z)))))),s(count(s(z),nil))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_1115]) ).
cnf(c_1270,plain,
eq2(eq(s(s(s(s(s(s(z)))))),s(z)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_29,c_1269]) ).
cnf(c_1271,plain,
eq2(eq(s(s(s(s(s(z))))),z),bfalse) != btrue,
inference(paramod,[status(thm)],[c_35,c_1270]) ).
cnf(c_1272,plain,
eq2(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_37,c_1271]) ).
cnf(c_1273,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_39,c_1272]) ).
cnf(c_1190,plain,
$false,
inference(copy,[status(thm)],[c_1273]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX201-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 16:55:07 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2197199 was started by sandbox on n004,
% 0.09/0.37 % Sat Sep 26 16:55:07 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 4.31/1.35
% 4.31/1.35 % SZS status Unsatisfiable for theBenchmark
% 4.31/1.35
% 4.31/1.35 % Proof 1 at 0.46 (+ 0.07) seconds.
% 4.31/1.35 % Length of proof is 60.
% 4.31/1.35 % Level of proof is 12.
% 4.31/1.35 % Maximum clause weight is 54.000.
% 4.31/1.35 % Given clauses 234.
% 4.31/1.35
% 4.31/1.35 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------