%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n026.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:50 PM UTC 2026
% Result : Unsatisfiable 5.30s 1.36s
% Output : CNFRefutation 5.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 77
% Number of leaves : 6
% Syntax : Number of clauses : 138 ( 138 unt; 0 nHn; 38 RR)
% Number of literals : 138 ( 137 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 15 ( 3 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 : 259 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
sFlat0 = multiply(a3,b3),
introduced(definition) ).
cnf(t12,plain,
multiply(a3,b3) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t2,axiom,
sFlat1 = multiply(multiply(a3,b3),c3),
introduced(definition) ).
cnf(t9,plain,
multiply(multiply(a3,b3),c3) = sFlat1,
inference(orient,[status(thm)],[t2]) ).
cnf(t3457,plain,
multiply(sFlat0,c3) = sFlat1,
inference(step,[status(thm)],[t9,t12]) ).
cnf(t13,plain,
multiply(sFlat0,c3) = sFlat1,
inference(rw,[status(thm)],[t3457]) ).
cnf(t14,plain,
multiply(sFlat0,c3) = sFlat1,
inference(orient,[status(thm)],[t13]) ).
cnf(t3,axiom,
sFlat2 = multiply(b3,c3),
introduced(definition) ).
cnf(t10,plain,
multiply(b3,c3) = sFlat2,
inference(orient,[status(thm)],[t3]) ).
cnf(t4,axiom,
sFlat3 = multiply(a3,multiply(b3,c3)),
introduced(definition) ).
cnf(t3456,plain,
sFlat3 = multiply(a3,sFlat2),
inference(step,[status(thm)],[t4,t10]) ).
cnf(t11,plain,
multiply(a3,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t3456]) ).
cnf(t0,axiom,
multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X3),X3))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t5,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X3),X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t7,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(cp,[status(thm)],[t5,t5]) ).
cnf(t125,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(orient,[status(thm)],[t7]) ).
cnf(t188,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(X2),X3)))),multiply(Y3,inverse(X3))),
inference(cp,[status(thm)],[t125,t125]) ).
cnf(t215,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X3)))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(Y3,inverse(multiply(inverse(X2),X3)))),multiply(Y3,inverse(X3))),
inference(orient,[status(thm)],[t188]) ).
cnf(t159,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))),X3)))),multiply(X1,inverse(X3))) = X2,
inference(cp,[status(thm)],[t125,t5]) ).
cnf(t189,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))),X3)))),multiply(X1,inverse(X3))) = X2,
inference(orient,[status(thm)],[t159]) ).
cnf(t224,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X3),inverse(multiply(inverse(Y3),Y3)))),Y3)))),multiply(X2,inverse(Y3)))))),multiply(X1,inverse(multiply(X2,inverse(Y3))))) = multiply(inverse(multiply(Y4,inverse(X3))),multiply(Y4,inverse(multiply(X2,inverse(Y3))))),
inference(cp,[status(thm)],[t215,t189]) ).
cnf(t3458,plain,
multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(multiply(X2,inverse(Y3))))) = multiply(inverse(multiply(Y4,inverse(X3))),multiply(Y4,inverse(multiply(X2,inverse(Y3))))),
inference(step,[status(thm)],[t224,t189]) ).
cnf(t253,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(X3,inverse(Y3))))) = multiply(inverse(multiply(Y4,inverse(X2))),multiply(Y4,inverse(multiply(X3,inverse(Y3))))),
inference(orient,[status(thm)],[t3458]) ).
cnf(t270,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(Y3),Y4)))),multiply(X3,inverse(Y4)))),inverse(multiply(inverse(Y4),Y4)))))) = multiply(inverse(multiply(Y5,inverse(X2))),multiply(Y5,inverse(Y3))),
inference(cp,[status(thm)],[t253,t5]) ).
cnf(t3459,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(Y3))) = multiply(inverse(multiply(Y5,inverse(X2))),multiply(Y5,inverse(Y3))),
inference(step,[status(thm)],[t270,t5]) ).
cnf(t308,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(X3))),
inference(orient,[status(thm)],[t3459]) ).
cnf(t312,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(X3))) = multiply(inverse(Y3),multiply(inverse(multiply(inverse(multiply(Y4,inverse(multiply(inverse(Y3),X2)))),multiply(Y4,inverse(X2)))),inverse(X3))),
inference(cp,[status(thm)],[t308,t5]) ).
cnf(t1315,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(X3))) = multiply(inverse(Y3),multiply(inverse(multiply(inverse(multiply(Y4,inverse(multiply(inverse(Y3),X2)))),multiply(Y4,inverse(X2)))),inverse(X3))),
inference(orient,[status(thm)],[t312]) ).
cnf(t1386,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(multiply(inverse(X2),X2)))) = multiply(inverse(X3),X3),
inference(cp,[status(thm)],[t1315,t5]) ).
cnf(t1440,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(multiply(inverse(X2),X2)))) = multiply(inverse(X3),X3),
inference(orient,[status(thm)],[t1386]) ).
cnf(t1441,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),Y3)))),multiply(X3,inverse(Y3)))),inverse(multiply(inverse(Y3),Y3)))),
inference(cp,[status(thm)],[t1440,t1315]) ).
cnf(t3460,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(step,[status(thm)],[t1441,t5]) ).
cnf(t1605,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t3460]) ).
cnf(t1612,plain,
X1 = multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))),multiply(X2,inverse(X1)))),inverse(multiply(inverse(X1),X1))),
inference(cp,[status(thm)],[t5,t1605]) ).
cnf(t1901,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X3),X3))) = X3,
inference(orient,[status(thm)],[t1612]) ).
cnf(t205,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))),X3))) = multiply(inverse(multiply(inverse(multiply(Y3,inverse(X2))),multiply(Y3,inverse(multiply(X1,inverse(X3)))))),inverse(multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X3))))),
inference(cp,[status(thm)],[t5,t189]) ).
cnf(t354,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(X3,inverse(Y3)))))),inverse(multiply(inverse(multiply(X3,inverse(Y3))),multiply(X3,inverse(Y3))))) = multiply(X3,inverse(multiply(inverse(multiply(inverse(X2),inverse(multiply(inverse(Y3),Y3)))),Y3))),
inference(orient,[status(thm)],[t205]) ).
cnf(t355,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3))) = X2,
inference(cp,[status(thm)],[t354,t5]) ).
cnf(t422,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X3),X3)))),X3))) = X2,
inference(orient,[status(thm)],[t355]) ).
cnf(t1615,plain,
multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(inverse(X2),X2)))),X2))),
inference(cp,[status(thm)],[t422,t1605]) ).
cnf(t1680,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),inverse(multiply(inverse(X3),X3)))),X3))) = multiply(X1,inverse(X3)),
inference(orient,[status(thm)],[t1615]) ).
cnf(t1690,plain,
multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),inverse(multiply(inverse(Y3),Y3)))),X2))),
inference(cp,[status(thm)],[t1680,t1605]) ).
cnf(t1729,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),inverse(multiply(inverse(X3),X3)))),Y3))) = multiply(X1,inverse(Y3)),
inference(orient,[status(thm)],[t1690]) ).
cnf(t1936,plain,
multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(X3),X3)),X2))),
inference(cp,[status(thm)],[t1729,t1901]) ).
cnf(t1962,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),X2)),X3))) = multiply(X1,inverse(X3)),
inference(orient,[status(thm)],[t1936]) ).
cnf(t2004,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X1))),
inference(cp,[status(thm)],[t189,t1962]) ).
cnf(t3464,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(sFlat0),sFlat0),
inference(step,[status(thm)],[t2004,t1605]) ).
cnf(t2032,plain,
inverse(multiply(inverse(X1),X1)) = multiply(inverse(sFlat0),sFlat0),
inference(orient,[status(thm)],[t3464]) ).
cnf(t3468,plain,
multiply(inverse(multiply(inverse(multiply(X1,multiply(inverse(sFlat0),sFlat0))),multiply(X1,inverse(X3)))),inverse(multiply(inverse(X3),X3))) = X3,
inference(step,[status(thm)],[t1901,t2032]) ).
cnf(t3469,plain,
multiply(inverse(multiply(inverse(multiply(X1,multiply(inverse(sFlat0),sFlat0))),multiply(X1,inverse(X3)))),multiply(inverse(sFlat0),sFlat0)) = X3,
inference(step,[status(thm)],[t3468,t2032]) ).
cnf(t2041,plain,
multiply(inverse(multiply(inverse(multiply(X1,multiply(inverse(sFlat0),sFlat0))),multiply(X1,inverse(X3)))),multiply(inverse(sFlat0),sFlat0)) = X3,
inference(rw,[status(thm)],[t3469]) ).
cnf(t2833,plain,
multiply(inverse(multiply(inverse(multiply(X1,multiply(inverse(sFlat0),sFlat0))),multiply(X1,inverse(X2)))),multiply(inverse(sFlat0),sFlat0)) = X2,
inference(orient,[status(thm)],[t2041]) ).
cnf(t3466,plain,
multiply(X1,inverse(multiply(multiply(inverse(sFlat0),sFlat0),X3))) = multiply(X1,inverse(X3)),
inference(step,[status(thm)],[t1962,t2032]) ).
cnf(t2039,plain,
multiply(X1,inverse(multiply(multiply(inverse(sFlat0),sFlat0),X3))) = multiply(X1,inverse(X3)),
inference(rw,[status(thm)],[t3466]) ).
cnf(t2050,plain,
multiply(X1,inverse(multiply(multiply(inverse(sFlat0),sFlat0),X2))) = multiply(X1,inverse(X2)),
inference(orient,[status(thm)],[t2039]) ).
cnf(t2052,plain,
multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(multiply(inverse(X3),X3),X2))),
inference(cp,[status(thm)],[t2050,t1605]) ).
cnf(t2057,plain,
multiply(X1,inverse(multiply(multiply(inverse(X2),X2),X3))) = multiply(X1,inverse(X3)),
inference(orient,[status(thm)],[t2052]) ).
cnf(t2839,plain,
multiply(multiply(inverse(X1),X1),X2) = multiply(inverse(multiply(inverse(multiply(X3,multiply(inverse(sFlat0),sFlat0))),multiply(X3,inverse(X2)))),multiply(inverse(sFlat0),sFlat0)),
inference(cp,[status(thm)],[t2833,t2057]) ).
cnf(t3489,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(step,[status(thm)],[t2839,t2833]) ).
cnf(t2857,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(orient,[status(thm)],[t3489]) ).
cnf(t2860,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(inverse(X2)),multiply(multiply(inverse(Y3),Y3),inverse(X3))),
inference(cp,[status(thm)],[t308,t2857]) ).
cnf(t3496,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(inverse(X2)),inverse(X3)),
inference(step,[status(thm)],[t2860,t2857]) ).
cnf(t2886,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(inverse(inverse(X2)),inverse(X3)),
inference(orient,[status(thm)],[t3496]) ).
cnf(t2890,plain,
multiply(inverse(inverse(X1)),inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,multiply(inverse(sFlat0),sFlat0))),
inference(cp,[status(thm)],[t2886,t2032]) ).
cnf(t3497,plain,
multiply(inverse(inverse(X1)),multiply(inverse(sFlat0),sFlat0)) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,multiply(inverse(sFlat0),sFlat0))),
inference(step,[status(thm)],[t2890,t2032]) ).
cnf(t2858,plain,
X1 = multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat0)),multiply(multiply(inverse(X2),X2),inverse(X1)))),multiply(inverse(sFlat0),sFlat0)),
inference(cp,[status(thm)],[t2833,t2857]) ).
cnf(t3493,plain,
X1 = multiply(inverse(multiply(multiply(inverse(sFlat0),sFlat0),multiply(multiply(inverse(X2),X2),inverse(X1)))),multiply(inverse(sFlat0),sFlat0)),
inference(step,[status(thm)],[t2858,t2032]) ).
cnf(t3494,plain,
X1 = multiply(inverse(multiply(multiply(inverse(X2),X2),inverse(X1))),multiply(inverse(sFlat0),sFlat0)),
inference(step,[status(thm)],[t3493,t2857]) ).
cnf(t3495,plain,
X1 = multiply(inverse(inverse(X1)),multiply(inverse(sFlat0),sFlat0)),
inference(step,[status(thm)],[t3494,t2857]) ).
cnf(t2875,plain,
multiply(inverse(inverse(X1)),multiply(inverse(sFlat0),sFlat0)) = X1,
inference(orient,[status(thm)],[t3495]) ).
cnf(t3498,plain,
X1 = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,multiply(inverse(sFlat0),sFlat0))),
inference(step,[status(thm)],[t3497,t2875]) ).
cnf(t2892,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(inverse(sFlat0),sFlat0))) = X2,
inference(orient,[status(thm)],[t3498]) ).
cnf(t2877,plain,
X1 = multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t2875,t1605]) ).
cnf(t2881,plain,
multiply(inverse(inverse(X1)),multiply(inverse(X2),X2)) = X1,
inference(orient,[status(thm)],[t2877]) ).
cnf(t2895,plain,
X1 = multiply(inverse(multiply(inverse(inverse(X2)),inverse(X1))),X2),
inference(cp,[status(thm)],[t2892,t2881]) ).
cnf(t2897,plain,
multiply(inverse(multiply(inverse(inverse(X1)),inverse(X2))),X1) = X2,
inference(orient,[status(thm)],[t2895]) ).
cnf(t2888,plain,
multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(X2)) = multiply(inverse(multiply(X3,multiply(inverse(sFlat0),sFlat0))),multiply(X3,inverse(X2))),
inference(cp,[status(thm)],[t2886,t2032]) ).
cnf(t3499,plain,
multiply(inverse(multiply(inverse(sFlat0),sFlat0)),inverse(X2)) = multiply(inverse(multiply(X3,multiply(inverse(sFlat0),sFlat0))),multiply(X3,inverse(X2))),
inference(step,[status(thm)],[t2888,t2032]) ).
cnf(t3500,plain,
multiply(multiply(inverse(sFlat0),sFlat0),inverse(X2)) = multiply(inverse(multiply(X3,multiply(inverse(sFlat0),sFlat0))),multiply(X3,inverse(X2))),
inference(step,[status(thm)],[t3499,t2032]) ).
cnf(t3501,plain,
inverse(X2) = multiply(inverse(multiply(X3,multiply(inverse(sFlat0),sFlat0))),multiply(X3,inverse(X2))),
inference(step,[status(thm)],[t3500,t2857]) ).
cnf(t2909,plain,
multiply(inverse(multiply(X1,multiply(inverse(sFlat0),sFlat0))),multiply(X1,inverse(X2))) = inverse(X2),
inference(orient,[status(thm)],[t3501]) ).
cnf(t2914,plain,
inverse(X1) = multiply(inverse(multiply(inverse(inverse(X1)),multiply(inverse(sFlat0),sFlat0))),multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t2909,t1605]) ).
cnf(t3502,plain,
inverse(X1) = multiply(inverse(X1),multiply(inverse(X2),X2)),
inference(step,[status(thm)],[t2914,t2875]) ).
cnf(t2917,plain,
multiply(inverse(X1),multiply(inverse(X2),X2)) = inverse(X1),
inference(orient,[status(thm)],[t3502]) ).
cnf(t2919,plain,
inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(X2))) = X2,
inference(cp,[status(thm)],[t2917,t2897]) ).
cnf(t3504,plain,
inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat0)),inverse(X2))) = X2,
inference(step,[status(thm)],[t2919,t2032]) ).
cnf(t3505,plain,
inverse(multiply(multiply(inverse(sFlat0),sFlat0),inverse(X2))) = X2,
inference(step,[status(thm)],[t3504,t2032]) ).
cnf(t3506,plain,
inverse(inverse(X2)) = X2,
inference(step,[status(thm)],[t3505,t2857]) ).
cnf(t2928,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t3506]) ).
cnf(t3509,plain,
multiply(inverse(multiply(X1,inverse(X2))),X1) = X2,
inference(step,[status(thm)],[t2897,t2928]) ).
cnf(t2942,plain,
multiply(inverse(multiply(X1,inverse(X2))),X1) = X2,
inference(rw,[status(thm)],[t3509]) ).
cnf(t2933,plain,
inverse(inverse(X1)) = multiply(X1,multiply(inverse(X2),X2)),
inference(cp,[status(thm)],[t2917,t2928]) ).
cnf(t3510,plain,
X1 = multiply(X1,multiply(inverse(X2),X2)),
inference(step,[status(thm)],[t2933,t2928]) ).
cnf(t2943,plain,
multiply(X1,multiply(inverse(X2),X2)) = X1,
inference(orient,[status(thm)],[t3510]) ).
cnf(t3507,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(X2,inverse(X3)),
inference(step,[status(thm)],[t2886,t2928]) ).
cnf(t2929,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))) = multiply(X2,inverse(X3)),
inference(orient,[status(thm)],[t3507]) ).
cnf(t2945,plain,
inverse(multiply(inverse(inverse(X1)),inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t2943,t2929]) ).
cnf(t3513,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(step,[status(thm)],[t2945,t2928]) ).
cnf(t2971,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t3513]) ).
cnf(t3517,plain,
multiply(multiply(X2,inverse(X1)),X1) = X2,
inference(step,[status(thm)],[t2942,t2971]) ).
cnf(t3003,plain,
multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(orient,[status(thm)],[t3517]) ).
cnf(t2974,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t2971,t2928]) ).
cnf(t2984,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t2974]) ).
cnf(t3004,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),X2),
inference(cp,[status(thm)],[t3003,t2984]) ).
cnf(t3054,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t3004]) ).
cnf(t3515,plain,
multiply(multiply(X2,inverse(X1)),multiply(X1,inverse(X3))) = multiply(X2,inverse(X3)),
inference(step,[status(thm)],[t2929,t2971]) ).
cnf(t2983,plain,
multiply(multiply(X2,inverse(X1)),multiply(X1,inverse(X3))) = multiply(X2,inverse(X3)),
inference(rw,[status(thm)],[t3515]) ).
cnf(t3372,plain,
multiply(multiply(X1,inverse(X2)),multiply(X2,inverse(X3))) = multiply(X1,inverse(X3)),
inference(orient,[status(thm)],[t2983]) ).
cnf(t3009,plain,
X1 = multiply(multiply(X1,X2),inverse(X2)),
inference(cp,[status(thm)],[t3003,t2928]) ).
cnf(t3011,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(orient,[status(thm)],[t3009]) ).
cnf(t3018,plain,
b3 = multiply(sFlat2,inverse(c3)),
inference(cp,[status(thm)],[t3011,t10]) ).
cnf(t3028,plain,
multiply(sFlat2,inverse(c3)) = b3,
inference(orient,[status(thm)],[t3018]) ).
cnf(t3377,plain,
multiply(sFlat2,inverse(X1)) = multiply(b3,multiply(c3,inverse(X1))),
inference(cp,[status(thm)],[t3372,t3028]) ).
cnf(t3419,plain,
multiply(b3,multiply(c3,inverse(X1))) = multiply(sFlat2,inverse(X1)),
inference(orient,[status(thm)],[t3377]) ).
cnf(t3015,plain,
sFlat0 = multiply(sFlat1,inverse(c3)),
inference(cp,[status(thm)],[t3011,t14]) ).
cnf(t3022,plain,
multiply(sFlat1,inverse(c3)) = sFlat0,
inference(orient,[status(thm)],[t3015]) ).
cnf(t3023,plain,
multiply(c3,inverse(sFlat1)) = inverse(sFlat0),
inference(cp,[status(thm)],[t2971,t3022]) ).
cnf(t3030,plain,
multiply(c3,inverse(sFlat1)) = inverse(sFlat0),
inference(orient,[status(thm)],[t3023]) ).
cnf(t3420,plain,
multiply(sFlat2,inverse(sFlat1)) = multiply(b3,inverse(sFlat0)),
inference(cp,[status(thm)],[t3419,t3030]) ).
cnf(t3017,plain,
a3 = multiply(sFlat0,inverse(b3)),
inference(cp,[status(thm)],[t3011,t12]) ).
cnf(t3026,plain,
multiply(sFlat0,inverse(b3)) = a3,
inference(orient,[status(thm)],[t3017]) ).
cnf(t3027,plain,
multiply(b3,inverse(sFlat0)) = inverse(a3),
inference(cp,[status(thm)],[t2971,t3026]) ).
cnf(t3040,plain,
multiply(b3,inverse(sFlat0)) = inverse(a3),
inference(orient,[status(thm)],[t3027]) ).
cnf(t3543,plain,
multiply(sFlat2,inverse(sFlat1)) = inverse(a3),
inference(step,[status(thm)],[t3420,t3040]) ).
cnf(t3435,plain,
multiply(sFlat2,inverse(sFlat1)) = inverse(a3),
inference(orient,[status(thm)],[t3543]) ).
cnf(t3442,plain,
inverse(inverse(sFlat1)) = multiply(inverse(inverse(a3)),sFlat2),
inference(cp,[status(thm)],[t3054,t3435]) ).
cnf(t3544,plain,
sFlat1 = multiply(inverse(inverse(a3)),sFlat2),
inference(step,[status(thm)],[t3442,t2928]) ).
cnf(t3545,plain,
sFlat1 = multiply(a3,sFlat2),
inference(step,[status(thm)],[t3544,t2928]) ).
cnf(t3546,plain,
sFlat1 = sFlat3,
inference(step,[status(thm)],[t3545,t11]) ).
cnf(t3450,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t3546]) ).
cnf(t3547,plain,
multiply(a3,sFlat2) = sFlat1,
inference(step,[status(thm)],[t11,t3450]) ).
cnf(t3451,plain,
multiply(a3,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t3547]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(sFlat0,c3) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t12]) ).
cnf(g0_1,plain,
sFlat1 != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[g0_0,t14]) ).
cnf(g0_2,plain,
sFlat1 != multiply(a3,sFlat2),
inference(rw,[status(thm)],[g0_1,t10]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t3451]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.58 % Computer : n026.cluster.edu
% 0.10/0.58 % Model : x86_64 x86_64
% 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.58 % Memory : 8046.5625MB
% 0.10/0.58 % OS : Linux 6.8.0-71-generic
% 0.10/0.58 % CPULimit : 300
% 0.10/0.58 % WCLimit : 300
% 0.10/0.58 % DateTime : Wed Sep 23 14:46:10 UTC 2026
% 0.10/0.58 % CPUTime :
% 0.10/0.58 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.30/1.36 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.30/1.36 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------