%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX203-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.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 : Fri Sep 25 03:32:06 PM UTC 2026
% Result : Unsatisfiable 23.64s 3.49s
% Output : CNFRefutation 23.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 26
% Syntax : Number of clauses : 166 ( 166 unt; 0 nHn; 14 RR)
% Number of literals : 166 ( 165 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 6 con; 0-3 aty)
% Number of variables : 322 ( 35 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(eg0,negated_conjecture,
eq2(psorted_rev(X),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
eqq(eq2(psorted_rev(X1),bfalse),btrue) = efalse,
inference(equality_encoding,[status(esa)],[eg0]) ).
cnf(t82,plain,
eqq(eq2(psorted_rev(X1),bfalse),btrue) = efalse,
inference(orient,[status(thm)],[t24]) ).
cnf(t33,axiom,
impl(eq2(sorted(rev(X1)),btrue),impl(eq2(unique(X1),btrue),eq2(leqNat(lengthNat(X1),s(s(s(z)))),btrue))) = psorted_rev(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t70,plain,
impl(eq2(sorted(rev(X1)),btrue),impl(eq2(unique(X1),btrue),eq2(leqNat(lengthNat(X1),s(s(s(z)))),btrue))) = psorted_rev(X1),
inference(orient,[status(thm)],[t33]) ).
cnf(t28,axiom,
append(rev(X1),cons(X2,nil)) = rev(cons(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t65,plain,
append(rev(X1),cons(X2,nil)) = rev(cons(X2,X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(t1,axiom,
rev(nil) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t56,plain,
rev(nil) = nil,
inference(orient,[status(thm)],[t1]) ).
cnf(t66,plain,
rev(cons(X1,nil)) = append(nil,cons(X1,nil)),
inference(cp,[status(thm)],[t65,t56]) ).
cnf(t6,axiom,
append(nil,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t34,plain,
append(nil,X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t12368,plain,
rev(cons(X1,nil)) = cons(X1,nil),
inference(step,[status(thm)],[t66,t34]) ).
cnf(t88,plain,
rev(cons(X1,nil)) = cons(X1,nil),
inference(orient,[status(thm)],[t12368]) ).
cnf(t89,plain,
rev(cons(X1,cons(X2,nil))) = append(cons(X2,nil),cons(X1,nil)),
inference(cp,[status(thm)],[t65,t88]) ).
cnf(t30,axiom,
cons(X1,append(X2,X3)) = append(cons(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t55,plain,
append(cons(X1,X2),X3) = cons(X1,append(X2,X3)),
inference(orient,[status(thm)],[t30]) ).
cnf(t12386,plain,
rev(cons(X1,cons(X2,nil))) = cons(X2,append(nil,cons(X1,nil))),
inference(step,[status(thm)],[t89,t55]) ).
cnf(t12387,plain,
rev(cons(X1,cons(X2,nil))) = cons(X2,cons(X1,nil)),
inference(step,[status(thm)],[t12386,t34]) ).
cnf(t112,plain,
rev(cons(X1,cons(X2,nil))) = cons(X2,cons(X1,nil)),
inference(orient,[status(thm)],[t12387]) ).
cnf(t113,plain,
rev(cons(X1,cons(X2,cons(X3,nil)))) = append(cons(X3,cons(X2,nil)),cons(X1,nil)),
inference(cp,[status(thm)],[t65,t112]) ).
cnf(t12394,plain,
rev(cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,append(cons(X2,nil),cons(X1,nil))),
inference(step,[status(thm)],[t113,t55]) ).
cnf(t12395,plain,
rev(cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,cons(X2,append(nil,cons(X1,nil)))),
inference(step,[status(thm)],[t12394,t55]) ).
cnf(t12396,plain,
rev(cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,cons(X2,cons(X1,nil))),
inference(step,[status(thm)],[t12395,t34]) ).
cnf(t151,plain,
rev(cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,cons(X2,cons(X1,nil))),
inference(orient,[status(thm)],[t12396]) ).
cnf(t152,plain,
rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = append(cons(Y3,cons(X3,cons(X2,nil))),cons(X1,nil)),
inference(cp,[status(thm)],[t65,t151]) ).
cnf(t12434,plain,
rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = cons(Y3,append(cons(X3,cons(X2,nil)),cons(X1,nil))),
inference(step,[status(thm)],[t152,t55]) ).
cnf(t12435,plain,
rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = cons(Y3,cons(X3,append(cons(X2,nil),cons(X1,nil)))),
inference(step,[status(thm)],[t12434,t55]) ).
cnf(t12436,plain,
rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = cons(Y3,cons(X3,cons(X2,append(nil,cons(X1,nil))))),
inference(step,[status(thm)],[t12435,t55]) ).
cnf(t12437,plain,
rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = cons(Y3,cons(X3,cons(X2,cons(X1,nil)))),
inference(step,[status(thm)],[t12436,t34]) ).
cnf(t235,plain,
rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = cons(Y3,cons(X3,cons(X2,cons(X1,nil)))),
inference(orient,[status(thm)],[t12437]) ).
cnf(t238,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(lengthNat(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),s(s(s(z)))),btrue))),
inference(cp,[status(thm)],[t70,t235]) ).
cnf(t25,axiom,
lengthNat(cons(X1,X2)) = s(lengthNat(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t54,plain,
lengthNat(cons(X1,X2)) = s(lengthNat(X2)),
inference(orient,[status(thm)],[t25]) ).
cnf(t13303,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(s(lengthNat(cons(X2,cons(X3,cons(Y3,nil))))),s(s(s(z)))),btrue))),
inference(step,[status(thm)],[t238,t54]) ).
cnf(t27,axiom,
leqNat(s(X1),s(X2)) = leqNat(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t59,plain,
leqNat(s(X1),s(X2)) = leqNat(X1,X2),
inference(orient,[status(thm)],[t27]) ).
cnf(t13304,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(lengthNat(cons(X2,cons(X3,cons(Y3,nil)))),s(s(z))),btrue))),
inference(step,[status(thm)],[t13303,t59]) ).
cnf(t13305,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(s(lengthNat(cons(X3,cons(Y3,nil)))),s(s(z))),btrue))),
inference(step,[status(thm)],[t13304,t54]) ).
cnf(t13306,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(lengthNat(cons(X3,cons(Y3,nil))),s(z)),btrue))),
inference(step,[status(thm)],[t13305,t59]) ).
cnf(t13307,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(s(lengthNat(cons(Y3,nil))),s(z)),btrue))),
inference(step,[status(thm)],[t13306,t54]) ).
cnf(t13308,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(lengthNat(cons(Y3,nil)),z),btrue))),
inference(step,[status(thm)],[t13307,t59]) ).
cnf(t13309,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(leqNat(s(lengthNat(nil)),z),btrue))),
inference(step,[status(thm)],[t13308,t54]) ).
cnf(t21,axiom,
leqNat(s(X1),z) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t50,plain,
leqNat(s(X1),z) = bfalse,
inference(orient,[status(thm)],[t21]) ).
cnf(t13310,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),eq2(bfalse,btrue))),
inference(step,[status(thm)],[t13309,t50]) ).
cnf(t10,axiom,
eq2(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t47,plain,
eq2(bfalse,btrue) = bfalse,
inference(orient,[status(thm)],[t10]) ).
cnf(t13311,plain,
psorted_rev(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))) = impl(eq2(sorted(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),impl(eq2(unique(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),bfalse)),
inference(step,[status(thm)],[t13310,t47]) ).
cnf(t6904,plain,
impl(eq2(sorted(cons(X1,cons(X2,cons(X3,cons(Y3,nil))))),btrue),impl(eq2(unique(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),btrue),bfalse)) = psorted_rev(cons(Y3,cons(X3,cons(X2,cons(X1,nil))))),
inference(orient,[status(thm)],[t13311]) ).
cnf(t29,axiom,
aux(X1,X2,elemNat(X1,X2)) = unique(cons(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t68,plain,
aux(X1,X2,elemNat(X1,X2)) = unique(cons(X1,X2)),
inference(orient,[status(thm)],[t29]) ).
cnf(t31,axiom,
orb(eq(X1,X2),elemNat(X1,X3)) = elemNat(X1,cons(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t75,plain,
orb(eq(X1,X2),elemNat(X1,X3)) = elemNat(X1,cons(X2,X3)),
inference(orient,[status(thm)],[t31]) ).
cnf(t19,axiom,
eq(s(X1),z) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t48,plain,
eq(s(X1),z) = bfalse,
inference(orient,[status(thm)],[t19]) ).
cnf(t78,plain,
elemNat(s(X1),cons(z,X2)) = orb(bfalse,elemNat(s(X1),X2)),
inference(cp,[status(thm)],[t75,t48]) ).
cnf(t16,axiom,
orb(bfalse,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t36,plain,
orb(bfalse,X1) = X1,
inference(orient,[status(thm)],[t16]) ).
cnf(t12385,plain,
elemNat(s(X1),cons(z,X2)) = elemNat(s(X1),X2),
inference(step,[status(thm)],[t78,t36]) ).
cnf(t107,plain,
elemNat(s(X1),cons(z,X2)) = elemNat(s(X1),X2),
inference(orient,[status(thm)],[t12385]) ).
cnf(t108,plain,
elemNat(s(X1),cons(X2,cons(z,X3))) = orb(eq(s(X1),X2),elemNat(s(X1),X3)),
inference(cp,[status(thm)],[t75,t107]) ).
cnf(t12389,plain,
elemNat(s(X1),cons(X2,cons(z,X3))) = elemNat(s(X1),cons(X2,X3)),
inference(step,[status(thm)],[t108,t75]) ).
cnf(t121,plain,
elemNat(s(X1),cons(X2,cons(z,X3))) = elemNat(s(X1),cons(X2,X3)),
inference(orient,[status(thm)],[t12389]) ).
cnf(t122,plain,
elemNat(s(X1),cons(X2,cons(X3,cons(z,Y3)))) = orb(eq(s(X1),X2),elemNat(s(X1),cons(X3,Y3))),
inference(cp,[status(thm)],[t75,t121]) ).
cnf(t12425,plain,
elemNat(s(X1),cons(X2,cons(X3,cons(z,Y3)))) = elemNat(s(X1),cons(X2,cons(X3,Y3))),
inference(step,[status(thm)],[t122,t75]) ).
cnf(t214,plain,
elemNat(s(X1),cons(X2,cons(X3,cons(z,Y3)))) = elemNat(s(X1),cons(X2,cons(X3,Y3))),
inference(orient,[status(thm)],[t12425]) ).
cnf(t216,plain,
unique(cons(s(X1),cons(X2,cons(X3,cons(z,Y3))))) = aux(s(X1),cons(X2,cons(X3,cons(z,Y3))),elemNat(s(X1),cons(X2,cons(X3,Y3)))),
inference(cp,[status(thm)],[t68,t214]) ).
cnf(t3488,plain,
aux(s(X1),cons(X2,cons(X3,cons(z,Y3))),elemNat(s(X1),cons(X2,cons(X3,Y3)))) = unique(cons(s(X1),cons(X2,cons(X3,cons(z,Y3))))),
inference(orient,[status(thm)],[t216]) ).
cnf(t26,axiom,
eq(s(X1),s(X2)) = eq(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t58,plain,
eq(s(X1),s(X2)) = eq(X1,X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t79,plain,
elemNat(s(X1),cons(s(X2),X3)) = orb(eq(X1,X2),elemNat(s(X1),X3)),
inference(cp,[status(thm)],[t75,t58]) ).
cnf(t136,plain,
orb(eq(X1,X2),elemNat(s(X1),X3)) = elemNat(s(X1),cons(s(X2),X3)),
inference(orient,[status(thm)],[t79]) ).
cnf(t7,axiom,
elemNat(X1,nil) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t51,plain,
elemNat(X1,nil) = bfalse,
inference(orient,[status(thm)],[t7]) ).
cnf(t80,plain,
elemNat(X1,cons(X2,nil)) = orb(eq(X1,X2),bfalse),
inference(cp,[status(thm)],[t75,t51]) ).
cnf(t97,plain,
elemNat(X1,cons(X2,nil)) = orb(eq(X1,X2),bfalse),
inference(orient,[status(thm)],[t80]) ).
cnf(t141,plain,
elemNat(s(X1),cons(s(X2),cons(X3,nil))) = orb(eq(X1,X2),orb(eq(s(X1),X3),bfalse)),
inference(cp,[status(thm)],[t136,t97]) ).
cnf(t227,plain,
orb(eq(X1,X2),orb(eq(s(X1),X3),bfalse)) = elemNat(s(X1),cons(s(X2),cons(X3,nil))),
inference(orient,[status(thm)],[t141]) ).
cnf(t229,plain,
elemNat(s(X1),cons(s(X2),cons(s(X3),nil))) = orb(eq(X1,X2),orb(eq(X1,X3),bfalse)),
inference(cp,[status(thm)],[t227,t58]) ).
cnf(t98,plain,
elemNat(X1,cons(X2,cons(X3,nil))) = orb(eq(X1,X2),orb(eq(X1,X3),bfalse)),
inference(cp,[status(thm)],[t75,t97]) ).
cnf(t160,plain,
orb(eq(X1,X2),orb(eq(X1,X3),bfalse)) = elemNat(X1,cons(X2,cons(X3,nil))),
inference(orient,[status(thm)],[t98]) ).
cnf(t12433,plain,
elemNat(s(X1),cons(s(X2),cons(s(X3),nil))) = elemNat(X1,cons(X2,cons(X3,nil))),
inference(step,[status(thm)],[t229,t160]) ).
cnf(t230,plain,
elemNat(s(X1),cons(s(X2),cons(s(X3),nil))) = elemNat(X1,cons(X2,cons(X3,nil))),
inference(orient,[status(thm)],[t12433]) ).
cnf(t3493,plain,
unique(cons(s(X1),cons(s(X2),cons(s(X3),cons(z,nil))))) = aux(s(X1),cons(s(X2),cons(s(X3),cons(z,nil))),elemNat(X1,cons(X2,cons(X3,nil)))),
inference(cp,[status(thm)],[t3488,t230]) ).
cnf(t7786,plain,
aux(s(X1),cons(s(X2),cons(s(X3),cons(z,nil))),elemNat(X1,cons(X2,cons(X3,nil)))) = unique(cons(s(X1),cons(s(X2),cons(s(X3),cons(z,nil))))),
inference(orient,[status(thm)],[t3493]) ).
cnf(t7800,plain,
unique(cons(s(s(X1)),cons(s(X2),cons(s(z),cons(z,nil))))) = aux(s(s(X1)),cons(s(X2),cons(s(z),cons(z,nil))),elemNat(s(X1),cons(X2,nil))),
inference(cp,[status(thm)],[t7786,t121]) ).
cnf(t13543,plain,
unique(cons(s(s(X1)),cons(s(X2),cons(s(z),cons(z,nil))))) = aux(s(s(X1)),cons(s(X2),cons(s(z),cons(z,nil))),orb(eq(s(X1),X2),bfalse)),
inference(step,[status(thm)],[t7800,t97]) ).
cnf(t10897,plain,
aux(s(s(X1)),cons(s(X2),cons(s(z),cons(z,nil))),orb(eq(s(X1),X2),bfalse)) = unique(cons(s(s(X1)),cons(s(X2),cons(s(z),cons(z,nil))))),
inference(orient,[status(thm)],[t13543]) ).
cnf(t10898,plain,
unique(cons(s(s(X1)),cons(s(s(X2)),cons(s(z),cons(z,nil))))) = aux(s(s(X1)),cons(s(s(X2)),cons(s(z),cons(z,nil))),orb(eq(X1,X2),bfalse)),
inference(cp,[status(thm)],[t10897,t58]) ).
cnf(t12252,plain,
aux(s(s(X1)),cons(s(s(X2)),cons(s(z),cons(z,nil))),orb(eq(X1,X2),bfalse)) = unique(cons(s(s(X1)),cons(s(s(X2)),cons(s(z),cons(z,nil))))),
inference(orient,[status(thm)],[t10898]) ).
cnf(t12254,plain,
unique(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = aux(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))),orb(bfalse,bfalse)),
inference(cp,[status(thm)],[t12252,t48]) ).
cnf(t13676,plain,
unique(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = aux(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))),bfalse),
inference(step,[status(thm)],[t12254,t36]) ).
cnf(t23,axiom,
aux(X1,X2,bfalse) = unique(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t67,plain,
aux(X1,X2,bfalse) = unique(X2),
inference(orient,[status(thm)],[t23]) ).
cnf(t13677,plain,
unique(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = unique(cons(s(s(z)),cons(s(z),cons(z,nil)))),
inference(step,[status(thm)],[t13676,t67]) ).
cnf(t123,plain,
unique(cons(s(X1),cons(X2,cons(z,X3)))) = aux(s(X1),cons(X2,cons(z,X3)),elemNat(s(X1),cons(X2,X3))),
inference(cp,[status(thm)],[t68,t121]) ).
cnf(t429,plain,
aux(s(X1),cons(X2,cons(z,X3)),elemNat(s(X1),cons(X2,X3))) = unique(cons(s(X1),cons(X2,cons(z,X3)))),
inference(orient,[status(thm)],[t123]) ).
cnf(t441,plain,
unique(cons(s(X1),cons(X2,cons(z,nil)))) = aux(s(X1),cons(X2,cons(z,nil)),orb(eq(s(X1),X2),bfalse)),
inference(cp,[status(thm)],[t429,t97]) ).
cnf(t454,plain,
aux(s(X1),cons(X2,cons(z,nil)),orb(eq(s(X1),X2),bfalse)) = unique(cons(s(X1),cons(X2,cons(z,nil)))),
inference(orient,[status(thm)],[t441]) ).
cnf(t455,plain,
unique(cons(s(X1),cons(s(X2),cons(z,nil)))) = aux(s(X1),cons(s(X2),cons(z,nil)),orb(eq(X1,X2),bfalse)),
inference(cp,[status(thm)],[t454,t58]) ).
cnf(t569,plain,
aux(s(X1),cons(s(X2),cons(z,nil)),orb(eq(X1,X2),bfalse)) = unique(cons(s(X1),cons(s(X2),cons(z,nil)))),
inference(orient,[status(thm)],[t455]) ).
cnf(t571,plain,
unique(cons(s(s(X1)),cons(s(z),cons(z,nil)))) = aux(s(s(X1)),cons(s(z),cons(z,nil)),orb(bfalse,bfalse)),
inference(cp,[status(thm)],[t569,t48]) ).
cnf(t12582,plain,
unique(cons(s(s(X1)),cons(s(z),cons(z,nil)))) = aux(s(s(X1)),cons(s(z),cons(z,nil)),bfalse),
inference(step,[status(thm)],[t571,t36]) ).
cnf(t12583,plain,
unique(cons(s(s(X1)),cons(s(z),cons(z,nil)))) = unique(cons(s(z),cons(z,nil))),
inference(step,[status(thm)],[t12582,t67]) ).
cnf(t99,plain,
unique(cons(X1,cons(X2,nil))) = aux(X1,cons(X2,nil),orb(eq(X1,X2),bfalse)),
inference(cp,[status(thm)],[t68,t97]) ).
cnf(t178,plain,
aux(X1,cons(X2,nil),orb(eq(X1,X2),bfalse)) = unique(cons(X1,cons(X2,nil))),
inference(orient,[status(thm)],[t99]) ).
cnf(t179,plain,
unique(cons(s(X1),cons(z,nil))) = aux(s(X1),cons(z,nil),orb(bfalse,bfalse)),
inference(cp,[status(thm)],[t178,t48]) ).
cnf(t12404,plain,
unique(cons(s(X1),cons(z,nil))) = aux(s(X1),cons(z,nil),bfalse),
inference(step,[status(thm)],[t179,t36]) ).
cnf(t12405,plain,
unique(cons(s(X1),cons(z,nil))) = unique(cons(z,nil)),
inference(step,[status(thm)],[t12404,t67]) ).
cnf(t69,plain,
unique(cons(X1,nil)) = aux(X1,nil,bfalse),
inference(cp,[status(thm)],[t68,t51]) ).
cnf(t12366,plain,
unique(cons(X1,nil)) = unique(nil),
inference(step,[status(thm)],[t69,t67]) ).
cnf(t3,axiom,
unique(nil) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t43,plain,
unique(nil) = btrue,
inference(orient,[status(thm)],[t3]) ).
cnf(t12367,plain,
unique(cons(X1,nil)) = btrue,
inference(step,[status(thm)],[t12366,t43]) ).
cnf(t86,plain,
unique(cons(X1,nil)) = btrue,
inference(orient,[status(thm)],[t12367]) ).
cnf(t12406,plain,
unique(cons(s(X1),cons(z,nil))) = btrue,
inference(step,[status(thm)],[t12405,t86]) ).
cnf(t181,plain,
unique(cons(s(X1),cons(z,nil))) = btrue,
inference(orient,[status(thm)],[t12406]) ).
cnf(t12584,plain,
unique(cons(s(s(X1)),cons(s(z),cons(z,nil)))) = btrue,
inference(step,[status(thm)],[t12583,t181]) ).
cnf(t576,plain,
unique(cons(s(s(X1)),cons(s(z),cons(z,nil)))) = btrue,
inference(orient,[status(thm)],[t12584]) ).
cnf(t13678,plain,
unique(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = btrue,
inference(step,[status(thm)],[t13677,t576]) ).
cnf(t12260,plain,
unique(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = btrue,
inference(orient,[status(thm)],[t13678]) ).
cnf(t12263,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(eq2(sorted(cons(z,cons(s(z),cons(s(s(z)),cons(s(s(s(X1))),nil))))),btrue),impl(eq2(btrue,btrue),bfalse)),
inference(cp,[status(thm)],[t6904,t12260]) ).
cnf(t32,axiom,
andb(leqNat(X1,X2),sorted(cons(X2,X3))) = sorted(cons(X1,cons(X2,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t60,plain,
andb(leqNat(X1,X2),sorted(cons(X2,X3))) = sorted(cons(X1,cons(X2,X3))),
inference(orient,[status(thm)],[t32]) ).
cnf(t15,axiom,
leqNat(z,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
leqNat(z,X1) = btrue,
inference(orient,[status(thm)],[t15]) ).
cnf(t61,plain,
sorted(cons(z,cons(X1,X2))) = andb(btrue,sorted(cons(X1,X2))),
inference(cp,[status(thm)],[t60,t40]) ).
cnf(t5,axiom,
andb(btrue,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t37,plain,
andb(btrue,X1) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t12384,plain,
sorted(cons(z,cons(X1,X2))) = sorted(cons(X1,X2)),
inference(step,[status(thm)],[t61,t37]) ).
cnf(t105,plain,
sorted(cons(z,cons(X1,X2))) = sorted(cons(X1,X2)),
inference(orient,[status(thm)],[t12384]) ).
cnf(t13688,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(eq2(sorted(cons(s(z),cons(s(s(z)),cons(s(s(s(X1))),nil)))),btrue),impl(eq2(btrue,btrue),bfalse)),
inference(step,[status(thm)],[t12263,t105]) ).
cnf(t63,plain,
sorted(cons(s(X1),cons(s(X2),X3))) = andb(leqNat(X1,X2),sorted(cons(s(X2),X3))),
inference(cp,[status(thm)],[t60,t59]) ).
cnf(t124,plain,
andb(leqNat(X1,X2),sorted(cons(s(X2),X3))) = sorted(cons(s(X1),cons(s(X2),X3))),
inference(orient,[status(thm)],[t63]) ).
cnf(t125,plain,
sorted(cons(s(z),cons(s(X1),X2))) = andb(btrue,sorted(cons(s(X1),X2))),
inference(cp,[status(thm)],[t124,t40]) ).
cnf(t12391,plain,
sorted(cons(s(z),cons(s(X1),X2))) = sorted(cons(s(X1),X2)),
inference(step,[status(thm)],[t125,t37]) ).
cnf(t133,plain,
sorted(cons(s(z),cons(s(X1),X2))) = sorted(cons(s(X1),X2)),
inference(orient,[status(thm)],[t12391]) ).
cnf(t13689,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(eq2(sorted(cons(s(s(z)),cons(s(s(s(X1))),nil))),btrue),impl(eq2(btrue,btrue),bfalse)),
inference(step,[status(thm)],[t13688,t133]) ).
cnf(t127,plain,
sorted(cons(s(s(X1)),cons(s(s(X2)),X3))) = andb(leqNat(X1,X2),sorted(cons(s(s(X2)),X3))),
inference(cp,[status(thm)],[t124,t59]) ).
cnf(t800,plain,
sorted(cons(s(s(X1)),cons(s(s(X2)),X3))) = andb(leqNat(X1,X2),sorted(cons(s(s(X2)),X3))),
inference(orient,[status(thm)],[t127]) ).
cnf(t815,plain,
sorted(cons(s(s(z)),cons(s(s(X1)),X2))) = andb(btrue,sorted(cons(s(s(X1)),X2))),
inference(cp,[status(thm)],[t800,t40]) ).
cnf(t12651,plain,
sorted(cons(s(s(z)),cons(s(s(X1)),X2))) = sorted(cons(s(s(X1)),X2)),
inference(step,[status(thm)],[t815,t37]) ).
cnf(t836,plain,
sorted(cons(s(s(z)),cons(s(s(X1)),X2))) = sorted(cons(s(s(X1)),X2)),
inference(orient,[status(thm)],[t12651]) ).
cnf(t13690,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(eq2(sorted(cons(s(s(s(X1))),nil)),btrue),impl(eq2(btrue,btrue),bfalse)),
inference(step,[status(thm)],[t13689,t836]) ).
cnf(t22,axiom,
sorted(cons(X1,nil)) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t41,plain,
sorted(cons(X1,nil)) = btrue,
inference(orient,[status(thm)],[t22]) ).
cnf(t13691,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(eq2(btrue,btrue),impl(eq2(btrue,btrue),bfalse)),
inference(step,[status(thm)],[t13690,t41]) ).
cnf(t9,axiom,
eq2(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t38,plain,
eq2(X1,X1) = btrue,
inference(orient,[status(thm)],[t9]) ).
cnf(t13692,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(btrue,impl(eq2(btrue,btrue),bfalse)),
inference(step,[status(thm)],[t13691,t38]) ).
cnf(t14,axiom,
impl(btrue,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
impl(btrue,X1) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t13693,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(eq2(btrue,btrue),bfalse),
inference(step,[status(thm)],[t13692,t35]) ).
cnf(t13694,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = impl(btrue,bfalse),
inference(step,[status(thm)],[t13693,t38]) ).
cnf(t13695,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = bfalse,
inference(step,[status(thm)],[t13694,t35]) ).
cnf(t12265,plain,
psorted_rev(cons(s(s(s(X1))),cons(s(s(z)),cons(s(z),cons(z,nil))))) = bfalse,
inference(orient,[status(thm)],[t13695]) ).
cnf(t12266,plain,
efalse = eqq(eq2(bfalse,bfalse),btrue),
inference(cp,[status(thm)],[t82,t12265]) ).
cnf(t13696,plain,
efalse = eqq(btrue,btrue),
inference(step,[status(thm)],[t12266,t38]) ).
cnf(t12,plain,
eqq(X1,X1) = etrue,
introduced(definition) ).
cnf(t81,plain,
eqq(X1,X1) = etrue,
inference(orient,[status(thm)],[t12]) ).
cnf(t13697,plain,
efalse = etrue,
inference(step,[status(thm)],[t13696,t81]) ).
cnf(t12267,plain,
efalse = etrue,
inference(orient,[status(thm)],[t13697]) ).
cnf(goal_0,negated_conjecture,
etrue != efalse,
introduced(definition) ).
cnf(g0_0,plain,
etrue != etrue,
inference(rw,[status(thm)],[goal_0,t12267]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX203-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 23:37:32 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 23.64/3.49 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 23.64/3.49 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------