%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN007+1.014 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 01:48:48 PM UTC 2026
% Result : Theorem 4.43s 1.34s
% Output : Refutation 5.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
( p_1
<=> ( p_2
<=> ( p_3
<=> ( p_4
<=> ( p_5
<=> ( p_6
<=> ( p_7
<=> ( p_8
<=> ( p_9
<=> ( p_10
<=> ( p_11
<=> ( p_12
<=> ( p_13
<=> ( p_14
<=> ( p_1
<=> ( p_2
<=> ( p_3
<=> ( p_4
<=> ( p_5
<=> ( p_6
<=> ( p_7
<=> ( p_8
<=> ( p_9
<=> ( p_10
<=> ( p_11
<=> ( p_12
<=> ( p_13
<=> p_14 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f2,negated_conjecture,
~ ( p_1
<=> ( p_2
<=> ( p_3
<=> ( p_4
<=> ( p_5
<=> ( p_6
<=> ( p_7
<=> ( p_8
<=> ( p_9
<=> ( p_10
<=> ( p_11
<=> ( p_12
<=> ( p_13
<=> ( p_14
<=> ( p_1
<=> ( p_2
<=> ( p_3
<=> ( p_4
<=> ( p_5
<=> ( p_6
<=> ( p_7
<=> ( p_8
<=> ( p_9
<=> ( p_10
<=> ( p_11
<=> ( p_12
<=> ( p_13
<=> p_14 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( p_1
<~> ( p_2
<=> ( p_3
<=> ( p_4
<=> ( p_5
<=> ( p_6
<=> ( p_7
<=> ( p_8
<=> ( p_9
<=> ( p_10
<=> ( p_11
<=> ( p_12
<=> ( p_13
<=> ( p_14
<=> ( p_1
<=> ( p_2
<=> ( p_3
<=> ( p_4
<=> ( p_5
<=> ( p_6
<=> ( p_7
<=> ( p_8
<=> ( p_9
<=> ( p_10
<=> ( p_11
<=> ( p_12
<=> ( p_13
<=> p_14 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(ennf_transformation,[],[f2]) ).
fof(f4,definition,
( sP0
<=> ( p_11
<=> ( p_12
<=> ( p_13
<=> p_14 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f5,definition,
( sP1
<=> ( p_10
<=> sP0 ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f6,definition,
( sP2
<=> ( p_9
<=> sP1 ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f7,definition,
( sP3
<=> ( p_8
<=> sP2 ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f8,definition,
( sP4
<=> ( p_7
<=> sP3 ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f9,definition,
( sP5
<=> ( p_6
<=> sP4 ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f10,definition,
( sP6
<=> ( p_5
<=> sP5 ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f11,definition,
( sP7
<=> ( p_4
<=> sP6 ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f12,definition,
( sP8
<=> ( p_3
<=> sP7 ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f13,definition,
( sP9
<=> ( p_2
<=> sP8 ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f14,definition,
( sP10
<=> ( p_1
<=> sP9 ) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f15,definition,
( sP11
<=> ( p_14
<=> sP10 ) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f16,definition,
( sP12
<=> ( p_13
<=> sP11 ) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f17,definition,
( sP13
<=> ( p_12
<=> sP12 ) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f18,definition,
( sP14
<=> ( p_11
<=> sP13 ) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f19,definition,
( sP15
<=> ( p_10
<=> sP14 ) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f20,definition,
( sP16
<=> ( p_9
<=> sP15 ) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f21,definition,
( sP17
<=> ( p_8
<=> sP16 ) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f22,definition,
( sP18
<=> ( p_7
<=> sP17 ) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f23,definition,
( sP19
<=> ( p_6
<=> sP18 ) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f24,definition,
( sP20
<=> ( p_5
<=> sP19 ) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f25,definition,
( sP21
<=> ( p_4
<=> sP20 ) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f26,definition,
( sP22
<=> ( p_3
<=> sP21 ) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f27,definition,
( sP23
<=> ( p_2
<=> sP22 ) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f28,plain,
( p_1
<~> sP23 ),
inference(definition_folding,[],[f3,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4]) ).
fof(f29,plain,
( ( sP23
| ( ( ~ sP22
| ~ p_2 )
& ( sP22
| p_2 ) ) )
& ( ( ( p_2
| ~ sP22 )
& ( sP22
| ~ p_2 ) )
| ~ sP23 ) ),
inference(nnf_transformation,[],[f27]) ).
fof(f30,plain,
( ( sP22
| ( ( ~ sP21
| ~ p_3 )
& ( sP21
| p_3 ) ) )
& ( ( ( p_3
| ~ sP21 )
& ( sP21
| ~ p_3 ) )
| ~ sP22 ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f31,plain,
( ( sP21
| ( ( ~ sP20
| ~ p_4 )
& ( sP20
| p_4 ) ) )
& ( ( ( p_4
| ~ sP20 )
& ( sP20
| ~ p_4 ) )
| ~ sP21 ) ),
inference(nnf_transformation,[],[f25]) ).
fof(f32,plain,
( ( sP20
| ( ( ~ sP19
| ~ p_5 )
& ( sP19
| p_5 ) ) )
& ( ( ( p_5
| ~ sP19 )
& ( sP19
| ~ p_5 ) )
| ~ sP20 ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f33,plain,
( ( sP19
| ( ( ~ sP18
| ~ p_6 )
& ( sP18
| p_6 ) ) )
& ( ( ( p_6
| ~ sP18 )
& ( sP18
| ~ p_6 ) )
| ~ sP19 ) ),
inference(nnf_transformation,[],[f23]) ).
fof(f34,plain,
( ( sP18
| ( ( ~ sP17
| ~ p_7 )
& ( sP17
| p_7 ) ) )
& ( ( ( p_7
| ~ sP17 )
& ( sP17
| ~ p_7 ) )
| ~ sP18 ) ),
inference(nnf_transformation,[],[f22]) ).
fof(f35,plain,
( ( sP17
| ( ( ~ sP16
| ~ p_8 )
& ( sP16
| p_8 ) ) )
& ( ( ( p_8
| ~ sP16 )
& ( sP16
| ~ p_8 ) )
| ~ sP17 ) ),
inference(nnf_transformation,[],[f21]) ).
fof(f36,plain,
( ( sP16
| ( ( ~ sP15
| ~ p_9 )
& ( sP15
| p_9 ) ) )
& ( ( ( p_9
| ~ sP15 )
& ( sP15
| ~ p_9 ) )
| ~ sP16 ) ),
inference(nnf_transformation,[],[f20]) ).
fof(f37,plain,
( ( sP15
| ( ( ~ sP14
| ~ p_10 )
& ( sP14
| p_10 ) ) )
& ( ( ( p_10
| ~ sP14 )
& ( sP14
| ~ p_10 ) )
| ~ sP15 ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f38,plain,
( ( sP14
| ( ( ~ sP13
| ~ p_11 )
& ( sP13
| p_11 ) ) )
& ( ( ( p_11
| ~ sP13 )
& ( sP13
| ~ p_11 ) )
| ~ sP14 ) ),
inference(nnf_transformation,[],[f18]) ).
fof(f39,plain,
( ( sP13
| ( ( ~ sP12
| ~ p_12 )
& ( sP12
| p_12 ) ) )
& ( ( ( p_12
| ~ sP12 )
& ( sP12
| ~ p_12 ) )
| ~ sP13 ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f40,plain,
( ( sP12
| ( ( ~ sP11
| ~ p_13 )
& ( sP11
| p_13 ) ) )
& ( ( ( p_13
| ~ sP11 )
& ( sP11
| ~ p_13 ) )
| ~ sP12 ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f41,plain,
( ( sP11
| ( ( ~ sP10
| ~ p_14 )
& ( sP10
| p_14 ) ) )
& ( ( ( p_14
| ~ sP10 )
& ( sP10
| ~ p_14 ) )
| ~ sP11 ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f42,plain,
( ( sP10
| ( ( ~ sP9
| ~ p_1 )
& ( sP9
| p_1 ) ) )
& ( ( ( p_1
| ~ sP9 )
& ( sP9
| ~ p_1 ) )
| ~ sP10 ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f43,plain,
( ( sP9
| ( ( ~ sP8
| ~ p_2 )
& ( sP8
| p_2 ) ) )
& ( ( ( p_2
| ~ sP8 )
& ( sP8
| ~ p_2 ) )
| ~ sP9 ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f44,plain,
( ( sP8
| ( ( ~ sP7
| ~ p_3 )
& ( sP7
| p_3 ) ) )
& ( ( ( p_3
| ~ sP7 )
& ( sP7
| ~ p_3 ) )
| ~ sP8 ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f45,plain,
( ( sP7
| ( ( ~ sP6
| ~ p_4 )
& ( sP6
| p_4 ) ) )
& ( ( ( p_4
| ~ sP6 )
& ( sP6
| ~ p_4 ) )
| ~ sP7 ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f46,plain,
( ( sP6
| ( ( ~ sP5
| ~ p_5 )
& ( sP5
| p_5 ) ) )
& ( ( ( p_5
| ~ sP5 )
& ( sP5
| ~ p_5 ) )
| ~ sP6 ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f47,plain,
( ( sP5
| ( ( ~ sP4
| ~ p_6 )
& ( sP4
| p_6 ) ) )
& ( ( ( p_6
| ~ sP4 )
& ( sP4
| ~ p_6 ) )
| ~ sP5 ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f48,plain,
( ( sP4
| ( ( ~ sP3
| ~ p_7 )
& ( sP3
| p_7 ) ) )
& ( ( ( p_7
| ~ sP3 )
& ( sP3
| ~ p_7 ) )
| ~ sP4 ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f49,plain,
( ( sP3
| ( ( ~ sP2
| ~ p_8 )
& ( sP2
| p_8 ) ) )
& ( ( ( p_8
| ~ sP2 )
& ( sP2
| ~ p_8 ) )
| ~ sP3 ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f50,plain,
( ( sP2
| ( ( ~ sP1
| ~ p_9 )
& ( sP1
| p_9 ) ) )
& ( ( ( p_9
| ~ sP1 )
& ( sP1
| ~ p_9 ) )
| ~ sP2 ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f51,plain,
( ( sP1
| ( ( ~ sP0
| ~ p_10 )
& ( sP0
| p_10 ) ) )
& ( ( ( p_10
| ~ sP0 )
& ( sP0
| ~ p_10 ) )
| ~ sP1 ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f52,plain,
( ( sP0
| ( ( ( ( ( ( ~ p_14
| ~ p_13 )
& ( p_14
| p_13 ) )
| ~ p_12 )
& ( ( ( p_13
| ~ p_14 )
& ( p_14
| ~ p_13 ) )
| p_12 ) )
| ~ p_11 )
& ( ( ( p_12
| ( ( ~ p_14
| ~ p_13 )
& ( p_14
| p_13 ) ) )
& ( ( ( p_13
| ~ p_14 )
& ( p_14
| ~ p_13 ) )
| ~ p_12 ) )
| p_11 ) ) )
& ( ( ( p_11
| ( ( ( ( ~ p_14
| ~ p_13 )
& ( p_14
| p_13 ) )
| ~ p_12 )
& ( ( ( p_13
| ~ p_14 )
& ( p_14
| ~ p_13 ) )
| p_12 ) ) )
& ( ( ( p_12
| ( ( ~ p_14
| ~ p_13 )
& ( p_14
| p_13 ) ) )
& ( ( ( p_13
| ~ p_14 )
& ( p_14
| ~ p_13 ) )
| ~ p_12 ) )
| ~ p_11 ) )
| ~ sP0 ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f53,plain,
( ( ~ sP23
| ~ p_1 )
& ( sP23
| p_1 ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f54,plain,
( sP22
| ~ p_2
| ~ sP23 ),
inference(cnf_transformation,[],[f29]) ).
fof(f55,plain,
( p_2
| ~ sP22
| ~ sP23 ),
inference(cnf_transformation,[],[f29]) ).
fof(f56,plain,
( sP23
| sP22
| p_2 ),
inference(cnf_transformation,[],[f29]) ).
fof(f57,plain,
( sP23
| ~ sP22
| ~ p_2 ),
inference(cnf_transformation,[],[f29]) ).
fof(f58,plain,
( sP21
| ~ p_3
| ~ sP22 ),
inference(cnf_transformation,[],[f30]) ).
fof(f59,plain,
( p_3
| ~ sP21
| ~ sP22 ),
inference(cnf_transformation,[],[f30]) ).
fof(f60,plain,
( sP22
| sP21
| p_3 ),
inference(cnf_transformation,[],[f30]) ).
fof(f61,plain,
( sP22
| ~ sP21
| ~ p_3 ),
inference(cnf_transformation,[],[f30]) ).
fof(f62,plain,
( sP20
| ~ p_4
| ~ sP21 ),
inference(cnf_transformation,[],[f31]) ).
fof(f63,plain,
( p_4
| ~ sP20
| ~ sP21 ),
inference(cnf_transformation,[],[f31]) ).
fof(f64,plain,
( sP21
| sP20
| p_4 ),
inference(cnf_transformation,[],[f31]) ).
fof(f65,plain,
( sP21
| ~ sP20
| ~ p_4 ),
inference(cnf_transformation,[],[f31]) ).
fof(f66,plain,
( sP19
| ~ p_5
| ~ sP20 ),
inference(cnf_transformation,[],[f32]) ).
fof(f67,plain,
( p_5
| ~ sP19
| ~ sP20 ),
inference(cnf_transformation,[],[f32]) ).
fof(f68,plain,
( sP20
| sP19
| p_5 ),
inference(cnf_transformation,[],[f32]) ).
fof(f69,plain,
( sP20
| ~ sP19
| ~ p_5 ),
inference(cnf_transformation,[],[f32]) ).
fof(f70,plain,
( sP18
| ~ p_6
| ~ sP19 ),
inference(cnf_transformation,[],[f33]) ).
fof(f71,plain,
( p_6
| ~ sP18
| ~ sP19 ),
inference(cnf_transformation,[],[f33]) ).
fof(f72,plain,
( sP19
| sP18
| p_6 ),
inference(cnf_transformation,[],[f33]) ).
fof(f73,plain,
( sP19
| ~ sP18
| ~ p_6 ),
inference(cnf_transformation,[],[f33]) ).
fof(f74,plain,
( sP17
| ~ p_7
| ~ sP18 ),
inference(cnf_transformation,[],[f34]) ).
fof(f75,plain,
( p_7
| ~ sP17
| ~ sP18 ),
inference(cnf_transformation,[],[f34]) ).
fof(f76,plain,
( sP18
| sP17
| p_7 ),
inference(cnf_transformation,[],[f34]) ).
fof(f77,plain,
( sP18
| ~ sP17
| ~ p_7 ),
inference(cnf_transformation,[],[f34]) ).
fof(f78,plain,
( sP16
| ~ p_8
| ~ sP17 ),
inference(cnf_transformation,[],[f35]) ).
fof(f79,plain,
( p_8
| ~ sP16
| ~ sP17 ),
inference(cnf_transformation,[],[f35]) ).
fof(f80,plain,
( sP17
| sP16
| p_8 ),
inference(cnf_transformation,[],[f35]) ).
fof(f81,plain,
( sP17
| ~ sP16
| ~ p_8 ),
inference(cnf_transformation,[],[f35]) ).
fof(f82,plain,
( sP15
| ~ p_9
| ~ sP16 ),
inference(cnf_transformation,[],[f36]) ).
fof(f83,plain,
( p_9
| ~ sP15
| ~ sP16 ),
inference(cnf_transformation,[],[f36]) ).
fof(f84,plain,
( sP16
| sP15
| p_9 ),
inference(cnf_transformation,[],[f36]) ).
fof(f85,plain,
( sP16
| ~ sP15
| ~ p_9 ),
inference(cnf_transformation,[],[f36]) ).
fof(f86,plain,
( sP14
| ~ p_10
| ~ sP15 ),
inference(cnf_transformation,[],[f37]) ).
fof(f87,plain,
( p_10
| ~ sP14
| ~ sP15 ),
inference(cnf_transformation,[],[f37]) ).
fof(f88,plain,
( sP15
| sP14
| p_10 ),
inference(cnf_transformation,[],[f37]) ).
fof(f89,plain,
( sP15
| ~ sP14
| ~ p_10 ),
inference(cnf_transformation,[],[f37]) ).
fof(f90,plain,
( sP13
| ~ p_11
| ~ sP14 ),
inference(cnf_transformation,[],[f38]) ).
fof(f91,plain,
( p_11
| ~ sP13
| ~ sP14 ),
inference(cnf_transformation,[],[f38]) ).
fof(f92,plain,
( sP14
| sP13
| p_11 ),
inference(cnf_transformation,[],[f38]) ).
fof(f93,plain,
( sP14
| ~ sP13
| ~ p_11 ),
inference(cnf_transformation,[],[f38]) ).
fof(f94,plain,
( sP12
| ~ p_12
| ~ sP13 ),
inference(cnf_transformation,[],[f39]) ).
fof(f95,plain,
( p_12
| ~ sP12
| ~ sP13 ),
inference(cnf_transformation,[],[f39]) ).
fof(f96,plain,
( sP13
| sP12
| p_12 ),
inference(cnf_transformation,[],[f39]) ).
fof(f97,plain,
( sP13
| ~ sP12
| ~ p_12 ),
inference(cnf_transformation,[],[f39]) ).
fof(f98,plain,
( sP11
| ~ p_13
| ~ sP12 ),
inference(cnf_transformation,[],[f40]) ).
fof(f99,plain,
( p_13
| ~ sP11
| ~ sP12 ),
inference(cnf_transformation,[],[f40]) ).
fof(f100,plain,
( sP12
| sP11
| p_13 ),
inference(cnf_transformation,[],[f40]) ).
fof(f101,plain,
( sP12
| ~ sP11
| ~ p_13 ),
inference(cnf_transformation,[],[f40]) ).
fof(f102,plain,
( sP10
| ~ p_14
| ~ sP11 ),
inference(cnf_transformation,[],[f41]) ).
fof(f103,plain,
( p_14
| ~ sP10
| ~ sP11 ),
inference(cnf_transformation,[],[f41]) ).
fof(f104,plain,
( sP11
| sP10
| p_14 ),
inference(cnf_transformation,[],[f41]) ).
fof(f105,plain,
( sP11
| ~ sP10
| ~ p_14 ),
inference(cnf_transformation,[],[f41]) ).
fof(f106,plain,
( sP9
| ~ p_1
| ~ sP10 ),
inference(cnf_transformation,[],[f42]) ).
fof(f107,plain,
( p_1
| ~ sP9
| ~ sP10 ),
inference(cnf_transformation,[],[f42]) ).
fof(f108,plain,
( sP10
| sP9
| p_1 ),
inference(cnf_transformation,[],[f42]) ).
fof(f109,plain,
( sP10
| ~ sP9
| ~ p_1 ),
inference(cnf_transformation,[],[f42]) ).
fof(f110,plain,
( sP8
| ~ p_2
| ~ sP9 ),
inference(cnf_transformation,[],[f43]) ).
fof(f111,plain,
( p_2
| ~ sP8
| ~ sP9 ),
inference(cnf_transformation,[],[f43]) ).
fof(f112,plain,
( sP9
| sP8
| p_2 ),
inference(cnf_transformation,[],[f43]) ).
fof(f113,plain,
( sP9
| ~ sP8
| ~ p_2 ),
inference(cnf_transformation,[],[f43]) ).
fof(f114,plain,
( sP7
| ~ p_3
| ~ sP8 ),
inference(cnf_transformation,[],[f44]) ).
fof(f115,plain,
( p_3
| ~ sP7
| ~ sP8 ),
inference(cnf_transformation,[],[f44]) ).
fof(f116,plain,
( sP8
| sP7
| p_3 ),
inference(cnf_transformation,[],[f44]) ).
fof(f117,plain,
( sP8
| ~ sP7
| ~ p_3 ),
inference(cnf_transformation,[],[f44]) ).
fof(f118,plain,
( sP6
| ~ p_4
| ~ sP7 ),
inference(cnf_transformation,[],[f45]) ).
fof(f119,plain,
( p_4
| ~ sP6
| ~ sP7 ),
inference(cnf_transformation,[],[f45]) ).
fof(f120,plain,
( sP7
| sP6
| p_4 ),
inference(cnf_transformation,[],[f45]) ).
fof(f121,plain,
( sP7
| ~ sP6
| ~ p_4 ),
inference(cnf_transformation,[],[f45]) ).
fof(f122,plain,
( sP5
| ~ p_5
| ~ sP6 ),
inference(cnf_transformation,[],[f46]) ).
fof(f123,plain,
( p_5
| ~ sP5
| ~ sP6 ),
inference(cnf_transformation,[],[f46]) ).
fof(f124,plain,
( sP6
| sP5
| p_5 ),
inference(cnf_transformation,[],[f46]) ).
fof(f125,plain,
( sP6
| ~ sP5
| ~ p_5 ),
inference(cnf_transformation,[],[f46]) ).
fof(f126,plain,
( sP4
| ~ p_6
| ~ sP5 ),
inference(cnf_transformation,[],[f47]) ).
fof(f127,plain,
( p_6
| ~ sP4
| ~ sP5 ),
inference(cnf_transformation,[],[f47]) ).
fof(f128,plain,
( sP5
| sP4
| p_6 ),
inference(cnf_transformation,[],[f47]) ).
fof(f129,plain,
( sP5
| ~ sP4
| ~ p_6 ),
inference(cnf_transformation,[],[f47]) ).
fof(f130,plain,
( sP3
| ~ p_7
| ~ sP4 ),
inference(cnf_transformation,[],[f48]) ).
fof(f131,plain,
( p_7
| ~ sP3
| ~ sP4 ),
inference(cnf_transformation,[],[f48]) ).
fof(f132,plain,
( sP4
| sP3
| p_7 ),
inference(cnf_transformation,[],[f48]) ).
fof(f133,plain,
( sP4
| ~ sP3
| ~ p_7 ),
inference(cnf_transformation,[],[f48]) ).
fof(f134,plain,
( sP2
| ~ p_8
| ~ sP3 ),
inference(cnf_transformation,[],[f49]) ).
fof(f135,plain,
( p_8
| ~ sP2
| ~ sP3 ),
inference(cnf_transformation,[],[f49]) ).
fof(f136,plain,
( sP3
| sP2
| p_8 ),
inference(cnf_transformation,[],[f49]) ).
fof(f137,plain,
( sP3
| ~ sP2
| ~ p_8 ),
inference(cnf_transformation,[],[f49]) ).
fof(f138,plain,
( sP1
| ~ p_9
| ~ sP2 ),
inference(cnf_transformation,[],[f50]) ).
fof(f139,plain,
( p_9
| ~ sP1
| ~ sP2 ),
inference(cnf_transformation,[],[f50]) ).
fof(f140,plain,
( sP2
| sP1
| p_9 ),
inference(cnf_transformation,[],[f50]) ).
fof(f141,plain,
( sP2
| ~ sP1
| ~ p_9 ),
inference(cnf_transformation,[],[f50]) ).
fof(f142,plain,
( sP0
| ~ p_10
| ~ sP1 ),
inference(cnf_transformation,[],[f51]) ).
fof(f143,plain,
( p_10
| ~ sP0
| ~ sP1 ),
inference(cnf_transformation,[],[f51]) ).
fof(f144,plain,
( sP1
| sP0
| p_10 ),
inference(cnf_transformation,[],[f51]) ).
fof(f145,plain,
( sP1
| ~ sP0
| ~ p_10 ),
inference(cnf_transformation,[],[f51]) ).
fof(f146,plain,
( p_14
| ~ p_13
| ~ p_12
| ~ p_11
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f147,plain,
( p_13
| ~ p_14
| ~ p_12
| ~ p_11
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f148,plain,
( p_12
| p_14
| p_13
| ~ p_11
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f149,plain,
( p_12
| ~ p_14
| ~ p_13
| ~ p_11
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f150,plain,
( p_11
| p_14
| ~ p_13
| p_12
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f151,plain,
( p_11
| p_13
| ~ p_14
| p_12
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f152,plain,
( p_11
| p_14
| p_13
| ~ p_12
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f153,plain,
( p_11
| ~ p_14
| ~ p_13
| ~ p_12
| ~ sP0 ),
inference(cnf_transformation,[],[f52]) ).
fof(f154,plain,
( sP0
| p_14
| ~ p_13
| ~ p_12
| p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f155,plain,
( sP0
| p_13
| ~ p_14
| ~ p_12
| p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f156,plain,
( sP0
| p_12
| p_14
| p_13
| p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f157,plain,
( sP0
| p_12
| ~ p_14
| ~ p_13
| p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f158,plain,
( sP0
| p_14
| ~ p_13
| p_12
| ~ p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f159,plain,
( sP0
| p_13
| ~ p_14
| p_12
| ~ p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f160,plain,
( sP0
| p_14
| p_13
| ~ p_12
| ~ p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f161,plain,
( sP0
| ~ p_14
| ~ p_13
| ~ p_12
| ~ p_11 ),
inference(cnf_transformation,[],[f52]) ).
fof(f162,plain,
( sP23
| p_1 ),
inference(cnf_transformation,[],[f53]) ).
fof(f163,plain,
( ~ sP23
| ~ p_1 ),
inference(cnf_transformation,[],[f53]) ).
fof(f165,definition,
( spl24_1
<=> p_1 ),
introduced(definition,[new_symbols(definition,[spl24_1])],[avatar_definition]) ).
fof(f169,definition,
( spl24_2
<=> sP23 ),
introduced(definition,[new_symbols(definition,[spl24_2])],[avatar_definition]) ).
fof(f172,plain,
( spl24_1
| spl24_2 ),
inference(avatar_split_clause,[],[f162,f169,f165]) ).
fof(f173,plain,
( ~ spl24_1
| ~ spl24_2 ),
inference(avatar_split_clause,[],[f163,f169,f165]) ).
fof(f175,definition,
( spl24_3
<=> sP0 ),
introduced(definition,[new_symbols(definition,[spl24_3])],[avatar_definition]) ).
fof(f179,definition,
( spl24_4
<=> p_11 ),
introduced(definition,[new_symbols(definition,[spl24_4])],[avatar_definition]) ).
fof(f183,definition,
( spl24_5
<=> p_12 ),
introduced(definition,[new_symbols(definition,[spl24_5])],[avatar_definition]) ).
fof(f187,definition,
( spl24_6
<=> p_13 ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
fof(f191,definition,
( spl24_7
<=> p_14 ),
introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition]) ).
fof(f194,plain,
( ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| spl24_7 ),
inference(avatar_split_clause,[],[f146,f191,f187,f183,f179,f175]) ).
fof(f195,plain,
( ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_7
| spl24_6 ),
inference(avatar_split_clause,[],[f147,f187,f191,f183,f179,f175]) ).
fof(f196,plain,
( ~ spl24_3
| ~ spl24_4
| spl24_6
| spl24_7
| spl24_5 ),
inference(avatar_split_clause,[],[f148,f183,f191,f187,f179,f175]) ).
fof(f197,plain,
( ~ spl24_3
| ~ spl24_4
| ~ spl24_6
| ~ spl24_7
| spl24_5 ),
inference(avatar_split_clause,[],[f149,f183,f191,f187,f179,f175]) ).
fof(f198,plain,
( ~ spl24_3
| spl24_5
| ~ spl24_6
| spl24_7
| spl24_4 ),
inference(avatar_split_clause,[],[f150,f179,f191,f187,f183,f175]) ).
fof(f199,plain,
( ~ spl24_3
| spl24_5
| ~ spl24_7
| spl24_6
| spl24_4 ),
inference(avatar_split_clause,[],[f151,f179,f187,f191,f183,f175]) ).
fof(f200,plain,
( ~ spl24_3
| ~ spl24_5
| spl24_6
| spl24_7
| spl24_4 ),
inference(avatar_split_clause,[],[f152,f179,f191,f187,f183,f175]) ).
fof(f201,plain,
( ~ spl24_3
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7
| spl24_4 ),
inference(avatar_split_clause,[],[f153,f179,f191,f187,f183,f175]) ).
fof(f202,plain,
( spl24_4
| ~ spl24_5
| ~ spl24_6
| spl24_7
| spl24_3 ),
inference(avatar_split_clause,[],[f154,f175,f191,f187,f183,f179]) ).
fof(f203,plain,
( spl24_4
| ~ spl24_5
| ~ spl24_7
| spl24_6
| spl24_3 ),
inference(avatar_split_clause,[],[f155,f175,f187,f191,f183,f179]) ).
fof(f204,plain,
( spl24_4
| spl24_6
| spl24_7
| spl24_5
| spl24_3 ),
inference(avatar_split_clause,[],[f156,f175,f183,f191,f187,f179]) ).
fof(f205,plain,
( spl24_4
| ~ spl24_6
| ~ spl24_7
| spl24_5
| spl24_3 ),
inference(avatar_split_clause,[],[f157,f175,f183,f191,f187,f179]) ).
fof(f206,plain,
( ~ spl24_4
| spl24_5
| ~ spl24_6
| spl24_7
| spl24_3 ),
inference(avatar_split_clause,[],[f158,f175,f191,f187,f183,f179]) ).
fof(f207,plain,
( ~ spl24_4
| spl24_5
| ~ spl24_7
| spl24_6
| spl24_3 ),
inference(avatar_split_clause,[],[f159,f175,f187,f191,f183,f179]) ).
fof(f208,plain,
( ~ spl24_4
| ~ spl24_5
| spl24_6
| spl24_7
| spl24_3 ),
inference(avatar_split_clause,[],[f160,f175,f191,f187,f183,f179]) ).
fof(f209,plain,
( ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7
| spl24_3 ),
inference(avatar_split_clause,[],[f161,f175,f191,f187,f183,f179]) ).
fof(f211,definition,
( spl24_8
<=> sP1 ),
introduced(definition,[new_symbols(definition,[spl24_8])],[avatar_definition]) ).
fof(f215,definition,
( spl24_9
<=> p_10 ),
introduced(definition,[new_symbols(definition,[spl24_9])],[avatar_definition]) ).
fof(f218,plain,
( ~ spl24_8
| ~ spl24_9
| spl24_3 ),
inference(avatar_split_clause,[],[f142,f175,f215,f211]) ).
fof(f219,plain,
( ~ spl24_8
| ~ spl24_3
| spl24_9 ),
inference(avatar_split_clause,[],[f143,f215,f175,f211]) ).
fof(f220,plain,
( spl24_9
| spl24_3
| spl24_8 ),
inference(avatar_split_clause,[],[f144,f211,f175,f215]) ).
fof(f221,plain,
( ~ spl24_9
| ~ spl24_3
| spl24_8 ),
inference(avatar_split_clause,[],[f145,f211,f175,f215]) ).
fof(f223,definition,
( spl24_10
<=> sP2 ),
introduced(definition,[new_symbols(definition,[spl24_10])],[avatar_definition]) ).
fof(f227,definition,
( spl24_11
<=> p_9 ),
introduced(definition,[new_symbols(definition,[spl24_11])],[avatar_definition]) ).
fof(f230,plain,
( ~ spl24_10
| ~ spl24_11
| spl24_8 ),
inference(avatar_split_clause,[],[f138,f211,f227,f223]) ).
fof(f231,plain,
( ~ spl24_10
| ~ spl24_8
| spl24_11 ),
inference(avatar_split_clause,[],[f139,f227,f211,f223]) ).
fof(f232,plain,
( spl24_11
| spl24_8
| spl24_10 ),
inference(avatar_split_clause,[],[f140,f223,f211,f227]) ).
fof(f233,plain,
( ~ spl24_11
| ~ spl24_8
| spl24_10 ),
inference(avatar_split_clause,[],[f141,f223,f211,f227]) ).
fof(f235,definition,
( spl24_12
<=> sP3 ),
introduced(definition,[new_symbols(definition,[spl24_12])],[avatar_definition]) ).
fof(f239,definition,
( spl24_13
<=> p_8 ),
introduced(definition,[new_symbols(definition,[spl24_13])],[avatar_definition]) ).
fof(f242,plain,
( ~ spl24_12
| ~ spl24_13
| spl24_10 ),
inference(avatar_split_clause,[],[f134,f223,f239,f235]) ).
fof(f243,plain,
( ~ spl24_12
| ~ spl24_10
| spl24_13 ),
inference(avatar_split_clause,[],[f135,f239,f223,f235]) ).
fof(f244,plain,
( spl24_13
| spl24_10
| spl24_12 ),
inference(avatar_split_clause,[],[f136,f235,f223,f239]) ).
fof(f245,plain,
( ~ spl24_13
| ~ spl24_10
| spl24_12 ),
inference(avatar_split_clause,[],[f137,f235,f223,f239]) ).
fof(f247,definition,
( spl24_14
<=> sP4 ),
introduced(definition,[new_symbols(definition,[spl24_14])],[avatar_definition]) ).
fof(f251,definition,
( spl24_15
<=> p_7 ),
introduced(definition,[new_symbols(definition,[spl24_15])],[avatar_definition]) ).
fof(f254,plain,
( ~ spl24_14
| ~ spl24_15
| spl24_12 ),
inference(avatar_split_clause,[],[f130,f235,f251,f247]) ).
fof(f255,plain,
( ~ spl24_14
| ~ spl24_12
| spl24_15 ),
inference(avatar_split_clause,[],[f131,f251,f235,f247]) ).
fof(f256,plain,
( spl24_15
| spl24_12
| spl24_14 ),
inference(avatar_split_clause,[],[f132,f247,f235,f251]) ).
fof(f257,plain,
( ~ spl24_15
| ~ spl24_12
| spl24_14 ),
inference(avatar_split_clause,[],[f133,f247,f235,f251]) ).
fof(f259,definition,
( spl24_16
<=> sP5 ),
introduced(definition,[new_symbols(definition,[spl24_16])],[avatar_definition]) ).
fof(f263,definition,
( spl24_17
<=> p_6 ),
introduced(definition,[new_symbols(definition,[spl24_17])],[avatar_definition]) ).
fof(f266,plain,
( ~ spl24_16
| ~ spl24_17
| spl24_14 ),
inference(avatar_split_clause,[],[f126,f247,f263,f259]) ).
fof(f267,plain,
( ~ spl24_16
| ~ spl24_14
| spl24_17 ),
inference(avatar_split_clause,[],[f127,f263,f247,f259]) ).
fof(f268,plain,
( spl24_17
| spl24_14
| spl24_16 ),
inference(avatar_split_clause,[],[f128,f259,f247,f263]) ).
fof(f269,plain,
( ~ spl24_17
| ~ spl24_14
| spl24_16 ),
inference(avatar_split_clause,[],[f129,f259,f247,f263]) ).
fof(f271,definition,
( spl24_18
<=> sP6 ),
introduced(definition,[new_symbols(definition,[spl24_18])],[avatar_definition]) ).
fof(f275,definition,
( spl24_19
<=> p_5 ),
introduced(definition,[new_symbols(definition,[spl24_19])],[avatar_definition]) ).
fof(f278,plain,
( ~ spl24_18
| ~ spl24_19
| spl24_16 ),
inference(avatar_split_clause,[],[f122,f259,f275,f271]) ).
fof(f279,plain,
( ~ spl24_18
| ~ spl24_16
| spl24_19 ),
inference(avatar_split_clause,[],[f123,f275,f259,f271]) ).
fof(f280,plain,
( spl24_19
| spl24_16
| spl24_18 ),
inference(avatar_split_clause,[],[f124,f271,f259,f275]) ).
fof(f281,plain,
( ~ spl24_19
| ~ spl24_16
| spl24_18 ),
inference(avatar_split_clause,[],[f125,f271,f259,f275]) ).
fof(f283,definition,
( spl24_20
<=> sP7 ),
introduced(definition,[new_symbols(definition,[spl24_20])],[avatar_definition]) ).
fof(f287,definition,
( spl24_21
<=> p_4 ),
introduced(definition,[new_symbols(definition,[spl24_21])],[avatar_definition]) ).
fof(f290,plain,
( ~ spl24_20
| ~ spl24_21
| spl24_18 ),
inference(avatar_split_clause,[],[f118,f271,f287,f283]) ).
fof(f291,plain,
( ~ spl24_20
| ~ spl24_18
| spl24_21 ),
inference(avatar_split_clause,[],[f119,f287,f271,f283]) ).
fof(f292,plain,
( spl24_21
| spl24_18
| spl24_20 ),
inference(avatar_split_clause,[],[f120,f283,f271,f287]) ).
fof(f293,plain,
( ~ spl24_21
| ~ spl24_18
| spl24_20 ),
inference(avatar_split_clause,[],[f121,f283,f271,f287]) ).
fof(f295,definition,
( spl24_22
<=> sP8 ),
introduced(definition,[new_symbols(definition,[spl24_22])],[avatar_definition]) ).
fof(f299,definition,
( spl24_23
<=> p_3 ),
introduced(definition,[new_symbols(definition,[spl24_23])],[avatar_definition]) ).
fof(f302,plain,
( ~ spl24_22
| ~ spl24_23
| spl24_20 ),
inference(avatar_split_clause,[],[f114,f283,f299,f295]) ).
fof(f303,plain,
( ~ spl24_22
| ~ spl24_20
| spl24_23 ),
inference(avatar_split_clause,[],[f115,f299,f283,f295]) ).
fof(f304,plain,
( spl24_23
| spl24_20
| spl24_22 ),
inference(avatar_split_clause,[],[f116,f295,f283,f299]) ).
fof(f305,plain,
( ~ spl24_23
| ~ spl24_20
| spl24_22 ),
inference(avatar_split_clause,[],[f117,f295,f283,f299]) ).
fof(f307,definition,
( spl24_24
<=> sP9 ),
introduced(definition,[new_symbols(definition,[spl24_24])],[avatar_definition]) ).
fof(f311,definition,
( spl24_25
<=> p_2 ),
introduced(definition,[new_symbols(definition,[spl24_25])],[avatar_definition]) ).
fof(f314,plain,
( ~ spl24_24
| ~ spl24_25
| spl24_22 ),
inference(avatar_split_clause,[],[f110,f295,f311,f307]) ).
fof(f315,plain,
( ~ spl24_24
| ~ spl24_22
| spl24_25 ),
inference(avatar_split_clause,[],[f111,f311,f295,f307]) ).
fof(f316,plain,
( spl24_25
| spl24_22
| spl24_24 ),
inference(avatar_split_clause,[],[f112,f307,f295,f311]) ).
fof(f317,plain,
( ~ spl24_25
| ~ spl24_22
| spl24_24 ),
inference(avatar_split_clause,[],[f113,f307,f295,f311]) ).
fof(f319,definition,
( spl24_26
<=> sP10 ),
introduced(definition,[new_symbols(definition,[spl24_26])],[avatar_definition]) ).
fof(f322,plain,
( ~ spl24_26
| ~ spl24_1
| spl24_24 ),
inference(avatar_split_clause,[],[f106,f307,f165,f319]) ).
fof(f323,plain,
( ~ spl24_26
| ~ spl24_24
| spl24_1 ),
inference(avatar_split_clause,[],[f107,f165,f307,f319]) ).
fof(f324,plain,
( spl24_1
| spl24_24
| spl24_26 ),
inference(avatar_split_clause,[],[f108,f319,f307,f165]) ).
fof(f325,plain,
( ~ spl24_1
| ~ spl24_24
| spl24_26 ),
inference(avatar_split_clause,[],[f109,f319,f307,f165]) ).
fof(f327,definition,
( spl24_27
<=> sP11 ),
introduced(definition,[new_symbols(definition,[spl24_27])],[avatar_definition]) ).
fof(f330,plain,
( ~ spl24_27
| ~ spl24_7
| spl24_26 ),
inference(avatar_split_clause,[],[f102,f319,f191,f327]) ).
fof(f331,plain,
( ~ spl24_27
| ~ spl24_26
| spl24_7 ),
inference(avatar_split_clause,[],[f103,f191,f319,f327]) ).
fof(f332,plain,
( spl24_7
| spl24_26
| spl24_27 ),
inference(avatar_split_clause,[],[f104,f327,f319,f191]) ).
fof(f333,plain,
( ~ spl24_7
| ~ spl24_26
| spl24_27 ),
inference(avatar_split_clause,[],[f105,f327,f319,f191]) ).
fof(f335,definition,
( spl24_28
<=> sP12 ),
introduced(definition,[new_symbols(definition,[spl24_28])],[avatar_definition]) ).
fof(f338,plain,
( ~ spl24_28
| ~ spl24_6
| spl24_27 ),
inference(avatar_split_clause,[],[f98,f327,f187,f335]) ).
fof(f339,plain,
( ~ spl24_28
| ~ spl24_27
| spl24_6 ),
inference(avatar_split_clause,[],[f99,f187,f327,f335]) ).
fof(f340,plain,
( spl24_6
| spl24_27
| spl24_28 ),
inference(avatar_split_clause,[],[f100,f335,f327,f187]) ).
fof(f341,plain,
( ~ spl24_6
| ~ spl24_27
| spl24_28 ),
inference(avatar_split_clause,[],[f101,f335,f327,f187]) ).
fof(f343,definition,
( spl24_29
<=> sP13 ),
introduced(definition,[new_symbols(definition,[spl24_29])],[avatar_definition]) ).
fof(f346,plain,
( ~ spl24_29
| ~ spl24_5
| spl24_28 ),
inference(avatar_split_clause,[],[f94,f335,f183,f343]) ).
fof(f347,plain,
( ~ spl24_29
| ~ spl24_28
| spl24_5 ),
inference(avatar_split_clause,[],[f95,f183,f335,f343]) ).
fof(f348,plain,
( spl24_5
| spl24_28
| spl24_29 ),
inference(avatar_split_clause,[],[f96,f343,f335,f183]) ).
fof(f349,plain,
( ~ spl24_5
| ~ spl24_28
| spl24_29 ),
inference(avatar_split_clause,[],[f97,f343,f335,f183]) ).
fof(f351,definition,
( spl24_30
<=> sP14 ),
introduced(definition,[new_symbols(definition,[spl24_30])],[avatar_definition]) ).
fof(f354,plain,
( ~ spl24_30
| ~ spl24_4
| spl24_29 ),
inference(avatar_split_clause,[],[f90,f343,f179,f351]) ).
fof(f355,plain,
( ~ spl24_30
| ~ spl24_29
| spl24_4 ),
inference(avatar_split_clause,[],[f91,f179,f343,f351]) ).
fof(f356,plain,
( spl24_4
| spl24_29
| spl24_30 ),
inference(avatar_split_clause,[],[f92,f351,f343,f179]) ).
fof(f357,plain,
( ~ spl24_4
| ~ spl24_29
| spl24_30 ),
inference(avatar_split_clause,[],[f93,f351,f343,f179]) ).
fof(f359,definition,
( spl24_31
<=> sP15 ),
introduced(definition,[new_symbols(definition,[spl24_31])],[avatar_definition]) ).
fof(f362,plain,
( ~ spl24_31
| ~ spl24_9
| spl24_30 ),
inference(avatar_split_clause,[],[f86,f351,f215,f359]) ).
fof(f363,plain,
( ~ spl24_31
| ~ spl24_30
| spl24_9 ),
inference(avatar_split_clause,[],[f87,f215,f351,f359]) ).
fof(f364,plain,
( spl24_9
| spl24_30
| spl24_31 ),
inference(avatar_split_clause,[],[f88,f359,f351,f215]) ).
fof(f365,plain,
( ~ spl24_9
| ~ spl24_30
| spl24_31 ),
inference(avatar_split_clause,[],[f89,f359,f351,f215]) ).
fof(f367,definition,
( spl24_32
<=> sP16 ),
introduced(definition,[new_symbols(definition,[spl24_32])],[avatar_definition]) ).
fof(f370,plain,
( ~ spl24_32
| ~ spl24_11
| spl24_31 ),
inference(avatar_split_clause,[],[f82,f359,f227,f367]) ).
fof(f371,plain,
( ~ spl24_32
| ~ spl24_31
| spl24_11 ),
inference(avatar_split_clause,[],[f83,f227,f359,f367]) ).
fof(f372,plain,
( spl24_11
| spl24_31
| spl24_32 ),
inference(avatar_split_clause,[],[f84,f367,f359,f227]) ).
fof(f373,plain,
( ~ spl24_11
| ~ spl24_31
| spl24_32 ),
inference(avatar_split_clause,[],[f85,f367,f359,f227]) ).
fof(f375,definition,
( spl24_33
<=> sP17 ),
introduced(definition,[new_symbols(definition,[spl24_33])],[avatar_definition]) ).
fof(f378,plain,
( ~ spl24_33
| ~ spl24_13
| spl24_32 ),
inference(avatar_split_clause,[],[f78,f367,f239,f375]) ).
fof(f379,plain,
( ~ spl24_33
| ~ spl24_32
| spl24_13 ),
inference(avatar_split_clause,[],[f79,f239,f367,f375]) ).
fof(f380,plain,
( spl24_13
| spl24_32
| spl24_33 ),
inference(avatar_split_clause,[],[f80,f375,f367,f239]) ).
fof(f381,plain,
( ~ spl24_13
| ~ spl24_32
| spl24_33 ),
inference(avatar_split_clause,[],[f81,f375,f367,f239]) ).
fof(f383,definition,
( spl24_34
<=> sP18 ),
introduced(definition,[new_symbols(definition,[spl24_34])],[avatar_definition]) ).
fof(f386,plain,
( ~ spl24_34
| ~ spl24_15
| spl24_33 ),
inference(avatar_split_clause,[],[f74,f375,f251,f383]) ).
fof(f387,plain,
( ~ spl24_34
| ~ spl24_33
| spl24_15 ),
inference(avatar_split_clause,[],[f75,f251,f375,f383]) ).
fof(f388,plain,
( spl24_15
| spl24_33
| spl24_34 ),
inference(avatar_split_clause,[],[f76,f383,f375,f251]) ).
fof(f389,plain,
( ~ spl24_15
| ~ spl24_33
| spl24_34 ),
inference(avatar_split_clause,[],[f77,f383,f375,f251]) ).
fof(f391,definition,
( spl24_35
<=> sP19 ),
introduced(definition,[new_symbols(definition,[spl24_35])],[avatar_definition]) ).
fof(f394,plain,
( ~ spl24_35
| ~ spl24_17
| spl24_34 ),
inference(avatar_split_clause,[],[f70,f383,f263,f391]) ).
fof(f395,plain,
( ~ spl24_35
| ~ spl24_34
| spl24_17 ),
inference(avatar_split_clause,[],[f71,f263,f383,f391]) ).
fof(f396,plain,
( spl24_17
| spl24_34
| spl24_35 ),
inference(avatar_split_clause,[],[f72,f391,f383,f263]) ).
fof(f397,plain,
( ~ spl24_17
| ~ spl24_34
| spl24_35 ),
inference(avatar_split_clause,[],[f73,f391,f383,f263]) ).
fof(f399,definition,
( spl24_36
<=> sP20 ),
introduced(definition,[new_symbols(definition,[spl24_36])],[avatar_definition]) ).
fof(f402,plain,
( ~ spl24_36
| ~ spl24_19
| spl24_35 ),
inference(avatar_split_clause,[],[f66,f391,f275,f399]) ).
fof(f403,plain,
( ~ spl24_36
| ~ spl24_35
| spl24_19 ),
inference(avatar_split_clause,[],[f67,f275,f391,f399]) ).
fof(f404,plain,
( spl24_19
| spl24_35
| spl24_36 ),
inference(avatar_split_clause,[],[f68,f399,f391,f275]) ).
fof(f405,plain,
( ~ spl24_19
| ~ spl24_35
| spl24_36 ),
inference(avatar_split_clause,[],[f69,f399,f391,f275]) ).
fof(f407,definition,
( spl24_37
<=> sP21 ),
introduced(definition,[new_symbols(definition,[spl24_37])],[avatar_definition]) ).
fof(f410,plain,
( ~ spl24_37
| ~ spl24_21
| spl24_36 ),
inference(avatar_split_clause,[],[f62,f399,f287,f407]) ).
fof(f411,plain,
( ~ spl24_37
| ~ spl24_36
| spl24_21 ),
inference(avatar_split_clause,[],[f63,f287,f399,f407]) ).
fof(f412,plain,
( spl24_21
| spl24_36
| spl24_37 ),
inference(avatar_split_clause,[],[f64,f407,f399,f287]) ).
fof(f413,plain,
( ~ spl24_21
| ~ spl24_36
| spl24_37 ),
inference(avatar_split_clause,[],[f65,f407,f399,f287]) ).
fof(f415,definition,
( spl24_38
<=> sP22 ),
introduced(definition,[new_symbols(definition,[spl24_38])],[avatar_definition]) ).
fof(f418,plain,
( ~ spl24_38
| ~ spl24_23
| spl24_37 ),
inference(avatar_split_clause,[],[f58,f407,f299,f415]) ).
fof(f419,plain,
( ~ spl24_38
| ~ spl24_37
| spl24_23 ),
inference(avatar_split_clause,[],[f59,f299,f407,f415]) ).
fof(f420,plain,
( spl24_23
| spl24_37
| spl24_38 ),
inference(avatar_split_clause,[],[f60,f415,f407,f299]) ).
fof(f421,plain,
( ~ spl24_23
| ~ spl24_37
| spl24_38 ),
inference(avatar_split_clause,[],[f61,f415,f407,f299]) ).
fof(f422,plain,
( ~ spl24_2
| ~ spl24_25
| spl24_38 ),
inference(avatar_split_clause,[],[f54,f415,f311,f169]) ).
fof(f423,plain,
( ~ spl24_2
| ~ spl24_38
| spl24_25 ),
inference(avatar_split_clause,[],[f55,f311,f415,f169]) ).
fof(f424,plain,
( spl24_25
| spl24_38
| spl24_2 ),
inference(avatar_split_clause,[],[f56,f169,f415,f311]) ).
fof(f425,plain,
( ~ spl24_25
| ~ spl24_38
| spl24_2 ),
inference(avatar_split_clause,[],[f57,f169,f415,f311]) ).
cnf(s1,plain,
( spl24_1
| spl24_2 ),
inference(sat_conversion,[],[f172]) ).
cnf(s2,plain,
( ~ spl24_1
| ~ spl24_2 ),
inference(sat_conversion,[],[f173]) ).
cnf(s3,plain,
( ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f194]) ).
cnf(s4,plain,
( ~ spl24_3
| ~ spl24_4
| ~ spl24_5
| spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f195]) ).
cnf(s5,plain,
( ~ spl24_3
| ~ spl24_4
| spl24_5
| spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f196]) ).
cnf(s6,plain,
( ~ spl24_3
| ~ spl24_4
| spl24_5
| ~ spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f197]) ).
cnf(s7,plain,
( ~ spl24_3
| spl24_4
| spl24_5
| ~ spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f198]) ).
cnf(s8,plain,
( ~ spl24_3
| spl24_4
| spl24_5
| spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f199]) ).
cnf(s9,plain,
( ~ spl24_3
| spl24_4
| ~ spl24_5
| spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f200]) ).
cnf(s10,plain,
( ~ spl24_3
| spl24_4
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f201]) ).
cnf(s11,plain,
( spl24_3
| spl24_4
| ~ spl24_5
| ~ spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f202]) ).
cnf(s12,plain,
( spl24_3
| spl24_4
| ~ spl24_5
| spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f203]) ).
cnf(s13,plain,
( spl24_3
| spl24_4
| spl24_5
| spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f204]) ).
cnf(s14,plain,
( spl24_3
| spl24_4
| spl24_5
| ~ spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f205]) ).
cnf(s15,plain,
( spl24_3
| ~ spl24_4
| spl24_5
| ~ spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f206]) ).
cnf(s16,plain,
( spl24_3
| ~ spl24_4
| spl24_5
| spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f207]) ).
cnf(s17,plain,
( spl24_3
| ~ spl24_4
| ~ spl24_5
| spl24_6
| spl24_7 ),
inference(sat_conversion,[],[f208]) ).
cnf(s18,plain,
( spl24_3
| ~ spl24_4
| ~ spl24_5
| ~ spl24_6
| ~ spl24_7 ),
inference(sat_conversion,[],[f209]) ).
cnf(s19,plain,
( spl24_3
| ~ spl24_8
| ~ spl24_9 ),
inference(sat_conversion,[],[f218]) ).
cnf(s20,plain,
( ~ spl24_3
| ~ spl24_8
| spl24_9 ),
inference(sat_conversion,[],[f219]) ).
cnf(s21,plain,
( spl24_3
| spl24_8
| spl24_9 ),
inference(sat_conversion,[],[f220]) ).
cnf(s22,plain,
( ~ spl24_3
| spl24_8
| ~ spl24_9 ),
inference(sat_conversion,[],[f221]) ).
cnf(s23,plain,
( spl24_8
| ~ spl24_10
| ~ spl24_11 ),
inference(sat_conversion,[],[f230]) ).
cnf(s24,plain,
( ~ spl24_8
| ~ spl24_10
| spl24_11 ),
inference(sat_conversion,[],[f231]) ).
cnf(s25,plain,
( spl24_8
| spl24_10
| spl24_11 ),
inference(sat_conversion,[],[f232]) ).
cnf(s26,plain,
( ~ spl24_8
| spl24_10
| ~ spl24_11 ),
inference(sat_conversion,[],[f233]) ).
cnf(s27,plain,
( spl24_10
| ~ spl24_12
| ~ spl24_13 ),
inference(sat_conversion,[],[f242]) ).
cnf(s28,plain,
( ~ spl24_10
| ~ spl24_12
| spl24_13 ),
inference(sat_conversion,[],[f243]) ).
cnf(s29,plain,
( spl24_10
| spl24_12
| spl24_13 ),
inference(sat_conversion,[],[f244]) ).
cnf(s30,plain,
( ~ spl24_10
| spl24_12
| ~ spl24_13 ),
inference(sat_conversion,[],[f245]) ).
cnf(s31,plain,
( spl24_12
| ~ spl24_14
| ~ spl24_15 ),
inference(sat_conversion,[],[f254]) ).
cnf(s32,plain,
( ~ spl24_12
| ~ spl24_14
| spl24_15 ),
inference(sat_conversion,[],[f255]) ).
cnf(s33,plain,
( spl24_12
| spl24_14
| spl24_15 ),
inference(sat_conversion,[],[f256]) ).
cnf(s34,plain,
( ~ spl24_12
| spl24_14
| ~ spl24_15 ),
inference(sat_conversion,[],[f257]) ).
cnf(s35,plain,
( spl24_14
| ~ spl24_16
| ~ spl24_17 ),
inference(sat_conversion,[],[f266]) ).
cnf(s36,plain,
( ~ spl24_14
| ~ spl24_16
| spl24_17 ),
inference(sat_conversion,[],[f267]) ).
cnf(s37,plain,
( spl24_14
| spl24_16
| spl24_17 ),
inference(sat_conversion,[],[f268]) ).
cnf(s38,plain,
( ~ spl24_14
| spl24_16
| ~ spl24_17 ),
inference(sat_conversion,[],[f269]) ).
cnf(s39,plain,
( spl24_16
| ~ spl24_18
| ~ spl24_19 ),
inference(sat_conversion,[],[f278]) ).
cnf(s40,plain,
( ~ spl24_16
| ~ spl24_18
| spl24_19 ),
inference(sat_conversion,[],[f279]) ).
cnf(s41,plain,
( spl24_16
| spl24_18
| spl24_19 ),
inference(sat_conversion,[],[f280]) ).
cnf(s42,plain,
( ~ spl24_16
| spl24_18
| ~ spl24_19 ),
inference(sat_conversion,[],[f281]) ).
cnf(s43,plain,
( spl24_18
| ~ spl24_20
| ~ spl24_21 ),
inference(sat_conversion,[],[f290]) ).
cnf(s44,plain,
( ~ spl24_18
| ~ spl24_20
| spl24_21 ),
inference(sat_conversion,[],[f291]) ).
cnf(s45,plain,
( spl24_18
| spl24_20
| spl24_21 ),
inference(sat_conversion,[],[f292]) ).
cnf(s46,plain,
( ~ spl24_18
| spl24_20
| ~ spl24_21 ),
inference(sat_conversion,[],[f293]) ).
cnf(s47,plain,
( spl24_20
| ~ spl24_22
| ~ spl24_23 ),
inference(sat_conversion,[],[f302]) ).
cnf(s48,plain,
( ~ spl24_20
| ~ spl24_22
| spl24_23 ),
inference(sat_conversion,[],[f303]) ).
cnf(s49,plain,
( spl24_20
| spl24_22
| spl24_23 ),
inference(sat_conversion,[],[f304]) ).
cnf(s50,plain,
( ~ spl24_20
| spl24_22
| ~ spl24_23 ),
inference(sat_conversion,[],[f305]) ).
cnf(s51,plain,
( spl24_22
| ~ spl24_24
| ~ spl24_25 ),
inference(sat_conversion,[],[f314]) ).
cnf(s52,plain,
( ~ spl24_22
| ~ spl24_24
| spl24_25 ),
inference(sat_conversion,[],[f315]) ).
cnf(s53,plain,
( spl24_22
| spl24_24
| spl24_25 ),
inference(sat_conversion,[],[f316]) ).
cnf(s54,plain,
( ~ spl24_22
| spl24_24
| ~ spl24_25 ),
inference(sat_conversion,[],[f317]) ).
cnf(s55,plain,
( ~ spl24_1
| spl24_24
| ~ spl24_26 ),
inference(sat_conversion,[],[f322]) ).
cnf(s56,plain,
( spl24_1
| ~ spl24_24
| ~ spl24_26 ),
inference(sat_conversion,[],[f323]) ).
cnf(s57,plain,
( spl24_1
| spl24_24
| spl24_26 ),
inference(sat_conversion,[],[f324]) ).
cnf(s58,plain,
( ~ spl24_1
| ~ spl24_24
| spl24_26 ),
inference(sat_conversion,[],[f325]) ).
cnf(s59,plain,
( ~ spl24_7
| spl24_26
| ~ spl24_27 ),
inference(sat_conversion,[],[f330]) ).
cnf(s60,plain,
( spl24_7
| ~ spl24_26
| ~ spl24_27 ),
inference(sat_conversion,[],[f331]) ).
cnf(s61,plain,
( spl24_7
| spl24_26
| spl24_27 ),
inference(sat_conversion,[],[f332]) ).
cnf(s62,plain,
( ~ spl24_7
| ~ spl24_26
| spl24_27 ),
inference(sat_conversion,[],[f333]) ).
cnf(s63,plain,
( ~ spl24_6
| spl24_27
| ~ spl24_28 ),
inference(sat_conversion,[],[f338]) ).
cnf(s64,plain,
( spl24_6
| ~ spl24_27
| ~ spl24_28 ),
inference(sat_conversion,[],[f339]) ).
cnf(s65,plain,
( spl24_6
| spl24_27
| spl24_28 ),
inference(sat_conversion,[],[f340]) ).
cnf(s66,plain,
( ~ spl24_6
| ~ spl24_27
| spl24_28 ),
inference(sat_conversion,[],[f341]) ).
cnf(s67,plain,
( ~ spl24_5
| spl24_28
| ~ spl24_29 ),
inference(sat_conversion,[],[f346]) ).
cnf(s68,plain,
( spl24_5
| ~ spl24_28
| ~ spl24_29 ),
inference(sat_conversion,[],[f347]) ).
cnf(s69,plain,
( spl24_5
| spl24_28
| spl24_29 ),
inference(sat_conversion,[],[f348]) ).
cnf(s70,plain,
( ~ spl24_5
| ~ spl24_28
| spl24_29 ),
inference(sat_conversion,[],[f349]) ).
cnf(s71,plain,
( ~ spl24_4
| spl24_29
| ~ spl24_30 ),
inference(sat_conversion,[],[f354]) ).
cnf(s72,plain,
( spl24_4
| ~ spl24_29
| ~ spl24_30 ),
inference(sat_conversion,[],[f355]) ).
cnf(s73,plain,
( spl24_4
| spl24_29
| spl24_30 ),
inference(sat_conversion,[],[f356]) ).
cnf(s74,plain,
( ~ spl24_4
| ~ spl24_29
| spl24_30 ),
inference(sat_conversion,[],[f357]) ).
cnf(s75,plain,
( ~ spl24_9
| spl24_30
| ~ spl24_31 ),
inference(sat_conversion,[],[f362]) ).
cnf(s76,plain,
( spl24_9
| ~ spl24_30
| ~ spl24_31 ),
inference(sat_conversion,[],[f363]) ).
cnf(s77,plain,
( spl24_9
| spl24_30
| spl24_31 ),
inference(sat_conversion,[],[f364]) ).
cnf(s78,plain,
( ~ spl24_9
| ~ spl24_30
| spl24_31 ),
inference(sat_conversion,[],[f365]) ).
cnf(s79,plain,
( ~ spl24_11
| spl24_31
| ~ spl24_32 ),
inference(sat_conversion,[],[f370]) ).
cnf(s80,plain,
( spl24_11
| ~ spl24_31
| ~ spl24_32 ),
inference(sat_conversion,[],[f371]) ).
cnf(s81,plain,
( spl24_11
| spl24_31
| spl24_32 ),
inference(sat_conversion,[],[f372]) ).
cnf(s82,plain,
( ~ spl24_11
| ~ spl24_31
| spl24_32 ),
inference(sat_conversion,[],[f373]) ).
cnf(s83,plain,
( ~ spl24_13
| spl24_32
| ~ spl24_33 ),
inference(sat_conversion,[],[f378]) ).
cnf(s84,plain,
( spl24_13
| ~ spl24_32
| ~ spl24_33 ),
inference(sat_conversion,[],[f379]) ).
cnf(s85,plain,
( spl24_13
| spl24_32
| spl24_33 ),
inference(sat_conversion,[],[f380]) ).
cnf(s86,plain,
( ~ spl24_13
| ~ spl24_32
| spl24_33 ),
inference(sat_conversion,[],[f381]) ).
cnf(s87,plain,
( ~ spl24_15
| spl24_33
| ~ spl24_34 ),
inference(sat_conversion,[],[f386]) ).
cnf(s88,plain,
( spl24_15
| ~ spl24_33
| ~ spl24_34 ),
inference(sat_conversion,[],[f387]) ).
cnf(s89,plain,
( spl24_15
| spl24_33
| spl24_34 ),
inference(sat_conversion,[],[f388]) ).
cnf(s90,plain,
( ~ spl24_15
| ~ spl24_33
| spl24_34 ),
inference(sat_conversion,[],[f389]) ).
cnf(s91,plain,
( ~ spl24_17
| spl24_34
| ~ spl24_35 ),
inference(sat_conversion,[],[f394]) ).
cnf(s92,plain,
( spl24_17
| ~ spl24_34
| ~ spl24_35 ),
inference(sat_conversion,[],[f395]) ).
cnf(s93,plain,
( spl24_17
| spl24_34
| spl24_35 ),
inference(sat_conversion,[],[f396]) ).
cnf(s94,plain,
( ~ spl24_17
| ~ spl24_34
| spl24_35 ),
inference(sat_conversion,[],[f397]) ).
cnf(s95,plain,
( ~ spl24_19
| spl24_35
| ~ spl24_36 ),
inference(sat_conversion,[],[f402]) ).
cnf(s96,plain,
( spl24_19
| ~ spl24_35
| ~ spl24_36 ),
inference(sat_conversion,[],[f403]) ).
cnf(s97,plain,
( spl24_19
| spl24_35
| spl24_36 ),
inference(sat_conversion,[],[f404]) ).
cnf(s98,plain,
( ~ spl24_19
| ~ spl24_35
| spl24_36 ),
inference(sat_conversion,[],[f405]) ).
cnf(s99,plain,
( ~ spl24_21
| spl24_36
| ~ spl24_37 ),
inference(sat_conversion,[],[f410]) ).
cnf(s100,plain,
( spl24_21
| ~ spl24_36
| ~ spl24_37 ),
inference(sat_conversion,[],[f411]) ).
cnf(s101,plain,
( spl24_21
| spl24_36
| spl24_37 ),
inference(sat_conversion,[],[f412]) ).
cnf(s102,plain,
( ~ spl24_21
| ~ spl24_36
| spl24_37 ),
inference(sat_conversion,[],[f413]) ).
cnf(s103,plain,
( ~ spl24_23
| spl24_37
| ~ spl24_38 ),
inference(sat_conversion,[],[f418]) ).
cnf(s104,plain,
( spl24_23
| ~ spl24_37
| ~ spl24_38 ),
inference(sat_conversion,[],[f419]) ).
cnf(s105,plain,
( spl24_23
| spl24_37
| spl24_38 ),
inference(sat_conversion,[],[f420]) ).
cnf(s106,plain,
( ~ spl24_23
| ~ spl24_37
| spl24_38 ),
inference(sat_conversion,[],[f421]) ).
cnf(s107,plain,
( ~ spl24_2
| ~ spl24_25
| spl24_38 ),
inference(sat_conversion,[],[f422]) ).
cnf(s108,plain,
( ~ spl24_2
| spl24_25
| ~ spl24_38 ),
inference(sat_conversion,[],[f423]) ).
cnf(s109,plain,
( spl24_2
| spl24_25
| spl24_38 ),
inference(sat_conversion,[],[f424]) ).
cnf(s110,plain,
( spl24_2
| ~ spl24_25
| ~ spl24_38 ),
inference(sat_conversion,[],[f425]) ).
cnf(s3403,plain,
( spl24_2
| spl24_26
| ~ spl24_24 ),
inference(rat,[],[s1,s58]) ).
cnf(s3404,plain,
( spl24_2
| ~ spl24_26
| spl24_24 ),
inference(rat,[],[s1,s55]) ).
cnf(s3405,plain,
( ~ spl24_2
| spl24_26
| spl24_24 ),
inference(rat,[],[s2,s57]) ).
cnf(s3406,plain,
( ~ spl24_2
| ~ spl24_26
| ~ spl24_24 ),
inference(rat,[],[s2,s56]) ).
cnf(s3407,plain,
( ~ spl24_25
| ~ spl24_38
| spl24_26
| spl24_24 ),
inference(rat,[],[s110,s3405]) ).
cnf(s3408,plain,
( ~ spl24_25
| ~ spl24_38
| ~ spl24_26
| ~ spl24_24 ),
inference(rat,[],[s110,s3406]) ).
cnf(s3409,plain,
( spl24_25
| spl24_38
| spl24_26
| spl24_24 ),
inference(rat,[],[s109,s3405]) ).
cnf(s3410,plain,
( spl24_25
| spl24_38
| ~ spl24_26
| ~ spl24_24 ),
inference(rat,[],[s109,s3406]) ).
cnf(s3411,plain,
( spl24_26
| ~ spl24_24
| spl24_25
| ~ spl24_38 ),
inference(rat,[],[s3403,s108]) ).
cnf(s3412,plain,
( spl24_26
| ~ spl24_24
| ~ spl24_25
| spl24_38 ),
inference(rat,[],[s3403,s107]) ).
cnf(s3413,plain,
( ~ spl24_26
| spl24_24
| spl24_25
| ~ spl24_38 ),
inference(rat,[],[s3404,s108]) ).
cnf(s3414,plain,
( ~ spl24_26
| spl24_24
| ~ spl24_25
| spl24_38 ),
inference(rat,[],[s3404,s107]) ).
cnf(s3415,plain,
( ~ spl24_10
| ~ spl24_11
| ~ spl24_3
| spl24_9 ),
inference(rat,[],[s23,s20]) ).
cnf(s3416,plain,
( ~ spl24_10
| ~ spl24_11
| ~ spl24_9
| spl24_3 ),
inference(rat,[],[s23,s19]) ).
cnf(s3417,plain,
( spl24_3
| spl24_9
| ~ spl24_11
| spl24_10 ),
inference(rat,[],[s21,s26]) ).
cnf(s3418,plain,
( spl24_3
| spl24_9
| ~ spl24_10
| spl24_11 ),
inference(rat,[],[s21,s24]) ).
cnf(s3419,plain,
( spl24_10
| spl24_11
| ~ spl24_3
| spl24_9 ),
inference(rat,[],[s25,s20]) ).
cnf(s3420,plain,
( spl24_10
| spl24_11
| ~ spl24_9
| spl24_3 ),
inference(rat,[],[s25,s19]) ).
cnf(s3421,plain,
( ~ spl24_9
| ~ spl24_3
| ~ spl24_11
| spl24_10 ),
inference(rat,[],[s22,s26]) ).
cnf(s3422,plain,
( ~ spl24_9
| ~ spl24_3
| ~ spl24_10
| spl24_11 ),
inference(rat,[],[s22,s24]) ).
cnf(s3423,plain,
( ~ spl24_14
| ~ spl24_15
| spl24_13
| ~ spl24_10 ),
inference(rat,[],[s31,s28]) ).
cnf(s3424,plain,
( ~ spl24_14
| ~ spl24_15
| ~ spl24_13
| spl24_10 ),
inference(rat,[],[s31,s27]) ).
cnf(s3425,plain,
( spl24_14
| spl24_15
| spl24_13
| ~ spl24_10 ),
inference(rat,[],[s33,s28]) ).
cnf(s3426,plain,
( spl24_14
| spl24_15
| ~ spl24_13
| spl24_10 ),
inference(rat,[],[s33,s27]) ).
cnf(s3427,plain,
( spl24_13
| spl24_10
| spl24_14
| ~ spl24_15 ),
inference(rat,[],[s29,s34]) ).
cnf(s3428,plain,
( spl24_13
| spl24_10
| ~ spl24_14
| spl24_15 ),
inference(rat,[],[s29,s32]) ).
cnf(s3429,plain,
( ~ spl24_13
| ~ spl24_10
| spl24_14
| ~ spl24_15 ),
inference(rat,[],[s30,s34]) ).
cnf(s3430,plain,
( ~ spl24_13
| ~ spl24_10
| ~ spl24_14
| spl24_15 ),
inference(rat,[],[s30,s32]) ).
cnf(s3431,plain,
( ~ spl24_18
| ~ spl24_19
| ~ spl24_17
| spl24_14 ),
inference(rat,[],[s39,s35]) ).
cnf(s3432,plain,
( ~ spl24_18
| ~ spl24_19
| spl24_17
| ~ spl24_14 ),
inference(rat,[],[s39,s36]) ).
cnf(s3433,plain,
( spl24_18
| spl24_19
| ~ spl24_17
| spl24_14 ),
inference(rat,[],[s41,s35]) ).
cnf(s3434,plain,
( spl24_18
| spl24_19
| spl24_17
| ~ spl24_14 ),
inference(rat,[],[s41,s36]) ).
cnf(s3435,plain,
( ~ spl24_17
| ~ spl24_14
| spl24_18
| ~ spl24_19 ),
inference(rat,[],[s38,s42]) ).
cnf(s3436,plain,
( ~ spl24_17
| ~ spl24_14
| ~ spl24_18
| spl24_19 ),
inference(rat,[],[s38,s40]) ).
cnf(s3437,plain,
( spl24_17
| spl24_14
| spl24_18
| ~ spl24_19 ),
inference(rat,[],[s37,s42]) ).
cnf(s3438,plain,
( spl24_17
| spl24_14
| ~ spl24_18
| spl24_19 ),
inference(rat,[],[s37,s40]) ).
cnf(s3439,plain,
( spl24_22
| spl24_23
| ~ spl24_18
| spl24_21 ),
inference(rat,[],[s49,s44]) ).
cnf(s3440,plain,
( spl24_22
| spl24_23
| ~ spl24_21
| spl24_18 ),
inference(rat,[],[s49,s43]) ).
cnf(s3441,plain,
( ~ spl24_22
| ~ spl24_23
| ~ spl24_18
| spl24_21 ),
inference(rat,[],[s47,s44]) ).
cnf(s3442,plain,
( ~ spl24_22
| ~ spl24_23
| ~ spl24_21
| spl24_18 ),
inference(rat,[],[s47,s43]) ).
cnf(s3443,plain,
( spl24_21
| spl24_18
| ~ spl24_22
| spl24_23 ),
inference(rat,[],[s45,s48]) ).
cnf(s3444,plain,
( spl24_21
| spl24_18
| spl24_22
| ~ spl24_23 ),
inference(rat,[],[s45,s50]) ).
cnf(s3445,plain,
( ~ spl24_18
| ~ spl24_21
| ~ spl24_22
| spl24_23 ),
inference(rat,[],[s46,s48]) ).
cnf(s3446,plain,
( ~ spl24_18
| ~ spl24_21
| spl24_22
| ~ spl24_23 ),
inference(rat,[],[s46,s50]) ).
cnf(s3447,plain,
( ~ spl24_28
| ~ spl24_6
| spl24_26
| ~ spl24_7 ),
inference(rat,[],[s63,s59]) ).
cnf(s3448,plain,
( ~ spl24_28
| ~ spl24_6
| ~ spl24_26
| spl24_7 ),
inference(rat,[],[s63,s60]) ).
cnf(s3449,plain,
( spl24_26
| spl24_7
| ~ spl24_28
| spl24_6 ),
inference(rat,[],[s61,s64]) ).
cnf(s3450,plain,
( spl24_26
| spl24_7
| spl24_28
| ~ spl24_6 ),
inference(rat,[],[s61,s66]) ).
cnf(s3451,plain,
( spl24_28
| spl24_6
| spl24_26
| ~ spl24_7 ),
inference(rat,[],[s65,s59]) ).
cnf(s3452,plain,
( spl24_28
| spl24_6
| ~ spl24_26
| spl24_7 ),
inference(rat,[],[s65,s60]) ).
cnf(s3453,plain,
( ~ spl24_26
| ~ spl24_7
| ~ spl24_28
| spl24_6 ),
inference(rat,[],[s62,s64]) ).
cnf(s3454,plain,
( ~ spl24_26
| ~ spl24_7
| spl24_28
| ~ spl24_6 ),
inference(rat,[],[s62,s66]) ).
cnf(s3455,plain,
( spl24_30
| spl24_4
| ~ spl24_28
| spl24_5 ),
inference(rat,[],[s73,s68]) ).
cnf(s3456,plain,
( spl24_30
| spl24_4
| spl24_28
| ~ spl24_5 ),
inference(rat,[],[s73,s67]) ).
cnf(s3457,plain,
( ~ spl24_30
| ~ spl24_4
| ~ spl24_28
| spl24_5 ),
inference(rat,[],[s71,s68]) ).
cnf(s3458,plain,
( ~ spl24_30
| ~ spl24_4
| spl24_28
| ~ spl24_5 ),
inference(rat,[],[s71,s67]) ).
cnf(s3459,plain,
( spl24_28
| spl24_5
| ~ spl24_30
| spl24_4 ),
inference(rat,[],[s69,s72]) ).
cnf(s3460,plain,
( spl24_28
| spl24_5
| spl24_30
| ~ spl24_4 ),
inference(rat,[],[s69,s74]) ).
cnf(s3461,plain,
( ~ spl24_28
| ~ spl24_5
| ~ spl24_30
| spl24_4 ),
inference(rat,[],[s70,s72]) ).
cnf(s3462,plain,
( ~ spl24_28
| ~ spl24_5
| spl24_30
| ~ spl24_4 ),
inference(rat,[],[s70,s74]) ).
cnf(s3463,plain,
( spl24_32
| spl24_11
| ~ spl24_30
| spl24_9 ),
inference(rat,[],[s81,s76]) ).
cnf(s3464,plain,
( spl24_32
| spl24_11
| spl24_30
| ~ spl24_9 ),
inference(rat,[],[s81,s75]) ).
cnf(s3465,plain,
( ~ spl24_32
| ~ spl24_11
| ~ spl24_30
| spl24_9 ),
inference(rat,[],[s79,s76]) ).
cnf(s3466,plain,
( ~ spl24_32
| ~ spl24_11
| spl24_30
| ~ spl24_9 ),
inference(rat,[],[s79,s75]) ).
cnf(s3467,plain,
( ~ spl24_30
| ~ spl24_9
| spl24_32
| ~ spl24_11 ),
inference(rat,[],[s78,s82]) ).
cnf(s3468,plain,
( ~ spl24_30
| ~ spl24_9
| ~ spl24_32
| spl24_11 ),
inference(rat,[],[s78,s80]) ).
cnf(s3469,plain,
( spl24_30
| spl24_9
| spl24_32
| ~ spl24_11 ),
inference(rat,[],[s77,s82]) ).
cnf(s3470,plain,
( spl24_30
| spl24_9
| ~ spl24_32
| spl24_11 ),
inference(rat,[],[s77,s80]) ).
cnf(s3471,plain,
( spl24_34
| spl24_15
| spl24_32
| ~ spl24_13 ),
inference(rat,[],[s89,s83]) ).
cnf(s3472,plain,
( spl24_34
| spl24_15
| ~ spl24_32
| spl24_13 ),
inference(rat,[],[s89,s84]) ).
cnf(s3473,plain,
( ~ spl24_34
| ~ spl24_15
| spl24_32
| ~ spl24_13 ),
inference(rat,[],[s87,s83]) ).
cnf(s3474,plain,
( ~ spl24_34
| ~ spl24_15
| ~ spl24_32
| spl24_13 ),
inference(rat,[],[s87,s84]) ).
cnf(s3475,plain,
( ~ spl24_32
| ~ spl24_13
| spl24_34
| ~ spl24_15 ),
inference(rat,[],[s86,s90]) ).
cnf(s3476,plain,
( ~ spl24_32
| ~ spl24_13
| ~ spl24_34
| spl24_15 ),
inference(rat,[],[s86,s88]) ).
cnf(s3477,plain,
( spl24_32
| spl24_13
| spl24_34
| ~ spl24_15 ),
inference(rat,[],[s85,s90]) ).
cnf(s3478,plain,
( spl24_32
| spl24_13
| ~ spl24_34
| spl24_15 ),
inference(rat,[],[s85,s88]) ).
cnf(s3479,plain,
( spl24_36
| spl24_19
| spl24_34
| ~ spl24_17 ),
inference(rat,[],[s97,s91]) ).
cnf(s3480,plain,
( spl24_36
| spl24_19
| ~ spl24_34
| spl24_17 ),
inference(rat,[],[s97,s92]) ).
cnf(s3481,plain,
( ~ spl24_36
| ~ spl24_19
| spl24_34
| ~ spl24_17 ),
inference(rat,[],[s95,s91]) ).
cnf(s3482,plain,
( ~ spl24_36
| ~ spl24_19
| ~ spl24_34
| spl24_17 ),
inference(rat,[],[s95,s92]) ).
cnf(s3483,plain,
( ~ spl24_34
| ~ spl24_17
| spl24_36
| ~ spl24_19 ),
inference(rat,[],[s94,s98]) ).
cnf(s3484,plain,
( ~ spl24_34
| ~ spl24_17
| ~ spl24_36
| spl24_19 ),
inference(rat,[],[s94,s96]) ).
cnf(s3485,plain,
( spl24_34
| spl24_17
| spl24_36
| ~ spl24_19 ),
inference(rat,[],[s93,s98]) ).
cnf(s3486,plain,
( spl24_34
| spl24_17
| ~ spl24_36
| spl24_19 ),
inference(rat,[],[s93,s96]) ).
cnf(s3487,plain,
( ~ spl24_38
| ~ spl24_23
| spl24_36
| ~ spl24_21 ),
inference(rat,[],[s103,s99]) ).
cnf(s3488,plain,
( ~ spl24_38
| ~ spl24_23
| ~ spl24_36
| spl24_21 ),
inference(rat,[],[s103,s100]) ).
cnf(s3489,plain,
( spl24_38
| spl24_23
| spl24_36
| ~ spl24_21 ),
inference(rat,[],[s105,s99]) ).
cnf(s3490,plain,
( spl24_38
| spl24_23
| ~ spl24_36
| spl24_21 ),
inference(rat,[],[s105,s100]) ).
cnf(s3491,plain,
( ~ spl24_36
| ~ spl24_21
| ~ spl24_38
| spl24_23 ),
inference(rat,[],[s102,s104]) ).
cnf(s3492,plain,
( ~ spl24_36
| ~ spl24_21
| spl24_38
| ~ spl24_23 ),
inference(rat,[],[s102,s106]) ).
cnf(s3493,plain,
( spl24_21
| spl24_36
| ~ spl24_38
| spl24_23 ),
inference(rat,[],[s101,s104]) ).
cnf(s3494,plain,
( spl24_21
| spl24_36
| spl24_38
| ~ spl24_23 ),
inference(rat,[],[s101,s106]) ).
cnf(s3495,plain,
( ~ spl24_25
| ~ spl24_22
| ~ spl24_38
| ~ spl24_26 ),
inference(rat,[],[s54,s3408]) ).
cnf(s3496,plain,
( ~ spl24_25
| ~ spl24_22
| spl24_26
| spl24_38 ),
inference(rat,[],[s54,s3412]) ).
cnf(s3497,plain,
( spl24_25
| spl24_22
| spl24_38
| ~ spl24_26 ),
inference(rat,[],[s53,s3410]) ).
cnf(s3498,plain,
( spl24_25
| spl24_22
| spl24_26
| ~ spl24_38 ),
inference(rat,[],[s53,s3411]) ).
cnf(s3499,plain,
( ~ spl24_25
| spl24_22
| ~ spl24_38
| spl24_26 ),
inference(rat,[],[s51,s3407]) ).
cnf(s3500,plain,
( spl24_25
| ~ spl24_22
| spl24_38
| spl24_26 ),
inference(rat,[],[s52,s3409]) ).
cnf(s3501,plain,
( spl24_25
| ~ spl24_22
| ~ spl24_26
| ~ spl24_38 ),
inference(rat,[],[s52,s3413]) ).
cnf(s3502,plain,
( ~ spl24_25
| spl24_22
| ~ spl24_26
| spl24_38 ),
inference(rat,[],[s51,s3414]) ).
cnf(s3503,plain,
( ~ spl24_22
| ~ spl24_38
| ~ spl24_26 ),
inference(rat,[],[s3501,s3495]) ).
cnf(s3504,plain,
( spl24_22
| spl24_38
| ~ spl24_26 ),
inference(rat,[],[s3502,s3497]) ).
cnf(s3505,plain,
( spl24_22
| spl24_26
| ~ spl24_38 ),
inference(rat,[],[s3498,s3499]) ).
cnf(s3506,plain,
( ~ spl24_22
| spl24_38
| spl24_26 ),
inference(rat,[],[s3500,s3496]) ).
cnf(s3507,plain,
( ~ spl24_10
| ~ spl24_11
| ~ spl24_3
| ~ spl24_32
| spl24_30 ),
inference(rat,[],[s3415,s3466]) ).
cnf(s3508,plain,
( ~ spl24_10
| ~ spl24_11
| ~ spl24_3
| ~ spl24_30
| spl24_32 ),
inference(rat,[],[s3415,s3467]) ).
cnf(s3509,plain,
( spl24_3
| ~ spl24_11
| spl24_10
| ~ spl24_32
| spl24_30 ),
inference(rat,[],[s3417,s3466]) ).
cnf(s3510,plain,
( spl24_3
| ~ spl24_11
| spl24_10
| ~ spl24_30
| spl24_32 ),
inference(rat,[],[s3417,s3467]) ).
cnf(s3511,plain,
( spl24_3
| ~ spl24_10
| spl24_11
| spl24_32
| spl24_30 ),
inference(rat,[],[s3418,s3464]) ).
cnf(s3512,plain,
( spl24_3
| ~ spl24_10
| spl24_11
| ~ spl24_30
| ~ spl24_32 ),
inference(rat,[],[s3418,s3468]) ).
cnf(s3513,plain,
( spl24_10
| spl24_11
| ~ spl24_3
| spl24_32
| spl24_30 ),
inference(rat,[],[s3419,s3464]) ).
cnf(s3514,plain,
( spl24_10
| spl24_11
| ~ spl24_3
| ~ spl24_30
| ~ spl24_32 ),
inference(rat,[],[s3419,s3468]) ).
cnf(s3515,plain,
( spl24_32
| spl24_11
| ~ spl24_30
| spl24_10
| spl24_3 ),
inference(rat,[],[s3463,s3420]) ).
cnf(s3516,plain,
( spl24_32
| spl24_11
| ~ spl24_30
| ~ spl24_3
| ~ spl24_10 ),
inference(rat,[],[s3463,s3422]) ).
cnf(s3517,plain,
( ~ spl24_32
| ~ spl24_11
| ~ spl24_30
| ~ spl24_10
| spl24_3 ),
inference(rat,[],[s3465,s3416]) ).
cnf(s3518,plain,
( ~ spl24_32
| ~ spl24_11
| ~ spl24_30
| ~ spl24_3
| spl24_10 ),
inference(rat,[],[s3465,s3421]) ).
cnf(s3519,plain,
( spl24_30
| spl24_32
| ~ spl24_11
| ~ spl24_10
| spl24_3 ),
inference(rat,[],[s3469,s3416]) ).
cnf(s3520,plain,
( spl24_30
| spl24_32
| ~ spl24_11
| ~ spl24_3
| spl24_10 ),
inference(rat,[],[s3469,s3421]) ).
cnf(s3521,plain,
( spl24_30
| ~ spl24_32
| spl24_11
| spl24_10
| spl24_3 ),
inference(rat,[],[s3470,s3420]) ).
cnf(s3522,plain,
( spl24_30
| ~ spl24_32
| spl24_11
| ~ spl24_3
| ~ spl24_10 ),
inference(rat,[],[s3470,s3422]) ).
cnf(s3523,plain,
( ~ spl24_10
| ~ spl24_3
| ~ spl24_30
| spl24_32 ),
inference(rat,[],[s3516,s3508]) ).
cnf(s3524,plain,
( ~ spl24_10
| ~ spl24_3
| ~ spl24_32
| spl24_30 ),
inference(rat,[],[s3522,s3507]) ).
cnf(s3525,plain,
( spl24_3
| spl24_10
| ~ spl24_32
| spl24_30 ),
inference(rat,[],[s3509,s3521]) ).
cnf(s3526,plain,
( spl24_3
| spl24_10
| ~ spl24_30
| spl24_32 ),
inference(rat,[],[s3510,s3515]) ).
cnf(s3527,plain,
( ~ spl24_32
| ~ spl24_30
| ~ spl24_10
| spl24_3 ),
inference(rat,[],[s3517,s3512]) ).
cnf(s3528,plain,
( ~ spl24_32
| ~ spl24_30
| ~ spl24_3
| spl24_10 ),
inference(rat,[],[s3518,s3514]) ).
cnf(s3529,plain,
( spl24_30
| spl24_32
| ~ spl24_10
| spl24_3 ),
inference(rat,[],[s3519,s3511]) ).
cnf(s3530,plain,
( spl24_30
| spl24_32
| ~ spl24_3
| spl24_10 ),
inference(rat,[],[s3520,s3513]) ).
cnf(s3531,plain,
( ~ spl24_14
| ~ spl24_15
| ~ spl24_10
| ~ spl24_34
| spl24_32 ),
inference(rat,[],[s3423,s3473]) ).
cnf(s3532,plain,
( ~ spl24_14
| ~ spl24_15
| ~ spl24_10
| ~ spl24_32
| spl24_34 ),
inference(rat,[],[s3423,s3475]) ).
cnf(s3533,plain,
( spl24_14
| spl24_15
| ~ spl24_10
| spl24_34
| spl24_32 ),
inference(rat,[],[s3425,s3471]) ).
cnf(s3534,plain,
( spl24_14
| spl24_15
| ~ spl24_10
| ~ spl24_32
| ~ spl24_34 ),
inference(rat,[],[s3425,s3476]) ).
cnf(s3535,plain,
( spl24_10
| spl24_14
| ~ spl24_15
| ~ spl24_34
| spl24_32 ),
inference(rat,[],[s3427,s3473]) ).
cnf(s3536,plain,
( spl24_10
| spl24_14
| ~ spl24_15
| ~ spl24_32
| spl24_34 ),
inference(rat,[],[s3427,s3475]) ).
cnf(s3537,plain,
( spl24_10
| ~ spl24_14
| spl24_15
| spl24_34
| spl24_32 ),
inference(rat,[],[s3428,s3471]) ).
cnf(s3538,plain,
( spl24_10
| ~ spl24_14
| spl24_15
| ~ spl24_32
| ~ spl24_34 ),
inference(rat,[],[s3428,s3476]) ).
cnf(s3539,plain,
( spl24_34
| spl24_15
| ~ spl24_32
| spl24_14
| spl24_10 ),
inference(rat,[],[s3472,s3426]) ).
cnf(s3540,plain,
( spl24_34
| spl24_15
| ~ spl24_32
| ~ spl24_10
| ~ spl24_14 ),
inference(rat,[],[s3472,s3430]) ).
cnf(s3541,plain,
( ~ spl24_34
| ~ spl24_15
| ~ spl24_32
| ~ spl24_14
| spl24_10 ),
inference(rat,[],[s3474,s3424]) ).
cnf(s3542,plain,
( ~ spl24_34
| ~ spl24_15
| ~ spl24_32
| ~ spl24_10
| spl24_14 ),
inference(rat,[],[s3474,s3429]) ).
cnf(s3543,plain,
( spl24_32
| spl24_34
| ~ spl24_15
| ~ spl24_14
| spl24_10 ),
inference(rat,[],[s3477,s3424]) ).
cnf(s3544,plain,
( spl24_32
| spl24_34
| ~ spl24_15
| ~ spl24_10
| spl24_14 ),
inference(rat,[],[s3477,s3429]) ).
cnf(s3545,plain,
( spl24_32
| ~ spl24_34
| spl24_15
| spl24_14
| spl24_10 ),
inference(rat,[],[s3478,s3426]) ).
cnf(s3546,plain,
( spl24_32
| ~ spl24_34
| spl24_15
| ~ spl24_10
| ~ spl24_14 ),
inference(rat,[],[s3478,s3430]) ).
cnf(s3547,plain,
( spl24_10
| spl24_14
| ~ spl24_34
| spl24_32 ),
inference(rat,[],[s3545,s3535]) ).
cnf(s3548,plain,
( ~ spl24_14
| ~ spl24_10
| ~ spl24_34
| spl24_32 ),
inference(rat,[],[s3546,s3531]) ).
cnf(s3549,plain,
( ~ spl24_14
| ~ spl24_10
| ~ spl24_32
| spl24_34 ),
inference(rat,[],[s3532,s3540]) ).
cnf(s3550,plain,
( spl24_10
| spl24_14
| ~ spl24_32
| spl24_34 ),
inference(rat,[],[s3536,s3539]) ).
cnf(s3551,plain,
( ~ spl24_34
| ~ spl24_32
| ~ spl24_14
| spl24_10 ),
inference(rat,[],[s3541,s3538]) ).
cnf(s3552,plain,
( ~ spl24_34
| ~ spl24_32
| ~ spl24_10
| spl24_14 ),
inference(rat,[],[s3542,s3534]) ).
cnf(s3553,plain,
( spl24_32
| spl24_34
| ~ spl24_14
| spl24_10 ),
inference(rat,[],[s3543,s3537]) ).
cnf(s3554,plain,
( spl24_32
| spl24_34
| ~ spl24_10
| spl24_14 ),
inference(rat,[],[s3544,s3533]) ).
cnf(s3555,plain,
( spl24_3
| ~ spl24_32
| spl24_30
| ~ spl24_14
| spl24_34 ),
inference(rat,[],[s3525,s3549]) ).
cnf(s3556,plain,
( spl24_3
| ~ spl24_32
| spl24_30
| ~ spl24_34
| spl24_14 ),
inference(rat,[],[s3525,s3552]) ).
cnf(s3557,plain,
( spl24_3
| ~ spl24_30
| spl24_32
| ~ spl24_14
| ~ spl24_34 ),
inference(rat,[],[s3526,s3548]) ).
cnf(s3558,plain,
( spl24_3
| ~ spl24_30
| spl24_32
| spl24_34
| spl24_14 ),
inference(rat,[],[s3526,s3554]) ).
cnf(s3559,plain,
( ~ spl24_32
| ~ spl24_30
| ~ spl24_3
| ~ spl24_14
| spl24_34 ),
inference(rat,[],[s3528,s3549]) ).
cnf(s3560,plain,
( ~ spl24_32
| ~ spl24_30
| ~ spl24_3
| ~ spl24_34
| spl24_14 ),
inference(rat,[],[s3528,s3552]) ).
cnf(s3561,plain,
( spl24_30
| spl24_32
| ~ spl24_3
| ~ spl24_14
| ~ spl24_34 ),
inference(rat,[],[s3530,s3548]) ).
cnf(s3562,plain,
( spl24_30
| spl24_32
| ~ spl24_3
| spl24_34
| spl24_14 ),
inference(rat,[],[s3530,s3554]) ).
cnf(s3563,plain,
( spl24_14
| ~ spl24_34
| spl24_32
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3547,s3523]) ).
cnf(s3564,plain,
( spl24_14
| ~ spl24_34
| spl24_32
| spl24_30
| spl24_3 ),
inference(rat,[],[s3547,s3529]) ).
cnf(s3565,plain,
( spl24_14
| ~ spl24_32
| spl24_34
| ~ spl24_3
| spl24_30 ),
inference(rat,[],[s3550,s3524]) ).
cnf(s3566,plain,
( spl24_14
| ~ spl24_32
| spl24_34
| ~ spl24_30
| spl24_3 ),
inference(rat,[],[s3550,s3527]) ).
cnf(s3567,plain,
( ~ spl24_34
| ~ spl24_32
| ~ spl24_14
| ~ spl24_3
| spl24_30 ),
inference(rat,[],[s3551,s3524]) ).
cnf(s3568,plain,
( ~ spl24_34
| ~ spl24_32
| ~ spl24_14
| ~ spl24_30
| spl24_3 ),
inference(rat,[],[s3551,s3527]) ).
cnf(s3569,plain,
( spl24_32
| spl24_34
| ~ spl24_14
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3553,s3523]) ).
cnf(s3570,plain,
( spl24_32
| spl24_34
| ~ spl24_14
| spl24_30
| spl24_3 ),
inference(rat,[],[s3553,s3529]) ).
cnf(s3571,plain,
( spl24_3
| spl24_30
| ~ spl24_34
| spl24_14 ),
inference(rat,[],[s3564,s3556]) ).
cnf(s3572,plain,
( spl24_3
| ~ spl24_30
| spl24_34
| spl24_14 ),
inference(rat,[],[s3566,s3558]) ).
cnf(s3573,plain,
( spl24_3
| ~ spl24_30
| ~ spl24_14
| ~ spl24_34 ),
inference(rat,[],[s3568,s3557]) ).
cnf(s3574,plain,
( spl24_3
| spl24_30
| ~ spl24_14
| spl24_34 ),
inference(rat,[],[s3570,s3555]) ).
cnf(s3575,plain,
( spl24_30
| ~ spl24_3
| ~ spl24_14
| ~ spl24_34 ),
inference(rat,[],[s3561,s3567]) ).
cnf(s3576,plain,
( spl24_30
| ~ spl24_3
| spl24_34
| spl24_14 ),
inference(rat,[],[s3562,s3565]) ).
cnf(s3577,plain,
( spl24_14
| ~ spl24_34
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3563,s3560]) ).
cnf(s3578,plain,
( spl24_34
| ~ spl24_14
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3569,s3559]) ).
cnf(s3579,plain,
( ~ spl24_18
| ~ spl24_19
| ~ spl24_14
| ~ spl24_36
| spl24_34 ),
inference(rat,[],[s3432,s3481]) ).
cnf(s3580,plain,
( ~ spl24_18
| ~ spl24_19
| ~ spl24_14
| ~ spl24_34
| spl24_36 ),
inference(rat,[],[s3432,s3483]) ).
cnf(s3581,plain,
( spl24_18
| spl24_19
| ~ spl24_14
| spl24_36
| spl24_34 ),
inference(rat,[],[s3434,s3479]) ).
cnf(s3582,plain,
( spl24_18
| spl24_19
| ~ spl24_14
| ~ spl24_34
| ~ spl24_36 ),
inference(rat,[],[s3434,s3484]) ).
cnf(s3583,plain,
( spl24_14
| spl24_18
| ~ spl24_19
| ~ spl24_36
| spl24_34 ),
inference(rat,[],[s3437,s3481]) ).
cnf(s3584,plain,
( spl24_14
| spl24_18
| ~ spl24_19
| ~ spl24_34
| spl24_36 ),
inference(rat,[],[s3437,s3483]) ).
cnf(s3585,plain,
( spl24_14
| ~ spl24_18
| spl24_19
| spl24_36
| spl24_34 ),
inference(rat,[],[s3438,s3479]) ).
cnf(s3586,plain,
( spl24_14
| ~ spl24_18
| spl24_19
| ~ spl24_34
| ~ spl24_36 ),
inference(rat,[],[s3438,s3484]) ).
cnf(s3587,plain,
( spl24_36
| spl24_19
| ~ spl24_34
| spl24_18
| spl24_14 ),
inference(rat,[],[s3480,s3433]) ).
cnf(s3588,plain,
( spl24_36
| spl24_19
| ~ spl24_34
| ~ spl24_14
| ~ spl24_18 ),
inference(rat,[],[s3480,s3436]) ).
cnf(s3589,plain,
( ~ spl24_36
| ~ spl24_19
| ~ spl24_34
| ~ spl24_18
| spl24_14 ),
inference(rat,[],[s3482,s3431]) ).
cnf(s3590,plain,
( ~ spl24_36
| ~ spl24_19
| ~ spl24_34
| ~ spl24_14
| spl24_18 ),
inference(rat,[],[s3482,s3435]) ).
cnf(s3591,plain,
( spl24_34
| spl24_36
| ~ spl24_19
| ~ spl24_18
| spl24_14 ),
inference(rat,[],[s3485,s3431]) ).
cnf(s3592,plain,
( spl24_34
| spl24_36
| ~ spl24_19
| ~ spl24_14
| spl24_18 ),
inference(rat,[],[s3485,s3435]) ).
cnf(s3593,plain,
( spl24_34
| ~ spl24_36
| spl24_19
| spl24_18
| spl24_14 ),
inference(rat,[],[s3486,s3433]) ).
cnf(s3594,plain,
( spl24_34
| ~ spl24_36
| spl24_19
| ~ spl24_14
| ~ spl24_18 ),
inference(rat,[],[s3486,s3436]) ).
cnf(s3595,plain,
( spl24_14
| spl24_18
| ~ spl24_36
| spl24_34 ),
inference(rat,[],[s3593,s3583]) ).
cnf(s3596,plain,
( ~ spl24_18
| ~ spl24_14
| ~ spl24_36
| spl24_34 ),
inference(rat,[],[s3594,s3579]) ).
cnf(s3597,plain,
( ~ spl24_18
| ~ spl24_14
| ~ spl24_34
| spl24_36 ),
inference(rat,[],[s3580,s3588]) ).
cnf(s3598,plain,
( spl24_14
| spl24_18
| ~ spl24_34
| spl24_36 ),
inference(rat,[],[s3584,s3587]) ).
cnf(s3599,plain,
( ~ spl24_36
| ~ spl24_34
| ~ spl24_18
| spl24_14 ),
inference(rat,[],[s3589,s3586]) ).
cnf(s3600,plain,
( ~ spl24_36
| ~ spl24_34
| ~ spl24_14
| spl24_18 ),
inference(rat,[],[s3590,s3582]) ).
cnf(s3601,plain,
( spl24_34
| spl24_36
| ~ spl24_18
| spl24_14 ),
inference(rat,[],[s3591,s3585]) ).
cnf(s3602,plain,
( spl24_34
| spl24_36
| ~ spl24_14
| spl24_18 ),
inference(rat,[],[s3592,s3581]) ).
cnf(s3603,plain,
( spl24_3
| spl24_30
| ~ spl24_34
| ~ spl24_18
| spl24_36 ),
inference(rat,[],[s3571,s3597]) ).
cnf(s3604,plain,
( spl24_3
| spl24_30
| ~ spl24_34
| ~ spl24_36
| spl24_18 ),
inference(rat,[],[s3571,s3600]) ).
cnf(s3605,plain,
( spl24_3
| ~ spl24_30
| spl24_34
| ~ spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3572,s3596]) ).
cnf(s3606,plain,
( spl24_3
| ~ spl24_30
| spl24_34
| spl24_36
| spl24_18 ),
inference(rat,[],[s3572,s3602]) ).
cnf(s3607,plain,
( spl24_30
| ~ spl24_3
| spl24_34
| ~ spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3576,s3596]) ).
cnf(s3608,plain,
( spl24_30
| ~ spl24_3
| spl24_34
| spl24_36
| spl24_18 ),
inference(rat,[],[s3576,s3602]) ).
cnf(s3609,plain,
( ~ spl24_34
| ~ spl24_3
| ~ spl24_30
| ~ spl24_18
| spl24_36 ),
inference(rat,[],[s3577,s3597]) ).
cnf(s3610,plain,
( ~ spl24_34
| ~ spl24_3
| ~ spl24_30
| ~ spl24_36
| spl24_18 ),
inference(rat,[],[s3577,s3600]) ).
cnf(s3611,plain,
( spl24_18
| ~ spl24_36
| spl24_34
| spl24_3
| spl24_30 ),
inference(rat,[],[s3595,s3574]) ).
cnf(s3612,plain,
( spl24_18
| ~ spl24_36
| spl24_34
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3595,s3578]) ).
cnf(s3613,plain,
( spl24_18
| ~ spl24_34
| spl24_36
| spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3598,s3573]) ).
cnf(s3614,plain,
( spl24_18
| ~ spl24_34
| spl24_36
| spl24_30
| ~ spl24_3 ),
inference(rat,[],[s3598,s3575]) ).
cnf(s3615,plain,
( ~ spl24_36
| ~ spl24_34
| ~ spl24_18
| spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3599,s3573]) ).
cnf(s3616,plain,
( ~ spl24_36
| ~ spl24_34
| ~ spl24_18
| spl24_30
| ~ spl24_3 ),
inference(rat,[],[s3599,s3575]) ).
cnf(s3617,plain,
( spl24_34
| spl24_36
| ~ spl24_18
| spl24_3
| spl24_30 ),
inference(rat,[],[s3601,s3574]) ).
cnf(s3618,plain,
( spl24_34
| spl24_36
| ~ spl24_18
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3601,s3578]) ).
cnf(s3619,plain,
( spl24_3
| spl24_30
| ~ spl24_36
| spl24_18 ),
inference(rat,[],[s3611,s3604]) ).
cnf(s3620,plain,
( spl24_3
| ~ spl24_30
| spl24_36
| spl24_18 ),
inference(rat,[],[s3613,s3606]) ).
cnf(s3621,plain,
( spl24_30
| ~ spl24_3
| spl24_36
| spl24_18 ),
inference(rat,[],[s3614,s3608]) ).
cnf(s3622,plain,
( spl24_3
| ~ spl24_30
| ~ spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3615,s3605]) ).
cnf(s3623,plain,
( spl24_30
| ~ spl24_3
| ~ spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3616,s3607]) ).
cnf(s3624,plain,
( spl24_3
| spl24_30
| ~ spl24_18
| spl24_36 ),
inference(rat,[],[s3617,s3603]) ).
cnf(s3625,plain,
( ~ spl24_3
| ~ spl24_30
| ~ spl24_18
| spl24_36 ),
inference(rat,[],[s3618,s3609]) ).
cnf(s3626,plain,
( spl24_18
| ~ spl24_36
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3612,s3610]) ).
cnf(s3627,plain,
( spl24_22
| spl24_23
| ~ spl24_18
| spl24_38
| spl24_36 ),
inference(rat,[],[s3439,s3489]) ).
cnf(s3628,plain,
( spl24_22
| spl24_23
| ~ spl24_18
| ~ spl24_36
| ~ spl24_38 ),
inference(rat,[],[s3439,s3491]) ).
cnf(s3629,plain,
( ~ spl24_22
| ~ spl24_23
| ~ spl24_18
| ~ spl24_38
| spl24_36 ),
inference(rat,[],[s3441,s3487]) ).
cnf(s3630,plain,
( ~ spl24_22
| ~ spl24_23
| ~ spl24_18
| ~ spl24_36
| spl24_38 ),
inference(rat,[],[s3441,s3492]) ).
cnf(s3631,plain,
( spl24_18
| ~ spl24_22
| spl24_23
| spl24_38
| spl24_36 ),
inference(rat,[],[s3443,s3489]) ).
cnf(s3632,plain,
( spl24_18
| ~ spl24_22
| spl24_23
| ~ spl24_36
| ~ spl24_38 ),
inference(rat,[],[s3443,s3491]) ).
cnf(s3633,plain,
( spl24_18
| spl24_22
| ~ spl24_23
| ~ spl24_38
| spl24_36 ),
inference(rat,[],[s3444,s3487]) ).
cnf(s3634,plain,
( spl24_18
| spl24_22
| ~ spl24_23
| ~ spl24_36
| spl24_38 ),
inference(rat,[],[s3444,s3492]) ).
cnf(s3635,plain,
( ~ spl24_38
| ~ spl24_23
| ~ spl24_36
| ~ spl24_22
| spl24_18 ),
inference(rat,[],[s3488,s3442]) ).
cnf(s3636,plain,
( ~ spl24_38
| ~ spl24_23
| ~ spl24_36
| ~ spl24_18
| spl24_22 ),
inference(rat,[],[s3488,s3446]) ).
cnf(s3637,plain,
( spl24_38
| spl24_23
| ~ spl24_36
| spl24_22
| spl24_18 ),
inference(rat,[],[s3490,s3440]) ).
cnf(s3638,plain,
( spl24_38
| spl24_23
| ~ spl24_36
| ~ spl24_18
| ~ spl24_22 ),
inference(rat,[],[s3490,s3445]) ).
cnf(s3639,plain,
( spl24_36
| ~ spl24_38
| spl24_23
| spl24_22
| spl24_18 ),
inference(rat,[],[s3493,s3440]) ).
cnf(s3640,plain,
( spl24_36
| ~ spl24_38
| spl24_23
| ~ spl24_18
| ~ spl24_22 ),
inference(rat,[],[s3493,s3445]) ).
cnf(s3641,plain,
( spl24_36
| spl24_38
| ~ spl24_23
| ~ spl24_22
| spl24_18 ),
inference(rat,[],[s3494,s3442]) ).
cnf(s3642,plain,
( spl24_36
| spl24_38
| ~ spl24_23
| ~ spl24_18
| spl24_22 ),
inference(rat,[],[s3494,s3446]) ).
cnf(s3643,plain,
( spl24_22
| ~ spl24_18
| ~ spl24_36
| ~ spl24_38 ),
inference(rat,[],[s3636,s3628]) ).
cnf(s3644,plain,
( ~ spl24_22
| ~ spl24_18
| ~ spl24_38
| spl24_36 ),
inference(rat,[],[s3640,s3629]) ).
cnf(s3645,plain,
( spl24_22
| ~ spl24_18
| spl24_38
| spl24_36 ),
inference(rat,[],[s3642,s3627]) ).
cnf(s3646,plain,
( spl24_18
| ~ spl24_22
| spl24_38
| spl24_36 ),
inference(rat,[],[s3631,s3641]) ).
cnf(s3647,plain,
( spl24_18
| ~ spl24_22
| ~ spl24_36
| ~ spl24_38 ),
inference(rat,[],[s3632,s3635]) ).
cnf(s3648,plain,
( spl24_38
| ~ spl24_36
| spl24_22
| spl24_18 ),
inference(rat,[],[s3637,s3634]) ).
cnf(s3649,plain,
( spl24_38
| ~ spl24_36
| ~ spl24_18
| ~ spl24_22 ),
inference(rat,[],[s3638,s3630]) ).
cnf(s3650,plain,
( spl24_36
| ~ spl24_38
| spl24_22
| spl24_18 ),
inference(rat,[],[s3639,s3633]) ).
cnf(s3651,plain,
( spl24_38
| ~ spl24_26
| spl24_18
| spl24_36 ),
inference(rat,[],[s3504,s3646]) ).
cnf(s3652,plain,
( spl24_38
| ~ spl24_26
| ~ spl24_36
| ~ spl24_18 ),
inference(rat,[],[s3504,s3649]) ).
cnf(s3653,plain,
( spl24_26
| ~ spl24_38
| ~ spl24_18
| spl24_36 ),
inference(rat,[],[s3505,s3644]) ).
cnf(s3654,plain,
( spl24_26
| ~ spl24_38
| spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3505,s3647]) ).
cnf(s3655,plain,
( spl24_38
| spl24_26
| ~ spl24_18
| spl24_36 ),
inference(rat,[],[s3506,s3645]) ).
cnf(s3656,plain,
( ~ spl24_38
| ~ spl24_26
| ~ spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3503,s3643]) ).
cnf(s3657,plain,
( spl24_38
| spl24_26
| ~ spl24_36
| spl24_18 ),
inference(rat,[],[s3506,s3648]) ).
cnf(s3658,plain,
( ~ spl24_38
| ~ spl24_26
| spl24_36
| spl24_18 ),
inference(rat,[],[s3503,s3650]) ).
cnf(s3659,plain,
( spl24_26
| ~ spl24_18
| spl24_36 ),
inference(rat,[],[s3655,s3653]) ).
cnf(s3660,plain,
( spl24_26
| spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3657,s3654]) ).
cnf(s3661,plain,
( ~ spl24_26
| spl24_18
| spl24_36 ),
inference(rat,[],[s3658,s3651]) ).
cnf(s3662,plain,
( ~ spl24_26
| ~ spl24_18
| ~ spl24_36 ),
inference(rat,[],[s3656,s3652]) ).
cnf(s3663,plain,
( ~ spl24_26
| spl24_36
| spl24_3
| spl24_30 ),
inference(rat,[],[s3661,s3624]) ).
cnf(s3664,plain,
( ~ spl24_26
| spl24_36
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3661,s3625]) ).
cnf(s3665,plain,
( spl24_26
| ~ spl24_36
| spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3660,s3622]) ).
cnf(s3666,plain,
( spl24_26
| ~ spl24_36
| spl24_30
| ~ spl24_3 ),
inference(rat,[],[s3660,s3623]) ).
cnf(s3667,plain,
( ~ spl24_26
| ~ spl24_36
| spl24_3
| spl24_30 ),
inference(rat,[],[s3662,s3619]) ).
cnf(s3668,plain,
( spl24_26
| spl24_36
| spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3659,s3620]) ).
cnf(s3669,plain,
( spl24_26
| spl24_36
| spl24_30
| ~ spl24_3 ),
inference(rat,[],[s3659,s3621]) ).
cnf(s3670,plain,
( ~ spl24_26
| ~ spl24_36
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3662,s3626]) ).
cnf(s3671,plain,
( ~ spl24_26
| spl24_3
| spl24_30 ),
inference(rat,[],[s3667,s3663]) ).
cnf(s3672,plain,
( spl24_26
| spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3668,s3665]) ).
cnf(s3673,plain,
( spl24_26
| spl24_30
| ~ spl24_3 ),
inference(rat,[],[s3669,s3666]) ).
cnf(s3674,plain,
( ~ spl24_26
| ~ spl24_3
| ~ spl24_30 ),
inference(rat,[],[s3670,s3664]) ).
cnf(s3675,plain,
( ~ spl24_26
| ~ spl24_6
| spl24_5
| spl24_4
| spl24_3 ),
inference(rat,[],[s3459,s3448,s3671,s14]) ).
cnf(s3676,plain,
( ~ spl24_6
| spl24_5
| spl24_4
| spl24_3 ),
inference(rat,[],[s3455,s3672,s3450,s3675,s14]) ).
cnf(s3677,plain,
( ~ spl24_26
| spl24_5
| spl24_4
| spl24_3 ),
inference(rat,[],[s3459,s3671,s3453,s13,s3676]) ).
cnf(s3678,plain,
( spl24_6
| spl24_5
| spl24_4
| spl24_3 ),
inference(rat,[],[s3455,s3451,s3672,s3677,s13]) ).
cnf(s3679,plain,
( spl24_5
| spl24_4
| spl24_3 ),
inference(rat,[],[s3678,s3676]) ).
cnf(s3680,plain,
( ~ spl24_26
| ~ spl24_6
| spl24_4
| spl24_3 ),
inference(rat,[],[s3461,s3671,s3454,s11,s3679]) ).
cnf(s3681,plain,
( ~ spl24_6
| ~ spl24_5
| spl24_3
| spl24_4 ),
inference(rat,[],[s3456,s3672,s3447,s3680,s11]) ).
cnf(s3682,plain,
( ~ spl24_26
| spl24_4
| spl24_3 ),
inference(rat,[],[s3461,s3452,s3671,s12,s3681,s3679]) ).
cnf(s3683,plain,
( spl24_6
| ~ spl24_5
| spl24_4
| spl24_3 ),
inference(rat,[],[s3456,s3672,s3449,s3682,s12]) ).
cnf(s3684,plain,
( ~ spl24_5
| spl24_4
| spl24_3 ),
inference(rat,[],[s3683,s3681]) ).
cnf(s3685,plain,
( spl24_4
| spl24_3 ),
inference(rat,[],[s3684,s3679]) ).
cnf(s3686,plain,
( ~ spl24_26
| ~ spl24_6
| spl24_5
| spl24_3 ),
inference(rat,[],[s3457,s3671,s3454,s15,s3685]) ).
cnf(s3687,plain,
( ~ spl24_6
| spl24_5
| ~ spl24_4
| spl24_3 ),
inference(rat,[],[s3460,s3672,s3447,s3686,s15]) ).
cnf(s3688,plain,
( ~ spl24_26
| spl24_5
| spl24_3 ),
inference(rat,[],[s3457,s3452,s3671,s16,s3687,s3685]) ).
cnf(s3689,plain,
( spl24_6
| spl24_5
| ~ spl24_4
| spl24_3 ),
inference(rat,[],[s3460,s3672,s3449,s3688,s16]) ).
cnf(s3690,plain,
( spl24_5
| spl24_3
| ~ spl24_4 ),
inference(rat,[],[s3689,s3687]) ).
cnf(s3691,plain,
( ~ spl24_26
| ~ spl24_6
| spl24_3 ),
inference(rat,[],[s3458,s3448,s3671,s18,s3690,s3685]) ).
cnf(s3692,plain,
( ~ spl24_6
| ~ spl24_5
| spl24_3
| ~ spl24_4 ),
inference(rat,[],[s3462,s3672,s3450,s3691,s18]) ).
cnf(s3693,plain,
( ~ spl24_26
| spl24_3 ),
inference(rat,[],[s3458,s3671,s3453,s17,s3692,s3690,s3685]) ).
cnf(s3694,plain,
( spl24_6
| spl24_3
| ~ spl24_4
| ~ spl24_5 ),
inference(rat,[],[s3462,s3451,s3672,s3693,s17]) ).
cnf(s3695,plain,
( ~ spl24_5
| ~ spl24_4
| spl24_3 ),
inference(rat,[],[s3694,s3692]) ).
cnf(s3696,plain,
( spl24_3
| ~ spl24_4 ),
inference(rat,[],[s3695,s3690]) ).
cnf(s3697,plain,
spl24_3,
inference(rat,[],[s3696,s3685]) ).
cnf(s3698,plain,
( ~ spl24_26
| ~ spl24_6
| spl24_5
| spl24_4 ),
inference(rat,[],[s3455,s3674,s3454,s7,s3697]) ).
cnf(s3699,plain,
( ~ spl24_6
| spl24_5
| spl24_4 ),
inference(rat,[],[s3459,s3673,s3447,s3698,s7,s3697]) ).
cnf(s3700,plain,
( ~ spl24_26
| spl24_5
| spl24_4 ),
inference(rat,[],[s3455,s3674,s3452,s8,s3699,s3697]) ).
cnf(s3701,plain,
( spl24_6
| spl24_5
| spl24_4 ),
inference(rat,[],[s3459,s3673,s3449,s3700,s8,s3697]) ).
cnf(s3702,plain,
( spl24_5
| spl24_4 ),
inference(rat,[],[s3701,s3699]) ).
cnf(s3703,plain,
( ~ spl24_26
| ~ spl24_6
| spl24_4 ),
inference(rat,[],[s3456,s3674,s3448,s10,s3702,s3697]) ).
cnf(s3704,plain,
( ~ spl24_6
| spl24_4
| ~ spl24_5 ),
inference(rat,[],[s3461,s3673,s3450,s3703,s10,s3697]) ).
cnf(s3705,plain,
( ~ spl24_26
| spl24_4 ),
inference(rat,[],[s3456,s3674,s3453,s9,s3704,s3702,s3697]) ).
cnf(s3706,plain,
( spl24_6
| spl24_4
| ~ spl24_5 ),
inference(rat,[],[s3461,s3451,s3673,s3705,s9,s3697]) ).
cnf(s3707,plain,
( spl24_4
| ~ spl24_5 ),
inference(rat,[],[s3706,s3704]) ).
cnf(s3708,plain,
spl24_4,
inference(rat,[],[s3707,s3702]) ).
cnf(s3709,plain,
( ~ spl24_26
| ~ spl24_6
| spl24_5 ),
inference(rat,[],[s3460,s3674,s3448,s6,s3708,s3697]) ).
cnf(s3710,plain,
( ~ spl24_6
| spl24_5 ),
inference(rat,[],[s3457,s3673,s3450,s3709,s6,s3697,s3708]) ).
cnf(s3711,plain,
( ~ spl24_26
| spl24_5 ),
inference(rat,[],[s3460,s3674,s3453,s5,s3710,s3708,s3697]) ).
cnf(s3712,plain,
( spl24_6
| spl24_5 ),
inference(rat,[],[s3457,s3451,s3673,s3711,s5,s3697,s3708]) ).
cnf(s3713,plain,
spl24_5,
inference(rat,[],[s3712,s3710]) ).
cnf(s3714,plain,
( ~ spl24_26
| ~ spl24_7
| ~ spl24_6 ),
inference(rat,[],[s3462,s3674,s3454,s3697,s3713,s3708]) ).
cnf(s3715,plain,
( spl24_26
| ~ spl24_7
| ~ spl24_6 ),
inference(rat,[],[s3458,s3673,s3447,s3697,s3713,s3708]) ).
cnf(s3716,plain,
( ~ spl24_7
| ~ spl24_6 ),
inference(rat,[],[s3715,s3714]) ).
cnf(s3717,plain,
~ spl24_6,
inference(rat,[],[s3716,s3,s3713,s3697,s3708]) ).
cnf(s3718,plain,
~ spl24_7,
inference(rat,[],[s4,s3713,s3708,s3697,s3717]) ).
cnf(s3719,plain,
~ spl24_26,
inference(rat,[],[s3462,s3674,s3452,s3708,s3713,s3697,s3717,s3718]) ).
cnf(s3720,plain,
~ spl24_28,
inference(rat,[],[s3449,s3717,s3718,s3719]) ).
cnf(s3721,plain,
spl24_30,
inference(rat,[],[s3673,s3697,s3719]) ).
cnf(s3722,plain,
$false,
inference(rat,[],[s3458,s3713,s3708,s3721,s3720]) ).
fof(f426,plain,
$false,
inference(avatar_sat_refutation,[],[s3722]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN007+1.014 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 % Computer : n008.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Mon Sep 28 15:20:43 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.24 Running first-order theorem proving
% 0.10/0.24 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.61/1.20 % (2333056)Detected formulas, will run a generic FOF schedule.
% 3.61/1.20 % (2333110)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=721633145:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 3.61/1.20 % (2333112)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2597236379:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 3.61/1.20 % (2333111)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1106080204:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 3.61/1.20 % (2333109)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2280612236:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 3.61/1.20 % (2333113)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1406721342:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 3.61/1.20 % (2333114)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1622440052:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 3.61/1.20 % (2333115)dis-21_1_sil=8000:lcm=predicate:random_seed=754668530:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 3.61/1.20 % (2333112)Refutation not found, incomplete strategy
% 3.61/1.20 % (2333112)------------------------------
% 3.61/1.20 % (2333112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.61/1.20 % (2333112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/1.20 % (2333112)CaDiCaL version: 2.1.3
% 3.61/1.20 % (2333112)Termination reason: Refutation not found, incomplete strategy
% 3.61/1.20 % (2333112)Time elapsed: 0.004 s
% 3.61/1.20 % (2333112)Peak memory usage: 88 MB
% 3.61/1.20 % (2333112)Instructions burned: 5 (million)
% 3.61/1.20 % (2333113)Instruction limit reached!
% 3.61/1.20 % (2333113)------------------------------
% 3.61/1.20 % (2333113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.61/1.20 % (2333113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/1.20 % (2333113)CaDiCaL version: 2.1.3
% 3.61/1.20 % (2333113)Termination reason: Instruction limit
% 3.61/1.20 % (2333113)Termination phase: Saturation
% 3.61/1.20 % (2333113)Time elapsed: 0.043 s
% 3.61/1.20 % (2333113)Peak memory usage: 87 MB
% 3.61/1.20 % (2333113)Instructions burned: 120 (million)
% 3.61/1.20 % (2333115)Instruction limit reached!
% 3.61/1.20 % (2333115)------------------------------
% 3.61/1.20 % (2333115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.61/1.20 % (2333115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/1.20 % (2333115)CaDiCaL version: 2.1.3
% 3.61/1.20 % (2333115)Termination reason: Instruction limit
% 3.61/1.20 % (2333115)Termination phase: Saturation
% 3.61/1.20 % (2333115)Time elapsed: 0.050 s
% 3.61/1.20 % (2333115)Peak memory usage: 89 MB
% 3.61/1.20 % (2333115)Instructions burned: 131 (million)
% 3.61/1.20 % (2333114)Instruction limit reached!
% 3.61/1.20 % (2333114)------------------------------
% 3.61/1.20 % (2333114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.61/1.20 % (2333114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/1.20 % (2333114)CaDiCaL version: 2.1.3
% 3.61/1.20 % (2333114)Termination reason: Instruction limit
% 3.61/1.20 % (2333114)Termination phase: Saturation
% 3.61/1.20 % (2333114)Time elapsed: 0.053 s
% 3.61/1.20 % (2333114)Peak memory usage: 90 MB
% 3.61/1.20 % (2333114)Instructions burned: 141 (million)
% 3.61/1.20 [W928 15:20:44.362029534 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.61/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.61/1.20 [W928 15:20:44.362053512 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 3.61/1.20 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 3.61/1.20 [W928 15:20:44.362077575 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.362089319 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.362115431 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.362120761 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.362134098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.362139435 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 % (2333124)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1311027705:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 4.43/1.34 % (2333125)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3261543625:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.43/1.34 % (2333123)lrs+10_1_sil=8000:sp=occurrence:random_seed=2816028131:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.43/1.34 % (2333124)Instruction limit reached!
% 4.43/1.34 % (2333124)------------------------------
% 4.43/1.34 % (2333124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.43/1.34 % (2333124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.43/1.34 % (2333124)CaDiCaL version: 2.1.3
% 4.43/1.34 % (2333124)Termination reason: Instruction limit
% 4.43/1.34 % (2333124)Termination phase: Saturation
% 4.43/1.34 % (2333124)Time elapsed: 0.059 s
% 4.43/1.34 % (2333124)Peak memory usage: 90 MB
% 4.43/1.34 % (2333124)Instructions burned: 157 (million)
% 4.43/1.34 % (2333112)------------------------------
% 4.43/1.34 % (2333112)------------------------------
% 4.43/1.34 % (2333125)First to succeed.
% 4.43/1.34 % (2333123)Also succeeded, but the first one will report.
% 4.43/1.34 % (2333125)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2333056"
% 4.43/1.34 % (2333129)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3620494351:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 4.43/1.34 % (2333110)Also succeeded, but the first one will report.
% 4.43/1.34 % (2333130)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3202096274:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 4.43/1.34 [W928 15:20:44.583603332 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.583634555 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.583669192 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.583681212 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.583707082 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.583765479 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.583798349 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.583810215 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584384310 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584411720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584448156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584461436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584487720 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584500646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584525926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 [W928 15:20:44.584537216 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 4.43/1.34 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 4.43/1.34 % (2333129)Also succeeded, but the first one will report.
% 4.43/1.34 % (2333125)Refutation found. Thanks to Tanya!
% 4.43/1.34 % SZS status Theorem for theBenchmark
% 4.43/1.34 % SZS output start Proof for theBenchmark
% See solution above
% 5.36/1.54 % (2333125)------------------------------
% 5.36/1.54 % (2333125)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.36/1.54 % (2333125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.36/1.54 % (2333125)CaDiCaL version: 2.1.3
% 5.36/1.54 % (2333125)Termination reason: Refutation
% 5.36/1.54 % (2333125)Time elapsed: 0.084 s
% 5.36/1.54 % (2333125)Peak memory usage: 91 MB
% 5.36/1.54 % (2333125)Instructions burned: 212 (million)
% 5.36/1.54 % (2333125)------------------------------
% 5.36/1.54 % (2333125)------------------------------
% 5.36/1.54 % (2333056)Success in time 0.666 s
% 5.36/1.54 % Vampire exiting
%------------------------------------------------------------------------------