%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET724+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 02:10:31 PM UTC 2026
% Result : Theorem 77.97s 10.31s
% Output : CNFRefutation 63.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 10
% Syntax : Number of formulae : 74 ( 8 unt; 6 def)
% Number of atoms : 388 ( 31 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 531 ( 217 ~; 227 |; 69 &)
% ( 12 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 7 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-7 aty)
% Number of variables : 263 ( 235 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f14,axiom,
! [G,F,A,B,C,X,Z] :
( ( member(Z,C)
& member(X,A) )
=> ( apply(compose_function(G,F,A,B,C),X,Z)
<=> ? [Y] :
( apply(G,Y,Z)
& apply(F,X,Y)
& member(Y,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [F,G,A,B] :
( equal_maps(F,G,A,B)
<=> ! [X,Y1,Y2] :
( ( member(Y2,B)
& member(Y1,B)
& member(X,A) )
=> ( ( apply(G,X,Y2)
& apply(F,X,Y1) )
=> Y1 = Y2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [F,A,B] :
( surjective(F,A,B)
<=> ! [Y] :
( member(Y,B)
=> ? [E] :
( apply(F,E,Y)
& member(E,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,conjecture,
! [F,G,H,A,B,C] :
( ( equal_maps(compose_function(G,F,A,B,C),compose_function(H,F,A,B,C),A,C)
& surjective(F,A,B)
& maps(H,B,C)
& maps(G,B,C)
& maps(F,A,B) )
=> equal_maps(G,H,B,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
~ ! [F,G,H,A,B,C] :
( ( equal_maps(compose_function(G,F,A,B,C),compose_function(H,F,A,B,C),A,C)
& surjective(F,A,B)
& maps(H,B,C)
& maps(G,B,C)
& maps(F,A,B) )
=> equal_maps(G,H,B,C) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
fof(f111,plain,
! [G,F,A,B,C,X,Z] :
( ( apply(compose_function(G,F,A,B,C),X,Z)
<=> ? [Y] :
( apply(G,Y,Z)
& apply(F,X,Y)
& member(Y,B) ) )
| ~ member(Z,C)
| ~ member(X,A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f112,plain,
! [G,F,A,B,C,X,Z] :
( ( ( ! [Y] :
( ~ apply(G,Y,Z)
| ~ apply(F,X,Y)
| ~ member(Y,B) )
| apply(compose_function(G,F,A,B,C),X,Z) )
& ( ? [Y] :
( apply(G,Y,Z)
& apply(F,X,Y)
& member(Y,B) )
| ~ apply(compose_function(G,F,A,B,C),X,Z) ) )
| ~ member(Z,C)
| ~ member(X,A) ),
inference(NNF_transformation,[status(thm)],[f111]) ).
fof(f113,plain,
! [A,C,X,Z] :
( ( ! [G,F,B] :
( ! [Y] :
( ~ apply(G,Y,Z)
| ~ apply(F,X,Y)
| ~ member(Y,B) )
| apply(compose_function(G,F,A,B,C),X,Z) )
& ! [G,F,B] :
( ? [Y] :
( apply(G,Y,Z)
& apply(F,X,Y)
& member(Y,B) )
| ~ apply(compose_function(G,F,A,B,C),X,Z) ) )
| ~ member(Z,C)
| ~ member(X,A) ),
inference(miniscoping,[status(thm)],[f112]) ).
fof(f114,plain,
! [A,C,X,Z] :
( ( ! [G,F,B] :
( ! [Y] :
( ~ apply(G,Y,Z)
| ~ apply(F,X,Y)
| ~ member(Y,B) )
| apply(compose_function(G,F,A,B,C),X,Z) )
& ! [G,F,B] :
( ( apply(G,sK11_skl(B,F,G,Z,X,C,A),Z)
& apply(F,X,sK11_skl(B,F,G,Z,X,C,A))
& member(sK11_skl(B,F,G,Z,X,C,A),B) )
| ~ apply(compose_function(G,F,A,B,C),X,Z) ) )
| ~ member(Z,C)
| ~ member(X,A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(Y,sK11_skl(B,F,G,Z,X,C,A))],[f113]) ).
fof(f118,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ member(X3,X6)
| ~ member(X4,X7)
| ~ apply(X5,X0,X3)
| apply(compose_function(X2,X5,X1,X6,X7),X0,X4)
| ~ apply(X2,X3,X4)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f119,plain,
! [F,G,A,B] :
( equal_maps(F,G,A,B)
<=> ! [X,Y1,Y2] :
( Y1 = Y2
| ~ apply(G,X,Y2)
| ~ apply(F,X,Y1)
| ~ member(Y2,B)
| ~ member(Y1,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f120,plain,
! [F,G,A,B] :
( ( ? [X,Y1,Y2] :
( Y1 != Y2
& apply(G,X,Y2)
& apply(F,X,Y1)
& member(Y2,B)
& member(Y1,B)
& member(X,A) )
| equal_maps(F,G,A,B) )
& ( ! [X,Y1,Y2] :
( Y1 = Y2
| ~ apply(G,X,Y2)
| ~ apply(F,X,Y1)
| ~ member(Y2,B)
| ~ member(Y1,B)
| ~ member(X,A) )
| ~ equal_maps(F,G,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f119]) ).
fof(f121,plain,
( ! [F,G,A,B] :
( ? [X,Y1,Y2] :
( Y1 != Y2
& apply(G,X,Y2)
& apply(F,X,Y1)
& member(Y2,B)
& member(Y1,B)
& member(X,A) )
| equal_maps(F,G,A,B) )
& ! [F,G,A,B] :
( ! [X,Y1,Y2] :
( Y1 = Y2
| ~ apply(G,X,Y2)
| ~ apply(F,X,Y1)
| ~ member(Y2,B)
| ~ member(Y1,B)
| ~ member(X,A) )
| ~ equal_maps(F,G,A,B) ) ),
inference(miniscoping,[status(thm)],[f120]) ).
fof(f122,plain,
( ! [F,G,A,B] :
( ( sK13_skl(B,A,G,F) != sK14_skl(B,A,G,F)
& apply(G,sK12_skl(B,A,G,F),sK14_skl(B,A,G,F))
& apply(F,sK12_skl(B,A,G,F),sK13_skl(B,A,G,F))
& member(sK14_skl(B,A,G,F),B)
& member(sK13_skl(B,A,G,F),B)
& member(sK12_skl(B,A,G,F),A) )
| equal_maps(F,G,A,B) )
& ! [F,G,A,B] :
( ! [X,Y1,Y2] :
( Y1 = Y2
| ~ apply(G,X,Y2)
| ~ apply(F,X,Y1)
| ~ member(Y2,B)
| ~ member(Y1,B)
| ~ member(X,A) )
| ~ equal_maps(F,G,A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl,sK14_skl]),skolemize(X,sK12_skl(B,A,G,F)),skolemize(Y1,sK13_skl(B,A,G,F)),skolemize(Y2,sK14_skl(B,A,G,F))],[f121]) ).
fof(f123,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X5 = X0
| ~ member(X5,X1)
| ~ equal_maps(X6,X4,X3,X1)
| ~ apply(X6,X2,X0)
| ~ apply(X4,X2,X5)
| ~ member(X2,X3)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( equal_maps(X3,X2,X1,X0)
| member(sK12_skl(X0,X1,X2,X3),X1) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f125,plain,
! [X0,X1,X2,X3] :
( member(sK13_skl(X3,X2,X1,X0),X3)
| equal_maps(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f126,plain,
! [X0,X1,X2,X3] :
( equal_maps(X3,X2,X1,X0)
| member(sK14_skl(X0,X1,X2,X3),X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f127,plain,
! [X0,X1,X2,X3] :
( equal_maps(X0,X3,X2,X1)
| apply(X0,sK12_skl(X1,X2,X3,X0),sK13_skl(X1,X2,X3,X0)) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( equal_maps(X3,X0,X2,X1)
| apply(X0,sK12_skl(X1,X2,X0,X3),sK14_skl(X1,X2,X0,X3)) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( sK14_skl(X3,X2,X1,X0) != sK13_skl(X3,X2,X1,X0)
| equal_maps(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f148,plain,
! [F,A,B] :
( surjective(F,A,B)
<=> ! [Y] :
( ? [E] :
( apply(F,E,Y)
& member(E,A) )
| ~ member(Y,B) ) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f149,plain,
! [F,A,B] :
( ( ? [Y] :
( ! [E] :
( ~ apply(F,E,Y)
| ~ member(E,A) )
& member(Y,B) )
| surjective(F,A,B) )
& ( ! [Y] :
( ? [E] :
( apply(F,E,Y)
& member(E,A) )
| ~ member(Y,B) )
| ~ surjective(F,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
( ! [F,A,B] :
( ? [Y] :
( ! [E] :
( ~ apply(F,E,Y)
| ~ member(E,A) )
& member(Y,B) )
| surjective(F,A,B) )
& ! [F,A,B] :
( ! [Y] :
( ? [E] :
( apply(F,E,Y)
& member(E,A) )
| ~ member(Y,B) )
| ~ surjective(F,A,B) ) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f151,plain,
( ! [F,A,B] :
( ( ! [E] :
( ~ apply(F,E,sK20_skl(B,A,F))
| ~ member(E,A) )
& member(sK20_skl(B,A,F),B) )
| surjective(F,A,B) )
& ! [F,A,B] :
( ! [Y] :
( ( apply(F,sK19_skl(Y,B,A,F),Y)
& member(sK19_skl(Y,B,A,F),A) )
| ~ member(Y,B) )
| ~ surjective(F,A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(E,sK19_skl(Y,B,A,F)),skolemize(Y,sK20_skl(B,A,F))],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3] :
( ~ surjective(X3,X2,X1)
| member(sK19_skl(X0,X1,X2,X3),X2)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [X0,X1,X2,X3] :
( ~ surjective(X2,X3,X1)
| apply(X2,sK19_skl(X0,X1,X3,X2),X0)
| ~ member(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f244,plain,
? [F,G,H,A,B,C] :
( ~ equal_maps(G,H,B,C)
& equal_maps(compose_function(G,F,A,B,C),compose_function(H,F,A,B,C),A,C)
& surjective(F,A,B)
& maps(H,B,C)
& maps(G,B,C)
& maps(F,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f245,plain,
? [G,H,B,C] :
( ~ equal_maps(G,H,B,C)
& ? [F,A] :
( equal_maps(compose_function(G,F,A,B,C),compose_function(H,F,A,B,C),A,C)
& surjective(F,A,B)
& maps(H,B,C)
& maps(G,B,C)
& maps(F,A,B) ) ),
inference(miniscoping,[status(thm)],[f244]) ).
fof(f246,plain,
( ~ equal_maps(sK39_skl,sK40_skl,sK41_skl,sK42_skl)
& equal_maps(compose_function(sK39_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK44_skl,sK42_skl)
& surjective(sK43_skl,sK44_skl,sK41_skl)
& maps(sK40_skl,sK41_skl,sK42_skl)
& maps(sK39_skl,sK41_skl,sK42_skl)
& maps(sK43_skl,sK44_skl,sK41_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl,sK40_skl,sK41_skl,sK42_skl,sK43_skl,sK44_skl]),skolemize(G,sK39_skl),skolemize(H,sK40_skl),skolemize(B,sK41_skl),skolemize(C,sK42_skl),skolemize(F,sK43_skl),skolemize(A,sK44_skl)],[f245]) ).
fof(f250,plain,
surjective(sK43_skl,sK44_skl,sK41_skl),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f251,plain,
equal_maps(compose_function(sK39_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK44_skl,sK42_skl),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f252,plain,
~ equal_maps(sK39_skl,sK40_skl,sK41_skl,sK42_skl),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f271,plain,
! [X0,X1,X2] :
( ~ apply(compose_function(sK39_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),X0,X2)
| ~ apply(compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),X0,X1)
| X2 = X1
| ~ member(X2,sK42_skl)
| ~ member(X1,sK42_skl)
| ~ member(X0,sK44_skl) ),
inference(resolution,[status(thm)],[f251,f123]) ).
fof(f619,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ member(X8,X7)
| ~ apply(X6,X0,X8)
| apply(compose_function(X6,X3,X4,X5,X7),sK19_skl(X0,X1,X2,X3),X8)
| ~ member(X0,X5)
| ~ surjective(X3,X2,X1)
| ~ member(X0,X1)
| ~ member(sK19_skl(X0,X1,X2,X3),X4) ),
inference(resolution,[status(thm)],[f153,f118]) ).
fof(f1472,plain,
sK13_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl) != sK14_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl),
inference(resolution,[status(thm)],[f129,f252]) ).
fof(f1474,plain,
! [X0] :
( ~ member(X0,sK41_skl)
| member(sK19_skl(X0,sK41_skl,sK44_skl,sK43_skl),sK44_skl) ),
inference(resolution,[status(thm)],[f152,f250]) ).
fof(f1511,plain,
! [X0,X1,X2] :
( ~ member(X1,sK41_skl)
| X0 = X2
| ~ member(X2,sK42_skl)
| ~ apply(compose_function(sK39_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),X0)
| ~ apply(compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),X2)
| ~ member(X0,sK42_skl) ),
inference(resolution,[status(thm)],[f1474,f271]) ).
fof(f2068,plain,
! [X0,X1,X2] :
( ~ member(X0,sK42_skl)
| ~ apply(sK39_skl,X1,X0)
| ~ member(X1,sK41_skl)
| ~ surjective(sK43_skl,sK44_skl,sK41_skl)
| ~ member(X1,sK41_skl)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X1,sK41_skl)
| X0 = X2
| ~ member(X2,sK42_skl)
| ~ apply(compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),X2)
| ~ member(X0,sK42_skl) ),
inference(resolution,[status(thm)],[f1511,f619]) ).
fof(f2069,definition,
! [X0,X1,X2] :
( sQ2_spl
<=> ( ~ member(X0,sK42_skl)
| ~ apply(sK39_skl,X1,X0)
| ~ member(X1,sK41_skl)
| ~ member(X1,sK41_skl)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X1,sK41_skl)
| X0 = X2
| ~ member(X2,sK42_skl)
| ~ apply(compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),X2)
| ~ member(X0,sK42_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f2070,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ member(X0,sK42_skl)
| ~ apply(sK39_skl,X1,X0)
| ~ member(X1,sK41_skl)
| ~ member(X1,sK41_skl)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X1,sK41_skl)
| X0 = X2
| ~ member(X2,sK42_skl)
| ~ apply(compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),X2)
| ~ member(X0,sK42_skl) ),
inference(component_clause,[status(thm)],[f2069]) ).
fof(f2072,definition,
( sQ3_spl
<=> surjective(sK43_skl,sK44_skl,sK41_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f2074,plain,
( sQ3_spl
| ~ surjective(sK43_skl,sK44_skl,sK41_skl) ),
inference(component_clause,[status(thm)],[f2072]) ).
fof(f2075,plain,
( ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f2068,f2069,f2072]) ).
fof(f2076,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ apply(sK39_skl,X1,X0)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X1,sK41_skl)
| X0 = X2
| ~ member(X2,sK42_skl)
| ~ apply(compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),X2)
| ~ member(X0,sK42_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f2070]) ).
fof(f2077,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ apply(compose_function(sK40_skl,sK43_skl,sK44_skl,sK41_skl,sK42_skl),sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),X0)
| X0 = X2
| ~ member(X2,sK42_skl)
| ~ member(X1,sK41_skl)
| ~ apply(sK39_skl,X1,X2)
| ~ member(X0,sK42_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2076,f1474]) ).
fof(f2281,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ member(X0,sK42_skl)
| ~ apply(sK40_skl,X1,X0)
| ~ member(X1,sK41_skl)
| ~ surjective(sK43_skl,sK44_skl,sK41_skl)
| ~ member(X1,sK41_skl)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X2,sK42_skl)
| X2 = X0
| ~ apply(sK39_skl,X1,X2)
| ~ member(X1,sK41_skl)
| ~ member(X0,sK42_skl) ),
inference(resolution,[status(thm)],[f2077,f619]) ).
fof(f2282,definition,
! [X0,X1,X2] :
( sQ4_spl
<=> ( ~ member(X0,sK42_skl)
| ~ apply(sK40_skl,X1,X0)
| ~ member(X1,sK41_skl)
| ~ member(X1,sK41_skl)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X2,sK42_skl)
| X2 = X0
| ~ apply(sK39_skl,X1,X2)
| ~ member(X1,sK41_skl)
| ~ member(X0,sK42_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f2283,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ member(X0,sK42_skl)
| ~ apply(sK40_skl,X1,X0)
| ~ member(X1,sK41_skl)
| ~ member(X1,sK41_skl)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X2,sK42_skl)
| X2 = X0
| ~ apply(sK39_skl,X1,X2)
| ~ member(X1,sK41_skl)
| ~ member(X0,sK42_skl) ),
inference(component_clause,[status(thm)],[f2282]) ).
fof(f2285,plain,
( ~ sQ2_spl
| ~ sQ3_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f2281,f2282,f2072,f2069]) ).
fof(f2286,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2074,f250]) ).
fof(f2287,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f2286]) ).
fof(f2288,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ apply(sK40_skl,X1,X0)
| ~ member(sK19_skl(X1,sK41_skl,sK44_skl,sK43_skl),sK44_skl)
| ~ member(X2,sK42_skl)
| X2 = X0
| ~ apply(sK39_skl,X1,X2)
| ~ member(X1,sK41_skl)
| ~ member(X0,sK42_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f2283]) ).
fof(f2289,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| X1 = X2
| ~ member(X1,sK42_skl)
| ~ member(X2,sK42_skl)
| ~ apply(sK39_skl,X0,X2)
| ~ member(X0,sK41_skl)
| ~ apply(sK40_skl,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2288,f1474]) ).
fof(f2336,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| equal_maps(sK39_skl,X2,X1,X0)
| ~ member(sK13_skl(X0,X1,X2,sK39_skl),sK42_skl)
| sK13_skl(X0,X1,X2,sK39_skl) = X3
| ~ apply(sK40_skl,sK12_skl(X0,X1,X2,sK39_skl),X3)
| ~ member(X3,sK42_skl)
| ~ member(sK12_skl(X0,X1,X2,sK39_skl),sK41_skl) ),
inference(resolution,[status(thm)],[f2289,f127]) ).
fof(f9861,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| equal_maps(sK39_skl,X1,X0,sK42_skl)
| equal_maps(sK39_skl,X1,X0,sK42_skl)
| sK13_skl(sK42_skl,X0,X1,sK39_skl) = X2
| ~ apply(sK40_skl,sK12_skl(sK42_skl,X0,X1,sK39_skl),X2)
| ~ member(X2,sK42_skl)
| ~ member(sK12_skl(sK42_skl,X0,X1,sK39_skl),sK41_skl) ),
inference(resolution,[status(thm)],[f2336,f125]) ).
fof(f9862,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| equal_maps(sK39_skl,X1,X0,sK42_skl)
| ~ member(sK12_skl(sK42_skl,X0,X1,sK39_skl),sK41_skl)
| X2 = sK13_skl(sK42_skl,X0,X1,sK39_skl)
| ~ member(X2,sK42_skl)
| ~ apply(sK40_skl,sK12_skl(sK42_skl,X0,X1,sK39_skl),X2) ),
inference(duplicate_literals_removal,[status(thm)],[f9861]) ).
fof(f10145,plain,
! [X0,X1] :
( ~ sQ4_spl
| equal_maps(sK39_skl,X0,sK41_skl,sK42_skl)
| equal_maps(sK39_skl,X0,sK41_skl,sK42_skl)
| X1 = sK13_skl(sK42_skl,sK41_skl,X0,sK39_skl)
| ~ member(X1,sK42_skl)
| ~ apply(sK40_skl,sK12_skl(sK42_skl,sK41_skl,X0,sK39_skl),X1) ),
inference(resolution,[status(thm)],[f9862,f124]) ).
fof(f10146,plain,
! [X0,X1] :
( ~ sQ4_spl
| equal_maps(sK39_skl,X1,sK41_skl,sK42_skl)
| X0 = sK13_skl(sK42_skl,sK41_skl,X1,sK39_skl)
| ~ apply(sK40_skl,sK12_skl(sK42_skl,sK41_skl,X1,sK39_skl),X0)
| ~ member(X0,sK42_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f10145]) ).
fof(f10147,plain,
( ~ sQ4_spl
| equal_maps(sK39_skl,sK40_skl,sK41_skl,sK42_skl)
| equal_maps(sK39_skl,sK40_skl,sK41_skl,sK42_skl)
| sK14_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl) = sK13_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl)
| ~ member(sK14_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl),sK42_skl) ),
inference(resolution,[status(thm)],[f10146,f128]) ).
fof(f10148,definition,
( sQ56_spl
<=> member(sK14_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl),sK42_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f10150,plain,
( sQ56_spl
| ~ member(sK14_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl),sK42_skl) ),
inference(component_clause,[status(thm)],[f10148]) ).
fof(f10151,definition,
( sQ57_spl
<=> sK14_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl) = sK13_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f10152,plain,
( ~ sQ57_spl
| sK14_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl) = sK13_skl(sK42_skl,sK41_skl,sK40_skl,sK39_skl) ),
inference(component_clause,[status(thm)],[f10151]) ).
fof(f10154,definition,
( sQ58_spl
<=> equal_maps(sK39_skl,sK40_skl,sK41_skl,sK42_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f10155,plain,
( ~ sQ58_spl
| equal_maps(sK39_skl,sK40_skl,sK41_skl,sK42_skl) ),
inference(component_clause,[status(thm)],[f10154]) ).
fof(f10157,plain,
( ~ sQ4_spl
| sQ58_spl
| sQ57_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f10147,f10148,f10151,f10154,f2282]) ).
fof(f10158,plain,
( ~ sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10155,f252]) ).
fof(f10159,plain,
~ sQ58_spl,
inference(contradiction_clause,[status(thm)],[f10158]) ).
fof(f10625,plain,
( sQ56_spl
| equal_maps(sK39_skl,sK40_skl,sK41_skl,sK42_skl) ),
inference(resolution,[status(thm)],[f10150,f126]) ).
fof(f10626,plain,
( sQ56_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f10625,f10154,f10148]) ).
fof(f10627,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10152,f1472]) ).
fof(f10628,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f10627]) ).
fof(f10629,plain,
$false,
inference(sat_refutation,[status(thm)],[f2075,f2285,f2287,f10157,f10159,f10626,f10628]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET724+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n009.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 05:33:57 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 77.97/10.31 % Refutation found
% 77.97/10.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 77.97/10.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 63.16/10.37 % Elapsed time: 10.008841 seconds
% 63.16/10.37 % CPU time: 78.573201 seconds
% 63.16/10.37 % Total memory used: 337.446 MB
% 63.16/10.37 % Net memory used: 296.122 MB
%------------------------------------------------------------------------------