%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG005-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 : n005.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:51:10 PM UTC 2026
% Result : Unsatisfiable 5.30s 1.15s
% Output : CNFRefutation 5.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 5
% Syntax : Number of clauses : 128 ( 128 unt; 0 nHn; 4 RR)
% Number of literals : 128 ( 127 equ; 3 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 : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 307 ( 63 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
difference(X1,difference(X2,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4,plain,
difference(X1,difference(X2,X1)) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t1,axiom,
difference(X1,difference(X1,X2)) = multiply(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
difference(X1,difference(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t1]) ).
cnf(t12,plain,
multiply(X1,difference(X1,X2)) = difference(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t8,t8]) ).
cnf(t34,plain,
difference(X1,multiply(X1,X2)) = multiply(X1,difference(X1,X2)),
inference(orient,[status(thm)],[t12]) ).
cnf(t11,plain,
difference(X1,X2) = difference(difference(X1,X2),multiply(X1,X2)),
inference(cp,[status(thm)],[t4,t8]) ).
cnf(t58,plain,
difference(difference(X1,X2),multiply(X1,X2)) = difference(X1,X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t5,plain,
difference(X1,X2) = difference(difference(X1,X2),X2),
inference(cp,[status(thm)],[t4,t4]) ).
cnf(t25,plain,
difference(difference(X1,X2),X2) = difference(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t26,plain,
difference(X1,difference(X1,X2)) = difference(multiply(X1,X2),difference(X1,X2)),
inference(cp,[status(thm)],[t25,t8]) ).
cnf(t3165,plain,
multiply(X1,X2) = difference(multiply(X1,X2),difference(X1,X2)),
inference(step,[status(thm)],[t26,t8]) ).
cnf(t71,plain,
difference(multiply(X1,X2),difference(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t3165]) ).
cnf(t2,axiom,
difference(X1,difference(X1,X2)) = difference(X2,difference(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t6,plain,
difference(X1,difference(X1,X2)) = difference(X2,difference(X2,X1)),
inference(orient,[status(thm)],[t2]) ).
cnf(t3160,plain,
multiply(X1,X2) = difference(X2,difference(X2,X1)),
inference(step,[status(thm)],[t6,t8]) ).
cnf(t3161,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(step,[status(thm)],[t3160,t8]) ).
cnf(t13,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(rw,[status(thm)],[t3161]) ).
cnf(t24,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t13]) ).
cnf(t72,plain,
multiply(X1,X2) = difference(multiply(X2,X1),difference(X1,X2)),
inference(cp,[status(thm)],[t71,t24]) ).
cnf(t126,plain,
difference(multiply(X1,X2),difference(X2,X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t72]) ).
cnf(t3,axiom,
difference(difference(X1,X2),difference(X3,X2)) = difference(difference(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t14,plain,
difference(difference(X1,X2),difference(X3,X2)) = difference(difference(X1,X3),X2),
inference(orient,[status(thm)],[t3]) ).
cnf(t15,plain,
difference(difference(X1,difference(X1,X2)),X2) = multiply(difference(X1,X2),X2),
inference(cp,[status(thm)],[t14,t8]) ).
cnf(t3162,plain,
difference(multiply(X1,X2),X2) = multiply(difference(X1,X2),X2),
inference(step,[status(thm)],[t15,t8]) ).
cnf(t3163,plain,
difference(multiply(X1,X2),X2) = multiply(X2,difference(X1,X2)),
inference(step,[status(thm)],[t3162,t24]) ).
cnf(t10,plain,
multiply(X1,difference(X2,X1)) = difference(X1,X1),
inference(cp,[status(thm)],[t8,t4]) ).
cnf(t30,plain,
multiply(X1,difference(X2,X1)) = difference(X1,X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t3164,plain,
difference(multiply(X1,X2),X2) = difference(X2,X2),
inference(step,[status(thm)],[t3163,t30]) ).
cnf(t41,plain,
difference(multiply(X1,X2),X2) = difference(X2,X2),
inference(orient,[status(thm)],[t3164]) ).
cnf(t43,plain,
difference(X1,X1) = difference(multiply(X1,X2),X1),
inference(cp,[status(thm)],[t41,t24]) ).
cnf(t47,plain,
difference(multiply(X1,X2),X1) = difference(X1,X1),
inference(orient,[status(thm)],[t43]) ).
cnf(t49,plain,
difference(difference(X1,multiply(X2,X3)),X2) = difference(difference(X1,X2),difference(X2,X2)),
inference(cp,[status(thm)],[t14,t47]) ).
cnf(t3168,plain,
difference(difference(X1,multiply(X2,X3)),X2) = difference(difference(X1,X2),X2),
inference(step,[status(thm)],[t49,t14]) ).
cnf(t3169,plain,
difference(difference(X1,multiply(X2,X3)),X2) = difference(X1,X2),
inference(step,[status(thm)],[t3168,t25]) ).
cnf(t98,plain,
difference(difference(X1,multiply(X2,X3)),X2) = difference(X1,X2),
inference(orient,[status(thm)],[t3169]) ).
cnf(t101,plain,
difference(multiply(X1,multiply(X2,X3)),X2) = difference(difference(multiply(X2,X3),multiply(X2,X3)),X2),
inference(cp,[status(thm)],[t98,t41]) ).
cnf(t3174,plain,
difference(multiply(X1,multiply(X2,X3)),X2) = difference(multiply(X2,X3),X2),
inference(step,[status(thm)],[t101,t98]) ).
cnf(t3175,plain,
difference(multiply(X1,multiply(X2,X3)),X2) = difference(X2,X2),
inference(step,[status(thm)],[t3174,t47]) ).
cnf(t195,plain,
difference(multiply(X1,multiply(X2,X3)),X2) = difference(X2,X2),
inference(orient,[status(thm)],[t3175]) ).
cnf(t197,plain,
difference(X1,X1) = difference(multiply(X2,difference(X1,X1)),X1),
inference(cp,[status(thm)],[t195,t30]) ).
cnf(t241,plain,
difference(multiply(X1,difference(X2,X2)),X2) = difference(X2,X2),
inference(orient,[status(thm)],[t197]) ).
cnf(t244,plain,
multiply(multiply(X1,difference(X2,X2)),X2) = difference(multiply(X2,multiply(X1,difference(X2,X2))),difference(X2,X2)),
inference(cp,[status(thm)],[t126,t241]) ).
cnf(t3178,plain,
multiply(X2,multiply(X1,difference(X2,X2))) = difference(multiply(X2,multiply(X1,difference(X2,X2))),difference(X2,X2)),
inference(step,[status(thm)],[t244,t24]) ).
cnf(t45,plain,
difference(difference(X1,multiply(X2,X3)),X3) = difference(difference(X1,X3),difference(X3,X3)),
inference(cp,[status(thm)],[t14,t41]) ).
cnf(t3166,plain,
difference(difference(X1,multiply(X2,X3)),X3) = difference(difference(X1,X3),X3),
inference(step,[status(thm)],[t45,t14]) ).
cnf(t3167,plain,
difference(difference(X1,multiply(X2,X3)),X3) = difference(X1,X3),
inference(step,[status(thm)],[t3166,t25]) ).
cnf(t86,plain,
difference(difference(X1,multiply(X2,X3)),X3) = difference(X1,X3),
inference(orient,[status(thm)],[t3167]) ).
cnf(t88,plain,
difference(multiply(X1,multiply(X2,X3)),X3) = difference(difference(multiply(X2,X3),multiply(X2,X3)),X3),
inference(cp,[status(thm)],[t86,t41]) ).
cnf(t3170,plain,
difference(multiply(X1,multiply(X2,X3)),X3) = difference(multiply(X2,X3),X3),
inference(step,[status(thm)],[t88,t86]) ).
cnf(t3171,plain,
difference(multiply(X1,multiply(X2,X3)),X3) = difference(X3,X3),
inference(step,[status(thm)],[t3170,t41]) ).
cnf(t168,plain,
difference(multiply(X1,multiply(X2,X3)),X3) = difference(X3,X3),
inference(orient,[status(thm)],[t3171]) ).
cnf(t3179,plain,
multiply(X2,multiply(X1,difference(X2,X2))) = difference(difference(X2,X2),difference(X2,X2)),
inference(step,[status(thm)],[t3178,t168]) ).
cnf(t3180,plain,
multiply(X2,multiply(X1,difference(X2,X2))) = difference(difference(X2,X2),X2),
inference(step,[status(thm)],[t3179,t14]) ).
cnf(t3181,plain,
multiply(X2,multiply(X1,difference(X2,X2))) = difference(X2,X2),
inference(step,[status(thm)],[t3180,t25]) ).
cnf(t264,plain,
multiply(X1,multiply(X2,difference(X1,X1))) = difference(X1,X1),
inference(orient,[status(thm)],[t3181]) ).
cnf(t269,plain,
difference(X1,multiply(X2,difference(X1,X1))) = difference(difference(X1,multiply(X2,difference(X1,X1))),difference(X1,X1)),
inference(cp,[status(thm)],[t58,t264]) ).
cnf(t3182,plain,
difference(X1,multiply(X2,difference(X1,X1))) = difference(X1,difference(X1,X1)),
inference(step,[status(thm)],[t269,t86]) ).
cnf(t3183,plain,
difference(X1,multiply(X2,difference(X1,X1))) = X1,
inference(step,[status(thm)],[t3182,t4]) ).
cnf(t277,plain,
difference(X1,multiply(X2,difference(X1,X1))) = X1,
inference(orient,[status(thm)],[t3183]) ).
cnf(t280,plain,
multiply(X1,difference(X2,X2)) = difference(multiply(X1,difference(X2,X2)),X2),
inference(cp,[status(thm)],[t4,t277]) ).
cnf(t3184,plain,
multiply(X1,difference(X2,X2)) = difference(X2,X2),
inference(step,[status(thm)],[t280,t241]) ).
cnf(t284,plain,
multiply(X1,difference(X2,X2)) = difference(X2,X2),
inference(orient,[status(thm)],[t3184]) ).
cnf(t285,plain,
difference(X1,X1) = multiply(difference(X1,X1),X2),
inference(cp,[status(thm)],[t284,t24]) ).
cnf(t297,plain,
multiply(difference(X1,X1),X2) = difference(X1,X1),
inference(orient,[status(thm)],[t285]) ).
cnf(t298,plain,
difference(X1,X1) = difference(X2,X2),
inference(cp,[status(thm)],[t297,t284]) ).
cnf(t308,plain,
difference(X1,X1) = difference(X2,X2),
inference(orient,[status(thm)],[t298]) ).
cnf(t310,plain,
X1 = difference(X1,difference(X2,X2)),
inference(cp,[status(thm)],[t4,t308]) ).
cnf(t327,plain,
difference(X1,difference(X2,X2)) = X1,
inference(orient,[status(thm)],[t310]) ).
cnf(t330,plain,
difference(X1,X1) = difference(difference(X1,X1),X2),
inference(cp,[status(thm)],[t4,t327]) ).
cnf(t334,plain,
difference(difference(X1,X1),X2) = difference(X1,X1),
inference(orient,[status(thm)],[t330]) ).
cnf(t335,plain,
difference(X1,X1) = difference(difference(X1,X2),X1),
inference(cp,[status(thm)],[t334,t14]) ).
cnf(t341,plain,
difference(difference(X1,X2),X1) = difference(X1,X1),
inference(orient,[status(thm)],[t335]) ).
cnf(t356,plain,
multiply(difference(X1,X2),X1) = difference(difference(X1,X2),difference(X1,X1)),
inference(cp,[status(thm)],[t8,t341]) ).
cnf(t3185,plain,
multiply(X1,difference(X1,X2)) = difference(difference(X1,X2),difference(X1,X1)),
inference(step,[status(thm)],[t356,t24]) ).
cnf(t3186,plain,
multiply(X1,difference(X1,X2)) = difference(X1,X2),
inference(step,[status(thm)],[t3185,t327]) ).
cnf(t359,plain,
multiply(X1,difference(X1,X2)) = difference(X1,X2),
inference(orient,[status(thm)],[t3186]) ).
cnf(t3187,plain,
difference(X1,multiply(X1,X2)) = difference(X1,X2),
inference(step,[status(thm)],[t34,t359]) ).
cnf(t360,plain,
difference(X1,multiply(X1,X2)) = difference(X1,X2),
inference(orient,[status(thm)],[t3187]) ).
cnf(t347,plain,
difference(difference(X1,multiply(X2,X3)),difference(X1,multiply(X2,X3))) = difference(difference(X1,X3),difference(X1,multiply(X2,X3))),
inference(cp,[status(thm)],[t341,t86]) ).
cnf(t3244,plain,
difference(difference(X1,X1),multiply(X2,X3)) = difference(difference(X1,X3),difference(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t347,t14]) ).
cnf(t3245,plain,
difference(X1,X1) = difference(difference(X1,X3),difference(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t3244,t334]) ).
cnf(t2254,plain,
difference(difference(X1,X2),difference(X1,multiply(X3,X2))) = difference(X1,X1),
inference(orient,[status(thm)],[t3245]) ).
cnf(t2259,plain,
difference(X1,X1) = difference(X1,difference(X1,multiply(X2,difference(X3,X1)))),
inference(cp,[status(thm)],[t2254,t4]) ).
cnf(t3246,plain,
difference(X1,X1) = multiply(X1,multiply(X2,difference(X3,X1))),
inference(step,[status(thm)],[t2259,t8]) ).
cnf(t2349,plain,
multiply(X1,multiply(X2,difference(X3,X1))) = difference(X1,X1),
inference(orient,[status(thm)],[t3246]) ).
cnf(t2379,plain,
difference(X1,multiply(X2,difference(X3,X1))) = difference(X1,difference(X1,X1)),
inference(cp,[status(thm)],[t360,t2349]) ).
cnf(t3267,plain,
difference(X1,multiply(X2,difference(X3,X1))) = X1,
inference(step,[status(thm)],[t2379,t327]) ).
cnf(t2454,plain,
difference(X1,multiply(X2,difference(X3,X1))) = X1,
inference(orient,[status(thm)],[t3267]) ).
cnf(t2456,plain,
X1 = difference(X1,multiply(difference(X2,X1),X3)),
inference(cp,[status(thm)],[t2454,t24]) ).
cnf(t2475,plain,
difference(X1,multiply(difference(X2,X1),X3)) = X1,
inference(orient,[status(thm)],[t2456]) ).
cnf(t2493,plain,
multiply(difference(X1,X2),X3) = difference(multiply(difference(X1,X2),X3),X2),
inference(cp,[status(thm)],[t4,t2475]) ).
cnf(t22,plain,
multiply(difference(X1,X2),difference(X3,X2)) = difference(difference(X1,X2),difference(difference(X1,X3),X2)),
inference(cp,[status(thm)],[t8,t14]) ).
cnf(t3203,plain,
multiply(difference(X1,X2),difference(X3,X2)) = difference(difference(X1,difference(X1,X3)),X2),
inference(step,[status(thm)],[t22,t14]) ).
cnf(t3204,plain,
multiply(difference(X1,X2),difference(X3,X2)) = difference(multiply(X1,X3),X2),
inference(step,[status(thm)],[t3203,t8]) ).
cnf(t635,plain,
multiply(difference(X1,X2),difference(X3,X2)) = difference(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t3204]) ).
cnf(t657,plain,
difference(multiply(difference(X1,X2),X3),X2) = multiply(difference(X1,X2),difference(X3,X2)),
inference(cp,[status(thm)],[t635,t25]) ).
cnf(t3219,plain,
difference(multiply(difference(X1,X2),X3),X2) = difference(multiply(X1,X3),X2),
inference(step,[status(thm)],[t657,t635]) ).
cnf(t1027,plain,
difference(multiply(difference(X1,X2),X3),X2) = difference(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t3219]) ).
cnf(t3268,plain,
multiply(difference(X1,X2),X3) = difference(multiply(X1,X3),X2),
inference(step,[status(thm)],[t2493,t1027]) ).
cnf(t35,plain,
multiply(X1,difference(X1,X2)) = difference(X1,multiply(X2,X1)),
inference(cp,[status(thm)],[t34,t24]) ).
cnf(t51,plain,
difference(X1,multiply(X2,X1)) = multiply(X1,difference(X1,X2)),
inference(orient,[status(thm)],[t35]) ).
cnf(t3189,plain,
difference(X1,multiply(X2,X1)) = difference(X1,X2),
inference(step,[status(thm)],[t51,t359]) ).
cnf(t362,plain,
difference(X1,multiply(X2,X1)) = difference(X1,X2),
inference(orient,[status(thm)],[t3189]) ).
cnf(t2377,plain,
difference(multiply(X1,difference(X2,X3)),X3) = difference(multiply(X1,difference(X2,X3)),difference(X3,X3)),
inference(cp,[status(thm)],[t362,t2349]) ).
cnf(t682,plain,
difference(multiply(X1,difference(X2,X3)),X3) = multiply(difference(X1,X3),difference(X2,X3)),
inference(cp,[status(thm)],[t635,t25]) ).
cnf(t3220,plain,
difference(multiply(X1,difference(X2,X3)),X3) = difference(multiply(X1,X2),X3),
inference(step,[status(thm)],[t682,t635]) ).
cnf(t1087,plain,
difference(multiply(X1,difference(X2,X3)),X3) = difference(multiply(X1,X2),X3),
inference(orient,[status(thm)],[t3220]) ).
cnf(t3247,plain,
difference(multiply(X1,X2),X3) = difference(multiply(X1,difference(X2,X3)),difference(X3,X3)),
inference(step,[status(thm)],[t2377,t1087]) ).
cnf(t3248,plain,
difference(multiply(X1,X2),X3) = multiply(X1,difference(X2,X3)),
inference(step,[status(thm)],[t3247,t327]) ).
cnf(t2399,plain,
difference(multiply(X1,X2),X3) = multiply(X1,difference(X2,X3)),
inference(orient,[status(thm)],[t3248]) ).
cnf(t3269,plain,
multiply(difference(X1,X2),X3) = multiply(X1,difference(X3,X2)),
inference(step,[status(thm)],[t3268,t2399]) ).
cnf(t2508,plain,
multiply(difference(X1,X2),X3) = multiply(X1,difference(X3,X2)),
inference(orient,[status(thm)],[t3269]) ).
cnf(t2520,plain,
multiply(X1,difference(X2,multiply(X1,X3))) = multiply(difference(X1,X3),X2),
inference(cp,[status(thm)],[t2508,t360]) ).
cnf(t3279,plain,
multiply(X1,difference(X2,multiply(X1,X3))) = multiply(X1,difference(X2,X3)),
inference(step,[status(thm)],[t2520,t2508]) ).
cnf(t2885,plain,
multiply(X1,difference(X2,multiply(X1,X3))) = multiply(X1,difference(X2,X3)),
inference(orient,[status(thm)],[t3279]) ).
cnf(t2549,plain,
difference(X1,difference(X2,X3)) = difference(X1,multiply(X2,difference(X1,X3))),
inference(cp,[status(thm)],[t362,t2508]) ).
cnf(t3049,plain,
difference(X1,multiply(X2,difference(X1,X3))) = difference(X1,difference(X2,X3)),
inference(orient,[status(thm)],[t2549]) ).
cnf(t3094,plain,
multiply(X1,difference(X2,difference(X2,X3))) = multiply(X1,difference(X2,difference(X1,X3))),
inference(cp,[status(thm)],[t2885,t3049]) ).
cnf(t3281,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,difference(X2,difference(X1,X3))),
inference(step,[status(thm)],[t3094,t8]) ).
cnf(t2524,plain,
multiply(X1,difference(X2,difference(X1,X3))) = multiply(multiply(X1,X3),X2),
inference(cp,[status(thm)],[t2508,t8]) ).
cnf(t2975,plain,
multiply(X1,difference(X2,difference(X1,X3))) = multiply(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t2524]) ).
cnf(t3282,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X3),X2),
inference(step,[status(thm)],[t3281,t2975]) ).
cnf(t3107,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t3282]) ).
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(a,multiply(c,b)) != multiply(a,multiply(b,c)),
inference(rw,[status(thm)],[goal_0,t3107]) ).
cnf(g0_1,plain,
multiply(a,multiply(c,b)) != multiply(a,multiply(c,b)),
inference(rw,[status(thm)],[g0_0,t24]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG005-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.16/0.41 % Computer : n005.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Fri Sep 25 04:30:02 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.30/1.15 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.30/1.15 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------