%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL670+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:08:29 PM UTC 2026
% Result : Theorem 234.45s 30.16s
% Output : CNFRefutation 177.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 39
% Syntax : Number of formulae : 201 ( 45 unt; 37 def)
% Number of atoms : 693 ( 0 equ)
% Maximal formula atoms : 49 ( 3 avg)
% Number of connectives : 905 ( 413 ~; 363 |; 92 &)
% ( 37 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 29 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 43 ( 42 usr; 37 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-3 aty)
% Number of variables : 246 ( 212 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : r1(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,conjecture,
~ ? [X] :
~ ( ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ( ! [X] :
( ~ ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( ~ ! [X] :
( ~ p2(X)
| ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ ! [X] :
( ~ ( ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& p2(X)
& ~ ! [Y] :
( ~ ( ~ p2(Y)
| ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ ! [X] :
( ~ ! [Y] :
( ~ p2(Y)
| ! [X] :
( p3(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ p4(Y)
| ~ r1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
~ ~ ? [X] :
~ ( ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ( ! [X] :
( ~ ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( ~ ! [X] :
( ~ p2(X)
| ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ ! [X] :
( ~ ( ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& p2(X)
& ~ ! [Y] :
( ~ ( ~ p2(Y)
| ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ ! [X] :
( ~ ! [Y] :
( ~ p2(Y)
| ! [X] :
( p3(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ p4(Y)
| ~ r1(X,Y) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f5,plain,
? [X] :
( ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ! [X] :
( ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ( ( ? [X] :
( ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( p2(X)
& ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ p2(X)
| ! [Y] :
( ( p2(Y)
& ? [X] :
( ~ p3(X)
& r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ! [X] :
( ? [Y] :
( p2(Y)
& ? [X] :
( ~ p3(X)
& r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ p4(Y)
| ~ r1(X,Y) ) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f6,definition,
! [Y,X] :
( sP0_prd(X,Y)
<=> ( p2(X)
& ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& r1(Y,X) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f7,plain,
? [X] :
( ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ! [X] :
( ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ( ( ? [X] :
( ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP0_prd(X,Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p2(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ p2(X)
| ! [Y] :
( ( p2(Y)
& ? [X] :
( ~ p3(X)
& r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ! [X] :
( ? [Y] :
( p2(Y)
& ? [X] :
( ~ p3(X)
& r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ p4(Y)
| ~ r1(X,Y) ) ),
inference(formula_renaming,[status(thm)],[f5,f6]) ).
fof(f8,plain,
( ! [Y] :
( ( p1(sK13_skl(Y))
& r1(Y,sK13_skl(Y)) )
| ! [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [X] :
( ( ~ p2(sK12_skl(X))
& r1(X,sK12_skl(X)) )
| ~ r1(sK11_skl,X) )
& r1(sK0_skl,sK11_skl)
& ~ p1(sK10_skl)
& r1(sK8_skl,sK10_skl)
& ! [Y] :
( p1(Y)
| ~ r1(sK9_skl,Y) )
& r1(sK8_skl,sK9_skl)
& r1(sK0_skl,sK8_skl)
& ! [Y] :
( ( ~ p1(sK7_skl(Y))
& r1(Y,sK7_skl(Y)) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ( ( ( ! [Y] :
( ~ p2(Y)
| ~ r1(sK6_skl(Y),Y) )
& r1(Y,sK6_skl(Y)) )
| ! [X] :
( ! [Y] :
( sP0_prd(sK5_skl(Y,X,Y),Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ! [Y] :
( ( ! [Y] :
( ~ p2(Y)
| ~ r1(sK4_skl(Y,X,Y),Y) )
& r1(Y,sK4_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ p2(X)
| ! [Y] :
( ( p2(Y)
& ~ p3(sK3_skl(Y,X,Y))
& r1(Y,sK3_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ! [X] :
( ( p2(sK1_skl(X,Y))
& ~ p3(sK2_skl(X,Y))
& r1(sK1_skl(X,Y),sK2_skl(X,Y))
& r1(X,sK1_skl(X,Y)) )
| ~ r1(Y,X) ) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ~ p4(Y)
| ~ r1(sK0_skl,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y)),skolemize(X,sK2_skl(X,Y)),skolemize(X,sK3_skl(Y,X,Y)),skolemize(X,sK4_skl(Y,X,Y)),skolemize(X,sK5_skl(Y,X,Y)),skolemize(X,sK6_skl(Y)),skolemize(X,sK7_skl(Y)),skolemize(Y,sK8_skl),skolemize(X,sK9_skl),skolemize(X,sK10_skl),skolemize(Y,sK11_skl),skolemize(Y,sK12_skl(X)),skolemize(X,sK13_skl(Y))],[f7]) ).
fof(f10,plain,
! [X0,X1] :
( r1(X1,sK1_skl(X1,X0))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f13,plain,
! [X0,X1] :
( p2(sK1_skl(X1,X0))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f18,plain,
! [X0,X1,X2,X3] :
( r1(X3,sK4_skl(X3,X1,X0))
| ~ r1(X1,X3)
| ~ p2(X1)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f19,plain,
! [X0,X1,X2,X3,X4] :
( ~ p2(X4)
| ~ r1(sK4_skl(X3,X1,X0),X4)
| ~ r1(X1,X3)
| ~ p2(X1)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f20,plain,
! [X0,X1,X2] :
( r1(X0,sK6_skl(X0))
| sP0_prd(sK5_skl(X2,X1,X0),X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f21,plain,
! [X0,X1,X2,X3] :
( ~ p2(X3)
| ~ r1(sK6_skl(X0),X3)
| sP0_prd(sK5_skl(X2,X1,X0),X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f24,plain,
r1(sK0_skl,sK8_skl),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f29,plain,
r1(sK0_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f30,plain,
! [X0] :
( r1(X0,sK12_skl(X0))
| ~ r1(sK11_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f31,plain,
! [X0] :
( ~ p2(sK12_skl(X0))
| ~ r1(sK11_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f34,plain,
! [Y,X] :
( ( ~ p2(X)
| ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X)
| sP0_prd(X,Y) )
& ( ( p2(X)
& ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& r1(Y,X) )
| ~ sP0_prd(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f35,plain,
( ! [Y,X] :
( ~ p2(X)
| ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X)
| sP0_prd(X,Y) )
& ! [Y,X] :
( ( p2(X)
& ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& r1(Y,X) )
| ~ sP0_prd(X,Y) ) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f36,plain,
( ! [Y,X] :
( ~ p2(X)
| ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X)
| sP0_prd(X,Y) )
& ! [Y,X] :
( ( p2(X)
& ~ p3(sK14_skl(X,Y))
& r1(X,sK14_skl(X,Y))
& r1(Y,X) )
| ~ sP0_prd(X,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(Y,sK14_skl(X,Y))],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( r1(X1,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f40,plain,
! [X0,X1] :
( p2(X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f46,plain,
! [X0,X1] :
( ~ sP0_prd(sK12_skl(X0),X1)
| ~ r1(sK11_skl,X0) ),
inference(resolution,[status(thm)],[f31,f40]) ).
fof(f52,plain,
! [X0] :
( r1(X0,sK1_skl(X0,sK11_skl))
| ~ r1(sK11_skl,X0) ),
inference(resolution,[status(thm)],[f10,f29]) ).
fof(f53,plain,
! [X0] :
( r1(X0,sK1_skl(X0,sK8_skl))
| ~ r1(sK8_skl,X0) ),
inference(resolution,[status(thm)],[f10,f24]) ).
fof(f55,plain,
! [X0] :
( r1(X0,sK1_skl(X0,sK0_skl))
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f10,f4]) ).
fof(f61,plain,
r1(sK11_skl,sK1_skl(sK11_skl,sK11_skl)),
inference(resolution,[status(thm)],[f52,f4]) ).
fof(f63,plain,
! [X0] : ~ sP0_prd(sK12_skl(sK1_skl(sK11_skl,sK11_skl)),X0),
inference(resolution,[status(thm)],[f61,f46]) ).
fof(f64,plain,
r1(sK1_skl(sK11_skl,sK11_skl),sK12_skl(sK1_skl(sK11_skl,sK11_skl))),
inference(resolution,[status(thm)],[f61,f30]) ).
fof(f68,plain,
r1(sK8_skl,sK1_skl(sK8_skl,sK8_skl)),
inference(resolution,[status(thm)],[f53,f4]) ).
fof(f71,plain,
r1(sK11_skl,sK1_skl(sK11_skl,sK0_skl)),
inference(resolution,[status(thm)],[f55,f29]) ).
fof(f72,plain,
r1(sK8_skl,sK1_skl(sK8_skl,sK0_skl)),
inference(resolution,[status(thm)],[f55,f24]) ).
fof(f74,plain,
r1(sK0_skl,sK1_skl(sK0_skl,sK0_skl)),
inference(resolution,[status(thm)],[f55,f4]) ).
fof(f76,plain,
! [X0] : ~ sP0_prd(sK12_skl(sK1_skl(sK11_skl,sK0_skl)),X0),
inference(resolution,[status(thm)],[f71,f46]) ).
fof(f77,plain,
r1(sK1_skl(sK11_skl,sK0_skl),sK12_skl(sK1_skl(sK11_skl,sK0_skl))),
inference(resolution,[status(thm)],[f71,f30]) ).
fof(f79,plain,
r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK1_skl(sK0_skl,sK0_skl),sK0_skl)),
inference(resolution,[status(thm)],[f74,f55]) ).
fof(f80,plain,
! [X0] :
( r1(X0,sK1_skl(X0,sK1_skl(sK0_skl,sK0_skl)))
| ~ r1(sK1_skl(sK0_skl,sK0_skl),X0) ),
inference(resolution,[status(thm)],[f74,f10]) ).
fof(f101,plain,
r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK0_skl,sK0_skl))),
inference(resolution,[status(thm)],[f80,f4]) ).
fof(f197,plain,
! [X0,X1,X2] :
( r1(X2,sK4_skl(X2,X0,sK11_skl))
| ~ r1(X0,X2)
| ~ p2(X0)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK11_skl,X0) ),
inference(resolution,[status(thm)],[f18,f29]) ).
fof(f203,plain,
! [X0,X1,X2,X3] :
( ~ p2(X3)
| ~ r1(sK4_skl(X2,X0,sK11_skl),X3)
| ~ r1(X0,X2)
| ~ p2(X0)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK11_skl,X0) ),
inference(resolution,[status(thm)],[f19,f29]) ).
fof(f209,plain,
! [X0,X1] :
( r1(sK11_skl,sK6_skl(sK11_skl))
| sP0_prd(sK5_skl(X1,X0,sK11_skl),X1)
| ~ r1(X0,X1)
| ~ r1(sK11_skl,X0) ),
inference(resolution,[status(thm)],[f20,f29]) ).
fof(f227,definition,
! [X0,X1] :
( sQ16_spl
<=> ( sP0_prd(sK5_skl(X1,X0,sK11_skl),X1)
| ~ r1(X0,X1)
| ~ r1(sK11_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f228,plain,
! [X0,X1] :
( ~ sQ16_spl
| sP0_prd(sK5_skl(X1,X0,sK11_skl),X1)
| ~ r1(X0,X1)
| ~ r1(sK11_skl,X0) ),
inference(component_clause,[status(thm)],[f227]) ).
fof(f230,definition,
( sQ17_spl
<=> r1(sK11_skl,sK6_skl(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( ~ sQ17_spl
| r1(sK11_skl,sK6_skl(sK11_skl)) ),
inference(component_clause,[status(thm)],[f230]) ).
fof(f233,plain,
( sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f209,f227,f230]) ).
fof(f260,definition,
( sQ23_spl
<=> r1(sK0_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f262,plain,
( sQ23_spl
| ~ r1(sK0_skl,sK11_skl) ),
inference(component_clause,[status(thm)],[f260]) ).
fof(f266,plain,
( sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f262,f29]) ).
fof(f267,plain,
sQ23_spl,
inference(contradiction_clause,[status(thm)],[f266]) ).
fof(f273,plain,
! [X0,X1,X2] :
( ~ p2(X2)
| ~ r1(sK6_skl(sK11_skl),X2)
| sP0_prd(sK5_skl(X1,X0,sK11_skl),X1)
| ~ r1(X0,X1)
| ~ r1(sK11_skl,X0) ),
inference(resolution,[status(thm)],[f21,f29]) ).
fof(f285,definition,
! [X2] :
( sQ26_spl
<=> ( ~ p2(X2)
| ~ r1(sK6_skl(sK11_skl),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f286,plain,
! [X0] :
( ~ sQ26_spl
| ~ p2(X0)
| ~ r1(sK6_skl(sK11_skl),X0) ),
inference(component_clause,[status(thm)],[f285]) ).
fof(f288,plain,
( sQ26_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f273,f227,f285]) ).
fof(f470,definition,
( sQ54_spl
<=> p2(sK1_skl(sK11_skl,sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( sQ54_spl
| ~ p2(sK1_skl(sK11_skl,sK11_skl)) ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,definition,
! [X1] :
( sQ55_spl
<=> ( r1(X1,sK4_skl(X1,sK1_skl(sK11_skl,sK11_skl),sK11_skl))
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f474,plain,
! [X0] :
( ~ sQ55_spl
| r1(X0,sK4_skl(X0,sK1_skl(sK11_skl,sK11_skl),sK11_skl))
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f659,definition,
! [X1,X2] :
( sQ100_spl
<=> ( ~ p2(X2)
| ~ r1(sK4_skl(X1,sK1_skl(sK11_skl,sK11_skl),sK11_skl),X2)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f660,plain,
! [X0,X1] :
( ~ sQ100_spl
| ~ p2(X1)
| ~ r1(sK4_skl(X0,sK1_skl(sK11_skl,sK11_skl),sK11_skl),X1)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f707,plain,
( sQ54_spl
| ~ r1(sK11_skl,sK11_skl)
| ~ r1(sK0_skl,sK11_skl) ),
inference(resolution,[status(thm)],[f472,f13]) ).
fof(f709,definition,
( sQ110_spl
<=> r1(sK11_skl,sK11_skl) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f711,plain,
( sQ110_spl
| ~ r1(sK11_skl,sK11_skl) ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f712,plain,
( sQ54_spl
| ~ sQ110_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f707,f260,f709,f470]) ).
fof(f713,plain,
( sQ110_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f711,f4]) ).
fof(f714,plain,
sQ110_spl,
inference(contradiction_clause,[status(thm)],[f713]) ).
fof(f874,plain,
! [X0,X1] :
( r1(X1,sK4_skl(X1,sK1_skl(sK11_skl,sK11_skl),sK11_skl))
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X1)
| ~ p2(sK1_skl(sK11_skl,sK11_skl))
| p2(X0)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ),
inference(resolution,[status(thm)],[f197,f61]) ).
fof(f890,definition,
! [X0] :
( sQ138_spl
<=> ( p2(X0)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f891,plain,
! [X0] :
( ~ sQ138_spl
| p2(X0)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ),
inference(component_clause,[status(thm)],[f890]) ).
fof(f893,plain,
( sQ55_spl
| ~ sQ54_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f874,f890,f470,f473]) ).
fof(f992,plain,
! [X0,X1,X2] :
( ~ p2(X2)
| ~ r1(sK4_skl(X1,sK1_skl(sK11_skl,sK11_skl),sK11_skl),X2)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X1)
| ~ p2(sK1_skl(sK11_skl,sK11_skl))
| p2(X0)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ),
inference(resolution,[status(thm)],[f203,f61]) ).
fof(f999,plain,
( sQ100_spl
| ~ sQ54_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f992,f890,f470,f659]) ).
fof(f1073,plain,
( ~ sQ138_spl
| p2(sK12_skl(sK1_skl(sK11_skl,sK11_skl))) ),
inference(resolution,[status(thm)],[f891,f64]) ).
fof(f1275,plain,
! [X0] :
( ~ sQ16_spl
| sP0_prd(sK5_skl(X0,sK1_skl(sK11_skl,sK11_skl),sK11_skl),X0)
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ),
inference(resolution,[status(thm)],[f228,f61]) ).
fof(f3290,plain,
( ~ sQ17_spl
| r1(sK6_skl(sK11_skl),sK1_skl(sK6_skl(sK11_skl),sK11_skl)) ),
inference(resolution,[status(thm)],[f231,f52]) ).
fof(f3770,plain,
( ~ sQ26_spl
| ~ sQ17_spl
| ~ p2(sK1_skl(sK6_skl(sK11_skl),sK11_skl)) ),
inference(resolution,[status(thm)],[f3290,f286]) ).
fof(f3771,plain,
( ~ sQ26_spl
| ~ sQ17_spl
| ~ r1(sK11_skl,sK6_skl(sK11_skl))
| ~ r1(sK0_skl,sK11_skl) ),
inference(resolution,[status(thm)],[f3770,f13]) ).
fof(f3773,plain,
( ~ sQ26_spl
| ~ sQ17_spl
| ~ sQ23_spl ),
inference(split_clause,[status(thm)],[f3771,f260,f230,f285]) ).
fof(f4833,definition,
( sQ523_spl
<=> r1(sK11_skl,sK1_skl(sK11_skl,sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ523_spl])],[split_symbol_definition]) ).
fof(f4835,plain,
( sQ523_spl
| ~ r1(sK11_skl,sK1_skl(sK11_skl,sK11_skl)) ),
inference(component_clause,[status(thm)],[f4833]) ).
fof(f4838,plain,
( sQ523_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4835,f61]) ).
fof(f4839,plain,
sQ523_spl,
inference(contradiction_clause,[status(thm)],[f4838]) ).
fof(f4848,definition,
( sQ525_spl
<=> r1(sK11_skl,sK1_skl(sK11_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ525_spl])],[split_symbol_definition]) ).
fof(f4850,plain,
( sQ525_spl
| ~ r1(sK11_skl,sK1_skl(sK11_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f4848]) ).
fof(f4853,plain,
( sQ525_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4850,f71]) ).
fof(f4854,plain,
sQ525_spl,
inference(contradiction_clause,[status(thm)],[f4853]) ).
fof(f4863,definition,
( sQ527_spl
<=> r1(sK8_skl,sK1_skl(sK8_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ527_spl])],[split_symbol_definition]) ).
fof(f4865,plain,
( sQ527_spl
| ~ r1(sK8_skl,sK1_skl(sK8_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f4863]) ).
fof(f4868,plain,
( sQ527_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4865,f68]) ).
fof(f4869,plain,
sQ527_spl,
inference(contradiction_clause,[status(thm)],[f4868]) ).
fof(f4878,definition,
( sQ529_spl
<=> r1(sK8_skl,sK1_skl(sK8_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ529_spl])],[split_symbol_definition]) ).
fof(f4880,plain,
( sQ529_spl
| ~ r1(sK8_skl,sK1_skl(sK8_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f4878]) ).
fof(f4883,plain,
( sQ529_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4880,f72]) ).
fof(f4884,plain,
sQ529_spl,
inference(contradiction_clause,[status(thm)],[f4883]) ).
fof(f4893,definition,
( sQ531_spl
<=> r1(sK0_skl,sK1_skl(sK0_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ531_spl])],[split_symbol_definition]) ).
fof(f4895,plain,
( sQ531_spl
| ~ r1(sK0_skl,sK1_skl(sK0_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f4893]) ).
fof(f4898,plain,
( sQ531_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4895,f74]) ).
fof(f4899,plain,
sQ531_spl,
inference(contradiction_clause,[status(thm)],[f4898]) ).
fof(f5353,definition,
( sQ579_spl
<=> r1(sK7_skl(sK11_skl),sK7_skl(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ579_spl])],[split_symbol_definition]) ).
fof(f5355,plain,
( sQ579_spl
| ~ r1(sK7_skl(sK11_skl),sK7_skl(sK11_skl)) ),
inference(component_clause,[status(thm)],[f5353]) ).
fof(f5358,plain,
( sQ579_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5355,f4]) ).
fof(f5359,plain,
sQ579_spl,
inference(contradiction_clause,[status(thm)],[f5358]) ).
fof(f5842,plain,
( ~ sQ55_spl
| r1(sK1_skl(sK11_skl,sK11_skl),sK4_skl(sK1_skl(sK11_skl,sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl)) ),
inference(resolution,[status(thm)],[f474,f4]) ).
fof(f5851,plain,
! [X0] :
( ~ sQ100_spl
| ~ p2(X0)
| ~ r1(sK4_skl(sK1_skl(sK11_skl,sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl),X0) ),
inference(resolution,[status(thm)],[f660,f4]) ).
fof(f5868,plain,
( ~ sQ138_spl
| ~ r1(sK11_skl,sK1_skl(sK11_skl,sK11_skl)) ),
inference(resolution,[status(thm)],[f1073,f31]) ).
fof(f5870,plain,
( ~ sQ138_spl
| ~ sQ523_spl ),
inference(split_clause,[status(thm)],[f5868,f4833,f890]) ).
fof(f5871,definition,
! [X0] :
( sQ651_spl
<=> ( ~ r1(X0,sK12_skl(sK1_skl(sK11_skl,sK11_skl)))
| sP0_prd(sK12_skl(sK1_skl(sK11_skl,sK11_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ651_spl])],[split_symbol_definition]) ).
fof(f5872,plain,
! [X0] :
( ~ sQ651_spl
| ~ r1(X0,sK12_skl(sK1_skl(sK11_skl,sK11_skl)))
| sP0_prd(sK12_skl(sK1_skl(sK11_skl,sK11_skl)),X0) ),
inference(component_clause,[status(thm)],[f5871]) ).
fof(f5878,plain,
! [X0] :
( ~ sQ651_spl
| ~ r1(X0,sK12_skl(sK1_skl(sK11_skl,sK11_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f5872,f63]) ).
fof(f5879,plain,
( ~ sQ651_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f64,f5878]) ).
fof(f5881,plain,
~ sQ651_spl,
inference(contradiction_clause,[status(thm)],[f5879]) ).
fof(f6042,definition,
( sQ672_spl
<=> r1(sK13_skl(sK11_skl),sK13_skl(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ672_spl])],[split_symbol_definition]) ).
fof(f6044,plain,
( sQ672_spl
| ~ r1(sK13_skl(sK11_skl),sK13_skl(sK11_skl)) ),
inference(component_clause,[status(thm)],[f6042]) ).
fof(f6047,plain,
( sQ672_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6044,f4]) ).
fof(f6048,plain,
sQ672_spl,
inference(contradiction_clause,[status(thm)],[f6047]) ).
fof(f6055,definition,
( sQ673_spl
<=> r1(sK7_skl(sK8_skl),sK7_skl(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ673_spl])],[split_symbol_definition]) ).
fof(f6057,plain,
( sQ673_spl
| ~ r1(sK7_skl(sK8_skl),sK7_skl(sK8_skl)) ),
inference(component_clause,[status(thm)],[f6055]) ).
fof(f6060,plain,
( sQ673_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6057,f4]) ).
fof(f6061,plain,
sQ673_spl,
inference(contradiction_clause,[status(thm)],[f6060]) ).
fof(f6098,definition,
! [X0] :
( sQ677_spl
<=> ( ~ r1(X0,sK12_skl(sK1_skl(sK11_skl,sK0_skl)))
| sP0_prd(sK12_skl(sK1_skl(sK11_skl,sK0_skl)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ677_spl])],[split_symbol_definition]) ).
fof(f6099,plain,
! [X0] :
( ~ sQ677_spl
| ~ r1(X0,sK12_skl(sK1_skl(sK11_skl,sK0_skl)))
| sP0_prd(sK12_skl(sK1_skl(sK11_skl,sK0_skl)),X0) ),
inference(component_clause,[status(thm)],[f6098]) ).
fof(f6105,plain,
! [X0] :
( ~ sQ677_spl
| ~ r1(X0,sK12_skl(sK1_skl(sK11_skl,sK0_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6099,f76]) ).
fof(f6106,plain,
( ~ sQ677_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f77,f6105]) ).
fof(f6108,plain,
~ sQ677_spl,
inference(contradiction_clause,[status(thm)],[f6106]) ).
fof(f6111,definition,
( sQ679_spl
<=> r1(sK12_skl(sK11_skl),sK12_skl(sK11_skl)) ),
introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition]) ).
fof(f6113,plain,
( sQ679_spl
| ~ r1(sK12_skl(sK11_skl),sK12_skl(sK11_skl)) ),
inference(component_clause,[status(thm)],[f6111]) ).
fof(f6116,plain,
( sQ679_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6113,f4]) ).
fof(f6117,plain,
sQ679_spl,
inference(contradiction_clause,[status(thm)],[f6116]) ).
fof(f6201,plain,
! [X0] :
( ~ sQ16_spl
| r1(X0,sK5_skl(X0,sK1_skl(sK11_skl,sK11_skl),sK11_skl))
| ~ r1(sK1_skl(sK11_skl,sK11_skl),X0) ),
inference(resolution,[status(thm)],[f1275,f37]) ).
fof(f7056,definition,
( sQ753_spl
<=> r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK0_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ753_spl])],[split_symbol_definition]) ).
fof(f7058,plain,
( sQ753_spl
| ~ r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK0_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f7056]) ).
fof(f7061,plain,
( sQ753_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7058,f4]) ).
fof(f7062,plain,
sQ753_spl,
inference(contradiction_clause,[status(thm)],[f7061]) ).
fof(f8921,definition,
( sQ908_spl
<=> r1(sK1_skl(sK8_skl,sK8_skl),sK1_skl(sK8_skl,sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ908_spl])],[split_symbol_definition]) ).
fof(f8923,plain,
( sQ908_spl
| ~ r1(sK1_skl(sK8_skl,sK8_skl),sK1_skl(sK8_skl,sK8_skl)) ),
inference(component_clause,[status(thm)],[f8921]) ).
fof(f8926,plain,
( sQ908_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8923,f4]) ).
fof(f8927,plain,
sQ908_spl,
inference(contradiction_clause,[status(thm)],[f8926]) ).
fof(f8946,definition,
( sQ911_spl
<=> r1(sK1_skl(sK8_skl,sK0_skl),sK1_skl(sK8_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ911_spl])],[split_symbol_definition]) ).
fof(f8948,plain,
( sQ911_spl
| ~ r1(sK1_skl(sK8_skl,sK0_skl),sK1_skl(sK8_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f8946]) ).
fof(f8951,plain,
( sQ911_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f8948,f4]) ).
fof(f8952,plain,
sQ911_spl,
inference(contradiction_clause,[status(thm)],[f8951]) ).
fof(f9042,definition,
( sQ926_spl
<=> r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK1_skl(sK0_skl,sK0_skl),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ926_spl])],[split_symbol_definition]) ).
fof(f9044,plain,
( sQ926_spl
| ~ r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK1_skl(sK0_skl,sK0_skl),sK0_skl)) ),
inference(component_clause,[status(thm)],[f9042]) ).
fof(f9047,plain,
( sQ926_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9044,f79]) ).
fof(f9048,plain,
sQ926_spl,
inference(contradiction_clause,[status(thm)],[f9047]) ).
fof(f9093,plain,
( ~ sQ16_spl
| ~ sQ55_spl
| r1(sK4_skl(sK1_skl(sK11_skl,sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl),sK5_skl(sK4_skl(sK1_skl(sK11_skl,sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl)) ),
inference(resolution,[status(thm)],[f5842,f6201]) ).
fof(f9941,definition,
( sQ982_spl
<=> r1(sK7_skl(sK7_skl(sK0_skl)),sK7_skl(sK7_skl(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ982_spl])],[split_symbol_definition]) ).
fof(f9943,plain,
( sQ982_spl
| ~ r1(sK7_skl(sK7_skl(sK0_skl)),sK7_skl(sK7_skl(sK0_skl))) ),
inference(component_clause,[status(thm)],[f9941]) ).
fof(f9946,plain,
( sQ982_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9943,f4]) ).
fof(f9947,plain,
sQ982_spl,
inference(contradiction_clause,[status(thm)],[f9946]) ).
fof(f10176,definition,
! [X0] :
( sQ1001_spl
<=> ~ r1(X0,sK5_skl(sK13_skl(sK11_skl),sK11_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1001_spl])],[split_symbol_definition]) ).
fof(f10177,plain,
! [X0] :
( ~ sQ1001_spl
| ~ r1(X0,sK5_skl(sK13_skl(sK11_skl),sK11_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f10176]) ).
fof(f10184,plain,
( ~ sQ1001_spl
| $false ),
inference(resolution,[status(thm)],[f10177,f4]) ).
fof(f10186,plain,
~ sQ1001_spl,
inference(contradiction_clause,[status(thm)],[f10184]) ).
fof(f10751,definition,
( sQ1028_spl
<=> r1(sK1_skl(sK11_skl,sK11_skl),sK12_skl(sK1_skl(sK11_skl,sK11_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1028_spl])],[split_symbol_definition]) ).
fof(f10753,plain,
( sQ1028_spl
| ~ r1(sK1_skl(sK11_skl,sK11_skl),sK12_skl(sK1_skl(sK11_skl,sK11_skl))) ),
inference(component_clause,[status(thm)],[f10751]) ).
fof(f10756,plain,
( sQ1028_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10753,f64]) ).
fof(f10757,plain,
sQ1028_spl,
inference(contradiction_clause,[status(thm)],[f10756]) ).
fof(f10761,definition,
( sQ1029_spl
<=> r1(sK1_skl(sK11_skl,sK0_skl),sK12_skl(sK1_skl(sK11_skl,sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1029_spl])],[split_symbol_definition]) ).
fof(f10763,plain,
( sQ1029_spl
| ~ r1(sK1_skl(sK11_skl,sK0_skl),sK12_skl(sK1_skl(sK11_skl,sK0_skl))) ),
inference(component_clause,[status(thm)],[f10761]) ).
fof(f10766,plain,
( sQ1029_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10763,f77]) ).
fof(f10767,plain,
sQ1029_spl,
inference(contradiction_clause,[status(thm)],[f10766]) ).
fof(f10879,definition,
( sQ1035_spl
<=> r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK0_skl,sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1035_spl])],[split_symbol_definition]) ).
fof(f10881,plain,
( sQ1035_spl
| ~ r1(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK1_skl(sK0_skl,sK0_skl),sK1_skl(sK0_skl,sK0_skl))) ),
inference(component_clause,[status(thm)],[f10879]) ).
fof(f10884,plain,
( sQ1035_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10881,f101]) ).
fof(f10885,plain,
sQ1035_spl,
inference(contradiction_clause,[status(thm)],[f10884]) ).
fof(f12546,definition,
( sQ1170_spl
<=> r1(sK13_skl(sK8_skl),sK13_skl(sK8_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1170_spl])],[split_symbol_definition]) ).
fof(f12548,plain,
( sQ1170_spl
| ~ r1(sK13_skl(sK8_skl),sK13_skl(sK8_skl)) ),
inference(component_clause,[status(thm)],[f12546]) ).
fof(f12551,plain,
( sQ1170_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12548,f4]) ).
fof(f12552,plain,
sQ1170_spl,
inference(contradiction_clause,[status(thm)],[f12551]) ).
fof(f12784,definition,
( sQ1176_spl
<=> r1(sK1_skl(sK7_skl(sK0_skl),sK0_skl),sK1_skl(sK7_skl(sK0_skl),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1176_spl])],[split_symbol_definition]) ).
fof(f12786,plain,
( sQ1176_spl
| ~ r1(sK1_skl(sK7_skl(sK0_skl),sK0_skl),sK1_skl(sK7_skl(sK0_skl),sK0_skl)) ),
inference(component_clause,[status(thm)],[f12784]) ).
fof(f12789,plain,
( sQ1176_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12786,f4]) ).
fof(f12790,plain,
sQ1176_spl,
inference(contradiction_clause,[status(thm)],[f12789]) ).
fof(f12862,definition,
( sQ1180_spl
<=> r1(sK1_skl(sK13_skl(sK0_skl),sK0_skl),sK1_skl(sK13_skl(sK0_skl),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1180_spl])],[split_symbol_definition]) ).
fof(f12864,plain,
( sQ1180_spl
| ~ r1(sK1_skl(sK13_skl(sK0_skl),sK0_skl),sK1_skl(sK13_skl(sK0_skl),sK0_skl)) ),
inference(component_clause,[status(thm)],[f12862]) ).
fof(f12867,plain,
( sQ1180_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f12864,f4]) ).
fof(f12868,plain,
sQ1180_spl,
inference(contradiction_clause,[status(thm)],[f12867]) ).
fof(f13253,definition,
( sQ1204_spl
<=> r1(sK6_skl(sK0_skl),sK6_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1204_spl])],[split_symbol_definition]) ).
fof(f13255,plain,
( sQ1204_spl
| ~ r1(sK6_skl(sK0_skl),sK6_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f13253]) ).
fof(f13258,plain,
( sQ1204_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13255,f4]) ).
fof(f13259,plain,
sQ1204_spl,
inference(contradiction_clause,[status(thm)],[f13258]) ).
fof(f13963,definition,
( sQ1314_spl
<=> r1(sK5_skl(sK0_skl,sK0_skl,sK0_skl),sK5_skl(sK0_skl,sK0_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1314_spl])],[split_symbol_definition]) ).
fof(f13965,plain,
( sQ1314_spl
| ~ r1(sK5_skl(sK0_skl,sK0_skl,sK0_skl),sK5_skl(sK0_skl,sK0_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f13963]) ).
fof(f13967,plain,
( sQ1314_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f13965,f4]) ).
fof(f13968,plain,
sQ1314_spl,
inference(contradiction_clause,[status(thm)],[f13967]) ).
fof(f15505,definition,
( sQ1389_spl
<=> r1(sK2_skl(sK0_skl,sK0_skl),sK2_skl(sK0_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1389_spl])],[split_symbol_definition]) ).
fof(f15507,plain,
( sQ1389_spl
| ~ r1(sK2_skl(sK0_skl,sK0_skl),sK2_skl(sK0_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f15505]) ).
fof(f15510,plain,
( sQ1389_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15507,f4]) ).
fof(f15511,plain,
sQ1389_spl,
inference(contradiction_clause,[status(thm)],[f15510]) ).
fof(f15553,definition,
( sQ1390_spl
<=> r1(sK13_skl(sK1_skl(sK0_skl,sK0_skl)),sK13_skl(sK1_skl(sK0_skl,sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ1390_spl])],[split_symbol_definition]) ).
fof(f15555,plain,
( sQ1390_spl
| ~ r1(sK13_skl(sK1_skl(sK0_skl,sK0_skl)),sK13_skl(sK1_skl(sK0_skl,sK0_skl))) ),
inference(component_clause,[status(thm)],[f15553]) ).
fof(f15558,plain,
( sQ1390_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f15555,f4]) ).
fof(f15559,plain,
sQ1390_spl,
inference(contradiction_clause,[status(thm)],[f15558]) ).
fof(f16289,plain,
( ~ sQ100_spl
| ~ sQ16_spl
| ~ sQ55_spl
| ~ p2(sK5_skl(sK4_skl(sK1_skl(sK11_skl,sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl)) ),
inference(resolution,[status(thm)],[f9093,f5851]) ).
fof(f16293,plain,
! [X0] :
( ~ sQ100_spl
| ~ sQ16_spl
| ~ sQ55_spl
| ~ sP0_prd(sK5_skl(sK4_skl(sK1_skl(sK11_skl,sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl),X0) ),
inference(resolution,[status(thm)],[f16289,f40]) ).
fof(f16294,plain,
( ~ sQ16_spl
| ~ sQ100_spl
| ~ sQ55_spl
| ~ r1(sK1_skl(sK11_skl,sK11_skl),sK4_skl(sK1_skl(sK11_skl,sK11_skl),sK1_skl(sK11_skl,sK11_skl),sK11_skl)) ),
inference(resolution,[status(thm)],[f16293,f1275]) ).
fof(f16295,plain,
( ~ sQ16_spl
| ~ sQ100_spl
| ~ sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f16294,f5842]) ).
fof(f16296,plain,
( ~ sQ16_spl
| ~ sQ100_spl
| ~ sQ55_spl ),
inference(contradiction_clause,[status(thm)],[f16295]) ).
fof(f16297,plain,
$false,
inference(sat_refutation,[status(thm)],[f233,f267,f288,f712,f714,f893,f999,f3773,f4839,f4854,f4869,f4884,f4899,f5359,f5870,f5881,f6048,f6061,f6108,f6117,f7062,f8927,f8952,f9048,f9947,f10186,f10757,f10767,f10885,f12552,f12790,f12868,f13259,f13968,f15511,f15559,f16296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL670+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n002.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 00:55:16 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.20/0.43 % Drodi V4.1.1
% 234.45/30.16 % Refutation found
% 234.45/30.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 234.45/30.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 61.15/30.21 % Elapsed time: 29.772395 seconds
% 61.15/30.21 % CPU time: 235.486283 seconds
% 61.15/30.21 % Total memory used: 271.282 MB
% 61.15/30.21 % Net memory used: 232.117 MB
%------------------------------------------------------------------------------