%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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 12:59:39 PM UTC 2026
% Result : Unsatisfiable 6.00s 1.33s
% Output : CNFRefutation 6.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 115
% Number of leaves : 10
% Syntax : Number of clauses : 297 ( 297 unt; 0 nHn; 70 RR)
% Number of literals : 297 ( 296 equ; 6 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 309 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
inference(orient,[status(thm)],[t2]) ).
cnf(t7,axiom,
multiply(add(X1,inverse(X1)),multiply(add(X1,X2),add(inverse(X1),X2))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,plain,
multiply(add(X1,inverse(X1)),multiply(add(X1,X2),add(inverse(X1),X2))) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t3,axiom,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t3]) ).
cnf(t3077,plain,
multiply(add(X1,inverse(X1)),add(X2,multiply(X1,inverse(X1)))) = X2,
inference(step,[status(thm)],[t10,t44]) ).
cnf(t1,axiom,
multiply(X1,inverse(X1)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t41,plain,
multiply(X1,inverse(X1)) = n0,
inference(orient,[status(thm)],[t1]) ).
cnf(t3078,plain,
multiply(add(X1,inverse(X1)),add(X2,n0)) = X2,
inference(step,[status(thm)],[t3077,t41]) ).
cnf(t49,plain,
multiply(add(X1,inverse(X1)),add(X2,n0)) = X2,
inference(rw,[status(thm)],[t3078]) ).
cnf(t0,axiom,
add(X1,inverse(X1)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t52,plain,
add(X1,inverse(X1)) = n1,
inference(orient,[status(thm)],[t0]) ).
cnf(t3081,plain,
multiply(n1,add(X2,n0)) = X2,
inference(step,[status(thm)],[t49,t52]) ).
cnf(t55,plain,
multiply(n1,add(X1,n0)) = X1,
inference(orient,[status(thm)],[t3081]) ).
cnf(t56,plain,
multiply(add(X1,n0),add(n1,X2)) = add(X1,multiply(X2,add(X1,n0))),
inference(cp,[status(thm)],[t28,t55]) ).
cnf(t85,plain,
add(X1,multiply(X2,add(X1,n0))) = multiply(add(X1,n0),add(n1,X2)),
inference(orient,[status(thm)],[t56]) ).
cnf(t87,plain,
multiply(add(X1,n0),add(n1,n1)) = add(X1,X1),
inference(cp,[status(thm)],[t85,t55]) ).
cnf(t100,plain,
multiply(add(X1,n0),add(n1,n1)) = add(X1,X1),
inference(orient,[status(thm)],[t87]) ).
cnf(t45,plain,
add(multiply(X1,X2),multiply(multiply(X3,X2),Y3)) = multiply(multiply(X2,add(X3,X1)),add(Y3,multiply(X1,X2))),
inference(cp,[status(thm)],[t44,t28]) ).
cnf(t415,plain,
multiply(multiply(X1,add(X2,X3)),add(Y3,multiply(X3,X1))) = add(multiply(X3,X1),multiply(multiply(X2,X1),Y3)),
inference(orient,[status(thm)],[t45]) ).
cnf(t417,plain,
add(multiply(n0,n1),multiply(multiply(X1,n1),X2)) = multiply(X1,add(X2,multiply(n0,n1))),
inference(cp,[status(thm)],[t415,t55]) ).
cnf(t627,plain,
add(multiply(n0,n1),multiply(multiply(X1,n1),X2)) = multiply(X1,add(X2,multiply(n0,n1))),
inference(orient,[status(thm)],[t417]) ).
cnf(t628,plain,
multiply(X1,add(n1,multiply(n0,n1))) = multiply(n1,add(n0,multiply(X1,n1))),
inference(cp,[status(thm)],[t627,t28]) ).
cnf(t5,axiom,
add(multiply(X1,inverse(X2)),add(multiply(X1,X1),multiply(inverse(X2),X1))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X1),multiply(inverse(X2),X1))) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t3074,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t25,t28]) ).
cnf(t38,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(rw,[status(thm)],[t3074]) ).
cnf(t115,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t38]) ).
cnf(t116,plain,
X1 = add(n0,multiply(X1,add(X1,inverse(X1)))),
inference(cp,[status(thm)],[t115,t41]) ).
cnf(t3082,plain,
X1 = add(n0,multiply(X1,n1)),
inference(step,[status(thm)],[t116,t52]) ).
cnf(t123,plain,
add(n0,multiply(X1,n1)) = X1,
inference(orient,[status(thm)],[t3082]) ).
cnf(t3087,plain,
multiply(X1,add(n1,multiply(n0,n1))) = multiply(n1,X1),
inference(step,[status(thm)],[t628,t123]) ).
cnf(t645,plain,
multiply(X1,add(n1,multiply(n0,n1))) = multiply(n1,X1),
inference(orient,[status(thm)],[t3087]) ).
cnf(t646,plain,
multiply(n1,add(X1,multiply(n0,n1))) = add(multiply(n0,n1),multiply(X1,n1)),
inference(cp,[status(thm)],[t645,t44]) ).
cnf(t3088,plain,
multiply(n1,add(X1,multiply(n0,n1))) = multiply(n1,add(n0,X1)),
inference(step,[status(thm)],[t646,t28]) ).
cnf(t658,plain,
multiply(n1,add(X1,multiply(n0,n1))) = multiply(n1,add(n0,X1)),
inference(orient,[status(thm)],[t3088]) ).
cnf(t659,plain,
multiply(n1,add(n0,n1)) = multiply(n1,n1),
inference(cp,[status(thm)],[t658,t645]) ).
cnf(t680,plain,
multiply(n1,add(n0,n1)) = multiply(n1,n1),
inference(orient,[status(thm)],[t659]) ).
cnf(t682,plain,
multiply(add(n0,n1),add(X1,n1)) = add(multiply(X1,add(n0,n1)),multiply(n1,n1)),
inference(cp,[status(thm)],[t28,t680]) ).
cnf(t3099,plain,
add(n1,multiply(n0,X1)) = add(multiply(X1,add(n0,n1)),multiply(n1,n1)),
inference(step,[status(thm)],[t682,t44]) ).
cnf(t828,plain,
add(multiply(X1,add(n0,n1)),multiply(n1,n1)) = add(n1,multiply(n0,X1)),
inference(orient,[status(thm)],[t3099]) ).
cnf(t829,plain,
add(n1,multiply(n0,n1)) = add(multiply(n1,n1),multiply(n1,n1)),
inference(cp,[status(thm)],[t828,t680]) ).
cnf(t3100,plain,
add(n1,multiply(n0,n1)) = multiply(n1,add(n1,n1)),
inference(step,[status(thm)],[t829,t28]) ).
cnf(t838,plain,
add(n1,multiply(n0,n1)) = multiply(n1,add(n1,n1)),
inference(orient,[status(thm)],[t3100]) ).
cnf(t3101,plain,
multiply(X1,multiply(n1,add(n1,n1))) = multiply(n1,X1),
inference(step,[status(thm)],[t645,t838]) ).
cnf(t845,plain,
multiply(X1,multiply(n1,add(n1,n1))) = multiply(n1,X1),
inference(rw,[status(thm)],[t3101]) ).
cnf(t853,plain,
multiply(X1,multiply(n1,add(n1,n1))) = multiply(n1,X1),
inference(orient,[status(thm)],[t845]) ).
cnf(t854,plain,
multiply(multiply(n1,add(n1,n1)),add(X1,X2)) = add(multiply(n1,X1),multiply(X2,multiply(n1,add(n1,n1)))),
inference(cp,[status(thm)],[t28,t853]) ).
cnf(t3107,plain,
multiply(multiply(n1,add(n1,n1)),add(X1,X2)) = add(multiply(n1,X1),multiply(n1,X2)),
inference(step,[status(thm)],[t854,t853]) ).
cnf(t1215,plain,
multiply(multiply(n1,add(n1,n1)),add(X1,X2)) = add(multiply(n1,X1),multiply(n1,X2)),
inference(orient,[status(thm)],[t3107]) ).
cnf(t1269,plain,
add(n1,multiply(n0,multiply(n1,add(n1,n1)))) = add(add(multiply(n1,n0),multiply(n1,n1)),multiply(n1,n1)),
inference(cp,[status(thm)],[t828,t1215]) ).
cnf(t3108,plain,
add(n1,multiply(n1,n0)) = add(add(multiply(n1,n0),multiply(n1,n1)),multiply(n1,n1)),
inference(step,[status(thm)],[t1269,t853]) ).
cnf(t661,plain,
multiply(n1,add(n0,n0)) = multiply(n1,n0),
inference(cp,[status(thm)],[t658,t123]) ).
cnf(t3089,plain,
n0 = multiply(n1,n0),
inference(step,[status(thm)],[t661,t55]) ).
cnf(t673,plain,
multiply(n1,n0) = n0,
inference(orient,[status(thm)],[t3089]) ).
cnf(t3109,plain,
add(n1,n0) = add(add(multiply(n1,n0),multiply(n1,n1)),multiply(n1,n1)),
inference(step,[status(thm)],[t3108,t673]) ).
cnf(t3110,plain,
add(n1,n0) = add(add(n0,multiply(n1,n1)),multiply(n1,n1)),
inference(step,[status(thm)],[t3109,t673]) ).
cnf(t3111,plain,
add(n1,n0) = add(n1,multiply(n1,n1)),
inference(step,[status(thm)],[t3110,t123]) ).
cnf(t1276,plain,
add(n1,multiply(n1,n1)) = add(n1,n0),
inference(orient,[status(thm)],[t3111]) ).
cnf(t53,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(n1,add(X2,inverse(X1))),
inference(cp,[status(thm)],[t44,t52]) ).
cnf(t58,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(n1,add(X2,inverse(X1))),
inference(orient,[status(thm)],[t53]) ).
cnf(t677,plain,
multiply(n1,add(n0,inverse(n1))) = add(inverse(n1),n0),
inference(cp,[status(thm)],[t58,t673]) ).
cnf(t739,plain,
multiply(n1,add(n0,inverse(n1))) = add(inverse(n1),n0),
inference(orient,[status(thm)],[t677]) ).
cnf(t1246,plain,
add(multiply(n1,n0),multiply(n1,multiply(X1,n1))) = multiply(multiply(n1,add(n1,n1)),X1),
inference(cp,[status(thm)],[t1215,t123]) ).
cnf(t3119,plain,
add(n0,multiply(n1,multiply(X1,n1))) = multiply(multiply(n1,add(n1,n1)),X1),
inference(step,[status(thm)],[t1246,t673]) ).
cnf(t1307,plain,
add(n0,multiply(n1,multiply(X1,n1))) = multiply(multiply(n1,add(n1,n1)),X1),
inference(orient,[status(thm)],[t3119]) ).
cnf(t54,plain,
add(inverse(X1),multiply(X2,X1)) = multiply(add(X2,inverse(X1)),n1),
inference(cp,[status(thm)],[t44,t52]) ).
cnf(t64,plain,
add(inverse(X1),multiply(X2,X1)) = multiply(add(X2,inverse(X1)),n1),
inference(orient,[status(thm)],[t54]) ).
cnf(t662,plain,
multiply(n1,add(n0,inverse(n1))) = multiply(n1,multiply(add(n0,inverse(n1)),n1)),
inference(cp,[status(thm)],[t658,t64]) ).
cnf(t3098,plain,
add(inverse(n1),n0) = multiply(n1,multiply(add(n0,inverse(n1)),n1)),
inference(step,[status(thm)],[t662,t739]) ).
cnf(t813,plain,
multiply(n1,multiply(add(n0,inverse(n1)),n1)) = add(inverse(n1),n0),
inference(orient,[status(thm)],[t3098]) ).
cnf(t1309,plain,
multiply(multiply(n1,add(n1,n1)),add(n0,inverse(n1))) = add(n0,add(inverse(n1),n0)),
inference(cp,[status(thm)],[t1307,t813]) ).
cnf(t3120,plain,
add(multiply(n1,n0),multiply(n1,inverse(n1))) = add(n0,add(inverse(n1),n0)),
inference(step,[status(thm)],[t1309,t1215]) ).
cnf(t3121,plain,
add(n0,multiply(n1,inverse(n1))) = add(n0,add(inverse(n1),n0)),
inference(step,[status(thm)],[t3120,t673]) ).
cnf(t42,plain,
multiply(inverse(X1),add(X1,X2)) = add(n0,multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t28,t41]) ).
cnf(t159,plain,
multiply(inverse(X1),add(X1,X2)) = add(n0,multiply(X2,inverse(X1))),
inference(orient,[status(thm)],[t42]) ).
cnf(t3122,plain,
multiply(inverse(n1),add(n1,n1)) = add(n0,add(inverse(n1),n0)),
inference(step,[status(thm)],[t3121,t159]) ).
cnf(t177,plain,
multiply(inverse(X1),add(X1,X1)) = add(n0,n0),
inference(cp,[status(thm)],[t159,t41]) ).
cnf(t182,plain,
multiply(inverse(X1),add(X1,X1)) = add(n0,n0),
inference(orient,[status(thm)],[t177]) ).
cnf(t3123,plain,
add(n0,n0) = add(n0,add(inverse(n1),n0)),
inference(step,[status(thm)],[t3122,t182]) ).
cnf(t1325,plain,
add(n0,add(inverse(n1),n0)) = add(n0,n0),
inference(orient,[status(thm)],[t3123]) ).
cnf(t1328,plain,
add(multiply(n1,n0),multiply(n1,add(inverse(n1),n0))) = multiply(multiply(n1,add(n1,n1)),add(n0,n0)),
inference(cp,[status(thm)],[t1215,t1325]) ).
cnf(t3124,plain,
add(n0,multiply(n1,add(inverse(n1),n0))) = multiply(multiply(n1,add(n1,n1)),add(n0,n0)),
inference(step,[status(thm)],[t1328,t673]) ).
cnf(t3125,plain,
add(n0,inverse(n1)) = multiply(multiply(n1,add(n1,n1)),add(n0,n0)),
inference(step,[status(thm)],[t3124,t55]) ).
cnf(t3126,plain,
add(n0,inverse(n1)) = add(multiply(n1,n0),multiply(n1,n0)),
inference(step,[status(thm)],[t3125,t1215]) ).
cnf(t3127,plain,
add(n0,inverse(n1)) = multiply(n0,add(n1,n1)),
inference(step,[status(thm)],[t3126,t28]) ).
cnf(t674,plain,
multiply(n0,add(n1,X1)) = add(n0,multiply(X1,n0)),
inference(cp,[status(thm)],[t28,t673]) ).
cnf(t688,plain,
add(n0,multiply(X1,n0)) = multiply(n0,add(n1,X1)),
inference(orient,[status(thm)],[t674]) ).
cnf(t690,plain,
multiply(n0,add(n1,n1)) = add(n0,n0),
inference(cp,[status(thm)],[t688,t673]) ).
cnf(t697,plain,
multiply(n0,add(n1,n1)) = add(n0,n0),
inference(orient,[status(thm)],[t690]) ).
cnf(t3128,plain,
add(n0,inverse(n1)) = add(n0,n0),
inference(step,[status(thm)],[t3127,t697]) ).
cnf(t1334,plain,
add(n0,inverse(n1)) = add(n0,n0),
inference(orient,[status(thm)],[t3128]) ).
cnf(t3129,plain,
multiply(n1,add(n0,n0)) = add(inverse(n1),n0),
inference(step,[status(thm)],[t739,t1334]) ).
cnf(t3130,plain,
n0 = add(inverse(n1),n0),
inference(step,[status(thm)],[t3129,t55]) ).
cnf(t1347,plain,
n0 = add(inverse(n1),n0),
inference(rw,[status(thm)],[t3130]) ).
cnf(t1350,plain,
add(inverse(n1),n0) = n0,
inference(orient,[status(thm)],[t1347]) ).
cnf(t1351,plain,
inverse(n1) = multiply(n1,n0),
inference(cp,[status(thm)],[t55,t1350]) ).
cnf(t3137,plain,
inverse(n1) = n0,
inference(step,[status(thm)],[t1351,t673]) ).
cnf(t1371,plain,
inverse(n1) = n0,
inference(orient,[status(thm)],[t3137]) ).
cnf(t1374,plain,
n1 = add(n1,n0),
inference(cp,[status(thm)],[t52,t1371]) ).
cnf(t1400,plain,
add(n1,n0) = n1,
inference(orient,[status(thm)],[t1374]) ).
cnf(t3151,plain,
add(n1,multiply(n1,n1)) = n1,
inference(step,[status(thm)],[t1276,t1400]) ).
cnf(t1401,plain,
add(n1,multiply(n1,n1)) = n1,
inference(orient,[status(thm)],[t3151]) ).
cnf(t1403,plain,
n1 = multiply(n1,n1),
inference(cp,[status(thm)],[t55,t1400]) ).
cnf(t1471,plain,
multiply(n1,n1) = n1,
inference(orient,[status(thm)],[t1403]) ).
cnf(t3216,plain,
add(n1,n1) = n1,
inference(step,[status(thm)],[t1401,t1471]) ).
cnf(t1488,plain,
add(n1,n1) = n1,
inference(rw,[status(thm)],[t3216]) ).
cnf(t1506,plain,
add(n1,n1) = n1,
inference(orient,[status(thm)],[t1488]) ).
cnf(t3234,plain,
multiply(add(X1,n0),n1) = add(X1,X1),
inference(step,[status(thm)],[t100,t1506]) ).
cnf(t1522,plain,
multiply(add(X1,n0),n1) = add(X1,X1),
inference(rw,[status(thm)],[t3234]) ).
cnf(t3238,plain,
multiply(X1,multiply(n1,n1)) = multiply(n1,X1),
inference(step,[status(thm)],[t853,t1506]) ).
cnf(t3239,plain,
multiply(X1,n1) = multiply(n1,X1),
inference(step,[status(thm)],[t3238,t1471]) ).
cnf(t1525,plain,
multiply(X1,n1) = multiply(n1,X1),
inference(rw,[status(thm)],[t3239]) ).
cnf(t1749,plain,
multiply(X1,n1) = multiply(n1,X1),
inference(orient,[status(thm)],[t1525]) ).
cnf(t3319,plain,
multiply(n1,add(X1,n0)) = add(X1,X1),
inference(step,[status(thm)],[t1522,t1749]) ).
cnf(t3320,plain,
X1 = add(X1,X1),
inference(step,[status(thm)],[t3319,t55]) ).
cnf(t2176,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t3320]) ).
cnf(t2177,plain,
multiply(X1,X2) = multiply(X2,add(X1,X1)),
inference(cp,[status(thm)],[t2176,t28]) ).
cnf(t3338,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(step,[status(thm)],[t2177,t2176]) ).
cnf(t2278,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t3338]) ).
cnf(t47,plain,
multiply(add(X1,X2),add(add(X3,X2),Y3)) = add(add(X2,multiply(X3,X1)),multiply(Y3,add(X1,X2))),
inference(cp,[status(thm)],[t28,t44]) ).
cnf(t2071,plain,
add(add(X1,multiply(X2,X3)),multiply(Y3,add(X3,X1))) = multiply(add(X3,X1),add(add(X2,X1),Y3)),
inference(orient,[status(thm)],[t47]) ).
cnf(t6,axiom,
add(multiply(X1,inverse(X2)),add(multiply(X1,X2),multiply(inverse(X2),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X2),multiply(inverse(X2),X2))) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t3075,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t19,t28]) ).
cnf(t39,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(rw,[status(thm)],[t3075]) ).
cnf(t127,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t39]) ).
cnf(t1388,plain,
X1 = add(multiply(X1,n0),multiply(n1,add(X1,inverse(n1)))),
inference(cp,[status(thm)],[t127,t1371]) ).
cnf(t3267,plain,
X1 = add(multiply(X1,n0),multiply(n1,add(X1,n0))),
inference(step,[status(thm)],[t1388,t1371]) ).
cnf(t3268,plain,
X1 = add(multiply(X1,n0),X1),
inference(step,[status(thm)],[t3267,t55]) ).
cnf(t1600,plain,
add(multiply(X1,n0),X1) = X1,
inference(orient,[status(thm)],[t3268]) ).
cnf(t1620,plain,
multiply(add(multiply(n0,n0),n0),add(n1,X1)) = add(multiply(n0,n0),multiply(X1,n0)),
inference(cp,[status(thm)],[t85,t1600]) ).
cnf(t1601,plain,
multiply(X1,n0) = multiply(n0,add(multiply(X1,n0),X1)),
inference(cp,[status(thm)],[t1600,t28]) ).
cnf(t3296,plain,
multiply(X1,n0) = multiply(n0,X1),
inference(step,[status(thm)],[t1601,t1600]) ).
cnf(t1770,plain,
multiply(X1,n0) = multiply(n0,X1),
inference(orient,[status(thm)],[t3296]) ).
cnf(t1774,plain,
X1 = add(multiply(n0,X1),X1),
inference(cp,[status(thm)],[t1600,t1770]) ).
cnf(t1786,plain,
add(multiply(n0,X1),X1) = X1,
inference(orient,[status(thm)],[t1774]) ).
cnf(t3312,plain,
multiply(n0,add(n1,X1)) = add(multiply(n0,n0),multiply(X1,n0)),
inference(step,[status(thm)],[t1620,t1786]) ).
cnf(t3313,plain,
multiply(n0,add(n1,X1)) = multiply(n0,add(n0,X1)),
inference(step,[status(thm)],[t3312,t28]) ).
cnf(t1981,plain,
multiply(n0,add(n0,X1)) = multiply(n0,add(n1,X1)),
inference(orient,[status(thm)],[t3313]) ).
cnf(t60,plain,
multiply(n1,add(add(X1,n0),inverse(n1))) = add(inverse(n1),X1),
inference(cp,[status(thm)],[t58,t55]) ).
cnf(t80,plain,
multiply(n1,add(add(X1,n0),inverse(n1))) = add(inverse(n1),X1),
inference(orient,[status(thm)],[t60]) ).
cnf(t3142,plain,
multiply(n1,add(add(X1,n0),n0)) = add(inverse(n1),X1),
inference(step,[status(thm)],[t80,t1371]) ).
cnf(t3143,plain,
add(X1,n0) = add(inverse(n1),X1),
inference(step,[status(thm)],[t3142,t55]) ).
cnf(t3144,plain,
add(X1,n0) = add(n0,X1),
inference(step,[status(thm)],[t3143,t1371]) ).
cnf(t1397,plain,
add(X1,n0) = add(n0,X1),
inference(rw,[status(thm)],[t3144]) ).
cnf(t1701,plain,
add(X1,n0) = add(n0,X1),
inference(orient,[status(thm)],[t1397]) ).
cnf(t43,plain,
multiply(inverse(X1),add(X2,X1)) = add(multiply(X2,inverse(X1)),n0),
inference(cp,[status(thm)],[t28,t41]) ).
cnf(t327,plain,
multiply(inverse(X1),add(X2,X1)) = add(multiply(X2,inverse(X1)),n0),
inference(orient,[status(thm)],[t43]) ).
cnf(t352,plain,
multiply(X1,inverse(X2)) = multiply(n1,multiply(inverse(X2),add(X1,X2))),
inference(cp,[status(thm)],[t55,t327]) ).
cnf(t370,plain,
multiply(n1,multiply(inverse(X1),add(X2,X1))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t352]) ).
cnf(t2183,plain,
add(X1,multiply(X2,X1)) = multiply(add(X2,X1),X1),
inference(cp,[status(thm)],[t44,t2176]) ).
cnf(t3344,plain,
add(X1,multiply(X2,X1)) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t2183,t2278]) ).
cnf(t2412,plain,
add(X1,multiply(X2,X1)) = multiply(X1,add(X2,X1)),
inference(orient,[status(thm)],[t3344]) ).
cnf(t59,plain,
multiply(n1,add(inverse(X1),inverse(X1))) = add(inverse(X1),n0),
inference(cp,[status(thm)],[t58,t41]) ).
cnf(t70,plain,
multiply(n1,add(inverse(X1),inverse(X1))) = add(inverse(X1),n0),
inference(orient,[status(thm)],[t59]) ).
cnf(t1375,plain,
add(inverse(n1),n0) = multiply(n1,add(n0,inverse(n1))),
inference(cp,[status(thm)],[t70,t1371]) ).
cnf(t3156,plain,
add(n0,n0) = multiply(n1,add(n0,inverse(n1))),
inference(step,[status(thm)],[t1375,t1371]) ).
cnf(t3157,plain,
add(n0,n0) = multiply(n1,add(n0,n0)),
inference(step,[status(thm)],[t3156,t1334]) ).
cnf(t3158,plain,
add(n0,n0) = n0,
inference(step,[status(thm)],[t3157,t55]) ).
cnf(t1419,plain,
add(n0,n0) = n0,
inference(orient,[status(thm)],[t3158]) ).
cnf(t3159,plain,
multiply(inverse(X1),add(X1,X1)) = n0,
inference(step,[status(thm)],[t182,t1419]) ).
cnf(t1420,plain,
multiply(inverse(X1),add(X1,X1)) = n0,
inference(orient,[status(thm)],[t3159]) ).
cnf(t1511,plain,
n0 = multiply(inverse(n1),n1),
inference(cp,[status(thm)],[t1420,t1506]) ).
cnf(t3243,plain,
n0 = multiply(n0,n1),
inference(step,[status(thm)],[t1511,t1371]) ).
cnf(t1529,plain,
multiply(n0,n1) = n0,
inference(orient,[status(thm)],[t3243]) ).
cnf(t1530,plain,
multiply(n1,add(n0,X1)) = add(n0,multiply(X1,n1)),
inference(cp,[status(thm)],[t28,t1529]) ).
cnf(t3281,plain,
multiply(n1,add(n0,X1)) = X1,
inference(step,[status(thm)],[t1530,t123]) ).
cnf(t1650,plain,
multiply(n1,add(n0,X1)) = X1,
inference(orient,[status(thm)],[t3281]) ).
cnf(t2427,plain,
multiply(add(n0,X1),add(n1,add(n0,X1))) = add(add(n0,X1),X1),
inference(cp,[status(thm)],[t2412,t1650]) ).
cnf(t9,axiom,
multiply(add(X1,inverse(X2)),multiply(add(X1,X2),add(inverse(X2),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
multiply(add(X1,inverse(X2)),multiply(add(X1,X2),add(inverse(X2),X2))) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t3080,plain,
multiply(add(X1,inverse(X2)),add(X2,multiply(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t11,t44]) ).
cnf(t51,plain,
multiply(add(X1,inverse(X2)),add(X2,multiply(X1,inverse(X2)))) = X1,
inference(rw,[status(thm)],[t3080]) ).
cnf(t146,plain,
multiply(add(X1,inverse(X2)),add(X2,multiply(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t51]) ).
cnf(t1446,plain,
n0 = multiply(inverse(n0),n0),
inference(cp,[status(thm)],[t1420,t1419]) ).
cnf(t1550,plain,
multiply(inverse(n0),n0) = n0,
inference(orient,[status(thm)],[t1446]) ).
cnf(t1602,plain,
inverse(n0) = add(n0,inverse(n0)),
inference(cp,[status(thm)],[t1600,t1550]) ).
cnf(t3269,plain,
inverse(n0) = n1,
inference(step,[status(thm)],[t1602,t52]) ).
cnf(t1627,plain,
inverse(n0) = n1,
inference(orient,[status(thm)],[t3269]) ).
cnf(t1631,plain,
X1 = multiply(add(X1,n1),add(n0,multiply(X1,inverse(n0)))),
inference(cp,[status(thm)],[t146,t1627]) ).
cnf(t3283,plain,
X1 = multiply(add(X1,n1),multiply(inverse(n0),add(n0,X1))),
inference(step,[status(thm)],[t1631,t159]) ).
cnf(t3284,plain,
X1 = multiply(add(X1,n1),multiply(n1,add(n0,X1))),
inference(step,[status(thm)],[t3283,t1627]) ).
cnf(t3285,plain,
X1 = multiply(add(X1,n1),X1),
inference(step,[status(thm)],[t3284,t1650]) ).
cnf(t1680,plain,
multiply(add(X1,n1),X1) = X1,
inference(orient,[status(thm)],[t3285]) ).
cnf(t1681,plain,
add(X1,n1) = add(n1,multiply(add(X1,n1),X1)),
inference(cp,[status(thm)],[t1680,t44]) ).
cnf(t3297,plain,
add(X1,n1) = add(n1,X1),
inference(step,[status(thm)],[t1681,t1680]) ).
cnf(t1808,plain,
add(X1,n1) = add(n1,X1),
inference(orient,[status(thm)],[t3297]) ).
cnf(t1813,plain,
X1 = multiply(add(n1,X1),X1),
inference(cp,[status(thm)],[t1680,t1808]) ).
cnf(t1828,plain,
multiply(add(n1,X1),X1) = X1,
inference(orient,[status(thm)],[t1813]) ).
cnf(t2302,plain,
multiply(add(n1,X1),X1) = X1,
inference(rw,[status(thm)],[t1828]) ).
cnf(t3339,plain,
multiply(X1,add(n1,X1)) = X1,
inference(step,[status(thm)],[t2302,t2278]) ).
cnf(t2305,plain,
multiply(X1,add(n1,X1)) = X1,
inference(orient,[status(thm)],[t3339]) ).
cnf(t3347,plain,
add(n0,X1) = add(add(n0,X1),X1),
inference(step,[status(thm)],[t2427,t2305]) ).
cnf(t2450,plain,
add(add(n0,X1),X1) = add(n0,X1),
inference(orient,[status(thm)],[t3347]) ).
cnf(t2473,plain,
multiply(add(n0,X1),inverse(X1)) = multiply(n1,multiply(inverse(X1),add(n0,X1))),
inference(cp,[status(thm)],[t370,t2450]) ).
cnf(t3351,plain,
multiply(inverse(X1),add(n0,X1)) = multiply(n1,multiply(inverse(X1),add(n0,X1))),
inference(step,[status(thm)],[t2473,t2278]) ).
cnf(t3352,plain,
multiply(inverse(X1),add(n0,X1)) = multiply(n0,inverse(X1)),
inference(step,[status(thm)],[t3351,t370]) ).
cnf(t2567,plain,
multiply(inverse(X1),add(n0,X1)) = multiply(n0,inverse(X1)),
inference(orient,[status(thm)],[t3352]) ).
cnf(t2578,plain,
multiply(n0,inverse(X1)) = multiply(inverse(X1),add(X1,n0)),
inference(cp,[status(thm)],[t2567,t1701]) ).
cnf(t2595,plain,
multiply(inverse(X1),add(X1,n0)) = multiply(n0,inverse(X1)),
inference(orient,[status(thm)],[t2578]) ).
cnf(t2617,plain,
multiply(add(X1,n0),add(n1,inverse(X1))) = add(X1,multiply(n0,inverse(X1))),
inference(cp,[status(thm)],[t85,t2595]) ).
cnf(t8,axiom,
multiply(add(X1,inverse(X2)),multiply(add(X1,X1),add(inverse(X2),X1))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t12,plain,
multiply(add(X1,inverse(X2)),multiply(add(X1,X1),add(inverse(X2),X1))) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t3079,plain,
multiply(add(X1,inverse(X2)),add(X1,multiply(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t12,t44]) ).
cnf(t50,plain,
multiply(add(X1,inverse(X2)),add(X1,multiply(X1,inverse(X2)))) = X1,
inference(rw,[status(thm)],[t3079]) ).
cnf(t137,plain,
multiply(add(X1,inverse(X2)),add(X1,multiply(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t50]) ).
cnf(t2200,plain,
inverse(X1) = add(multiply(inverse(X1),inverse(X1)),multiply(inverse(X1),inverse(X1))),
inference(cp,[status(thm)],[t115,t2176]) ).
cnf(t3328,plain,
inverse(X1) = multiply(inverse(X1),add(inverse(X1),inverse(X1))),
inference(step,[status(thm)],[t2200,t28]) ).
cnf(t3329,plain,
inverse(X1) = multiply(inverse(X1),inverse(X1)),
inference(step,[status(thm)],[t3328,t2176]) ).
cnf(t2242,plain,
multiply(inverse(X1),inverse(X1)) = inverse(X1),
inference(orient,[status(thm)],[t3329]) ).
cnf(t2250,plain,
inverse(X1) = multiply(add(inverse(X1),inverse(X1)),add(X1,inverse(X1))),
inference(cp,[status(thm)],[t146,t2242]) ).
cnf(t3330,plain,
inverse(X1) = add(inverse(X1),multiply(inverse(X1),X1)),
inference(step,[status(thm)],[t2250,t44]) ).
cnf(t3292,plain,
add(inverse(X1),multiply(X2,X1)) = multiply(n1,add(X2,inverse(X1))),
inference(step,[status(thm)],[t64,t1749]) ).
cnf(t1750,plain,
add(inverse(X1),multiply(X2,X1)) = multiply(n1,add(X2,inverse(X1))),
inference(orient,[status(thm)],[t3292]) ).
cnf(t3331,plain,
inverse(X1) = multiply(n1,add(inverse(X1),inverse(X1))),
inference(step,[status(thm)],[t3330,t1750]) ).
cnf(t3332,plain,
inverse(X1) = multiply(n1,inverse(X1)),
inference(step,[status(thm)],[t3331,t2176]) ).
cnf(t2253,plain,
multiply(n1,inverse(X1)) = inverse(X1),
inference(orient,[status(thm)],[t3332]) ).
cnf(t2264,plain,
n1 = multiply(add(n1,inverse(X1)),add(n1,inverse(X1))),
inference(cp,[status(thm)],[t137,t2253]) ).
cnf(t3335,plain,
n1 = add(inverse(X1),multiply(n1,n1)),
inference(step,[status(thm)],[t2264,t44]) ).
cnf(t3336,plain,
n1 = add(inverse(X1),n1),
inference(step,[status(thm)],[t3335,t1471]) ).
cnf(t3337,plain,
n1 = add(n1,inverse(X1)),
inference(step,[status(thm)],[t3336,t1808]) ).
cnf(t2267,plain,
add(n1,inverse(X1)) = n1,
inference(orient,[status(thm)],[t3337]) ).
cnf(t3363,plain,
multiply(add(X1,n0),n1) = add(X1,multiply(n0,inverse(X1))),
inference(step,[status(thm)],[t2617,t2267]) ).
cnf(t3364,plain,
multiply(n1,add(X1,n0)) = add(X1,multiply(n0,inverse(X1))),
inference(step,[status(thm)],[t3363,t1749]) ).
cnf(t3365,plain,
X1 = add(X1,multiply(n0,inverse(X1))),
inference(step,[status(thm)],[t3364,t55]) ).
cnf(t2596,plain,
multiply(n0,inverse(X1)) = add(n0,multiply(n0,inverse(X1))),
inference(cp,[status(thm)],[t2595,t159]) ).
cnf(t1447,plain,
add(n0,multiply(n0,X1)) = multiply(n0,add(X1,n0)),
inference(cp,[status(thm)],[t44,t1419]) ).
cnf(t1890,plain,
add(n0,multiply(n0,X1)) = multiply(n0,add(X1,n0)),
inference(orient,[status(thm)],[t1447]) ).
cnf(t57,plain,
multiply(add(X1,n0),add(X2,n1)) = add(multiply(X2,add(X1,n0)),X1),
inference(cp,[status(thm)],[t28,t55]) ).
cnf(t91,plain,
add(multiply(X1,add(X2,n0)),X2) = multiply(add(X2,n0),add(X1,n1)),
inference(orient,[status(thm)],[t57]) ).
cnf(t1619,plain,
multiply(add(multiply(n0,n0),n0),add(X1,n1)) = add(multiply(X1,n0),multiply(n0,n0)),
inference(cp,[status(thm)],[t91,t1600]) ).
cnf(t3307,plain,
multiply(n0,add(X1,n1)) = add(multiply(X1,n0),multiply(n0,n0)),
inference(step,[status(thm)],[t1619,t1786]) ).
cnf(t3308,plain,
multiply(n0,add(X1,n1)) = multiply(n0,add(X1,n0)),
inference(step,[status(thm)],[t3307,t28]) ).
cnf(t1961,plain,
multiply(n0,add(X1,n0)) = multiply(n0,add(X1,n1)),
inference(orient,[status(thm)],[t3308]) ).
cnf(t3309,plain,
add(n0,multiply(n0,X1)) = multiply(n0,add(X1,n1)),
inference(step,[status(thm)],[t1890,t1961]) ).
cnf(t1962,plain,
add(n0,multiply(n0,X1)) = multiply(n0,add(X1,n1)),
inference(orient,[status(thm)],[t3309]) ).
cnf(t3353,plain,
multiply(n0,inverse(X1)) = multiply(n0,add(inverse(X1),n1)),
inference(step,[status(thm)],[t2596,t1962]) ).
cnf(t3354,plain,
multiply(n0,inverse(X1)) = multiply(n0,add(n1,inverse(X1))),
inference(step,[status(thm)],[t3353,t1808]) ).
cnf(t3355,plain,
multiply(n0,inverse(X1)) = multiply(n0,n1),
inference(step,[status(thm)],[t3354,t2267]) ).
cnf(t3356,plain,
multiply(n0,inverse(X1)) = multiply(n1,n0),
inference(step,[status(thm)],[t3355,t1770]) ).
cnf(t3357,plain,
multiply(n0,inverse(X1)) = n0,
inference(step,[status(thm)],[t3356,t673]) ).
cnf(t2630,plain,
multiply(n0,inverse(X1)) = n0,
inference(orient,[status(thm)],[t3357]) ).
cnf(t3366,plain,
X1 = add(X1,n0),
inference(step,[status(thm)],[t3365,t2630]) ).
cnf(t2663,plain,
add(X1,n0) = X1,
inference(orient,[status(thm)],[t3366]) ).
cnf(t3369,plain,
X1 = add(n0,X1),
inference(step,[status(thm)],[t1701,t2663]) ).
cnf(t2675,plain,
X1 = add(n0,X1),
inference(rw,[status(thm)],[t3369]) ).
cnf(t2683,plain,
add(n0,X1) = X1,
inference(orient,[status(thm)],[t2675]) ).
cnf(t3382,plain,
multiply(n0,X1) = multiply(n0,add(n1,X1)),
inference(step,[status(thm)],[t1981,t2683]) ).
cnf(t2702,plain,
multiply(n0,X1) = multiply(n0,add(n1,X1)),
inference(rw,[status(thm)],[t3382]) ).
cnf(t2792,plain,
multiply(n0,add(n1,X1)) = multiply(n0,X1),
inference(orient,[status(thm)],[t2702]) ).
cnf(t2802,plain,
multiply(add(n1,X1),add(add(X2,X1),n0)) = add(add(X1,multiply(X2,n1)),multiply(n0,X1)),
inference(cp,[status(thm)],[t2071,t2792]) ).
cnf(t3418,plain,
multiply(add(n1,X1),add(X2,X1)) = add(add(X1,multiply(X2,n1)),multiply(n0,X1)),
inference(step,[status(thm)],[t2802,t2663]) ).
cnf(t3419,plain,
add(X1,multiply(n1,X2)) = add(add(X1,multiply(X2,n1)),multiply(n0,X1)),
inference(step,[status(thm)],[t3418,t44]) ).
cnf(t3372,plain,
multiply(n1,X1) = X1,
inference(step,[status(thm)],[t55,t2663]) ).
cnf(t2678,plain,
multiply(n1,X1) = X1,
inference(rw,[status(thm)],[t3372]) ).
cnf(t2706,plain,
multiply(n1,X1) = X1,
inference(orient,[status(thm)],[t2678]) ).
cnf(t3420,plain,
add(X1,X2) = add(add(X1,multiply(X2,n1)),multiply(n0,X1)),
inference(step,[status(thm)],[t3419,t2706]) ).
cnf(t1979,plain,
multiply(add(X1,n0),add(n1,n0)) = add(X1,multiply(n0,add(X1,n1))),
inference(cp,[status(thm)],[t85,t1961]) ).
cnf(t3317,plain,
add(n0,multiply(X1,n1)) = add(X1,multiply(n0,add(X1,n1))),
inference(step,[status(thm)],[t1979,t44]) ).
cnf(t3318,plain,
X1 = add(X1,multiply(n0,add(X1,n1))),
inference(step,[status(thm)],[t3317,t123]) ).
cnf(t2028,plain,
add(X1,multiply(n0,add(X1,n1))) = X1,
inference(orient,[status(thm)],[t3318]) ).
cnf(t3371,plain,
multiply(n0,X1) = multiply(n0,add(X1,n1)),
inference(step,[status(thm)],[t1961,t2663]) ).
cnf(t2677,plain,
multiply(n0,X1) = multiply(n0,add(X1,n1)),
inference(rw,[status(thm)],[t3371]) ).
cnf(t2746,plain,
multiply(n0,add(X1,n1)) = multiply(n0,X1),
inference(orient,[status(thm)],[t2677]) ).
cnf(t3397,plain,
add(X1,multiply(n0,X1)) = X1,
inference(step,[status(thm)],[t2028,t2746]) ).
cnf(t3398,plain,
multiply(X1,add(n0,X1)) = X1,
inference(step,[status(thm)],[t3397,t2412]) ).
cnf(t3399,plain,
multiply(X1,X1) = X1,
inference(step,[status(thm)],[t3398,t2683]) ).
cnf(t2761,plain,
multiply(X1,X1) = X1,
inference(rw,[status(thm)],[t3399]) ).
cnf(t2762,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t2761]) ).
cnf(t2763,plain,
add(X1,X2) = add(X2,multiply(X1,X1)),
inference(cp,[status(thm)],[t2762,t44]) ).
cnf(t3400,plain,
add(X1,X2) = add(X2,X1),
inference(step,[status(thm)],[t2763,t2762]) ).
cnf(t2772,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t3400]) ).
cnf(t3421,plain,
add(X1,X2) = add(multiply(n0,X1),add(X1,multiply(X2,n1))),
inference(step,[status(thm)],[t3420,t2772]) ).
cnf(t3385,plain,
multiply(X1,n1) = X1,
inference(step,[status(thm)],[t123,t2683]) ).
cnf(t2705,plain,
multiply(X1,n1) = X1,
inference(rw,[status(thm)],[t3385]) ).
cnf(t2730,plain,
multiply(X1,n1) = X1,
inference(orient,[status(thm)],[t2705]) ).
cnf(t3422,plain,
add(X1,X2) = add(multiply(n0,X1),add(X1,X2)),
inference(step,[status(thm)],[t3421,t2730]) ).
cnf(t3031,plain,
add(multiply(n0,X1),add(X1,X2)) = add(X1,X2),
inference(orient,[status(thm)],[t3422]) ).
cnf(t3040,plain,
add(X1,inverse(X1)) = add(multiply(n0,X1),n1),
inference(cp,[status(thm)],[t3031,t52]) ).
cnf(t3423,plain,
n1 = add(multiply(n0,X1),n1),
inference(step,[status(thm)],[t3040,t52]) ).
cnf(t3424,plain,
n1 = add(n1,multiply(n0,X1)),
inference(step,[status(thm)],[t3423,t1808]) ).
cnf(t1629,plain,
multiply(n1,add(X1,inverse(n0))) = add(n1,multiply(n0,X1)),
inference(cp,[status(thm)],[t58,t1627]) ).
cnf(t3316,plain,
multiply(n1,add(X1,n1)) = add(n1,multiply(n0,X1)),
inference(step,[status(thm)],[t1629,t1627]) ).
cnf(t2015,plain,
add(n1,multiply(n0,X1)) = multiply(n1,add(X1,n1)),
inference(orient,[status(thm)],[t3316]) ).
cnf(t3392,plain,
add(n1,multiply(n0,X1)) = add(X1,n1),
inference(step,[status(thm)],[t2015,t2706]) ).
cnf(t2713,plain,
add(n1,multiply(n0,X1)) = add(X1,n1),
inference(orient,[status(thm)],[t3392]) ).
cnf(t3425,plain,
n1 = add(X1,n1),
inference(step,[status(thm)],[t3424,t2713]) ).
cnf(t3056,plain,
add(X1,n1) = n1,
inference(orient,[status(thm)],[t3425]) ).
cnf(goal_0,negated_conjecture,
multiply(add(a,b),b) != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(add(a,b),b) != multiply(b,add(a,b)),
inference(rw,[status(thm)],[goal_0,t2278]) ).
cnf(g0_1,plain,
multiply(add(a,b),b) != multiply(b,add(a,n1)),
inference(rw,[status(thm)],[g0_0]) ).
cnf(g0_2,plain,
multiply(add(a,b),b) != multiply(add(a,n1),b),
inference(rw,[status(thm)],[g0_1,t2278]) ).
cnf(g0_3,plain,
multiply(add(a,b),b) != multiply(n1,b),
inference(rw,[status(thm)],[g0_2,t3056]) ).
cnf(g0_4,plain,
multiply(add(a,b),b) != b,
inference(rw,[status(thm)],[g0_3,t2706]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 06:35:19 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.00/1.33 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.00/1.33 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------