%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP441-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 : 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:52 PM UTC 2026
% Result : Unsatisfiable 4.74s 1.40s
% Output : CNFRefutation 4.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 2
% Syntax : Number of clauses : 108 ( 108 unt; 0 nHn; 3 RR)
% Number of literals : 108 ( 107 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 : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 347 ( 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(t8233,plain,
multiply(c3,multiply(c3,multiply(multiply(inverse(c3),c3),inverse(multiply(inverse(X3),multiply(c3,c3)))))) = X3,
inference(step,[status(thm)],[t1062,t855]) ).
cnf(t1063,plain,
multiply(c3,multiply(c3,multiply(multiply(inverse(c3),c3),inverse(multiply(inverse(X1),multiply(c3,c3)))))) = X1,
inference(orient,[status(thm)],[t8233]) ).
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(t8236,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)],[t8236]) ).
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(c3,multiply(X2,multiply(multiply(inverse(X2),multiply(c3,multiply(multiply(inverse(c3),c3),inverse(multiply(inverse(X3),multiply(c3,c3)))))),inverse(multiply(X1,X3)))))),
inference(cp,[status(thm)],[t1,t1063]) ).
cnf(t1214,plain,
inverse(multiply(c3,multiply(X1,multiply(multiply(inverse(X1),multiply(c3,multiply(multiply(inverse(c3),c3),inverse(multiply(inverse(X2),multiply(c3,c3)))))),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(c3,multiply(Y4,multiply(multiply(inverse(Y4),multiply(c3,multiply(multiply(inverse(c3),c3),inverse(multiply(inverse(Y5),multiply(c3,c3)))))),inverse(multiply(X4,Y5))))))))),
inference(cp,[status(thm)],[t1853,t1214]) ).
cnf(t8237,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)],[t8237]) ).
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(t8240,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)],[t8240]) ).
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(t8235,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)],[t8235]) ).
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(t8239,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)],[t8239]) ).
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(t8241,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)],[t8241]) ).
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(t8242,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)],[t8242]) ).
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(t8260,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)],[t8260]) ).
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(t8261,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)],[t8261]) ).
cnf(t6722,plain,
X1 = multiply(multiply(X2,inverse(X2)),X1),
inference(cp,[status(thm)],[t6706,t5860]) ).
cnf(t6878,plain,
multiply(multiply(X1,inverse(X1)),X2) = X2,
inference(orient,[status(thm)],[t6722]) ).
cnf(t6913,plain,
X1 = inverse(multiply(X2,multiply(X3,inverse(multiply(X1,multiply(X2,inverse(inverse(X3)))))))),
inference(cp,[status(thm)],[t1,t6878]) ).
cnf(t6494,plain,
inverse(multiply(X1,X2)) = multiply(inverse(X2),inverse(X1)),
inference(cp,[status(thm)],[t5681,t6469]) ).
cnf(t7027,plain,
multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(orient,[status(thm)],[t6494]) ).
cnf(t5876,plain,
X1 = multiply(X2,multiply(inverse(X2),X1)),
inference(cp,[status(thm)],[t5681,t5860]) ).
cnf(t6252,plain,
multiply(X1,multiply(inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t5876]) ).
cnf(t6496,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(cp,[status(thm)],[t6252,t6469]) ).
cnf(t7109,plain,
inverse(multiply(X1,inverse(X2))) = multiply(X2,inverse(X1)),
inference(orient,[status(thm)],[t6496]) ).
cnf(t7123,plain,
inverse(multiply(X1,multiply(X2,inverse(X3)))) = multiply(multiply(X3,inverse(X2)),inverse(X1)),
inference(cp,[status(thm)],[t7027,t7109]) ).
cnf(t7609,plain,
inverse(multiply(X1,multiply(X2,inverse(X3)))) = multiply(multiply(X3,inverse(X2)),inverse(X1)),
inference(orient,[status(thm)],[t7123]) ).
cnf(t8275,plain,
X1 = multiply(multiply(multiply(X1,multiply(X2,inverse(inverse(X3)))),inverse(X3)),inverse(X2)),
inference(step,[status(thm)],[t6913,t7609]) ).
cnf(t8276,plain,
X1 = multiply(multiply(multiply(X1,multiply(X2,X3)),inverse(X3)),inverse(X2)),
inference(step,[status(thm)],[t8275,t5860]) ).
cnf(t8009,plain,
multiply(multiply(multiply(X1,multiply(X2,X3)),inverse(X3)),inverse(X2)) = X1,
inference(orient,[status(thm)],[t8276]) ).
cnf(t6495,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),inverse(inverse(X2))),
inference(cp,[status(thm)],[t6469,t6469]) ).
cnf(t8273,plain,
inverse(X1) = inverse(multiply(inverse(X2),multiply(X2,X1))),
inference(step,[status(thm)],[t6495,t7027]) ).
cnf(t7042,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(cp,[status(thm)],[t7027,t5860]) ).
cnf(t7172,plain,
inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(orient,[status(thm)],[t7042]) ).
cnf(t8274,plain,
inverse(X1) = multiply(inverse(multiply(X2,X1)),X2),
inference(step,[status(thm)],[t8273,t7172]) ).
cnf(t7268,plain,
multiply(inverse(multiply(X1,X2)),X1) = inverse(X2),
inference(orient,[status(thm)],[t8274]) ).
cnf(t8012,plain,
inverse(multiply(multiply(X1,X2),X3)) = multiply(multiply(inverse(X3),inverse(X2)),inverse(X1)),
inference(cp,[status(thm)],[t8009,t7268]) ).
cnf(t8277,plain,
inverse(multiply(multiply(X1,X2),X3)) = multiply(inverse(multiply(X2,X3)),inverse(X1)),
inference(step,[status(thm)],[t8012,t7027]) ).
cnf(t8278,plain,
inverse(multiply(multiply(X1,X2),X3)) = inverse(multiply(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t8277,t7027]) ).
cnf(t8108,plain,
inverse(multiply(multiply(X1,X2),X3)) = inverse(multiply(X1,multiply(X2,X3))),
inference(orient,[status(thm)],[t8278]) ).
cnf(t8140,plain,
multiply(multiply(X1,X2),X3) = inverse(inverse(multiply(X1,multiply(X2,X3)))),
inference(cp,[status(thm)],[t5860,t8108]) ).
cnf(t8285,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(step,[status(thm)],[t8140,t5860]) ).
cnf(t8204,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t8285]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(rw,[status(thm)],[goal_0,t8204]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP441-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 14:48:54 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.74/1.40 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.74/1.40 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------