%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO022-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 12:59:39 PM UTC 2026
% Result : Unsatisfiable 6.64s 6.53s
% Output : CNFRefutation 6.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 9
% Syntax : Number of clauses : 151 ( 151 unt; 0 nHn; 103 RR)
% Number of literals : 151 ( 150 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 74 ( 20 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
add(multiply(X1,X2),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
add(multiply(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t3,axiom,
multiply(add(X1,X2),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
multiply(add(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t12,plain,
X1 = add(X1,X1),
inference(cp,[status(thm)],[t11,t10]) ).
cnf(t51,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t4,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t14,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
inference(orient,[status(thm)],[t4]) ).
cnf(t52,plain,
multiply(X1,X2) = multiply(X2,add(X1,X1)),
inference(cp,[status(thm)],[t51,t14]) ).
cnf(t2953,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(step,[status(thm)],[t52,t51]) ).
cnf(t382,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t2953]) ).
cnf(t6,axiom,
sFlat0 = multiply(a,b),
introduced(definition) ).
cnf(t42,plain,
multiply(a,b) = sFlat0,
inference(orient,[status(thm)],[t6]) ).
cnf(t399,plain,
multiply(a,b) = sFlat0,
inference(rw,[status(thm)],[t42]) ).
cnf(t2955,plain,
multiply(b,a) = sFlat0,
inference(step,[status(thm)],[t399,t382]) ).
cnf(t408,plain,
multiply(b,a) = sFlat0,
inference(orient,[status(thm)],[t2955]) ).
cnf(t7,axiom,
sFlat1 = multiply(multiply(a,b),c),
introduced(definition) ).
cnf(t22,plain,
multiply(multiply(a,b),c) = sFlat1,
inference(orient,[status(thm)],[t7]) ).
cnf(t2928,plain,
multiply(sFlat0,c) = sFlat1,
inference(step,[status(thm)],[t22,t42]) ).
cnf(t46,plain,
multiply(sFlat0,c) = sFlat1,
inference(rw,[status(thm)],[t2928]) ).
cnf(t69,plain,
multiply(sFlat0,c) = sFlat1,
inference(orient,[status(thm)],[t46]) ).
cnf(t8,axiom,
sFlat2 = multiply(b,c),
introduced(definition) ).
cnf(t34,plain,
multiply(b,c) = sFlat2,
inference(orient,[status(thm)],[t8]) ).
cnf(t392,plain,
multiply(b,c) = sFlat2,
inference(rw,[status(thm)],[t34]) ).
cnf(t2954,plain,
multiply(c,b) = sFlat2,
inference(step,[status(thm)],[t392,t382]) ).
cnf(t403,plain,
multiply(c,b) = sFlat2,
inference(orient,[status(thm)],[t2954]) ).
cnf(t9,axiom,
sFlat3 = multiply(a,multiply(b,c)),
introduced(definition) ).
cnf(t2927,plain,
sFlat3 = multiply(a,sFlat2),
inference(step,[status(thm)],[t9,t34]) ).
cnf(t38,plain,
multiply(a,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t2927]) ).
cnf(t400,plain,
multiply(a,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t38]) ).
cnf(t2956,plain,
multiply(sFlat2,a) = sFlat3,
inference(step,[status(thm)],[t400,t382]) ).
cnf(t413,plain,
multiply(sFlat2,a) = sFlat3,
inference(orient,[status(thm)],[t2956]) ).
cnf(t415,plain,
multiply(a,add(sFlat2,X1)) = add(sFlat3,multiply(X1,a)),
inference(cp,[status(thm)],[t14,t413]) ).
cnf(t2892,plain,
add(sFlat3,multiply(X1,a)) = multiply(a,add(sFlat2,X1)),
inference(orient,[status(thm)],[t415]) ).
cnf(t13,plain,
X1 = multiply(X1,X1),
inference(cp,[status(thm)],[t10,t11]) ).
cnf(t56,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t59,plain,
multiply(X1,add(X2,X1)) = add(multiply(X2,X1),X1),
inference(cp,[status(thm)],[t14,t56]) ).
cnf(t2932,plain,
multiply(X1,add(X2,X1)) = X1,
inference(step,[status(thm)],[t59,t11]) ).
cnf(t149,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t2932]) ).
cnf(t5,axiom,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t26,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t412,plain,
a = add(sFlat0,a),
inference(cp,[status(thm)],[t11,t408]) ).
cnf(t434,plain,
add(sFlat0,a) = a,
inference(orient,[status(thm)],[t412]) ).
cnf(t436,plain,
add(a,multiply(sFlat0,X1)) = multiply(a,add(X1,a)),
inference(cp,[status(thm)],[t26,t434]) ).
cnf(t2961,plain,
add(a,multiply(sFlat0,X1)) = a,
inference(step,[status(thm)],[t436,t149]) ).
cnf(t614,plain,
add(a,multiply(sFlat0,X1)) = a,
inference(orient,[status(thm)],[t2961]) ).
cnf(t55,plain,
add(X1,multiply(X2,X1)) = multiply(add(X2,X1),X1),
inference(cp,[status(thm)],[t26,t51]) ).
cnf(t2931,plain,
add(X1,multiply(X2,X1)) = X1,
inference(step,[status(thm)],[t55,t10]) ).
cnf(t104,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t2931]) ).
cnf(t388,plain,
X1 = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t104,t382]) ).
cnf(t543,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t388]) ).
cnf(t548,plain,
sFlat0 = add(sFlat0,sFlat1),
inference(cp,[status(thm)],[t543,t69]) ).
cnf(t564,plain,
add(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t548]) ).
cnf(t565,plain,
sFlat1 = multiply(sFlat1,sFlat0),
inference(cp,[status(thm)],[t149,t564]) ).
cnf(t2958,plain,
sFlat1 = multiply(sFlat0,sFlat1),
inference(step,[status(thm)],[t565,t382]) ).
cnf(t578,plain,
multiply(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t2958]) ).
cnf(t615,plain,
a = add(a,sFlat1),
inference(cp,[status(thm)],[t614,t578]) ).
cnf(t622,plain,
add(a,sFlat1) = a,
inference(orient,[status(thm)],[t615]) ).
cnf(t623,plain,
sFlat1 = multiply(sFlat1,a),
inference(cp,[status(thm)],[t149,t622]) ).
cnf(t627,plain,
multiply(sFlat1,a) = sFlat1,
inference(orient,[status(thm)],[t623]) ).
cnf(t2898,plain,
multiply(a,add(sFlat2,sFlat1)) = add(sFlat3,sFlat1),
inference(cp,[status(thm)],[t2892,t627]) ).
cnf(t57,plain,
add(X1,X2) = add(X2,multiply(X1,X1)),
inference(cp,[status(thm)],[t56,t26]) ).
cnf(t2968,plain,
add(X1,X2) = add(X2,X1),
inference(step,[status(thm)],[t57,t56]) ).
cnf(t741,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t2968]) ).
cnf(t3107,plain,
multiply(a,add(sFlat1,sFlat2)) = add(sFlat3,sFlat1),
inference(step,[status(thm)],[t2898,t741]) ).
cnf(t405,plain,
multiply(b,add(c,X1)) = add(sFlat2,multiply(X1,b)),
inference(cp,[status(thm)],[t14,t403]) ).
cnf(t2457,plain,
add(sFlat2,multiply(X1,b)) = multiply(b,add(c,X1)),
inference(orient,[status(thm)],[t405]) ).
cnf(t45,plain,
b = add(sFlat0,b),
inference(cp,[status(thm)],[t11,t42]) ).
cnf(t66,plain,
add(sFlat0,b) = b,
inference(orient,[status(thm)],[t45]) ).
cnf(t68,plain,
add(b,multiply(X1,sFlat0)) = multiply(add(X1,b),b),
inference(cp,[status(thm)],[t26,t66]) ).
cnf(t2936,plain,
add(b,multiply(X1,sFlat0)) = b,
inference(step,[status(thm)],[t68,t10]) ).
cnf(t260,plain,
add(b,multiply(X1,sFlat0)) = b,
inference(orient,[status(thm)],[t2936]) ).
cnf(t385,plain,
b = add(b,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t260,t382]) ).
cnf(t473,plain,
add(b,multiply(sFlat0,X1)) = b,
inference(orient,[status(thm)],[t385]) ).
cnf(t474,plain,
b = add(b,sFlat1),
inference(cp,[status(thm)],[t473,t69]) ).
cnf(t480,plain,
add(b,sFlat1) = b,
inference(orient,[status(thm)],[t474]) ).
cnf(t481,plain,
sFlat1 = multiply(sFlat1,b),
inference(cp,[status(thm)],[t149,t480]) ).
cnf(t490,plain,
multiply(sFlat1,b) = sFlat1,
inference(orient,[status(thm)],[t481]) ).
cnf(t2463,plain,
multiply(b,add(c,sFlat1)) = add(sFlat2,sFlat1),
inference(cp,[status(thm)],[t2457,t490]) ).
cnf(t3068,plain,
multiply(b,add(sFlat1,c)) = add(sFlat2,sFlat1),
inference(step,[status(thm)],[t2463,t741]) ).
cnf(t72,plain,
c = add(sFlat1,c),
inference(cp,[status(thm)],[t11,t69]) ).
cnf(t73,plain,
add(sFlat1,c) = c,
inference(orient,[status(thm)],[t72]) ).
cnf(t3069,plain,
multiply(b,c) = add(sFlat2,sFlat1),
inference(step,[status(thm)],[t3068,t73]) ).
cnf(t3070,plain,
multiply(c,b) = add(sFlat2,sFlat1),
inference(step,[status(thm)],[t3069,t382]) ).
cnf(t3071,plain,
sFlat2 = add(sFlat2,sFlat1),
inference(step,[status(thm)],[t3070,t403]) ).
cnf(t3072,plain,
sFlat2 = add(sFlat1,sFlat2),
inference(step,[status(thm)],[t3071,t741]) ).
cnf(t2479,plain,
add(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t3072]) ).
cnf(t3108,plain,
multiply(a,sFlat2) = add(sFlat3,sFlat1),
inference(step,[status(thm)],[t3107,t2479]) ).
cnf(t3109,plain,
multiply(sFlat2,a) = add(sFlat3,sFlat1),
inference(step,[status(thm)],[t3108,t382]) ).
cnf(t3110,plain,
sFlat3 = add(sFlat3,sFlat1),
inference(step,[status(thm)],[t3109,t413]) ).
cnf(t3111,plain,
sFlat3 = add(sFlat1,sFlat3),
inference(step,[status(thm)],[t3110,t741]) ).
cnf(t70,plain,
multiply(c,add(sFlat0,X1)) = add(sFlat1,multiply(X1,c)),
inference(cp,[status(thm)],[t14,t69]) ).
cnf(t1889,plain,
add(sFlat1,multiply(X1,c)) = multiply(c,add(sFlat0,X1)),
inference(orient,[status(thm)],[t70]) ).
cnf(t37,plain,
c = add(sFlat2,c),
inference(cp,[status(thm)],[t11,t34]) ).
cnf(t60,plain,
add(sFlat2,c) = c,
inference(orient,[status(thm)],[t37]) ).
cnf(t62,plain,
add(c,multiply(X1,sFlat2)) = multiply(add(X1,c),c),
inference(cp,[status(thm)],[t26,t60]) ).
cnf(t2933,plain,
add(c,multiply(X1,sFlat2)) = c,
inference(step,[status(thm)],[t62,t10]) ).
cnf(t188,plain,
add(c,multiply(X1,sFlat2)) = c,
inference(orient,[status(thm)],[t2933]) ).
cnf(t107,plain,
sFlat2 = add(sFlat2,sFlat3),
inference(cp,[status(thm)],[t104,t38]) ).
cnf(t118,plain,
add(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t107]) ).
cnf(t156,plain,
sFlat3 = multiply(sFlat3,sFlat2),
inference(cp,[status(thm)],[t149,t118]) ).
cnf(t171,plain,
multiply(sFlat3,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t156]) ).
cnf(t189,plain,
c = add(c,sFlat3),
inference(cp,[status(thm)],[t188,t171]) ).
cnf(t195,plain,
add(c,sFlat3) = c,
inference(orient,[status(thm)],[t189]) ).
cnf(t197,plain,
sFlat3 = multiply(sFlat3,c),
inference(cp,[status(thm)],[t149,t195]) ).
cnf(t203,plain,
multiply(sFlat3,c) = sFlat3,
inference(orient,[status(thm)],[t197]) ).
cnf(t1892,plain,
multiply(c,add(sFlat0,sFlat3)) = add(sFlat1,sFlat3),
inference(cp,[status(thm)],[t1889,t203]) ).
cnf(t1906,plain,
multiply(c,add(sFlat0,sFlat3)) = add(sFlat1,sFlat3),
inference(orient,[status(thm)],[t1892]) ).
cnf(t410,plain,
multiply(a,add(b,X1)) = add(sFlat0,multiply(X1,a)),
inference(cp,[status(thm)],[t14,t408]) ).
cnf(t2659,plain,
add(sFlat0,multiply(X1,a)) = multiply(a,add(b,X1)),
inference(orient,[status(thm)],[t410]) ).
cnf(t414,plain,
a = add(a,sFlat3),
inference(cp,[status(thm)],[t104,t413]) ).
cnf(t438,plain,
add(a,sFlat3) = a,
inference(orient,[status(thm)],[t414]) ).
cnf(t439,plain,
sFlat3 = multiply(sFlat3,a),
inference(cp,[status(thm)],[t149,t438]) ).
cnf(t458,plain,
multiply(sFlat3,a) = sFlat3,
inference(orient,[status(thm)],[t439]) ).
cnf(t2664,plain,
multiply(a,add(b,sFlat3)) = add(sFlat0,sFlat3),
inference(cp,[status(thm)],[t2659,t458]) ).
cnf(t3084,plain,
multiply(a,add(sFlat3,b)) = add(sFlat0,sFlat3),
inference(step,[status(thm)],[t2664,t741]) ).
cnf(t119,plain,
sFlat3 = multiply(sFlat2,sFlat3),
inference(cp,[status(thm)],[t10,t118]) ).
cnf(t133,plain,
multiply(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t119]) ).
cnf(t135,plain,
multiply(sFlat3,add(X1,sFlat2)) = add(multiply(X1,sFlat3),sFlat3),
inference(cp,[status(thm)],[t14,t133]) ).
cnf(t2941,plain,
multiply(sFlat3,add(X1,sFlat2)) = sFlat3,
inference(step,[status(thm)],[t135,t11]) ).
cnf(t287,plain,
multiply(sFlat3,add(X1,sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t2941]) ).
cnf(t404,plain,
b = add(b,sFlat2),
inference(cp,[status(thm)],[t104,t403]) ).
cnf(t418,plain,
add(b,sFlat2) = b,
inference(orient,[status(thm)],[t404]) ).
cnf(t419,plain,
sFlat3 = multiply(sFlat3,b),
inference(cp,[status(thm)],[t287,t418]) ).
cnf(t447,plain,
multiply(sFlat3,b) = sFlat3,
inference(orient,[status(thm)],[t419]) ).
cnf(t451,plain,
b = add(sFlat3,b),
inference(cp,[status(thm)],[t11,t447]) ).
cnf(t465,plain,
add(sFlat3,b) = b,
inference(orient,[status(thm)],[t451]) ).
cnf(t3085,plain,
multiply(a,b) = add(sFlat0,sFlat3),
inference(step,[status(thm)],[t3084,t465]) ).
cnf(t3086,plain,
multiply(b,a) = add(sFlat0,sFlat3),
inference(step,[status(thm)],[t3085,t382]) ).
cnf(t3087,plain,
sFlat0 = add(sFlat0,sFlat3),
inference(step,[status(thm)],[t3086,t408]) ).
cnf(t2681,plain,
add(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t3087]) ).
cnf(t3091,plain,
multiply(c,sFlat0) = add(sFlat1,sFlat3),
inference(step,[status(thm)],[t1906,t2681]) ).
cnf(t2694,plain,
multiply(c,sFlat0) = add(sFlat1,sFlat3),
inference(rw,[status(thm)],[t3091]) ).
cnf(t3093,plain,
multiply(sFlat0,c) = add(sFlat1,sFlat3),
inference(step,[status(thm)],[t2694,t382]) ).
cnf(t3094,plain,
sFlat1 = add(sFlat1,sFlat3),
inference(step,[status(thm)],[t3093,t69]) ).
cnf(t2710,plain,
add(sFlat1,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t3094]) ).
cnf(t3112,plain,
sFlat3 = sFlat1,
inference(step,[status(thm)],[t3111,t2710]) ).
cnf(t2912,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t3112]) ).
cnf(t3113,plain,
multiply(sFlat2,a) = sFlat1,
inference(step,[status(thm)],[t413,t2912]) ).
cnf(t2913,plain,
multiply(sFlat2,a) = sFlat1,
inference(orient,[status(thm)],[t3113]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a,b),c) != multiply(a,multiply(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(c,multiply(a,b)) != multiply(a,multiply(b,c)),
inference(rw,[status(thm)],[goal_0,t382]) ).
cnf(g0_1,plain,
multiply(c,multiply(b,a)) != multiply(a,multiply(b,c)),
inference(rw,[status(thm)],[g0_0,t382]) ).
cnf(g0_2,plain,
multiply(c,sFlat0) != multiply(a,multiply(b,c)),
inference(rw,[status(thm)],[g0_1,t408]) ).
cnf(g0_3,plain,
multiply(sFlat0,c) != multiply(a,multiply(b,c)),
inference(rw,[status(thm)],[g0_2,t382]) ).
cnf(g0_4,plain,
sFlat1 != multiply(a,multiply(b,c)),
inference(rw,[status(thm)],[g0_3,t69]) ).
cnf(g0_5,plain,
sFlat1 != multiply(a,multiply(c,b)),
inference(rw,[status(thm)],[g0_4,t382]) ).
cnf(g0_6,plain,
sFlat1 != multiply(a,sFlat2),
inference(rw,[status(thm)],[g0_5,t403]) ).
cnf(g0_7,plain,
sFlat1 != multiply(sFlat2,a),
inference(rw,[status(thm)],[g0_6,t382]) ).
cnf(g0_8,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_7,t2913]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO022-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.36 % Computer : n018.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Fri Sep 25 06:37:10 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.64/6.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.64/6.53 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------