%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET711+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 : 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 02:10:30 PM UTC 2026
% Result : Theorem 282.92s 36.41s
% Output : CNFRefutation 230.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 9
% Syntax : Number of formulae : 84 ( 7 unt; 4 def)
% Number of atoms : 395 ( 31 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 488 ( 177 ~; 210 |; 81 &)
% ( 13 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 5 prp; 0-4 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-4 aty)
% Number of variables : 283 ( 257 !; 26 ?)
% Comments :
%------------------------------------------------------------------------------
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(f17,axiom,
! [F,A,B] :
( injective(F,A,B)
<=> ! [X1,X2,Y] :
( ( member(Y,B)
& member(X2,A)
& member(X1,A) )
=> ( ( apply(F,X2,Y)
& apply(F,X1,Y) )
=> X1 = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [F,A,B] :
( one_to_one(F,A,B)
<=> ( surjective(F,A,B)
& injective(F,A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [G,F,A,B] :
( inverse_predicate(G,F,A,B)
<=> ! [X,Y] :
( ( member(Y,B)
& member(X,A) )
=> ( apply(F,X,Y)
<=> apply(G,Y,X) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,conjecture,
! [F,G,H,A,B] :
( ( inverse_predicate(H,F,A,B)
& inverse_predicate(G,F,A,B)
& one_to_one(F,A,B)
& maps(F,A,B) )
=> equal_maps(G,H,B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
~ ! [F,G,H,A,B] :
( ( inverse_predicate(H,F,A,B)
& inverse_predicate(G,F,A,B)
& one_to_one(F,A,B)
& maps(F,A,B) )
=> equal_maps(G,H,B,A) ),
inference(negated_conjecture,[status(cth)],[f29]) ).
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] :
( ~ member(X1,X4)
| X2 = X6
| ~ member(X6,X5)
| ~ apply(X3,X1,X6)
| ~ member(X2,X5)
| ~ equal_maps(X0,X3,X4,X5)
| ~ apply(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f124,plain,
! [X0,X1,X2,X3] :
( member(sK12_skl(X3,X2,X1,X0),X2)
| equal_maps(X0,X1,X2,X3) ),
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] :
( apply(X1,sK12_skl(X3,X2,X1,X0),sK14_skl(X3,X2,X1,X0))
| equal_maps(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f129,plain,
! [X0,X1,X2,X3] :
( equal_maps(X3,X2,X1,X0)
| sK14_skl(X0,X1,X2,X3) != sK13_skl(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f137,plain,
! [F,A,B] :
( injective(F,A,B)
<=> ! [X1,X2,Y] :
( X1 = X2
| ~ apply(F,X2,Y)
| ~ apply(F,X1,Y)
| ~ member(Y,B)
| ~ member(X2,A)
| ~ member(X1,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f138,plain,
! [F,A,B] :
( ( ? [X1,X2,Y] :
( X1 != X2
& apply(F,X2,Y)
& apply(F,X1,Y)
& member(Y,B)
& member(X2,A)
& member(X1,A) )
| injective(F,A,B) )
& ( ! [X1,X2,Y] :
( X1 = X2
| ~ apply(F,X2,Y)
| ~ apply(F,X1,Y)
| ~ member(Y,B)
| ~ member(X2,A)
| ~ member(X1,A) )
| ~ injective(F,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
( ! [F,A,B] :
( ? [X1,X2,Y] :
( X1 != X2
& apply(F,X2,Y)
& apply(F,X1,Y)
& member(Y,B)
& member(X2,A)
& member(X1,A) )
| injective(F,A,B) )
& ! [F,A,B] :
( ! [X1,X2,Y] :
( X1 = X2
| ~ apply(F,X2,Y)
| ~ apply(F,X1,Y)
| ~ member(Y,B)
| ~ member(X2,A)
| ~ member(X1,A) )
| ~ injective(F,A,B) ) ),
inference(miniscoping,[status(thm)],[f138]) ).
fof(f140,plain,
( ! [F,A,B] :
( ( sK16_skl(B,A,F) != sK17_skl(B,A,F)
& apply(F,sK17_skl(B,A,F),sK18_skl(B,A,F))
& apply(F,sK16_skl(B,A,F),sK18_skl(B,A,F))
& member(sK18_skl(B,A,F),B)
& member(sK17_skl(B,A,F),A)
& member(sK16_skl(B,A,F),A) )
| injective(F,A,B) )
& ! [F,A,B] :
( ! [X1,X2,Y] :
( X1 = X2
| ~ apply(F,X2,Y)
| ~ apply(F,X1,Y)
| ~ member(Y,B)
| ~ member(X2,A)
| ~ member(X1,A) )
| ~ injective(F,A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(X1,sK16_skl(B,A,F)),skolemize(X2,sK17_skl(B,A,F)),skolemize(Y,sK18_skl(B,A,F))],[f139]) ).
fof(f141,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ apply(X3,X1,X5)
| ~ member(X0,X2)
| ~ member(X5,X4)
| ~ apply(X3,X0,X5)
| ~ injective(X3,X2,X4)
| ~ member(X1,X2)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f156,plain,
! [F,A,B] :
( ( ~ surjective(F,A,B)
| ~ injective(F,A,B)
| one_to_one(F,A,B) )
& ( ( surjective(F,A,B)
& injective(F,A,B) )
| ~ one_to_one(F,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f157,plain,
( ! [F,A,B] :
( ~ surjective(F,A,B)
| ~ injective(F,A,B)
| one_to_one(F,A,B) )
& ! [F,A,B] :
( ( surjective(F,A,B)
& injective(F,A,B) )
| ~ one_to_one(F,A,B) ) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f158,plain,
! [X0,X1,X2] :
( ~ one_to_one(X0,X1,X2)
| injective(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f161,plain,
! [G,F,A,B] :
( inverse_predicate(G,F,A,B)
<=> ! [X,Y] :
( ( apply(F,X,Y)
<=> apply(G,Y,X) )
| ~ member(Y,B)
| ~ member(X,A) ) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f162,plain,
! [G,F,A,B] :
( ( ? [X,Y] :
( ( apply(G,Y,X)
| apply(F,X,Y) )
& ( ~ apply(G,Y,X)
| ~ apply(F,X,Y) )
& member(Y,B)
& member(X,A) )
| inverse_predicate(G,F,A,B) )
& ( ! [X,Y] :
( ( ( ~ apply(G,Y,X)
| apply(F,X,Y) )
& ( apply(G,Y,X)
| ~ apply(F,X,Y) ) )
| ~ member(Y,B)
| ~ member(X,A) )
| ~ inverse_predicate(G,F,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f161]) ).
fof(f163,plain,
( ! [G,F,A,B] :
( ? [X,Y] :
( ( apply(G,Y,X)
| apply(F,X,Y) )
& ( ~ apply(G,Y,X)
| ~ apply(F,X,Y) )
& member(Y,B)
& member(X,A) )
| inverse_predicate(G,F,A,B) )
& ! [G,F,A,B] :
( ! [X,Y] :
( ( ( ~ apply(G,Y,X)
| apply(F,X,Y) )
& ( apply(G,Y,X)
| ~ apply(F,X,Y) ) )
| ~ member(Y,B)
| ~ member(X,A) )
| ~ inverse_predicate(G,F,A,B) ) ),
inference(miniscoping,[status(thm)],[f162]) ).
fof(f164,plain,
( ! [G,F,A,B] :
( ( ( apply(G,sK22_skl(B,A,F,G),sK21_skl(B,A,F,G))
| apply(F,sK21_skl(B,A,F,G),sK22_skl(B,A,F,G)) )
& ( ~ apply(G,sK22_skl(B,A,F,G),sK21_skl(B,A,F,G))
| ~ apply(F,sK21_skl(B,A,F,G),sK22_skl(B,A,F,G)) )
& member(sK22_skl(B,A,F,G),B)
& member(sK21_skl(B,A,F,G),A) )
| inverse_predicate(G,F,A,B) )
& ! [G,F,A,B] :
( ! [X,Y] :
( ( ( ~ apply(G,Y,X)
| apply(F,X,Y) )
& ( apply(G,Y,X)
| ~ apply(F,X,Y) ) )
| ~ member(Y,B)
| ~ member(X,A) )
| ~ inverse_predicate(G,F,A,B) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(X,sK21_skl(B,A,F,G)),skolemize(Y,sK22_skl(B,A,F,G))],[f163]) ).
fof(f166,plain,
! [X0,X1,X2,X3,X4,X5] :
( apply(X4,X2,X1)
| ~ member(X2,X5)
| ~ inverse_predicate(X0,X4,X5,X3)
| ~ member(X1,X3)
| ~ apply(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f244,plain,
? [F,G,H,A,B] :
( ~ equal_maps(G,H,B,A)
& inverse_predicate(H,F,A,B)
& inverse_predicate(G,F,A,B)
& one_to_one(F,A,B)
& maps(F,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f245,plain,
? [G,H,A,B] :
( ~ equal_maps(G,H,B,A)
& ? [F] :
( inverse_predicate(H,F,A,B)
& inverse_predicate(G,F,A,B)
& one_to_one(F,A,B)
& maps(F,A,B) ) ),
inference(miniscoping,[status(thm)],[f244]) ).
fof(f246,plain,
( ~ equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl)
& inverse_predicate(sK40_skl,sK43_skl,sK41_skl,sK42_skl)
& inverse_predicate(sK39_skl,sK43_skl,sK41_skl,sK42_skl)
& one_to_one(sK43_skl,sK41_skl,sK42_skl)
& maps(sK43_skl,sK41_skl,sK42_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39_skl,sK40_skl,sK41_skl,sK42_skl,sK43_skl]),skolemize(G,sK39_skl),skolemize(H,sK40_skl),skolemize(A,sK41_skl),skolemize(B,sK42_skl),skolemize(F,sK43_skl)],[f245]) ).
fof(f248,plain,
one_to_one(sK43_skl,sK41_skl,sK42_skl),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f249,plain,
inverse_predicate(sK39_skl,sK43_skl,sK41_skl,sK42_skl),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f250,plain,
inverse_predicate(sK40_skl,sK43_skl,sK41_skl,sK42_skl),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f251,plain,
~ equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl),
inference(cnf_transformation,[status(thm)],[f246]) ).
fof(f271,plain,
injective(sK43_skl,sK41_skl,sK42_skl),
inference(resolution,[status(thm)],[f158,f248]) ).
fof(f386,plain,
! [X0,X1,X2] :
( X2 = X0
| ~ apply(sK43_skl,X2,X1)
| ~ member(X0,sK41_skl)
| ~ member(X1,sK42_skl)
| ~ member(X2,sK41_skl)
| ~ apply(sK43_skl,X0,X1) ),
inference(resolution,[status(thm)],[f141,f271]) ).
fof(f756,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ member(sK12_skl(X3,X2,X1,X0),X5)
| ~ apply(X4,sK12_skl(X3,X2,X1,X0),X7)
| ~ member(sK13_skl(X3,X2,X1,X0),X6)
| ~ member(X7,X6)
| X7 = sK13_skl(X3,X2,X1,X0)
| ~ equal_maps(X4,X0,X5,X6)
| equal_maps(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f127,f123]) ).
fof(f758,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ member(sK13_skl(X0,X1,X2,X3),X6)
| equal_maps(X3,X2,X1,X0)
| ~ inverse_predicate(X3,X5,X6,X4)
| apply(X5,sK13_skl(X0,X1,X2,X3),sK12_skl(X0,X1,X2,X3))
| ~ member(sK12_skl(X0,X1,X2,X3),X4) ),
inference(resolution,[status(thm)],[f127,f166]) ).
fof(f763,plain,
! [X0,X1,X2] :
( apply(sK43_skl,sK13_skl(X0,X1,X2,sK40_skl),sK12_skl(X0,X1,X2,sK40_skl))
| ~ member(sK13_skl(X0,X1,X2,sK40_skl),sK41_skl)
| equal_maps(sK40_skl,X2,X1,X0)
| ~ member(sK12_skl(X0,X1,X2,sK40_skl),sK42_skl) ),
inference(resolution,[status(thm)],[f758,f250]) ).
fof(f808,plain,
! [X0,X1] :
( equal_maps(sK40_skl,X1,X0,sK41_skl)
| apply(sK43_skl,sK13_skl(sK41_skl,X0,X1,sK40_skl),sK12_skl(sK41_skl,X0,X1,sK40_skl))
| equal_maps(sK40_skl,X1,X0,sK41_skl)
| ~ member(sK12_skl(sK41_skl,X0,X1,sK40_skl),sK42_skl) ),
inference(resolution,[status(thm)],[f763,f125]) ).
fof(f809,plain,
! [X0,X1] :
( equal_maps(sK40_skl,X1,X0,sK41_skl)
| ~ member(sK12_skl(sK41_skl,X0,X1,sK40_skl),sK42_skl)
| apply(sK43_skl,sK13_skl(sK41_skl,X0,X1,sK40_skl),sK12_skl(sK41_skl,X0,X1,sK40_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f808]) ).
fof(f844,plain,
! [X0] :
( equal_maps(sK40_skl,X0,sK42_skl,sK41_skl)
| equal_maps(sK40_skl,X0,sK42_skl,sK41_skl)
| apply(sK43_skl,sK13_skl(sK41_skl,sK42_skl,X0,sK40_skl),sK12_skl(sK41_skl,sK42_skl,X0,sK40_skl)) ),
inference(resolution,[status(thm)],[f809,f124]) ).
fof(f845,plain,
! [X0] :
( apply(sK43_skl,sK13_skl(sK41_skl,sK42_skl,X0,sK40_skl),sK12_skl(sK41_skl,sK42_skl,X0,sK40_skl))
| equal_maps(sK40_skl,X0,sK42_skl,sK41_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f844]) ).
fof(f878,plain,
! [X0,X1] :
( sK13_skl(sK41_skl,sK42_skl,X0,sK40_skl) = X1
| ~ member(X1,sK41_skl)
| ~ member(sK12_skl(sK41_skl,sK42_skl,X0,sK40_skl),sK42_skl)
| ~ member(sK13_skl(sK41_skl,sK42_skl,X0,sK40_skl),sK41_skl)
| ~ apply(sK43_skl,X1,sK12_skl(sK41_skl,sK42_skl,X0,sK40_skl))
| equal_maps(sK40_skl,X0,sK42_skl,sK41_skl) ),
inference(resolution,[status(thm)],[f845,f386]) ).
fof(f884,plain,
! [X0,X1] :
( X1 = sK13_skl(sK41_skl,sK42_skl,X0,sK40_skl)
| ~ apply(sK43_skl,X1,sK12_skl(sK41_skl,sK42_skl,X0,sK40_skl))
| ~ member(X1,sK41_skl)
| equal_maps(sK40_skl,X0,sK42_skl,sK41_skl)
| ~ member(sK12_skl(sK41_skl,sK42_skl,X0,sK40_skl),sK42_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f878,f125]) ).
fof(f1078,plain,
! [X0,X1] :
( sK13_skl(sK41_skl,sK42_skl,X1,sK40_skl) = X0
| equal_maps(sK40_skl,X1,sK42_skl,sK41_skl)
| ~ member(X0,sK41_skl)
| ~ apply(sK43_skl,X0,sK12_skl(sK41_skl,sK42_skl,X1,sK40_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f884,f124]) ).
fof(f1428,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ member(sK12_skl(X3,X2,X1,X0),X4)
| ~ member(sK13_skl(X3,X2,X1,X0),X5)
| ~ member(sK14_skl(X3,X2,X1,X0),X5)
| sK14_skl(X3,X2,X1,X0) = sK13_skl(X3,X2,X1,X0)
| ~ equal_maps(X1,X0,X4,X5)
| equal_maps(X0,X1,X2,X3)
| equal_maps(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f128,f756]) ).
fof(f1432,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ member(sK12_skl(X4,X5,X0,X6),X3)
| apply(X1,sK14_skl(X4,X5,X0,X6),sK12_skl(X4,X5,X0,X6))
| equal_maps(X6,X0,X5,X4)
| ~ member(sK14_skl(X4,X5,X0,X6),X2)
| ~ inverse_predicate(X0,X1,X2,X3) ),
inference(resolution,[status(thm)],[f128,f166]) ).
fof(f1435,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ member(sK13_skl(X0,X1,X2,X3),X4)
| ~ member(sK12_skl(X0,X1,X2,X3),X5)
| equal_maps(X3,X2,X1,X0)
| ~ equal_maps(X2,X3,X5,X4)
| ~ member(sK14_skl(X0,X1,X2,X3),X4)
| sK14_skl(X0,X1,X2,X3) = sK13_skl(X0,X1,X2,X3) ),
inference(duplicate_literals_removal,[status(thm)],[f1428]) ).
fof(f2236,plain,
! [X0,X1,X2] :
( equal_maps(X2,sK39_skl,X1,X0)
| apply(sK43_skl,sK14_skl(X0,X1,sK39_skl,X2),sK12_skl(X0,X1,sK39_skl,X2))
| ~ member(sK14_skl(X0,X1,sK39_skl,X2),sK41_skl)
| ~ member(sK12_skl(X0,X1,sK39_skl,X2),sK42_skl) ),
inference(resolution,[status(thm)],[f1432,f249]) ).
fof(f3207,plain,
! [X0,X1] :
( equal_maps(X1,sK39_skl,X0,sK41_skl)
| equal_maps(X1,sK39_skl,X0,sK41_skl)
| apply(sK43_skl,sK14_skl(sK41_skl,X0,sK39_skl,X1),sK12_skl(sK41_skl,X0,sK39_skl,X1))
| ~ member(sK12_skl(sK41_skl,X0,sK39_skl,X1),sK42_skl) ),
inference(resolution,[status(thm)],[f2236,f126]) ).
fof(f3208,plain,
! [X0,X1] :
( apply(sK43_skl,sK14_skl(sK41_skl,X1,sK39_skl,X0),sK12_skl(sK41_skl,X1,sK39_skl,X0))
| ~ member(sK12_skl(sK41_skl,X1,sK39_skl,X0),sK42_skl)
| equal_maps(X0,sK39_skl,X1,sK41_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f3207]) ).
fof(f3209,plain,
! [X0] :
( equal_maps(X0,sK39_skl,sK42_skl,sK41_skl)
| apply(sK43_skl,sK14_skl(sK41_skl,sK42_skl,sK39_skl,X0),sK12_skl(sK41_skl,sK42_skl,sK39_skl,X0))
| equal_maps(X0,sK39_skl,sK42_skl,sK41_skl) ),
inference(resolution,[status(thm)],[f3208,f124]) ).
fof(f3210,plain,
! [X0] :
( apply(sK43_skl,sK14_skl(sK41_skl,sK42_skl,sK39_skl,X0),sK12_skl(sK41_skl,sK42_skl,sK39_skl,X0))
| equal_maps(X0,sK39_skl,sK42_skl,sK41_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f3209]) ).
fof(f3211,plain,
( sK13_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) = sK14_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl)
| equal_maps(sK40_skl,sK39_skl,sK42_skl,sK41_skl)
| ~ member(sK14_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl),sK41_skl)
| equal_maps(sK40_skl,sK39_skl,sK42_skl,sK41_skl) ),
inference(resolution,[status(thm)],[f3210,f1078]) ).
fof(f3231,definition,
( sQ50_spl
<=> equal_maps(sK40_skl,sK39_skl,sK42_skl,sK41_skl) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f3232,plain,
( ~ sQ50_spl
| equal_maps(sK40_skl,sK39_skl,sK42_skl,sK41_skl) ),
inference(component_clause,[status(thm)],[f3231]) ).
fof(f3233,plain,
( sQ50_spl
| ~ equal_maps(sK40_skl,sK39_skl,sK42_skl,sK41_skl) ),
inference(component_clause,[status(thm)],[f3231]) ).
fof(f3234,definition,
( sQ51_spl
<=> member(sK14_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl),sK41_skl) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f3236,plain,
( sQ51_spl
| ~ member(sK14_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl),sK41_skl) ),
inference(component_clause,[status(thm)],[f3234]) ).
fof(f3237,definition,
( sQ52_spl
<=> sK13_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) = sK14_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f3238,plain,
( ~ sQ52_spl
| sK13_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) = sK14_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) ),
inference(component_clause,[status(thm)],[f3237]) ).
fof(f3240,plain,
( sQ52_spl
| ~ sQ51_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f3211,f3231,f3234,f3237]) ).
fof(f3253,plain,
( sQ51_spl
| equal_maps(sK40_skl,sK39_skl,sK42_skl,sK41_skl) ),
inference(resolution,[status(thm)],[f3236,f126]) ).
fof(f5382,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ member(sK14_skl(X4,X5,X0,X1),X3)
| ~ member(sK13_skl(X4,X5,X0,X1),X3)
| equal_maps(X1,X0,X5,X4)
| ~ member(sK12_skl(X4,X5,X0,X1),X2)
| ~ equal_maps(X0,X1,X2,X3) ),
inference(forward_subsumption_resolution,[status(thm)],[f1435,f129]) ).
fof(f5384,plain,
! [X0,X1] :
( ~ sQ50_spl
| ~ member(sK14_skl(X0,X1,sK40_skl,sK39_skl),sK41_skl)
| equal_maps(sK39_skl,sK40_skl,X1,X0)
| ~ member(sK13_skl(X0,X1,sK40_skl,sK39_skl),sK41_skl)
| ~ member(sK12_skl(X0,X1,sK40_skl,sK39_skl),sK42_skl) ),
inference(resolution,[status(thm)],[f5382,f3232]) ).
fof(f5465,plain,
! [X0] :
( ~ sQ50_spl
| equal_maps(sK39_skl,sK40_skl,X0,sK41_skl)
| equal_maps(sK39_skl,sK40_skl,X0,sK41_skl)
| ~ member(sK13_skl(sK41_skl,X0,sK40_skl,sK39_skl),sK41_skl)
| ~ member(sK12_skl(sK41_skl,X0,sK40_skl,sK39_skl),sK42_skl) ),
inference(resolution,[status(thm)],[f5384,f126]) ).
fof(f5466,plain,
! [X0] :
( ~ sQ50_spl
| equal_maps(sK39_skl,sK40_skl,X0,sK41_skl)
| ~ member(sK13_skl(sK41_skl,X0,sK40_skl,sK39_skl),sK41_skl)
| ~ member(sK12_skl(sK41_skl,X0,sK40_skl,sK39_skl),sK42_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f5465]) ).
fof(f5467,plain,
! [X0] :
( ~ sQ50_spl
| equal_maps(sK39_skl,sK40_skl,X0,sK41_skl)
| ~ member(sK12_skl(sK41_skl,X0,sK40_skl,sK39_skl),sK42_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5466,f125]) ).
fof(f5511,plain,
( ~ sQ50_spl
| equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl)
| equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl) ),
inference(resolution,[status(thm)],[f5467,f124]) ).
fof(f5512,definition,
( sQ193_spl
<=> equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl) ),
introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition]) ).
fof(f5513,plain,
( ~ sQ193_spl
| equal_maps(sK39_skl,sK40_skl,sK42_skl,sK41_skl) ),
inference(component_clause,[status(thm)],[f5512]) ).
fof(f5515,plain,
( ~ sQ50_spl
| sQ193_spl ),
inference(split_clause,[status(thm)],[f5511,f5512,f3231]) ).
fof(f5516,plain,
( sQ51_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f3253,f3231,f3234]) ).
fof(f5519,plain,
( ~ sQ193_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5513,f251]) ).
fof(f5520,plain,
~ sQ193_spl,
inference(contradiction_clause,[status(thm)],[f5519]) ).
fof(f5532,plain,
( sQ50_spl
| sK14_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) != sK13_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) ),
inference(resolution,[status(thm)],[f3233,f129]) ).
fof(f5881,plain,
( sQ50_spl
| ~ sQ52_spl
| sK13_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) != sK13_skl(sK41_skl,sK42_skl,sK39_skl,sK40_skl) ),
inference(forward_demodulation,[status(thm)],[f3238,f5532]) ).
fof(f5882,plain,
( sQ50_spl
| ~ sQ52_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f5881]) ).
fof(f5883,plain,
( sQ50_spl
| ~ sQ52_spl ),
inference(contradiction_clause,[status(thm)],[f5882]) ).
fof(f5884,plain,
$false,
inference(sat_refutation,[status(thm)],[f3240,f5515,f5516,f5520,f5883]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET711+4 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.53 % Computer : n015.cluster.edu
% 0.11/0.53 % Model : x86_64 x86_64
% 0.11/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.53 % Memory : 8046.5625MB
% 0.11/0.53 % OS : Linux 6.8.0-71-generic
% 0.11/0.53 % CPULimit : 300
% 0.11/0.53 % WCLimit : 300
% 0.11/0.53 % DateTime : Mon Sep 21 05:36:21 UTC 2026
% 0.11/0.54 % CPUTime :
% 0.11/0.55 % Drodi V4.1.1
% 282.92/36.41 % Refutation found
% 282.92/36.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 282.92/36.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 240.92/37.62 % Elapsed time: 36.864308 seconds
% 240.92/37.62 % CPU time: 275.152168 seconds
% 240.92/37.62 % Total memory used: 591.218 MB
% 240.92/37.62 % Net memory used: 511.150 MB
%------------------------------------------------------------------------------