%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWX203-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n017.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:49 PM UTC 2026
% Result : Unsatisfiable 35.06s 5.31s
% Output : CNFRefutation 35.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 28
% Syntax : Number of formulae : 147 ( 147 unt; 3 def)
% Number of atoms : 288 ( 146 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 14 ( 14 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 4 con; 0-3 aty)
% Number of variables : 183 ( 0 sgn 183 !; 0 ?; 140 :)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] : aux(X0,X1,bfalse) = unique(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_001) ).
fof(f5,axiom,
! [X0] : orb(bfalse,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_003) ).
fof(f6,axiom,
! [X0] : leqNat(z,X0) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_004) ).
fof(f7,plain,
! [X0] : btrue = leqNat(z,X0),
inference(reorient_equations,[],[f6]) ).
fof(f8,axiom,
! [X0] : leqNat(s(X0),z) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
fof(f9,plain,
! [X0] : bfalse = leqNat(s(X0),z),
inference(reorient_equations,[],[f8]) ).
fof(f10,axiom,
! [X0,X1] : leqNat(s(X0),s(X1)) = leqNat(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
fof(f11,axiom,
lengthNat(nil) = z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
fof(f12,plain,
z = lengthNat(nil),
inference(reorient_equations,[],[f11]) ).
fof(f13,axiom,
! [X0,X1] : lengthNat(cons(X0,X1)) = s(lengthNat(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_008) ).
fof(f14,axiom,
! [X0] : impl(btrue,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_009) ).
fof(f17,axiom,
! [X0] : elemNat(X0,nil) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_011) ).
fof(f18,plain,
! [X0] : bfalse = elemNat(X0,nil),
inference(reorient_equations,[],[f17]) ).
fof(f19,axiom,
! [X2,X0,X1] : elemNat(X0,cons(X1,X2)) = orb(eq(X0,X1),elemNat(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
fof(f20,axiom,
unique(nil) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_013) ).
fof(f21,plain,
btrue = unique(nil),
inference(reorient_equations,[],[f20]) ).
fof(f22,axiom,
! [X0,X1] : unique(cons(X0,X1)) = aux(X0,X1,elemNat(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
fof(f23,axiom,
! [X0] : append(nil,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_015) ).
fof(f24,axiom,
! [X2,X0,X1] : append(cons(X0,X1),X2) = cons(X0,append(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
fof(f25,axiom,
rev(nil) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_017) ).
fof(f26,plain,
nil = rev(nil),
inference(reorient_equations,[],[f25]) ).
fof(f27,axiom,
! [X0,X1] : rev(cons(X0,X1)) = append(rev(X1),cons(X0,nil)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_018) ).
fof(f28,axiom,
! [X0] : andb(btrue,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
fof(f33,axiom,
! [X0] : sorted(cons(X0,nil)) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_022) ).
fof(f34,plain,
! [X0] : btrue = sorted(cons(X0,nil)),
inference(reorient_equations,[],[f33]) ).
fof(f35,axiom,
! [X2,X0,X1] : sorted(cons(X0,cons(X1,X2))) = andb(leqNat(X0,X1),sorted(cons(X1,X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_023) ).
fof(f36,axiom,
! [X0] : psorted_rev(X0) = impl(eq2(sorted(rev(X0)),btrue),impl(eq2(unique(X0),btrue),eq2(leqNat(lengthNat(X0),s(s(s(z)))),btrue))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_024) ).
fof(f37,axiom,
eq2(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_025) ).
fof(f38,plain,
bfalse = eq2(bfalse,btrue),
inference(reorient_equations,[],[f37]) ).
fof(f41,axiom,
! [X0,X1] : eq(s(X0),s(X1)) = eq(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_027) ).
fof(f42,plain,
! [X0,X1] : eq(X0,X1) = eq(s(X0),s(X1)),
inference(reorient_equations,[],[f41]) ).
fof(f45,axiom,
! [X0] : eq(s(X0),z) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_029) ).
fof(f46,plain,
! [X0] : bfalse = eq(s(X0),z),
inference(reorient_equations,[],[f45]) ).
fof(f49,axiom,
! [X0] : eq2(X0,X0) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_031) ).
fof(f50,plain,
! [X0] : btrue = eq2(X0,X0),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
! [X0] : eq2(psorted_rev(X0),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f52,plain,
! [X0] : btrue != eq2(psorted_rev(X0),bfalse),
inference(reorient_equations,[],[f51]) ).
fof(f53,plain,
! [X0] : btrue != eq2(impl(eq2(sorted(rev(X0)),btrue),impl(eq2(unique(X0),btrue),eq2(leqNat(lengthNat(X0),s(s(s(z)))),btrue))),bfalse),
inference(definition_unfolding,[],[f52,f36]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i] : aux(X0,X1,bfalse) = unique(X1),
inference(cnf_transformation,[],[f2]) ).
tcf(c_85,plain,
! [X0: $i] : orb(bfalse,X0) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_86,plain,
! [X0: $i] : leqNat(z,X0) = btrue,
inference(cnf_transformation,[],[f7]) ).
tcf(c_87,plain,
! [X0: $i] : leqNat(s(X0),z) = bfalse,
inference(cnf_transformation,[],[f9]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i] : leqNat(s(X0),s(X1)) = leqNat(X0,X1),
inference(cnf_transformation,[],[f10]) ).
tcf(c_89,plain,
lengthNat(nil) = z,
inference(cnf_transformation,[],[f12]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i] : lengthNat(cons(X0,X1)) = s(lengthNat(X1)),
inference(cnf_transformation,[],[f13]) ).
tcf(c_91,plain,
! [X0: $i] : impl(btrue,X0) = X0,
inference(cnf_transformation,[],[f14]) ).
tcf(c_93,plain,
! [X0: $i] : elemNat(X0,nil) = bfalse,
inference(cnf_transformation,[],[f18]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i,X2: $i] : orb(eq(X0,X1),elemNat(X0,X2)) = elemNat(X0,cons(X1,X2)),
inference(cnf_transformation,[],[f19]) ).
tcf(c_95,plain,
unique(nil) = btrue,
inference(cnf_transformation,[],[f21]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i] : aux(X0,X1,elemNat(X0,X1)) = unique(cons(X0,X1)),
inference(cnf_transformation,[],[f22]) ).
tcf(c_97,plain,
! [X0: $i] : append(nil,X0) = X0,
inference(cnf_transformation,[],[f23]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i] : cons(X0,append(X1,X2)) = append(cons(X0,X1),X2),
inference(cnf_transformation,[],[f24]) ).
tcf(c_99,plain,
rev(nil) = nil,
inference(cnf_transformation,[],[f26]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i] : append(rev(X0),cons(X1,nil)) = rev(cons(X1,X0)),
inference(cnf_transformation,[],[f27]) ).
tcf(c_101,plain,
! [X0: $i] : andb(btrue,X0) = X0,
inference(cnf_transformation,[],[f28]) ).
tcf(c_104,plain,
! [X0: $i] : sorted(cons(X0,nil)) = btrue,
inference(cnf_transformation,[],[f34]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : andb(leqNat(X0,X1),sorted(cons(X1,X2))) = sorted(cons(X0,cons(X1,X2))),
inference(cnf_transformation,[],[f35]) ).
tcf(c_106,plain,
eq2(bfalse,btrue) = bfalse,
inference(cnf_transformation,[],[f38]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i] : eq(s(X0),s(X1)) = eq(X0,X1),
inference(cnf_transformation,[],[f42]) ).
tcf(c_110,plain,
! [X0: $i] : eq(s(X0),z) = bfalse,
inference(cnf_transformation,[],[f46]) ).
tcf(c_112,plain,
! [X0: $i] : eq2(X0,X0) = btrue,
inference(cnf_transformation,[],[f50]) ).
tcf(c_113,negated_conjecture,
! [X0: $i] : eq2(impl(eq2(sorted(rev(X0)),btrue),impl(eq2(unique(X0),btrue),eq2(leqNat(lengthNat(X0),s(s(s(z)))),btrue))),bfalse) != btrue,
inference(cnf_transformation,[],[f53]) ).
tcf(c_221,definition,
iPr_def_10 = s(z),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_222,definition,
iPr_def_11 = s(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_223,definition,
iPr_def_12 = s(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_224,negated_conjecture,
! [X0: $i] : eq2(impl(eq2(sorted(rev(X0)),btrue),impl(eq2(unique(X0),btrue),eq2(leqNat(lengthNat(X0),iPr_def_12),btrue))),bfalse) != btrue,
inference(demodulation,[status(thm)],[c_113,c_221,c_222,c_223]) ).
tcf(c_4451,plain,
! [X0: $i,X1: $i,X2: $i] : andb(leqNat(X0,X1),sorted(cons(s(X1),X2))) = sorted(cons(s(X0),cons(s(X1),X2))),
inference(superposition,[status(thm)],[c_88,c_105]) ).
tcf(c_4452,plain,
! [X0: $i,X1: $i,X2: $i] : andb(leqNat(X0,X1),sorted(cons(s(s(X1)),X2))) = sorted(cons(s(s(X0)),cons(s(s(X1)),X2))),
inference(superposition,[status(thm)],[c_88,c_4451]) ).
tcf(c_4456,plain,
! [X0: $i] : leqNat(s(X0),iPr_def_10) = leqNat(X0,z),
inference(superposition,[status(thm)],[c_221,c_88]) ).
tcf(c_4457,plain,
! [X0: $i] : eq(s(X0),iPr_def_10) = eq(X0,z),
inference(superposition,[status(thm)],[c_221,c_108]) ).
tcf(c_4459,plain,
! [X0: $i,X1: $i] : eq2(impl(eq2(sorted(rev(cons(X0,X1))),btrue),impl(eq2(unique(cons(X0,X1)),btrue),eq2(leqNat(s(lengthNat(X1)),iPr_def_12),btrue))),bfalse) != btrue,
inference(superposition,[status(thm)],[c_90,c_224]) ).
tcf(c_4464,plain,
! [X0: $i,X1: $i] : andb(btrue,sorted(cons(X0,X1))) = sorted(cons(z,cons(X0,X1))),
inference(superposition,[status(thm)],[c_86,c_105]) ).
tcf(c_4465,plain,
! [X0: $i,X1: $i] : sorted(cons(z,cons(X0,X1))) = sorted(cons(X0,X1)),
inference(demodulation,[status(thm)],[c_4464,c_101]) ).
tcf(c_4469,plain,
! [X0: $i,X1: $i,X2: $i] : eq2(impl(eq2(sorted(rev(cons(X0,cons(X1,X2)))),btrue),impl(eq2(unique(cons(X0,cons(X1,X2))),btrue),eq2(leqNat(s(s(lengthNat(X2))),iPr_def_12),btrue))),bfalse) != btrue,
inference(superposition,[status(thm)],[c_90,c_4459]) ).
tcf(c_4474,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eq2(impl(eq2(sorted(rev(cons(X0,cons(X1,cons(X2,X3))))),btrue),impl(eq2(unique(cons(X0,cons(X1,cons(X2,X3)))),btrue),eq2(leqNat(s(s(s(lengthNat(X3)))),iPr_def_12),btrue))),bfalse) != btrue,
inference(superposition,[status(thm)],[c_90,c_4469]) ).
tcf(c_4483,plain,
leqNat(iPr_def_10,z) = bfalse,
inference(superposition,[status(thm)],[c_221,c_87]) ).
tcf(c_4490,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : eq2(impl(eq2(sorted(rev(cons(X0,cons(X1,cons(X2,cons(X3,X4)))))),btrue),impl(eq2(unique(cons(X0,cons(X1,cons(X2,cons(X3,X4))))),btrue),eq2(leqNat(s(s(s(s(lengthNat(X4))))),iPr_def_12),btrue))),bfalse) != btrue,
inference(superposition,[status(thm)],[c_90,c_4474]) ).
tcf(c_4494,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eq2(impl(eq2(sorted(rev(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))),btrue),impl(eq2(unique(cons(X0,cons(X1,cons(X2,cons(X3,nil))))),btrue),eq2(leqNat(s(s(s(s(z)))),iPr_def_12),btrue))),bfalse) != btrue,
inference(superposition,[status(thm)],[c_89,c_4490]) ).
tcf(c_4496,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eq2(impl(eq2(sorted(rev(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))),btrue),impl(eq2(unique(cons(X0,cons(X1,cons(X2,cons(X3,nil))))),btrue),eq2(leqNat(s(iPr_def_12),iPr_def_12),btrue))),bfalse) != btrue,
inference(light_normalisation,[status(thm)],[c_4494,c_221,c_222,c_223]) ).
tcf(c_4499,plain,
! [X0: $i] : aux(X0,nil,bfalse) = unique(cons(X0,nil)),
inference(superposition,[status(thm)],[c_93,c_96]) ).
tcf(c_4500,plain,
! [X0: $i] : unique(cons(X0,nil)) = unique(nil),
inference(demodulation,[status(thm)],[c_4499,c_83]) ).
tcf(c_4501,plain,
! [X0: $i] : unique(cons(X0,nil)) = btrue,
inference(light_normalisation,[status(thm)],[c_4500,c_95]) ).
tcf(c_4527,plain,
! [X0: $i] : append(nil,cons(X0,nil)) = rev(cons(X0,nil)),
inference(superposition,[status(thm)],[c_99,c_100]) ).
tcf(c_4529,plain,
! [X0: $i] : rev(cons(X0,nil)) = cons(X0,nil),
inference(demodulation,[status(thm)],[c_4527,c_97]) ).
tcf(c_4540,plain,
! [X0: $i,X1: $i,X2: $i] : orb(eq(X0,X1),elemNat(s(X0),X2)) = elemNat(s(X0),cons(s(X1),X2)),
inference(superposition,[status(thm)],[c_108,c_94]) ).
tcf(c_4541,plain,
! [X0: $i,X1: $i] : orb(eq(X0,X1),bfalse) = elemNat(X0,cons(X1,nil)),
inference(superposition,[status(thm)],[c_93,c_94]) ).
tcf(c_4575,plain,
! [X0: $i,X1: $i] : sorted(cons(s(s(z)),cons(s(s(X0)),X1))) = andb(btrue,sorted(cons(s(s(X0)),X1))),
inference(superposition,[status(thm)],[c_86,c_4452]) ).
tcf(c_4584,plain,
! [X0: $i,X1: $i] : sorted(cons(s(s(z)),cons(s(s(X0)),X1))) = sorted(cons(s(s(X0)),X1)),
inference(demodulation,[status(thm)],[c_4575,c_101]) ).
tcf(c_4585,plain,
! [X0: $i,X1: $i] : sorted(cons(iPr_def_11,cons(s(s(X0)),X1))) = sorted(cons(s(s(X0)),X1)),
inference(light_normalisation,[status(thm)],[c_4584,c_221,c_222]) ).
tcf(c_4656,plain,
eq(iPr_def_10,z) = bfalse,
inference(superposition,[status(thm)],[c_221,c_110]) ).
tcf(c_4693,plain,
! [X0: $i] : elemNat(s(X0),cons(z,nil)) = orb(bfalse,bfalse),
inference(superposition,[status(thm)],[c_110,c_4541]) ).
tcf(c_4694,plain,
! [X0: $i] : elemNat(s(X0),cons(z,nil)) = bfalse,
inference(demodulation,[status(thm)],[c_4693,c_85]) ).
tcf(c_4696,plain,
elemNat(iPr_def_10,cons(z,nil)) = bfalse,
inference(superposition,[status(thm)],[c_221,c_4694]) ).
tcf(c_4719,plain,
eq(iPr_def_11,z) = bfalse,
inference(superposition,[status(thm)],[c_222,c_110]) ).
tcf(c_4722,plain,
! [X0: $i] : sorted(cons(iPr_def_11,cons(s(iPr_def_11),X0))) = sorted(cons(s(iPr_def_11),X0)),
inference(superposition,[status(thm)],[c_222,c_4585]) ).
tcf(c_4730,plain,
leqNat(iPr_def_10,z) = leqNat(iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_222,c_4456]) ).
tcf(c_4735,plain,
! [X0: $i,X1: $i] : andb(leqNat(X0,iPr_def_10),sorted(cons(iPr_def_11,X1))) = sorted(cons(s(X0),cons(iPr_def_11,X1))),
inference(superposition,[status(thm)],[c_222,c_4451]) ).
tcf(c_4736,plain,
! [X0: $i] : leqNat(s(X0),iPr_def_11) = leqNat(X0,iPr_def_10),
inference(superposition,[status(thm)],[c_222,c_88]) ).
tcf(c_4738,plain,
leqNat(iPr_def_11,iPr_def_10) = bfalse,
inference(light_normalisation,[status(thm)],[c_4730,c_4483]) ).
tcf(c_4743,plain,
! [X0: $i] : sorted(cons(iPr_def_11,cons(iPr_def_12,X0))) = sorted(cons(iPr_def_12,X0)),
inference(light_normalisation,[status(thm)],[c_4722,c_223]) ).
tcf(c_4752,plain,
aux(iPr_def_10,cons(z,nil),bfalse) = unique(cons(iPr_def_10,cons(z,nil))),
inference(superposition,[status(thm)],[c_4696,c_96]) ).
tcf(c_4753,plain,
unique(cons(iPr_def_10,cons(z,nil))) = btrue,
inference(demodulation,[status(thm)],[c_4752,c_83,c_4501]) ).
tcf(c_4777,plain,
! [X0: $i] : sorted(cons(s(z),cons(iPr_def_11,X0))) = andb(btrue,sorted(cons(iPr_def_11,X0))),
inference(superposition,[status(thm)],[c_86,c_4735]) ).
tcf(c_4784,plain,
! [X0: $i] : sorted(cons(s(z),cons(iPr_def_11,X0))) = sorted(cons(iPr_def_11,X0)),
inference(demodulation,[status(thm)],[c_4777,c_101]) ).
tcf(c_4785,plain,
! [X0: $i] : sorted(cons(iPr_def_10,cons(iPr_def_11,X0))) = sorted(cons(iPr_def_11,X0)),
inference(light_normalisation,[status(thm)],[c_4784,c_221]) ).
tcf(c_4804,plain,
leqNat(iPr_def_11,iPr_def_10) = leqNat(iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_223,c_4736]) ).
tcf(c_4808,plain,
eq(iPr_def_12,z) = bfalse,
inference(superposition,[status(thm)],[c_223,c_110]) ).
tcf(c_4824,plain,
! [X0: $i] : leqNat(s(X0),iPr_def_12) = leqNat(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_223,c_88]) ).
tcf(c_4827,plain,
leqNat(iPr_def_12,iPr_def_11) = bfalse,
inference(light_normalisation,[status(thm)],[c_4804,c_4738]) ).
tcf(c_4830,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eq2(impl(eq2(sorted(rev(cons(X0,cons(X1,cons(X2,cons(X3,nil)))))),btrue),impl(eq2(unique(cons(X0,cons(X1,cons(X2,cons(X3,nil))))),btrue),eq2(leqNat(iPr_def_12,iPr_def_11),btrue))),bfalse) != btrue,
inference(demodulation,[status(thm)],[c_4496,c_4824]) ).
tcf(c_4996,plain,
eq(iPr_def_10,z) = eq(iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_222,c_4457]) ).
tcf(c_4997,plain,
eq(iPr_def_11,z) = eq(iPr_def_12,iPr_def_10),
inference(superposition,[status(thm)],[c_223,c_4457]) ).
tcf(c_5000,plain,
eq(iPr_def_12,iPr_def_10) = bfalse,
inference(light_normalisation,[status(thm)],[c_4997,c_4719]) ).
tcf(c_5001,plain,
eq(iPr_def_11,iPr_def_10) = bfalse,
inference(light_normalisation,[status(thm)],[c_4996,c_4656]) ).
tcf(c_6149,plain,
elemNat(iPr_def_11,cons(iPr_def_10,nil)) = orb(bfalse,bfalse),
inference(superposition,[status(thm)],[c_5001,c_4541]) ).
tcf(c_6151,plain,
elemNat(iPr_def_11,cons(iPr_def_10,nil)) = bfalse,
inference(demodulation,[status(thm)],[c_6149,c_85]) ).
tcf(c_6405,plain,
! [X0: $i,X1: $i] : append(cons(X0,nil),cons(X1,nil)) = rev(cons(X1,cons(X0,nil))),
inference(superposition,[status(thm)],[c_4529,c_100]) ).
tcf(c_6407,plain,
! [X0: $i,X1: $i] : rev(cons(X0,cons(X1,nil))) = cons(X1,cons(X0,nil)),
inference(demodulation,[status(thm)],[c_6405,c_97,c_98]) ).
tcf(c_6413,plain,
! [X0: $i,X1: $i,X2: $i] : append(cons(X0,cons(X1,nil)),cons(X2,nil)) = rev(cons(X2,cons(X1,cons(X0,nil)))),
inference(superposition,[status(thm)],[c_6407,c_100]) ).
tcf(c_6415,plain,
! [X0: $i,X1: $i,X2: $i] : rev(cons(X0,cons(X1,cons(X2,nil)))) = cons(X2,cons(X1,cons(X0,nil))),
inference(demodulation,[status(thm)],[c_6413,c_97,c_98]) ).
tcf(c_6488,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : append(cons(X0,cons(X1,cons(X2,nil))),cons(X3,nil)) = rev(cons(X3,cons(X2,cons(X1,cons(X0,nil))))),
inference(superposition,[status(thm)],[c_6415,c_100]) ).
tcf(c_6490,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : rev(cons(X0,cons(X1,cons(X2,cons(X3,nil))))) = cons(X3,cons(X2,cons(X1,cons(X0,nil)))),
inference(demodulation,[status(thm)],[c_6488,c_97,c_98]) ).
tcf(c_6603,plain,
elemNat(iPr_def_12,cons(iPr_def_10,nil)) = orb(bfalse,bfalse),
inference(superposition,[status(thm)],[c_5000,c_4541]) ).
tcf(c_6605,plain,
elemNat(iPr_def_12,cons(iPr_def_10,nil)) = bfalse,
inference(demodulation,[status(thm)],[c_6603,c_85]) ).
tcf(c_6669,plain,
! [X0: $i] : elemNat(s(iPr_def_11),cons(s(iPr_def_10),X0)) = orb(bfalse,elemNat(s(iPr_def_11),X0)),
inference(superposition,[status(thm)],[c_5001,c_4540]) ).
tcf(c_6682,plain,
! [X0: $i] : elemNat(s(iPr_def_11),cons(s(iPr_def_10),X0)) = elemNat(s(iPr_def_11),X0),
inference(demodulation,[status(thm)],[c_6669,c_85]) ).
tcf(c_6683,plain,
! [X0: $i] : elemNat(iPr_def_12,cons(iPr_def_11,X0)) = elemNat(iPr_def_12,X0),
inference(light_normalisation,[status(thm)],[c_6682,c_222,c_223]) ).
tcf(c_6780,plain,
! [X0: $i] : aux(iPr_def_12,cons(iPr_def_11,X0),elemNat(iPr_def_12,X0)) = unique(cons(iPr_def_12,cons(iPr_def_11,X0))),
inference(superposition,[status(thm)],[c_6683,c_96]) ).
tcf(c_8828,plain,
! [X0: $i] : orb(bfalse,elemNat(iPr_def_11,X0)) = elemNat(iPr_def_11,cons(z,X0)),
inference(superposition,[status(thm)],[c_4719,c_94]) ).
tcf(c_8832,plain,
! [X0: $i] : elemNat(iPr_def_11,cons(z,X0)) = elemNat(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_8828,c_85]) ).
tcf(c_9086,plain,
! [X0: $i,X1: $i] : orb(eq(iPr_def_11,X0),elemNat(iPr_def_11,X1)) = elemNat(iPr_def_11,cons(X0,cons(z,X1))),
inference(superposition,[status(thm)],[c_8832,c_94]) ).
tcf(c_9096,plain,
! [X0: $i,X1: $i] : elemNat(iPr_def_11,cons(X0,cons(z,X1))) = elemNat(iPr_def_11,cons(X0,X1)),
inference(demodulation,[status(thm)],[c_9086,c_94]) ).
tcf(c_16712,plain,
! [X0: $i] : orb(bfalse,elemNat(iPr_def_12,X0)) = elemNat(iPr_def_12,cons(z,X0)),
inference(superposition,[status(thm)],[c_4808,c_94]) ).
tcf(c_16716,plain,
! [X0: $i] : elemNat(iPr_def_12,cons(z,X0)) = elemNat(iPr_def_12,X0),
inference(demodulation,[status(thm)],[c_16712,c_85]) ).
tcf(c_16734,plain,
! [X0: $i,X1: $i] : orb(eq(iPr_def_12,X0),elemNat(iPr_def_12,X1)) = elemNat(iPr_def_12,cons(X0,cons(z,X1))),
inference(superposition,[status(thm)],[c_16716,c_94]) ).
tcf(c_16746,plain,
! [X0: $i,X1: $i] : elemNat(iPr_def_12,cons(X0,cons(z,X1))) = elemNat(iPr_def_12,cons(X0,X1)),
inference(demodulation,[status(thm)],[c_16734,c_94]) ).
tcf(c_21349,plain,
! [X0: $i,X1: $i] : aux(iPr_def_11,cons(X0,cons(z,X1)),elemNat(iPr_def_11,cons(X0,X1))) = unique(cons(iPr_def_11,cons(X0,cons(z,X1)))),
inference(superposition,[status(thm)],[c_9096,c_96]) ).
tcf(c_21490,plain,
aux(iPr_def_11,cons(iPr_def_10,cons(z,nil)),bfalse) = unique(cons(iPr_def_11,cons(iPr_def_10,cons(z,nil)))),
inference(superposition,[status(thm)],[c_6151,c_21349]) ).
tcf(c_21505,plain,
unique(cons(iPr_def_11,cons(iPr_def_10,cons(z,nil)))) = unique(cons(iPr_def_10,cons(z,nil))),
inference(demodulation,[status(thm)],[c_21490,c_83]) ).
tcf(c_21506,plain,
unique(cons(iPr_def_11,cons(iPr_def_10,cons(z,nil)))) = btrue,
inference(light_normalisation,[status(thm)],[c_21505,c_4753]) ).
tcf(c_30046,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : eq2(impl(eq2(sorted(cons(X0,cons(X1,cons(X2,cons(X3,nil))))),btrue),impl(eq2(unique(cons(X3,cons(X2,cons(X1,cons(X0,nil))))),btrue),bfalse)),bfalse) != btrue,
inference(light_normalisation,[status(thm)],[c_4830,c_106,c_4827,c_6490]) ).
tcf(c_36769,plain,
! [X0: $i,X1: $i] : aux(iPr_def_12,cons(iPr_def_11,cons(X0,cons(z,X1))),elemNat(iPr_def_12,cons(X0,X1))) = unique(cons(iPr_def_12,cons(iPr_def_11,cons(X0,cons(z,X1))))),
inference(superposition,[status(thm)],[c_16746,c_6780]) ).
tcf(c_37368,plain,
aux(iPr_def_12,cons(iPr_def_11,cons(iPr_def_10,cons(z,nil))),bfalse) = unique(cons(iPr_def_12,cons(iPr_def_11,cons(iPr_def_10,cons(z,nil))))),
inference(superposition,[status(thm)],[c_6605,c_36769]) ).
tcf(c_37384,plain,
unique(cons(iPr_def_12,cons(iPr_def_11,cons(iPr_def_10,cons(z,nil))))) = unique(cons(iPr_def_11,cons(iPr_def_10,cons(z,nil)))),
inference(demodulation,[status(thm)],[c_37368,c_83]) ).
tcf(c_37385,plain,
unique(cons(iPr_def_12,cons(iPr_def_11,cons(iPr_def_10,cons(z,nil))))) = btrue,
inference(light_normalisation,[status(thm)],[c_37384,c_21506]) ).
tcf(c_42198,plain,
eq2(impl(eq2(sorted(cons(z,cons(iPr_def_10,cons(iPr_def_11,cons(iPr_def_12,nil))))),btrue),impl(eq2(btrue,btrue),bfalse)),bfalse) != btrue,
inference(superposition,[status(thm)],[c_37385,c_30046]) ).
tcf(c_42199,plain,
$false,
inference(ground_joinability,[status(thm)],[c_42198,c_91,c_104,c_112,c_4743,c_4785,c_4465]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX203-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n017.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 23:32:46 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.40 Running UEQ theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 35.06/5.31 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 35.06/5.31 % SZS status Started for theBenchmark.p
% 35.06/5.31 % SZS status Unsatisfiable for theBenchmark.p
% 35.06/5.31
% 35.06/5.31 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 35.06/5.31
% 35.06/5.31 % ------ iProver source info
% 35.06/5.31
% 35.06/5.31 % git: date: 2026-07-19 20:42:38 +0200
% 35.06/5.31 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 35.06/5.31 % git: non_committed_changes: false
% 35.06/5.31
% 35.06/5.31 % ------ Parsing...% successful
% 35.06/5.31
% 35.06/5.31
% 35.06/5.31 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 35.06/5.31
% 35.06/5.31 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 35.06/5.31
% 35.06/5.31 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 35.06/5.31
% 35.06/5.31 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 35.06/5.31 % ------ Proving...
% 35.06/5.31 % ------ Problem Properties
% 35.06/5.31
% 35.06/5.31 %
% 35.06/5.31 % clauses 35
% 35.06/5.31 % conjectures 1
% 35.06/5.31 % EPR 0
% 35.06/5.31 % Horn 35
% 35.06/5.31 % unary 35
% 35.06/5.31 % binary 0
% 35.06/5.31 % lits 35
% 35.06/5.31 % lits eq 35
% 35.06/5.31 % fd_pure 0
% 35.06/5.31 % fd_pseudo 0
% 35.06/5.31 % fd_cond 0
% 35.06/5.31 % fd_pseudo_cond 0
% 35.06/5.31 % AC symbols 0
% 35.06/5.31
% 35.06/5.31 % ------ Input Options Time Limit: Unbounded
% 35.06/5.31
% 35.06/5.31
% 35.06/5.31 % ------
% 35.06/5.31 % Current options:
% 35.06/5.31 % ------
% 35.06/5.31
% 35.06/5.31
% 35.06/5.31 %
% 35.06/5.31
% 35.06/5.31 % ------ Proving...
% 35.06/5.31 %
% 35.06/5.31
% 35.06/5.31 % SZS status Unsatisfiable for theBenchmark.p
% 35.06/5.31
% 35.06/5.31 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 35.06/5.32
% 35.06/5.32
%------------------------------------------------------------------------------