%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP467-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 : n001.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:26:56 PM UTC 2026
% Result : Unsatisfiable 5.71s 1.18s
% Output : CNFRefutation 5.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 7
% Syntax : Number of clauses : 65 ( 65 unt; 0 nHn; 36 RR)
% Number of literals : 65 ( 64 equ; 7 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 54 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
divide(divide(X1,X1),divide(X2,divide(divide(X3,divide(X4,X2)),inverse(X4)))) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
divide(divide(X1,X1),divide(X2,divide(divide(X3,divide(X4,X2)),inverse(X4)))) = X3,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,axiom,
sF1 = divide(inverse(b2),inverse(b2)),
introduced(definition) ).
cnf(t1,axiom,
sF0 = inverse(b2),
introduced(definition) ).
cnf(t5,plain,
inverse(b2) = sF0,
inference(orient,[status(thm)],[t1]) ).
cnf(t709,plain,
sF1 = divide(sF0,inverse(b2)),
inference(step,[status(thm)],[t2,t5]) ).
cnf(t710,plain,
sF1 = divide(sF0,sF0),
inference(step,[status(thm)],[t709,t5]) ).
cnf(t7,plain,
divide(sF0,sF0) = sF1,
inference(orient,[status(thm)],[t710]) ).
cnf(t12,plain,
X1 = divide(sF1,divide(X2,divide(divide(X1,divide(X3,X2)),inverse(X3)))),
inference(cp,[status(thm)],[t9,t7]) ).
cnf(t17,plain,
divide(sF1,divide(X1,divide(divide(X2,divide(X3,X1)),inverse(X3)))) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t10,plain,
X1 = divide(divide(X2,X2),divide(X3,divide(divide(X1,divide(b2,X3)),sF0))),
inference(cp,[status(thm)],[t9,t5]) ).
cnf(t56,plain,
divide(divide(X1,X1),divide(X2,divide(divide(X3,divide(b2,X2)),sF0))) = X3,
inference(orient,[status(thm)],[t10]) ).
cnf(t18,plain,
X1 = divide(sF1,divide(X2,divide(divide(X1,divide(b2,X2)),sF0))),
inference(cp,[status(thm)],[t17,t5]) ).
cnf(t38,plain,
divide(sF1,divide(X1,divide(divide(X2,divide(b2,X1)),sF0))) = X2,
inference(orient,[status(thm)],[t18]) ).
cnf(t59,plain,
sF1 = divide(divide(X1,X1),divide(divide(divide(X2,divide(b2,b2)),sF0),divide(X2,sF0))),
inference(cp,[status(thm)],[t56,t38]) ).
cnf(t446,plain,
divide(divide(X1,X1),divide(divide(divide(X2,divide(b2,b2)),sF0),divide(X2,sF0))) = sF1,
inference(orient,[status(thm)],[t59]) ).
cnf(t447,plain,
sF1 = divide(divide(X1,X1),divide(divide(divide(sF0,divide(b2,b2)),sF0),sF1)),
inference(cp,[status(thm)],[t446,t7]) ).
cnf(t461,plain,
divide(divide(X1,X1),divide(divide(divide(sF0,divide(b2,b2)),sF0),sF1)) = sF1,
inference(orient,[status(thm)],[t447]) ).
cnf(t466,plain,
divide(X1,X1) = divide(sF1,divide(sF1,divide(sF1,inverse(divide(divide(sF0,divide(b2,b2)),sF0))))),
inference(cp,[status(thm)],[t17,t461]) ).
cnf(t41,plain,
sF1 = divide(sF1,divide(divide(divide(X1,divide(b2,b2)),sF0),divide(X1,sF0))),
inference(cp,[status(thm)],[t38,t38]) ).
cnf(t102,plain,
divide(sF1,divide(divide(divide(X1,divide(b2,b2)),sF0),divide(X1,sF0))) = sF1,
inference(orient,[status(thm)],[t41]) ).
cnf(t103,plain,
sF1 = divide(sF1,divide(divide(divide(sF0,divide(b2,b2)),sF0),sF1)),
inference(cp,[status(thm)],[t102,t7]) ).
cnf(t108,plain,
divide(sF1,divide(divide(divide(sF0,divide(b2,b2)),sF0),sF1)) = sF1,
inference(orient,[status(thm)],[t103]) ).
cnf(t111,plain,
sF1 = divide(sF1,divide(sF1,divide(sF1,inverse(divide(divide(sF0,divide(b2,b2)),sF0))))),
inference(cp,[status(thm)],[t17,t108]) ).
cnf(t230,plain,
divide(sF1,divide(sF1,divide(sF1,inverse(divide(divide(sF0,divide(b2,b2)),sF0))))) = sF1,
inference(orient,[status(thm)],[t111]) ).
cnf(t715,plain,
divide(X1,X1) = sF1,
inference(step,[status(thm)],[t466,t230]) ).
cnf(t473,plain,
divide(X1,X1) = sF1,
inference(orient,[status(thm)],[t715]) ).
cnf(t20,plain,
X1 = divide(sF1,divide(sF0,divide(divide(X1,sF1),inverse(sF0)))),
inference(cp,[status(thm)],[t17,t7]) ).
cnf(t28,plain,
divide(sF1,divide(sF0,divide(divide(X1,sF1),inverse(sF0)))) = X1,
inference(orient,[status(thm)],[t20]) ).
cnf(t32,plain,
X1 = divide(sF1,divide(divide(sF0,divide(divide(X2,sF1),inverse(sF0))),divide(divide(X1,X2),inverse(sF1)))),
inference(cp,[status(thm)],[t17,t28]) ).
cnf(t665,plain,
divide(sF1,divide(divide(sF0,divide(divide(X1,sF1),inverse(sF0))),divide(divide(X2,X1),inverse(sF1)))) = X2,
inference(orient,[status(thm)],[t32]) ).
cnf(t3,axiom,
sF2 = inverse(a2),
introduced(definition) ).
cnf(t6,plain,
inverse(a2) = sF2,
inference(orient,[status(thm)],[t3]) ).
cnf(t19,plain,
X1 = divide(sF1,divide(X2,divide(divide(X1,divide(a2,X2)),sF2))),
inference(cp,[status(thm)],[t17,t6]) ).
cnf(t46,plain,
divide(sF1,divide(X1,divide(divide(X2,divide(a2,X1)),sF2))) = X2,
inference(orient,[status(thm)],[t19]) ).
cnf(t498,plain,
divide(a2,X1) = divide(sF1,divide(X1,divide(sF1,sF2))),
inference(cp,[status(thm)],[t46,t473]) ).
cnf(t4,axiom,
sF3 = divide(divide(inverse(b2),inverse(b2)),inverse(a2)),
introduced(definition) ).
cnf(t711,plain,
sF3 = divide(divide(sF0,inverse(b2)),inverse(a2)),
inference(step,[status(thm)],[t4,t5]) ).
cnf(t712,plain,
sF3 = divide(divide(sF0,sF0),inverse(a2)),
inference(step,[status(thm)],[t711,t5]) ).
cnf(t713,plain,
sF3 = divide(sF1,inverse(a2)),
inference(step,[status(thm)],[t712,t7]) ).
cnf(t714,plain,
sF3 = divide(sF1,sF2),
inference(step,[status(thm)],[t713,t6]) ).
cnf(t8,plain,
divide(sF1,sF2) = sF3,
inference(orient,[status(thm)],[t714]) ).
cnf(t727,plain,
divide(a2,X1) = divide(sF1,divide(X1,sF3)),
inference(step,[status(thm)],[t498,t8]) ).
cnf(t579,plain,
divide(sF1,divide(X1,sF3)) = divide(a2,X1),
inference(orient,[status(thm)],[t727]) ).
cnf(t582,plain,
divide(a2,sF3) = divide(sF1,sF1),
inference(cp,[status(thm)],[t579,t473]) ).
cnf(t730,plain,
divide(a2,sF3) = sF1,
inference(step,[status(thm)],[t582,t473]) ).
cnf(t591,plain,
divide(a2,sF3) = sF1,
inference(orient,[status(thm)],[t730]) ).
cnf(t684,plain,
a2 = divide(sF1,divide(divide(sF0,divide(divide(sF3,sF1),inverse(sF0))),divide(sF1,inverse(sF1)))),
inference(cp,[status(thm)],[t665,t591]) ).
cnf(t492,plain,
divide(X1,X2) = divide(sF1,divide(X2,divide(sF1,inverse(X1)))),
inference(cp,[status(thm)],[t17,t473]) ).
cnf(t618,plain,
divide(sF1,divide(X1,divide(sF1,inverse(X2)))) = divide(X2,X1),
inference(orient,[status(thm)],[t492]) ).
cnf(t736,plain,
a2 = divide(sF1,divide(sF0,divide(divide(sF3,sF1),inverse(sF0)))),
inference(step,[status(thm)],[t684,t618]) ).
cnf(t737,plain,
a2 = sF3,
inference(step,[status(thm)],[t736,t28]) ).
cnf(t696,plain,
a2 = sF3,
inference(orient,[status(thm)],[t737]) ).
cnf(t738,plain,
inverse(sF3) = sF2,
inference(step,[status(thm)],[t6,t696]) ).
cnf(t697,plain,
inverse(sF3) = sF2,
inference(rw,[status(thm)],[t738]) ).
cnf(t707,plain,
inverse(sF3) = sF2,
inference(orient,[status(thm)],[t697]) ).
cnf(u0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
multiply(A,B) = divide(A,inverse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
divide(divide(inverse(b2),inverse(b2)),inverse(a2)) != a2,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
divide(sF1,inverse(a2)) != a2,
inference(rw,[status(thm)],[goal_0,t473]) ).
cnf(g0_1,plain,
divide(sF1,inverse(sF3)) != a2,
inference(rw,[status(thm)],[g0_0,t696]) ).
cnf(g0_2,plain,
divide(sF1,sF2) != a2,
inference(rw,[status(thm)],[g0_1,t707]) ).
cnf(g0_3,plain,
sF3 != a2,
inference(rw,[status(thm)],[g0_2,t8]) ).
cnf(g0_4,plain,
sF3 != sF3,
inference(rw,[status(thm)],[g0_3,t696]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP467-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n001.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 : Wed Sep 23 14:55:20 UTC 2026
% 0.13/0.37 % CPUTime :
% 0.13/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.71/1.18 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.71/1.18 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------