%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP470-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 : n007.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 8.24s 1.88s
% Output : CNFRefutation 8.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 140
% Number of leaves : 7
% Syntax : Number of clauses : 294 ( 294 unt; 0 nHn; 155 RR)
% Number of literals : 294 ( 293 equ; 8 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 : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 193 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
divide(inverse(divide(X1,divide(X2,divide(X3,X4)))),divide(divide(X4,X3),X1)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
divide(inverse(divide(X1,divide(X2,divide(X3,X4)))),divide(divide(X4,X3),X1)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,axiom,
sFlat1 = divide(inverse(b2),inverse(b2)),
introduced(definition) ).
cnf(t14,plain,
divide(inverse(b2),inverse(b2)) = sFlat1,
inference(orient,[status(thm)],[t2]) ).
cnf(t1,axiom,
sFlat0 = inverse(b2),
introduced(definition) ).
cnf(t18,plain,
inverse(b2) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t2598,plain,
divide(sFlat0,inverse(b2)) = sFlat1,
inference(step,[status(thm)],[t14,t18]) ).
cnf(t2599,plain,
divide(sFlat0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t2598,t18]) ).
cnf(t19,plain,
divide(sFlat0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t2599]) ).
cnf(t21,plain,
divide(sFlat0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t19]) ).
cnf(t22,plain,
X1 = divide(inverse(divide(X2,divide(X1,sFlat1))),divide(divide(sFlat0,sFlat0),X2)),
inference(cp,[status(thm)],[t5,t21]) ).
cnf(t2601,plain,
X1 = divide(inverse(divide(X2,divide(X1,sFlat1))),divide(sFlat1,X2)),
inference(step,[status(thm)],[t22,t21]) ).
cnf(t27,plain,
divide(inverse(divide(X1,divide(X2,sFlat1))),divide(sFlat1,X1)) = X2,
inference(orient,[status(thm)],[t2601]) ).
cnf(t32,plain,
inverse(divide(X1,divide(X2,sFlat1))) = divide(inverse(divide(X3,X2)),divide(divide(X1,sFlat1),X3)),
inference(cp,[status(thm)],[t5,t27]) ).
cnf(t88,plain,
divide(inverse(divide(X1,X2)),divide(divide(X3,sFlat1),X1)) = inverse(divide(X3,divide(X2,sFlat1))),
inference(orient,[status(thm)],[t32]) ).
cnf(t6,plain,
divide(X1,X2) = divide(inverse(X3),divide(divide(X4,Y4),inverse(divide(divide(Y4,X4),divide(X3,divide(X2,X1)))))),
inference(cp,[status(thm)],[t5,t5]) ).
cnf(t378,plain,
divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,divide(X4,Y4)))))) = divide(Y4,X4),
inference(orient,[status(thm)],[t6]) ).
cnf(t4,axiom,
sFlat3 = divide(divide(inverse(b2),inverse(b2)),inverse(a2)),
introduced(definition) ).
cnf(t10,plain,
divide(divide(inverse(b2),inverse(b2)),inverse(a2)) = sFlat3,
inference(orient,[status(thm)],[t4]) ).
cnf(t2597,plain,
divide(sFlat1,inverse(a2)) = sFlat3,
inference(step,[status(thm)],[t10,t14]) ).
cnf(t17,plain,
divide(sFlat1,inverse(a2)) = sFlat3,
inference(rw,[status(thm)],[t2597]) ).
cnf(t3,axiom,
sFlat2 = inverse(a2),
introduced(definition) ).
cnf(t20,plain,
inverse(a2) = sFlat2,
inference(orient,[status(thm)],[t3]) ).
cnf(t2600,plain,
divide(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t17,t20]) ).
cnf(t24,plain,
divide(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t2600]) ).
cnf(t29,plain,
X1 = divide(inverse(divide(sFlat2,divide(X1,sFlat1))),sFlat3),
inference(cp,[status(thm)],[t27,t24]) ).
cnf(t35,plain,
divide(inverse(divide(sFlat2,divide(X1,sFlat1))),sFlat3) = X1,
inference(orient,[status(thm)],[t29]) ).
cnf(t25,plain,
X1 = divide(inverse(divide(X2,divide(X1,sFlat3))),divide(divide(sFlat2,sFlat1),X2)),
inference(cp,[status(thm)],[t5,t24]) ).
cnf(t52,plain,
divide(inverse(divide(X1,divide(X2,sFlat3))),divide(divide(sFlat2,sFlat1),X1)) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(t2602,plain,
inverse(divide(sFlat2,divide(divide(X2,sFlat3),sFlat1))) = X2,
inference(step,[status(thm)],[t52,t88]) ).
cnf(t109,plain,
inverse(divide(sFlat2,divide(divide(X2,sFlat3),sFlat1))) = X2,
inference(rw,[status(thm)],[t2602]) ).
cnf(t110,plain,
inverse(divide(sFlat2,divide(divide(X1,sFlat3),sFlat1))) = X1,
inference(orient,[status(thm)],[t109]) ).
cnf(t111,plain,
inverse(divide(X1,divide(divide(divide(X2,sFlat3),sFlat1),sFlat1))) = divide(X2,divide(divide(X1,sFlat1),sFlat2)),
inference(cp,[status(thm)],[t88,t110]) ).
cnf(t129,plain,
inverse(divide(X1,divide(divide(divide(X2,sFlat3),sFlat1),sFlat1))) = divide(X2,divide(divide(X1,sFlat1),sFlat2)),
inference(orient,[status(thm)],[t111]) ).
cnf(t135,plain,
divide(divide(X1,sFlat3),sFlat1) = divide(divide(X1,divide(divide(sFlat2,sFlat1),sFlat2)),sFlat3),
inference(cp,[status(thm)],[t35,t129]) ).
cnf(t139,plain,
divide(divide(X1,divide(divide(sFlat2,sFlat1),sFlat2)),sFlat3) = divide(divide(X1,sFlat3),sFlat1),
inference(orient,[status(thm)],[t135]) ).
cnf(t140,plain,
divide(divide(inverse(divide(sFlat2,X1)),sFlat3),sFlat1) = divide(inverse(divide(sFlat2,divide(X1,sFlat1))),sFlat3),
inference(cp,[status(thm)],[t139,t88]) ).
cnf(t2603,plain,
divide(divide(inverse(divide(sFlat2,X1)),sFlat3),sFlat1) = X1,
inference(step,[status(thm)],[t140,t35]) ).
cnf(t148,plain,
divide(divide(inverse(divide(sFlat2,X1)),sFlat3),sFlat1) = X1,
inference(orient,[status(thm)],[t2603]) ).
cnf(t56,plain,
divide(sFlat2,sFlat1) = divide(inverse(X1),divide(sFlat1,inverse(divide(sFlat1,divide(X1,sFlat3))))),
inference(cp,[status(thm)],[t27,t52]) ).
cnf(t62,plain,
divide(inverse(X1),divide(sFlat1,inverse(divide(sFlat1,divide(X1,sFlat3))))) = divide(sFlat2,sFlat1),
inference(orient,[status(thm)],[t56]) ).
cnf(t64,plain,
divide(sFlat2,sFlat1) = divide(sFlat2,divide(sFlat1,inverse(divide(sFlat1,divide(a2,sFlat3))))),
inference(cp,[status(thm)],[t62,t20]) ).
cnf(t73,plain,
divide(sFlat2,divide(sFlat1,inverse(divide(sFlat1,divide(a2,sFlat3))))) = divide(sFlat2,sFlat1),
inference(orient,[status(thm)],[t64]) ).
cnf(t150,plain,
divide(sFlat1,inverse(divide(sFlat1,divide(a2,sFlat3)))) = divide(divide(inverse(divide(sFlat2,sFlat1)),sFlat3),sFlat1),
inference(cp,[status(thm)],[t148,t73]) ).
cnf(t2604,plain,
divide(sFlat1,inverse(divide(sFlat1,divide(a2,sFlat3)))) = sFlat1,
inference(step,[status(thm)],[t150,t148]) ).
cnf(t160,plain,
divide(sFlat1,inverse(divide(sFlat1,divide(a2,sFlat3)))) = sFlat1,
inference(orient,[status(thm)],[t2604]) ).
cnf(t163,plain,
X1 = divide(inverse(divide(X2,divide(X1,sFlat1))),divide(divide(inverse(divide(sFlat1,divide(a2,sFlat3))),sFlat1),X2)),
inference(cp,[status(thm)],[t5,t160]) ).
cnf(t2605,plain,
X1 = inverse(divide(inverse(divide(sFlat1,divide(a2,sFlat3))),divide(divide(X1,sFlat1),sFlat1))),
inference(step,[status(thm)],[t163,t88]) ).
cnf(t2606,plain,
X1 = inverse(inverse(divide(X1,divide(divide(a2,sFlat3),sFlat1)))),
inference(step,[status(thm)],[t2605,t88]) ).
cnf(t166,plain,
inverse(inverse(divide(X1,divide(divide(a2,sFlat3),sFlat1)))) = X1,
inference(orient,[status(thm)],[t2606]) ).
cnf(t167,plain,
inverse(divide(sFlat1,divide(X1,divide(sFlat3,a2)))) = inverse(inverse(X1)),
inference(cp,[status(thm)],[t166,t5]) ).
cnf(t170,plain,
inverse(divide(sFlat1,divide(X1,divide(sFlat3,a2)))) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t167]) ).
cnf(t173,plain,
X1 = divide(inverse(inverse(X1)),divide(divide(a2,sFlat3),sFlat1)),
inference(cp,[status(thm)],[t5,t170]) ).
cnf(t176,plain,
divide(inverse(inverse(X1)),divide(divide(a2,sFlat3),sFlat1)) = X1,
inference(orient,[status(thm)],[t173]) ).
cnf(t185,plain,
divide(a2,sFlat3) = divide(inverse(X1),divide(sFlat1,inverse(inverse(X1)))),
inference(cp,[status(thm)],[t27,t176]) ).
cnf(t219,plain,
divide(inverse(X1),divide(sFlat1,inverse(inverse(X1)))) = divide(a2,sFlat3),
inference(orient,[status(thm)],[t185]) ).
cnf(t220,plain,
divide(a2,sFlat3) = divide(X1,divide(sFlat1,inverse(inverse(inverse(divide(X1,divide(divide(a2,sFlat3),sFlat1))))))),
inference(cp,[status(thm)],[t219,t166]) ).
cnf(t2610,plain,
divide(a2,sFlat3) = divide(X1,divide(sFlat1,inverse(X1))),
inference(step,[status(thm)],[t220,t166]) ).
cnf(t231,plain,
divide(X1,divide(sFlat1,inverse(X1))) = divide(a2,sFlat3),
inference(orient,[status(thm)],[t2610]) ).
cnf(t467,plain,
divide(divide(sFlat1,inverse(X1)),X1) = divide(inverse(X2),divide(divide(X3,X4),inverse(divide(divide(X4,X3),divide(X2,divide(a2,sFlat3)))))),
inference(cp,[status(thm)],[t378,t231]) ).
cnf(t2619,plain,
divide(divide(sFlat1,inverse(X1)),X1) = divide(sFlat3,a2),
inference(step,[status(thm)],[t467,t378]) ).
cnf(t506,plain,
divide(divide(sFlat1,inverse(X1)),X1) = divide(sFlat3,a2),
inference(orient,[status(thm)],[t2619]) ).
cnf(t232,plain,
divide(a2,sFlat3) = divide(divide(sFlat1,divide(a2,sFlat3)),sFlat1),
inference(cp,[status(thm)],[t231,t160]) ).
cnf(t254,plain,
divide(divide(sFlat1,divide(a2,sFlat3)),sFlat1) = divide(a2,sFlat3),
inference(orient,[status(thm)],[t232]) ).
cnf(t468,plain,
divide(sFlat1,divide(sFlat1,divide(a2,sFlat3))) = divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,divide(a2,sFlat3)))))),
inference(cp,[status(thm)],[t378,t254]) ).
cnf(t2620,plain,
divide(sFlat1,divide(sFlat1,divide(a2,sFlat3))) = divide(sFlat3,a2),
inference(step,[status(thm)],[t468,t378]) ).
cnf(t550,plain,
divide(sFlat1,divide(sFlat1,divide(a2,sFlat3))) = divide(sFlat3,a2),
inference(orient,[status(thm)],[t2620]) ).
cnf(t30,plain,
sFlat1 = divide(inverse(X1),divide(sFlat1,inverse(divide(sFlat1,divide(X1,sFlat1))))),
inference(cp,[status(thm)],[t27,t27]) ).
cnf(t38,plain,
divide(inverse(X1),divide(sFlat1,inverse(divide(sFlat1,divide(X1,sFlat1))))) = sFlat1,
inference(orient,[status(thm)],[t30]) ).
cnf(t264,plain,
sFlat1 = divide(inverse(divide(sFlat1,divide(a2,sFlat3))),divide(sFlat1,inverse(divide(sFlat1,divide(a2,sFlat3))))),
inference(cp,[status(thm)],[t38,t254]) ).
cnf(t2612,plain,
sFlat1 = divide(inverse(divide(sFlat1,divide(a2,sFlat3))),sFlat1),
inference(step,[status(thm)],[t264,t160]) ).
cnf(t270,plain,
divide(inverse(divide(sFlat1,divide(a2,sFlat3))),sFlat1) = sFlat1,
inference(orient,[status(thm)],[t2612]) ).
cnf(t276,plain,
inverse(divide(sFlat1,divide(a2,sFlat3))) = divide(inverse(divide(sFlat2,sFlat1)),sFlat3),
inference(cp,[status(thm)],[t35,t270]) ).
cnf(t278,plain,
inverse(divide(sFlat1,divide(a2,sFlat3))) = divide(inverse(divide(sFlat2,sFlat1)),sFlat3),
inference(orient,[status(thm)],[t276]) ).
cnf(t2613,plain,
divide(sFlat1,divide(inverse(divide(sFlat2,sFlat1)),sFlat3)) = sFlat1,
inference(step,[status(thm)],[t160,t278]) ).
cnf(t285,plain,
divide(sFlat1,divide(inverse(divide(sFlat2,sFlat1)),sFlat3)) = sFlat1,
inference(rw,[status(thm)],[t2613]) ).
cnf(t286,plain,
divide(sFlat1,divide(inverse(divide(sFlat2,sFlat1)),sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t285]) ).
cnf(t287,plain,
inverse(divide(X1,divide(divide(inverse(divide(sFlat2,sFlat1)),sFlat3),sFlat1))) = divide(inverse(sFlat1),divide(divide(X1,sFlat1),sFlat1)),
inference(cp,[status(thm)],[t88,t286]) ).
cnf(t2615,plain,
inverse(divide(X1,sFlat1)) = divide(inverse(sFlat1),divide(divide(X1,sFlat1),sFlat1)),
inference(step,[status(thm)],[t287,t148]) ).
cnf(t322,plain,
divide(inverse(sFlat1),divide(divide(X1,sFlat1),sFlat1)) = inverse(divide(X1,sFlat1)),
inference(orient,[status(thm)],[t2615]) ).
cnf(t324,plain,
inverse(divide(divide(inverse(divide(sFlat2,X1)),sFlat3),sFlat1)) = divide(inverse(sFlat1),divide(X1,sFlat1)),
inference(cp,[status(thm)],[t322,t148]) ).
cnf(t2616,plain,
inverse(X1) = divide(inverse(sFlat1),divide(X1,sFlat1)),
inference(step,[status(thm)],[t324,t148]) ).
cnf(t332,plain,
divide(inverse(sFlat1),divide(X1,sFlat1)) = inverse(X1),
inference(orient,[status(thm)],[t2616]) ).
cnf(t241,plain,
X1 = divide(inverse(divide(X2,divide(a2,sFlat3))),divide(divide(inverse(X1),sFlat1),X2)),
inference(cp,[status(thm)],[t5,t231]) ).
cnf(t2614,plain,
X1 = inverse(divide(inverse(X1),divide(divide(a2,sFlat3),sFlat1))),
inference(step,[status(thm)],[t241,t88]) ).
cnf(t299,plain,
inverse(divide(inverse(X1),divide(divide(a2,sFlat3),sFlat1))) = X1,
inference(orient,[status(thm)],[t2614]) ).
cnf(t338,plain,
sFlat1 = inverse(inverse(divide(a2,sFlat3))),
inference(cp,[status(thm)],[t299,t332]) ).
cnf(t347,plain,
inverse(inverse(divide(a2,sFlat3))) = sFlat1,
inference(orient,[status(thm)],[t338]) ).
cnf(t349,plain,
divide(a2,sFlat3) = divide(sFlat1,divide(divide(a2,sFlat3),sFlat1)),
inference(cp,[status(thm)],[t176,t347]) ).
cnf(t369,plain,
divide(sFlat1,divide(divide(a2,sFlat3),sFlat1)) = divide(a2,sFlat3),
inference(orient,[status(thm)],[t349]) ).
cnf(t484,plain,
divide(divide(divide(a2,sFlat3),sFlat1),sFlat1) = divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,divide(a2,sFlat3)))))),
inference(cp,[status(thm)],[t378,t369]) ).
cnf(t2621,plain,
divide(divide(divide(a2,sFlat3),sFlat1),sFlat1) = divide(sFlat3,a2),
inference(step,[status(thm)],[t484,t378]) ).
cnf(t559,plain,
divide(divide(divide(a2,sFlat3),sFlat1),sFlat1) = divide(sFlat3,a2),
inference(orient,[status(thm)],[t2621]) ).
cnf(t560,plain,
inverse(divide(divide(a2,sFlat3),sFlat1)) = divide(inverse(sFlat1),divide(sFlat3,a2)),
inference(cp,[status(thm)],[t332,t559]) ).
cnf(t516,plain,
inverse(divide(sFlat1,inverse(sFlat1))) = divide(inverse(sFlat1),divide(sFlat3,a2)),
inference(cp,[status(thm)],[t332,t506]) ).
cnf(t540,plain,
divide(inverse(sFlat1),divide(sFlat3,a2)) = inverse(divide(sFlat1,inverse(sFlat1))),
inference(orient,[status(thm)],[t516]) ).
cnf(t2622,plain,
inverse(divide(divide(a2,sFlat3),sFlat1)) = inverse(divide(sFlat1,inverse(sFlat1))),
inference(step,[status(thm)],[t560,t540]) ).
cnf(t572,plain,
inverse(divide(divide(a2,sFlat3),sFlat1)) = inverse(divide(sFlat1,inverse(sFlat1))),
inference(orient,[status(thm)],[t2622]) ).
cnf(t576,plain,
divide(divide(a2,sFlat3),sFlat1) = divide(inverse(inverse(divide(sFlat1,inverse(sFlat1)))),divide(divide(a2,sFlat3),sFlat1)),
inference(cp,[status(thm)],[t176,t572]) ).
cnf(t2623,plain,
divide(divide(a2,sFlat3),sFlat1) = divide(sFlat1,inverse(sFlat1)),
inference(step,[status(thm)],[t576,t176]) ).
cnf(t581,plain,
divide(divide(a2,sFlat3),sFlat1) = divide(sFlat1,inverse(sFlat1)),
inference(orient,[status(thm)],[t2623]) ).
cnf(t597,plain,
divide(sFlat1,divide(a2,sFlat3)) = divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,divide(sFlat1,inverse(sFlat1))))))),
inference(cp,[status(thm)],[t378,t581]) ).
cnf(t2630,plain,
divide(sFlat1,divide(a2,sFlat3)) = divide(inverse(sFlat1),sFlat1),
inference(step,[status(thm)],[t597,t378]) ).
cnf(t604,plain,
divide(sFlat1,divide(a2,sFlat3)) = divide(inverse(sFlat1),sFlat1),
inference(orient,[status(thm)],[t2630]) ).
cnf(t2631,plain,
divide(sFlat1,divide(inverse(sFlat1),sFlat1)) = divide(sFlat3,a2),
inference(step,[status(thm)],[t550,t604]) ).
cnf(t89,plain,
inverse(divide(X1,divide(divide(X2,divide(sFlat1,X1)),sFlat1))) = X2,
inference(cp,[status(thm)],[t88,t5]) ).
cnf(t114,plain,
inverse(divide(X1,divide(divide(X2,divide(sFlat1,X1)),sFlat1))) = X2,
inference(orient,[status(thm)],[t89]) ).
cnf(t345,plain,
inverse(sFlat1) = inverse(divide(sFlat1,divide(inverse(sFlat1),sFlat1))),
inference(cp,[status(thm)],[t114,t332]) ).
cnf(t353,plain,
inverse(divide(sFlat1,divide(inverse(sFlat1),sFlat1))) = inverse(sFlat1),
inference(orient,[status(thm)],[t345]) ).
cnf(t356,plain,
divide(sFlat1,divide(inverse(sFlat1),sFlat1)) = divide(inverse(inverse(sFlat1)),divide(divide(a2,sFlat3),sFlat1)),
inference(cp,[status(thm)],[t176,t353]) ).
cnf(t2617,plain,
divide(sFlat1,divide(inverse(sFlat1),sFlat1)) = sFlat1,
inference(step,[status(thm)],[t356,t176]) ).
cnf(t361,plain,
divide(sFlat1,divide(inverse(sFlat1),sFlat1)) = sFlat1,
inference(orient,[status(thm)],[t2617]) ).
cnf(t2632,plain,
sFlat1 = divide(sFlat3,a2),
inference(step,[status(thm)],[t2631,t361]) ).
cnf(t613,plain,
sFlat1 = divide(sFlat3,a2),
inference(rw,[status(thm)],[t2632]) ).
cnf(t616,plain,
divide(sFlat3,a2) = sFlat1,
inference(orient,[status(thm)],[t613]) ).
cnf(t2637,plain,
divide(divide(sFlat1,inverse(X1)),X1) = sFlat1,
inference(step,[status(thm)],[t506,t616]) ).
cnf(t619,plain,
divide(divide(sFlat1,inverse(X1)),X1) = sFlat1,
inference(orient,[status(thm)],[t2637]) ).
cnf(t177,plain,
divide(sFlat1,divide(X1,divide(sFlat3,a2))) = divide(inverse(inverse(inverse(X1))),divide(divide(a2,sFlat3),sFlat1)),
inference(cp,[status(thm)],[t176,t170]) ).
cnf(t2607,plain,
divide(sFlat1,divide(X1,divide(sFlat3,a2))) = inverse(X1),
inference(step,[status(thm)],[t177,t176]) ).
cnf(t189,plain,
divide(sFlat1,divide(X1,divide(sFlat3,a2))) = inverse(X1),
inference(orient,[status(thm)],[t2607]) ).
cnf(t196,plain,
sFlat1 = inverse(divide(divide(sFlat3,a2),divide(inverse(sFlat1),sFlat1))),
inference(cp,[status(thm)],[t114,t189]) ).
cnf(t293,plain,
inverse(divide(divide(sFlat3,a2),divide(inverse(sFlat1),sFlat1))) = sFlat1,
inference(orient,[status(thm)],[t196]) ).
cnf(t2641,plain,
inverse(divide(sFlat1,divide(inverse(sFlat1),sFlat1))) = sFlat1,
inference(step,[status(thm)],[t293,t616]) ).
cnf(t2642,plain,
inverse(sFlat1) = sFlat1,
inference(step,[status(thm)],[t2641,t361]) ).
cnf(t630,plain,
inverse(sFlat1) = sFlat1,
inference(rw,[status(thm)],[t2642]) ).
cnf(t631,plain,
inverse(sFlat1) = sFlat1,
inference(orient,[status(thm)],[t630]) ).
cnf(t636,plain,
sFlat1 = divide(divide(sFlat1,sFlat1),sFlat1),
inference(cp,[status(thm)],[t619,t631]) ).
cnf(t644,plain,
divide(divide(sFlat1,sFlat1),sFlat1) = sFlat1,
inference(orient,[status(thm)],[t636]) ).
cnf(t646,plain,
inverse(divide(sFlat1,divide(X1,sFlat1))) = divide(inverse(divide(sFlat1,X1)),sFlat1),
inference(cp,[status(thm)],[t88,t644]) ).
cnf(t2640,plain,
divide(sFlat1,divide(X1,sFlat1)) = inverse(X1),
inference(step,[status(thm)],[t189,t616]) ).
cnf(t629,plain,
divide(sFlat1,divide(X1,sFlat1)) = inverse(X1),
inference(rw,[status(thm)],[t2640]) ).
cnf(t682,plain,
divide(sFlat1,divide(X1,sFlat1)) = inverse(X1),
inference(orient,[status(thm)],[t629]) ).
cnf(t2666,plain,
inverse(inverse(X1)) = divide(inverse(divide(sFlat1,X1)),sFlat1),
inference(step,[status(thm)],[t646,t682]) ).
cnf(t871,plain,
divide(inverse(divide(sFlat1,X1)),sFlat1) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t2666]) ).
cnf(t877,plain,
inverse(inverse(divide(X1,sFlat1))) = divide(inverse(inverse(X1)),sFlat1),
inference(cp,[status(thm)],[t871,t682]) ).
cnf(t889,plain,
inverse(inverse(divide(X1,sFlat1))) = divide(inverse(inverse(X1)),sFlat1),
inference(orient,[status(thm)],[t877]) ).
cnf(t2648,plain,
divide(sFlat1,divide(sFlat1,sFlat1)) = sFlat1,
inference(step,[status(thm)],[t361,t631]) ).
cnf(t642,plain,
divide(sFlat1,divide(sFlat1,sFlat1)) = sFlat1,
inference(rw,[status(thm)],[t2648]) ).
cnf(t659,plain,
divide(sFlat1,divide(sFlat1,sFlat1)) = sFlat1,
inference(orient,[status(thm)],[t642]) ).
cnf(t664,plain,
sFlat1 = divide(inverse(sFlat1),divide(sFlat1,inverse(sFlat1))),
inference(cp,[status(thm)],[t38,t659]) ).
cnf(t2650,plain,
sFlat1 = divide(sFlat1,divide(sFlat1,inverse(sFlat1))),
inference(step,[status(thm)],[t664,t631]) ).
cnf(t2651,plain,
sFlat1 = divide(a2,sFlat3),
inference(step,[status(thm)],[t2650,t231]) ).
cnf(t669,plain,
divide(a2,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t2651]) ).
cnf(t676,plain,
divide(a2,divide(divide(X1,sFlat1),sFlat2)) = inverse(divide(X1,divide(divide(sFlat1,sFlat1),sFlat1))),
inference(cp,[status(thm)],[t129,t669]) ).
cnf(t2667,plain,
divide(a2,divide(divide(X1,sFlat1),sFlat2)) = inverse(divide(X1,sFlat1)),
inference(step,[status(thm)],[t676,t644]) ).
cnf(t932,plain,
divide(a2,divide(divide(X1,sFlat1),sFlat2)) = inverse(divide(X1,sFlat1)),
inference(orient,[status(thm)],[t2667]) ).
cnf(t936,plain,
inverse(divide(divide(inverse(divide(sFlat2,X1)),sFlat3),sFlat1)) = divide(a2,divide(X1,sFlat2)),
inference(cp,[status(thm)],[t932,t148]) ).
cnf(t2668,plain,
inverse(X1) = divide(a2,divide(X1,sFlat2)),
inference(step,[status(thm)],[t936,t148]) ).
cnf(t946,plain,
divide(a2,divide(X1,sFlat2)) = inverse(X1),
inference(orient,[status(thm)],[t2668]) ).
cnf(t650,plain,
divide(sFlat1,sFlat1) = divide(inverse(divide(X1,sFlat1)),divide(sFlat1,X1)),
inference(cp,[status(thm)],[t27,t644]) ).
cnf(t1170,plain,
divide(inverse(divide(X1,sFlat1)),divide(sFlat1,X1)) = divide(sFlat1,sFlat1),
inference(orient,[status(thm)],[t650]) ).
cnf(t183,plain,
a2 = divide(inverse(sFlat2),divide(divide(a2,sFlat3),sFlat1)),
inference(cp,[status(thm)],[t176,t20]) ).
cnf(t208,plain,
divide(inverse(sFlat2),divide(divide(a2,sFlat3),sFlat1)) = a2,
inference(orient,[status(thm)],[t183]) ).
cnf(t210,plain,
divide(a2,sFlat3) = divide(inverse(a2),divide(sFlat1,inverse(sFlat2))),
inference(cp,[status(thm)],[t27,t208]) ).
cnf(t2609,plain,
divide(a2,sFlat3) = divide(sFlat2,divide(sFlat1,inverse(sFlat2))),
inference(step,[status(thm)],[t210,t20]) ).
cnf(t214,plain,
divide(sFlat2,divide(sFlat1,inverse(sFlat2))) = divide(a2,sFlat3),
inference(orient,[status(thm)],[t2609]) ).
cnf(t216,plain,
divide(sFlat1,inverse(sFlat2)) = divide(divide(inverse(divide(a2,sFlat3)),sFlat3),sFlat1),
inference(cp,[status(thm)],[t148,t214]) ).
cnf(t311,plain,
divide(divide(inverse(divide(a2,sFlat3)),sFlat3),sFlat1) = divide(sFlat1,inverse(sFlat2)),
inference(orient,[status(thm)],[t216]) ).
cnf(t2656,plain,
divide(divide(inverse(sFlat1),sFlat3),sFlat1) = divide(sFlat1,inverse(sFlat2)),
inference(step,[status(thm)],[t311,t669]) ).
cnf(t2657,plain,
divide(divide(sFlat1,sFlat3),sFlat1) = divide(sFlat1,inverse(sFlat2)),
inference(step,[status(thm)],[t2656,t631]) ).
cnf(t681,plain,
divide(divide(sFlat1,sFlat3),sFlat1) = divide(sFlat1,inverse(sFlat2)),
inference(rw,[status(thm)],[t2657]) ).
cnf(t710,plain,
divide(divide(sFlat1,sFlat3),sFlat1) = divide(sFlat1,inverse(sFlat2)),
inference(orient,[status(thm)],[t681]) ).
cnf(t935,plain,
inverse(divide(divide(sFlat1,sFlat3),sFlat1)) = divide(a2,divide(divide(sFlat1,inverse(sFlat2)),sFlat2)),
inference(cp,[status(thm)],[t932,t710]) ).
cnf(t2669,plain,
inverse(divide(sFlat1,inverse(sFlat2))) = divide(a2,divide(divide(sFlat1,inverse(sFlat2)),sFlat2)),
inference(step,[status(thm)],[t935,t710]) ).
cnf(t2670,plain,
inverse(divide(sFlat1,inverse(sFlat2))) = divide(a2,sFlat1),
inference(step,[status(thm)],[t2669,t619]) ).
cnf(t956,plain,
inverse(divide(sFlat1,inverse(sFlat2))) = divide(a2,sFlat1),
inference(orient,[status(thm)],[t2670]) ).
cnf(t959,plain,
inverse(inverse(inverse(sFlat2))) = divide(divide(a2,sFlat1),sFlat1),
inference(cp,[status(thm)],[t871,t956]) ).
cnf(t963,plain,
divide(divide(a2,sFlat1),sFlat1) = inverse(inverse(inverse(sFlat2))),
inference(orient,[status(thm)],[t959]) ).
cnf(t1172,plain,
divide(sFlat1,sFlat1) = divide(inverse(inverse(inverse(inverse(sFlat2)))),divide(sFlat1,divide(a2,sFlat1))),
inference(cp,[status(thm)],[t1170,t963]) ).
cnf(t2675,plain,
divide(sFlat1,sFlat1) = divide(inverse(inverse(inverse(inverse(sFlat2)))),inverse(a2)),
inference(step,[status(thm)],[t1172,t682]) ).
cnf(t2676,plain,
divide(sFlat1,sFlat1) = divide(inverse(inverse(inverse(inverse(sFlat2)))),sFlat2),
inference(step,[status(thm)],[t2675,t20]) ).
cnf(t1197,plain,
divide(inverse(inverse(inverse(inverse(sFlat2)))),sFlat2) = divide(sFlat1,sFlat1),
inference(orient,[status(thm)],[t2676]) ).
cnf(t1198,plain,
inverse(inverse(inverse(inverse(inverse(sFlat2))))) = divide(a2,divide(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t946,t1197]) ).
cnf(t968,plain,
divide(inverse(inverse(divide(a2,sFlat1))),sFlat1) = inverse(inverse(inverse(inverse(inverse(sFlat2))))),
inference(cp,[status(thm)],[t889,t963]) ).
cnf(t2671,plain,
divide(divide(inverse(inverse(a2)),sFlat1),sFlat1) = inverse(inverse(inverse(inverse(inverse(sFlat2))))),
inference(step,[status(thm)],[t968,t889]) ).
cnf(t2672,plain,
divide(divide(inverse(sFlat2),sFlat1),sFlat1) = inverse(inverse(inverse(inverse(inverse(sFlat2))))),
inference(step,[status(thm)],[t2671,t20]) ).
cnf(t1004,plain,
inverse(inverse(inverse(inverse(inverse(sFlat2))))) = divide(divide(inverse(sFlat2),sFlat1),sFlat1),
inference(orient,[status(thm)],[t2672]) ).
cnf(t2677,plain,
divide(divide(inverse(sFlat2),sFlat1),sFlat1) = divide(a2,divide(sFlat1,sFlat1)),
inference(step,[status(thm)],[t1198,t1004]) ).
cnf(t1207,plain,
divide(divide(inverse(sFlat2),sFlat1),sFlat1) = divide(a2,divide(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t2677]) ).
cnf(t1215,plain,
divide(inverse(inverse(divide(inverse(sFlat2),sFlat1))),sFlat1) = inverse(inverse(divide(a2,divide(sFlat1,sFlat1)))),
inference(cp,[status(thm)],[t889,t1207]) ).
cnf(t2686,plain,
divide(divide(inverse(inverse(inverse(sFlat2))),sFlat1),sFlat1) = inverse(inverse(divide(a2,divide(sFlat1,sFlat1)))),
inference(step,[status(thm)],[t1215,t889]) ).
cnf(t693,plain,
X1 = inverse(inverse(divide(X1,divide(sFlat1,sFlat1)))),
inference(cp,[status(thm)],[t114,t682]) ).
cnf(t778,plain,
inverse(inverse(divide(X1,divide(sFlat1,sFlat1)))) = X1,
inference(orient,[status(thm)],[t693]) ).
cnf(t2687,plain,
divide(divide(inverse(inverse(inverse(sFlat2))),sFlat1),sFlat1) = a2,
inference(step,[status(thm)],[t2686,t778]) ).
cnf(t1265,plain,
divide(divide(inverse(inverse(inverse(sFlat2))),sFlat1),sFlat1) = a2,
inference(orient,[status(thm)],[t2687]) ).
cnf(t1276,plain,
divide(inverse(inverse(inverse(sFlat2))),sFlat1) = divide(inverse(divide(sFlat2,a2)),sFlat3),
inference(cp,[status(thm)],[t35,t1265]) ).
cnf(t1293,plain,
divide(inverse(inverse(inverse(sFlat2))),sFlat1) = divide(inverse(divide(sFlat2,a2)),sFlat3),
inference(orient,[status(thm)],[t1276]) ).
cnf(t1298,plain,
divide(inverse(inverse(inverse(inverse(inverse(sFlat2))))),sFlat1) = inverse(inverse(divide(inverse(divide(sFlat2,a2)),sFlat3))),
inference(cp,[status(thm)],[t889,t1293]) ).
cnf(t2678,plain,
inverse(inverse(inverse(inverse(inverse(sFlat2))))) = divide(a2,divide(sFlat1,sFlat1)),
inference(step,[status(thm)],[t1004,t1207]) ).
cnf(t1208,plain,
inverse(inverse(inverse(inverse(inverse(sFlat2))))) = divide(a2,divide(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t2678]) ).
cnf(t2690,plain,
divide(divide(a2,divide(sFlat1,sFlat1)),sFlat1) = inverse(inverse(divide(inverse(divide(sFlat2,a2)),sFlat3))),
inference(step,[status(thm)],[t1298,t1208]) ).
cnf(t685,plain,
inverse(divide(inverse(divide(sFlat2,X1)),sFlat3)) = divide(sFlat1,X1),
inference(cp,[status(thm)],[t682,t148]) ).
cnf(t830,plain,
inverse(divide(inverse(divide(sFlat2,X1)),sFlat3)) = divide(sFlat1,X1),
inference(orient,[status(thm)],[t685]) ).
cnf(t2691,plain,
divide(divide(a2,divide(sFlat1,sFlat1)),sFlat1) = inverse(divide(sFlat1,a2)),
inference(step,[status(thm)],[t2690,t830]) ).
cnf(t1319,plain,
divide(divide(a2,divide(sFlat1,sFlat1)),sFlat1) = inverse(divide(sFlat1,a2)),
inference(orient,[status(thm)],[t2691]) ).
cnf(t1320,plain,
inverse(divide(a2,divide(sFlat1,sFlat1))) = divide(sFlat1,inverse(divide(sFlat1,a2))),
inference(cp,[status(thm)],[t682,t1319]) ).
cnf(t2627,plain,
inverse(divide(inverse(X1),divide(sFlat1,inverse(sFlat1)))) = X1,
inference(step,[status(thm)],[t299,t581]) ).
cnf(t601,plain,
inverse(divide(inverse(X1),divide(sFlat1,inverse(sFlat1)))) = X1,
inference(rw,[status(thm)],[t2627]) ).
cnf(t2665,plain,
inverse(divide(inverse(X1),divide(sFlat1,sFlat1))) = X1,
inference(step,[status(thm)],[t601,t631]) ).
cnf(t842,plain,
inverse(divide(inverse(X1),divide(sFlat1,sFlat1))) = X1,
inference(orient,[status(thm)],[t2665]) ).
cnf(t675,plain,
a2 = inverse(divide(sFlat2,divide(sFlat1,sFlat1))),
inference(cp,[status(thm)],[t110,t669]) ).
cnf(t704,plain,
inverse(divide(sFlat2,divide(sFlat1,sFlat1))) = a2,
inference(orient,[status(thm)],[t675]) ).
cnf(t846,plain,
divide(sFlat2,divide(sFlat1,sFlat1)) = inverse(divide(a2,divide(sFlat1,sFlat1))),
inference(cp,[status(thm)],[t842,t704]) ).
cnf(t863,plain,
inverse(divide(a2,divide(sFlat1,sFlat1))) = divide(sFlat2,divide(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t846]) ).
cnf(t2692,plain,
divide(sFlat2,divide(sFlat1,sFlat1)) = divide(sFlat1,inverse(divide(sFlat1,a2))),
inference(step,[status(thm)],[t1320,t863]) ).
cnf(t1343,plain,
divide(sFlat1,inverse(divide(sFlat1,a2))) = divide(sFlat2,divide(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t2692]) ).
cnf(t1354,plain,
divide(inverse(divide(sFlat1,a2)),sFlat1) = divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,divide(sFlat2,divide(sFlat1,sFlat1))))))),
inference(cp,[status(thm)],[t378,t1343]) ).
cnf(t2693,plain,
inverse(inverse(a2)) = divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,divide(sFlat2,divide(sFlat1,sFlat1))))))),
inference(step,[status(thm)],[t1354,t871]) ).
cnf(t2694,plain,
inverse(sFlat2) = divide(inverse(X1),divide(divide(X2,X3),inverse(divide(divide(X3,X2),divide(X1,divide(sFlat2,divide(sFlat1,sFlat1))))))),
inference(step,[status(thm)],[t2693,t20]) ).
cnf(t2695,plain,
inverse(sFlat2) = divide(divide(sFlat1,sFlat1),sFlat2),
inference(step,[status(thm)],[t2694,t378]) ).
cnf(t1355,plain,
divide(divide(sFlat1,sFlat1),sFlat2) = inverse(sFlat2),
inference(orient,[status(thm)],[t2695]) ).
cnf(t1358,plain,
inverse(divide(sFlat1,divide(X1,sFlat1))) = divide(inverse(divide(sFlat2,X1)),inverse(sFlat2)),
inference(cp,[status(thm)],[t88,t1355]) ).
cnf(t2698,plain,
inverse(inverse(X1)) = divide(inverse(divide(sFlat2,X1)),inverse(sFlat2)),
inference(step,[status(thm)],[t1358,t682]) ).
cnf(t1379,plain,
divide(inverse(divide(sFlat2,X1)),inverse(sFlat2)) = inverse(inverse(X1)),
inference(orient,[status(thm)],[t2698]) ).
cnf(t2652,plain,
divide(X1,divide(sFlat1,inverse(X1))) = sFlat1,
inference(step,[status(thm)],[t231,t669]) ).
cnf(t670,plain,
divide(X1,divide(sFlat1,inverse(X1))) = sFlat1,
inference(orient,[status(thm)],[t2652]) ).
cnf(t1384,plain,
inverse(inverse(divide(sFlat1,inverse(sFlat2)))) = divide(inverse(sFlat1),inverse(sFlat2)),
inference(cp,[status(thm)],[t1379,t670]) ).
cnf(t878,plain,
inverse(inverse(divide(sFlat1,X1))) = divide(sFlat1,inverse(inverse(X1))),
inference(cp,[status(thm)],[t682,t871]) ).
cnf(t900,plain,
inverse(inverse(divide(sFlat1,X1))) = divide(sFlat1,inverse(inverse(X1))),
inference(orient,[status(thm)],[t878]) ).
cnf(t2699,plain,
divide(sFlat1,inverse(inverse(inverse(sFlat2)))) = divide(inverse(sFlat1),inverse(sFlat2)),
inference(step,[status(thm)],[t1384,t900]) ).
cnf(t958,plain,
divide(sFlat1,inverse(inverse(inverse(sFlat2)))) = inverse(divide(a2,sFlat1)),
inference(cp,[status(thm)],[t900,t956]) ).
cnf(t979,plain,
divide(sFlat1,inverse(inverse(inverse(sFlat2)))) = inverse(divide(a2,sFlat1)),
inference(orient,[status(thm)],[t958]) ).
cnf(t2700,plain,
inverse(divide(a2,sFlat1)) = divide(inverse(sFlat1),inverse(sFlat2)),
inference(step,[status(thm)],[t2699,t979]) ).
cnf(t2701,plain,
inverse(divide(a2,sFlat1)) = divide(sFlat1,inverse(sFlat2)),
inference(step,[status(thm)],[t2700,t631]) ).
cnf(t1393,plain,
inverse(divide(a2,sFlat1)) = divide(sFlat1,inverse(sFlat2)),
inference(orient,[status(thm)],[t2701]) ).
cnf(t1400,plain,
divide(inverse(inverse(a2)),sFlat1) = inverse(divide(sFlat1,inverse(sFlat2))),
inference(cp,[status(thm)],[t889,t1393]) ).
cnf(t2708,plain,
divide(inverse(sFlat2),sFlat1) = inverse(divide(sFlat1,inverse(sFlat2))),
inference(step,[status(thm)],[t1400,t20]) ).
cnf(t2709,plain,
divide(inverse(sFlat2),sFlat1) = divide(a2,sFlat1),
inference(step,[status(thm)],[t2708,t956]) ).
cnf(t1409,plain,
divide(inverse(sFlat2),sFlat1) = divide(a2,sFlat1),
inference(orient,[status(thm)],[t2709]) ).
cnf(t1418,plain,
inverse(sFlat2) = divide(inverse(divide(X1,divide(a2,sFlat1))),divide(sFlat1,X1)),
inference(cp,[status(thm)],[t27,t1409]) ).
cnf(t2719,plain,
inverse(sFlat2) = a2,
inference(step,[status(thm)],[t1418,t27]) ).
cnf(t1430,plain,
inverse(sFlat2) = a2,
inference(orient,[status(thm)],[t2719]) ).
cnf(t182,plain,
b2 = divide(inverse(sFlat0),divide(divide(a2,sFlat3),sFlat1)),
inference(cp,[status(thm)],[t176,t18]) ).
cnf(t198,plain,
divide(inverse(sFlat0),divide(divide(a2,sFlat3),sFlat1)) = b2,
inference(orient,[status(thm)],[t182]) ).
cnf(t2625,plain,
divide(inverse(sFlat0),divide(sFlat1,inverse(sFlat1))) = b2,
inference(step,[status(thm)],[t198,t581]) ).
cnf(t599,plain,
divide(inverse(sFlat0),divide(sFlat1,inverse(sFlat1))) = b2,
inference(rw,[status(thm)],[t2625]) ).
cnf(t2661,plain,
divide(inverse(sFlat0),divide(sFlat1,sFlat1)) = b2,
inference(step,[status(thm)],[t599,t631]) ).
cnf(t752,plain,
divide(inverse(sFlat0),divide(sFlat1,sFlat1)) = b2,
inference(orient,[status(thm)],[t2661]) ).
cnf(t28,plain,
divide(X1,X2) = divide(inverse(X3),divide(sFlat1,inverse(divide(sFlat1,divide(X3,divide(X2,X1)))))),
inference(cp,[status(thm)],[t27,t5]) ).
cnf(t1740,plain,
divide(inverse(X1),divide(sFlat1,inverse(divide(sFlat1,divide(X1,divide(X2,X3)))))) = divide(X3,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t1762,plain,
divide(X1,X2) = divide(inverse(divide(sFlat1,inverse(divide(X2,X1)))),divide(sFlat1,inverse(divide(sFlat1,sFlat1)))),
inference(cp,[status(thm)],[t1740,t619]) ).
cnf(t683,plain,
inverse(divide(sFlat1,sFlat1)) = divide(sFlat1,sFlat1),
inference(cp,[status(thm)],[t682,t644]) ).
cnf(t700,plain,
inverse(divide(sFlat1,sFlat1)) = divide(sFlat1,sFlat1),
inference(orient,[status(thm)],[t683]) ).
cnf(t2829,plain,
divide(X1,X2) = divide(inverse(divide(sFlat1,inverse(divide(X2,X1)))),divide(sFlat1,divide(sFlat1,sFlat1))),
inference(step,[status(thm)],[t1762,t700]) ).
cnf(t2830,plain,
divide(X1,X2) = divide(inverse(divide(sFlat1,inverse(divide(X2,X1)))),sFlat1),
inference(step,[status(thm)],[t2829,t659]) ).
cnf(t2831,plain,
divide(X1,X2) = inverse(inverse(inverse(divide(X2,X1)))),
inference(step,[status(thm)],[t2830,t871]) ).
cnf(t1853,plain,
inverse(inverse(inverse(divide(X1,X2)))) = divide(X2,X1),
inference(orient,[status(thm)],[t2831]) ).
cnf(t687,plain,
X1 = divide(inverse(inverse(X1)),divide(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t27,t682]) ).
cnf(t766,plain,
divide(inverse(inverse(X1)),divide(sFlat1,sFlat1)) = X1,
inference(orient,[status(thm)],[t687]) ).
cnf(t779,plain,
inverse(divide(X1,divide(sFlat1,sFlat1))) = divide(inverse(X1),divide(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t766,t778]) ).
cnf(t925,plain,
inverse(divide(X1,divide(sFlat1,sFlat1))) = divide(inverse(X1),divide(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t779]) ).
cnf(t1857,plain,
divide(divide(sFlat1,sFlat1),X1) = inverse(inverse(divide(inverse(X1),divide(sFlat1,sFlat1)))),
inference(cp,[status(thm)],[t1853,t925]) ).
cnf(t2832,plain,
divide(divide(sFlat1,sFlat1),X1) = inverse(X1),
inference(step,[status(thm)],[t1857,t778]) ).
cnf(t1889,plain,
divide(divide(sFlat1,sFlat1),X1) = inverse(X1),
inference(orient,[status(thm)],[t2832]) ).
cnf(t1906,plain,
divide(sFlat1,sFlat1) = inverse(divide(X1,divide(inverse(divide(sFlat1,X1)),sFlat1))),
inference(cp,[status(thm)],[t114,t1889]) ).
cnf(t2861,plain,
divide(sFlat1,sFlat1) = inverse(divide(X1,inverse(inverse(X1)))),
inference(step,[status(thm)],[t1906,t871]) ).
cnf(t2377,plain,
inverse(divide(X1,inverse(inverse(X1)))) = divide(sFlat1,sFlat1),
inference(orient,[status(thm)],[t2861]) ).
cnf(t2413,plain,
divide(X1,inverse(inverse(X1))) = divide(inverse(divide(sFlat1,sFlat1)),divide(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t766,t2377]) ).
cnf(t2864,plain,
divide(X1,inverse(inverse(X1))) = divide(sFlat1,sFlat1),
inference(step,[status(thm)],[t2413,t1170]) ).
cnf(t2456,plain,
divide(X1,inverse(inverse(X1))) = divide(sFlat1,sFlat1),
inference(orient,[status(thm)],[t2864]) ).
cnf(t2492,plain,
divide(inverse(inverse(X1)),X1) = inverse(inverse(inverse(divide(sFlat1,sFlat1)))),
inference(cp,[status(thm)],[t1853,t2456]) ).
cnf(t2865,plain,
divide(inverse(inverse(X1)),X1) = divide(sFlat1,sFlat1),
inference(step,[status(thm)],[t2492,t1853]) ).
cnf(t2503,plain,
divide(inverse(inverse(X1)),X1) = divide(sFlat1,sFlat1),
inference(orient,[status(thm)],[t2865]) ).
cnf(t2537,plain,
X1 = divide(inverse(divide(sFlat1,sFlat1)),divide(sFlat1,inverse(inverse(divide(X1,sFlat1))))),
inference(cp,[status(thm)],[t27,t2503]) ).
cnf(t2866,plain,
X1 = divide(divide(sFlat1,sFlat1),divide(sFlat1,inverse(inverse(divide(X1,sFlat1))))),
inference(step,[status(thm)],[t2537,t700]) ).
cnf(t2867,plain,
X1 = inverse(divide(sFlat1,inverse(inverse(divide(X1,sFlat1))))),
inference(step,[status(thm)],[t2866,t1889]) ).
cnf(t1856,plain,
divide(X1,sFlat1) = inverse(divide(sFlat1,inverse(inverse(X1)))),
inference(cp,[status(thm)],[t1853,t900]) ).
cnf(t2326,plain,
inverse(divide(sFlat1,inverse(inverse(X1)))) = divide(X1,sFlat1),
inference(orient,[status(thm)],[t1856]) ).
cnf(t2868,plain,
X1 = divide(divide(X1,sFlat1),sFlat1),
inference(step,[status(thm)],[t2867,t2326]) ).
cnf(t1894,plain,
divide(X1,divide(sFlat1,sFlat1)) = inverse(inverse(inverse(inverse(X1)))),
inference(cp,[status(thm)],[t1853,t1889]) ).
cnf(t1868,plain,
divide(divide(X1,sFlat2),a2) = inverse(inverse(inverse(inverse(X1)))),
inference(cp,[status(thm)],[t1853,t946]) ).
cnf(t1915,plain,
inverse(inverse(inverse(inverse(X1)))) = divide(divide(X1,sFlat2),a2),
inference(orient,[status(thm)],[t1868]) ).
cnf(t1878,plain,
divide(divide(X1,sFlat1),sFlat1) = inverse(inverse(inverse(inverse(X1)))),
inference(cp,[status(thm)],[t1853,t682]) ).
cnf(t2837,plain,
divide(divide(X1,sFlat1),sFlat1) = divide(divide(X1,sFlat2),a2),
inference(step,[status(thm)],[t1878,t1915]) ).
cnf(t1980,plain,
divide(divide(X1,sFlat2),a2) = divide(divide(X1,sFlat1),sFlat1),
inference(orient,[status(thm)],[t2837]) ).
cnf(t2838,plain,
inverse(inverse(inverse(inverse(X1)))) = divide(divide(X1,sFlat1),sFlat1),
inference(step,[status(thm)],[t1915,t1980]) ).
cnf(t1981,plain,
inverse(inverse(inverse(inverse(X1)))) = divide(divide(X1,sFlat1),sFlat1),
inference(orient,[status(thm)],[t2838]) ).
cnf(t2841,plain,
divide(X1,divide(sFlat1,sFlat1)) = divide(divide(X1,sFlat1),sFlat1),
inference(step,[status(thm)],[t1894,t1981]) ).
cnf(t2011,plain,
divide(divide(X1,sFlat1),sFlat1) = divide(X1,divide(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t2841]) ).
cnf(t2869,plain,
X1 = divide(X1,divide(sFlat1,sFlat1)),
inference(step,[status(thm)],[t2868,t2011]) ).
cnf(t2548,plain,
divide(X1,divide(sFlat1,sFlat1)) = X1,
inference(orient,[status(thm)],[t2869]) ).
cnf(t2877,plain,
inverse(sFlat0) = b2,
inference(step,[status(thm)],[t752,t2548]) ).
cnf(t2578,plain,
inverse(sFlat0) = b2,
inference(rw,[status(thm)],[t2877]) ).
cnf(t2580,plain,
inverse(sFlat0) = b2,
inference(orient,[status(thm)],[t2578]) ).
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,
inverse(sFlat2) != a2,
inference(rw,[status(thm)],[goal_0,t1430]) ).
cnf(g0_1,plain,
inverse(sFlat2) != divide(divide(inverse(b2),inverse(inverse(sFlat0))),inverse(a2)),
inference(rw,[status(thm)],[g0_0,t2580]) ).
cnf(g0_2,plain,
inverse(sFlat2) != divide(divide(inverse(b2),inverse(inverse(sFlat0))),sFlat2),
inference(rw,[status(thm)],[g0_1,t20]) ).
cnf(g0_3,plain,
inverse(sFlat2) != divide(divide(sFlat0,inverse(inverse(sFlat0))),sFlat2),
inference(rw,[status(thm)],[g0_2,t18]) ).
cnf(g0_4,plain,
inverse(sFlat2) != divide(divide(sFlat1,sFlat1),sFlat2),
inference(rw,[status(thm)],[g0_3,t2456]) ).
cnf(g0_5,plain,
inverse(sFlat2) != inverse(sFlat2),
inference(rw,[status(thm)],[g0_4,t1889]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP470-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n007.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:48:37 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.24/1.88 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.24/1.88 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------