%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX202-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 : 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:19 AM UTC 2026
% Result : Unsatisfiable 0.12s 10.83s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 27
% Syntax : Number of formulae : 151 ( 151 unt; 0 def)
% Number of atoms : 151 ( 150 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 46 ( 46 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 12 ( 2 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 : 309 ( 14 sgn 52 !; 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_676,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_677,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_676]) ).
cnf(c_678,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_677]) ).
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_678]) ).
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_wrong2(VAR_0,VAR_1) = impl(eq2(leqNat(count(VAR_1,VAR_0),s(s(s(s(s(z)))))),bfalse),eq(count(s(VAR_1),VAR_0),count(VAR_1,msort(VAR_0)))),
file('theBenchmark.p',axiom_027) ).
cnf(c_32,plain,
prop_msort_permutation_wrong2(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(s(B),A),count(B,msort(A)))),
inference(clausify,[status(thm)],[axiom_027]) ).
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_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_wrong2(VAR_0,VAR_1),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_40,plain,
eq2(prop_msort_permutation_wrong2(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(s(A),B),count(A,msort(B)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_32,c_40]) ).
cnf(c_679,plain,
aux(z,A,B,pair2(nil,B)) = splitAtNat(s(z),cons(A,B)),
inference(paramod,[status(thm)],[c_7,c_10]) ).
cnf(c_680,plain,
pair2(cons(A,nil),B) = splitAtNat(s(z),cons(A,B)),
inference(paramod,[status(thm)],[c_1,c_679]) ).
cnf(c_42,plain,
splitAtNat(s(z),cons(A,B)) = pair2(cons(A,nil),B),
inference(copy,[status(thm)],[c_680]) ).
cnf(c_681,plain,
aux2(z,A,B,C,btrue) = merge(cons(z,A),cons(B,C)),
inference(paramod,[status(thm)],[c_11,c_17]) ).
cnf(c_682,plain,
cons(z,merge(A,cons(B,C))) = merge(cons(z,A),cons(B,C)),
inference(paramod,[status(thm)],[c_2,c_681]) ).
cnf(c_44,plain,
merge(cons(z,A),cons(B,C)) = cons(z,merge(A,cons(B,C))),
inference(copy,[status(thm)],[c_682]) ).
cnf(c_683,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_684,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_683]) ).
cnf(c_685,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_684]) ).
cnf(c_686,plain,
merge(msort(cons(A,nil)),msort(cons(B,nil))) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_4,c_685]) ).
cnf(c_687,plain,
merge(cons(A,nil),msort(cons(B,nil))) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_26,c_686]) ).
cnf(c_688,plain,
merge(cons(A,nil),cons(B,nil)) = msort(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_26,c_687]) ).
cnf(c_47,plain,
msort(cons(A,cons(B,nil))) = merge(cons(A,nil),cons(B,nil)),
inference(copy,[status(thm)],[c_688]) ).
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_689,plain,
aux4(s(A),z,B,bfalse) = count(s(A),cons(z,B)),
inference(paramod,[status(thm)],[c_36,c_31]) ).
cnf(c_690,plain,
count(s(A),B) = count(s(A),cons(z,B)),
inference(paramod,[status(thm)],[c_6,c_689]) ).
cnf(c_50,plain,
count(s(A),cons(z,B)) = count(s(A),B),
inference(copy,[status(thm)],[c_690]) ).
cnf(c_691,plain,
aux4(A,A,B,btrue) = count(A,cons(A,B)),
inference(paramod,[status(thm)],[c_38,c_31]) ).
cnf(c_692,plain,
s(count(A,B)) = count(A,cons(A,B)),
inference(paramod,[status(thm)],[c_5,c_691]) ).
cnf(c_52,plain,
count(A,cons(A,B)) = s(count(A,B)),
inference(copy,[status(thm)],[c_692]) ).
cnf(c_693,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_694,plain,
pair2(cons(A,cons(B,nil)),C) = splitAtNat(s(s(z)),cons(A,cons(B,C))),
inference(paramod,[status(thm)],[c_1,c_693]) ).
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_694]) ).
cnf(c_695,plain,
eq2(impl(eq2(leqNat(s(count(A,B)),s(s(s(s(s(z)))))),bfalse),eq(count(s(A),cons(A,B)),count(A,msort(cons(A,B))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_41]) ).
cnf(c_57,plain,
eq2(impl(eq2(leqNat(count(A,B),s(s(s(s(z))))),bfalse),eq(count(s(A),cons(A,B)),count(A,msort(cons(A,B))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_695]) ).
cnf(c_67,plain,
eq2(impl(eq2(leqNat(count(z,A),s(s(s(s(z))))),bfalse),eq(count(s(z),A),count(z,msort(cons(z,A))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_57]) ).
cnf(c_696,plain,
eq2(impl(eq2(leqNat(s(count(z,A)),s(s(s(s(z))))),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,A)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_67]) ).
cnf(c_697,plain,
eq2(impl(eq2(leqNat(count(z,A),s(s(s(z)))),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,A)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_696]) ).
cnf(c_68,plain,
eq2(impl(eq2(leqNat(count(z,A),s(s(s(z)))),bfalse),eq(count(s(z),A),count(z,msort(cons(z,cons(z,A)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_697]) ).
cnf(c_698,plain,
eq2(impl(eq2(leqNat(s(count(z,A)),s(s(s(z)))),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,A))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_68]) ).
cnf(c_699,plain,
eq2(impl(eq2(leqNat(count(z,A),s(s(z))),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,A))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_698]) ).
cnf(c_71,plain,
eq2(impl(eq2(leqNat(count(z,A),s(s(z))),bfalse),eq(count(s(z),A),count(z,msort(cons(z,cons(z,cons(z,A))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_699]) ).
cnf(c_700,plain,
eq2(impl(eq2(leqNat(s(count(z,A)),s(s(z))),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,cons(z,A)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_71]) ).
cnf(c_701,plain,
eq2(impl(eq2(leqNat(count(z,A),s(z)),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,cons(z,A)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_700]) ).
cnf(c_88,plain,
eq2(impl(eq2(leqNat(count(z,A),s(z)),bfalse),eq(count(s(z),A),count(z,msort(cons(z,cons(z,cons(z,cons(z,A)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_701]) ).
cnf(c_702,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_703,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_702]) ).
cnf(c_105,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_703]) ).
cnf(c_704,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_705,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_704]) ).
cnf(c_706,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_705]) ).
cnf(c_707,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_706]) ).
cnf(c_708,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_707]) ).
cnf(c_709,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_708]) ).
cnf(c_107,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_709]) ).
cnf(c_710,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_108,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_710]) ).
cnf(c_711,plain,
eq2(impl(eq2(leqNat(s(count(z,A)),s(z)),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,A))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_88]) ).
cnf(c_712,plain,
eq2(impl(eq2(leqNat(count(z,A),z),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,A))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_13,c_711]) ).
cnf(c_110,plain,
eq2(impl(eq2(leqNat(count(z,A),z),bfalse),eq(count(s(z),A),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,A))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_712]) ).
cnf(c_713,plain,
eq2(impl(eq2(leqNat(s(count(z,A)),z),bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,A)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_110]) ).
cnf(c_714,plain,
eq2(impl(eq2(bfalse,bfalse),eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,A)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_12,c_713]) ).
cnf(c_715,plain,
eq2(impl(btrue,eq(count(s(z),cons(z,A)),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,A)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_39,c_714]) ).
cnf(c_716,plain,
eq2(impl(btrue,eq(count(s(z),A),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,A)))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_715]) ).
cnf(c_187,plain,
eq2(eq(count(s(z),A),count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,A))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_20,c_716]) ).
cnf(c_190,plain,
eq2(eq(z,count(z,msort(cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,nil))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_29,c_187]) ).
cnf(c_343,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_108]) ).
cnf(c_717,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_343]) ).
cnf(c_520,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_717]) ).
cnf(c_718,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,nil)))),splitAtNat(s(s(s(div2(z)))),cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil)))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil))))))),
inference(paramod,[status(thm)],[c_18,c_520]) ).
cnf(c_719,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,nil)))),splitAtNat(s(s(s(z))),cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil)))))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil))))))),
inference(paramod,[status(thm)],[c_22,c_718]) ).
cnf(c_720,plain,
aux3(A,B,cons(C,cons(D,cons(E,cons(F,nil)))),pair2(cons(A,cons(B,cons(C,nil))),cons(D,cons(E,cons(F,nil))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil))))))),
inference(paramod,[status(thm)],[c_105,c_719]) ).
cnf(c_721,plain,
merge(msort(cons(A,cons(B,cons(C,nil)))),msort(cons(D,cons(E,cons(F,nil))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil))))))),
inference(paramod,[status(thm)],[c_4,c_720]) ).
cnf(c_722,plain,
merge(merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))),msort(cons(D,cons(E,cons(F,nil))))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil))))))),
inference(paramod,[status(thm)],[c_107,c_721]) ).
cnf(c_723,plain,
merge(merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))),merge(cons(D,nil),merge(cons(E,nil),cons(F,nil)))) = msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil))))))),
inference(paramod,[status(thm)],[c_107,c_722]) ).
cnf(c_673,plain,
msort(cons(A,cons(B,cons(C,cons(D,cons(E,cons(F,nil))))))) = merge(merge(cons(A,nil),merge(cons(B,nil),cons(C,nil))),merge(cons(D,nil),merge(cons(E,nil),cons(F,nil)))),
inference(copy,[status(thm)],[c_723]) ).
cnf(c_724,plain,
eq2(eq(z,count(z,merge(merge(cons(z,nil),merge(cons(z,nil),cons(z,nil))),merge(cons(z,nil),merge(cons(z,nil),cons(z,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_673,c_190]) ).
cnf(c_725,plain,
eq2(eq(z,count(z,merge(merge(cons(z,nil),cons(z,merge(nil,cons(z,nil)))),merge(cons(z,nil),merge(cons(z,nil),cons(z,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_724]) ).
cnf(c_726,plain,
eq2(eq(z,count(z,merge(merge(cons(z,nil),cons(z,cons(z,nil))),merge(cons(z,nil),merge(cons(z,nil),cons(z,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_725]) ).
cnf(c_727,plain,
eq2(eq(z,count(z,merge(cons(z,merge(nil,cons(z,cons(z,nil)))),merge(cons(z,nil),merge(cons(z,nil),cons(z,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_726]) ).
cnf(c_728,plain,
eq2(eq(z,count(z,merge(cons(z,cons(z,cons(z,nil))),merge(cons(z,nil),merge(cons(z,nil),cons(z,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_727]) ).
cnf(c_729,plain,
eq2(eq(z,count(z,merge(cons(z,cons(z,cons(z,nil))),merge(cons(z,nil),cons(z,merge(nil,cons(z,nil))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_728]) ).
cnf(c_730,plain,
eq2(eq(z,count(z,merge(cons(z,cons(z,cons(z,nil))),merge(cons(z,nil),cons(z,cons(z,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_729]) ).
cnf(c_731,plain,
eq2(eq(z,count(z,merge(cons(z,cons(z,cons(z,nil))),cons(z,merge(nil,cons(z,cons(z,nil))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_730]) ).
cnf(c_732,plain,
eq2(eq(z,count(z,merge(cons(z,cons(z,cons(z,nil))),cons(z,cons(z,cons(z,nil)))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_731]) ).
cnf(c_733,plain,
eq2(eq(z,count(z,cons(z,merge(cons(z,cons(z,nil)),cons(z,cons(z,cons(z,nil))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_732]) ).
cnf(c_734,plain,
eq2(eq(z,count(z,cons(z,cons(z,merge(cons(z,nil),cons(z,cons(z,cons(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_733]) ).
cnf(c_735,plain,
eq2(eq(z,count(z,cons(z,cons(z,cons(z,merge(nil,cons(z,cons(z,cons(z,nil))))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_44,c_734]) ).
cnf(c_736,plain,
eq2(eq(z,count(z,cons(z,cons(z,cons(z,cons(z,cons(z,cons(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_735]) ).
cnf(c_737,plain,
eq2(eq(z,s(count(z,cons(z,cons(z,cons(z,cons(z,cons(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_736]) ).
cnf(c_738,plain,
eq2(eq(z,s(s(count(z,cons(z,cons(z,cons(z,cons(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_737]) ).
cnf(c_739,plain,
eq2(eq(z,s(s(s(count(z,cons(z,cons(z,cons(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_738]) ).
cnf(c_740,plain,
eq2(eq(z,s(s(s(s(count(z,cons(z,cons(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_739]) ).
cnf(c_741,plain,
eq2(eq(z,s(s(s(s(s(count(z,cons(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_740]) ).
cnf(c_742,plain,
eq2(eq(z,s(s(s(s(s(s(count(z,nil)))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_741]) ).
cnf(c_743,plain,
eq2(eq(z,s(s(s(s(s(s(z))))))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_29,c_742]) ).
cnf(c_744,plain,
eq2(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_36,c_743]) ).
cnf(c_745,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_39,c_744]) ).
cnf(c_675,plain,
$false,
inference(copy,[status(thm)],[c_745]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX202-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/10.58 % Computer : n010.cluster.edu
% 0.09/10.58 % Model : x86_64 x86_64
% 0.09/10.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.58 % Memory : 8046.5625MB
% 0.09/10.58 % OS : Linux 6.8.0-71-generic
% 0.09/10.58 % CPULimit : 300
% 0.09/10.58 % WCLimit : 300
% 0.09/10.58 % DateTime : Sat Sep 26 16:55:43 UTC 2026
% 0.09/10.59 % CPUTime :
% 0.09/10.59 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/10.59 % Process 3754106 was started by sandbox on n010,
% 0.09/10.59 % Sat Sep 26 16:55:43 2026
% 0.09/10.59 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/10.59
% 0.09/10.59 % From the command line: assign(max_seconds, 300).
% 0.12/10.83
% 0.12/10.83 % SZS status Unsatisfiable for theBenchmark
% 0.12/10.83
% 0.12/10.83 % Proof 1 at 0.19 (+ 0.03) seconds.
% 0.12/10.83 % Length of proof is 54.
% 0.12/10.83 % Level of proof is 11.
% 0.12/10.83 % Maximum clause weight is 47.000.
% 0.12/10.83 % Given clauses 187.
% 0.12/10.83
% 0.12/10.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------