%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP440-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 : n008.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:52 PM UTC 2026
% Result : Unsatisfiable 6.00s 1.51s
% Output : CNFRefutation 6.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 2
% Syntax : Number of clauses : 81 ( 81 unt; 0 nHn; 3 RR)
% Number of literals : 81 ( 80 equ; 2 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 : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 280 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(X4,multiply(X1,X3))))))) = X4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t1,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(X4,multiply(X1,X3))))))) = X4,
inference(orient,[status(thm)],[t0]) ).
cnf(t3,plain,
X1 = inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),multiply(multiply(inverse(X2),X4),inverse(multiply(Y4,multiply(X1,X4))))),Y4)))),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t4,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(multiply(inverse(X1),X3),inverse(multiply(X4,multiply(Y4,X3))))),X4)))) = Y4,
inference(orient,[status(thm)],[t3]) ).
cnf(t7,plain,
X1 = inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),multiply(multiply(inverse(X2),multiply(multiply(inverse(X1),X4),inverse(multiply(Y4,multiply(Y5,X4))))),Y4)),Y5)))),
inference(cp,[status(thm)],[t4,t1]) ).
cnf(t13,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(multiply(inverse(X1),multiply(multiply(inverse(X3),X4),inverse(multiply(Y4,multiply(Y5,X4))))),Y4)),Y5)))) = X3,
inference(orient,[status(thm)],[t7]) ).
cnf(t18,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(X4,multiply(X1,X3)))))) = inverse(multiply(Y4,multiply(Y5,multiply(multiply(inverse(Y5),multiply(multiply(inverse(Y4),multiply(multiply(X4,Y6),inverse(multiply(Y7,multiply(Y8,Y6))))),Y7)),Y8)))),
inference(cp,[status(thm)],[t13,t1]) ).
cnf(t855,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(X4,multiply(X1,X3)))))) = inverse(multiply(Y4,multiply(Y5,multiply(multiply(inverse(Y5),multiply(multiply(inverse(Y4),multiply(multiply(X4,Y6),inverse(multiply(Y7,multiply(Y8,Y6))))),Y7)),Y8)))),
inference(orient,[status(thm)],[t18]) ).
cnf(t1061,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(X4,multiply(X1,X3)))))) = multiply(Y4,multiply(Y5,multiply(multiply(inverse(Y5),Y6),inverse(multiply(X4,multiply(Y4,Y6)))))),
inference(cp,[status(thm)],[t855,t855]) ).
cnf(t1299,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(X4,multiply(X1,X3)))))) = multiply(Y4,multiply(Y5,multiply(multiply(inverse(Y5),Y6),inverse(multiply(X4,multiply(Y4,Y6)))))),
inference(orient,[status(thm)],[t1061]) ).
cnf(t1062,plain,
inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(multiply(inverse(X1),multiply(multiply(inverse(X3),X4),inverse(multiply(Y4,multiply(Y5,X4))))),Y4)),Y5)))) = X3,
inference(rw,[status(thm)],[t13]) ).
cnf(t6878,plain,
multiply(b2,multiply(b2,multiply(multiply(inverse(b2),b2),inverse(multiply(inverse(X3),multiply(b2,b2)))))) = X3,
inference(step,[status(thm)],[t1062,t855]) ).
cnf(t1063,plain,
multiply(b2,multiply(b2,multiply(multiply(inverse(b2),b2),inverse(multiply(inverse(X1),multiply(b2,b2)))))) = X1,
inference(orient,[status(thm)],[t6878]) ).
cnf(t1300,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(inverse(X4),multiply(X1,X3)))))) = X4,
inference(cp,[status(thm)],[t1299,t1063]) ).
cnf(t1390,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X3),inverse(multiply(inverse(X4),multiply(X1,X3)))))) = X4,
inference(orient,[status(thm)],[t1300]) ).
cnf(t1429,plain,
X1 = multiply(X2,multiply(X3,multiply(X4,inverse(multiply(inverse(X1),multiply(X2,multiply(Y4,multiply(multiply(inverse(Y4),Y5),inverse(multiply(inverse(X4),multiply(inverse(X3),Y5))))))))))),
inference(cp,[status(thm)],[t1390,t1390]) ).
cnf(t1601,plain,
multiply(X1,multiply(X2,multiply(X3,inverse(multiply(inverse(X4),multiply(X1,multiply(Y4,multiply(multiply(inverse(Y4),Y5),inverse(multiply(inverse(X3),multiply(inverse(X2),Y5))))))))))) = X4,
inference(orient,[status(thm)],[t1429]) ).
cnf(t1613,plain,
X1 = multiply(inverse(X2),multiply(X2,multiply(X3,inverse(multiply(inverse(X1),X3))))),
inference(cp,[status(thm)],[t1601,t1390]) ).
cnf(t1735,plain,
multiply(inverse(X1),multiply(X1,multiply(X2,inverse(multiply(inverse(X3),X2))))) = X3,
inference(orient,[status(thm)],[t1613]) ).
cnf(t1774,plain,
X1 = multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(X3,inverse(multiply(inverse(X4),X3)))),inverse(X4)))),
inference(cp,[status(thm)],[t1390,t1735]) ).
cnf(t1853,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(X3,inverse(multiply(inverse(X4),X3)))),inverse(X4)))) = X1,
inference(orient,[status(thm)],[t1774]) ).
cnf(t1906,plain,
X1 = inverse(multiply(X2,multiply(X3,multiply(inverse(X3),inverse(multiply(X1,multiply(X2,multiply(X4,multiply(multiply(inverse(X4),multiply(Y4,inverse(multiply(inverse(Y5),Y4)))),inverse(Y5)))))))))),
inference(cp,[status(thm)],[t1,t1853]) ).
cnf(t6881,plain,
X1 = inverse(multiply(X2,multiply(X3,multiply(inverse(X3),inverse(multiply(X1,X2)))))),
inference(step,[status(thm)],[t1906,t1853]) ).
cnf(t2100,plain,
inverse(multiply(X1,multiply(X2,multiply(inverse(X2),inverse(multiply(X3,X1)))))) = X3,
inference(orient,[status(thm)],[t6881]) ).
cnf(t2136,plain,
X1 = inverse(multiply(multiply(X2,multiply(inverse(X2),inverse(multiply(X3,X1)))),multiply(X4,multiply(inverse(X4),X3)))),
inference(cp,[status(thm)],[t2100,t2100]) ).
cnf(t2907,plain,
inverse(multiply(multiply(X1,multiply(inverse(X1),inverse(multiply(X2,X3)))),multiply(X4,multiply(inverse(X4),X2)))) = X3,
inference(orient,[status(thm)],[t2136]) ).
cnf(t1078,plain,
X1 = inverse(multiply(b2,multiply(X2,multiply(multiply(inverse(X2),multiply(b2,multiply(multiply(inverse(b2),b2),inverse(multiply(inverse(X3),multiply(b2,b2)))))),inverse(multiply(X1,X3)))))),
inference(cp,[status(thm)],[t1,t1063]) ).
cnf(t1214,plain,
inverse(multiply(b2,multiply(X1,multiply(multiply(inverse(X1),multiply(b2,multiply(multiply(inverse(b2),b2),inverse(multiply(inverse(X2),multiply(b2,b2)))))),inverse(multiply(X3,X2)))))) = X3,
inference(orient,[status(thm)],[t1078]) ).
cnf(t1880,plain,
X1 = multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(X3,inverse(multiply(X4,X3)))),inverse(multiply(b2,multiply(Y4,multiply(multiply(inverse(Y4),multiply(b2,multiply(multiply(inverse(b2),b2),inverse(multiply(inverse(Y5),multiply(b2,b2)))))),inverse(multiply(X4,Y5))))))))),
inference(cp,[status(thm)],[t1853,t1214]) ).
cnf(t6882,plain,
X1 = multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(X3,inverse(multiply(X4,X3)))),X4))),
inference(step,[status(thm)],[t1880,t1214]) ).
cnf(t2208,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(X3,inverse(multiply(X4,X3)))),X4))) = X1,
inference(orient,[status(thm)],[t6882]) ).
cnf(t2221,plain,
X1 = multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(multiply(X3,multiply(inverse(X3),inverse(multiply(X4,Y4)))),X4)),Y4))),
inference(cp,[status(thm)],[t2208,t2100]) ).
cnf(t3770,plain,
multiply(X1,multiply(X2,multiply(multiply(inverse(X2),multiply(multiply(X3,multiply(inverse(X3),inverse(multiply(X4,Y4)))),X4)),Y4))) = X1,
inference(orient,[status(thm)],[t2221]) ).
cnf(t3773,plain,
X1 = multiply(X1,multiply(X2,multiply(inverse(X2),multiply(multiply(X3,multiply(inverse(X3),inverse(multiply(X4,multiply(Y4,multiply(multiply(inverse(Y4),multiply(Y5,inverse(multiply(Y6,Y5)))),Y6)))))),X4)))),
inference(cp,[status(thm)],[t3770,t2208]) ).
cnf(t6885,plain,
X1 = multiply(X1,multiply(X2,multiply(inverse(X2),multiply(multiply(X3,multiply(inverse(X3),inverse(X4))),X4)))),
inference(step,[status(thm)],[t3773,t2208]) ).
cnf(t3947,plain,
multiply(X1,multiply(X2,multiply(inverse(X2),multiply(multiply(X3,multiply(inverse(X3),inverse(X4))),X4)))) = X1,
inference(orient,[status(thm)],[t6885]) ).
cnf(t1902,plain,
X1 = multiply(X2,multiply(X3,multiply(inverse(X3),inverse(multiply(inverse(X1),multiply(X2,multiply(X4,multiply(multiply(inverse(X4),multiply(Y4,inverse(multiply(inverse(Y5),Y4)))),inverse(Y5))))))))),
inference(cp,[status(thm)],[t1390,t1853]) ).
cnf(t6880,plain,
X1 = multiply(X2,multiply(X3,multiply(inverse(X3),inverse(multiply(inverse(X1),X2))))),
inference(step,[status(thm)],[t1902,t1853]) ).
cnf(t1991,plain,
multiply(X1,multiply(X2,multiply(inverse(X2),inverse(multiply(inverse(X3),X1))))) = X3,
inference(orient,[status(thm)],[t6880]) ).
cnf(t2011,plain,
X1 = multiply(multiply(X1,multiply(X2,inverse(multiply(inverse(X3),X2)))),multiply(X4,multiply(inverse(X4),inverse(X3)))),
inference(cp,[status(thm)],[t1991,t1735]) ).
cnf(t2585,plain,
multiply(multiply(X1,multiply(X2,inverse(multiply(inverse(X3),X2)))),multiply(X4,multiply(inverse(X4),inverse(X3)))) = X1,
inference(orient,[status(thm)],[t2011]) ).
cnf(t2605,plain,
X1 = multiply(multiply(X1,multiply(X2,inverse(multiply(X3,X2)))),multiply(X4,multiply(inverse(X4),inverse(multiply(Y4,multiply(Y5,multiply(inverse(Y5),inverse(multiply(X3,Y4))))))))),
inference(cp,[status(thm)],[t2585,t2100]) ).
cnf(t6884,plain,
X1 = multiply(multiply(X1,multiply(X2,inverse(multiply(X3,X2)))),multiply(X4,multiply(inverse(X4),X3))),
inference(step,[status(thm)],[t2605,t2100]) ).
cnf(t2690,plain,
multiply(multiply(X1,multiply(X2,inverse(multiply(X3,X2)))),multiply(X4,multiply(inverse(X4),X3))) = X1,
inference(orient,[status(thm)],[t6884]) ).
cnf(t3949,plain,
multiply(X1,multiply(X2,inverse(multiply(multiply(multiply(X3,multiply(inverse(X3),inverse(X4))),X4),X2)))) = X1,
inference(cp,[status(thm)],[t3947,t2690]) ).
cnf(t4110,plain,
multiply(X1,multiply(X2,inverse(multiply(multiply(multiply(X3,multiply(inverse(X3),inverse(X4))),X4),X2)))) = X1,
inference(orient,[status(thm)],[t3949]) ).
cnf(t4177,plain,
multiply(multiply(X1,multiply(inverse(X1),inverse(X2))),X2) = inverse(multiply(inverse(X3),X3)),
inference(cp,[status(thm)],[t2100,t4110]) ).
cnf(t4302,plain,
multiply(multiply(X1,multiply(inverse(X1),inverse(X2))),X2) = inverse(multiply(inverse(X3),X3)),
inference(orient,[status(thm)],[t4177]) ).
cnf(t4338,plain,
multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t2907,t4302]) ).
cnf(t4532,plain,
multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X2),X2))),
inference(orient,[status(thm)],[t4338]) ).
cnf(t4774,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(cp,[status(thm)],[t4532,t4532]) ).
cnf(t4775,plain,
multiply(inverse(X1),X1) = multiply(inverse(X2),X2),
inference(orient,[status(thm)],[t4774]) ).
cnf(t4807,plain,
X1 = inverse(multiply(X2,multiply(inverse(multiply(X1,X2)),multiply(inverse(X3),X3)))),
inference(cp,[status(thm)],[t2100,t4775]) ).
cnf(t4927,plain,
inverse(multiply(X1,multiply(inverse(multiply(X2,X1)),multiply(inverse(X3),X3)))) = X2,
inference(orient,[status(thm)],[t4807]) ).
cnf(t4928,plain,
inverse(X1) = inverse(multiply(X1,multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t4927,t4775]) ).
cnf(t5095,plain,
inverse(multiply(X1,multiply(inverse(X2),X2))) = inverse(X1),
inference(orient,[status(thm)],[t4928]) ).
cnf(t5132,plain,
multiply(X1,multiply(inverse(X2),X2)) = multiply(X3,multiply(X4,multiply(multiply(inverse(X4),Y4),inverse(multiply(inverse(X1),multiply(X3,Y4)))))),
inference(cp,[status(thm)],[t1390,t5095]) ).
cnf(t6886,plain,
multiply(X1,multiply(inverse(X2),X2)) = X1,
inference(step,[status(thm)],[t5132,t1390]) ).
cnf(t5239,plain,
multiply(X1,multiply(inverse(X2),X2)) = X1,
inference(orient,[status(thm)],[t6886]) ).
cnf(t5267,plain,
X1 = multiply(X1,inverse(multiply(inverse(X2),X2))),
inference(cp,[status(thm)],[t5239,t5239]) ).
cnf(t5390,plain,
multiply(X1,inverse(multiply(inverse(X2),X2))) = X1,
inference(orient,[status(thm)],[t5267]) ).
cnf(t5432,plain,
X1 = multiply(inverse(X2),multiply(X2,X1)),
inference(cp,[status(thm)],[t1735,t5390]) ).
cnf(t5681,plain,
multiply(inverse(X1),multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t5432]) ).
cnf(t5690,plain,
X1 = inverse(inverse(X1)),
inference(cp,[status(thm)],[t5681,t5239]) ).
cnf(t5860,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t5690]) ).
cnf(t6887,plain,
inverse(multiply(X1,inverse(multiply(X2,X1)))) = X2,
inference(step,[status(thm)],[t4927,t5239]) ).
cnf(t5389,plain,
inverse(multiply(X1,inverse(multiply(X2,X1)))) = X2,
inference(rw,[status(thm)],[t6887]) ).
cnf(t6386,plain,
inverse(multiply(X1,inverse(multiply(X2,X1)))) = X2,
inference(orient,[status(thm)],[t5389]) ).
cnf(t6413,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(cp,[status(thm)],[t5860,t6386]) ).
cnf(t6469,plain,
multiply(X1,inverse(multiply(X2,X1))) = inverse(X2),
inference(orient,[status(thm)],[t6413]) ).
cnf(t6491,plain,
inverse(inverse(X1)) = multiply(multiply(X1,X2),inverse(X2)),
inference(cp,[status(thm)],[t6469,t5681]) ).
cnf(t6905,plain,
X1 = multiply(multiply(X1,X2),inverse(X2)),
inference(step,[status(thm)],[t6491,t5860]) ).
cnf(t6573,plain,
multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(orient,[status(thm)],[t6905]) ).
cnf(t6583,plain,
X1 = multiply(multiply(X1,inverse(X2)),X2),
inference(cp,[status(thm)],[t6573,t5860]) ).
cnf(t6630,plain,
multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(orient,[status(thm)],[t6583]) ).
cnf(t6632,plain,
inverse(inverse(X1)) = multiply(multiply(inverse(X2),X2),X1),
inference(cp,[status(thm)],[t6630,t4775]) ).
cnf(t6906,plain,
X1 = multiply(multiply(inverse(X2),X2),X1),
inference(step,[status(thm)],[t6632,t5860]) ).
cnf(t6706,plain,
multiply(multiply(inverse(X1),X1),X2) = X2,
inference(orient,[status(thm)],[t6906]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
a2 != a2,
inference(rw,[status(thm)],[goal_0,t6706]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP440-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.37 % Computer : n008.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 14:46:23 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.00/1.51 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.00/1.51 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------