%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : GRP292-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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:20 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.41s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 39
% Syntax : Number of formulae : 222 ( 18 unt; 21 def)
% Number of atoms : 682 ( 243 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 870 ( 410 ~; 439 |; 0 &)
% ( 21 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 22 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-2 aty)
% Number of variables : 65 ( 65 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : multiply(identity,X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] : multiply(inverse(X),X) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X,Y,Z] : multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
( multiply(sk_c3,sk_c4) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
( multiply(sk_c3,sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
( multiply(sk_c3,sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
( multiply(sk_c3,sk_c4) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
( inverse(sk_c3) = sk_c4
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
( multiply(sk_c3,sk_c4) = sk_c6
| inverse(sk_c2) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
( inverse(sk_c3) = sk_c4
| inverse(sk_c2) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [X3,X4,X2,X1] :
( multiply(X1,sk_c5) != sk_c6
| inverse(X2) != X1
| multiply(X2,X1) != sk_c6
| multiply(sk_c5,sk_c6) != sk_c7
| inverse(X4) != sk_c5
| multiply(X4,sk_c5) != sk_c6
| inverse(X3) != sk_c7
| multiply(X3,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,plain,
! [X0] : multiply(identity,X0) = X0,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f26,plain,
! [X0] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f27,plain,
! [X0,X1,X2] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f28,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f29,plain,
( multiply(sk_c3,sk_c4) = sk_c6
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f33,plain,
( multiply(sk_c3,sk_c4) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f35,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f37,plain,
( multiply(sk_c3,sk_c4) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f39,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c1) = sk_c7 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f40,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| multiply(sk_c2,sk_c5) = sk_c6 ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f41,plain,
( multiply(sk_c3,sk_c4) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f42,plain,
( inverse(sk_c3) = sk_c4
| multiply(sk_c2,sk_c5) = sk_c6 ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f43,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| multiply(sk_c2,sk_c5) = sk_c6 ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f44,plain,
( multiply(sk_c5,sk_c6) = sk_c7
| inverse(sk_c2) = sk_c5 ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f45,plain,
( multiply(sk_c3,sk_c4) = sk_c6
| inverse(sk_c2) = sk_c5 ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f46,plain,
( inverse(sk_c3) = sk_c4
| inverse(sk_c2) = sk_c5 ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f47,plain,
( multiply(sk_c4,sk_c5) = sk_c6
| inverse(sk_c2) = sk_c5 ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f48,plain,
! [X1] :
( multiply(X1,sk_c5) != sk_c6
| ! [X2] :
( inverse(X2) != X1
| multiply(X2,X1) != sk_c6
| multiply(sk_c5,sk_c6) != sk_c7
| ! [X4] :
( inverse(X4) != sk_c5
| multiply(X4,sk_c5) != sk_c6
| ! [X3] :
( inverse(X3) != sk_c7
| multiply(X3,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ) ) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f49,plain,
! [X0,X1,X2,X3] :
( multiply(X3,sk_c5) != sk_c6
| inverse(X2) != X3
| multiply(X2,X3) != sk_c6
| multiply(sk_c5,sk_c6) != sk_c7
| inverse(X1) != sk_c5
| multiply(X1,sk_c5) != sk_c6
| inverse(X0) != sk_c7
| multiply(X0,sk_c7) != sk_c6
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,definition,
( sQ0_spl
<=> multiply(sk_c7,sk_c6) = sk_c5 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f51,plain,
( ~ sQ0_spl
| multiply(sk_c7,sk_c6) = sk_c5 ),
inference(component_clause,[status(thm)],[f50]) ).
fof(f52,plain,
( sQ0_spl
| multiply(sk_c7,sk_c6) != sk_c5 ),
inference(component_clause,[status(thm)],[f50]) ).
fof(f53,definition,
( sQ1_spl
<=> multiply(sk_c5,sk_c6) = sk_c7 ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f54,plain,
( ~ sQ1_spl
| multiply(sk_c5,sk_c6) = sk_c7 ),
inference(component_clause,[status(thm)],[f53]) ).
fof(f55,plain,
( sQ1_spl
| multiply(sk_c5,sk_c6) != sk_c7 ),
inference(component_clause,[status(thm)],[f53]) ).
fof(f56,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f28,f50,f53]) ).
fof(f57,definition,
( sQ2_spl
<=> multiply(sk_c3,sk_c4) = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f58,plain,
( ~ sQ2_spl
| multiply(sk_c3,sk_c4) = sk_c6 ),
inference(component_clause,[status(thm)],[f57]) ).
fof(f60,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f29,f50,f57]) ).
fof(f61,definition,
( sQ3_spl
<=> inverse(sk_c3) = sk_c4 ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f62,plain,
( ~ sQ3_spl
| inverse(sk_c3) = sk_c4 ),
inference(component_clause,[status(thm)],[f61]) ).
fof(f65,definition,
( sQ4_spl
<=> multiply(sk_c4,sk_c5) = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f66,plain,
( ~ sQ4_spl
| multiply(sk_c4,sk_c5) = sk_c6 ),
inference(component_clause,[status(thm)],[f65]) ).
fof(f69,definition,
( sQ5_spl
<=> multiply(sk_c1,sk_c7) = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f70,plain,
( ~ sQ5_spl
| multiply(sk_c1,sk_c7) = sk_c6 ),
inference(component_clause,[status(thm)],[f69]) ).
fof(f73,plain,
( sQ2_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f33,f69,f57]) ).
fof(f75,plain,
( sQ4_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f35,f69,f65]) ).
fof(f76,definition,
( sQ6_spl
<=> inverse(sk_c1) = sk_c7 ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f77,plain,
( ~ sQ6_spl
| inverse(sk_c1) = sk_c7 ),
inference(component_clause,[status(thm)],[f76]) ).
fof(f80,plain,
( sQ2_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f37,f76,f57]) ).
fof(f82,plain,
( sQ4_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f39,f76,f65]) ).
fof(f83,definition,
( sQ7_spl
<=> multiply(sk_c2,sk_c5) = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f84,plain,
( ~ sQ7_spl
| multiply(sk_c2,sk_c5) = sk_c6 ),
inference(component_clause,[status(thm)],[f83]) ).
fof(f86,plain,
( sQ1_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f40,f83,f53]) ).
fof(f87,plain,
( sQ2_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f41,f83,f57]) ).
fof(f88,plain,
( sQ3_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f42,f83,f61]) ).
fof(f89,plain,
( sQ4_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f43,f83,f65]) ).
fof(f90,definition,
( sQ8_spl
<=> inverse(sk_c2) = sk_c5 ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f91,plain,
( ~ sQ8_spl
| inverse(sk_c2) = sk_c5 ),
inference(component_clause,[status(thm)],[f90]) ).
fof(f93,plain,
( sQ1_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f44,f90,f53]) ).
fof(f94,plain,
( sQ2_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f45,f90,f57]) ).
fof(f95,plain,
( sQ3_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f46,f90,f61]) ).
fof(f96,plain,
( sQ4_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f47,f90,f65]) ).
fof(f97,definition,
! [X0] :
( sQ9_spl
<=> ( inverse(X0) != sk_c7
| multiply(X0,sk_c7) != sk_c6 ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f98,plain,
! [X0] :
( ~ sQ9_spl
| inverse(X0) != sk_c7
| multiply(X0,sk_c7) != sk_c6 ),
inference(component_clause,[status(thm)],[f97]) ).
fof(f100,definition,
! [X1] :
( sQ10_spl
<=> ( inverse(X1) != sk_c5
| multiply(X1,sk_c5) != sk_c6 ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f101,plain,
! [X0] :
( ~ sQ10_spl
| inverse(X0) != sk_c5
| multiply(X0,sk_c5) != sk_c6 ),
inference(component_clause,[status(thm)],[f100]) ).
fof(f103,definition,
! [X2,X3] :
( sQ11_spl
<=> ( multiply(X3,sk_c5) != sk_c6
| inverse(X2) != X3
| multiply(X2,X3) != sk_c6 ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f104,plain,
! [X0,X1] :
( ~ sQ11_spl
| multiply(X1,sk_c5) != sk_c6
| inverse(X0) != X1
| multiply(X0,X1) != sk_c6 ),
inference(component_clause,[status(thm)],[f103]) ).
fof(f106,plain,
( sQ11_spl
| ~ sQ1_spl
| sQ10_spl
| sQ9_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f49,f50,f97,f100,f53,f103]) ).
fof(f107,plain,
! [X0] :
( ~ sQ11_spl
| multiply(inverse(X0),sk_c5) != sk_c6
| multiply(X0,inverse(X0)) != sk_c6 ),
inference(destructive_equality_resolution,[status(thm)],[f104]) ).
fof(f109,plain,
! [X0] :
( ~ sQ1_spl
| multiply(sk_c7,X0) = multiply(sk_c5,multiply(sk_c6,X0)) ),
inference(paramodulation,[status(thm)],[f54,f27]) ).
fof(f146,plain,
( ~ sQ3_spl
| ~ sQ11_spl
| multiply(sk_c4,sk_c5) != sk_c6
| multiply(sk_c3,inverse(sk_c3)) != sk_c6 ),
inference(paramodulation,[status(thm)],[f62,f107]) ).
fof(f161,definition,
( sQ16_spl
<=> multiply(sk_c3,inverse(sk_c3)) = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f163,plain,
( sQ16_spl
| multiply(sk_c3,inverse(sk_c3)) != sk_c6 ),
inference(component_clause,[status(thm)],[f161]) ).
fof(f164,plain,
( ~ sQ3_spl
| ~ sQ11_spl
| ~ sQ4_spl
| ~ sQ16_spl ),
inference(split_clause,[status(thm)],[f146,f161,f65,f103,f61]) ).
fof(f165,plain,
( sQ16_spl
| ~ sQ3_spl
| multiply(sk_c3,sk_c4) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f62,f163]) ).
fof(f166,plain,
( sQ16_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sk_c6 != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f58,f165]) ).
fof(f167,plain,
( sQ16_spl
| ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f166]) ).
fof(f168,plain,
( sQ16_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f167]) ).
fof(f173,plain,
( ~ sQ7_spl
| ~ sQ10_spl
| inverse(sk_c2) != sk_c5
| sk_c6 != sk_c6 ),
inference(paramodulation,[status(thm)],[f84,f101]) ).
fof(f182,definition,
( sQ19_spl
<=> sk_c6 = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f184,plain,
( sQ19_spl
| sk_c6 != sk_c6 ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f185,plain,
( ~ sQ7_spl
| ~ sQ10_spl
| ~ sQ8_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f173,f182,f90,f100,f83]) ).
fof(f190,plain,
( sQ19_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f184]) ).
fof(f191,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f190]) ).
fof(f193,plain,
( ~ sQ3_spl
| multiply(sk_c4,sk_c3) = identity ),
inference(paramodulation,[status(thm)],[f62,f26]) ).
fof(f194,plain,
( ~ sQ6_spl
| multiply(sk_c7,sk_c1) = identity ),
inference(paramodulation,[status(thm)],[f77,f26]) ).
fof(f195,plain,
! [X0,X1] : multiply(identity,X0) = multiply(inverse(X1),multiply(X1,X0)),
inference(paramodulation,[status(thm)],[f26,f27]) ).
fof(f196,plain,
! [X0,X1] : X0 = multiply(inverse(X1),multiply(X1,X0)),
inference(forward_demodulation,[status(thm)],[f25,f195]) ).
fof(f213,plain,
( ~ sQ10_spl
| inverse(inverse(sk_c5)) != sk_c5
| identity != sk_c6 ),
inference(paramodulation,[status(thm)],[f26,f101]) ).
fof(f218,definition,
( sQ21_spl
<=> identity = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f220,plain,
( sQ21_spl
| identity != sk_c6 ),
inference(component_clause,[status(thm)],[f218]) ).
fof(f221,definition,
( sQ22_spl
<=> inverse(inverse(sk_c5)) = sk_c5 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( sQ22_spl
| inverse(inverse(sk_c5)) != sk_c5 ),
inference(component_clause,[status(thm)],[f221]) ).
fof(f224,plain,
( ~ sQ10_spl
| ~ sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f213,f218,f221,f100]) ).
fof(f252,plain,
( ~ sQ4_spl
| sk_c5 = multiply(inverse(sk_c4),sk_c6) ),
inference(paramodulation,[status(thm)],[f66,f196]) ).
fof(f253,plain,
( ~ sQ3_spl
| sk_c3 = multiply(inverse(sk_c4),identity) ),
inference(paramodulation,[status(thm)],[f193,f196]) ).
fof(f256,plain,
! [X0,X1] : multiply(X0,X1) = multiply(inverse(inverse(X0)),X1),
inference(paramodulation,[status(thm)],[f196,f196]) ).
fof(f257,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),identity),
inference(paramodulation,[status(thm)],[f26,f196]) ).
fof(f258,plain,
! [X0] : X0 = multiply(inverse(identity),X0),
inference(paramodulation,[status(thm)],[f25,f196]) ).
fof(f263,plain,
( ~ sQ2_spl
| sk_c4 = multiply(inverse(sk_c3),sk_c6) ),
inference(paramodulation,[status(thm)],[f58,f196]) ).
fof(f266,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| sk_c4 = multiply(sk_c4,sk_c6) ),
inference(forward_demodulation,[status(thm)],[f62,f263]) ).
fof(f273,plain,
! [X0] : X0 = multiply(inverse(inverse(identity)),X0),
inference(paramodulation,[status(thm)],[f258,f196]) ).
fof(f280,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| sk_c6 = multiply(inverse(sk_c4),sk_c4) ),
inference(paramodulation,[status(thm)],[f266,f196]) ).
fof(f283,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| sk_c6 = identity ),
inference(forward_demodulation,[status(thm)],[f26,f280]) ).
fof(f284,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f283,f220]) ).
fof(f285,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f284]) ).
fof(f325,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sk_c3 = multiply(inverse(sk_c4),sk_c6) ),
inference(forward_demodulation,[status(thm)],[f283,f253]) ).
fof(f327,plain,
( sQ22_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ4_spl
| inverse(inverse(sk_c5)) != sk_c3 ),
inference(backward_demodulation,[status(thm)],[f336,f223]) ).
fof(f336,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ4_spl
| sk_c3 = sk_c5 ),
inference(forward_demodulation,[status(thm)],[f252,f325]) ).
fof(f337,plain,
( sQ22_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ4_spl
| inverse(inverse(sk_c3)) != sk_c3 ),
inference(forward_demodulation,[status(thm)],[f336,f327]) ).
fof(f338,plain,
( sQ22_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ4_spl
| inverse(sk_c4) != sk_c3 ),
inference(forward_demodulation,[status(thm)],[f62,f337]) ).
fof(f355,definition,
( sQ29_spl
<=> inverse(sk_c4) = sk_c3 ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f357,plain,
( sQ29_spl
| inverse(sk_c4) != sk_c3 ),
inference(component_clause,[status(thm)],[f355]) ).
fof(f363,definition,
( sQ31_spl
<=> inverse(inverse(sk_c3)) = sk_c3 ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f365,plain,
( sQ31_spl
| inverse(inverse(sk_c3)) != sk_c3 ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f373,plain,
( ~ sQ7_spl
| sk_c5 = multiply(inverse(sk_c2),sk_c6) ),
inference(paramodulation,[status(thm)],[f84,f196]) ).
fof(f375,plain,
( ~ sQ7_spl
| ~ sQ8_spl
| sk_c5 = multiply(sk_c5,sk_c6) ),
inference(forward_demodulation,[status(thm)],[f91,f373]) ).
fof(f376,plain,
( ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| sk_c5 = sk_c7 ),
inference(forward_demodulation,[status(thm)],[f54,f375]) ).
fof(f389,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| multiply(sk_c5,sk_c1) = identity ),
inference(forward_demodulation,[status(thm)],[f376,f194]) ).
fof(f390,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| sk_c1 = multiply(inverse(sk_c5),identity) ),
inference(paramodulation,[status(thm)],[f389,f196]) ).
fof(f401,definition,
( sQ32_spl
<=> multiply(identity,inverse(identity)) = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f403,plain,
( sQ32_spl
| multiply(identity,inverse(identity)) != sk_c6 ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f421,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| multiply(sk_c6,X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f283,f25]) ).
fof(f445,plain,
( sQ31_spl
| ~ sQ3_spl
| inverse(sk_c4) != sk_c3 ),
inference(forward_demodulation,[status(thm)],[f62,f365]) ).
fof(f476,plain,
! [X0] :
( ~ sQ5_spl
| multiply(sk_c6,X0) = multiply(sk_c1,multiply(sk_c7,X0)) ),
inference(paramodulation,[status(thm)],[f70,f27]) ).
fof(f502,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),identity),
inference(paramodulation,[status(thm)],[f26,f196]) ).
fof(f508,plain,
( ~ sQ8_spl
| multiply(sk_c5,sk_c2) = identity ),
inference(paramodulation,[status(thm)],[f91,f26]) ).
fof(f538,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| multiply(sk_c5,X0) = multiply(sk_c5,multiply(sk_c6,X0)) ),
inference(forward_demodulation,[status(thm)],[f376,f109]) ).
fof(f539,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| multiply(sk_c6,X0) = multiply(inverse(sk_c5),multiply(sk_c5,X0)) ),
inference(paramodulation,[status(thm)],[f538,f196]) ).
fof(f541,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| multiply(sk_c6,X0) = X0 ),
inference(forward_demodulation,[status(thm)],[f196,f539]) ).
fof(f546,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| X0 = multiply(inverse(sk_c6),X0) ),
inference(paramodulation,[status(thm)],[f541,f196]) ).
fof(f552,plain,
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sk_c6 = identity ),
inference(paramodulation,[status(thm)],[f26,f546]) ).
fof(f564,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| multiply(inverse(X0),X0) = sk_c6 ),
inference(backward_demodulation,[status(thm)],[f283,f26]) ).
fof(f623,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| X0 = multiply(inverse(inverse(X0)),sk_c6) ),
inference(paramodulation,[status(thm)],[f564,f196]) ).
fof(f671,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| X0 = multiply(inverse(inverse(sk_c6)),X0) ),
inference(forward_demodulation,[status(thm)],[f283,f273]) ).
fof(f674,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| inverse(sk_c6) = sk_c6 ),
inference(paramodulation,[status(thm)],[f564,f671]) ).
fof(f811,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| multiply(inverse(X0),X0) = sk_c6 ),
inference(forward_demodulation,[status(thm)],[f552,f26]) ).
fof(f819,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| multiply(sk_c5,sk_c1) = sk_c6 ),
inference(forward_demodulation,[status(thm)],[f552,f389]) ).
fof(f829,plain,
( ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ7_spl
| multiply(sk_c5,sk_c2) = sk_c6 ),
inference(forward_demodulation,[status(thm)],[f552,f508]) ).
fof(f846,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| X0 = multiply(sk_c1,multiply(sk_c7,X0)) ),
inference(forward_demodulation,[status(thm)],[f541,f476]) ).
fof(f847,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| X0 = multiply(sk_c1,multiply(sk_c5,X0)) ),
inference(forward_demodulation,[status(thm)],[f376,f846]) ).
fof(f848,plain,
( ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ5_spl
| sk_c2 = multiply(sk_c1,sk_c6) ),
inference(paramodulation,[status(thm)],[f829,f847]) ).
fof(f849,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sk_c1 = multiply(sk_c1,sk_c6) ),
inference(paramodulation,[status(thm)],[f819,f847]) ).
fof(f863,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sk_c1 = sk_c2 ),
inference(forward_demodulation,[status(thm)],[f848,f849]) ).
fof(f874,definition,
( sQ47_spl
<=> multiply(inverse(sk_c6),inverse(inverse(sk_c6))) = sk_c6 ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f876,plain,
( sQ47_spl
| multiply(inverse(sk_c6),inverse(inverse(sk_c6))) != sk_c6 ),
inference(component_clause,[status(thm)],[f874]) ).
fof(f893,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| inverse(X0) != sk_c7
| multiply(X0,sk_c5) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f376,f98]) ).
fof(f894,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| inverse(X0) != sk_c5
| multiply(X0,sk_c5) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f376,f893]) ).
fof(f896,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| X0 = multiply(inverse(inverse(X0)),sk_c6) ),
inference(forward_demodulation,[status(thm)],[f552,f502]) ).
fof(f907,plain,
( ~ sQ7_spl
| ~ sQ9_spl
| ~ sQ8_spl
| ~ sQ1_spl
| inverse(sk_c2) != sk_c5 ),
inference(resolution,[status(thm)],[f894,f84]) ).
fof(f913,plain,
( ~ sQ7_spl
| ~ sQ9_spl
| ~ sQ1_spl
| ~ sQ8_spl ),
inference(split_clause,[status(thm)],[f907,f90,f53,f97,f83]) ).
fof(f946,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sk_c2 = multiply(inverse(sk_c5),identity) ),
inference(forward_demodulation,[status(thm)],[f863,f390]) ).
fof(f947,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sk_c2 = multiply(inverse(sk_c5),sk_c6) ),
inference(forward_demodulation,[status(thm)],[f552,f946]) ).
fof(f1004,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| X0 = multiply(X0,sk_c6) ),
inference(backward_demodulation,[status(thm)],[f256,f896]) ).
fof(f1020,plain,
( ~ sQ6_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ5_spl
| sk_c2 = inverse(sk_c5) ),
inference(backward_demodulation,[status(thm)],[f1004,f947]) ).
fof(f1021,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sk_c4 = inverse(sk_c3) ),
inference(backward_demodulation,[status(thm)],[f1004,f263]) ).
fof(f1035,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1021,f61,f90,f83,f53,f57]) ).
fof(f1040,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| X0 = multiply(X0,sk_c6) ),
inference(forward_demodulation,[status(thm)],[f256,f623]) ).
fof(f1046,plain,
! [X0] : X0 = multiply(X0,identity),
inference(forward_demodulation,[status(thm)],[f256,f257]) ).
fof(f1077,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| inverse(inverse(X0)) = multiply(X0,sk_c6) ),
inference(paramodulation,[status(thm)],[f256,f1040]) ).
fof(f1086,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ3_spl
| inverse(inverse(X0)) = X0 ),
inference(forward_demodulation,[status(thm)],[f1040,f1077]) ).
fof(f1099,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ9_spl
| inverse(inverse(sk_c7)) != sk_c7
| sk_c6 != sk_c6 ),
inference(paramodulation,[status(thm)],[f564,f98]) ).
fof(f1108,definition,
( sQ51_spl
<=> inverse(inverse(sk_c7)) = sk_c7 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1110,plain,
( sQ51_spl
| inverse(inverse(sk_c7)) != sk_c7 ),
inference(component_clause,[status(thm)],[f1108]) ).
fof(f1111,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ9_spl
| ~ sQ51_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f1099,f182,f1108,f97,f61,f57]) ).
fof(f1121,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| inverse(sk_c4) = sk_c3 ),
inference(paramodulation,[status(thm)],[f62,f1086]) ).
fof(f1124,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sQ22_spl
| ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1121,f338]) ).
fof(f1125,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sQ22_spl
| ~ sQ4_spl ),
inference(contradiction_clause,[status(thm)],[f1124]) ).
fof(f1126,plain,
( ~ sQ1_spl
| ~ sQ2_spl
| ~ sQ3_spl
| sk_c5 = sk_c7 ),
inference(forward_demodulation,[status(thm)],[f1040,f54]) ).
fof(f1149,plain,
( sQ31_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sk_c3 != sk_c3 ),
inference(forward_demodulation,[status(thm)],[f1121,f445]) ).
fof(f1150,plain,
( sQ31_spl
| ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1149]) ).
fof(f1151,plain,
( sQ31_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1150]) ).
fof(f1152,plain,
( sQ29_spl
| ~ sQ3_spl
| ~ sQ2_spl
| sk_c3 != sk_c3 ),
inference(forward_demodulation,[status(thm)],[f1121,f357]) ).
fof(f1153,plain,
( sQ29_spl
| ~ sQ3_spl
| ~ sQ2_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1152]) ).
fof(f1154,plain,
( sQ29_spl
| ~ sQ3_spl
| ~ sQ2_spl ),
inference(contradiction_clause,[status(thm)],[f1153]) ).
fof(f1321,plain,
( sQ51_spl
| ~ sQ2_spl
| ~ sQ3_spl
| sk_c7 != sk_c7 ),
inference(forward_demodulation,[status(thm)],[f1086,f1110]) ).
fof(f1322,plain,
( sQ51_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sk_c5 != sk_c7 ),
inference(forward_demodulation,[status(thm)],[f1126,f1321]) ).
fof(f1323,plain,
( sQ51_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sk_c5 != sk_c5 ),
inference(forward_demodulation,[status(thm)],[f1126,f1322]) ).
fof(f1324,plain,
( sQ51_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1323]) ).
fof(f1325,plain,
( sQ51_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1324]) ).
fof(f1328,plain,
( sQ47_spl
| ~ sQ2_spl
| ~ sQ3_spl
| multiply(sk_c6,inverse(inverse(sk_c6))) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f674,f876]) ).
fof(f1329,plain,
( sQ47_spl
| ~ sQ2_spl
| ~ sQ3_spl
| inverse(inverse(sk_c6)) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f421,f1328]) ).
fof(f1330,plain,
( sQ47_spl
| ~ sQ2_spl
| ~ sQ3_spl
| sk_c6 != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f1086,f1329]) ).
fof(f1331,plain,
( sQ47_spl
| ~ sQ2_spl
| ~ sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1330]) ).
fof(f1332,plain,
( sQ47_spl
| ~ sQ2_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f1331]) ).
fof(f1340,plain,
( sQ32_spl
| ~ sQ2_spl
| ~ sQ3_spl
| multiply(sk_c6,inverse(identity)) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f283,f403]) ).
fof(f1341,plain,
( sQ32_spl
| ~ sQ2_spl
| ~ sQ3_spl
| inverse(identity) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f421,f1340]) ).
fof(f1342,plain,
( sQ32_spl
| ~ sQ2_spl
| ~ sQ3_spl
| inverse(sk_c6) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f283,f1341]) ).
fof(f1343,plain,
( sQ32_spl
| ~ sQ2_spl
| ~ sQ3_spl
| sk_c6 != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f674,f1342]) ).
fof(f1344,plain,
( sQ32_spl
| ~ sQ2_spl
| ~ sQ3_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1343]) ).
fof(f1345,plain,
( sQ32_spl
| ~ sQ2_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f1344]) ).
fof(f1396,plain,
( sQ0_spl
| ~ sQ2_spl
| ~ sQ3_spl
| sk_c7 != sk_c5 ),
inference(forward_demodulation,[status(thm)],[f1040,f52]) ).
fof(f1397,plain,
( sQ0_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| sk_c5 != sk_c5 ),
inference(forward_demodulation,[status(thm)],[f1126,f1396]) ).
fof(f1398,plain,
( sQ0_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1397]) ).
fof(f1399,plain,
( sQ0_spl
| ~ sQ2_spl
| ~ sQ3_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1398]) ).
fof(f1447,plain,
( ~ sQ11_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| multiply(sk_c5,inverse(sk_c5)) != sk_c6 ),
inference(resolution,[status(thm)],[f811,f107]) ).
fof(f1457,plain,
( ~ sQ11_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ6_spl
| ~ sQ5_spl
| multiply(sk_c5,sk_c2) != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f1020,f1447]) ).
fof(f1471,plain,
( ~ sQ8_spl
| ~ sQ1_spl
| ~ sQ7_spl
| multiply(sk_c5,sk_c2) = sk_c6 ),
inference(forward_demodulation,[status(thm)],[f552,f508]) ).
fof(f1507,plain,
( ~ sQ11_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ6_spl
| ~ sQ5_spl
| sk_c6 != sk_c6 ),
inference(forward_demodulation,[status(thm)],[f1471,f1457]) ).
fof(f1508,plain,
( ~ sQ11_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ6_spl
| ~ sQ5_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f1507]) ).
fof(f1509,plain,
( ~ sQ11_spl
| ~ sQ1_spl
| ~ sQ7_spl
| ~ sQ8_spl
| ~ sQ6_spl
| ~ sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f1508]) ).
fof(f1533,plain,
! [X0] : X0 = multiply(inverse(inverse(X0)),identity),
inference(paramodulation,[status(thm)],[f26,f196]) ).
fof(f1535,plain,
! [X0] : X0 = inverse(inverse(X0)),
inference(forward_demodulation,[status(thm)],[f1046,f1533]) ).
fof(f1546,plain,
( ~ sQ8_spl
| sk_c2 = inverse(sk_c5) ),
inference(paramodulation,[status(thm)],[f91,f1535]) ).
fof(f1552,plain,
( ~ sQ8_spl
| multiply(sk_c2,sk_c5) = identity ),
inference(paramodulation,[status(thm)],[f1546,f26]) ).
fof(f1555,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sk_c6 = identity ),
inference(forward_demodulation,[status(thm)],[f84,f1552]) ).
fof(f1563,plain,
! [X0] :
( ~ sQ8_spl
| ~ sQ7_spl
| X0 = multiply(X0,sk_c6) ),
inference(backward_demodulation,[status(thm)],[f1555,f1046]) ).
fof(f1589,plain,
( sQ1_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sk_c5 != sk_c7 ),
inference(backward_demodulation,[status(thm)],[f1563,f55]) ).
fof(f1590,plain,
( ~ sQ0_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sk_c7 = sk_c5 ),
inference(backward_demodulation,[status(thm)],[f1563,f51]) ).
fof(f1599,plain,
( ~ sQ0_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1590,f1589]) ).
fof(f1600,plain,
( ~ sQ0_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f1599]) ).
fof(f1601,plain,
$false,
inference(sat_refutation,[status(thm)],[f56,f60,f73,f75,f80,f82,f86,f87,f88,f89,f93,f94,f95,f96,f106,f164,f168,f185,f191,f224,f285,f913,f1035,f1111,f1125,f1151,f1154,f1325,f1332,f1345,f1399,f1509,f1600]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP292-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.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.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:11:50 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.38 % Drodi V4.1.1
% 0.13/0.41 % Refutation found
% 0.13/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.13/0.43 % Elapsed time: 0.061862 seconds
% 0.13/0.43 % CPU time: 0.233697 seconds
% 0.13/0.43 % Total memory used: 105.021 MB
% 0.13/0.43 % Net memory used: 104.643 MB
%------------------------------------------------------------------------------