%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX192-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 : n008.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 70.50s 10.41s
% Output : CNFRefutation 70.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 30
% Syntax : Number of formulae : 124 ( 118 unt; 0 def)
% Number of atoms : 130 ( 129 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 46 ( 40 ~; 6 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 14 ( 3 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_5349,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_5349]) ).
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] : propm5(VAR_0) = impl(eq2(opt(d(VAR_0)),x(y(x2,y(x2,y(x2,x2))),y(x2,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,
propm5(A) = impl(eq2(opt(d(A)),x(y(x2,y(x2,y(x2,x2))),y(x2,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(propm5(VAR_0),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_118,plain,
eq3(propm5(A),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_5350,plain,
eq3(impl(eq2(opt(d(A)),x(y(x2,y(x2,y(x2,x2))),y(x2,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,y(x2,x2))),y(x2,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_5350]) ).
cnf(c_124,plain,
fail32(x2,A) = y(x2,opt(A)),
inference(paramod,[status(thm)],[c_86,c_39]) ).
cnf(c_5351,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_5351]) ).
cnf(c_5352,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_5352]) ).
cnf(c_5353,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_5353]) ).
cnf(c_5354,plain,
opt(y(x2,n(s(A)))) = fail12(x2,n(s(A))),
inference(paramod,[status(thm)],[c_84,c_52]) ).
cnf(c_5355,plain,
opt(y(x2,n(s(A)))) = fail22(x2,n(s(A))),
inference(paramod,[status(thm)],[c_51,c_5354]) ).
cnf(c_171,plain,
fail22(x2,n(s(A))) = opt(y(x2,n(s(A)))),
inference(copy,[status(thm)],[c_5355]) ).
cnf(c_5356,plain,
opt(y(x2,x(A,B))) = fail12(x2,x(A,B)),
inference(paramod,[status(thm)],[c_84,c_54]) ).
cnf(c_5357,plain,
opt(y(x2,x(A,B))) = fail22(x2,x(A,B)),
inference(paramod,[status(thm)],[c_51,c_5356]) ).
cnf(c_5358,plain,
opt(y(x2,x(A,B))) = fail32(x2,x(A,B)),
inference(paramod,[status(thm)],[c_43,c_5357]) ).
cnf(c_173,plain,
opt(y(x2,x(A,B))) = y(x2,opt(x(A,B))),
inference(paramod,[status(thm)],[c_124,c_5358]) ).
cnf(c_186,plain,
eq2(y(n(A),B),y(x2,C)) = bfalse,
inference(resolve,[status(thm)],[c_98,c_94]) ).
cnf(c_238,plain,
eq2(y(A,B),y(A,C)) = eq2(B,C),
inference(resolve,[status(thm)],[c_116,c_95]) ).
cnf(c_239,plain,
eq2(x(A,B),x(A,C)) = eq2(B,C),
inference(resolve,[status(thm)],[c_116,c_93]) ).
cnf(c_244,plain,
impl(eq2(A,A),B) = B,
inference(paramod,[status(thm)],[c_116,c_57]) ).
cnf(c_250,plain,
eq3(impl(eq2(opt(x(y(d(A),B),y(A,d(B)))),x(y(x2,y(x2,y(x2,x2))),y(x2,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_5359,plain,
aux(y(n(A),B),y(x2,C),bfalse) = fail1(y(n(A),B),y(x2,C)),
inference(paramod,[status(thm)],[c_186,c_18]) ).
cnf(c_5360,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_5359]) ).
cnf(c_5361,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_5360]) ).
cnf(c_364,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_5361]) ).
cnf(c_418,plain,
opt(y(n(s(z)),y(A,B))) = y(A,B),
inference(paramod,[status(thm)],[c_159,c_47]) ).
cnf(c_5362,plain,
eq3(impl(eq2(opt(x(y(n(s(z)),A),y(x2,d(A)))),x(y(x2,y(x2,y(x2,x2))),y(x2,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_250]) ).
cnf(c_428,plain,
eq3(impl(eq2(x(opt(y(n(s(z)),A)),opt(y(x2,d(A)))),x(y(x2,y(x2,y(x2,x2))),y(x2,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_364,c_5362]) ).
cnf(c_478,plain,
opt(y(n(s(z)),x2)) = x2,
inference(paramod,[status(thm)],[c_160,c_47]) ).
cnf(c_587,plain,
opt(y(x2,n(s(z)))) = x2,
inference(paramod,[status(thm)],[c_171,c_41]) ).
cnf(c_5363,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,y(x2,x2))),y(x2,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_428]) ).
cnf(c_5364,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,y(x2,x2))),y(x2,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_418,c_5363]) ).
cnf(c_699,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,y(x2,x2))),y(x2,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_5364]) ).
cnf(c_5365,plain,
eq3(impl(eq2(y(x2,opt(x(y(d(x2),y(x2,y(x2,x2))),y(x2,d(y(x2,y(x2,x2))))))),y(x2,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_239,c_699]) ).
cnf(c_5366,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,y(x2,x2))),y(x2,d(y(x2,y(x2,x2))))))),y(x2,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_5365]) ).
cnf(c_5367,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,y(x2,x2))),y(x2,x(y(d(x2),y(x2,x2)),y(x2,d(y(x2,x2)))))))),y(x2,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_5366]) ).
cnf(c_5368,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,y(x2,x2))),y(x2,x(y(n(s(z)),y(x2,x2)),y(x2,d(y(x2,x2)))))))),y(x2,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_5367]) ).
cnf(c_5369,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,y(x2,x2))),y(x2,x(y(n(s(z)),y(x2,x2)),y(x2,x(y(d(x2),x2),y(x2,d(x2))))))))),y(x2,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_5368]) ).
cnf(c_5370,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,y(x2,x2))),y(x2,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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_5369]) ).
cnf(c_5371,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),y(x2,y(x2,x2))),y(x2,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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_5370]) ).
cnf(c_5372,plain,
eq3(impl(eq2(y(x2,x(opt(y(n(s(z)),y(x2,y(x2,x2)))),opt(y(x2,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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_364,c_5371]) ).
cnf(c_5373,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),opt(y(x2,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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_418,c_5372]) ).
cnf(c_5374,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_173,c_5373]) ).
cnf(c_5375,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_364,c_5374]) ).
cnf(c_5376,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_418,c_5375]) ).
cnf(c_5377,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_173,c_5376]) ).
cnf(c_5378,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),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,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_364,c_5377]) ).
cnf(c_5379,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,opt(y(x2,n(s(z)))))))))),y(x2,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_478,c_5378]) ).
cnf(c_5380,plain,
eq3(impl(eq2(y(x2,x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))),y(x2,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_587,c_5379]) ).
cnf(c_5381,plain,
eq3(impl(eq2(x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2))))),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_238,c_5380]) ).
cnf(c_5382,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_239,c_5381]) ).
cnf(c_5383,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_238,c_5382]) ).
cnf(c_5384,plain,
eq3(impl(eq2(y(x2,x(x2,x2)),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_239,c_5383]) ).
cnf(c_5385,plain,
eq3(impl(eq2(x(x2,x2),x(x2,x2)),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_238,c_5384]) ).
cnf(c_5386,plain,
eq3(impl(eq2(x2,x2),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_239,c_5385]) ).
cnf(c_5387,plain,
eq3(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_244,c_5386]) ).
cnf(c_5388,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_117,c_5387]) ).
cnf(c_5348,plain,
$false,
inference(copy,[status(thm)],[c_5388]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX192-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n008.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sat Sep 26 16:54:09 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.38 % Process 4089324 was started by sandbox2 on n008,
% 0.08/0.38 % Sat Sep 26 16:54:09 2026
% 0.08/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.38
% 0.08/0.38 % From the command line: assign(max_seconds, 300).
% 70.50/10.41
% 70.50/10.41 % given #500 (A,wt=34): 374 fail12(n(s(A)),fail1(n(s(B)),n(C))) = opt(y(n(s(A)),fail1(n(s(B)),n(C)))). [para(132(a,1),156(a,1,2)),rewrite([132(12)])].
% 70.50/10.41
% 70.50/10.41 % SZS status Unsatisfiable for theBenchmark
% 70.50/10.41
% 70.50/10.41 % Proof 1 at 1.62 (+ 0.27) seconds.
% 70.50/10.41 % Length of proof is 54.
% 70.50/10.41 % Level of proof is 6.
% 70.50/10.41 % Maximum clause weight is 78.000.
% 70.50/10.41 % Given clauses 624.
% 70.50/10.41
% 70.50/10.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------