%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX191-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 : n019.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:17 AM UTC 2026
% Result : Unsatisfiable 23.26s 8.38s
% Output : CNFRefutation 23.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 30
% Syntax : Number of formulae : 117 ( 111 unt; 0 def)
% Number of atoms : 123 ( 122 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 39 ( 33 ~; 6 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 4 con; 0-3 aty)
% Number of variables : 188 ( 9 sgn 55 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_003,axiom,
! [VAR_0,VAR_1,VAR_2] : aux(y(VAR_0,VAR_1),VAR_2,bfalse) = x(opt(y(VAR_0,VAR_1)),opt(VAR_2)),
file('theBenchmark.p',axiom_003) ).
cnf(c_4,plain,
aux(y(A,B),C,bfalse) = x(opt(y(A,B)),opt(C)),
inference(clausify,[status(thm)],[axiom_003]) ).
fof(axiom_005,axiom,
! [VAR_0,VAR_1] : fail2(VAR_0,VAR_1) = aux(VAR_0,VAR_1,eq2(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_005) ).
cnf(c_6,plain,
fail2(A,B) = aux(A,B,eq2(A,B)),
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_011,axiom,
! [VAR_0,VAR_1,VAR_2] : fail1(y(VAR_0,VAR_1),VAR_2) = fail2(y(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',axiom_011) ).
cnf(c_17,plain,
fail1(y(A,B),C) = fail2(y(A,B),C),
inference(clausify,[status(thm)],[axiom_011]) ).
cnf(c_7047,plain,
fail1(y(A,B),C) = aux(y(A,B),C,eq2(y(A,B),C)),
inference(paramod,[status(thm)],[c_6,c_17]) ).
cnf(c_18,plain,
aux(y(A,B),C,eq2(y(A,B),C)) = fail1(y(A,B),C),
inference(copy,[status(thm)],[c_7047]) ).
fof(axiom_016,axiom,
! [VAR_0,VAR_1,VAR_2] : fail(VAR_0,y(VAR_1,VAR_2)) = fail1(VAR_0,y(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_016) ).
cnf(c_24,plain,
fail(A,y(B,C)) = fail1(A,y(B,C)),
inference(clausify,[status(thm)],[axiom_016]) ).
fof(axiom_018,axiom,
! [VAR_0,VAR_1] : fail4(VAR_0,VAR_1) = y(opt(VAR_0),opt(VAR_1)),
file('theBenchmark.p',axiom_018) ).
cnf(c_26,plain,
fail4(A,B) = y(opt(A),opt(B)),
inference(clausify,[status(thm)],[axiom_018]) ).
fof(axiom_025,axiom,
! [VAR_0] : fail32(x2,VAR_0) = fail4(x2,VAR_0),
file('theBenchmark.p',axiom_025) ).
cnf(c_38,plain,
fail32(x2,A) = fail4(x2,A),
inference(clausify,[status(thm)],[axiom_025]) ).
cnf(c_39,plain,
fail32(x2,A) = y(opt(x2),opt(A)),
inference(paramod,[status(thm)],[c_26,c_38]) ).
fof(axiom_027,axiom,
! [VAR_0] : fail22(VAR_0,n(s(z))) = VAR_0,
file('theBenchmark.p',axiom_027) ).
cnf(c_41,plain,
fail22(A,n(s(z))) = A,
inference(clausify,[status(thm)],[axiom_027]) ).
fof(axiom_029,axiom,
! [VAR_0,VAR_1,VAR_2] : fail22(VAR_0,x(VAR_1,VAR_2)) = fail32(VAR_0,x(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_029) ).
cnf(c_43,plain,
fail22(A,x(B,C)) = fail32(A,x(B,C)),
inference(clausify,[status(thm)],[axiom_029]) ).
fof(axiom_033,axiom,
! [VAR_0] : fail12(n(s(z)),VAR_0) = VAR_0,
file('theBenchmark.p',axiom_033) ).
cnf(c_47,plain,
fail12(n(s(z)),A) = A,
inference(clausify,[status(thm)],[axiom_033]) ).
fof(axiom_037,axiom,
! [VAR_0] : fail12(x2,VAR_0) = fail22(x2,VAR_0),
file('theBenchmark.p',axiom_037) ).
cnf(c_51,plain,
fail12(x2,A) = fail22(x2,A),
inference(clausify,[status(thm)],[axiom_037]) ).
fof(axiom_038,axiom,
! [VAR_0,VAR_1] : fail3(VAR_0,n(s(VAR_1))) = fail12(VAR_0,n(s(VAR_1))),
file('theBenchmark.p',axiom_038) ).
cnf(c_52,plain,
fail3(A,n(s(B))) = fail12(A,n(s(B))),
inference(clausify,[status(thm)],[axiom_038]) ).
fof(axiom_040,axiom,
! [VAR_0,VAR_1,VAR_2] : fail3(VAR_0,x(VAR_1,VAR_2)) = fail12(VAR_0,x(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_040) ).
cnf(c_54,plain,
fail3(A,x(B,C)) = fail12(A,x(B,C)),
inference(clausify,[status(thm)],[axiom_040]) ).
fof(axiom_041,axiom,
! [VAR_0,VAR_1,VAR_2] : fail3(VAR_0,y(VAR_1,VAR_2)) = fail12(VAR_0,y(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_041) ).
cnf(c_55,plain,
fail3(A,y(B,C)) = fail12(A,y(B,C)),
inference(clausify,[status(thm)],[axiom_041]) ).
fof(axiom_042,axiom,
! [VAR_0] : fail3(VAR_0,x2) = fail12(VAR_0,x2),
file('theBenchmark.p',axiom_042) ).
cnf(c_56,plain,
fail3(A,x2) = fail12(A,x2),
inference(clausify,[status(thm)],[axiom_042]) ).
fof(axiom_043,axiom,
! [VAR_0] : impl(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_043) ).
cnf(c_57,plain,
impl(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_043]) ).
fof(axiom_047,axiom,
! [VAR_0,VAR_1] : d(y(VAR_0,VAR_1)) = x(y(d(VAR_0),VAR_1),y(VAR_0,d(VAR_1))),
file('theBenchmark.p',axiom_047) ).
cnf(c_61,plain,
d(y(A,B)) = x(y(d(A),B),y(A,d(B))),
inference(clausify,[status(thm)],[axiom_047]) ).
fof(axiom_048,axiom,
d(x2) = n(s(z)),
file('theBenchmark.p',axiom_048) ).
cnf(c_62,plain,
d(x2) = n(s(z)),
inference(clausify,[status(thm)],[axiom_048]) ).
fof(axiom_056,axiom,
! [VAR_0,VAR_1,VAR_2] : opt(x(y(VAR_0,VAR_1),VAR_2)) = fail(y(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',axiom_056) ).
cnf(c_72,plain,
opt(x(y(A,B),C)) = fail(y(A,B),C),
inference(clausify,[status(thm)],[axiom_056]) ).
cnf(c_73,plain,
fail(y(A,B),C) = opt(x(y(A,B),C)),
inference(copy,[status(thm)],[c_72]) ).
fof(axiom_058,axiom,
! [VAR_0,VAR_1] : opt(y(n(s(VAR_0)),VAR_1)) = fail3(n(s(VAR_0)),VAR_1),
file('theBenchmark.p',axiom_058) ).
cnf(c_76,plain,
opt(y(n(s(A)),B)) = fail3(n(s(A)),B),
inference(clausify,[status(thm)],[axiom_058]) ).
cnf(c_77,plain,
fail3(n(s(A)),B) = opt(y(n(s(A)),B)),
inference(copy,[status(thm)],[c_76]) ).
fof(axiom_062,axiom,
! [VAR_0] : opt(y(x2,VAR_0)) = fail3(x2,VAR_0),
file('theBenchmark.p',axiom_062) ).
cnf(c_83,plain,
opt(y(x2,A)) = fail3(x2,A),
inference(clausify,[status(thm)],[axiom_062]) ).
cnf(c_84,plain,
fail3(x2,A) = opt(y(x2,A)),
inference(copy,[status(thm)],[c_83]) ).
fof(axiom_064,axiom,
opt(x2) = x2,
file('theBenchmark.p',axiom_064) ).
cnf(c_86,plain,
opt(x2) = x2,
inference(clausify,[status(thm)],[axiom_064]) ).
fof(axiom_065,axiom,
! [VAR_0] : propm4(VAR_0) = impl(eq2(opt(d(VAR_0)),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),eq3(btrue,bfalse)),
file('theBenchmark.p',axiom_065) ).
cnf(c_87,plain,
propm4(A) = impl(eq2(opt(d(A)),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),eq3(btrue,bfalse)),
inference(clausify,[status(thm)],[axiom_065]) ).
fof(axiom_067,axiom,
eq3(btrue,bfalse) = bfalse,
file('theBenchmark.p',axiom_067) ).
cnf(c_89,plain,
eq3(btrue,bfalse) = bfalse,
inference(clausify,[status(thm)],[axiom_067]) ).
fof(axiom_070,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( eq2(x(VAR_0,VAR_2),x(VAR_1,VAR_3)) = eq2(VAR_2,VAR_3)
| eq2(VAR_0,VAR_1) != btrue ),
file('theBenchmark.p',axiom_070) ).
cnf(c_93,plain,
( eq2(x(A,C),x(B,D)) = eq2(C,D)
| eq2(A,B) != btrue ),
inference(clausify,[status(thm)],[axiom_070]) ).
fof(axiom_071,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( eq2(y(VAR_0,VAR_2),y(VAR_1,VAR_3)) = bfalse
| eq2(VAR_0,VAR_1) != bfalse ),
file('theBenchmark.p',axiom_071) ).
cnf(c_94,plain,
( eq2(y(A,C),y(B,D)) = bfalse
| eq2(A,B) != bfalse ),
inference(clausify,[status(thm)],[axiom_071]) ).
fof(axiom_072,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( eq2(y(VAR_0,VAR_2),y(VAR_1,VAR_3)) = eq2(VAR_2,VAR_3)
| eq2(VAR_0,VAR_1) != btrue ),
file('theBenchmark.p',axiom_072) ).
cnf(c_95,plain,
( eq2(y(A,C),y(B,D)) = eq2(C,D)
| eq2(A,B) != btrue ),
inference(clausify,[status(thm)],[axiom_072]) ).
fof(axiom_075,axiom,
! [VAR_0] : eq2(n(VAR_0),x2) = bfalse,
file('theBenchmark.p',axiom_075) ).
cnf(c_98,plain,
eq2(n(A),x2) = bfalse,
inference(clausify,[status(thm)],[axiom_075]) ).
fof(axiom_089,axiom,
! [VAR_0] : eq2(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_089) ).
cnf(c_116,plain,
eq2(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_089]) ).
fof(axiom_090,axiom,
! [VAR_0] : eq3(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_090) ).
cnf(c_117,plain,
eq3(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_090]) ).
fof(goal,axiom,
! [VAR_0] : eq3(propm4(VAR_0),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_118,plain,
eq3(propm4(A),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_7048,plain,
eq3(impl(eq2(opt(d(A)),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),eq3(btrue,bfalse)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_87,c_118]) ).
cnf(c_119,plain,
eq3(impl(eq2(opt(d(A)),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_89,c_7048]) ).
cnf(c_124,plain,
fail32(x2,A) = y(x2,opt(A)),
inference(paramod,[status(thm)],[c_86,c_39]) ).
cnf(c_7049,plain,
opt(x(y(A,B),y(C,D))) = fail1(y(A,B),y(C,D)),
inference(paramod,[status(thm)],[c_73,c_24]) ).
cnf(c_149,plain,
fail1(y(A,B),y(C,D)) = opt(x(y(A,B),y(C,D))),
inference(copy,[status(thm)],[c_7049]) ).
cnf(c_7050,plain,
opt(y(n(s(A)),y(B,C))) = fail12(n(s(A)),y(B,C)),
inference(paramod,[status(thm)],[c_77,c_55]) ).
cnf(c_159,plain,
fail12(n(s(A)),y(B,C)) = opt(y(n(s(A)),y(B,C))),
inference(copy,[status(thm)],[c_7050]) ).
cnf(c_7051,plain,
opt(y(n(s(A)),x2)) = fail12(n(s(A)),x2),
inference(paramod,[status(thm)],[c_77,c_56]) ).
cnf(c_160,plain,
fail12(n(s(A)),x2) = opt(y(n(s(A)),x2)),
inference(copy,[status(thm)],[c_7051]) ).
cnf(c_7052,plain,
opt(y(x2,n(s(A)))) = fail12(x2,n(s(A))),
inference(paramod,[status(thm)],[c_84,c_52]) ).
cnf(c_7053,plain,
opt(y(x2,n(s(A)))) = fail22(x2,n(s(A))),
inference(paramod,[status(thm)],[c_51,c_7052]) ).
cnf(c_171,plain,
fail22(x2,n(s(A))) = opt(y(x2,n(s(A)))),
inference(copy,[status(thm)],[c_7053]) ).
cnf(c_7054,plain,
opt(y(x2,x(A,B))) = fail12(x2,x(A,B)),
inference(paramod,[status(thm)],[c_84,c_54]) ).
cnf(c_7055,plain,
opt(y(x2,x(A,B))) = fail22(x2,x(A,B)),
inference(paramod,[status(thm)],[c_51,c_7054]) ).
cnf(c_7056,plain,
opt(y(x2,x(A,B))) = fail32(x2,x(A,B)),
inference(paramod,[status(thm)],[c_43,c_7055]) ).
cnf(c_173,plain,
opt(y(x2,x(A,B))) = y(x2,opt(x(A,B))),
inference(paramod,[status(thm)],[c_124,c_7056]) ).
cnf(c_187,plain,
eq2(y(n(A),B),y(x2,C)) = bfalse,
inference(resolve,[status(thm)],[c_94,c_98]) ).
cnf(c_243,plain,
eq2(y(A,B),y(A,C)) = eq2(B,C),
inference(resolve,[status(thm)],[c_95,c_116]) ).
cnf(c_244,plain,
eq2(x(A,B),x(A,C)) = eq2(B,C),
inference(resolve,[status(thm)],[c_93,c_116]) ).
cnf(c_249,plain,
impl(eq2(A,A),B) = B,
inference(paramod,[status(thm)],[c_116,c_57]) ).
cnf(c_257,plain,
eq3(impl(eq2(opt(x(y(d(A),B),y(A,d(B)))),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_119]) ).
cnf(c_7057,plain,
aux(y(n(A),B),y(x2,C),bfalse) = fail1(y(n(A),B),y(x2,C)),
inference(paramod,[status(thm)],[c_187,c_18]) ).
cnf(c_7058,plain,
x(opt(y(n(A),B)),opt(y(x2,C))) = fail1(y(n(A),B),y(x2,C)),
inference(paramod,[status(thm)],[c_4,c_7057]) ).
cnf(c_7059,plain,
x(opt(y(n(A),B)),opt(y(x2,C))) = opt(x(y(n(A),B),y(x2,C))),
inference(paramod,[status(thm)],[c_149,c_7058]) ).
cnf(c_379,plain,
opt(x(y(n(A),B),y(x2,C))) = x(opt(y(n(A),B)),opt(y(x2,C))),
inference(copy,[status(thm)],[c_7059]) ).
cnf(c_458,plain,
opt(y(n(s(z)),y(A,B))) = y(A,B),
inference(paramod,[status(thm)],[c_159,c_47]) ).
cnf(c_461,plain,
opt(y(n(s(z)),x2)) = x2,
inference(paramod,[status(thm)],[c_160,c_47]) ).
cnf(c_7060,plain,
eq3(impl(eq2(opt(x(y(n(s(z)),A),y(x2,d(A)))),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_257]) ).
cnf(c_467,plain,
eq3(impl(eq2(x(opt(y(n(s(z)),A)),opt(y(x2,d(A)))),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_379,c_7060]) ).
cnf(c_7061,plain,
eq3(impl(eq2(x(opt(y(n(s(z)),y(A,B))),opt(y(x2,x(y(d(A),B),y(A,d(B)))))),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_467]) ).
cnf(c_7062,plain,
eq3(impl(eq2(x(y(A,B),opt(y(x2,x(y(d(A),B),y(A,d(B)))))),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_458,c_7061]) ).
cnf(c_560,plain,
eq3(impl(eq2(x(y(A,B),y(x2,opt(x(y(d(A),B),y(A,d(B)))))),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_173,c_7062]) ).
cnf(c_588,plain,
opt(y(x2,n(s(z)))) = x2,
inference(paramod,[status(thm)],[c_171,c_41]) ).
cnf(c_7063,plain,
eq3(impl(eq2(y(x2,opt(x(y(d(x2),y(x2,x2)),y(x2,d(y(x2,x2)))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_244,c_560]) ).
cnf(c_7064,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,x2)),y(x2,d(y(x2,x2)))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_7063]) ).
cnf(c_7065,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,x2)),y(x2,x(y(d(x2),x2),y(x2,d(x2))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_7064]) ).
cnf(c_7066,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,x2)),y(x2,x(y(n(s(z)),x2),y(x2,d(x2))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_7065]) ).
cnf(c_7067,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,x2)),y(x2,x(y(n(s(z)),x2),y(x2,n(s(z)))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_7066]) ).
cnf(c_7068,plain,
eq3(impl(eq2(y(x2,x(opt(y(n(s(z)),y(x2,x2))),opt(y(x2,x(y(n(s(z)),x2),y(x2,n(s(z)))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_379,c_7067]) ).
cnf(c_7069,plain,
eq3(impl(eq2(y(x2,x(y(x2,x2),opt(y(x2,x(y(n(s(z)),x2),y(x2,n(s(z)))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_458,c_7068]) ).
cnf(c_7070,plain,
eq3(impl(eq2(y(x2,x(y(x2,x2),y(x2,opt(x(y(n(s(z)),x2),y(x2,n(s(z)))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_173,c_7069]) ).
cnf(c_7071,plain,
eq3(impl(eq2(y(x2,x(y(x2,x2),y(x2,x(opt(y(n(s(z)),x2)),opt(y(x2,n(s(z)))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_379,c_7070]) ).
cnf(c_7072,plain,
eq3(impl(eq2(y(x2,x(y(x2,x2),y(x2,x(x2,opt(y(x2,n(s(z)))))))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_461,c_7071]) ).
cnf(c_7073,plain,
eq3(impl(eq2(y(x2,x(y(x2,x2),y(x2,x(x2,x2)))),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_588,c_7072]) ).
cnf(c_7074,plain,
eq3(impl(eq2(x(y(x2,x2),y(x2,x(x2,x2))),x(y(x2,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_243,c_7073]) ).
cnf(c_7075,plain,
eq3(impl(eq2(y(x2,x(x2,x2)),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_244,c_7074]) ).
cnf(c_7076,plain,
eq3(impl(eq2(x(x2,x2),x(x2,x2)),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_243,c_7075]) ).
cnf(c_7077,plain,
eq3(impl(eq2(x2,x2),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_244,c_7076]) ).
cnf(c_7078,plain,
eq3(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_249,c_7077]) ).
cnf(c_7079,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_117,c_7078]) ).
cnf(c_7046,plain,
$false,
inference(copy,[status(thm)],[c_7079]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX191-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.11/5.37 % Computer : n019.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sat Sep 26 16:53:55 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.38 % Process 1777958 was started by sandbox on n019,
% 0.11/5.38 % Sat Sep 26 16:53:55 2026
% 0.11/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/5.38
% 0.11/5.38 % From the command line: assign(max_seconds, 300).
% 23.26/8.38
% 23.26/8.38 % given #500 (F,wt=90): 1932 eq3(impl(eq2(x(y(d(A),x(n(B),x2)),y(A,x(n(z),n(s(z))))),x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),bfalse),bfalse) != btrue. [para(62(a,1),833(a,1,1,1,1,2,2,2))].
% 23.26/8.38
% 23.26/8.38 % SZS status Unsatisfiable for theBenchmark
% 23.26/8.38
% 23.26/8.38 % Proof 1 at 2.52 (+ 0.44) seconds.
% 23.26/8.38 % Length of proof is 54.
% 23.26/8.38 % Level of proof is 6.
% 23.26/8.38 % Maximum clause weight is 95.000.
% 23.26/8.38 % Given clauses 873.
% 23.26/8.38
% 23.26/8.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------