%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : NUN066+2 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 01:57:11 PM UTC 2026
% Result : Theorem 1.10s 0.66s
% Output : CNFRefutation 1.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 41
% Syntax : Number of formulae : 268 ( 24 unt; 32 def)
% Number of atoms : 723 ( 201 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 743 ( 288 ~; 351 |; 72 &)
% ( 32 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 28 prp; 0-4 aty)
% Number of functors : 16 ( 16 usr; 1 con; 0-2 aty)
% Number of variables : 307 ( 272 !; 35 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
? [Y24] :
! [X19] :
( ( X19 = Y24
& r1(X19) )
| ( X19 != Y24
& ~ r1(X19) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X11] :
? [Y21] :
! [X12] :
( ( X12 = Y21
& r2(X11,X12) )
| ( X12 != Y21
& ~ r2(X11,X12) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X13,X14] :
? [Y22] :
! [X15] :
( ( X15 = Y22
& r3(X13,X14,X15) )
| ( X15 != Y22
& ~ r3(X13,X14,X15) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X1,X8] :
? [Y4] :
( ? [Y7] :
( r3(X1,X8,Y7)
& r2(Y7,Y4) )
& ? [Y5] :
( Y5 = Y4
& ? [Y15] :
( r3(X1,Y15,Y5)
& r2(X8,Y15) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X3,X10] :
( X3 = X10
| ! [Y12] :
( ~ r2(X10,Y12)
| ! [Y13] :
( Y13 != Y12
| ~ r2(X3,Y13) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X4] :
? [Y9] :
( Y9 = X4
& ? [Y16] :
( r3(X4,Y16,Y9)
& r1(Y16) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X6] :
( ? [Y1,Y11] :
( X6 = Y11
& r2(Y1,Y11) )
| ? [Y19] :
( X6 = Y19
& r1(Y19) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X7,Y10] :
( ~ r2(X7,Y10)
| ! [Y20] :
( Y20 != Y10
| ~ r1(Y20) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,conjecture,
? [Y1] :
( ! [Y5] :
( Y1 != Y5
| ~ r1(Y5) )
& ! [Y2] :
( Y1 != Y2
| ! [Y3] :
( ~ r2(Y3,Y2)
| ! [Y4] :
( ~ r2(Y4,Y3)
| ~ r1(Y4) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
~ ? [Y1] :
( ! [Y5] :
( Y1 != Y5
| ~ r1(Y5) )
& ! [Y2] :
( Y1 != Y2
| ! [Y3] :
( ~ r2(Y3,Y2)
| ! [Y4] :
( ~ r2(Y4,Y3)
| ~ r1(Y4) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f12]) ).
fof(f14,definition,
! [Y24,X19] :
( sP0_prd(X19,Y24)
<=> ( X19 != Y24
& ~ r1(X19) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f15,plain,
? [Y24] :
! [X19] :
( ( X19 = Y24
& r1(X19) )
| sP0_prd(X19,Y24) ),
inference(formula_renaming,[status(thm)],[f1,f14]) ).
fof(f16,plain,
! [X19] :
( ( X19 = sK0_skl
& r1(X19) )
| sP0_prd(X19,sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(Y24,sK0_skl)],[f15]) ).
fof(f17,plain,
! [X0] :
( r1(X0)
| sP0_prd(X0,sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f18,plain,
! [X0] :
( X0 = sK0_skl
| sP0_prd(X0,sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f19,definition,
! [X11,Y21,X12] :
( sP1_prd(X12,Y21,X11)
<=> ( X12 != Y21
& ~ r2(X11,X12) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f20,plain,
! [X11] :
? [Y21] :
! [X12] :
( ( X12 = Y21
& r2(X11,X12) )
| sP1_prd(X12,Y21,X11) ),
inference(formula_renaming,[status(thm)],[f2,f19]) ).
fof(f21,plain,
! [X11,X12] :
( ( X12 = sK1_skl(X11)
& r2(X11,X12) )
| sP1_prd(X12,sK1_skl(X11),X11) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(Y21,sK1_skl(X11))],[f20]) ).
fof(f22,plain,
! [X0,X1] :
( r2(X1,X0)
| sP1_prd(X0,sK1_skl(X1),X1) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f23,plain,
! [X0,X1] :
( X0 = sK1_skl(X1)
| sP1_prd(X0,sK1_skl(X1),X1) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f24,definition,
! [X13,X14,Y22,X15] :
( sP2_prd(X15,Y22,X14,X13)
<=> ( X15 != Y22
& ~ r3(X13,X14,X15) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f25,plain,
! [X13,X14] :
? [Y22] :
! [X15] :
( ( X15 = Y22
& r3(X13,X14,X15) )
| sP2_prd(X15,Y22,X14,X13) ),
inference(formula_renaming,[status(thm)],[f3,f24]) ).
fof(f26,plain,
! [X13,X14,X15] :
( ( X15 = sK2_skl(X14,X13)
& r3(X13,X14,X15) )
| sP2_prd(X15,sK2_skl(X14,X13),X14,X13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y22,sK2_skl(X14,X13))],[f25]) ).
fof(f28,plain,
! [X0,X1,X2] :
( X0 = sK2_skl(X1,X2)
| sP2_prd(X0,sK2_skl(X1,X2),X1,X2) ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f34,plain,
! [X1,X8] :
( r3(X1,X8,sK7_skl(X8,X1))
& r2(sK7_skl(X8,X1),sK4_skl(X8,X1))
& sK5_skl(X8,X1) = sK4_skl(X8,X1)
& r3(X1,sK6_skl(X8,X1),sK5_skl(X8,X1))
& r2(X8,sK6_skl(X8,X1)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl]),skolemize(Y4,sK4_skl(X8,X1)),skolemize(Y5,sK5_skl(X8,X1)),skolemize(Y15,sK6_skl(X8,X1)),skolemize(Y7,sK7_skl(X8,X1))],[f5]) ).
fof(f38,plain,
! [X0,X1] : r2(sK7_skl(X0,X1),sK4_skl(X0,X1)),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f39,plain,
! [X0,X1] : r3(X0,X1,sK7_skl(X1,X0)),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f46,plain,
! [X0,X1,X2,X3] :
( X0 = X3
| ~ r2(X3,X2)
| X1 != X2
| ~ r2(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f47,plain,
! [X4] :
( sK12_skl(X4) = X4
& r3(X4,sK13_skl(X4),sK12_skl(X4))
& r1(sK13_skl(X4)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl,sK13_skl]),skolemize(Y9,sK12_skl(X4)),skolemize(Y16,sK13_skl(X4))],[f8]) ).
fof(f48,plain,
! [X0] : r1(sK13_skl(X0)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [X0] : r3(X0,sK13_skl(X0),sK12_skl(X0)),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f50,plain,
! [X0] : sK12_skl(X0) = X0,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f56,definition,
! [X6,Y19] :
( sP4_prd(Y19,X6)
<=> ( X6 = Y19
& r1(Y19) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f57,plain,
! [X6] :
( ? [Y1,Y11] :
( X6 = Y11
& r2(Y1,Y11) )
| ? [Y19] : sP4_prd(Y19,X6) ),
inference(formula_renaming,[status(thm)],[f10,f56]) ).
fof(f58,plain,
! [X6] :
( ? [Y11] :
( X6 = Y11
& ? [Y1] : r2(Y1,Y11) )
| ? [Y19] : sP4_prd(Y19,X6) ),
inference(miniscoping,[status(thm)],[f57]) ).
fof(f59,plain,
! [X6] :
( ( X6 = sK18_skl(X6)
& r2(sK19_skl(X6),sK18_skl(X6)) )
| sP4_prd(sK17_skl(X6),X6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl,sK19_skl]),skolemize(Y19,sK17_skl(X6)),skolemize(Y11,sK18_skl(X6)),skolemize(Y1,sK19_skl(X6))],[f58]) ).
fof(f60,plain,
! [X0] :
( r2(sK19_skl(X0),sK18_skl(X0))
| sP4_prd(sK17_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
! [X0] :
( X0 = sK18_skl(X0)
| sP4_prd(sK17_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f62,plain,
! [Y10] :
( ! [X7] : ~ r2(X7,Y10)
| ! [Y20] :
( Y20 != Y10
| ~ r1(Y20) ) ),
inference(miniscoping,[status(thm)],[f11]) ).
fof(f63,plain,
! [X0,X1,X2] :
( ~ r2(X2,X1)
| X0 != X1
| ~ r1(X0) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [Y1] :
( ? [Y5] :
( Y1 = Y5
& r1(Y5) )
| ? [Y2] :
( Y1 = Y2
& ? [Y3] :
( r2(Y3,Y2)
& ? [Y4] :
( r2(Y4,Y3)
& r1(Y4) ) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f65,definition,
! [Y1,Y2] :
( sP5_prd(Y2,Y1)
<=> ( Y1 = Y2
& ? [Y3] :
( r2(Y3,Y2)
& ? [Y4] :
( r2(Y4,Y3)
& r1(Y4) ) ) ) ),
introduced(definition,[new_symbols(definition,[sP5_prd])],[]) ).
fof(f66,plain,
! [Y1] :
( ? [Y5] :
( Y1 = Y5
& r1(Y5) )
| ? [Y2] : sP5_prd(Y2,Y1) ),
inference(formula_renaming,[status(thm)],[f64,f65]) ).
fof(f67,plain,
! [Y1] :
( ( Y1 = sK21_skl(Y1)
& r1(sK21_skl(Y1)) )
| sP5_prd(sK20_skl(Y1),Y1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl]),skolemize(Y2,sK20_skl(Y1)),skolemize(Y5,sK21_skl(Y1))],[f66]) ).
fof(f68,plain,
! [X0] :
( r1(sK21_skl(X0))
| sP5_prd(sK20_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f69,plain,
! [X0] :
( X0 = sK21_skl(X0)
| sP5_prd(sK20_skl(X0),X0) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f70,plain,
! [Y24,X19] :
( ( X19 = Y24
| r1(X19)
| sP0_prd(X19,Y24) )
& ( ( X19 != Y24
& ~ r1(X19) )
| ~ sP0_prd(X19,Y24) ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f71,plain,
( ! [Y24,X19] :
( X19 = Y24
| r1(X19)
| sP0_prd(X19,Y24) )
& ! [Y24,X19] :
( ( X19 != Y24
& ~ r1(X19) )
| ~ sP0_prd(X19,Y24) ) ),
inference(miniscoping,[status(thm)],[f70]) ).
fof(f72,plain,
! [X0,X1] :
( ~ r1(X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f73,plain,
! [X0,X1] :
( X0 != X1
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f75,plain,
! [X11,Y21,X12] :
( ( X12 = Y21
| r2(X11,X12)
| sP1_prd(X12,Y21,X11) )
& ( ( X12 != Y21
& ~ r2(X11,X12) )
| ~ sP1_prd(X12,Y21,X11) ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f76,plain,
( ! [X11,Y21,X12] :
( X12 = Y21
| r2(X11,X12)
| sP1_prd(X12,Y21,X11) )
& ! [X11,Y21,X12] :
( ( X12 != Y21
& ~ r2(X11,X12) )
| ~ sP1_prd(X12,Y21,X11) ) ),
inference(miniscoping,[status(thm)],[f75]) ).
fof(f77,plain,
! [X0,X1,X2] :
( ~ r2(X2,X0)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] :
( X0 != X1
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f80,plain,
! [X13,X14,Y22,X15] :
( ( X15 = Y22
| r3(X13,X14,X15)
| sP2_prd(X15,Y22,X14,X13) )
& ( ( X15 != Y22
& ~ r3(X13,X14,X15) )
| ~ sP2_prd(X15,Y22,X14,X13) ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f81,plain,
( ! [X13,X14,Y22,X15] :
( X15 = Y22
| r3(X13,X14,X15)
| sP2_prd(X15,Y22,X14,X13) )
& ! [X13,X14,Y22,X15] :
( ( X15 != Y22
& ~ r3(X13,X14,X15) )
| ~ sP2_prd(X15,Y22,X14,X13) ) ),
inference(miniscoping,[status(thm)],[f80]) ).
fof(f82,plain,
! [X0,X1,X2,X3] :
( ~ r3(X3,X2,X0)
| ~ sP2_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f90,plain,
! [X6,Y19] :
( ( X6 != Y19
| ~ r1(Y19)
| sP4_prd(Y19,X6) )
& ( ( X6 = Y19
& r1(Y19) )
| ~ sP4_prd(Y19,X6) ) ),
inference(NNF_transformation,[status(thm)],[f56]) ).
fof(f91,plain,
( ! [X6,Y19] :
( X6 != Y19
| ~ r1(Y19)
| sP4_prd(Y19,X6) )
& ! [X6,Y19] :
( ( X6 = Y19
& r1(Y19) )
| ~ sP4_prd(Y19,X6) ) ),
inference(miniscoping,[status(thm)],[f90]) ).
fof(f93,plain,
! [X0,X1] :
( X1 = X0
| ~ sP4_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f95,plain,
! [Y1,Y2] :
( ( Y1 != Y2
| ! [Y3] :
( ~ r2(Y3,Y2)
| ! [Y4] :
( ~ r2(Y4,Y3)
| ~ r1(Y4) ) )
| sP5_prd(Y2,Y1) )
& ( ( Y1 = Y2
& ? [Y3] :
( r2(Y3,Y2)
& ? [Y4] :
( r2(Y4,Y3)
& r1(Y4) ) ) )
| ~ sP5_prd(Y2,Y1) ) ),
inference(NNF_transformation,[status(thm)],[f65]) ).
fof(f96,plain,
( ! [Y1,Y2] :
( Y1 != Y2
| ! [Y3] :
( ~ r2(Y3,Y2)
| ! [Y4] :
( ~ r2(Y4,Y3)
| ~ r1(Y4) ) )
| sP5_prd(Y2,Y1) )
& ! [Y1,Y2] :
( ( Y1 = Y2
& ? [Y3] :
( r2(Y3,Y2)
& ? [Y4] :
( r2(Y4,Y3)
& r1(Y4) ) ) )
| ~ sP5_prd(Y2,Y1) ) ),
inference(miniscoping,[status(thm)],[f95]) ).
fof(f97,plain,
( ! [Y1,Y2] :
( Y1 != Y2
| ! [Y3] :
( ~ r2(Y3,Y2)
| ! [Y4] :
( ~ r2(Y4,Y3)
| ~ r1(Y4) ) )
| sP5_prd(Y2,Y1) )
& ! [Y1,Y2] :
( ( Y1 = Y2
& r2(sK22_skl(Y2,Y1),Y2)
& r2(sK23_skl(Y2,Y1),sK22_skl(Y2,Y1))
& r1(sK23_skl(Y2,Y1)) )
| ~ sP5_prd(Y2,Y1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl,sK23_skl]),skolemize(Y3,sK22_skl(Y2,Y1)),skolemize(Y4,sK23_skl(Y2,Y1))],[f96]) ).
fof(f98,plain,
! [X0,X1] :
( r1(sK23_skl(X0,X1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( r2(sK23_skl(X0,X1),sK22_skl(X0,X1))
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f100,plain,
! [X0,X1] :
( r2(sK22_skl(X0,X1),X0)
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f101,plain,
! [X0,X1] :
( X1 = X0
| ~ sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f102,plain,
! [X0,X1,X2,X3] :
( X1 != X0
| ~ r2(X3,X0)
| ~ r2(X2,X3)
| ~ r1(X2)
| sP5_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f105,plain,
! [X0,X1,X2] :
( X0 = X2
| ~ r2(X2,X1)
| ~ r2(X0,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f46]) ).
fof(f106,plain,
! [X0] : r3(X0,sK13_skl(X0),X0),
inference(backward_demodulation,[status(thm)],[f50,f49]) ).
fof(f108,plain,
! [X0,X1] :
( ~ r2(X1,X0)
| ~ r1(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f63]) ).
fof(f109,plain,
! [X0] : ~ sP0_prd(X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f73]) ).
fof(f110,plain,
! [X0,X1] : ~ sP1_prd(X0,X0,X1),
inference(destructive_equality_resolution,[status(thm)],[f78]) ).
fof(f114,plain,
! [X0,X1,X2] :
( ~ r2(X2,X0)
| ~ r2(X1,X2)
| ~ r1(X1)
| sP5_prd(X0,X0) ),
inference(destructive_equality_resolution,[status(thm)],[f102]) ).
fof(f115,plain,
! [X0] :
( X0 = sK20_skl(X0)
| X0 = sK21_skl(X0) ),
inference(resolution,[status(thm)],[f69,f101]) ).
fof(f116,plain,
! [X0] :
( X0 = sK20_skl(X0)
| r1(X0)
| sP5_prd(sK20_skl(X0),X0) ),
inference(paramodulation,[status(thm)],[f115,f68]) ).
fof(f117,plain,
! [X0] :
( X0 = sK20_skl(X0)
| r1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f116,f101]) ).
fof(f121,plain,
! [X0] :
( X0 = sK21_skl(X0)
| r2(sK22_skl(sK20_skl(X0),X0),sK20_skl(X0)) ),
inference(resolution,[status(thm)],[f100,f69]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ~ sP5_prd(X0,X1)
| ~ r2(X2,sK23_skl(X0,X1))
| ~ r1(X2)
| sP5_prd(sK22_skl(X0,X1),sK22_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f114,f99]) ).
fof(f126,plain,
! [X0] :
( ~ r1(sK20_skl(X0))
| X0 = sK21_skl(X0) ),
inference(resolution,[status(thm)],[f121,f108]) ).
fof(f143,plain,
r1(sK0_skl),
inference(resolution,[status(thm)],[f17,f109]) ).
fof(f144,plain,
! [X0] :
( ~ r1(X0)
| X0 = sK0_skl ),
inference(resolution,[status(thm)],[f18,f72]) ).
fof(f146,plain,
! [X0] : r2(X0,sK1_skl(X0)),
inference(resolution,[status(thm)],[f22,f110]) ).
fof(f297,plain,
! [X0] : sK13_skl(X0) = sK0_skl,
inference(resolution,[status(thm)],[f144,f48]) ).
fof(f298,plain,
! [X0] :
( sP5_prd(sK20_skl(X0),X0)
| sK21_skl(X0) = sK0_skl ),
inference(resolution,[status(thm)],[f144,f68]) ).
fof(f299,plain,
! [X0,X1] :
( ~ sP5_prd(X0,X1)
| sK23_skl(X0,X1) = sK0_skl ),
inference(resolution,[status(thm)],[f144,f98]) ).
fof(f300,plain,
! [X0] :
( X0 = sK20_skl(X0)
| X0 = sK0_skl ),
inference(resolution,[status(thm)],[f144,f117]) ).
fof(f306,plain,
! [X0] : r3(X0,sK0_skl,X0),
inference(backward_demodulation,[status(thm)],[f297,f106]) ).
fof(f309,plain,
! [X0,X1] :
( X0 = X1
| ~ r2(X0,sK1_skl(X1)) ),
inference(resolution,[status(thm)],[f146,f105]) ).
fof(f310,plain,
! [X0] : ~ r1(sK1_skl(X0)),
inference(resolution,[status(thm)],[f146,f108]) ).
fof(f311,plain,
! [X0] : sK1_skl(X0) = sK20_skl(sK1_skl(X0)),
inference(resolution,[status(thm)],[f310,f117]) ).
fof(f314,plain,
! [X0,X1] :
( X1 = sK20_skl(X1)
| X0 = sK20_skl(X0)
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f300,f300]) ).
fof(f315,plain,
! [X0,X1] :
( X1 = sK20_skl(X1)
| r3(X0,X1,X0) ),
inference(paramodulation,[status(thm)],[f300,f306]) ).
fof(f317,plain,
! [X0,X1] :
( X1 = sK20_skl(X1)
| X0 = sK0_skl
| sP0_prd(X0,X1) ),
inference(paramodulation,[status(thm)],[f300,f18]) ).
fof(f318,plain,
! [X0,X1] :
( X1 = sK20_skl(X1)
| r1(X0)
| sP0_prd(X0,X1) ),
inference(paramodulation,[status(thm)],[f300,f17]) ).
fof(f319,plain,
! [X0] :
( X0 = sK20_skl(X0)
| sK0_skl != sK20_skl(X0) ),
inference(equality_factoring,[status(thm)],[f300]) ).
fof(f366,plain,
! [X0] :
( sK20_skl(X0) = sK20_skl(sK20_skl(X0))
| X0 = sK20_skl(X0)
| sK0_skl != sK0_skl ),
inference(paramodulation,[status(thm)],[f300,f319]) ).
fof(f372,definition,
( sQ0_spl
<=> sK0_skl = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( sQ0_spl
| sK0_skl != sK0_skl ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f375,definition,
! [X0] :
( sQ1_spl
<=> ( sK20_skl(X0) = sK20_skl(sK20_skl(X0))
| X0 = sK20_skl(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f378,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f366,f372,f375]) ).
fof(f379,plain,
( sQ0_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f374]) ).
fof(f380,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f379]) ).
fof(f385,plain,
! [X0] :
( X0 = sK21_skl(X0)
| sK23_skl(sK20_skl(X0),X0) = sK0_skl ),
inference(resolution,[status(thm)],[f299,f69]) ).
fof(f386,plain,
! [X0] :
( sK0_skl = sK20_skl(sK0_skl)
| X0 = sK20_skl(X0)
| X0 = sK0_skl ),
inference(resolution,[status(thm)],[f314,f319]) ).
fof(f418,definition,
! [X0] :
( sQ2_spl
<=> ( X0 = sK20_skl(X0)
| X0 = sK0_skl ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f421,definition,
( sQ3_spl
<=> sK0_skl = sK20_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( ~ sQ3_spl
| sK0_skl = sK20_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f423,plain,
( sQ3_spl
| sK0_skl != sK20_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,plain,
( sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f386,f418,f421]) ).
fof(f430,plain,
! [X0] :
( X0 = sK20_skl(X0)
| sK21_skl(X0) = sK0_skl ),
inference(resolution,[status(thm)],[f298,f101]) ).
fof(f442,plain,
! [X0] :
( X0 = sK20_skl(X0)
| r1(sK0_skl)
| sP5_prd(sK20_skl(X0),X0) ),
inference(paramodulation,[status(thm)],[f430,f68]) ).
fof(f449,definition,
! [X0] :
( sQ5_spl
<=> ( X0 = sK20_skl(X0)
| sP5_prd(sK20_skl(X0),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f450,plain,
! [X0] :
( ~ sQ5_spl
| X0 = sK20_skl(X0)
| sP5_prd(sK20_skl(X0),X0) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,definition,
( sQ6_spl
<=> r1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f442,f449,f452]) ).
fof(f475,plain,
! [X0] :
( ~ sQ5_spl
| ~ r1(X0)
| X0 = sK21_skl(X0) ),
inference(backward_demodulation,[status(thm)],[f538,f126]) ).
fof(f478,plain,
! [X0] :
( ~ sQ5_spl
| r1(sK21_skl(X0))
| sP5_prd(X0,X0) ),
inference(backward_demodulation,[status(thm)],[f538,f68]) ).
fof(f538,plain,
! [X0] :
( ~ sQ5_spl
| X0 = sK20_skl(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f450,f101]) ).
fof(f662,plain,
( ~ sQ5_spl
| sK0_skl = sK21_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f475,f143]) ).
fof(f672,plain,
( ~ sQ5_spl
| r1(sK0_skl)
| sP5_prd(sK0_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f662,f478]) ).
fof(f673,definition,
( sQ7_spl
<=> sP5_prd(sK0_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f674,plain,
( ~ sQ7_spl
| sP5_prd(sK0_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f673]) ).
fof(f675,plain,
( sQ7_spl
| ~ sP5_prd(sK0_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f673]) ).
fof(f676,plain,
( ~ sQ5_spl
| sQ6_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f672,f673,f452,f449]) ).
fof(f686,plain,
! [X0] :
( X0 = sK0_skl
| X0 = sK21_skl(X0)
| sP5_prd(X0,X0) ),
inference(paramodulation,[status(thm)],[f300,f69]) ).
fof(f693,plain,
! [X0,X1] :
( X1 = sK1_skl(X0)
| ~ r2(X0,X1) ),
inference(resolution,[status(thm)],[f77,f23]) ).
fof(f697,plain,
! [X0,X1] :
( ~ sP5_prd(X0,X1)
| sK22_skl(X0,X1) = sK1_skl(sK23_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f693,f99]) ).
fof(f822,plain,
( ~ sQ3_spl
| sK0_skl = sK21_skl(sK0_skl)
| sP5_prd(sK0_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f422,f69]) ).
fof(f826,definition,
( sQ8_spl
<=> sK0_skl = sK21_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f827,plain,
( ~ sQ8_spl
| sK0_skl = sK21_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f826]) ).
fof(f829,plain,
( ~ sQ3_spl
| sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f822,f673,f826,f421]) ).
fof(f831,plain,
( ~ sQ7_spl
| sK23_skl(sK0_skl,sK0_skl) = sK0_skl ),
inference(resolution,[status(thm)],[f674,f299]) ).
fof(f832,plain,
( ~ sQ7_spl
| r2(sK22_skl(sK0_skl,sK0_skl),sK0_skl) ),
inference(resolution,[status(thm)],[f674,f100]) ).
fof(f834,plain,
! [X0] :
( ~ sQ7_spl
| ~ sP5_prd(sK0_skl,sK0_skl)
| ~ r2(X0,sK0_skl)
| ~ r1(X0)
| sP5_prd(sK22_skl(sK0_skl,sK0_skl),sK22_skl(sK0_skl,sK0_skl)) ),
inference(paramodulation,[status(thm)],[f831,f123]) ).
fof(f835,plain,
( ~ sQ7_spl
| r2(sK0_skl,sK22_skl(sK0_skl,sK0_skl))
| ~ sP5_prd(sK0_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f831,f99]) ).
fof(f836,plain,
( ~ sQ7_spl
| r1(sK0_skl)
| ~ sP5_prd(sK0_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f831,f98]) ).
fof(f837,definition,
( sQ9_spl
<=> sP5_prd(sK22_skl(sK0_skl,sK0_skl),sK22_skl(sK0_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f838,plain,
( ~ sQ9_spl
| sP5_prd(sK22_skl(sK0_skl,sK0_skl),sK22_skl(sK0_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f837]) ).
fof(f839,plain,
( sQ9_spl
| ~ sP5_prd(sK22_skl(sK0_skl,sK0_skl),sK22_skl(sK0_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f837]) ).
fof(f840,definition,
! [X0] :
( sQ10_spl
<=> ( ~ r2(X0,sK0_skl)
| ~ r1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f841,plain,
! [X0] :
( ~ sQ10_spl
| ~ r2(X0,sK0_skl)
| ~ r1(X0) ),
inference(component_clause,[status(thm)],[f840]) ).
fof(f843,plain,
( ~ sQ7_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f834,f837,f840,f673]) ).
fof(f844,definition,
( sQ11_spl
<=> r2(sK0_skl,sK22_skl(sK0_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f845,plain,
( ~ sQ11_spl
| r2(sK0_skl,sK22_skl(sK0_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f844]) ).
fof(f847,plain,
( sQ11_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f835,f673,f844]) ).
fof(f848,plain,
( sQ6_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f836,f673,f452]) ).
fof(f863,plain,
! [X0,X1] : sK4_skl(X0,X1) = sK1_skl(sK7_skl(X0,X1)),
inference(resolution,[status(thm)],[f38,f693]) ).
fof(f866,plain,
! [X0,X1] : ~ r1(sK4_skl(X0,X1)),
inference(resolution,[status(thm)],[f38,f108]) ).
fof(f921,plain,
! [X0,X1] :
( ~ r1(X0)
| X1 = sK20_skl(X1)
| r1(X0) ),
inference(resolution,[status(thm)],[f318,f72]) ).
fof(f923,definition,
! [X0] :
( sQ13_spl
<=> ( ~ r1(X0)
| r1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f926,definition,
! [X1] :
( sQ14_spl
<=> X1 = sK20_skl(X1) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f927,plain,
! [X0] :
( ~ sQ14_spl
| X0 = sK20_skl(X0) ),
inference(component_clause,[status(thm)],[f926]) ).
fof(f929,plain,
( sQ14_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f921,f923,f926]) ).
fof(f930,plain,
! [X0,X1] :
( ~ r1(X0)
| X1 = sK20_skl(X1)
| X0 = sK0_skl ),
inference(resolution,[status(thm)],[f317,f72]) ).
fof(f932,definition,
! [X0] :
( sQ15_spl
<=> ( ~ r1(X0)
| X0 = sK0_skl ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f935,plain,
( sQ14_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f930,f932,f926]) ).
fof(f937,plain,
( sQ3_spl
| ~ sQ14_spl
| sK0_skl != sK0_skl ),
inference(backward_demodulation,[status(thm)],[f927,f423]) ).
fof(f1017,plain,
( sQ3_spl
| ~ sQ14_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f937,f372,f926,f421]) ).
fof(f1195,plain,
! [X0] :
( X0 = sK17_skl(X0)
| X0 = sK18_skl(X0) ),
inference(resolution,[status(thm)],[f61,f93]) ).
fof(f1213,plain,
! [X0] :
( X0 = sK17_skl(X0)
| r2(sK19_skl(X0),sK18_skl(X0)) ),
inference(resolution,[status(thm)],[f60,f93]) ).
fof(f1218,plain,
( ~ sQ11_spl
| sK22_skl(sK0_skl,sK0_skl) = sK1_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f845,f693]) ).
fof(f1219,plain,
! [X0] :
( ~ sQ11_spl
| ~ r2(X0,sK0_skl)
| ~ r1(X0)
| sP5_prd(sK22_skl(sK0_skl,sK0_skl),sK22_skl(sK0_skl,sK0_skl)) ),
inference(resolution,[status(thm)],[f845,f114]) ).
fof(f1227,plain,
( ~ sQ7_spl
| ~ sQ11_spl
| r2(sK1_skl(sK0_skl),sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1218,f832]) ).
fof(f1229,plain,
( ~ sQ11_spl
| sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f1219,f837,f840,f844]) ).
fof(f1236,plain,
( ~ sQ7_spl
| ~ sQ11_spl
| ~ r1(sK0_skl) ),
inference(resolution,[status(thm)],[f1227,f108]) ).
fof(f1241,plain,
( ~ sQ7_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1236,f143]) ).
fof(f1242,plain,
( ~ sQ7_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f1241]) ).
fof(f1323,plain,
! [X0,X1] :
( X0 = sK21_skl(X0)
| ~ sP5_prd(sK20_skl(X0),X0)
| ~ r2(X1,sK0_skl)
| ~ r1(X1)
| sP5_prd(sK22_skl(sK20_skl(X0),X0),sK22_skl(sK20_skl(X0),X0)) ),
inference(paramodulation,[status(thm)],[f385,f123]) ).
fof(f1326,definition,
! [X0] :
( sQ20_spl
<=> ( X0 = sK21_skl(X0)
| ~ sP5_prd(sK20_skl(X0),X0)
| sP5_prd(sK22_skl(sK20_skl(X0),X0),sK22_skl(sK20_skl(X0),X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f1329,plain,
( sQ10_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1323,f1326,f840]) ).
fof(f1372,plain,
! [X0,X1,X2] :
( X2 = sK2_skl(X1,X0)
| ~ r3(X0,X1,X2) ),
inference(resolution,[status(thm)],[f82,f28]) ).
fof(f1375,plain,
! [X0] : X0 = sK2_skl(sK0_skl,X0),
inference(resolution,[status(thm)],[f1372,f306]) ).
fof(f1376,plain,
! [X0,X1] : sK7_skl(X0,X1) = sK2_skl(X0,X1),
inference(resolution,[status(thm)],[f1372,f39]) ).
fof(f1377,plain,
! [X0,X1] :
( X1 = sK20_skl(X1)
| X0 = sK2_skl(X1,X0) ),
inference(resolution,[status(thm)],[f1372,f315]) ).
fof(f1379,plain,
! [X0,X1] : sK4_skl(X0,X1) = sK1_skl(sK2_skl(X0,X1)),
inference(backward_demodulation,[status(thm)],[f1376,f863]) ).
fof(f1395,plain,
! [X0] :
( sK0_skl = sK20_skl(sK0_skl)
| X0 = X0 ),
inference(paramodulation,[status(thm)],[f1375,f1377]) ).
fof(f1399,definition,
! [X0] :
( sQ22_spl
<=> X0 = X0 ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f1402,plain,
( sQ3_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f1395,f1399,f421]) ).
fof(f1455,plain,
! [X0] : sK4_skl(sK0_skl,X0) = sK1_skl(X0),
inference(paramodulation,[status(thm)],[f1375,f1379]) ).
fof(f1456,plain,
! [X0,X1] :
( X0 = sK20_skl(X0)
| sK4_skl(X0,X1) = sK1_skl(X1) ),
inference(paramodulation,[status(thm)],[f1377,f1379]) ).
fof(f1479,plain,
! [X0,X1] :
( X1 = sK20_skl(X1)
| ~ r1(sK1_skl(X0)) ),
inference(paramodulation,[status(thm)],[f1456,f866]) ).
fof(f1481,definition,
! [X0] :
( sQ26_spl
<=> ~ r1(sK1_skl(X0)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f1484,plain,
( sQ14_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f1479,f1481,f926]) ).
fof(f1778,definition,
! [X0] :
( sQ28_spl
<=> X0 = sK2_skl(sK0_skl,X0) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1792,plain,
! [X0] :
( X0 = sK2_skl(sK0_skl,X0)
| sK0_skl = sK20_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f319,f1377]) ).
fof(f1798,plain,
( sQ28_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1792,f421,f1778]) ).
fof(f1859,definition,
( sQ30_spl
<=> r1(sK1_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1860,plain,
( ~ sQ30_spl
| r1(sK1_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1859]) ).
fof(f1861,plain,
( sQ30_spl
| ~ r1(sK1_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1859]) ).
fof(f1924,plain,
! [X0] :
( ~ r1(sK18_skl(X0))
| X0 = sK17_skl(X0) ),
inference(resolution,[status(thm)],[f1213,f108]) ).
fof(f1926,plain,
! [X0] :
( X0 = sK17_skl(X0)
| X0 = sK17_skl(X0)
| r2(sK19_skl(X0),X0) ),
inference(paramodulation,[status(thm)],[f1195,f1213]) ).
fof(f1927,plain,
! [X0] :
( X0 = sK17_skl(X0)
| r2(sK19_skl(X0),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1926]) ).
fof(f1937,plain,
! [X0] :
( sK0_skl = sK20_skl(sK0_skl)
| sK1_skl(X0) = sK1_skl(X0) ),
inference(paramodulation,[status(thm)],[f1455,f1456]) ).
fof(f1943,definition,
! [X0] :
( sQ33_spl
<=> sK1_skl(X0) = sK1_skl(X0) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f1946,plain,
( sQ3_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1937,f1943,f421]) ).
fof(f1972,plain,
! [X0] :
( X0 = sK17_skl(X0)
| ~ r1(X0)
| X0 = sK17_skl(X0) ),
inference(paramodulation,[status(thm)],[f1195,f1924]) ).
fof(f1973,plain,
! [X0] :
( ~ r1(X0)
| X0 = sK17_skl(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1972]) ).
fof(f1977,plain,
sK0_skl = sK17_skl(sK0_skl),
inference(resolution,[status(thm)],[f1973,f143]) ).
fof(f1985,plain,
( sK0_skl = sK18_skl(sK0_skl)
| sP4_prd(sK0_skl,sK0_skl) ),
inference(paramodulation,[status(thm)],[f1977,f61]) ).
fof(f1986,definition,
( sQ34_spl
<=> sK0_skl = sK18_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f1987,plain,
( ~ sQ34_spl
| sK0_skl = sK18_skl(sK0_skl) ),
inference(component_clause,[status(thm)],[f1986]) ).
fof(f1994,definition,
( sQ36_spl
<=> sP4_prd(sK0_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f2000,plain,
( sQ34_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f1985,f1994,f1986]) ).
fof(f2003,plain,
( ~ sQ34_spl
| ~ r1(sK0_skl)
| sK0_skl = sK17_skl(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1987,f1924]) ).
fof(f2008,definition,
( sQ37_spl
<=> sK0_skl = sK17_skl(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f2012,plain,
( ~ sQ34_spl
| ~ sQ6_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f2003,f2008,f452,f1986]) ).
fof(f2118,plain,
( ~ sQ10_spl
| ~ r1(sK19_skl(sK0_skl))
| sK0_skl = sK17_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f1927,f841]) ).
fof(f2126,definition,
( sQ39_spl
<=> r1(sK19_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f2129,plain,
( ~ sQ10_spl
| ~ sQ39_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f2118,f2008,f2126,f840]) ).
fof(f2130,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| sP5_prd(sK1_skl(sK0_skl),sK22_skl(sK0_skl,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1218,f838]) ).
fof(f2131,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| sP5_prd(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1218,f2130]) ).
fof(f2154,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| sK22_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) = sK1_skl(sK23_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl))) ),
inference(resolution,[status(thm)],[f2131,f697]) ).
fof(f2155,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| sK23_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) = sK0_skl ),
inference(resolution,[status(thm)],[f2131,f299]) ).
fof(f2156,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| r2(sK22_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)),sK1_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f2131,f100]) ).
fof(f2158,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| sK22_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) = sK1_skl(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f2155,f2154]) ).
fof(f2159,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| r2(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f2158,f2156]) ).
fof(f2160,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| sK1_skl(sK0_skl) = sK0_skl ),
inference(resolution,[status(thm)],[f2159,f309]) ).
fof(f2164,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| ~ r1(sK1_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f2159,f108]) ).
fof(f2181,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| ~ r1(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2160,f2164]) ).
fof(f2182,plain,
( ~ sQ9_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2181,f143]) ).
fof(f2183,plain,
( ~ sQ9_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2182]) ).
fof(f2215,plain,
( sQ9_spl
| ~ sQ11_spl
| ~ sP5_prd(sK1_skl(sK0_skl),sK22_skl(sK0_skl,sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1218,f839]) ).
fof(f2216,plain,
( sQ9_spl
| ~ sQ11_spl
| ~ sP5_prd(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1218,f2215]) ).
fof(f2224,plain,
( sQ9_spl
| ~ sQ11_spl
| sK1_skl(sK0_skl) = sK0_skl
| sK1_skl(sK0_skl) = sK21_skl(sK1_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f2216,f686]) ).
fof(f2225,definition,
( sQ42_spl
<=> sK1_skl(sK0_skl) = sK21_skl(sK1_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f2226,plain,
( ~ sQ42_spl
| sK1_skl(sK0_skl) = sK21_skl(sK1_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2225]) ).
fof(f2227,plain,
( sQ42_spl
| sK1_skl(sK0_skl) != sK21_skl(sK1_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2225]) ).
fof(f2228,definition,
( sQ43_spl
<=> sK1_skl(sK0_skl) = sK0_skl ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f2229,plain,
( ~ sQ43_spl
| sK1_skl(sK0_skl) = sK0_skl ),
inference(component_clause,[status(thm)],[f2228]) ).
fof(f2231,plain,
( sQ9_spl
| ~ sQ11_spl
| sQ43_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f2224,f2225,f2228,f844,f837]) ).
fof(f2234,plain,
( ~ sQ42_spl
| r1(sK1_skl(sK0_skl))
| sP5_prd(sK20_skl(sK1_skl(sK0_skl)),sK1_skl(sK0_skl)) ),
inference(paramodulation,[status(thm)],[f2226,f68]) ).
fof(f2245,definition,
( sQ46_spl
<=> sP5_prd(sK20_skl(sK1_skl(sK0_skl)),sK1_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f2246,plain,
( ~ sQ46_spl
| sP5_prd(sK20_skl(sK1_skl(sK0_skl)),sK1_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2245]) ).
fof(f2247,plain,
( sQ46_spl
| ~ sP5_prd(sK20_skl(sK1_skl(sK0_skl)),sK1_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2245]) ).
fof(f2248,plain,
( ~ sQ42_spl
| sQ30_spl
| sQ46_spl ),
inference(split_clause,[status(thm)],[f2234,f2245,f1859,f2225]) ).
fof(f2253,plain,
( ~ sQ11_spl
| ~ sQ43_spl
| sK22_skl(sK0_skl,sK0_skl) = sK0_skl ),
inference(backward_demodulation,[status(thm)],[f2229,f1218]) ).
fof(f2259,plain,
( ~ sQ46_spl
| sP5_prd(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f311,f2246]) ).
fof(f2260,plain,
( ~ sQ46_spl
| ~ sQ43_spl
| sP5_prd(sK0_skl,sK1_skl(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f2229,f2259]) ).
fof(f2261,plain,
( ~ sQ46_spl
| ~ sQ43_spl
| sP5_prd(sK0_skl,sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2229,f2260]) ).
fof(f2262,plain,
( ~ sQ46_spl
| ~ sQ43_spl
| sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2261,f675]) ).
fof(f2263,plain,
( ~ sQ46_spl
| ~ sQ43_spl
| sQ7_spl ),
inference(contradiction_clause,[status(thm)],[f2262]) ).
fof(f2264,plain,
( ~ sQ46_spl
| sQ9_spl
| ~ sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2259,f2216]) ).
fof(f2265,plain,
( ~ sQ46_spl
| sQ9_spl
| ~ sQ11_spl ),
inference(contradiction_clause,[status(thm)],[f2264]) ).
fof(f2266,plain,
( sQ46_spl
| ~ sP5_prd(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f311,f2247]) ).
fof(f2269,plain,
( sQ42_spl
| ~ sQ43_spl
| sK1_skl(sK0_skl) != sK21_skl(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f2229,f2227]) ).
fof(f2274,plain,
( sQ42_spl
| ~ sQ43_spl
| sK0_skl != sK21_skl(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2229,f2269]) ).
fof(f2275,plain,
( sQ42_spl
| ~ sQ43_spl
| ~ sQ8_spl
| sK0_skl != sK0_skl ),
inference(forward_demodulation,[status(thm)],[f827,f2274]) ).
fof(f2276,plain,
( sQ42_spl
| ~ sQ43_spl
| ~ sQ8_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2275]) ).
fof(f2277,plain,
( sQ42_spl
| ~ sQ43_spl
| ~ sQ8_spl ),
inference(contradiction_clause,[status(thm)],[f2276]) ).
fof(f2302,plain,
( ~ sQ46_spl
| sK22_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) = sK1_skl(sK23_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl))) ),
inference(resolution,[status(thm)],[f2259,f697]) ).
fof(f2303,plain,
( ~ sQ46_spl
| sK23_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) = sK0_skl ),
inference(resolution,[status(thm)],[f2259,f299]) ).
fof(f2304,plain,
( ~ sQ46_spl
| r2(sK22_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)),sK1_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f2259,f100]) ).
fof(f2306,plain,
( ~ sQ46_spl
| sK22_skl(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) = sK1_skl(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f2303,f2302]) ).
fof(f2307,plain,
( ~ sQ46_spl
| r2(sK1_skl(sK0_skl),sK1_skl(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f2306,f2304]) ).
fof(f2318,plain,
( ~ sQ46_spl
| sK1_skl(sK0_skl) = sK0_skl ),
inference(resolution,[status(thm)],[f2307,f309]) ).
fof(f2323,plain,
( ~ sQ46_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f2318,f2228,f2245]) ).
fof(f2352,plain,
( sQ46_spl
| sK1_skl(sK0_skl) = sK0_skl
| sK1_skl(sK0_skl) = sK21_skl(sK1_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f2266,f686]) ).
fof(f2353,plain,
( sQ46_spl
| sQ43_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f2352,f2225,f2228,f2245]) ).
fof(f2354,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1860,f310]) ).
fof(f2355,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f2354]) ).
fof(f2361,plain,
( ~ sQ11_spl
| ~ sQ43_spl
| sK0_skl = sK1_skl(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2253,f1218]) ).
fof(f2367,plain,
( sQ30_spl
| ~ sQ11_spl
| ~ sQ43_spl
| ~ r1(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2361,f1861]) ).
fof(f2368,plain,
( sQ30_spl
| ~ sQ11_spl
| ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2367,f143]) ).
fof(f2369,plain,
( sQ30_spl
| ~ sQ11_spl
| ~ sQ43_spl ),
inference(contradiction_clause,[status(thm)],[f2368]) ).
fof(f2377,plain,
( sQ42_spl
| ~ sQ43_spl
| sK0_skl = sK20_skl(sK0_skl) ),
inference(resolution,[status(thm)],[f2274,f115]) ).
fof(f2381,plain,
( sQ42_spl
| ~ sQ43_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f2377,f421,f2228,f2225]) ).
fof(f2385,plain,
$false,
inference(sat_refutation,[status(thm)],[f378,f380,f424,f455,f676,f829,f843,f847,f848,f929,f935,f1017,f1229,f1242,f1329,f1402,f1484,f1798,f1946,f2000,f2012,f2129,f2183,f2231,f2248,f2263,f2265,f2277,f2323,f2353,f2355,f2369,f2381]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN066+2 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n010.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 03:24:27 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 1.10/0.66 % Refutation found
% 1.10/0.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.10/0.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.10/0.69 % Elapsed time: 0.303438 seconds
% 1.10/0.69 % CPU time: 2.089643 seconds
% 1.10/0.69 % Total memory used: 139.822 MB
% 1.10/0.69 % Net memory used: 133.610 MB
%------------------------------------------------------------------------------