%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE104-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n018.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 89.60s 18.86s
% Output : CNFRefutation 89.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 53
% Syntax : Number of clauses : 670 ( 670 unt; 0 nHn; 535 RR)
% Number of literals : 670 ( 669 equ; 20 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 44 ( 44 usr; 33 con; 0-2 aty)
% Number of variables : 174 ( 15 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t22,axiom,
sF0 = antidomain(sK2_goals_X1),
introduced(definition) ).
cnf(t50,plain,
antidomain(sK2_goals_X1) = sF0,
inference(orient,[status(thm)],[t22]) ).
cnf(t23,axiom,
sF1 = antidomain(antidomain(sK2_goals_X1)),
introduced(definition) ).
cnf(t41673,plain,
sF1 = antidomain(sF0),
inference(step,[status(thm)],[t23,t50]) ).
cnf(t58,plain,
antidomain(sF0) = sF1,
inference(orient,[status(thm)],[t41673]) ).
cnf(t38,axiom,
sF16 = antidomain(antidomain(antidomain(sK2_goals_X1))),
introduced(definition) ).
cnf(t41677,plain,
sF16 = antidomain(antidomain(sF0)),
inference(step,[status(thm)],[t38,t50]) ).
cnf(t41678,plain,
sF16 = antidomain(sF1),
inference(step,[status(thm)],[t41677,t58]) ).
cnf(t77,plain,
antidomain(sF1) = sF16,
inference(orient,[status(thm)],[t41678]) ).
cnf(t18,axiom,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t287,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t7,axiom,
multiplication(antidomain(X1),X1) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t63,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t7]) ).
cnf(t67,plain,
zero = multiplication(sF1,sF0),
inference(cp,[status(thm)],[t63,t58]) ).
cnf(t72,plain,
multiplication(sF1,sF0) = zero,
inference(orient,[status(thm)],[t67]) ).
cnf(t298,plain,
multiplication(addition(sF1,X1),sF0) = addition(zero,multiplication(X1,sF0)),
inference(cp,[status(thm)],[t287,t72]) ).
cnf(t8,axiom,
addition(X1,X2) = addition(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t79,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(t53,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t80,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t79,t53]) ).
cnf(t82,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t80]) ).
cnf(t42109,plain,
multiplication(addition(sF1,X1),sF0) = multiplication(X1,sF0),
inference(step,[status(thm)],[t298,t82]) ).
cnf(t2140,plain,
multiplication(addition(sF1,X1),sF0) = multiplication(X1,sF0),
inference(orient,[status(thm)],[t42109]) ).
cnf(t11,axiom,
addition(antidomain(antidomain(X1)),antidomain(X1)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t41685,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t11,t79]) ).
cnf(t108,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(orient,[status(thm)],[t41685]) ).
cnf(t111,plain,
one = addition(sF1,antidomain(antidomain(sF0))),
inference(cp,[status(thm)],[t108,t58]) ).
cnf(t41692,plain,
one = addition(sF1,antidomain(sF1)),
inference(step,[status(thm)],[t111,t58]) ).
cnf(t41693,plain,
one = addition(sF1,sF16),
inference(step,[status(thm)],[t41692,t77]) ).
cnf(t127,plain,
addition(sF1,sF16) = one,
inference(orient,[status(thm)],[t41693]) ).
cnf(t2141,plain,
multiplication(sF16,sF0) = multiplication(one,sF0),
inference(cp,[status(thm)],[t2140,t127]) ).
cnf(t17,axiom,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t242,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t17]) ).
cnf(t78,plain,
zero = multiplication(sF16,sF1),
inference(cp,[status(thm)],[t63,t77]) ).
cnf(t81,plain,
multiplication(sF16,sF1) = zero,
inference(orient,[status(thm)],[t78]) ).
cnf(t261,plain,
multiplication(sF16,addition(X1,sF1)) = addition(multiplication(sF16,X1),zero),
inference(cp,[status(thm)],[t242,t81]) ).
cnf(t42065,plain,
multiplication(sF16,addition(X1,sF1)) = multiplication(sF16,X1),
inference(step,[status(thm)],[t261,t53]) ).
cnf(t1721,plain,
multiplication(sF16,addition(X1,sF1)) = multiplication(sF16,X1),
inference(orient,[status(thm)],[t42065]) ).
cnf(t109,plain,
one = addition(sF0,antidomain(antidomain(sK2_goals_X1))),
inference(cp,[status(thm)],[t108,t50]) ).
cnf(t41688,plain,
one = addition(sF0,antidomain(sF0)),
inference(step,[status(thm)],[t109,t50]) ).
cnf(t41689,plain,
one = addition(sF0,sF1),
inference(step,[status(thm)],[t41688,t58]) ).
cnf(t121,plain,
addition(sF0,sF1) = one,
inference(orient,[status(thm)],[t41689]) ).
cnf(t1723,plain,
multiplication(sF16,sF0) = multiplication(sF16,one),
inference(cp,[status(thm)],[t1721,t121]) ).
cnf(t2,axiom,
multiplication(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t54,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t42066,plain,
multiplication(sF16,sF0) = sF16,
inference(step,[status(thm)],[t1723,t54]) ).
cnf(t1730,plain,
multiplication(sF16,sF0) = sF16,
inference(orient,[status(thm)],[t42066]) ).
cnf(t42110,plain,
sF16 = multiplication(one,sF0),
inference(step,[status(thm)],[t2141,t1730]) ).
cnf(t4,axiom,
multiplication(one,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t56,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t42111,plain,
sF16 = sF0,
inference(step,[status(thm)],[t42110,t56]) ).
cnf(t2153,plain,
sF16 = sF0,
inference(orient,[status(thm)],[t42111]) ).
cnf(t42112,plain,
antidomain(sF1) = sF0,
inference(step,[status(thm)],[t77,t2153]) ).
cnf(t2154,plain,
antidomain(sF1) = sF0,
inference(orient,[status(thm)],[t42112]) ).
cnf(t43,axiom,
sF21 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))),
introduced(definition) ).
cnf(t41941,plain,
sF21 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0))))))),
inference(step,[status(thm)],[t43,t50]) ).
cnf(t41942,plain,
sF21 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1)))))),
inference(step,[status(thm)],[t41941,t58]) ).
cnf(t41943,plain,
sF21 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF16))))),
inference(step,[status(thm)],[t41942,t77]) ).
cnf(t39,axiom,
sF17 = antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))),
introduced(definition) ).
cnf(t41682,plain,
sF17 = antidomain(antidomain(antidomain(sF0))),
inference(step,[status(thm)],[t39,t50]) ).
cnf(t41683,plain,
sF17 = antidomain(antidomain(sF1)),
inference(step,[status(thm)],[t41682,t58]) ).
cnf(t41684,plain,
sF17 = antidomain(sF16),
inference(step,[status(thm)],[t41683,t77]) ).
cnf(t104,plain,
antidomain(sF16) = sF17,
inference(orient,[status(thm)],[t41684]) ).
cnf(t41944,plain,
sF21 = multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF17)))),
inference(step,[status(thm)],[t41943,t104]) ).
cnf(t40,axiom,
sF18 = antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))),
introduced(definition) ).
cnf(t41911,plain,
sF18 = antidomain(antidomain(antidomain(antidomain(sF0)))),
inference(step,[status(thm)],[t40,t50]) ).
cnf(t41912,plain,
sF18 = antidomain(antidomain(antidomain(sF1))),
inference(step,[status(thm)],[t41911,t58]) ).
cnf(t41913,plain,
sF18 = antidomain(antidomain(sF16)),
inference(step,[status(thm)],[t41912,t77]) ).
cnf(t41914,plain,
sF18 = antidomain(sF17),
inference(step,[status(thm)],[t41913,t104]) ).
cnf(t877,plain,
antidomain(sF17) = sF18,
inference(orient,[status(thm)],[t41914]) ).
cnf(t41945,plain,
sF21 = multiplication(sK3_goals_X0,antidomain(antidomain(sF18))),
inference(step,[status(thm)],[t41944,t877]) ).
cnf(t41,axiom,
sF19 = antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))),
introduced(definition) ).
cnf(t41919,plain,
sF19 = antidomain(antidomain(antidomain(antidomain(antidomain(sF0))))),
inference(step,[status(thm)],[t41,t50]) ).
cnf(t41920,plain,
sF19 = antidomain(antidomain(antidomain(antidomain(sF1)))),
inference(step,[status(thm)],[t41919,t58]) ).
cnf(t41921,plain,
sF19 = antidomain(antidomain(antidomain(sF16))),
inference(step,[status(thm)],[t41920,t77]) ).
cnf(t41922,plain,
sF19 = antidomain(antidomain(sF17)),
inference(step,[status(thm)],[t41921,t104]) ).
cnf(t41923,plain,
sF19 = antidomain(sF18),
inference(step,[status(thm)],[t41922,t877]) ).
cnf(t904,plain,
antidomain(sF18) = sF19,
inference(orient,[status(thm)],[t41923]) ).
cnf(t41946,plain,
sF21 = multiplication(sK3_goals_X0,antidomain(sF19)),
inference(step,[status(thm)],[t41945,t904]) ).
cnf(t42,axiom,
sF20 = antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))),
introduced(definition) ).
cnf(t41930,plain,
sF20 = antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0)))))),
inference(step,[status(thm)],[t42,t50]) ).
cnf(t41931,plain,
sF20 = antidomain(antidomain(antidomain(antidomain(antidomain(sF1))))),
inference(step,[status(thm)],[t41930,t58]) ).
cnf(t41932,plain,
sF20 = antidomain(antidomain(antidomain(antidomain(sF16)))),
inference(step,[status(thm)],[t41931,t77]) ).
cnf(t41933,plain,
sF20 = antidomain(antidomain(antidomain(sF17))),
inference(step,[status(thm)],[t41932,t104]) ).
cnf(t41934,plain,
sF20 = antidomain(antidomain(sF18)),
inference(step,[status(thm)],[t41933,t877]) ).
cnf(t41935,plain,
sF20 = antidomain(sF19),
inference(step,[status(thm)],[t41934,t904]) ).
cnf(t935,plain,
antidomain(sF19) = sF20,
inference(orient,[status(thm)],[t41935]) ).
cnf(t41947,plain,
sF21 = multiplication(sK3_goals_X0,sF20),
inference(step,[status(thm)],[t41946,t935]) ).
cnf(t965,plain,
multiplication(sK3_goals_X0,sF20) = sF21,
inference(orient,[status(thm)],[t41947]) ).
cnf(t2218,plain,
antidomain(sF1) = sF20,
inference(rw,[status(thm)],[t935]) ).
cnf(t42131,plain,
sF0 = sF20,
inference(step,[status(thm)],[t2218,t2154]) ).
cnf(t2221,plain,
sF20 = sF0,
inference(orient,[status(thm)],[t42131]) ).
cnf(t42132,plain,
multiplication(sK3_goals_X0,sF0) = sF21,
inference(step,[status(thm)],[t965,t2221]) ).
cnf(t2225,plain,
multiplication(sK3_goals_X0,sF0) = sF21,
inference(rw,[status(thm)],[t42132]) ).
cnf(t2343,plain,
multiplication(sK3_goals_X0,sF0) = sF21,
inference(orient,[status(thm)],[t2225]) ).
cnf(t44,axiom,
sF22 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))))),
introduced(definition) ).
cnf(t41948,plain,
sF22 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0)))))))),
inference(step,[status(thm)],[t44,t50]) ).
cnf(t41949,plain,
sF22 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1))))))),
inference(step,[status(thm)],[t41948,t58]) ).
cnf(t41950,plain,
sF22 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF16)))))),
inference(step,[status(thm)],[t41949,t77]) ).
cnf(t41951,plain,
sF22 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF17))))),
inference(step,[status(thm)],[t41950,t104]) ).
cnf(t41952,plain,
sF22 = antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF18)))),
inference(step,[status(thm)],[t41951,t877]) ).
cnf(t41953,plain,
sF22 = antidomain(multiplication(sK3_goals_X0,antidomain(sF19))),
inference(step,[status(thm)],[t41952,t904]) ).
cnf(t41954,plain,
sF22 = antidomain(multiplication(sK3_goals_X0,sF20)),
inference(step,[status(thm)],[t41953,t935]) ).
cnf(t41955,plain,
sF22 = antidomain(sF21),
inference(step,[status(thm)],[t41954,t965]) ).
cnf(t1000,plain,
antidomain(sF21) = sF22,
inference(orient,[status(thm)],[t41955]) ).
cnf(t45,axiom,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))),
introduced(definition) ).
cnf(t41959,plain,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0))))))))),
inference(step,[status(thm)],[t45,t50]) ).
cnf(t41960,plain,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1)))))))),
inference(step,[status(thm)],[t41959,t58]) ).
cnf(t41961,plain,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF16))))))),
inference(step,[status(thm)],[t41960,t77]) ).
cnf(t41962,plain,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF17)))))),
inference(step,[status(thm)],[t41961,t104]) ).
cnf(t41963,plain,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF18))))),
inference(step,[status(thm)],[t41962,t877]) ).
cnf(t41964,plain,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF19)))),
inference(step,[status(thm)],[t41963,t904]) ).
cnf(t41965,plain,
sF23 = antidomain(antidomain(multiplication(sK3_goals_X0,sF20))),
inference(step,[status(thm)],[t41964,t935]) ).
cnf(t41966,plain,
sF23 = antidomain(antidomain(sF21)),
inference(step,[status(thm)],[t41965,t965]) ).
cnf(t41967,plain,
sF23 = antidomain(sF22),
inference(step,[status(thm)],[t41966,t1000]) ).
cnf(t1030,plain,
antidomain(sF22) = sF23,
inference(orient,[status(thm)],[t41967]) ).
cnf(t46,axiom,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))))))),
introduced(definition) ).
cnf(t41972,plain,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0)))))))))),
inference(step,[status(thm)],[t46,t50]) ).
cnf(t41973,plain,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1))))))))),
inference(step,[status(thm)],[t41972,t58]) ).
cnf(t41974,plain,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF16)))))))),
inference(step,[status(thm)],[t41973,t77]) ).
cnf(t41975,plain,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF17))))))),
inference(step,[status(thm)],[t41974,t104]) ).
cnf(t41976,plain,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF18)))))),
inference(step,[status(thm)],[t41975,t877]) ).
cnf(t41977,plain,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF19))))),
inference(step,[status(thm)],[t41976,t904]) ).
cnf(t41978,plain,
sF24 = antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF20)))),
inference(step,[status(thm)],[t41977,t935]) ).
cnf(t41979,plain,
sF24 = antidomain(antidomain(antidomain(sF21))),
inference(step,[status(thm)],[t41978,t965]) ).
cnf(t41980,plain,
sF24 = antidomain(antidomain(sF22)),
inference(step,[status(thm)],[t41979,t1000]) ).
cnf(t41981,plain,
sF24 = antidomain(sF23),
inference(step,[status(thm)],[t41980,t1030]) ).
cnf(t1062,plain,
antidomain(sF23) = sF24,
inference(orient,[status(thm)],[t41981]) ).
cnf(t1032,plain,
zero = multiplication(sF23,sF22),
inference(cp,[status(thm)],[t63,t1030]) ).
cnf(t1042,plain,
multiplication(sF23,sF22) = zero,
inference(orient,[status(thm)],[t1032]) ).
cnf(t1046,plain,
multiplication(addition(sF23,X1),sF22) = addition(zero,multiplication(X1,sF22)),
inference(cp,[status(thm)],[t287,t1042]) ).
cnf(t42482,plain,
multiplication(addition(sF23,X1),sF22) = multiplication(X1,sF22),
inference(step,[status(thm)],[t1046,t82]) ).
cnf(t9554,plain,
multiplication(addition(sF23,X1),sF22) = multiplication(X1,sF22),
inference(orient,[status(thm)],[t42482]) ).
cnf(t1033,plain,
one = addition(sF23,antidomain(antidomain(sF22))),
inference(cp,[status(thm)],[t108,t1030]) ).
cnf(t41971,plain,
one = addition(sF23,antidomain(sF23)),
inference(step,[status(thm)],[t1033,t1030]) ).
cnf(t1056,plain,
addition(sF23,antidomain(sF23)) = one,
inference(orient,[status(thm)],[t41971]) ).
cnf(t41982,plain,
addition(sF23,sF24) = one,
inference(step,[status(thm)],[t1056,t1062]) ).
cnf(t1063,plain,
addition(sF23,sF24) = one,
inference(rw,[status(thm)],[t41982]) ).
cnf(t1068,plain,
addition(sF23,sF24) = one,
inference(orient,[status(thm)],[t1063]) ).
cnf(t9555,plain,
multiplication(sF24,sF22) = multiplication(one,sF22),
inference(cp,[status(thm)],[t9554,t1068]) ).
cnf(t248,plain,
multiplication(antidomain(X1),addition(X2,X1)) = addition(multiplication(antidomain(X1),X2),zero),
inference(cp,[status(thm)],[t242,t63]) ).
cnf(t42287,plain,
multiplication(antidomain(X1),addition(X2,X1)) = multiplication(antidomain(X1),X2),
inference(step,[status(thm)],[t248,t53]) ).
cnf(t4089,plain,
multiplication(antidomain(X1),addition(X2,X1)) = multiplication(antidomain(X1),X2),
inference(orient,[status(thm)],[t42287]) ).
cnf(t1002,plain,
one = addition(sF22,antidomain(antidomain(sF21))),
inference(cp,[status(thm)],[t108,t1000]) ).
cnf(t41958,plain,
one = addition(sF22,antidomain(sF22)),
inference(step,[status(thm)],[t1002,t1000]) ).
cnf(t1019,plain,
addition(sF22,antidomain(sF22)) = one,
inference(orient,[status(thm)],[t41958]) ).
cnf(t41968,plain,
addition(sF22,sF23) = one,
inference(step,[status(thm)],[t1019,t1030]) ).
cnf(t1031,plain,
addition(sF22,sF23) = one,
inference(rw,[status(thm)],[t41968]) ).
cnf(t1036,plain,
addition(sF22,sF23) = one,
inference(orient,[status(thm)],[t1031]) ).
cnf(t4109,plain,
multiplication(antidomain(sF23),sF22) = multiplication(antidomain(sF23),one),
inference(cp,[status(thm)],[t4089,t1036]) ).
cnf(t42288,plain,
multiplication(sF24,sF22) = multiplication(antidomain(sF23),one),
inference(step,[status(thm)],[t4109,t1062]) ).
cnf(t42289,plain,
multiplication(sF24,sF22) = antidomain(sF23),
inference(step,[status(thm)],[t42288,t54]) ).
cnf(t42290,plain,
multiplication(sF24,sF22) = sF24,
inference(step,[status(thm)],[t42289,t1062]) ).
cnf(t4147,plain,
multiplication(sF24,sF22) = sF24,
inference(orient,[status(thm)],[t42290]) ).
cnf(t42483,plain,
sF24 = multiplication(one,sF22),
inference(step,[status(thm)],[t9555,t4147]) ).
cnf(t42484,plain,
sF24 = sF22,
inference(step,[status(thm)],[t42483,t56]) ).
cnf(t9579,plain,
sF24 = sF22,
inference(orient,[status(thm)],[t42484]) ).
cnf(t42485,plain,
antidomain(sF23) = sF22,
inference(step,[status(thm)],[t1062,t9579]) ).
cnf(t9580,plain,
antidomain(sF23) = sF22,
inference(orient,[status(thm)],[t42485]) ).
cnf(t24,axiom,
sF2 = antidomain(sK1_goals_X2),
introduced(definition) ).
cnf(t51,plain,
antidomain(sK1_goals_X2) = sF2,
inference(orient,[status(thm)],[t24]) ).
cnf(t25,axiom,
sF3 = antidomain(antidomain(sK1_goals_X2)),
introduced(definition) ).
cnf(t41674,plain,
sF3 = antidomain(sF2),
inference(step,[status(thm)],[t25,t51]) ).
cnf(t59,plain,
antidomain(sF2) = sF3,
inference(orient,[status(thm)],[t41674]) ).
cnf(t49,axiom,
sF27 = addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))))))))),antidomain(antidomain(sK1_goals_X2))),
introduced(definition) ).
cnf(t42017,plain,
sF27 = addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))),
inference(step,[status(thm)],[t49,t79]) ).
cnf(t42018,plain,
sF27 = addition(antidomain(sF2),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))),
inference(step,[status(thm)],[t42017,t51]) ).
cnf(t42019,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))),
inference(step,[status(thm)],[t42018,t59]) ).
cnf(t42020,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0))))))))))))),
inference(step,[status(thm)],[t42019,t50]) ).
cnf(t42021,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1)))))))))))),
inference(step,[status(thm)],[t42020,t58]) ).
cnf(t42022,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF16))))))))))),
inference(step,[status(thm)],[t42021,t77]) ).
cnf(t42023,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF17)))))))))),
inference(step,[status(thm)],[t42022,t104]) ).
cnf(t42024,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF18))))))))),
inference(step,[status(thm)],[t42023,t877]) ).
cnf(t42025,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF19)))))))),
inference(step,[status(thm)],[t42024,t904]) ).
cnf(t42026,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF20))))))),
inference(step,[status(thm)],[t42025,t935]) ).
cnf(t42027,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(antidomain(sF21)))))),
inference(step,[status(thm)],[t42026,t965]) ).
cnf(t42028,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(antidomain(sF22))))),
inference(step,[status(thm)],[t42027,t1000]) ).
cnf(t42029,plain,
sF27 = addition(sF3,antidomain(antidomain(antidomain(sF23)))),
inference(step,[status(thm)],[t42028,t1030]) ).
cnf(t42030,plain,
sF27 = addition(sF3,antidomain(antidomain(sF24))),
inference(step,[status(thm)],[t42029,t1062]) ).
cnf(t47,axiom,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))),
introduced(definition) ).
cnf(t41986,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0))))))))))),
inference(step,[status(thm)],[t47,t50]) ).
cnf(t41987,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1)))))))))),
inference(step,[status(thm)],[t41986,t58]) ).
cnf(t41988,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF16))))))))),
inference(step,[status(thm)],[t41987,t77]) ).
cnf(t41989,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF17)))))))),
inference(step,[status(thm)],[t41988,t104]) ).
cnf(t41990,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF18))))))),
inference(step,[status(thm)],[t41989,t877]) ).
cnf(t41991,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF19)))))),
inference(step,[status(thm)],[t41990,t904]) ).
cnf(t41992,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF20))))),
inference(step,[status(thm)],[t41991,t935]) ).
cnf(t41993,plain,
sF25 = antidomain(antidomain(antidomain(antidomain(sF21)))),
inference(step,[status(thm)],[t41992,t965]) ).
cnf(t41994,plain,
sF25 = antidomain(antidomain(antidomain(sF22))),
inference(step,[status(thm)],[t41993,t1000]) ).
cnf(t41995,plain,
sF25 = antidomain(antidomain(sF23)),
inference(step,[status(thm)],[t41994,t1030]) ).
cnf(t41996,plain,
sF25 = antidomain(sF24),
inference(step,[status(thm)],[t41995,t1062]) ).
cnf(t1094,plain,
antidomain(sF24) = sF25,
inference(orient,[status(thm)],[t41996]) ).
cnf(t42031,plain,
sF27 = addition(sF3,antidomain(sF25)),
inference(step,[status(thm)],[t42030,t1094]) ).
cnf(t48,axiom,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))))))))),
introduced(definition) ).
cnf(t42001,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0)))))))))))),
inference(step,[status(thm)],[t48,t50]) ).
cnf(t42002,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1))))))))))),
inference(step,[status(thm)],[t42001,t58]) ).
cnf(t42003,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF16)))))))))),
inference(step,[status(thm)],[t42002,t77]) ).
cnf(t42004,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF17))))))))),
inference(step,[status(thm)],[t42003,t104]) ).
cnf(t42005,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF18)))))))),
inference(step,[status(thm)],[t42004,t877]) ).
cnf(t42006,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF19))))))),
inference(step,[status(thm)],[t42005,t904]) ).
cnf(t42007,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF20)))))),
inference(step,[status(thm)],[t42006,t935]) ).
cnf(t42008,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(antidomain(sF21))))),
inference(step,[status(thm)],[t42007,t965]) ).
cnf(t42009,plain,
sF26 = antidomain(antidomain(antidomain(antidomain(sF22)))),
inference(step,[status(thm)],[t42008,t1000]) ).
cnf(t42010,plain,
sF26 = antidomain(antidomain(antidomain(sF23))),
inference(step,[status(thm)],[t42009,t1030]) ).
cnf(t42011,plain,
sF26 = antidomain(antidomain(sF24)),
inference(step,[status(thm)],[t42010,t1062]) ).
cnf(t42012,plain,
sF26 = antidomain(sF25),
inference(step,[status(thm)],[t42011,t1094]) ).
cnf(t1126,plain,
antidomain(sF25) = sF26,
inference(orient,[status(thm)],[t42012]) ).
cnf(t42032,plain,
sF27 = addition(sF3,sF26),
inference(step,[status(thm)],[t42031,t1126]) ).
cnf(t1158,plain,
addition(sF3,sF26) = sF27,
inference(orient,[status(thm)],[t42032]) ).
cnf(t9613,plain,
antidomain(sF23) = sF26,
inference(rw,[status(thm)],[t1126]) ).
cnf(t42504,plain,
sF22 = sF26,
inference(step,[status(thm)],[t9613,t9580]) ).
cnf(t9630,plain,
sF26 = sF22,
inference(orient,[status(thm)],[t42504]) ).
cnf(t42505,plain,
addition(sF3,sF22) = sF27,
inference(step,[status(thm)],[t1158,t9630]) ).
cnf(t9634,plain,
addition(sF3,sF22) = sF27,
inference(rw,[status(thm)],[t42505]) ).
cnf(t9720,plain,
addition(sF3,sF22) = sF27,
inference(orient,[status(thm)],[t9634]) ).
cnf(t288,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t287,t56]) ).
cnf(t1817,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t288]) ).
cnf(t26,axiom,
sF4 = antidomain(antidomain(antidomain(sK1_goals_X2))),
introduced(definition) ).
cnf(t41675,plain,
sF4 = antidomain(antidomain(sF2)),
inference(step,[status(thm)],[t26,t51]) ).
cnf(t41676,plain,
sF4 = antidomain(sF3),
inference(step,[status(thm)],[t41675,t59]) ).
cnf(t74,plain,
antidomain(sF3) = sF4,
inference(orient,[status(thm)],[t41676]) ).
cnf(t75,plain,
zero = multiplication(sF4,sF3),
inference(cp,[status(thm)],[t63,t74]) ).
cnf(t76,plain,
multiplication(sF4,sF3) = zero,
inference(orient,[status(thm)],[t75]) ).
cnf(t257,plain,
multiplication(sF4,addition(sF3,X1)) = addition(zero,multiplication(sF4,X1)),
inference(cp,[status(thm)],[t242,t76]) ).
cnf(t42059,plain,
multiplication(sF4,addition(sF3,X1)) = multiplication(sF4,X1),
inference(step,[status(thm)],[t257,t82]) ).
cnf(t1624,plain,
multiplication(sF4,addition(sF3,X1)) = multiplication(sF4,X1),
inference(orient,[status(thm)],[t42059]) ).
cnf(t1627,plain,
multiplication(sF4,sF26) = multiplication(sF4,sF27),
inference(cp,[status(thm)],[t1624,t1158]) ).
cnf(t1642,plain,
multiplication(sF4,sF27) = multiplication(sF4,sF26),
inference(orient,[status(thm)],[t1627]) ).
cnf(t2394,plain,
multiplication(sF2,sF27) = multiplication(sF4,sF26),
inference(rw,[status(thm)],[t1642]) ).
cnf(t68,plain,
zero = multiplication(sF3,sF2),
inference(cp,[status(thm)],[t63,t59]) ).
cnf(t73,plain,
multiplication(sF3,sF2) = zero,
inference(orient,[status(thm)],[t68]) ).
cnf(t300,plain,
multiplication(addition(sF3,X1),sF2) = addition(zero,multiplication(X1,sF2)),
inference(cp,[status(thm)],[t287,t73]) ).
cnf(t42138,plain,
multiplication(addition(sF3,X1),sF2) = multiplication(X1,sF2),
inference(step,[status(thm)],[t300,t82]) ).
cnf(t2361,plain,
multiplication(addition(sF3,X1),sF2) = multiplication(X1,sF2),
inference(orient,[status(thm)],[t42138]) ).
cnf(t112,plain,
one = addition(sF3,antidomain(antidomain(sF2))),
inference(cp,[status(thm)],[t108,t59]) ).
cnf(t41694,plain,
one = addition(sF3,antidomain(sF3)),
inference(step,[status(thm)],[t112,t59]) ).
cnf(t41695,plain,
one = addition(sF3,sF4),
inference(step,[status(thm)],[t41694,t74]) ).
cnf(t130,plain,
addition(sF3,sF4) = one,
inference(orient,[status(thm)],[t41695]) ).
cnf(t2362,plain,
multiplication(sF4,sF2) = multiplication(one,sF2),
inference(cp,[status(thm)],[t2361,t130]) ).
cnf(t258,plain,
multiplication(sF4,addition(X1,sF3)) = addition(multiplication(sF4,X1),zero),
inference(cp,[status(thm)],[t242,t76]) ).
cnf(t42061,plain,
multiplication(sF4,addition(X1,sF3)) = multiplication(sF4,X1),
inference(step,[status(thm)],[t258,t53]) ).
cnf(t1650,plain,
multiplication(sF4,addition(X1,sF3)) = multiplication(sF4,X1),
inference(orient,[status(thm)],[t42061]) ).
cnf(t110,plain,
one = addition(sF2,antidomain(antidomain(sK1_goals_X2))),
inference(cp,[status(thm)],[t108,t51]) ).
cnf(t41690,plain,
one = addition(sF2,antidomain(sF2)),
inference(step,[status(thm)],[t110,t51]) ).
cnf(t41691,plain,
one = addition(sF2,sF3),
inference(step,[status(thm)],[t41690,t59]) ).
cnf(t124,plain,
addition(sF2,sF3) = one,
inference(orient,[status(thm)],[t41691]) ).
cnf(t1652,plain,
multiplication(sF4,sF2) = multiplication(sF4,one),
inference(cp,[status(thm)],[t1650,t124]) ).
cnf(t42062,plain,
multiplication(sF4,sF2) = sF4,
inference(step,[status(thm)],[t1652,t54]) ).
cnf(t1685,plain,
multiplication(sF4,sF2) = sF4,
inference(orient,[status(thm)],[t42062]) ).
cnf(t42139,plain,
sF4 = multiplication(one,sF2),
inference(step,[status(thm)],[t2362,t1685]) ).
cnf(t42140,plain,
sF4 = sF2,
inference(step,[status(thm)],[t42139,t56]) ).
cnf(t2375,plain,
sF4 = sF2,
inference(orient,[status(thm)],[t42140]) ).
cnf(t42158,plain,
multiplication(sF2,sF27) = multiplication(sF2,sF26),
inference(step,[status(thm)],[t2394,t2375]) ).
cnf(t2441,plain,
multiplication(sF2,sF27) = multiplication(sF2,sF26),
inference(orient,[status(thm)],[t42158]) ).
cnf(t2450,plain,
multiplication(addition(one,sF2),sF27) = addition(sF27,multiplication(sF2,sF26)),
inference(cp,[status(thm)],[t1817,t2441]) ).
cnf(t289,plain,
multiplication(addition(X1,one),X2) = addition(multiplication(X1,X2),X2),
inference(cp,[status(thm)],[t287,t56]) ).
cnf(t42076,plain,
multiplication(addition(X1,one),X2) = addition(X2,multiplication(X1,X2)),
inference(step,[status(thm)],[t289,t79]) ).
cnf(t42077,plain,
multiplication(addition(X1,one),X2) = multiplication(addition(one,X1),X2),
inference(step,[status(thm)],[t42076,t1817]) ).
cnf(t1920,plain,
multiplication(addition(X1,one),X2) = multiplication(addition(one,X1),X2),
inference(orient,[status(thm)],[t42077]) ).
cnf(t42706,plain,
multiplication(addition(sF2,one),sF27) = addition(sF27,multiplication(sF2,sF26)),
inference(step,[status(thm)],[t2450,t1920]) ).
cnf(t13,axiom,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t85,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(t52,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t87,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t85,t52]) ).
cnf(t150,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t87]) ).
cnf(t155,plain,
addition(sF2,sF3) = addition(sF2,one),
inference(cp,[status(thm)],[t150,t124]) ).
cnf(t41706,plain,
one = addition(sF2,one),
inference(step,[status(thm)],[t155,t124]) ).
cnf(t184,plain,
addition(sF2,one) = one,
inference(orient,[status(thm)],[t41706]) ).
cnf(t42707,plain,
multiplication(one,sF27) = addition(sF27,multiplication(sF2,sF26)),
inference(step,[status(thm)],[t42706,t184]) ).
cnf(t42708,plain,
sF27 = addition(sF27,multiplication(sF2,sF26)),
inference(step,[status(thm)],[t42707,t56]) ).
cnf(t42709,plain,
sF27 = addition(sF27,multiplication(sF2,sF22)),
inference(step,[status(thm)],[t42708,t9630]) ).
cnf(t14285,plain,
addition(sF27,multiplication(sF2,sF22)) = sF27,
inference(orient,[status(thm)],[t42709]) ).
cnf(t16,axiom,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t90,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t6,axiom,
multiplication(X1,coantidomain(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t60,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t29,axiom,
sF7 = coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))),
introduced(definition) ).
cnf(t41790,plain,
sF7 = coantidomain(antidomain(antidomain(antidomain(antidomain(sF2))))),
inference(step,[status(thm)],[t29,t51]) ).
cnf(t41791,plain,
sF7 = coantidomain(antidomain(antidomain(antidomain(sF3)))),
inference(step,[status(thm)],[t41790,t59]) ).
cnf(t41792,plain,
sF7 = coantidomain(antidomain(antidomain(sF4))),
inference(step,[status(thm)],[t41791,t74]) ).
cnf(t27,axiom,
sF5 = antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))),
introduced(definition) ).
cnf(t41679,plain,
sF5 = antidomain(antidomain(antidomain(sF2))),
inference(step,[status(thm)],[t27,t51]) ).
cnf(t41680,plain,
sF5 = antidomain(antidomain(sF3)),
inference(step,[status(thm)],[t41679,t59]) ).
cnf(t41681,plain,
sF5 = antidomain(sF4),
inference(step,[status(thm)],[t41680,t74]) ).
cnf(t100,plain,
antidomain(sF4) = sF5,
inference(orient,[status(thm)],[t41681]) ).
cnf(t41793,plain,
sF7 = coantidomain(antidomain(sF5)),
inference(step,[status(thm)],[t41792,t100]) ).
cnf(t28,axiom,
sF6 = antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))),
introduced(definition) ).
cnf(t41781,plain,
sF6 = antidomain(antidomain(antidomain(antidomain(sF2)))),
inference(step,[status(thm)],[t28,t51]) ).
cnf(t41782,plain,
sF6 = antidomain(antidomain(antidomain(sF3))),
inference(step,[status(thm)],[t41781,t59]) ).
cnf(t41783,plain,
sF6 = antidomain(antidomain(sF4)),
inference(step,[status(thm)],[t41782,t74]) ).
cnf(t41784,plain,
sF6 = antidomain(sF5),
inference(step,[status(thm)],[t41783,t100]) ).
cnf(t538,plain,
antidomain(sF5) = sF6,
inference(orient,[status(thm)],[t41784]) ).
cnf(t41794,plain,
sF7 = coantidomain(sF6),
inference(step,[status(thm)],[t41793,t538]) ).
cnf(t569,plain,
coantidomain(sF6) = sF7,
inference(orient,[status(thm)],[t41794]) ).
cnf(t570,plain,
zero = multiplication(sF6,sF7),
inference(cp,[status(thm)],[t60,t569]) ).
cnf(t574,plain,
multiplication(sF6,sF7) = zero,
inference(orient,[status(thm)],[t570]) ).
cnf(t2406,plain,
antidomain(sF3) = sF6,
inference(rw,[status(thm)],[t538]) ).
cnf(t42141,plain,
antidomain(sF3) = sF2,
inference(step,[status(thm)],[t74,t2375]) ).
cnf(t2376,plain,
antidomain(sF3) = sF2,
inference(orient,[status(thm)],[t42141]) ).
cnf(t42154,plain,
sF2 = sF6,
inference(step,[status(thm)],[t2406,t2376]) ).
cnf(t2413,plain,
sF6 = sF2,
inference(orient,[status(thm)],[t42154]) ).
cnf(t42156,plain,
multiplication(sF2,sF7) = zero,
inference(step,[status(thm)],[t574,t2413]) ).
cnf(t2418,plain,
multiplication(sF2,sF7) = zero,
inference(rw,[status(thm)],[t42156]) ).
cnf(t2535,plain,
multiplication(sF2,sF7) = zero,
inference(orient,[status(thm)],[t2418]) ).
cnf(t2536,plain,
multiplication(sF2,addition(sF7,X1)) = addition(zero,multiplication(sF2,X1)),
inference(cp,[status(thm)],[t242,t2535]) ).
cnf(t42710,plain,
multiplication(sF2,addition(sF7,X1)) = multiplication(sF2,X1),
inference(step,[status(thm)],[t2536,t82]) ).
cnf(t14310,plain,
multiplication(sF2,addition(sF7,X1)) = multiplication(sF2,X1),
inference(orient,[status(thm)],[t42710]) ).
cnf(t12,axiom,
addition(coantidomain(coantidomain(X1)),coantidomain(X1)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t41700,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(step,[status(thm)],[t12,t79]) ).
cnf(t139,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t41700]) ).
cnf(t571,plain,
one = addition(sF7,coantidomain(coantidomain(sF6))),
inference(cp,[status(thm)],[t139,t569]) ).
cnf(t41797,plain,
one = addition(sF7,coantidomain(sF7)),
inference(step,[status(thm)],[t571,t569]) ).
cnf(t588,plain,
addition(sF7,coantidomain(sF7)) = one,
inference(orient,[status(thm)],[t41797]) ).
cnf(t30,axiom,
sF8 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),
introduced(definition) ).
cnf(t41798,plain,
sF8 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),
inference(step,[status(thm)],[t30,t51]) ).
cnf(t41799,plain,
sF8 = coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),
inference(step,[status(thm)],[t41798,t59]) ).
cnf(t41800,plain,
sF8 = coantidomain(coantidomain(antidomain(antidomain(sF4)))),
inference(step,[status(thm)],[t41799,t74]) ).
cnf(t41801,plain,
sF8 = coantidomain(coantidomain(antidomain(sF5))),
inference(step,[status(thm)],[t41800,t100]) ).
cnf(t41802,plain,
sF8 = coantidomain(coantidomain(sF6)),
inference(step,[status(thm)],[t41801,t538]) ).
cnf(t41803,plain,
sF8 = coantidomain(sF7),
inference(step,[status(thm)],[t41802,t569]) ).
cnf(t610,plain,
coantidomain(sF7) = sF8,
inference(orient,[status(thm)],[t41803]) ).
cnf(t41804,plain,
addition(sF7,sF8) = one,
inference(step,[status(thm)],[t588,t610]) ).
cnf(t611,plain,
addition(sF7,sF8) = one,
inference(rw,[status(thm)],[t41804]) ).
cnf(t616,plain,
addition(sF7,sF8) = one,
inference(orient,[status(thm)],[t611]) ).
cnf(t14311,plain,
multiplication(sF2,sF8) = multiplication(sF2,one),
inference(cp,[status(thm)],[t14310,t616]) ).
cnf(t42711,plain,
multiplication(sF2,sF8) = sF2,
inference(step,[status(thm)],[t14311,t54]) ).
cnf(t14345,plain,
multiplication(sF2,sF8) = sF2,
inference(orient,[status(thm)],[t42711]) ).
cnf(t14346,plain,
multiplication(sF2,multiplication(sF8,X1)) = multiplication(sF2,X1),
inference(cp,[status(thm)],[t90,t14345]) ).
cnf(t24789,plain,
multiplication(sF2,multiplication(sF8,X1)) = multiplication(sF2,X1),
inference(orient,[status(thm)],[t14346]) ).
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(t336,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(orient,[status(thm)],[t19]) ).
cnf(t1004,plain,
antidomain(multiplication(X1,antidomain(antidomain(sF21)))) = addition(antidomain(multiplication(X1,sF21)),antidomain(multiplication(X1,antidomain(sF22)))),
inference(cp,[status(thm)],[t336,t1000]) ).
cnf(t43225,plain,
antidomain(multiplication(X1,antidomain(sF22))) = addition(antidomain(multiplication(X1,sF21)),antidomain(multiplication(X1,antidomain(sF22)))),
inference(step,[status(thm)],[t1004,t1000]) ).
cnf(t43226,plain,
antidomain(multiplication(X1,sF23)) = addition(antidomain(multiplication(X1,sF21)),antidomain(multiplication(X1,antidomain(sF22)))),
inference(step,[status(thm)],[t43225,t1030]) ).
cnf(t43227,plain,
antidomain(multiplication(X1,sF23)) = addition(antidomain(multiplication(X1,sF21)),antidomain(multiplication(X1,sF23))),
inference(step,[status(thm)],[t43226,t1030]) ).
cnf(t21274,plain,
addition(antidomain(multiplication(X1,sF21)),antidomain(multiplication(X1,sF23))) = antidomain(multiplication(X1,sF23)),
inference(orient,[status(thm)],[t43227]) ).
cnf(t32,axiom,
sF10 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)),
introduced(definition) ).
cnf(t41816,plain,
sF10 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0)),
inference(step,[status(thm)],[t32,t51]) ).
cnf(t41817,plain,
sF10 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0)),
inference(step,[status(thm)],[t41816,t59]) ).
cnf(t41818,plain,
sF10 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0)),
inference(step,[status(thm)],[t41817,t74]) ).
cnf(t41819,plain,
sF10 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0)),
inference(step,[status(thm)],[t41818,t100]) ).
cnf(t41820,plain,
sF10 = coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0)),
inference(step,[status(thm)],[t41819,t538]) ).
cnf(t41821,plain,
sF10 = coantidomain(multiplication(coantidomain(sF7),sK3_goals_X0)),
inference(step,[status(thm)],[t41820,t569]) ).
cnf(t41822,plain,
sF10 = coantidomain(multiplication(sF8,sK3_goals_X0)),
inference(step,[status(thm)],[t41821,t610]) ).
cnf(t31,axiom,
sF9 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0),
introduced(definition) ).
cnf(t41808,plain,
sF9 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0),
inference(step,[status(thm)],[t31,t51]) ).
cnf(t41809,plain,
sF9 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0),
inference(step,[status(thm)],[t41808,t59]) ).
cnf(t41810,plain,
sF9 = multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0),
inference(step,[status(thm)],[t41809,t74]) ).
cnf(t41811,plain,
sF9 = multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0),
inference(step,[status(thm)],[t41810,t100]) ).
cnf(t41812,plain,
sF9 = multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0),
inference(step,[status(thm)],[t41811,t538]) ).
cnf(t41813,plain,
sF9 = multiplication(coantidomain(sF7),sK3_goals_X0),
inference(step,[status(thm)],[t41812,t569]) ).
cnf(t41814,plain,
sF9 = multiplication(sF8,sK3_goals_X0),
inference(step,[status(thm)],[t41813,t610]) ).
cnf(t640,plain,
multiplication(sF8,sK3_goals_X0) = sF9,
inference(orient,[status(thm)],[t41814]) ).
cnf(t41823,plain,
sF10 = coantidomain(sF9),
inference(step,[status(thm)],[t41822,t640]) ).
cnf(t717,plain,
coantidomain(sF9) = sF10,
inference(orient,[status(thm)],[t41823]) ).
cnf(t718,plain,
zero = multiplication(sF9,sF10),
inference(cp,[status(thm)],[t60,t717]) ).
cnf(t727,plain,
multiplication(sF9,sF10) = zero,
inference(orient,[status(thm)],[t718]) ).
cnf(t728,plain,
multiplication(sF9,multiplication(sF10,X1)) = multiplication(zero,X1),
inference(cp,[status(thm)],[t90,t727]) ).
cnf(t5,axiom,
multiplication(zero,X1) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t57,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t42201,plain,
multiplication(sF9,multiplication(sF10,X1)) = zero,
inference(step,[status(thm)],[t728,t57]) ).
cnf(t3259,plain,
multiplication(sF9,multiplication(sF10,X1)) = zero,
inference(orient,[status(thm)],[t42201]) ).
cnf(t37,axiom,
sF15 = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
introduced(definition) ).
cnf(t41888,plain,
sF15 = addition(antidomain(sF0),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
inference(step,[status(thm)],[t37,t50]) ).
cnf(t41889,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
inference(step,[status(thm)],[t41888,t58]) ).
cnf(t41890,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0))))))),
inference(step,[status(thm)],[t41889,t51]) ).
cnf(t41891,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0))))))),
inference(step,[status(thm)],[t41890,t59]) ).
cnf(t41892,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0))))))),
inference(step,[status(thm)],[t41891,t74]) ).
cnf(t41893,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0))))))),
inference(step,[status(thm)],[t41892,t100]) ).
cnf(t41894,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0))))))),
inference(step,[status(thm)],[t41893,t538]) ).
cnf(t41895,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF7),sK3_goals_X0))))))),
inference(step,[status(thm)],[t41894,t569]) ).
cnf(t41896,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(sF8,sK3_goals_X0))))))),
inference(step,[status(thm)],[t41895,t610]) ).
cnf(t41897,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(sF9)))))),
inference(step,[status(thm)],[t41896,t640]) ).
cnf(t41898,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(sF10))))),
inference(step,[status(thm)],[t41897,t717]) ).
cnf(t33,axiom,
sF11 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))),
introduced(definition) ).
cnf(t41824,plain,
sF11 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0))),
inference(step,[status(thm)],[t33,t51]) ).
cnf(t41825,plain,
sF11 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0))),
inference(step,[status(thm)],[t41824,t59]) ).
cnf(t41826,plain,
sF11 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0))),
inference(step,[status(thm)],[t41825,t74]) ).
cnf(t41827,plain,
sF11 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0))),
inference(step,[status(thm)],[t41826,t100]) ).
cnf(t41828,plain,
sF11 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0))),
inference(step,[status(thm)],[t41827,t538]) ).
cnf(t41829,plain,
sF11 = coantidomain(coantidomain(multiplication(coantidomain(sF7),sK3_goals_X0))),
inference(step,[status(thm)],[t41828,t569]) ).
cnf(t41830,plain,
sF11 = coantidomain(coantidomain(multiplication(sF8,sK3_goals_X0))),
inference(step,[status(thm)],[t41829,t610]) ).
cnf(t41831,plain,
sF11 = coantidomain(coantidomain(sF9)),
inference(step,[status(thm)],[t41830,t640]) ).
cnf(t41832,plain,
sF11 = coantidomain(sF10),
inference(step,[status(thm)],[t41831,t717]) ).
cnf(t722,plain,
coantidomain(sF10) = sF11,
inference(orient,[status(thm)],[t41832]) ).
cnf(t41899,plain,
sF15 = addition(sF1,antidomain(antidomain(antidomain(sF11)))),
inference(step,[status(thm)],[t41898,t722]) ).
cnf(t34,axiom,
sF12 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))),
introduced(definition) ).
cnf(t41834,plain,
sF12 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0)))),
inference(step,[status(thm)],[t34,t51]) ).
cnf(t41835,plain,
sF12 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0)))),
inference(step,[status(thm)],[t41834,t59]) ).
cnf(t41836,plain,
sF12 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0)))),
inference(step,[status(thm)],[t41835,t74]) ).
cnf(t41837,plain,
sF12 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0)))),
inference(step,[status(thm)],[t41836,t100]) ).
cnf(t41838,plain,
sF12 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0)))),
inference(step,[status(thm)],[t41837,t538]) ).
cnf(t41839,plain,
sF12 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF7),sK3_goals_X0)))),
inference(step,[status(thm)],[t41838,t569]) ).
cnf(t41840,plain,
sF12 = antidomain(coantidomain(coantidomain(multiplication(sF8,sK3_goals_X0)))),
inference(step,[status(thm)],[t41839,t610]) ).
cnf(t41841,plain,
sF12 = antidomain(coantidomain(coantidomain(sF9))),
inference(step,[status(thm)],[t41840,t640]) ).
cnf(t41842,plain,
sF12 = antidomain(coantidomain(sF10)),
inference(step,[status(thm)],[t41841,t717]) ).
cnf(t41843,plain,
sF12 = antidomain(sF11),
inference(step,[status(thm)],[t41842,t722]) ).
cnf(t740,plain,
antidomain(sF11) = sF12,
inference(orient,[status(thm)],[t41843]) ).
cnf(t41900,plain,
sF15 = addition(sF1,antidomain(antidomain(sF12))),
inference(step,[status(thm)],[t41899,t740]) ).
cnf(t35,axiom,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))),
introduced(definition) ).
cnf(t41849,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0))))),
inference(step,[status(thm)],[t35,t51]) ).
cnf(t41850,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0))))),
inference(step,[status(thm)],[t41849,t59]) ).
cnf(t41851,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0))))),
inference(step,[status(thm)],[t41850,t74]) ).
cnf(t41852,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0))))),
inference(step,[status(thm)],[t41851,t100]) ).
cnf(t41853,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0))))),
inference(step,[status(thm)],[t41852,t538]) ).
cnf(t41854,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF7),sK3_goals_X0))))),
inference(step,[status(thm)],[t41853,t569]) ).
cnf(t41855,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(multiplication(sF8,sK3_goals_X0))))),
inference(step,[status(thm)],[t41854,t610]) ).
cnf(t41856,plain,
sF13 = antidomain(antidomain(coantidomain(coantidomain(sF9)))),
inference(step,[status(thm)],[t41855,t640]) ).
cnf(t41857,plain,
sF13 = antidomain(antidomain(coantidomain(sF10))),
inference(step,[status(thm)],[t41856,t717]) ).
cnf(t41858,plain,
sF13 = antidomain(antidomain(sF11)),
inference(step,[status(thm)],[t41857,t722]) ).
cnf(t41859,plain,
sF13 = antidomain(sF12),
inference(step,[status(thm)],[t41858,t740]) ).
cnf(t774,plain,
antidomain(sF12) = sF13,
inference(orient,[status(thm)],[t41859]) ).
cnf(t41901,plain,
sF15 = addition(sF1,antidomain(sF13)),
inference(step,[status(thm)],[t41900,t774]) ).
cnf(t36,axiom,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),
introduced(definition) ).
cnf(t41865,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0)))))),
inference(step,[status(thm)],[t36,t51]) ).
cnf(t41866,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0)))))),
inference(step,[status(thm)],[t41865,t59]) ).
cnf(t41867,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0)))))),
inference(step,[status(thm)],[t41866,t74]) ).
cnf(t41868,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0)))))),
inference(step,[status(thm)],[t41867,t100]) ).
cnf(t41869,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0)))))),
inference(step,[status(thm)],[t41868,t538]) ).
cnf(t41870,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF7),sK3_goals_X0)))))),
inference(step,[status(thm)],[t41869,t569]) ).
cnf(t41871,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(sF8,sK3_goals_X0)))))),
inference(step,[status(thm)],[t41870,t610]) ).
cnf(t41872,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(coantidomain(sF9))))),
inference(step,[status(thm)],[t41871,t640]) ).
cnf(t41873,plain,
sF14 = antidomain(antidomain(antidomain(coantidomain(sF10)))),
inference(step,[status(thm)],[t41872,t717]) ).
cnf(t41874,plain,
sF14 = antidomain(antidomain(antidomain(sF11))),
inference(step,[status(thm)],[t41873,t722]) ).
cnf(t41875,plain,
sF14 = antidomain(antidomain(sF12)),
inference(step,[status(thm)],[t41874,t740]) ).
cnf(t41876,plain,
sF14 = antidomain(sF13),
inference(step,[status(thm)],[t41875,t774]) ).
cnf(t804,plain,
antidomain(sF13) = sF14,
inference(orient,[status(thm)],[t41876]) ).
cnf(t41902,plain,
sF15 = addition(sF1,sF14),
inference(step,[status(thm)],[t41901,t804]) ).
cnf(t846,plain,
addition(sF1,sF14) = sF15,
inference(orient,[status(thm)],[t41902]) ).
cnf(t2143,plain,
multiplication(sF14,sF0) = multiplication(sF15,sF0),
inference(cp,[status(thm)],[t2140,t846]) ).
cnf(t2226,plain,
multiplication(sF15,sF0) = multiplication(sF14,sF0),
inference(orient,[status(thm)],[t2143]) ).
cnf(t805,plain,
zero = multiplication(sF14,sF13),
inference(cp,[status(thm)],[t63,t804]) ).
cnf(t809,plain,
multiplication(sF14,sF13) = zero,
inference(orient,[status(thm)],[t805]) ).
cnf(t812,plain,
multiplication(sF14,addition(X1,sF13)) = addition(multiplication(sF14,X1),zero),
inference(cp,[status(thm)],[t242,t809]) ).
cnf(t42255,plain,
multiplication(sF14,addition(X1,sF13)) = multiplication(sF14,X1),
inference(step,[status(thm)],[t812,t53]) ).
cnf(t3894,plain,
multiplication(sF14,addition(X1,sF13)) = multiplication(sF14,X1),
inference(orient,[status(thm)],[t42255]) ).
cnf(t742,plain,
one = addition(sF12,antidomain(antidomain(sF11))),
inference(cp,[status(thm)],[t108,t740]) ).
cnf(t41884,plain,
one = addition(sF12,antidomain(sF12)),
inference(step,[status(thm)],[t742,t740]) ).
cnf(t41885,plain,
one = addition(sF12,sF13),
inference(step,[status(thm)],[t41884,t774]) ).
cnf(t836,plain,
addition(sF12,sF13) = one,
inference(orient,[status(thm)],[t41885]) ).
cnf(t3896,plain,
multiplication(sF14,sF12) = multiplication(sF14,one),
inference(cp,[status(thm)],[t3894,t836]) ).
cnf(t775,plain,
zero = multiplication(sF13,sF12),
inference(cp,[status(thm)],[t63,t774]) ).
cnf(t779,plain,
multiplication(sF13,sF12) = zero,
inference(orient,[status(thm)],[t775]) ).
cnf(t783,plain,
multiplication(addition(sF13,X1),sF12) = addition(zero,multiplication(X1,sF12)),
inference(cp,[status(thm)],[t287,t779]) ).
cnf(t42242,plain,
multiplication(addition(sF13,X1),sF12) = multiplication(X1,sF12),
inference(step,[status(thm)],[t783,t82]) ).
cnf(t3749,plain,
multiplication(addition(sF13,X1),sF12) = multiplication(X1,sF12),
inference(orient,[status(thm)],[t42242]) ).
cnf(t776,plain,
one = addition(sF13,antidomain(antidomain(sF12))),
inference(cp,[status(thm)],[t108,t774]) ).
cnf(t41886,plain,
one = addition(sF13,antidomain(sF13)),
inference(step,[status(thm)],[t776,t774]) ).
cnf(t41887,plain,
one = addition(sF13,sF14),
inference(step,[status(thm)],[t41886,t804]) ).
cnf(t841,plain,
addition(sF13,sF14) = one,
inference(orient,[status(thm)],[t41887]) ).
cnf(t3750,plain,
multiplication(sF14,sF12) = multiplication(one,sF12),
inference(cp,[status(thm)],[t3749,t841]) ).
cnf(t42243,plain,
multiplication(sF14,sF12) = sF12,
inference(step,[status(thm)],[t3750,t56]) ).
cnf(t3761,plain,
multiplication(sF14,sF12) = sF12,
inference(orient,[status(thm)],[t42243]) ).
cnf(t42256,plain,
sF12 = multiplication(sF14,one),
inference(step,[status(thm)],[t3896,t3761]) ).
cnf(t42257,plain,
sF12 = sF14,
inference(step,[status(thm)],[t42256,t54]) ).
cnf(t3904,plain,
sF14 = sF12,
inference(orient,[status(thm)],[t42257]) ).
cnf(t42264,plain,
multiplication(sF15,sF0) = multiplication(sF12,sF0),
inference(step,[status(thm)],[t2226,t3904]) ).
cnf(t3915,plain,
multiplication(sF15,sF0) = multiplication(sF12,sF0),
inference(orient,[status(thm)],[t42264]) ).
cnf(u3,axiom,
addition(domain(sK2_goals_X1),backward_box(sK3_goals_X0,domain(sK1_goals_X2))) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u7,axiom,
backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u0,axiom,
c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d2,axiom,
c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
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(d7,axiom,
backward_box(X0,X1) = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X0)))))),
inference(definition_unfolding,[status(thm)],[u7,d2,d5]) ).
cnf(t21,plain,
addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) = one,
inference(definition_unfolding,[status(thm)],[u3,d0,d7]) ).
cnf(t41765,plain,
addition(antidomain(sF0),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t21,t50]) ).
cnf(t41766,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t41765,t58]) ).
cnf(t41767,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF2)))))),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t41766,t51]) ).
cnf(t41768,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF3))))),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t41767,t59]) ).
cnf(t41769,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF4)))),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t41768,t74]) ).
cnf(t41770,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t41769,t100]) ).
cnf(t477,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF5))),sK3_goals_X0))))))) = one,
inference(orient,[status(thm)],[t41770]) ).
cnf(t41786,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t477,t538]) ).
cnf(t540,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF6)),sK3_goals_X0))))))) = one,
inference(rw,[status(thm)],[t41786]) ).
cnf(t42840,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF2)),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t540,t2413]) ).
cnf(t42155,plain,
coantidomain(sF2) = sF7,
inference(step,[status(thm)],[t569,t2413]) ).
cnf(t2417,plain,
coantidomain(sF2) = sF7,
inference(rw,[status(thm)],[t42155]) ).
cnf(t2419,plain,
coantidomain(sF2) = sF7,
inference(orient,[status(thm)],[t2417]) ).
cnf(t42841,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF7),sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t42840,t2419]) ).
cnf(t42842,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(sF8,sK3_goals_X0))))))) = one,
inference(step,[status(thm)],[t42841,t610]) ).
cnf(t42843,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(sF9)))))) = one,
inference(step,[status(thm)],[t42842,t640]) ).
cnf(t42844,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(sF10))))) = one,
inference(step,[status(thm)],[t42843,t717]) ).
cnf(t42845,plain,
addition(sF1,antidomain(antidomain(antidomain(sF11)))) = one,
inference(step,[status(thm)],[t42844,t722]) ).
cnf(t42846,plain,
addition(sF1,antidomain(antidomain(sF12))) = one,
inference(step,[status(thm)],[t42845,t740]) ).
cnf(t42847,plain,
addition(sF1,antidomain(sF13)) = one,
inference(step,[status(thm)],[t42846,t774]) ).
cnf(t42258,plain,
antidomain(sF13) = sF12,
inference(step,[status(thm)],[t804,t3904]) ).
cnf(t3905,plain,
antidomain(sF13) = sF12,
inference(orient,[status(thm)],[t42258]) ).
cnf(t42848,plain,
addition(sF1,sF12) = one,
inference(step,[status(thm)],[t42847,t3905]) ).
cnf(t42261,plain,
addition(sF1,sF12) = sF15,
inference(step,[status(thm)],[t846,t3904]) ).
cnf(t3911,plain,
addition(sF1,sF12) = sF15,
inference(rw,[status(thm)],[t42261]) ).
cnf(t3927,plain,
addition(sF1,sF12) = sF15,
inference(orient,[status(thm)],[t3911]) ).
cnf(t42849,plain,
sF15 = one,
inference(step,[status(thm)],[t42848,t3927]) ).
cnf(t17442,plain,
one = sF15,
inference(orient,[status(thm)],[t42849]) ).
cnf(t42851,plain,
multiplication(sF15,X1) = X1,
inference(step,[status(thm)],[t56,t17442]) ).
cnf(t17444,plain,
multiplication(sF15,X1) = X1,
inference(rw,[status(thm)],[t42851]) ).
cnf(t17731,plain,
multiplication(sF15,X1) = X1,
inference(orient,[status(thm)],[t17444]) ).
cnf(t43017,plain,
sF0 = multiplication(sF12,sF0),
inference(step,[status(thm)],[t3915,t17731]) ).
cnf(t17733,plain,
sF0 = multiplication(sF12,sF0),
inference(rw,[status(thm)],[t43017]) ).
cnf(t784,plain,
multiplication(addition(X1,sF13),sF12) = addition(multiplication(X1,sF12),zero),
inference(cp,[status(thm)],[t287,t779]) ).
cnf(t42244,plain,
multiplication(addition(X1,sF13),sF12) = multiplication(X1,sF12),
inference(step,[status(thm)],[t784,t53]) ).
cnf(t3778,plain,
multiplication(addition(X1,sF13),sF12) = multiplication(X1,sF12),
inference(orient,[status(thm)],[t42244]) ).
cnf(t153,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = addition(antidomain(X1),one),
inference(cp,[status(thm)],[t150,t108]) ).
cnf(t41723,plain,
one = addition(antidomain(X1),one),
inference(step,[status(thm)],[t153,t108]) ).
cnf(t41724,plain,
one = addition(one,antidomain(X1)),
inference(step,[status(thm)],[t41723,t79]) ).
cnf(t274,plain,
addition(one,antidomain(X1)) = one,
inference(orient,[status(thm)],[t41724]) ).
cnf(t777,plain,
one = addition(one,sF13),
inference(cp,[status(thm)],[t274,t774]) ).
cnf(t41860,plain,
one = addition(sF13,one),
inference(step,[status(thm)],[t777,t79]) ).
cnf(t787,plain,
addition(sF13,one) = one,
inference(orient,[status(thm)],[t41860]) ).
cnf(t17485,plain,
addition(sF13,sF15) = one,
inference(rw,[status(thm)],[t787]) ).
cnf(t719,plain,
one = addition(sF10,coantidomain(coantidomain(sF9))),
inference(cp,[status(thm)],[t139,t717]) ).
cnf(t41862,plain,
one = addition(sF10,coantidomain(sF10)),
inference(step,[status(thm)],[t719,t717]) ).
cnf(t41863,plain,
one = addition(sF10,sF11),
inference(step,[status(thm)],[t41862,t722]) ).
cnf(t793,plain,
addition(sF10,sF11) = one,
inference(orient,[status(thm)],[t41863]) ).
cnf(t795,plain,
addition(sF10,addition(sF11,X1)) = addition(one,X1),
inference(cp,[status(thm)],[t85,t793]) ).
cnf(t3827,plain,
addition(sF10,addition(sF11,X1)) = addition(one,X1),
inference(orient,[status(thm)],[t795]) ).
cnf(t741,plain,
zero = multiplication(sF12,sF11),
inference(cp,[status(thm)],[t63,t740]) ).
cnf(t759,plain,
multiplication(sF12,sF11) = zero,
inference(orient,[status(thm)],[t741]) ).
cnf(t763,plain,
multiplication(addition(sF12,X1),sF11) = addition(zero,multiplication(X1,sF11)),
inference(cp,[status(thm)],[t287,t759]) ).
cnf(t42229,plain,
multiplication(addition(sF12,X1),sF11) = multiplication(X1,sF11),
inference(step,[status(thm)],[t763,t82]) ).
cnf(t3642,plain,
multiplication(addition(sF12,X1),sF11) = multiplication(X1,sF11),
inference(orient,[status(thm)],[t42229]) ).
cnf(t3643,plain,
multiplication(sF13,sF11) = multiplication(one,sF11),
inference(cp,[status(thm)],[t3642,t836]) ).
cnf(t42230,plain,
multiplication(sF13,sF11) = sF11,
inference(step,[status(thm)],[t3643,t56]) ).
cnf(t3654,plain,
multiplication(sF13,sF11) = sF11,
inference(orient,[status(thm)],[t42230]) ).
cnf(t3656,plain,
multiplication(sF13,addition(sF11,X1)) = addition(sF11,multiplication(sF13,X1)),
inference(cp,[status(thm)],[t242,t3654]) ).
cnf(t17388,plain,
addition(sF11,multiplication(sF13,X1)) = multiplication(sF13,addition(sF11,X1)),
inference(orient,[status(thm)],[t3656]) ).
cnf(t17389,plain,
multiplication(sF13,addition(sF11,one)) = addition(sF11,sF13),
inference(cp,[status(thm)],[t17388,t54]) ).
cnf(t160,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = addition(coantidomain(X1),one),
inference(cp,[status(thm)],[t150,t139]) ).
cnf(t41725,plain,
one = addition(coantidomain(X1),one),
inference(step,[status(thm)],[t160,t139]) ).
cnf(t41726,plain,
one = addition(one,coantidomain(X1)),
inference(step,[status(thm)],[t41725,t79]) ).
cnf(t316,plain,
addition(one,coantidomain(X1)) = one,
inference(orient,[status(thm)],[t41726]) ).
cnf(t725,plain,
one = addition(one,sF11),
inference(cp,[status(thm)],[t316,t722]) ).
cnf(t41844,plain,
one = addition(sF11,one),
inference(step,[status(thm)],[t725,t79]) ).
cnf(t753,plain,
addition(sF11,one) = one,
inference(orient,[status(thm)],[t41844]) ).
cnf(t42837,plain,
multiplication(sF13,one) = addition(sF11,sF13),
inference(step,[status(thm)],[t17389,t753]) ).
cnf(t42838,plain,
sF13 = addition(sF11,sF13),
inference(step,[status(thm)],[t42837,t54]) ).
cnf(t17417,plain,
addition(sF11,sF13) = sF13,
inference(orient,[status(thm)],[t42838]) ).
cnf(t17431,plain,
addition(one,sF13) = addition(sF10,sF13),
inference(cp,[status(thm)],[t3827,t17417]) ).
cnf(t43010,plain,
addition(sF13,one) = addition(sF10,sF13),
inference(step,[status(thm)],[t17431,t79]) ).
cnf(t43011,plain,
addition(sF13,sF15) = addition(sF10,sF13),
inference(step,[status(thm)],[t43010,t17442]) ).
cnf(t17676,plain,
addition(sF13,sF15) = addition(sF10,sF13),
inference(orient,[status(thm)],[t43011]) ).
cnf(t43036,plain,
addition(sF10,sF13) = one,
inference(step,[status(thm)],[t17485,t17676]) ).
cnf(t43037,plain,
addition(sF10,sF13) = sF15,
inference(step,[status(thm)],[t43036,t17442]) ).
cnf(t17979,plain,
addition(sF10,sF13) = sF15,
inference(orient,[status(thm)],[t43037]) ).
cnf(t17995,plain,
multiplication(sF10,sF12) = multiplication(sF15,sF12),
inference(cp,[status(thm)],[t3778,t17979]) ).
cnf(t723,plain,
zero = multiplication(sF10,sF11),
inference(cp,[status(thm)],[t60,t722]) ).
cnf(t745,plain,
multiplication(sF10,sF11) = zero,
inference(orient,[status(thm)],[t723]) ).
cnf(t751,plain,
antidomain(multiplication(sF10,antidomain(antidomain(sF11)))) = addition(antidomain(zero),antidomain(multiplication(sF10,antidomain(antidomain(sF11))))),
inference(cp,[status(thm)],[t336,t745]) ).
cnf(t42215,plain,
antidomain(multiplication(sF10,antidomain(sF12))) = addition(antidomain(zero),antidomain(multiplication(sF10,antidomain(antidomain(sF11))))),
inference(step,[status(thm)],[t751,t740]) ).
cnf(t42216,plain,
antidomain(multiplication(sF10,sF13)) = addition(antidomain(zero),antidomain(multiplication(sF10,antidomain(antidomain(sF11))))),
inference(step,[status(thm)],[t42215,t774]) ).
cnf(t66,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t63,t54]) ).
cnf(t69,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t66]) ).
cnf(t113,plain,
one = addition(zero,antidomain(antidomain(one))),
inference(cp,[status(thm)],[t108,t69]) ).
cnf(t41686,plain,
one = antidomain(antidomain(one)),
inference(step,[status(thm)],[t113,t82]) ).
cnf(t41687,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t41686,t69]) ).
cnf(t120,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t41687]) ).
cnf(t42217,plain,
antidomain(multiplication(sF10,sF13)) = addition(one,antidomain(multiplication(sF10,antidomain(antidomain(sF11))))),
inference(step,[status(thm)],[t42216,t120]) ).
cnf(t42218,plain,
antidomain(multiplication(sF10,sF13)) = one,
inference(step,[status(thm)],[t42217,t274]) ).
cnf(t3546,plain,
antidomain(multiplication(sF10,sF13)) = one,
inference(orient,[status(thm)],[t42218]) ).
cnf(t3547,plain,
zero = multiplication(one,multiplication(sF10,sF13)),
inference(cp,[status(thm)],[t63,t3546]) ).
cnf(t42219,plain,
zero = multiplication(sF10,sF13),
inference(step,[status(thm)],[t3547,t56]) ).
cnf(t3551,plain,
multiplication(sF10,sF13) = zero,
inference(orient,[status(thm)],[t42219]) ).
cnf(t3555,plain,
multiplication(sF10,addition(X1,sF13)) = addition(multiplication(sF10,X1),zero),
inference(cp,[status(thm)],[t242,t3551]) ).
cnf(t42816,plain,
multiplication(sF10,addition(X1,sF13)) = multiplication(sF10,X1),
inference(step,[status(thm)],[t3555,t53]) ).
cnf(t16956,plain,
multiplication(sF10,addition(X1,sF13)) = multiplication(sF10,X1),
inference(orient,[status(thm)],[t42816]) ).
cnf(t16958,plain,
multiplication(sF10,sF12) = multiplication(sF10,one),
inference(cp,[status(thm)],[t16956,t836]) ).
cnf(t42819,plain,
multiplication(sF10,sF12) = sF10,
inference(step,[status(thm)],[t16958,t54]) ).
cnf(t16992,plain,
multiplication(sF10,sF12) = sF10,
inference(orient,[status(thm)],[t42819]) ).
cnf(t43040,plain,
sF10 = multiplication(sF15,sF12),
inference(step,[status(thm)],[t17995,t16992]) ).
cnf(t43041,plain,
sF10 = sF12,
inference(step,[status(thm)],[t43040,t17731]) ).
cnf(t18005,plain,
sF12 = sF10,
inference(orient,[status(thm)],[t43041]) ).
cnf(t43083,plain,
sF0 = multiplication(sF10,sF0),
inference(step,[status(thm)],[t17733,t18005]) ).
cnf(t18257,plain,
multiplication(sF10,sF0) = sF0,
inference(orient,[status(thm)],[t43083]) ).
cnf(t18264,plain,
zero = multiplication(sF9,sF0),
inference(cp,[status(thm)],[t3259,t18257]) ).
cnf(t641,plain,
multiplication(sF8,multiplication(sK3_goals_X0,X1)) = multiplication(sF9,X1),
inference(cp,[status(thm)],[t90,t640]) ).
cnf(t3057,plain,
multiplication(sF8,multiplication(sK3_goals_X0,X1)) = multiplication(sF9,X1),
inference(orient,[status(thm)],[t641]) ).
cnf(t3061,plain,
multiplication(sF9,sF0) = multiplication(sF8,sF21),
inference(cp,[status(thm)],[t3057,t2343]) ).
cnf(t3071,plain,
multiplication(sF9,sF0) = multiplication(sF8,sF21),
inference(orient,[status(thm)],[t3061]) ).
cnf(t43090,plain,
zero = multiplication(sF8,sF21),
inference(step,[status(thm)],[t18264,t3071]) ).
cnf(t18571,plain,
multiplication(sF8,sF21) = zero,
inference(orient,[status(thm)],[t43090]) ).
cnf(t21278,plain,
antidomain(multiplication(sF8,sF23)) = addition(antidomain(zero),antidomain(multiplication(sF8,sF23))),
inference(cp,[status(thm)],[t21274,t18571]) ).
cnf(t42856,plain,
antidomain(zero) = sF15,
inference(step,[status(thm)],[t120,t17442]) ).
cnf(t17449,plain,
antidomain(zero) = sF15,
inference(orient,[status(thm)],[t42856]) ).
cnf(t43228,plain,
antidomain(multiplication(sF8,sF23)) = addition(sF15,antidomain(multiplication(sF8,sF23))),
inference(step,[status(thm)],[t21278,t17449]) ).
cnf(t17467,plain,
addition(sF15,antidomain(X1)) = one,
inference(rw,[status(thm)],[t274]) ).
cnf(t43095,plain,
addition(sF15,antidomain(X1)) = sF15,
inference(step,[status(thm)],[t17467,t17442]) ).
cnf(t18655,plain,
addition(sF15,antidomain(X1)) = sF15,
inference(orient,[status(thm)],[t43095]) ).
cnf(t43229,plain,
antidomain(multiplication(sF8,sF23)) = sF15,
inference(step,[status(thm)],[t43228,t18655]) ).
cnf(t21302,plain,
antidomain(multiplication(sF8,sF23)) = sF15,
inference(orient,[status(thm)],[t43229]) ).
cnf(t21303,plain,
zero = multiplication(sF15,multiplication(sF8,sF23)),
inference(cp,[status(thm)],[t63,t21302]) ).
cnf(t43230,plain,
zero = multiplication(sF8,sF23),
inference(step,[status(thm)],[t21303,t17731]) ).
cnf(t21313,plain,
multiplication(sF8,sF23) = zero,
inference(orient,[status(thm)],[t43230]) ).
cnf(t24795,plain,
multiplication(sF2,sF23) = multiplication(sF2,zero),
inference(cp,[status(thm)],[t24789,t21313]) ).
cnf(t3,axiom,
multiplication(X1,zero) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t55,plain,
multiplication(X1,zero) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t43391,plain,
multiplication(sF2,sF23) = zero,
inference(step,[status(thm)],[t24795,t55]) ).
cnf(t24885,plain,
multiplication(sF2,sF23) = zero,
inference(orient,[status(thm)],[t43391]) ).
cnf(t24887,plain,
multiplication(sF2,addition(sF23,X1)) = addition(zero,multiplication(sF2,X1)),
inference(cp,[status(thm)],[t242,t24885]) ).
cnf(t43854,plain,
multiplication(sF2,addition(sF23,X1)) = multiplication(sF2,X1),
inference(step,[status(thm)],[t24887,t82]) ).
cnf(t41457,plain,
multiplication(sF2,addition(sF23,X1)) = multiplication(sF2,X1),
inference(orient,[status(thm)],[t43854]) ).
cnf(t9722,plain,
addition(sF3,addition(sF22,X1)) = addition(sF27,X1),
inference(cp,[status(thm)],[t85,t9720]) ).
cnf(t20905,plain,
addition(sF3,addition(sF22,X1)) = addition(sF27,X1),
inference(orient,[status(thm)],[t9722]) ).
cnf(t42887,plain,
addition(sF22,sF23) = sF15,
inference(step,[status(thm)],[t1036,t17442]) ).
cnf(t17501,plain,
addition(sF22,sF23) = sF15,
inference(orient,[status(thm)],[t42887]) ).
cnf(t20911,plain,
addition(sF27,sF23) = addition(sF3,sF15),
inference(cp,[status(thm)],[t20905,t17501]) ).
cnf(t43209,plain,
addition(sF23,sF27) = addition(sF3,sF15),
inference(step,[status(thm)],[t20911,t79]) ).
cnf(t157,plain,
addition(sF3,sF4) = addition(sF3,one),
inference(cp,[status(thm)],[t150,t130]) ).
cnf(t41708,plain,
one = addition(sF3,one),
inference(step,[status(thm)],[t157,t130]) ).
cnf(t192,plain,
addition(sF3,one) = one,
inference(orient,[status(thm)],[t41708]) ).
cnf(t17462,plain,
addition(sF3,sF15) = one,
inference(rw,[status(thm)],[t192]) ).
cnf(t43030,plain,
addition(sF3,sF15) = sF15,
inference(step,[status(thm)],[t17462,t17442]) ).
cnf(t17815,plain,
addition(sF3,sF15) = sF15,
inference(orient,[status(thm)],[t43030]) ).
cnf(t43210,plain,
addition(sF23,sF27) = sF15,
inference(step,[status(thm)],[t43209,t17815]) ).
cnf(t20948,plain,
addition(sF23,sF27) = sF15,
inference(orient,[status(thm)],[t43210]) ).
cnf(t41462,plain,
multiplication(sF2,sF27) = multiplication(sF2,sF15),
inference(cp,[status(thm)],[t41457,t20948]) ).
cnf(t42510,plain,
multiplication(sF2,sF27) = multiplication(sF2,sF22),
inference(step,[status(thm)],[t2441,t9630]) ).
cnf(t9639,plain,
multiplication(sF2,sF27) = multiplication(sF2,sF22),
inference(orient,[status(thm)],[t42510]) ).
cnf(t43855,plain,
multiplication(sF2,sF22) = multiplication(sF2,sF15),
inference(step,[status(thm)],[t41462,t9639]) ).
cnf(t42850,plain,
multiplication(X1,sF15) = X1,
inference(step,[status(thm)],[t54,t17442]) ).
cnf(t17443,plain,
multiplication(X1,sF15) = X1,
inference(rw,[status(thm)],[t42850]) ).
cnf(t17708,plain,
multiplication(X1,sF15) = X1,
inference(orient,[status(thm)],[t17443]) ).
cnf(t43856,plain,
multiplication(sF2,sF22) = sF2,
inference(step,[status(thm)],[t43855,t17708]) ).
cnf(t41510,plain,
multiplication(sF2,sF22) = sF2,
inference(orient,[status(thm)],[t43856]) ).
cnf(t43859,plain,
addition(sF27,sF2) = sF27,
inference(step,[status(thm)],[t14285,t41510]) ).
cnf(t41513,plain,
addition(sF27,sF2) = sF27,
inference(rw,[status(thm)],[t43859]) ).
cnf(t43863,plain,
addition(sF2,sF27) = sF27,
inference(step,[status(thm)],[t41513,t79]) ).
cnf(t126,plain,
addition(sF2,addition(sF3,X1)) = addition(one,X1),
inference(cp,[status(thm)],[t85,t124]) ).
cnf(t593,plain,
addition(sF2,addition(sF3,X1)) = addition(one,X1),
inference(orient,[status(thm)],[t126]) ).
cnf(t1164,plain,
addition(one,sF26) = addition(sF2,sF27),
inference(cp,[status(thm)],[t593,t1158]) ).
cnf(t42034,plain,
addition(sF26,one) = addition(sF2,sF27),
inference(step,[status(thm)],[t1164,t79]) ).
cnf(t1130,plain,
one = addition(one,sF26),
inference(cp,[status(thm)],[t274,t1126]) ).
cnf(t42014,plain,
one = addition(sF26,one),
inference(step,[status(thm)],[t1130,t79]) ).
cnf(t1146,plain,
addition(sF26,one) = one,
inference(orient,[status(thm)],[t42014]) ).
cnf(t42035,plain,
one = addition(sF2,sF27),
inference(step,[status(thm)],[t42034,t1146]) ).
cnf(t1172,plain,
addition(sF2,sF27) = one,
inference(orient,[status(thm)],[t42035]) ).
cnf(t42890,plain,
addition(sF2,sF27) = sF15,
inference(step,[status(thm)],[t1172,t17442]) ).
cnf(t17505,plain,
addition(sF2,sF27) = sF15,
inference(orient,[status(thm)],[t42890]) ).
cnf(t43864,plain,
sF15 = sF27,
inference(step,[status(thm)],[t43863,t17505]) ).
cnf(t41552,plain,
sF27 = sF15,
inference(orient,[status(thm)],[t43864]) ).
cnf(t43865,plain,
addition(sF3,sF22) = sF15,
inference(step,[status(thm)],[t9720,t41552]) ).
cnf(t41561,plain,
addition(sF3,sF22) = sF15,
inference(orient,[status(thm)],[t43865]) ).
cnf(u4,negated_conjecture,
addition(forward_box(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)) != one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u6,axiom,
forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u2,axiom,
forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d4,axiom,
forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(d6,axiom,
forward_box(X0,X1) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))),
inference(definition_unfolding,[status(thm)],[u6,d2,d4]) ).
cnf(goal_0,negated_conjecture,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(definition_unfolding,[status(thm)],[u4,d0,d6]) ).
cnf(g0_0,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF0)))))))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[goal_0,t50]) ).
cnf(g0_1,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sF1))))))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_0,t58]) ).
cnf(g0_2,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(sF0)))))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_1,t2154]) ).
cnf(g0_3,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sF1))))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_2,t58]) ).
cnf(g0_4,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(sF0)))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_3,t2154]) ).
cnf(g0_5,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sF1))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_4,t58]) ).
cnf(g0_6,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,sF0)))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_5,t2154]) ).
cnf(g0_7,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(sF21))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_6,t2343]) ).
cnf(g0_8,plain,
addition(antidomain(antidomain(antidomain(antidomain(sF22)))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_7,t1000]) ).
cnf(g0_9,plain,
addition(antidomain(antidomain(antidomain(sF23))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_8,t1030]) ).
cnf(g0_10,plain,
addition(antidomain(antidomain(sF22)),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_9,t9580]) ).
cnf(g0_11,plain,
addition(antidomain(sF23),antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_10,t1030]) ).
cnf(g0_12,plain,
addition(sF22,antidomain(antidomain(sK1_goals_X2))) != one,
inference(rw,[status(thm)],[g0_11,t9580]) ).
cnf(g0_13,plain,
addition(sF22,antidomain(sF2)) != one,
inference(rw,[status(thm)],[g0_12,t51]) ).
cnf(g0_14,plain,
addition(sF22,sF3) != one,
inference(rw,[status(thm)],[g0_13,t59]) ).
cnf(g0_15,plain,
addition(sF3,sF22) != one,
inference(rw,[status(thm)],[g0_14,t79]) ).
cnf(g0_16,plain,
sF15 != one,
inference(rw,[status(thm)],[g0_15,t41561]) ).
cnf(g0_17,plain,
sF15 != sF15,
inference(rw,[status(thm)],[g0_16,t17442]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE104-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n018.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Wed Sep 23 18:59:07 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 89.60/18.86 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 89.60/18.86 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------