%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO067-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 : n014.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 12:59:43 PM UTC 2026
% Result : Unsatisfiable 8.34s 1.70s
% Output : CNFRefutation 8.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 2
% Syntax : Number of clauses : 78 ( 78 unt; 0 nHn; 5 RR)
% Number of literals : 78 ( 77 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-3 aty)
% Number of variables : 297 ( 9 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
multiply(multiply(X1,inverse(X1),X2),inverse(multiply(multiply(X3,X4,X5),X6,multiply(X3,X4,X7))),multiply(X4,multiply(X7,X6,X5),X3)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,plain,
multiply(multiply(X1,inverse(X1),X2),inverse(multiply(multiply(X3,X4,X5),X6,multiply(X3,X4,X7))),multiply(X4,multiply(X7,X6,X5),X3)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t5,plain,
X1 = multiply(multiply(X2,inverse(X2),X1),inverse(multiply(multiply(X3,X4,multiply(X5,multiply(X6,X7,Y7),Y8)),inverse(multiply(multiply(Y8,X5,Y7),X7,multiply(Y8,X5,X6))),multiply(X3,X4,multiply(Y9,inverse(Y9),Y10)))),multiply(X4,Y10,X3)),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t14,plain,
multiply(multiply(X1,inverse(X1),X2),inverse(multiply(multiply(X3,X4,multiply(X5,multiply(X6,X7,Y7),Y8)),inverse(multiply(multiply(Y8,X5,Y7),X7,multiply(Y8,X5,X6))),multiply(X3,X4,multiply(Y9,inverse(Y9),Y10)))),multiply(X4,Y10,X3)) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t30,plain,
X1 = multiply(multiply(X2,inverse(X2),X1),inverse(multiply(X3,multiply(multiply(X4,inverse(X4),inverse(X3)),inverse(multiply(multiply(X5,X6,X7),Y7,multiply(X5,X6,Y8))),multiply(X6,multiply(Y8,Y7,X7),X5)),multiply(Y9,inverse(Y9),Y10))),multiply(inverse(X3),Y10,X3)),
inference(cp,[status(thm)],[t14,t14]) ).
cnf(t774,plain,
X1 = multiply(multiply(X2,inverse(X2),X1),inverse(multiply(X3,inverse(X3),multiply(Y9,inverse(Y9),Y10))),multiply(inverse(X3),Y10,X3)),
inference(step,[status(thm)],[t30,t1]) ).
cnf(t42,plain,
multiply(multiply(X1,inverse(X1),X2),inverse(multiply(X3,inverse(X3),multiply(X4,inverse(X4),X5))),multiply(inverse(X3),X5,X3)) = X2,
inference(orient,[status(thm)],[t774]) ).
cnf(t46,plain,
multiply(inverse(X1),X2,X1) = multiply(multiply(X3,inverse(X3),X2),inverse(multiply(X4,inverse(X4),multiply(X5,inverse(X5),X6))),multiply(inverse(X4),X6,X4)),
inference(cp,[status(thm)],[t42,t42]) ).
cnf(t775,plain,
multiply(inverse(X1),X2,X1) = X2,
inference(step,[status(thm)],[t46,t42]) ).
cnf(t63,plain,
multiply(inverse(X1),X2,X1) = X2,
inference(orient,[status(thm)],[t775]) ).
cnf(t2,plain,
multiply(X1,multiply(X2,inverse(multiply(X3,X1,X4)),X4),X3) = multiply(multiply(X3,X1,X2),inverse(multiply(multiply(X5,X6,X7),Y7,multiply(X5,X6,Y8))),multiply(X6,multiply(Y8,Y7,X7),X5)),
inference(cp,[status(thm)],[t1,t1]) ).
cnf(t6,plain,
multiply(X1,multiply(X2,inverse(multiply(X3,X1,X4)),X4),X3) = multiply(multiply(X3,X1,X2),inverse(multiply(multiply(X5,X6,X7),Y7,multiply(X5,X6,Y8))),multiply(X6,multiply(Y8,Y7,X7),X5)),
inference(orient,[status(thm)],[t2]) ).
cnf(t65,plain,
multiply(X1,inverse(multiply(X2,inverse(X2),X3)),X3) = multiply(multiply(X2,inverse(X2),X1),inverse(multiply(multiply(X4,X5,X6),X7,multiply(X4,X5,Y7))),multiply(X5,multiply(Y7,X7,X6),X4)),
inference(cp,[status(thm)],[t63,t6]) ).
cnf(t777,plain,
multiply(X1,inverse(multiply(X2,inverse(X2),X3)),X3) = X1,
inference(step,[status(thm)],[t65,t1]) ).
cnf(t82,plain,
multiply(X1,inverse(multiply(X2,inverse(X2),X3)),X3) = X1,
inference(orient,[status(thm)],[t777]) ).
cnf(t84,plain,
inverse(X1) = inverse(multiply(X2,inverse(X2),X1)),
inference(cp,[status(thm)],[t82,t63]) ).
cnf(t99,plain,
inverse(multiply(X1,inverse(X1),X2)) = inverse(X2),
inference(orient,[status(thm)],[t84]) ).
cnf(t778,plain,
multiply(X1,inverse(X3),X3) = X1,
inference(step,[status(thm)],[t82,t99]) ).
cnf(t100,plain,
multiply(X1,inverse(X2),X2) = X1,
inference(rw,[status(thm)],[t778]) ).
cnf(t116,plain,
multiply(X1,inverse(X2),X2) = X1,
inference(orient,[status(thm)],[t100]) ).
cnf(t117,plain,
X1 = multiply(X1,inverse(X2),multiply(X3,inverse(X3),X2)),
inference(cp,[status(thm)],[t116,t99]) ).
cnf(t273,plain,
multiply(X1,inverse(X2),multiply(X3,inverse(X3),X2)) = X1,
inference(orient,[status(thm)],[t117]) ).
cnf(t282,plain,
X1 = multiply(multiply(X2,inverse(X2),X1),inverse(multiply(X3,inverse(X3),X4)),multiply(inverse(X3),multiply(X5,inverse(X5),X4),X3)),
inference(cp,[status(thm)],[t1,t273]) ).
cnf(t779,plain,
X1 = multiply(multiply(X2,inverse(X2),X1),inverse(X4),multiply(inverse(X3),multiply(X5,inverse(X5),X4),X3)),
inference(step,[status(thm)],[t282,t99]) ).
cnf(t780,plain,
X1 = multiply(multiply(X2,inverse(X2),X1),inverse(X4),multiply(X5,inverse(X5),X4)),
inference(step,[status(thm)],[t779,t63]) ).
cnf(t781,plain,
X1 = multiply(X2,inverse(X2),X1),
inference(step,[status(thm)],[t780,t273]) ).
cnf(t303,plain,
multiply(X1,inverse(X1),X2) = X2,
inference(orient,[status(thm)],[t781]) ).
cnf(t782,plain,
multiply(X2,inverse(multiply(multiply(X3,X4,X5),X6,multiply(X3,X4,X7))),multiply(X4,multiply(X7,X6,X5),X3)) = X2,
inference(step,[status(thm)],[t1,t303]) ).
cnf(t304,plain,
multiply(X1,inverse(multiply(multiply(X2,X3,X4),X5,multiply(X2,X3,X6))),multiply(X3,multiply(X6,X5,X4),X2)) = X1,
inference(rw,[status(thm)],[t782]) ).
cnf(t376,plain,
multiply(X1,inverse(multiply(multiply(X2,X3,X4),X5,multiply(X2,X3,X6))),multiply(X3,multiply(X6,X5,X4),X2)) = X1,
inference(orient,[status(thm)],[t304]) ).
cnf(t393,plain,
multiply(multiply(X1,X2,X3),X4,multiply(X1,X2,X5)) = multiply(X2,multiply(X5,X4,X3),X1),
inference(cp,[status(thm)],[t376,t303]) ).
cnf(t408,plain,
multiply(multiply(X1,X2,X3),X4,multiply(X1,X2,X5)) = multiply(X2,multiply(X5,X4,X3),X1),
inference(orient,[status(thm)],[t393]) ).
cnf(t313,plain,
multiply(multiply(X1,X2,multiply(X1,X2,X3)),inverse(multiply(multiply(X4,X5,X6),X7,multiply(X4,X5,Y7))),multiply(X5,multiply(Y7,X7,X6),X4)) = multiply(X2,X3,X1),
inference(cp,[status(thm)],[t6,t303]) ).
cnf(t124,plain,
multiply(multiply(X1,inverse(X2),X3),inverse(multiply(multiply(X4,X5,X6),X7,multiply(X4,X5,Y7))),multiply(X5,multiply(Y7,X7,X6),X4)) = multiply(inverse(X2),multiply(X3,inverse(X1),X2),X1),
inference(cp,[status(thm)],[t6,t116]) ).
cnf(t794,plain,
multiply(multiply(X1,inverse(X2),X3),inverse(multiply(X5,multiply(Y7,X7,X6),X4)),multiply(X5,multiply(Y7,X7,X6),X4)) = multiply(inverse(X2),multiply(X3,inverse(X1),X2),X1),
inference(step,[status(thm)],[t124,t408]) ).
cnf(t795,plain,
multiply(X1,inverse(X2),X3) = multiply(inverse(X2),multiply(X3,inverse(X1),X2),X1),
inference(step,[status(thm)],[t794,t116]) ).
cnf(t436,plain,
multiply(inverse(X1),multiply(X2,inverse(X3),X1),X3) = multiply(X3,inverse(X1),X2),
inference(orient,[status(thm)],[t795]) ).
cnf(t437,plain,
multiply(X1,inverse(X2),X1) = multiply(inverse(X2),X2,X1),
inference(cp,[status(thm)],[t436,t303]) ).
cnf(t310,plain,
X1 = inverse(inverse(X1)),
inference(cp,[status(thm)],[t303,t63]) ).
cnf(t314,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t310]) ).
cnf(t321,plain,
X1 = multiply(inverse(X2),X2,X1),
inference(cp,[status(thm)],[t303,t314]) ).
cnf(t372,plain,
multiply(inverse(X1),X1,X2) = X2,
inference(orient,[status(thm)],[t321]) ).
cnf(t799,plain,
multiply(X1,inverse(X2),X1) = X1,
inference(step,[status(thm)],[t437,t372]) ).
cnf(t457,plain,
multiply(X1,inverse(X2),X1) = X1,
inference(orient,[status(thm)],[t799]) ).
cnf(t458,plain,
X1 = multiply(X1,X2,X1),
inference(cp,[status(thm)],[t457,t314]) ).
cnf(t461,plain,
multiply(X1,X2,X1) = X1,
inference(orient,[status(thm)],[t458]) ).
cnf(t464,plain,
multiply(X1,multiply(X2,X3,X4),X2) = multiply(multiply(X2,X1,X4),X3,X2),
inference(cp,[status(thm)],[t408,t461]) ).
cnf(t419,plain,
multiply(inverse(X1),multiply(X2,X3,X4),X1) = multiply(X4,X3,multiply(X1,inverse(X1),X2)),
inference(cp,[status(thm)],[t408,t303]) ).
cnf(t792,plain,
multiply(X2,X3,X4) = multiply(X4,X3,multiply(X1,inverse(X1),X2)),
inference(step,[status(thm)],[t419,t63]) ).
cnf(t793,plain,
multiply(X2,X3,X4) = multiply(X4,X3,X2),
inference(step,[status(thm)],[t792,t303]) ).
cnf(t428,plain,
multiply(X1,X2,X3) = multiply(X3,X2,X1),
inference(orient,[status(thm)],[t793]) ).
cnf(t802,plain,
multiply(X1,multiply(X2,X3,X4),X2) = multiply(X2,X3,multiply(X2,X1,X4)),
inference(step,[status(thm)],[t464,t428]) ).
cnf(t493,plain,
multiply(X1,multiply(X2,X3,X4),X2) = multiply(X2,X3,multiply(X2,X1,X4)),
inference(orient,[status(thm)],[t802]) ).
cnf(t319,plain,
X1 = multiply(X2,X1,inverse(X2)),
inference(cp,[status(thm)],[t63,t314]) ).
cnf(t353,plain,
multiply(X1,X2,inverse(X1)) = X2,
inference(orient,[status(thm)],[t319]) ).
cnf(t440,plain,
multiply(X1,inverse(inverse(X2)),X2) = multiply(inverse(inverse(X2)),inverse(X1),X1),
inference(cp,[status(thm)],[t436,t353]) ).
cnf(t796,plain,
multiply(X1,X2,X2) = multiply(inverse(inverse(X2)),inverse(X1),X1),
inference(step,[status(thm)],[t440,t314]) ).
cnf(t797,plain,
multiply(X1,X2,X2) = inverse(inverse(X2)),
inference(step,[status(thm)],[t796,t116]) ).
cnf(t798,plain,
multiply(X1,X2,X2) = X2,
inference(step,[status(thm)],[t797,t314]) ).
cnf(t447,plain,
multiply(X1,X2,X2) = X2,
inference(orient,[status(thm)],[t798]) ).
cnf(t449,plain,
X1 = multiply(X1,X1,X2),
inference(cp,[status(thm)],[t447,t428]) ).
cnf(t453,plain,
multiply(X1,X1,X2) = X1,
inference(orient,[status(thm)],[t449]) ).
cnf(t503,plain,
multiply(X1,X2,multiply(X1,multiply(X1,X2,X3),X3)) = multiply(X1,X2,X3),
inference(cp,[status(thm)],[t493,t453]) ).
cnf(t452,plain,
multiply(X1,multiply(X1,X2,X3),X4) = multiply(multiply(X4,X1,X3),X2,X1),
inference(cp,[status(thm)],[t408,t447]) ).
cnf(t801,plain,
multiply(X1,multiply(X1,X2,X3),X4) = multiply(X1,X2,multiply(X4,X1,X3)),
inference(step,[status(thm)],[t452,t428]) ).
cnf(t481,plain,
multiply(X1,multiply(X1,X2,X3),X4) = multiply(X1,X2,multiply(X4,X1,X3)),
inference(orient,[status(thm)],[t801]) ).
cnf(t803,plain,
multiply(X1,X2,multiply(X1,X2,multiply(X3,X1,X3))) = multiply(X1,X2,X3),
inference(step,[status(thm)],[t503,t481]) ).
cnf(t804,plain,
multiply(X1,X2,multiply(X1,X2,X3)) = multiply(X1,X2,X3),
inference(step,[status(thm)],[t803,t461]) ).
cnf(t553,plain,
multiply(X1,X2,multiply(X1,X2,X3)) = multiply(X1,X2,X3),
inference(orient,[status(thm)],[t804]) ).
cnf(t808,plain,
multiply(multiply(X1,X2,X3),inverse(multiply(multiply(X4,X5,X6),X7,multiply(X4,X5,Y7))),multiply(X5,multiply(Y7,X7,X6),X4)) = multiply(X2,X3,X1),
inference(step,[status(thm)],[t313,t553]) ).
cnf(t809,plain,
multiply(multiply(X1,X2,X3),inverse(multiply(X5,multiply(Y7,X7,X6),X4)),multiply(X5,multiply(Y7,X7,X6),X4)) = multiply(X2,X3,X1),
inference(step,[status(thm)],[t808,t408]) ).
cnf(t810,plain,
multiply(X1,X2,X3) = multiply(X2,X3,X1),
inference(step,[status(thm)],[t809,t116]) ).
cnf(t744,plain,
multiply(X1,X2,X3) = multiply(X2,X3,X1),
inference(orient,[status(thm)],[t810]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(d,e,a),b,multiply(d,e,c)) != multiply(d,e,multiply(a,b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(e,multiply(c,b,a),d) != multiply(d,e,multiply(a,b,c)),
inference(rw,[status(thm)],[goal_0,t408]) ).
cnf(g0_1,plain,
multiply(e,multiply(c,b,a),d) != multiply(e,multiply(a,b,c),d),
inference(rw,[status(thm)],[g0_0,t744]) ).
cnf(g0_2,plain,
multiply(e,multiply(c,b,a),d) != multiply(e,multiply(c,b,a),d),
inference(rw,[status(thm)],[g0_1,t428]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO067-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 06:42:02 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.34/1.70 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.34/1.70 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------