%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX189-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 : n011.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:16 AM UTC 2026
% Result : Unsatisfiable 51.07s 7.85s
% Output : CNFRefutation 51.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 30
% Syntax : Number of formulae : 110 ( 104 unt; 0 def)
% Number of atoms : 116 ( 115 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 32 ( 26 ~; 6 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 10 ( 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_14107,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_14107]) ).
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] : prop2(VAR_0) = impl(eq2(opt(d(VAR_0)),x(y(x2,x2),y(x2,x(x2,x2)))),eq3(btrue,bfalse)),
file('theBenchmark.p',axiom_065) ).
cnf(c_87,plain,
prop2(A) = impl(eq2(opt(d(A)),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(prop2(VAR_0),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_118,plain,
eq3(prop2(A),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_14108,plain,
eq3(impl(eq2(opt(d(A)),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,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_89,c_14108]) ).
cnf(c_124,plain,
fail32(x2,A) = y(x2,opt(A)),
inference(paramod,[status(thm)],[c_86,c_39]) ).
cnf(c_14109,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_14109]) ).
cnf(c_14110,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_14110]) ).
cnf(c_14111,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_14111]) ).
cnf(c_14112,plain,
opt(y(x2,n(s(A)))) = fail12(x2,n(s(A))),
inference(paramod,[status(thm)],[c_84,c_52]) ).
cnf(c_14113,plain,
opt(y(x2,n(s(A)))) = fail22(x2,n(s(A))),
inference(paramod,[status(thm)],[c_51,c_14112]) ).
cnf(c_171,plain,
fail22(x2,n(s(A))) = opt(y(x2,n(s(A)))),
inference(copy,[status(thm)],[c_14113]) ).
cnf(c_14114,plain,
opt(y(x2,x(A,B))) = fail12(x2,x(A,B)),
inference(paramod,[status(thm)],[c_84,c_54]) ).
cnf(c_14115,plain,
opt(y(x2,x(A,B))) = fail22(x2,x(A,B)),
inference(paramod,[status(thm)],[c_51,c_14114]) ).
cnf(c_14116,plain,
opt(y(x2,x(A,B))) = fail32(x2,x(A,B)),
inference(paramod,[status(thm)],[c_43,c_14115]) ).
cnf(c_173,plain,
opt(y(x2,x(A,B))) = y(x2,opt(x(A,B))),
inference(paramod,[status(thm)],[c_124,c_14116]) ).
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,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_119]) ).
cnf(c_14117,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_14118,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_14117]) ).
cnf(c_14119,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_14118]) ).
cnf(c_388,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_14119]) ).
cnf(c_469,plain,
opt(y(n(s(z)),y(A,B))) = y(A,B),
inference(paramod,[status(thm)],[c_159,c_47]) ).
cnf(c_472,plain,
opt(y(n(s(z)),x2)) = x2,
inference(paramod,[status(thm)],[c_160,c_47]) ).
cnf(c_14120,plain,
eq3(impl(eq2(opt(x(y(n(s(z)),A),y(x2,d(A)))),x(y(x2,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_257]) ).
cnf(c_532,plain,
eq3(impl(eq2(x(opt(y(n(s(z)),A)),opt(y(x2,d(A)))),x(y(x2,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_388,c_14120]) ).
cnf(c_612,plain,
opt(y(x2,n(s(z)))) = x2,
inference(paramod,[status(thm)],[c_171,c_41]) ).
cnf(c_14121,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,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_532]) ).
cnf(c_14122,plain,
eq3(impl(eq2(x(y(A,B),opt(y(x2,x(y(d(A),B),y(A,d(B)))))),x(y(x2,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_469,c_14121]) ).
cnf(c_1895,plain,
eq3(impl(eq2(x(y(A,B),y(x2,opt(x(y(d(A),B),y(A,d(B)))))),x(y(x2,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_173,c_14122]) ).
cnf(c_14123,plain,
eq3(impl(eq2(y(x2,opt(x(y(d(x2),x2),y(x2,d(x2))))),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_244,c_1895]) ).
cnf(c_14124,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),x2),y(x2,d(x2))))),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_14123]) ).
cnf(c_14125,plain,
eq3(impl(eq2(y(x2,opt(x(y(n(s(z)),x2),y(x2,n(s(z)))))),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_62,c_14124]) ).
cnf(c_14126,plain,
eq3(impl(eq2(y(x2,x(opt(y(n(s(z)),x2)),opt(y(x2,n(s(z)))))),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_388,c_14125]) ).
cnf(c_14127,plain,
eq3(impl(eq2(y(x2,x(x2,opt(y(x2,n(s(z)))))),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_472,c_14126]) ).
cnf(c_14128,plain,
eq3(impl(eq2(y(x2,x(x2,x2)),y(x2,x(x2,x2))),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_612,c_14127]) ).
cnf(c_14129,plain,
eq3(impl(eq2(x(x2,x2),x(x2,x2)),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_243,c_14128]) ).
cnf(c_14130,plain,
eq3(impl(eq2(x2,x2),bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_244,c_14129]) ).
cnf(c_14131,plain,
eq3(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_249,c_14130]) ).
cnf(c_14132,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_117,c_14131]) ).
cnf(c_14106,plain,
$false,
inference(copy,[status(thm)],[c_14132]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX189-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.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 16:54:00 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1086427 was started by sandbox2 on n011,
% 0.10/0.37 % Sat Sep 26 16:54:00 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 51.07/7.85
% 51.07/7.85 % given #500 (F,wt=77): 599 eq3(impl(eq2(opt(x(y(n(z),A),y(fail1(n(B),n(C)),d(A)))),x(y(x2,x2),y(x2,x(x2,x2)))),bfalse),bfalse) != eq2(D,D). [para(130(a,1),292(a,1,1,1,1,1,1,1))].
% 51.07/7.85
% 51.07/7.85 % given #1000 (W,wt=46): 881 eq2(x(y(y(A,B),C),D),x(y(n(E),F),V6)) = bfalse. [hyper(92,a,205,a)].
% 51.07/7.85
% 51.07/7.85 % SZS status Unsatisfiable for theBenchmark
% 51.07/7.85
% 51.07/7.85 % Proof 1 at 6.10 (+ 1.08) seconds.
% 51.07/7.85 % Length of proof is 54.
% 51.07/7.85 % Level of proof is 6.
% 51.07/7.85 % Maximum clause weight is 82.000.
% 51.07/7.85 % Given clauses 1254.
% 51.07/7.85
% 51.07/7.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------