%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN508-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:00:02 PM UTC 2026
% Result : Unsatisfiable 2.38s 1.04s
% Output : Refutation 2.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 238
% Syntax : Number of formulae : 913 ( 15 unt; 124 def)
% Number of atoms : 3037 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 3791 (1667 ~;2000 |; 0 &)
% ( 124 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 155 ( 154 usr; 151 prp; 0-1 aty)
% Number of functors : 24 ( 24 usr; 24 con; 0-0 aty)
% Number of variables : 147 ( 0 sgn 147 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,negated_conjecture,
( ~ hskp30
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
fof(f9,negated_conjecture,
( ~ hskp23
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause9) ).
fof(f15,negated_conjecture,
( ~ hskp17
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause15) ).
fof(f33,negated_conjecture,
( hskp23
| hskp30
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f35,negated_conjecture,
( hskp25
| hskp18
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( hskp6
| hskp1
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( hskp6
| hskp8
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f38,negated_conjecture,
( hskp16
| hskp24
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause38) ).
fof(f40,negated_conjecture,
( hskp7
| hskp14
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause40) ).
fof(f43,negated_conjecture,
( hskp22
| hskp8
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( hskp18
| hskp11
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp31
| c0_1(a723) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp31
| c1_1(a723) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp31
| c3_1(a723) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f48,negated_conjecture,
( ~ hskp30
| c0_1(a714) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause48) ).
fof(f49,negated_conjecture,
( ~ hskp30
| c2_1(a714) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f50,negated_conjecture,
( ~ hskp30
| c3_1(a714) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause50) ).
fof(f51,negated_conjecture,
( ~ hskp29
| c1_1(a709) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp29
| c2_1(a709) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f53,negated_conjecture,
( ~ hskp29
| c3_1(a709) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause53) ).
fof(f54,negated_conjecture,
( ~ hskp28
| c0_1(a705) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause54) ).
fof(f55,negated_conjecture,
( ~ hskp28
| c1_1(a705) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f56,negated_conjecture,
( ~ hskp28
| c2_1(a705) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause56) ).
fof(f61,negated_conjecture,
( ~ hskp25
| c2_1(a764) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp24
| c0_1(a762) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f66,negated_conjecture,
( ~ hskp22
| c1_1(a756) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( ~ hskp22
| c2_1(a756) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp21
| c2_1(a748) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp21
| c3_1(a748) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f71,negated_conjecture,
( ~ hskp19
| c1_1(a741) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp19
| c3_1(a741) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp18
| c2_1(a739) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp18
| c3_1(a739) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp16
| c0_1(a732) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f76,negated_conjecture,
( ~ hskp16
| c3_1(a732) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause76) ).
fof(f78,negated_conjecture,
( ~ hskp14
| c1_1(a730) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause78) ).
fof(f79,negated_conjecture,
( ~ hskp14
| c3_1(a730) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp13
| c3_1(a727) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp12
| c2_1(a725) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ hskp11
| c3_1(a721) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f86,negated_conjecture,
( ~ hskp8
| c1_1(a718) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause86) ).
fof(f87,negated_conjecture,
( ~ hskp7
| c0_1(a717) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f88,negated_conjecture,
( ~ hskp6
| c0_1(a716) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause88) ).
fof(f89,negated_conjecture,
( ~ hskp6
| c2_1(a716) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ hskp4
| c0_1(a711) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f92,negated_conjecture,
( ~ hskp1
| c0_1(a707) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f96,negated_conjecture,
( ~ c1_1(a764)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause96) ).
fof(f97,negated_conjecture,
( ~ c2_1(a762)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f99,negated_conjecture,
( ~ c3_1(a756)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c0_1(a748)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f103,negated_conjecture,
( ~ c0_1(a741)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c1_1(a739)
| ~ hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c0_1(a734)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c1_1(a734)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c3_1(a734)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c1_1(a732)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f111,negated_conjecture,
( ~ c2_1(a730)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f112,negated_conjecture,
( ~ c0_1(a727)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause112) ).
fof(f113,negated_conjecture,
( ~ c2_1(a727)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ c0_1(a725)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c1_1(a725)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c0_1(a721)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c1_1(a721)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f121,negated_conjecture,
( ~ c0_1(a718)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c2_1(a718)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c2_1(a717)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c3_1(a717)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ c3_1(a716)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c0_1(a713)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c2_1(a713)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
( ~ c3_1(a713)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f131,negated_conjecture,
( ~ c1_1(a710)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause131) ).
fof(f132,negated_conjecture,
( ~ c2_1(a710)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
( ~ c3_1(a710)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f136,negated_conjecture,
( ~ c1_1(a707)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
( ~ c2_1(a707)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f138,negated_conjecture,
( ~ c0_1(a706)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause138) ).
fof(f139,negated_conjecture,
( ~ c1_1(a706)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause139) ).
fof(f146,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| hskp1
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp30
| hskp18 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp6
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp16
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f155,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp14
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause155) ).
fof(f160,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp1
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp18
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp21
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp29
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f165,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp30
| hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause165) ).
fof(f166,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp28
| hskp31 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f168,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp16
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause168) ).
fof(f169,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp19
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f171,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp31
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp8
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f175,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause175) ).
fof(f181,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c1_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f185,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp29 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause185) ).
fof(f188,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause188) ).
fof(f189,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c0_1(X1)
| c2_1(X1)
| hskp31 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause189) ).
fof(f192,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X1)
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause192) ).
fof(f194,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause194) ).
fof(f199,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c3_1(X0)
| c0_1(X2)
| c2_1(X2)
| c3_1(X2)
| c0_1(X1)
| c1_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause199) ).
fof(f200,negated_conjecture,
! [X2,X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X2)
| c1_1(X0)
| c2_1(X0)
| c1_1(X1)
| c2_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause200) ).
fof(f201,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause201) ).
fof(f202,negated_conjecture,
! [X2,X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X2)
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause202) ).
fof(f203,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| c0_1(X2)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause203) ).
fof(f204,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause204) ).
fof(f205,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c2_1(X2)
| c1_1(X1)
| c0_1(X2)
| c1_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause205) ).
fof(f206,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X2)
| c1_1(X1)
| c0_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause206) ).
fof(f207,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X2)
| ~ c1_1(X2)
| c3_1(X0)
| c3_1(X1)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause207) ).
fof(f208,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c2_1(X2)
| ~ c3_1(X2)
| c3_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause208) ).
fof(f210,definition,
( spl0_1
<=> ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f211,plain,
( ! [X2] :
( ~ c2_1(X2)
| c0_1(X2)
| ~ c3_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f213,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f214,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f216,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f219,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f220,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f219]) ).
fof(f221,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f208,f219,f216,f213,f210]) ).
fof(f223,definition,
( spl0_5
<=> ! [X2] :
( ~ c0_1(X2)
| c2_1(X2)
| ~ c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f224,plain,
( ! [X2] :
( c2_1(X2)
| ~ c0_1(X2)
| ~ c1_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f223]) ).
fof(f226,definition,
( spl0_6
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f227,plain,
( ! [X1] :
( c3_1(X1)
| ~ c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f226]) ).
fof(f228,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f207,f213,f216,f226,f223]) ).
fof(f230,definition,
( spl0_7
<=> ! [X2] :
( ~ c1_1(X2)
| c2_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f231,plain,
( ! [X2] :
( c2_1(X2)
| ~ c1_1(X2)
| c0_1(X2) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f230]) ).
fof(f233,definition,
( spl0_8
<=> ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f234,plain,
( ! [X1] :
( ~ c2_1(X1)
| c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f233]) ).
fof(f235,plain,
( spl0_7
| spl0_8
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f206,f219,f216,f233,f230]) ).
fof(f237,definition,
( spl0_9
<=> ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f238,plain,
( ! [X2] :
( ~ c2_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f237]) ).
fof(f240,definition,
( spl0_10
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f241,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f240]) ).
fof(f242,plain,
( spl0_9
| spl0_8
| ~ spl0_3
| spl0_10 ),
inference(avatar_split_clause,[],[f205,f240,f216,f233,f237]) ).
fof(f244,definition,
( spl0_11
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f245,plain,
( ! [X2] :
( c3_1(X2)
| c0_1(X2)
| c1_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f244]) ).
fof(f247,definition,
( spl0_12
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f248,plain,
( ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f249,plain,
( spl0_11
| spl0_1
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f204,f247,f216,f210,f244]) ).
fof(f251,definition,
( spl0_13
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f252,plain,
( ! [X2] :
( c2_1(X2)
| c3_1(X2)
| c0_1(X2) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f254,definition,
( spl0_14
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f255,plain,
( ! [X1] :
( c2_1(X1)
| ~ c0_1(X1)
| c1_1(X1) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f257,definition,
( spl0_15
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f258,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f257]) ).
fof(f259,plain,
( spl0_13
| spl0_14
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f203,f257,f216,f254,f251]) ).
fof(f261,definition,
( spl0_16
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f262,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f261]) ).
fof(f263,plain,
( spl0_9
| spl0_16
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f202,f210,f216,f261,f237]) ).
fof(f264,plain,
( spl0_11
| spl0_9
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f201,f257,f216,f237,f244]) ).
fof(f266,definition,
( spl0_17
<=> ! [X0] :
( ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f267,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c1_1(X0) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f266]) ).
fof(f268,plain,
( spl0_7
| spl0_14
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f200,f266,f216,f254,f230]) ).
fof(f269,plain,
( spl0_13
| spl0_16
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f199,f213,f216,f261,f251]) ).
fof(f275,definition,
( spl0_19
<=> ! [X2] :
( c1_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f276,plain,
( ! [X2] :
( c2_1(X2)
| c3_1(X2)
| c1_1(X2) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f286,definition,
( spl0_22
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f289,definition,
( spl0_23
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f290,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f293,definition,
( spl0_24
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f296,definition,
( spl0_25
<=> ! [X1] :
( ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f297,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1)
| ~ c1_1(X1) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f296]) ).
fof(f298,plain,
( spl0_24
| spl0_25
| ~ spl0_3
| spl0_15 ),
inference(avatar_split_clause,[],[f194,f257,f216,f296,f293]) ).
fof(f300,definition,
( spl0_26
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f304,definition,
( spl0_27
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f306,plain,
( spl0_27
| spl0_8
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f192,f223,f216,f233,f304]) ).
fof(f308,definition,
( spl0_28
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f313,definition,
( spl0_29
<=> hskp31 ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f315,plain,
( spl0_29
| spl0_7
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f189,f247,f216,f230,f313]) ).
fof(f317,definition,
( spl0_30
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f320,definition,
( spl0_31
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f321,plain,
( ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f320]) ).
fof(f322,plain,
( spl0_30
| spl0_31
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f188,f226,f216,f320,f317]) ).
fof(f324,definition,
( spl0_32
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f332,definition,
( spl0_34
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f335,definition,
( spl0_35
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f336,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( spl0_34
| spl0_35
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f185,f233,f216,f335,f332]) ).
fof(f342,definition,
( spl0_37
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f343,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f345,plain,
( spl0_24
| spl0_7
| ~ spl0_3
| spl0_6 ),
inference(avatar_split_clause,[],[f183,f226,f216,f230,f293]) ).
fof(f347,definition,
( spl0_38
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f349,plain,
( spl0_38
| spl0_7
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f182,f233,f216,f230,f347]) ).
fof(f351,definition,
( spl0_39
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f354,definition,
( spl0_40
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f355,plain,
( ! [X0] :
( c2_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f356,plain,
( spl0_39
| spl0_16
| ~ spl0_3
| spl0_40 ),
inference(avatar_split_clause,[],[f181,f354,f216,f261,f351]) ).
fof(f358,definition,
( spl0_41
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f365,definition,
( spl0_43
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f368,definition,
( spl0_44
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f369,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f368]) ).
fof(f372,definition,
( spl0_45
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f373,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f372]) ).
fof(f378,definition,
( spl0_46
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f380,plain,
( spl0_46
| spl0_11
| ~ spl0_3
| spl0_37 ),
inference(avatar_split_clause,[],[f175,f342,f216,f244,f378]) ).
fof(f382,definition,
( spl0_47
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f384,plain,
( spl0_47
| spl0_19
| ~ spl0_3
| spl0_44 ),
inference(avatar_split_clause,[],[f174,f368,f216,f275,f382]) ).
fof(f385,plain,
( spl0_34
| spl0_11
| spl0_13
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f173,f216,f251,f244,f332]) ).
fof(f387,definition,
( spl0_48
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f390,definition,
( spl0_49
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f392,plain,
( spl0_48
| spl0_49
| ~ spl0_3
| spl0_45 ),
inference(avatar_split_clause,[],[f172,f372,f216,f390,f387]) ).
fof(f394,definition,
( spl0_50
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f396,plain,
( spl0_50
| spl0_29
| ~ spl0_3
| spl0_2 ),
inference(avatar_split_clause,[],[f171,f213,f216,f313,f394]) ).
fof(f401,definition,
( spl0_52
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f404,plain,
( spl0_49
| spl0_26
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f169,f223,f216,f300,f390]) ).
fof(f405,plain,
( spl0_47
| spl0_30
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f168,f223,f216,f317,f382]) ).
fof(f407,plain,
( spl0_29
| spl0_24
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f166,f223,f216,f293,f313]) ).
fof(f409,definition,
( spl0_53
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f411,plain,
( spl0_53
| spl0_41
| ~ spl0_3
| spl0_8 ),
inference(avatar_split_clause,[],[f165,f233,f216,f358,f409]) ).
fof(f413,definition,
( spl0_54
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f416,plain,
( spl0_54
| spl0_34
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f163,f289,f216,f332,f413]) ).
fof(f418,definition,
( spl0_55
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f420,plain,
( spl0_47
| spl0_55
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f162,f210,f216,f418,f382]) ).
fof(f422,definition,
( spl0_56
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f424,plain,
( spl0_47
| spl0_56
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f161,f296,f216,f422,f382]) ).
fof(f425,plain,
( spl0_49
| spl0_50
| ~ spl0_3
| spl0_25 ),
inference(avatar_split_clause,[],[f160,f296,f216,f394,f390]) ).
fof(f436,definition,
( spl0_59
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f439,plain,
( spl0_47
| spl0_27
| ~ spl0_3
| spl0_17 ),
inference(avatar_split_clause,[],[f155,f266,f216,f304,f382]) ).
fof(f440,plain,
( spl0_53
| spl0_30
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f154,f254,f216,f317,f409]) ).
fof(f441,plain,
( spl0_43
| spl0_39
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f153,f254,f216,f351,f365]) ).
fof(f442,plain,
( spl0_56
| spl0_41
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f152,f254,f216,f358,f422]) ).
fof(f455,definition,
( spl0_62
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f457,plain,
( spl0_62
| spl0_50
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f146,f230,f216,f394,f455]) ).
fof(f478,definition,
( spl0_67
<=> c1_1(a706) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f479,plain,
( ~ c1_1(a706)
| spl0_67 ),
inference(avatar_component_clause,[],[f478]) ).
fof(f480,plain,
( ~ spl0_48
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f139,f478,f387]) ).
fof(f482,definition,
( spl0_68
<=> c0_1(a706) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f483,plain,
( ~ c0_1(a706)
| spl0_68 ),
inference(avatar_component_clause,[],[f482]) ).
fof(f484,plain,
( ~ spl0_48
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f138,f482,f387]) ).
fof(f487,definition,
( spl0_69
<=> c2_1(a707) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f488,plain,
( ~ c2_1(a707)
| spl0_69 ),
inference(avatar_component_clause,[],[f487]) ).
fof(f489,plain,
( ~ spl0_50
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f137,f487,f394]) ).
fof(f491,definition,
( spl0_70
<=> c1_1(a707) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f492,plain,
( ~ c1_1(a707)
| spl0_70 ),
inference(avatar_component_clause,[],[f491]) ).
fof(f493,plain,
( ~ spl0_50
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f136,f491,f394]) ).
fof(f505,definition,
( spl0_73
<=> c3_1(a710) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f507,plain,
( ~ spl0_46
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f133,f505,f378]) ).
fof(f509,definition,
( spl0_74
<=> c2_1(a710) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f510,plain,
( ~ c2_1(a710)
| spl0_74 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f511,plain,
( ~ spl0_46
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f132,f509,f378]) ).
fof(f513,definition,
( spl0_75
<=> c1_1(a710) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f514,plain,
( ~ c1_1(a710)
| spl0_75 ),
inference(avatar_component_clause,[],[f513]) ).
fof(f515,plain,
( ~ spl0_46
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f131,f513,f378]) ).
fof(f527,definition,
( spl0_78
<=> c3_1(a713) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f528,plain,
( ~ c3_1(a713)
| spl0_78 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f529,plain,
( ~ spl0_54
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f128,f527,f413]) ).
fof(f531,definition,
( spl0_79
<=> c2_1(a713) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f532,plain,
( ~ c2_1(a713)
| spl0_79 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f533,plain,
( ~ spl0_54
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f127,f531,f413]) ).
fof(f535,definition,
( spl0_80
<=> c0_1(a713) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f536,plain,
( ~ c0_1(a713)
| spl0_80 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f537,plain,
( ~ spl0_54
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f126,f535,f413]) ).
fof(f540,definition,
( spl0_81
<=> c3_1(a716) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f541,plain,
( ~ c3_1(a716)
| spl0_81 ),
inference(avatar_component_clause,[],[f540]) ).
fof(f542,plain,
( ~ spl0_39
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f125,f540,f351]) ).
fof(f545,definition,
( spl0_82
<=> c3_1(a717) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f546,plain,
( ~ c3_1(a717)
| spl0_82 ),
inference(avatar_component_clause,[],[f545]) ).
fof(f547,plain,
( ~ spl0_52
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f124,f545,f401]) ).
fof(f549,definition,
( spl0_83
<=> c2_1(a717) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f550,plain,
( ~ c2_1(a717)
| spl0_83 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f551,plain,
( ~ spl0_52
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f123,f549,f401]) ).
fof(f554,definition,
( spl0_84
<=> c2_1(a718) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f555,plain,
( ~ c2_1(a718)
| spl0_84 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f556,plain,
( ~ spl0_49
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f122,f554,f390]) ).
fof(f558,definition,
( spl0_85
<=> c0_1(a718) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f559,plain,
( ~ c0_1(a718)
| spl0_85 ),
inference(avatar_component_clause,[],[f558]) ).
fof(f560,plain,
( ~ spl0_49
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f121,f558,f390]) ).
fof(f577,definition,
( spl0_89
<=> c1_1(a721) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f578,plain,
( ~ c1_1(a721)
| spl0_89 ),
inference(avatar_component_clause,[],[f577]) ).
fof(f579,plain,
( ~ spl0_38
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f117,f577,f347]) ).
fof(f581,definition,
( spl0_90
<=> c0_1(a721) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f582,plain,
( ~ c0_1(a721)
| spl0_90 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( ~ spl0_38
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f116,f581,f347]) ).
fof(f586,definition,
( spl0_91
<=> c1_1(a725) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f587,plain,
( ~ c1_1(a725)
| spl0_91 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f588,plain,
( ~ spl0_62
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f115,f586,f455]) ).
fof(f590,definition,
( spl0_92
<=> c0_1(a725) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f591,plain,
( ~ c0_1(a725)
| spl0_92 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f592,plain,
( ~ spl0_62
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f114,f590,f455]) ).
fof(f595,definition,
( spl0_93
<=> c2_1(a727) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f596,plain,
( ~ c2_1(a727)
| spl0_93 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f597,plain,
( ~ spl0_43
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f113,f595,f365]) ).
fof(f599,definition,
( spl0_94
<=> c0_1(a727) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f600,plain,
( ~ c0_1(a727)
| spl0_94 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f601,plain,
( ~ spl0_43
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f112,f599,f365]) ).
fof(f604,definition,
( spl0_95
<=> c2_1(a730) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f605,plain,
( ~ c2_1(a730)
| spl0_95 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f606,plain,
( ~ spl0_27
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f111,f604,f304]) ).
fof(f618,definition,
( spl0_98
<=> c1_1(a732) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f619,plain,
( ~ c1_1(a732)
| spl0_98 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f620,plain,
( ~ spl0_30
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f108,f618,f317]) ).
fof(f623,definition,
( spl0_99
<=> c3_1(a734) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f624,plain,
( ~ c3_1(a734)
| spl0_99 ),
inference(avatar_component_clause,[],[f623]) ).
fof(f625,plain,
( ~ spl0_47
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f107,f623,f382]) ).
fof(f627,definition,
( spl0_100
<=> c1_1(a734) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f628,plain,
( ~ c1_1(a734)
| spl0_100 ),
inference(avatar_component_clause,[],[f627]) ).
fof(f629,plain,
( ~ spl0_47
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f106,f627,f382]) ).
fof(f631,definition,
( spl0_101
<=> c0_1(a734) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f632,plain,
( ~ c0_1(a734)
| spl0_101 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f633,plain,
( ~ spl0_47
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f105,f631,f382]) ).
fof(f636,definition,
( spl0_102
<=> c1_1(a739) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f637,plain,
( ~ c1_1(a739)
| spl0_102 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f638,plain,
( ~ spl0_56
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f104,f636,f422]) ).
fof(f641,definition,
( spl0_103
<=> c0_1(a741) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f642,plain,
( ~ c0_1(a741)
| spl0_103 ),
inference(avatar_component_clause,[],[f641]) ).
fof(f643,plain,
( ~ spl0_26
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f103,f641,f300]) ).
fof(f655,definition,
( spl0_106
<=> c0_1(a748) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f656,plain,
( ~ c0_1(a748)
| spl0_106 ),
inference(avatar_component_clause,[],[f655]) ).
fof(f657,plain,
( ~ spl0_55
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f100,f655,f418]) ).
fof(f660,definition,
( spl0_107
<=> c3_1(a756) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f661,plain,
( ~ c3_1(a756)
| spl0_107 ),
inference(avatar_component_clause,[],[f660]) ).
fof(f662,plain,
( ~ spl0_53
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f99,f660,f409]) ).
fof(f670,definition,
( spl0_109
<=> c2_1(a762) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f671,plain,
( ~ c2_1(a762)
| spl0_109 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f672,plain,
( ~ spl0_59
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f97,f670,f436]) ).
fof(f675,definition,
( spl0_110
<=> c1_1(a764) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f676,plain,
( ~ c1_1(a764)
| spl0_110 ),
inference(avatar_component_clause,[],[f675]) ).
fof(f677,plain,
( ~ spl0_22
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f96,f675,f286]) ).
fof(f693,definition,
( spl0_114
<=> c0_1(a707) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f694,plain,
( c0_1(a707)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f695,plain,
( spl0_114
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f92,f394,f693]) ).
fof(f701,definition,
( spl0_116
<=> c0_1(a711) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f702,plain,
( c0_1(a711)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f701]) ).
fof(f703,plain,
( spl0_116
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f90,f308,f701]) ).
fof(f705,definition,
( spl0_117
<=> c2_1(a716) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f706,plain,
( c2_1(a716)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f707,plain,
( spl0_117
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f89,f351,f705]) ).
fof(f709,definition,
( spl0_118
<=> c0_1(a716) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f710,plain,
( c0_1(a716)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f711,plain,
( spl0_118
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f88,f351,f709]) ).
fof(f713,definition,
( spl0_119
<=> c0_1(a717) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f714,plain,
( c0_1(a717)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f715,plain,
( spl0_119
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f87,f401,f713]) ).
fof(f717,definition,
( spl0_120
<=> c1_1(a718) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f718,plain,
( c1_1(a718)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f717]) ).
fof(f719,plain,
( spl0_120
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f86,f390,f717]) ).
fof(f733,definition,
( spl0_124
<=> c3_1(a721) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f734,plain,
( c3_1(a721)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f735,plain,
( spl0_124
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f82,f347,f733]) ).
fof(f737,definition,
( spl0_125
<=> c2_1(a725) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f738,plain,
( c2_1(a725)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f739,plain,
( spl0_125
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f81,f455,f737]) ).
fof(f741,definition,
( spl0_126
<=> c3_1(a727) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f743,plain,
( spl0_126
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f80,f365,f741]) ).
fof(f745,definition,
( spl0_127
<=> c3_1(a730) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f746,plain,
( c3_1(a730)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f747,plain,
( spl0_127
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f79,f304,f745]) ).
fof(f749,definition,
( spl0_128
<=> c1_1(a730) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f750,plain,
( c1_1(a730)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f751,plain,
( spl0_128
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f78,f304,f749]) ).
fof(f757,definition,
( spl0_130
<=> c3_1(a732) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f758,plain,
( c3_1(a732)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f757]) ).
fof(f759,plain,
( spl0_130
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f76,f317,f757]) ).
fof(f761,definition,
( spl0_131
<=> c0_1(a732) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f762,plain,
( c0_1(a732)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f763,plain,
( spl0_131
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f75,f317,f761]) ).
fof(f765,definition,
( spl0_132
<=> c3_1(a739) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f766,plain,
( c3_1(a739)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f765]) ).
fof(f767,plain,
( spl0_132
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f74,f422,f765]) ).
fof(f769,definition,
( spl0_133
<=> c2_1(a739) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f770,plain,
( c2_1(a739)
| ~ spl0_133 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f771,plain,
( spl0_133
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f73,f422,f769]) ).
fof(f773,definition,
( spl0_134
<=> c3_1(a741) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f774,plain,
( c3_1(a741)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f775,plain,
( spl0_134
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f72,f300,f773]) ).
fof(f777,definition,
( spl0_135
<=> c1_1(a741) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f778,plain,
( c1_1(a741)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f777]) ).
fof(f779,plain,
( spl0_135
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f71,f300,f777]) ).
fof(f785,definition,
( spl0_137
<=> c3_1(a748) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f786,plain,
( c3_1(a748)
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f787,plain,
( spl0_137
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f69,f418,f785]) ).
fof(f789,definition,
( spl0_138
<=> c2_1(a748) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f790,plain,
( c2_1(a748)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f789]) ).
fof(f791,plain,
( spl0_138
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f68,f418,f789]) ).
fof(f793,definition,
( spl0_139
<=> c2_1(a756) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f794,plain,
( c2_1(a756)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f795,plain,
( spl0_139
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f67,f409,f793]) ).
fof(f797,definition,
( spl0_140
<=> c1_1(a756) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f798,plain,
( c1_1(a756)
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f797]) ).
fof(f799,plain,
( spl0_140
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f66,f409,f797]) ).
fof(f813,definition,
( spl0_144
<=> c0_1(a762) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f814,plain,
( c0_1(a762)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f813]) ).
fof(f815,plain,
( spl0_144
| ~ spl0_59 ),
inference(avatar_split_clause,[],[f62,f436,f813]) ).
fof(f817,definition,
( spl0_145
<=> c2_1(a764) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f818,plain,
( c2_1(a764)
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f817]) ).
fof(f819,plain,
( spl0_145
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f61,f286,f817]) ).
fof(f837,definition,
( spl0_150
<=> c2_1(a705) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f838,plain,
( c2_1(a705)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f837]) ).
fof(f840,plain,
( spl0_150
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f56,f293,f837]) ).
fof(f842,definition,
( spl0_151
<=> c1_1(a705) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f843,plain,
( c1_1(a705)
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f844,plain,
( spl0_151
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f55,f293,f842]) ).
fof(f846,definition,
( spl0_152
<=> c0_1(a705) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f847,plain,
( c0_1(a705)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f846]) ).
fof(f848,plain,
( spl0_152
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f54,f293,f846]) ).
fof(f850,definition,
( spl0_153
<=> c3_1(a709) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f851,plain,
( c3_1(a709)
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f850]) ).
fof(f853,plain,
( spl0_153
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f53,f332,f850]) ).
fof(f855,definition,
( spl0_154
<=> c2_1(a709) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f856,plain,
( c2_1(a709)
| ~ spl0_154 ),
inference(avatar_component_clause,[],[f855]) ).
fof(f857,plain,
( spl0_154
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f52,f332,f855]) ).
fof(f859,definition,
( spl0_155
<=> c1_1(a709) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f860,plain,
( c1_1(a709)
| ~ spl0_155 ),
inference(avatar_component_clause,[],[f859]) ).
fof(f861,plain,
( spl0_155
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f51,f332,f859]) ).
fof(f863,definition,
( spl0_156
<=> c3_1(a714) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f864,plain,
( c3_1(a714)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f866,plain,
( spl0_156
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f50,f358,f863]) ).
fof(f868,definition,
( spl0_157
<=> c2_1(a714) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f869,plain,
( c2_1(a714)
| ~ spl0_157 ),
inference(avatar_component_clause,[],[f868]) ).
fof(f870,plain,
( spl0_157
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f49,f358,f868]) ).
fof(f872,definition,
( spl0_158
<=> c0_1(a714) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f873,plain,
( c0_1(a714)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f874,plain,
( spl0_158
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f48,f358,f872]) ).
fof(f876,definition,
( spl0_159
<=> c3_1(a723) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f877,plain,
( c3_1(a723)
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f876]) ).
fof(f879,plain,
( spl0_159
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f47,f313,f876]) ).
fof(f881,definition,
( spl0_160
<=> c1_1(a723) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f882,plain,
( c1_1(a723)
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f881]) ).
fof(f883,plain,
( spl0_160
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f46,f313,f881]) ).
fof(f885,definition,
( spl0_161
<=> c0_1(a723) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f886,plain,
( c0_1(a723)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f885]) ).
fof(f887,plain,
( spl0_161
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f45,f313,f885]) ).
fof(f888,plain,
( spl0_54
| spl0_38
| spl0_56 ),
inference(avatar_split_clause,[],[f44,f422,f347,f413]) ).
fof(f889,plain,
( spl0_38
| spl0_49
| spl0_53 ),
inference(avatar_split_clause,[],[f43,f409,f390,f347]) ).
fof(f892,plain,
( spl0_49
| spl0_27
| spl0_52 ),
inference(avatar_split_clause,[],[f40,f401,f304,f390]) ).
fof(f894,plain,
( spl0_28
| spl0_59
| spl0_30 ),
inference(avatar_split_clause,[],[f38,f317,f436,f308]) ).
fof(f895,plain,
( spl0_56
| spl0_49
| spl0_39 ),
inference(avatar_split_clause,[],[f37,f351,f390,f422]) ).
fof(f896,plain,
( spl0_55
| spl0_50
| spl0_39 ),
inference(avatar_split_clause,[],[f36,f351,f394,f418]) ).
fof(f897,plain,
( spl0_62
| spl0_56
| spl0_22 ),
inference(avatar_split_clause,[],[f35,f286,f422,f455]) ).
fof(f899,plain,
( spl0_47
| spl0_41
| spl0_32 ),
inference(avatar_split_clause,[],[f33,f324,f358,f382]) ).
fof(f918,plain,
( spl0_3
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f15,f382,f216]) ).
fof(f924,plain,
( spl0_3
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f9,f324,f216]) ).
fof(f931,plain,
( spl0_3
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f2,f358,f216]) ).
fof(f947,plain,
( c1_1(a725)
| ~ c3_1(a725)
| ~ spl0_8
| ~ spl0_125 ),
inference(resolution,[],[f234,f738]) ).
fof(f949,plain,
( ~ c3_1(a725)
| ~ spl0_8
| spl0_91
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f947,f587]) ).
fof(f951,plain,
( c0_1(a725)
| c1_1(a725)
| ~ spl0_8
| ~ spl0_11
| spl0_91
| ~ spl0_125 ),
inference(resolution,[],[f245,f949]) ).
fof(f953,plain,
( c0_1(a734)
| c1_1(a734)
| ~ spl0_11
| spl0_99 ),
inference(resolution,[],[f245,f624]) ).
fof(f956,plain,
( c1_1(a734)
| ~ spl0_11
| spl0_99
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f953,f632]) ).
fof(f957,plain,
( c1_1(a725)
| ~ spl0_8
| ~ spl0_11
| spl0_91
| spl0_92
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f951,f591]) ).
fof(f958,plain,
( $false
| ~ spl0_11
| spl0_99
| spl0_100
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f956,f628]) ).
fof(f959,plain,
( ~ spl0_11
| spl0_99
| spl0_100
| spl0_101 ),
inference(avatar_contradiction_clause,[],[f958]) ).
fof(f960,plain,
( $false
| ~ spl0_8
| ~ spl0_11
| spl0_91
| spl0_92
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f957,f587]) ).
fof(f961,plain,
( ~ spl0_8
| ~ spl0_11
| spl0_91
| spl0_92
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f960]) ).
fof(f962,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_6
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f248,f227]) ).
fof(f970,plain,
( c3_1(a713)
| c0_1(a713)
| ~ spl0_13
| spl0_79 ),
inference(resolution,[],[f252,f532]) ).
fof(f974,plain,
( c0_1(a713)
| ~ spl0_13
| spl0_78
| spl0_79 ),
inference(forward_subsumption_resolution,[],[f970,f528]) ).
fof(f976,plain,
( $false
| ~ spl0_13
| spl0_78
| spl0_79
| spl0_80 ),
inference(forward_subsumption_resolution,[],[f974,f536]) ).
fof(f977,plain,
( ~ spl0_13
| spl0_78
| spl0_79
| spl0_80 ),
inference(avatar_contradiction_clause,[],[f976]) ).
fof(f978,plain,
( ! [X1] :
( c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_5
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f255,f224]) ).
fof(f996,plain,
( c1_1(a739)
| ~ c3_1(a739)
| ~ spl0_8
| ~ spl0_133 ),
inference(resolution,[],[f770,f234]) ).
fof(f1002,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_2
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f336,f214]) ).
fof(f1006,plain,
( ~ c0_1(a756)
| ~ spl0_6
| ~ spl0_12
| ~ spl0_140 ),
inference(resolution,[],[f798,f962]) ).
fof(f1018,plain,
( c3_1(a756)
| ~ spl0_2
| ~ spl0_35
| ~ spl0_139 ),
inference(resolution,[],[f1002,f794]) ).
fof(f1023,plain,
( $false
| ~ spl0_2
| ~ spl0_35
| spl0_107
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f1018,f661]) ).
fof(f1024,plain,
( ~ spl0_2
| ~ spl0_35
| spl0_107
| ~ spl0_139 ),
inference(avatar_contradiction_clause,[],[f1023]) ).
fof(f1025,plain,
( ! [X1] :
( c3_1(X1)
| c0_1(X1) )
| ~ spl0_13
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f336,f252]) ).
fof(f1026,plain,
( c0_1(a756)
| ~ spl0_13
| ~ spl0_35
| spl0_107 ),
inference(resolution,[],[f1025,f661]) ).
fof(f1028,plain,
( c0_1(a734)
| ~ spl0_13
| ~ spl0_35
| spl0_99 ),
inference(resolution,[],[f1025,f624]) ).
fof(f1030,plain,
( $false
| ~ spl0_13
| ~ spl0_35
| spl0_99
| spl0_101 ),
inference(forward_subsumption_resolution,[],[f1028,f632]) ).
fof(f1031,plain,
( ~ spl0_13
| ~ spl0_35
| spl0_99
| spl0_101 ),
inference(avatar_contradiction_clause,[],[f1030]) ).
fof(f1032,plain,
( $false
| ~ spl0_6
| ~ spl0_12
| ~ spl0_13
| ~ spl0_35
| spl0_107
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f1026,f1006]) ).
fof(f1033,plain,
( ~ spl0_6
| ~ spl0_12
| ~ spl0_13
| ~ spl0_35
| spl0_107
| ~ spl0_140 ),
inference(avatar_contradiction_clause,[],[f1032]) ).
fof(f1035,plain,
( ! [X2] :
( c2_1(X2)
| ~ c1_1(X2) )
| ~ spl0_5
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f231,f224]) ).
fof(f1037,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f220,f224]) ).
fof(f1041,plain,
( ~ c0_1(a717)
| ~ c1_1(a717)
| ~ spl0_5
| spl0_83 ),
inference(resolution,[],[f550,f224]) ).
fof(f1043,definition,
( spl0_162
<=> c1_1(a717) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1044,plain,
( ~ c1_1(a717)
| spl0_162 ),
inference(avatar_component_clause,[],[f1043]) ).
fof(f1052,plain,
( ! [X1] :
( c3_1(X1)
| ~ c1_1(X1) )
| ~ spl0_6
| ~ spl0_13
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f227,f1025]) ).
fof(f1055,plain,
( ! [X1] :
( ~ c1_1(X1)
| c0_1(X1) )
| ~ spl0_13
| ~ spl0_25
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f297,f1025]) ).
fof(f1071,plain,
( ~ c1_1(a756)
| ~ spl0_6
| ~ spl0_13
| ~ spl0_35
| spl0_107 ),
inference(resolution,[],[f1052,f661]) ).
fof(f1076,plain,
( $false
| ~ spl0_6
| ~ spl0_13
| ~ spl0_35
| spl0_107
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f1071,f798]) ).
fof(f1077,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_35
| spl0_107
| ~ spl0_140 ),
inference(avatar_contradiction_clause,[],[f1076]) ).
fof(f1117,plain,
( ~ c1_1(a717)
| ~ spl0_5
| spl0_83
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f1041,f714]) ).
fof(f1126,plain,
( ~ spl0_162
| ~ spl0_5
| spl0_83
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1117,f713,f549,f223,f1043]) ).
fof(f1149,plain,
( ~ c1_1(a730)
| ~ spl0_5
| ~ spl0_7
| spl0_95 ),
inference(resolution,[],[f1035,f605]) ).
fof(f1157,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| spl0_95
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f1149,f750]) ).
fof(f1158,plain,
( ~ spl0_5
| ~ spl0_7
| spl0_95
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f1157]) ).
fof(f1220,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f262,f1055]) ).
fof(f1221,plain,
( ! [X1] : c0_1(X1)
| ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f1220,f1025]) ).
fof(f1224,plain,
( $false
| ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35
| spl0_101 ),
inference(resolution,[],[f1221,f632]) ).
fof(f1227,plain,
( ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35
| spl0_101 ),
inference(avatar_contradiction_clause,[],[f1224]) ).
fof(f1230,plain,
( ! [X1] :
( c2_1(X1)
| c3_1(X1) )
| ~ spl0_13
| ~ spl0_31
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f321,f1025]) ).
fof(f1245,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_5
| ~ spl0_7
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f267,f1035]) ).
fof(f1294,plain,
( $false
| ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35
| spl0_106 ),
inference(resolution,[],[f1221,f656]) ).
fof(f1295,plain,
( ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35
| spl0_106 ),
inference(avatar_contradiction_clause,[],[f1294]) ).
fof(f1307,plain,
( ~ c0_1(a762)
| ~ spl0_5
| ~ spl0_14
| spl0_109 ),
inference(resolution,[],[f978,f671]) ).
fof(f1310,plain,
( ~ c0_1(a717)
| ~ spl0_5
| ~ spl0_14
| spl0_83 ),
inference(resolution,[],[f978,f550]) ).
fof(f1314,plain,
( $false
| ~ spl0_5
| ~ spl0_14
| spl0_109
| ~ spl0_144 ),
inference(forward_subsumption_resolution,[],[f1307,f814]) ).
fof(f1315,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_109
| ~ spl0_144 ),
inference(avatar_contradiction_clause,[],[f1314]) ).
fof(f1338,plain,
( c3_1(a717)
| ~ spl0_13
| ~ spl0_31
| ~ spl0_35
| spl0_83 ),
inference(resolution,[],[f1230,f550]) ).
fof(f1339,plain,
( $false
| ~ spl0_13
| ~ spl0_31
| ~ spl0_35
| spl0_82
| spl0_83 ),
inference(forward_subsumption_resolution,[],[f1338,f546]) ).
fof(f1340,plain,
( ~ spl0_13
| ~ spl0_31
| ~ spl0_35
| spl0_82
| spl0_83 ),
inference(avatar_contradiction_clause,[],[f1339]) ).
fof(f1431,plain,
( c1_1(a714)
| ~ c0_1(a714)
| ~ spl0_23
| ~ spl0_156 ),
inference(resolution,[],[f290,f864]) ).
fof(f1437,plain,
( c1_1(a732)
| ~ c0_1(a732)
| ~ spl0_23
| ~ spl0_130 ),
inference(resolution,[],[f290,f758]) ).
fof(f1446,plain,
( ~ c0_1(a732)
| ~ spl0_23
| spl0_98
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1437,f619]) ).
fof(f1450,definition,
( spl0_164
<=> c1_1(a748) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1451,plain,
( c1_1(a748)
| ~ spl0_164 ),
inference(avatar_component_clause,[],[f1450]) ).
fof(f1455,plain,
( $false
| ~ spl0_23
| spl0_98
| ~ spl0_130
| ~ spl0_131 ),
inference(forward_subsumption_resolution,[],[f1446,f762]) ).
fof(f1456,plain,
( ~ spl0_23
| spl0_98
| ~ spl0_130
| ~ spl0_131 ),
inference(avatar_contradiction_clause,[],[f1455]) ).
fof(f1478,plain,
( ! [X1] :
( c1_1(X1)
| c0_1(X1) )
| ~ spl0_13
| ~ spl0_16
| ~ spl0_35 ),
inference(forward_subsumption_resolution,[],[f262,f1025]) ).
fof(f1487,plain,
( ~ c0_1(a709)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_155 ),
inference(resolution,[],[f1037,f860]) ).
fof(f1498,plain,
( ~ c0_1(a714)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_23
| ~ spl0_156 ),
inference(forward_subsumption_resolution,[],[f1431,f1037]) ).
fof(f1507,plain,
( $false
| ~ spl0_4
| ~ spl0_5
| ~ spl0_23
| ~ spl0_156
| ~ spl0_158 ),
inference(forward_subsumption_resolution,[],[f1498,f873]) ).
fof(f1508,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_23
| ~ spl0_156
| ~ spl0_158 ),
inference(avatar_contradiction_clause,[],[f1507]) ).
fof(f1537,plain,
( c0_1(a721)
| ~ spl0_13
| ~ spl0_16
| ~ spl0_35
| spl0_89 ),
inference(resolution,[],[f1478,f578]) ).
fof(f1546,plain,
( $false
| ~ spl0_13
| ~ spl0_16
| ~ spl0_35
| spl0_89
| spl0_90 ),
inference(forward_subsumption_resolution,[],[f1537,f582]) ).
fof(f1547,plain,
( ~ spl0_13
| ~ spl0_16
| ~ spl0_35
| spl0_89
| spl0_90 ),
inference(avatar_contradiction_clause,[],[f1546]) ).
fof(f1552,plain,
( ~ c0_1(a709)
| ~ c1_1(a709)
| ~ spl0_4
| ~ spl0_154 ),
inference(resolution,[],[f220,f856]) ).
fof(f1553,plain,
( ~ c0_1(a705)
| ~ c1_1(a705)
| ~ spl0_4
| ~ spl0_150 ),
inference(resolution,[],[f220,f838]) ).
fof(f1561,plain,
( ~ c1_1(a705)
| ~ spl0_4
| ~ spl0_150
| ~ spl0_152 ),
inference(forward_subsumption_resolution,[],[f1553,f847]) ).
fof(f1562,plain,
( ~ c0_1(a709)
| ~ spl0_4
| ~ spl0_154
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f1552,f860]) ).
fof(f1564,plain,
( $false
| ~ spl0_4
| ~ spl0_150
| ~ spl0_151
| ~ spl0_152 ),
inference(forward_subsumption_resolution,[],[f1561,f843]) ).
fof(f1565,plain,
( ~ spl0_4
| ~ spl0_150
| ~ spl0_151
| ~ spl0_152 ),
inference(avatar_contradiction_clause,[],[f1564]) ).
fof(f1569,plain,
( ~ c1_1(a727)
| c0_1(a727)
| ~ spl0_7
| spl0_93 ),
inference(resolution,[],[f231,f596]) ).
fof(f1570,plain,
( ~ c1_1(a718)
| c0_1(a718)
| ~ spl0_7
| spl0_84 ),
inference(resolution,[],[f231,f555]) ).
fof(f1575,plain,
( c0_1(a718)
| ~ spl0_7
| spl0_84
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f1570,f718]) ).
fof(f1576,plain,
( ~ c1_1(a727)
| ~ spl0_7
| spl0_93
| spl0_94 ),
inference(forward_subsumption_resolution,[],[f1569,f600]) ).
fof(f1578,plain,
( $false
| ~ spl0_7
| spl0_84
| spl0_85
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f1575,f559]) ).
fof(f1579,plain,
( ~ spl0_7
| spl0_84
| spl0_85
| ~ spl0_120 ),
inference(avatar_contradiction_clause,[],[f1578]) ).
fof(f1581,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c3_1(X0)
| c0_1(X0) )
| ~ spl0_9
| ~ spl0_13 ),
inference(resolution,[],[f238,f252]) ).
fof(f1585,plain,
( c1_1(a748)
| c0_1(a748)
| ~ spl0_9
| ~ spl0_138 ),
inference(resolution,[],[f238,f790]) ).
fof(f1586,plain,
( c1_1(a739)
| c0_1(a739)
| ~ spl0_9
| ~ spl0_133 ),
inference(resolution,[],[f238,f770]) ).
fof(f1587,plain,
( c1_1(a725)
| c0_1(a725)
| ~ spl0_9
| ~ spl0_125 ),
inference(resolution,[],[f238,f738]) ).
fof(f1589,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_9
| ~ spl0_13 ),
inference(duplicate_literal_removal,[],[f1581]) ).
fof(f1593,plain,
( c0_1(a725)
| ~ spl0_9
| spl0_91
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f1587,f587]) ).
fof(f1594,plain,
( c0_1(a739)
| ~ spl0_9
| spl0_102
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f1586,f637]) ).
fof(f1595,plain,
( c1_1(a748)
| ~ spl0_9
| spl0_106
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f1585,f656]) ).
fof(f1596,plain,
( $false
| ~ spl0_9
| spl0_91
| spl0_92
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f1593,f591]) ).
fof(f1597,plain,
( ~ spl0_9
| spl0_91
| spl0_92
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f1596]) ).
fof(f1598,plain,
( spl0_164
| ~ spl0_9
| spl0_106
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1595,f789,f655,f237,f1450]) ).
fof(f1617,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_9
| ~ spl0_17 ),
inference(resolution,[],[f267,f238]) ).
fof(f1620,plain,
( ~ c3_1(a727)
| c1_1(a727)
| ~ spl0_17
| spl0_93 ),
inference(resolution,[],[f267,f596]) ).
fof(f1622,plain,
( ~ c3_1(a707)
| c1_1(a707)
| ~ spl0_17
| spl0_69 ),
inference(resolution,[],[f267,f488]) ).
fof(f1624,plain,
( ! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_9
| ~ spl0_17 ),
inference(duplicate_literal_removal,[],[f1617]) ).
fof(f1626,plain,
( ~ c3_1(a707)
| ~ spl0_17
| spl0_69
| spl0_70 ),
inference(forward_subsumption_resolution,[],[f1622,f492]) ).
fof(f1706,plain,
( spl0_11
| ~ spl0_9
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1589,f251,f237,f244]) ).
fof(f1711,definition,
( spl0_167
<=> c0_1(a710) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1715,plain,
( ! [X0] :
( c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_1
| ~ spl0_7 ),
inference(resolution,[],[f211,f231]) ).
fof(f1718,plain,
( c0_1(a709)
| ~ c3_1(a709)
| ~ spl0_1
| ~ spl0_154 ),
inference(resolution,[],[f211,f856]) ).
fof(f1724,plain,
( ! [X0] :
( c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) )
| ~ spl0_1
| ~ spl0_7 ),
inference(duplicate_literal_removal,[],[f1715]) ).
fof(f1727,plain,
( c0_1(a709)
| ~ spl0_1
| ~ spl0_153
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f1718,f851]) ).
fof(f1728,plain,
( spl0_25
| ~ spl0_1
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f1724,f230,f210,f296]) ).
fof(f1804,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f258,f214]) ).
fof(f1809,plain,
( ~ c0_1(a705)
| ~ spl0_2
| ~ spl0_15
| ~ spl0_150 ),
inference(resolution,[],[f1804,f838]) ).
fof(f1817,plain,
( $false
| ~ spl0_2
| ~ spl0_15
| ~ spl0_150
| ~ spl0_152 ),
inference(forward_subsumption_resolution,[],[f1809,f847]) ).
fof(f1818,plain,
( ~ spl0_2
| ~ spl0_15
| ~ spl0_150
| ~ spl0_152 ),
inference(avatar_contradiction_clause,[],[f1817]) ).
fof(f1827,plain,
( c3_1(a717)
| c1_1(a717)
| ~ spl0_19
| spl0_83 ),
inference(resolution,[],[f276,f550]) ).
fof(f1828,plain,
( c3_1(a707)
| c1_1(a707)
| ~ spl0_19
| spl0_69 ),
inference(resolution,[],[f276,f488]) ).
fof(f1889,plain,
( ~ c1_1(a730)
| ~ c3_1(a730)
| ~ spl0_40
| spl0_95 ),
inference(resolution,[],[f355,f605]) ).
fof(f1895,plain,
( ~ c3_1(a730)
| ~ spl0_40
| spl0_95
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f1889,f750]) ).
fof(f1897,plain,
( $false
| ~ spl0_40
| spl0_95
| ~ spl0_127
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f1895,f746]) ).
fof(f1898,plain,
( ~ spl0_40
| spl0_95
| ~ spl0_127
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f1897]) ).
fof(f1899,plain,
( c3_1(a716)
| ~ c0_1(a716)
| ~ spl0_2
| ~ spl0_117 ),
inference(resolution,[],[f706,f214]) ).
fof(f1901,plain,
( ~ c0_1(a716)
| ~ spl0_2
| spl0_81
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f1899,f541]) ).
fof(f1902,plain,
( $false
| ~ spl0_2
| spl0_81
| ~ spl0_117
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f1901,f710]) ).
fof(f1903,plain,
( ~ spl0_2
| spl0_81
| ~ spl0_117
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f1902]) ).
fof(f1904,plain,
( ! [X1] :
( c1_1(X1)
| c0_1(X1) )
| ~ spl0_11
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f262,f245]) ).
fof(f1913,plain,
( c0_1(a727)
| ~ spl0_7
| ~ spl0_11
| ~ spl0_16
| spl0_93
| spl0_94 ),
inference(resolution,[],[f1904,f1576]) ).
fof(f1914,plain,
( c0_1(a721)
| ~ spl0_11
| ~ spl0_16
| spl0_89 ),
inference(resolution,[],[f1904,f578]) ).
fof(f1921,plain,
( c0_1(a706)
| ~ spl0_11
| ~ spl0_16
| spl0_67 ),
inference(resolution,[],[f1904,f479]) ).
fof(f1922,plain,
( $false
| ~ spl0_11
| ~ spl0_16
| spl0_67
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f1921,f483]) ).
fof(f1923,plain,
( ~ spl0_11
| ~ spl0_16
| spl0_67
| spl0_68 ),
inference(avatar_contradiction_clause,[],[f1922]) ).
fof(f1925,plain,
( $false
| ~ spl0_11
| ~ spl0_16
| spl0_89
| spl0_90 ),
inference(forward_subsumption_resolution,[],[f1914,f582]) ).
fof(f1926,plain,
( ~ spl0_11
| ~ spl0_16
| spl0_89
| spl0_90 ),
inference(avatar_contradiction_clause,[],[f1925]) ).
fof(f1927,plain,
( $false
| ~ spl0_7
| ~ spl0_11
| ~ spl0_16
| spl0_93
| spl0_94 ),
inference(forward_subsumption_resolution,[],[f1913,f600]) ).
fof(f1928,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_16
| spl0_93
| spl0_94 ),
inference(avatar_contradiction_clause,[],[f1927]) ).
fof(f1941,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_7
| ~ spl0_10 ),
inference(resolution,[],[f241,f231]) ).
fof(f1943,plain,
( ~ c3_1(a709)
| ~ c1_1(a709)
| ~ spl0_10
| ~ spl0_154 ),
inference(resolution,[],[f241,f856]) ).
fof(f1945,plain,
( ~ c3_1(a748)
| ~ c1_1(a748)
| ~ spl0_10
| ~ spl0_138 ),
inference(resolution,[],[f241,f790]) ).
fof(f1949,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_7
| ~ spl0_10 ),
inference(duplicate_literal_removal,[],[f1941]) ).
fof(f1950,plain,
( ~ c1_1(a748)
| ~ spl0_10
| ~ spl0_137
| ~ spl0_138 ),
inference(forward_subsumption_resolution,[],[f1945,f786]) ).
fof(f1951,plain,
( ~ c1_1(a709)
| ~ spl0_10
| ~ spl0_153
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f1943,f851]) ).
fof(f1952,plain,
( spl0_25
| ~ spl0_7
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f1949,f240,f230,f296]) ).
fof(f1953,plain,
( $false
| ~ spl0_10
| ~ spl0_137
| ~ spl0_138
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f1950,f1451]) ).
fof(f1954,plain,
( ~ spl0_10
| ~ spl0_137
| ~ spl0_138
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f1953]) ).
fof(f1955,plain,
( $false
| ~ spl0_10
| ~ spl0_153
| ~ spl0_154
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f1951,f860]) ).
fof(f1956,plain,
( ~ spl0_10
| ~ spl0_153
| ~ spl0_154
| ~ spl0_155 ),
inference(avatar_contradiction_clause,[],[f1955]) ).
fof(f2022,plain,
( ~ c3_1(a709)
| ~ c0_1(a709)
| ~ spl0_15
| ~ spl0_154 ),
inference(resolution,[],[f258,f856]) ).
fof(f2025,plain,
( ~ c3_1(a739)
| ~ c0_1(a739)
| ~ spl0_15
| ~ spl0_133 ),
inference(resolution,[],[f258,f770]) ).
fof(f2028,plain,
( ~ c0_1(a739)
| ~ spl0_15
| ~ spl0_132
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2025,f766]) ).
fof(f2029,plain,
( $false
| ~ spl0_9
| ~ spl0_15
| spl0_102
| ~ spl0_132
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f2028,f1594]) ).
fof(f2030,plain,
( ~ spl0_9
| ~ spl0_15
| spl0_102
| ~ spl0_132
| ~ spl0_133 ),
inference(avatar_contradiction_clause,[],[f2029]) ).
fof(f2038,plain,
( ~ c0_1(a723)
| ~ spl0_6
| ~ spl0_12
| ~ spl0_160 ),
inference(resolution,[],[f962,f882]) ).
fof(f2052,plain,
( $false
| ~ spl0_6
| ~ spl0_12
| ~ spl0_160
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f2038,f886]) ).
fof(f2053,plain,
( ~ spl0_6
| ~ spl0_12
| ~ spl0_160
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f2052]) ).
fof(f2054,plain,
( ! [X2] :
( ~ c2_1(X2)
| ~ c3_1(X2) )
| ~ spl0_1
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f211,f258]) ).
fof(f2057,plain,
( ~ c3_1(a709)
| ~ spl0_1
| ~ spl0_4
| ~ spl0_154
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f1718,f1562]) ).
fof(f2058,plain,
( $false
| ~ spl0_1
| ~ spl0_4
| ~ spl0_153
| ~ spl0_154
| ~ spl0_155 ),
inference(forward_subsumption_resolution,[],[f2057,f851]) ).
fof(f2059,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_153
| ~ spl0_154
| ~ spl0_155 ),
inference(avatar_contradiction_clause,[],[f2058]) ).
fof(f2093,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_15
| ~ spl0_37 ),
inference(forward_subsumption_resolution,[],[f343,f2054]) ).
fof(f2097,plain,
( ~ c0_1(a723)
| ~ spl0_1
| ~ spl0_15
| ~ spl0_37
| ~ spl0_159 ),
inference(resolution,[],[f2093,f877]) ).
fof(f2112,plain,
( $false
| ~ spl0_1
| ~ spl0_15
| ~ spl0_37
| ~ spl0_159
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f2097,f886]) ).
fof(f2113,plain,
( ~ spl0_1
| ~ spl0_15
| ~ spl0_37
| ~ spl0_159
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f2112]) ).
fof(f2159,definition,
( spl0_174
<=> c0_1(a709) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f2193,plain,
( spl0_174
| ~ spl0_1
| ~ spl0_153
| ~ spl0_154 ),
inference(avatar_split_clause,[],[f1727,f855,f850,f210,f2159]) ).
fof(f2203,plain,
( c0_1(a748)
| ~ c3_1(a748)
| ~ spl0_1
| ~ spl0_138 ),
inference(resolution,[],[f211,f790]) ).
fof(f2214,plain,
( c1_1(a764)
| ~ c3_1(a764)
| ~ spl0_8
| ~ spl0_145 ),
inference(resolution,[],[f234,f818]) ).
fof(f2216,plain,
( c1_1(a748)
| ~ c3_1(a748)
| ~ spl0_8
| ~ spl0_138 ),
inference(resolution,[],[f234,f790]) ).
fof(f2220,plain,
( ~ c3_1(a764)
| ~ spl0_8
| spl0_110
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2214,f676]) ).
fof(f2236,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_8
| ~ spl0_14 ),
inference(resolution,[],[f255,f234]) ).
fof(f2244,plain,
( ~ c0_1(a707)
| c1_1(a707)
| ~ spl0_14
| spl0_69 ),
inference(resolution,[],[f255,f488]) ).
fof(f2245,plain,
( ~ c0_1(a710)
| c1_1(a710)
| ~ spl0_14
| spl0_74 ),
inference(resolution,[],[f255,f510]) ).
fof(f2247,plain,
( ! [X0] :
( ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_8
| ~ spl0_14 ),
inference(duplicate_literal_removal,[],[f2236]) ).
fof(f2249,plain,
( c1_1(a707)
| ~ spl0_14
| spl0_69
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2244,f694]) ).
fof(f2253,plain,
( spl0_23
| ~ spl0_8
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f2247,f254,f233,f289]) ).
fof(f2256,plain,
( $false
| ~ spl0_14
| spl0_69
| spl0_70
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2249,f492]) ).
fof(f2257,plain,
( ~ spl0_14
| spl0_69
| spl0_70
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f2256]) ).
fof(f2271,plain,
( ~ c1_1(a727)
| c0_1(a727)
| ~ spl0_7
| spl0_93 ),
inference(resolution,[],[f231,f596]) ).
fof(f2298,plain,
( c0_1(a709)
| ~ c1_1(a709)
| ~ spl0_25
| ~ spl0_153 ),
inference(resolution,[],[f297,f851]) ).
fof(f2299,plain,
( c0_1(a741)
| ~ c1_1(a741)
| ~ spl0_25
| ~ spl0_134 ),
inference(resolution,[],[f297,f774]) ).
fof(f2309,plain,
( ~ c1_1(a741)
| ~ spl0_25
| spl0_103
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2299,f642]) ).
fof(f2311,plain,
( $false
| ~ spl0_25
| spl0_103
| ~ spl0_134
| ~ spl0_135 ),
inference(forward_subsumption_resolution,[],[f2309,f778]) ).
fof(f2312,plain,
( ~ spl0_25
| spl0_103
| ~ spl0_134
| ~ spl0_135 ),
inference(avatar_contradiction_clause,[],[f2311]) ).
fof(f2316,definition,
( spl0_175
<=> c1_1(a727) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f2328,plain,
( spl0_175
| ~ spl0_126
| ~ spl0_17
| spl0_93 ),
inference(avatar_split_clause,[],[f1620,f595,f266,f741,f2316]) ).
fof(f2344,plain,
( spl0_94
| ~ spl0_175
| ~ spl0_7
| spl0_93 ),
inference(avatar_split_clause,[],[f2271,f595,f230,f2316,f599]) ).
fof(f2347,plain,
( c0_1(a748)
| ~ c1_1(a748)
| ~ spl0_25
| ~ spl0_137 ),
inference(resolution,[],[f786,f297]) ).
fof(f2348,plain,
( ~ c1_1(a748)
| ~ spl0_25
| spl0_106
| ~ spl0_137 ),
inference(forward_subsumption_resolution,[],[f2347,f656]) ).
fof(f2349,plain,
( $false
| ~ spl0_25
| spl0_106
| ~ spl0_137
| ~ spl0_164 ),
inference(forward_subsumption_resolution,[],[f2348,f1451]) ).
fof(f2350,plain,
( ~ spl0_25
| spl0_106
| ~ spl0_137
| ~ spl0_164 ),
inference(avatar_contradiction_clause,[],[f2349]) ).
fof(f2435,plain,
( c3_1(a764)
| c1_1(a764)
| ~ spl0_44
| ~ spl0_145 ),
inference(resolution,[],[f369,f818]) ).
fof(f2446,plain,
( c3_1(a764)
| ~ spl0_44
| spl0_110
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2435,f676]) ).
fof(f2457,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0) )
| ~ spl0_44
| ~ spl0_45 ),
inference(forward_subsumption_resolution,[],[f373,f369]) ).
fof(f2467,plain,
( c3_1(a756)
| ~ spl0_44
| ~ spl0_45
| ~ spl0_139 ),
inference(resolution,[],[f2457,f794]) ).
fof(f2481,plain,
( $false
| ~ spl0_44
| ~ spl0_45
| spl0_107
| ~ spl0_139 ),
inference(forward_subsumption_resolution,[],[f2467,f661]) ).
fof(f2482,plain,
( ~ spl0_44
| ~ spl0_45
| spl0_107
| ~ spl0_139 ),
inference(avatar_contradiction_clause,[],[f2481]) ).
fof(f2502,plain,
( ~ c3_1(a739)
| ~ spl0_8
| spl0_102
| ~ spl0_133 ),
inference(forward_subsumption_resolution,[],[f996,f637]) ).
fof(f2521,plain,
( ~ spl0_132
| ~ spl0_8
| spl0_102
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f2502,f769,f636,f233,f765]) ).
fof(f2525,plain,
( c3_1(a710)
| c0_1(a710)
| ~ spl0_13
| spl0_74 ),
inference(resolution,[],[f510,f252]) ).
fof(f2551,plain,
( ~ c3_1(a739)
| ~ spl0_1
| ~ spl0_15
| ~ spl0_133 ),
inference(resolution,[],[f2054,f770]) ).
fof(f2555,plain,
( ~ spl0_132
| ~ spl0_1
| ~ spl0_15
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f2551,f769,f257,f210,f765]) ).
fof(f2559,plain,
( ~ spl0_174
| ~ spl0_4
| ~ spl0_5
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f1487,f859,f223,f219,f2159]) ).
fof(f2563,plain,
( ~ spl0_174
| ~ spl0_4
| ~ spl0_154
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f1562,f859,f855,f219,f2159]) ).
fof(f2577,plain,
( ~ c0_1(a709)
| ~ spl0_15
| ~ spl0_153
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f2022,f851]) ).
fof(f2580,plain,
( ~ spl0_174
| ~ spl0_15
| ~ spl0_153
| ~ spl0_154 ),
inference(avatar_split_clause,[],[f2577,f855,f850,f257,f2159]) ).
fof(f2584,plain,
( ~ c0_1(a723)
| ~ spl0_4
| ~ spl0_5
| ~ spl0_160 ),
inference(resolution,[],[f1037,f882]) ).
fof(f2597,plain,
( $false
| ~ spl0_4
| ~ spl0_5
| ~ spl0_160
| ~ spl0_161 ),
inference(forward_subsumption_resolution,[],[f2584,f886]) ).
fof(f2598,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_160
| ~ spl0_161 ),
inference(avatar_contradiction_clause,[],[f2597]) ).
fof(f2606,plain,
( ! [X1] :
( ~ c3_1(X1)
| c1_1(X1) )
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_17 ),
inference(forward_subsumption_resolution,[],[f234,f1245]) ).
fof(f2613,plain,
( c1_1(a721)
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_17
| ~ spl0_124 ),
inference(resolution,[],[f2606,f734]) ).
fof(f2617,plain,
( $false
| ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_17
| spl0_89
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f2613,f578]) ).
fof(f2618,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_17
| spl0_89
| ~ spl0_124 ),
inference(avatar_contradiction_clause,[],[f2617]) ).
fof(f2644,definition,
( spl0_178
<=> c3_1(a764) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f2651,plain,
( ~ spl0_119
| ~ spl0_5
| ~ spl0_14
| spl0_83 ),
inference(avatar_split_clause,[],[f1310,f549,f254,f223,f713]) ).
fof(f2654,plain,
( ~ c0_1(a710)
| ~ spl0_14
| spl0_74
| spl0_75 ),
inference(forward_subsumption_resolution,[],[f2245,f514]) ).
fof(f2676,plain,
( ~ spl0_167
| ~ spl0_14
| spl0_74
| spl0_75 ),
inference(avatar_split_clause,[],[f2654,f513,f509,f254,f1711]) ).
fof(f2696,plain,
( ! [X0] : ~ c0_1(X0)
| ~ spl0_2
| ~ spl0_5
| ~ spl0_14
| ~ spl0_15 ),
inference(forward_subsumption_resolution,[],[f1804,f978]) ).
fof(f2701,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| ~ spl0_14
| ~ spl0_15
| ~ spl0_116 ),
inference(resolution,[],[f2696,f702]) ).
fof(f2704,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_14
| ~ spl0_15
| ~ spl0_116 ),
inference(avatar_contradiction_clause,[],[f2701]) ).
fof(f2714,plain,
( spl0_16
| ~ spl0_9
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f1624,f266,f237,f261]) ).
fof(f2728,plain,
( spl0_178
| ~ spl0_44
| spl0_110
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f2446,f817,f675,f368,f2644]) ).
fof(f2757,plain,
( ~ c3_1(a714)
| ~ c0_1(a714)
| ~ spl0_15
| ~ spl0_157 ),
inference(resolution,[],[f258,f869]) ).
fof(f2764,plain,
( ~ c0_1(a714)
| ~ spl0_15
| ~ spl0_156
| ~ spl0_157 ),
inference(forward_subsumption_resolution,[],[f2757,f864]) ).
fof(f2765,plain,
( $false
| ~ spl0_15
| ~ spl0_156
| ~ spl0_157
| ~ spl0_158 ),
inference(forward_subsumption_resolution,[],[f2764,f873]) ).
fof(f2766,plain,
( ~ spl0_15
| ~ spl0_156
| ~ spl0_157
| ~ spl0_158 ),
inference(avatar_contradiction_clause,[],[f2765]) ).
fof(f2775,plain,
( ~ spl0_137
| spl0_106
| ~ spl0_1
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f2203,f789,f210,f655,f785]) ).
fof(f2781,plain,
( ~ spl0_137
| spl0_164
| ~ spl0_8
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f2216,f789,f233,f1450,f785]) ).
fof(f2782,plain,
( ~ spl0_178
| ~ spl0_8
| spl0_110
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f2220,f817,f675,f233,f2644]) ).
fof(f2839,plain,
( ~ spl0_155
| spl0_174
| ~ spl0_25
| ~ spl0_153 ),
inference(avatar_split_clause,[],[f2298,f850,f296,f2159,f859]) ).
fof(f2859,plain,
( c3_1(a717)
| ~ spl0_19
| spl0_83
| spl0_162 ),
inference(forward_subsumption_resolution,[],[f1827,f1044]) ).
fof(f2860,plain,
( c1_1(a707)
| ~ spl0_17
| ~ spl0_19
| spl0_69
| spl0_70 ),
inference(forward_subsumption_resolution,[],[f1828,f1626]) ).
fof(f2871,plain,
( spl0_167
| spl0_73
| ~ spl0_13
| spl0_74 ),
inference(avatar_split_clause,[],[f2525,f509,f251,f505,f1711]) ).
fof(f2872,plain,
( spl0_82
| ~ spl0_19
| spl0_83
| spl0_162 ),
inference(avatar_split_clause,[],[f2859,f1043,f549,f275,f545]) ).
fof(f2873,plain,
( $false
| ~ spl0_17
| ~ spl0_19
| spl0_69
| spl0_70 ),
inference(forward_subsumption_resolution,[],[f2860,f492]) ).
fof(f2874,plain,
( ~ spl0_17
| ~ spl0_19
| spl0_69
| spl0_70 ),
inference(avatar_contradiction_clause,[],[f2873]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f221]) ).
cnf(s2,plain,
( spl0_2
| ~ spl0_3
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f228]) ).
cnf(s3,plain,
( ~ spl0_3
| spl0_4
| spl0_7
| spl0_8 ),
inference(sat_conversion,[],[f235]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_8
| spl0_9
| spl0_10 ),
inference(sat_conversion,[],[f242]) ).
cnf(s5,plain,
( spl0_1
| ~ spl0_3
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f249]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_13
| spl0_14
| spl0_15 ),
inference(sat_conversion,[],[f259]) ).
cnf(s7,plain,
( spl0_1
| ~ spl0_3
| spl0_9
| spl0_16 ),
inference(sat_conversion,[],[f263]) ).
cnf(s8,plain,
( ~ spl0_3
| spl0_9
| spl0_11
| spl0_15 ),
inference(sat_conversion,[],[f264]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_7
| spl0_14
| spl0_17 ),
inference(sat_conversion,[],[f268]) ).
cnf(s10,plain,
( spl0_2
| ~ spl0_3
| spl0_13
| spl0_16 ),
inference(sat_conversion,[],[f269]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_15
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f298]) ).
cnf(s17,plain,
( ~ spl0_3
| spl0_5
| spl0_8
| spl0_27 ),
inference(sat_conversion,[],[f306]) ).
cnf(s20,plain,
( ~ spl0_3
| spl0_7
| spl0_12
| spl0_29 ),
inference(sat_conversion,[],[f315]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_6
| spl0_30
| spl0_31 ),
inference(sat_conversion,[],[f322]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_8
| spl0_34
| spl0_35 ),
inference(sat_conversion,[],[f337]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_6
| spl0_7
| spl0_24 ),
inference(sat_conversion,[],[f345]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_7
| spl0_8
| spl0_38 ),
inference(sat_conversion,[],[f349]) ).
cnf(s28,plain,
( ~ spl0_3
| spl0_16
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f356]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_11
| spl0_37
| spl0_46 ),
inference(sat_conversion,[],[f380]) ).
cnf(s35,plain,
( ~ spl0_3
| spl0_19
| spl0_44
| spl0_47 ),
inference(sat_conversion,[],[f384]) ).
cnf(s36,plain,
( ~ spl0_3
| spl0_11
| spl0_13
| spl0_34 ),
inference(sat_conversion,[],[f385]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_45
| spl0_48
| spl0_49 ),
inference(sat_conversion,[],[f392]) ).
cnf(s38,plain,
( spl0_2
| ~ spl0_3
| spl0_29
| spl0_50 ),
inference(sat_conversion,[],[f396]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_5
| spl0_26
| spl0_49 ),
inference(sat_conversion,[],[f404]) ).
cnf(s41,plain,
( ~ spl0_3
| spl0_5
| spl0_30
| spl0_47 ),
inference(sat_conversion,[],[f405]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_5
| spl0_24
| spl0_29 ),
inference(sat_conversion,[],[f407]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_8
| spl0_41
| spl0_53 ),
inference(sat_conversion,[],[f411]) ).
cnf(s46,plain,
( ~ spl0_3
| spl0_23
| spl0_34
| spl0_54 ),
inference(sat_conversion,[],[f416]) ).
cnf(s47,plain,
( spl0_1
| ~ spl0_3
| spl0_47
| spl0_55 ),
inference(sat_conversion,[],[f420]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_25
| spl0_47
| spl0_56 ),
inference(sat_conversion,[],[f424]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_25
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f425]) ).
cnf(s54,plain,
( ~ spl0_3
| spl0_17
| spl0_27
| spl0_47 ),
inference(sat_conversion,[],[f439]) ).
cnf(s55,plain,
( ~ spl0_3
| spl0_14
| spl0_30
| spl0_53 ),
inference(sat_conversion,[],[f440]) ).
cnf(s56,plain,
( ~ spl0_3
| spl0_14
| spl0_39
| spl0_43 ),
inference(sat_conversion,[],[f441]) ).
cnf(s57,plain,
( ~ spl0_3
| spl0_14
| spl0_41
| spl0_56 ),
inference(sat_conversion,[],[f442]) ).
cnf(s63,plain,
( ~ spl0_3
| spl0_7
| spl0_50
| spl0_62 ),
inference(sat_conversion,[],[f457]) ).
cnf(s70,plain,
( ~ spl0_48
| ~ spl0_67 ),
inference(sat_conversion,[],[f480]) ).
cnf(s71,plain,
( ~ spl0_48
| ~ spl0_68 ),
inference(sat_conversion,[],[f484]) ).
cnf(s72,plain,
( ~ spl0_50
| ~ spl0_69 ),
inference(sat_conversion,[],[f489]) ).
cnf(s73,plain,
( ~ spl0_50
| ~ spl0_70 ),
inference(sat_conversion,[],[f493]) ).
cnf(s76,plain,
( ~ spl0_46
| ~ spl0_73 ),
inference(sat_conversion,[],[f507]) ).
cnf(s77,plain,
( ~ spl0_46
| ~ spl0_74 ),
inference(sat_conversion,[],[f511]) ).
cnf(s78,plain,
( ~ spl0_46
| ~ spl0_75 ),
inference(sat_conversion,[],[f515]) ).
cnf(s81,plain,
( ~ spl0_54
| ~ spl0_78 ),
inference(sat_conversion,[],[f529]) ).
cnf(s82,plain,
( ~ spl0_54
| ~ spl0_79 ),
inference(sat_conversion,[],[f533]) ).
cnf(s83,plain,
( ~ spl0_54
| ~ spl0_80 ),
inference(sat_conversion,[],[f537]) ).
cnf(s84,plain,
( ~ spl0_39
| ~ spl0_81 ),
inference(sat_conversion,[],[f542]) ).
cnf(s85,plain,
( ~ spl0_52
| ~ spl0_82 ),
inference(sat_conversion,[],[f547]) ).
cnf(s86,plain,
( ~ spl0_52
| ~ spl0_83 ),
inference(sat_conversion,[],[f551]) ).
cnf(s87,plain,
( ~ spl0_49
| ~ spl0_84 ),
inference(sat_conversion,[],[f556]) ).
cnf(s88,plain,
( ~ spl0_49
| ~ spl0_85 ),
inference(sat_conversion,[],[f560]) ).
cnf(s92,plain,
( ~ spl0_38
| ~ spl0_89 ),
inference(sat_conversion,[],[f579]) ).
cnf(s93,plain,
( ~ spl0_38
| ~ spl0_90 ),
inference(sat_conversion,[],[f583]) ).
cnf(s94,plain,
( ~ spl0_62
| ~ spl0_91 ),
inference(sat_conversion,[],[f588]) ).
cnf(s95,plain,
( ~ spl0_62
| ~ spl0_92 ),
inference(sat_conversion,[],[f592]) ).
cnf(s96,plain,
( ~ spl0_43
| ~ spl0_93 ),
inference(sat_conversion,[],[f597]) ).
cnf(s97,plain,
( ~ spl0_43
| ~ spl0_94 ),
inference(sat_conversion,[],[f601]) ).
cnf(s98,plain,
( ~ spl0_27
| ~ spl0_95 ),
inference(sat_conversion,[],[f606]) ).
cnf(s101,plain,
( ~ spl0_30
| ~ spl0_98 ),
inference(sat_conversion,[],[f620]) ).
cnf(s102,plain,
( ~ spl0_47
| ~ spl0_99 ),
inference(sat_conversion,[],[f625]) ).
cnf(s103,plain,
( ~ spl0_47
| ~ spl0_100 ),
inference(sat_conversion,[],[f629]) ).
cnf(s104,plain,
( ~ spl0_47
| ~ spl0_101 ),
inference(sat_conversion,[],[f633]) ).
cnf(s105,plain,
( ~ spl0_56
| ~ spl0_102 ),
inference(sat_conversion,[],[f638]) ).
cnf(s106,plain,
( ~ spl0_26
| ~ spl0_103 ),
inference(sat_conversion,[],[f643]) ).
cnf(s109,plain,
( ~ spl0_55
| ~ spl0_106 ),
inference(sat_conversion,[],[f657]) ).
cnf(s110,plain,
( ~ spl0_53
| ~ spl0_107 ),
inference(sat_conversion,[],[f662]) ).
cnf(s112,plain,
( ~ spl0_59
| ~ spl0_109 ),
inference(sat_conversion,[],[f672]) ).
cnf(s113,plain,
( ~ spl0_22
| ~ spl0_110 ),
inference(sat_conversion,[],[f677]) ).
cnf(s117,plain,
( ~ spl0_50
| spl0_114 ),
inference(sat_conversion,[],[f695]) ).
cnf(s119,plain,
( ~ spl0_28
| spl0_116 ),
inference(sat_conversion,[],[f703]) ).
cnf(s120,plain,
( ~ spl0_39
| spl0_117 ),
inference(sat_conversion,[],[f707]) ).
cnf(s121,plain,
( ~ spl0_39
| spl0_118 ),
inference(sat_conversion,[],[f711]) ).
cnf(s122,plain,
( ~ spl0_52
| spl0_119 ),
inference(sat_conversion,[],[f715]) ).
cnf(s123,plain,
( ~ spl0_49
| spl0_120 ),
inference(sat_conversion,[],[f719]) ).
cnf(s127,plain,
( ~ spl0_38
| spl0_124 ),
inference(sat_conversion,[],[f735]) ).
cnf(s128,plain,
( ~ spl0_62
| spl0_125 ),
inference(sat_conversion,[],[f739]) ).
cnf(s129,plain,
( ~ spl0_43
| spl0_126 ),
inference(sat_conversion,[],[f743]) ).
cnf(s130,plain,
( ~ spl0_27
| spl0_127 ),
inference(sat_conversion,[],[f747]) ).
cnf(s131,plain,
( ~ spl0_27
| spl0_128 ),
inference(sat_conversion,[],[f751]) ).
cnf(s133,plain,
( ~ spl0_30
| spl0_130 ),
inference(sat_conversion,[],[f759]) ).
cnf(s134,plain,
( ~ spl0_30
| spl0_131 ),
inference(sat_conversion,[],[f763]) ).
cnf(s135,plain,
( ~ spl0_56
| spl0_132 ),
inference(sat_conversion,[],[f767]) ).
cnf(s136,plain,
( ~ spl0_56
| spl0_133 ),
inference(sat_conversion,[],[f771]) ).
cnf(s137,plain,
( ~ spl0_26
| spl0_134 ),
inference(sat_conversion,[],[f775]) ).
cnf(s138,plain,
( ~ spl0_26
| spl0_135 ),
inference(sat_conversion,[],[f779]) ).
cnf(s140,plain,
( ~ spl0_55
| spl0_137 ),
inference(sat_conversion,[],[f787]) ).
cnf(s141,plain,
( ~ spl0_55
| spl0_138 ),
inference(sat_conversion,[],[f791]) ).
cnf(s142,plain,
( ~ spl0_53
| spl0_139 ),
inference(sat_conversion,[],[f795]) ).
cnf(s143,plain,
( ~ spl0_53
| spl0_140 ),
inference(sat_conversion,[],[f799]) ).
cnf(s147,plain,
( ~ spl0_59
| spl0_144 ),
inference(sat_conversion,[],[f815]) ).
cnf(s148,plain,
( ~ spl0_22
| spl0_145 ),
inference(sat_conversion,[],[f819]) ).
cnf(s153,plain,
( ~ spl0_24
| spl0_150 ),
inference(sat_conversion,[],[f840]) ).
cnf(s154,plain,
( ~ spl0_24
| spl0_151 ),
inference(sat_conversion,[],[f844]) ).
cnf(s155,plain,
( ~ spl0_24
| spl0_152 ),
inference(sat_conversion,[],[f848]) ).
cnf(s156,plain,
( ~ spl0_34
| spl0_153 ),
inference(sat_conversion,[],[f853]) ).
cnf(s157,plain,
( ~ spl0_34
| spl0_154 ),
inference(sat_conversion,[],[f857]) ).
cnf(s158,plain,
( ~ spl0_34
| spl0_155 ),
inference(sat_conversion,[],[f861]) ).
cnf(s159,plain,
( ~ spl0_41
| spl0_156 ),
inference(sat_conversion,[],[f866]) ).
cnf(s160,plain,
( ~ spl0_41
| spl0_157 ),
inference(sat_conversion,[],[f870]) ).
cnf(s161,plain,
( ~ spl0_41
| spl0_158 ),
inference(sat_conversion,[],[f874]) ).
cnf(s162,plain,
( ~ spl0_29
| spl0_159 ),
inference(sat_conversion,[],[f879]) ).
cnf(s163,plain,
( ~ spl0_29
| spl0_160 ),
inference(sat_conversion,[],[f883]) ).
cnf(s164,plain,
( ~ spl0_29
| spl0_161 ),
inference(sat_conversion,[],[f887]) ).
cnf(s165,plain,
( spl0_38
| spl0_54
| spl0_56 ),
inference(sat_conversion,[],[f888]) ).
cnf(s166,plain,
( spl0_38
| spl0_49
| spl0_53 ),
inference(sat_conversion,[],[f889]) ).
cnf(s169,plain,
( spl0_27
| spl0_49
| spl0_52 ),
inference(sat_conversion,[],[f892]) ).
cnf(s171,plain,
( spl0_28
| spl0_30
| spl0_59 ),
inference(sat_conversion,[],[f894]) ).
cnf(s172,plain,
( spl0_39
| spl0_49
| spl0_56 ),
inference(sat_conversion,[],[f895]) ).
cnf(s173,plain,
( spl0_39
| spl0_50
| spl0_55 ),
inference(sat_conversion,[],[f896]) ).
cnf(s174,plain,
( spl0_22
| spl0_56
| spl0_62 ),
inference(sat_conversion,[],[f897]) ).
cnf(s176,plain,
( spl0_32
| spl0_41
| spl0_47 ),
inference(sat_conversion,[],[f899]) ).
cnf(s194,plain,
( spl0_3
| ~ spl0_47 ),
inference(sat_conversion,[],[f918]) ).
cnf(s200,plain,
( spl0_3
| ~ spl0_32 ),
inference(sat_conversion,[],[f924]) ).
cnf(s207,plain,
( spl0_3
| ~ spl0_41 ),
inference(sat_conversion,[],[f931]) ).
cnf(s210,plain,
( ~ spl0_11
| spl0_99
| spl0_100
| spl0_101 ),
inference(sat_conversion,[],[f959]) ).
cnf(s211,plain,
( ~ spl0_8
| ~ spl0_11
| spl0_91
| spl0_92
| ~ spl0_125 ),
inference(sat_conversion,[],[f961]) ).
cnf(s212,plain,
( ~ spl0_13
| spl0_78
| spl0_79
| spl0_80 ),
inference(sat_conversion,[],[f977]) ).
cnf(s218,plain,
( ~ spl0_2
| ~ spl0_35
| spl0_107
| ~ spl0_139 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s219,plain,
( ~ spl0_13
| ~ spl0_35
| spl0_99
| spl0_101 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s220,plain,
( ~ spl0_6
| ~ spl0_12
| ~ spl0_13
| ~ spl0_35
| spl0_107
| ~ spl0_140 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s227,plain,
( ~ spl0_6
| ~ spl0_13
| ~ spl0_35
| spl0_107
| ~ spl0_140 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s235,plain,
( ~ spl0_5
| spl0_83
| ~ spl0_119
| ~ spl0_162 ),
inference(sat_conversion,[],[f1126]) ).
cnf(s246,plain,
( ~ spl0_5
| ~ spl0_7
| spl0_95
| ~ spl0_128 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s267,plain,
( ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35
| spl0_101 ),
inference(sat_conversion,[],[f1227]) ).
cnf(s282,plain,
( ~ spl0_13
| ~ spl0_16
| ~ spl0_25
| ~ spl0_35
| spl0_106 ),
inference(sat_conversion,[],[f1295]) ).
cnf(s289,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_109
| ~ spl0_144 ),
inference(sat_conversion,[],[f1315]) ).
cnf(s290,plain,
( ~ spl0_13
| ~ spl0_31
| ~ spl0_35
| spl0_82
| spl0_83 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s313,plain,
( ~ spl0_23
| spl0_98
| ~ spl0_130
| ~ spl0_131 ),
inference(sat_conversion,[],[f1456]) ).
cnf(s324,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_23
| ~ spl0_156
| ~ spl0_158 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s329,plain,
( ~ spl0_13
| ~ spl0_16
| ~ spl0_35
| spl0_89
| spl0_90 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s332,plain,
( ~ spl0_4
| ~ spl0_150
| ~ spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s333,plain,
( ~ spl0_7
| spl0_84
| spl0_85
| ~ spl0_120 ),
inference(sat_conversion,[],[f1579]) ).
cnf(s335,plain,
( ~ spl0_9
| spl0_91
| spl0_92
| ~ spl0_125 ),
inference(sat_conversion,[],[f1597]) ).
cnf(s336,plain,
( ~ spl0_9
| spl0_106
| ~ spl0_138
| spl0_164 ),
inference(sat_conversion,[],[f1598]) ).
cnf(s356,plain,
( ~ spl0_9
| spl0_11
| ~ spl0_13 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s360,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_25 ),
inference(sat_conversion,[],[f1728]) ).
cnf(s380,plain,
( ~ spl0_2
| ~ spl0_15
| ~ spl0_150
| ~ spl0_152 ),
inference(sat_conversion,[],[f1818]) ).
cnf(s393,plain,
( ~ spl0_40
| spl0_95
| ~ spl0_127
| ~ spl0_128 ),
inference(sat_conversion,[],[f1898]) ).
cnf(s394,plain,
( ~ spl0_2
| spl0_81
| ~ spl0_117
| ~ spl0_118 ),
inference(sat_conversion,[],[f1903]) ).
cnf(s397,plain,
( ~ spl0_11
| ~ spl0_16
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s399,plain,
( ~ spl0_11
| ~ spl0_16
| spl0_89
| spl0_90 ),
inference(sat_conversion,[],[f1926]) ).
cnf(s400,plain,
( ~ spl0_7
| ~ spl0_11
| ~ spl0_16
| spl0_93
| spl0_94 ),
inference(sat_conversion,[],[f1928]) ).
cnf(s402,plain,
( ~ spl0_7
| ~ spl0_10
| spl0_25 ),
inference(sat_conversion,[],[f1952]) ).
cnf(s403,plain,
( ~ spl0_10
| ~ spl0_137
| ~ spl0_138
| ~ spl0_164 ),
inference(sat_conversion,[],[f1954]) ).
cnf(s404,plain,
( ~ spl0_10
| ~ spl0_153
| ~ spl0_154
| ~ spl0_155 ),
inference(sat_conversion,[],[f1956]) ).
cnf(s419,plain,
( ~ spl0_9
| ~ spl0_15
| spl0_102
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f2030]) ).
cnf(s425,plain,
( ~ spl0_6
| ~ spl0_12
| ~ spl0_160
| ~ spl0_161 ),
inference(sat_conversion,[],[f2053]) ).
cnf(s427,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_153
| ~ spl0_154
| ~ spl0_155 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s435,plain,
( ~ spl0_1
| ~ spl0_15
| ~ spl0_37
| ~ spl0_159
| ~ spl0_161 ),
inference(sat_conversion,[],[f2113]) ).
cnf(s462,plain,
( ~ spl0_1
| ~ spl0_153
| ~ spl0_154
| spl0_174 ),
inference(sat_conversion,[],[f2193]) ).
cnf(s473,plain,
( ~ spl0_8
| ~ spl0_14
| spl0_23 ),
inference(sat_conversion,[],[f2253]) ).
cnf(s475,plain,
( ~ spl0_14
| spl0_69
| spl0_70
| ~ spl0_114 ),
inference(sat_conversion,[],[f2257]) ).
cnf(s482,plain,
( ~ spl0_25
| spl0_103
| ~ spl0_134
| ~ spl0_135 ),
inference(sat_conversion,[],[f2312]) ).
cnf(s491,plain,
( ~ spl0_17
| spl0_93
| ~ spl0_126
| spl0_175 ),
inference(sat_conversion,[],[f2328]) ).
cnf(s500,plain,
( ~ spl0_7
| spl0_93
| spl0_94
| ~ spl0_175 ),
inference(sat_conversion,[],[f2344]) ).
cnf(s503,plain,
( ~ spl0_25
| spl0_106
| ~ spl0_137
| ~ spl0_164 ),
inference(sat_conversion,[],[f2350]) ).
cnf(s525,plain,
( ~ spl0_44
| ~ spl0_45
| spl0_107
| ~ spl0_139 ),
inference(sat_conversion,[],[f2482]) ).
cnf(s538,plain,
( ~ spl0_8
| spl0_102
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f2521]) ).
cnf(s541,plain,
( ~ spl0_1
| ~ spl0_15
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f2555]) ).
cnf(s544,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_155
| ~ spl0_174 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s546,plain,
( ~ spl0_4
| ~ spl0_154
| ~ spl0_155
| ~ spl0_174 ),
inference(sat_conversion,[],[f2563]) ).
cnf(s565,plain,
( ~ spl0_15
| ~ spl0_153
| ~ spl0_154
| ~ spl0_174 ),
inference(sat_conversion,[],[f2580]) ).
cnf(s570,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_160
| ~ spl0_161 ),
inference(sat_conversion,[],[f2598]) ).
cnf(s575,plain,
( ~ spl0_5
| ~ spl0_7
| ~ spl0_8
| ~ spl0_17
| spl0_89
| ~ spl0_124 ),
inference(sat_conversion,[],[f2618]) ).
cnf(s593,plain,
( ~ spl0_5
| ~ spl0_14
| spl0_83
| ~ spl0_119 ),
inference(sat_conversion,[],[f2651]) ).
cnf(s601,plain,
( ~ spl0_14
| spl0_74
| spl0_75
| ~ spl0_167 ),
inference(sat_conversion,[],[f2676]) ).
cnf(s608,plain,
( ~ spl0_2
| ~ spl0_5
| ~ spl0_14
| ~ spl0_15
| ~ spl0_116 ),
inference(sat_conversion,[],[f2704]) ).
cnf(s614,plain,
( ~ spl0_9
| spl0_16
| ~ spl0_17 ),
inference(sat_conversion,[],[f2714]) ).
cnf(s622,plain,
( ~ spl0_44
| spl0_110
| ~ spl0_145
| spl0_178 ),
inference(sat_conversion,[],[f2728]) ).
cnf(s636,plain,
( ~ spl0_15
| ~ spl0_156
| ~ spl0_157
| ~ spl0_158 ),
inference(sat_conversion,[],[f2766]) ).
cnf(s640,plain,
( ~ spl0_1
| spl0_106
| ~ spl0_137
| ~ spl0_138 ),
inference(sat_conversion,[],[f2775]) ).
cnf(s643,plain,
( ~ spl0_8
| ~ spl0_137
| ~ spl0_138
| spl0_164 ),
inference(sat_conversion,[],[f2781]) ).
cnf(s644,plain,
( ~ spl0_8
| spl0_110
| ~ spl0_145
| ~ spl0_178 ),
inference(sat_conversion,[],[f2782]) ).
cnf(s677,plain,
( ~ spl0_25
| ~ spl0_153
| ~ spl0_155
| spl0_174 ),
inference(sat_conversion,[],[f2839]) ).
cnf(s733,plain,
( ~ spl0_13
| spl0_73
| spl0_74
| spl0_167 ),
inference(sat_conversion,[],[f2871]) ).
cnf(s734,plain,
( ~ spl0_19
| spl0_82
| spl0_83
| spl0_162 ),
inference(sat_conversion,[],[f2872]) ).
cnf(s735,plain,
( ~ spl0_17
| ~ spl0_19
| spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f2874]) ).
cnf(s738,plain,
spl0_3,
inference(rat,[],[s176,s194,s200,s207]) ).
cnf(s739,plain,
( ~ spl0_34
| ~ spl0_10 ),
inference(rat,[],[s404,s156,s157,s158]) ).
cnf(s740,plain,
( spl0_9
| spl0_89
| spl0_90
| spl0_8
| spl0_1 ),
inference(rat,[],[s329,s24,s36,s739,s399,s7,s4,s738]) ).
cnf(s741,plain,
( spl0_11
| spl0_34
| ~ spl0_9 ),
inference(rat,[],[s36,s356,s738]) ).
cnf(s743,plain,
( ~ spl0_47
| ~ spl0_13
| ~ spl0_35 ),
inference(rat,[],[s219,s102,s104]) ).
cnf(s744,plain,
( ~ spl0_10
| spl0_89
| spl0_90
| spl0_8
| spl0_2
| spl0_1 ),
inference(rat,[],[s336,s403,s109,s140,s141,s47,s743,s10,s399,s741,s24,s739,s740,s738]) ).
cnf(s745,plain,
( ~ spl0_54
| ~ spl0_13 ),
inference(rat,[],[s212,s81,s82,s83]) ).
cnf(s746,plain,
( spl0_34
| ~ spl0_13
| spl0_8
| spl0_5 ),
inference(rat,[],[s313,s101,s133,s134,s41,s743,s46,s24,s745,s738]) ).
cnf(s748,plain,
( ~ spl0_47
| ~ spl0_11 ),
inference(rat,[],[s210,s102,s103,s104]) ).
cnf(s749,plain,
( ~ spl0_24
| ~ spl0_4 ),
inference(rat,[],[s332,s153,s154,s155]) ).
cnf(s750,plain,
( ~ spl0_9
| spl0_106
| ~ spl0_137
| ~ spl0_138
| spl0_47
| spl0_24 ),
inference(rat,[],[s419,s105,s135,s136,s48,s15,s503,s336,s738]) ).
cnf(s751,plain,
( ~ spl0_8
| spl0_106
| ~ spl0_137
| ~ spl0_138
| spl0_47 ),
inference(rat,[],[s538,s105,s135,s136,s48,s503,s643,s738]) ).
cnf(s752,plain,
( ~ spl0_38
| spl0_47
| spl0_2
| spl0_1 ),
inference(rat,[],[s744,s92,s93,s4,s751,s750,s109,s140,s141,s47,s749,s1,s738]) ).
cnf(s753,plain,
( ~ spl0_49
| ~ spl0_7 ),
inference(rat,[],[s333,s87,s88,s123]) ).
cnf(s754,plain,
( spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s482,s106,s137,s138,s40,s753,s402,s27,s752,s4,s751,s750,s109,s140,s141,s47,s748,s5,s425,s163,s164,s43,s2,s749,s1,s738]) ).
cnf(s755,plain,
( ~ spl0_27
| ~ spl0_7
| ~ spl0_5 ),
inference(rat,[],[s246,s98,s131]) ).
cnf(s756,plain,
( ~ spl0_11
| spl0_2
| spl0_1 ),
inference(rat,[],[s397,s70,s71,s37,s525,s35,s734,s235,s85,s86,s122,s169,s755,s110,s142,s166,s753,s27,s7,s751,s750,s109,s140,s141,s752,s47,s748,s749,s1,s754,s738]) ).
cnf(s757,plain,
( spl0_47
| spl0_8
| spl0_2
| spl0_1 ),
inference(rat,[],[s282,s36,s24,s402,s739,s4,s7,s750,s27,s109,s140,s141,s752,s47,s749,s1,s756,s738]) ).
cnf(s758,plain,
( spl0_9
| ~ spl0_7
| spl0_101
| spl0_8
| spl0_11
| spl0_1 ),
inference(rat,[],[s267,s36,s24,s402,s739,s4,s7,s738]) ).
cnf(s759,plain,
( ~ spl0_41
| ~ spl0_15 ),
inference(rat,[],[s636,s159,s160,s161]) ).
cnf(s760,plain,
( ~ spl0_7
| spl0_8
| spl0_2
| spl0_1 ),
inference(rat,[],[s419,s105,s135,s136,s57,s759,s6,s356,s758,s593,s86,s122,s169,s755,s753,s754,s756,s104,s757,s738]) ).
cnf(s761,plain,
( ~ spl0_29
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s570,s163,s164]) ).
cnf(s762,plain,
( ~ spl0_9
| spl0_14
| spl0_11
| ~ spl0_5
| ~ spl0_4 ),
inference(rat,[],[s419,s105,s135,s136,s57,s759,s15,s677,s544,s156,s158,s741,s749,s738]) ).
cnf(s763,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s227,s36,s24,s110,s143,s739,s26,s44,s4,s760,s538,s105,s135,s136,s57,s759,s8,s762,s475,s72,s73,s117,s38,s761,s756,s754,s749,s1,s738]) ).
cnf(s764,plain,
( ~ spl0_53
| ~ spl0_35
| ~ spl0_2 ),
inference(rat,[],[s218,s110,s142]) ).
cnf(s765,plain,
( spl0_38
| spl0_53
| spl0_8 ),
inference(rat,[],[s753,s166,s27,s738]) ).
cnf(s766,plain,
( spl0_9
| spl0_8
| spl0_1 ),
inference(rat,[],[s740,s92,s93,s765,s764,s24,s739,s4,s763,s738]) ).
cnf(s767,plain,
( ~ spl0_39
| ~ spl0_2 ),
inference(rat,[],[s394,s84,s120,s121]) ).
cnf(s768,plain,
( ~ spl0_11
| spl0_1 ),
inference(rat,[],[s393,s98,s130,s131,s28,s54,s400,s491,s500,s96,s97,s129,s56,s475,s72,s73,s117,s49,s753,s3,s503,s749,s336,s750,s766,s751,s109,s140,s141,s47,s748,s767,s763,s738]) ).
cnf(s770,plain,
( ~ spl0_50
| ~ spl0_14 ),
inference(rat,[],[s475,s72,s73,s117]) ).
cnf(s771,plain,
( spl0_106
| ~ spl0_137
| ~ spl0_138
| ~ spl0_25
| ~ spl0_9 ),
inference(rat,[],[s503,s336]) ).
cnf(s772,plain,
( spl0_49
| spl0_13
| ~ spl0_9
| spl0_39 ),
inference(rat,[],[s109,s771,s140,s141,s173,s49,s770,s6,s419,s105,s135,s136,s172,s738]) ).
cnf(s773,plain,
( ~ spl0_62
| ~ spl0_9 ),
inference(rat,[],[s335,s94,s95,s128]) ).
cnf(s774,plain,
( spl0_8
| spl0_1 ),
inference(rat,[],[s419,s105,s135,s136,s57,s770,s63,s773,s759,s15,s677,s546,s749,s3,s753,s772,s156,s157,s158,s741,s356,s766,s767,s763,s768,s738]) ).
cnf(s775,plain,
( ~ spl0_56
| ~ spl0_8 ),
inference(rat,[],[s538,s105,s135,s136]) ).
cnf(s776,plain,
( ~ spl0_29
| ~ spl0_6
| ~ spl0_12 ),
inference(rat,[],[s425,s163,s164]) ).
cnf(s777,plain,
( ~ spl0_59
| ~ spl0_5
| ~ spl0_14 ),
inference(rat,[],[s289,s112,s147]) ).
cnf(s778,plain,
( ~ spl0_30
| ~ spl0_23 ),
inference(rat,[],[s313,s101,s133,s134]) ).
cnf(s779,plain,
( spl0_24
| spl0_5
| spl0_1 ),
inference(rat,[],[s776,s43,s26,s5,s768,s753,s172,s775,s774,s767,s763,s738]) ).
cnf(s780,plain,
( ~ spl0_24
| ~ spl0_15
| ~ spl0_2 ),
inference(rat,[],[s380,s153,s155]) ).
cnf(s781,plain,
( ~ spl0_15
| spl0_1 ),
inference(rat,[],[s171,s119,s777,s608,s779,s780,s778,s473,s57,s759,s763,s775,s774,s738]) ).
cnf(s782,plain,
spl0_1,
inference(rat,[],[s770,s63,s6,s773,s356,s8,s781,s753,s172,s775,s774,s768,s767,s763,s738]) ).
cnf(s783,plain,
( ~ spl0_26
| ~ spl0_25 ),
inference(rat,[],[s482,s106,s137,s138]) ).
cnf(s784,plain,
( ~ spl0_15
| spl0_14 ),
inference(rat,[],[s541,s135,s136,s57,s759,s782,s738]) ).
cnf(s785,plain,
( spl0_34
| ~ spl0_7
| spl0_8 ),
inference(rat,[],[s227,s110,s143,s55,s21,s778,s290,s46,s24,s85,s745,s6,s784,s593,s86,s122,s169,s755,s40,s783,s360,s753,s738,s782]) ).
cnf(s786,plain,
( ~ spl0_38
| ~ spl0_16
| ~ spl0_11 ),
inference(rat,[],[s399,s92,s93]) ).
cnf(s787,plain,
( ~ spl0_7
| ~ spl0_11
| spl0_8 ),
inference(rat,[],[s397,s70,s71,s37,s525,s110,s142,s166,s786,s614,s4,s739,s785,s35,s734,s235,s85,s86,s122,s169,s54,s755,s40,s783,s753,s360,s748,s738,s782]) ).
cnf(s788,plain,
( spl0_5
| spl0_34
| spl0_16
| spl0_8 ),
inference(rat,[],[s28,s767,s393,s10,s98,s130,s131,s746,s17,s738]) ).
cnf(s789,plain,
( spl0_2
| ~ spl0_12
| spl0_29
| ~ spl0_35
| spl0_34
| ~ spl0_6
| spl0_16 ),
inference(rat,[],[s220,s110,s143,s55,s778,s46,s770,s745,s38,s10,s738]) ).
cnf(s790,plain,
~ spl0_55,
inference(rat,[],[s640,s109,s140,s141,s782]) ).
cnf(s791,plain,
( ~ spl0_7
| spl0_8 ),
inference(rat,[],[s593,s86,s122,s6,s169,s356,s565,s755,s4,s677,s40,s739,s156,s157,s158,s783,s787,s785,s753,s360,s738,s782]) ).
cnf(s792,plain,
( spl0_34
| spl0_16
| spl0_8 ),
inference(rat,[],[s46,s745,s324,s6,s759,s159,s161,s770,s44,s173,s764,s767,s789,s20,s761,s788,s24,s26,s749,s3,s791,s738,s790]) ).
cnf(s793,plain,
( ~ spl0_34
| ~ spl0_4 ),
inference(rat,[],[s427,s156,s157,s158,s782]) ).
cnf(s794,plain,
( spl0_7
| spl0_8 ),
inference(rat,[],[s36,s329,s786,s792,s24,s793,s92,s93,s3,s27,s738]) ).
cnf(s795,plain,
spl0_8,
inference(rat,[],[s794,s791]) ).
cnf(s796,plain,
~ spl0_56,
inference(rat,[],[s775,s795]) ).
cnf(s797,plain,
~ spl0_7,
inference(rat,[],[s356,s8,s748,s54,s575,s92,s127,s165,s745,s6,s784,s593,s86,s122,s169,s755,s40,s783,s753,s360,s738,s795,s796,s782]) ).
cnf(s800,plain,
( ~ spl0_62
| ~ spl0_11 ),
inference(rat,[],[s211,s94,s95,s128,s795]) ).
cnf(s801,plain,
~ spl0_11,
inference(rat,[],[s35,s622,s735,s644,s9,s113,s148,s770,s72,s73,s174,s63,s800,s748,s738,s795,s797,s796]) ).
cnf(s802,plain,
( ~ spl0_154
| ~ spl0_153
| ~ spl0_15 ),
inference(rat,[],[s462,s565,s782]) ).
cnf(s803,plain,
~ spl0_15,
inference(rat,[],[s802,s156,s157,s36,s733,s601,s76,s77,s78,s34,s435,s162,s164,s38,s767,s173,s770,s784,s801,s738,s782,s790]) ).
cnf(s804,plain,
spl0_9,
inference(rat,[],[s8,s801,s738,s803]) ).
cnf(s805,plain,
~ spl0_13,
inference(rat,[],[s356,s801,s804]) ).
cnf(s807,plain,
~ spl0_62,
inference(rat,[],[s773,s804]) ).
cnf(s808,plain,
spl0_14,
inference(rat,[],[s6,s803,s738,s805]) ).
cnf(s814,plain,
spl0_50,
inference(rat,[],[s63,s738,s797,s807]) ).
cnf(s816,plain,
$false,
inference(rat,[],[s770,s808,s814]) ).
fof(f2876,plain,
$false,
inference(avatar_sat_refutation,[],[s816]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN508-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.22 % Computer : n019.cluster.edu
% 0.10/0.22 % Model : x86_64 x86_64
% 0.10/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22 % Memory : 8046.5625MB
% 0.10/0.22 % OS : Linux 6.8.0-71-generic
% 0.10/0.22 % CPULimit : 300
% 0.10/0.22 % WCLimit : 300
% 0.10/0.22 % DateTime : Mon Sep 28 16:20:49 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.26 Running first-order theorem proving
% 0.10/0.26 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.38/1.04 % (4130764)Input is clausal, will run a generic CNF schedule.
% 2.38/1.04 % (4130775)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3511622342:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.38/1.04 % (4130775)First to succeed.
% 2.38/1.04 % (4130775)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4130764"
% 2.38/1.04 % (4130777)dis-21_1_sil=8000:lcm=predicate:random_seed=3547686901:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 2.38/1.04 % (4130773)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4193513801:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.38/1.04 % (4130772)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2785261120:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.38/1.04 % (4130774)lrs+10_1_sil=8000:sp=occurrence:random_seed=573416202:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.38/1.04 % (4130771)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1870385792:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.38/1.04 % (4130776)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2619258569:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.38/1.04 % (4130777)Also succeeded, but the first one will report.
% 2.38/1.04 % (4130776)Also succeeded, but the first one will report.
% 2.38/1.04 % (4130774)Also succeeded, but the first one will report.
% 2.38/1.04 % (4130775)Refutation found. Thanks to Tanya!
% 2.38/1.04 % SZS status Unsatisfiable for theBenchmark
% 2.38/1.04 % SZS output start Proof for theBenchmark
% See solution above
% 2.81/1.23 % (4130775)------------------------------
% 2.81/1.23 % (4130775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.81/1.23 % (4130775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.81/1.23 % (4130775)CaDiCaL version: 2.1.3
% 2.81/1.23 % (4130775)Termination reason: Refutation
% 2.81/1.23 % (4130775)Time elapsed: 0.024 s
% 2.81/1.23 % (4130775)Peak memory usage: 90 MB
% 2.81/1.23 % (4130775)Instructions burned: 63 (million)
% 2.81/1.23 % (4130775)------------------------------
% 2.81/1.23 % (4130775)------------------------------
% 2.81/1.23 % (4130764)Success in time 0.287 s
% 2.81/1.23 % Vampire exiting
%------------------------------------------------------------------------------