%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:33:38 PM UTC 2026
% Result : Unsatisfiable 150.08s 19.47s
% Output : CNFRefutation 86.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 6
% Syntax : Number of formulae : 132 ( 132 unt; 4 def)
% Number of atoms : 132 ( 131 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 16 ( 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 : 249 ( 249 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : multiply(multiply(inverse(multiply(A,inverse(multiply(B,C)))),multiply(A,inverse(C))),inverse(multiply(inverse(C),C))) = B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))) = X1,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f4,plain,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f5,definition,
sF1_fnc = multiply(a3,b3),
introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition]) ).
fof(f6,definition,
sF0_fnc = multiply(sF1_fnc,c3),
introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition]) ).
fof(f7,definition,
sF3_fnc = multiply(b3,c3),
introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition]) ).
fof(f8,definition,
sF2_fnc = multiply(a3,sF3_fnc),
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(f10,plain,
! [X0,X1,X2] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X2))),inverse(multiply(inverse(X2),X2))) = inverse(X2),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f11,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(multiply(X1,X2)))),multiply(X3,inverse(X2))),
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f16,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(X3,multiply(inverse(X2),X2))))),X1),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = X3,
inference(paramodulation,[status(thm)],[f3,f3]) ).
fof(f66,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(a3,inverse(multiply(X1,X2)))),multiply(a3,inverse(X2))),
inference(equality_split,[status(thm)],[f11]) ).
fof(f67,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(a3,inverse(multiply(X1,X2)))),multiply(a3,inverse(X2))),
inference(equality_split,[status(thm)],[f11]) ).
fof(f68,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(a3,inverse(multiply(multiply(X0,inverse(multiply(inverse(X1),X1))),X1)))),multiply(a3,inverse(X1))),
inference(paramodulation,[status(thm)],[f3,f66]) ).
fof(f96,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X2))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),X2)))),multiply(a3,inverse(X2))),
inference(paramodulation,[status(thm)],[f3,f67]) ).
fof(f133,plain,
! [X0,X1] : multiply(inverse(X0),multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),inverse(X1))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f67,f96]) ).
fof(f164,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X2)))),multiply(a3,inverse(X2)))))),multiply(a3,inverse(multiply(a3,inverse(X2))))),
inference(paramodulation,[status(thm)],[f68,f67]) ).
fof(f166,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))),inverse(multiply(inverse(multiply(a3,inverse(X2))),multiply(a3,inverse(X2))))) = inverse(multiply(a3,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X2)))),
inference(paramodulation,[status(thm)],[f68,f3]) ).
fof(f173,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(multiply(a3,inverse(X2))))),
inference(forward_demodulation,[status(thm)],[f68,f164]) ).
fof(f204,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),inverse(multiply(X2,multiply(inverse(X1),X1))))),X0),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))) = X2,
inference(forward_demodulation,[status(thm)],[f67,f16]) ).
fof(f230,plain,
! [X0,X1,X2] : multiply(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,X0)))),multiply(a3,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),X2),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = inverse(multiply(inverse(X0),X0)),
inference(paramodulation,[status(thm)],[f204,f10]) ).
fof(f235,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),inverse(multiply(X2,multiply(inverse(X1),X1))))),X0),inverse(multiply(X3,multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))),X2),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))) = X3,
inference(paramodulation,[status(thm)],[f204,f3]) ).
fof(f238,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))) = multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X3,X2)))),multiply(a3,inverse(X2))),inverse(multiply(X1,multiply(inverse(X2),X2))))),X3),
inference(paramodulation,[status(thm)],[f204,f3]) ).
fof(f244,plain,
! [X0,X1,X2] : multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(inverse(X1),X1))))),multiply(a3,inverse(multiply(inverse(X1),X1)))) = multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,X1)))),multiply(a3,inverse(X1))),inverse(multiply(X0,multiply(inverse(X1),X1))))),X2),
inference(forward_demodulation,[status(thm)],[f66,f238]) ).
fof(f502,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(a3,inverse(X2))))),
inference(paramodulation,[status(thm)],[f173,f173]) ).
fof(f566,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(a3,inverse(X2))))) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(multiply(a3,inverse(X2))))),
inference(equality_split,[status(thm)],[f502]) ).
fof(f1857,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,inverse(multiply(a3,inverse(X1))))),inverse(multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(X1))))) = inverse(multiply(a3,inverse(multiply(multiply(X0,inverse(multiply(inverse(X1),X1))),X1)))),
inference(forward_demodulation,[status(thm)],[f566,f166]) ).
fof(f1858,plain,
! [X0,X1] : X0 = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),inverse(multiply(inverse(X1),X1))),X1)))),
inference(paramodulation,[status(thm)],[f3,f1857]) ).
fof(f1908,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,inverse(multiply(a3,inverse(multiply(multiply(multiply(X2,multiply(a3,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3)))))),
inference(paramodulation,[status(thm)],[f1858,f566]) ).
fof(f1970,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)) = multiply(inverse(multiply(a3,inverse(X1))),multiply(a3,X2)),
inference(forward_demodulation,[status(thm)],[f1858,f1908]) ).
fof(f2108,plain,
! [X0,X1,X2,X3] : multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),X3)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X2),X2)))),multiply(a3,X3)),
inference(paramodulation,[status(thm)],[f3,f1970]) ).
fof(f2113,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(a3,inverse(multiply(a3,inverse(multiply(multiply(multiply(X1,multiply(a3,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3)))))),multiply(a3,X2)),
inference(paramodulation,[status(thm)],[f1858,f1970]) ).
fof(f2245,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(a3,X1)),multiply(a3,X2)),
inference(forward_demodulation,[status(thm)],[f1858,f2113]) ).
fof(f2256,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X1))),multiply(inverse(multiply(X2,X0)),X3)) = multiply(inverse(multiply(a3,multiply(X2,X1))),multiply(a3,X3)),
inference(paramodulation,[status(thm)],[f2245,f2245]) ).
fof(f2306,plain,
! [X0] : multiply(inverse(multiply(b3,X0)),sF3_fnc) = multiply(inverse(multiply(a3,X0)),multiply(a3,c3)),
inference(paramodulation,[status(thm)],[f7,f2245]) ).
fof(f2309,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X3,X1)),multiply(X3,X2)),
inference(paramodulation,[status(thm)],[f2245,f2245]) ).
fof(f2423,plain,
! [X0,X1,X2] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(a3,X1)),multiply(a3,X2)),
inference(equality_split,[status(thm)],[f2309]) ).
fof(f11014,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X1))),multiply(inverse(multiply(a3,X0)),multiply(a3,X2))) = multiply(inverse(multiply(a3,multiply(X3,X1))),multiply(a3,multiply(X3,X2))),
inference(paramodulation,[status(thm)],[f2423,f2256]) ).
fof(f11180,plain,
! [X0,X1,X2] : multiply(inverse(multiply(a3,multiply(a3,X0))),multiply(a3,multiply(a3,X1))) = multiply(inverse(multiply(a3,multiply(X2,X0))),multiply(a3,multiply(X2,X1))),
inference(forward_demodulation,[status(thm)],[f2256,f11014]) ).
fof(f12791,plain,
! [X0,X1,X2] : multiply(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X2,X0)))),multiply(a3,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),X2),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X0)))) = inverse(multiply(inverse(X0),X0)),
inference(forward_demodulation,[status(thm)],[f2423,f230]) ).
fof(f19090,plain,
! [X0,X1,X2,X3] : multiply(inverse(multiply(a3,multiply(X0,X1))),multiply(a3,multiply(X0,X2))) = multiply(inverse(multiply(a3,multiply(X3,X1))),multiply(a3,multiply(X3,X2))),
inference(paramodulation,[status(thm)],[f11180,f11180]) ).
fof(f20612,plain,
! [X0,X1,X2] : multiply(inverse(multiply(a3,multiply(X0,X1))),multiply(a3,multiply(X0,X2))) = multiply(inverse(multiply(a3,multiply(a3,X1))),multiply(a3,multiply(a3,X2))),
inference(equality_split,[status(thm)],[f19090]) ).
fof(f21646,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),inverse(multiply(X2,multiply(inverse(X1),X1))))),X0),inverse(multiply(X3,multiply(inverse(multiply(a3,X1)),multiply(a3,X1)))))),X2),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))))) = X3,
inference(forward_demodulation,[status(thm)],[f2423,f235]) ).
fof(f21647,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),inverse(multiply(X2,multiply(inverse(X1),X1))))),X0),inverse(multiply(X3,multiply(inverse(multiply(a3,X1)),multiply(a3,X1)))))),X2),inverse(multiply(inverse(multiply(a3,multiply(inverse(X1),X1))),multiply(a3,multiply(inverse(X1),X1))))) = X3,
inference(forward_demodulation,[status(thm)],[f2423,f21646]) ).
fof(f21648,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),inverse(multiply(X2,multiply(inverse(X1),X1))))),X0),inverse(multiply(X3,multiply(inverse(multiply(a3,X1)),multiply(a3,X1)))))),X2),inverse(multiply(inverse(multiply(a3,multiply(a3,X1))),multiply(a3,multiply(a3,X1))))) = X3,
inference(forward_demodulation,[status(thm)],[f20612,f21647]) ).
fof(f25008,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(inverse(X1),X1))))),multiply(a3,inverse(multiply(inverse(X1),X1)))),inverse(multiply(X2,multiply(inverse(multiply(a3,X1)),multiply(a3,X1)))))),X0),inverse(multiply(inverse(multiply(a3,multiply(a3,X1))),multiply(a3,multiply(a3,X1))))) = X2,
inference(backward_demodulation,[status(thm)],[f244,f21648]) ).
fof(f25010,plain,
! [X0,X1] : multiply(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(a3,inverse(multiply(X1,multiply(inverse(X0),X0))))),multiply(a3,inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X0)))) = inverse(multiply(inverse(X0),X0)),
inference(backward_demodulation,[status(thm)],[f244,f12791]) ).
fof(f25241,plain,
! [X0] : multiply(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(a3,inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X0)))) = inverse(multiply(inverse(X0),X0)),
inference(forward_demodulation,[status(thm)],[f133,f25010]) ).
fof(f25242,plain,
! [X0] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0))))),multiply(a3,inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X0)))) = inverse(multiply(inverse(X0),X0)),
inference(forward_demodulation,[status(thm)],[f133,f25241]) ).
fof(f25243,plain,
! [X0] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X0))))),multiply(a3,inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X0)))) = inverse(multiply(inverse(X0),X0)),
inference(forward_demodulation,[status(thm)],[f2423,f25242]) ).
fof(f44560,plain,
! [X0,X1,X2] : multiply(inverse(X0),multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),X2)) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X1)))),multiply(a3,X2)),
inference(forward_demodulation,[status(thm)],[f2423,f2108]) ).
fof(f44578,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(a3,inverse(multiply(inverse(X1),X1)))),multiply(a3,inverse(multiply(inverse(X1),X1)))),
inference(paramodulation,[status(thm)],[f3,f44560]) ).
fof(f45033,plain,
! [X0] : multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X0)))),multiply(a3,inverse(multiply(inverse(X0),X0)))) = multiply(inverse(a3),a3),
inference(equality_split,[status(thm)],[f44578]) ).
fof(f45034,plain,
! [X0] : multiply(inverse(X0),X0) = multiply(inverse(a3),a3),
inference(equality_split,[status(thm)],[f44578]) ).
fof(f45122,plain,
! [X0] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,inverse(multiply(inverse(X0),X0)))),multiply(a3,inverse(multiply(inverse(X0),X0))))))),multiply(a3,inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(a3),a3))) = inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),
inference(paramodulation,[status(thm)],[f45033,f25243]) ).
fof(f45475,plain,
! [X0,X1] : X0 = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),inverse(multiply(inverse(a3),a3))),X1)))),
inference(paramodulation,[status(thm)],[f45034,f1858]) ).
fof(f45480,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(a3,inverse(multiply(multiply(X0,inverse(multiply(inverse(a3),a3))),X1)))),multiply(a3,inverse(X1))),
inference(paramodulation,[status(thm)],[f45034,f68]) ).
fof(f45485,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(a3),a3))) = X1,
inference(paramodulation,[status(thm)],[f45034,f3]) ).
fof(f45619,plain,
! [X0,X1] : multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(X0),X1)) = multiply(inverse(multiply(a3,X0)),multiply(a3,X1)),
inference(paramodulation,[status(thm)],[f45034,f2423]) ).
fof(f45887,plain,
! [X0] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),multiply(a3,inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(a3),a3))) = inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),
inference(forward_demodulation,[status(thm)],[f45033,f45122]) ).
fof(f45888,plain,
! [X0] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),multiply(a3,inverse(multiply(inverse(a3),a3)))),inverse(multiply(inverse(a3),a3))) = inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),
inference(forward_demodulation,[status(thm)],[f45034,f45887]) ).
fof(f45889,plain,
! [X0] : multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(a3),a3))) = inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),
inference(forward_demodulation,[status(thm)],[f45033,f45888]) ).
fof(f45890,plain,
multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(a3),a3))) = inverse(multiply(inverse(a3),a3)),
inference(forward_demodulation,[status(thm)],[f45034,f45889]) ).
fof(f46842,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),inverse(multiply(inverse(a3),a3))) = X0,
inference(forward_demodulation,[status(thm)],[f2423,f45485]) ).
fof(f49647,plain,
! [X0] : inverse(multiply(a3,inverse(X0))) = inverse(multiply(a3,inverse(multiply(multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(a3),a3))),X0)))),
inference(paramodulation,[status(thm)],[f45034,f45475]) ).
fof(f49797,plain,
! [X0] : inverse(multiply(a3,inverse(X0))) = inverse(multiply(a3,inverse(multiply(inverse(multiply(inverse(a3),a3)),X0)))),
inference(forward_demodulation,[status(thm)],[f45890,f49647]) ).
fof(f51288,plain,
multiply(multiply(inverse(multiply(a3,inverse(inverse(multiply(inverse(a3),a3))))),multiply(a3,inverse(inverse(multiply(inverse(a3),a3))))),inverse(multiply(inverse(a3),a3))) = multiply(inverse(a3),a3),
inference(paramodulation,[status(thm)],[f45890,f46842]) ).
fof(f51448,plain,
multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(a3),a3))) = multiply(inverse(a3),a3),
inference(forward_demodulation,[status(thm)],[f45034,f51288]) ).
fof(f51449,plain,
inverse(multiply(inverse(a3),a3)) = multiply(inverse(a3),a3),
inference(forward_demodulation,[status(thm)],[f45890,f51448]) ).
fof(f51650,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))),multiply(inverse(a3),a3)) = X0,
inference(backward_demodulation,[status(thm)],[f51449,f46842]) ).
fof(f51651,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(a3,inverse(multiply(multiply(X0,multiply(inverse(a3),a3)),X1)))),multiply(a3,inverse(X1))),
inference(backward_demodulation,[status(thm)],[f51449,f45480]) ).
fof(f51652,plain,
! [X0] : inverse(multiply(a3,inverse(X0))) = inverse(multiply(a3,inverse(multiply(multiply(inverse(a3),a3),X0)))),
inference(backward_demodulation,[status(thm)],[f51449,f49797]) ).
fof(f51654,plain,
! [X0,X1] : X0 = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),
inference(backward_demodulation,[status(thm)],[f51449,f45475]) ).
fof(f51660,plain,
! [X0,X1] : multiply(multiply(inverse(a3),a3),multiply(inverse(X0),X1)) = multiply(inverse(multiply(a3,X0)),multiply(a3,X1)),
inference(backward_demodulation,[status(thm)],[f51449,f45619]) ).
fof(f53038,plain,
! [X0] : multiply(inverse(multiply(b3,inverse(multiply(multiply(inverse(a3),a3),X0)))),sF3_fnc) = multiply(inverse(multiply(a3,inverse(X0))),multiply(a3,c3)),
inference(paramodulation,[status(thm)],[f51652,f2306]) ).
fof(f53392,plain,
! [X0] : multiply(inverse(multiply(b3,inverse(multiply(multiply(inverse(a3),a3),X0)))),sF3_fnc) = multiply(inverse(multiply(b3,inverse(X0))),sF3_fnc),
inference(forward_demodulation,[status(thm)],[f2306,f53038]) ).
fof(f55598,plain,
! [X0,X1] : multiply(X0,multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))) = multiply(inverse(a3),a3),
inference(paramodulation,[status(thm)],[f51654,f45034]) ).
fof(f55653,plain,
! [X0,X1,X2,X3] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,multiply(a3,inverse(multiply(multiply(multiply(X2,multiply(a3,inverse(X3))),multiply(inverse(a3),a3)),X3))))))),multiply(X1,inverse(multiply(a3,inverse(multiply(multiply(multiply(X2,multiply(a3,inverse(X3))),multiply(inverse(a3),a3)),X3)))))),X2)),inverse(multiply(inverse(multiply(a3,inverse(multiply(multiply(multiply(X2,multiply(a3,inverse(X3))),multiply(inverse(a3),a3)),X3)))),multiply(a3,inverse(multiply(multiply(multiply(X2,multiply(a3,inverse(X3))),multiply(inverse(a3),a3)),X3)))))) = inverse(multiply(a3,inverse(multiply(multiply(multiply(X2,multiply(a3,inverse(X3))),multiply(inverse(a3),a3)),X3)))),
inference(paramodulation,[status(thm)],[f51654,f10]) ).
fof(f56332,plain,
! [X0,X1,X2] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,multiply(a3,inverse(multiply(multiply(multiply(X1,multiply(a3,inverse(X2))),multiply(inverse(a3),a3)),X2))))))),multiply(a3,inverse(multiply(a3,inverse(multiply(multiply(multiply(X1,multiply(a3,inverse(X2))),multiply(inverse(a3),a3)),X2)))))),X1)),inverse(multiply(inverse(multiply(a3,inverse(multiply(multiply(multiply(X1,multiply(a3,inverse(X2))),multiply(inverse(a3),a3)),X2)))),multiply(a3,inverse(multiply(multiply(multiply(X1,multiply(a3,inverse(X2))),multiply(inverse(a3),a3)),X2)))))) = inverse(multiply(a3,inverse(multiply(multiply(multiply(X1,multiply(a3,inverse(X2))),multiply(inverse(a3),a3)),X2)))),
inference(forward_demodulation,[status(thm)],[f2423,f55653]) ).
fof(f56333,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1))))))),multiply(a3,X0)),inverse(multiply(inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))))) = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),
inference(forward_demodulation,[status(thm)],[f44560,f56332]) ).
fof(f56334,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),multiply(a3,X0)),inverse(multiply(inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))))) = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),
inference(forward_demodulation,[status(thm)],[f45034,f56333]) ).
fof(f56335,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,X0)),inverse(multiply(inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))))) = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),
inference(forward_demodulation,[status(thm)],[f51449,f56334]) ).
fof(f56336,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,X0)),inverse(multiply(inverse(a3),a3))) = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),
inference(forward_demodulation,[status(thm)],[f45034,f56335]) ).
fof(f56337,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,X0)),multiply(inverse(a3),a3)) = inverse(multiply(a3,inverse(multiply(multiply(multiply(X0,multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))),
inference(forward_demodulation,[status(thm)],[f51449,f56336]) ).
fof(f56338,plain,
! [X0] : multiply(multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,X0)),multiply(inverse(a3),a3)) = X0,
inference(forward_demodulation,[status(thm)],[f51654,f56337]) ).
fof(f58906,plain,
multiply(multiply(inverse(multiply(b3,multiply(inverse(a3),a3))),sF3_fnc),multiply(inverse(a3),a3)) = c3,
inference(paramodulation,[status(thm)],[f2306,f56338]) ).
fof(f68517,plain,
! [X0] : multiply(multiply(inverse(multiply(a3,inverse(multiply(inverse(multiply(b3,inverse(X0))),sF3_fnc)))),multiply(a3,inverse(sF3_fnc))),multiply(inverse(a3),a3)) = inverse(multiply(b3,inverse(multiply(multiply(inverse(a3),a3),X0)))),
inference(paramodulation,[status(thm)],[f53392,f51650]) ).
fof(f68598,plain,
! [X0] : inverse(multiply(b3,inverse(X0))) = inverse(multiply(b3,inverse(multiply(multiply(inverse(a3),a3),X0)))),
inference(forward_demodulation,[status(thm)],[f51650,f68517]) ).
fof(f68676,plain,
! [X0,X1] : inverse(multiply(b3,inverse(multiply(inverse(X0),X1)))) = inverse(multiply(b3,inverse(multiply(inverse(multiply(a3,X0)),multiply(a3,X1))))),
inference(paramodulation,[status(thm)],[f51660,f68598]) ).
fof(f89834,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(a3,inverse(multiply(inverse(a3),a3)))),multiply(a3,inverse(multiply(a3,inverse(multiply(multiply(multiply(multiply(X0,multiply(inverse(a3),a3)),multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))))),
inference(paramodulation,[status(thm)],[f55598,f51651]) ).
fof(f90160,plain,
! [X0,X1] : X0 = multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,inverse(multiply(a3,inverse(multiply(multiply(multiply(multiply(X0,multiply(inverse(a3),a3)),multiply(a3,inverse(X1))),multiply(inverse(a3),a3)),X1)))))),
inference(forward_demodulation,[status(thm)],[f51449,f89834]) ).
fof(f90161,plain,
! [X0] : X0 = multiply(inverse(multiply(a3,multiply(inverse(a3),a3))),multiply(a3,multiply(X0,multiply(inverse(a3),a3)))),
inference(forward_demodulation,[status(thm)],[f51654,f90160]) ).
fof(f90750,plain,
! [X0] : inverse(multiply(b3,inverse(multiply(inverse(multiply(inverse(a3),a3)),multiply(X0,multiply(inverse(a3),a3)))))) = inverse(multiply(b3,inverse(X0))),
inference(paramodulation,[status(thm)],[f90161,f68676]) ).
fof(f90819,plain,
! [X0] : inverse(multiply(b3,inverse(multiply(multiply(inverse(a3),a3),multiply(X0,multiply(inverse(a3),a3)))))) = inverse(multiply(b3,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f51449,f90750]) ).
fof(f90820,plain,
! [X0] : inverse(multiply(b3,inverse(multiply(X0,multiply(inverse(a3),a3))))) = inverse(multiply(b3,inverse(X0))),
inference(forward_demodulation,[status(thm)],[f68598,f90819]) ).
fof(f90948,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(b3,inverse(X0))),multiply(b3,inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = multiply(inverse(multiply(a3,inverse(multiply(multiply(X0,multiply(inverse(a3),a3)),X1)))),multiply(a3,inverse(X1))),
inference(paramodulation,[status(thm)],[f90820,f66]) ).
fof(f91159,plain,
! [X0,X1] : multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))) = multiply(inverse(multiply(a3,inverse(multiply(multiply(X0,multiply(inverse(a3),a3)),X1)))),multiply(a3,inverse(X1))),
inference(forward_demodulation,[status(thm)],[f66,f90948]) ).
fof(f91160,plain,
! [X0,X1] : multiply(inverse(multiply(a3,inverse(multiply(X0,X1)))),multiply(a3,inverse(X1))) = X0,
inference(forward_demodulation,[status(thm)],[f51651,f91159]) ).
fof(f92338,plain,
! [X0] : X0 = multiply(X0,multiply(inverse(a3),a3)),
inference(backward_demodulation,[status(thm)],[f91160,f51651]) ).
fof(f92347,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(multiply(a3,X2)),multiply(a3,X2)))))),X0),inverse(multiply(inverse(multiply(a3,multiply(a3,X2))),multiply(a3,multiply(a3,X2))))) = X1,
inference(backward_demodulation,[status(thm)],[f91160,f25008]) ).
fof(f92659,plain,
! [X0,X1,X2] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(a3),a3))))),X0),inverse(multiply(inverse(multiply(a3,multiply(a3,X2))),multiply(a3,multiply(a3,X2))))) = X1,
inference(forward_demodulation,[status(thm)],[f45034,f92347]) ).
fof(f92660,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(a3),a3))))),X0),inverse(multiply(inverse(a3),a3))) = X1,
inference(forward_demodulation,[status(thm)],[f45034,f92659]) ).
fof(f92661,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(a3),a3))))),X0),multiply(inverse(a3),a3)) = X1,
inference(forward_demodulation,[status(thm)],[f51449,f92660]) ).
fof(f93201,plain,
multiply(inverse(multiply(b3,multiply(inverse(a3),a3))),sF3_fnc) = c3,
inference(backward_demodulation,[status(thm)],[f92338,f58906]) ).
fof(f93365,plain,
multiply(inverse(b3),sF3_fnc) = c3,
inference(forward_demodulation,[status(thm)],[f92338,f93201]) ).
fof(f94514,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(a3),a3))))),X0) = X1,
inference(forward_demodulation,[status(thm)],[f92338,f92661]) ).
fof(f94516,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),X0) = X1,
inference(forward_demodulation,[status(thm)],[f92338,f94514]) ).
fof(f94527,plain,
! [X0] : multiply(inverse(multiply(b3,inverse(X0))),b3) = multiply(multiply(inverse(a3),a3),X0),
inference(paramodulation,[status(thm)],[f68598,f94516]) ).
fof(f94718,plain,
! [X0] : X0 = multiply(multiply(inverse(a3),a3),X0),
inference(forward_demodulation,[status(thm)],[f94516,f94527]) ).
fof(f95565,plain,
! [X0] : multiply(inverse(inverse(X0)),multiply(inverse(a3),a3)) = X0,
inference(paramodulation,[status(thm)],[f94718,f94516]) ).
fof(f95870,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f92338,f95565]) ).
fof(f95987,plain,
! [X0,X1,X2] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(X2))))),multiply(X1,inverse(inverse(X2)))),X2)),inverse(multiply(inverse(inverse(X2)),inverse(X2)))) = inverse(inverse(X2)),
inference(paramodulation,[status(thm)],[f95870,f10]) ).
fof(f96241,plain,
! [X0,X1] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(a3,inverse(multiply(X0,inverse(X1))))),multiply(a3,inverse(inverse(X1)))),X1)),inverse(multiply(inverse(inverse(X1)),inverse(X1)))) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f2423,f95987]) ).
fof(f96242,plain,
! [X0,X1] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(inverse(inverse(X1)),inverse(X1)))) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f91160,f96241]) ).
fof(f96243,plain,
! [X0,X1] : multiply(multiply(inverse(X0),multiply(X0,X1)),inverse(multiply(inverse(a3),a3))) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f45034,f96242]) ).
fof(f96244,plain,
! [X0,X1] : multiply(multiply(inverse(X0),multiply(X0,X1)),multiply(inverse(a3),a3)) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f51449,f96243]) ).
fof(f96245,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = inverse(inverse(X1)),
inference(forward_demodulation,[status(thm)],[f92338,f96244]) ).
fof(f96246,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(forward_demodulation,[status(thm)],[f95870,f96245]) ).
fof(f96266,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(paramodulation,[status(thm)],[f95870,f96246]) ).
fof(f96357,plain,
! [X0,X1] : multiply(inverse(inverse(multiply(X0,inverse(X1)))),X1) = X0,
inference(paramodulation,[status(thm)],[f94516,f96246]) ).
fof(f96584,plain,
! [X0,X1] : multiply(multiply(X0,inverse(X1)),X1) = X0,
inference(forward_demodulation,[status(thm)],[f95870,f96357]) ).
fof(f97420,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = X0,
inference(paramodulation,[status(thm)],[f95870,f96584]) ).
fof(f98005,plain,
multiply(c3,inverse(sF3_fnc)) = inverse(b3),
inference(paramodulation,[status(thm)],[f93365,f97420]) ).
fof(f101195,plain,
multiply(inverse(multiply(a3,inverse(inverse(b3)))),multiply(a3,inverse(inverse(sF3_fnc)))) = c3,
inference(paramodulation,[status(thm)],[f98005,f91160]) ).
fof(f101239,plain,
multiply(inverse(multiply(a3,b3)),multiply(a3,inverse(inverse(sF3_fnc)))) = c3,
inference(forward_demodulation,[status(thm)],[f95870,f101195]) ).
fof(f101240,plain,
multiply(inverse(sF1_fnc),multiply(a3,inverse(inverse(sF3_fnc)))) = c3,
inference(forward_demodulation,[status(thm)],[f5,f101239]) ).
fof(f101241,plain,
multiply(inverse(sF1_fnc),multiply(a3,sF3_fnc)) = c3,
inference(forward_demodulation,[status(thm)],[f95870,f101240]) ).
fof(f101242,plain,
multiply(inverse(sF1_fnc),sF2_fnc) = c3,
inference(forward_demodulation,[status(thm)],[f8,f101241]) ).
fof(f101480,plain,
multiply(sF1_fnc,c3) = sF2_fnc,
inference(paramodulation,[status(thm)],[f101242,f96266]) ).
fof(f101509,plain,
sF0_fnc = sF2_fnc,
inference(forward_demodulation,[status(thm)],[f6,f101480]) ).
fof(f101510,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f101509,f9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n016.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sun Sep 20 20:17:06 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.45 % Drodi V4.1.1
% 150.08/19.47 % Refutation found
% 150.08/19.47 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 150.08/19.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.85/19.65 % Elapsed time: 19.183860 seconds
% 14.85/19.65 % CPU time: 151.316114 seconds
% 14.85/19.65 % Total memory used: 1.220 GB
% 14.85/19.65 % Net memory used: 1.181 GB
%------------------------------------------------------------------------------