%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP480-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:27:09 PM UTC 2026
% Result : Unsatisfiable 7.13s 6.74s
% Output : CNFRefutation 7.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 3
% Syntax : Number of clauses : 123 ( 123 unt; 0 nHn; 3 RR)
% Number of literals : 123 ( 122 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 477 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
divide(inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,X4)))),X4) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2,plain,
divide(inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,X4)))),X4) = X3,
inference(orient,[status(thm)],[t1]) ).
cnf(t3,plain,
inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,divide(X4,Y4))))) = divide(inverse(divide(divide(divide(Y5,Y5),X4),X3)),Y4),
inference(cp,[status(thm)],[t2,t2]) ).
cnf(t489,plain,
inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,divide(X4,Y4))))) = divide(inverse(divide(divide(divide(Y5,Y5),X4),X3)),Y4),
inference(orient,[status(thm)],[t3]) ).
cnf(t521,plain,
X1 = divide(divide(inverse(divide(divide(divide(X2,X2),X3),X1)),X4),divide(X3,X4)),
inference(cp,[status(thm)],[t2,t489]) ).
cnf(t606,plain,
divide(divide(inverse(divide(divide(divide(X1,X1),X2),X3)),X4),divide(X2,X4)) = X3,
inference(orient,[status(thm)],[t521]) ).
cnf(t0,axiom,
divide(X1,inverse(X2)) = multiply(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
divide(X1,inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t0]) ).
cnf(t607,plain,
X1 = divide(multiply(inverse(divide(divide(divide(X2,X2),X3),X1)),X4),divide(X3,inverse(X4))),
inference(cp,[status(thm)],[t606,t5]) ).
cnf(t8760,plain,
X1 = divide(multiply(inverse(divide(divide(divide(X2,X2),X3),X1)),X4),multiply(X3,X4)),
inference(step,[status(thm)],[t607,t5]) ).
cnf(t661,plain,
divide(multiply(inverse(divide(divide(divide(X1,X1),X2),X3)),X4),multiply(X2,X4)) = X3,
inference(orient,[status(thm)],[t8760]) ).
cnf(t665,plain,
X1 = divide(multiply(inverse(divide(multiply(divide(X2,X2),X3),X1)),X4),multiply(inverse(X3),X4)),
inference(cp,[status(thm)],[t661,t5]) ).
cnf(t931,plain,
divide(multiply(inverse(divide(multiply(divide(X1,X1),X2),X3)),X4),multiply(inverse(X2),X4)) = X3,
inference(orient,[status(thm)],[t665]) ).
cnf(t629,plain,
X1 = divide(divide(inverse(divide(X2,X1)),X3),divide(divide(X4,inverse(divide(divide(divide(Y4,Y4),X4),X2))),X3)),
inference(cp,[status(thm)],[t606,t606]) ).
cnf(t8782,plain,
X1 = divide(divide(inverse(divide(X2,X1)),X3),divide(multiply(X4,divide(divide(divide(Y4,Y4),X4),X2)),X3)),
inference(step,[status(thm)],[t629,t5]) ).
cnf(t2580,plain,
divide(divide(inverse(divide(X1,X2)),X3),divide(multiply(X4,divide(divide(divide(Y4,Y4),X4),X1)),X3)) = X2,
inference(orient,[status(thm)],[t8782]) ).
cnf(t2670,plain,
divide(inverse(divide(divide(divide(X1,X1),multiply(X2,divide(divide(divide(X3,X3),X2),X4))),Y4)),Y5) = inverse(divide(divide(divide(Y6,Y6),divide(inverse(divide(X4,Y7)),Y5)),divide(Y4,Y7))),
inference(cp,[status(thm)],[t489,t2580]) ).
cnf(t657,plain,
divide(inverse(divide(divide(divide(X1,X1),X2),divide(inverse(divide(divide(divide(X3,X3),X4),Y4)),divide(X2,Y5)))),Y5) = inverse(divide(divide(divide(Y6,Y6),X4),Y4)),
inference(cp,[status(thm)],[t489,t606]) ).
cnf(t8761,plain,
inverse(divide(divide(divide(X3,X3),X4),Y4)) = inverse(divide(divide(divide(Y6,Y6),X4),Y4)),
inference(step,[status(thm)],[t657,t2]) ).
cnf(t1252,plain,
inverse(divide(divide(divide(X1,X1),X2),X3)) = inverse(divide(divide(divide(X4,X4),X2),X3)),
inference(orient,[status(thm)],[t8761]) ).
cnf(t1255,plain,
inverse(divide(divide(divide(X1,X1),divide(X2,inverse(divide(divide(divide(X3,X3),X2),X4)))),Y4)) = inverse(divide(X4,Y4)),
inference(cp,[status(thm)],[t1252,t606]) ).
cnf(t8772,plain,
inverse(divide(divide(divide(X1,X1),multiply(X2,divide(divide(divide(X3,X3),X2),X4))),Y4)) = inverse(divide(X4,Y4)),
inference(step,[status(thm)],[t1255,t5]) ).
cnf(t1952,plain,
inverse(divide(divide(divide(X1,X1),multiply(X2,divide(divide(divide(X3,X3),X2),X4))),Y4)) = inverse(divide(X4,Y4)),
inference(orient,[status(thm)],[t8772]) ).
cnf(t8783,plain,
divide(inverse(divide(X4,Y4)),Y5) = inverse(divide(divide(divide(Y6,Y6),divide(inverse(divide(X4,Y7)),Y5)),divide(Y4,Y7))),
inference(step,[status(thm)],[t2670,t1952]) ).
cnf(t2675,plain,
inverse(divide(divide(divide(X1,X1),divide(inverse(divide(X2,X3)),X4)),divide(Y4,X3))) = divide(inverse(divide(X2,Y4)),X4),
inference(orient,[status(thm)],[t8783]) ).
cnf(t2690,plain,
divide(inverse(divide(X1,X2)),inverse(X3)) = inverse(divide(divide(divide(X4,X4),multiply(inverse(divide(X1,Y4)),X3)),divide(X2,Y4))),
inference(cp,[status(thm)],[t2675,t5]) ).
cnf(t8789,plain,
multiply(inverse(divide(X1,X2)),X3) = inverse(divide(divide(divide(X4,X4),multiply(inverse(divide(X1,Y4)),X3)),divide(X2,Y4))),
inference(step,[status(thm)],[t2690,t5]) ).
cnf(t3335,plain,
inverse(divide(divide(divide(X1,X1),multiply(inverse(divide(X2,X3)),X4)),divide(Y4,X3))) = multiply(inverse(divide(X2,Y4)),X4),
inference(orient,[status(thm)],[t8789]) ).
cnf(t2677,plain,
divide(inverse(divide(X1,X2)),inverse(divide(divide(divide(X3,X3),inverse(divide(X1,X4))),Y4))) = inverse(divide(Y4,divide(X2,X4))),
inference(cp,[status(thm)],[t2675,t606]) ).
cnf(t8784,plain,
multiply(inverse(divide(X1,X2)),divide(divide(divide(X3,X3),inverse(divide(X1,X4))),Y4)) = inverse(divide(Y4,divide(X2,X4))),
inference(step,[status(thm)],[t2677,t5]) ).
cnf(t8785,plain,
multiply(inverse(divide(X1,X2)),divide(multiply(divide(X3,X3),divide(X1,X4)),Y4)) = inverse(divide(Y4,divide(X2,X4))),
inference(step,[status(thm)],[t8784,t5]) ).
cnf(t2759,plain,
multiply(inverse(divide(X1,X2)),divide(multiply(divide(X3,X3),divide(X1,X4)),Y4)) = inverse(divide(Y4,divide(X2,X4))),
inference(orient,[status(thm)],[t8785]) ).
cnf(t3341,plain,
multiply(inverse(divide(X1,X2)),divide(multiply(divide(X3,X3),divide(X1,X4)),Y4)) = inverse(divide(divide(divide(Y5,Y5),inverse(divide(Y4,divide(Y6,X4)))),divide(X2,Y6))),
inference(cp,[status(thm)],[t3335,t2759]) ).
cnf(t8790,plain,
inverse(divide(Y4,divide(X2,X4))) = inverse(divide(divide(divide(Y5,Y5),inverse(divide(Y4,divide(Y6,X4)))),divide(X2,Y6))),
inference(step,[status(thm)],[t3341,t2759]) ).
cnf(t8791,plain,
inverse(divide(Y4,divide(X2,X4))) = inverse(divide(multiply(divide(Y5,Y5),divide(Y4,divide(Y6,X4))),divide(X2,Y6))),
inference(step,[status(thm)],[t8790,t5]) ).
cnf(t3428,plain,
inverse(divide(multiply(divide(X1,X1),divide(X2,divide(X3,X4))),divide(Y4,X3))) = inverse(divide(X2,divide(Y4,X4))),
inference(orient,[status(thm)],[t8791]) ).
cnf(t3485,plain,
divide(X1,X2) = divide(multiply(inverse(divide(X3,divide(X1,X4))),Y4),multiply(inverse(divide(X3,divide(X2,X4))),Y4)),
inference(cp,[status(thm)],[t931,t3428]) ).
cnf(t5377,plain,
divide(multiply(inverse(divide(X1,divide(X2,X3))),X4),multiply(inverse(divide(X1,divide(Y4,X3))),X4)) = divide(X2,Y4),
inference(orient,[status(thm)],[t3485]) ).
cnf(t2798,plain,
inverse(divide(X1,divide(X2,inverse(X3)))) = multiply(inverse(divide(X4,X2)),divide(multiply(divide(Y4,Y4),multiply(X4,X3)),X1)),
inference(cp,[status(thm)],[t2759,t5]) ).
cnf(t8786,plain,
inverse(divide(X1,multiply(X2,X3))) = multiply(inverse(divide(X4,X2)),divide(multiply(divide(Y4,Y4),multiply(X4,X3)),X1)),
inference(step,[status(thm)],[t2798,t5]) ).
cnf(t2831,plain,
multiply(inverse(divide(X1,X2)),divide(multiply(divide(X3,X3),multiply(X1,X4)),Y4)) = inverse(divide(Y4,multiply(X2,X4))),
inference(orient,[status(thm)],[t8786]) ).
cnf(t2868,plain,
inverse(divide(X1,multiply(X2,X3))) = multiply(inverse(divide(X4,X2)),divide(multiply(multiply(inverse(Y4),Y4),multiply(X4,X3)),X1)),
inference(cp,[status(thm)],[t2831,t5]) ).
cnf(t3740,plain,
multiply(inverse(divide(X1,X2)),divide(multiply(multiply(inverse(X3),X3),multiply(X1,X4)),Y4)) = inverse(divide(Y4,multiply(X2,X4))),
inference(orient,[status(thm)],[t2868]) ).
cnf(t5381,plain,
divide(X1,X2) = divide(inverse(divide(X3,multiply(divide(X1,X4),Y4))),multiply(inverse(divide(Y5,divide(X2,X4))),divide(multiply(multiply(inverse(Y6),Y6),multiply(Y5,Y4)),X3))),
inference(cp,[status(thm)],[t5377,t3740]) ).
cnf(t8802,plain,
divide(X1,X2) = divide(inverse(divide(X3,multiply(divide(X1,X4),Y4))),inverse(divide(X3,multiply(divide(X2,X4),Y4)))),
inference(step,[status(thm)],[t5381,t3740]) ).
cnf(t8803,plain,
divide(X1,X2) = multiply(inverse(divide(X3,multiply(divide(X1,X4),Y4))),divide(X3,multiply(divide(X2,X4),Y4))),
inference(step,[status(thm)],[t8802,t5]) ).
cnf(t5675,plain,
multiply(inverse(divide(X1,multiply(divide(X2,X3),X4))),divide(X1,multiply(divide(Y4,X3),X4))) = divide(X2,Y4),
inference(orient,[status(thm)],[t8803]) ).
cnf(t5702,plain,
divide(X1,X2) = multiply(inverse(divide(X3,multiply(multiply(X1,X4),Y4))),divide(X3,multiply(divide(X2,inverse(X4)),Y4))),
inference(cp,[status(thm)],[t5675,t5]) ).
cnf(t8807,plain,
divide(X1,X2) = multiply(inverse(divide(X3,multiply(multiply(X1,X4),Y4))),divide(X3,multiply(multiply(X2,X4),Y4))),
inference(step,[status(thm)],[t5702,t5]) ).
cnf(t6184,plain,
multiply(inverse(divide(X1,multiply(multiply(X2,X3),X4))),divide(X1,multiply(multiply(Y4,X3),X4))) = divide(X2,Y4),
inference(orient,[status(thm)],[t8807]) ).
cnf(t2796,plain,
inverse(divide(X1,divide(X2,X3))) = multiply(inverse(divide(X4,X2)),divide(multiply(multiply(inverse(Y4),Y4),divide(X4,X3)),X1)),
inference(cp,[status(thm)],[t2759,t5]) ).
cnf(t3636,plain,
multiply(inverse(divide(X1,X2)),divide(multiply(multiply(inverse(X3),X3),divide(X1,X4)),Y4)) = inverse(divide(Y4,divide(X2,X4))),
inference(orient,[status(thm)],[t2796]) ).
cnf(t5380,plain,
divide(X1,X2) = divide(inverse(divide(X3,divide(divide(X1,X4),Y4))),multiply(inverse(divide(Y5,divide(X2,X4))),divide(multiply(multiply(inverse(Y6),Y6),divide(Y5,Y4)),X3))),
inference(cp,[status(thm)],[t5377,t3636]) ).
cnf(t8800,plain,
divide(X1,X2) = divide(inverse(divide(X3,divide(divide(X1,X4),Y4))),inverse(divide(X3,divide(divide(X2,X4),Y4)))),
inference(step,[status(thm)],[t5380,t3636]) ).
cnf(t8801,plain,
divide(X1,X2) = multiply(inverse(divide(X3,divide(divide(X1,X4),Y4))),divide(X3,divide(divide(X2,X4),Y4))),
inference(step,[status(thm)],[t8800,t5]) ).
cnf(t5546,plain,
multiply(inverse(divide(X1,divide(divide(X2,X3),X4))),divide(X1,divide(divide(Y4,X3),X4))) = divide(X2,Y4),
inference(orient,[status(thm)],[t8801]) ).
cnf(t5551,plain,
divide(X1,X2) = multiply(inverse(divide(X3,divide(divide(X1,X4),Y4))),divide(multiply(divide(Y5,Y5),divide(X3,divide(Y6,Y4))),divide(divide(X2,X4),Y6))),
inference(cp,[status(thm)],[t5546,t3428]) ).
cnf(t8804,plain,
divide(X1,X2) = inverse(divide(divide(divide(X2,X4),Y6),divide(divide(divide(X1,X4),Y4),divide(Y6,Y4)))),
inference(step,[status(thm)],[t5551,t2759]) ).
cnf(t5791,plain,
inverse(divide(divide(divide(X1,X2),X3),divide(divide(divide(X4,X2),Y4),divide(X3,Y4)))) = divide(X4,X1),
inference(orient,[status(thm)],[t8804]) ).
cnf(t5795,plain,
divide(X1,X2) = inverse(divide(divide(divide(X3,X3),X4),divide(divide(divide(X1,X2),Y4),divide(X4,Y4)))),
inference(cp,[status(thm)],[t5791,t1252]) ).
cnf(t6317,plain,
inverse(divide(divide(divide(X1,X1),X2),divide(divide(divide(X3,X4),Y4),divide(X2,Y4)))) = divide(X3,X4),
inference(orient,[status(thm)],[t5795]) ).
cnf(t6340,plain,
divide(divide(inverse(divide(X1,X2)),X3),divide(multiply(X4,divide(divide(divide(Y4,Y4),X4),X1)),X3)) = inverse(divide(divide(divide(Y5,Y5),Y6),divide(divide(X2,Y7),divide(Y6,Y7)))),
inference(cp,[status(thm)],[t6317,t2580]) ).
cnf(t8808,plain,
X2 = inverse(divide(divide(divide(Y5,Y5),Y6),divide(divide(X2,Y7),divide(Y6,Y7)))),
inference(step,[status(thm)],[t6340,t2580]) ).
cnf(t6407,plain,
inverse(divide(divide(divide(X1,X1),X2),divide(divide(X3,X4),divide(X2,X4)))) = X3,
inference(orient,[status(thm)],[t8808]) ).
cnf(t6489,plain,
divide(divide(X1,X2),divide(X3,X2)) = divide(multiply(X1,X4),multiply(X3,X4)),
inference(cp,[status(thm)],[t661,t6407]) ).
cnf(t6498,plain,
divide(divide(X1,X2),divide(X3,X2)) = divide(multiply(X1,X4),multiply(X3,X4)),
inference(orient,[status(thm)],[t6489]) ).
cnf(t6580,plain,
divide(X1,X2) = divide(multiply(inverse(divide(multiply(divide(X3,X3),X4),multiply(X1,X4))),Y4),multiply(X2,Y4)),
inference(cp,[status(thm)],[t661,t6498]) ).
cnf(t7421,plain,
divide(multiply(inverse(divide(multiply(divide(X1,X1),X2),multiply(X3,X2))),X4),multiply(Y4,X4)) = divide(X3,Y4),
inference(orient,[status(thm)],[t6580]) ).
cnf(t7527,plain,
divide(X1,X2) = multiply(inverse(divide(X3,multiply(X1,X4))),divide(multiply(inverse(divide(multiply(divide(Y4,Y4),Y5),multiply(X3,Y5))),Y6),multiply(multiply(X2,X4),Y6))),
inference(cp,[status(thm)],[t6184,t7421]) ).
cnf(t8812,plain,
divide(X1,X2) = multiply(inverse(divide(X3,multiply(X1,X4))),divide(X3,multiply(X2,X4))),
inference(step,[status(thm)],[t7527,t7421]) ).
cnf(t7619,plain,
multiply(inverse(divide(X1,multiply(X2,X3))),divide(X1,multiply(X4,X3))) = divide(X2,X4),
inference(orient,[status(thm)],[t8812]) ).
cnf(t8813,plain,
divide(multiply(X2,X3),multiply(Y4,X3)) = divide(X2,Y4),
inference(step,[status(thm)],[t6184,t7619]) ).
cnf(t7772,plain,
divide(multiply(X2,X3),multiply(Y4,X3)) = divide(X2,Y4),
inference(rw,[status(thm)],[t8813]) ).
cnf(t7774,plain,
divide(multiply(X1,X2),multiply(X3,X2)) = divide(X1,X3),
inference(orient,[status(thm)],[t7772]) ).
cnf(t6620,plain,
divide(inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,X4)))),X4) = inverse(divide(divide(divide(Y4,Y4),Y5),divide(multiply(X3,Y6),multiply(Y5,Y6)))),
inference(cp,[status(thm)],[t489,t6498]) ).
cnf(t8810,plain,
X3 = inverse(divide(divide(divide(Y4,Y4),Y5),divide(multiply(X3,Y6),multiply(Y5,Y6)))),
inference(step,[status(thm)],[t6620,t2]) ).
cnf(t6939,plain,
inverse(divide(divide(divide(X1,X1),X2),divide(multiply(X3,X4),multiply(X2,X4)))) = X3,
inference(orient,[status(thm)],[t8810]) ).
cnf(t6943,plain,
X1 = inverse(divide(multiply(divide(X2,X2),X3),divide(multiply(X1,X4),multiply(inverse(X3),X4)))),
inference(cp,[status(thm)],[t6939,t5]) ).
cnf(t7040,plain,
inverse(divide(multiply(divide(X1,X1),X2),divide(multiply(X3,X4),multiply(inverse(X2),X4)))) = X3,
inference(orient,[status(thm)],[t6943]) ).
cnf(t8819,plain,
inverse(divide(multiply(divide(X1,X1),X2),divide(X3,inverse(X2)))) = X3,
inference(step,[status(thm)],[t7040,t7774]) ).
cnf(t8820,plain,
inverse(divide(multiply(divide(X1,X1),X2),multiply(X3,X2))) = X3,
inference(step,[status(thm)],[t8819,t5]) ).
cnf(t8821,plain,
inverse(divide(divide(X1,X1),X3)) = X3,
inference(step,[status(thm)],[t8820,t7774]) ).
cnf(t7900,plain,
inverse(divide(divide(X1,X1),X3)) = X3,
inference(rw,[status(thm)],[t8821]) ).
cnf(t8121,plain,
inverse(divide(divide(X1,X1),X2)) = X2,
inference(orient,[status(thm)],[t7900]) ).
cnf(t8130,plain,
X1 = inverse(divide(multiply(inverse(X2),X2),X1)),
inference(cp,[status(thm)],[t8121,t5]) ).
cnf(t8204,plain,
inverse(divide(multiply(inverse(X1),X1),X2)) = X2,
inference(orient,[status(thm)],[t8130]) ).
cnf(t8205,plain,
multiply(X1,X2) = inverse(divide(inverse(X2),X1)),
inference(cp,[status(thm)],[t8204,t7774]) ).
cnf(t8273,plain,
inverse(divide(inverse(X1),X2)) = multiply(X2,X1),
inference(orient,[status(thm)],[t8205]) ).
cnf(t8291,plain,
multiply(inverse(X1),X2) = inverse(multiply(inverse(X2),X1)),
inference(cp,[status(thm)],[t8273,t5]) ).
cnf(t8355,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t8291]) ).
cnf(t8358,plain,
multiply(inverse(divide(X1,multiply(X2,X3))),divide(X1,multiply(X4,X3))) = inverse(divide(X4,X2)),
inference(cp,[status(thm)],[t8355,t7619]) ).
cnf(t8853,plain,
divide(X2,X4) = inverse(divide(X4,X2)),
inference(step,[status(thm)],[t8358,t7619]) ).
cnf(t8439,plain,
inverse(divide(X1,X2)) = divide(X2,X1),
inference(orient,[status(thm)],[t8853]) ).
cnf(t8876,plain,
divide(X2,divide(X1,X1)) = X2,
inference(step,[status(thm)],[t8121,t8439]) ).
cnf(t8462,plain,
divide(X2,divide(X1,X1)) = X2,
inference(rw,[status(thm)],[t8876]) ).
cnf(t8491,plain,
divide(X1,divide(X2,X2)) = X1,
inference(orient,[status(thm)],[t8462]) ).
cnf(t8493,plain,
divide(divide(X1,X1),X2) = inverse(X2),
inference(cp,[status(thm)],[t8439,t8491]) ).
cnf(t8544,plain,
divide(divide(X1,X1),X2) = inverse(X2),
inference(orient,[status(thm)],[t8493]) ).
cnf(t8545,plain,
inverse(inverse(X1)) = multiply(divide(X2,X2),X1),
inference(cp,[status(thm)],[t8544,t5]) ).
cnf(t8549,plain,
divide(X1,divide(X2,X2)) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t8439,t8544]) ).
cnf(t8937,plain,
X1 = inverse(inverse(X1)),
inference(step,[status(thm)],[t8549,t8491]) ).
cnf(t8557,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t8937]) ).
cnf(t8940,plain,
X1 = multiply(divide(X2,X2),X1),
inference(step,[status(thm)],[t8545,t8557]) ).
cnf(t8584,plain,
multiply(divide(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t8940]) ).
cnf(t8588,plain,
divide(X1,divide(X2,X2)) = divide(multiply(X1,X3),X3),
inference(cp,[status(thm)],[t7774,t8584]) ).
cnf(t8943,plain,
X1 = divide(multiply(X1,X3),X3),
inference(step,[status(thm)],[t8588,t8491]) ).
cnf(t8591,plain,
divide(multiply(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t8943]) ).
cnf(t8592,plain,
X1 = multiply(multiply(X1,inverse(X2)),X2),
inference(cp,[status(thm)],[t8591,t5]) ).
cnf(t8558,plain,
multiply(X1,inverse(X2)) = divide(X1,X2),
inference(cp,[status(thm)],[t5,t8557]) ).
cnf(t8559,plain,
multiply(X1,inverse(X2)) = divide(X1,X2),
inference(orient,[status(thm)],[t8558]) ).
cnf(t8944,plain,
X1 = multiply(divide(X1,X2),X2),
inference(step,[status(thm)],[t8592,t8559]) ).
cnf(t8596,plain,
multiply(divide(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t8944]) ).
cnf(t8601,plain,
divide(X1,divide(X2,X3)) = divide(multiply(X1,X3),X2),
inference(cp,[status(thm)],[t7774,t8596]) ).
cnf(t8449,plain,
multiply(X1,divide(X2,X3)) = divide(X1,divide(X3,X2)),
inference(cp,[status(thm)],[t5,t8439]) ).
cnf(t8706,plain,
divide(X1,divide(X2,X3)) = multiply(X1,divide(X3,X2)),
inference(orient,[status(thm)],[t8449]) ).
cnf(t8946,plain,
multiply(X1,divide(X3,X2)) = divide(multiply(X1,X3),X2),
inference(step,[status(thm)],[t8601,t8706]) ).
cnf(t8733,plain,
divide(multiply(X1,X2),X3) = multiply(X1,divide(X2,X3)),
inference(orient,[status(thm)],[t8946]) ).
cnf(t8736,plain,
multiply(X1,divide(X2,inverse(X3))) = multiply(multiply(X1,X2),X3),
inference(cp,[status(thm)],[t8733,t5]) ).
cnf(t8947,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t8736,t5]) ).
cnf(t8744,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t8947]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t8744]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP480-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/5.58 % Computer : n004.cluster.edu
% 0.10/5.58 % Model : x86_64 x86_64
% 0.10/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.58 % Memory : 8046.5625MB
% 0.10/5.58 % OS : Linux 6.8.0-71-generic
% 0.10/5.58 % CPULimit : 300
% 0.10/5.58 % WCLimit : 300
% 0.10/5.58 % DateTime : Wed Sep 23 14:52:12 UTC 2026
% 0.10/5.58 % CPUTime :
% 0.10/5.58 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.13/6.74 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.13/6.74 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------