%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP014-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 12:32:16 PM UTC 2026
% Result : Unsatisfiable 34.60s 4.97s
% Output : CNFRefutation 32.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 6
% Syntax : Number of formulae : 146 ( 146 unt; 4 def)
% Number of atoms : 146 ( 145 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 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 : 339 ( 339 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,W,Z] : multiply(X,inverse(multiply(multiply(inverse(multiply(inverse(Y),multiply(inverse(X),W))),Z),inverse(multiply(Y,Z))))) = W,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(a,multiply(b,c)) != multiply(multiply(a,b),c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),X3),inverse(multiply(X1,X3))))) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
multiply(a,multiply(b,c)) != multiply(multiply(a,b),c),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f5,definition,
sF1_fnc = multiply(b,c),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f6,definition,
sF0_fnc = multiply(a,sF1_fnc),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f7,definition,
sF3_fnc = multiply(a,b),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f8,definition,
sF2_fnc = multiply(sF3_fnc,c),
introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition]) ).
fof(f9,plain,
sF0_fnc != sF2_fnc,
inference(definition_folding,[],[f4,f8,f7,f6,f5]) ).
fof(f11,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),X5),inverse(multiply(X4,X5)))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f12,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X0),X1))),c),inverse(sF2_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f8,f3]) ).
fof(f13,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X0),X1))),b),inverse(sF3_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f7,f3]) ).
fof(f14,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X0),X1))),sF1_fnc),inverse(sF0_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f6,f3]) ).
fof(f15,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(X0),X1))),c),inverse(sF1_fnc)))) = X1,
inference(paramodulation,[status(thm)],[f5,f3]) ).
fof(f16,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(X3),multiply(inverse(X1),X4))),X5),inverse(multiply(X3,X5))))),inverse(X4)))) = X2,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f17,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f12,f12]) ).
fof(f18,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f3,f12]) ).
fof(f22,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(inverse(X0)),X1))),b),inverse(sF3_fnc))),
inference(paramodulation,[status(thm)],[f13,f13]) ).
fof(f23,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f12,f13]) ).
fof(f30,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),sF1_fnc),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(inverse(X0)),X1))),b),inverse(sF3_fnc))),
inference(paramodulation,[status(thm)],[f13,f14]) ).
fof(f34,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(inverse(X0)),X1))),sF1_fnc),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f14,f13]) ).
fof(f39,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b),X1)),c),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(inverse(X0)),X1))),sF1_fnc),inverse(sF0_fnc))),
inference(paramodulation,[status(thm)],[f14,f15]) ).
fof(f44,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),sF1_fnc),inverse(sF0_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(inverse(X0)),X1))),c),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f15,f14]) ).
fof(f54,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X2)),c),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc))))),X2))),c),inverse(sF2_fnc))),
inference(paramodulation,[status(thm)],[f17,f17]) ).
fof(f55,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc))))) = X1,
inference(paramodulation,[status(thm)],[f17,f12]) ).
fof(f57,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc)))),X2))),c),inverse(sF1_fnc)))) = X2,
inference(paramodulation,[status(thm)],[f17,f15]) ).
fof(f66,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X2)),c),inverse(sF2_fnc)))))) = multiply(inverse(inverse(X1)),X2),
inference(paramodulation,[status(thm)],[f17,f55]) ).
fof(f85,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(inverse(X2)),multiply(inverse(X2),X1)),
inference(paramodulation,[status(thm)],[f12,f66]) ).
fof(f120,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = multiply(inverse(X2),multiply(X2,X1)),
inference(paramodulation,[status(thm)],[f85,f85]) ).
fof(f148,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(X1,X2))),X3),inverse(multiply(inverse(X0),X3))))) = X2,
inference(paramodulation,[status(thm)],[f85,f3]) ).
fof(f171,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))) = multiply(inverse(X3),multiply(X3,multiply(X0,X2))),
inference(paramodulation,[status(thm)],[f120,f120]) ).
fof(f173,plain,
! [X0] : multiply(inverse(sF3_fnc),sF2_fnc) = multiply(inverse(X0),multiply(X0,c)),
inference(paramodulation,[status(thm)],[f8,f120]) ).
fof(f174,plain,
! [X0] : multiply(inverse(a),sF3_fnc) = multiply(inverse(X0),multiply(X0,b)),
inference(paramodulation,[status(thm)],[f7,f120]) ).
fof(f175,plain,
! [X0] : multiply(inverse(a),sF0_fnc) = multiply(inverse(X0),multiply(X0,sF1_fnc)),
inference(paramodulation,[status(thm)],[f6,f120]) ).
fof(f176,plain,
! [X0] : multiply(inverse(b),sF1_fnc) = multiply(inverse(X0),multiply(X0,c)),
inference(paramodulation,[status(thm)],[f5,f120]) ).
fof(f234,plain,
multiply(inverse(sF3_fnc),sF2_fnc) = multiply(inverse(b),sF1_fnc),
inference(paramodulation,[status(thm)],[f5,f173]) ).
fof(f270,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X0),c))),c),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(sF3_fnc),sF2_fnc))),X2),inverse(multiply(X1,X2)))),
inference(paramodulation,[status(thm)],[f173,f18]) ).
fof(f273,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X0),X1))),c),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(X3),multiply(X3,X1)))),X4),inverse(multiply(X2,X4)))),
inference(paramodulation,[status(thm)],[f120,f18]) ).
fof(f314,plain,
! [X0,X1] : c = inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(sF3_fnc),sF2_fnc))),X1),inverse(multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f12,f270]) ).
fof(f317,plain,
! [X0,X1,X2,X3] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X2),multiply(X2,X0)))),X3),inverse(multiply(X1,X3)))),
inference(forward_demodulation,[status(thm)],[f12,f273]) ).
fof(f396,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X0),b))),c),inverse(sF2_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(a),sF3_fnc))),X2),inverse(multiply(X1,X2)))),
inference(paramodulation,[status(thm)],[f174,f18]) ).
fof(f418,plain,
! [X0,X1] : b = inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(a),sF3_fnc))),X1),inverse(multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f12,f396]) ).
fof(f666,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X2)),c),inverse(sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f18,f11]) ).
fof(f722,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(X1),X3))),c),inverse(sF1_fnc)))),inverse(X3)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X2)),c),inverse(sF2_fnc)))),
inference(paramodulation,[status(thm)],[f15,f666]) ).
fof(f735,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc)))))),c),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f666,f15]) ).
fof(f757,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X0)),c),inverse(sF2_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f15,f735]) ).
fof(f770,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X1),X3))),c),inverse(sF2_fnc)))),inverse(X3)))) = X2,
inference(forward_demodulation,[status(thm)],[f666,f16]) ).
fof(f801,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X1),X3))),c),inverse(sF2_fnc)))),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X4),X5))),c),inverse(sF2_fnc)))),inverse(X5))),
inference(paramodulation,[status(thm)],[f770,f770]) ).
fof(f1143,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X0),X1))),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X2),multiply(X2,X1)))),b),inverse(sF3_fnc))),
inference(paramodulation,[status(thm)],[f120,f22]) ).
fof(f1155,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc))))) = X1,
inference(paramodulation,[status(thm)],[f22,f13]) ).
fof(f1205,plain,
! [X0,X1] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X1),multiply(X1,X0)))),b),inverse(sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f13,f1143]) ).
fof(f1355,plain,
! [X0,X1,X2,X3,X4] : multiply(X0,inverse(multiply(multiply(inverse(X1),multiply(X1,X2)),inverse(multiply(inverse(X0),multiply(multiply(inverse(X3),multiply(X3,X4)),X2)))))) = X4,
inference(paramodulation,[status(thm)],[f120,f148]) ).
fof(f1612,plain,
! [X0,X1] : c = inverse(multiply(multiply(inverse(multiply(inverse(X0),multiply(inverse(b),sF1_fnc))),X1),inverse(multiply(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f234,f314]) ).
fof(f1637,plain,
! [X0] : c = inverse(multiply(multiply(inverse(multiply(inverse(a),sF0_fnc)),X0),inverse(multiply(inverse(b),X0)))),
inference(paramodulation,[status(thm)],[f175,f1612]) ).
fof(f1734,plain,
c = inverse(multiply(multiply(inverse(a),sF3_fnc),inverse(multiply(inverse(b),multiply(multiply(inverse(a),sF0_fnc),b))))),
inference(paramodulation,[status(thm)],[f174,f1637]) ).
fof(f1940,plain,
! [X0,X1] : X0 = inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(X1),multiply(X1,X0)))),c),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f5,f317]) ).
fof(f2039,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X1),X3))),b),inverse(sF3_fnc)))),inverse(X3)))) = X2,
inference(backward_demodulation,[status(thm)],[f2047,f770]) ).
fof(f2042,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),X3),inverse(multiply(X1,X3))))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X2)),b),inverse(sF3_fnc)))),
inference(backward_demodulation,[status(thm)],[f2047,f666]) ).
fof(f2047,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f17,f23]) ).
fof(f2349,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(a),X2)),b),inverse(sF3_fnc)))))),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X1),X3))),b),inverse(sF3_fnc)))),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),X2)),X5),inverse(multiply(X4,X5)))),
inference(paramodulation,[status(thm)],[f2042,f2039]) ).
fof(f2352,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(X0),inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))))),c),inverse(sF1_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),X1)),X3),inverse(multiply(X2,X3)))),
inference(paramodulation,[status(thm)],[f2042,f15]) ).
fof(f2384,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a),X0)),b),inverse(sF3_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f2039,f2349]) ).
fof(f2387,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a),X0)),b),inverse(sF3_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(X1),X0)),X2),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[status(thm)],[f15,f2352]) ).
fof(f2455,plain,
b = inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(a),sF3_fnc))),c),inverse(sF1_fnc))),
inference(paramodulation,[status(thm)],[f5,f418]) ).
fof(f4185,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),sF1_fnc),inverse(sF0_fnc)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))),
inference(forward_demodulation,[status(thm)],[f22,f30]) ).
fof(f7349,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(b),X1)),c),inverse(sF1_fnc)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))),
inference(forward_demodulation,[status(thm)],[f34,f39]) ).
fof(f7512,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(inverse(X0)),X1))),c),inverse(sF1_fnc))),
inference(forward_demodulation,[status(thm)],[f4185,f44]) ).
fof(f9268,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X1),X3))),b),inverse(sF3_fnc)))),inverse(X3)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X2)),c),inverse(sF2_fnc)))),
inference(forward_demodulation,[status(thm)],[f7349,f722]) ).
fof(f9270,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X1),X3))),b),inverse(sF3_fnc)))),inverse(X3)))) = multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X2)),b),inverse(sF3_fnc)))),
inference(forward_demodulation,[status(thm)],[f2047,f9268]) ).
fof(f14494,plain,
! [X0,X1,X2,X3,X4,X5] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(X1),X2)),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X1),X3))),b),inverse(sF3_fnc)))),inverse(X3)))) = inverse(multiply(multiply(inverse(multiply(inverse(X4),multiply(inverse(inverse(X0)),X2))),inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X4),X5))),c),inverse(sF2_fnc)))),inverse(X5))),
inference(forward_demodulation,[status(thm)],[f2047,f801]) ).
fof(f14495,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(X2),X3))),c),inverse(sF2_fnc)))),inverse(X3))),
inference(forward_demodulation,[status(thm)],[f9270,f14494]) ).
fof(f14496,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(X2),multiply(inverse(inverse(X0)),X1))),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X2),X3))),b),inverse(sF3_fnc)))),inverse(X3))),
inference(forward_demodulation,[status(thm)],[f2047,f14495]) ).
fof(f20579,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(multiply(inverse(X2),multiply(X2,inverse(multiply(multiply(inverse(multiply(inverse(a),X3)),b),inverse(sF3_fnc))))),inverse(X3)))) = X1,
inference(paramodulation,[status(thm)],[f1155,f1355]) ).
fof(f20952,plain,
! [X0,X1,X2] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(X2,inverse(X2)))) = X1,
inference(forward_demodulation,[status(thm)],[f1155,f20579]) ).
fof(f21023,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,X2))),inverse(multiply(X3,inverse(X3)))) = multiply(X0,X2),
inference(paramodulation,[status(thm)],[f171,f20952]) ).
fof(f21233,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(X0,inverse(multiply(X1,inverse(X1))))) = multiply(inverse(multiply(inverse(X2),multiply(X2,X3))),X3),
inference(paramodulation,[status(thm)],[f20952,f120]) ).
fof(f23998,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(inverse(X0),multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc))))))),multiply(inverse(X2),multiply(X2,inverse(multiply(X3,inverse(X3)))))) = X1,
inference(paramodulation,[status(thm)],[f21233,f1155]) ).
fof(f24131,plain,
! [X0,X1,X2] : multiply(inverse(inverse(X0)),multiply(inverse(X1),multiply(X1,inverse(multiply(X2,inverse(X2)))))) = X0,
inference(forward_demodulation,[status(thm)],[f1155,f23998]) ).
fof(f24148,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,inverse(multiply(X2,inverse(X2)))))) = X1,
inference(paramodulation,[status(thm)],[f171,f24131]) ).
fof(f24303,plain,
! [X0,X1,X2,X3] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X0),inverse(multiply(X1,inverse(X1)))))),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(X2),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(inverse(X2)),X3))),b),inverse(sF3_fnc)))),inverse(X3))),
inference(paramodulation,[status(thm)],[f24131,f14496]) ).
fof(f24415,plain,
! [X0,X1,X2] : inverse(multiply(X0,inverse(X0))) = inverse(multiply(multiply(inverse(X1),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(inverse(X1)),X2))),b),inverse(sF3_fnc)))),inverse(X2))),
inference(forward_demodulation,[status(thm)],[f13,f24303]) ).
fof(f24416,plain,
! [X0,X1] : inverse(multiply(X0,inverse(X0))) = inverse(multiply(X1,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f13,f24415]) ).
fof(f24588,plain,
! [X0,X1,X2,X3] : multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(inverse(X1),multiply(X1,inverse(multiply(X2,inverse(X2)))))) = multiply(X3,inverse(X3)),
inference(paramodulation,[status(thm)],[f24416,f24131]) ).
fof(f24594,plain,
! [X0,X1,X2,X3,X4] : multiply(multiply(inverse(inverse(multiply(X0,inverse(X0)))),multiply(inverse(X1),multiply(X1,X2))),inverse(multiply(X3,inverse(X3)))) = multiply(multiply(X4,inverse(X4)),X2),
inference(paramodulation,[status(thm)],[f24416,f21023]) ).
fof(f24893,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[status(thm)],[f24131,f24588]) ).
fof(f24894,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),X1) = multiply(multiply(X2,inverse(X2)),X1),
inference(forward_demodulation,[status(thm)],[f21023,f24594]) ).
fof(f25860,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,multiply(X1,inverse(X1)))) = multiply(X2,inverse(X2)),
inference(paramodulation,[status(thm)],[f24893,f24148]) ).
fof(f26424,plain,
! [X0,X1,X2] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(X1),multiply(X1,multiply(X2,inverse(X2)))))),b),inverse(sF3_fnc)))) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f25860,f13]) ).
fof(f26535,plain,
! [X0,X1] : multiply(X0,multiply(X1,inverse(X1))) = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f1205,f26424]) ).
fof(f26551,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,inverse(X1))) = inverse(inverse(inverse(X1))),
inference(paramodulation,[status(thm)],[f120,f26535]) ).
fof(f26943,plain,
! [X0] : multiply(inverse(X0),multiply(X0,c)) = inverse(inverse(inverse(multiply(multiply(inverse(a),sF3_fnc),inverse(multiply(inverse(b),multiply(multiply(inverse(a),sF0_fnc),b))))))),
inference(paramodulation,[status(thm)],[f1734,f26551]) ).
fof(f26948,plain,
! [X0] : multiply(inverse(X0),multiply(X0,b)) = inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(a),sF3_fnc))),c),inverse(sF1_fnc))))),
inference(paramodulation,[status(thm)],[f2455,f26551]) ).
fof(f26950,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(X0,X1)) = inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(X2),multiply(X2,X1)))),c),inverse(sF1_fnc))))),
inference(paramodulation,[status(thm)],[f1940,f26551]) ).
fof(f27118,plain,
multiply(inverse(b),sF1_fnc) = inverse(inverse(inverse(multiply(multiply(inverse(a),sF3_fnc),inverse(multiply(inverse(b),multiply(multiply(inverse(a),sF0_fnc),b))))))),
inference(forward_demodulation,[status(thm)],[f176,f26943]) ).
fof(f27119,plain,
multiply(inverse(b),sF1_fnc) = inverse(inverse(c)),
inference(forward_demodulation,[status(thm)],[f1734,f27118]) ).
fof(f27127,plain,
multiply(inverse(a),sF3_fnc) = inverse(inverse(inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(inverse(a),sF3_fnc))),c),inverse(sF1_fnc))))),
inference(forward_demodulation,[status(thm)],[f174,f26948]) ).
fof(f27128,plain,
multiply(inverse(a),sF3_fnc) = inverse(inverse(b)),
inference(forward_demodulation,[status(thm)],[f2455,f27127]) ).
fof(f27131,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f1940,f26950]) ).
fof(f27471,plain,
! [X0,X1] : inverse(inverse(multiply(X0,inverse(multiply(X1,inverse(X1)))))) = X0,
inference(backward_demodulation,[status(thm)],[f27131,f24148]) ).
fof(f27477,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),inverse(multiply(X1,inverse(X1)))) = X0,
inference(backward_demodulation,[status(thm)],[f27131,f20952]) ).
fof(f27604,plain,
! [X0,X1] : inverse(inverse(multiply(X0,inverse(X0)))) = multiply(X1,inverse(X1)),
inference(paramodulation,[status(thm)],[f24416,f27471]) ).
fof(f27811,plain,
! [X0,X1,X2] : multiply(X0,inverse(X0)) = multiply(inverse(multiply(X1,inverse(X1))),multiply(X2,inverse(X2))),
inference(paramodulation,[status(thm)],[f27604,f24893]) ).
fof(f27907,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = inverse(inverse(inverse(multiply(X1,inverse(X1))))),
inference(forward_demodulation,[status(thm)],[f26535,f27811]) ).
fof(f27944,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = inverse(multiply(X1,inverse(X1))),
inference(paramodulation,[status(thm)],[f27471,f27907]) ).
fof(f28196,plain,
! [X0,X1] : multiply(X0,inverse(multiply(X1,inverse(X1)))) = inverse(inverse(X0)),
inference(paramodulation,[status(thm)],[f27944,f26535]) ).
fof(f28197,plain,
! [X0,X1,X2] : multiply(multiply(X0,inverse(X0)),X1) = multiply(inverse(multiply(X2,inverse(X2))),X1),
inference(paramodulation,[status(thm)],[f27944,f24894]) ).
fof(f28227,plain,
! [X0,X1] : multiply(inverse(inverse(X0)),multiply(X1,inverse(X1))) = X0,
inference(paramodulation,[status(thm)],[f27944,f27477]) ).
fof(f28282,plain,
! [X0] : inverse(inverse(inverse(inverse(X0)))) = X0,
inference(forward_demodulation,[status(thm)],[f26535,f28227]) ).
fof(f28340,plain,
! [X0,X1] : multiply(X0,multiply(inverse(inverse(inverse(X0))),X1)) = inverse(inverse(X1)),
inference(paramodulation,[status(thm)],[f28282,f27131]) ).
fof(f28615,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(a),X0)),b),inverse(sF3_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X0)),c),inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f757,f2384]) ).
fof(f32339,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a),X2)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc))))),X2))),c),inverse(sF2_fnc))),
inference(forward_demodulation,[status(thm)],[f28615,f54]) ).
fof(f32340,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a),X2)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc))))),X2))),b),inverse(sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f28615,f32339]) ).
fof(f32341,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a),X2)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc))))),X2))),b),inverse(sF3_fnc))),
inference(forward_demodulation,[status(thm)],[f28615,f32340]) ).
fof(f32924,plain,
! [X0,X1,X2] : multiply(multiply(multiply(inverse(multiply(inverse(sF3_fnc),multiply(inverse(inverse(X0)),X1))),c),inverse(sF2_fnc)),inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc)))),X2))),b),inverse(sF3_fnc)))) = X2,
inference(forward_demodulation,[status(thm)],[f7349,f57]) ).
fof(f32925,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc))))),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(sF3_fnc),X1)),c),inverse(sF2_fnc)))),X2)))),b),inverse(sF3_fnc))) = X2,
inference(forward_demodulation,[status(thm)],[f32341,f32924]) ).
fof(f32926,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc))))),multiply(multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))),X2)))),b),inverse(sF3_fnc))) = X2,
inference(forward_demodulation,[status(thm)],[f28615,f32925]) ).
fof(f32927,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(a),inverse(inverse(X0)))),b),inverse(sF3_fnc))) = X0,
inference(forward_demodulation,[status(thm)],[f27131,f32926]) ).
fof(f33297,plain,
! [X0,X1,X2] : inverse(multiply(multiply(inverse(multiply(inverse(a),inverse(inverse(X0)))),b),inverse(sF3_fnc))) = inverse(multiply(multiply(multiply(X1,inverse(X1)),X2),inverse(multiply(X0,X2)))),
inference(paramodulation,[status(thm)],[f28197,f2387]) ).
fof(f33515,plain,
! [X0,X1,X2] : X0 = inverse(multiply(multiply(multiply(X1,inverse(X1)),X2),inverse(multiply(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f32927,f33297]) ).
fof(f42041,plain,
! [X0,X1,X2] : X0 = inverse(multiply(multiply(X1,inverse(X1)),inverse(multiply(X0,inverse(multiply(X2,inverse(X2))))))),
inference(paramodulation,[status(thm)],[f24894,f33515]) ).
fof(f42334,plain,
! [X0,X1] : X0 = inverse(multiply(multiply(X1,inverse(X1)),inverse(inverse(inverse(X0))))),
inference(forward_demodulation,[status(thm)],[f28196,f42041]) ).
fof(f42503,plain,
! [X0,X1] : inverse(X0) = inverse(multiply(multiply(X1,inverse(X1)),X0)),
inference(paramodulation,[status(thm)],[f28282,f42334]) ).
fof(f42905,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(a),inverse(inverse(X0)))),b),inverse(sF3_fnc))) = multiply(multiply(X1,inverse(X1)),X0),
inference(paramodulation,[status(thm)],[f42503,f32927]) ).
fof(f43063,plain,
! [X0,X1] : X0 = multiply(multiply(X1,inverse(X1)),X0),
inference(forward_demodulation,[status(thm)],[f32927,f42905]) ).
fof(f43081,plain,
! [X0,X1] : X0 = inverse(multiply(X1,inverse(multiply(X0,X1)))),
inference(backward_demodulation,[status(thm)],[f43063,f33515]) ).
fof(f43082,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(X1,inverse(X1))),X0),
inference(backward_demodulation,[status(thm)],[f43063,f28197]) ).
fof(f43540,plain,
! [X0,X1] : X0 = inverse(multiply(inverse(multiply(X1,X0)),X1)),
inference(paramodulation,[status(thm)],[f43081,f43081]) ).
fof(f43739,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = inverse(inverse(X1)),
inference(paramodulation,[status(thm)],[f27131,f43082]) ).
fof(f43940,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f43063,f43739]) ).
fof(f44091,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = inverse(inverse(X1)),
inference(backward_demodulation,[status(thm)],[f43940,f28340]) ).
fof(f44095,plain,
multiply(inverse(a),sF3_fnc) = b,
inference(backward_demodulation,[status(thm)],[f43940,f27128]) ).
fof(f44098,plain,
multiply(inverse(b),sF1_fnc) = c,
inference(backward_demodulation,[status(thm)],[f43940,f27119]) ).
fof(f44121,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(X0,X1))),c),inverse(sF1_fnc))),
inference(backward_demodulation,[status(thm)],[f43940,f7512]) ).
fof(f44122,plain,
! [X0,X1] : multiply(X0,inverse(multiply(multiply(inverse(multiply(inverse(a),X1)),b),inverse(sF3_fnc)))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(X0,X1))),sF1_fnc),inverse(sF0_fnc))),
inference(backward_demodulation,[status(thm)],[f43940,f34]) ).
fof(f44158,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(forward_demodulation,[status(thm)],[f43940,f44091]) ).
fof(f44336,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(X0,multiply(inverse(X0),X1)))),c),inverse(sF1_fnc))) = X1,
inference(backward_demodulation,[status(thm)],[f44121,f13]) ).
fof(f44465,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(X0,multiply(inverse(X0),X1)))),sF1_fnc),inverse(sF0_fnc))) = X1,
inference(backward_demodulation,[status(thm)],[f44467,f44336]) ).
fof(f44467,plain,
! [X0,X1] : inverse(multiply(multiply(inverse(multiply(inverse(b),multiply(X0,X1))),c),inverse(sF1_fnc))) = inverse(multiply(multiply(inverse(multiply(inverse(a),multiply(X0,X1))),sF1_fnc),inverse(sF0_fnc))),
inference(forward_demodulation,[status(thm)],[f44121,f44122]) ).
fof(f44718,plain,
! [X0] : inverse(multiply(multiply(inverse(multiply(inverse(a),X0)),sF1_fnc),inverse(sF0_fnc))) = X0,
inference(forward_demodulation,[status(thm)],[f44158,f44465]) ).
fof(f44725,plain,
inverse(multiply(multiply(inverse(b),sF1_fnc),inverse(sF0_fnc))) = sF3_fnc,
inference(paramodulation,[status(thm)],[f44095,f44718]) ).
fof(f44756,plain,
inverse(multiply(c,inverse(sF0_fnc))) = sF3_fnc,
inference(forward_demodulation,[status(thm)],[f44098,f44725]) ).
fof(f49066,plain,
inverse(sF0_fnc) = inverse(multiply(sF3_fnc,c)),
inference(paramodulation,[status(thm)],[f44756,f43540]) ).
fof(f49092,plain,
inverse(sF0_fnc) = inverse(sF2_fnc),
inference(forward_demodulation,[status(thm)],[f8,f49066]) ).
fof(f49109,plain,
sF2_fnc = inverse(inverse(sF0_fnc)),
inference(paramodulation,[status(thm)],[f49092,f43940]) ).
fof(f49118,plain,
sF2_fnc = sF0_fnc,
inference(forward_demodulation,[status(thm)],[f43940,f49109]) ).
fof(f49119,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f49118,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP014-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.52 % Computer : n019.cluster.edu
% 0.10/0.52 % Model : x86_64 x86_64
% 0.10/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.52 % Memory : 8046.5625MB
% 0.10/0.52 % OS : Linux 6.8.0-71-generic
% 0.10/0.52 % CPULimit : 300
% 0.10/0.52 % WCLimit : 300
% 0.10/0.52 % DateTime : Sun Sep 20 19:53:51 UTC 2026
% 0.10/0.52 % CPUTime :
% 0.10/0.53 % Drodi V4.1.1
% 34.60/4.97 % Refutation found
% 34.60/4.97 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 34.60/4.97 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 21.30/6.28 % Elapsed time: 5.537720 seconds
% 21.30/6.28 % CPU time: 29.345364 seconds
% 21.30/6.28 % Total memory used: 513.897 MB
% 21.30/6.28 % Net memory used: 504.941 MB
%------------------------------------------------------------------------------