%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX203-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 : n005.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 5.26s 1.20s
% Output : CNFRefutation 5.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 26
% Syntax : Number of formulae : 176 ( 176 unt; 0 def)
% Number of atoms : 176 ( 175 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 30 ( 30 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 4 con; 0-3 aty)
% Number of variables : 263 ( 29 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [VAR_0,VAR_1] : aux(VAR_0,VAR_1,bfalse) = unique(VAR_1),
file('theBenchmark.p',axiom_001) ).
cnf(c_2,plain,
aux(A,B,bfalse) = unique(B),
inference(clausify,[status(thm)],[axiom_001]) ).
fof(axiom_003,axiom,
! [VAR_0] : orb(bfalse,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_003) ).
cnf(c_4,plain,
orb(bfalse,A) = A,
inference(clausify,[status(thm)],[axiom_003]) ).
fof(axiom_004,axiom,
! [VAR_0] : leqNat(z,VAR_0) = btrue,
file('theBenchmark.p',axiom_004) ).
cnf(c_5,plain,
leqNat(z,A) = btrue,
inference(clausify,[status(thm)],[axiom_004]) ).
fof(axiom_005,axiom,
! [VAR_0] : leqNat(s(VAR_0),z) = bfalse,
file('theBenchmark.p',axiom_005) ).
cnf(c_6,plain,
leqNat(s(A),z) = bfalse,
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_006,axiom,
! [VAR_0,VAR_1] : leqNat(s(VAR_0),s(VAR_1)) = leqNat(VAR_0,VAR_1),
file('theBenchmark.p',axiom_006) ).
cnf(c_7,plain,
leqNat(s(A),s(B)) = leqNat(A,B),
inference(clausify,[status(thm)],[axiom_006]) ).
fof(axiom_007,axiom,
lengthNat(nil) = z,
file('theBenchmark.p',axiom_007) ).
cnf(c_8,plain,
lengthNat(nil) = z,
inference(clausify,[status(thm)],[axiom_007]) ).
fof(axiom_008,axiom,
! [VAR_0,VAR_1] : lengthNat(cons(VAR_0,VAR_1)) = s(lengthNat(VAR_1)),
file('theBenchmark.p',axiom_008) ).
cnf(c_9,plain,
lengthNat(cons(A,B)) = s(lengthNat(B)),
inference(clausify,[status(thm)],[axiom_008]) ).
fof(axiom_009,axiom,
! [VAR_0] : impl(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_009) ).
cnf(c_10,plain,
impl(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_009]) ).
fof(axiom_011,axiom,
! [VAR_0] : elemNat(VAR_0,nil) = bfalse,
file('theBenchmark.p',axiom_011) ).
cnf(c_12,plain,
elemNat(A,nil) = bfalse,
inference(clausify,[status(thm)],[axiom_011]) ).
fof(axiom_012,axiom,
! [VAR_0,VAR_1,VAR_2] : elemNat(VAR_0,cons(VAR_1,VAR_2)) = orb(eq(VAR_0,VAR_1),elemNat(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_012) ).
cnf(c_13,plain,
elemNat(A,cons(B,C)) = orb(eq(A,B),elemNat(A,C)),
inference(clausify,[status(thm)],[axiom_012]) ).
cnf(c_14,plain,
orb(eq(A,B),elemNat(A,C)) = elemNat(A,cons(B,C)),
inference(copy,[status(thm)],[c_13]) ).
fof(axiom_013,axiom,
unique(nil) = btrue,
file('theBenchmark.p',axiom_013) ).
cnf(c_15,plain,
unique(nil) = btrue,
inference(clausify,[status(thm)],[axiom_013]) ).
cnf(c_16,plain,
btrue = unique(nil),
inference(copy,[status(thm)],[c_15]) ).
fof(axiom_014,axiom,
! [VAR_0,VAR_1] : unique(cons(VAR_0,VAR_1)) = aux(VAR_0,VAR_1,elemNat(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_014) ).
cnf(c_17,plain,
unique(cons(A,B)) = aux(A,B,elemNat(A,B)),
inference(clausify,[status(thm)],[axiom_014]) ).
cnf(c_18,plain,
aux(A,B,elemNat(A,B)) = unique(cons(A,B)),
inference(copy,[status(thm)],[c_17]) ).
fof(axiom_015,axiom,
! [VAR_0] : append(nil,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_015) ).
cnf(c_19,plain,
append(nil,A) = A,
inference(clausify,[status(thm)],[axiom_015]) ).
fof(axiom_016,axiom,
! [VAR_0,VAR_1,VAR_2] : append(cons(VAR_0,VAR_1),VAR_2) = cons(VAR_0,append(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_016) ).
cnf(c_20,plain,
append(cons(A,B),C) = cons(A,append(B,C)),
inference(clausify,[status(thm)],[axiom_016]) ).
fof(axiom_017,axiom,
rev(nil) = nil,
file('theBenchmark.p',axiom_017) ).
cnf(c_21,plain,
rev(nil) = nil,
inference(clausify,[status(thm)],[axiom_017]) ).
fof(axiom_018,axiom,
! [VAR_0,VAR_1] : rev(cons(VAR_0,VAR_1)) = append(rev(VAR_1),cons(VAR_0,nil)),
file('theBenchmark.p',axiom_018) ).
cnf(c_22,plain,
rev(cons(A,B)) = append(rev(B),cons(A,nil)),
inference(clausify,[status(thm)],[axiom_018]) ).
cnf(c_23,plain,
append(rev(A),cons(B,nil)) = rev(cons(B,A)),
inference(copy,[status(thm)],[c_22]) ).
fof(axiom_019,axiom,
! [VAR_0] : andb(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_019) ).
cnf(c_24,plain,
andb(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_019]) ).
cnf(c_25,plain,
andb(unique(nil),A) = A,
inference(paramod,[status(thm)],[c_16,c_24]) ).
fof(axiom_021,axiom,
sorted(nil) = btrue,
file('theBenchmark.p',axiom_021) ).
cnf(c_27,plain,
sorted(nil) = btrue,
inference(clausify,[status(thm)],[axiom_021]) ).
cnf(c_467,plain,
sorted(nil) = unique(nil),
inference(paramod,[status(thm)],[c_16,c_27]) ).
cnf(c_28,plain,
unique(nil) = sorted(nil),
inference(copy,[status(thm)],[c_467]) ).
fof(axiom_022,axiom,
! [VAR_0] : sorted(cons(VAR_0,nil)) = btrue,
file('theBenchmark.p',axiom_022) ).
cnf(c_29,plain,
sorted(cons(A,nil)) = btrue,
inference(clausify,[status(thm)],[axiom_022]) ).
cnf(c_468,plain,
sorted(cons(A,nil)) = unique(nil),
inference(paramod,[status(thm)],[c_16,c_29]) ).
cnf(c_30,plain,
sorted(cons(A,nil)) = sorted(nil),
inference(paramod,[status(thm)],[c_28,c_468]) ).
fof(axiom_023,axiom,
! [VAR_0,VAR_1,VAR_2] : sorted(cons(VAR_0,cons(VAR_1,VAR_2))) = andb(leqNat(VAR_0,VAR_1),sorted(cons(VAR_1,VAR_2))),
file('theBenchmark.p',axiom_023) ).
cnf(c_31,plain,
sorted(cons(A,cons(B,C))) = andb(leqNat(A,B),sorted(cons(B,C))),
inference(clausify,[status(thm)],[axiom_023]) ).
cnf(c_32,plain,
andb(leqNat(A,B),sorted(cons(B,C))) = sorted(cons(A,cons(B,C))),
inference(copy,[status(thm)],[c_31]) ).
fof(axiom_024,axiom,
! [VAR_0] : psorted_rev(VAR_0) = impl(eq2(sorted(rev(VAR_0)),btrue),impl(eq2(unique(VAR_0),btrue),eq2(leqNat(lengthNat(VAR_0),s(s(s(z)))),btrue))),
file('theBenchmark.p',axiom_024) ).
cnf(c_33,plain,
psorted_rev(A) = impl(eq2(sorted(rev(A)),btrue),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))),
inference(clausify,[status(thm)],[axiom_024]) ).
cnf(c_469,plain,
psorted_rev(A) = impl(eq2(sorted(rev(A)),unique(nil)),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))),
inference(paramod,[status(thm)],[c_16,c_33]) ).
cnf(c_470,plain,
psorted_rev(A) = impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))),
inference(paramod,[status(thm)],[c_28,c_469]) ).
cnf(c_471,plain,
psorted_rev(A) = impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),unique(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))),
inference(paramod,[status(thm)],[c_16,c_470]) ).
cnf(c_472,plain,
psorted_rev(A) = impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))),
inference(paramod,[status(thm)],[c_28,c_471]) ).
cnf(c_473,plain,
psorted_rev(A) = impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),unique(nil)))),
inference(paramod,[status(thm)],[c_16,c_472]) ).
cnf(c_34,plain,
psorted_rev(A) = impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),sorted(nil)))),
inference(paramod,[status(thm)],[c_28,c_473]) ).
fof(axiom_025,axiom,
eq2(bfalse,btrue) = bfalse,
file('theBenchmark.p',axiom_025) ).
cnf(c_35,plain,
eq2(bfalse,btrue) = bfalse,
inference(clausify,[status(thm)],[axiom_025]) ).
cnf(c_474,plain,
eq2(bfalse,unique(nil)) = bfalse,
inference(paramod,[status(thm)],[c_16,c_35]) ).
cnf(c_36,plain,
eq2(bfalse,sorted(nil)) = bfalse,
inference(paramod,[status(thm)],[c_28,c_474]) ).
fof(axiom_027,axiom,
! [VAR_0,VAR_1] : eq(s(VAR_0),s(VAR_1)) = eq(VAR_0,VAR_1),
file('theBenchmark.p',axiom_027) ).
cnf(c_39,plain,
eq(s(A),s(B)) = eq(A,B),
inference(clausify,[status(thm)],[axiom_027]) ).
fof(axiom_029,axiom,
! [VAR_0] : eq(s(VAR_0),z) = bfalse,
file('theBenchmark.p',axiom_029) ).
cnf(c_41,plain,
eq(s(A),z) = bfalse,
inference(clausify,[status(thm)],[axiom_029]) ).
fof(axiom_031,axiom,
! [VAR_0] : eq2(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_031) ).
cnf(c_44,plain,
eq2(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_031]) ).
cnf(c_475,plain,
eq2(A,A) = unique(nil),
inference(paramod,[status(thm)],[c_16,c_44]) ).
cnf(c_45,plain,
eq2(A,A) = sorted(nil),
inference(paramod,[status(thm)],[c_28,c_475]) ).
fof(goal,axiom,
! [VAR_0] : eq2(psorted_rev(VAR_0),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_46,plain,
eq2(psorted_rev(A),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_476,plain,
eq2(impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),sorted(nil)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_34,c_46]) ).
cnf(c_477,plain,
eq2(impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),sorted(nil)))),bfalse) != unique(nil),
inference(paramod,[status(thm)],[c_16,c_476]) ).
cnf(c_47,plain,
eq2(impl(eq2(sorted(rev(A)),sorted(nil)),impl(eq2(unique(A),sorted(nil)),eq2(leqNat(lengthNat(A),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_28,c_477]) ).
cnf(c_478,plain,
impl(unique(nil),A) = A,
inference(paramod,[status(thm)],[c_16,c_10]) ).
cnf(c_49,plain,
impl(sorted(nil),A) = A,
inference(paramod,[status(thm)],[c_28,c_478]) ).
cnf(c_479,plain,
leqNat(z,A) = unique(nil),
inference(paramod,[status(thm)],[c_16,c_5]) ).
cnf(c_50,plain,
leqNat(z,A) = sorted(nil),
inference(paramod,[status(thm)],[c_28,c_479]) ).
cnf(c_53,plain,
andb(sorted(nil),A) = A,
inference(paramod,[status(thm)],[c_28,c_25]) ).
cnf(c_55,plain,
orb(eq(A,B),bfalse) = elemNat(A,cons(B,nil)),
inference(paramod,[status(thm)],[c_12,c_14]) ).
cnf(c_480,plain,
aux(A,nil,bfalse) = unique(cons(A,nil)),
inference(paramod,[status(thm)],[c_12,c_18]) ).
cnf(c_481,plain,
unique(nil) = unique(cons(A,nil)),
inference(paramod,[status(thm)],[c_2,c_480]) ).
cnf(c_482,plain,
sorted(nil) = unique(cons(A,nil)),
inference(paramod,[status(thm)],[c_28,c_481]) ).
cnf(c_56,plain,
unique(cons(A,nil)) = sorted(nil),
inference(copy,[status(thm)],[c_482]) ).
cnf(c_483,plain,
append(nil,cons(A,nil)) = rev(cons(A,nil)),
inference(paramod,[status(thm)],[c_21,c_23]) ).
cnf(c_484,plain,
cons(A,nil) = rev(cons(A,nil)),
inference(paramod,[status(thm)],[c_19,c_483]) ).
cnf(c_57,plain,
rev(cons(A,nil)) = cons(A,nil),
inference(copy,[status(thm)],[c_484]) ).
cnf(c_59,plain,
andb(leqNat(A,B),sorted(cons(s(B),C))) = sorted(cons(s(A),cons(s(B),C))),
inference(paramod,[status(thm)],[c_7,c_32]) ).
cnf(c_485,plain,
andb(leqNat(A,B),sorted(nil)) = sorted(cons(A,cons(B,nil))),
inference(paramod,[status(thm)],[c_30,c_32]) ).
cnf(c_60,plain,
sorted(cons(A,cons(B,nil))) = andb(leqNat(A,B),sorted(nil)),
inference(copy,[status(thm)],[c_485]) ).
cnf(c_61,plain,
orb(eq(A,B),elemNat(s(A),C)) = elemNat(s(A),cons(s(B),C)),
inference(paramod,[status(thm)],[c_39,c_14]) ).
cnf(c_486,plain,
orb(bfalse,elemNat(s(A),B)) = elemNat(s(A),cons(z,B)),
inference(paramod,[status(thm)],[c_41,c_14]) ).
cnf(c_487,plain,
elemNat(s(A),B) = elemNat(s(A),cons(z,B)),
inference(paramod,[status(thm)],[c_4,c_486]) ).
cnf(c_63,plain,
elemNat(s(A),cons(z,B)) = elemNat(s(A),B),
inference(copy,[status(thm)],[c_487]) ).
cnf(c_488,plain,
orb(eq(A,B),bfalse) = elemNat(s(A),cons(s(B),nil)),
inference(paramod,[status(thm)],[c_39,c_55]) ).
cnf(c_489,plain,
elemNat(A,cons(B,nil)) = elemNat(s(A),cons(s(B),nil)),
inference(paramod,[status(thm)],[c_55,c_488]) ).
cnf(c_68,plain,
elemNat(s(A),cons(s(B),nil)) = elemNat(A,cons(B,nil)),
inference(copy,[status(thm)],[c_489]) ).
cnf(c_490,plain,
append(cons(A,nil),cons(B,nil)) = rev(cons(B,cons(A,nil))),
inference(paramod,[status(thm)],[c_57,c_23]) ).
cnf(c_491,plain,
cons(A,append(nil,cons(B,nil))) = rev(cons(B,cons(A,nil))),
inference(paramod,[status(thm)],[c_20,c_490]) ).
cnf(c_492,plain,
cons(A,cons(B,nil)) = rev(cons(B,cons(A,nil))),
inference(paramod,[status(thm)],[c_19,c_491]) ).
cnf(c_71,plain,
rev(cons(A,cons(B,nil))) = cons(B,cons(A,nil)),
inference(copy,[status(thm)],[c_492]) ).
cnf(c_493,plain,
orb(eq(s(A),B),elemNat(s(A),C)) = elemNat(s(A),cons(B,cons(z,C))),
inference(paramod,[status(thm)],[c_63,c_14]) ).
cnf(c_494,plain,
elemNat(s(A),cons(B,C)) = elemNat(s(A),cons(B,cons(z,C))),
inference(paramod,[status(thm)],[c_14,c_493]) ).
cnf(c_75,plain,
elemNat(s(A),cons(B,cons(z,C))) = elemNat(s(A),cons(B,C)),
inference(copy,[status(thm)],[c_494]) ).
cnf(c_76,plain,
aux(s(A),cons(z,B),elemNat(s(A),B)) = unique(cons(s(A),cons(z,B))),
inference(paramod,[status(thm)],[c_63,c_18]) ).
cnf(c_495,plain,
orb(bfalse,elemNat(s(s(A)),B)) = elemNat(s(s(A)),cons(s(z),B)),
inference(paramod,[status(thm)],[c_41,c_61]) ).
cnf(c_496,plain,
elemNat(s(s(A)),B) = elemNat(s(s(A)),cons(s(z),B)),
inference(paramod,[status(thm)],[c_4,c_495]) ).
cnf(c_89,plain,
elemNat(s(s(A)),cons(s(z),B)) = elemNat(s(s(A)),B),
inference(copy,[status(thm)],[c_496]) ).
cnf(c_497,plain,
orb(eq(A,B),elemNat(A,cons(C,nil))) = elemNat(s(A),cons(s(B),cons(s(C),nil))),
inference(paramod,[status(thm)],[c_68,c_61]) ).
cnf(c_498,plain,
elemNat(A,cons(B,cons(C,nil))) = elemNat(s(A),cons(s(B),cons(s(C),nil))),
inference(paramod,[status(thm)],[c_14,c_497]) ).
cnf(c_90,plain,
elemNat(s(A),cons(s(B),cons(s(C),nil))) = elemNat(A,cons(B,cons(C,nil))),
inference(copy,[status(thm)],[c_498]) ).
cnf(c_499,plain,
orb(eq(s(A),B),elemNat(s(A),cons(C,D))) = elemNat(s(A),cons(B,cons(C,cons(z,D)))),
inference(paramod,[status(thm)],[c_75,c_14]) ).
cnf(c_500,plain,
elemNat(s(A),cons(B,cons(C,D))) = elemNat(s(A),cons(B,cons(C,cons(z,D)))),
inference(paramod,[status(thm)],[c_14,c_499]) ).
cnf(c_96,plain,
elemNat(s(A),cons(B,cons(C,cons(z,D)))) = elemNat(s(A),cons(B,cons(C,D))),
inference(copy,[status(thm)],[c_500]) ).
cnf(c_97,plain,
aux(s(A),cons(B,cons(z,C)),elemNat(s(A),cons(B,C))) = unique(cons(s(A),cons(B,cons(z,C)))),
inference(paramod,[status(thm)],[c_75,c_18]) ).
cnf(c_501,plain,
andb(sorted(nil),sorted(cons(s(A),B))) = sorted(cons(s(z),cons(s(A),B))),
inference(paramod,[status(thm)],[c_50,c_59]) ).
cnf(c_502,plain,
sorted(cons(s(A),B)) = sorted(cons(s(z),cons(s(A),B))),
inference(paramod,[status(thm)],[c_53,c_501]) ).
cnf(c_100,plain,
sorted(cons(s(z),cons(s(A),B))) = sorted(cons(s(A),B)),
inference(copy,[status(thm)],[c_502]) ).
cnf(c_503,plain,
append(cons(A,cons(B,nil)),cons(C,nil)) = rev(cons(C,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_71,c_23]) ).
cnf(c_504,plain,
cons(A,append(cons(B,nil),cons(C,nil))) = rev(cons(C,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_20,c_503]) ).
cnf(c_505,plain,
cons(A,cons(B,append(nil,cons(C,nil)))) = rev(cons(C,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_20,c_504]) ).
cnf(c_506,plain,
cons(A,cons(B,cons(C,nil))) = rev(cons(C,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_19,c_505]) ).
cnf(c_102,plain,
rev(cons(A,cons(B,cons(C,nil)))) = cons(C,cons(B,cons(A,nil))),
inference(copy,[status(thm)],[c_506]) ).
cnf(c_507,plain,
aux(s(A),cons(z,nil),bfalse) = unique(cons(s(A),cons(z,nil))),
inference(paramod,[status(thm)],[c_12,c_76]) ).
cnf(c_508,plain,
unique(cons(z,nil)) = unique(cons(s(A),cons(z,nil))),
inference(paramod,[status(thm)],[c_2,c_507]) ).
cnf(c_509,plain,
sorted(nil) = unique(cons(s(A),cons(z,nil))),
inference(paramod,[status(thm)],[c_56,c_508]) ).
cnf(c_103,plain,
unique(cons(s(A),cons(z,nil))) = sorted(nil),
inference(copy,[status(thm)],[c_509]) ).
cnf(c_510,plain,
andb(leqNat(A,s(z)),sorted(cons(s(B),C))) = sorted(cons(A,cons(s(z),cons(s(B),C)))),
inference(paramod,[status(thm)],[c_100,c_32]) ).
cnf(c_122,plain,
sorted(cons(A,cons(s(z),cons(s(B),C)))) = andb(leqNat(A,s(z)),sorted(cons(s(B),C))),
inference(copy,[status(thm)],[c_510]) ).
cnf(c_155,plain,
aux(s(A),cons(B,cons(C,cons(z,D))),elemNat(s(A),cons(B,cons(C,D)))) = unique(cons(s(A),cons(B,cons(C,cons(z,D))))),
inference(paramod,[status(thm)],[c_96,c_18]) ).
cnf(c_511,plain,
append(cons(A,cons(B,cons(C,nil))),cons(D,nil)) = rev(cons(D,cons(C,cons(B,cons(A,nil))))),
inference(paramod,[status(thm)],[c_102,c_23]) ).
cnf(c_512,plain,
cons(A,append(cons(B,cons(C,nil)),cons(D,nil))) = rev(cons(D,cons(C,cons(B,cons(A,nil))))),
inference(paramod,[status(thm)],[c_20,c_511]) ).
cnf(c_513,plain,
cons(A,cons(B,append(cons(C,nil),cons(D,nil)))) = rev(cons(D,cons(C,cons(B,cons(A,nil))))),
inference(paramod,[status(thm)],[c_20,c_512]) ).
cnf(c_514,plain,
cons(A,cons(B,cons(C,append(nil,cons(D,nil))))) = rev(cons(D,cons(C,cons(B,cons(A,nil))))),
inference(paramod,[status(thm)],[c_20,c_513]) ).
cnf(c_515,plain,
cons(A,cons(B,cons(C,cons(D,nil)))) = rev(cons(D,cons(C,cons(B,cons(A,nil))))),
inference(paramod,[status(thm)],[c_19,c_514]) ).
cnf(c_161,plain,
rev(cons(A,cons(B,cons(C,cons(D,nil))))) = cons(D,cons(C,cons(B,cons(A,nil)))),
inference(copy,[status(thm)],[c_515]) ).
cnf(c_176,plain,
aux(s(A),cons(s(B),cons(z,nil)),elemNat(A,cons(B,nil))) = unique(cons(s(A),cons(s(B),cons(z,nil)))),
inference(paramod,[status(thm)],[c_68,c_97]) ).
cnf(c_516,plain,
aux(s(s(A)),cons(s(z),cons(z,nil)),elemNat(s(A),nil)) = unique(cons(s(s(A)),cons(s(z),cons(z,nil)))),
inference(paramod,[status(thm)],[c_63,c_176]) ).
cnf(c_517,plain,
aux(s(s(A)),cons(s(z),cons(z,nil)),bfalse) = unique(cons(s(s(A)),cons(s(z),cons(z,nil)))),
inference(paramod,[status(thm)],[c_12,c_516]) ).
cnf(c_518,plain,
unique(cons(s(z),cons(z,nil))) = unique(cons(s(s(A)),cons(s(z),cons(z,nil)))),
inference(paramod,[status(thm)],[c_2,c_517]) ).
cnf(c_519,plain,
sorted(nil) = unique(cons(s(s(A)),cons(s(z),cons(z,nil)))),
inference(paramod,[status(thm)],[c_103,c_518]) ).
cnf(c_187,plain,
unique(cons(s(s(A)),cons(s(z),cons(z,nil)))) = sorted(nil),
inference(copy,[status(thm)],[c_519]) ).
cnf(c_350,plain,
aux(s(A),cons(s(B),cons(s(C),cons(z,nil))),elemNat(A,cons(B,cons(C,nil)))) = unique(cons(s(A),cons(s(B),cons(s(C),cons(z,nil))))),
inference(paramod,[status(thm)],[c_90,c_155]) ).
cnf(c_419,plain,
aux(s(s(A)),cons(s(B),cons(s(z),cons(z,nil))),elemNat(s(A),cons(B,nil))) = unique(cons(s(s(A)),cons(s(B),cons(s(z),cons(z,nil))))),
inference(paramod,[status(thm)],[c_75,c_350]) ).
cnf(c_520,plain,
aux(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))),elemNat(s(s(A)),nil)) = unique(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),
inference(paramod,[status(thm)],[c_89,c_419]) ).
cnf(c_521,plain,
aux(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))),bfalse) = unique(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),
inference(paramod,[status(thm)],[c_12,c_520]) ).
cnf(c_522,plain,
unique(cons(s(s(z)),cons(s(z),cons(z,nil)))) = unique(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),
inference(paramod,[status(thm)],[c_2,c_521]) ).
cnf(c_523,plain,
sorted(nil) = unique(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),
inference(paramod,[status(thm)],[c_187,c_522]) ).
cnf(c_464,plain,
unique(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = sorted(nil),
inference(copy,[status(thm)],[c_523]) ).
cnf(c_524,plain,
eq2(impl(eq2(sorted(rev(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil)))))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_464,c_47]) ).
cnf(c_525,plain,
eq2(impl(eq2(sorted(cons(z,cons(s(z),cons(s(s(z)),cons(s(s(s(A))),nil))))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_161,c_524]) ).
cnf(c_526,plain,
eq2(impl(eq2(andb(leqNat(z,s(z)),sorted(cons(s(s(z)),cons(s(s(s(A))),nil)))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_122,c_525]) ).
cnf(c_527,plain,
eq2(impl(eq2(andb(sorted(nil),sorted(cons(s(s(z)),cons(s(s(s(A))),nil)))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_50,c_526]) ).
cnf(c_528,plain,
eq2(impl(eq2(andb(sorted(nil),andb(leqNat(s(s(z)),s(s(s(A)))),sorted(nil))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_60,c_527]) ).
cnf(c_529,plain,
eq2(impl(eq2(andb(sorted(nil),andb(leqNat(s(z),s(s(A))),sorted(nil))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_7,c_528]) ).
cnf(c_530,plain,
eq2(impl(eq2(andb(sorted(nil),andb(leqNat(z,s(A)),sorted(nil))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_7,c_529]) ).
cnf(c_531,plain,
eq2(impl(eq2(andb(sorted(nil),andb(sorted(nil),sorted(nil))),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_50,c_530]) ).
cnf(c_532,plain,
eq2(impl(eq2(andb(sorted(nil),sorted(nil)),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_53,c_531]) ).
cnf(c_533,plain,
eq2(impl(eq2(sorted(nil),sorted(nil)),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_53,c_532]) ).
cnf(c_534,plain,
eq2(impl(sorted(nil),impl(eq2(sorted(nil),sorted(nil)),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_45,c_533]) ).
cnf(c_535,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(lengthNat(cons(s(s(s(A))),cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_45,c_534]) ).
cnf(c_536,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(lengthNat(cons(s(s(z)),cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_9,c_535]) ).
cnf(c_537,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(s(lengthNat(cons(s(z),cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_9,c_536]) ).
cnf(c_538,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(s(s(lengthNat(cons(z,nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_9,c_537]) ).
cnf(c_539,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(s(s(s(lengthNat(nil))))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_9,c_538]) ).
cnf(c_540,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(s(s(s(z)))),s(s(s(z)))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_8,c_539]) ).
cnf(c_541,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(s(s(z))),s(s(z))),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_7,c_540]) ).
cnf(c_542,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(s(z)),s(z)),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_7,c_541]) ).
cnf(c_543,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(leqNat(s(z),z),sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_7,c_542]) ).
cnf(c_544,plain,
eq2(impl(sorted(nil),impl(sorted(nil),eq2(bfalse,sorted(nil)))),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_6,c_543]) ).
cnf(c_545,plain,
eq2(impl(sorted(nil),impl(sorted(nil),bfalse)),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_36,c_544]) ).
cnf(c_546,plain,
eq2(impl(sorted(nil),bfalse),bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_49,c_545]) ).
cnf(c_547,plain,
eq2(bfalse,bfalse) != sorted(nil),
inference(paramod,[status(thm)],[c_49,c_546]) ).
cnf(c_548,plain,
sorted(nil) != sorted(nil),
inference(paramod,[status(thm)],[c_45,c_547]) ).
cnf(c_466,plain,
$false,
inference(copy,[status(thm)],[c_548]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX203-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n005.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sat Sep 26 16:54:46 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.44 % Process 2593374 was started by sandbox2 on n005,
% 0.18/0.44 % Sat Sep 26 16:54:46 2026
% 0.18/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.44
% 0.18/0.44 % From the command line: assign(max_seconds, 300).
% 5.26/1.20
% 5.26/1.20 % SZS status Unsatisfiable for theBenchmark
% 5.26/1.20
% 5.26/1.20 % Proof 1 at 0.61 (+ 0.13) seconds.
% 5.26/1.20 % Length of proof is 68.
% 5.26/1.20 % Level of proof is 9.
% 5.26/1.20 % Maximum clause weight is 99.000.
% 5.26/1.20 % Given clauses 408.
% 5.26/1.20
% 5.26/1.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------