%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE084-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.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 01:51:34 PM UTC 2026
% Result : Unsatisfiable 7.78s 1.62s
% Output : CNFRefutation 7.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 22
% Syntax : Number of clauses : 148 ( 148 unt; 0 nHn; 96 RR)
% Number of literals : 148 ( 147 equ; 8 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 77 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t21,axiom,
sF0 = antidomain(sK1_goals_X1),
introduced(definition) ).
cnf(t29,plain,
antidomain(sK1_goals_X1) = sF0,
inference(orient,[status(thm)],[t21]) ).
cnf(t22,axiom,
sF1 = antidomain(antidomain(sK1_goals_X1)),
introduced(definition) ).
cnf(t2945,plain,
sF1 = antidomain(sF0),
inference(step,[status(thm)],[t22,t29]) ).
cnf(t36,plain,
antidomain(sF0) = sF1,
inference(orient,[status(thm)],[t2945]) ).
cnf(t23,axiom,
sF2 = multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1))),
introduced(definition) ).
cnf(t2947,plain,
sF2 = multiplication(sK2_goals_X0,antidomain(sF0)),
inference(step,[status(thm)],[t23,t29]) ).
cnf(t2948,plain,
sF2 = multiplication(sK2_goals_X0,sF1),
inference(step,[status(thm)],[t2947,t36]) ).
cnf(t70,plain,
multiplication(sK2_goals_X0,sF1) = sF2,
inference(orient,[status(thm)],[t2948]) ).
cnf(t24,axiom,
sF3 = antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1)))),
introduced(definition) ).
cnf(t3010,plain,
sF3 = antidomain(multiplication(sK2_goals_X0,antidomain(sF0))),
inference(step,[status(thm)],[t24,t29]) ).
cnf(t3011,plain,
sF3 = antidomain(multiplication(sK2_goals_X0,sF1)),
inference(step,[status(thm)],[t3010,t36]) ).
cnf(t3012,plain,
sF3 = antidomain(sF2),
inference(step,[status(thm)],[t3011,t70]) ).
cnf(t510,plain,
antidomain(sF2) = sF3,
inference(orient,[status(thm)],[t3012]) ).
cnf(t26,axiom,
sF5 = multiplication(sK2_goals_X0,sK1_goals_X1),
introduced(definition) ).
cnf(t37,plain,
multiplication(sK2_goals_X0,sK1_goals_X1) = sF5,
inference(orient,[status(thm)],[t26]) ).
cnf(t27,axiom,
sF6 = antidomain(multiplication(sK2_goals_X0,sK1_goals_X1)),
introduced(definition) ).
cnf(t2946,plain,
sF6 = antidomain(sF5),
inference(step,[status(thm)],[t27,t37]) ).
cnf(t48,plain,
antidomain(sF5) = sF6,
inference(orient,[status(thm)],[t2946]) ).
cnf(t17,axiom,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t209,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t17]) ).
cnf(t7,axiom,
multiplication(antidomain(X1),X1) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t7]) ).
cnf(t19,axiom,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t335,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(orient,[status(thm)],[t19]) ).
cnf(t16,axiom,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t57,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t61,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = multiplication(zero,X2),
inference(cp,[status(thm)],[t57,t40]) ).
cnf(t5,axiom,
multiplication(zero,X1) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t3046,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(step,[status(thm)],[t61,t35]) ).
cnf(t770,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(orient,[status(thm)],[t3046]) ).
cnf(t71,plain,
multiplication(sK2_goals_X0,multiplication(sF1,X1)) = multiplication(sF2,X1),
inference(cp,[status(thm)],[t57,t70]) ).
cnf(t159,plain,
multiplication(sK2_goals_X0,multiplication(sF1,X1)) = multiplication(sF2,X1),
inference(orient,[status(thm)],[t71]) ).
cnf(t18,axiom,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t270,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t41,plain,
zero = multiplication(sF0,sK1_goals_X1),
inference(cp,[status(thm)],[t40,t29]) ).
cnf(t46,plain,
multiplication(sF0,sK1_goals_X1) = zero,
inference(orient,[status(thm)],[t41]) ).
cnf(t279,plain,
multiplication(addition(sF0,X1),sK1_goals_X1) = addition(zero,multiplication(X1,sK1_goals_X1)),
inference(cp,[status(thm)],[t270,t46]) ).
cnf(t8,axiom,
addition(X1,X2) = addition(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t65,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
addition(X1,zero) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t66,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t65,t31]) ).
cnf(t69,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t66]) ).
cnf(t3059,plain,
multiplication(addition(sF0,X1),sK1_goals_X1) = multiplication(X1,sK1_goals_X1),
inference(step,[status(thm)],[t279,t69]) ).
cnf(t1046,plain,
multiplication(addition(sF0,X1),sK1_goals_X1) = multiplication(X1,sK1_goals_X1),
inference(orient,[status(thm)],[t3059]) ).
cnf(t11,axiom,
addition(antidomain(antidomain(X1)),antidomain(X1)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2954,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t11,t65]) ).
cnf(t85,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(orient,[status(thm)],[t2954]) ).
cnf(t86,plain,
one = addition(sF0,antidomain(antidomain(sK1_goals_X1))),
inference(cp,[status(thm)],[t85,t29]) ).
cnf(t2957,plain,
one = addition(sF0,antidomain(sF0)),
inference(step,[status(thm)],[t86,t29]) ).
cnf(t2958,plain,
one = addition(sF0,sF1),
inference(step,[status(thm)],[t2957,t36]) ).
cnf(t95,plain,
addition(sF0,sF1) = one,
inference(orient,[status(thm)],[t2958]) ).
cnf(t1047,plain,
multiplication(sF1,sK1_goals_X1) = multiplication(one,sK1_goals_X1),
inference(cp,[status(thm)],[t1046,t95]) ).
cnf(t4,axiom,
multiplication(one,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t3060,plain,
multiplication(sF1,sK1_goals_X1) = sK1_goals_X1,
inference(step,[status(thm)],[t1047,t34]) ).
cnf(t1059,plain,
multiplication(sF1,sK1_goals_X1) = sK1_goals_X1,
inference(orient,[status(thm)],[t3060]) ).
cnf(t1061,plain,
multiplication(sF2,sK1_goals_X1) = multiplication(sK2_goals_X0,sK1_goals_X1),
inference(cp,[status(thm)],[t159,t1059]) ).
cnf(t3061,plain,
multiplication(sF2,sK1_goals_X1) = sF5,
inference(step,[status(thm)],[t1061,t37]) ).
cnf(t1070,plain,
multiplication(sF2,sK1_goals_X1) = sF5,
inference(orient,[status(thm)],[t3061]) ).
cnf(t1080,plain,
zero = multiplication(antidomain(sF2),sF5),
inference(cp,[status(thm)],[t770,t1070]) ).
cnf(t3064,plain,
zero = multiplication(sF3,sF5),
inference(step,[status(thm)],[t1080,t510]) ).
cnf(t1119,plain,
multiplication(sF3,sF5) = zero,
inference(orient,[status(thm)],[t3064]) ).
cnf(t1125,plain,
antidomain(multiplication(sF3,antidomain(antidomain(sF5)))) = addition(antidomain(zero),antidomain(multiplication(sF3,antidomain(antidomain(sF5))))),
inference(cp,[status(thm)],[t335,t1119]) ).
cnf(t3072,plain,
antidomain(multiplication(sF3,antidomain(sF6))) = addition(antidomain(zero),antidomain(multiplication(sF3,antidomain(antidomain(sF5))))),
inference(step,[status(thm)],[t1125,t48]) ).
cnf(t28,axiom,
sF7 = antidomain(antidomain(multiplication(sK2_goals_X0,sK1_goals_X1))),
introduced(definition) ).
cnf(t2949,plain,
sF7 = antidomain(antidomain(sF5)),
inference(step,[status(thm)],[t28,t37]) ).
cnf(t2950,plain,
sF7 = antidomain(sF6),
inference(step,[status(thm)],[t2949,t48]) ).
cnf(t72,plain,
antidomain(sF6) = sF7,
inference(orient,[status(thm)],[t2950]) ).
cnf(t3073,plain,
antidomain(multiplication(sF3,sF7)) = addition(antidomain(zero),antidomain(multiplication(sF3,antidomain(antidomain(sF5))))),
inference(step,[status(thm)],[t3072,t72]) ).
cnf(t2,axiom,
multiplication(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t42,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t40,t32]) ).
cnf(t45,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t42]) ).
cnf(t88,plain,
one = addition(zero,antidomain(antidomain(one))),
inference(cp,[status(thm)],[t85,t45]) ).
cnf(t2955,plain,
one = antidomain(antidomain(one)),
inference(step,[status(thm)],[t88,t69]) ).
cnf(t2956,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t2955,t45]) ).
cnf(t94,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t2956]) ).
cnf(t3074,plain,
antidomain(multiplication(sF3,sF7)) = addition(one,antidomain(multiplication(sF3,antidomain(antidomain(sF5))))),
inference(step,[status(thm)],[t3073,t94]) ).
cnf(t13,axiom,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t53,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t0,axiom,
addition(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t55,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t53,t30]) ).
cnf(t76,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t55]) ).
cnf(t93,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = addition(antidomain(X1),one),
inference(cp,[status(thm)],[t76,t85]) ).
cnf(t2970,plain,
one = addition(antidomain(X1),one),
inference(step,[status(thm)],[t93,t85]) ).
cnf(t2971,plain,
one = addition(one,antidomain(X1)),
inference(step,[status(thm)],[t2970,t65]) ).
cnf(t129,plain,
addition(one,antidomain(X1)) = one,
inference(orient,[status(thm)],[t2971]) ).
cnf(t3075,plain,
antidomain(multiplication(sF3,sF7)) = one,
inference(step,[status(thm)],[t3074,t129]) ).
cnf(t1145,plain,
antidomain(multiplication(sF3,sF7)) = one,
inference(orient,[status(thm)],[t3075]) ).
cnf(t1146,plain,
zero = multiplication(one,multiplication(sF3,sF7)),
inference(cp,[status(thm)],[t40,t1145]) ).
cnf(t3076,plain,
zero = multiplication(sF3,sF7),
inference(step,[status(thm)],[t1146,t34]) ).
cnf(t1150,plain,
multiplication(sF3,sF7) = zero,
inference(orient,[status(thm)],[t3076]) ).
cnf(t1154,plain,
multiplication(sF3,addition(X1,sF7)) = addition(multiplication(sF3,X1),zero),
inference(cp,[status(thm)],[t209,t1150]) ).
cnf(t3249,plain,
multiplication(sF3,addition(X1,sF7)) = multiplication(sF3,X1),
inference(step,[status(thm)],[t1154,t31]) ).
cnf(t2889,plain,
multiplication(sF3,addition(X1,sF7)) = multiplication(sF3,X1),
inference(orient,[status(thm)],[t3249]) ).
cnf(t89,plain,
one = addition(sF6,antidomain(antidomain(sF5))),
inference(cp,[status(thm)],[t85,t48]) ).
cnf(t2959,plain,
one = addition(sF6,antidomain(sF6)),
inference(step,[status(thm)],[t89,t48]) ).
cnf(t2960,plain,
one = addition(sF6,sF7),
inference(step,[status(thm)],[t2959,t72]) ).
cnf(t99,plain,
addition(sF6,sF7) = one,
inference(orient,[status(thm)],[t2960]) ).
cnf(t2890,plain,
multiplication(sF3,sF6) = multiplication(sF3,one),
inference(cp,[status(thm)],[t2889,t99]) ).
cnf(t73,plain,
zero = multiplication(sF7,sF6),
inference(cp,[status(thm)],[t40,t72]) ).
cnf(t74,plain,
multiplication(sF7,sF6) = zero,
inference(orient,[status(thm)],[t73]) ).
cnf(t291,plain,
multiplication(addition(X1,sF7),sF6) = addition(multiplication(X1,sF6),zero),
inference(cp,[status(thm)],[t270,t74]) ).
cnf(t3099,plain,
multiplication(addition(X1,sF7),sF6) = multiplication(X1,sF6),
inference(step,[status(thm)],[t291,t31]) ).
cnf(t1313,plain,
multiplication(addition(X1,sF7),sF6) = multiplication(X1,sF6),
inference(orient,[status(thm)],[t3099]) ).
cnf(t339,plain,
antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1)))) = addition(antidomain(sF5),antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1))))),
inference(cp,[status(thm)],[t335,t37]) ).
cnf(t2985,plain,
antidomain(multiplication(sK2_goals_X0,antidomain(sF0))) = addition(antidomain(sF5),antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1))))),
inference(step,[status(thm)],[t339,t29]) ).
cnf(t2986,plain,
antidomain(multiplication(sK2_goals_X0,sF1)) = addition(antidomain(sF5),antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1))))),
inference(step,[status(thm)],[t2985,t36]) ).
cnf(t2987,plain,
antidomain(sF2) = addition(antidomain(sF5),antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1))))),
inference(step,[status(thm)],[t2986,t70]) ).
cnf(t2988,plain,
antidomain(sF2) = addition(sF6,antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1))))),
inference(step,[status(thm)],[t2987,t48]) ).
cnf(t2989,plain,
antidomain(sF2) = addition(sF6,antidomain(multiplication(sK2_goals_X0,antidomain(sF0)))),
inference(step,[status(thm)],[t2988,t29]) ).
cnf(t2990,plain,
antidomain(sF2) = addition(sF6,antidomain(multiplication(sK2_goals_X0,sF1))),
inference(step,[status(thm)],[t2989,t36]) ).
cnf(t2991,plain,
antidomain(sF2) = addition(sF6,antidomain(sF2)),
inference(step,[status(thm)],[t2990,t70]) ).
cnf(t364,plain,
addition(sF6,antidomain(sF2)) = antidomain(sF2),
inference(orient,[status(thm)],[t2991]) ).
cnf(t511,plain,
addition(sF6,sF3) = antidomain(sF2),
inference(rw,[status(thm)],[t364]) ).
cnf(t3014,plain,
addition(sF3,sF6) = antidomain(sF2),
inference(step,[status(thm)],[t511,t65]) ).
cnf(t3015,plain,
addition(sF3,sF6) = sF3,
inference(step,[status(thm)],[t3014,t510]) ).
cnf(t518,plain,
addition(sF3,sF6) = sF3,
inference(orient,[status(thm)],[t3015]) ).
cnf(t520,plain,
addition(sF3,addition(sF6,X1)) = addition(sF3,X1),
inference(cp,[status(thm)],[t53,t518]) ).
cnf(t1675,plain,
addition(sF3,addition(sF6,X1)) = addition(sF3,X1),
inference(orient,[status(thm)],[t520]) ).
cnf(t1678,plain,
addition(sF3,sF7) = addition(sF3,one),
inference(cp,[status(thm)],[t1675,t99]) ).
cnf(t515,plain,
one = addition(one,sF3),
inference(cp,[status(thm)],[t129,t510]) ).
cnf(t3016,plain,
one = addition(sF3,one),
inference(step,[status(thm)],[t515,t65]) ).
cnf(t534,plain,
addition(sF3,one) = one,
inference(orient,[status(thm)],[t3016]) ).
cnf(t3132,plain,
addition(sF3,sF7) = one,
inference(step,[status(thm)],[t1678,t534]) ).
cnf(t1691,plain,
addition(sF3,sF7) = one,
inference(orient,[status(thm)],[t3132]) ).
cnf(t1699,plain,
multiplication(sF3,sF6) = multiplication(one,sF6),
inference(cp,[status(thm)],[t1313,t1691]) ).
cnf(t3133,plain,
multiplication(sF3,sF6) = sF6,
inference(step,[status(thm)],[t1699,t34]) ).
cnf(t1701,plain,
multiplication(sF3,sF6) = sF6,
inference(orient,[status(thm)],[t3133]) ).
cnf(t3250,plain,
sF6 = multiplication(sF3,one),
inference(step,[status(thm)],[t2890,t1701]) ).
cnf(t3251,plain,
sF6 = sF3,
inference(step,[status(thm)],[t3250,t32]) ).
cnf(t2898,plain,
sF6 = sF3,
inference(orient,[status(thm)],[t3251]) ).
cnf(t3252,plain,
antidomain(sF5) = sF3,
inference(step,[status(thm)],[t48,t2898]) ).
cnf(t2899,plain,
antidomain(sF5) = sF3,
inference(orient,[status(thm)],[t3252]) ).
cnf(u0,negated_conjecture,
domain(multiplication(sK2_goals_X0,sK1_goals_X1)) != domain(multiplication(sK2_goals_X0,domain(sK1_goals_X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
antidomain(antidomain(multiplication(sK2_goals_X0,antidomain(antidomain(sK1_goals_X1))))) != antidomain(antidomain(multiplication(sK2_goals_X0,sK1_goals_X1))),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
antidomain(antidomain(multiplication(sK2_goals_X0,antidomain(sF0)))) != antidomain(antidomain(multiplication(sK2_goals_X0,sK1_goals_X1))),
inference(rw,[status(thm)],[goal_0,t29]) ).
cnf(g0_1,plain,
antidomain(antidomain(multiplication(sK2_goals_X0,sF1))) != antidomain(antidomain(multiplication(sK2_goals_X0,sK1_goals_X1))),
inference(rw,[status(thm)],[g0_0,t36]) ).
cnf(g0_2,plain,
antidomain(antidomain(sF2)) != antidomain(antidomain(multiplication(sK2_goals_X0,sK1_goals_X1))),
inference(rw,[status(thm)],[g0_1,t70]) ).
cnf(g0_3,plain,
antidomain(sF3) != antidomain(antidomain(multiplication(sK2_goals_X0,sK1_goals_X1))),
inference(rw,[status(thm)],[g0_2,t510]) ).
cnf(g0_4,plain,
antidomain(sF3) != antidomain(antidomain(sF5)),
inference(rw,[status(thm)],[g0_3,t37]) ).
cnf(g0_5,plain,
antidomain(sF3) != antidomain(sF3),
inference(rw,[status(thm)],[g0_4,t2899]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE084-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/0.40 % Computer : n006.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Wed Sep 23 18:53:12 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.78/1.62 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.78/1.62 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------