%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO023-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 : n002.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 14.99s 2.50s
% Output : CNFRefutation 14.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 102
% Number of leaves : 13
% Syntax : Number of clauses : 305 ( 305 unt; 0 nHn; 95 RR)
% Number of literals : 305 ( 304 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 : 14 ( 14 usr; 10 con; 0-3 aty)
% Number of variables : 306 ( 55 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
sF0 = add(a,b),
introduced(definition) ).
cnf(t11,plain,
add(a,b) = sF0,
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
sF1 = add(a,c),
introduced(definition) ).
cnf(t12,plain,
add(a,c) = sF1,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
sF2 = multiply(add(a,b),add(a,c)),
introduced(definition) ).
cnf(t7848,plain,
sF2 = multiply(sF0,add(a,c)),
inference(step,[status(thm)],[t8,t11]) ).
cnf(t7849,plain,
sF2 = multiply(sF0,sF1),
inference(step,[status(thm)],[t7848,t12]) ).
cnf(t92,plain,
multiply(sF0,sF1) = sF2,
inference(orient,[status(thm)],[t7849]) ).
cnf(t9,axiom,
sF3 = multiply(b,c),
introduced(definition) ).
cnf(t13,plain,
multiply(b,c) = sF3,
inference(orient,[status(thm)],[t9]) ).
cnf(t10,axiom,
sF4 = add(a,multiply(b,c)),
introduced(definition) ).
cnf(t7845,plain,
sF4 = add(a,sF3),
inference(step,[status(thm)],[t10,t13]) ).
cnf(t22,plain,
add(a,sF3) = sF4,
inference(orient,[status(thm)],[t7845]) ).
cnf(t2,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
inference(orient,[status(thm)],[t2]) ).
cnf(t1,axiom,
multiply(add(X1,X2),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
multiply(add(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t28,plain,
multiply(X1,add(add(X2,X1),X3)) = add(X1,multiply(X3,X1)),
inference(cp,[status(thm)],[t25,t15]) ).
cnf(t108,plain,
multiply(X1,add(add(X2,X1),X3)) = add(X1,multiply(X3,X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(u0,axiom,
pixley(X,X,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
pixley(X,Y,Z) = add(multiply(X,inverse(Y)),add(multiply(X,Z),multiply(inverse(Y),Z))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3,plain,
add(multiply(X1,inverse(X1)),add(multiply(X1,X2),multiply(inverse(X1),X2))) = X2,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t7846,plain,
add(multiply(X1,inverse(X1)),multiply(X2,add(X1,inverse(X1)))) = X2,
inference(step,[status(thm)],[t3,t25]) ).
cnf(t0,axiom,
add(X1,inverse(X1)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t14,plain,
add(X1,inverse(X1)) = n1,
inference(orient,[status(thm)],[t0]) ).
cnf(t7847,plain,
add(multiply(X1,inverse(X1)),multiply(X2,n1)) = X2,
inference(step,[status(thm)],[t7846,t14]) ).
cnf(t71,plain,
add(multiply(X1,inverse(X1)),multiply(X2,n1)) = X2,
inference(orient,[status(thm)],[t7847]) ).
cnf(t72,plain,
add(X1,n1) = add(multiply(X2,inverse(X2)),n1),
inference(cp,[status(thm)],[t71,t15]) ).
cnf(t18,plain,
inverse(X1) = multiply(n1,inverse(X1)),
inference(cp,[status(thm)],[t15,t14]) ).
cnf(t21,plain,
multiply(n1,inverse(X1)) = inverse(X1),
inference(orient,[status(thm)],[t18]) ).
cnf(t73,plain,
X1 = add(inverse(n1),multiply(X1,n1)),
inference(cp,[status(thm)],[t71,t21]) ).
cnf(t90,plain,
add(inverse(n1),multiply(X1,n1)) = X1,
inference(orient,[status(thm)],[t73]) ).
cnf(t91,plain,
add(X1,n1) = add(inverse(n1),n1),
inference(cp,[status(thm)],[t90,t15]) ).
cnf(t165,plain,
add(X1,n1) = add(inverse(n1),n1),
inference(orient,[status(thm)],[t91]) ).
cnf(t7864,plain,
add(X1,n1) = add(inverse(n1),n1),
inference(step,[status(thm)],[t72,t165]) ).
cnf(t7865,plain,
add(X1,n1) = add(f1,n1),
inference(step,[status(thm)],[t7864,t165]) ).
cnf(t430,plain,
add(X1,n1) = add(f1,n1),
inference(orient,[status(thm)],[t7865]) ).
cnf(t433,plain,
add(X1,multiply(n1,X1)) = multiply(X1,add(f1,n1)),
inference(cp,[status(thm)],[t108,t430]) ).
cnf(t439,plain,
add(X1,multiply(n1,X1)) = multiply(X1,add(f1,n1)),
inference(orient,[status(thm)],[t433]) ).
cnf(t74,plain,
multiply(X1,n1) = multiply(X1,multiply(X1,n1)),
inference(cp,[status(thm)],[t15,t71]) ).
cnf(t87,plain,
multiply(X1,multiply(X1,n1)) = multiply(X1,n1),
inference(orient,[status(thm)],[t74]) ).
cnf(t443,plain,
multiply(multiply(n1,n1),add(f1,n1)) = add(multiply(n1,n1),multiply(n1,n1)),
inference(cp,[status(thm)],[t439,t87]) ).
cnf(t7867,plain,
multiply(multiply(n1,n1),add(f1,n1)) = multiply(n1,add(n1,n1)),
inference(step,[status(thm)],[t443,t25]) ).
cnf(t7868,plain,
multiply(multiply(n1,n1),add(f1,n1)) = multiply(n1,add(f1,n1)),
inference(step,[status(thm)],[t7867,t430]) ).
cnf(t457,plain,
multiply(multiply(n1,n1),add(f1,n1)) = multiply(n1,add(f1,n1)),
inference(orient,[status(thm)],[t7868]) ).
cnf(t460,plain,
multiply(add(f1,n1),add(X1,multiply(n1,n1))) = add(multiply(X1,add(f1,n1)),multiply(n1,add(f1,n1))),
inference(cp,[status(thm)],[t25,t457]) ).
cnf(t7956,plain,
multiply(add(f1,n1),add(X1,multiply(n1,n1))) = multiply(add(f1,n1),add(X1,n1)),
inference(step,[status(thm)],[t460,t25]) ).
cnf(t3024,plain,
multiply(add(f1,n1),add(X1,multiply(n1,n1))) = multiply(add(f1,n1),add(X1,n1)),
inference(orient,[status(thm)],[t7956]) ).
cnf(t3027,plain,
multiply(add(f1,n1),add(inverse(n1),n1)) = multiply(add(f1,n1),n1),
inference(cp,[status(thm)],[t3024,t90]) ).
cnf(t7957,plain,
multiply(add(f1,n1),add(f1,n1)) = multiply(add(f1,n1),n1),
inference(step,[status(thm)],[t3027,t165]) ).
cnf(t38,plain,
multiply(X1,X2) = multiply(multiply(X2,add(X3,X1)),multiply(X1,X2)),
inference(cp,[status(thm)],[t15,t25]) ).
cnf(t167,plain,
multiply(multiply(X1,add(X2,X3)),multiply(X3,X1)) = multiply(X3,X1),
inference(orient,[status(thm)],[t38]) ).
cnf(t171,plain,
multiply(X1,add(X2,add(X3,X1))) = multiply(add(X3,X1),multiply(X1,add(X2,add(X3,X1)))),
inference(cp,[status(thm)],[t167,t15]) ).
cnf(t29,plain,
multiply(X1,add(X2,add(X3,X1))) = add(multiply(X2,X1),X1),
inference(cp,[status(thm)],[t25,t15]) ).
cnf(t119,plain,
multiply(X1,add(X2,add(X3,X1))) = add(multiply(X2,X1),X1),
inference(orient,[status(thm)],[t29]) ).
cnf(t7881,plain,
add(multiply(X2,X1),X1) = multiply(add(X3,X1),multiply(X1,add(X2,add(X3,X1)))),
inference(step,[status(thm)],[t171,t119]) ).
cnf(t7882,plain,
add(multiply(X2,X1),X1) = multiply(add(X3,X1),add(multiply(X2,X1),X1)),
inference(step,[status(thm)],[t7881,t119]) ).
cnf(t912,plain,
multiply(add(X1,X2),add(multiply(X3,X2),X2)) = add(multiply(X3,X2),X2),
inference(orient,[status(thm)],[t7882]) ).
cnf(t914,plain,
add(multiply(add(X1,X2),X2),X2) = multiply(add(X3,X2),add(X2,X2)),
inference(cp,[status(thm)],[t912,t15]) ).
cnf(t7885,plain,
add(X2,X2) = multiply(add(X3,X2),add(X2,X2)),
inference(step,[status(thm)],[t914,t15]) ).
cnf(t1006,plain,
multiply(add(X1,X2),add(X2,X2)) = add(X2,X2),
inference(orient,[status(thm)],[t7885]) ).
cnf(t1022,plain,
add(n1,n1) = multiply(add(X1,n1),add(f1,n1)),
inference(cp,[status(thm)],[t1006,t430]) ).
cnf(t7889,plain,
add(f1,n1) = multiply(add(X1,n1),add(f1,n1)),
inference(step,[status(thm)],[t1022,t430]) ).
cnf(t1084,plain,
multiply(add(X1,n1),add(f1,n1)) = add(f1,n1),
inference(orient,[status(thm)],[t7889]) ).
cnf(t7958,plain,
add(f1,n1) = multiply(add(f1,n1),n1),
inference(step,[status(thm)],[t7957,t1084]) ).
cnf(t7959,plain,
add(f1,n1) = n1,
inference(step,[status(thm)],[t7958,t15]) ).
cnf(t3045,plain,
add(f1,n1) = n1,
inference(orient,[status(thm)],[t7959]) ).
cnf(t7962,plain,
add(X1,multiply(n1,X1)) = multiply(X1,n1),
inference(step,[status(thm)],[t439,t3045]) ).
cnf(t3048,plain,
add(X1,multiply(n1,X1)) = multiply(X1,n1),
inference(orient,[status(thm)],[t7962]) ).
cnf(t170,plain,
multiply(inverse(X1),X2) = multiply(multiply(X2,n1),multiply(inverse(X1),X2)),
inference(cp,[status(thm)],[t167,t14]) ).
cnf(t389,plain,
multiply(multiply(X1,n1),multiply(inverse(X2),X1)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t170]) ).
cnf(t390,plain,
multiply(inverse(X1),add(X2,n1)) = multiply(n1,multiply(inverse(X1),add(X2,n1))),
inference(cp,[status(thm)],[t389,t15]) ).
cnf(t419,plain,
multiply(n1,multiply(inverse(X1),add(X2,n1))) = multiply(inverse(X1),add(X2,n1)),
inference(orient,[status(thm)],[t390]) ).
cnf(t3066,plain,
multiply(inverse(X1),add(f1,n1)) = multiply(n1,multiply(inverse(X1),n1)),
inference(cp,[status(thm)],[t419,t3045]) ).
cnf(t7969,plain,
multiply(inverse(X1),n1) = multiply(n1,multiply(inverse(X1),n1)),
inference(step,[status(thm)],[t3066,t3045]) ).
cnf(t3127,plain,
multiply(n1,multiply(inverse(X1),n1)) = multiply(inverse(X1),n1),
inference(orient,[status(thm)],[t7969]) ).
cnf(t3131,plain,
multiply(multiply(inverse(X1),n1),n1) = add(multiply(inverse(X1),n1),multiply(inverse(X1),n1)),
inference(cp,[status(thm)],[t3048,t3127]) ).
cnf(t7970,plain,
multiply(multiply(inverse(X1),n1),n1) = multiply(n1,add(inverse(X1),inverse(X1))),
inference(step,[status(thm)],[t3131,t25]) ).
cnf(t34,plain,
multiply(inverse(X1),add(n1,X2)) = add(inverse(X1),multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t25,t21]) ).
cnf(t129,plain,
add(inverse(X1),multiply(X2,inverse(X1))) = multiply(inverse(X1),add(n1,X2)),
inference(orient,[status(thm)],[t34]) ).
cnf(t130,plain,
multiply(inverse(X1),add(n1,n1)) = add(inverse(X1),inverse(X1)),
inference(cp,[status(thm)],[t129,t21]) ).
cnf(t7916,plain,
multiply(inverse(X1),add(f1,n1)) = add(inverse(X1),inverse(X1)),
inference(step,[status(thm)],[t130,t430]) ).
cnf(t2412,plain,
multiply(inverse(X1),add(f1,n1)) = add(inverse(X1),inverse(X1)),
inference(orient,[status(thm)],[t7916]) ).
cnf(t7964,plain,
multiply(inverse(X1),n1) = add(inverse(X1),inverse(X1)),
inference(step,[status(thm)],[t2412,t3045]) ).
cnf(t3053,plain,
multiply(inverse(X1),n1) = add(inverse(X1),inverse(X1)),
inference(rw,[status(thm)],[t7964]) ).
cnf(t3093,plain,
add(inverse(X1),inverse(X1)) = multiply(inverse(X1),n1),
inference(orient,[status(thm)],[t3053]) ).
cnf(t7971,plain,
multiply(multiply(inverse(X1),n1),n1) = multiply(n1,multiply(inverse(X1),n1)),
inference(step,[status(thm)],[t7970,t3093]) ).
cnf(t7972,plain,
multiply(multiply(inverse(X1),n1),n1) = multiply(inverse(X1),n1),
inference(step,[status(thm)],[t7971,t3127]) ).
cnf(t3141,plain,
multiply(multiply(inverse(X1),n1),n1) = multiply(inverse(X1),n1),
inference(orient,[status(thm)],[t7972]) ).
cnf(t3144,plain,
multiply(inverse(X1),n1) = add(multiply(X2,inverse(X2)),multiply(inverse(X1),n1)),
inference(cp,[status(thm)],[t71,t3141]) ).
cnf(t7973,plain,
multiply(inverse(X1),n1) = inverse(X1),
inference(step,[status(thm)],[t3144,t71]) ).
cnf(t3157,plain,
multiply(inverse(X1),n1) = inverse(X1),
inference(orient,[status(thm)],[t7973]) ).
cnf(t3166,plain,
inverse(X1) = add(inverse(n1),inverse(X1)),
inference(cp,[status(thm)],[t90,t3157]) ).
cnf(t3259,plain,
add(inverse(n1),inverse(X1)) = inverse(X1),
inference(orient,[status(thm)],[t3166]) ).
cnf(t3260,plain,
inverse(inverse(n1)) = n1,
inference(cp,[status(thm)],[t3259,t14]) ).
cnf(t3276,plain,
inverse(inverse(n1)) = n1,
inference(orient,[status(thm)],[t3260]) ).
cnf(t3278,plain,
X1 = add(multiply(inverse(n1),n1),multiply(X1,n1)),
inference(cp,[status(thm)],[t71,t3276]) ).
cnf(t7988,plain,
X1 = multiply(n1,add(inverse(n1),X1)),
inference(step,[status(thm)],[t3278,t25]) ).
cnf(t3464,plain,
multiply(n1,add(inverse(n1),X1)) = X1,
inference(orient,[status(thm)],[t7988]) ).
cnf(t3473,plain,
multiply(add(inverse(n1),X1),n1) = add(add(inverse(n1),X1),X1),
inference(cp,[status(thm)],[t3048,t3464]) ).
cnf(t3162,plain,
multiply(n1,add(inverse(X1),X2)) = add(inverse(X1),multiply(X2,n1)),
inference(cp,[status(thm)],[t25,t3157]) ).
cnf(t3361,plain,
add(inverse(X1),multiply(X2,n1)) = multiply(n1,add(inverse(X1),X2)),
inference(orient,[status(thm)],[t3162]) ).
cnf(t3469,plain,
multiply(X1,n1) = multiply(n1,multiply(n1,add(inverse(n1),X1))),
inference(cp,[status(thm)],[t3464,t3361]) ).
cnf(t7990,plain,
multiply(X1,n1) = multiply(n1,X1),
inference(step,[status(thm)],[t3469,t3464]) ).
cnf(t3500,plain,
multiply(X1,n1) = multiply(n1,X1),
inference(orient,[status(thm)],[t7990]) ).
cnf(t7999,plain,
multiply(n1,add(inverse(n1),X1)) = add(add(inverse(n1),X1),X1),
inference(step,[status(thm)],[t3473,t3500]) ).
cnf(t8000,plain,
X1 = add(add(inverse(n1),X1),X1),
inference(step,[status(thm)],[t7999,t3464]) ).
cnf(t3666,plain,
add(add(inverse(n1),X1),X1) = X1,
inference(orient,[status(thm)],[t8000]) ).
cnf(t3677,plain,
add(X1,multiply(X2,X1)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t108,t3666]) ).
cnf(t4251,plain,
add(X1,multiply(X2,X1)) = multiply(X1,add(X1,X2)),
inference(orient,[status(thm)],[t3677]) ).
cnf(t8040,plain,
multiply(X1,add(add(X2,X1),X3)) = multiply(X1,add(X1,X3)),
inference(step,[status(thm)],[t108,t4251]) ).
cnf(t4255,plain,
multiply(X1,add(add(X2,X1),X3)) = multiply(X1,add(X1,X3)),
inference(orient,[status(thm)],[t8040]) ).
cnf(u2,axiom,
pixley(X,Y,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X1),multiply(inverse(X2),X1))) = X1,
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(t7850,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t4,t25]) ).
cnf(t104,plain,
add(multiply(X1,inverse(X2)),multiply(X1,add(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t7850]) ).
cnf(t3560,plain,
multiply(n1,add(inverse(X1),X2)) = add(inverse(X1),multiply(n1,X2)),
inference(cp,[status(thm)],[t3361,t3500]) ).
cnf(t5737,plain,
add(inverse(X1),multiply(n1,X2)) = multiply(n1,add(inverse(X1),X2)),
inference(orient,[status(thm)],[t3560]) ).
cnf(t5755,plain,
multiply(n1,X1) = add(multiply(n1,add(inverse(n1),X1)),multiply(n1,X1)),
inference(cp,[status(thm)],[t3666,t5737]) ).
cnf(t8163,plain,
multiply(n1,X1) = add(X1,multiply(n1,X1)),
inference(step,[status(thm)],[t5755,t3464]) ).
cnf(t8164,plain,
multiply(n1,X1) = multiply(X1,add(X1,n1)),
inference(step,[status(thm)],[t8163,t4251]) ).
cnf(t7960,plain,
add(X1,n1) = n1,
inference(step,[status(thm)],[t430,t3045]) ).
cnf(t3046,plain,
add(X1,n1) = n1,
inference(orient,[status(thm)],[t7960]) ).
cnf(t8165,plain,
multiply(n1,X1) = multiply(X1,n1),
inference(step,[status(thm)],[t8164,t3046]) ).
cnf(t5810,plain,
multiply(n1,X1) = multiply(X1,n1),
inference(orient,[status(thm)],[t8165]) ).
cnf(t5823,plain,
n1 = add(multiply(n1,inverse(X1)),multiply(add(n1,inverse(X1)),n1)),
inference(cp,[status(thm)],[t104,t5810]) ).
cnf(t8166,plain,
n1 = add(inverse(X1),multiply(add(n1,inverse(X1)),n1)),
inference(step,[status(thm)],[t5823,t21]) ).
cnf(t8167,plain,
n1 = multiply(n1,add(inverse(X1),add(n1,inverse(X1)))),
inference(step,[status(thm)],[t8166,t3361]) ).
cnf(t3679,plain,
add(multiply(X1,X2),X2) = multiply(X2,add(X1,X2)),
inference(cp,[status(thm)],[t119,t3666]) ).
cnf(t4371,plain,
add(multiply(X1,X2),X2) = multiply(X2,add(X1,X2)),
inference(orient,[status(thm)],[t3679]) ).
cnf(t3676,plain,
add(X1,multiply(X1,X1)) = multiply(X1,X1),
inference(cp,[status(thm)],[t108,t3666]) ).
cnf(t3674,plain,
X1 = multiply(X1,X1),
inference(cp,[status(thm)],[t15,t3666]) ).
cnf(t3741,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t3674]) ).
cnf(t8020,plain,
add(X1,X1) = multiply(X1,X1),
inference(step,[status(thm)],[t3676,t3741]) ).
cnf(t8021,plain,
add(X1,X1) = X1,
inference(step,[status(thm)],[t8020,t3741]) ).
cnf(t3859,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t8021]) ).
cnf(t3927,plain,
add(X1,multiply(add(X2,X1),X1)) = multiply(X1,add(X2,X1)),
inference(cp,[status(thm)],[t108,t3859]) ).
cnf(t8084,plain,
multiply(X1,add(X1,add(X2,X1))) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t3927,t4251]) ).
cnf(t8062,plain,
multiply(X1,add(X2,add(X3,X1))) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t119,t4371]) ).
cnf(t4375,plain,
multiply(X1,add(X2,add(X3,X1))) = multiply(X1,add(X2,X1)),
inference(orient,[status(thm)],[t8062]) ).
cnf(t8085,plain,
multiply(X1,add(X1,X1)) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t8084,t4375]) ).
cnf(t8086,plain,
multiply(X1,X1) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t8085,t3859]) ).
cnf(t8087,plain,
X1 = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t8086,t3741]) ).
cnf(t4682,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t8087]) ).
cnf(t8094,plain,
add(multiply(X1,X2),X2) = X2,
inference(step,[status(thm)],[t4371,t4682]) ).
cnf(t4689,plain,
add(multiply(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t8094]) ).
cnf(t4727,plain,
add(X1,X2) = add(X2,add(X1,X2)),
inference(cp,[status(thm)],[t4689,t4682]) ).
cnf(t5479,plain,
add(X1,add(X2,X1)) = add(X2,X1),
inference(orient,[status(thm)],[t4727]) ).
cnf(t8168,plain,
n1 = multiply(n1,add(n1,inverse(X1))),
inference(step,[status(thm)],[t8167,t5479]) ).
cnf(t3062,plain,
add(n1,multiply(X1,n1)) = multiply(n1,add(n1,X1)),
inference(cp,[status(thm)],[t108,t3045]) ).
cnf(t3114,plain,
add(n1,multiply(X1,n1)) = multiply(n1,add(n1,X1)),
inference(orient,[status(thm)],[t3062]) ).
cnf(t3180,plain,
multiply(n1,add(n1,inverse(X1))) = add(n1,inverse(X1)),
inference(cp,[status(thm)],[t3114,t3157]) ).
cnf(t3397,plain,
multiply(n1,add(n1,inverse(X1))) = add(n1,inverse(X1)),
inference(orient,[status(thm)],[t3180]) ).
cnf(t8169,plain,
n1 = add(n1,inverse(X1)),
inference(step,[status(thm)],[t8168,t3397]) ).
cnf(t5863,plain,
add(n1,inverse(X1)) = n1,
inference(orient,[status(thm)],[t8169]) ).
cnf(u1,axiom,
pixley(X,Y,Y) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
add(multiply(X1,inverse(X2)),add(multiply(X1,X2),multiply(inverse(X2),X2))) = X1,
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t7851,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(step,[status(thm)],[t5,t25]) ).
cnf(t146,plain,
add(multiply(X1,inverse(X2)),multiply(X2,add(X1,inverse(X2)))) = X1,
inference(orient,[status(thm)],[t7851]) ).
cnf(t5825,plain,
X1 = add(multiply(X1,inverse(n1)),multiply(add(X1,inverse(n1)),n1)),
inference(cp,[status(thm)],[t146,t5810]) ).
cnf(t35,plain,
multiply(inverse(X1),add(X2,n1)) = add(multiply(X2,inverse(X1)),inverse(X1)),
inference(cp,[status(thm)],[t25,t21]) ).
cnf(t131,plain,
add(multiply(X1,inverse(X2)),inverse(X2)) = multiply(inverse(X2),add(X1,n1)),
inference(orient,[status(thm)],[t35]) ).
cnf(t150,plain,
multiply(X1,inverse(X2)) = add(multiply(multiply(X1,inverse(X2)),inverse(X2)),multiply(X2,multiply(inverse(X2),add(X1,n1)))),
inference(cp,[status(thm)],[t146,t131]) ).
cnf(t7979,plain,
multiply(X1,inverse(X2)) = add(multiply(multiply(X1,inverse(X2)),inverse(X2)),multiply(X2,multiply(inverse(X2),n1))),
inference(step,[status(thm)],[t150,t3046]) ).
cnf(t7980,plain,
multiply(X1,inverse(X2)) = add(multiply(multiply(X1,inverse(X2)),inverse(X2)),multiply(X2,inverse(X2))),
inference(step,[status(thm)],[t7979,t3157]) ).
cnf(t7981,plain,
multiply(X1,inverse(X2)) = multiply(inverse(X2),add(multiply(X1,inverse(X2)),X2)),
inference(step,[status(thm)],[t7980,t25]) ).
cnf(t3310,plain,
multiply(inverse(X1),add(multiply(X2,inverse(X1)),X1)) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t7981]) ).
cnf(t3314,plain,
multiply(X1,inverse(n1)) = multiply(inverse(n1),n1),
inference(cp,[status(thm)],[t3310,t3046]) ).
cnf(t7982,plain,
multiply(X1,inverse(n1)) = inverse(n1),
inference(step,[status(thm)],[t3314,t3157]) ).
cnf(t3337,plain,
multiply(X1,inverse(n1)) = inverse(n1),
inference(orient,[status(thm)],[t7982]) ).
cnf(t8170,plain,
X1 = add(inverse(n1),multiply(add(X1,inverse(n1)),n1)),
inference(step,[status(thm)],[t5825,t3337]) ).
cnf(t8171,plain,
X1 = multiply(n1,add(inverse(n1),add(X1,inverse(n1)))),
inference(step,[status(thm)],[t8170,t3361]) ).
cnf(t8172,plain,
X1 = add(X1,inverse(n1)),
inference(step,[status(thm)],[t8171,t3464]) ).
cnf(t5877,plain,
add(X1,inverse(n1)) = X1,
inference(orient,[status(thm)],[t8172]) ).
cnf(t5878,plain,
X1 = add(multiply(X1,inverse(n1)),multiply(X1,X1)),
inference(cp,[status(thm)],[t104,t5877]) ).
cnf(t8173,plain,
X1 = add(inverse(n1),multiply(X1,X1)),
inference(step,[status(thm)],[t5878,t3337]) ).
cnf(t8174,plain,
X1 = add(inverse(n1),X1),
inference(step,[status(thm)],[t8173,t3741]) ).
cnf(t5888,plain,
add(inverse(n1),X1) = X1,
inference(orient,[status(thm)],[t8174]) ).
cnf(t8178,plain,
multiply(n1,X1) = X1,
inference(step,[status(thm)],[t3464,t5888]) ).
cnf(t5892,plain,
multiply(n1,X1) = X1,
inference(rw,[status(thm)],[t8178]) ).
cnf(t5907,plain,
multiply(n1,X1) = X1,
inference(orient,[status(thm)],[t5892]) ).
cnf(t5934,plain,
n1 = add(inverse(X1),multiply(X1,add(n1,inverse(X1)))),
inference(cp,[status(thm)],[t146,t5907]) ).
cnf(t8199,plain,
n1 = add(inverse(X1),multiply(X1,n1)),
inference(step,[status(thm)],[t5934,t5863]) ).
cnf(t8184,plain,
add(inverse(X1),multiply(X2,n1)) = add(inverse(X1),X2),
inference(step,[status(thm)],[t3361,t5907]) ).
cnf(t5914,plain,
add(inverse(X1),multiply(X2,n1)) = add(inverse(X1),X2),
inference(orient,[status(thm)],[t8184]) ).
cnf(t8200,plain,
n1 = add(inverse(X1),X1),
inference(step,[status(thm)],[t8199,t5914]) ).
cnf(t6070,plain,
add(inverse(X1),X1) = n1,
inference(orient,[status(thm)],[t8200]) ).
cnf(t6074,plain,
inverse(inverse(X1)) = add(multiply(inverse(inverse(X1)),inverse(X1)),multiply(X1,n1)),
inference(cp,[status(thm)],[t146,t6070]) ).
cnf(t5894,plain,
inverse(n1) = add(multiply(inverse(n1),inverse(X1)),multiply(X1,inverse(X1))),
inference(cp,[status(thm)],[t146,t5888]) ).
cnf(t8194,plain,
inverse(n1) = multiply(inverse(X1),add(inverse(n1),X1)),
inference(step,[status(thm)],[t5894,t25]) ).
cnf(t8195,plain,
inverse(n1) = multiply(inverse(X1),X1),
inference(step,[status(thm)],[t8194,t5888]) ).
cnf(t6020,plain,
multiply(inverse(X1),X1) = inverse(n1),
inference(orient,[status(thm)],[t8195]) ).
cnf(t8201,plain,
inverse(inverse(X1)) = add(inverse(n1),multiply(X1,n1)),
inference(step,[status(thm)],[t6074,t6020]) ).
cnf(t8202,plain,
inverse(inverse(X1)) = multiply(X1,n1),
inference(step,[status(thm)],[t8201,t5888]) ).
cnf(t8188,plain,
multiply(X1,n1) = X1,
inference(step,[status(thm)],[t3500,t5907]) ).
cnf(t5918,plain,
multiply(X1,n1) = X1,
inference(orient,[status(thm)],[t8188]) ).
cnf(t8203,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t8202,t5918]) ).
cnf(t6098,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t8203]) ).
cnf(t6115,plain,
n1 = add(n1,X1),
inference(cp,[status(thm)],[t5863,t6098]) ).
cnf(t6116,plain,
add(n1,X1) = n1,
inference(orient,[status(thm)],[t6115]) ).
cnf(t6122,plain,
multiply(X1,add(X1,X2)) = multiply(X1,add(n1,X2)),
inference(cp,[status(thm)],[t4255,t6116]) ).
cnf(t8249,plain,
multiply(X1,add(X1,X2)) = multiply(X1,n1),
inference(step,[status(thm)],[t6122,t6116]) ).
cnf(t8250,plain,
multiply(X1,add(X1,X2)) = X1,
inference(step,[status(thm)],[t8249,t5918]) ).
cnf(t6481,plain,
multiply(X1,add(X1,X2)) = X1,
inference(orient,[status(thm)],[t8250]) ).
cnf(t6514,plain,
a = multiply(a,sF4),
inference(cp,[status(thm)],[t6481,t22]) ).
cnf(t6597,plain,
multiply(a,sF4) = a,
inference(orient,[status(thm)],[t6514]) ).
cnf(t6598,plain,
multiply(sF4,add(a,X1)) = add(a,multiply(X1,sF4)),
inference(cp,[status(thm)],[t25,t6597]) ).
cnf(t7788,plain,
add(a,multiply(X1,sF4)) = multiply(sF4,add(a,X1)),
inference(orient,[status(thm)],[t6598]) ).
cnf(t26,plain,
multiply(c,add(b,X1)) = add(sF3,multiply(X1,c)),
inference(cp,[status(thm)],[t25,t13]) ).
cnf(t39,plain,
add(sF3,multiply(X1,c)) = multiply(c,add(b,X1)),
inference(orient,[status(thm)],[t26]) ).
cnf(t40,plain,
multiply(c,add(b,b)) = add(sF3,sF3),
inference(cp,[status(thm)],[t39,t13]) ).
cnf(t65,plain,
multiply(c,add(b,b)) = add(sF3,sF3),
inference(orient,[status(thm)],[t40]) ).
cnf(t3860,plain,
multiply(c,b) = add(sF3,sF3),
inference(rw,[status(thm)],[t65]) ).
cnf(t8032,plain,
multiply(c,b) = sF3,
inference(step,[status(thm)],[t3860,t3859]) ).
cnf(t3943,plain,
multiply(c,b) = sF3,
inference(orient,[status(thm)],[t8032]) ).
cnf(t3945,plain,
multiply(b,add(X1,c)) = add(multiply(X1,b),sF3),
inference(cp,[status(thm)],[t25,t3943]) ).
cnf(t4796,plain,
add(multiply(X1,b),sF3) = multiply(b,add(X1,c)),
inference(orient,[status(thm)],[t3945]) ).
cnf(t5950,plain,
multiply(b,add(n1,c)) = add(b,sF3),
inference(cp,[status(thm)],[t4796,t5907]) ).
cnf(t8229,plain,
multiply(b,n1) = add(b,sF3),
inference(step,[status(thm)],[t5950,t6116]) ).
cnf(t8230,plain,
b = add(b,sF3),
inference(step,[status(thm)],[t8229,t5918]) ).
cnf(t6341,plain,
add(b,sF3) = b,
inference(orient,[status(thm)],[t8230]) ).
cnf(t6351,plain,
sF3 = multiply(sF3,b),
inference(cp,[status(thm)],[t4682,t6341]) ).
cnf(t6369,plain,
multiply(sF3,b) = sF3,
inference(orient,[status(thm)],[t6351]) ).
cnf(t6371,plain,
multiply(b,add(X1,sF3)) = add(multiply(X1,b),sF3),
inference(cp,[status(thm)],[t25,t6369]) ).
cnf(t8317,plain,
multiply(b,add(X1,sF3)) = multiply(b,add(X1,c)),
inference(step,[status(thm)],[t6371,t4796]) ).
cnf(t7134,plain,
multiply(b,add(X1,c)) = multiply(b,add(X1,sF3)),
inference(orient,[status(thm)],[t8317]) ).
cnf(t7138,plain,
multiply(b,add(a,sF3)) = multiply(b,sF1),
inference(cp,[status(thm)],[t7134,t12]) ).
cnf(t8320,plain,
multiply(b,sF4) = multiply(b,sF1),
inference(step,[status(thm)],[t7138,t22]) ).
cnf(t7157,plain,
multiply(b,sF4) = multiply(b,sF1),
inference(orient,[status(thm)],[t8320]) ).
cnf(t7793,plain,
multiply(sF4,add(a,b)) = add(a,multiply(b,sF1)),
inference(cp,[status(thm)],[t7788,t7157]) ).
cnf(t8365,plain,
multiply(sF4,sF0) = add(a,multiply(b,sF1)),
inference(step,[status(thm)],[t7793,t11]) ).
cnf(t23,plain,
sF3 = multiply(sF4,sF3),
inference(cp,[status(thm)],[t15,t22]) ).
cnf(t24,plain,
multiply(sF4,sF3) = sF3,
inference(orient,[status(thm)],[t23]) ).
cnf(t36,plain,
multiply(sF3,add(sF4,X1)) = add(sF3,multiply(X1,sF3)),
inference(cp,[status(thm)],[t25,t24]) ).
cnf(t59,plain,
add(sF3,multiply(X1,sF3)) = multiply(sF3,add(sF4,X1)),
inference(orient,[status(thm)],[t36]) ).
cnf(t61,plain,
multiply(sF3,add(sF4,sF4)) = add(sF3,sF3),
inference(cp,[status(thm)],[t59,t24]) ).
cnf(t84,plain,
multiply(sF3,add(sF4,sF4)) = add(sF3,sF3),
inference(orient,[status(thm)],[t61]) ).
cnf(t3863,plain,
multiply(sF3,sF4) = add(sF3,sF3),
inference(rw,[status(thm)],[t84]) ).
cnf(t8035,plain,
multiply(sF3,sF4) = sF3,
inference(step,[status(thm)],[t3863,t3859]) ).
cnf(t4167,plain,
multiply(sF3,sF4) = sF3,
inference(orient,[status(thm)],[t8035]) ).
cnf(t4168,plain,
multiply(sF4,add(sF3,X1)) = add(sF3,multiply(X1,sF4)),
inference(cp,[status(thm)],[t25,t4167]) ).
cnf(t5022,plain,
add(sF3,multiply(X1,sF4)) = multiply(sF4,add(sF3,X1)),
inference(orient,[status(thm)],[t4168]) ).
cnf(t6511,plain,
a = multiply(a,sF0),
inference(cp,[status(thm)],[t6481,t11]) ).
cnf(t6573,plain,
multiply(a,sF0) = a,
inference(orient,[status(thm)],[t6511]) ).
cnf(t6574,plain,
multiply(sF0,add(a,X1)) = add(a,multiply(X1,sF0)),
inference(cp,[status(thm)],[t25,t6573]) ).
cnf(t7528,plain,
add(a,multiply(X1,sF0)) = multiply(sF0,add(a,X1)),
inference(orient,[status(thm)],[t6574]) ).
cnf(t6345,plain,
multiply(sF3,add(sF3,X1)) = multiply(sF3,add(b,X1)),
inference(cp,[status(thm)],[t4255,t6341]) ).
cnf(t8311,plain,
sF3 = multiply(sF3,add(b,X1)),
inference(step,[status(thm)],[t6345,t6481]) ).
cnf(t7035,plain,
multiply(sF3,add(b,X1)) = sF3,
inference(orient,[status(thm)],[t8311]) ).
cnf(t16,plain,
b = multiply(sF0,b),
inference(cp,[status(thm)],[t15,t11]) ).
cnf(t19,plain,
multiply(sF0,b) = b,
inference(orient,[status(thm)],[t16]) ).
cnf(t30,plain,
multiply(b,add(sF0,X1)) = add(b,multiply(X1,b)),
inference(cp,[status(thm)],[t25,t19]) ).
cnf(t47,plain,
add(b,multiply(X1,b)) = multiply(b,add(sF0,X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t49,plain,
multiply(b,add(sF0,sF0)) = add(b,b),
inference(cp,[status(thm)],[t47,t19]) ).
cnf(t78,plain,
multiply(b,add(sF0,sF0)) = add(b,b),
inference(orient,[status(thm)],[t49]) ).
cnf(t3861,plain,
multiply(b,sF0) = add(b,b),
inference(rw,[status(thm)],[t78]) ).
cnf(t8033,plain,
multiply(b,sF0) = b,
inference(step,[status(thm)],[t3861,t3859]) ).
cnf(t4134,plain,
multiply(b,sF0) = b,
inference(orient,[status(thm)],[t8033]) ).
cnf(t4135,plain,
multiply(sF0,add(b,X1)) = add(b,multiply(X1,sF0)),
inference(cp,[status(thm)],[t25,t4134]) ).
cnf(t4830,plain,
add(b,multiply(X1,sF0)) = multiply(sF0,add(b,X1)),
inference(orient,[status(thm)],[t4135]) ).
cnf(t4831,plain,
multiply(sF0,add(b,add(X1,sF0))) = add(b,sF0),
inference(cp,[status(thm)],[t4830,t15]) ).
cnf(t8088,plain,
multiply(X1,add(X2,add(X3,X1))) = X1,
inference(step,[status(thm)],[t4375,t4682]) ).
cnf(t4683,plain,
multiply(X1,add(X2,add(X3,X1))) = X1,
inference(orient,[status(thm)],[t8088]) ).
cnf(t8112,plain,
sF0 = add(b,sF0),
inference(step,[status(thm)],[t4831,t4683]) ).
cnf(t4835,plain,
add(b,sF0) = sF0,
inference(orient,[status(thm)],[t8112]) ).
cnf(t7039,plain,
sF3 = multiply(sF3,sF0),
inference(cp,[status(thm)],[t7035,t4835]) ).
cnf(t7051,plain,
multiply(sF3,sF0) = sF3,
inference(orient,[status(thm)],[t7039]) ).
cnf(t7534,plain,
multiply(sF0,add(a,sF3)) = add(a,sF3),
inference(cp,[status(thm)],[t7528,t7051]) ).
cnf(t8342,plain,
multiply(sF0,sF4) = add(a,sF3),
inference(step,[status(thm)],[t7534,t22]) ).
cnf(t8343,plain,
multiply(sF0,sF4) = sF4,
inference(step,[status(thm)],[t8342,t22]) ).
cnf(t7544,plain,
multiply(sF0,sF4) = sF4,
inference(orient,[status(thm)],[t8343]) ).
cnf(t7552,plain,
multiply(sF4,add(sF3,sF0)) = add(sF3,sF4),
inference(cp,[status(thm)],[t5022,t7544]) ).
cnf(t7060,plain,
sF0 = add(sF3,sF0),
inference(cp,[status(thm)],[t4689,t7051]) ).
cnf(t7072,plain,
add(sF3,sF0) = sF0,
inference(orient,[status(thm)],[t7060]) ).
cnf(t8346,plain,
multiply(sF4,sF0) = add(sF3,sF4),
inference(step,[status(thm)],[t7552,t7072]) ).
cnf(t5023,plain,
multiply(sF4,add(sF3,add(X1,sF4))) = add(sF3,sF4),
inference(cp,[status(thm)],[t5022,t15]) ).
cnf(t8114,plain,
sF4 = add(sF3,sF4),
inference(step,[status(thm)],[t5023,t4683]) ).
cnf(t5026,plain,
add(sF3,sF4) = sF4,
inference(orient,[status(thm)],[t8114]) ).
cnf(t8347,plain,
multiply(sF4,sF0) = sF4,
inference(step,[status(thm)],[t8346,t5026]) ).
cnf(t7602,plain,
multiply(sF4,sF0) = sF4,
inference(orient,[status(thm)],[t8347]) ).
cnf(t8366,plain,
sF4 = add(a,multiply(b,sF1)),
inference(step,[status(thm)],[t8365,t7602]) ).
cnf(t6512,plain,
a = multiply(a,sF1),
inference(cp,[status(thm)],[t6481,t12]) ).
cnf(t6585,plain,
multiply(a,sF1) = a,
inference(orient,[status(thm)],[t6512]) ).
cnf(t6586,plain,
multiply(sF1,add(a,X1)) = add(a,multiply(X1,sF1)),
inference(cp,[status(thm)],[t25,t6585]) ).
cnf(t7708,plain,
add(a,multiply(X1,sF1)) = multiply(sF1,add(a,X1)),
inference(orient,[status(thm)],[t6586]) ).
cnf(t8367,plain,
sF4 = multiply(sF1,add(a,b)),
inference(step,[status(thm)],[t8366,t7708]) ).
cnf(t8368,plain,
sF4 = multiply(sF1,sF0),
inference(step,[status(thm)],[t8367,t11]) ).
cnf(t93,plain,
multiply(sF1,add(sF0,X1)) = add(sF2,multiply(X1,sF1)),
inference(cp,[status(thm)],[t25,t92]) ).
cnf(t95,plain,
add(sF2,multiply(X1,sF1)) = multiply(sF1,add(sF0,X1)),
inference(orient,[status(thm)],[t93]) ).
cnf(t97,plain,
multiply(sF1,add(sF0,sF0)) = add(sF2,sF2),
inference(cp,[status(thm)],[t95,t92]) ).
cnf(t101,plain,
multiply(sF1,add(sF0,sF0)) = add(sF2,sF2),
inference(orient,[status(thm)],[t97]) ).
cnf(t3864,plain,
multiply(sF1,sF0) = add(sF2,sF2),
inference(rw,[status(thm)],[t101]) ).
cnf(t8036,plain,
multiply(sF1,sF0) = sF2,
inference(step,[status(thm)],[t3864,t3859]) ).
cnf(t4180,plain,
multiply(sF1,sF0) = sF2,
inference(orient,[status(thm)],[t8036]) ).
cnf(t8369,plain,
sF4 = sF2,
inference(step,[status(thm)],[t8368,t4180]) ).
cnf(t7800,plain,
sF4 = sF2,
inference(orient,[status(thm)],[t8369]) ).
cnf(t8370,plain,
add(a,sF3) = sF2,
inference(step,[status(thm)],[t22,t7800]) ).
cnf(t7801,plain,
add(a,sF3) = sF2,
inference(orient,[status(thm)],[t8370]) ).
cnf(goal_0,negated_conjecture,
multiply(add(a,b),add(a,c)) != add(a,multiply(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(sF0,add(a,c)) != add(a,multiply(b,c)),
inference(rw,[status(thm)],[goal_0,t11]) ).
cnf(g0_1,plain,
multiply(sF0,sF1) != add(a,multiply(b,c)),
inference(rw,[status(thm)],[g0_0,t12]) ).
cnf(g0_2,plain,
sF2 != add(a,multiply(b,c)),
inference(rw,[status(thm)],[g0_1,t92]) ).
cnf(g0_3,plain,
sF2 != add(a,sF3),
inference(rw,[status(thm)],[g0_2,t13]) ).
cnf(g0_4,plain,
sF2 != sF2,
inference(rw,[status(thm)],[g0_3,t7801]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO023-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n002.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Fri Sep 25 06:37:36 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.99/2.50 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.99/2.50 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------