%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN723+1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:17:58 PM UTC 2026
% Result : Theorem 0.22s 0.27s
% Output : Refutation 0.22s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( ? [X0] :
! [X1] :
( p(X0)
<=> p(X1) )
<=> ( ( ? [X0] : q(X0)
<=> ! [X1] : r(X1) )
<=> ( ( ? [X0] :
! [X1] :
( q(X0)
<=> q(X1) )
<=> ( ? [X0] : r(X0)
<=> ! [X1] : s(X1) ) )
<=> ( ? [X0] :
! [X1] :
( r(X0)
<=> r(X1) )
<=> ( ( ? [X0] : s(X0)
<=> ! [X1] : p(X1) )
<=> ( ? [X0] :
! [X1] :
( s(X0)
<=> s(X1) )
<=> ( ? [X0] : p(X0)
<=> ! [X1] : q(X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm138) ).
fof(f2,negated_conjecture,
~ ( ? [X0] :
! [X1] :
( p(X0)
<=> p(X1) )
<=> ( ( ? [X0] : q(X0)
<=> ! [X1] : r(X1) )
<=> ( ( ? [X0] :
! [X1] :
( q(X0)
<=> q(X1) )
<=> ( ? [X0] : r(X0)
<=> ! [X1] : s(X1) ) )
<=> ( ? [X0] :
! [X1] :
( r(X0)
<=> r(X1) )
<=> ( ( ? [X0] : s(X0)
<=> ! [X1] : p(X1) )
<=> ( ? [X0] :
! [X1] :
( s(X0)
<=> s(X1) )
<=> ( ? [X0] : p(X0)
<=> ! [X1] : q(X1) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ( ? [X0] :
! [X1] :
( p(X0)
<=> p(X1) )
<=> ( ( ? [X2] : q(X2)
<=> ! [X3] : r(X3) )
<=> ( ( ? [X4] :
! [X5] :
( q(X4)
<=> q(X5) )
<=> ( ? [X6] : r(X6)
<=> ! [X7] : s(X7) ) )
<=> ( ? [X8] :
! [X9] :
( r(X8)
<=> r(X9) )
<=> ( ( ? [X10] : s(X10)
<=> ! [X11] : p(X11) )
<=> ( ? [X12] :
! [X13] :
( s(X12)
<=> s(X13) )
<=> ( ? [X14] : p(X14)
<=> ! [X15] : q(X15) ) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
( ? [X0] :
! [X1] :
( p(X0)
<=> p(X1) )
<~> ( ( ? [X2] : q(X2)
<=> ! [X3] : r(X3) )
<=> ( ( ? [X4] :
! [X5] :
( q(X4)
<=> q(X5) )
<=> ( ? [X6] : r(X6)
<=> ! [X7] : s(X7) ) )
<=> ( ? [X8] :
! [X9] :
( r(X8)
<=> r(X9) )
<=> ( ( ? [X10] : s(X10)
<=> ! [X11] : p(X11) )
<=> ( ? [X12] :
! [X13] :
( s(X12)
<=> s(X13) )
<=> ( ? [X14] : p(X14)
<=> ! [X15] : q(X15) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
! [X14,X15,X13] :
( q(X15)
| ~ p(X14)
| ~ s(X13)
| s(sK21)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f6,plain,
! [X14,X15,X13] :
( q(X15)
| ~ p(X14)
| s(X13)
| ~ s(sK21)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f7,plain,
! [X13] :
( ~ q(sK24)
| p(sK23)
| ~ s(X13)
| s(sK21)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f8,plain,
! [X13] :
( ~ q(sK24)
| p(sK23)
| s(X13)
| ~ s(sK21)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f9,plain,
! [X14,X12] :
( ~ q(sK24)
| ~ p(X14)
| s(sK22(X12))
| s(X12)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f10,plain,
! [X14,X12] :
( ~ q(sK24)
| ~ p(X14)
| ~ s(sK22(X12))
| ~ s(X12)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f11,plain,
! [X15,X12] :
( q(X15)
| p(sK23)
| s(sK22(X12))
| s(X12)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f12,plain,
! [X15,X12] :
( q(X15)
| p(sK23)
| ~ s(sK22(X12))
| ~ s(X12)
| sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f13,plain,
! [X14,X13] :
( ~ q(sK24)
| ~ p(X14)
| ~ s(X13)
| s(sK21)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f14,plain,
! [X14,X13] :
( ~ q(sK24)
| ~ p(X14)
| s(X13)
| ~ s(sK21)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f15,plain,
! [X15,X13] :
( q(X15)
| p(sK23)
| ~ s(X13)
| s(sK21)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f16,plain,
! [X15,X13] :
( q(X15)
| p(sK23)
| s(X13)
| ~ s(sK21)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f17,plain,
! [X14,X15,X12] :
( q(X15)
| ~ p(X14)
| s(sK22(X12))
| s(X12)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f18,plain,
! [X14,X15,X12] :
( q(X15)
| ~ p(X14)
| ~ s(sK22(X12))
| ~ s(X12)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f19,plain,
! [X12] :
( ~ q(sK24)
| p(sK23)
| s(sK22(X12))
| s(X12)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f20,plain,
! [X12] :
( ~ q(sK24)
| p(sK23)
| ~ s(sK22(X12))
| ~ s(X12)
| ~ sP15 ),
inference(cnf_transformation,[],[f4]) ).
fof(f21,plain,
! [X8,X9] :
( sP16(X9,X8)
| r(X8)
| r(X9) ),
inference(cnf_transformation,[],[f4]) ).
fof(f22,plain,
! [X8,X9] :
( sP16(X9,X8)
| ~ r(X8)
| ~ r(X9) ),
inference(cnf_transformation,[],[f4]) ).
fof(f23,plain,
! [X8,X9] :
( ~ sP16(X9,X8)
| r(X8)
| ~ r(X9) ),
inference(cnf_transformation,[],[f4]) ).
fof(f24,plain,
! [X8,X9] :
( ~ sP16(X9,X8)
| ~ r(X8)
| r(X9) ),
inference(cnf_transformation,[],[f4]) ).
fof(f25,plain,
! [X11] :
( p(X11)
| ~ sP18 ),
inference(cnf_transformation,[],[f4]) ).
fof(f26,plain,
( ~ p(sK20)
| sP18 ),
inference(cnf_transformation,[],[f4]) ).
fof(f27,plain,
( s(sK19)
| ~ sP17 ),
inference(cnf_transformation,[],[f4]) ).
fof(f28,plain,
! [X10] :
( ~ s(X10)
| sP17 ),
inference(cnf_transformation,[],[f4]) ).
fof(f29,plain,
! [X6,X7,X5] :
( s(X7)
| ~ r(X6)
| ~ q(X5)
| q(sK9)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f30,plain,
! [X6,X7,X5] :
( s(X7)
| ~ r(X6)
| q(X5)
| ~ q(sK9)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f31,plain,
! [X5] :
( ~ s(sK13)
| r(sK12)
| ~ q(X5)
| q(sK9)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f32,plain,
! [X5] :
( ~ s(sK13)
| r(sK12)
| q(X5)
| ~ q(sK9)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f33,plain,
! [X6,X4] :
( ~ s(sK13)
| ~ r(X6)
| q(sK11(X4))
| q(X4)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f34,plain,
! [X6,X4] :
( ~ s(sK13)
| ~ r(X6)
| ~ q(sK11(X4))
| ~ q(X4)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f35,plain,
! [X7,X4] :
( s(X7)
| r(sK12)
| q(sK11(X4))
| q(X4)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f36,plain,
! [X7,X4] :
( s(X7)
| r(sK12)
| ~ q(sK11(X4))
| ~ q(X4)
| sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f37,plain,
! [X6,X5] :
( ~ s(sK13)
| ~ r(X6)
| ~ q(X5)
| q(sK9)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f38,plain,
! [X6,X5] :
( ~ s(sK13)
| ~ r(X6)
| q(X5)
| ~ q(sK9)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f39,plain,
! [X7,X5] :
( s(X7)
| r(sK12)
| ~ q(X5)
| q(sK9)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f40,plain,
! [X7,X5] :
( s(X7)
| r(sK12)
| q(X5)
| ~ q(sK9)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f41,plain,
! [X6,X7,X4] :
( s(X7)
| ~ r(X6)
| q(sK11(X4))
| q(X4)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f42,plain,
! [X6,X7,X4] :
( s(X7)
| ~ r(X6)
| ~ q(sK11(X4))
| ~ q(X4)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f43,plain,
! [X4] :
( ~ s(sK13)
| r(sK12)
| q(sK11(X4))
| q(X4)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f44,plain,
! [X4] :
( ~ s(sK13)
| r(sK12)
| ~ q(sK11(X4))
| ~ q(X4)
| ~ sP5 ),
inference(cnf_transformation,[],[f4]) ).
fof(f45,plain,
! [X9] :
( sP15
| sP18
| sP17
| sP16(X9,sK10)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f46,plain,
! [X9] :
( sP15
| ~ sP18
| ~ sP17
| sP16(X9,sK10)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f47,plain,
! [X9] :
( ~ sP15
| ~ sP18
| sP17
| sP16(X9,sK10)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f48,plain,
! [X9] :
( ~ sP15
| sP18
| ~ sP17
| sP16(X9,sK10)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f49,plain,
! [X8] :
( ~ sP15
| sP18
| sP17
| ~ sP16(sK14(X8),X8)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f50,plain,
! [X8] :
( ~ sP15
| ~ sP18
| ~ sP17
| ~ sP16(sK14(X8),X8)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f51,plain,
! [X8] :
( sP15
| ~ sP18
| sP17
| ~ sP16(sK14(X8),X8)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f52,plain,
! [X8] :
( sP15
| sP18
| ~ sP17
| ~ sP16(sK14(X8),X8)
| sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f53,plain,
! [X9] :
( ~ sP15
| sP18
| sP17
| sP16(X9,sK10)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f54,plain,
! [X9] :
( ~ sP15
| ~ sP18
| ~ sP17
| sP16(X9,sK10)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f55,plain,
! [X9] :
( sP15
| ~ sP18
| sP17
| sP16(X9,sK10)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f56,plain,
! [X9] :
( sP15
| sP18
| ~ sP17
| sP16(X9,sK10)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f57,plain,
! [X8] :
( sP15
| sP18
| sP17
| ~ sP16(sK14(X8),X8)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f58,plain,
! [X8] :
( sP15
| ~ sP18
| ~ sP17
| ~ sP16(sK14(X8),X8)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f59,plain,
! [X8] :
( ~ sP15
| ~ sP18
| sP17
| ~ sP16(sK14(X8),X8)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f60,plain,
! [X8] :
( ~ sP15
| sP18
| ~ sP17
| ~ sP16(sK14(X8),X8)
| ~ sP6 ),
inference(cnf_transformation,[],[f4]) ).
fof(f61,plain,
! [X0,X1] :
( sP2(X1,X0)
| p(X0)
| p(X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f62,plain,
! [X0,X1] :
( sP2(X1,X0)
| ~ p(X0)
| ~ p(X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f63,plain,
! [X0,X1] :
( ~ sP2(X1,X0)
| p(X0)
| ~ p(X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f64,plain,
! [X0,X1] :
( ~ sP2(X1,X0)
| ~ p(X0)
| p(X1) ),
inference(cnf_transformation,[],[f4]) ).
fof(f65,plain,
! [X3] :
( r(X3)
| ~ sP4 ),
inference(cnf_transformation,[],[f4]) ).
fof(f66,plain,
( ~ r(sK8)
| sP4 ),
inference(cnf_transformation,[],[f4]) ).
fof(f67,plain,
( q(sK7)
| ~ sP3 ),
inference(cnf_transformation,[],[f4]) ).
fof(f68,plain,
! [X2] :
( ~ q(X2)
| sP3 ),
inference(cnf_transformation,[],[f4]) ).
fof(f69,plain,
! [X0] :
( ~ sP6
| sP5
| sP4
| ~ sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f70,plain,
! [X0] :
( sP6
| ~ sP5
| sP4
| ~ sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f71,plain,
! [X0] :
( ~ sP6
| sP5
| ~ sP4
| sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f72,plain,
! [X0] :
( sP6
| ~ sP5
| ~ sP4
| sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f73,plain,
! [X0] :
( sP6
| sP5
| ~ sP4
| ~ sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f74,plain,
! [X0] :
( ~ sP6
| ~ sP5
| ~ sP4
| ~ sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f75,plain,
! [X0] :
( sP6
| sP5
| sP4
| sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f76,plain,
! [X0] :
( ~ sP6
| ~ sP5
| sP4
| sP3
| ~ sP2(sK1(X0),X0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f77,plain,
! [X1] :
( sP6
| sP5
| sP4
| ~ sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f78,plain,
! [X1] :
( ~ sP6
| ~ sP5
| sP4
| ~ sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f79,plain,
! [X1] :
( sP6
| sP5
| ~ sP4
| sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f80,plain,
! [X1] :
( ~ sP6
| ~ sP5
| ~ sP4
| sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f81,plain,
! [X1] :
( ~ sP6
| sP5
| ~ sP4
| ~ sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f82,plain,
! [X1] :
( sP6
| ~ sP5
| ~ sP4
| ~ sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f83,plain,
! [X1] :
( ~ sP6
| sP5
| sP4
| sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f84,plain,
! [X1] :
( sP6
| ~ sP5
| sP4
| sP3
| sP2(X1,sK0) ),
inference(cnf_transformation,[],[f4]) ).
fof(f86,definition,
( spl25_1
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl25_1])],[avatar_definition]) ).
fof(f90,definition,
( spl25_2
<=> s(sK21) ),
introduced(definition,[new_symbols(definition,[spl25_2])],[avatar_definition]) ).
fof(f91,plain,
( ~ s(sK21)
| spl25_2 ),
inference(avatar_component_clause,[],[f90]) ).
fof(f94,definition,
( spl25_3
<=> ! [X13] : ~ s(X13) ),
introduced(definition,[new_symbols(definition,[spl25_3])],[avatar_definition]) ).
fof(f95,plain,
( ! [X13] : ~ s(X13)
| ~ spl25_3 ),
inference(avatar_component_clause,[],[f94]) ).
fof(f97,definition,
( spl25_4
<=> ! [X14] : ~ p(X14) ),
introduced(definition,[new_symbols(definition,[spl25_4])],[avatar_definition]) ).
fof(f98,plain,
( ! [X14] : ~ p(X14)
| ~ spl25_4 ),
inference(avatar_component_clause,[],[f97]) ).
fof(f100,definition,
( spl25_5
<=> ! [X15] : q(X15) ),
introduced(definition,[new_symbols(definition,[spl25_5])],[avatar_definition]) ).
fof(f101,plain,
( ! [X15] : q(X15)
| ~ spl25_5 ),
inference(avatar_component_clause,[],[f100]) ).
fof(f102,plain,
( spl25_1
| spl25_2
| spl25_3
| spl25_4
| spl25_5 ),
inference(avatar_split_clause,[],[f5,f100,f97,f94,f90,f86]) ).
fof(f104,definition,
( spl25_6
<=> ! [X13] : s(X13) ),
introduced(definition,[new_symbols(definition,[spl25_6])],[avatar_definition]) ).
fof(f105,plain,
( ! [X13] : s(X13)
| ~ spl25_6 ),
inference(avatar_component_clause,[],[f104]) ).
fof(f106,plain,
( spl25_1
| ~ spl25_2
| spl25_6
| spl25_4
| spl25_5 ),
inference(avatar_split_clause,[],[f6,f100,f97,f104,f90,f86]) ).
fof(f108,definition,
( spl25_7
<=> p(sK23) ),
introduced(definition,[new_symbols(definition,[spl25_7])],[avatar_definition]) ).
fof(f110,plain,
( p(sK23)
| ~ spl25_7 ),
inference(avatar_component_clause,[],[f108]) ).
fof(f112,definition,
( spl25_8
<=> q(sK24) ),
introduced(definition,[new_symbols(definition,[spl25_8])],[avatar_definition]) ).
fof(f114,plain,
( ~ q(sK24)
| spl25_8 ),
inference(avatar_component_clause,[],[f112]) ).
fof(f115,plain,
( spl25_1
| spl25_2
| spl25_3
| spl25_7
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f7,f112,f108,f94,f90,f86]) ).
fof(f116,plain,
( spl25_1
| ~ spl25_2
| spl25_6
| spl25_7
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f8,f112,f108,f104,f90,f86]) ).
fof(f118,definition,
( spl25_9
<=> ! [X12] :
( s(sK22(X12))
| s(X12) ) ),
introduced(definition,[new_symbols(definition,[spl25_9])],[avatar_definition]) ).
fof(f119,plain,
( ! [X12] :
( s(sK22(X12))
| s(X12) )
| ~ spl25_9 ),
inference(avatar_component_clause,[],[f118]) ).
fof(f120,plain,
( spl25_1
| spl25_9
| spl25_4
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f9,f112,f97,f118,f86]) ).
fof(f122,definition,
( spl25_10
<=> ! [X12] :
( ~ s(sK22(X12))
| ~ s(X12) ) ),
introduced(definition,[new_symbols(definition,[spl25_10])],[avatar_definition]) ).
fof(f123,plain,
( ! [X12] :
( ~ s(sK22(X12))
| ~ s(X12) )
| ~ spl25_10 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f124,plain,
( spl25_1
| spl25_10
| spl25_4
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f10,f112,f97,f122,f86]) ).
fof(f125,plain,
( spl25_1
| spl25_9
| spl25_7
| spl25_5 ),
inference(avatar_split_clause,[],[f11,f100,f108,f118,f86]) ).
fof(f126,plain,
( spl25_1
| spl25_10
| spl25_7
| spl25_5 ),
inference(avatar_split_clause,[],[f12,f100,f108,f122,f86]) ).
fof(f127,plain,
( ~ spl25_1
| spl25_2
| spl25_3
| spl25_4
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f13,f112,f97,f94,f90,f86]) ).
fof(f128,plain,
( ~ spl25_1
| ~ spl25_2
| spl25_6
| spl25_4
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f14,f112,f97,f104,f90,f86]) ).
fof(f129,plain,
( ~ spl25_1
| spl25_2
| spl25_3
| spl25_7
| spl25_5 ),
inference(avatar_split_clause,[],[f15,f100,f108,f94,f90,f86]) ).
fof(f130,plain,
( ~ spl25_1
| ~ spl25_2
| spl25_6
| spl25_7
| spl25_5 ),
inference(avatar_split_clause,[],[f16,f100,f108,f104,f90,f86]) ).
fof(f131,plain,
( ~ spl25_1
| spl25_9
| spl25_4
| spl25_5 ),
inference(avatar_split_clause,[],[f17,f100,f97,f118,f86]) ).
fof(f132,plain,
( ~ spl25_1
| spl25_10
| spl25_4
| spl25_5 ),
inference(avatar_split_clause,[],[f18,f100,f97,f122,f86]) ).
fof(f133,plain,
( ~ spl25_1
| spl25_9
| spl25_7
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f19,f112,f108,f118,f86]) ).
fof(f134,plain,
( ~ spl25_1
| spl25_10
| spl25_7
| ~ spl25_8 ),
inference(avatar_split_clause,[],[f20,f112,f108,f122,f86]) ).
fof(f136,definition,
( spl25_11
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl25_11])],[avatar_definition]) ).
fof(f140,definition,
( spl25_12
<=> ! [X11] : p(X11) ),
introduced(definition,[new_symbols(definition,[spl25_12])],[avatar_definition]) ).
fof(f141,plain,
( ! [X11] : p(X11)
| ~ spl25_12 ),
inference(avatar_component_clause,[],[f140]) ).
fof(f142,plain,
( ~ spl25_11
| spl25_12 ),
inference(avatar_split_clause,[],[f25,f140,f136]) ).
fof(f144,definition,
( spl25_13
<=> p(sK20) ),
introduced(definition,[new_symbols(definition,[spl25_13])],[avatar_definition]) ).
fof(f146,plain,
( ~ p(sK20)
| spl25_13 ),
inference(avatar_component_clause,[],[f144]) ).
fof(f147,plain,
( spl25_11
| ~ spl25_13 ),
inference(avatar_split_clause,[],[f26,f144,f136]) ).
fof(f149,definition,
( spl25_14
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl25_14])],[avatar_definition]) ).
fof(f153,definition,
( spl25_15
<=> s(sK19) ),
introduced(definition,[new_symbols(definition,[spl25_15])],[avatar_definition]) ).
fof(f155,plain,
( s(sK19)
| ~ spl25_15 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f156,plain,
( ~ spl25_14
| spl25_15 ),
inference(avatar_split_clause,[],[f27,f153,f149]) ).
fof(f157,plain,
( spl25_14
| spl25_3 ),
inference(avatar_split_clause,[],[f28,f94,f149]) ).
fof(f159,definition,
( spl25_16
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl25_16])],[avatar_definition]) ).
fof(f163,definition,
( spl25_17
<=> q(sK9) ),
introduced(definition,[new_symbols(definition,[spl25_17])],[avatar_definition]) ).
fof(f167,definition,
( spl25_18
<=> ! [X5] : ~ q(X5) ),
introduced(definition,[new_symbols(definition,[spl25_18])],[avatar_definition]) ).
fof(f168,plain,
( ! [X5] : ~ q(X5)
| ~ spl25_18 ),
inference(avatar_component_clause,[],[f167]) ).
fof(f170,definition,
( spl25_19
<=> ! [X6] : ~ r(X6) ),
introduced(definition,[new_symbols(definition,[spl25_19])],[avatar_definition]) ).
fof(f171,plain,
( ! [X6] : ~ r(X6)
| ~ spl25_19 ),
inference(avatar_component_clause,[],[f170]) ).
fof(f172,plain,
( spl25_16
| spl25_17
| spl25_18
| spl25_19
| spl25_6 ),
inference(avatar_split_clause,[],[f29,f104,f170,f167,f163,f159]) ).
fof(f173,plain,
( spl25_16
| ~ spl25_17
| spl25_5
| spl25_19
| spl25_6 ),
inference(avatar_split_clause,[],[f30,f104,f170,f100,f163,f159]) ).
fof(f175,definition,
( spl25_20
<=> r(sK12) ),
introduced(definition,[new_symbols(definition,[spl25_20])],[avatar_definition]) ).
fof(f177,plain,
( r(sK12)
| ~ spl25_20 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f179,definition,
( spl25_21
<=> s(sK13) ),
introduced(definition,[new_symbols(definition,[spl25_21])],[avatar_definition]) ).
fof(f181,plain,
( ~ s(sK13)
| spl25_21 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f182,plain,
( spl25_16
| spl25_17
| spl25_18
| spl25_20
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f31,f179,f175,f167,f163,f159]) ).
fof(f183,plain,
( spl25_16
| ~ spl25_17
| spl25_5
| spl25_20
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f32,f179,f175,f100,f163,f159]) ).
fof(f185,definition,
( spl25_22
<=> ! [X4] :
( q(sK11(X4))
| q(X4) ) ),
introduced(definition,[new_symbols(definition,[spl25_22])],[avatar_definition]) ).
fof(f186,plain,
( ! [X4] :
( q(sK11(X4))
| q(X4) )
| ~ spl25_22 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f187,plain,
( spl25_16
| spl25_22
| spl25_19
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f33,f179,f170,f185,f159]) ).
fof(f189,definition,
( spl25_23
<=> ! [X4] :
( ~ q(sK11(X4))
| ~ q(X4) ) ),
introduced(definition,[new_symbols(definition,[spl25_23])],[avatar_definition]) ).
fof(f190,plain,
( ! [X4] :
( ~ q(sK11(X4))
| ~ q(X4) )
| ~ spl25_23 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f191,plain,
( spl25_16
| spl25_23
| spl25_19
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f34,f179,f170,f189,f159]) ).
fof(f192,plain,
( spl25_16
| spl25_22
| spl25_20
| spl25_6 ),
inference(avatar_split_clause,[],[f35,f104,f175,f185,f159]) ).
fof(f193,plain,
( spl25_16
| spl25_23
| spl25_20
| spl25_6 ),
inference(avatar_split_clause,[],[f36,f104,f175,f189,f159]) ).
fof(f194,plain,
( ~ spl25_16
| spl25_17
| spl25_18
| spl25_19
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f37,f179,f170,f167,f163,f159]) ).
fof(f195,plain,
( ~ spl25_16
| ~ spl25_17
| spl25_5
| spl25_19
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f38,f179,f170,f100,f163,f159]) ).
fof(f196,plain,
( ~ spl25_16
| spl25_17
| spl25_18
| spl25_20
| spl25_6 ),
inference(avatar_split_clause,[],[f39,f104,f175,f167,f163,f159]) ).
fof(f197,plain,
( ~ spl25_16
| ~ spl25_17
| spl25_5
| spl25_20
| spl25_6 ),
inference(avatar_split_clause,[],[f40,f104,f175,f100,f163,f159]) ).
fof(f198,plain,
( ~ spl25_16
| spl25_22
| spl25_19
| spl25_6 ),
inference(avatar_split_clause,[],[f41,f104,f170,f185,f159]) ).
fof(f199,plain,
( ~ spl25_16
| spl25_23
| spl25_19
| spl25_6 ),
inference(avatar_split_clause,[],[f42,f104,f170,f189,f159]) ).
fof(f200,plain,
( ~ spl25_16
| spl25_22
| spl25_20
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f43,f179,f175,f185,f159]) ).
fof(f201,plain,
( ~ spl25_16
| spl25_23
| spl25_20
| ~ spl25_21 ),
inference(avatar_split_clause,[],[f44,f179,f175,f189,f159]) ).
fof(f203,definition,
( spl25_24
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl25_24])],[avatar_definition]) ).
fof(f207,definition,
( spl25_25
<=> ! [X9] : sP16(X9,sK10) ),
introduced(definition,[new_symbols(definition,[spl25_25])],[avatar_definition]) ).
fof(f208,plain,
( ! [X9] : sP16(X9,sK10)
| ~ spl25_25 ),
inference(avatar_component_clause,[],[f207]) ).
fof(f209,plain,
( spl25_24
| spl25_25
| spl25_14
| spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f45,f86,f136,f149,f207,f203]) ).
fof(f210,plain,
( spl25_24
| spl25_25
| ~ spl25_14
| ~ spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f46,f86,f136,f149,f207,f203]) ).
fof(f211,plain,
( spl25_24
| spl25_25
| spl25_14
| ~ spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f47,f86,f136,f149,f207,f203]) ).
fof(f212,plain,
( spl25_24
| spl25_25
| ~ spl25_14
| spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f48,f86,f136,f149,f207,f203]) ).
fof(f214,definition,
( spl25_26
<=> ! [X8] : ~ sP16(sK14(X8),X8) ),
introduced(definition,[new_symbols(definition,[spl25_26])],[avatar_definition]) ).
fof(f215,plain,
( ! [X8] : ~ sP16(sK14(X8),X8)
| ~ spl25_26 ),
inference(avatar_component_clause,[],[f214]) ).
fof(f216,plain,
( spl25_24
| spl25_26
| spl25_14
| spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f49,f86,f136,f149,f214,f203]) ).
fof(f217,plain,
( spl25_24
| spl25_26
| ~ spl25_14
| ~ spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f50,f86,f136,f149,f214,f203]) ).
fof(f218,plain,
( spl25_24
| spl25_26
| spl25_14
| ~ spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f51,f86,f136,f149,f214,f203]) ).
fof(f219,plain,
( spl25_24
| spl25_26
| ~ spl25_14
| spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f52,f86,f136,f149,f214,f203]) ).
fof(f220,plain,
( ~ spl25_24
| spl25_25
| spl25_14
| spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f53,f86,f136,f149,f207,f203]) ).
fof(f221,plain,
( ~ spl25_24
| spl25_25
| ~ spl25_14
| ~ spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f54,f86,f136,f149,f207,f203]) ).
fof(f222,plain,
( ~ spl25_24
| spl25_25
| spl25_14
| ~ spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f55,f86,f136,f149,f207,f203]) ).
fof(f223,plain,
( ~ spl25_24
| spl25_25
| ~ spl25_14
| spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f56,f86,f136,f149,f207,f203]) ).
fof(f224,plain,
( ~ spl25_24
| spl25_26
| spl25_14
| spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f57,f86,f136,f149,f214,f203]) ).
fof(f225,plain,
( ~ spl25_24
| spl25_26
| ~ spl25_14
| ~ spl25_11
| spl25_1 ),
inference(avatar_split_clause,[],[f58,f86,f136,f149,f214,f203]) ).
fof(f226,plain,
( ~ spl25_24
| spl25_26
| spl25_14
| ~ spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f59,f86,f136,f149,f214,f203]) ).
fof(f227,plain,
( ~ spl25_24
| spl25_26
| ~ spl25_14
| spl25_11
| ~ spl25_1 ),
inference(avatar_split_clause,[],[f60,f86,f136,f149,f214,f203]) ).
fof(f229,definition,
( spl25_27
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl25_27])],[avatar_definition]) ).
fof(f233,definition,
( spl25_28
<=> ! [X3] : r(X3) ),
introduced(definition,[new_symbols(definition,[spl25_28])],[avatar_definition]) ).
fof(f234,plain,
( ! [X3] : r(X3)
| ~ spl25_28 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f235,plain,
( ~ spl25_27
| spl25_28 ),
inference(avatar_split_clause,[],[f65,f233,f229]) ).
fof(f237,definition,
( spl25_29
<=> r(sK8) ),
introduced(definition,[new_symbols(definition,[spl25_29])],[avatar_definition]) ).
fof(f239,plain,
( ~ r(sK8)
| spl25_29 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f240,plain,
( spl25_27
| ~ spl25_29 ),
inference(avatar_split_clause,[],[f66,f237,f229]) ).
fof(f242,definition,
( spl25_30
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl25_30])],[avatar_definition]) ).
fof(f246,definition,
( spl25_31
<=> q(sK7) ),
introduced(definition,[new_symbols(definition,[spl25_31])],[avatar_definition]) ).
fof(f248,plain,
( q(sK7)
| ~ spl25_31 ),
inference(avatar_component_clause,[],[f246]) ).
fof(f249,plain,
( ~ spl25_30
| spl25_31 ),
inference(avatar_split_clause,[],[f67,f246,f242]) ).
fof(f250,plain,
( spl25_30
| spl25_18 ),
inference(avatar_split_clause,[],[f68,f167,f242]) ).
fof(f252,definition,
( spl25_32
<=> ! [X0] : ~ sP2(sK1(X0),X0) ),
introduced(definition,[new_symbols(definition,[spl25_32])],[avatar_definition]) ).
fof(f253,plain,
( ! [X0] : ~ sP2(sK1(X0),X0)
| ~ spl25_32 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f254,plain,
( spl25_32
| ~ spl25_30
| spl25_27
| spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f69,f203,f159,f229,f242,f252]) ).
fof(f255,plain,
( spl25_32
| ~ spl25_30
| spl25_27
| ~ spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f70,f203,f159,f229,f242,f252]) ).
fof(f256,plain,
( spl25_32
| spl25_30
| ~ spl25_27
| spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f71,f203,f159,f229,f242,f252]) ).
fof(f257,plain,
( spl25_32
| spl25_30
| ~ spl25_27
| ~ spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f72,f203,f159,f229,f242,f252]) ).
fof(f258,plain,
( spl25_32
| ~ spl25_30
| ~ spl25_27
| spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f73,f203,f159,f229,f242,f252]) ).
fof(f259,plain,
( spl25_32
| ~ spl25_30
| ~ spl25_27
| ~ spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f74,f203,f159,f229,f242,f252]) ).
fof(f260,plain,
( spl25_32
| spl25_30
| spl25_27
| spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f75,f203,f159,f229,f242,f252]) ).
fof(f261,plain,
( spl25_32
| spl25_30
| spl25_27
| ~ spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f76,f203,f159,f229,f242,f252]) ).
fof(f263,definition,
( spl25_33
<=> ! [X1] : sP2(X1,sK0) ),
introduced(definition,[new_symbols(definition,[spl25_33])],[avatar_definition]) ).
fof(f264,plain,
( ! [X1] : sP2(X1,sK0)
| ~ spl25_33 ),
inference(avatar_component_clause,[],[f263]) ).
fof(f265,plain,
( spl25_33
| ~ spl25_30
| spl25_27
| spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f77,f203,f159,f229,f242,f263]) ).
fof(f266,plain,
( spl25_33
| ~ spl25_30
| spl25_27
| ~ spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f78,f203,f159,f229,f242,f263]) ).
fof(f267,plain,
( spl25_33
| spl25_30
| ~ spl25_27
| spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f79,f203,f159,f229,f242,f263]) ).
fof(f268,plain,
( spl25_33
| spl25_30
| ~ spl25_27
| ~ spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f80,f203,f159,f229,f242,f263]) ).
fof(f269,plain,
( spl25_33
| ~ spl25_30
| ~ spl25_27
| spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f81,f203,f159,f229,f242,f263]) ).
fof(f270,plain,
( spl25_33
| ~ spl25_30
| ~ spl25_27
| ~ spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f82,f203,f159,f229,f242,f263]) ).
fof(f271,plain,
( spl25_33
| spl25_30
| spl25_27
| spl25_16
| ~ spl25_24 ),
inference(avatar_split_clause,[],[f83,f203,f159,f229,f242,f263]) ).
fof(f272,plain,
( spl25_33
| spl25_30
| spl25_27
| ~ spl25_16
| spl25_24 ),
inference(avatar_split_clause,[],[f84,f203,f159,f229,f242,f263]) ).
fof(f273,plain,
( $false
| ~ spl25_5
| spl25_8 ),
inference(forward_subsumption_resolution,[],[f114,f101]) ).
fof(f274,plain,
( ~ spl25_5
| spl25_8 ),
inference(avatar_contradiction_clause,[],[f273]) ).
fof(f275,plain,
( $false
| ~ spl25_5
| ~ spl25_18 ),
inference(forward_subsumption_resolution,[],[f168,f101]) ).
fof(f276,plain,
( ~ spl25_5
| ~ spl25_18 ),
inference(avatar_contradiction_clause,[],[f275]) ).
fof(f277,plain,
( ! [X4] : ~ q(X4)
| ~ spl25_5
| ~ spl25_23 ),
inference(forward_subsumption_resolution,[],[f190,f101]) ).
fof(f278,plain,
( $false
| ~ spl25_5
| ~ spl25_23 ),
inference(forward_subsumption_resolution,[],[f277,f101]) ).
fof(f279,plain,
( ~ spl25_5
| ~ spl25_23 ),
inference(avatar_contradiction_clause,[],[f278]) ).
fof(f280,plain,
( ! [X0] :
( r(sK10)
| ~ r(X0) )
| ~ spl25_25 ),
inference(resolution,[],[f23,f208]) ).
fof(f285,plain,
( ! [X0] :
( ~ r(sK10)
| r(X0) )
| ~ spl25_25 ),
inference(resolution,[],[f24,f208]) ).
fof(f290,plain,
( ! [X0] :
( p(sK1(X0))
| p(X0) )
| ~ spl25_32 ),
inference(resolution,[],[f61,f253]) ).
fof(f291,plain,
( ! [X0] : p(sK1(X0))
| ~ spl25_4
| ~ spl25_32 ),
inference(forward_subsumption_resolution,[],[f290,f98]) ).
fof(f292,plain,
( $false
| ~ spl25_4
| ~ spl25_32 ),
inference(forward_subsumption_resolution,[],[f291,f98]) ).
fof(f293,plain,
( ~ spl25_4
| ~ spl25_32 ),
inference(avatar_contradiction_clause,[],[f292]) ).
fof(f294,plain,
( $false
| ~ spl25_19
| ~ spl25_20 ),
inference(forward_subsumption_resolution,[],[f177,f171]) ).
fof(f295,plain,
( ~ spl25_19
| ~ spl25_20 ),
inference(avatar_contradiction_clause,[],[f294]) ).
fof(f296,plain,
( $false
| ~ spl25_3
| ~ spl25_6 ),
inference(forward_subsumption_resolution,[],[f105,f95]) ).
fof(f297,plain,
( ~ spl25_3
| ~ spl25_6 ),
inference(avatar_contradiction_clause,[],[f296]) ).
fof(f299,definition,
( spl25_34
<=> r(sK10) ),
introduced(definition,[new_symbols(definition,[spl25_34])],[avatar_definition]) ).
fof(f302,plain,
( spl25_19
| spl25_34
| ~ spl25_25 ),
inference(avatar_split_clause,[],[f280,f207,f299,f170]) ).
fof(f303,plain,
( spl25_28
| ~ spl25_34
| ~ spl25_25 ),
inference(avatar_split_clause,[],[f285,f207,f299,f233]) ).
fof(f304,plain,
( $false
| ~ spl25_18
| ~ spl25_31 ),
inference(resolution,[],[f248,f168]) ).
fof(f305,plain,
( ~ spl25_18
| ~ spl25_31 ),
inference(avatar_contradiction_clause,[],[f304]) ).
fof(f306,plain,
( ! [X12] : s(X12)
| ~ spl25_3
| ~ spl25_9 ),
inference(forward_subsumption_resolution,[],[f119,f95]) ).
fof(f307,plain,
( $false
| ~ spl25_3
| ~ spl25_9 ),
inference(forward_subsumption_resolution,[],[f306,f95]) ).
fof(f308,plain,
( ~ spl25_3
| ~ spl25_9 ),
inference(avatar_contradiction_clause,[],[f307]) ).
fof(f309,plain,
( $false
| ~ spl25_28
| spl25_29 ),
inference(resolution,[],[f234,f239]) ).
fof(f310,plain,
( ~ spl25_28
| spl25_29 ),
inference(avatar_contradiction_clause,[],[f309]) ).
fof(f313,plain,
( ! [X0] :
( r(X0)
| r(sK14(X0)) )
| ~ spl25_26 ),
inference(resolution,[],[f215,f21]) ).
fof(f315,plain,
( ! [X0] : r(X0)
| ~ spl25_19
| ~ spl25_26 ),
inference(forward_subsumption_resolution,[],[f313,f171]) ).
fof(f316,plain,
( $false
| ~ spl25_19
| ~ spl25_26 ),
inference(forward_subsumption_resolution,[],[f315,f171]) ).
fof(f317,plain,
( ~ spl25_19
| ~ spl25_26 ),
inference(avatar_contradiction_clause,[],[f316]) ).
fof(f318,plain,
( $false
| spl25_2
| ~ spl25_6 ),
inference(resolution,[],[f105,f91]) ).
fof(f319,plain,
( $false
| ~ spl25_6
| spl25_21 ),
inference(resolution,[],[f105,f181]) ).
fof(f320,plain,
( ~ spl25_6
| spl25_21 ),
inference(avatar_contradiction_clause,[],[f319]) ).
fof(f321,plain,
( spl25_2
| ~ spl25_6 ),
inference(avatar_contradiction_clause,[],[f318]) ).
fof(f323,plain,
( ! [X0] : ~ s(X0)
| ~ spl25_6
| ~ spl25_10 ),
inference(resolution,[],[f123,f105]) ).
fof(f324,plain,
( $false
| ~ spl25_6
| ~ spl25_10 ),
inference(forward_subsumption_resolution,[],[f323,f105]) ).
fof(f325,plain,
( ~ spl25_6
| ~ spl25_10 ),
inference(avatar_contradiction_clause,[],[f324]) ).
fof(f326,plain,
( $false
| ~ spl25_3
| ~ spl25_15 ),
inference(resolution,[],[f95,f155]) ).
fof(f327,plain,
( ~ spl25_3
| ~ spl25_15 ),
inference(avatar_contradiction_clause,[],[f326]) ).
fof(f328,plain,
( $false
| ~ spl25_12
| spl25_13 ),
inference(resolution,[],[f141,f146]) ).
fof(f329,plain,
( ~ spl25_12
| spl25_13 ),
inference(avatar_contradiction_clause,[],[f328]) ).
fof(f331,plain,
( ! [X0] :
( ~ p(X0)
| ~ p(sK1(X0)) )
| ~ spl25_32 ),
inference(resolution,[],[f62,f253]) ).
fof(f332,plain,
( ! [X0] : ~ p(sK1(X0))
| ~ spl25_12
| ~ spl25_32 ),
inference(forward_subsumption_resolution,[],[f331,f141]) ).
fof(f333,plain,
( $false
| ~ spl25_12
| ~ spl25_32 ),
inference(forward_subsumption_resolution,[],[f332,f141]) ).
fof(f334,plain,
( ~ spl25_12
| ~ spl25_32 ),
inference(avatar_contradiction_clause,[],[f333]) ).
fof(f335,plain,
( $false
| ~ spl25_19
| ~ spl25_28 ),
inference(forward_subsumption_resolution,[],[f234,f171]) ).
fof(f336,plain,
( ~ spl25_19
| ~ spl25_28 ),
inference(avatar_contradiction_clause,[],[f335]) ).
fof(f339,plain,
( ! [X0] : q(X0)
| ~ spl25_18
| ~ spl25_22 ),
inference(resolution,[],[f168,f186]) ).
fof(f340,plain,
( $false
| ~ spl25_18
| ~ spl25_22 ),
inference(forward_subsumption_resolution,[],[f339,f168]) ).
fof(f341,plain,
( ~ spl25_18
| ~ spl25_22 ),
inference(avatar_contradiction_clause,[],[f340]) ).
fof(f344,plain,
( $false
| ~ spl25_32
| ~ spl25_33 ),
inference(resolution,[],[f264,f253]) ).
fof(f345,plain,
( ~ spl25_32
| ~ spl25_33 ),
inference(avatar_contradiction_clause,[],[f344]) ).
fof(f348,plain,
( ! [X0] :
( p(sK0)
| ~ p(X0) )
| ~ spl25_33 ),
inference(resolution,[],[f63,f264]) ).
fof(f352,definition,
( spl25_35
<=> p(sK0) ),
introduced(definition,[new_symbols(definition,[spl25_35])],[avatar_definition]) ).
fof(f354,plain,
( p(sK0)
| ~ spl25_35 ),
inference(avatar_component_clause,[],[f352]) ).
fof(f355,plain,
( spl25_4
| spl25_35
| ~ spl25_33 ),
inference(avatar_split_clause,[],[f348,f263,f352,f97]) ).
fof(f358,plain,
( ! [X0] :
( ~ p(sK0)
| p(X0) )
| ~ spl25_33 ),
inference(resolution,[],[f64,f264]) ).
fof(f361,plain,
( ! [X0] : p(X0)
| ~ spl25_33
| ~ spl25_35 ),
inference(forward_subsumption_resolution,[],[f358,f354]) ).
fof(f362,plain,
( spl25_12
| ~ spl25_33
| ~ spl25_35 ),
inference(avatar_split_clause,[],[f361,f352,f263,f140]) ).
fof(f363,plain,
( $false
| ~ spl25_4
| ~ spl25_12 ),
inference(forward_subsumption_resolution,[],[f141,f98]) ).
fof(f364,plain,
( ~ spl25_4
| ~ spl25_12 ),
inference(avatar_contradiction_clause,[],[f363]) ).
fof(f367,plain,
( $false
| ~ spl25_4
| ~ spl25_7 ),
inference(resolution,[],[f98,f110]) ).
fof(f368,plain,
( ~ spl25_4
| ~ spl25_7 ),
inference(avatar_contradiction_clause,[],[f367]) ).
fof(f371,plain,
( ! [X0] :
( ~ r(X0)
| ~ r(sK14(X0)) )
| ~ spl25_26 ),
inference(resolution,[],[f215,f22]) ).
fof(f373,plain,
( ! [X0] : ~ r(sK14(X0))
| ~ spl25_26
| ~ spl25_28 ),
inference(forward_subsumption_resolution,[],[f371,f234]) ).
fof(f374,plain,
( $false
| ~ spl25_26
| ~ spl25_28 ),
inference(forward_subsumption_resolution,[],[f373,f234]) ).
fof(f375,plain,
( ~ spl25_26
| ~ spl25_28 ),
inference(avatar_contradiction_clause,[],[f374]) ).
cnf(s1,plain,
( spl25_1
| spl25_2
| spl25_3
| spl25_4
| spl25_5 ),
inference(sat_conversion,[],[f102]) ).
cnf(s2,plain,
( spl25_1
| ~ spl25_2
| spl25_4
| spl25_5
| spl25_6 ),
inference(sat_conversion,[],[f106]) ).
cnf(s3,plain,
( spl25_1
| spl25_2
| spl25_3
| spl25_7
| ~ spl25_8 ),
inference(sat_conversion,[],[f115]) ).
cnf(s4,plain,
( spl25_1
| ~ spl25_2
| spl25_6
| spl25_7
| ~ spl25_8 ),
inference(sat_conversion,[],[f116]) ).
cnf(s5,plain,
( spl25_1
| spl25_4
| ~ spl25_8
| spl25_9 ),
inference(sat_conversion,[],[f120]) ).
cnf(s6,plain,
( spl25_1
| spl25_4
| ~ spl25_8
| spl25_10 ),
inference(sat_conversion,[],[f124]) ).
cnf(s7,plain,
( spl25_1
| spl25_5
| spl25_7
| spl25_9 ),
inference(sat_conversion,[],[f125]) ).
cnf(s8,plain,
( spl25_1
| spl25_5
| spl25_7
| spl25_10 ),
inference(sat_conversion,[],[f126]) ).
cnf(s9,plain,
( ~ spl25_1
| spl25_2
| spl25_3
| spl25_4
| ~ spl25_8 ),
inference(sat_conversion,[],[f127]) ).
cnf(s10,plain,
( ~ spl25_1
| ~ spl25_2
| spl25_4
| spl25_6
| ~ spl25_8 ),
inference(sat_conversion,[],[f128]) ).
cnf(s11,plain,
( ~ spl25_1
| spl25_2
| spl25_3
| spl25_5
| spl25_7 ),
inference(sat_conversion,[],[f129]) ).
cnf(s12,plain,
( ~ spl25_1
| ~ spl25_2
| spl25_5
| spl25_6
| spl25_7 ),
inference(sat_conversion,[],[f130]) ).
cnf(s13,plain,
( ~ spl25_1
| spl25_4
| spl25_5
| spl25_9 ),
inference(sat_conversion,[],[f131]) ).
cnf(s14,plain,
( ~ spl25_1
| spl25_4
| spl25_5
| spl25_10 ),
inference(sat_conversion,[],[f132]) ).
cnf(s15,plain,
( ~ spl25_1
| spl25_7
| ~ spl25_8
| spl25_9 ),
inference(sat_conversion,[],[f133]) ).
cnf(s16,plain,
( ~ spl25_1
| spl25_7
| ~ spl25_8
| spl25_10 ),
inference(sat_conversion,[],[f134]) ).
cnf(s17,plain,
( ~ spl25_11
| spl25_12 ),
inference(sat_conversion,[],[f142]) ).
cnf(s18,plain,
( spl25_11
| ~ spl25_13 ),
inference(sat_conversion,[],[f147]) ).
cnf(s19,plain,
( ~ spl25_14
| spl25_15 ),
inference(sat_conversion,[],[f156]) ).
cnf(s20,plain,
( spl25_3
| spl25_14 ),
inference(sat_conversion,[],[f157]) ).
cnf(s21,plain,
( spl25_6
| spl25_16
| spl25_17
| spl25_18
| spl25_19 ),
inference(sat_conversion,[],[f172]) ).
cnf(s22,plain,
( spl25_5
| spl25_6
| spl25_16
| ~ spl25_17
| spl25_19 ),
inference(sat_conversion,[],[f173]) ).
cnf(s23,plain,
( spl25_16
| spl25_17
| spl25_18
| spl25_20
| ~ spl25_21 ),
inference(sat_conversion,[],[f182]) ).
cnf(s24,plain,
( spl25_5
| spl25_16
| ~ spl25_17
| spl25_20
| ~ spl25_21 ),
inference(sat_conversion,[],[f183]) ).
cnf(s25,plain,
( spl25_16
| spl25_19
| ~ spl25_21
| spl25_22 ),
inference(sat_conversion,[],[f187]) ).
cnf(s26,plain,
( spl25_16
| spl25_19
| ~ spl25_21
| spl25_23 ),
inference(sat_conversion,[],[f191]) ).
cnf(s27,plain,
( spl25_6
| spl25_16
| spl25_20
| spl25_22 ),
inference(sat_conversion,[],[f192]) ).
cnf(s28,plain,
( spl25_6
| spl25_16
| spl25_20
| spl25_23 ),
inference(sat_conversion,[],[f193]) ).
cnf(s29,plain,
( ~ spl25_16
| spl25_17
| spl25_18
| spl25_19
| ~ spl25_21 ),
inference(sat_conversion,[],[f194]) ).
cnf(s30,plain,
( spl25_5
| ~ spl25_16
| ~ spl25_17
| spl25_19
| ~ spl25_21 ),
inference(sat_conversion,[],[f195]) ).
cnf(s31,plain,
( spl25_6
| ~ spl25_16
| spl25_17
| spl25_18
| spl25_20 ),
inference(sat_conversion,[],[f196]) ).
cnf(s32,plain,
( spl25_5
| spl25_6
| ~ spl25_16
| ~ spl25_17
| spl25_20 ),
inference(sat_conversion,[],[f197]) ).
cnf(s33,plain,
( spl25_6
| ~ spl25_16
| spl25_19
| spl25_22 ),
inference(sat_conversion,[],[f198]) ).
cnf(s34,plain,
( spl25_6
| ~ spl25_16
| spl25_19
| spl25_23 ),
inference(sat_conversion,[],[f199]) ).
cnf(s35,plain,
( ~ spl25_16
| spl25_20
| ~ spl25_21
| spl25_22 ),
inference(sat_conversion,[],[f200]) ).
cnf(s36,plain,
( ~ spl25_16
| spl25_20
| ~ spl25_21
| spl25_23 ),
inference(sat_conversion,[],[f201]) ).
cnf(s37,plain,
( spl25_1
| spl25_11
| spl25_14
| spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f209]) ).
cnf(s38,plain,
( spl25_1
| ~ spl25_11
| ~ spl25_14
| spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f210]) ).
cnf(s39,plain,
( ~ spl25_1
| ~ spl25_11
| spl25_14
| spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f211]) ).
cnf(s40,plain,
( ~ spl25_1
| spl25_11
| ~ spl25_14
| spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f212]) ).
cnf(s41,plain,
( ~ spl25_1
| spl25_11
| spl25_14
| spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f216]) ).
cnf(s42,plain,
( ~ spl25_1
| ~ spl25_11
| ~ spl25_14
| spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f217]) ).
cnf(s43,plain,
( spl25_1
| ~ spl25_11
| spl25_14
| spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f218]) ).
cnf(s44,plain,
( spl25_1
| spl25_11
| ~ spl25_14
| spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f219]) ).
cnf(s45,plain,
( ~ spl25_1
| spl25_11
| spl25_14
| ~ spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f220]) ).
cnf(s46,plain,
( ~ spl25_1
| ~ spl25_11
| ~ spl25_14
| ~ spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f221]) ).
cnf(s47,plain,
( spl25_1
| ~ spl25_11
| spl25_14
| ~ spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f222]) ).
cnf(s48,plain,
( spl25_1
| spl25_11
| ~ spl25_14
| ~ spl25_24
| spl25_25 ),
inference(sat_conversion,[],[f223]) ).
cnf(s49,plain,
( spl25_1
| spl25_11
| spl25_14
| ~ spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f224]) ).
cnf(s50,plain,
( spl25_1
| ~ spl25_11
| ~ spl25_14
| ~ spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f225]) ).
cnf(s51,plain,
( ~ spl25_1
| ~ spl25_11
| spl25_14
| ~ spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f226]) ).
cnf(s52,plain,
( ~ spl25_1
| spl25_11
| ~ spl25_14
| ~ spl25_24
| spl25_26 ),
inference(sat_conversion,[],[f227]) ).
cnf(s53,plain,
( ~ spl25_27
| spl25_28 ),
inference(sat_conversion,[],[f235]) ).
cnf(s54,plain,
( spl25_27
| ~ spl25_29 ),
inference(sat_conversion,[],[f240]) ).
cnf(s55,plain,
( ~ spl25_30
| spl25_31 ),
inference(sat_conversion,[],[f249]) ).
cnf(s56,plain,
( spl25_18
| spl25_30 ),
inference(sat_conversion,[],[f250]) ).
cnf(s57,plain,
( spl25_16
| ~ spl25_24
| spl25_27
| ~ spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f254]) ).
cnf(s58,plain,
( ~ spl25_16
| spl25_24
| spl25_27
| ~ spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f255]) ).
cnf(s59,plain,
( spl25_16
| ~ spl25_24
| ~ spl25_27
| spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f256]) ).
cnf(s60,plain,
( ~ spl25_16
| spl25_24
| ~ spl25_27
| spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f257]) ).
cnf(s61,plain,
( spl25_16
| spl25_24
| ~ spl25_27
| ~ spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f258]) ).
cnf(s62,plain,
( ~ spl25_16
| ~ spl25_24
| ~ spl25_27
| ~ spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f259]) ).
cnf(s63,plain,
( spl25_16
| spl25_24
| spl25_27
| spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f260]) ).
cnf(s64,plain,
( ~ spl25_16
| ~ spl25_24
| spl25_27
| spl25_30
| spl25_32 ),
inference(sat_conversion,[],[f261]) ).
cnf(s65,plain,
( spl25_16
| spl25_24
| spl25_27
| ~ spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f265]) ).
cnf(s66,plain,
( ~ spl25_16
| ~ spl25_24
| spl25_27
| ~ spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f266]) ).
cnf(s67,plain,
( spl25_16
| spl25_24
| ~ spl25_27
| spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f267]) ).
cnf(s68,plain,
( ~ spl25_16
| ~ spl25_24
| ~ spl25_27
| spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f268]) ).
cnf(s69,plain,
( spl25_16
| ~ spl25_24
| ~ spl25_27
| ~ spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f269]) ).
cnf(s70,plain,
( ~ spl25_16
| spl25_24
| ~ spl25_27
| ~ spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f270]) ).
cnf(s71,plain,
( spl25_16
| ~ spl25_24
| spl25_27
| spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f271]) ).
cnf(s72,plain,
( ~ spl25_16
| spl25_24
| spl25_27
| spl25_30
| spl25_33 ),
inference(sat_conversion,[],[f272]) ).
cnf(s73,plain,
( ~ spl25_5
| spl25_8 ),
inference(sat_conversion,[],[f274]) ).
cnf(s74,plain,
( ~ spl25_5
| ~ spl25_18 ),
inference(sat_conversion,[],[f276]) ).
cnf(s75,plain,
( ~ spl25_5
| ~ spl25_23 ),
inference(sat_conversion,[],[f279]) ).
cnf(s76,plain,
( ~ spl25_4
| ~ spl25_32 ),
inference(sat_conversion,[],[f293]) ).
cnf(s77,plain,
( ~ spl25_19
| ~ spl25_20 ),
inference(sat_conversion,[],[f295]) ).
cnf(s78,plain,
( ~ spl25_3
| ~ spl25_6 ),
inference(sat_conversion,[],[f297]) ).
cnf(s79,plain,
( spl25_19
| ~ spl25_25
| spl25_34 ),
inference(sat_conversion,[],[f302]) ).
cnf(s80,plain,
( ~ spl25_25
| spl25_28
| ~ spl25_34 ),
inference(sat_conversion,[],[f303]) ).
cnf(s81,plain,
( ~ spl25_18
| ~ spl25_31 ),
inference(sat_conversion,[],[f305]) ).
cnf(s82,plain,
( ~ spl25_3
| ~ spl25_9 ),
inference(sat_conversion,[],[f308]) ).
cnf(s83,plain,
( ~ spl25_28
| spl25_29 ),
inference(sat_conversion,[],[f310]) ).
cnf(s85,plain,
( ~ spl25_19
| ~ spl25_26 ),
inference(sat_conversion,[],[f317]) ).
cnf(s86,plain,
( ~ spl25_6
| spl25_21 ),
inference(sat_conversion,[],[f320]) ).
cnf(s87,plain,
( spl25_2
| ~ spl25_6 ),
inference(sat_conversion,[],[f321]) ).
cnf(s88,plain,
( ~ spl25_6
| ~ spl25_10 ),
inference(sat_conversion,[],[f325]) ).
cnf(s89,plain,
( ~ spl25_3
| ~ spl25_15 ),
inference(sat_conversion,[],[f327]) ).
cnf(s90,plain,
( ~ spl25_12
| spl25_13 ),
inference(sat_conversion,[],[f329]) ).
cnf(s91,plain,
( ~ spl25_12
| ~ spl25_32 ),
inference(sat_conversion,[],[f334]) ).
cnf(s92,plain,
( ~ spl25_19
| ~ spl25_28 ),
inference(sat_conversion,[],[f336]) ).
cnf(s94,plain,
( ~ spl25_18
| ~ spl25_22 ),
inference(sat_conversion,[],[f341]) ).
cnf(s95,plain,
( ~ spl25_32
| ~ spl25_33 ),
inference(sat_conversion,[],[f345]) ).
cnf(s96,plain,
( spl25_4
| ~ spl25_33
| spl25_35 ),
inference(sat_conversion,[],[f355]) ).
cnf(s97,plain,
( spl25_12
| ~ spl25_33
| ~ spl25_35 ),
inference(sat_conversion,[],[f362]) ).
cnf(s98,plain,
( ~ spl25_4
| ~ spl25_12 ),
inference(sat_conversion,[],[f364]) ).
cnf(s100,plain,
( ~ spl25_4
| ~ spl25_7 ),
inference(sat_conversion,[],[f368]) ).
cnf(s102,plain,
( ~ spl25_26
| ~ spl25_28 ),
inference(sat_conversion,[],[f375]) ).
cnf(s103,plain,
( ~ spl25_33
| spl25_12
| spl25_4 ),
inference(rat,[],[s96,s97]) ).
cnf(s104,plain,
( spl25_24
| spl25_16
| spl25_33
| spl25_11
| ~ spl25_30
| ~ spl25_14
| spl25_1 ),
inference(rat,[],[s53,s102,s65,s44]) ).
cnf(s105,plain,
( spl25_16
| spl25_33
| spl25_11
| ~ spl25_5
| ~ spl25_14
| spl25_6
| spl25_1 ),
inference(rat,[],[s80,s83,s79,s54,s48,s69,s104,s77,s28,s75,s56,s74]) ).
cnf(s106,plain,
( spl25_11
| ~ spl25_5
| spl25_4
| ~ spl25_14
| spl25_6
| spl25_1 ),
inference(rat,[],[s66,s44,s53,s85,s92,s34,s105,s103,s90,s18,s75,s56,s74]) ).
cnf(s107,plain,
( spl25_24
| spl25_19
| spl25_16
| ~ spl25_11
| ~ spl25_30
| ~ spl25_14
| spl25_1 ),
inference(rat,[],[s83,s80,s54,s79,s61,s38,s91,s17]) ).
cnf(s108,plain,
( spl25_16
| ~ spl25_11
| ~ spl25_30
| spl25_23
| ~ spl25_14
| spl25_6
| spl25_1 ),
inference(rat,[],[s53,s102,s57,s50,s107,s77,s28,s91,s17]) ).
cnf(s109,plain,
( spl25_4
| spl25_3
| spl25_2
| spl25_1 ),
inference(rat,[],[s58,s50,s53,s85,s92,s34,s108,s91,s17,s106,s56,s74,s75,s1,s87,s20]) ).
cnf(s110,plain,
( spl25_24
| spl25_16
| spl25_5
| spl25_11
| spl25_32
| ~ spl25_14
| spl25_6
| spl25_1 ),
inference(rat,[],[s81,s55,s21,s63,s22,s53,s85,s102,s44]) ).
cnf(s111,plain,
( spl25_27
| ~ spl25_25
| ~ spl25_24
| spl25_16
| spl25_32
| spl25_6 ),
inference(rat,[],[s77,s27,s79,s94,s80,s56,s83,s57,s54]) ).
cnf(s112,plain,
( spl25_16
| spl25_5
| spl25_1
| spl25_11
| spl25_32
| ~ spl25_14
| spl25_6 ),
inference(rat,[],[s21,s81,s22,s55,s92,s59,s53,s111,s48,s110]) ).
cnf(s113,plain,
( spl25_24
| ~ spl25_16
| spl25_11
| spl25_32
| ~ spl25_14
| spl25_6
| spl25_1 ),
inference(rat,[],[s56,s94,s58,s33,s53,s85,s102,s44]) ).
cnf(s114,plain,
( spl25_27
| ~ spl25_25
| ~ spl25_24
| ~ spl25_16
| spl25_5
| spl25_32
| spl25_6 ),
inference(rat,[],[s32,s31,s77,s79,s81,s80,s55,s83,s64,s54]) ).
cnf(s115,plain,
( ~ spl25_25
| ~ spl25_24
| spl25_6
| ~ spl25_16
| spl25_5
| spl25_32 ),
inference(rat,[],[s94,s33,s56,s92,s62,s53,s114]) ).
cnf(s116,plain,
( spl25_5
| spl25_11
| spl25_1
| spl25_6
| spl25_32
| ~ spl25_14 ),
inference(rat,[],[s115,s48,s113,s112]) ).
cnf(s117,plain,
( spl25_3
| spl25_2
| spl25_1 ),
inference(rat,[],[s116,s73,s17,s3,s76,s98,s100,s109,s20,s87]) ).
cnf(s118,plain,
( spl25_24
| spl25_19
| spl25_16
| spl25_11
| spl25_32
| ~ spl25_30
| spl25_14
| spl25_1 ),
inference(rat,[],[s83,s80,s54,s79,s61,s37]) ).
cnf(s119,plain,
( spl25_19
| spl25_16
| spl25_1
| spl25_11
| spl25_32
| ~ spl25_30
| spl25_14 ),
inference(rat,[],[s53,s102,s57,s49,s118]) ).
cnf(s120,plain,
( spl25_16
| ~ spl25_5
| spl25_2
| spl25_1 ),
inference(rat,[],[s119,s77,s28,s87,s19,s89,s75,s56,s74,s76,s17,s98,s5,s73,s82,s117]) ).
cnf(s121,plain,
( ~ spl25_5
| spl25_2
| spl25_1 ),
inference(rat,[],[s58,s49,s53,s85,s92,s34,s120,s17,s76,s98,s5,s56,s73,s74,s75,s87,s82,s19,s89,s117]) ).
cnf(s122,plain,
( ~ spl25_19
| ~ spl25_30
| spl25_16
| spl25_33
| spl25_11
| spl25_14
| spl25_1 ),
inference(rat,[],[s65,s49,s53,s85,s92]) ).
cnf(s123,plain,
( ~ spl25_30
| spl25_16
| spl25_11
| spl25_2
| spl25_1 ),
inference(rat,[],[s21,s22,s122,s81,s55,s87,s19,s89,s103,s90,s18,s100,s7,s121,s82,s117]) ).
cnf(s126,plain,
( spl25_24
| spl25_19
| spl25_30
| spl25_16
| spl25_33
| spl25_11
| spl25_14
| spl25_1 ),
inference(rat,[],[s83,s80,s54,s79,s67,s37]) ).
cnf(s127,plain,
( spl25_19
| spl25_30
| spl25_1
| spl25_16
| spl25_33
| spl25_11
| spl25_14 ),
inference(rat,[],[s53,s102,s71,s49,s126]) ).
cnf(s128,plain,
( spl25_16
| spl25_11
| spl25_2
| spl25_1 ),
inference(rat,[],[s127,s77,s27,s94,s56,s123,s87,s19,s89,s103,s90,s18,s100,s7,s121,s82,s117]) ).
cnf(s129,plain,
( spl25_20
| spl25_18
| ~ spl25_16
| spl25_5
| spl25_6 ),
inference(rat,[],[s32,s31]) ).
cnf(s130,plain,
( spl25_24
| spl25_19
| ~ spl25_30
| ~ spl25_16
| spl25_33
| spl25_11
| spl25_14
| spl25_1 ),
inference(rat,[],[s83,s80,s54,s79,s70,s37]) ).
cnf(s131,plain,
( spl25_19
| ~ spl25_30
| spl25_1
| ~ spl25_16
| spl25_33
| spl25_11
| spl25_14 ),
inference(rat,[],[s53,s102,s66,s49,s130]) ).
cnf(s132,plain,
( ~ spl25_30
| spl25_11
| spl25_2
| spl25_1 ),
inference(rat,[],[s131,s77,s129,s81,s55,s87,s19,s89,s103,s90,s18,s100,s7,s121,s82,s117,s128]) ).
cnf(s133,plain,
( spl25_11
| spl25_2
| spl25_1 ),
inference(rat,[],[s72,s49,s53,s85,s92,s33,s94,s56,s132,s128,s103,s90,s18,s87,s19,s89,s100,s7,s121,s82,s117]) ).
cnf(s134,plain,
( spl25_19
| spl25_18
| spl25_16
| spl25_5
| spl25_6 ),
inference(rat,[],[s21,s22]) ).
cnf(s135,plain,
( ~ spl25_30
| spl25_16
| spl25_2
| spl25_1 ),
inference(rat,[],[s57,s43,s53,s85,s92,s134,s81,s55,s87,s19,s89,s117,s121,s91,s17,s133]) ).
cnf(s136,plain,
( spl25_24
| spl25_16
| spl25_2
| spl25_1 ),
inference(rat,[],[s53,s102,s63,s43,s19,s89,s117,s91,s17,s133,s135]) ).
cnf(s137,plain,
( spl25_16
| spl25_2
| spl25_1 ),
inference(rat,[],[s111,s59,s47,s136,s135,s87,s19,s89,s117,s91,s17,s133]) ).
cnf(s138,plain,
( spl25_30
| spl25_2
| spl25_1 ),
inference(rat,[],[s64,s43,s53,s85,s92,s33,s94,s56,s87,s19,s89,s117,s91,s17,s133,s137]) ).
cnf(s139,plain,
( spl25_24
| spl25_2
| spl25_1 ),
inference(rat,[],[s53,s102,s58,s43,s19,s89,s117,s91,s17,s133,s137,s138]) ).
cnf(s140,plain,
( spl25_2
| spl25_1 ),
inference(rat,[],[s115,s47,s139,s137,s91,s17,s133,s121,s19,s89,s117,s87]) ).
cnf(s141,plain,
( spl25_30
| ~ spl25_11
| spl25_16
| spl25_1 ),
inference(rat,[],[s63,s50,s53,s85,s92,s20,s25,s78,s86,s2,s74,s94,s56,s140,s98,s91,s17]) ).
cnf(s142,plain,
( ~ spl25_3
| spl25_4
| spl25_1 ),
inference(rat,[],[s73,s2,s5,s78,s82,s140]) ).
cnf(s143,plain,
( spl25_6
| ~ spl25_11
| spl25_16
| spl25_1 ),
inference(rat,[],[s75,s108,s2,s140,s141,s20,s142,s98,s17]) ).
cnf(s144,plain,
( spl25_20
| spl25_5
| ~ spl25_21
| spl25_18
| spl25_16 ),
inference(rat,[],[s24,s23]) ).
cnf(s145,plain,
( ~ spl25_11
| spl25_16
| spl25_1 ),
inference(rat,[],[s53,s102,s57,s50,s107,s77,s144,s73,s6,s86,s88,s143,s20,s142,s81,s55,s141,s91,s98,s17]) ).
cnf(s146,plain,
( ~ spl25_3
| spl25_1 ),
inference(rat,[],[s73,s4,s7,s100,s142,s78,s82,s140]) ).
cnf(s147,plain,
( spl25_6
| spl25_5
| spl25_11
| spl25_1 ),
inference(rat,[],[s76,s116,s2,s140,s20,s146]) ).
cnf(s148,plain,
( spl25_30
| spl25_16
| spl25_1 ),
inference(rat,[],[s71,s44,s53,s103,s85,s92,s100,s25,s8,s86,s88,s147,s74,s94,s56,s20,s146,s90,s18,s145]) ).
cnf(s149,plain,
( spl25_6
| spl25_11
| spl25_1 ),
inference(rat,[],[s100,s4,s106,s73,s147,s140,s20,s146]) ).
cnf(s150,plain,
( spl25_5
| spl25_16
| spl25_1 ),
inference(rat,[],[s80,s83,s79,s54,s48,s69,s104,s103,s77,s100,s144,s8,s20,s146,s90,s18,s81,s55,s148,s88,s86,s149,s145]) ).
cnf(s151,plain,
( spl25_16
| spl25_1 ),
inference(rat,[],[s57,s44,s53,s76,s85,s92,s6,s26,s73,s75,s150,s86,s88,s149,s148,s145,s20,s146]) ).
cnf(s152,plain,
( spl25_24
| spl25_30
| ~ spl25_11
| spl25_1 ),
inference(rat,[],[s83,s80,s54,s79,s60,s38,s20,s146,s91,s77,s35,s86,s2,s74,s140,s98,s17,s151,s94,s56]) ).
cnf(s153,plain,
( spl25_30
| ~ spl25_11
| spl25_1 ),
inference(rat,[],[s53,s102,s64,s50,s152,s20,s146,s151,s91,s17]) ).
cnf(s154,plain,
( spl25_6
| spl25_19
| spl25_4
| spl25_1 ),
inference(rat,[],[s75,s34,s2,s140,s151]) ).
cnf(s155,plain,
( spl25_19
| ~ spl25_11
| spl25_1 ),
inference(rat,[],[s30,s73,s29,s6,s86,s88,s154,s151,s98,s17,s81,s55,s153]) ).
cnf(s156,plain,
( ~ spl25_11
| spl25_1 ),
inference(rat,[],[s58,s50,s53,s85,s92,s155,s153,s91,s17,s20,s146,s151]) ).
cnf(s157,plain,
( ~ spl25_27
| spl25_30
| spl25_1 ),
inference(rat,[],[s44,s102,s68,s53,s20,s146,s151,s103,s100,s8,s74,s56,s88,s149,s90,s18,s156]) ).
cnf(s158,plain,
( spl25_30
| spl25_1 ),
inference(rat,[],[s79,s80,s48,s83,s72,s54,s157,s103,s100,s77,s8,s35,s74,s94,s56,s20,s146,s151,s90,s18,s88,s86,s149,s156]) ).
cnf(s159,plain,
( ~ spl25_27
| spl25_1 ),
inference(rat,[],[s6,s73,s76,s30,s62,s29,s44,s92,s102,s53,s20,s146,s151,s88,s86,s149,s156,s81,s55,s158]) ).
cnf(s160,plain,
( spl25_24
| spl25_1 ),
inference(rat,[],[s73,s30,s6,s29,s76,s85,s58,s44,s20,s146,s151,s88,s86,s149,s156,s81,s55,s158,s159]) ).
cnf(s161,plain,
spl25_1,
inference(rat,[],[s75,s36,s8,s77,s100,s79,s103,s80,s66,s48,s160,s83,s54,s159,s158,s86,s88,s90,s149,s18,s156,s151,s20,s146]) ).
cnf(s162,plain,
( ~ spl25_27
| spl25_14
| spl25_16
| ~ spl25_11 ),
inference(rat,[],[s51,s102,s61,s53,s91,s56,s74,s13,s82,s20,s98,s17,s161]) ).
cnf(s163,plain,
( spl25_14
| spl25_16
| ~ spl25_11 ),
inference(rat,[],[s79,s80,s39,s83,s57,s54,s162,s77,s56,s28,s74,s75,s13,s78,s82,s20,s98,s91,s17,s161]) ).
cnf(s164,plain,
( ~ spl25_27
| spl25_30
| spl25_16
| ~ spl25_11 ),
inference(rat,[],[s42,s102,s59,s53,s91,s17,s163,s161]) ).
cnf(s165,plain,
( spl25_30
| spl25_16
| ~ spl25_11 ),
inference(rat,[],[s111,s46,s63,s164,s88,s14,s74,s56,s98,s91,s17,s163,s161]) ).
cnf(s166,plain,
( spl25_5
| spl25_19
| spl25_18
| spl25_16
| spl25_4 ),
inference(rat,[],[s88,s134,s14,s161]) ).
cnf(s167,plain,
( spl25_19
| spl25_18
| spl25_3
| spl25_16
| spl25_4 ),
inference(rat,[],[s10,s86,s9,s26,s73,s75,s166,s161]) ).
cnf(s168,plain,
( spl25_16
| ~ spl25_11 ),
inference(rat,[],[s57,s42,s53,s85,s92,s167,s81,s55,s165,s89,s19,s163,s98,s91,s17,s161]) ).
cnf(s169,plain,
( spl25_30
| ~ spl25_11 ),
inference(rat,[],[s64,s42,s53,s85,s92,s20,s33,s82,s88,s13,s14,s74,s94,s56,s98,s91,s17,s168,s161]) ).
cnf(s170,plain,
( spl25_14
| ~ spl25_11 ),
inference(rat,[],[s58,s51,s53,s85,s92,s34,s75,s13,s78,s82,s20,s98,s91,s17,s168,s169,s161]) ).
cnf(s171,plain,
( ~ spl25_27
| ~ spl25_11 ),
inference(rat,[],[s42,s102,s62,s53,s91,s17,s168,s169,s170,s161]) ).
cnf(s172,plain,
( spl25_5
| ~ spl25_11 ),
inference(rat,[],[s88,s115,s14,s98,s46,s58,s171,s168,s91,s17,s169,s170,s161]) ).
cnf(s173,plain,
~ spl25_11,
inference(rat,[],[s10,s86,s9,s36,s73,s75,s172,s77,s79,s80,s46,s83,s58,s54,s171,s89,s19,s170,s169,s168,s91,s98,s17,s161]) ).
cnf(s174,plain,
~ spl25_13,
inference(rat,[],[s18,s173]) ).
cnf(s175,plain,
~ spl25_12,
inference(rat,[],[s90,s174]) ).
cnf(s176,plain,
( ~ spl25_27
| spl25_14
| spl25_30
| spl25_16 ),
inference(rat,[],[s41,s102,s59,s53,s76,s13,s82,s20,s74,s56,s161,s173]) ).
cnf(s177,plain,
( spl25_14
| spl25_30
| spl25_16 ),
inference(rat,[],[s111,s45,s63,s176,s76,s13,s78,s82,s20,s74,s56,s161,s173]) ).
cnf(s178,plain,
( ~ spl25_27
| spl25_30
| spl25_16 ),
inference(rat,[],[s11,s12,s100,s103,s86,s67,s25,s52,s92,s102,s53,s94,s74,s56,s89,s19,s177,s161,s175,s173]) ).
cnf(s179,plain,
( spl25_24
| spl25_30
| spl25_16 ),
inference(rat,[],[s27,s88,s77,s14,s79,s76,s80,s63,s40,s94,s74,s56,s177,s83,s54,s178,s161,s173]) ).
cnf(s180,plain,
( spl25_30
| spl25_16 ),
inference(rat,[],[s11,s12,s86,s100,s25,s103,s85,s71,s52,s179,s178,s89,s19,s177,s74,s94,s56,s161,s175,s173]) ).
cnf(s181,plain,
( ~ spl25_27
| spl25_14
| spl25_16 ),
inference(rat,[],[s100,s15,s103,s73,s69,s134,s41,s92,s102,s53,s81,s55,s180,s82,s78,s20,s161,s175,s173]) ).
cnf(s182,plain,
( spl25_24
| spl25_14
| spl25_16 ),
inference(rat,[],[s15,s73,s100,s134,s103,s85,s65,s41,s81,s55,s180,s82,s78,s20,s181,s161,s175,s173]) ).
cnf(s183,plain,
( spl25_14
| spl25_16 ),
inference(rat,[],[s28,s75,s77,s13,s79,s76,s80,s57,s45,s182,s83,s54,s181,s78,s82,s20,s180,s161,s173]) ).
cnf(s184,plain,
( ~ spl25_27
| spl25_16 ),
inference(rat,[],[s76,s61,s167,s52,s92,s102,s53,s81,s55,s180,s89,s19,s183,s173,s161]) ).
cnf(s185,plain,
( spl25_5
| spl25_24
| spl25_16 ),
inference(rat,[],[s86,s12,s144,s11,s81,s55,s89,s19,s100,s103,s65,s180,s77,s79,s80,s83,s54,s184,s40,s183,s161,s173,s175]) ).
cnf(s186,plain,
( spl25_24
| spl25_16 ),
inference(rat,[],[s88,s16,s28,s73,s75,s185,s77,s100,s79,s103,s80,s65,s40,s180,s183,s83,s54,s184,s161,s175,s173]) ).
cnf(s187,plain,
spl25_16,
inference(rat,[],[s167,s76,s85,s57,s52,s186,s184,s89,s19,s183,s81,s55,s180,s173,s161]) ).
cnf(s188,plain,
( spl25_14
| spl25_22
| spl25_24 ),
inference(rat,[],[s33,s85,s78,s41,s20,s187,s161,s173]) ).
cnf(s189,plain,
( ~ spl25_27
| spl25_30
| spl25_24 ),
inference(rat,[],[s88,s14,s33,s76,s92,s60,s53,s94,s74,s56,s161,s187]) ).
cnf(s190,plain,
( spl25_30
| spl25_24 ),
inference(rat,[],[s86,s35,s12,s77,s11,s79,s100,s80,s103,s83,s72,s54,s189,s89,s40,s19,s188,s74,s94,s56,s187,s161,s175,s173]) ).
cnf(s191,plain,
( spl25_14
| spl25_24 ),
inference(rat,[],[s13,s76,s75,s58,s34,s53,s85,s102,s78,s82,s41,s20,s190,s161,s187,s173]) ).
cnf(s192,plain,
( spl25_6
| spl25_7
| spl25_19
| spl25_3 ),
inference(rat,[],[s11,s12,s75,s34,s161,s187]) ).
cnf(s193,plain,
( ~ spl25_27
| spl25_24 ),
inference(rat,[],[s30,s73,s29,s16,s86,s88,s192,s100,s103,s92,s70,s53,s81,s55,s190,s89,s19,s191,s187,s161,s175]) ).
cnf(s194,plain,
( spl25_6
| spl25_24 ),
inference(rat,[],[s10,s9,s73,s129,s81,s55,s89,s19,s76,s58,s190,s77,s79,s80,s83,s54,s193,s40,s191,s161,s187,s173]) ).
cnf(s195,plain,
spl25_24,
inference(rat,[],[s75,s36,s14,s86,s88,s194,s77,s79,s80,s76,s83,s58,s54,s193,s40,s191,s190,s187,s161,s173]) ).
cnf(s196,plain,
( ~ spl25_28
| spl25_22 ),
inference(rat,[],[s78,s20,s33,s52,s92,s102,s187,s173,s161,s195]) ).
cnf(s197,plain,
spl25_30,
inference(rat,[],[s85,s52,s33,s20,s88,s82,s14,s13,s76,s64,s53,s196,s74,s94,s56,s173,s161,s195,s187]) ).
cnf(s198,plain,
spl25_31,
inference(rat,[],[s55,s197]) ).
cnf(s199,plain,
~ spl25_18,
inference(rat,[],[s81,s198]) ).
cnf(s200,plain,
~ spl25_27,
inference(rat,[],[s75,s34,s13,s78,s82,s20,s52,s76,s92,s102,s62,s53,s187,s161,s173,s195,s197]) ).
cnf(s202,plain,
spl25_33,
inference(rat,[],[s66,s197,s195,s187,s200]) ).
cnf(s205,plain,
~ spl25_32,
inference(rat,[],[s95,s202]) ).
cnf(s206,plain,
spl25_4,
inference(rat,[],[s103,s175,s202]) ).
cnf(s207,plain,
~ spl25_7,
inference(rat,[],[s100,s206]) ).
cnf(s208,plain,
( spl25_14
| spl25_6 ),
inference(rat,[],[s73,s15,s115,s82,s45,s20,s161,s207,s187,s195,s205,s173]) ).
cnf(s209,plain,
spl25_6,
inference(rat,[],[s192,s85,s89,s52,s19,s208,s207,s173,s161,s195]) ).
cnf(s210,plain,
~ spl25_10,
inference(rat,[],[s88,s209]) ).
cnf(s212,plain,
spl25_21,
inference(rat,[],[s86,s209]) ).
cnf(s213,plain,
~ spl25_3,
inference(rat,[],[s78,s209]) ).
cnf(s214,plain,
~ spl25_8,
inference(rat,[],[s16,s207,s161,s210]) ).
cnf(s215,plain,
spl25_14,
inference(rat,[],[s20,s213]) ).
cnf(s216,plain,
~ spl25_5,
inference(rat,[],[s73,s214]) ).
cnf(s218,plain,
spl25_26,
inference(rat,[],[s52,s195,s161,s173,s215]) ).
cnf(s219,plain,
~ spl25_19,
inference(rat,[],[s85,s218]) ).
cnf(s221,plain,
spl25_17,
inference(rat,[],[s29,s212,s187,s199,s219]) ).
cnf(s222,plain,
$false,
inference(rat,[],[s30,s212,s187,s216,s219,s221]) ).
fof(f376,plain,
$false,
inference(avatar_sat_refutation,[],[s222]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN723+1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n015.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 16:52:17 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.27 % (2770206)Will run a generic schedule for satisfiability detection.
% 0.22/0.27 % (2770219)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3315396576:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.22/0.27 % (2770216)% WARNING: option uhcvi not known.
% 0.22/0.27 % (2770219) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2770206-2770219"...
% 0.22/0.27 % (2770216)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3136641892:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.22/0.27 % (2770218)dis+10_1_sil=32000:sp=arity:random_seed=1768489429:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.22/0.27 % (2770217)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1512628379:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.22/0.27 % (2770215)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3747824963_2999 on theBenchmark for (2999ds/0Mi)
% 0.22/0.27 % (2770221)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1694869561:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.22/0.27 % (2770220)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1111864243:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.22/0.27 % (2770219)...printing done.
% 0.22/0.27 % (2770219)Refutation found. Thanks to Tanya!
% 0.22/0.27 % SZS status Theorem for theBenchmark
% 0.22/0.27 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/0.28 % (2770219)------------------------------
% 0.22/0.28 % (2770219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/0.28 % (2770219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/0.28 % (2770219)CaDiCaL version: 2.1.3
% 0.22/0.28 % (2770219)Termination reason: Refutation
% 0.22/0.28 % (2770219)Time elapsed: 0.008 s
% 0.22/0.28 % (2770219)Peak memory usage: 12 MB
% 0.22/0.28 % (2770219)Instructions burned: 22 (million)
% 0.22/0.28 % (2770206)Success in time 0.038 s
% 0.22/0.28 % Vampire exiting
%------------------------------------------------------------------------------