%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN485-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:13:35 PM UTC 2026
% Result : Unsatisfiable 0.17s 0.29s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 230
% Syntax : Number of formulae : 880 ( 20 unt; 119 def)
% Number of atoms : 2955 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 3747 (1672 ~;1956 |; 0 &)
% ( 119 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 149 ( 148 usr; 145 prp; 0-1 aty)
% Number of functors : 23 ( 23 usr; 23 con; 0-0 aty)
% Number of variables : 170 ( 0 sgn 170 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp17
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
fof(f7,negated_conjecture,
( ~ hskp24
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
fof(f8,negated_conjecture,
( ~ hskp23
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
fof(f26,negated_conjecture,
( ~ hskp5
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
fof(f34,negated_conjecture,
( hskp17
| hskp23
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
( hskp23
| hskp24
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f39,negated_conjecture,
( hskp12
| hskp25
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause39) ).
fof(f40,negated_conjecture,
( ~ hskp29
| c1_1(a2077) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f42,negated_conjecture,
( ~ hskp29
| c3_1(a2077) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp28
| c0_1(a2075) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp28
| c1_1(a2075) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f46,negated_conjecture,
( ~ hskp27
| c0_1(a2073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp27
| c1_1(a2073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp27
| c3_1(a2073) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp26
| c0_1(a2069) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp26
| c2_1(a2069) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp26
| c3_1(a2069) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp25
| c1_1(a2172) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f55,negated_conjecture,
( ~ hskp23
| c0_1(a2149) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f57,negated_conjecture,
( ~ hskp22
| c2_1(a2140) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause57) ).
fof(f58,negated_conjecture,
( ~ hskp22
| c3_1(a2140) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause58) ).
fof(f62,negated_conjecture,
( ~ hskp18
| c1_1(a2116) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp17
| c0_1(a2110) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp17
| c2_1(a2110) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f66,negated_conjecture,
( ~ hskp15
| c0_1(a2099) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
fof(f68,negated_conjecture,
( ~ hskp12
| c1_1(a2095) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp11
| c0_1(a2093) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp10
| c2_1(a2087) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f73,negated_conjecture,
( ~ hskp8
| c1_1(a2082) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp8
| c2_1(a2082) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp7
| c0_1(a2079) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp7
| c1_1(a2079) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f77,negated_conjecture,
( ~ hskp6
| c0_1(a2078) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f78,negated_conjecture,
( ~ hskp5
| c1_1(a2076) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp5
| c3_1(a2076) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp4
| c1_1(a2074) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp4
| c3_1(a2074) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp2
| c0_1(a2071) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ hskp2
| c2_1(a2071) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f84,negated_conjecture,
( ~ hskp1
| c0_1(a2070) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause84) ).
fof(f85,negated_conjecture,
( ~ hskp1
| c3_1(a2070) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause85) ).
fof(f86,negated_conjecture,
( ~ hskp0
| c3_1(a2068) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ c0_1(a2172)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ c3_1(a2172)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f90,negated_conjecture,
( ~ c1_1(a2149)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c0_1(a2140)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f93,negated_conjecture,
( ~ c1_1(a2130)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f94,negated_conjecture,
( ~ c2_1(a2130)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause94) ).
fof(f95,negated_conjecture,
( ~ c3_1(a2130)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause95) ).
fof(f98,negated_conjecture,
( ~ c2_1(a2116)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c3_1(a2116)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c1_1(a2110)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f103,negated_conjecture,
( ~ c2_1(a2099)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f111,negated_conjecture,
( ~ c2_1(a2095)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c1_1(a2093)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c3_1(a2093)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ c1_1(a2087)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c3_1(a2087)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f117,negated_conjecture,
( ~ c0_1(a2082)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f120,negated_conjecture,
( ~ c2_1(a2078)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c0_1(a2076)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c2_1(a2074)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c0_1(a2072)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c1_1(a2072)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ c3_1(a2072)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c3_1(a2071)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c2_1(a2070)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ c0_1(a2068)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
( ~ c2_1(a2068)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| hskp26
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f132,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c3_1(X0)
| hskp28
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f134,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp17
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause134) ).
fof(f137,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp26
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp1
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f141,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp27
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp11
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp26
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp11
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp7
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp17
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f156,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
fof(f159,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f161,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f165,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause165) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f168,negated_conjecture,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f171,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f176,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X1)
| c2_1(X1)
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f177,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| c3_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause177) ).
fof(f179,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f181,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X1)
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f184,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| c2_1(X0)
| c2_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f186,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c3_1(X0)
| c2_1(X1)
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause186) ).
fof(f187,negated_conjecture,
! [X2,X0,X1] :
( ~ ndr1_0
| ~ c1_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X0)
| c2_1(X0)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause187) ).
fof(f188,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f190,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause190) ).
fof(f193,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c1_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause193) ).
fof(f194,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c2_1(X0)
| c2_1(X1)
| c0_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause194) ).
fof(f195,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| ~ c3_1(X2)
| c2_1(X0)
| c1_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause195) ).
fof(f196,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause196) ).
fof(f198,definition,
( spl0_1
<=> ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f199,plain,
( ! [X2] :
( ~ c0_1(X2)
| c3_1(X2)
| c1_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f198]) ).
fof(f201,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f202,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f204,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f208,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f209,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f208]) ).
fof(f210,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f196,f208,f204,f201,f198]) ).
fof(f212,definition,
( spl0_5
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f213,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2)
| ~ c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f212]) ).
fof(f215,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f216,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f215]) ).
fof(f218,definition,
( spl0_7
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f219,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f218]) ).
fof(f220,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f195,f218,f204,f215,f212]) ).
fof(f222,definition,
( spl0_8
<=> ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f223,plain,
( ! [X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c0_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f225,definition,
( spl0_9
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f226,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f225]) ).
fof(f228,definition,
( spl0_10
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f229,plain,
( ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f230,plain,
( spl0_8
| spl0_9
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f194,f228,f204,f225,f222]) ).
fof(f232,definition,
( spl0_11
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f233,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f232]) ).
fof(f235,definition,
( spl0_12
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f236,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f235]) ).
fof(f238,definition,
( spl0_13
<=> ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f239,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f238]) ).
fof(f240,plain,
( spl0_11
| spl0_12
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f193,f238,f204,f235,f232]) ).
fof(f242,definition,
( spl0_14
<=> ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f243,plain,
( ! [X2] :
( ~ c3_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f242]) ).
fof(f245,definition,
( spl0_15
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f246,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c2_1(X1) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f248,definition,
( spl0_16
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f249,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f248]) ).
fof(f252,definition,
( spl0_17
<=> ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f253,plain,
( ! [X2] :
( ~ c3_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f252]) ).
fof(f255,definition,
( spl0_18
<=> ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f256,plain,
( ! [X1] :
( ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f255]) ).
fof(f259,definition,
( spl0_19
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f260,plain,
( ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f259]) ).
fof(f262,definition,
( spl0_20
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f263,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f264,plain,
( spl0_19
| spl0_20
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f190,f228,f204,f262,f259]) ).
fof(f266,definition,
( spl0_21
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f270,definition,
( spl0_22
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f271,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f270]) ).
fof(f272,plain,
( spl0_21
| spl0_15
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f189,f270,f204,f245,f266]) ).
fof(f274,definition,
( spl0_23
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f277,plain,
( spl0_23
| spl0_12
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f188,f270,f204,f235,f274]) ).
fof(f279,definition,
( spl0_24
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f280,plain,
( ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f282,definition,
( spl0_25
<=> ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f283,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f282]) ).
fof(f285,definition,
( spl0_26
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f286,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f285]) ).
fof(f287,plain,
( spl0_24
| spl0_25
| spl0_26
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f187,f204,f285,f282,f279]) ).
fof(f289,definition,
( spl0_27
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f293,definition,
( spl0_28
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f294,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f295,plain,
( spl0_27
| spl0_9
| ~ spl0_3
| spl0_28 ),
inference(avatar_split_clause,[],[f186,f293,f204,f225,f289]) ).
fof(f297,definition,
( spl0_29
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f305,definition,
( spl0_31
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f308,plain,
( spl0_31
| spl0_7
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f184,f228,f204,f218,f305]) ).
fof(f310,definition,
( spl0_32
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f318,definition,
( spl0_34
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f321,plain,
( spl0_34
| spl0_15
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f182,f225,f204,f245,f318]) ).
fof(f323,definition,
( spl0_35
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f327,definition,
( spl0_36
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f328,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f330,definition,
( spl0_37
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f331,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f330]) ).
fof(f332,plain,
( spl0_35
| spl0_36
| ~ spl0_3
| spl0_37 ),
inference(avatar_split_clause,[],[f181,f330,f204,f327,f323]) ).
fof(f334,definition,
( spl0_38
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f335,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f334]) ).
fof(f338,definition,
( spl0_39
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f341,plain,
( spl0_39
| spl0_12
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f179,f245,f204,f235,f338]) ).
fof(f343,plain,
( spl0_27
| spl0_18
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f177,f208,f204,f255,f289]) ).
fof(f345,definition,
( spl0_40
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f348,plain,
( spl0_40
| spl0_17
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f176,f208,f204,f252,f345]) ).
fof(f350,definition,
( spl0_41
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f354,plain,
( spl0_35
| spl0_6
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f174,f248,f204,f215,f323]) ).
fof(f356,definition,
( spl0_42
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f359,plain,
( spl0_42
| spl0_6
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f173,f248,f204,f215,f356]) ).
fof(f360,plain,
( spl0_34
| spl0_1
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f172,f228,f204,f198,f318]) ).
fof(f361,plain,
( spl0_23
| spl0_1
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f171,f245,f204,f198,f274]) ).
fof(f369,definition,
( spl0_44
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f372,plain,
( spl0_44
| spl0_5
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f168,f327,f204,f212,f369]) ).
fof(f374,definition,
( spl0_45
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f375,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f376,plain,
( spl0_32
| spl0_45
| ~ spl0_3
| spl0_20 ),
inference(avatar_split_clause,[],[f167,f262,f204,f374,f310]) ).
fof(f379,definition,
( spl0_46
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f382,plain,
( spl0_46
| spl0_8
| ~ spl0_3
| spl0_45 ),
inference(avatar_split_clause,[],[f165,f374,f204,f222,f379]) ).
fof(f390,definition,
( spl0_48
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f395,definition,
( spl0_49
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f398,plain,
( spl0_49
| spl0_14
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f161,f215,f204,f242,f395]) ).
fof(f400,definition,
( spl0_50
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f405,definition,
( spl0_51
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f408,plain,
( spl0_51
| spl0_24
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f159,f208,f204,f279,f405]) ).
fof(f414,plain,
( spl0_32
| spl0_8
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f157,f334,f204,f222,f310]) ).
fof(f415,plain,
( spl0_27
| spl0_17
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f156,f327,f204,f252,f289]) ).
fof(f416,plain,
( spl0_35
| spl0_26
| ~ spl0_3
| spl0_20 ),
inference(avatar_split_clause,[],[f155,f262,f204,f285,f323]) ).
fof(f418,definition,
( spl0_53
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f419,plain,
( ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( spl0_27
| spl0_53
| ~ spl0_3
| spl0_20 ),
inference(avatar_split_clause,[],[f154,f262,f204,f418,f289]) ).
fof(f421,plain,
( spl0_39
| spl0_53
| ~ spl0_3
| spl0_11 ),
inference(avatar_split_clause,[],[f153,f232,f204,f418,f338]) ).
fof(f423,definition,
( spl0_54
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f426,plain,
( spl0_54
| spl0_42
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f152,f201,f204,f356,f423]) ).
fof(f435,plain,
( spl0_44
| spl0_41
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f147,f245,f204,f350,f369]) ).
fof(f436,plain,
( spl0_40
| spl0_32
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f146,f215,f204,f310,f345]) ).
fof(f437,plain,
( spl0_31
| spl0_23
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f145,f215,f204,f274,f305]) ).
fof(f438,plain,
( spl0_51
| spl0_32
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f144,f235,f204,f310,f405]) ).
fof(f439,plain,
( spl0_50
| spl0_39
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f143,f235,f204,f338,f400]) ).
fof(f441,definition,
( spl0_56
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f445,plain,
( spl0_54
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f141,f218,f204,f423]) ).
fof(f451,plain,
( spl0_35
| spl0_46
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f139,f198,f204,f379,f323]) ).
fof(f453,definition,
( spl0_58
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f456,plain,
( spl0_58
| spl0_23
| ~ spl0_3
| spl0_36 ),
inference(avatar_split_clause,[],[f138,f327,f204,f274,f453]) ).
fof(f457,plain,
( spl0_51
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f137,f212,f204,f405]) ).
fof(f464,plain,
( spl0_46
| spl0_42
| spl0_25
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f134,f204,f282,f356,f379]) ).
fof(f466,plain,
( spl0_31
| spl0_56
| spl0_53
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f132,f204,f418,f441,f305]) ).
fof(f468,plain,
( spl0_46
| spl0_23
| spl0_24
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f130,f204,f279,f274,f379]) ).
fof(f470,definition,
( spl0_60
<=> c2_1(a2068) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f472,plain,
( ~ c2_1(a2068)
| spl0_60 ),
inference(avatar_component_clause,[],[f470]) ).
fof(f473,plain,
( ~ spl0_51
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f129,f470,f405]) ).
fof(f475,definition,
( spl0_61
<=> c0_1(a2068) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f477,plain,
( ~ c0_1(a2068)
| spl0_61 ),
inference(avatar_component_clause,[],[f475]) ).
fof(f478,plain,
( ~ spl0_51
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f128,f475,f405]) ).
fof(f480,definition,
( spl0_62
<=> c2_1(a2070) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f482,plain,
( ~ c2_1(a2070)
| spl0_62 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f483,plain,
( ~ spl0_46
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f127,f480,f379]) ).
fof(f485,definition,
( spl0_63
<=> c3_1(a2071) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f488,plain,
( ~ spl0_48
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f126,f485,f390]) ).
fof(f490,definition,
( spl0_64
<=> c3_1(a2072) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f492,plain,
( ~ c3_1(a2072)
| spl0_64 ),
inference(avatar_component_clause,[],[f490]) ).
fof(f493,plain,
( ~ spl0_34
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f125,f490,f318]) ).
fof(f495,definition,
( spl0_65
<=> c1_1(a2072) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f497,plain,
( ~ c1_1(a2072)
| spl0_65 ),
inference(avatar_component_clause,[],[f495]) ).
fof(f498,plain,
( ~ spl0_34
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f124,f495,f318]) ).
fof(f500,definition,
( spl0_66
<=> c0_1(a2072) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f502,plain,
( ~ c0_1(a2072)
| spl0_66 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f503,plain,
( ~ spl0_34
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f123,f500,f318]) ).
fof(f505,definition,
( spl0_67
<=> c2_1(a2074) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f507,plain,
( ~ c2_1(a2074)
| spl0_67 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f508,plain,
( ~ spl0_27
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f122,f505,f289]) ).
fof(f510,definition,
( spl0_68
<=> c0_1(a2076) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f512,plain,
( ~ c0_1(a2076)
| spl0_68 ),
inference(avatar_component_clause,[],[f510]) ).
fof(f513,plain,
( ~ spl0_31
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f121,f510,f305]) ).
fof(f515,definition,
( spl0_69
<=> c2_1(a2078) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f518,plain,
( ~ spl0_49
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f120,f515,f395]) ).
fof(f530,definition,
( spl0_72
<=> c0_1(a2082) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f532,plain,
( ~ c0_1(a2082)
| spl0_72 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f533,plain,
( ~ spl0_35
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f117,f530,f323]) ).
fof(f540,definition,
( spl0_74
<=> c3_1(a2087) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f542,plain,
( ~ c3_1(a2087)
| spl0_74 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f543,plain,
( ~ spl0_40
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f115,f540,f345]) ).
fof(f545,definition,
( spl0_75
<=> c1_1(a2087) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f547,plain,
( ~ c1_1(a2087)
| spl0_75 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f548,plain,
( ~ spl0_40
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f114,f545,f345]) ).
fof(f550,definition,
( spl0_76
<=> c3_1(a2093) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f552,plain,
( ~ c3_1(a2093)
| spl0_76 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f553,plain,
( ~ spl0_32
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f113,f550,f310]) ).
fof(f555,definition,
( spl0_77
<=> c1_1(a2093) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f557,plain,
( ~ c1_1(a2093)
| spl0_77 ),
inference(avatar_component_clause,[],[f555]) ).
fof(f558,plain,
( ~ spl0_32
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f112,f555,f310]) ).
fof(f560,definition,
( spl0_78
<=> c2_1(a2095) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f563,plain,
( ~ spl0_29
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f111,f560,f297]) ).
fof(f600,definition,
( spl0_86
<=> c2_1(a2099) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f602,plain,
( ~ c2_1(a2099)
| spl0_86 ),
inference(avatar_component_clause,[],[f600]) ).
fof(f603,plain,
( ~ spl0_44
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f103,f600,f369]) ).
fof(f615,definition,
( spl0_89
<=> c1_1(a2110) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f618,plain,
( ~ spl0_42
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f100,f615,f356]) ).
fof(f620,definition,
( spl0_90
<=> c3_1(a2116) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f622,plain,
( ~ c3_1(a2116)
| spl0_90 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f623,plain,
( ~ spl0_58
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f99,f620,f453]) ).
fof(f625,definition,
( spl0_91
<=> c2_1(a2116) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f627,plain,
( ~ c2_1(a2116)
| spl0_91 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f628,plain,
( ~ spl0_58
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f98,f625,f453]) ).
fof(f640,definition,
( spl0_94
<=> c3_1(a2130) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f642,plain,
( ~ c3_1(a2130)
| spl0_94 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f643,plain,
( ~ spl0_21
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f95,f640,f266]) ).
fof(f645,definition,
( spl0_95
<=> c2_1(a2130) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f647,plain,
( ~ c2_1(a2130)
| spl0_95 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f648,plain,
( ~ spl0_21
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f94,f645,f266]) ).
fof(f650,definition,
( spl0_96
<=> c1_1(a2130) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f652,plain,
( ~ c1_1(a2130)
| spl0_96 ),
inference(avatar_component_clause,[],[f650]) ).
fof(f653,plain,
( ~ spl0_21
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f93,f650,f266]) ).
fof(f660,definition,
( spl0_98
<=> c0_1(a2140) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f662,plain,
( ~ c0_1(a2140)
| spl0_98 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f663,plain,
( ~ spl0_54
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f91,f660,f423]) ).
fof(f665,definition,
( spl0_99
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f669,definition,
( spl0_100
<=> c1_1(a2149) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f672,plain,
( ~ spl0_99
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f90,f669,f665]) ).
fof(f674,definition,
( spl0_101
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f683,definition,
( spl0_103
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f687,definition,
( spl0_104
<=> c3_1(a2172) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f689,plain,
( ~ c3_1(a2172)
| spl0_104 ),
inference(avatar_component_clause,[],[f687]) ).
fof(f690,plain,
( ~ spl0_103
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f88,f687,f683]) ).
fof(f692,definition,
( spl0_105
<=> c0_1(a2172) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f694,plain,
( ~ c0_1(a2172)
| spl0_105 ),
inference(avatar_component_clause,[],[f692]) ).
fof(f695,plain,
( ~ spl0_103
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f87,f692,f683]) ).
fof(f697,definition,
( spl0_106
<=> c3_1(a2068) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f699,plain,
( c3_1(a2068)
| ~ spl0_106 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f700,plain,
( spl0_106
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f86,f405,f697]) ).
fof(f702,definition,
( spl0_107
<=> c3_1(a2070) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f704,plain,
( c3_1(a2070)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f702]) ).
fof(f705,plain,
( spl0_107
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f85,f379,f702]) ).
fof(f707,definition,
( spl0_108
<=> c0_1(a2070) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f709,plain,
( c0_1(a2070)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f707]) ).
fof(f710,plain,
( spl0_108
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f84,f379,f707]) ).
fof(f712,definition,
( spl0_109
<=> c2_1(a2071) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f714,plain,
( c2_1(a2071)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f715,plain,
( spl0_109
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f83,f390,f712]) ).
fof(f717,definition,
( spl0_110
<=> c0_1(a2071) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f719,plain,
( c0_1(a2071)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f720,plain,
( spl0_110
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f82,f390,f717]) ).
fof(f722,definition,
( spl0_111
<=> c3_1(a2074) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f724,plain,
( c3_1(a2074)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f725,plain,
( spl0_111
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f81,f289,f722]) ).
fof(f727,definition,
( spl0_112
<=> c1_1(a2074) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f729,plain,
( c1_1(a2074)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f727]) ).
fof(f730,plain,
( spl0_112
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f80,f289,f727]) ).
fof(f732,definition,
( spl0_113
<=> c3_1(a2076) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f734,plain,
( c3_1(a2076)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f732]) ).
fof(f735,plain,
( spl0_113
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f79,f305,f732]) ).
fof(f737,definition,
( spl0_114
<=> c1_1(a2076) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f739,plain,
( c1_1(a2076)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f740,plain,
( spl0_114
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f78,f305,f737]) ).
fof(f742,definition,
( spl0_115
<=> c0_1(a2078) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f744,plain,
( c0_1(a2078)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f745,plain,
( spl0_115
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f77,f395,f742]) ).
fof(f747,definition,
( spl0_116
<=> c1_1(a2079) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f750,plain,
( spl0_116
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f76,f350,f747]) ).
fof(f752,definition,
( spl0_117
<=> c0_1(a2079) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f754,plain,
( c0_1(a2079)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f755,plain,
( spl0_117
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f75,f350,f752]) ).
fof(f757,definition,
( spl0_118
<=> c2_1(a2082) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f759,plain,
( c2_1(a2082)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f760,plain,
( spl0_118
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f74,f323,f757]) ).
fof(f762,definition,
( spl0_119
<=> c1_1(a2082) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f764,plain,
( c1_1(a2082)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f762]) ).
fof(f765,plain,
( spl0_119
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f73,f323,f762]) ).
fof(f777,definition,
( spl0_122
<=> c2_1(a2087) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f779,plain,
( c2_1(a2087)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f780,plain,
( spl0_122
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f70,f345,f777]) ).
fof(f782,definition,
( spl0_123
<=> c0_1(a2093) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f784,plain,
( c0_1(a2093)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f782]) ).
fof(f785,plain,
( spl0_123
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f69,f310,f782]) ).
fof(f787,definition,
( spl0_124
<=> c1_1(a2095) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f789,plain,
( c1_1(a2095)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f790,plain,
( spl0_124
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f68,f297,f787]) ).
fof(f797,definition,
( spl0_126
<=> c0_1(a2099) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f799,plain,
( c0_1(a2099)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f800,plain,
( spl0_126
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f66,f369,f797]) ).
fof(f807,definition,
( spl0_128
<=> c2_1(a2110) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f809,plain,
( c2_1(a2110)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f807]) ).
fof(f810,plain,
( spl0_128
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f64,f356,f807]) ).
fof(f812,definition,
( spl0_129
<=> c0_1(a2110) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f814,plain,
( c0_1(a2110)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f812]) ).
fof(f815,plain,
( spl0_129
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f63,f356,f812]) ).
fof(f817,definition,
( spl0_130
<=> c1_1(a2116) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f819,plain,
( c1_1(a2116)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f820,plain,
( spl0_130
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f62,f453,f817]) ).
fof(f837,definition,
( spl0_134
<=> c3_1(a2140) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f839,plain,
( c3_1(a2140)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f840,plain,
( spl0_134
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f58,f423,f837]) ).
fof(f842,definition,
( spl0_135
<=> c2_1(a2140) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f844,plain,
( c2_1(a2140)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f845,plain,
( spl0_135
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f57,f423,f842]) ).
fof(f852,definition,
( spl0_137
<=> c0_1(a2149) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f854,plain,
( c0_1(a2149)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f855,plain,
( spl0_137
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f55,f665,f852]) ).
fof(f867,definition,
( spl0_140
<=> c1_1(a2172) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f869,plain,
( c1_1(a2172)
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f870,plain,
( spl0_140
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f52,f683,f867]) ).
fof(f872,definition,
( spl0_141
<=> c3_1(a2069) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f874,plain,
( c3_1(a2069)
| ~ spl0_141 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f875,plain,
( spl0_141
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f51,f274,f872]) ).
fof(f877,definition,
( spl0_142
<=> c2_1(a2069) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f879,plain,
( c2_1(a2069)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f877]) ).
fof(f880,plain,
( spl0_142
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f50,f274,f877]) ).
fof(f882,definition,
( spl0_143
<=> c0_1(a2069) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f884,plain,
( c0_1(a2069)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f885,plain,
( spl0_143
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f49,f274,f882]) ).
fof(f887,definition,
( spl0_144
<=> c3_1(a2073) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f889,plain,
( c3_1(a2073)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f887]) ).
fof(f890,plain,
( spl0_144
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f48,f338,f887]) ).
fof(f892,definition,
( spl0_145
<=> c1_1(a2073) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f895,plain,
( spl0_145
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f47,f338,f892]) ).
fof(f897,definition,
( spl0_146
<=> c0_1(a2073) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f899,plain,
( c0_1(a2073)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f900,plain,
( spl0_146
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f46,f338,f897]) ).
fof(f907,definition,
( spl0_148
<=> c1_1(a2075) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f909,plain,
( c1_1(a2075)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f907]) ).
fof(f910,plain,
( spl0_148
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f44,f441,f907]) ).
fof(f912,definition,
( spl0_149
<=> c0_1(a2075) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f914,plain,
( c0_1(a2075)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f912]) ).
fof(f915,plain,
( spl0_149
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f43,f441,f912]) ).
fof(f917,definition,
( spl0_150
<=> c3_1(a2077) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f919,plain,
( c3_1(a2077)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f917]) ).
fof(f920,plain,
( spl0_150
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f42,f400,f917]) ).
fof(f927,definition,
( spl0_152
<=> c1_1(a2077) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f930,plain,
( spl0_152
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f40,f400,f927]) ).
fof(f931,plain,
( spl0_58
| spl0_103
| spl0_29 ),
inference(avatar_split_clause,[],[f39,f297,f683,f453]) ).
fof(f935,plain,
( spl0_31
| spl0_101
| spl0_99 ),
inference(avatar_split_clause,[],[f35,f665,f674,f305]) ).
fof(f936,plain,
( spl0_46
| spl0_99
| spl0_42 ),
inference(avatar_split_clause,[],[f34,f356,f665,f379]) ).
fof(f944,plain,
( spl0_3
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f26,f305,f204]) ).
fof(f962,plain,
( spl0_3
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f8,f665,f204]) ).
fof(f963,plain,
( spl0_3
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f7,f674,f204]) ).
fof(f969,plain,
( spl0_48
| spl0_42 ),
inference(avatar_split_clause,[],[f1,f356,f390]) ).
fof(f970,plain,
( ! [X2] :
( ~ c3_1(X2)
| ~ c1_1(X2) )
| ~ spl0_2
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f213,f202]) ).
fof(f971,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_2
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f216,f202]) ).
fof(f972,plain,
( ! [X1] :
( ~ c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_4
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f226,f209]) ).
fof(f974,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1) )
| ~ spl0_15
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f263,f246]) ).
fof(f975,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1) )
| ~ spl0_10
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f328,f229]) ).
fof(f988,plain,
( ! [X2] :
( c0_1(X2)
| c1_1(X2) )
| ~ spl0_11
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f280,f233]) ).
fof(f989,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1) )
| ~ spl0_7
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f335,f219]) ).
fof(f1002,plain,
( ~ c3_1(a2070)
| ~ spl0_2
| ~ spl0_6
| ~ spl0_108 ),
inference(resolution,[],[f971,f709]) ).
fof(f1003,plain,
( $false
| ~ spl0_2
| ~ spl0_6
| ~ spl0_107
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f1002,f704]) ).
fof(f1004,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_107
| ~ spl0_108 ),
inference(avatar_contradiction_clause,[],[f1003]) ).
fof(f1013,plain,
( c1_1(a2110)
| ~ spl0_15
| ~ spl0_20
| ~ spl0_128 ),
inference(resolution,[],[f974,f809]) ).
fof(f1027,plain,
( c1_1(a2072)
| ~ spl0_11
| ~ spl0_24
| spl0_66 ),
inference(resolution,[],[f988,f502]) ).
fof(f1030,plain,
( ! [X1] :
( c0_1(X1)
| c3_1(X1) )
| ~ spl0_18
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f419,f256]) ).
fof(f1031,plain,
( ! [X2] :
( c2_1(X2)
| c1_1(X2) )
| ~ spl0_7
| ~ spl0_24
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f280,f989]) ).
fof(f1032,plain,
( ! [X2] :
( c3_1(X2)
| c2_1(X2) )
| ~ spl0_7
| ~ spl0_19
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f260,f989]) ).
fof(f1044,plain,
( c3_1(a2072)
| ~ spl0_18
| ~ spl0_53
| spl0_66 ),
inference(resolution,[],[f1030,f502]) ).
fof(f1050,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_7
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f271,f219]) ).
fof(f1101,plain,
( ~ c1_1(a2077)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_150 ),
inference(resolution,[],[f970,f919]) ).
fof(f1103,plain,
( ~ c1_1(a2076)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_113 ),
inference(resolution,[],[f970,f734]) ).
fof(f1104,plain,
( ~ c1_1(a2074)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_111 ),
inference(resolution,[],[f970,f724]) ).
fof(f1107,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| ~ spl0_111
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f1104,f729]) ).
fof(f1108,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_111
| ~ spl0_112 ),
inference(avatar_contradiction_clause,[],[f1107]) ).
fof(f1144,plain,
( ! [X1] :
( c3_1(X1)
| c1_1(X1) )
| ~ spl0_20
| ~ spl0_25 ),
inference(forward_subsumption_resolution,[],[f263,f283]) ).
fof(f1231,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0) )
| ~ spl0_7
| ~ spl0_24
| ~ spl0_26
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f286,f1031]) ).
fof(f1232,plain,
( ! [X0] : c2_1(X0)
| ~ spl0_7
| ~ spl0_24
| ~ spl0_26
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f1231,f989]) ).
fof(f1236,plain,
( $false
| ~ spl0_7
| ~ spl0_24
| ~ spl0_26
| ~ spl0_38
| spl0_67 ),
inference(resolution,[],[f1232,f507]) ).
fof(f1241,plain,
( ~ spl0_7
| ~ spl0_24
| ~ spl0_26
| ~ spl0_38
| spl0_67 ),
inference(avatar_contradiction_clause,[],[f1236]) ).
fof(f1247,plain,
( spl0_89
| ~ spl0_15
| ~ spl0_20
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f1013,f807,f262,f245,f615]) ).
fof(f1255,plain,
( c2_1(a2099)
| ~ spl0_7
| ~ spl0_38
| ~ spl0_126 ),
inference(resolution,[],[f799,f989]) ).
fof(f1257,plain,
( $false
| ~ spl0_7
| ~ spl0_38
| spl0_86
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f1255,f602]) ).
fof(f1258,plain,
( ~ spl0_7
| ~ spl0_38
| spl0_86
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f1257]) ).
fof(f1322,plain,
( c2_1(a2078)
| ~ spl0_7
| ~ spl0_38
| ~ spl0_115 ),
inference(resolution,[],[f744,f989]) ).
fof(f1337,plain,
( spl0_65
| ~ spl0_11
| ~ spl0_24
| spl0_66 ),
inference(avatar_split_clause,[],[f1027,f500,f279,f232,f495]) ).
fof(f1436,plain,
( c2_1(a2130)
| ~ spl0_7
| ~ spl0_19
| ~ spl0_38
| spl0_94 ),
inference(resolution,[],[f1032,f642]) ).
fof(f1556,plain,
( c3_1(a2172)
| c2_1(a2172)
| ~ spl0_16
| ~ spl0_140 ),
inference(resolution,[],[f249,f869]) ).
fof(f1559,plain,
( c3_1(a2116)
| c2_1(a2116)
| ~ spl0_16
| ~ spl0_130 ),
inference(resolution,[],[f249,f819]) ).
fof(f1570,plain,
( c2_1(a2116)
| ~ spl0_16
| spl0_90
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1559,f622]) ).
fof(f1571,plain,
( c2_1(a2172)
| ~ spl0_16
| spl0_104
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f1556,f689]) ).
fof(f1572,plain,
( $false
| ~ spl0_16
| spl0_90
| spl0_91
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1570,f627]) ).
fof(f1573,plain,
( ~ spl0_16
| spl0_90
| spl0_91
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f1572]) ).
fof(f1574,plain,
( ! [X2] :
( c3_1(X2)
| c1_1(X2) )
| ~ spl0_1
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f199,f419]) ).
fof(f1575,plain,
( ! [X2] :
( c0_1(X2)
| c3_1(X2) )
| ~ spl0_8
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f223,f260]) ).
fof(f1577,plain,
( spl0_64
| ~ spl0_18
| ~ spl0_53
| spl0_66 ),
inference(avatar_split_clause,[],[f1044,f500,f418,f255,f490]) ).
fof(f1615,plain,
( c1_1(a2087)
| ~ spl0_1
| ~ spl0_53
| spl0_74 ),
inference(resolution,[],[f1574,f542]) ).
fof(f1621,plain,
( $false
| ~ spl0_1
| ~ spl0_53
| spl0_74
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f1615,f547]) ).
fof(f1622,plain,
( ~ spl0_1
| ~ spl0_53
| spl0_74
| spl0_75 ),
inference(avatar_contradiction_clause,[],[f1621]) ).
fof(f1745,plain,
( ~ c1_1(a2075)
| ~ spl0_7
| ~ spl0_22
| ~ spl0_149 ),
inference(resolution,[],[f1050,f914]) ).
fof(f1753,plain,
( ~ c1_1(a2079)
| ~ spl0_7
| ~ spl0_22
| ~ spl0_117 ),
inference(resolution,[],[f1050,f754]) ).
fof(f1801,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_13
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f239,f271]) ).
fof(f1812,plain,
( c2_1(a2068)
| ~ spl0_10
| ~ spl0_36
| ~ spl0_106 ),
inference(resolution,[],[f975,f699]) ).
fof(f1856,plain,
( ~ c2_1(a2110)
| ~ spl0_13
| ~ spl0_22
| ~ spl0_129 ),
inference(resolution,[],[f1801,f814]) ).
fof(f1860,plain,
( ~ c2_1(a2071)
| ~ spl0_13
| ~ spl0_22
| ~ spl0_110 ),
inference(resolution,[],[f1801,f719]) ).
fof(f1861,plain,
( $false
| ~ spl0_13
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f1860,f714]) ).
fof(f1862,plain,
( ~ spl0_13
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f1861]) ).
fof(f1863,plain,
( $false
| ~ spl0_13
| ~ spl0_22
| ~ spl0_128
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f1856,f809]) ).
fof(f1864,plain,
( ~ spl0_13
| ~ spl0_22
| ~ spl0_128
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f1863]) ).
fof(f1871,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_10
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f249,f229]) ).
fof(f1881,plain,
( ~ c3_1(a2069)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_143 ),
inference(resolution,[],[f972,f884]) ).
fof(f1888,plain,
( ~ c3_1(a2070)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_108 ),
inference(resolution,[],[f972,f709]) ).
fof(f1891,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_141
| ~ spl0_143 ),
inference(forward_subsumption_resolution,[],[f1881,f874]) ).
fof(f1892,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_141
| ~ spl0_143 ),
inference(avatar_contradiction_clause,[],[f1891]) ).
fof(f1934,plain,
( ~ c3_1(a2069)
| ~ c2_1(a2069)
| ~ spl0_4
| ~ spl0_143 ),
inference(resolution,[],[f209,f884]) ).
fof(f1944,plain,
( ~ c2_1(a2069)
| ~ spl0_4
| ~ spl0_141
| ~ spl0_143 ),
inference(forward_subsumption_resolution,[],[f1934,f874]) ).
fof(f1956,plain,
( c2_1(a2070)
| ~ c1_1(a2070)
| ~ spl0_7
| ~ spl0_108 ),
inference(resolution,[],[f219,f709]) ).
fof(f1965,plain,
( c3_1(a2087)
| c0_1(a2087)
| ~ spl0_8
| ~ spl0_122 ),
inference(resolution,[],[f223,f779]) ).
fof(f1984,plain,
( c2_1(a2074)
| ~ c1_1(a2074)
| ~ spl0_10
| ~ spl0_111 ),
inference(resolution,[],[f229,f724]) ).
fof(f1985,plain,
( c2_1(a2070)
| ~ c1_1(a2070)
| ~ spl0_10
| ~ spl0_107 ),
inference(resolution,[],[f229,f704]) ).
fof(f2040,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_8
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f294,f223]) ).
fof(f2076,plain,
( c1_1(a2087)
| ~ spl0_15
| ~ spl0_20
| ~ spl0_122 ),
inference(resolution,[],[f974,f779]) ).
fof(f2106,plain,
( ~ c3_1(a2073)
| ~ c1_1(a2073)
| ~ spl0_2
| ~ spl0_146 ),
inference(resolution,[],[f899,f202]) ).
fof(f2146,plain,
( ~ c1_1(a2074)
| ~ spl0_10
| spl0_67
| ~ spl0_111 ),
inference(forward_subsumption_resolution,[],[f1984,f507]) ).
fof(f2156,plain,
( $false
| ~ spl0_10
| spl0_67
| ~ spl0_111
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f2146,f729]) ).
fof(f2157,plain,
( ~ spl0_10
| spl0_67
| ~ spl0_111
| ~ spl0_112 ),
inference(avatar_contradiction_clause,[],[f2156]) ).
fof(f2173,plain,
( ~ c1_1(a2073)
| ~ spl0_2
| ~ spl0_144
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f2106,f889]) ).
fof(f2348,plain,
( ~ c1_1(a2070)
| ~ spl0_7
| spl0_62
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f1956,f482]) ).
fof(f2359,plain,
( ~ spl0_107
| ~ spl0_4
| ~ spl0_9
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1888,f707,f225,f208,f702]) ).
fof(f2361,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_11
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f213,f988]) ).
fof(f2363,plain,
( spl0_60
| ~ spl0_10
| ~ spl0_36
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f1812,f697,f327,f228,f470]) ).
fof(f2372,plain,
( ~ spl0_148
| ~ spl0_7
| ~ spl0_22
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1745,f912,f270,f218,f907]) ).
fof(f2376,plain,
( ~ spl0_116
| ~ spl0_7
| ~ spl0_22
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1753,f752,f270,f218,f747]) ).
fof(f2384,plain,
( spl0_75
| ~ spl0_15
| ~ spl0_20
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f2076,f777,f262,f245,f545]) ).
fof(f2393,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c2_1(X1) )
| ~ spl0_15
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f246,f331]) ).
fof(f2407,plain,
( ! [X2] : ~ c3_1(X2)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_9
| ~ spl0_11
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f2361,f972]) ).
fof(f2419,plain,
( $false
| ~ spl0_4
| ~ spl0_5
| ~ spl0_9
| ~ spl0_11
| ~ spl0_24
| ~ spl0_150 ),
inference(resolution,[],[f2407,f919]) ).
fof(f2446,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_9
| ~ spl0_11
| ~ spl0_24
| ~ spl0_150 ),
inference(avatar_contradiction_clause,[],[f2419]) ).
fof(f2447,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_8
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f236,f223]) ).
fof(f2453,definition,
( spl0_155
<=> c0_1(a2087) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f2455,plain,
( c0_1(a2087)
| ~ spl0_155 ),
inference(avatar_component_clause,[],[f2453]) ).
fof(f2456,plain,
( spl0_155
| spl0_74
| ~ spl0_8
| ~ spl0_122 ),
inference(avatar_split_clause,[],[f1965,f777,f222,f540,f2453]) ).
fof(f2551,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_4
| ~ spl0_28 ),
inference(forward_subsumption_resolution,[],[f209,f294]) ).
fof(f2556,plain,
( ~ c2_1(a2110)
| ~ spl0_4
| ~ spl0_28
| ~ spl0_129 ),
inference(resolution,[],[f2551,f814]) ).
fof(f2562,plain,
( ~ c2_1(a2071)
| ~ spl0_4
| ~ spl0_28
| ~ spl0_110 ),
inference(resolution,[],[f2551,f719]) ).
fof(f2564,plain,
( $false
| ~ spl0_4
| ~ spl0_28
| ~ spl0_109
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f2562,f714]) ).
fof(f2565,plain,
( ~ spl0_4
| ~ spl0_28
| ~ spl0_109
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f2564]) ).
fof(f2568,plain,
( $false
| ~ spl0_4
| ~ spl0_28
| ~ spl0_128
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f2556,f809]) ).
fof(f2569,plain,
( ~ spl0_4
| ~ spl0_28
| ~ spl0_128
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f2568]) ).
fof(f2574,plain,
( ~ spl0_152
| ~ spl0_2
| ~ spl0_5
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f1101,f917,f212,f201,f927]) ).
fof(f2575,plain,
( ~ spl0_114
| ~ spl0_2
| ~ spl0_5
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f1103,f732,f212,f201,f737]) ).
fof(f2576,plain,
( ~ spl0_145
| ~ spl0_2
| ~ spl0_144
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f2173,f897,f887,f201,f892]) ).
fof(f2602,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_12
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f236,f253]) ).
fof(f2661,definition,
( spl0_156
<=> c2_1(a2172) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f2663,plain,
( c2_1(a2172)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f2661]) ).
fof(f2670,plain,
( spl0_156
| ~ spl0_16
| spl0_104
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f1571,f867,f687,f248,f2661]) ).
fof(f2700,plain,
( c0_1(a2068)
| ~ spl0_12
| ~ spl0_17
| ~ spl0_106 ),
inference(resolution,[],[f2602,f699]) ).
fof(f2701,plain,
( $false
| ~ spl0_12
| ~ spl0_17
| spl0_61
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f2700,f477]) ).
fof(f2702,plain,
( ~ spl0_12
| ~ spl0_17
| spl0_61
| ~ spl0_106 ),
inference(avatar_contradiction_clause,[],[f2701]) ).
fof(f2752,plain,
( c3_1(a2072)
| ~ spl0_8
| ~ spl0_19
| spl0_66 ),
inference(resolution,[],[f1575,f502]) ).
fof(f2753,plain,
( $false
| ~ spl0_8
| ~ spl0_19
| spl0_64
| spl0_66 ),
inference(forward_subsumption_resolution,[],[f2752,f492]) ).
fof(f2754,plain,
( ~ spl0_8
| ~ spl0_19
| spl0_64
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f2753]) ).
fof(f2781,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_7
| ~ spl0_26 ),
inference(forward_subsumption_resolution,[],[f219,f286]) ).
fof(f2793,plain,
( c3_1(a2071)
| ~ spl0_8
| ~ spl0_28
| ~ spl0_109 ),
inference(resolution,[],[f2040,f714]) ).
fof(f2829,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_1
| ~ spl0_6 ),
inference(forward_subsumption_resolution,[],[f216,f199]) ).
fof(f2837,plain,
( c2_1(a2095)
| ~ spl0_7
| ~ spl0_26
| ~ spl0_124 ),
inference(resolution,[],[f2781,f789]) ).
fof(f2856,plain,
( c1_1(a2130)
| ~ spl0_20
| ~ spl0_25
| spl0_94 ),
inference(resolution,[],[f1144,f642]) ).
fof(f2857,plain,
( c1_1(a2072)
| ~ spl0_20
| ~ spl0_25
| spl0_64 ),
inference(resolution,[],[f1144,f492]) ).
fof(f2858,plain,
( $false
| ~ spl0_20
| ~ spl0_25
| spl0_64
| spl0_65 ),
inference(forward_subsumption_resolution,[],[f2857,f497]) ).
fof(f2859,plain,
( ~ spl0_20
| ~ spl0_25
| spl0_64
| spl0_65 ),
inference(avatar_contradiction_clause,[],[f2858]) ).
fof(f2860,plain,
( $false
| ~ spl0_20
| ~ spl0_25
| spl0_94
| spl0_96 ),
inference(forward_subsumption_resolution,[],[f2856,f652]) ).
fof(f2861,plain,
( ~ spl0_20
| ~ spl0_25
| spl0_94
| spl0_96 ),
inference(avatar_contradiction_clause,[],[f2860]) ).
fof(f2871,plain,
( spl0_78
| ~ spl0_7
| ~ spl0_26
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f2837,f787,f285,f218,f560]) ).
fof(f2889,plain,
( c3_1(a2093)
| c1_1(a2093)
| ~ spl0_1
| ~ spl0_123 ),
inference(resolution,[],[f199,f784]) ).
fof(f2896,plain,
( c1_1(a2093)
| ~ spl0_1
| spl0_76
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f2889,f552]) ).
fof(f2900,plain,
( $false
| ~ spl0_1
| spl0_76
| spl0_77
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f2896,f557]) ).
fof(f2901,plain,
( ~ spl0_1
| spl0_76
| spl0_77
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f2900]) ).
fof(f2904,plain,
( ! [X2] :
( ~ c3_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f213,f243]) ).
fof(f2907,plain,
( ! [X2] :
( c0_1(X2)
| c1_1(X2) )
| ~ spl0_8
| ~ spl0_12
| ~ spl0_24 ),
inference(forward_subsumption_resolution,[],[f280,f2447]) ).
fof(f2932,plain,
( c2_1(a2070)
| ~ spl0_10
| ~ spl0_36
| ~ spl0_107 ),
inference(resolution,[],[f975,f704]) ).
fof(f2934,plain,
( $false
| ~ spl0_10
| ~ spl0_36
| spl0_62
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f2932,f482]) ).
fof(f2935,plain,
( ~ spl0_10
| ~ spl0_36
| spl0_62
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f2934]) ).
fof(f2956,plain,
( c0_1(a2140)
| ~ spl0_8
| ~ spl0_12
| ~ spl0_135 ),
inference(resolution,[],[f2447,f844]) ).
fof(f2963,plain,
( c0_1(a2082)
| ~ spl0_8
| ~ spl0_12
| ~ spl0_118 ),
inference(resolution,[],[f2447,f759]) ).
fof(f2974,plain,
( $false
| ~ spl0_8
| ~ spl0_12
| spl0_72
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f2963,f532]) ).
fof(f2975,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_72
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f2974]) ).
fof(f3025,definition,
( spl0_160
<=> c1_1(a2070) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f3027,plain,
( c1_1(a2070)
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f3025]) ).
fof(f3038,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_10
| ~ spl0_16
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f271,f1871]) ).
fof(f3077,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_5
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f213,f256]) ).
fof(f3081,plain,
( ! [X2] : ~ c1_1(X2)
| ~ spl0_5
| ~ spl0_10
| ~ spl0_16
| ~ spl0_18
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f3077,f3038]) ).
fof(f3125,plain,
( ! [X2] :
( c2_1(X2)
| c1_1(X2) )
| ~ spl0_24
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f280,f335]) ).
fof(f3170,plain,
( c0_1(a2068)
| ~ spl0_5
| ~ spl0_14
| ~ spl0_106 ),
inference(resolution,[],[f2904,f699]) ).
fof(f3171,plain,
( $false
| ~ spl0_5
| ~ spl0_14
| spl0_61
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f3170,f477]) ).
fof(f3172,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_61
| ~ spl0_106 ),
inference(avatar_contradiction_clause,[],[f3171]) ).
fof(f3189,plain,
( $false
| ~ spl0_5
| ~ spl0_10
| ~ spl0_16
| ~ spl0_18
| ~ spl0_22
| ~ spl0_148 ),
inference(resolution,[],[f3081,f909]) ).
fof(f3208,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_16
| ~ spl0_18
| ~ spl0_22
| ~ spl0_148 ),
inference(avatar_contradiction_clause,[],[f3189]) ).
fof(f3242,plain,
( c1_1(a2149)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_137 ),
inference(resolution,[],[f2829,f854]) ).
fof(f3244,plain,
( c1_1(a2110)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_129 ),
inference(resolution,[],[f2829,f814]) ).
fof(f3249,plain,
( c1_1(a2070)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_108 ),
inference(resolution,[],[f2829,f709]) ).
fof(f3258,plain,
( ~ c1_1(a2070)
| ~ spl0_10
| spl0_62
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f1985,f482]) ).
fof(f3259,plain,
( $false
| ~ spl0_10
| spl0_62
| ~ spl0_107
| ~ spl0_160 ),
inference(forward_subsumption_resolution,[],[f3258,f3027]) ).
fof(f3260,plain,
( ~ spl0_10
| spl0_62
| ~ spl0_107
| ~ spl0_160 ),
inference(avatar_contradiction_clause,[],[f3259]) ).
fof(f3262,plain,
( spl0_69
| ~ spl0_7
| ~ spl0_38
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f1322,f742,f334,f218,f515]) ).
fof(f3265,plain,
( ~ spl0_160
| ~ spl0_7
| spl0_62
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f2348,f707,f480,f218,f3025]) ).
fof(f3269,plain,
( ! [X1] :
( ~ c3_1(X1)
| c2_1(X1) )
| ~ spl0_7
| ~ spl0_26
| ~ spl0_36 ),
inference(forward_subsumption_resolution,[],[f328,f2781]) ).
fof(f3336,plain,
( c2_1(a2070)
| ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| ~ spl0_107 ),
inference(resolution,[],[f3269,f704]) ).
fof(f3337,plain,
( c2_1(a2068)
| ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| ~ spl0_106 ),
inference(resolution,[],[f3269,f699]) ).
fof(f3338,plain,
( $false
| ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| spl0_60
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f3337,f472]) ).
fof(f3339,plain,
( ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| spl0_60
| ~ spl0_106 ),
inference(avatar_contradiction_clause,[],[f3338]) ).
fof(f3340,plain,
( $false
| ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| spl0_62
| ~ spl0_107 ),
inference(forward_subsumption_resolution,[],[f3336,f482]) ).
fof(f3341,plain,
( ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| spl0_62
| ~ spl0_107 ),
inference(avatar_contradiction_clause,[],[f3340]) ).
fof(f3347,plain,
( spl0_100
| ~ spl0_1
| ~ spl0_6
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f3242,f852,f215,f198,f669]) ).
fof(f3354,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_1
| ~ spl0_6
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f271,f2829]) ).
fof(f3355,plain,
( spl0_160
| ~ spl0_1
| ~ spl0_6
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f3249,f707,f215,f198,f3025]) ).
fof(f3391,plain,
( spl0_63
| ~ spl0_8
| ~ spl0_28
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f2793,f712,f293,f222,f485]) ).
fof(f3406,plain,
( c3_1(a2087)
| ~ spl0_8
| ~ spl0_28
| ~ spl0_122 ),
inference(resolution,[],[f2040,f779]) ).
fof(f3409,plain,
( $false
| ~ spl0_8
| ~ spl0_28
| spl0_74
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f3406,f542]) ).
fof(f3410,plain,
( ~ spl0_8
| ~ spl0_28
| spl0_74
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f3409]) ).
fof(f3419,plain,
( c0_1(a2082)
| ~ spl0_5
| ~ spl0_18
| ~ spl0_119 ),
inference(resolution,[],[f3077,f764]) ).
fof(f3424,plain,
( $false
| ~ spl0_5
| ~ spl0_18
| spl0_72
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f3419,f532]) ).
fof(f3425,plain,
( ~ spl0_5
| ~ spl0_18
| spl0_72
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f3424]) ).
fof(f3430,plain,
( spl0_98
| ~ spl0_8
| ~ spl0_12
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f2956,f842,f235,f222,f660]) ).
fof(f3455,plain,
( c0_1(a2172)
| ~ spl0_8
| ~ spl0_12
| ~ spl0_156 ),
inference(resolution,[],[f2663,f2447]) ).
fof(f3456,plain,
( $false
| ~ spl0_8
| ~ spl0_12
| spl0_105
| ~ spl0_156 ),
inference(forward_subsumption_resolution,[],[f3455,f694]) ).
fof(f3457,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_105
| ~ spl0_156 ),
inference(avatar_contradiction_clause,[],[f3456]) ).
fof(f3471,plain,
( c1_1(a2072)
| ~ spl0_8
| ~ spl0_12
| ~ spl0_24
| spl0_66 ),
inference(resolution,[],[f2907,f502]) ).
fof(f3472,plain,
( $false
| ~ spl0_8
| ~ spl0_12
| ~ spl0_24
| spl0_65
| spl0_66 ),
inference(forward_subsumption_resolution,[],[f3471,f497]) ).
fof(f3473,plain,
( ~ spl0_8
| ~ spl0_12
| ~ spl0_24
| spl0_65
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f3472]) ).
fof(f3495,plain,
( c3_1(a2087)
| c1_1(a2087)
| ~ spl0_1
| ~ spl0_155 ),
inference(resolution,[],[f199,f2455]) ).
fof(f3500,plain,
( c1_1(a2087)
| ~ spl0_1
| spl0_74
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f3495,f542]) ).
fof(f3501,plain,
( $false
| ~ spl0_1
| spl0_74
| spl0_75
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f3500,f547]) ).
fof(f3502,plain,
( ~ spl0_1
| spl0_74
| spl0_75
| ~ spl0_155 ),
inference(avatar_contradiction_clause,[],[f3501]) ).
fof(f3533,plain,
( c1_1(a2130)
| ~ spl0_24
| ~ spl0_38
| spl0_95 ),
inference(resolution,[],[f3125,f647]) ).
fof(f3537,plain,
( $false
| ~ spl0_24
| ~ spl0_38
| spl0_95
| spl0_96 ),
inference(forward_subsumption_resolution,[],[f3533,f652]) ).
fof(f3538,plain,
( ~ spl0_24
| ~ spl0_38
| spl0_95
| spl0_96 ),
inference(avatar_contradiction_clause,[],[f3537]) ).
fof(f3553,plain,
( c0_1(a2076)
| ~ c1_1(a2076)
| ~ spl0_5
| ~ spl0_113 ),
inference(resolution,[],[f213,f734]) ).
fof(f3559,plain,
( ~ c1_1(a2076)
| ~ spl0_5
| spl0_68
| ~ spl0_113 ),
inference(forward_subsumption_resolution,[],[f3553,f512]) ).
fof(f3563,plain,
( $false
| ~ spl0_5
| spl0_68
| ~ spl0_113
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f3559,f739]) ).
fof(f3564,plain,
( ~ spl0_5
| spl0_68
| ~ spl0_113
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f3563]) ).
fof(f3568,plain,
( spl0_89
| ~ spl0_1
| ~ spl0_6
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f3244,f812,f215,f198,f615]) ).
fof(f3594,plain,
( ~ c2_1(a2071)
| ~ spl0_1
| ~ spl0_6
| ~ spl0_22
| ~ spl0_110 ),
inference(resolution,[],[f3354,f719]) ).
fof(f3596,plain,
( $false
| ~ spl0_1
| ~ spl0_6
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f3594,f714]) ).
fof(f3597,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f3596]) ).
fof(f3611,plain,
( $false
| ~ spl0_7
| ~ spl0_19
| ~ spl0_38
| spl0_94
| spl0_95 ),
inference(forward_subsumption_resolution,[],[f1436,f647]) ).
fof(f3612,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_38
| spl0_94
| spl0_95 ),
inference(avatar_contradiction_clause,[],[f3611]) ).
fof(f3657,plain,
( ~ c2_1(a2069)
| ~ spl0_15
| ~ spl0_37
| ~ spl0_141 ),
inference(resolution,[],[f2393,f874]) ).
fof(f3677,plain,
( $false
| ~ spl0_15
| ~ spl0_37
| ~ spl0_141
| ~ spl0_142 ),
inference(forward_subsumption_resolution,[],[f3657,f879]) ).
fof(f3678,plain,
( ~ spl0_15
| ~ spl0_37
| ~ spl0_141
| ~ spl0_142 ),
inference(avatar_contradiction_clause,[],[f3677]) ).
fof(f3735,plain,
( c0_1(a2140)
| ~ c2_1(a2140)
| ~ spl0_12
| ~ spl0_134 ),
inference(resolution,[],[f236,f839]) ).
fof(f3744,plain,
( ~ c2_1(a2140)
| ~ spl0_12
| spl0_98
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f3735,f662]) ).
fof(f3746,plain,
( $false
| ~ spl0_12
| spl0_98
| ~ spl0_134
| ~ spl0_135 ),
inference(forward_subsumption_resolution,[],[f3744,f844]) ).
fof(f3747,plain,
( ~ spl0_12
| spl0_98
| ~ spl0_134
| ~ spl0_135 ),
inference(avatar_contradiction_clause,[],[f3746]) ).
fof(f3780,plain,
( ~ c3_1(a2073)
| ~ spl0_4
| ~ spl0_9
| ~ spl0_146 ),
inference(resolution,[],[f972,f899]) ).
fof(f3786,plain,
( $false
| ~ spl0_4
| ~ spl0_9
| ~ spl0_144
| ~ spl0_146 ),
inference(forward_subsumption_resolution,[],[f3780,f889]) ).
fof(f3787,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_144
| ~ spl0_146 ),
inference(avatar_contradiction_clause,[],[f3786]) ).
fof(f3809,plain,
( c2_1(a2070)
| ~ c3_1(a2070)
| ~ spl0_9
| ~ spl0_108 ),
inference(resolution,[],[f709,f226]) ).
fof(f3816,plain,
( ~ c3_1(a2070)
| ~ spl0_9
| spl0_62
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f3809,f482]) ).
fof(f3817,plain,
( $false
| ~ spl0_9
| spl0_62
| ~ spl0_107
| ~ spl0_108 ),
inference(forward_subsumption_resolution,[],[f3816,f704]) ).
fof(f3818,plain,
( ~ spl0_9
| spl0_62
| ~ spl0_107
| ~ spl0_108 ),
inference(avatar_contradiction_clause,[],[f3817]) ).
fof(f3953,plain,
( c0_1(a2082)
| ~ c1_1(a2082)
| ~ spl0_45
| ~ spl0_118 ),
inference(resolution,[],[f375,f759]) ).
fof(f3957,plain,
( ~ c1_1(a2082)
| ~ spl0_45
| spl0_72
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f3953,f532]) ).
fof(f3960,plain,
( $false
| ~ spl0_45
| spl0_72
| ~ spl0_118
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f3957,f764]) ).
fof(f3961,plain,
( ~ spl0_45
| spl0_72
| ~ spl0_118
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f3960]) ).
fof(f4055,plain,
( c2_1(a2068)
| c0_1(a2068)
| ~ spl0_17
| ~ spl0_106 ),
inference(resolution,[],[f253,f699]) ).
fof(f4056,plain,
( c0_1(a2068)
| ~ spl0_17
| spl0_60
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f4055,f472]) ).
fof(f4062,plain,
( $false
| ~ spl0_17
| spl0_60
| spl0_61
| ~ spl0_106 ),
inference(forward_subsumption_resolution,[],[f4056,f477]) ).
fof(f4063,plain,
( ~ spl0_17
| spl0_60
| spl0_61
| ~ spl0_106 ),
inference(avatar_contradiction_clause,[],[f4062]) ).
fof(f4073,plain,
( ~ spl0_142
| ~ spl0_4
| ~ spl0_141
| ~ spl0_143 ),
inference(avatar_split_clause,[],[f1944,f882,f872,f208,f877]) ).
fof(f4169,plain,
( ~ c2_1(a2071)
| ~ c1_1(a2071)
| ~ spl0_22
| ~ spl0_110 ),
inference(resolution,[],[f271,f719]) ).
fof(f4171,plain,
( ~ c2_1(a2071)
| ~ spl0_15
| ~ spl0_20
| ~ spl0_22
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f4169,f974]) ).
fof(f4178,plain,
( $false
| ~ spl0_15
| ~ spl0_20
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f4171,f714]) ).
fof(f4179,plain,
( ~ spl0_15
| ~ spl0_20
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f4178]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f210]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f220]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f230]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_11
| spl0_12
| spl0_13 ),
inference(sat_conversion,[],[f240]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_10
| spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f264]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_15
| spl0_21
| spl0_22 ),
inference(sat_conversion,[],[f272]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_12
| spl0_22
| spl0_23 ),
inference(sat_conversion,[],[f277]) ).
cnf(s10,plain,
( ~ spl0_3
| spl0_24
| spl0_25
| spl0_26 ),
inference(sat_conversion,[],[f287]) ).
cnf(s11,plain,
( ~ spl0_3
| spl0_9
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f295]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_7
| spl0_10
| spl0_31 ),
inference(sat_conversion,[],[f308]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_9
| spl0_15
| spl0_34 ),
inference(sat_conversion,[],[f321]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_35
| spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f332]) ).
cnf(s18,plain,
( ~ spl0_3
| spl0_12
| spl0_15
| spl0_39 ),
inference(sat_conversion,[],[f341]) ).
cnf(s20,plain,
( ~ spl0_3
| spl0_4
| spl0_18
| spl0_27 ),
inference(sat_conversion,[],[f343]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_4
| spl0_17
| spl0_40 ),
inference(sat_conversion,[],[f348]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_6
| spl0_16
| spl0_35 ),
inference(sat_conversion,[],[f354]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_6
| spl0_16
| spl0_42 ),
inference(sat_conversion,[],[f359]) ).
cnf(s25,plain,
( spl0_1
| ~ spl0_3
| spl0_10
| spl0_34 ),
inference(sat_conversion,[],[f360]) ).
cnf(s26,plain,
( spl0_1
| ~ spl0_3
| spl0_15
| spl0_23 ),
inference(sat_conversion,[],[f361]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_5
| spl0_36
| spl0_44 ),
inference(sat_conversion,[],[f372]) ).
cnf(s30,plain,
( ~ spl0_3
| spl0_20
| spl0_32
| spl0_45 ),
inference(sat_conversion,[],[f376]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_8
| spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f382]) ).
cnf(s36,plain,
( ~ spl0_3
| spl0_6
| spl0_14
| spl0_49 ),
inference(sat_conversion,[],[f398]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_4
| spl0_24
| spl0_51 ),
inference(sat_conversion,[],[f408]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_8
| spl0_32
| spl0_38 ),
inference(sat_conversion,[],[f414]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_17
| spl0_27
| spl0_36 ),
inference(sat_conversion,[],[f415]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_20
| spl0_26
| spl0_35 ),
inference(sat_conversion,[],[f416]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_20
| spl0_27
| spl0_53 ),
inference(sat_conversion,[],[f420]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_11
| spl0_39
| spl0_53 ),
inference(sat_conversion,[],[f421]) ).
cnf(s45,plain,
( spl0_2
| ~ spl0_3
| spl0_42
| spl0_54 ),
inference(sat_conversion,[],[f426]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_15
| spl0_41
| spl0_44 ),
inference(sat_conversion,[],[f435]) ).
cnf(s51,plain,
( ~ spl0_3
| spl0_6
| spl0_32
| spl0_40 ),
inference(sat_conversion,[],[f436]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_6
| spl0_23
| spl0_31 ),
inference(sat_conversion,[],[f437]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_12
| spl0_32
| spl0_51 ),
inference(sat_conversion,[],[f438]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_12
| spl0_39
| spl0_50 ),
inference(sat_conversion,[],[f439]) ).
cnf(s56,plain,
( ~ spl0_3
| spl0_7
| spl0_54 ),
inference(sat_conversion,[],[f445]) ).
cnf(s58,plain,
( spl0_1
| ~ spl0_3
| spl0_35
| spl0_46 ),
inference(sat_conversion,[],[f451]) ).
cnf(s59,plain,
( ~ spl0_3
| spl0_23
| spl0_36
| spl0_58 ),
inference(sat_conversion,[],[f456]) ).
cnf(s60,plain,
( ~ spl0_3
| spl0_5
| spl0_51 ),
inference(sat_conversion,[],[f457]) ).
cnf(s63,plain,
( ~ spl0_3
| spl0_25
| spl0_42
| spl0_46 ),
inference(sat_conversion,[],[f464]) ).
cnf(s65,plain,
( ~ spl0_3
| spl0_31
| spl0_53
| spl0_56 ),
inference(sat_conversion,[],[f466]) ).
cnf(s67,plain,
( ~ spl0_3
| spl0_23
| spl0_24
| spl0_46 ),
inference(sat_conversion,[],[f468]) ).
cnf(s68,plain,
( ~ spl0_51
| ~ spl0_60 ),
inference(sat_conversion,[],[f473]) ).
cnf(s69,plain,
( ~ spl0_51
| ~ spl0_61 ),
inference(sat_conversion,[],[f478]) ).
cnf(s70,plain,
( ~ spl0_46
| ~ spl0_62 ),
inference(sat_conversion,[],[f483]) ).
cnf(s71,plain,
( ~ spl0_48
| ~ spl0_63 ),
inference(sat_conversion,[],[f488]) ).
cnf(s72,plain,
( ~ spl0_34
| ~ spl0_64 ),
inference(sat_conversion,[],[f493]) ).
cnf(s73,plain,
( ~ spl0_34
| ~ spl0_65 ),
inference(sat_conversion,[],[f498]) ).
cnf(s74,plain,
( ~ spl0_34
| ~ spl0_66 ),
inference(sat_conversion,[],[f503]) ).
cnf(s75,plain,
( ~ spl0_27
| ~ spl0_67 ),
inference(sat_conversion,[],[f508]) ).
cnf(s76,plain,
( ~ spl0_31
| ~ spl0_68 ),
inference(sat_conversion,[],[f513]) ).
cnf(s77,plain,
( ~ spl0_49
| ~ spl0_69 ),
inference(sat_conversion,[],[f518]) ).
cnf(s80,plain,
( ~ spl0_35
| ~ spl0_72 ),
inference(sat_conversion,[],[f533]) ).
cnf(s82,plain,
( ~ spl0_40
| ~ spl0_74 ),
inference(sat_conversion,[],[f543]) ).
cnf(s83,plain,
( ~ spl0_40
| ~ spl0_75 ),
inference(sat_conversion,[],[f548]) ).
cnf(s84,plain,
( ~ spl0_32
| ~ spl0_76 ),
inference(sat_conversion,[],[f553]) ).
cnf(s85,plain,
( ~ spl0_32
| ~ spl0_77 ),
inference(sat_conversion,[],[f558]) ).
cnf(s86,plain,
( ~ spl0_29
| ~ spl0_78 ),
inference(sat_conversion,[],[f563]) ).
cnf(s94,plain,
( ~ spl0_44
| ~ spl0_86 ),
inference(sat_conversion,[],[f603]) ).
cnf(s97,plain,
( ~ spl0_42
| ~ spl0_89 ),
inference(sat_conversion,[],[f618]) ).
cnf(s98,plain,
( ~ spl0_58
| ~ spl0_90 ),
inference(sat_conversion,[],[f623]) ).
cnf(s99,plain,
( ~ spl0_58
| ~ spl0_91 ),
inference(sat_conversion,[],[f628]) ).
cnf(s102,plain,
( ~ spl0_21
| ~ spl0_94 ),
inference(sat_conversion,[],[f643]) ).
cnf(s103,plain,
( ~ spl0_21
| ~ spl0_95 ),
inference(sat_conversion,[],[f648]) ).
cnf(s104,plain,
( ~ spl0_21
| ~ spl0_96 ),
inference(sat_conversion,[],[f653]) ).
cnf(s106,plain,
( ~ spl0_54
| ~ spl0_98 ),
inference(sat_conversion,[],[f663]) ).
cnf(s107,plain,
( ~ spl0_99
| ~ spl0_100 ),
inference(sat_conversion,[],[f672]) ).
cnf(s109,plain,
( ~ spl0_103
| ~ spl0_104 ),
inference(sat_conversion,[],[f690]) ).
cnf(s110,plain,
( ~ spl0_103
| ~ spl0_105 ),
inference(sat_conversion,[],[f695]) ).
cnf(s111,plain,
( ~ spl0_51
| spl0_106 ),
inference(sat_conversion,[],[f700]) ).
cnf(s112,plain,
( ~ spl0_46
| spl0_107 ),
inference(sat_conversion,[],[f705]) ).
cnf(s113,plain,
( ~ spl0_46
| spl0_108 ),
inference(sat_conversion,[],[f710]) ).
cnf(s114,plain,
( ~ spl0_48
| spl0_109 ),
inference(sat_conversion,[],[f715]) ).
cnf(s115,plain,
( ~ spl0_48
| spl0_110 ),
inference(sat_conversion,[],[f720]) ).
cnf(s116,plain,
( ~ spl0_27
| spl0_111 ),
inference(sat_conversion,[],[f725]) ).
cnf(s117,plain,
( ~ spl0_27
| spl0_112 ),
inference(sat_conversion,[],[f730]) ).
cnf(s118,plain,
( ~ spl0_31
| spl0_113 ),
inference(sat_conversion,[],[f735]) ).
cnf(s119,plain,
( ~ spl0_31
| spl0_114 ),
inference(sat_conversion,[],[f740]) ).
cnf(s120,plain,
( ~ spl0_49
| spl0_115 ),
inference(sat_conversion,[],[f745]) ).
cnf(s121,plain,
( ~ spl0_41
| spl0_116 ),
inference(sat_conversion,[],[f750]) ).
cnf(s122,plain,
( ~ spl0_41
| spl0_117 ),
inference(sat_conversion,[],[f755]) ).
cnf(s123,plain,
( ~ spl0_35
| spl0_118 ),
inference(sat_conversion,[],[f760]) ).
cnf(s124,plain,
( ~ spl0_35
| spl0_119 ),
inference(sat_conversion,[],[f765]) ).
cnf(s127,plain,
( ~ spl0_40
| spl0_122 ),
inference(sat_conversion,[],[f780]) ).
cnf(s128,plain,
( ~ spl0_32
| spl0_123 ),
inference(sat_conversion,[],[f785]) ).
cnf(s129,plain,
( ~ spl0_29
| spl0_124 ),
inference(sat_conversion,[],[f790]) ).
cnf(s131,plain,
( ~ spl0_44
| spl0_126 ),
inference(sat_conversion,[],[f800]) ).
cnf(s133,plain,
( ~ spl0_42
| spl0_128 ),
inference(sat_conversion,[],[f810]) ).
cnf(s134,plain,
( ~ spl0_42
| spl0_129 ),
inference(sat_conversion,[],[f815]) ).
cnf(s135,plain,
( ~ spl0_58
| spl0_130 ),
inference(sat_conversion,[],[f820]) ).
cnf(s139,plain,
( ~ spl0_54
| spl0_134 ),
inference(sat_conversion,[],[f840]) ).
cnf(s140,plain,
( ~ spl0_54
| spl0_135 ),
inference(sat_conversion,[],[f845]) ).
cnf(s142,plain,
( ~ spl0_99
| spl0_137 ),
inference(sat_conversion,[],[f855]) ).
cnf(s145,plain,
( ~ spl0_103
| spl0_140 ),
inference(sat_conversion,[],[f870]) ).
cnf(s146,plain,
( ~ spl0_23
| spl0_141 ),
inference(sat_conversion,[],[f875]) ).
cnf(s147,plain,
( ~ spl0_23
| spl0_142 ),
inference(sat_conversion,[],[f880]) ).
cnf(s148,plain,
( ~ spl0_23
| spl0_143 ),
inference(sat_conversion,[],[f885]) ).
cnf(s149,plain,
( ~ spl0_39
| spl0_144 ),
inference(sat_conversion,[],[f890]) ).
cnf(s150,plain,
( ~ spl0_39
| spl0_145 ),
inference(sat_conversion,[],[f895]) ).
cnf(s151,plain,
( ~ spl0_39
| spl0_146 ),
inference(sat_conversion,[],[f900]) ).
cnf(s153,plain,
( ~ spl0_56
| spl0_148 ),
inference(sat_conversion,[],[f910]) ).
cnf(s154,plain,
( ~ spl0_56
| spl0_149 ),
inference(sat_conversion,[],[f915]) ).
cnf(s155,plain,
( ~ spl0_50
| spl0_150 ),
inference(sat_conversion,[],[f920]) ).
cnf(s157,plain,
( ~ spl0_50
| spl0_152 ),
inference(sat_conversion,[],[f930]) ).
cnf(s158,plain,
( spl0_29
| spl0_58
| spl0_103 ),
inference(sat_conversion,[],[f931]) ).
cnf(s162,plain,
( spl0_31
| spl0_99
| spl0_101 ),
inference(sat_conversion,[],[f935]) ).
cnf(s163,plain,
( spl0_42
| spl0_46
| spl0_99 ),
inference(sat_conversion,[],[f936]) ).
cnf(s171,plain,
( spl0_3
| ~ spl0_31 ),
inference(sat_conversion,[],[f944]) ).
cnf(s189,plain,
( spl0_3
| ~ spl0_99 ),
inference(sat_conversion,[],[f962]) ).
cnf(s190,plain,
( spl0_3
| ~ spl0_101 ),
inference(sat_conversion,[],[f963]) ).
cnf(s196,plain,
( spl0_42
| spl0_48 ),
inference(sat_conversion,[],[f969]) ).
cnf(s203,plain,
( ~ spl0_2
| ~ spl0_6
| ~ spl0_107
| ~ spl0_108 ),
inference(sat_conversion,[],[f1004]) ).
cnf(s226,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_111
| ~ spl0_112 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s257,plain,
( ~ spl0_7
| ~ spl0_24
| ~ spl0_26
| ~ spl0_38
| spl0_67 ),
inference(sat_conversion,[],[f1241]) ).
cnf(s261,plain,
( ~ spl0_15
| ~ spl0_20
| spl0_89
| ~ spl0_128 ),
inference(sat_conversion,[],[f1247]) ).
cnf(s263,plain,
( ~ spl0_7
| ~ spl0_38
| spl0_86
| ~ spl0_126 ),
inference(sat_conversion,[],[f1258]) ).
cnf(s285,plain,
( ~ spl0_11
| ~ spl0_24
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f1337]) ).
cnf(s335,plain,
( ~ spl0_16
| spl0_90
| spl0_91
| ~ spl0_130 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s336,plain,
( ~ spl0_18
| ~ spl0_53
| spl0_64
| spl0_66 ),
inference(sat_conversion,[],[f1577]) ).
cnf(s338,plain,
( ~ spl0_1
| ~ spl0_53
| spl0_74
| spl0_75 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s399,plain,
( ~ spl0_13
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f1862]) ).
cnf(s400,plain,
( ~ spl0_13
| ~ spl0_22
| ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f1864]) ).
cnf(s403,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_141
| ~ spl0_143 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s438,plain,
( ~ spl0_10
| spl0_67
| ~ spl0_111
| ~ spl0_112 ),
inference(sat_conversion,[],[f2157]) ).
cnf(s507,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_107
| ~ spl0_108 ),
inference(sat_conversion,[],[f2359]) ).
cnf(s509,plain,
( ~ spl0_10
| ~ spl0_36
| spl0_60
| ~ spl0_106 ),
inference(sat_conversion,[],[f2363]) ).
cnf(s510,plain,
( ~ spl0_7
| ~ spl0_22
| ~ spl0_148
| ~ spl0_149 ),
inference(sat_conversion,[],[f2372]) ).
cnf(s514,plain,
( ~ spl0_7
| ~ spl0_22
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f2376]) ).
cnf(s517,plain,
( ~ spl0_15
| ~ spl0_20
| spl0_75
| ~ spl0_122 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s539,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_9
| ~ spl0_11
| ~ spl0_24
| ~ spl0_150 ),
inference(sat_conversion,[],[f2446]) ).
cnf(s541,plain,
( ~ spl0_8
| spl0_74
| ~ spl0_122
| spl0_155 ),
inference(sat_conversion,[],[f2456]) ).
cnf(s564,plain,
( ~ spl0_4
| ~ spl0_28
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f2565]) ).
cnf(s566,plain,
( ~ spl0_4
| ~ spl0_28
| ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f2569]) ).
cnf(s569,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_150
| ~ spl0_152 ),
inference(sat_conversion,[],[f2574]) ).
cnf(s570,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f2575]) ).
cnf(s571,plain,
( ~ spl0_2
| ~ spl0_144
| ~ spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f2576]) ).
cnf(s598,plain,
( ~ spl0_16
| spl0_104
| ~ spl0_140
| spl0_156 ),
inference(sat_conversion,[],[f2670]) ).
cnf(s601,plain,
( ~ spl0_12
| ~ spl0_17
| spl0_61
| ~ spl0_106 ),
inference(sat_conversion,[],[f2702]) ).
cnf(s614,plain,
( ~ spl0_8
| ~ spl0_19
| spl0_64
| spl0_66 ),
inference(sat_conversion,[],[f2754]) ).
cnf(s635,plain,
( ~ spl0_20
| ~ spl0_25
| spl0_64
| spl0_65 ),
inference(sat_conversion,[],[f2859]) ).
cnf(s636,plain,
( ~ spl0_20
| ~ spl0_25
| spl0_94
| spl0_96 ),
inference(sat_conversion,[],[f2861]) ).
cnf(s641,plain,
( ~ spl0_7
| ~ spl0_26
| spl0_78
| ~ spl0_124 ),
inference(sat_conversion,[],[f2871]) ).
cnf(s642,plain,
( ~ spl0_1
| spl0_76
| spl0_77
| ~ spl0_123 ),
inference(sat_conversion,[],[f2901]) ).
cnf(s652,plain,
( ~ spl0_10
| ~ spl0_36
| spl0_62
| ~ spl0_107 ),
inference(sat_conversion,[],[f2935]) ).
cnf(s657,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_72
| ~ spl0_118 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s732,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_61
| ~ spl0_106 ),
inference(sat_conversion,[],[f3172]) ).
cnf(s749,plain,
( ~ spl0_5
| ~ spl0_10
| ~ spl0_16
| ~ spl0_18
| ~ spl0_22
| ~ spl0_148 ),
inference(sat_conversion,[],[f3208]) ).
cnf(s769,plain,
( ~ spl0_10
| spl0_62
| ~ spl0_107
| ~ spl0_160 ),
inference(sat_conversion,[],[f3260]) ).
cnf(s770,plain,
( ~ spl0_7
| ~ spl0_38
| spl0_69
| ~ spl0_115 ),
inference(sat_conversion,[],[f3262]) ).
cnf(s771,plain,
( ~ spl0_7
| spl0_62
| ~ spl0_108
| ~ spl0_160 ),
inference(sat_conversion,[],[f3265]) ).
cnf(s786,plain,
( ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| spl0_60
| ~ spl0_106 ),
inference(sat_conversion,[],[f3339]) ).
cnf(s787,plain,
( ~ spl0_7
| ~ spl0_26
| ~ spl0_36
| spl0_62
| ~ spl0_107 ),
inference(sat_conversion,[],[f3341]) ).
cnf(s790,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_100
| ~ spl0_137 ),
inference(sat_conversion,[],[f3347]) ).
cnf(s794,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_108
| spl0_160 ),
inference(sat_conversion,[],[f3355]) ).
cnf(s801,plain,
( ~ spl0_8
| ~ spl0_28
| spl0_63
| ~ spl0_109 ),
inference(sat_conversion,[],[f3391]) ).
cnf(s804,plain,
( ~ spl0_8
| ~ spl0_28
| spl0_74
| ~ spl0_122 ),
inference(sat_conversion,[],[f3410]) ).
cnf(s807,plain,
( ~ spl0_5
| ~ spl0_18
| spl0_72
| ~ spl0_119 ),
inference(sat_conversion,[],[f3425]) ).
cnf(s810,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_98
| ~ spl0_135 ),
inference(sat_conversion,[],[f3430]) ).
cnf(s813,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_105
| ~ spl0_156 ),
inference(sat_conversion,[],[f3457]) ).
cnf(s814,plain,
( ~ spl0_8
| ~ spl0_12
| ~ spl0_24
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f3473]) ).
cnf(s820,plain,
( ~ spl0_1
| spl0_74
| spl0_75
| ~ spl0_155 ),
inference(sat_conversion,[],[f3502]) ).
cnf(s826,plain,
( ~ spl0_24
| ~ spl0_38
| spl0_95
| spl0_96 ),
inference(sat_conversion,[],[f3538]) ).
cnf(s829,plain,
( ~ spl0_5
| spl0_68
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f3564]) ).
cnf(s831,plain,
( ~ spl0_1
| ~ spl0_6
| spl0_89
| ~ spl0_129 ),
inference(sat_conversion,[],[f3568]) ).
cnf(s837,plain,
( ~ spl0_1
| ~ spl0_6
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f3597]) ).
cnf(s845,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_38
| spl0_94
| spl0_95 ),
inference(sat_conversion,[],[f3612]) ).
cnf(s859,plain,
( ~ spl0_15
| ~ spl0_37
| ~ spl0_141
| ~ spl0_142 ),
inference(sat_conversion,[],[f3678]) ).
cnf(s869,plain,
( ~ spl0_12
| spl0_98
| ~ spl0_134
| ~ spl0_135 ),
inference(sat_conversion,[],[f3747]) ).
cnf(s878,plain,
( ~ spl0_4
| ~ spl0_9
| ~ spl0_144
| ~ spl0_146 ),
inference(sat_conversion,[],[f3787]) ).
cnf(s890,plain,
( ~ spl0_9
| spl0_62
| ~ spl0_107
| ~ spl0_108 ),
inference(sat_conversion,[],[f3818]) ).
cnf(s899,plain,
( ~ spl0_45
| spl0_72
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f3961]) ).
cnf(s928,plain,
( ~ spl0_17
| spl0_60
| spl0_61
| ~ spl0_106 ),
inference(sat_conversion,[],[f4063]) ).
cnf(s933,plain,
( ~ spl0_4
| ~ spl0_141
| ~ spl0_142
| ~ spl0_143 ),
inference(sat_conversion,[],[f4073]) ).
cnf(s938,plain,
( ~ spl0_15
| ~ spl0_20
| ~ spl0_22
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f4179]) ).
cnf(s943,plain,
spl0_3,
inference(rat,[],[s162,s171,s189,s190]) ).
cnf(s944,plain,
( ~ spl0_10
| ~ spl0_51 ),
inference(rat,[],[s438,s75,s116,s117,s41,s509,s928,s68,s69,s111,s943]) ).
cnf(s945,plain,
( ~ spl0_23
| ~ spl0_9
| ~ spl0_4 ),
inference(rat,[],[s403,s146,s148]) ).
cnf(s946,plain,
( spl0_12
| spl0_11
| ~ spl0_42
| spl0_23 ),
inference(rat,[],[s400,s9,s4,s134,s133,s943]) ).
cnf(s947,plain,
( ~ spl0_39
| ~ spl0_9
| ~ spl0_4 ),
inference(rat,[],[s878,s149,s151]) ).
cnf(s948,plain,
( ~ spl0_46
| ~ spl0_9
| ~ spl0_4 ),
inference(rat,[],[s507,s112,s113]) ).
cnf(s949,plain,
( spl0_8
| spl0_10
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s899,s80,s123,s124,s58,s32,s948,s3,s943]) ).
cnf(s950,plain,
( ~ spl0_9
| spl0_25
| ~ spl0_8
| spl0_65
| spl0_66
| ~ spl0_4 ),
inference(rat,[],[s946,s814,s285,s63,s67,s948,s945,s943]) ).
cnf(s951,plain,
( ~ spl0_23
| ~ spl0_4 ),
inference(rat,[],[s933,s146,s147,s148]) ).
cnf(s952,plain,
( ~ spl0_42
| ~ spl0_20
| ~ spl0_15 ),
inference(rat,[],[s261,s97,s133]) ).
cnf(s953,plain,
( ~ spl0_20
| ~ spl0_15
| spl0_23
| spl0_2 ),
inference(rat,[],[s9,s869,s938,s106,s139,s140,s114,s115,s45,s196,s952,s943]) ).
cnf(s954,plain,
( spl0_46
| spl0_8
| spl0_1 ),
inference(rat,[],[s899,s80,s123,s124,s58,s32,s943]) ).
cnf(s955,plain,
( ~ spl0_27
| ~ spl0_10 ),
inference(rat,[],[s438,s75,s116,s117]) ).
cnf(s956,plain,
( ~ spl0_48
| ~ spl0_28
| ~ spl0_4 ),
inference(rat,[],[s564,s114,s115]) ).
cnf(s957,plain,
( ~ spl0_28
| ~ spl0_4 ),
inference(rat,[],[s566,s133,s134,s196,s956]) ).
cnf(s958,plain,
( spl0_10
| spl0_2
| spl0_1 ),
inference(rat,[],[s614,s72,s74,s7,s949,s25,s953,s26,s951,s1,s943]) ).
cnf(s959,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s399,s114,s115,s196,s4,s946,s539,s155,s54,s9,s657,s80,s123,s954,s67,s58,s948,s947,s11,s60,s955,s944,s958,s957,s951,s1,s943]) ).
cnf(s960,plain,
( spl0_10
| ~ spl0_4
| spl0_1 ),
inference(rat,[],[s335,s98,s99,s135,s59,s787,s10,s814,s24,s2,s9,s226,s203,s938,s116,s117,s70,s112,s113,s114,s115,s11,s63,s196,s950,s952,s635,s7,s614,s72,s73,s74,s949,s25,s959,s957,s26,s951,s943]) ).
cnf(s961,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s569,s155,s157,s54,s657,s80,s123,s954,s58,s948,s947,s11,s60,s955,s944,s960,s957,s959,s943]) ).
cnf(s962,plain,
( spl0_8
| spl0_10
| spl0_1 ),
inference(rat,[],[s890,s70,s112,s113,s3,s954,s943]) ).
cnf(s963,plain,
( ~ spl0_39
| ~ spl0_2 ),
inference(rat,[],[s571,s149,s150,s151]) ).
cnf(s964,plain,
( spl0_46
| spl0_10
| spl0_1 ),
inference(rat,[],[s18,s657,s952,s80,s123,s63,s58,s963,s959,s635,s7,s614,s962,s74,s72,s73,s25,s943]) ).
cnf(s965,plain,
( ~ spl0_103
| ~ spl0_12
| ~ spl0_16
| ~ spl0_8 ),
inference(rat,[],[s598,s813,s109,s110,s145]) ).
cnf(s966,plain,
( ~ spl0_29
| ~ spl0_26
| ~ spl0_7 ),
inference(rat,[],[s641,s86,s129]) ).
cnf(s967,plain,
( spl0_42
| spl0_10
| spl0_1 ),
inference(rat,[],[s335,s98,s99,s135,s158,s966,s965,s10,s814,s18,s517,s83,s127,s21,s928,s68,s69,s111,s2,s60,s226,s116,s117,s11,s801,s71,s114,s24,s196,s961,s963,s635,s7,s614,s962,s74,s72,s73,s25,s203,s959,s890,s112,s70,s113,s964,s943]) ).
cnf(s968,plain,
( ~ spl0_16
| spl0_29
| ~ spl0_12
| ~ spl0_8 ),
inference(rat,[],[s335,s98,s99,s135,s158,s965]) ).
cnf(s969,plain,
( spl0_10
| spl0_1 ),
inference(rat,[],[s657,s80,s123,s23,s968,s966,s2,s226,s116,s117,s11,s804,s82,s127,s21,s601,s69,s111,s38,s10,s814,s18,s952,s967,s890,s203,s70,s112,s113,s964,s635,s7,s614,s962,s72,s73,s74,s25,s961,s963,s959,s943]) ).
cnf(s970,plain,
( ~ spl0_46
| ~ spl0_9 ),
inference(rat,[],[s890,s70,s112,s113]) ).
cnf(s971,plain,
( ~ spl0_35
| spl0_1 ),
inference(rat,[],[s807,s80,s124,s60,s944,s20,s955,s969,s961,s943]) ).
cnf(s974,plain,
( ~ spl0_34
| spl0_1 ),
inference(rat,[],[s44,s285,s336,s72,s73,s74,s963,s959,s38,s944,s20,s955,s969,s961,s943]) ).
cnf(s975,plain,
( ~ spl0_23
| spl0_1 ),
inference(rat,[],[s859,s146,s147,s16,s652,s70,s969,s112,s15,s974,s970,s58,s971,s943]) ).
cnf(s976,plain,
spl0_1,
inference(rat,[],[s570,s118,s119,s52,s975,s203,s112,s113,s58,s971,s60,s944,s969,s959,s943]) ).
cnf(s977,plain,
( ~ spl0_40
| ~ spl0_8 ),
inference(rat,[],[s541,s820,s82,s83,s127,s976]) ).
cnf(s980,plain,
~ spl0_32,
inference(rat,[],[s642,s84,s85,s128,s976]) ).
cnf(s981,plain,
( ~ spl0_99
| ~ spl0_6 ),
inference(rat,[],[s790,s107,s142,s976]) ).
cnf(s983,plain,
( ~ spl0_31
| ~ spl0_5 ),
inference(rat,[],[s829,s76,s118,s119]) ).
cnf(s984,plain,
( ~ spl0_46
| ~ spl0_7
| ~ spl0_6 ),
inference(rat,[],[s771,s794,s70,s113,s976]) ).
cnf(s985,plain,
( ~ spl0_42
| ~ spl0_6 ),
inference(rat,[],[s831,s97,s134,s976]) ).
cnf(s986,plain,
~ spl0_8,
inference(rat,[],[s928,s21,s68,s69,s111,s951,s53,s9,s810,s106,s140,s56,s837,s984,s114,s115,s163,s196,s985,s981,s51,s977,s943,s980,s976]) ).
cnf(s987,plain,
spl0_38,
inference(rat,[],[s40,s943,s986,s980]) ).
cnf(s988,plain,
( spl0_5
| spl0_15
| ~ spl0_116
| ~ spl0_117
| spl0_60
| ~ spl0_106
| spl0_24
| spl0_10
| spl0_6 ),
inference(rat,[],[s263,s94,s131,s29,s786,s10,s636,s7,s845,s102,s103,s104,s8,s514,s2,s987,s943]) ).
cnf(s989,plain,
( ~ spl0_5
| ~ spl0_51
| spl0_10
| spl0_6 ),
inference(rat,[],[s770,s77,s120,s36,s13,s732,s983,s111,s69,s987,s943]) ).
cnf(s992,plain,
( ~ spl0_44
| ~ spl0_7 ),
inference(rat,[],[s263,s94,s131,s987]) ).
cnf(s993,plain,
( spl0_5
| spl0_15
| spl0_10
| spl0_6 ),
inference(rat,[],[s826,s103,s104,s8,s514,s988,s121,s122,s50,s992,s68,s111,s2,s60,s987,s943]) ).
cnf(s994,plain,
( spl0_15
| spl0_10
| spl0_6
| spl0_4 ),
inference(rat,[],[s826,s103,s104,s8,s510,s153,s154,s38,s65,s13,s989,s983,s993,s338,s82,s83,s51,s987,s943,s980,s976]) ).
cnf(s995,plain,
( ~ spl0_35
| ~ spl0_45 ),
inference(rat,[],[s899,s80,s123,s124]) ).
cnf(s996,plain,
( spl0_5
| ~ spl0_26
| spl0_6 ),
inference(rat,[],[s29,s786,s992,s68,s111,s2,s60,s943]) ).
cnf(s997,plain,
( spl0_10
| spl0_6
| spl0_4 ),
inference(rat,[],[s257,s38,s13,s989,s983,s996,s42,s995,s75,s43,s517,s994,s32,s970,s3,s127,s338,s82,s83,s51,s987,s943,s986,s980,s976]) ).
cnf(s998,plain,
( ~ spl0_21
| ~ spl0_24 ),
inference(rat,[],[s826,s103,s104,s987]) ).
cnf(s999,plain,
( spl0_6
| spl0_4 ),
inference(rat,[],[s807,s80,s124,s23,s749,s8,s998,s153,s65,s517,s983,s43,s20,s38,s60,s955,s944,s997,s338,s82,s83,s127,s51,s943,s976,s980]) ).
cnf(s1000,plain,
~ spl0_6,
inference(rat,[],[s769,s3,s794,s970,s70,s112,s113,s163,s985,s981,s986,s943,s976]) ).
cnf(s1001,plain,
spl0_40,
inference(rat,[],[s51,s980,s943,s1000]) ).
cnf(s1002,plain,
spl0_4,
inference(rat,[],[s999,s1000]) ).
cnf(s1003,plain,
spl0_122,
inference(rat,[],[s127,s1001]) ).
cnf(s1004,plain,
~ spl0_75,
inference(rat,[],[s83,s1001]) ).
cnf(s1006,plain,
~ spl0_23,
inference(rat,[],[s951,s1002]) ).
cnf(s1010,plain,
spl0_31,
inference(rat,[],[s52,s943,s1000,s1006]) ).
cnf(s1014,plain,
~ spl0_5,
inference(rat,[],[s983,s1010]) ).
cnf(s1015,plain,
spl0_51,
inference(rat,[],[s60,s943,s1014]) ).
cnf(s1017,plain,
~ spl0_26,
inference(rat,[],[s996,s1000,s1014]) ).
cnf(s1027,plain,
spl0_20,
inference(rat,[],[s995,s30,s42,s980,s943,s1017]) ).
cnf(s1028,plain,
~ spl0_10,
inference(rat,[],[s944,s1015]) ).
cnf(s1030,plain,
~ spl0_15,
inference(rat,[],[s517,s1003,s1004,s1027]) ).
cnf(s1034,plain,
$false,
inference(rat,[],[s993,s1000,s1014,s1028,s1030]) ).
fof(f4188,plain,
$false,
inference(avatar_sat_refutation,[],[s1034]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN485-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n013.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 16:14:51 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.29 % (1304788)Will run a generic schedule for satisfiability detection.
% 0.17/0.29 % (1304798)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3323721033:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.29 % (1304794)% WARNING: option uhcvi not known.
% 0.17/0.29 % (1304793)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3526496756_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.29 % (1304795)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2490789654:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.29 % (1304796)dis+10_1_sil=32000:sp=arity:random_seed=2413236650:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.29 % (1304794)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=554885911:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.29 % (1304797)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2131177501:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.29 % (1304799)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4056849695:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.29 % Detected minimum model sizes of [1]
% 0.17/0.29 % Detected maximum model sizes of [30]
% 0.17/0.29 % TRYING [1]
% 0.17/0.29 % TRYING [2]
% 0.17/0.29 % TRYING [3]
% 0.17/0.29 % TRYING [4]
% 0.17/0.29 % (1304798) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1304788-1304798"...
% 0.17/0.29 % (1304798)...printing done.
% 0.17/0.29 % (1304798)Refutation found. Thanks to Tanya!
% 0.17/0.29 % SZS status Unsatisfiable for theBenchmark
% 0.17/0.29 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/0.29 % (1304798)------------------------------
% 0.17/0.29 % (1304798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.29 % (1304798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.29 % (1304798)CaDiCaL version: 2.1.3
% 0.17/0.29 % (1304798)Termination reason: Refutation
% 0.17/0.29 % (1304798)Time elapsed: 0.032 s
% 0.17/0.29 % (1304798)Peak memory usage: 14 MB
% 0.17/0.29 % (1304798)Instructions burned: 89 (million)
% 0.17/0.29 % (1304788)Success in time 0.066 s
% 0.17/0.29 % Vampire exiting
%------------------------------------------------------------------------------