%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE108-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 : n016.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:37 PM UTC 2026
% Result : Unsatisfiable 50.30s 7.02s
% Output : CNFRefutation 50.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 41
% Syntax : Number of clauses : 487 ( 487 unt; 0 nHn; 386 RR)
% Number of literals : 487 ( 486 equ; 15 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 27 con; 0-2 aty)
% Number of variables : 133 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t22,axiom,
sF0 = antidomain(sK2_goals_X1),
introduced(definition) ).
cnf(t44,plain,
antidomain(sK2_goals_X1) = sF0,
inference(orient,[status(thm)],[t22]) ).
cnf(t23,axiom,
sF1 = antidomain(antidomain(sK2_goals_X1)),
introduced(definition) ).
cnf(t22351,plain,
sF1 = antidomain(sF0),
inference(step,[status(thm)],[t23,t44]) ).
cnf(t52,plain,
antidomain(sF0) = sF1,
inference(orient,[status(thm)],[t22351]) ).
cnf(t38,axiom,
sF16 = coantidomain(antidomain(antidomain(sK2_goals_X1))),
introduced(definition) ).
cnf(t22355,plain,
sF16 = coantidomain(antidomain(sF0)),
inference(step,[status(thm)],[t38,t44]) ).
cnf(t22356,plain,
sF16 = coantidomain(sF1),
inference(step,[status(thm)],[t22355,t52]) ).
cnf(t71,plain,
coantidomain(sF1) = sF16,
inference(orient,[status(thm)],[t22356]) ).
cnf(t17,axiom,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t236,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t17]) ).
cnf(t6,axiom,
multiplication(X1,coantidomain(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t54,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t39,axiom,
sF17 = coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),
introduced(definition) ).
cnf(t22360,plain,
sF17 = coantidomain(coantidomain(antidomain(sF0))),
inference(step,[status(thm)],[t39,t44]) ).
cnf(t22361,plain,
sF17 = coantidomain(coantidomain(sF1)),
inference(step,[status(thm)],[t22360,t52]) ).
cnf(t22362,plain,
sF17 = coantidomain(sF16),
inference(step,[status(thm)],[t22361,t71]) ).
cnf(t98,plain,
coantidomain(sF16) = sF17,
inference(orient,[status(thm)],[t22362]) ).
cnf(t99,plain,
zero = multiplication(sF16,sF17),
inference(cp,[status(thm)],[t54,t98]) ).
cnf(t100,plain,
multiplication(sF16,sF17) = zero,
inference(orient,[status(thm)],[t99]) ).
cnf(t259,plain,
multiplication(sF16,addition(X1,sF17)) = addition(multiplication(sF16,X1),zero),
inference(cp,[status(thm)],[t236,t100]) ).
cnf(t1,axiom,
addition(X1,zero) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t47,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t22668,plain,
multiplication(sF16,addition(X1,sF17)) = multiplication(sF16,X1),
inference(step,[status(thm)],[t259,t47]) ).
cnf(t1563,plain,
multiplication(sF16,addition(X1,sF17)) = multiplication(sF16,X1),
inference(orient,[status(thm)],[t22668]) ).
cnf(t13,axiom,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t79,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t11,axiom,
addition(antidomain(antidomain(X1)),antidomain(X1)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t8,axiom,
addition(X1,X2) = addition(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t73,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t22363,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t11,t73]) ).
cnf(t102,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(orient,[status(thm)],[t22363]) ).
cnf(t103,plain,
one = addition(sF0,antidomain(antidomain(sK2_goals_X1))),
inference(cp,[status(thm)],[t102,t44]) ).
cnf(t22366,plain,
one = addition(sF0,antidomain(sF0)),
inference(step,[status(thm)],[t103,t44]) ).
cnf(t22367,plain,
one = addition(sF0,sF1),
inference(step,[status(thm)],[t22366,t52]) ).
cnf(t113,plain,
addition(sF0,sF1) = one,
inference(orient,[status(thm)],[t22367]) ).
cnf(t115,plain,
addition(sF0,addition(sF1,X1)) = addition(one,X1),
inference(cp,[status(thm)],[t79,t113]) ).
cnf(t511,plain,
addition(sF0,addition(sF1,X1)) = addition(one,X1),
inference(orient,[status(thm)],[t115]) ).
cnf(t18,axiom,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t279,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t72,plain,
zero = multiplication(sF1,sF16),
inference(cp,[status(thm)],[t54,t71]) ).
cnf(t75,plain,
multiplication(sF1,sF16) = zero,
inference(orient,[status(thm)],[t72]) ).
cnf(t254,plain,
multiplication(sF1,addition(sF16,X1)) = addition(zero,multiplication(sF1,X1)),
inference(cp,[status(thm)],[t236,t75]) ).
cnf(t74,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t73,t47]) ).
cnf(t76,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t74]) ).
cnf(t22658,plain,
multiplication(sF1,addition(sF16,X1)) = multiplication(sF1,X1),
inference(step,[status(thm)],[t254,t76]) ).
cnf(t1474,plain,
multiplication(sF1,addition(sF16,X1)) = multiplication(sF1,X1),
inference(orient,[status(thm)],[t22658]) ).
cnf(t12,axiom,
addition(coantidomain(coantidomain(X1)),coantidomain(X1)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22375,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(step,[status(thm)],[t12,t73]) ).
cnf(t128,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t22375]) ).
cnf(t130,plain,
one = addition(sF16,coantidomain(coantidomain(sF1))),
inference(cp,[status(thm)],[t128,t71]) ).
cnf(t22378,plain,
one = addition(sF16,coantidomain(sF16)),
inference(step,[status(thm)],[t130,t71]) ).
cnf(t22379,plain,
one = addition(sF16,sF17),
inference(step,[status(thm)],[t22378,t98]) ).
cnf(t135,plain,
addition(sF16,sF17) = one,
inference(orient,[status(thm)],[t22379]) ).
cnf(t1475,plain,
multiplication(sF1,sF17) = multiplication(sF1,one),
inference(cp,[status(thm)],[t1474,t135]) ).
cnf(t2,axiom,
multiplication(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t48,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t22659,plain,
multiplication(sF1,sF17) = sF1,
inference(step,[status(thm)],[t1475,t48]) ).
cnf(t1485,plain,
multiplication(sF1,sF17) = sF1,
inference(orient,[status(thm)],[t22659]) ).
cnf(t1488,plain,
multiplication(addition(sF1,X1),sF17) = addition(sF1,multiplication(X1,sF17)),
inference(cp,[status(thm)],[t279,t1485]) ).
cnf(t10334,plain,
addition(sF1,multiplication(X1,sF17)) = multiplication(addition(sF1,X1),sF17),
inference(orient,[status(thm)],[t1488]) ).
cnf(t4,axiom,
multiplication(one,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t10335,plain,
multiplication(addition(sF1,one),sF17) = addition(sF1,sF17),
inference(cp,[status(thm)],[t10334,t50]) ).
cnf(t0,axiom,
addition(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t46,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t81,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t79,t46]) ).
cnf(t144,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t81]) ).
cnf(t105,plain,
one = addition(sF1,antidomain(antidomain(sF0))),
inference(cp,[status(thm)],[t102,t52]) ).
cnf(t22374,plain,
one = addition(sF1,antidomain(sF1)),
inference(step,[status(thm)],[t105,t52]) ).
cnf(t125,plain,
addition(sF1,antidomain(sF1)) = one,
inference(orient,[status(thm)],[t22374]) ).
cnf(t152,plain,
addition(sF1,antidomain(sF1)) = addition(sF1,one),
inference(cp,[status(thm)],[t144,t125]) ).
cnf(t22386,plain,
one = addition(sF1,one),
inference(step,[status(thm)],[t152,t125]) ).
cnf(t190,plain,
addition(sF1,one) = one,
inference(orient,[status(thm)],[t22386]) ).
cnf(t23073,plain,
multiplication(one,sF17) = addition(sF1,sF17),
inference(step,[status(thm)],[t10335,t190]) ).
cnf(t23074,plain,
sF17 = addition(sF1,sF17),
inference(step,[status(thm)],[t23073,t50]) ).
cnf(t10359,plain,
addition(sF1,sF17) = sF17,
inference(orient,[status(thm)],[t23074]) ).
cnf(t10364,plain,
addition(one,sF17) = addition(sF0,sF17),
inference(cp,[status(thm)],[t511,t10359]) ).
cnf(t23076,plain,
addition(sF17,one) = addition(sF0,sF17),
inference(step,[status(thm)],[t10364,t73]) ).
cnf(t132,plain,
one = addition(sF17,coantidomain(coantidomain(sF16))),
inference(cp,[status(thm)],[t128,t98]) ).
cnf(t22381,plain,
one = addition(sF17,coantidomain(sF17)),
inference(step,[status(thm)],[t132,t98]) ).
cnf(t141,plain,
addition(sF17,coantidomain(sF17)) = one,
inference(orient,[status(thm)],[t22381]) ).
cnf(t156,plain,
addition(sF17,coantidomain(sF17)) = addition(sF17,one),
inference(cp,[status(thm)],[t144,t141]) ).
cnf(t22389,plain,
one = addition(sF17,one),
inference(step,[status(thm)],[t156,t141]) ).
cnf(t202,plain,
addition(sF17,one) = one,
inference(orient,[status(thm)],[t22389]) ).
cnf(t23077,plain,
one = addition(sF0,sF17),
inference(step,[status(thm)],[t23076,t202]) ).
cnf(t10387,plain,
addition(sF0,sF17) = one,
inference(orient,[status(thm)],[t23077]) ).
cnf(t10394,plain,
multiplication(sF16,sF0) = multiplication(sF16,one),
inference(cp,[status(thm)],[t1563,t10387]) ).
cnf(t20,axiom,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t397,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(orient,[status(thm)],[t20]) ).
cnf(t7,axiom,
multiplication(antidomain(X1),X1) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t57,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t7]) ).
cnf(t61,plain,
zero = multiplication(sF1,sF0),
inference(cp,[status(thm)],[t57,t52]) ).
cnf(t66,plain,
multiplication(sF1,sF0) = zero,
inference(orient,[status(thm)],[t61]) ).
cnf(t404,plain,
coantidomain(multiplication(coantidomain(coantidomain(sF1)),sF0)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF1)),sF0))),
inference(cp,[status(thm)],[t397,t66]) ).
cnf(t22432,plain,
coantidomain(multiplication(coantidomain(sF16),sF0)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF1)),sF0))),
inference(step,[status(thm)],[t404,t71]) ).
cnf(t22433,plain,
coantidomain(multiplication(sF17,sF0)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF1)),sF0))),
inference(step,[status(thm)],[t22432,t98]) ).
cnf(t55,plain,
zero = coantidomain(one),
inference(cp,[status(thm)],[t54,t50]) ).
cnf(t56,plain,
coantidomain(one) = zero,
inference(orient,[status(thm)],[t55]) ).
cnf(t129,plain,
one = addition(zero,coantidomain(coantidomain(one))),
inference(cp,[status(thm)],[t128,t56]) ).
cnf(t22376,plain,
one = coantidomain(coantidomain(one)),
inference(step,[status(thm)],[t129,t76]) ).
cnf(t22377,plain,
one = coantidomain(zero),
inference(step,[status(thm)],[t22376,t56]) ).
cnf(t134,plain,
coantidomain(zero) = one,
inference(orient,[status(thm)],[t22377]) ).
cnf(t22434,plain,
coantidomain(multiplication(sF17,sF0)) = addition(one,coantidomain(multiplication(coantidomain(coantidomain(sF1)),sF0))),
inference(step,[status(thm)],[t22433,t134]) ).
cnf(t153,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = addition(coantidomain(X1),one),
inference(cp,[status(thm)],[t144,t128]) ).
cnf(t22402,plain,
one = addition(coantidomain(X1),one),
inference(step,[status(thm)],[t153,t128]) ).
cnf(t22403,plain,
one = addition(one,coantidomain(X1)),
inference(step,[status(thm)],[t22402,t73]) ).
cnf(t308,plain,
addition(one,coantidomain(X1)) = one,
inference(orient,[status(thm)],[t22403]) ).
cnf(t22435,plain,
coantidomain(multiplication(sF17,sF0)) = one,
inference(step,[status(thm)],[t22434,t308]) ).
cnf(t445,plain,
coantidomain(multiplication(sF17,sF0)) = one,
inference(orient,[status(thm)],[t22435]) ).
cnf(t446,plain,
zero = multiplication(multiplication(sF17,sF0),one),
inference(cp,[status(thm)],[t54,t445]) ).
cnf(t22436,plain,
zero = multiplication(sF17,sF0),
inference(step,[status(thm)],[t446,t48]) ).
cnf(t449,plain,
multiplication(sF17,sF0) = zero,
inference(orient,[status(thm)],[t22436]) ).
cnf(t455,plain,
multiplication(addition(X1,sF17),sF0) = addition(multiplication(X1,sF0),zero),
inference(cp,[status(thm)],[t279,t449]) ).
cnf(t22768,plain,
multiplication(addition(X1,sF17),sF0) = multiplication(X1,sF0),
inference(step,[status(thm)],[t455,t47]) ).
cnf(t2709,plain,
multiplication(addition(X1,sF17),sF0) = multiplication(X1,sF0),
inference(orient,[status(thm)],[t22768]) ).
cnf(t2711,plain,
multiplication(sF16,sF0) = multiplication(one,sF0),
inference(cp,[status(thm)],[t2709,t135]) ).
cnf(t22769,plain,
multiplication(sF16,sF0) = sF0,
inference(step,[status(thm)],[t2711,t50]) ).
cnf(t2720,plain,
multiplication(sF16,sF0) = sF0,
inference(orient,[status(thm)],[t22769]) ).
cnf(t23078,plain,
sF0 = multiplication(sF16,one),
inference(step,[status(thm)],[t10394,t2720]) ).
cnf(t23079,plain,
sF0 = sF16,
inference(step,[status(thm)],[t23078,t48]) ).
cnf(t10414,plain,
sF16 = sF0,
inference(orient,[status(thm)],[t23079]) ).
cnf(t23080,plain,
coantidomain(sF1) = sF0,
inference(step,[status(thm)],[t71,t10414]) ).
cnf(t10415,plain,
coantidomain(sF1) = sF0,
inference(orient,[status(thm)],[t23080]) ).
cnf(t23082,plain,
coantidomain(sF0) = sF17,
inference(step,[status(thm)],[t98,t10414]) ).
cnf(t10418,plain,
coantidomain(sF0) = sF17,
inference(rw,[status(thm)],[t23082]) ).
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(t330,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(orient,[status(thm)],[t19]) ).
cnf(t58,plain,
zero = multiplication(sF0,sK2_goals_X1),
inference(cp,[status(thm)],[t57,t44]) ).
cnf(t64,plain,
multiplication(sF0,sK2_goals_X1) = zero,
inference(orient,[status(thm)],[t58]) ).
cnf(t339,plain,
antidomain(multiplication(sF0,antidomain(antidomain(sK2_goals_X1)))) = addition(antidomain(zero),antidomain(multiplication(sF0,antidomain(antidomain(sK2_goals_X1))))),
inference(cp,[status(thm)],[t330,t64]) ).
cnf(t22407,plain,
antidomain(multiplication(sF0,antidomain(sF0))) = addition(antidomain(zero),antidomain(multiplication(sF0,antidomain(antidomain(sK2_goals_X1))))),
inference(step,[status(thm)],[t339,t44]) ).
cnf(t22408,plain,
antidomain(multiplication(sF0,sF1)) = addition(antidomain(zero),antidomain(multiplication(sF0,antidomain(antidomain(sK2_goals_X1))))),
inference(step,[status(thm)],[t22407,t52]) ).
cnf(t60,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t57,t48]) ).
cnf(t63,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t60]) ).
cnf(t107,plain,
one = addition(zero,antidomain(antidomain(one))),
inference(cp,[status(thm)],[t102,t63]) ).
cnf(t22364,plain,
one = antidomain(antidomain(one)),
inference(step,[status(thm)],[t107,t76]) ).
cnf(t22365,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t22364,t63]) ).
cnf(t112,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t22365]) ).
cnf(t22409,plain,
antidomain(multiplication(sF0,sF1)) = addition(one,antidomain(multiplication(sF0,antidomain(antidomain(sK2_goals_X1))))),
inference(step,[status(thm)],[t22408,t112]) ).
cnf(t147,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = addition(antidomain(X1),one),
inference(cp,[status(thm)],[t144,t102]) ).
cnf(t22400,plain,
one = addition(antidomain(X1),one),
inference(step,[status(thm)],[t147,t102]) ).
cnf(t22401,plain,
one = addition(one,antidomain(X1)),
inference(step,[status(thm)],[t22400,t73]) ).
cnf(t268,plain,
addition(one,antidomain(X1)) = one,
inference(orient,[status(thm)],[t22401]) ).
cnf(t22410,plain,
antidomain(multiplication(sF0,sF1)) = one,
inference(step,[status(thm)],[t22409,t268]) ).
cnf(t357,plain,
antidomain(multiplication(sF0,sF1)) = one,
inference(orient,[status(thm)],[t22410]) ).
cnf(t358,plain,
zero = multiplication(one,multiplication(sF0,sF1)),
inference(cp,[status(thm)],[t57,t357]) ).
cnf(t22411,plain,
zero = multiplication(sF0,sF1),
inference(step,[status(thm)],[t358,t50]) ).
cnf(t361,plain,
multiplication(sF0,sF1) = zero,
inference(orient,[status(thm)],[t22411]) ).
cnf(t366,plain,
multiplication(addition(sF0,X1),sF1) = addition(zero,multiplication(X1,sF1)),
inference(cp,[status(thm)],[t279,t361]) ).
cnf(t22748,plain,
multiplication(addition(sF0,X1),sF1) = multiplication(X1,sF1),
inference(step,[status(thm)],[t366,t76]) ).
cnf(t2327,plain,
multiplication(addition(sF0,X1),sF1) = multiplication(X1,sF1),
inference(orient,[status(thm)],[t22748]) ).
cnf(t10396,plain,
multiplication(sF17,sF1) = multiplication(one,sF1),
inference(cp,[status(thm)],[t2327,t10387]) ).
cnf(t452,plain,
multiplication(sF17,addition(sF0,X1)) = addition(zero,multiplication(sF17,X1)),
inference(cp,[status(thm)],[t236,t449]) ).
cnf(t22762,plain,
multiplication(sF17,addition(sF0,X1)) = multiplication(sF17,X1),
inference(step,[status(thm)],[t452,t76]) ).
cnf(t2644,plain,
multiplication(sF17,addition(sF0,X1)) = multiplication(sF17,X1),
inference(orient,[status(thm)],[t22762]) ).
cnf(t2645,plain,
multiplication(sF17,sF1) = multiplication(sF17,one),
inference(cp,[status(thm)],[t2644,t113]) ).
cnf(t22763,plain,
multiplication(sF17,sF1) = sF17,
inference(step,[status(thm)],[t2645,t48]) ).
cnf(t2659,plain,
multiplication(sF17,sF1) = sF17,
inference(orient,[status(thm)],[t22763]) ).
cnf(t23099,plain,
sF17 = multiplication(one,sF1),
inference(step,[status(thm)],[t10396,t2659]) ).
cnf(t23100,plain,
sF17 = sF1,
inference(step,[status(thm)],[t23099,t50]) ).
cnf(t10467,plain,
sF17 = sF1,
inference(orient,[status(thm)],[t23100]) ).
cnf(t23109,plain,
coantidomain(sF0) = sF1,
inference(step,[status(thm)],[t10418,t10467]) ).
cnf(t10507,plain,
coantidomain(sF0) = sF1,
inference(orient,[status(thm)],[t23109]) ).
cnf(t16,axiom,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t84,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t1486,plain,
multiplication(sF1,multiplication(sF17,X1)) = multiplication(sF1,X1),
inference(cp,[status(thm)],[t84,t1485]) ).
cnf(t10223,plain,
multiplication(sF1,multiplication(sF17,X1)) = multiplication(sF1,X1),
inference(orient,[status(thm)],[t1486]) ).
cnf(t40,axiom,
sF18 = multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0),
introduced(definition) ).
cnf(t22593,plain,
sF18 = multiplication(coantidomain(coantidomain(antidomain(sF0))),sK3_goals_X0),
inference(step,[status(thm)],[t40,t44]) ).
cnf(t22594,plain,
sF18 = multiplication(coantidomain(coantidomain(sF1)),sK3_goals_X0),
inference(step,[status(thm)],[t22593,t52]) ).
cnf(t22595,plain,
sF18 = multiplication(coantidomain(sF16),sK3_goals_X0),
inference(step,[status(thm)],[t22594,t71]) ).
cnf(t22596,plain,
sF18 = multiplication(sF17,sK3_goals_X0),
inference(step,[status(thm)],[t22595,t98]) ).
cnf(t864,plain,
multiplication(sF17,sK3_goals_X0) = sF18,
inference(orient,[status(thm)],[t22596]) ).
cnf(t10224,plain,
multiplication(sF1,sK3_goals_X0) = multiplication(sF1,sF18),
inference(cp,[status(thm)],[t10223,t864]) ).
cnf(t10251,plain,
multiplication(sF1,sK3_goals_X0) = multiplication(sF1,sF18),
inference(orient,[status(thm)],[t10224]) ).
cnf(t10471,plain,
multiplication(sF1,sK3_goals_X0) = sF18,
inference(rw,[status(thm)],[t864]) ).
cnf(t23113,plain,
multiplication(sF1,sF18) = sF18,
inference(step,[status(thm)],[t10471,t10251]) ).
cnf(t10578,plain,
multiplication(sF1,sF18) = sF18,
inference(orient,[status(thm)],[t23113]) ).
cnf(t23114,plain,
multiplication(sF1,sK3_goals_X0) = sF18,
inference(step,[status(thm)],[t10251,t10578]) ).
cnf(t10579,plain,
multiplication(sF1,sK3_goals_X0) = sF18,
inference(orient,[status(thm)],[t23114]) ).
cnf(t41,axiom,
sF19 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0)),
introduced(definition) ).
cnf(t22600,plain,
sF19 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF0))),sK3_goals_X0)),
inference(step,[status(thm)],[t41,t44]) ).
cnf(t22601,plain,
sF19 = coantidomain(multiplication(coantidomain(coantidomain(sF1)),sK3_goals_X0)),
inference(step,[status(thm)],[t22600,t52]) ).
cnf(t22602,plain,
sF19 = coantidomain(multiplication(coantidomain(sF16),sK3_goals_X0)),
inference(step,[status(thm)],[t22601,t71]) ).
cnf(t22603,plain,
sF19 = coantidomain(multiplication(sF17,sK3_goals_X0)),
inference(step,[status(thm)],[t22602,t98]) ).
cnf(t22604,plain,
sF19 = coantidomain(sF18),
inference(step,[status(thm)],[t22603,t864]) ).
cnf(t901,plain,
coantidomain(sF18) = sF19,
inference(orient,[status(thm)],[t22604]) ).
cnf(t42,axiom,
sF20 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0))),
introduced(definition) ).
cnf(t22608,plain,
sF20 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF0))),sK3_goals_X0))),
inference(step,[status(thm)],[t42,t44]) ).
cnf(t22609,plain,
sF20 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF1)),sK3_goals_X0))),
inference(step,[status(thm)],[t22608,t52]) ).
cnf(t22610,plain,
sF20 = coantidomain(coantidomain(multiplication(coantidomain(sF16),sK3_goals_X0))),
inference(step,[status(thm)],[t22609,t71]) ).
cnf(t22611,plain,
sF20 = coantidomain(coantidomain(multiplication(sF17,sK3_goals_X0))),
inference(step,[status(thm)],[t22610,t98]) ).
cnf(t22612,plain,
sF20 = coantidomain(coantidomain(sF18)),
inference(step,[status(thm)],[t22611,t864]) ).
cnf(t22613,plain,
sF20 = coantidomain(sF19),
inference(step,[status(thm)],[t22612,t901]) ).
cnf(t931,plain,
coantidomain(sF19) = sF20,
inference(orient,[status(thm)],[t22613]) ).
cnf(t24,axiom,
sF2 = antidomain(sK1_goals_X2),
introduced(definition) ).
cnf(t45,plain,
antidomain(sK1_goals_X2) = sF2,
inference(orient,[status(thm)],[t24]) ).
cnf(t25,axiom,
sF3 = antidomain(antidomain(sK1_goals_X2)),
introduced(definition) ).
cnf(t22352,plain,
sF3 = antidomain(sF2),
inference(step,[status(thm)],[t25,t45]) ).
cnf(t53,plain,
antidomain(sF2) = sF3,
inference(orient,[status(thm)],[t22352]) ).
cnf(t43,axiom,
sF21 = addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))),
introduced(definition) ).
cnf(t22618,plain,
sF21 = addition(antidomain(antidomain(sK1_goals_X2)),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0)))),
inference(step,[status(thm)],[t43,t73]) ).
cnf(t22619,plain,
sF21 = addition(antidomain(sF2),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0)))),
inference(step,[status(thm)],[t22618,t45]) ).
cnf(t22620,plain,
sF21 = addition(sF3,coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0)))),
inference(step,[status(thm)],[t22619,t53]) ).
cnf(t22621,plain,
sF21 = addition(sF3,coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF0))),sK3_goals_X0)))),
inference(step,[status(thm)],[t22620,t44]) ).
cnf(t22622,plain,
sF21 = addition(sF3,coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF1)),sK3_goals_X0)))),
inference(step,[status(thm)],[t22621,t52]) ).
cnf(t22623,plain,
sF21 = addition(sF3,coantidomain(coantidomain(multiplication(coantidomain(sF16),sK3_goals_X0)))),
inference(step,[status(thm)],[t22622,t71]) ).
cnf(t22624,plain,
sF21 = addition(sF3,coantidomain(coantidomain(multiplication(sF17,sK3_goals_X0)))),
inference(step,[status(thm)],[t22623,t98]) ).
cnf(t22625,plain,
sF21 = addition(sF3,coantidomain(coantidomain(sF18))),
inference(step,[status(thm)],[t22624,t864]) ).
cnf(t22626,plain,
sF21 = addition(sF3,coantidomain(sF19)),
inference(step,[status(thm)],[t22625,t901]) ).
cnf(t22627,plain,
sF21 = addition(sF3,sF20),
inference(step,[status(thm)],[t22626,t931]) ).
cnf(t963,plain,
addition(sF3,sF20) = sF21,
inference(orient,[status(thm)],[t22627]) ).
cnf(t59,plain,
zero = multiplication(sF2,sK1_goals_X2),
inference(cp,[status(thm)],[t57,t45]) ).
cnf(t65,plain,
multiplication(sF2,sK1_goals_X2) = zero,
inference(orient,[status(thm)],[t59]) ).
cnf(t340,plain,
antidomain(multiplication(sF2,antidomain(antidomain(sK1_goals_X2)))) = addition(antidomain(zero),antidomain(multiplication(sF2,antidomain(antidomain(sK1_goals_X2))))),
inference(cp,[status(thm)],[t330,t65]) ).
cnf(t22412,plain,
antidomain(multiplication(sF2,antidomain(sF2))) = addition(antidomain(zero),antidomain(multiplication(sF2,antidomain(antidomain(sK1_goals_X2))))),
inference(step,[status(thm)],[t340,t45]) ).
cnf(t22413,plain,
antidomain(multiplication(sF2,sF3)) = addition(antidomain(zero),antidomain(multiplication(sF2,antidomain(antidomain(sK1_goals_X2))))),
inference(step,[status(thm)],[t22412,t53]) ).
cnf(t22414,plain,
antidomain(multiplication(sF2,sF3)) = addition(one,antidomain(multiplication(sF2,antidomain(antidomain(sK1_goals_X2))))),
inference(step,[status(thm)],[t22413,t112]) ).
cnf(t22415,plain,
antidomain(multiplication(sF2,sF3)) = one,
inference(step,[status(thm)],[t22414,t268]) ).
cnf(t369,plain,
antidomain(multiplication(sF2,sF3)) = one,
inference(orient,[status(thm)],[t22415]) ).
cnf(t370,plain,
zero = multiplication(one,multiplication(sF2,sF3)),
inference(cp,[status(thm)],[t57,t369]) ).
cnf(t22416,plain,
zero = multiplication(sF2,sF3),
inference(step,[status(thm)],[t370,t50]) ).
cnf(t373,plain,
multiplication(sF2,sF3) = zero,
inference(orient,[status(thm)],[t22416]) ).
cnf(t378,plain,
multiplication(addition(sF2,X1),sF3) = addition(zero,multiplication(X1,sF3)),
inference(cp,[status(thm)],[t279,t373]) ).
cnf(t22754,plain,
multiplication(addition(sF2,X1),sF3) = multiplication(X1,sF3),
inference(step,[status(thm)],[t378,t76]) ).
cnf(t2397,plain,
multiplication(addition(sF2,X1),sF3) = multiplication(X1,sF3),
inference(orient,[status(thm)],[t22754]) ).
cnf(t104,plain,
one = addition(sF2,antidomain(antidomain(sK1_goals_X2))),
inference(cp,[status(thm)],[t102,t45]) ).
cnf(t22368,plain,
one = addition(sF2,antidomain(sF2)),
inference(step,[status(thm)],[t104,t45]) ).
cnf(t22369,plain,
one = addition(sF2,sF3),
inference(step,[status(thm)],[t22368,t53]) ).
cnf(t116,plain,
addition(sF2,sF3) = one,
inference(orient,[status(thm)],[t22369]) ).
cnf(t118,plain,
addition(sF2,addition(sF3,X1)) = addition(one,X1),
inference(cp,[status(thm)],[t79,t116]) ).
cnf(t519,plain,
addition(sF2,addition(sF3,X1)) = addition(one,X1),
inference(orient,[status(thm)],[t118]) ).
cnf(t969,plain,
addition(one,sF20) = addition(sF2,sF21),
inference(cp,[status(thm)],[t519,t963]) ).
cnf(t22629,plain,
addition(sF20,one) = addition(sF2,sF21),
inference(step,[status(thm)],[t969,t73]) ).
cnf(t935,plain,
one = addition(one,sF20),
inference(cp,[status(thm)],[t308,t931]) ).
cnf(t22615,plain,
one = addition(sF20,one),
inference(step,[status(thm)],[t935,t73]) ).
cnf(t951,plain,
addition(sF20,one) = one,
inference(orient,[status(thm)],[t22615]) ).
cnf(t22630,plain,
one = addition(sF2,sF21),
inference(step,[status(thm)],[t22629,t951]) ).
cnf(t977,plain,
addition(sF2,sF21) = one,
inference(orient,[status(thm)],[t22630]) ).
cnf(t2399,plain,
multiplication(sF21,sF3) = multiplication(one,sF3),
inference(cp,[status(thm)],[t2397,t977]) ).
cnf(t22755,plain,
multiplication(sF21,sF3) = sF3,
inference(step,[status(thm)],[t2399,t50]) ).
cnf(t2409,plain,
multiplication(sF21,sF3) = sF3,
inference(orient,[status(thm)],[t22755]) ).
cnf(t2411,plain,
multiplication(sF21,addition(sF3,X1)) = addition(sF3,multiplication(sF21,X1)),
inference(cp,[status(thm)],[t236,t2409]) ).
cnf(t13046,plain,
addition(sF3,multiplication(sF21,X1)) = multiplication(sF21,addition(sF3,X1)),
inference(orient,[status(thm)],[t2411]) ).
cnf(t62,plain,
zero = multiplication(sF3,sF2),
inference(cp,[status(thm)],[t57,t53]) ).
cnf(t67,plain,
multiplication(sF3,sF2) = zero,
inference(orient,[status(thm)],[t62]) ).
cnf(t292,plain,
multiplication(addition(sF3,X1),sF2) = addition(zero,multiplication(X1,sF2)),
inference(cp,[status(thm)],[t279,t67]) ).
cnf(t22704,plain,
multiplication(addition(sF3,X1),sF2) = multiplication(X1,sF2),
inference(step,[status(thm)],[t292,t76]) ).
cnf(t1950,plain,
multiplication(addition(sF3,X1),sF2) = multiplication(X1,sF2),
inference(orient,[status(thm)],[t22704]) ).
cnf(t1953,plain,
multiplication(sF20,sF2) = multiplication(sF21,sF2),
inference(cp,[status(thm)],[t1950,t963]) ).
cnf(t2033,plain,
multiplication(sF21,sF2) = multiplication(sF20,sF2),
inference(orient,[status(thm)],[t1953]) ).
cnf(t13050,plain,
multiplication(sF21,addition(sF3,sF2)) = addition(sF3,multiplication(sF20,sF2)),
inference(cp,[status(thm)],[t13046,t2033]) ).
cnf(t253,plain,
multiplication(X1,addition(X2,X3)) = addition(multiplication(X1,X3),multiplication(X1,X2)),
inference(cp,[status(thm)],[t236,t73]) ).
cnf(t22911,plain,
multiplication(X1,addition(X2,X3)) = multiplication(X1,addition(X3,X2)),
inference(step,[status(thm)],[t253,t236]) ).
cnf(t4524,plain,
multiplication(X1,addition(X2,X3)) = multiplication(X1,addition(X3,X2)),
inference(orient,[status(thm)],[t22911]) ).
cnf(t23679,plain,
multiplication(sF21,addition(sF2,sF3)) = addition(sF3,multiplication(sF20,sF2)),
inference(step,[status(thm)],[t13050,t4524]) ).
cnf(t23680,plain,
multiplication(sF21,one) = addition(sF3,multiplication(sF20,sF2)),
inference(step,[status(thm)],[t23679,t116]) ).
cnf(t23681,plain,
sF21 = addition(sF3,multiplication(sF20,sF2)),
inference(step,[status(thm)],[t23680,t48]) ).
cnf(t905,plain,
coantidomain(multiplication(coantidomain(coantidomain(sF18)),X1)) = addition(coantidomain(multiplication(sF18,X1)),coantidomain(multiplication(coantidomain(sF19),X1))),
inference(cp,[status(thm)],[t397,t901]) ).
cnf(t23633,plain,
coantidomain(multiplication(coantidomain(sF19),X1)) = addition(coantidomain(multiplication(sF18,X1)),coantidomain(multiplication(coantidomain(sF19),X1))),
inference(step,[status(thm)],[t905,t901]) ).
cnf(t23634,plain,
coantidomain(multiplication(sF20,X1)) = addition(coantidomain(multiplication(sF18,X1)),coantidomain(multiplication(coantidomain(sF19),X1))),
inference(step,[status(thm)],[t23633,t931]) ).
cnf(t23635,plain,
coantidomain(multiplication(sF20,X1)) = addition(coantidomain(multiplication(sF18,X1)),coantidomain(multiplication(sF20,X1))),
inference(step,[status(thm)],[t23634,t931]) ).
cnf(t21367,plain,
addition(coantidomain(multiplication(sF18,X1)),coantidomain(multiplication(sF20,X1))) = coantidomain(multiplication(sF20,X1)),
inference(orient,[status(thm)],[t23635]) ).
cnf(t865,plain,
multiplication(sF17,multiplication(sK3_goals_X0,X1)) = multiplication(sF18,X1),
inference(cp,[status(thm)],[t84,t864]) ).
cnf(t3501,plain,
multiplication(sF17,multiplication(sK3_goals_X0,X1)) = multiplication(sF18,X1),
inference(orient,[status(thm)],[t865]) ).
cnf(t31,axiom,
sF9 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))),
introduced(definition) ).
cnf(t22484,plain,
sF9 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2))))))),
inference(step,[status(thm)],[t31,t45]) ).
cnf(t22485,plain,
sF9 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF3)))))),
inference(step,[status(thm)],[t22484,t53]) ).
cnf(t26,axiom,
sF4 = antidomain(antidomain(antidomain(sK1_goals_X2))),
introduced(definition) ).
cnf(t22353,plain,
sF4 = antidomain(antidomain(sF2)),
inference(step,[status(thm)],[t26,t45]) ).
cnf(t22354,plain,
sF4 = antidomain(sF3),
inference(step,[status(thm)],[t22353,t53]) ).
cnf(t68,plain,
antidomain(sF3) = sF4,
inference(orient,[status(thm)],[t22354]) ).
cnf(t22486,plain,
sF9 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF4))))),
inference(step,[status(thm)],[t22485,t68]) ).
cnf(t27,axiom,
sF5 = antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))),
introduced(definition) ).
cnf(t22357,plain,
sF5 = antidomain(antidomain(antidomain(sF2))),
inference(step,[status(thm)],[t27,t45]) ).
cnf(t22358,plain,
sF5 = antidomain(antidomain(sF3)),
inference(step,[status(thm)],[t22357,t53]) ).
cnf(t22359,plain,
sF5 = antidomain(sF4),
inference(step,[status(thm)],[t22358,t68]) ).
cnf(t94,plain,
antidomain(sF4) = sF5,
inference(orient,[status(thm)],[t22359]) ).
cnf(t22487,plain,
sF9 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF5)))),
inference(step,[status(thm)],[t22486,t94]) ).
cnf(t28,axiom,
sF6 = antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))),
introduced(definition) ).
cnf(t22457,plain,
sF6 = antidomain(antidomain(antidomain(antidomain(sF2)))),
inference(step,[status(thm)],[t28,t45]) ).
cnf(t22458,plain,
sF6 = antidomain(antidomain(antidomain(sF3))),
inference(step,[status(thm)],[t22457,t53]) ).
cnf(t22459,plain,
sF6 = antidomain(antidomain(sF4)),
inference(step,[status(thm)],[t22458,t68]) ).
cnf(t22460,plain,
sF6 = antidomain(sF5),
inference(step,[status(thm)],[t22459,t94]) ).
cnf(t527,plain,
antidomain(sF5) = sF6,
inference(orient,[status(thm)],[t22460]) ).
cnf(t22488,plain,
sF9 = multiplication(sK3_goals_X0,antidomain(antidomain(sF6))),
inference(step,[status(thm)],[t22487,t527]) ).
cnf(t29,axiom,
sF7 = antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))),
introduced(definition) ).
cnf(t22465,plain,
sF7 = antidomain(antidomain(antidomain(antidomain(antidomain(sF2))))),
inference(step,[status(thm)],[t29,t45]) ).
cnf(t22466,plain,
sF7 = antidomain(antidomain(antidomain(antidomain(sF3)))),
inference(step,[status(thm)],[t22465,t53]) ).
cnf(t22467,plain,
sF7 = antidomain(antidomain(antidomain(sF4))),
inference(step,[status(thm)],[t22466,t68]) ).
cnf(t22468,plain,
sF7 = antidomain(antidomain(sF5)),
inference(step,[status(thm)],[t22467,t94]) ).
cnf(t22469,plain,
sF7 = antidomain(sF6),
inference(step,[status(thm)],[t22468,t527]) ).
cnf(t567,plain,
antidomain(sF6) = sF7,
inference(orient,[status(thm)],[t22469]) ).
cnf(t22489,plain,
sF9 = multiplication(sK3_goals_X0,antidomain(sF7)),
inference(step,[status(thm)],[t22488,t567]) ).
cnf(t30,axiom,
sF8 = antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),
introduced(definition) ).
cnf(t22474,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),
inference(step,[status(thm)],[t30,t45]) ).
cnf(t22475,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(antidomain(sF3))))),
inference(step,[status(thm)],[t22474,t53]) ).
cnf(t22476,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(sF4)))),
inference(step,[status(thm)],[t22475,t68]) ).
cnf(t22477,plain,
sF8 = antidomain(antidomain(antidomain(sF5))),
inference(step,[status(thm)],[t22476,t94]) ).
cnf(t22478,plain,
sF8 = antidomain(antidomain(sF6)),
inference(step,[status(thm)],[t22477,t527]) ).
cnf(t22479,plain,
sF8 = antidomain(sF7),
inference(step,[status(thm)],[t22478,t567]) ).
cnf(t597,plain,
antidomain(sF7) = sF8,
inference(orient,[status(thm)],[t22479]) ).
cnf(t22490,plain,
sF9 = multiplication(sK3_goals_X0,sF8),
inference(step,[status(thm)],[t22489,t597]) ).
cnf(t636,plain,
multiplication(sK3_goals_X0,sF8) = sF9,
inference(orient,[status(thm)],[t22490]) ).
cnf(t2025,plain,
antidomain(sF3) = sF8,
inference(rw,[status(thm)],[t597]) ).
cnf(t106,plain,
one = addition(sF3,antidomain(antidomain(sF2))),
inference(cp,[status(thm)],[t102,t53]) ).
cnf(t22370,plain,
one = addition(sF3,antidomain(sF3)),
inference(step,[status(thm)],[t106,t53]) ).
cnf(t22371,plain,
one = addition(sF3,sF4),
inference(step,[status(thm)],[t22370,t68]) ).
cnf(t119,plain,
addition(sF3,sF4) = one,
inference(orient,[status(thm)],[t22371]) ).
cnf(t1951,plain,
multiplication(sF4,sF2) = multiplication(one,sF2),
inference(cp,[status(thm)],[t1950,t119]) ).
cnf(t69,plain,
zero = multiplication(sF4,sF3),
inference(cp,[status(thm)],[t57,t68]) ).
cnf(t70,plain,
multiplication(sF4,sF3) = zero,
inference(orient,[status(thm)],[t69]) ).
cnf(t252,plain,
multiplication(sF4,addition(X1,sF3)) = addition(multiplication(sF4,X1),zero),
inference(cp,[status(thm)],[t236,t70]) ).
cnf(t22656,plain,
multiplication(sF4,addition(X1,sF3)) = multiplication(sF4,X1),
inference(step,[status(thm)],[t252,t47]) ).
cnf(t1457,plain,
multiplication(sF4,addition(X1,sF3)) = multiplication(sF4,X1),
inference(orient,[status(thm)],[t22656]) ).
cnf(t1459,plain,
multiplication(sF4,sF2) = multiplication(sF4,one),
inference(cp,[status(thm)],[t1457,t116]) ).
cnf(t22657,plain,
multiplication(sF4,sF2) = sF4,
inference(step,[status(thm)],[t1459,t48]) ).
cnf(t1466,plain,
multiplication(sF4,sF2) = sF4,
inference(orient,[status(thm)],[t22657]) ).
cnf(t22705,plain,
sF4 = multiplication(one,sF2),
inference(step,[status(thm)],[t1951,t1466]) ).
cnf(t22706,plain,
sF4 = sF2,
inference(step,[status(thm)],[t22705,t50]) ).
cnf(t1963,plain,
sF4 = sF2,
inference(orient,[status(thm)],[t22706]) ).
cnf(t22707,plain,
antidomain(sF3) = sF2,
inference(step,[status(thm)],[t68,t1963]) ).
cnf(t1964,plain,
antidomain(sF3) = sF2,
inference(orient,[status(thm)],[t22707]) ).
cnf(t22726,plain,
sF2 = sF8,
inference(step,[status(thm)],[t2025,t1964]) ).
cnf(t2028,plain,
sF8 = sF2,
inference(orient,[status(thm)],[t22726]) ).
cnf(t22727,plain,
multiplication(sK3_goals_X0,sF2) = sF9,
inference(step,[status(thm)],[t636,t2028]) ).
cnf(t2032,plain,
multiplication(sK3_goals_X0,sF2) = sF9,
inference(rw,[status(thm)],[t22727]) ).
cnf(t2093,plain,
multiplication(sK3_goals_X0,sF2) = sF9,
inference(orient,[status(thm)],[t2032]) ).
cnf(t3505,plain,
multiplication(sF18,sF2) = multiplication(sF17,sF9),
inference(cp,[status(thm)],[t3501,t2093]) ).
cnf(t3514,plain,
multiplication(sF18,sF2) = multiplication(sF17,sF9),
inference(orient,[status(thm)],[t3505]) ).
cnf(t23102,plain,
multiplication(sF18,sF2) = multiplication(sF1,sF9),
inference(step,[status(thm)],[t3514,t10467]) ).
cnf(t10485,plain,
multiplication(sF18,sF2) = multiplication(sF1,sF9),
inference(orient,[status(thm)],[t23102]) ).
cnf(t32,axiom,
sF10 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))))),
introduced(definition) ).
cnf(t22492,plain,
sF10 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))))),
inference(step,[status(thm)],[t32,t45]) ).
cnf(t22493,plain,
sF10 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF3))))))),
inference(step,[status(thm)],[t22492,t53]) ).
cnf(t22494,plain,
sF10 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF4)))))),
inference(step,[status(thm)],[t22493,t68]) ).
cnf(t22495,plain,
sF10 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF5))))),
inference(step,[status(thm)],[t22494,t94]) ).
cnf(t22496,plain,
sF10 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF6)))),
inference(step,[status(thm)],[t22495,t527]) ).
cnf(t22497,plain,
sF10 = antidomain(multiplication(sK3_goals_X0,antidomain(sF7))),
inference(step,[status(thm)],[t22496,t567]) ).
cnf(t22498,plain,
sF10 = antidomain(multiplication(sK3_goals_X0,sF8)),
inference(step,[status(thm)],[t22497,t597]) ).
cnf(t22499,plain,
sF10 = antidomain(sF9),
inference(step,[status(thm)],[t22498,t636]) ).
cnf(t692,plain,
antidomain(sF9) = sF10,
inference(orient,[status(thm)],[t22499]) ).
cnf(t693,plain,
zero = multiplication(sF10,sF9),
inference(cp,[status(thm)],[t57,t692]) ).
cnf(t702,plain,
multiplication(sF10,sF9) = zero,
inference(orient,[status(thm)],[t693]) ).
cnf(t707,plain,
multiplication(addition(X1,sF10),sF9) = addition(multiplication(X1,sF9),zero),
inference(cp,[status(thm)],[t279,t702]) ).
cnf(t22792,plain,
multiplication(addition(X1,sF10),sF9) = multiplication(X1,sF9),
inference(step,[status(thm)],[t707,t47]) ).
cnf(t3012,plain,
multiplication(addition(X1,sF10),sF9) = multiplication(X1,sF9),
inference(orient,[status(thm)],[t22792]) ).
cnf(t37,axiom,
sF15 = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))))))),
introduced(definition) ).
cnf(t22570,plain,
sF15 = addition(antidomain(sF0),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))))))),
inference(step,[status(thm)],[t37,t44]) ).
cnf(t22571,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))))))),
inference(step,[status(thm)],[t22570,t52]) ).
cnf(t22572,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2))))))))))))),
inference(step,[status(thm)],[t22571,t45]) ).
cnf(t22573,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF3)))))))))))),
inference(step,[status(thm)],[t22572,t53]) ).
cnf(t22574,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF4))))))))))),
inference(step,[status(thm)],[t22573,t68]) ).
cnf(t22575,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF5)))))))))),
inference(step,[status(thm)],[t22574,t94]) ).
cnf(t22576,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF6))))))))),
inference(step,[status(thm)],[t22575,t527]) ).
cnf(t22577,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF7)))))))),
inference(step,[status(thm)],[t22576,t567]) ).
cnf(t22578,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF8))))))),
inference(step,[status(thm)],[t22577,t597]) ).
cnf(t22579,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(antidomain(sF9)))))),
inference(step,[status(thm)],[t22578,t636]) ).
cnf(t22580,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(antidomain(sF10))))),
inference(step,[status(thm)],[t22579,t692]) ).
cnf(t33,axiom,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))),
introduced(definition) ).
cnf(t22500,plain,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2))))))))),
inference(step,[status(thm)],[t33,t45]) ).
cnf(t22501,plain,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF3)))))))),
inference(step,[status(thm)],[t22500,t53]) ).
cnf(t22502,plain,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF4))))))),
inference(step,[status(thm)],[t22501,t68]) ).
cnf(t22503,plain,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF5)))))),
inference(step,[status(thm)],[t22502,t94]) ).
cnf(t22504,plain,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF6))))),
inference(step,[status(thm)],[t22503,t527]) ).
cnf(t22505,plain,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF7)))),
inference(step,[status(thm)],[t22504,t567]) ).
cnf(t22506,plain,
sF11 = antidomain(antidomain(multiplication(sK3_goals_X0,sF8))),
inference(step,[status(thm)],[t22505,t597]) ).
cnf(t22507,plain,
sF11 = antidomain(antidomain(sF9)),
inference(step,[status(thm)],[t22506,t636]) ).
cnf(t22508,plain,
sF11 = antidomain(sF10),
inference(step,[status(thm)],[t22507,t692]) ).
cnf(t697,plain,
antidomain(sF10) = sF11,
inference(orient,[status(thm)],[t22508]) ).
cnf(t22581,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(sF11)))),
inference(step,[status(thm)],[t22580,t697]) ).
cnf(t34,axiom,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))))))),
introduced(definition) ).
cnf(t22512,plain,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))))))),
inference(step,[status(thm)],[t34,t45]) ).
cnf(t22513,plain,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF3))))))))),
inference(step,[status(thm)],[t22512,t53]) ).
cnf(t22514,plain,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF4)))))))),
inference(step,[status(thm)],[t22513,t68]) ).
cnf(t22515,plain,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF5))))))),
inference(step,[status(thm)],[t22514,t94]) ).
cnf(t22516,plain,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF6)))))),
inference(step,[status(thm)],[t22515,t527]) ).
cnf(t22517,plain,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF7))))),
inference(step,[status(thm)],[t22516,t567]) ).
cnf(t22518,plain,
sF12 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF8)))),
inference(step,[status(thm)],[t22517,t597]) ).
cnf(t22519,plain,
sF12 = antidomain(antidomain(antidomain(sF9))),
inference(step,[status(thm)],[t22518,t636]) ).
cnf(t22520,plain,
sF12 = antidomain(antidomain(sF10)),
inference(step,[status(thm)],[t22519,t692]) ).
cnf(t22521,plain,
sF12 = antidomain(sF11),
inference(step,[status(thm)],[t22520,t697]) ).
cnf(t729,plain,
antidomain(sF11) = sF12,
inference(orient,[status(thm)],[t22521]) ).
cnf(t22582,plain,
sF15 = addition(sF1,antidomain(antidomain(sF12))),
inference(step,[status(thm)],[t22581,t729]) ).
cnf(t35,axiom,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))))),
introduced(definition) ).
cnf(t22527,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2))))))))))),
inference(step,[status(thm)],[t35,t45]) ).
cnf(t22528,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF3)))))))))),
inference(step,[status(thm)],[t22527,t53]) ).
cnf(t22529,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF4))))))))),
inference(step,[status(thm)],[t22528,t68]) ).
cnf(t22530,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF5)))))))),
inference(step,[status(thm)],[t22529,t94]) ).
cnf(t22531,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF6))))))),
inference(step,[status(thm)],[t22530,t527]) ).
cnf(t22532,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF7)))))),
inference(step,[status(thm)],[t22531,t567]) ).
cnf(t22533,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF8))))),
inference(step,[status(thm)],[t22532,t597]) ).
cnf(t22534,plain,
sF13 = antidomain(antidomain(antidomain(antidomain(sF9)))),
inference(step,[status(thm)],[t22533,t636]) ).
cnf(t22535,plain,
sF13 = antidomain(antidomain(antidomain(sF10))),
inference(step,[status(thm)],[t22534,t692]) ).
cnf(t22536,plain,
sF13 = antidomain(antidomain(sF11)),
inference(step,[status(thm)],[t22535,t697]) ).
cnf(t22537,plain,
sF13 = antidomain(sF12),
inference(step,[status(thm)],[t22536,t729]) ).
cnf(t754,plain,
antidomain(sF12) = sF13,
inference(orient,[status(thm)],[t22537]) ).
cnf(t22583,plain,
sF15 = addition(sF1,antidomain(sF13)),
inference(step,[status(thm)],[t22582,t754]) ).
cnf(t36,axiom,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))))))))),
introduced(definition) ).
cnf(t22549,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))))))))),
inference(step,[status(thm)],[t36,t45]) ).
cnf(t22550,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF3))))))))))),
inference(step,[status(thm)],[t22549,t53]) ).
cnf(t22551,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF4)))))))))),
inference(step,[status(thm)],[t22550,t68]) ).
cnf(t22552,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF5))))))))),
inference(step,[status(thm)],[t22551,t94]) ).
cnf(t22553,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF6)))))))),
inference(step,[status(thm)],[t22552,t527]) ).
cnf(t22554,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF7))))))),
inference(step,[status(thm)],[t22553,t567]) ).
cnf(t22555,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF8)))))),
inference(step,[status(thm)],[t22554,t597]) ).
cnf(t22556,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(antidomain(sF9))))),
inference(step,[status(thm)],[t22555,t636]) ).
cnf(t22557,plain,
sF14 = antidomain(antidomain(antidomain(antidomain(sF10)))),
inference(step,[status(thm)],[t22556,t692]) ).
cnf(t22558,plain,
sF14 = antidomain(antidomain(antidomain(sF11))),
inference(step,[status(thm)],[t22557,t697]) ).
cnf(t22559,plain,
sF14 = antidomain(antidomain(sF12)),
inference(step,[status(thm)],[t22558,t729]) ).
cnf(t22560,plain,
sF14 = antidomain(sF13),
inference(step,[status(thm)],[t22559,t754]) ).
cnf(t796,plain,
antidomain(sF13) = sF14,
inference(orient,[status(thm)],[t22560]) ).
cnf(t22584,plain,
sF15 = addition(sF1,sF14),
inference(step,[status(thm)],[t22583,t796]) ).
cnf(t833,plain,
addition(sF1,sF14) = sF15,
inference(orient,[status(thm)],[t22584]) ).
cnf(t3221,plain,
antidomain(sF11) = sF14,
inference(rw,[status(thm)],[t796]) ).
cnf(t730,plain,
zero = multiplication(sF12,sF11),
inference(cp,[status(thm)],[t57,t729]) ).
cnf(t735,plain,
multiplication(sF12,sF11) = zero,
inference(orient,[status(thm)],[t730]) ).
cnf(t738,plain,
multiplication(sF12,addition(X1,sF11)) = addition(multiplication(sF12,X1),zero),
inference(cp,[status(thm)],[t236,t735]) ).
cnf(t22815,plain,
multiplication(sF12,addition(X1,sF11)) = multiplication(sF12,X1),
inference(step,[status(thm)],[t738,t47]) ).
cnf(t3191,plain,
multiplication(sF12,addition(X1,sF11)) = multiplication(sF12,X1),
inference(orient,[status(thm)],[t22815]) ).
cnf(t694,plain,
one = addition(sF10,antidomain(antidomain(sF9))),
inference(cp,[status(thm)],[t102,t692]) ).
cnf(t22525,plain,
one = addition(sF10,antidomain(sF10)),
inference(step,[status(thm)],[t694,t692]) ).
cnf(t22526,plain,
one = addition(sF10,sF11),
inference(step,[status(thm)],[t22525,t697]) ).
cnf(t749,plain,
addition(sF10,sF11) = one,
inference(orient,[status(thm)],[t22526]) ).
cnf(t3193,plain,
multiplication(sF12,sF10) = multiplication(sF12,one),
inference(cp,[status(thm)],[t3191,t749]) ).
cnf(t698,plain,
zero = multiplication(sF11,sF10),
inference(cp,[status(thm)],[t57,t697]) ).
cnf(t715,plain,
multiplication(sF11,sF10) = zero,
inference(orient,[status(thm)],[t698]) ).
cnf(t719,plain,
multiplication(addition(sF11,X1),sF10) = addition(zero,multiplication(X1,sF10)),
inference(cp,[status(thm)],[t279,t715]) ).
cnf(t22797,plain,
multiplication(addition(sF11,X1),sF10) = multiplication(X1,sF10),
inference(step,[status(thm)],[t719,t76]) ).
cnf(t3073,plain,
multiplication(addition(sF11,X1),sF10) = multiplication(X1,sF10),
inference(orient,[status(thm)],[t22797]) ).
cnf(t699,plain,
one = addition(sF11,antidomain(antidomain(sF10))),
inference(cp,[status(thm)],[t102,t697]) ).
cnf(t22540,plain,
one = addition(sF11,antidomain(sF11)),
inference(step,[status(thm)],[t699,t697]) ).
cnf(t22541,plain,
one = addition(sF11,sF12),
inference(step,[status(thm)],[t22540,t729]) ).
cnf(t773,plain,
addition(sF11,sF12) = one,
inference(orient,[status(thm)],[t22541]) ).
cnf(t3074,plain,
multiplication(sF12,sF10) = multiplication(one,sF10),
inference(cp,[status(thm)],[t3073,t773]) ).
cnf(t22798,plain,
multiplication(sF12,sF10) = sF10,
inference(step,[status(thm)],[t3074,t50]) ).
cnf(t3085,plain,
multiplication(sF12,sF10) = sF10,
inference(orient,[status(thm)],[t22798]) ).
cnf(t22816,plain,
sF10 = multiplication(sF12,one),
inference(step,[status(thm)],[t3193,t3085]) ).
cnf(t22817,plain,
sF10 = sF12,
inference(step,[status(thm)],[t22816,t48]) ).
cnf(t3201,plain,
sF12 = sF10,
inference(orient,[status(thm)],[t22817]) ).
cnf(t22818,plain,
antidomain(sF11) = sF10,
inference(step,[status(thm)],[t729,t3201]) ).
cnf(t3202,plain,
antidomain(sF11) = sF10,
inference(orient,[status(thm)],[t22818]) ).
cnf(t22826,plain,
sF10 = sF14,
inference(step,[status(thm)],[t3221,t3202]) ).
cnf(t3226,plain,
sF14 = sF10,
inference(orient,[status(thm)],[t22826]) ).
cnf(t22827,plain,
addition(sF1,sF10) = sF15,
inference(step,[status(thm)],[t833,t3226]) ).
cnf(t3229,plain,
addition(sF1,sF10) = sF15,
inference(rw,[status(thm)],[t22827]) ).
cnf(t3240,plain,
addition(sF1,sF10) = sF15,
inference(orient,[status(thm)],[t3229]) ).
cnf(t3253,plain,
multiplication(sF1,sF9) = multiplication(sF15,sF9),
inference(cp,[status(thm)],[t3012,t3240]) ).
cnf(t3266,plain,
multiplication(sF15,sF9) = multiplication(sF1,sF9),
inference(orient,[status(thm)],[t3253]) ).
cnf(t18207,plain,
multiplication(sF10,sF9) = multiplication(sF1,sF9),
inference(rw,[status(thm)],[t3266]) ).
cnf(t23517,plain,
zero = multiplication(sF1,sF9),
inference(step,[status(thm)],[t18207,t702]) ).
cnf(t18394,plain,
multiplication(sF1,sF9) = zero,
inference(orient,[status(thm)],[t23517]) ).
cnf(t23518,plain,
multiplication(sF18,sF2) = zero,
inference(step,[status(thm)],[t10485,t18394]) ).
cnf(t18395,plain,
multiplication(sF18,sF2) = zero,
inference(orient,[status(thm)],[t23518]) ).
cnf(t21372,plain,
coantidomain(multiplication(sF20,sF2)) = addition(coantidomain(zero),coantidomain(multiplication(sF20,sF2))),
inference(cp,[status(thm)],[t21367,t18395]) ).
cnf(t23636,plain,
coantidomain(multiplication(sF20,sF2)) = addition(one,coantidomain(multiplication(sF20,sF2))),
inference(step,[status(thm)],[t21372,t134]) ).
cnf(t23637,plain,
coantidomain(multiplication(sF20,sF2)) = one,
inference(step,[status(thm)],[t23636,t308]) ).
cnf(t21397,plain,
coantidomain(multiplication(sF20,sF2)) = one,
inference(orient,[status(thm)],[t23637]) ).
cnf(t21398,plain,
zero = multiplication(multiplication(sF20,sF2),one),
inference(cp,[status(thm)],[t54,t21397]) ).
cnf(t23638,plain,
zero = multiplication(sF20,sF2),
inference(step,[status(thm)],[t21398,t48]) ).
cnf(t21405,plain,
multiplication(sF20,sF2) = zero,
inference(orient,[status(thm)],[t23638]) ).
cnf(t23682,plain,
sF21 = addition(sF3,zero),
inference(step,[status(thm)],[t23681,t21405]) ).
cnf(t23683,plain,
sF21 = sF3,
inference(step,[status(thm)],[t23682,t47]) ).
cnf(t22192,plain,
sF21 = sF3,
inference(orient,[status(thm)],[t23683]) ).
cnf(t23684,plain,
addition(sF3,sF20) = sF3,
inference(step,[status(thm)],[t963,t22192]) ).
cnf(t22193,plain,
addition(sF3,sF20) = sF3,
inference(orient,[status(thm)],[t23684]) ).
cnf(u4,negated_conjecture,
addition(backward_diamond(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)) != domain(sK1_goals_X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u5,axiom,
backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d1,axiom,
codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d5,axiom,
backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[status(thm)],[u5,d1]) ).
cnf(goal_0,negated_conjecture,
addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(definition_unfolding,[status(thm)],[u4,d0,d5]) ).
cnf(g0_0,plain,
addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF0))),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[goal_0,t44]) ).
cnf(g0_1,plain,
addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF1)),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_0,t52]) ).
cnf(g0_2,plain,
addition(coantidomain(coantidomain(multiplication(coantidomain(sF0),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_1,t10415]) ).
cnf(g0_3,plain,
addition(coantidomain(coantidomain(multiplication(sF1,sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_2,t10507]) ).
cnf(g0_4,plain,
addition(coantidomain(coantidomain(sF18)),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_3,t10579]) ).
cnf(g0_5,plain,
addition(coantidomain(sF19),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_4,t901]) ).
cnf(g0_6,plain,
addition(sF20,antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_5,t931]) ).
cnf(g0_7,plain,
addition(sF20,antidomain(sF2)) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_6,t45]) ).
cnf(g0_8,plain,
addition(sF20,sF3) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_7,t53]) ).
cnf(g0_9,plain,
addition(sF3,sF20) != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_8,t73]) ).
cnf(g0_10,plain,
sF3 != antidomain(antidomain(sK1_goals_X2)),
inference(rw,[status(thm)],[g0_9,t22193]) ).
cnf(g0_11,plain,
sF3 != antidomain(sF2),
inference(rw,[status(thm)],[g0_10,t45]) ).
cnf(g0_12,plain,
sF3 != sF3,
inference(rw,[status(thm)],[g0_11,t53]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : KLE108-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.15/0.64 % Computer : n016.cluster.edu
% 0.15/0.64 % Model : x86_64 x86_64
% 0.15/0.64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.64 % Memory : 8046.5625MB
% 0.15/0.64 % OS : Linux 6.8.0-71-generic
% 0.15/0.64 % CPULimit : 300
% 0.15/0.64 % WCLimit : 300
% 0.15/0.64 % DateTime : Wed Sep 23 19:02:30 UTC 2026
% 0.15/0.64 % CPUTime :
% 0.15/0.65 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 50.30/7.02 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 50.30/7.02 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------