%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX242-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 : n007.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:26 AM UTC 2026
% Result : Unsatisfiable 11.01s 2.10s
% Output : CNFRefutation 11.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 24
% Syntax : Number of formulae : 100 ( 95 unt; 0 def)
% Number of atoms : 105 ( 104 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 45 ( 40 ~; 5 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 4 con; 0-8 aty)
% Number of variables : 298 ( 17 sgn 67 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_004,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] : aux3(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,btrue) = unifyloop(VAR_0,append(VAR_3,VAR_1),append(VAR_6,VAR_4)),
file('theBenchmark.p',axiom_004) ).
cnf(c_5,plain,
aux3(A,B,C,D,E,F,V6,btrue) = unifyloop(A,append(D,B),append(V6,E)),
inference(clausify,[status(thm)],[axiom_004]) ).
fof(axiom_008,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : aux5(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,btrue) = unifyloop(VAR_0,VAR_2,VAR_3),
file('theBenchmark.p',axiom_008) ).
cnf(c_10,plain,
aux5(A,B,C,D,E,btrue) = unifyloop(A,C,D),
inference(clausify,[status(thm)],[axiom_008]) ).
fof(axiom_011,axiom,
! [VAR_0,VAR_1,VAR_2] : aux6(VAR_0,VAR_1,just(VAR_2)) = eq3(subst(VAR_2,VAR_0),subst(VAR_2,VAR_1)),
file('theBenchmark.p',axiom_011) ).
cnf(c_13,plain,
aux6(A,B,just(C)) = eq3(subst(C,A),subst(C,B)),
inference(clausify,[status(thm)],[axiom_011]) ).
cnf(c_14,plain,
eq3(subst(A,B),subst(A,C)) = aux6(B,C,just(A)),
inference(copy,[status(thm)],[c_13]) ).
fof(axiom_018,axiom,
! [VAR_0,VAR_1,VAR_2] : subst(VAR_0,app(VAR_1,VAR_2)) = app(VAR_1,substList(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_018) ).
cnf(c_22,plain,
subst(A,app(B,C)) = app(B,substList(A,C)),
inference(clausify,[status(thm)],[axiom_018]) ).
fof(axiom_019,axiom,
! [VAR_0,VAR_1] : subst(VAR_0,var(VAR_1)) = apply1(VAR_0,VAR_1),
file('theBenchmark.p',axiom_019) ).
cnf(c_23,plain,
subst(A,var(B)) = apply1(A,B),
inference(clausify,[status(thm)],[axiom_019]) ).
fof(axiom_020,axiom,
! [VAR_0] : substList(VAR_0,nil) = nil,
file('theBenchmark.p',axiom_020) ).
cnf(c_24,plain,
substList(A,nil) = nil,
inference(clausify,[status(thm)],[axiom_020]) ).
fof(axiom_021,axiom,
! [VAR_0,VAR_1,VAR_2] : substList(VAR_0,cons(VAR_1,VAR_2)) = cons(subst(VAR_0,VAR_1),substList(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_021) ).
cnf(c_25,plain,
substList(A,cons(B,C)) = cons(subst(A,B),substList(A,C)),
inference(clausify,[status(thm)],[axiom_021]) ).
cnf(c_26,plain,
cons(subst(A,B),substList(A,C)) = substList(A,cons(B,C)),
inference(copy,[status(thm)],[c_25]) ).
fof(axiom_031,axiom,
! [VAR_0] : unifyloop(VAR_0,nil,nil) = just(VAR_0),
file('theBenchmark.p',axiom_031) ).
cnf(c_40,plain,
unifyloop(A,nil,nil) = just(A),
inference(clausify,[status(thm)],[axiom_031]) ).
cnf(c_41,plain,
just(A) = unifyloop(A,nil,nil),
inference(copy,[status(thm)],[c_40]) ).
fof(axiom_034,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] : unifyloop(VAR_0,cons(app(VAR_1,VAR_2),VAR_3),cons(app(VAR_4,VAR_5),VAR_6)) = aux3(VAR_0,VAR_3,VAR_1,VAR_2,VAR_6,VAR_4,VAR_5,eq2(VAR_1,VAR_4)),
file('theBenchmark.p',axiom_034) ).
cnf(c_45,plain,
unifyloop(A,cons(app(B,C),D),cons(app(E,F),V6)) = aux3(A,D,B,C,V6,E,F,eq2(B,E)),
inference(clausify,[status(thm)],[axiom_034]) ).
fof(axiom_037,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : unifyloop(VAR_0,cons(var(VAR_1),VAR_2),cons(VAR_3,VAR_4)) = unifyvar(VAR_0,VAR_1,VAR_3,VAR_2,VAR_4),
file('theBenchmark.p',axiom_037) ).
cnf(c_50,plain,
unifyloop(A,cons(var(B),C),cons(D,E)) = unifyvar(A,B,D,C,E),
inference(clausify,[status(thm)],[axiom_037]) ).
fof(axiom_039,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : unifyvar(VAR_0,VAR_1,var(VAR_2),VAR_3,VAR_4) = aux5(VAR_0,VAR_1,VAR_3,VAR_4,VAR_2,eq2(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_039) ).
cnf(c_53,plain,
unifyvar(A,B,var(C),D,E) = aux5(A,B,D,E,C,eq2(B,C)),
inference(clausify,[status(thm)],[axiom_039]) ).
cnf(c_54,plain,
aux5(A,B,C,D,E,eq2(B,E)) = unifyvar(A,B,var(E),C,D),
inference(copy,[status(thm)],[c_53]) ).
fof(axiom_041,axiom,
! [VAR_0,VAR_1] : unify2(VAR_0,VAR_1) = unifyloop(lam3,cons(VAR_0,nil),cons(VAR_1,nil)),
file('theBenchmark.p',axiom_041) ).
cnf(c_57,plain,
unify2(A,B) = unifyloop(lam3,cons(A,nil),cons(B,nil)),
inference(clausify,[status(thm)],[axiom_041]) ).
fof(axiom_042,axiom,
! [VAR_0,VAR_1] : unificationOK(VAR_0,VAR_1) = aux6(VAR_0,VAR_1,unify2(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_042) ).
cnf(c_58,plain,
unificationOK(A,B) = aux6(A,B,unify2(A,B)),
inference(clausify,[status(thm)],[axiom_042]) ).
cnf(c_59,plain,
unificationOK(A,B) = aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))),
inference(paramod,[status(thm)],[c_57,c_58]) ).
fof(axiom_043,axiom,
! [VAR_0,VAR_1] : prop_unify_makes_equal(VAR_0,VAR_1) = eq4(unificationOK(VAR_0,VAR_1),btrue),
file('theBenchmark.p',axiom_043) ).
cnf(c_60,plain,
prop_unify_makes_equal(A,B) = eq4(unificationOK(A,B),btrue),
inference(clausify,[status(thm)],[axiom_043]) ).
cnf(c_61,plain,
prop_unify_makes_equal(A,B) = eq4(aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))),btrue),
inference(paramod,[status(thm)],[c_59,c_60]) ).
fof(axiom_046,axiom,
! [VAR_0] : append(nil,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_046) ).
cnf(c_65,plain,
append(nil,A) = A,
inference(clausify,[status(thm)],[axiom_046]) ).
fof(axiom_047,axiom,
! [VAR_0,VAR_1,VAR_2] : append(cons(VAR_0,VAR_1),VAR_2) = cons(VAR_0,append(VAR_1,VAR_2)),
file('theBenchmark.p',axiom_047) ).
cnf(c_66,plain,
append(cons(A,B),C) = cons(A,append(B,C)),
inference(clausify,[status(thm)],[axiom_047]) ).
fof(axiom_054,axiom,
eq4(bfalse,btrue) = bfalse,
file('theBenchmark.p',axiom_054) ).
cnf(c_73,plain,
eq4(bfalse,btrue) = bfalse,
inference(clausify,[status(thm)],[axiom_054]) ).
fof(axiom_056,axiom,
! [VAR_0] : eq2(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_056) ).
cnf(c_75,plain,
eq2(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_056]) ).
fof(axiom_058,axiom,
! [VAR_0] : eq4(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_058) ).
cnf(c_77,plain,
eq4(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_058]) ).
fof(axiom_060,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( eq(cons(VAR_0,VAR_2),cons(VAR_1,VAR_3)) = bfalse
| eq3(VAR_0,VAR_1) != bfalse ),
file('theBenchmark.p',axiom_060) ).
cnf(c_79,plain,
( eq(cons(A,C),cons(B,D)) = bfalse
| eq3(A,B) != bfalse ),
inference(clausify,[status(thm)],[axiom_060]) ).
fof(axiom_062,axiom,
! [VAR_0,VAR_1] : eq(nil,cons(VAR_0,VAR_1)) = bfalse,
file('theBenchmark.p',axiom_062) ).
cnf(c_81,plain,
eq(nil,cons(A,B)) = bfalse,
inference(clausify,[status(thm)],[axiom_062]) ).
fof(axiom_065,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( eq3(app(VAR_0,VAR_2),app(VAR_1,VAR_3)) = eq(VAR_2,VAR_3)
| eq2(VAR_0,VAR_1) != btrue ),
file('theBenchmark.p',axiom_065) ).
cnf(c_84,plain,
( eq3(app(A,C),app(B,D)) = eq(C,D)
| eq2(A,B) != btrue ),
inference(clausify,[status(thm)],[axiom_065]) ).
fof(axiom_071,axiom,
! [VAR_0] : apply1(lam3,VAR_0) = var(VAR_0),
file('theBenchmark.p',axiom_071) ).
cnf(c_91,plain,
apply1(lam3,A) = var(A),
inference(clausify,[status(thm)],[axiom_071]) ).
fof(goal,axiom,
! [VAR_0,VAR_1] : eq4(prop_unify_makes_equal(VAR_0,VAR_1),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_92,plain,
eq4(prop_unify_makes_equal(A,B),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_93,plain,
eq4(eq4(aux6(A,B,unifyloop(lam3,cons(A,nil),cons(B,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_61,c_92]) ).
cnf(c_96,plain,
eq3(subst(A,B),subst(A,C)) = aux6(B,C,unifyloop(A,nil,nil)),
inference(paramod,[status(thm)],[c_41,c_14]) ).
cnf(c_99,plain,
cons(app(A,substList(B,C)),substList(B,D)) = substList(B,cons(app(A,C),D)),
inference(paramod,[status(thm)],[c_22,c_26]) ).
cnf(c_3858,plain,
cons(subst(A,B),nil) = substList(A,cons(B,nil)),
inference(paramod,[status(thm)],[c_24,c_26]) ).
cnf(c_101,plain,
substList(A,cons(B,nil)) = cons(subst(A,B),nil),
inference(copy,[status(thm)],[c_3858]) ).
cnf(c_3859,plain,
aux5(A,B,C,D,B,btrue) = unifyvar(A,B,var(B),C,D),
inference(paramod,[status(thm)],[c_75,c_54]) ).
cnf(c_3860,plain,
unifyloop(A,C,D) = unifyvar(A,B,var(B),C,D),
inference(paramod,[status(thm)],[c_10,c_3859]) ).
cnf(c_139,plain,
unifyvar(A,B,var(B),C,D) = unifyloop(A,C,D),
inference(copy,[status(thm)],[c_3860]) ).
cnf(c_152,plain,
eq3(app(A,B),app(A,C)) = eq(B,C),
inference(resolve,[status(thm)],[c_84,c_75]) ).
cnf(c_166,plain,
eq4(eq4(aux6(app(A,B),app(C,D),aux3(lam3,nil,A,B,nil,C,D,eq2(A,C))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_45,c_93]) ).
cnf(c_3861,plain,
cons(app(A,nil),substList(B,C)) = substList(B,cons(app(A,nil),C)),
inference(paramod,[status(thm)],[c_24,c_99]) ).
cnf(c_183,plain,
substList(A,cons(app(B,nil),C)) = cons(app(B,nil),substList(A,C)),
inference(copy,[status(thm)],[c_3861]) ).
cnf(c_3862,plain,
eq4(eq4(aux6(app(A,B),app(A,C),aux3(lam3,nil,A,B,nil,A,C,btrue)),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_75,c_166]) ).
cnf(c_192,plain,
eq4(eq4(aux6(app(A,B),app(A,C),unifyloop(lam3,append(B,nil),append(C,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_5,c_3862]) ).
cnf(c_200,plain,
eq4(eq4(aux6(app(A,B),app(A,cons(C,D)),unifyloop(lam3,append(B,nil),cons(C,append(D,nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_66,c_192]) ).
cnf(c_216,plain,
eq4(eq4(aux6(app(A,B),app(A,cons(C,nil)),unifyloop(lam3,append(B,nil),cons(C,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_65,c_200]) ).
cnf(c_225,plain,
eq4(eq4(aux6(app(A,cons(B,C)),app(A,cons(D,nil)),unifyloop(lam3,cons(B,append(C,nil)),cons(D,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_66,c_216]) ).
cnf(c_251,plain,
eq4(eq4(aux6(app(A,cons(app(B,C),D)),app(A,cons(app(E,F),nil)),aux3(lam3,append(D,nil),B,C,nil,E,F,eq2(B,E))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_45,c_225]) ).
cnf(c_264,plain,
( eq(cons(app(C,A),D),cons(app(C,B),E)) = bfalse
| eq(A,B) != bfalse ),
inference(paramod,[status(thm)],[c_152,c_79]) ).
cnf(c_3863,plain,
eq4(eq4(aux6(app(A,cons(app(B,C),D)),app(A,cons(app(B,E),nil)),aux3(lam3,append(D,nil),B,C,nil,B,E,btrue)),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_75,c_251]) ).
cnf(c_367,plain,
eq4(eq4(aux6(app(A,cons(app(B,C),D)),app(A,cons(app(B,E),nil)),unifyloop(lam3,append(C,append(D,nil)),append(E,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_5,c_3863]) ).
cnf(c_513,plain,
eq4(eq4(aux6(app(A,cons(app(B,nil),C)),app(A,cons(app(B,D),nil)),unifyloop(lam3,append(C,nil),append(D,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_65,c_367]) ).
cnf(c_520,plain,
eq4(eq4(aux6(app(A,cons(app(B,nil),cons(C,D))),app(A,cons(app(B,E),nil)),unifyloop(lam3,cons(C,append(D,nil)),append(E,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_66,c_513]) ).
cnf(c_673,plain,
eq4(eq4(aux6(app(A,cons(app(B,nil),cons(C,nil))),app(A,cons(app(B,D),nil)),unifyloop(lam3,cons(C,nil),append(D,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_65,c_520]) ).
cnf(c_676,plain,
eq4(eq4(aux6(app(A,cons(app(B,nil),cons(C,nil))),app(A,cons(app(B,cons(D,E)),nil)),unifyloop(lam3,cons(C,nil),cons(D,append(E,nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_66,c_673]) ).
cnf(c_2233,plain,
eq(cons(app(A,nil),B),cons(app(A,cons(C,D)),E)) = bfalse,
inference(resolve,[status(thm)],[c_264,c_81]) ).
cnf(c_2980,plain,
eq4(eq4(aux6(app(A,cons(app(B,nil),cons(C,nil))),app(A,cons(app(B,cons(D,nil)),nil)),unifyloop(lam3,cons(C,nil),cons(D,nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_65,c_676]) ).
cnf(c_2984,plain,
eq4(eq4(aux6(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,cons(app(B,cons(D,nil)),nil)),unifyvar(lam3,C,D,nil,nil)),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_2980]) ).
cnf(c_3012,plain,
eq4(eq4(aux6(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,cons(app(B,cons(var(C),nil)),nil)),unifyloop(lam3,nil,nil)),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_139,c_2984]) ).
cnf(c_3864,plain,
eq4(eq4(eq3(subst(lam3,app(A,cons(app(B,nil),cons(var(C),nil)))),subst(lam3,app(A,cons(app(B,cons(var(C),nil)),nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_96,c_3012]) ).
cnf(c_3865,plain,
eq4(eq4(eq3(app(A,substList(lam3,cons(app(B,nil),cons(var(C),nil)))),subst(lam3,app(A,cons(app(B,cons(var(C),nil)),nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_22,c_3864]) ).
cnf(c_3866,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),substList(lam3,cons(var(C),nil)))),subst(lam3,app(A,cons(app(B,cons(var(C),nil)),nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_183,c_3865]) ).
cnf(c_3867,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(subst(lam3,var(C)),nil))),subst(lam3,app(A,cons(app(B,cons(var(C),nil)),nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_101,c_3866]) ).
cnf(c_3868,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(apply1(lam3,C),nil))),subst(lam3,app(A,cons(app(B,cons(var(C),nil)),nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_23,c_3867]) ).
cnf(c_3869,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(var(C),nil))),subst(lam3,app(A,cons(app(B,cons(var(C),nil)),nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_91,c_3868]) ).
cnf(c_3870,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,substList(lam3,cons(app(B,cons(var(C),nil)),nil)))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_22,c_3869]) ).
cnf(c_3871,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,cons(subst(lam3,app(B,cons(var(C),nil))),nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_101,c_3870]) ).
cnf(c_3872,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,cons(app(B,substList(lam3,cons(var(C),nil))),nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_22,c_3871]) ).
cnf(c_3873,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,cons(app(B,cons(subst(lam3,var(C)),nil)),nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_101,c_3872]) ).
cnf(c_3874,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,cons(app(B,cons(apply1(lam3,C),nil)),nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_23,c_3873]) ).
cnf(c_3875,plain,
eq4(eq4(eq3(app(A,cons(app(B,nil),cons(var(C),nil))),app(A,cons(app(B,cons(var(C),nil)),nil))),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_91,c_3874]) ).
cnf(c_3876,plain,
eq4(eq4(eq(cons(app(B,nil),cons(var(C),nil)),cons(app(B,cons(var(C),nil)),nil)),btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_152,c_3875]) ).
cnf(c_3877,plain,
eq4(eq4(bfalse,btrue),bfalse) != btrue,
inference(paramod,[status(thm)],[c_2233,c_3876]) ).
cnf(c_3878,plain,
eq4(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_73,c_3877]) ).
cnf(c_3879,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_77,c_3878]) ).
cnf(c_3857,plain,
$false,
inference(copy,[status(thm)],[c_3879]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX242-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.09/0.55 % Computer : n007.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Sat Sep 26 17:00:24 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.09/0.56 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.56 % Process 30980 was started by sandbox2 on n007,
% 0.09/0.56 % Sat Sep 26 17:00:24 2026
% 0.09/0.56 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.56
% 0.12/0.56 % From the command line: assign(max_seconds, 300).
% 11.01/2.10
% 11.01/2.10 % given #500 (T,wt=28): 2260 aux6(A,A,aux4(B,C,nil,nil,D,E,bfalse)) = btrue. [para(991(a,1),175(a,1,3))].
% 11.01/2.10
% 11.01/2.10 % SZS status Unsatisfiable for theBenchmark
% 11.01/2.10
% 11.01/2.10 % Proof 1 at 1.15 (+ 0.24) seconds.
% 11.01/2.10 % Length of proof is 54.
% 11.01/2.10 % Level of proof is 18.
% 11.01/2.10 % Maximum clause weight is 86.000.
% 11.01/2.10 % Given clauses 737.
% 11.01/2.10
% 11.01/2.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------