%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP425-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 : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:26:50 PM UTC 2026
% Result : Unsatisfiable 13.99s 2.34s
% Output : CNFRefutation 13.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 4
% Syntax : Number of clauses : 110 ( 110 unt; 0 nHn; 25 RR)
% Number of literals : 110 ( 109 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 150 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(t4,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(t1,axiom,
sFlat0 = inverse(b2),
introduced(definition) ).
cnf(t8,plain,
inverse(b2) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t10,plain,
X1 = multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sFlat0))),inverse(multiply(inverse(b2),b2))),
inference(cp,[status(thm)],[t4,t8]) ).
cnf(t3137,plain,
X1 = multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sFlat0))),inverse(multiply(sFlat0,b2))),
inference(step,[status(thm)],[t10,t8]) ).
cnf(t2,axiom,
sFlat1 = multiply(inverse(b2),b2),
introduced(definition) ).
cnf(t3134,plain,
sFlat1 = multiply(sFlat0,b2),
inference(step,[status(thm)],[t2,t8]) ).
cnf(t12,plain,
multiply(sFlat0,b2) = sFlat1,
inference(orient,[status(thm)],[t3134]) ).
cnf(t3138,plain,
X1 = multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X1),b2)))),multiply(X2,sFlat0))),inverse(sFlat1)),
inference(step,[status(thm)],[t3137,t12]) ).
cnf(t14,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),b2)))),multiply(X1,sFlat0))),inverse(sFlat1)) = X2,
inference(orient,[status(thm)],[t3138]) ).
cnf(t17,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),b2)))),multiply(X1,sFlat0)) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1)))),
inference(cp,[status(thm)],[t4,t14]) ).
cnf(t270,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),b2)))),multiply(X1,sFlat0)) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1)))),
inference(orient,[status(thm)],[t17]) ).
cnf(t284,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2)))),multiply(X1,sFlat0)) = X2,
inference(cp,[status(thm)],[t270,t4]) ).
cnf(t312,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2)))),multiply(X1,sFlat0)) = X2,
inference(orient,[status(thm)],[t284]) ).
cnf(t315,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(multiply(X1,sFlat0))))),inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),
inference(cp,[status(thm)],[t4,t312]) ).
cnf(t343,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(X3,sFlat0))))),inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,sFlat0)))) = multiply(X3,inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))),
inference(orient,[status(thm)],[t315]) ).
cnf(t345,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X1,sFlat0))),inverse(sFlat1))),b2))) = X2,
inference(cp,[status(thm)],[t343,t4]) ).
cnf(t386,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X1,sFlat0))),inverse(sFlat1))),b2))) = X2,
inference(orient,[status(thm)],[t345]) ).
cnf(t400,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,sFlat0))),inverse(sFlat1))),b2)),b2)))),multiply(X1,sFlat0)) = multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1)))),
inference(cp,[status(thm)],[t270,t386]) ).
cnf(t859,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),multiply(X3,sFlat0))),inverse(sFlat1))),b2)),b2)))),multiply(X1,sFlat0)) = multiply(inverse(multiply(inverse(X2),multiply(X3,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1)))),
inference(orient,[status(thm)],[t400]) ).
cnf(t880,plain,
multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,sFlat0))),inverse(sFlat1))),b2) = multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1))))),inverse(sFlat1)),
inference(cp,[status(thm)],[t14,t859]) ).
cnf(t888,plain,
multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1))))),inverse(sFlat1)) = multiply(inverse(multiply(inverse(multiply(inverse(X1),multiply(X2,sFlat0))),inverse(sFlat1))),b2),
inference(orient,[status(thm)],[t880]) ).
cnf(t16,plain,
b2 = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sFlat0,b2)))),multiply(X1,sFlat0))),inverse(sFlat1)),
inference(cp,[status(thm)],[t14,t8]) ).
cnf(t3139,plain,
b2 = multiply(inverse(multiply(inverse(multiply(X1,inverse(sFlat1))),multiply(X1,sFlat0))),inverse(sFlat1)),
inference(step,[status(thm)],[t16,t12]) ).
cnf(t19,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(sFlat1))),multiply(X1,sFlat0))),inverse(sFlat1)) = b2,
inference(orient,[status(thm)],[t3139]) ).
cnf(t22,plain,
multiply(inverse(multiply(X1,inverse(sFlat1))),multiply(X1,sFlat0)) = multiply(inverse(multiply(inverse(multiply(X2,inverse(b2))),multiply(X2,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1)))),
inference(cp,[status(thm)],[t4,t19]) ).
cnf(t3146,plain,
multiply(inverse(multiply(X1,inverse(sFlat1))),multiply(X1,sFlat0)) = multiply(inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1)))),
inference(step,[status(thm)],[t22,t8]) ).
cnf(t146,plain,
multiply(inverse(multiply(X1,inverse(sFlat1))),multiply(X1,sFlat0)) = multiply(inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,inverse(inverse(sFlat1))))),inverse(multiply(inverse(inverse(sFlat1)),inverse(sFlat1)))),
inference(orient,[status(thm)],[t3146]) ).
cnf(t894,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0))),inverse(sFlat1))),b2) = multiply(inverse(multiply(inverse(multiply(X2,inverse(sFlat1))),multiply(X2,sFlat0))),inverse(sFlat1)),
inference(cp,[status(thm)],[t888,t146]) ).
cnf(t3155,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0))),inverse(sFlat1))),b2) = b2,
inference(step,[status(thm)],[t894,t19]) ).
cnf(t921,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0))),inverse(sFlat1))),b2) = b2,
inference(orient,[status(thm)],[t3155]) ).
cnf(t923,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)) = multiply(inverse(multiply(X2,inverse(b2))),multiply(X2,sFlat0)),
inference(cp,[status(thm)],[t312,t921]) ).
cnf(t3156,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)) = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,sFlat0)),
inference(step,[status(thm)],[t923,t8]) ).
cnf(t934,plain,
multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)) = multiply(inverse(multiply(X2,sFlat0)),multiply(X2,sFlat0)),
inference(orient,[status(thm)],[t3156]) ).
cnf(t935,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))) = multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(multiply(X1,sFlat0))))),inverse(multiply(inverse(multiply(Y3,sFlat0)),multiply(Y3,sFlat0)))),
inference(cp,[status(thm)],[t343,t934]) ).
cnf(t1250,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(multiply(X3,sFlat0))))),inverse(multiply(inverse(multiply(Y3,sFlat0)),multiply(Y3,sFlat0)))) = multiply(X3,inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))),
inference(orient,[status(thm)],[t935]) ).
cnf(t1281,plain,
multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(X1),inverse(sFlat1))),b2))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),sFlat0)))),multiply(X2,inverse(sFlat0)))),inverse(X1))),X3)),inverse(multiply(inverse(multiply(Y3,sFlat0)),multiply(Y3,sFlat0)))),
inference(cp,[status(thm)],[t1250,t4]) ).
cnf(t2603,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),sFlat0)))),multiply(X1,inverse(sFlat0)))),inverse(X3))),X2)),inverse(multiply(inverse(multiply(Y3,sFlat0)),multiply(Y3,sFlat0)))) = multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(X3),inverse(sFlat1))),b2))),
inference(orient,[status(thm)],[t1281]) ).
cnf(t2604,plain,
multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,sFlat0)))),
inference(cp,[status(thm)],[t2603,t4]) ).
cnf(t9,plain,
b2 = multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sFlat0,X2)))),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t4,t8]) ).
cnf(t31,plain,
multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sFlat0,X2)))),multiply(X1,inverse(X2)))),inverse(multiply(inverse(X2),X2))) = b2,
inference(orient,[status(thm)],[t9]) ).
cnf(t1279,plain,
multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(X1),inverse(sFlat1))),b2))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(sFlat0,sFlat0)))),multiply(X2,inverse(sFlat0)))),inverse(X1))),b2)),inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,sFlat0)))),
inference(cp,[status(thm)],[t1250,t31]) ).
cnf(t2133,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(sFlat0,sFlat0)))),multiply(X1,inverse(sFlat0)))),inverse(X2))),b2)),inverse(multiply(inverse(multiply(X3,sFlat0)),multiply(X3,sFlat0)))) = multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))),
inference(orient,[status(thm)],[t1279]) ).
cnf(t2134,plain,
multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(multiply(inverse(b2),b2)),inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),
inference(cp,[status(thm)],[t2133,t31]) ).
cnf(t3174,plain,
multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(multiply(sFlat0,b2)),inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),
inference(step,[status(thm)],[t2134,t8]) ).
cnf(t3175,plain,
multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),
inference(step,[status(thm)],[t3174,t12]) ).
cnf(t2165,plain,
multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(multiply(inverse(sFlat0),sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(X1,sFlat0)),multiply(X1,sFlat0)))),
inference(orient,[status(thm)],[t3175]) ).
cnf(t3177,plain,
multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)))) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,sFlat0)))),
inference(step,[status(thm)],[t2604,t2165]) ).
cnf(t2642,plain,
multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(multiply(X2,sFlat0)),multiply(X2,sFlat0)))) = multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)))),
inference(orient,[status(thm)],[t3177]) ).
cnf(t2643,plain,
multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)))) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),inverse(sFlat1))),b2))),
inference(cp,[status(thm)],[t2642,t1250]) ).
cnf(t2674,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0)))),
inference(orient,[status(thm)],[t2643]) ).
cnf(t2682,plain,
multiply(X1,sFlat0) = multiply(inverse(multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0))))),multiply(X1,sFlat0)),
inference(cp,[status(thm)],[t312,t2674]) ).
cnf(t2718,plain,
multiply(inverse(multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0))))),multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t2682]) ).
cnf(t895,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sFlat0))),inverse(sFlat1))),b2) = multiply(inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),b2)))),multiply(X3,sFlat0))),inverse(sFlat1)),
inference(cp,[status(thm)],[t888,t270]) ).
cnf(t3157,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sFlat0))),inverse(sFlat1))),b2) = X2,
inference(step,[status(thm)],[t895,t14]) ).
cnf(t971,plain,
multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sFlat0))),inverse(sFlat1))),b2) = X2,
inference(orient,[status(thm)],[t3157]) ).
cnf(t1000,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sFlat0)) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,sFlat0)),
inference(cp,[status(thm)],[t312,t971]) ).
cnf(t1011,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sFlat0)) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,sFlat0)),
inference(orient,[status(thm)],[t1000]) ).
cnf(t2719,plain,
multiply(inverse(sFlat1),sFlat0) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0))))),multiply(X1,sFlat0)),
inference(cp,[status(thm)],[t2718,t1011]) ).
cnf(t2749,plain,
multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0))))),multiply(X1,sFlat0)) = multiply(inverse(sFlat1),sFlat0),
inference(orient,[status(thm)],[t2719]) ).
cnf(t2753,plain,
multiply(inverse(sFlat1),sFlat0) = multiply(inverse(multiply(inverse(sFlat1),inverse(multiply(inverse(multiply(sFlat0,sFlat0)),multiply(sFlat0,sFlat0))))),multiply(inverse(multiply(inverse(X1),X1)),sFlat0)),
inference(cp,[status(thm)],[t2749,t2642]) ).
cnf(t3179,plain,
multiply(inverse(sFlat1),sFlat0) = multiply(inverse(multiply(inverse(X1),X1)),sFlat0),
inference(step,[status(thm)],[t2753,t2718]) ).
cnf(t2776,plain,
multiply(inverse(multiply(inverse(X1),X1)),sFlat0) = multiply(inverse(sFlat1),sFlat0),
inference(orient,[status(thm)],[t3179]) ).
cnf(t2781,plain,
multiply(inverse(X1),X1) = multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(sFlat1),sFlat0)))),multiply(X2,inverse(sFlat0)))),inverse(multiply(inverse(sFlat0),sFlat0))),
inference(cp,[status(thm)],[t4,t2776]) ).
cnf(t3181,plain,
multiply(inverse(X1),X1) = sFlat1,
inference(step,[status(thm)],[t2781,t4]) ).
cnf(t2837,plain,
multiply(inverse(X1),X1) = sFlat1,
inference(orient,[status(thm)],[t3181]) ).
cnf(t3208,plain,
multiply(inverse(multiply(inverse(sFlat1),inverse(sFlat1))),multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(step,[status(thm)],[t2718,t2837]) ).
cnf(t2910,plain,
multiply(inverse(multiply(inverse(sFlat1),inverse(sFlat1))),multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(rw,[status(thm)],[t3208]) ).
cnf(t2969,plain,
multiply(inverse(multiply(inverse(sFlat1),inverse(sFlat1))),multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t2910]) ).
cnf(t3194,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(sFlat1),inverse(sFlat1)),
inference(step,[status(thm)],[t2674,t2837]) ).
cnf(t2850,plain,
multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,sFlat0)),inverse(sFlat1))),b2))) = multiply(inverse(sFlat1),inverse(sFlat1)),
inference(orient,[status(thm)],[t3194]) ).
cnf(t2856,plain,
multiply(inverse(sFlat1),inverse(sFlat1)) = multiply(inverse(sFlat0),inverse(multiply(inverse(multiply(inverse(sFlat1),inverse(sFlat1))),b2))),
inference(cp,[status(thm)],[t2850,t2837]) ).
cnf(t3212,plain,
multiply(inverse(multiply(inverse(sFlat1),inverse(sFlat1))),b2) = b2,
inference(step,[status(thm)],[t921,t2837]) ).
cnf(t2912,plain,
multiply(inverse(multiply(inverse(sFlat1),inverse(sFlat1))),b2) = b2,
inference(rw,[status(thm)],[t3212]) ).
cnf(t2940,plain,
multiply(inverse(multiply(inverse(sFlat1),inverse(sFlat1))),b2) = b2,
inference(orient,[status(thm)],[t2912]) ).
cnf(t3255,plain,
multiply(inverse(sFlat1),inverse(sFlat1)) = multiply(inverse(sFlat0),inverse(b2)),
inference(step,[status(thm)],[t2856,t2940]) ).
cnf(t3256,plain,
multiply(inverse(sFlat1),inverse(sFlat1)) = multiply(inverse(sFlat0),sFlat0),
inference(step,[status(thm)],[t3255,t8]) ).
cnf(t3257,plain,
multiply(inverse(sFlat1),inverse(sFlat1)) = sFlat1,
inference(step,[status(thm)],[t3256,t2837]) ).
cnf(t2991,plain,
multiply(inverse(sFlat1),inverse(sFlat1)) = sFlat1,
inference(orient,[status(thm)],[t3257]) ).
cnf(t3260,plain,
multiply(inverse(sFlat1),multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(step,[status(thm)],[t2969,t2991]) ).
cnf(t2997,plain,
multiply(inverse(sFlat1),multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(rw,[status(thm)],[t3260]) ).
cnf(t3010,plain,
multiply(inverse(sFlat1),multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t2997]) ).
cnf(t2889,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sFlat0)) = multiply(inverse(sFlat1),multiply(inverse(inverse(X2)),sFlat0)),
inference(cp,[status(thm)],[t1011,t2837]) ).
cnf(t2973,plain,
multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,sFlat0)) = multiply(inverse(sFlat1),multiply(inverse(inverse(X2)),sFlat0)),
inference(orient,[status(thm)],[t2889]) ).
cnf(t3249,plain,
multiply(inverse(sFlat1),multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))),sFlat0)) = X2,
inference(step,[status(thm)],[t312,t2973]) ).
cnf(t2981,plain,
multiply(inverse(sFlat1),multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))),sFlat0)) = X2,
inference(rw,[status(thm)],[t3249]) ).
cnf(t3280,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),inverse(sFlat1))),b2))),sFlat0) = X2,
inference(step,[status(thm)],[t2981,t3010]) ).
cnf(t3069,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),inverse(sFlat1))),b2))),sFlat0) = X1,
inference(orient,[status(thm)],[t3280]) ).
cnf(t3071,plain,
inverse(sFlat1) = multiply(inverse(inverse(multiply(inverse(sFlat1),b2))),sFlat0),
inference(cp,[status(thm)],[t3069,t2837]) ).
cnf(t3261,plain,
multiply(inverse(sFlat1),b2) = b2,
inference(step,[status(thm)],[t2940,t2991]) ).
cnf(t2998,plain,
multiply(inverse(sFlat1),b2) = b2,
inference(rw,[status(thm)],[t3261]) ).
cnf(t2999,plain,
multiply(inverse(sFlat1),b2) = b2,
inference(orient,[status(thm)],[t2998]) ).
cnf(t3281,plain,
inverse(sFlat1) = multiply(inverse(inverse(b2)),sFlat0),
inference(step,[status(thm)],[t3071,t2999]) ).
cnf(t3282,plain,
inverse(sFlat1) = multiply(inverse(sFlat0),sFlat0),
inference(step,[status(thm)],[t3281,t8]) ).
cnf(t3283,plain,
inverse(sFlat1) = sFlat1,
inference(step,[status(thm)],[t3282,t2837]) ).
cnf(t3084,plain,
inverse(sFlat1) = sFlat1,
inference(orient,[status(thm)],[t3283]) ).
cnf(t3285,plain,
multiply(sFlat1,multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(step,[status(thm)],[t3010,t3084]) ).
cnf(t3089,plain,
multiply(sFlat1,multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(rw,[status(thm)],[t3285]) ).
cnf(t3109,plain,
multiply(sFlat1,multiply(X1,sFlat0)) = multiply(X1,sFlat0),
inference(orient,[status(thm)],[t3089]) ).
cnf(t3300,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),sFlat1)),b2))),sFlat0) = X1,
inference(step,[status(thm)],[t3069,t3084]) ).
cnf(t3097,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),sFlat1)),b2))),sFlat0) = X1,
inference(rw,[status(thm)],[t3300]) ).
cnf(t3120,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),sFlat1)),b2))),sFlat0) = X1,
inference(orient,[status(thm)],[t3097]) ).
cnf(t3123,plain,
multiply(inverse(inverse(multiply(inverse(multiply(inverse(X1),sFlat1)),b2))),sFlat0) = multiply(sFlat1,X1),
inference(cp,[status(thm)],[t3109,t3120]) ).
cnf(t3314,plain,
X1 = multiply(sFlat1,X1),
inference(step,[status(thm)],[t3123,t3120]) ).
cnf(t3126,plain,
multiply(sFlat1,X1) = X1,
inference(orient,[status(thm)],[t3314]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(sFlat1,a2) != a2,
inference(rw,[status(thm)],[goal_0,t2837]) ).
cnf(g0_1,plain,
a2 != a2,
inference(rw,[status(thm)],[g0_0,t3126]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP425-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n005.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:43:19 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 13.99/2.34 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.99/2.34 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------