%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG012-1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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 11:47:44 AM UTC 2026
% Result : Unsatisfiable 9.63s 1.79s
% Output : CNFRefutation 9.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 35
% Syntax : Number of formulae : 161 ( 18 unt; 24 def)
% Number of atoms : 577 ( 2 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 870 ( 454 ~; 392 |; 0 &)
% ( 24 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 25 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 264 ( 264 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] : f(X,f(Y,Z)) = f(f(X,Y),Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X] :
( d2(X)
| d1(X)
| c(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,hypothesis,
! [X] :
( ~ d1(X)
| ~ c(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,hypothesis,
! [X] :
( ~ d2(X)
| ~ c(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,hypothesis,
! [X] :
( ~ d2(X)
| ~ d1(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
c(a1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
d1(a2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
d2(a3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
! [X,Y] :
( ~ c(Y)
| ~ c(X)
| d1(f(X,Y))
| d2(f(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
! [X,Y] :
( ~ d1(Y)
| ~ d1(X)
| c(f(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
! [X,Y] :
( ~ d2(Y)
| ~ d2(X)
| c(f(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,plain,
! [X0,X1,X2] : f(X0,f(X1,X2)) = f(f(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f13,plain,
! [X0] :
( d2(X0)
| d1(X0)
| c(X0) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f14,plain,
! [X0] :
( ~ d1(X0)
| ~ c(X0) ),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f15,plain,
! [X0] :
( ~ d2(X0)
| ~ c(X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f16,plain,
! [X0] :
( ~ d2(X0)
| ~ d1(X0) ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f17,plain,
c(a1),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f18,plain,
d1(a2),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f19,plain,
d2(a3),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f20,plain,
! [Y] :
( ~ c(Y)
| ! [X] :
( ~ c(X)
| d1(f(X,Y))
| d2(f(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f21,plain,
! [X0,X1] :
( ~ c(X1)
| ~ c(X0)
| d1(f(X0,X1))
| d2(f(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f22,plain,
! [Y] :
( ~ d1(Y)
| ! [X] :
( ~ d1(X)
| c(f(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f23,plain,
! [X0,X1] :
( ~ d1(X1)
| ~ d1(X0)
| c(f(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [Y] :
( ~ d2(Y)
| ! [X] :
( ~ d2(X)
| c(f(X,Y)) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f25,plain,
! [X0,X1] :
( ~ d2(X1)
| ~ d2(X0)
| c(f(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f26,plain,
! [X0,X1] :
( ~ c(X1)
| ~ c(X0)
| d1(f(X0,X1))
| ~ c(f(X0,X1)) ),
inference(resolution,[status(thm)],[f15,f21]) ).
fof(f27,plain,
! [X0,X1] :
( ~ c(X1)
| ~ c(X0)
| ~ c(f(X0,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26,f14]) ).
fof(f28,plain,
! [X0,X1] :
( ~ d2(X1)
| ~ d2(X0)
| ~ c(X1)
| ~ c(X0) ),
inference(resolution,[status(thm)],[f27,f25]) ).
fof(f29,plain,
! [X0,X1] :
( ~ d1(X1)
| ~ d1(X0)
| ~ c(X1)
| ~ c(X0) ),
inference(resolution,[status(thm)],[f27,f23]) ).
fof(f30,definition,
! [X0] :
( sQ0_spl
<=> ( ~ d2(X0)
| ~ c(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f33,plain,
sQ0_spl,
inference(split_clause,[status(thm)],[f28,f30]) ).
fof(f34,definition,
! [X0] :
( sQ1_spl
<=> ( ~ d1(X0)
| ~ c(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f37,plain,
sQ1_spl,
inference(split_clause,[status(thm)],[f29,f34]) ).
fof(f43,plain,
! [X0,X1,X2] :
( ~ c(X2)
| ~ c(f(X0,X1))
| ~ c(f(X0,f(X1,X2))) ),
inference(paramodulation,[status(thm)],[f12,f27]) ).
fof(f45,plain,
! [X0,X1,X2] :
( ~ d2(X2)
| ~ d2(f(X0,X1))
| c(f(X0,f(X1,X2))) ),
inference(paramodulation,[status(thm)],[f12,f25]) ).
fof(f46,plain,
! [X0,X1,X2] :
( ~ d1(X2)
| ~ d1(f(X0,X1))
| c(f(X0,f(X1,X2))) ),
inference(paramodulation,[status(thm)],[f12,f23]) ).
fof(f50,plain,
! [X0,X1,X2] :
( ~ d2(f(X1,X2))
| ~ d2(X0)
| ~ c(X2)
| ~ c(f(X0,X1)) ),
inference(resolution,[status(thm)],[f43,f25]) ).
fof(f51,plain,
! [X0,X1,X2] :
( ~ d1(f(X1,X2))
| ~ d1(X0)
| ~ c(X2)
| ~ c(f(X0,X1)) ),
inference(resolution,[status(thm)],[f43,f23]) ).
fof(f56,plain,
! [X0,X1,X2] :
( ~ c(f(X1,X2))
| ~ c(X0)
| ~ d2(X2)
| ~ d2(f(X0,X1)) ),
inference(resolution,[status(thm)],[f45,f27]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ~ c(f(X1,X2))
| ~ c(X0)
| ~ d1(X2)
| ~ d1(f(X0,X1)) ),
inference(resolution,[status(thm)],[f46,f27]) ).
fof(f73,plain,
! [X0,X1,X2] :
( ~ c(X2)
| ~ c(X1)
| d1(f(X1,X2))
| ~ d2(X0)
| ~ c(X2)
| ~ c(f(X0,X1)) ),
inference(resolution,[status(thm)],[f50,f21]) ).
fof(f76,plain,
! [X0,X1,X2] :
( ~ c(X1)
| d1(f(X1,X2))
| ~ d2(X0)
| ~ c(X2)
| ~ c(f(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f73]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ c(X2)
| ~ c(X1)
| d1(f(X1,X2))
| ~ c(f(X2,X0))
| ~ c(X1)
| ~ d2(X0) ),
inference(resolution,[status(thm)],[f56,f21]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ c(X2)
| d1(f(X1,X2))
| ~ c(f(X2,X0))
| ~ c(X1)
| ~ d2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f79]) ).
fof(f103,plain,
~ d1(a3),
inference(resolution,[status(thm)],[f19,f16]) ).
fof(f104,plain,
~ c(a3),
inference(resolution,[status(thm)],[f19,f15]) ).
fof(f105,plain,
( d2(a3)
| c(a3) ),
inference(resolution,[status(thm)],[f103,f13]) ).
fof(f106,definition,
( sQ4_spl
<=> c(a3) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f107,plain,
( ~ sQ4_spl
| c(a3) ),
inference(component_clause,[status(thm)],[f106]) ).
fof(f109,definition,
( sQ5_spl
<=> d2(a3) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f112,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f105,f106,f109]) ).
fof(f113,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f107,f104]) ).
fof(f114,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f113]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( ~ c(f(X2,X3))
| ~ c(X1)
| ~ d1(X3)
| ~ c(X1)
| ~ d2(X0)
| ~ c(X2)
| ~ c(f(X0,X1)) ),
inference(resolution,[status(thm)],[f76,f65]) ).
fof(f116,plain,
! [X0,X1,X2,X3] :
( ~ d1(X3)
| ~ c(X2)
| ~ c(f(X3,X1))
| ~ c(X1)
| ~ d2(X0)
| ~ c(X2)
| ~ c(f(X0,X1)) ),
inference(resolution,[status(thm)],[f76,f51]) ).
fof(f119,definition,
! [X0,X1] :
( sQ6_spl
<=> ( ~ c(X1)
| ~ c(X1)
| ~ d2(X0)
| ~ c(f(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f120,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ c(X1)
| ~ c(X1)
| ~ d2(X0)
| ~ c(f(X0,X1)) ),
inference(component_clause,[status(thm)],[f119]) ).
fof(f122,definition,
! [X2,X3] :
( sQ7_spl
<=> ( ~ c(f(X2,X3))
| ~ d1(X3)
| ~ c(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f123,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ c(f(X0,X1))
| ~ d1(X1)
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f122]) ).
fof(f125,plain,
( sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f115,f119,f122]) ).
fof(f126,definition,
! [X0,X1,X3] :
( sQ8_spl
<=> ( ~ d1(X3)
| ~ c(f(X3,X1))
| ~ c(X1)
| ~ d2(X0)
| ~ c(f(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f129,definition,
! [X2] :
( sQ9_spl
<=> ( ~ c(X2)
| ~ c(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f130,plain,
! [X0] :
( ~ sQ9_spl
| ~ c(X0)
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f129]) ).
fof(f132,plain,
( sQ9_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f116,f126,f129]) ).
fof(f133,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ c(X1)
| ~ d2(X0)
| ~ c(f(X0,X1)) ),
inference(duplicate_literals_removal,[status(thm)],[f120]) ).
fof(f139,plain,
! [X0,X1,X2] :
( ~ sQ6_spl
| ~ c(X2)
| ~ d2(f(X0,X1))
| ~ c(f(X0,f(X1,X2))) ),
inference(paramodulation,[status(thm)],[f12,f133]) ).
fof(f140,definition,
! [X0] :
( sQ10_spl
<=> ( ~ d2(X0)
| ~ d2(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f141,plain,
! [X0] :
( ~ sQ10_spl
| ~ d2(X0)
| ~ d2(X0) ),
inference(component_clause,[status(thm)],[f140]) ).
fof(f159,plain,
! [X0,X1,X2] :
( ~ sQ6_spl
| ~ d1(f(X1,X2))
| ~ d1(X0)
| ~ c(X2)
| ~ d2(f(X0,X1)) ),
inference(resolution,[status(thm)],[f139,f23]) ).
fof(f178,plain,
! [X0,X1,X2] :
( ~ sQ6_spl
| d1(f(X1,X2))
| c(f(X1,X2))
| ~ d1(f(X2,X0))
| ~ d1(X1)
| ~ c(X0) ),
inference(resolution,[status(thm)],[f159,f13]) ).
fof(f181,plain,
! [X0,X1,X2] :
( ~ sQ6_spl
| d1(f(X1,X2))
| ~ d1(f(X2,X0))
| ~ d1(X1)
| ~ c(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f178,f51]) ).
fof(f193,plain,
! [X0,X1,X2,X3] :
( ~ sQ6_spl
| d1(f(X3,X1))
| ~ d1(X3)
| ~ c(X2)
| ~ c(X2)
| ~ c(f(X2,X0))
| ~ c(X1)
| ~ d2(X0) ),
inference(resolution,[status(thm)],[f82,f181]) ).
fof(f195,plain,
! [X0,X1,X2,X3] :
( ~ c(f(X2,X3))
| ~ c(X1)
| ~ d1(X3)
| ~ c(X2)
| ~ c(f(X2,X0))
| ~ c(X1)
| ~ d2(X0) ),
inference(resolution,[status(thm)],[f82,f65]) ).
fof(f196,plain,
! [X0,X1,X2,X3] :
( ~ d1(X3)
| ~ c(X2)
| ~ c(f(X3,X1))
| ~ c(X2)
| ~ c(f(X2,X0))
| ~ c(X1)
| ~ d2(X0) ),
inference(resolution,[status(thm)],[f82,f51]) ).
fof(f199,definition,
! [X0,X2] :
( sQ14_spl
<=> ( ~ c(X2)
| ~ c(X2)
| ~ c(f(X2,X0))
| ~ d2(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f200,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ c(X1)
| ~ c(X1)
| ~ c(f(X1,X0))
| ~ d2(X0) ),
inference(component_clause,[status(thm)],[f199]) ).
fof(f202,definition,
! [X1,X3] :
( sQ15_spl
<=> ( d1(f(X3,X1))
| ~ d1(X3)
| ~ c(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f203,plain,
! [X0,X1] :
( ~ sQ15_spl
| d1(f(X1,X0))
| ~ d1(X1)
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f202]) ).
fof(f205,plain,
( ~ sQ6_spl
| sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f193,f199,f202,f119]) ).
fof(f206,definition,
! [X0,X2,X3] :
( sQ16_spl
<=> ( ~ d1(X3)
| ~ c(f(X2,X3))
| ~ c(X2)
| ~ c(f(X2,X0))
| ~ d2(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f210,plain,
( sQ9_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f195,f206,f129]) ).
fof(f211,definition,
! [X1,X3] :
( sQ17_spl
<=> ( ~ d1(X3)
| ~ c(f(X3,X1))
| ~ c(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f212,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ d1(X1)
| ~ c(f(X1,X0))
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f211]) ).
fof(f214,plain,
( sQ17_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f196,f199,f211]) ).
fof(f215,plain,
! [X0,X1] :
( ~ sQ14_spl
| ~ c(X1)
| ~ c(f(X1,X0))
| ~ d2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f200]) ).
fof(f216,plain,
! [X0] :
( ~ sQ9_spl
| ~ c(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f130]) ).
fof(f218,plain,
( ~ sQ9_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f17,f216]) ).
fof(f225,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f218]) ).
fof(f271,plain,
! [X0,X1,X2] :
( ~ sQ17_spl
| ~ d1(f(X1,X2))
| ~ c(f(X1,f(X2,X0)))
| ~ c(X0) ),
inference(paramodulation,[status(thm)],[f12,f212]) ).
fof(f272,definition,
! [X1] :
( sQ18_spl
<=> ( ~ d1(X1)
| ~ d1(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f273,plain,
! [X0] :
( ~ sQ18_spl
| ~ d1(X0)
| ~ d1(X0) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f286,plain,
! [X0,X1,X2] :
( ~ sQ14_spl
| ~ d1(X1)
| ~ d1(f(X2,X0))
| ~ c(X2)
| ~ d2(f(X0,X1)) ),
inference(resolution,[status(thm)],[f215,f46]) ).
fof(f336,plain,
! [X0,X1,X2] :
( ~ sQ17_spl
| ~ d1(X0)
| ~ c(f(X1,X2))
| ~ d2(X2)
| ~ d2(f(X0,X1)) ),
inference(resolution,[status(thm)],[f45,f212]) ).
fof(f348,plain,
! [X0,X1,X2] :
( ~ sQ17_spl
| ~ d1(f(X2,X0))
| ~ d1(X1)
| ~ d1(f(X1,X2))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f271,f23]) ).
fof(f357,plain,
! [X0,X1,X2] :
( ~ sQ17_spl
| ~ sQ6_spl
| ~ d1(f(X2,X0))
| ~ d1(X1)
| ~ c(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f348,f181]) ).
fof(f364,definition,
! [X1] :
( sQ21_spl
<=> ~ d1(X1) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f365,plain,
! [X0] :
( ~ sQ21_spl
| ~ d1(X0) ),
inference(component_clause,[status(thm)],[f364]) ).
fof(f374,plain,
( ~ sQ21_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f18,f365]) ).
fof(f376,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f374]) ).
fof(f414,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ d1(f(X1,X2))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f123,f46]) ).
fof(f415,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ d2(X2)
| ~ d2(f(X0,X1))
| ~ d1(f(X1,X2))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f123,f45]) ).
fof(f455,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| d2(f(X1,X2))
| c(f(X1,X2))
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f414,f13]) ).
fof(f457,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| d2(f(X1,X2))
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f455,f65]) ).
fof(f506,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| ~ d2(X3)
| ~ d1(f(X2,X3))
| ~ c(X1)
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f457,f415]) ).
fof(f510,plain,
! [X0,X1,X2,X3] :
( ~ sQ7_spl
| ~ c(f(X2,X3))
| ~ c(X1)
| ~ d2(X3)
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f457,f56]) ).
fof(f514,definition,
! [X0,X1] :
( sQ23_spl
<=> ( ~ c(X1)
| ~ d1(f(X0,X1))
| ~ c(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f515,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ c(X1)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f514]) ).
fof(f517,definition,
! [X2,X3] :
( sQ24_spl
<=> ( ~ d2(X3)
| ~ d1(f(X2,X3))
| ~ d1(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f518,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ d2(X1)
| ~ d1(f(X0,X1))
| ~ d1(X0) ),
inference(component_clause,[status(thm)],[f517]) ).
fof(f520,plain,
( ~ sQ7_spl
| sQ24_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f506,f514,f517,f122]) ).
fof(f528,definition,
! [X2,X3] :
( sQ27_spl
<=> ( ~ c(f(X2,X3))
| ~ d2(X3)
| ~ d1(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f529,plain,
! [X0,X1] :
( ~ sQ27_spl
| ~ c(f(X0,X1))
| ~ d2(X1)
| ~ d1(X0) ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f536,plain,
( ~ sQ7_spl
| sQ27_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f510,f514,f528,f122]) ).
fof(f537,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ c(X1)
| ~ c(X0)
| d2(f(X0,X1)) ),
inference(backward_subsumption_resolution,[status(thm)],[f21,f515]) ).
fof(f541,plain,
! [X0,X1,X2] :
( ~ sQ7_spl
| ~ sQ23_spl
| ~ d2(X2)
| ~ d1(f(X1,X2))
| ~ c(X0)
| ~ c(X1)
| ~ c(X0) ),
inference(resolution,[status(thm)],[f537,f415]) ).
fof(f545,plain,
! [X0,X1,X2] :
( ~ sQ23_spl
| ~ c(f(X1,X2))
| ~ c(X0)
| ~ d2(X2)
| ~ c(X1)
| ~ c(X0) ),
inference(resolution,[status(thm)],[f537,f56]) ).
fof(f549,definition,
! [X1,X2] :
( sQ29_spl
<=> ( ~ d2(X2)
| ~ d1(f(X1,X2))
| ~ c(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f550,plain,
! [X0,X1] :
( ~ sQ29_spl
| ~ d2(X1)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f549]) ).
fof(f552,plain,
( ~ sQ7_spl
| ~ sQ23_spl
| sQ29_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f541,f129,f549,f514,f122]) ).
fof(f557,definition,
! [X1,X2] :
( sQ31_spl
<=> ( ~ c(f(X1,X2))
| ~ d2(X2)
| ~ c(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f558,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ c(f(X0,X1))
| ~ d2(X1)
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f557]) ).
fof(f565,plain,
( ~ sQ23_spl
| sQ31_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f545,f129,f557,f514]) ).
fof(f575,plain,
! [X0,X1,X2] :
( ~ sQ6_spl
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(f(X1,X2))
| ~ d2(X0) ),
inference(resolution,[status(thm)],[f133,f46]) ).
fof(f648,plain,
! [X0] :
( ~ sQ10_spl
| ~ d2(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f141]) ).
fof(f652,plain,
( ~ sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19,f648]) ).
fof(f654,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f652]) ).
fof(f688,plain,
! [X0,X1,X2] :
( ~ sQ14_spl
| d1(f(X1,X2))
| c(f(X1,X2))
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f286,f13]) ).
fof(f690,plain,
! [X0,X1,X2] :
( ~ sQ14_spl
| d1(f(X1,X2))
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f688,f65]) ).
fof(f791,plain,
! [X0,X1,X2,X3] :
( ~ sQ6_spl
| ~ sQ14_spl
| ~ d1(X3)
| ~ c(f(X2,X3))
| ~ d2(X1)
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f690,f575]) ).
fof(f793,plain,
! [X0,X1,X2,X3] :
( ~ sQ14_spl
| ~ c(f(X2,X3))
| ~ c(X1)
| ~ d1(X3)
| ~ d1(X2)
| ~ d1(f(X0,X1))
| ~ c(X0) ),
inference(resolution,[status(thm)],[f690,f65]) ).
fof(f801,definition,
! [X2,X3] :
( sQ34_spl
<=> ( ~ d1(X3)
| ~ c(f(X2,X3))
| ~ d1(X2) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f802,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ d1(X1)
| ~ c(f(X0,X1))
| ~ d1(X0) ),
inference(component_clause,[status(thm)],[f801]) ).
fof(f804,plain,
( ~ sQ6_spl
| ~ sQ14_spl
| sQ34_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f791,f549,f801,f199,f119]) ).
fof(f809,plain,
( ~ sQ14_spl
| sQ34_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f793,f514,f801,f199]) ).
fof(f818,plain,
! [X0,X1] :
( ~ sQ29_spl
| d2(f(X0,X1))
| c(f(X0,X1))
| ~ d2(X1)
| ~ c(X0) ),
inference(resolution,[status(thm)],[f550,f13]) ).
fof(f852,plain,
! [X0,X1] :
( ~ sQ29_spl
| ~ sQ31_spl
| d2(f(X0,X1))
| ~ d2(X1)
| ~ c(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f818,f558]) ).
fof(f861,plain,
! [X0,X1,X2] :
( ~ sQ29_spl
| ~ sQ31_spl
| ~ c(f(X1,X2))
| ~ c(X0)
| ~ d2(X2)
| ~ d2(X1)
| ~ c(X0) ),
inference(resolution,[status(thm)],[f852,f56]) ).
fof(f866,definition,
! [X1,X2] :
( sQ36_spl
<=> ( ~ c(f(X1,X2))
| ~ d2(X2)
| ~ d2(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f867,plain,
! [X0,X1] :
( ~ sQ36_spl
| ~ c(f(X0,X1))
| ~ d2(X1)
| ~ d2(X0) ),
inference(component_clause,[status(thm)],[f866]) ).
fof(f869,plain,
( ~ sQ29_spl
| ~ sQ31_spl
| sQ36_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f861,f129,f866,f557,f549]) ).
fof(f871,plain,
! [X0,X1] :
( ~ sQ36_spl
| ~ d2(X1)
| ~ d2(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f867,f25]) ).
fof(f881,definition,
! [X1] :
( sQ38_spl
<=> ~ d2(X1) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f882,plain,
! [X0] :
( ~ sQ38_spl
| ~ d2(X0) ),
inference(component_clause,[status(thm)],[f881]) ).
fof(f898,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ d1(X1)
| ~ d1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f23]) ).
fof(f899,plain,
! [X0] :
( ~ sQ18_spl
| ~ d1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f273]) ).
fof(f902,plain,
( ~ sQ36_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f871,f881,f866]) ).
fof(f903,plain,
( ~ sQ38_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f19,f882]) ).
fof(f906,plain,
~ sQ38_spl,
inference(contradiction_clause,[status(thm)],[f903]) ).
fof(f922,plain,
! [X0,X1] :
( ~ sQ24_spl
| d2(f(X0,X1))
| c(f(X0,X1))
| ~ d2(X1)
| ~ d1(X0) ),
inference(resolution,[status(thm)],[f518,f13]) ).
fof(f942,plain,
! [X0,X1] :
( ~ sQ24_spl
| ~ sQ27_spl
| d2(f(X0,X1))
| ~ d2(X1)
| ~ d1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f922,f529]) ).
fof(f1032,plain,
( ~ sQ18_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f899,f364,f272]) ).
fof(f1035,plain,
! [X0,X1,X2] :
( ~ sQ24_spl
| ~ sQ27_spl
| ~ sQ17_spl
| ~ d2(X1)
| ~ d1(X2)
| ~ d1(X2)
| ~ c(f(X1,X0))
| ~ d2(X0) ),
inference(resolution,[status(thm)],[f336,f942]) ).
fof(f1041,plain,
( ~ sQ24_spl
| ~ sQ27_spl
| ~ sQ17_spl
| sQ18_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1035,f866,f272,f211,f528,f517]) ).
fof(f1042,definition,
! [X0,X2] :
( sQ44_spl
<=> ( ~ d1(f(X2,X0))
| ~ c(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f1043,plain,
! [X0,X1] :
( ~ sQ44_spl
| ~ d1(f(X1,X0))
| ~ c(X0) ),
inference(component_clause,[status(thm)],[f1042]) ).
fof(f1045,plain,
( ~ sQ17_spl
| ~ sQ6_spl
| sQ21_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f357,f1042,f364,f119,f211]) ).
fof(f1051,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ sQ44_spl
| ~ d1(X1)
| ~ d1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f23,f1053]) ).
fof(f1053,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ sQ44_spl
| ~ d1(X1)
| ~ c(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f203,f1043]) ).
fof(f1064,plain,
( ~ sQ15_spl
| ~ sQ44_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f1051,f364,f1042,f202]) ).
fof(f1069,plain,
( ~ sQ34_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f898,f364,f801]) ).
fof(f1071,plain,
$false,
inference(sat_refutation,[status(thm)],[f33,f37,f112,f114,f125,f132,f205,f210,f214,f225,f376,f520,f536,f552,f565,f654,f804,f809,f869,f902,f906,f1032,f1041,f1045,f1064,f1069]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG012-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.47 % Computer : n008.cluster.edu
% 0.18/0.47 % Model : x86_64 x86_64
% 0.18/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.47 % Memory : 8046.5625MB
% 0.18/0.47 % OS : Linux 6.8.0-71-generic
% 0.18/0.47 % CPULimit : 300
% 0.18/0.47 % WCLimit : 300
% 0.18/0.47 % DateTime : Mon Sep 21 12:53:23 UTC 2026
% 0.18/0.47 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 9.63/1.79 % Refutation found
% 9.63/1.79 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.63/1.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 9.63/1.82 % Elapsed time: 1.329050 seconds
% 9.63/1.82 % CPU time: 9.993727 seconds
% 9.63/1.82 % Total memory used: 155.269 MB
% 9.63/1.82 % Net memory used: 145.045 MB
%------------------------------------------------------------------------------