%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE110-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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:51:38 PM UTC 2026
% Result : Unsatisfiable 48.26s 7.61s
% Output : CNFRefutation 48.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 91
% Number of leaves : 46
% Syntax : Number of clauses : 733 ( 733 unt; 0 nHn; 561 RR)
% Number of literals : 733 ( 732 equ; 41 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 20 ( 4 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 24 con; 0-4 aty)
% Number of variables : 235 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t21,axiom,
sF0 = antidomain(sK2_goals_X0),
introduced(definition) ).
cnf(t40,plain,
antidomain(sK2_goals_X0) = sF0,
inference(orient,[status(thm)],[t21]) ).
cnf(t22,axiom,
sF1 = antidomain(antidomain(sK2_goals_X0)),
introduced(definition) ).
cnf(t27292,plain,
sF1 = antidomain(sF0),
inference(step,[status(thm)],[t22,t40]) ).
cnf(t47,plain,
antidomain(sF0) = sF1,
inference(orient,[status(thm)],[t27292]) ).
cnf(t23,axiom,
sF2 = antidomain(antidomain(antidomain(sK2_goals_X0))),
introduced(definition) ).
cnf(t27293,plain,
sF2 = antidomain(antidomain(sF0)),
inference(step,[status(thm)],[t23,t40]) ).
cnf(t27294,plain,
sF2 = antidomain(sF1),
inference(step,[status(thm)],[t27293,t47]) ).
cnf(t58,plain,
antidomain(sF1) = sF2,
inference(orient,[status(thm)],[t27294]) ).
cnf(t18,axiom,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t250,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(t51,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t7]) ).
cnf(t54,plain,
zero = multiplication(sF1,sF0),
inference(cp,[status(thm)],[t51,t47]) ).
cnf(t57,plain,
multiplication(sF1,sF0) = zero,
inference(orient,[status(thm)],[t54]) ).
cnf(t259,plain,
multiplication(addition(sF1,X1),sF0) = addition(zero,multiplication(X1,sF0)),
inference(cp,[status(thm)],[t250,t57]) ).
cnf(t8,axiom,
addition(X1,X2) = addition(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t76,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(t42,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t77,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t76,t42]) ).
cnf(t82,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t77]) ).
cnf(t27621,plain,
multiplication(addition(sF1,X1),sF0) = multiplication(X1,sF0),
inference(step,[status(thm)],[t259,t82]) ).
cnf(t1600,plain,
multiplication(addition(sF1,X1),sF0) = multiplication(X1,sF0),
inference(orient,[status(thm)],[t27621]) ).
cnf(t11,axiom,
addition(antidomain(antidomain(X1)),antidomain(X1)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27303,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t11,t76]) ).
cnf(t95,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(orient,[status(thm)],[t27303]) ).
cnf(t97,plain,
one = addition(sF1,antidomain(antidomain(sF0))),
inference(cp,[status(thm)],[t95,t47]) ).
cnf(t27311,plain,
one = addition(sF1,antidomain(sF1)),
inference(step,[status(thm)],[t97,t47]) ).
cnf(t27312,plain,
one = addition(sF1,sF2),
inference(step,[status(thm)],[t27311,t58]) ).
cnf(t118,plain,
addition(sF1,sF2) = one,
inference(orient,[status(thm)],[t27312]) ).
cnf(t1601,plain,
multiplication(sF2,sF0) = multiplication(one,sF0),
inference(cp,[status(thm)],[t1600,t118]) ).
cnf(t17,axiom,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t195,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t17]) ).
cnf(t59,plain,
zero = multiplication(sF2,sF1),
inference(cp,[status(thm)],[t51,t58]) ).
cnf(t60,plain,
multiplication(sF2,sF1) = zero,
inference(orient,[status(thm)],[t59]) ).
cnf(t207,plain,
multiplication(sF2,addition(X1,sF1)) = addition(multiplication(sF2,X1),zero),
inference(cp,[status(thm)],[t195,t60]) ).
cnf(t27374,plain,
multiplication(sF2,addition(X1,sF1)) = multiplication(sF2,X1),
inference(step,[status(thm)],[t207,t42]) ).
cnf(t545,plain,
multiplication(sF2,addition(X1,sF1)) = multiplication(sF2,X1),
inference(orient,[status(thm)],[t27374]) ).
cnf(t96,plain,
one = addition(sF0,antidomain(antidomain(sK2_goals_X0))),
inference(cp,[status(thm)],[t95,t40]) ).
cnf(t27309,plain,
one = addition(sF0,antidomain(sF0)),
inference(step,[status(thm)],[t96,t40]) ).
cnf(t27310,plain,
one = addition(sF0,sF1),
inference(step,[status(thm)],[t27309,t47]) ).
cnf(t113,plain,
addition(sF0,sF1) = one,
inference(orient,[status(thm)],[t27310]) ).
cnf(t547,plain,
multiplication(sF2,sF0) = multiplication(sF2,one),
inference(cp,[status(thm)],[t545,t113]) ).
cnf(t2,axiom,
multiplication(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t27375,plain,
multiplication(sF2,sF0) = sF2,
inference(step,[status(thm)],[t547,t43]) ).
cnf(t553,plain,
multiplication(sF2,sF0) = sF2,
inference(orient,[status(thm)],[t27375]) ).
cnf(t27622,plain,
sF2 = multiplication(one,sF0),
inference(step,[status(thm)],[t1601,t553]) ).
cnf(t4,axiom,
multiplication(one,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t27623,plain,
sF2 = sF0,
inference(step,[status(thm)],[t27622,t45]) ).
cnf(t1616,plain,
sF2 = sF0,
inference(orient,[status(thm)],[t27623]) ).
cnf(t27624,plain,
antidomain(sF1) = sF0,
inference(step,[status(thm)],[t58,t1616]) ).
cnf(t1617,plain,
antidomain(sF1) = sF0,
inference(orient,[status(thm)],[t27624]) ).
cnf(t25,axiom,
sF4 = multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0))))),
introduced(definition) ).
cnf(t27354,plain,
sF4 = multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0)))),
inference(step,[status(thm)],[t25,t40]) ).
cnf(t27355,plain,
sF4 = multiplication(sK1_goals_X1,antidomain(antidomain(sF1))),
inference(step,[status(thm)],[t27354,t47]) ).
cnf(t27356,plain,
sF4 = multiplication(sK1_goals_X1,antidomain(sF2)),
inference(step,[status(thm)],[t27355,t58]) ).
cnf(t24,axiom,
sF3 = antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))),
introduced(definition) ).
cnf(t27295,plain,
sF3 = antidomain(antidomain(antidomain(sF0))),
inference(step,[status(thm)],[t24,t40]) ).
cnf(t27296,plain,
sF3 = antidomain(antidomain(sF1)),
inference(step,[status(thm)],[t27295,t47]) ).
cnf(t27297,plain,
sF3 = antidomain(sF2),
inference(step,[status(thm)],[t27296,t58]) ).
cnf(t74,plain,
antidomain(sF2) = sF3,
inference(orient,[status(thm)],[t27297]) ).
cnf(t27357,plain,
sF4 = multiplication(sK1_goals_X1,sF3),
inference(step,[status(thm)],[t27356,t74]) ).
cnf(t416,plain,
multiplication(sK1_goals_X1,sF3) = sF4,
inference(orient,[status(thm)],[t27357]) ).
cnf(t1620,plain,
antidomain(sF0) = sF3,
inference(rw,[status(thm)],[t74]) ).
cnf(t27636,plain,
sF1 = sF3,
inference(step,[status(thm)],[t1620,t47]) ).
cnf(t1645,plain,
sF3 = sF1,
inference(orient,[status(thm)],[t27636]) ).
cnf(t27637,plain,
multiplication(sK1_goals_X1,sF1) = sF4,
inference(step,[status(thm)],[t416,t1645]) ).
cnf(t1651,plain,
multiplication(sK1_goals_X1,sF1) = sF4,
inference(rw,[status(thm)],[t27637]) ).
cnf(t1740,plain,
multiplication(sK1_goals_X1,sF1) = sF4,
inference(orient,[status(thm)],[t1651]) ).
cnf(t26,axiom,
sF5 = antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))),
introduced(definition) ).
cnf(t27367,plain,
sF5 = antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))),
inference(step,[status(thm)],[t26,t40]) ).
cnf(t27368,plain,
sF5 = antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))),
inference(step,[status(thm)],[t27367,t47]) ).
cnf(t27369,plain,
sF5 = antidomain(multiplication(sK1_goals_X1,antidomain(sF2))),
inference(step,[status(thm)],[t27368,t58]) ).
cnf(t27370,plain,
sF5 = antidomain(multiplication(sK1_goals_X1,sF3)),
inference(step,[status(thm)],[t27369,t74]) ).
cnf(t27371,plain,
sF5 = antidomain(sF4),
inference(step,[status(thm)],[t27370,t416]) ).
cnf(t518,plain,
antidomain(sF4) = sF5,
inference(orient,[status(thm)],[t27371]) ).
cnf(t27,axiom,
sF6 = antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0))))))),
introduced(definition) ).
cnf(t27377,plain,
sF6 = antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0)))))),
inference(step,[status(thm)],[t27,t40]) ).
cnf(t27378,plain,
sF6 = antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1))))),
inference(step,[status(thm)],[t27377,t47]) ).
cnf(t27379,plain,
sF6 = antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2)))),
inference(step,[status(thm)],[t27378,t58]) ).
cnf(t27380,plain,
sF6 = antidomain(antidomain(multiplication(sK1_goals_X1,sF3))),
inference(step,[status(thm)],[t27379,t74]) ).
cnf(t27381,plain,
sF6 = antidomain(antidomain(sF4)),
inference(step,[status(thm)],[t27380,t416]) ).
cnf(t27382,plain,
sF6 = antidomain(sF5),
inference(step,[status(thm)],[t27381,t518]) ).
cnf(t569,plain,
antidomain(sF5) = sF6,
inference(orient,[status(thm)],[t27382]) ).
cnf(t28,axiom,
sF7 = antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))),
introduced(definition) ).
cnf(t27387,plain,
sF7 = antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))),
inference(step,[status(thm)],[t28,t40]) ).
cnf(t27388,plain,
sF7 = antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))),
inference(step,[status(thm)],[t27387,t47]) ).
cnf(t27389,plain,
sF7 = antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))),
inference(step,[status(thm)],[t27388,t58]) ).
cnf(t27390,plain,
sF7 = antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))),
inference(step,[status(thm)],[t27389,t74]) ).
cnf(t27391,plain,
sF7 = antidomain(antidomain(antidomain(sF4))),
inference(step,[status(thm)],[t27390,t416]) ).
cnf(t27392,plain,
sF7 = antidomain(antidomain(sF5)),
inference(step,[status(thm)],[t27391,t518]) ).
cnf(t27393,plain,
sF7 = antidomain(sF6),
inference(step,[status(thm)],[t27392,t569]) ).
cnf(t609,plain,
antidomain(sF6) = sF7,
inference(orient,[status(thm)],[t27393]) ).
cnf(t611,plain,
zero = multiplication(sF7,sF6),
inference(cp,[status(thm)],[t51,t609]) ).
cnf(t622,plain,
multiplication(sF7,sF6) = zero,
inference(orient,[status(thm)],[t611]) ).
cnf(t625,plain,
multiplication(sF7,addition(X1,sF6)) = addition(multiplication(sF7,X1),zero),
inference(cp,[status(thm)],[t195,t622]) ).
cnf(t27699,plain,
multiplication(sF7,addition(X1,sF6)) = multiplication(sF7,X1),
inference(step,[status(thm)],[t625,t42]) ).
cnf(t2291,plain,
multiplication(sF7,addition(X1,sF6)) = multiplication(sF7,X1),
inference(orient,[status(thm)],[t27699]) ).
cnf(t520,plain,
one = addition(sF5,antidomain(antidomain(sF4))),
inference(cp,[status(thm)],[t95,t518]) ).
cnf(t27373,plain,
one = addition(sF5,antidomain(sF5)),
inference(step,[status(thm)],[t520,t518]) ).
cnf(t539,plain,
addition(sF5,antidomain(sF5)) = one,
inference(orient,[status(thm)],[t27373]) ).
cnf(t27383,plain,
addition(sF5,sF6) = one,
inference(step,[status(thm)],[t539,t569]) ).
cnf(t570,plain,
addition(sF5,sF6) = one,
inference(rw,[status(thm)],[t27383]) ).
cnf(t583,plain,
addition(sF5,sF6) = one,
inference(orient,[status(thm)],[t570]) ).
cnf(t2292,plain,
multiplication(sF7,sF5) = multiplication(sF7,one),
inference(cp,[status(thm)],[t2291,t583]) ).
cnf(t571,plain,
zero = multiplication(sF6,sF5),
inference(cp,[status(thm)],[t51,t569]) ).
cnf(t589,plain,
multiplication(sF6,sF5) = zero,
inference(orient,[status(thm)],[t571]) ).
cnf(t593,plain,
multiplication(addition(sF6,X1),sF5) = addition(zero,multiplication(X1,sF5)),
inference(cp,[status(thm)],[t250,t589]) ).
cnf(t27681,plain,
multiplication(addition(sF6,X1),sF5) = multiplication(X1,sF5),
inference(step,[status(thm)],[t593,t82]) ).
cnf(t2157,plain,
multiplication(addition(sF6,X1),sF5) = multiplication(X1,sF5),
inference(orient,[status(thm)],[t27681]) ).
cnf(t572,plain,
one = addition(sF6,antidomain(antidomain(sF5))),
inference(cp,[status(thm)],[t95,t569]) ).
cnf(t27386,plain,
one = addition(sF6,antidomain(sF6)),
inference(step,[status(thm)],[t572,t569]) ).
cnf(t603,plain,
addition(sF6,antidomain(sF6)) = one,
inference(orient,[status(thm)],[t27386]) ).
cnf(t27394,plain,
addition(sF6,sF7) = one,
inference(step,[status(thm)],[t603,t609]) ).
cnf(t610,plain,
addition(sF6,sF7) = one,
inference(rw,[status(thm)],[t27394]) ).
cnf(t616,plain,
addition(sF6,sF7) = one,
inference(orient,[status(thm)],[t610]) ).
cnf(t2158,plain,
multiplication(sF7,sF5) = multiplication(one,sF5),
inference(cp,[status(thm)],[t2157,t616]) ).
cnf(t27682,plain,
multiplication(sF7,sF5) = sF5,
inference(step,[status(thm)],[t2158,t45]) ).
cnf(t2168,plain,
multiplication(sF7,sF5) = sF5,
inference(orient,[status(thm)],[t27682]) ).
cnf(t27700,plain,
sF5 = multiplication(sF7,one),
inference(step,[status(thm)],[t2292,t2168]) ).
cnf(t27701,plain,
sF5 = sF7,
inference(step,[status(thm)],[t27700,t43]) ).
cnf(t2300,plain,
sF7 = sF5,
inference(orient,[status(thm)],[t27701]) ).
cnf(t27702,plain,
antidomain(sF6) = sF5,
inference(step,[status(thm)],[t609,t2300]) ).
cnf(t2301,plain,
antidomain(sF6) = sF5,
inference(orient,[status(thm)],[t27702]) ).
cnf(t31,axiom,
sF10 = coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0))))))))))),
introduced(definition) ).
cnf(t27420,plain,
sF10 = coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0)))))))))),
inference(step,[status(thm)],[t31,t40]) ).
cnf(t27421,plain,
sF10 = coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1))))))))),
inference(step,[status(thm)],[t27420,t47]) ).
cnf(t27422,plain,
sF10 = coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2)))))))),
inference(step,[status(thm)],[t27421,t58]) ).
cnf(t27423,plain,
sF10 = coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3))))))),
inference(step,[status(thm)],[t27422,t74]) ).
cnf(t27424,plain,
sF10 = coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4)))))),
inference(step,[status(thm)],[t27423,t416]) ).
cnf(t27425,plain,
sF10 = coantidomain(antidomain(antidomain(antidomain(antidomain(sF5))))),
inference(step,[status(thm)],[t27424,t518]) ).
cnf(t27426,plain,
sF10 = coantidomain(antidomain(antidomain(antidomain(sF6)))),
inference(step,[status(thm)],[t27425,t569]) ).
cnf(t27427,plain,
sF10 = coantidomain(antidomain(antidomain(sF7))),
inference(step,[status(thm)],[t27426,t609]) ).
cnf(t29,axiom,
sF8 = antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0))))))))),
introduced(definition) ).
cnf(t27397,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0)))))))),
inference(step,[status(thm)],[t29,t40]) ).
cnf(t27398,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1))))))),
inference(step,[status(thm)],[t27397,t47]) ).
cnf(t27399,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2)))))),
inference(step,[status(thm)],[t27398,t58]) ).
cnf(t27400,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3))))),
inference(step,[status(thm)],[t27399,t74]) ).
cnf(t27401,plain,
sF8 = antidomain(antidomain(antidomain(antidomain(sF4)))),
inference(step,[status(thm)],[t27400,t416]) ).
cnf(t27402,plain,
sF8 = antidomain(antidomain(antidomain(sF5))),
inference(step,[status(thm)],[t27401,t518]) ).
cnf(t27403,plain,
sF8 = antidomain(antidomain(sF6)),
inference(step,[status(thm)],[t27402,t569]) ).
cnf(t27404,plain,
sF8 = antidomain(sF7),
inference(step,[status(thm)],[t27403,t609]) ).
cnf(t642,plain,
antidomain(sF7) = sF8,
inference(orient,[status(thm)],[t27404]) ).
cnf(t27428,plain,
sF10 = coantidomain(antidomain(sF8)),
inference(step,[status(thm)],[t27427,t642]) ).
cnf(t30,axiom,
sF9 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))),
introduced(definition) ).
cnf(t27408,plain,
sF9 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))),
inference(step,[status(thm)],[t30,t40]) ).
cnf(t27409,plain,
sF9 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))),
inference(step,[status(thm)],[t27408,t47]) ).
cnf(t27410,plain,
sF9 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))),
inference(step,[status(thm)],[t27409,t58]) ).
cnf(t27411,plain,
sF9 = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))),
inference(step,[status(thm)],[t27410,t74]) ).
cnf(t27412,plain,
sF9 = antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))),
inference(step,[status(thm)],[t27411,t416]) ).
cnf(t27413,plain,
sF9 = antidomain(antidomain(antidomain(antidomain(sF5)))),
inference(step,[status(thm)],[t27412,t518]) ).
cnf(t27414,plain,
sF9 = antidomain(antidomain(antidomain(sF6))),
inference(step,[status(thm)],[t27413,t569]) ).
cnf(t27415,plain,
sF9 = antidomain(antidomain(sF7)),
inference(step,[status(thm)],[t27414,t609]) ).
cnf(t27416,plain,
sF9 = antidomain(sF8),
inference(step,[status(thm)],[t27415,t642]) ).
cnf(t675,plain,
antidomain(sF8) = sF9,
inference(orient,[status(thm)],[t27416]) ).
cnf(t27429,plain,
sF10 = coantidomain(sF9),
inference(step,[status(thm)],[t27428,t675]) ).
cnf(t708,plain,
coantidomain(sF9) = sF10,
inference(orient,[status(thm)],[t27429]) ).
cnf(t2321,plain,
antidomain(sF6) = sF9,
inference(rw,[status(thm)],[t675]) ).
cnf(t27711,plain,
sF5 = sF9,
inference(step,[status(thm)],[t2321,t2301]) ).
cnf(t2326,plain,
sF9 = sF5,
inference(orient,[status(thm)],[t27711]) ).
cnf(t27712,plain,
coantidomain(sF5) = sF10,
inference(step,[status(thm)],[t708,t2326]) ).
cnf(t2330,plain,
coantidomain(sF5) = sF10,
inference(rw,[status(thm)],[t27712]) ).
cnf(t2333,plain,
coantidomain(sF5) = sF10,
inference(orient,[status(thm)],[t2330]) ).
cnf(t591,plain,
multiplication(sF6,addition(sF5,X1)) = addition(zero,multiplication(sF6,X1)),
inference(cp,[status(thm)],[t195,t589]) ).
cnf(t27678,plain,
multiplication(sF6,addition(sF5,X1)) = multiplication(sF6,X1),
inference(step,[status(thm)],[t591,t82]) ).
cnf(t2128,plain,
multiplication(sF6,addition(sF5,X1)) = multiplication(sF6,X1),
inference(orient,[status(thm)],[t27678]) ).
cnf(t12,axiom,
addition(coantidomain(coantidomain(X1)),coantidomain(X1)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27304,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(step,[status(thm)],[t12,t76]) ).
cnf(t105,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t27304]) ).
cnf(t710,plain,
one = addition(sF10,coantidomain(coantidomain(sF9))),
inference(cp,[status(thm)],[t105,t708]) ).
cnf(t27431,plain,
one = addition(sF10,coantidomain(sF10)),
inference(step,[status(thm)],[t710,t708]) ).
cnf(t729,plain,
addition(sF10,coantidomain(sF10)) = one,
inference(orient,[status(thm)],[t27431]) ).
cnf(t32,axiom,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),
introduced(definition) ).
cnf(t27435,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),
inference(step,[status(thm)],[t32,t40]) ).
cnf(t27436,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),
inference(step,[status(thm)],[t27435,t47]) ).
cnf(t27437,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),
inference(step,[status(thm)],[t27436,t58]) ).
cnf(t27438,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),
inference(step,[status(thm)],[t27437,t74]) ).
cnf(t27439,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),
inference(step,[status(thm)],[t27438,t416]) ).
cnf(t27440,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),
inference(step,[status(thm)],[t27439,t518]) ).
cnf(t27441,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),
inference(step,[status(thm)],[t27440,t569]) ).
cnf(t27442,plain,
sF11 = coantidomain(coantidomain(antidomain(antidomain(sF7)))),
inference(step,[status(thm)],[t27441,t609]) ).
cnf(t27443,plain,
sF11 = coantidomain(coantidomain(antidomain(sF8))),
inference(step,[status(thm)],[t27442,t642]) ).
cnf(t27444,plain,
sF11 = coantidomain(coantidomain(sF9)),
inference(step,[status(thm)],[t27443,t675]) ).
cnf(t27445,plain,
sF11 = coantidomain(sF10),
inference(step,[status(thm)],[t27444,t708]) ).
cnf(t762,plain,
coantidomain(sF10) = sF11,
inference(orient,[status(thm)],[t27445]) ).
cnf(t27446,plain,
addition(sF10,sF11) = one,
inference(step,[status(thm)],[t729,t762]) ).
cnf(t763,plain,
addition(sF10,sF11) = one,
inference(rw,[status(thm)],[t27446]) ).
cnf(t769,plain,
addition(sF10,sF11) = one,
inference(orient,[status(thm)],[t763]) ).
cnf(t14,axiom,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t134,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t14]) ).
cnf(t138,plain,
X1 = ifeq(leq(X2,X1),true,addition(X1,X2),X1),
inference(cp,[status(thm)],[t134,t76]) ).
cnf(t2434,plain,
ifeq(leq(X1,X2),true,addition(X2,X1),X2) = X2,
inference(orient,[status(thm)],[t138]) ).
cnf(t15,axiom,
ifeq2(addition(X1,X2),X2,leq(X1,X2),true) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t170,plain,
ifeq2(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(t278,plain,
true = ifeq2(multiplication(addition(X1,X2),X3),multiplication(X2,X3),leq(multiplication(X1,X3),multiplication(X2,X3)),true),
inference(cp,[status(thm)],[t170,t250]) ).
cnf(t9172,plain,
ifeq2(multiplication(addition(X1,X2),X3),multiplication(X2,X3),leq(multiplication(X1,X3),multiplication(X2,X3)),true) = true,
inference(orient,[status(thm)],[t278]) ).
cnf(t13,axiom,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t63,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(t41,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t65,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t63,t41]) ).
cnf(t83,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t65]) ).
cnf(t109,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = addition(coantidomain(X1),one),
inference(cp,[status(thm)],[t83,t105]) ).
cnf(t27331,plain,
one = addition(coantidomain(X1),one),
inference(step,[status(thm)],[t109,t105]) ).
cnf(t27332,plain,
one = addition(one,coantidomain(X1)),
inference(step,[status(thm)],[t27331,t76]) ).
cnf(t222,plain,
addition(one,coantidomain(X1)) = one,
inference(orient,[status(thm)],[t27332]) ).
cnf(t766,plain,
one = addition(one,sF11),
inference(cp,[status(thm)],[t222,t762]) ).
cnf(t27447,plain,
one = addition(sF11,one),
inference(step,[status(thm)],[t766,t76]) ).
cnf(t784,plain,
addition(sF11,one) = one,
inference(orient,[status(thm)],[t27447]) ).
cnf(t9208,plain,
true = ifeq2(multiplication(one,X1),multiplication(one,X1),leq(multiplication(sF11,X1),multiplication(one,X1)),true),
inference(cp,[status(thm)],[t9172,t784]) ).
cnf(t10,axiom,
ifeq2(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t62,plain,
ifeq2(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t28352,plain,
true = leq(multiplication(sF11,X1),multiplication(one,X1)),
inference(step,[status(thm)],[t9208,t62]) ).
cnf(t28353,plain,
true = leq(multiplication(sF11,X1),X1),
inference(step,[status(thm)],[t28352,t45]) ).
cnf(t19911,plain,
leq(multiplication(sF11,X1),X1) = true,
inference(orient,[status(thm)],[t28353]) ).
cnf(t6,axiom,
multiplication(X1,coantidomain(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t48,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t6]) ).
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(t363,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(orient,[status(thm)],[t20]) ).
cnf(t367,plain,
coantidomain(multiplication(coantidomain(coantidomain(antidomain(X1))),X1)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(X1))),X1))),
inference(cp,[status(thm)],[t363,t51]) ).
cnf(t49,plain,
zero = coantidomain(one),
inference(cp,[status(thm)],[t48,t45]) ).
cnf(t50,plain,
coantidomain(one) = zero,
inference(orient,[status(thm)],[t49]) ).
cnf(t106,plain,
one = addition(zero,coantidomain(coantidomain(one))),
inference(cp,[status(thm)],[t105,t50]) ).
cnf(t27307,plain,
one = coantidomain(coantidomain(one)),
inference(step,[status(thm)],[t106,t82]) ).
cnf(t27308,plain,
one = coantidomain(zero),
inference(step,[status(thm)],[t27307,t50]) ).
cnf(t112,plain,
coantidomain(zero) = one,
inference(orient,[status(thm)],[t27308]) ).
cnf(t28167,plain,
coantidomain(multiplication(coantidomain(coantidomain(antidomain(X1))),X1)) = addition(one,coantidomain(multiplication(coantidomain(coantidomain(antidomain(X1))),X1))),
inference(step,[status(thm)],[t367,t112]) ).
cnf(t28168,plain,
coantidomain(multiplication(coantidomain(coantidomain(antidomain(X1))),X1)) = one,
inference(step,[status(thm)],[t28167,t222]) ).
cnf(t13325,plain,
coantidomain(multiplication(coantidomain(coantidomain(antidomain(X1))),X1)) = one,
inference(orient,[status(thm)],[t28168]) ).
cnf(t13328,plain,
one = coantidomain(multiplication(coantidomain(coantidomain(sF5)),sF6)),
inference(cp,[status(thm)],[t13325,t2301]) ).
cnf(t28176,plain,
one = coantidomain(multiplication(coantidomain(sF10),sF6)),
inference(step,[status(thm)],[t13328,t2333]) ).
cnf(t28177,plain,
one = coantidomain(multiplication(sF11,sF6)),
inference(step,[status(thm)],[t28176,t762]) ).
cnf(t13384,plain,
coantidomain(multiplication(sF11,sF6)) = one,
inference(orient,[status(thm)],[t28177]) ).
cnf(t13385,plain,
zero = multiplication(multiplication(sF11,sF6),one),
inference(cp,[status(thm)],[t48,t13384]) ).
cnf(t28178,plain,
zero = multiplication(sF11,sF6),
inference(step,[status(thm)],[t13385,t43]) ).
cnf(t13392,plain,
multiplication(sF11,sF6) = zero,
inference(orient,[status(thm)],[t28178]) ).
cnf(t13396,plain,
multiplication(sF11,addition(X1,sF6)) = addition(multiplication(sF11,X1),zero),
inference(cp,[status(thm)],[t195,t13392]) ).
cnf(t28553,plain,
multiplication(sF11,addition(X1,sF6)) = multiplication(sF11,X1),
inference(step,[status(thm)],[t13396,t42]) ).
cnf(t23491,plain,
multiplication(sF11,addition(X1,sF6)) = multiplication(sF11,X1),
inference(orient,[status(thm)],[t28553]) ).
cnf(t23492,plain,
multiplication(sF11,sF5) = multiplication(sF11,one),
inference(cp,[status(thm)],[t23491,t583]) ).
cnf(t28554,plain,
multiplication(sF11,sF5) = sF11,
inference(step,[status(thm)],[t23492,t43]) ).
cnf(t23523,plain,
multiplication(sF11,sF5) = sF11,
inference(orient,[status(thm)],[t28554]) ).
cnf(t23552,plain,
true = leq(sF11,sF5),
inference(cp,[status(thm)],[t19911,t23523]) ).
cnf(t23553,plain,
leq(sF11,sF5) = true,
inference(orient,[status(thm)],[t23552]) ).
cnf(t23556,plain,
sF5 = ifeq(true,true,addition(sF5,sF11),sF5),
inference(cp,[status(thm)],[t2434,t23553]) ).
cnf(t9,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t61,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t28555,plain,
sF5 = addition(sF5,sF11),
inference(step,[status(thm)],[t23556,t61]) ).
cnf(t103,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = addition(antidomain(X1),one),
inference(cp,[status(thm)],[t83,t95]) ).
cnf(t27323,plain,
one = addition(antidomain(X1),one),
inference(step,[status(thm)],[t103,t95]) ).
cnf(t27324,plain,
one = addition(one,antidomain(X1)),
inference(step,[status(thm)],[t27323,t76]) ).
cnf(t162,plain,
addition(one,antidomain(X1)) = one,
inference(orient,[status(thm)],[t27324]) ).
cnf(t521,plain,
one = addition(one,sF5),
inference(cp,[status(thm)],[t162,t518]) ).
cnf(t27372,plain,
one = addition(sF5,one),
inference(step,[status(thm)],[t521,t76]) ).
cnf(t533,plain,
addition(sF5,one) = one,
inference(orient,[status(thm)],[t27372]) ).
cnf(t9203,plain,
true = ifeq2(multiplication(one,X1),multiplication(one,X1),leq(multiplication(sF5,X1),multiplication(one,X1)),true),
inference(cp,[status(thm)],[t9172,t533]) ).
cnf(t28344,plain,
true = leq(multiplication(sF5,X1),multiplication(one,X1)),
inference(step,[status(thm)],[t9203,t62]) ).
cnf(t28345,plain,
true = leq(multiplication(sF5,X1),X1),
inference(step,[status(thm)],[t28344,t45]) ).
cnf(t19803,plain,
leq(multiplication(sF5,X1),X1) = true,
inference(orient,[status(thm)],[t28345]) ).
cnf(t709,plain,
zero = multiplication(sF9,sF10),
inference(cp,[status(thm)],[t48,t708]) ).
cnf(t714,plain,
multiplication(sF9,sF10) = zero,
inference(orient,[status(thm)],[t709]) ).
cnf(t27713,plain,
multiplication(sF5,sF10) = zero,
inference(step,[status(thm)],[t714,t2326]) ).
cnf(t2331,plain,
multiplication(sF5,sF10) = zero,
inference(rw,[status(thm)],[t27713]) ).
cnf(t2496,plain,
multiplication(sF5,sF10) = zero,
inference(orient,[status(thm)],[t2331]) ).
cnf(t2497,plain,
multiplication(sF5,addition(sF10,X1)) = addition(zero,multiplication(sF5,X1)),
inference(cp,[status(thm)],[t195,t2496]) ).
cnf(t27983,plain,
multiplication(sF5,addition(sF10,X1)) = multiplication(sF5,X1),
inference(step,[status(thm)],[t2497,t82]) ).
cnf(t8496,plain,
multiplication(sF5,addition(sF10,X1)) = multiplication(sF5,X1),
inference(orient,[status(thm)],[t27983]) ).
cnf(t8498,plain,
multiplication(sF5,sF11) = multiplication(sF5,one),
inference(cp,[status(thm)],[t8496,t769]) ).
cnf(t27984,plain,
multiplication(sF5,sF11) = sF5,
inference(step,[status(thm)],[t8498,t43]) ).
cnf(t8521,plain,
multiplication(sF5,sF11) = sF5,
inference(orient,[status(thm)],[t27984]) ).
cnf(t19813,plain,
true = leq(sF5,sF11),
inference(cp,[status(thm)],[t19803,t8521]) ).
cnf(t19825,plain,
leq(sF5,sF11) = true,
inference(orient,[status(thm)],[t19813]) ).
cnf(t19826,plain,
sF11 = ifeq(true,true,addition(sF5,sF11),sF11),
inference(cp,[status(thm)],[t134,t19825]) ).
cnf(t28346,plain,
sF11 = addition(sF5,sF11),
inference(step,[status(thm)],[t19826,t61]) ).
cnf(t19830,plain,
addition(sF5,sF11) = sF11,
inference(orient,[status(thm)],[t28346]) ).
cnf(t28556,plain,
sF5 = sF11,
inference(step,[status(thm)],[t28555,t19830]) ).
cnf(t23558,plain,
sF11 = sF5,
inference(orient,[status(thm)],[t28556]) ).
cnf(t28559,plain,
addition(sF10,sF5) = one,
inference(step,[status(thm)],[t769,t23558]) ).
cnf(t23561,plain,
addition(sF10,sF5) = one,
inference(rw,[status(thm)],[t28559]) ).
cnf(t28581,plain,
addition(sF5,sF10) = one,
inference(step,[status(thm)],[t23561,t76]) ).
cnf(t23647,plain,
addition(sF5,sF10) = one,
inference(orient,[status(thm)],[t28581]) ).
cnf(t23654,plain,
multiplication(sF6,sF10) = multiplication(sF6,one),
inference(cp,[status(thm)],[t2128,t23647]) ).
cnf(t253,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = addition(zero,multiplication(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t250,t48]) ).
cnf(t27903,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(step,[status(thm)],[t253,t82]) ).
cnf(t6200,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t27903]) ).
cnf(t6206,plain,
multiplication(sF6,coantidomain(sF5)) = multiplication(one,coantidomain(sF5)),
inference(cp,[status(thm)],[t6200,t583]) ).
cnf(t27904,plain,
multiplication(sF6,sF10) = multiplication(one,coantidomain(sF5)),
inference(step,[status(thm)],[t6206,t2333]) ).
cnf(t27905,plain,
multiplication(sF6,sF10) = coantidomain(sF5),
inference(step,[status(thm)],[t27904,t45]) ).
cnf(t27906,plain,
multiplication(sF6,sF10) = sF10,
inference(step,[status(thm)],[t27905,t2333]) ).
cnf(t6241,plain,
multiplication(sF6,sF10) = sF10,
inference(orient,[status(thm)],[t27906]) ).
cnf(t28582,plain,
sF10 = multiplication(sF6,one),
inference(step,[status(thm)],[t23654,t6241]) ).
cnf(t28583,plain,
sF10 = sF6,
inference(step,[status(thm)],[t28582,t43]) ).
cnf(t23671,plain,
sF10 = sF6,
inference(orient,[status(thm)],[t28583]) ).
cnf(t28585,plain,
coantidomain(sF5) = sF6,
inference(step,[status(thm)],[t2333,t23671]) ).
cnf(t23675,plain,
coantidomain(sF5) = sF6,
inference(orient,[status(thm)],[t28585]) ).
cnf(t28557,plain,
coantidomain(sF10) = sF5,
inference(step,[status(thm)],[t762,t23558]) ).
cnf(t23559,plain,
coantidomain(sF10) = sF5,
inference(orient,[status(thm)],[t28557]) ).
cnf(t28584,plain,
coantidomain(sF6) = sF5,
inference(step,[status(thm)],[t23559,t23671]) ).
cnf(t23674,plain,
coantidomain(sF6) = sF5,
inference(rw,[status(thm)],[t28584]) ).
cnf(t23718,plain,
coantidomain(sF6) = sF5,
inference(orient,[status(thm)],[t23674]) ).
cnf(t16,axiom,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t67,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t16]) ).
cnf(t8522,plain,
multiplication(sF5,multiplication(sF11,X1)) = multiplication(sF5,X1),
inference(cp,[status(thm)],[t67,t8521]) ).
cnf(t19474,plain,
multiplication(sF5,multiplication(sF11,X1)) = multiplication(sF5,X1),
inference(orient,[status(thm)],[t8522]) ).
cnf(t33,axiom,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1),
introduced(definition) ).
cnf(t27448,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1),
inference(step,[status(thm)],[t33,t40]) ).
cnf(t27449,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1),
inference(step,[status(thm)],[t27448,t47]) ).
cnf(t27450,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),sK1_goals_X1),
inference(step,[status(thm)],[t27449,t58]) ).
cnf(t27451,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),sK1_goals_X1),
inference(step,[status(thm)],[t27450,t74]) ).
cnf(t27452,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1),
inference(step,[status(thm)],[t27451,t416]) ).
cnf(t27453,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1),
inference(step,[status(thm)],[t27452,t518]) ).
cnf(t27454,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1),
inference(step,[status(thm)],[t27453,t569]) ).
cnf(t27455,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(antidomain(sF7)))),sK1_goals_X1),
inference(step,[status(thm)],[t27454,t609]) ).
cnf(t27456,plain,
sF12 = multiplication(coantidomain(coantidomain(antidomain(sF8))),sK1_goals_X1),
inference(step,[status(thm)],[t27455,t642]) ).
cnf(t27457,plain,
sF12 = multiplication(coantidomain(coantidomain(sF9)),sK1_goals_X1),
inference(step,[status(thm)],[t27456,t675]) ).
cnf(t27458,plain,
sF12 = multiplication(coantidomain(sF10),sK1_goals_X1),
inference(step,[status(thm)],[t27457,t708]) ).
cnf(t27459,plain,
sF12 = multiplication(sF11,sK1_goals_X1),
inference(step,[status(thm)],[t27458,t762]) ).
cnf(t790,plain,
multiplication(sF11,sK1_goals_X1) = sF12,
inference(orient,[status(thm)],[t27459]) ).
cnf(t19475,plain,
multiplication(sF5,sK1_goals_X1) = multiplication(sF5,sF12),
inference(cp,[status(thm)],[t19474,t790]) ).
cnf(t19512,plain,
multiplication(sF5,sK1_goals_X1) = multiplication(sF5,sF12),
inference(orient,[status(thm)],[t19475]) ).
cnf(t23565,plain,
multiplication(sF5,sK1_goals_X1) = sF12,
inference(rw,[status(thm)],[t790]) ).
cnf(t28592,plain,
multiplication(sF5,sF12) = sF12,
inference(step,[status(thm)],[t23565,t19512]) ).
cnf(t23773,plain,
multiplication(sF5,sF12) = sF12,
inference(orient,[status(thm)],[t28592]) ).
cnf(t28593,plain,
multiplication(sF5,sK1_goals_X1) = sF12,
inference(step,[status(thm)],[t19512,t23773]) ).
cnf(t23774,plain,
multiplication(sF5,sK1_goals_X1) = sF12,
inference(orient,[status(thm)],[t28593]) ).
cnf(t34,axiom,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)),
introduced(definition) ).
cnf(t27462,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1)),
inference(step,[status(thm)],[t34,t40]) ).
cnf(t27463,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1)),
inference(step,[status(thm)],[t27462,t47]) ).
cnf(t27464,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),sK1_goals_X1)),
inference(step,[status(thm)],[t27463,t58]) ).
cnf(t27465,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),sK1_goals_X1)),
inference(step,[status(thm)],[t27464,t74]) ).
cnf(t27466,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1)),
inference(step,[status(thm)],[t27465,t416]) ).
cnf(t27467,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1)),
inference(step,[status(thm)],[t27466,t518]) ).
cnf(t27468,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1)),
inference(step,[status(thm)],[t27467,t569]) ).
cnf(t27469,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF7)))),sK1_goals_X1)),
inference(step,[status(thm)],[t27468,t609]) ).
cnf(t27470,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF8))),sK1_goals_X1)),
inference(step,[status(thm)],[t27469,t642]) ).
cnf(t27471,plain,
sF13 = coantidomain(multiplication(coantidomain(coantidomain(sF9)),sK1_goals_X1)),
inference(step,[status(thm)],[t27470,t675]) ).
cnf(t27472,plain,
sF13 = coantidomain(multiplication(coantidomain(sF10),sK1_goals_X1)),
inference(step,[status(thm)],[t27471,t708]) ).
cnf(t27473,plain,
sF13 = coantidomain(multiplication(sF11,sK1_goals_X1)),
inference(step,[status(thm)],[t27472,t762]) ).
cnf(t27474,plain,
sF13 = coantidomain(sF12),
inference(step,[status(thm)],[t27473,t790]) ).
cnf(t821,plain,
coantidomain(sF12) = sF13,
inference(orient,[status(thm)],[t27474]) ).
cnf(t35,axiom,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))),
introduced(definition) ).
cnf(t27478,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1))),
inference(step,[status(thm)],[t35,t40]) ).
cnf(t27479,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1))),
inference(step,[status(thm)],[t27478,t47]) ).
cnf(t27480,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),sK1_goals_X1))),
inference(step,[status(thm)],[t27479,t58]) ).
cnf(t27481,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),sK1_goals_X1))),
inference(step,[status(thm)],[t27480,t74]) ).
cnf(t27482,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1))),
inference(step,[status(thm)],[t27481,t416]) ).
cnf(t27483,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1))),
inference(step,[status(thm)],[t27482,t518]) ).
cnf(t27484,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1))),
inference(step,[status(thm)],[t27483,t569]) ).
cnf(t27485,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF7)))),sK1_goals_X1))),
inference(step,[status(thm)],[t27484,t609]) ).
cnf(t27486,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF8))),sK1_goals_X1))),
inference(step,[status(thm)],[t27485,t642]) ).
cnf(t27487,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF9)),sK1_goals_X1))),
inference(step,[status(thm)],[t27486,t675]) ).
cnf(t27488,plain,
sF14 = coantidomain(coantidomain(multiplication(coantidomain(sF10),sK1_goals_X1))),
inference(step,[status(thm)],[t27487,t708]) ).
cnf(t27489,plain,
sF14 = coantidomain(coantidomain(multiplication(sF11,sK1_goals_X1))),
inference(step,[status(thm)],[t27488,t762]) ).
cnf(t27490,plain,
sF14 = coantidomain(coantidomain(sF12)),
inference(step,[status(thm)],[t27489,t790]) ).
cnf(t27491,plain,
sF14 = coantidomain(sF13),
inference(step,[status(thm)],[t27490,t821]) ).
cnf(t855,plain,
coantidomain(sF13) = sF14,
inference(orient,[status(thm)],[t27491]) ).
cnf(t36,axiom,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))),
introduced(definition) ).
cnf(t27495,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1)))),
inference(step,[status(thm)],[t36,t40]) ).
cnf(t27496,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27495,t47]) ).
cnf(t27497,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27496,t58]) ).
cnf(t27498,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27497,t74]) ).
cnf(t27499,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27498,t416]) ).
cnf(t27500,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27499,t518]) ).
cnf(t27501,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27500,t569]) ).
cnf(t27502,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF7)))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27501,t609]) ).
cnf(t27503,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF8))),sK1_goals_X1)))),
inference(step,[status(thm)],[t27502,t642]) ).
cnf(t27504,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF9)),sK1_goals_X1)))),
inference(step,[status(thm)],[t27503,t675]) ).
cnf(t27505,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF10),sK1_goals_X1)))),
inference(step,[status(thm)],[t27504,t708]) ).
cnf(t27506,plain,
sF15 = antidomain(coantidomain(coantidomain(multiplication(sF11,sK1_goals_X1)))),
inference(step,[status(thm)],[t27505,t762]) ).
cnf(t27507,plain,
sF15 = antidomain(coantidomain(coantidomain(sF12))),
inference(step,[status(thm)],[t27506,t790]) ).
cnf(t27508,plain,
sF15 = antidomain(coantidomain(sF13)),
inference(step,[status(thm)],[t27507,t821]) ).
cnf(t27509,plain,
sF15 = antidomain(sF14),
inference(step,[status(thm)],[t27508,t855]) ).
cnf(t889,plain,
antidomain(sF14) = sF15,
inference(orient,[status(thm)],[t27509]) ).
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(t301,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(orient,[status(thm)],[t19]) ).
cnf(t305,plain,
antidomain(multiplication(X1,antidomain(antidomain(coantidomain(X1))))) = addition(antidomain(zero),antidomain(multiplication(X1,antidomain(antidomain(coantidomain(X1)))))),
inference(cp,[status(thm)],[t301,t48]) ).
cnf(t53,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t51,t43]) ).
cnf(t55,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t53]) ).
cnf(t98,plain,
one = addition(zero,antidomain(antidomain(one))),
inference(cp,[status(thm)],[t95,t55]) ).
cnf(t27305,plain,
one = antidomain(antidomain(one)),
inference(step,[status(thm)],[t98,t82]) ).
cnf(t27306,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t27305,t55]) ).
cnf(t111,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t27306]) ).
cnf(t28049,plain,
antidomain(multiplication(X1,antidomain(antidomain(coantidomain(X1))))) = addition(one,antidomain(multiplication(X1,antidomain(antidomain(coantidomain(X1)))))),
inference(step,[status(thm)],[t305,t111]) ).
cnf(t28050,plain,
antidomain(multiplication(X1,antidomain(antidomain(coantidomain(X1))))) = one,
inference(step,[status(thm)],[t28049,t162]) ).
cnf(t10480,plain,
antidomain(multiplication(X1,antidomain(antidomain(coantidomain(X1))))) = one,
inference(orient,[status(thm)],[t28050]) ).
cnf(t10482,plain,
one = antidomain(multiplication(sF13,antidomain(antidomain(sF14)))),
inference(cp,[status(thm)],[t10480,t855]) ).
cnf(t28051,plain,
one = antidomain(multiplication(sF13,antidomain(sF15))),
inference(step,[status(thm)],[t10482,t889]) ).
cnf(t37,axiom,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))),
introduced(definition) ).
cnf(t27516,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1))))),
inference(step,[status(thm)],[t37,t40]) ).
cnf(t27517,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27516,t47]) ).
cnf(t27518,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27517,t58]) ).
cnf(t27519,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27518,t74]) ).
cnf(t27520,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27519,t416]) ).
cnf(t27521,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27520,t518]) ).
cnf(t27522,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27521,t569]) ).
cnf(t27523,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF7)))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27522,t609]) ).
cnf(t27524,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF8))),sK1_goals_X1))))),
inference(step,[status(thm)],[t27523,t642]) ).
cnf(t27525,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF9)),sK1_goals_X1))))),
inference(step,[status(thm)],[t27524,t675]) ).
cnf(t27526,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF10),sK1_goals_X1))))),
inference(step,[status(thm)],[t27525,t708]) ).
cnf(t27527,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(multiplication(sF11,sK1_goals_X1))))),
inference(step,[status(thm)],[t27526,t762]) ).
cnf(t27528,plain,
sF16 = antidomain(antidomain(coantidomain(coantidomain(sF12)))),
inference(step,[status(thm)],[t27527,t790]) ).
cnf(t27529,plain,
sF16 = antidomain(antidomain(coantidomain(sF13))),
inference(step,[status(thm)],[t27528,t821]) ).
cnf(t27530,plain,
sF16 = antidomain(antidomain(sF14)),
inference(step,[status(thm)],[t27529,t855]) ).
cnf(t27531,plain,
sF16 = antidomain(sF15),
inference(step,[status(thm)],[t27530,t889]) ).
cnf(t936,plain,
antidomain(sF15) = sF16,
inference(orient,[status(thm)],[t27531]) ).
cnf(t28052,plain,
one = antidomain(multiplication(sF13,sF16)),
inference(step,[status(thm)],[t28051,t936]) ).
cnf(t10493,plain,
antidomain(multiplication(sF13,sF16)) = one,
inference(orient,[status(thm)],[t28052]) ).
cnf(t10494,plain,
zero = multiplication(one,multiplication(sF13,sF16)),
inference(cp,[status(thm)],[t51,t10493]) ).
cnf(t28053,plain,
zero = multiplication(sF13,sF16),
inference(step,[status(thm)],[t10494,t45]) ).
cnf(t10501,plain,
multiplication(sF13,sF16) = zero,
inference(orient,[status(thm)],[t28053]) ).
cnf(t10505,plain,
multiplication(sF13,addition(X1,sF16)) = addition(multiplication(sF13,X1),zero),
inference(cp,[status(thm)],[t195,t10501]) ).
cnf(t28412,plain,
multiplication(sF13,addition(X1,sF16)) = multiplication(sF13,X1),
inference(step,[status(thm)],[t10505,t42]) ).
cnf(t21135,plain,
multiplication(sF13,addition(X1,sF16)) = multiplication(sF13,X1),
inference(orient,[status(thm)],[t28412]) ).
cnf(t891,plain,
one = addition(sF15,antidomain(antidomain(sF14))),
inference(cp,[status(thm)],[t95,t889]) ).
cnf(t27511,plain,
one = addition(sF15,antidomain(sF15)),
inference(step,[status(thm)],[t891,t889]) ).
cnf(t909,plain,
addition(sF15,antidomain(sF15)) = one,
inference(orient,[status(thm)],[t27511]) ).
cnf(t27532,plain,
addition(sF15,sF16) = one,
inference(step,[status(thm)],[t909,t936]) ).
cnf(t937,plain,
addition(sF15,sF16) = one,
inference(rw,[status(thm)],[t27532]) ).
cnf(t949,plain,
addition(sF15,sF16) = one,
inference(orient,[status(thm)],[t937]) ).
cnf(t21136,plain,
multiplication(sF13,sF15) = multiplication(sF13,one),
inference(cp,[status(thm)],[t21135,t949]) ).
cnf(t938,plain,
zero = multiplication(sF16,sF15),
inference(cp,[status(thm)],[t51,t936]) ).
cnf(t955,plain,
multiplication(sF16,sF15) = zero,
inference(orient,[status(thm)],[t938]) ).
cnf(t960,plain,
multiplication(addition(X1,sF16),sF15) = addition(multiplication(X1,sF15),zero),
inference(cp,[status(thm)],[t250,t955]) ).
cnf(t27786,plain,
multiplication(addition(X1,sF16),sF15) = multiplication(X1,sF15),
inference(step,[status(thm)],[t960,t42]) ).
cnf(t3314,plain,
multiplication(addition(X1,sF16),sF15) = multiplication(X1,sF15),
inference(orient,[status(thm)],[t27786]) ).
cnf(t823,plain,
one = addition(sF13,coantidomain(coantidomain(sF12))),
inference(cp,[status(thm)],[t105,t821]) ).
cnf(t27476,plain,
one = addition(sF13,coantidomain(sF13)),
inference(step,[status(thm)],[t823,t821]) ).
cnf(t842,plain,
addition(sF13,coantidomain(sF13)) = one,
inference(orient,[status(thm)],[t27476]) ).
cnf(t27492,plain,
addition(sF13,sF14) = one,
inference(step,[status(thm)],[t842,t855]) ).
cnf(t856,plain,
addition(sF13,sF14) = one,
inference(rw,[status(thm)],[t27492]) ).
cnf(t862,plain,
addition(sF13,sF14) = one,
inference(orient,[status(thm)],[t856]) ).
cnf(t864,plain,
addition(sF13,addition(sF14,X1)) = addition(one,X1),
inference(cp,[status(thm)],[t63,t862]) ).
cnf(t2869,plain,
addition(sF13,addition(sF14,X1)) = addition(one,X1),
inference(orient,[status(thm)],[t864]) ).
cnf(t890,plain,
zero = multiplication(sF15,sF14),
inference(cp,[status(thm)],[t51,t889]) ).
cnf(t895,plain,
multiplication(sF15,sF14) = zero,
inference(orient,[status(thm)],[t890]) ).
cnf(t899,plain,
multiplication(addition(sF15,X1),sF14) = addition(zero,multiplication(X1,sF14)),
inference(cp,[status(thm)],[t250,t895]) ).
cnf(t27771,plain,
multiplication(addition(sF15,X1),sF14) = multiplication(X1,sF14),
inference(step,[status(thm)],[t899,t82]) ).
cnf(t3059,plain,
multiplication(addition(sF15,X1),sF14) = multiplication(X1,sF14),
inference(orient,[status(thm)],[t27771]) ).
cnf(t3060,plain,
multiplication(sF16,sF14) = multiplication(one,sF14),
inference(cp,[status(thm)],[t3059,t949]) ).
cnf(t27772,plain,
multiplication(sF16,sF14) = sF14,
inference(step,[status(thm)],[t3060,t45]) ).
cnf(t3070,plain,
multiplication(sF16,sF14) = sF14,
inference(orient,[status(thm)],[t27772]) ).
cnf(t3072,plain,
multiplication(sF16,addition(sF14,X1)) = addition(sF14,multiplication(sF16,X1)),
inference(cp,[status(thm)],[t195,t3070]) ).
cnf(t10921,plain,
addition(sF14,multiplication(sF16,X1)) = multiplication(sF16,addition(sF14,X1)),
inference(orient,[status(thm)],[t3072]) ).
cnf(t10922,plain,
multiplication(sF16,addition(sF14,one)) = addition(sF14,sF16),
inference(cp,[status(thm)],[t10921,t43]) ).
cnf(t859,plain,
one = addition(one,sF14),
inference(cp,[status(thm)],[t222,t855]) ).
cnf(t27493,plain,
one = addition(sF14,one),
inference(step,[status(thm)],[t859,t76]) ).
cnf(t877,plain,
addition(sF14,one) = one,
inference(orient,[status(thm)],[t27493]) ).
cnf(t28084,plain,
multiplication(sF16,one) = addition(sF14,sF16),
inference(step,[status(thm)],[t10922,t877]) ).
cnf(t28085,plain,
sF16 = addition(sF14,sF16),
inference(step,[status(thm)],[t28084,t43]) ).
cnf(t10954,plain,
addition(sF14,sF16) = sF16,
inference(orient,[status(thm)],[t28085]) ).
cnf(t10965,plain,
addition(one,sF16) = addition(sF13,sF16),
inference(cp,[status(thm)],[t2869,t10954]) ).
cnf(t28089,plain,
addition(sF16,one) = addition(sF13,sF16),
inference(step,[status(thm)],[t10965,t76]) ).
cnf(t940,plain,
one = addition(one,sF16),
inference(cp,[status(thm)],[t162,t936]) ).
cnf(t27550,plain,
one = addition(sF16,one),
inference(step,[status(thm)],[t940,t76]) ).
cnf(t963,plain,
addition(sF16,one) = one,
inference(orient,[status(thm)],[t27550]) ).
cnf(t28090,plain,
one = addition(sF13,sF16),
inference(step,[status(thm)],[t28089,t963]) ).
cnf(t11231,plain,
addition(sF13,sF16) = one,
inference(orient,[status(thm)],[t28090]) ).
cnf(t11245,plain,
multiplication(sF13,sF15) = multiplication(one,sF15),
inference(cp,[status(thm)],[t3314,t11231]) ).
cnf(t28092,plain,
multiplication(sF13,sF15) = sF15,
inference(step,[status(thm)],[t11245,t45]) ).
cnf(t11283,plain,
multiplication(sF13,sF15) = sF15,
inference(orient,[status(thm)],[t28092]) ).
cnf(t28413,plain,
sF15 = multiplication(sF13,one),
inference(step,[status(thm)],[t21136,t11283]) ).
cnf(t28414,plain,
sF15 = sF13,
inference(step,[status(thm)],[t28413,t43]) ).
cnf(t21166,plain,
sF15 = sF13,
inference(orient,[status(thm)],[t28414]) ).
cnf(t28415,plain,
antidomain(sF14) = sF13,
inference(step,[status(thm)],[t889,t21166]) ).
cnf(t21167,plain,
antidomain(sF14) = sF13,
inference(orient,[status(thm)],[t28415]) ).
cnf(t28417,plain,
antidomain(sF13) = sF16,
inference(step,[status(thm)],[t936,t21166]) ).
cnf(t21172,plain,
antidomain(sF13) = sF16,
inference(rw,[status(thm)],[t28417]) ).
cnf(t21263,plain,
antidomain(sF13) = sF16,
inference(orient,[status(thm)],[t21172]) ).
cnf(t200,plain,
multiplication(antidomain(X1),addition(X1,X2)) = addition(zero,multiplication(antidomain(X1),X2)),
inference(cp,[status(thm)],[t195,t51]) ).
cnf(t27822,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(step,[status(thm)],[t200,t82]) ).
cnf(t3901,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(orient,[status(thm)],[t27822]) ).
cnf(t3909,plain,
multiplication(antidomain(sF13),sF14) = multiplication(antidomain(sF13),one),
inference(cp,[status(thm)],[t3901,t862]) ).
cnf(t27824,plain,
multiplication(antidomain(sF13),sF14) = antidomain(sF13),
inference(step,[status(thm)],[t3909,t43]) ).
cnf(t3935,plain,
multiplication(antidomain(sF13),sF14) = antidomain(sF13),
inference(orient,[status(thm)],[t27824]) ).
cnf(t21264,plain,
multiplication(sF16,sF14) = antidomain(sF13),
inference(rw,[status(thm)],[t3935]) ).
cnf(t28458,plain,
sF14 = antidomain(sF13),
inference(step,[status(thm)],[t21264,t3070]) ).
cnf(t28459,plain,
sF14 = sF16,
inference(step,[status(thm)],[t28458,t21263]) ).
cnf(t21503,plain,
sF16 = sF14,
inference(orient,[status(thm)],[t28459]) ).
cnf(t28466,plain,
antidomain(sF13) = sF14,
inference(step,[status(thm)],[t21263,t21503]) ).
cnf(t21553,plain,
antidomain(sF13) = sF14,
inference(orient,[status(thm)],[t28466]) ).
cnf(t824,plain,
one = addition(one,sF13),
inference(cp,[status(thm)],[t222,t821]) ).
cnf(t27475,plain,
one = addition(sF13,one),
inference(step,[status(thm)],[t824,t76]) ).
cnf(t836,plain,
addition(sF13,one) = one,
inference(orient,[status(thm)],[t27475]) ).
cnf(t9211,plain,
true = ifeq2(multiplication(one,X1),multiplication(one,X1),leq(multiplication(sF13,X1),multiplication(one,X1)),true),
inference(cp,[status(thm)],[t9172,t836]) ).
cnf(t28354,plain,
true = leq(multiplication(sF13,X1),multiplication(one,X1)),
inference(step,[status(thm)],[t9211,t62]) ).
cnf(t28355,plain,
true = leq(multiplication(sF13,X1),X1),
inference(step,[status(thm)],[t28354,t45]) ).
cnf(t19926,plain,
leq(multiplication(sF13,X1),X1) = true,
inference(orient,[status(thm)],[t28355]) ).
cnf(t10504,plain,
multiplication(sF13,addition(sF16,X1)) = addition(zero,multiplication(sF13,X1)),
inference(cp,[status(thm)],[t195,t10501]) ).
cnf(t28384,plain,
multiplication(sF13,addition(sF16,X1)) = multiplication(sF13,X1),
inference(step,[status(thm)],[t10504,t82]) ).
cnf(t20803,plain,
multiplication(sF13,addition(sF16,X1)) = multiplication(sF13,X1),
inference(orient,[status(thm)],[t28384]) ).
cnf(t39,axiom,
sF18 = addition(antidomain(antidomain(sK2_goals_X0)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))),
introduced(definition) ).
cnf(t27552,plain,
sF18 = addition(antidomain(sF0),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t39,t40]) ).
cnf(t27553,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27552,t47]) ).
cnf(t27554,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27553,t40]) ).
cnf(t27555,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27554,t47]) ).
cnf(t27556,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27555,t58]) ).
cnf(t27557,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27556,t74]) ).
cnf(t27558,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27557,t416]) ).
cnf(t27559,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27558,t518]) ).
cnf(t27560,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27559,t569]) ).
cnf(t27561,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF7)))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27560,t609]) ).
cnf(t27562,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF8))),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27561,t642]) ).
cnf(t27563,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF9)),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27562,t675]) ).
cnf(t27564,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF10),sK1_goals_X1))))))),
inference(step,[status(thm)],[t27563,t708]) ).
cnf(t27565,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(sF11,sK1_goals_X1))))))),
inference(step,[status(thm)],[t27564,t762]) ).
cnf(t27566,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(sF12)))))),
inference(step,[status(thm)],[t27565,t790]) ).
cnf(t27567,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(coantidomain(sF13))))),
inference(step,[status(thm)],[t27566,t821]) ).
cnf(t27568,plain,
sF18 = addition(sF1,antidomain(antidomain(antidomain(sF14)))),
inference(step,[status(thm)],[t27567,t855]) ).
cnf(t27569,plain,
sF18 = addition(sF1,antidomain(antidomain(sF15))),
inference(step,[status(thm)],[t27568,t889]) ).
cnf(t27570,plain,
sF18 = addition(sF1,antidomain(sF16)),
inference(step,[status(thm)],[t27569,t936]) ).
cnf(t38,axiom,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
introduced(definition) ).
cnf(t27533,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t38,t40]) ).
cnf(t27534,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27533,t47]) ).
cnf(t27535,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF2))))))))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27534,t58]) ).
cnf(t27536,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF3)))))))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27535,t74]) ).
cnf(t27537,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27536,t416]) ).
cnf(t27538,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27537,t518]) ).
cnf(t27539,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27538,t569]) ).
cnf(t27540,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF7)))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27539,t609]) ).
cnf(t27541,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF8))),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27540,t642]) ).
cnf(t27542,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF9)),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27541,t675]) ).
cnf(t27543,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF10),sK1_goals_X1)))))),
inference(step,[status(thm)],[t27542,t708]) ).
cnf(t27544,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(sF11,sK1_goals_X1)))))),
inference(step,[status(thm)],[t27543,t762]) ).
cnf(t27545,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(coantidomain(sF12))))),
inference(step,[status(thm)],[t27544,t790]) ).
cnf(t27546,plain,
sF17 = antidomain(antidomain(antidomain(coantidomain(sF13)))),
inference(step,[status(thm)],[t27545,t821]) ).
cnf(t27547,plain,
sF17 = antidomain(antidomain(antidomain(sF14))),
inference(step,[status(thm)],[t27546,t855]) ).
cnf(t27548,plain,
sF17 = antidomain(antidomain(sF15)),
inference(step,[status(thm)],[t27547,t889]) ).
cnf(t27549,plain,
sF17 = antidomain(sF16),
inference(step,[status(thm)],[t27548,t936]) ).
cnf(t943,plain,
antidomain(sF16) = sF17,
inference(orient,[status(thm)],[t27549]) ).
cnf(t27571,plain,
sF18 = addition(sF1,sF17),
inference(step,[status(thm)],[t27570,t943]) ).
cnf(t983,plain,
addition(sF1,sF17) = sF18,
inference(orient,[status(thm)],[t27571]) ).
cnf(t944,plain,
zero = multiplication(sF17,sF16),
inference(cp,[status(thm)],[t51,t943]) ).
cnf(t969,plain,
multiplication(sF17,sF16) = zero,
inference(orient,[status(thm)],[t944]) ).
cnf(t972,plain,
multiplication(sF17,addition(X1,sF16)) = addition(multiplication(sF17,X1),zero),
inference(cp,[status(thm)],[t195,t969]) ).
cnf(t27791,plain,
multiplication(sF17,addition(X1,sF16)) = multiplication(sF17,X1),
inference(step,[status(thm)],[t972,t42]) ).
cnf(t3450,plain,
multiplication(sF17,addition(X1,sF16)) = multiplication(sF17,X1),
inference(orient,[status(thm)],[t27791]) ).
cnf(t3451,plain,
multiplication(sF17,sF15) = multiplication(sF17,one),
inference(cp,[status(thm)],[t3450,t949]) ).
cnf(t959,plain,
multiplication(addition(sF16,X1),sF15) = addition(zero,multiplication(X1,sF15)),
inference(cp,[status(thm)],[t250,t955]) ).
cnf(t27784,plain,
multiplication(addition(sF16,X1),sF15) = multiplication(X1,sF15),
inference(step,[status(thm)],[t959,t82]) ).
cnf(t3285,plain,
multiplication(addition(sF16,X1),sF15) = multiplication(X1,sF15),
inference(orient,[status(thm)],[t27784]) ).
cnf(t939,plain,
one = addition(sF16,antidomain(antidomain(sF15))),
inference(cp,[status(thm)],[t95,t936]) ).
cnf(t27583,plain,
one = addition(sF16,antidomain(sF16)),
inference(step,[status(thm)],[t939,t936]) ).
cnf(t27584,plain,
one = addition(sF16,sF17),
inference(step,[status(thm)],[t27583,t943]) ).
cnf(t1062,plain,
addition(sF16,sF17) = one,
inference(orient,[status(thm)],[t27584]) ).
cnf(t3286,plain,
multiplication(sF17,sF15) = multiplication(one,sF15),
inference(cp,[status(thm)],[t3285,t1062]) ).
cnf(t27785,plain,
multiplication(sF17,sF15) = sF15,
inference(step,[status(thm)],[t3286,t45]) ).
cnf(t3296,plain,
multiplication(sF17,sF15) = sF15,
inference(orient,[status(thm)],[t27785]) ).
cnf(t27792,plain,
sF15 = multiplication(sF17,one),
inference(step,[status(thm)],[t3451,t3296]) ).
cnf(t27793,plain,
sF15 = sF17,
inference(step,[status(thm)],[t27792,t43]) ).
cnf(t3459,plain,
sF17 = sF15,
inference(orient,[status(thm)],[t27793]) ).
cnf(t27796,plain,
addition(sF1,sF15) = sF18,
inference(step,[status(thm)],[t983,t3459]) ).
cnf(t3465,plain,
addition(sF1,sF15) = sF18,
inference(rw,[status(thm)],[t27796]) ).
cnf(t3482,plain,
addition(sF1,sF15) = sF18,
inference(orient,[status(thm)],[t3465]) ).
cnf(t3484,plain,
addition(sF1,addition(sF15,X1)) = addition(sF18,X1),
inference(cp,[status(thm)],[t63,t3482]) ).
cnf(t12381,plain,
addition(sF1,addition(sF15,X1)) = addition(sF18,X1),
inference(orient,[status(thm)],[t3484]) ).
cnf(t12389,plain,
addition(sF18,sF16) = addition(sF1,one),
inference(cp,[status(thm)],[t12381,t949]) ).
cnf(t28135,plain,
addition(sF16,sF18) = addition(sF1,one),
inference(step,[status(thm)],[t12389,t76]) ).
cnf(t85,plain,
addition(X1,X2) = addition(addition(X1,X2),X1),
inference(cp,[status(thm)],[t83,t76]) ).
cnf(t27302,plain,
addition(X1,X2) = addition(X1,addition(X2,X1)),
inference(step,[status(thm)],[t85,t63]) ).
cnf(t90,plain,
addition(X1,addition(X2,X1)) = addition(X1,X2),
inference(orient,[status(thm)],[t27302]) ).
cnf(t117,plain,
addition(sF1,sF0) = addition(sF1,one),
inference(cp,[status(thm)],[t90,t113]) ).
cnf(t27316,plain,
addition(sF0,sF1) = addition(sF1,one),
inference(step,[status(thm)],[t117,t76]) ).
cnf(t27317,plain,
one = addition(sF1,one),
inference(step,[status(thm)],[t27316,t113]) ).
cnf(t131,plain,
addition(sF1,one) = one,
inference(orient,[status(thm)],[t27317]) ).
cnf(t28136,plain,
addition(sF16,sF18) = one,
inference(step,[status(thm)],[t28135,t131]) ).
cnf(t12425,plain,
addition(sF16,sF18) = one,
inference(orient,[status(thm)],[t28136]) ).
cnf(t20807,plain,
multiplication(sF13,sF18) = multiplication(sF13,one),
inference(cp,[status(thm)],[t20803,t12425]) ).
cnf(t28385,plain,
multiplication(sF13,sF18) = sF13,
inference(step,[status(thm)],[t20807,t43]) ).
cnf(t20839,plain,
multiplication(sF13,sF18) = sF13,
inference(orient,[status(thm)],[t28385]) ).
cnf(t20876,plain,
true = leq(sF13,sF18),
inference(cp,[status(thm)],[t19926,t20839]) ).
cnf(t20877,plain,
leq(sF13,sF18) = true,
inference(orient,[status(thm)],[t20876]) ).
cnf(t20878,plain,
sF18 = ifeq(true,true,addition(sF13,sF18),sF18),
inference(cp,[status(thm)],[t134,t20877]) ).
cnf(t28386,plain,
sF18 = addition(sF13,sF18),
inference(step,[status(thm)],[t20878,t61]) ).
cnf(t79,plain,
addition(X1,addition(X2,X3)) = addition(addition(X2,X1),X3),
inference(cp,[status(thm)],[t63,t76]) ).
cnf(t27600,plain,
addition(X1,addition(X2,X3)) = addition(X2,addition(X1,X3)),
inference(step,[status(thm)],[t79,t63]) ).
cnf(t1253,plain,
addition(X1,addition(X2,X3)) = addition(X2,addition(X1,X3)),
inference(orient,[status(thm)],[t27600]) ).
cnf(t3490,plain,
addition(sF1,addition(X1,sF15)) = addition(X1,sF18),
inference(cp,[status(thm)],[t1253,t3482]) ).
cnf(t12866,plain,
addition(sF1,addition(X1,sF15)) = addition(X1,sF18),
inference(orient,[status(thm)],[t3490]) ).
cnf(t898,plain,
multiplication(sF15,addition(X1,sF14)) = addition(multiplication(sF15,X1),zero),
inference(cp,[status(thm)],[t195,t895]) ).
cnf(t27769,plain,
multiplication(sF15,addition(X1,sF14)) = multiplication(sF15,X1),
inference(step,[status(thm)],[t898,t42]) ).
cnf(t3038,plain,
multiplication(sF15,addition(X1,sF14)) = multiplication(sF15,X1),
inference(orient,[status(thm)],[t27769]) ).
cnf(t3039,plain,
multiplication(sF15,sF13) = multiplication(sF15,one),
inference(cp,[status(thm)],[t3038,t862]) ).
cnf(t27770,plain,
multiplication(sF15,sF13) = sF15,
inference(step,[status(thm)],[t3039,t43]) ).
cnf(t3048,plain,
multiplication(sF15,sF13) = sF15,
inference(orient,[status(thm)],[t27770]) ).
cnf(t3052,plain,
multiplication(addition(sF15,X1),sF13) = addition(sF15,multiplication(X1,sF13)),
inference(cp,[status(thm)],[t250,t3048]) ).
cnf(t10775,plain,
addition(sF15,multiplication(X1,sF13)) = multiplication(addition(sF15,X1),sF13),
inference(orient,[status(thm)],[t3052]) ).
cnf(t10776,plain,
multiplication(addition(sF15,one),sF13) = addition(sF15,sF13),
inference(cp,[status(thm)],[t10775,t45]) ).
cnf(t892,plain,
one = addition(one,sF15),
inference(cp,[status(thm)],[t162,t889]) ).
cnf(t27510,plain,
one = addition(sF15,one),
inference(step,[status(thm)],[t892,t76]) ).
cnf(t903,plain,
addition(sF15,one) = one,
inference(orient,[status(thm)],[t27510]) ).
cnf(t28076,plain,
multiplication(one,sF13) = addition(sF15,sF13),
inference(step,[status(thm)],[t10776,t903]) ).
cnf(t28077,plain,
sF13 = addition(sF15,sF13),
inference(step,[status(thm)],[t28076,t45]) ).
cnf(t28078,plain,
sF13 = addition(sF13,sF15),
inference(step,[status(thm)],[t28077,t76]) ).
cnf(t10803,plain,
addition(sF13,sF15) = sF13,
inference(orient,[status(thm)],[t28078]) ).
cnf(t12871,plain,
addition(sF13,sF18) = addition(sF1,sF13),
inference(cp,[status(thm)],[t12866,t10803]) ).
cnf(t12926,plain,
addition(sF13,sF18) = addition(sF1,sF13),
inference(orient,[status(thm)],[t12871]) ).
cnf(t28387,plain,
sF18 = addition(sF1,sF13),
inference(step,[status(thm)],[t28386,t12926]) ).
cnf(t20882,plain,
addition(sF1,sF13) = sF18,
inference(orient,[status(thm)],[t28387]) ).
cnf(t20843,plain,
multiplication(addition(sF13,X1),sF18) = addition(sF13,multiplication(X1,sF18)),
inference(cp,[status(thm)],[t250,t20839]) ).
cnf(t27115,plain,
addition(sF13,multiplication(X1,sF18)) = multiplication(addition(sF13,X1),sF18),
inference(orient,[status(thm)],[t20843]) ).
cnf(t822,plain,
zero = multiplication(sF12,sF13),
inference(cp,[status(thm)],[t48,t821]) ).
cnf(t827,plain,
multiplication(sF12,sF13) = zero,
inference(orient,[status(thm)],[t822]) ).
cnf(t834,plain,
coantidomain(multiplication(coantidomain(coantidomain(sF12)),sF13)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF12)),sF13))),
inference(cp,[status(thm)],[t363,t827]) ).
cnf(t27749,plain,
coantidomain(multiplication(coantidomain(sF13),sF13)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF12)),sF13))),
inference(step,[status(thm)],[t834,t821]) ).
cnf(t27750,plain,
coantidomain(multiplication(sF14,sF13)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF12)),sF13))),
inference(step,[status(thm)],[t27749,t855]) ).
cnf(t27751,plain,
coantidomain(multiplication(sF14,sF13)) = addition(one,coantidomain(multiplication(coantidomain(coantidomain(sF12)),sF13))),
inference(step,[status(thm)],[t27750,t112]) ).
cnf(t27752,plain,
coantidomain(multiplication(sF14,sF13)) = one,
inference(step,[status(thm)],[t27751,t222]) ).
cnf(t2843,plain,
coantidomain(multiplication(sF14,sF13)) = one,
inference(orient,[status(thm)],[t27752]) ).
cnf(t2844,plain,
zero = multiplication(multiplication(sF14,sF13),one),
inference(cp,[status(thm)],[t48,t2843]) ).
cnf(t27753,plain,
zero = multiplication(sF14,sF13),
inference(step,[status(thm)],[t2844,t43]) ).
cnf(t2848,plain,
multiplication(sF14,sF13) = zero,
inference(orient,[status(thm)],[t27753]) ).
cnf(t2851,plain,
multiplication(sF14,addition(sF13,X1)) = addition(zero,multiplication(sF14,X1)),
inference(cp,[status(thm)],[t195,t2848]) ).
cnf(t28044,plain,
multiplication(sF14,addition(sF13,X1)) = multiplication(sF14,X1),
inference(step,[status(thm)],[t2851,t82]) ).
cnf(t10392,plain,
multiplication(sF14,addition(sF13,X1)) = multiplication(sF14,X1),
inference(orient,[status(thm)],[t28044]) ).
cnf(t12953,plain,
multiplication(sF14,sF18) = multiplication(sF14,addition(sF1,sF13)),
inference(cp,[status(thm)],[t10392,t12926]) ).
cnf(t2852,plain,
multiplication(sF14,addition(X1,sF13)) = addition(multiplication(sF14,X1),zero),
inference(cp,[status(thm)],[t195,t2848]) ).
cnf(t28045,plain,
multiplication(sF14,addition(X1,sF13)) = multiplication(sF14,X1),
inference(step,[status(thm)],[t2852,t42]) ).
cnf(t10416,plain,
multiplication(sF14,addition(X1,sF13)) = multiplication(sF14,X1),
inference(orient,[status(thm)],[t28045]) ).
cnf(t28152,plain,
multiplication(sF14,sF18) = multiplication(sF14,sF1),
inference(step,[status(thm)],[t12953,t10416]) ).
cnf(t12985,plain,
multiplication(sF14,sF18) = multiplication(sF14,sF1),
inference(orient,[status(thm)],[t28152]) ).
cnf(t791,plain,
multiplication(sF11,multiplication(sK1_goals_X1,X1)) = multiplication(sF12,X1),
inference(cp,[status(thm)],[t67,t790]) ).
cnf(t2661,plain,
multiplication(sF11,multiplication(sK1_goals_X1,X1)) = multiplication(sF12,X1),
inference(orient,[status(thm)],[t791]) ).
cnf(t1741,plain,
multiplication(sK1_goals_X1,multiplication(sF1,X1)) = multiplication(sF4,X1),
inference(cp,[status(thm)],[t67,t1740]) ).
cnf(t5893,plain,
multiplication(sK1_goals_X1,multiplication(sF1,X1)) = multiplication(sF4,X1),
inference(orient,[status(thm)],[t1741]) ).
cnf(t52,plain,
zero = multiplication(sF0,sK2_goals_X0),
inference(cp,[status(thm)],[t51,t40]) ).
cnf(t56,plain,
multiplication(sF0,sK2_goals_X0) = zero,
inference(orient,[status(thm)],[t52]) ).
cnf(t257,plain,
multiplication(addition(sF0,X1),sK2_goals_X0) = addition(zero,multiplication(X1,sK2_goals_X0)),
inference(cp,[status(thm)],[t250,t56]) ).
cnf(t27603,plain,
multiplication(addition(sF0,X1),sK2_goals_X0) = multiplication(X1,sK2_goals_X0),
inference(step,[status(thm)],[t257,t82]) ).
cnf(t1424,plain,
multiplication(addition(sF0,X1),sK2_goals_X0) = multiplication(X1,sK2_goals_X0),
inference(orient,[status(thm)],[t27603]) ).
cnf(t1425,plain,
multiplication(sF1,sK2_goals_X0) = multiplication(one,sK2_goals_X0),
inference(cp,[status(thm)],[t1424,t113]) ).
cnf(t27606,plain,
multiplication(sF1,sK2_goals_X0) = sK2_goals_X0,
inference(step,[status(thm)],[t1425,t45]) ).
cnf(t1485,plain,
multiplication(sF1,sK2_goals_X0) = sK2_goals_X0,
inference(orient,[status(thm)],[t27606]) ).
cnf(t5903,plain,
multiplication(sF4,sK2_goals_X0) = multiplication(sK1_goals_X1,sK2_goals_X0),
inference(cp,[status(thm)],[t5893,t1485]) ).
cnf(t5999,plain,
multiplication(sK1_goals_X1,sK2_goals_X0) = multiplication(sF4,sK2_goals_X0),
inference(orient,[status(thm)],[t5903]) ).
cnf(t6008,plain,
multiplication(sF12,sK2_goals_X0) = multiplication(sF11,multiplication(sF4,sK2_goals_X0)),
inference(cp,[status(thm)],[t2661,t5999]) ).
cnf(t17317,plain,
multiplication(sF11,multiplication(sF4,sK2_goals_X0)) = multiplication(sF12,sK2_goals_X0),
inference(orient,[status(thm)],[t6008]) ).
cnf(t13327,plain,
one = coantidomain(multiplication(coantidomain(coantidomain(sF5)),sF4)),
inference(cp,[status(thm)],[t13325,t518]) ).
cnf(t28169,plain,
one = coantidomain(multiplication(coantidomain(sF10),sF4)),
inference(step,[status(thm)],[t13327,t2333]) ).
cnf(t28170,plain,
one = coantidomain(multiplication(sF11,sF4)),
inference(step,[status(thm)],[t28169,t762]) ).
cnf(t13343,plain,
coantidomain(multiplication(sF11,sF4)) = one,
inference(orient,[status(thm)],[t28170]) ).
cnf(t13344,plain,
zero = multiplication(multiplication(sF11,sF4),one),
inference(cp,[status(thm)],[t48,t13343]) ).
cnf(t28171,plain,
zero = multiplication(sF11,sF4),
inference(step,[status(thm)],[t13344,t43]) ).
cnf(t13352,plain,
multiplication(sF11,sF4) = zero,
inference(orient,[status(thm)],[t28171]) ).
cnf(t13359,plain,
multiplication(sF11,multiplication(sF4,X1)) = multiplication(zero,X1),
inference(cp,[status(thm)],[t67,t13352]) ).
cnf(t5,axiom,
multiplication(zero,X1) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t46,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t28527,plain,
multiplication(sF11,multiplication(sF4,X1)) = zero,
inference(step,[status(thm)],[t13359,t46]) ).
cnf(t22978,plain,
multiplication(sF11,multiplication(sF4,X1)) = zero,
inference(orient,[status(thm)],[t28527]) ).
cnf(t28530,plain,
zero = multiplication(sF12,sK2_goals_X0),
inference(step,[status(thm)],[t17317,t22978]) ).
cnf(t22981,plain,
zero = multiplication(sF12,sK2_goals_X0),
inference(rw,[status(thm)],[t28530]) ).
cnf(t23012,plain,
multiplication(sF12,sK2_goals_X0) = zero,
inference(orient,[status(thm)],[t22981]) ).
cnf(t23018,plain,
coantidomain(multiplication(coantidomain(coantidomain(sF12)),sK2_goals_X0)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF12)),sK2_goals_X0))),
inference(cp,[status(thm)],[t363,t23012]) ).
cnf(t28533,plain,
coantidomain(multiplication(coantidomain(sF13),sK2_goals_X0)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF12)),sK2_goals_X0))),
inference(step,[status(thm)],[t23018,t821]) ).
cnf(t28534,plain,
coantidomain(multiplication(sF14,sK2_goals_X0)) = addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(sF12)),sK2_goals_X0))),
inference(step,[status(thm)],[t28533,t855]) ).
cnf(t28535,plain,
coantidomain(multiplication(sF14,sK2_goals_X0)) = addition(one,coantidomain(multiplication(coantidomain(coantidomain(sF12)),sK2_goals_X0))),
inference(step,[status(thm)],[t28534,t112]) ).
cnf(t28536,plain,
coantidomain(multiplication(sF14,sK2_goals_X0)) = one,
inference(step,[status(thm)],[t28535,t222]) ).
cnf(t23041,plain,
coantidomain(multiplication(sF14,sK2_goals_X0)) = one,
inference(orient,[status(thm)],[t28536]) ).
cnf(t23042,plain,
zero = multiplication(multiplication(sF14,sK2_goals_X0),one),
inference(cp,[status(thm)],[t48,t23041]) ).
cnf(t28537,plain,
zero = multiplication(sF14,sK2_goals_X0),
inference(step,[status(thm)],[t23042,t43]) ).
cnf(t23049,plain,
multiplication(sF14,sK2_goals_X0) = zero,
inference(orient,[status(thm)],[t28537]) ).
cnf(t23056,plain,
antidomain(multiplication(sF14,antidomain(antidomain(sK2_goals_X0)))) = addition(antidomain(zero),antidomain(multiplication(sF14,antidomain(antidomain(sK2_goals_X0))))),
inference(cp,[status(thm)],[t301,t23049]) ).
cnf(t28538,plain,
antidomain(multiplication(sF14,antidomain(sF0))) = addition(antidomain(zero),antidomain(multiplication(sF14,antidomain(antidomain(sK2_goals_X0))))),
inference(step,[status(thm)],[t23056,t40]) ).
cnf(t28539,plain,
antidomain(multiplication(sF14,sF1)) = addition(antidomain(zero),antidomain(multiplication(sF14,antidomain(antidomain(sK2_goals_X0))))),
inference(step,[status(thm)],[t28538,t47]) ).
cnf(t28540,plain,
antidomain(multiplication(sF14,sF1)) = addition(one,antidomain(multiplication(sF14,antidomain(antidomain(sK2_goals_X0))))),
inference(step,[status(thm)],[t28539,t111]) ).
cnf(t28541,plain,
antidomain(multiplication(sF14,sF1)) = one,
inference(step,[status(thm)],[t28540,t162]) ).
cnf(t23080,plain,
antidomain(multiplication(sF14,sF1)) = one,
inference(orient,[status(thm)],[t28541]) ).
cnf(t23081,plain,
zero = multiplication(one,multiplication(sF14,sF1)),
inference(cp,[status(thm)],[t51,t23080]) ).
cnf(t28542,plain,
zero = multiplication(sF14,sF1),
inference(step,[status(thm)],[t23081,t45]) ).
cnf(t23088,plain,
multiplication(sF14,sF1) = zero,
inference(orient,[status(thm)],[t28542]) ).
cnf(t28543,plain,
multiplication(sF14,sF18) = zero,
inference(step,[status(thm)],[t12985,t23088]) ).
cnf(t23089,plain,
multiplication(sF14,sF18) = zero,
inference(orient,[status(thm)],[t28543]) ).
cnf(t27121,plain,
multiplication(addition(sF13,sF14),sF18) = addition(sF13,zero),
inference(cp,[status(thm)],[t27115,t23089]) ).
cnf(t28714,plain,
multiplication(one,sF18) = addition(sF13,zero),
inference(step,[status(thm)],[t27121,t862]) ).
cnf(t28715,plain,
sF18 = addition(sF13,zero),
inference(step,[status(thm)],[t28714,t45]) ).
cnf(t28716,plain,
sF18 = sF13,
inference(step,[status(thm)],[t28715,t42]) ).
cnf(t27157,plain,
sF18 = sF13,
inference(orient,[status(thm)],[t28716]) ).
cnf(t28758,plain,
addition(sF1,sF13) = sF13,
inference(step,[status(thm)],[t20882,t27157]) ).
cnf(t27248,plain,
addition(sF1,sF13) = sF13,
inference(orient,[status(thm)],[t28758]) ).
cnf(u3,negated_conjecture,
addition(domain(sK2_goals_X0),backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0)))) != backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
domain(X0) = antidomain(antidomain(X0)),
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(u6,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(u4,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)],[u4,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)],[u6,d2,d5]) ).
cnf(goal_0,negated_conjecture,
addition(antidomain(antidomain(sK2_goals_X0)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(definition_unfolding,[status(thm)],[u3,d0,d4,d7]) ).
cnf(g0_0,plain,
addition(antidomain(sF0),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[goal_0,t40]) ).
cnf(g0_1,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_0,t47]) ).
cnf(g0_2,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_1,t40]) ).
cnf(g0_3,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_2,t47]) ).
cnf(g0_4,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF0))))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_3,t1617]) ).
cnf(g0_5,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF1)))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_4,t47]) ).
cnf(g0_6,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_5,t1740]) ).
cnf(g0_7,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_6,t518]) ).
cnf(g0_8,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_7,t569]) ).
cnf(g0_9,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF5)))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_8,t2301]) ).
cnf(g0_10,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF6))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_9,t569]) ).
cnf(g0_11,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF5)),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_10,t2301]) ).
cnf(g0_12,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF6),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_11,t23675]) ).
cnf(g0_13,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(sF5,sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_12,t23718]) ).
cnf(g0_14,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(coantidomain(sF12)))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_13,t23774]) ).
cnf(g0_15,plain,
addition(sF1,antidomain(antidomain(antidomain(coantidomain(sF13))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_14,t821]) ).
cnf(g0_16,plain,
addition(sF1,antidomain(antidomain(antidomain(sF14)))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_15,t855]) ).
cnf(g0_17,plain,
addition(sF1,antidomain(antidomain(sF13))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_16,t21167]) ).
cnf(g0_18,plain,
addition(sF1,antidomain(sF14)) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_17,t21553]) ).
cnf(g0_19,plain,
addition(sF1,sF13) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_18,t21167]) ).
cnf(g0_20,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_19,t27248]) ).
cnf(g0_21,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(sF0))))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_20,t40]) ).
cnf(g0_22,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(sF1)))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_21,t47]) ).
cnf(g0_23,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(sF0))))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_22,t1617]) ).
cnf(g0_24,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,sF1)))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_23,t47]) ).
cnf(g0_25,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sF4))))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_24,t1740]) ).
cnf(g0_26,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(sF5)))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_25,t518]) ).
cnf(g0_27,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sF6))))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_26,t569]) ).
cnf(g0_28,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sF5)))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_27,t2301]) ).
cnf(g0_29,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sF6))),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_28,t569]) ).
cnf(g0_30,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(sF5)),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_29,t2301]) ).
cnf(g0_31,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(sF6),sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_30,t23675]) ).
cnf(g0_32,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(sF5,sK1_goals_X1)))))),
inference(rw,[status(thm)],[g0_31,t23718]) ).
cnf(g0_33,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(coantidomain(sF12))))),
inference(rw,[status(thm)],[g0_32,t23774]) ).
cnf(g0_34,plain,
sF13 != antidomain(antidomain(antidomain(coantidomain(sF13)))),
inference(rw,[status(thm)],[g0_33,t821]) ).
cnf(g0_35,plain,
sF13 != antidomain(antidomain(antidomain(sF14))),
inference(rw,[status(thm)],[g0_34,t855]) ).
cnf(g0_36,plain,
sF13 != antidomain(antidomain(sF13)),
inference(rw,[status(thm)],[g0_35,t21167]) ).
cnf(g0_37,plain,
sF13 != antidomain(sF14),
inference(rw,[status(thm)],[g0_36,t21553]) ).
cnf(g0_38,plain,
sF13 != sF13,
inference(rw,[status(thm)],[g0_37,t21167]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_38]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE110-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 18:58:27 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 48.26/7.61 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 48.26/7.61 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------