%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL640+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:08:06 PM UTC 2026
% Result : Theorem 40.70s 5.56s
% Output : CNFRefutation 40.70s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X] :
~ ( ~ ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ( ( ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ( ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| p1(Y) )
& ( ~ ! [X] :
( ~ ! [Y] :
( ~ ( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) ) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) ) ) )
| ~ r1(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ? [X] :
~ ( ~ ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ( ( ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ( ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| p1(Y) )
& ( ~ ! [X] :
( ~ ! [Y] :
( ~ ( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) ) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) ) ) )
| ~ r1(X,Y) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
? [X] :
( ? [Y] :
( ! [X] :
( ? [Y] :
( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ( ( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( p1(X)
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| p1(Y) )
& ( ? [X] :
( ! [Y] :
( ( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) ) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& p1(X)
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ? [Y] :
( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) ) ) )
| ~ r1(X,Y) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,definition,
! [X,Y] :
( sP0_prd(Y,X)
<=> ( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f5,definition,
! [X,Y] :
( sP1_prd(Y,X)
<=> ( ~ p1(Y)
& r1(X,Y) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f6,definition,
! [Y,X] :
( sP2_prd(X,Y)
<=> ( p1(X)
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f7,plain,
? [X] :
( ? [Y] :
( ! [X] :
( ? [Y] :
( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) )
| p1(X)
| ~ r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ( ( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP2_prd(X,Y)
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ? [Y] : sP1_prd(Y,X)
| ~ r1(Y,X) )
| p1(Y) )
& ( ? [X] :
( ! [Y] :
( ( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) ) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& p1(X)
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ? [Y] : sP0_prd(Y,X)
| ~ r1(Y,X) )
| ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) ) ) )
| ~ r1(X,Y) ) ),
inference(formula_renaming,[status(thm)],[f3,f6,f5,f4]) ).
fof(f8,plain,
( ! [X] :
( ( p1(sK13_skl(X))
& ~ p1(sK14_skl(X))
& r1(sK13_skl(X),sK14_skl(X))
& r1(X,sK13_skl(X)) )
| p1(X)
| ~ r1(sK10_skl,X) )
& ! [Y] :
( p1(Y)
| ~ r1(sK12_skl,Y) )
& r1(sK10_skl,sK12_skl)
& ~ p1(sK11_skl)
& r1(sK10_skl,sK11_skl)
& r1(sK0_skl,sK10_skl)
& ! [Y] :
( ( ( ( ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(sK9_skl(Y),Y) )
& ~ p1(sK9_skl(Y))
& r1(Y,sK9_skl(Y)) )
| ! [X] :
( ! [Y] :
( sP2_prd(sK8_skl(Y,X,Y),Y)
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
& ! [X] :
( ( ~ p1(sK7_skl(X,Y))
& r1(X,sK7_skl(X,Y)) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ( ( ! [Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(sK6_skl(Y),Y) )
& ~ p1(sK6_skl(Y))
& r1(Y,sK6_skl(Y)) )
| ! [X] :
( sP1_prd(sK5_skl(X,Y),X)
| ~ r1(Y,X) )
| p1(Y) )
& ( ( ! [Y] :
( ( p1(Y)
& ~ p1(sK4_skl(Y,Y))
& r1(Y,sK4_skl(Y,Y)) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK2_skl(Y),Y) )
& p1(sK2_skl(Y))
& ~ p1(sK3_skl(Y))
& r1(sK2_skl(Y),sK3_skl(Y))
& r1(Y,sK2_skl(Y)) )
| ! [X] :
( sP0_prd(sK1_skl(X,Y),X)
| ~ r1(Y,X) )
| ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) ) ) )
| ~ 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,sK14_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y)),skolemize(X,sK2_skl(Y)),skolemize(Y,sK3_skl(Y)),skolemize(X,sK4_skl(Y,Y)),skolemize(Y,sK5_skl(X,Y)),skolemize(X,sK6_skl(Y)),skolemize(Y,sK7_skl(X,Y)),skolemize(X,sK8_skl(Y,X,Y)),skolemize(X,sK9_skl(Y)),skolemize(Y,sK10_skl),skolemize(X,sK11_skl),skolemize(X,sK12_skl),skolemize(Y,sK13_skl(X)),skolemize(X,sK14_skl(X))],[f7]) ).
fof(f9,plain,
! [X0,X1,X2] :
( r1(X0,sK2_skl(X0))
| sP0_prd(sK1_skl(X2,X0),X2)
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f10,plain,
! [X0,X1,X2] :
( r1(sK2_skl(X0),sK3_skl(X0))
| sP0_prd(sK1_skl(X2,X0),X2)
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f11,plain,
! [X0,X1,X2] :
( ~ p1(sK3_skl(X0))
| sP0_prd(sK1_skl(X2,X0),X2)
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f15,plain,
! [X0,X1,X2,X3,X4,X5] :
( p1(X3)
| ~ p1(X4)
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(sK2_skl(X0),X3)
| sP0_prd(sK1_skl(X2,X0),X2)
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f16,plain,
! [X0,X1] :
( r1(X0,sK6_skl(X0))
| sP1_prd(sK5_skl(X1,X0),X1)
| ~ r1(X0,X1)
| p1(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f17,plain,
! [X0,X1] :
( ~ p1(sK6_skl(X0))
| sP1_prd(sK5_skl(X1,X0),X1)
| ~ r1(X0,X1)
| p1(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f18,plain,
! [X0,X1,X2,X3] :
( ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3)
| ~ r1(sK6_skl(X0),X2)
| sP1_prd(sK5_skl(X1,X0),X1)
| ~ r1(X0,X1)
| p1(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f19,plain,
! [X0,X1,X2,X3] :
( r1(X1,sK7_skl(X1,X0))
| p1(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f20,plain,
! [X0,X1,X2,X3] :
( ~ p1(sK7_skl(X1,X0))
| p1(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f21,plain,
! [X0,X1,X2] :
( r1(X0,sK9_skl(X0))
| sP2_prd(sK8_skl(X2,X1,X0),X2)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f22,plain,
! [X0,X1,X2] :
( ~ p1(sK9_skl(X0))
| sP2_prd(sK8_skl(X2,X1,X0),X2)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f23,plain,
! [X0,X1,X2,X3,X4] :
( ~ p1(X3)
| p1(X4)
| ~ r1(X3,X4)
| ~ r1(sK9_skl(X0),X3)
| sP2_prd(sK8_skl(X2,X1,X0),X2)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f24,plain,
r1(sK0_skl,sK10_skl),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f25,plain,
r1(sK10_skl,sK11_skl),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f26,plain,
~ p1(sK11_skl),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f27,plain,
r1(sK10_skl,sK12_skl),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f28,plain,
! [X0] :
( p1(X0)
| ~ r1(sK12_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f29,plain,
! [X0] :
( r1(X0,sK13_skl(X0))
| p1(X0)
| ~ r1(sK10_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f30,plain,
! [X0] :
( r1(sK13_skl(X0),sK14_skl(X0))
| p1(X0)
| ~ r1(sK10_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f31,plain,
! [X0] :
( ~ p1(sK14_skl(X0))
| p1(X0)
| ~ r1(sK10_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f32,plain,
! [X0] :
( p1(sK13_skl(X0))
| p1(X0)
| ~ r1(sK10_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f33,plain,
! [X,Y] :
( ( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y)
| sP0_prd(Y,X) )
& ( ( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) )
| ~ sP0_prd(Y,X) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f34,plain,
( ! [X,Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y)
| sP0_prd(Y,X) )
& ! [X,Y] :
( ( p1(Y)
& ? [X] :
( ~ p1(X)
& r1(Y,X) )
& r1(X,Y) )
| ~ sP0_prd(Y,X) ) ),
inference(miniscoping,[status(thm)],[f33]) ).
fof(f35,plain,
( ! [X,Y] :
( ~ p1(Y)
| ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y)
| sP0_prd(Y,X) )
& ! [X,Y] :
( ( p1(Y)
& ~ p1(sK15_skl(Y,X))
& r1(Y,sK15_skl(Y,X))
& r1(X,Y) )
| ~ sP0_prd(Y,X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X,sK15_skl(Y,X))],[f34]) ).
fof(f36,plain,
! [X0,X1] :
( r1(X1,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [X0,X1] :
( r1(X0,sK15_skl(X0,X1))
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f38,plain,
! [X0,X1] :
( ~ p1(sK15_skl(X0,X1))
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f39,plain,
! [X0,X1] :
( p1(X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f41,plain,
! [X,Y] :
( ( p1(Y)
| ~ r1(X,Y)
| sP1_prd(Y,X) )
& ( ( ~ p1(Y)
& r1(X,Y) )
| ~ sP1_prd(Y,X) ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f42,plain,
( ! [X,Y] :
( p1(Y)
| ~ r1(X,Y)
| sP1_prd(Y,X) )
& ! [X,Y] :
( ( ~ p1(Y)
& r1(X,Y) )
| ~ sP1_prd(Y,X) ) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f43,plain,
! [X0,X1] :
( r1(X1,X0)
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f44,plain,
! [X0,X1] :
( ~ p1(X0)
| ~ sP1_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f46,plain,
! [Y,X] :
( ( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X)
| sP2_prd(X,Y) )
& ( ( p1(X)
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
| ~ sP2_prd(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f47,plain,
( ! [Y,X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X)
| sP2_prd(X,Y) )
& ! [Y,X] :
( ( p1(X)
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
| ~ sP2_prd(X,Y) ) ),
inference(miniscoping,[status(thm)],[f46]) ).
fof(f48,plain,
( ! [Y,X] :
( ~ p1(X)
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X)
| sP2_prd(X,Y) )
& ! [Y,X] :
( ( p1(X)
& ~ p1(sK16_skl(X,Y))
& r1(X,sK16_skl(X,Y))
& r1(Y,X) )
| ~ sP2_prd(X,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(Y,sK16_skl(X,Y))],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( r1(X1,X0)
| ~ sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0,X1] :
( r1(X0,sK16_skl(X0,X1))
| ~ sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f51,plain,
! [X0,X1] :
( ~ p1(sK16_skl(X0,X1))
| ~ sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f52,plain,
! [X0,X1] :
( p1(X0)
| ~ sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f53,plain,
! [X0,X1,X2] :
( ~ p1(X0)
| p1(X2)
| ~ r1(X0,X2)
| ~ r1(X1,X0)
| sP2_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f54,plain,
! [X0,X1] :
( r1(sK10_skl,sK2_skl(sK10_skl))
| sP0_prd(sK1_skl(X1,sK10_skl),X1)
| ~ r1(sK10_skl,X1)
| ~ p1(sK10_skl)
| p1(X0)
| ~ r1(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f9,f24]) ).
fof(f55,plain,
! [X0,X1] :
( r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(X1,sK10_skl),X1)
| ~ r1(sK10_skl,X1)
| ~ p1(sK10_skl)
| p1(X0)
| ~ r1(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f10,f24]) ).
fof(f57,plain,
! [X0] :
( ~ p1(sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl)
| p1(sK11_skl)
| ~ r1(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f11,f25]) ).
fof(f60,plain,
! [X0] :
( ~ p1(sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl)
| p1(sK11_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f57,f24]) ).
fof(f111,plain,
! [X0,X1,X2,X3] :
( p1(X1)
| ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK2_skl(sK10_skl),X1)
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl)
| p1(sK11_skl)
| ~ r1(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f15,f25]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( p1(X1)
| ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK2_skl(sK10_skl),X1)
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl)
| p1(sK11_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f111,f24]) ).
fof(f152,plain,
! [X0] :
( r1(sK10_skl,sK6_skl(sK10_skl))
| sP1_prd(sK5_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f16,f24]) ).
fof(f157,plain,
( ~ p1(sK6_skl(sK10_skl))
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl)
| ~ r1(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f17,f27]) ).
fof(f162,plain,
( ~ p1(sK6_skl(sK10_skl))
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f157,f24]) ).
fof(f209,plain,
! [X0,X1] :
( ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK6_skl(sK10_skl),X0)
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl)
| ~ r1(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f18,f27]) ).
fof(f214,plain,
! [X0,X1] :
( ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK6_skl(sK10_skl),X0)
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f209,f24]) ).
fof(f216,plain,
! [X0,X1,X2] :
( r1(X0,sK7_skl(X0,sK10_skl))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f19,f24]) ).
fof(f234,plain,
! [X0,X1] :
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK12_skl,X0) ),
inference(resolution,[status(thm)],[f216,f27]) ).
fof(f236,plain,
! [X0,X1] :
( r1(sK10_skl,sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(X1,X0,sK10_skl),X1)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK10_skl,X0) ),
inference(resolution,[status(thm)],[f21,f24]) ).
fof(f343,plain,
( r1(sK10_skl,sK6_skl(sK10_skl))
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f152,f27]) ).
fof(f345,plain,
( r1(sK12_skl,sK5_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f343,f43]) ).
fof(f346,plain,
( ~ p1(sK5_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f343,f44]) ).
fof(f350,plain,
( p1(sK5_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f345,f28]) ).
fof(f363,plain,
( r1(sK10_skl,sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f350,f346]) ).
fof(f369,plain,
( r1(sK13_skl(sK6_skl(sK10_skl)),sK14_skl(sK6_skl(sK10_skl)))
| p1(sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f363,f30]) ).
fof(f370,plain,
( r1(sK6_skl(sK10_skl),sK13_skl(sK6_skl(sK10_skl)))
| p1(sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f363,f29]) ).
fof(f371,plain,
( p1(sK13_skl(sK6_skl(sK10_skl)))
| p1(sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f363,f32]) ).
fof(f394,plain,
! [X0] :
( r1(sK10_skl,sK2_skl(sK10_skl))
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl)
| p1(sK11_skl) ),
inference(resolution,[status(thm)],[f54,f25]) ).
fof(f395,plain,
! [X0] :
( r1(sK10_skl,sK2_skl(sK10_skl))
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f394,f26]) ).
fof(f398,plain,
! [X0] :
( r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl)
| p1(sK11_skl) ),
inference(resolution,[status(thm)],[f55,f25]) ).
fof(f399,plain,
! [X0] :
( r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f398,f26]) ).
fof(f435,plain,
! [X0] :
( ~ p1(sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f60,f26]) ).
fof(f437,plain,
( ~ p1(sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK10_skl) ),
inference(resolution,[status(thm)],[f435,f27]) ).
fof(f454,plain,
( r1(sK10_skl,sK2_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK10_skl) ),
inference(resolution,[status(thm)],[f395,f27]) ).
fof(f468,plain,
( r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK10_skl) ),
inference(resolution,[status(thm)],[f399,f27]) ).
fof(f496,plain,
! [X0,X1,X2,X3] :
( p1(X1)
| ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK2_skl(sK10_skl),X1)
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0)
| ~ p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f115,f26]) ).
fof(f501,plain,
! [X0] :
( p1(sK6_skl(sK10_skl))
| p1(sK10_skl)
| ~ p1(sK13_skl(sK6_skl(sK10_skl)))
| p1(X0)
| ~ r1(sK13_skl(sK6_skl(sK10_skl)),X0)
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f214,f370]) ).
fof(f502,plain,
! [X0] :
( p1(sK6_skl(sK10_skl))
| ~ p1(sK13_skl(sK6_skl(sK10_skl)))
| p1(X0)
| ~ r1(sK13_skl(sK6_skl(sK10_skl)),X0)
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f501]) ).
fof(f503,plain,
! [X0] :
( p1(sK6_skl(sK10_skl))
| p1(X0)
| ~ r1(sK13_skl(sK6_skl(sK10_skl)),X0)
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f502,f371]) ).
fof(f536,plain,
! [X0] :
( p1(X0)
| ~ r1(sK13_skl(sK6_skl(sK10_skl)),X0)
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f503,f162]) ).
fof(f537,plain,
( p1(sK6_skl(sK10_skl))
| p1(sK10_skl)
| p1(sK14_skl(sK6_skl(sK10_skl)))
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f536,f369]) ).
fof(f538,plain,
( p1(sK6_skl(sK10_skl))
| p1(sK14_skl(sK6_skl(sK10_skl)))
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f537]) ).
fof(f539,plain,
( p1(sK14_skl(sK6_skl(sK10_skl)))
| sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f538,f162]) ).
fof(f540,plain,
( r1(sK12_skl,sK5_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK6_skl(sK10_skl)))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f539,f43]) ).
fof(f541,plain,
( ~ p1(sK5_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK6_skl(sK10_skl)))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f539,f44]) ).
fof(f543,plain,
( p1(sK5_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK6_skl(sK10_skl)))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f540,f28]) ).
fof(f556,plain,
( p1(sK14_skl(sK6_skl(sK10_skl)))
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f543,f541]) ).
fof(f561,plain,
( p1(sK6_skl(sK10_skl))
| ~ r1(sK10_skl,sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f556,f31]) ).
fof(f562,plain,
( p1(sK6_skl(sK10_skl))
| p1(sK10_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f561,f363]) ).
fof(f567,plain,
( sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK10_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f162,f562]) ).
fof(f570,plain,
( r1(sK12_skl,sK5_skl(sK12_skl,sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f567,f43]) ).
fof(f571,plain,
( ~ p1(sK5_skl(sK12_skl,sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f567,f44]) ).
fof(f611,plain,
( p1(sK5_skl(sK12_skl,sK10_skl))
| p1(sK10_skl) ),
inference(resolution,[status(thm)],[f570,f28]) ).
fof(f624,plain,
p1(sK10_skl),
inference(forward_subsumption_resolution,[status(thm)],[f611,f571]) ).
fof(f629,plain,
! [X0,X1,X2,X3] :
( p1(X1)
| ~ p1(X2)
| p1(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK2_skl(sK10_skl),X1)
| sP0_prd(sK1_skl(X0,sK10_skl),X0)
| ~ r1(sK10_skl,X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f496,f624]) ).
fof(f636,plain,
( ~ p1(sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f437,f624]) ).
fof(f639,plain,
( r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f468,f624]) ).
fof(f641,plain,
( r1(sK10_skl,sK2_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f454,f624]) ).
fof(f646,plain,
! [X0,X1,X2] :
( p1(X0)
| ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK2_skl(sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f629,f27]) ).
fof(f756,plain,
( r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f641,f37]) ).
fof(f757,plain,
( r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f641,f36]) ).
fof(f758,plain,
( p1(sK1_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f641,f39]) ).
fof(f792,plain,
! [X0] :
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f757,f234]) ).
fof(f796,plain,
! [X0,X1] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(X1)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X1)
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f757,f20]) ).
fof(f799,plain,
! [X0] :
( ~ p1(sK1_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f757,f53]) ).
fof(f806,plain,
! [X0] :
( p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f799,f758]) ).
fof(f1217,plain,
( r1(sK10_skl,sK2_skl(sK10_skl))
| r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f792,f756]) ).
fof(f1219,plain,
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1217]) ).
fof(f1221,plain,
( r1(sK10_skl,sK2_skl(sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f806,f756]) ).
fof(f1223,plain,
( p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1221]) ).
fof(f1276,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1219,f38]) ).
fof(f1277,plain,
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1276,f641]) ).
fof(f1279,plain,
( p1(sK7_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1277,f28]) ).
fof(f1296,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1223,f38]) ).
fof(f1297,plain,
( sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1296,f641]) ).
fof(f1298,plain,
( r1(sK1_skl(sK12_skl,sK10_skl),sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1297,f50]) ).
fof(f1413,plain,
! [X0,X1] :
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK3_skl(sK10_skl))
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK3_skl(sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f646,f639]) ).
fof(f1415,plain,
! [X0,X1] :
( p1(sK3_skl(sK10_skl))
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK3_skl(sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f1413]) ).
fof(f1416,plain,
! [X0,X1] :
( ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK3_skl(sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1415,f636]) ).
fof(f1524,plain,
! [X0] :
( r1(sK10_skl,sK2_skl(sK10_skl))
| ~ p1(sK7_skl(sK12_skl,X0))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f796,f1298]) ).
fof(f1526,plain,
! [X0] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1524]) ).
fof(f1528,plain,
( r1(sK10_skl,sK2_skl(sK10_skl))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| ~ r1(sK0_skl,sK10_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1526,f1279]) ).
fof(f1529,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| ~ r1(sK0_skl,sK10_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f1528]) ).
fof(f1530,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1529,f24]) ).
fof(f1531,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1530,f27]) ).
fof(f1532,plain,
( ~ sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK2_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1531,f51]) ).
fof(f1533,plain,
r1(sK10_skl,sK2_skl(sK10_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1532,f1297]) ).
fof(f1541,plain,
! [X0] :
( r1(sK10_skl,sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0)
| p1(X0)
| ~ r1(sK2_skl(sK10_skl),X0) ),
inference(resolution,[status(thm)],[f1533,f236]) ).
fof(f1549,plain,
! [X0,X1,X2] :
( ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK9_skl(sK10_skl),X1)
| sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0)
| p1(X0)
| ~ r1(sK2_skl(sK10_skl),X0)
| ~ r1(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f1533,f23]) ).
fof(f1550,plain,
! [X0] :
( ~ p1(sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0)
| p1(X0)
| ~ r1(sK2_skl(sK10_skl),X0)
| ~ r1(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f1533,f22]) ).
fof(f1564,plain,
! [X0,X1,X2] :
( ~ p1(X1)
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK9_skl(sK10_skl),X1)
| sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0)
| p1(X0)
| ~ r1(sK2_skl(sK10_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1549,f24]) ).
fof(f1565,plain,
! [X0] :
( ~ p1(sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0)
| p1(X0)
| ~ r1(sK2_skl(sK10_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1550,f24]) ).
fof(f1785,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))
| p1(sK3_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1565,f639]) ).
fof(f1787,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1785,f636]) ).
fof(f1790,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))
| p1(sK3_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1541,f639]) ).
fof(f1792,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl))
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1790,f636]) ).
fof(f2049,plain,
( r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1792,f50]) ).
fof(f2050,plain,
( r1(sK3_skl(sK10_skl),sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1792,f49]) ).
fof(f2051,plain,
( p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1792,f52]) ).
fof(f2058,plain,
! [X0] :
( ~ p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f2050,f1416]) ).
fof(f2076,plain,
! [X0] :
( ~ p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f2058]) ).
fof(f2077,plain,
! [X0] :
( p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2076,f2051]) ).
fof(f2373,plain,
! [X0,X1] :
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK9_skl(sK10_skl),X0)
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))
| p1(sK3_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f1564,f639]) ).
fof(f2375,plain,
! [X0,X1] :
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK9_skl(sK10_skl),X0)
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2373,f636]) ).
fof(f3207,plain,
( p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f2049,f2077]) ).
fof(f3229,plain,
( p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f3207]) ).
fof(f3235,plain,
( ~ sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3229,f51]) ).
fof(f3236,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3235,f1792]) ).
fof(f3237,plain,
( r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3236,f37]) ).
fof(f3238,plain,
( r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3236,f36]) ).
fof(f3239,plain,
( p1(sK1_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3236,f39]) ).
fof(f3240,plain,
! [X0] :
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3238,f234]) ).
fof(f3252,plain,
! [X0,X1] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(X1)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X1)
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3238,f20]) ).
fof(f3255,plain,
! [X0] :
( ~ p1(sK1_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3238,f53]) ).
fof(f3269,plain,
! [X0] :
( p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3255,f3239]) ).
fof(f3294,plain,
( r1(sK10_skl,sK9_skl(sK10_skl))
| r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3240,f3237]) ).
fof(f3295,plain,
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f3294]) ).
fof(f3296,plain,
( r1(sK10_skl,sK9_skl(sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3269,f3237]) ).
fof(f3297,plain,
( p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f3296]) ).
fof(f3298,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3295,f38]) ).
fof(f3299,plain,
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3298,f3236]) ).
fof(f3301,plain,
( p1(sK7_skl(sK12_skl,sK10_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3299,f28]) ).
fof(f3326,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3297,f38]) ).
fof(f3327,plain,
( sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3326,f3236]) ).
fof(f3328,plain,
( r1(sK1_skl(sK12_skl,sK10_skl),sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3327,f50]) ).
fof(f3355,plain,
! [X0] :
( r1(sK10_skl,sK9_skl(sK10_skl))
| ~ p1(sK7_skl(sK12_skl,X0))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3252,f3328]) ).
fof(f3357,plain,
! [X0] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f3355]) ).
fof(f3359,plain,
( r1(sK10_skl,sK9_skl(sK10_skl))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| ~ r1(sK0_skl,sK10_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3357,f3301]) ).
fof(f3360,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| ~ r1(sK0_skl,sK10_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f3359]) ).
fof(f3361,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3360,f24]) ).
fof(f3362,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3361,f27]) ).
fof(f3363,plain,
( ~ sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK10_skl,sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3362,f51]) ).
fof(f3364,plain,
r1(sK10_skl,sK9_skl(sK10_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f3363,f3327]) ).
fof(f3374,plain,
( r1(sK13_skl(sK9_skl(sK10_skl)),sK14_skl(sK9_skl(sK10_skl)))
| p1(sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3364,f30]) ).
fof(f3375,plain,
( r1(sK9_skl(sK10_skl),sK13_skl(sK9_skl(sK10_skl)))
| p1(sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3364,f29]) ).
fof(f3376,plain,
( p1(sK13_skl(sK9_skl(sK10_skl)))
| p1(sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3364,f32]) ).
fof(f3403,plain,
! [X0] :
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK13_skl(sK9_skl(sK10_skl)))
| p1(X0)
| ~ r1(sK13_skl(sK9_skl(sK10_skl)),X0)
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))
| p1(sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3375,f2375]) ).
fof(f3426,plain,
! [X0] :
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK13_skl(sK9_skl(sK10_skl)))
| p1(X0)
| ~ r1(sK13_skl(sK9_skl(sK10_skl)),X0)
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3403,f1787]) ).
fof(f3894,plain,
( p1(sK9_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| ~ p1(sK13_skl(sK9_skl(sK10_skl)))
| p1(sK14_skl(sK9_skl(sK10_skl)))
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f3426,f3374]) ).
fof(f3897,plain,
( p1(sK9_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl)))
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3894,f3376]) ).
fof(f3898,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl)))
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3897,f1787]) ).
fof(f3899,plain,
( r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f3898,f50]) ).
fof(f3900,plain,
( r1(sK3_skl(sK10_skl),sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f3898,f49]) ).
fof(f3901,plain,
( p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f3898,f52]) ).
fof(f3911,plain,
! [X0] :
( ~ p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f3900,f1416]) ).
fof(f3937,plain,
! [X0] :
( ~ p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(duplicate_literals_removal,[status(thm)],[f3911]) ).
fof(f3938,plain,
! [X0] :
( p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3937,f3901]) ).
fof(f4229,plain,
( p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f3899,f3938]) ).
fof(f4251,plain,
( p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(duplicate_literals_removal,[status(thm)],[f4229]) ).
fof(f4257,plain,
( ~ sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4251,f51]) ).
fof(f4258,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4257,f3898]) ).
fof(f4259,plain,
( r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4258,f37]) ).
fof(f4260,plain,
( r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4258,f36]) ).
fof(f4261,plain,
( p1(sK1_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4258,f39]) ).
fof(f4264,plain,
! [X0] :
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4260,f234]) ).
fof(f4277,plain,
! [X0,X1] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(X1)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X1)
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4260,f20]) ).
fof(f4280,plain,
! [X0] :
( ~ p1(sK1_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4260,f53]) ).
fof(f4294,plain,
! [X0] :
( p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4280,f4261]) ).
fof(f4320,plain,
( p1(sK14_skl(sK9_skl(sK10_skl)))
| r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4264,f4259]) ).
fof(f4321,plain,
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(duplicate_literals_removal,[status(thm)],[f4320]) ).
fof(f4322,plain,
( p1(sK14_skl(sK9_skl(sK10_skl)))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4294,f4259]) ).
fof(f4323,plain,
( p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(duplicate_literals_removal,[status(thm)],[f4322]) ).
fof(f4324,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4321,f38]) ).
fof(f4325,plain,
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4324,f4258]) ).
fof(f4327,plain,
( p1(sK7_skl(sK12_skl,sK10_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4325,f28]) ).
fof(f4353,plain,
( p1(sK9_skl(sK10_skl))
| ~ r1(sK10_skl,sK9_skl(sK10_skl))
| p1(sK7_skl(sK12_skl,sK10_skl)) ),
inference(resolution,[status(thm)],[f4327,f31]) ).
fof(f4354,plain,
( p1(sK9_skl(sK10_skl))
| p1(sK7_skl(sK12_skl,sK10_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4353,f3364]) ).
fof(f4355,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4323,f38]) ).
fof(f4356,plain,
( sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4355,f4258]) ).
fof(f4357,plain,
( r1(sK1_skl(sK12_skl,sK10_skl),sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4356,f50]) ).
fof(f4385,plain,
! [X0] :
( p1(sK14_skl(sK9_skl(sK10_skl)))
| ~ p1(sK7_skl(sK12_skl,X0))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4277,f4357]) ).
fof(f4387,plain,
! [X0] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(duplicate_literals_removal,[status(thm)],[f4385]) ).
fof(f4389,plain,
( p1(sK9_skl(sK10_skl))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| ~ r1(sK0_skl,sK10_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4387,f4354]) ).
fof(f4390,plain,
( p1(sK9_skl(sK10_skl))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4389,f24]) ).
fof(f4391,plain,
( p1(sK9_skl(sK10_skl))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4390,f27]) ).
fof(f4392,plain,
( ~ sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| p1(sK9_skl(sK10_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(resolution,[status(thm)],[f4391,f51]) ).
fof(f4393,plain,
( p1(sK9_skl(sK10_skl))
| p1(sK14_skl(sK9_skl(sK10_skl))) ),
inference(forward_subsumption_resolution,[status(thm)],[f4392,f4356]) ).
fof(f4397,plain,
( p1(sK9_skl(sK10_skl))
| ~ r1(sK10_skl,sK9_skl(sK10_skl))
| p1(sK9_skl(sK10_skl)) ),
inference(resolution,[status(thm)],[f4393,f31]) ).
fof(f4398,plain,
( ~ r1(sK10_skl,sK9_skl(sK10_skl))
| p1(sK9_skl(sK10_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f4397]) ).
fof(f4399,plain,
p1(sK9_skl(sK10_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f4398,f3364]) ).
fof(f4417,plain,
( sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f1787,f4399]) ).
fof(f4459,plain,
( r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f4417,f50]) ).
fof(f4460,plain,
( r1(sK3_skl(sK10_skl),sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f4417,f49]) ).
fof(f4461,plain,
( p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f4417,f52]) ).
fof(f4522,plain,
! [X0] :
( ~ p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f4460,f1416]) ).
fof(f4549,plain,
! [X0] :
( ~ p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))
| p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f4522]) ).
fof(f4550,plain,
! [X0] :
( p1(X0)
| ~ r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X0)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4549,f4461]) ).
fof(f5319,plain,
( p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f4459,f4550]) ).
fof(f5340,plain,
( p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f5319]) ).
fof(f5346,plain,
( ~ sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))
| sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f5340,f51]) ).
fof(f5347,plain,
sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl),
inference(forward_subsumption_resolution,[status(thm)],[f5346,f4417]) ).
fof(f5348,plain,
r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
inference(resolution,[status(thm)],[f5347,f37]) ).
fof(f5349,plain,
r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl)),
inference(resolution,[status(thm)],[f5347,f36]) ).
fof(f5350,plain,
p1(sK1_skl(sK12_skl,sK10_skl)),
inference(resolution,[status(thm)],[f5347,f39]) ).
fof(f5351,plain,
! [X0] :
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0) ),
inference(resolution,[status(thm)],[f5349,f234]) ).
fof(f5362,plain,
! [X0,X1] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(X1)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X1)
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f5349,f20]) ).
fof(f5365,plain,
! [X0] :
( ~ p1(sK1_skl(sK12_skl,sK10_skl))
| p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f5349,f53]) ).
fof(f5379,plain,
! [X0] :
( p1(X0)
| ~ r1(sK1_skl(sK12_skl,sK10_skl),X0)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5365,f5350]) ).
fof(f5405,plain,
( r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))
| p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl)) ),
inference(resolution,[status(thm)],[f5351,f5348]) ).
fof(f5407,plain,
( p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f5379,f5348]) ).
fof(f5408,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)) ),
inference(resolution,[status(thm)],[f5405,f38]) ).
fof(f5409,plain,
r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f5408,f5347]) ).
fof(f5410,plain,
p1(sK7_skl(sK12_skl,sK10_skl)),
inference(resolution,[status(thm)],[f5409,f28]) ).
fof(f5438,plain,
( ~ sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)
| sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl) ),
inference(resolution,[status(thm)],[f5407,f38]) ).
fof(f5439,plain,
sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl),
inference(forward_subsumption_resolution,[status(thm)],[f5438,f5347]) ).
fof(f5440,plain,
r1(sK1_skl(sK12_skl,sK10_skl),sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
inference(resolution,[status(thm)],[f5439,f50]) ).
fof(f5471,plain,
! [X0] :
( ~ p1(sK7_skl(sK12_skl,X0))
| p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(X0,sK12_skl)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f5362,f5440]) ).
fof(f5473,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl)
| ~ r1(sK0_skl,sK10_skl) ),
inference(resolution,[status(thm)],[f5471,f5410]) ).
fof(f5474,plain,
( p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))
| ~ r1(sK10_skl,sK12_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5473,f24]) ).
fof(f5475,plain,
p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f5474,f27]) ).
fof(f5476,plain,
~ sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl),
inference(resolution,[status(thm)],[f5475,f51]) ).
fof(f5477,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f5476,f5439]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL640+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n008.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 00:43:08 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 40.70/5.56 % Refutation found
% 40.70/5.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 40.70/5.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 40.70/5.59 % Elapsed time: 5.220227 seconds
% 40.70/5.59 % CPU time: 41.209414 seconds
% 40.70/5.59 % Total memory used: 154.050 MB
% 40.70/5.59 % Net memory used: 140.633 MB
%------------------------------------------------------------------------------