%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN455-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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:08:56 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.30s
% Output : Refutation 0.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 251
% Syntax : Number of formulae : 973 ( 40 unt; 127 def)
% Number of atoms : 3169 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 3957 (1761 ~;2069 |; 0 &)
% ( 127 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 159 ( 158 usr; 155 prp; 0-1 aty)
% Number of functors : 26 ( 26 usr; 26 con; 0-0 aty)
% Number of variables : 164 ( 0 sgn 164 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,negated_conjecture,
( ~ hskp26
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
fof(f10,negated_conjecture,
( ~ hskp21
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
fof(f26,negated_conjecture,
( ~ hskp5
| ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause26) ).
fof(f32,negated_conjecture,
( hskp26
| hskp5
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause32) ).
fof(f33,negated_conjecture,
( hskp20
| hskp14
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause33) ).
fof(f34,negated_conjecture,
( hskp12
| hskp13
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause34) ).
fof(f35,negated_conjecture,
( ~ hskp30
| c0_1(a942) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause35) ).
fof(f36,negated_conjecture,
( ~ hskp30
| c1_1(a942) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause36) ).
fof(f37,negated_conjecture,
( ~ hskp30
| c2_1(a942) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause37) ).
fof(f41,negated_conjecture,
( ~ hskp28
| c0_1(a916) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause41) ).
fof(f42,negated_conjecture,
( ~ hskp28
| c1_1(a916) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause42) ).
fof(f43,negated_conjecture,
( ~ hskp28
| c3_1(a916) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause43) ).
fof(f44,negated_conjecture,
( ~ hskp27
| c1_1(a900) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause44) ).
fof(f45,negated_conjecture,
( ~ hskp27
| c2_1(a900) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause45) ).
fof(f46,negated_conjecture,
( ~ hskp27
| c3_1(a900) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause46) ).
fof(f47,negated_conjecture,
( ~ hskp26
| c0_1(a979) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause47) ).
fof(f49,negated_conjecture,
( ~ hskp25
| c0_1(a960) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause49) ).
fof(f51,negated_conjecture,
( ~ hskp23
| c1_1(a954) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause51) ).
fof(f52,negated_conjecture,
( ~ hskp23
| c3_1(a954) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause52) ).
fof(f55,negated_conjecture,
( ~ hskp20
| c0_1(a939) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause55) ).
fof(f59,negated_conjecture,
( ~ hskp16
| c1_1(a926) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause59) ).
fof(f60,negated_conjecture,
( ~ hskp16
| c2_1(a926) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause60) ).
fof(f61,negated_conjecture,
( ~ hskp15
| c2_1(a924) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause61) ).
fof(f62,negated_conjecture,
( ~ hskp14
| c3_1(a923) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause62) ).
fof(f63,negated_conjecture,
( ~ hskp13
| c2_1(a921) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause63) ).
fof(f64,negated_conjecture,
( ~ hskp12
| c1_1(a917) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause64) ).
fof(f65,negated_conjecture,
( ~ hskp12
| c3_1(a917) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause65) ).
fof(f66,negated_conjecture,
( ~ hskp11
| c0_1(a914) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause66) ).
fof(f67,negated_conjecture,
( ~ hskp11
| c3_1(a914) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause67) ).
fof(f68,negated_conjecture,
( ~ hskp10
| c1_1(a912) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause68) ).
fof(f69,negated_conjecture,
( ~ hskp10
| c2_1(a912) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause69) ).
fof(f70,negated_conjecture,
( ~ hskp9
| c2_1(a910) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause70) ).
fof(f71,negated_conjecture,
( ~ hskp8
| c1_1(a909) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause71) ).
fof(f72,negated_conjecture,
( ~ hskp7
| c1_1(a908) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause72) ).
fof(f73,negated_conjecture,
( ~ hskp6
| c0_1(a907) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause73) ).
fof(f74,negated_conjecture,
( ~ hskp6
| c1_1(a907) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause74) ).
fof(f75,negated_conjecture,
( ~ hskp5
| c0_1(a906) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause75) ).
fof(f77,negated_conjecture,
( ~ hskp4
| c3_1(a905) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause77) ).
fof(f79,negated_conjecture,
( ~ hskp2
| c0_1(a903) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause79) ).
fof(f80,negated_conjecture,
( ~ hskp1
| c0_1(a902) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause80) ).
fof(f81,negated_conjecture,
( ~ hskp1
| c2_1(a902) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause81) ).
fof(f82,negated_conjecture,
( ~ c3_1(a979)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause82) ).
fof(f83,negated_conjecture,
( ~ c1_1(a960)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause83) ).
fof(f87,negated_conjecture,
( ~ c0_1(a954)
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause87) ).
fof(f89,negated_conjecture,
( ~ c0_1(a946)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause89) ).
fof(f90,negated_conjecture,
( ~ c2_1(a946)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause90) ).
fof(f91,negated_conjecture,
( ~ c3_1(a946)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause91) ).
fof(f92,negated_conjecture,
( ~ c1_1(a939)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause92) ).
fof(f93,negated_conjecture,
( ~ c3_1(a939)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause93) ).
fof(f97,negated_conjecture,
( ~ c1_1(a936)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause97) ).
fof(f98,negated_conjecture,
( ~ c2_1(a936)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause98) ).
fof(f99,negated_conjecture,
( ~ c3_1(a936)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause99) ).
fof(f100,negated_conjecture,
( ~ c3_1(a926)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause100) ).
fof(f101,negated_conjecture,
( ~ c0_1(a924)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause101) ).
fof(f103,negated_conjecture,
( ~ c0_1(a923)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause103) ).
fof(f104,negated_conjecture,
( ~ c1_1(a923)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause104) ).
fof(f105,negated_conjecture,
( ~ c0_1(a921)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause105) ).
fof(f106,negated_conjecture,
( ~ c3_1(a921)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause106) ).
fof(f107,negated_conjecture,
( ~ c2_1(a917)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause107) ).
fof(f108,negated_conjecture,
( ~ c2_1(a914)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause108) ).
fof(f109,negated_conjecture,
( ~ c0_1(a912)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause109) ).
fof(f110,negated_conjecture,
( ~ c1_1(a910)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause110) ).
fof(f111,negated_conjecture,
( ~ c3_1(a910)
| ~ hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause111) ).
fof(f113,negated_conjecture,
( ~ c3_1(a909)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause113) ).
fof(f114,negated_conjecture,
( ~ c2_1(a908)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause114) ).
fof(f115,negated_conjecture,
( ~ c3_1(a908)
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause115) ).
fof(f116,negated_conjecture,
( ~ c2_1(a907)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause116) ).
fof(f117,negated_conjecture,
( ~ c3_1(a906)
| ~ hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause117) ).
fof(f118,negated_conjecture,
( ~ c0_1(a905)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause118) ).
fof(f119,negated_conjecture,
( ~ c2_1(a905)
| ~ hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause119) ).
fof(f120,negated_conjecture,
( ~ c1_1(a904)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause120) ).
fof(f121,negated_conjecture,
( ~ c2_1(a904)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause121) ).
fof(f122,negated_conjecture,
( ~ c2_1(a903)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause122) ).
fof(f123,negated_conjecture,
( ~ c3_1(a903)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause123) ).
fof(f124,negated_conjecture,
( ~ c1_1(a902)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause124) ).
fof(f125,negated_conjecture,
( ~ c0_1(a901)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause125) ).
fof(f126,negated_conjecture,
( ~ c1_1(a901)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause126) ).
fof(f127,negated_conjecture,
( ~ c3_1(a901)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause127) ).
fof(f128,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| hskp1
| hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause128) ).
fof(f129,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp27
| hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause129) ).
fof(f130,negated_conjecture,
! [X0] :
( ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c3_1(X0)
| hskp11
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause130) ).
fof(f132,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp3
| hskp4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause132) ).
fof(f133,negated_conjecture,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c1_1(X0)
| hskp6
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause133) ).
fof(f135,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp28
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause135) ).
fof(f136,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c3_1(X0)
| hskp2
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause136) ).
fof(f137,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| hskp12
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause137) ).
fof(f140,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c3_1(X0)
| hskp30
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause140) ).
fof(f141,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c1_1(X0)
| hskp28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause141) ).
fof(f142,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp6
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause142) ).
fof(f143,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp1
| hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause143) ).
fof(f144,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| hskp30
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause144) ).
fof(f145,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp3
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause145) ).
fof(f146,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp7
| hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause146) ).
fof(f147,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp28
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause147) ).
fof(f148,negated_conjecture,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| hskp7
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause148) ).
fof(f151,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp5
| hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause151) ).
fof(f152,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp25
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause152) ).
fof(f153,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| hskp10
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause153) ).
fof(f154,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp27
| hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause154) ).
fof(f156,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0)
| hskp20
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause156) ).
fof(f157,negated_conjecture,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp23
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause157) ).
fof(f158,negated_conjecture,
! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| hskp11
| hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause158) ).
fof(f159,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| c1_1(X0)
| c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause159) ).
fof(f160,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause160) ).
fof(f161,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause161) ).
fof(f162,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause162) ).
fof(f163,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X0)
| c2_1(X1)
| c3_1(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause163) ).
fof(f164,negated_conjecture,
! [X0,X1] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c0_1(X0)
| c0_1(X1)
| c3_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause164) ).
fof(f166,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| hskp27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause166) ).
fof(f167,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c2_1(X0)
| c3_1(X0)
| c1_1(X1)
| hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause167) ).
fof(f169,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c3_1(X0)
| c2_1(X1)
| c3_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause169) ).
fof(f170,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X1)
| c1_1(X1)
| hskp5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause170) ).
fof(f171,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c2_1(X1)
| hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause171) ).
fof(f172,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| c1_1(X1)
| c3_1(X1)
| hskp9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause172) ).
fof(f173,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c1_1(X1)
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause173) ).
fof(f174,negated_conjecture,
! [X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| c2_1(X1)
| c3_1(X1)
| hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause174) ).
fof(f176,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause176) ).
fof(f178,negated_conjecture,
! [X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c3_1(X1)
| c1_1(X1)
| hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause178) ).
fof(f179,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X0)
| c3_1(X0)
| c0_1(X1)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause179) ).
fof(f180,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c2_1(X1)
| c2_1(X0)
| c3_1(X0)
| c0_1(X1)
| c0_1(X2)
| c1_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause180) ).
fof(f181,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c0_1(X1)
| c2_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause181) ).
fof(f182,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| c3_1(X0)
| c3_1(X1)
| c0_1(X2)
| c1_1(X2)
| c2_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause182) ).
fof(f183,negated_conjecture,
! [X2,X0,X1] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X1)
| ~ c1_1(X2)
| ~ c2_1(X2)
| c2_1(X0)
| c1_1(X1)
| c3_1(X1)
| c0_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause183) ).
fof(f184,negated_conjecture,
! [X2,X0,X1] :
( ~ c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X1)
| ~ c2_1(X1)
| ~ c1_1(X2)
| c3_1(X1)
| c2_1(X2)
| c3_1(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause184) ).
fof(f186,definition,
( spl0_1
<=> ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f187,plain,
( ! [X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c2_1(X2) )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f186]) ).
fof(f189,definition,
( spl0_2
<=> ! [X1] :
( ~ c0_1(X1)
| c3_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f190,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f192,definition,
( spl0_3
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f196,definition,
( spl0_4
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f197,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f198,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f184,f196,f192,f189,f186]) ).
fof(f200,definition,
( spl0_5
<=> ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f201,plain,
( ! [X2] :
( ~ c1_1(X2)
| c0_1(X2)
| ~ c2_1(X2) )
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f200]) ).
fof(f203,definition,
( spl0_6
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f204,plain,
( ! [X1] :
( c1_1(X1)
| c3_1(X1)
| ~ c2_1(X1) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f203]) ).
fof(f206,definition,
( spl0_7
<=> ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f207,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f208,plain,
( spl0_5
| spl0_6
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f183,f206,f192,f203,f200]) ).
fof(f210,definition,
( spl0_8
<=> ! [X2] :
( c0_1(X2)
| c2_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f211,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2)
| c0_1(X2) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f210]) ).
fof(f213,definition,
( spl0_9
<=> ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f214,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f213]) ).
fof(f215,plain,
( spl0_8
| spl0_2
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f182,f213,f192,f189,f210]) ).
fof(f217,definition,
( spl0_10
<=> ! [X1] :
( ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f218,plain,
( ! [X1] :
( c2_1(X1)
| ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f219,plain,
( spl0_8
| spl0_10
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f181,f196,f192,f217,f210]) ).
fof(f221,definition,
( spl0_11
<=> ! [X2] :
( c0_1(X2)
| c3_1(X2)
| c1_1(X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f222,plain,
( ! [X2] :
( c1_1(X2)
| c3_1(X2)
| c0_1(X2) )
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f221]) ).
fof(f224,definition,
( spl0_12
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f225,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f224]) ).
fof(f226,plain,
( spl0_11
| spl0_5
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f180,f224,f192,f200,f221]) ).
fof(f228,definition,
( spl0_13
<=> ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f229,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f228]) ).
fof(f231,definition,
( spl0_14
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f232,plain,
( ! [X0] :
( c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f231]) ).
fof(f233,plain,
( spl0_8
| spl0_13
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f179,f231,f192,f228,f210]) ).
fof(f235,definition,
( spl0_15
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f239,definition,
( spl0_16
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f240,plain,
( ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X1) )
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f241,plain,
( spl0_15
| spl0_16
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f178,f196,f192,f239,f235]) ).
fof(f243,definition,
( spl0_17
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f247,definition,
( spl0_18
<=> ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f248,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f250,definition,
( spl0_19
<=> ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f251,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f250]) ).
fof(f254,definition,
( spl0_20
<=> ! [X1] :
( c0_1(X1)
| c3_1(X1)
| c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f255,plain,
( ! [X1] :
( c2_1(X1)
| c3_1(X1)
| c0_1(X1) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f254]) ).
fof(f256,plain,
( spl0_11
| spl0_20
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f176,f224,f192,f254,f221]) ).
fof(f258,definition,
( spl0_21
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f262,definition,
( spl0_22
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f263,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f262]) ).
fof(f265,definition,
( spl0_23
<=> ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f266,plain,
( ! [X0] :
( ~ c1_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f269,definition,
( spl0_24
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f272,plain,
( spl0_24
| spl0_1
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f174,f250,f192,f186,f269]) ).
fof(f274,definition,
( spl0_25
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f278,definition,
( spl0_26
<=> ! [X1] :
( ~ c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f279,plain,
( ! [X1] :
( c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X1) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f281,definition,
( spl0_27
<=> ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f282,plain,
( ! [X0] :
( ~ c0_1(X0)
| c2_1(X0)
| ~ c1_1(X0) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f281]) ).
fof(f283,plain,
( spl0_25
| spl0_26
| ~ spl0_3
| spl0_27 ),
inference(avatar_split_clause,[],[f173,f281,f192,f278,f274]) ).
fof(f285,definition,
( spl0_28
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f289,definition,
( spl0_29
<=> ! [X0] :
( ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f290,plain,
( ! [X0] :
( ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f289]) ).
fof(f291,plain,
( spl0_28
| spl0_14
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f172,f289,f192,f231,f285]) ).
fof(f293,definition,
( spl0_30
<=> ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f294,plain,
( ! [X1] :
( ~ c0_1(X1)
| c2_1(X1)
| c1_1(X1) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f293]) ).
fof(f295,plain,
( spl0_17
| spl0_30
| ~ spl0_3
| spl0_4 ),
inference(avatar_split_clause,[],[f171,f196,f192,f293,f243]) ).
fof(f297,definition,
( spl0_31
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f301,definition,
( spl0_32
<=> ! [X1] :
( ~ c3_1(X1)
| c1_1(X1)
| c0_1(X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f302,plain,
( ! [X1] :
( c1_1(X1)
| ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f303,plain,
( spl0_31
| spl0_32
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f170,f250,f192,f301,f297]) ).
fof(f304,plain,
( spl0_25
| spl0_12
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f169,f265,f192,f224,f274]) ).
fof(f311,definition,
( spl0_34
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f314,plain,
( spl0_34
| spl0_16
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f167,f186,f192,f239,f311]) ).
fof(f316,definition,
( spl0_35
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f319,plain,
( spl0_35
| spl0_26
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f166,f186,f192,f278,f316]) ).
fof(f325,plain,
( spl0_31
| spl0_13
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f164,f247,f192,f228,f297]) ).
fof(f326,plain,
( spl0_1
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f163,f206,f192,f186]) ).
fof(f328,definition,
( spl0_37
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f332,definition,
( spl0_38
<=> ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f333,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f332]) ).
fof(f334,plain,
( spl0_37
| spl0_20
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f162,f332,f192,f254,f328]) ).
fof(f335,plain,
( spl0_25
| spl0_8
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f161,f262,f192,f210,f274]) ).
fof(f336,plain,
( spl0_35
| spl0_8
| ~ spl0_3
| spl0_38 ),
inference(avatar_split_clause,[],[f160,f332,f192,f210,f316]) ).
fof(f337,plain,
( spl0_28
| spl0_20
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f159,f293,f192,f254,f285]) ).
fof(f339,definition,
( spl0_39
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f343,definition,
( spl0_40
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f346,plain,
( spl0_39
| spl0_40
| ~ spl0_3
| spl0_19 ),
inference(avatar_split_clause,[],[f158,f250,f192,f343,f339]) ).
fof(f348,definition,
( spl0_41
<=> hskp23 ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f351,plain,
( spl0_17
| spl0_41
| ~ spl0_3
| spl0_29 ),
inference(avatar_split_clause,[],[f157,f289,f192,f348,f243]) ).
fof(f353,definition,
( spl0_42
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f356,plain,
( spl0_37
| spl0_42
| ~ spl0_3
| spl0_9 ),
inference(avatar_split_clause,[],[f156,f213,f192,f353,f328]) ).
fof(f358,definition,
( spl0_43
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f362,definition,
( spl0_44
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f367,definition,
( spl0_45
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f370,plain,
( spl0_45
| spl0_35
| ~ spl0_3
| spl0_23 ),
inference(avatar_split_clause,[],[f154,f265,f192,f316,f367]) ).
fof(f372,definition,
( spl0_46
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f375,plain,
( spl0_34
| spl0_46
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f153,f206,f192,f372,f311]) ).
fof(f376,plain,
( spl0_34
| spl0_21
| ~ spl0_3
| spl0_7 ),
inference(avatar_split_clause,[],[f152,f206,f192,f258,f311]) ).
fof(f378,definition,
( spl0_47
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f381,plain,
( spl0_47
| spl0_31
| ~ spl0_3
| spl0_22 ),
inference(avatar_split_clause,[],[f151,f262,f192,f297,f378]) ).
fof(f388,plain,
( spl0_45
| spl0_47
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f148,f247,f192,f378,f367]) ).
fof(f390,definition,
( spl0_49
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f393,plain,
( spl0_24
| spl0_49
| ~ spl0_3
| spl0_18 ),
inference(avatar_split_clause,[],[f147,f247,f192,f390,f269]) ).
fof(f395,definition,
( spl0_50
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f398,plain,
( spl0_50
| spl0_47
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f146,f200,f192,f378,f395]) ).
fof(f400,definition,
( spl0_51
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f403,plain,
( spl0_45
| spl0_51
| ~ spl0_3
| spl0_5 ),
inference(avatar_split_clause,[],[f145,f200,f192,f400,f367]) ).
fof(f404,plain,
( spl0_28
| spl0_44
| ~ spl0_3
| spl0_1 ),
inference(avatar_split_clause,[],[f144,f186,f192,f362,f285]) ).
fof(f405,plain,
( spl0_41
| spl0_15
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f143,f224,f192,f235,f348]) ).
fof(f407,definition,
( spl0_52
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f410,plain,
( spl0_50
| spl0_52
| ~ spl0_3
| spl0_12 ),
inference(avatar_split_clause,[],[f142,f224,f192,f407,f395]) ).
fof(f411,plain,
( spl0_49
| ~ spl0_3
| spl0_16 ),
inference(avatar_split_clause,[],[f141,f239,f192,f390]) ).
fof(f412,plain,
( spl0_47
| spl0_44
| ~ spl0_3
| spl0_14 ),
inference(avatar_split_clause,[],[f140,f231,f192,f362,f378]) ).
fof(f426,plain,
( spl0_43
| spl0_39
| ~ spl0_3
| spl0_30 ),
inference(avatar_split_clause,[],[f137,f293,f192,f339,f358]) ).
fof(f428,definition,
( spl0_56
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f431,plain,
( spl0_25
| spl0_56
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f136,f228,f192,f428,f274]) ).
fof(f432,plain,
( spl0_39
| spl0_49
| ~ spl0_3
| spl0_13 ),
inference(avatar_split_clause,[],[f135,f228,f192,f390,f339]) ).
fof(f437,plain,
( spl0_47
| spl0_52
| ~ spl0_3
| spl0_32 ),
inference(avatar_split_clause,[],[f133,f301,f192,f407,f378]) ).
fof(f439,definition,
( spl0_58
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f443,definition,
( spl0_59
<=> ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f444,plain,
( ! [X0] :
( ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f445,plain,
( spl0_58
| spl0_51
| ~ spl0_3
| spl0_59 ),
inference(avatar_split_clause,[],[f132,f443,f192,f400,f439]) ).
fof(f447,definition,
( spl0_60
<=> ! [X0] :
( c1_1(X0)
| c3_1(X0)
| c2_1(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f448,plain,
( ! [X0] :
( c1_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( spl0_35
| spl0_40
| spl0_60
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f130,f192,f447,f343,f316]) ).
fof(f451,plain,
( spl0_46
| spl0_35
| spl0_20
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f129,f192,f254,f316,f372]) ).
fof(f452,plain,
( spl0_56
| spl0_15
| spl0_8
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f128,f192,f210,f235,f428]) ).
fof(f454,definition,
( spl0_61
<=> c3_1(a901) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f456,plain,
( ~ c3_1(a901)
| spl0_61 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f457,plain,
( ~ spl0_25
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f127,f454,f274]) ).
fof(f459,definition,
( spl0_62
<=> c1_1(a901) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f461,plain,
( ~ c1_1(a901)
| spl0_62 ),
inference(avatar_component_clause,[],[f459]) ).
fof(f462,plain,
( ~ spl0_25
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f126,f459,f274]) ).
fof(f464,definition,
( spl0_63
<=> c0_1(a901) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f466,plain,
( ~ c0_1(a901)
| spl0_63 ),
inference(avatar_component_clause,[],[f464]) ).
fof(f467,plain,
( ~ spl0_25
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f125,f464,f274]) ).
fof(f469,definition,
( spl0_64
<=> c1_1(a902) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f471,plain,
( ~ c1_1(a902)
| spl0_64 ),
inference(avatar_component_clause,[],[f469]) ).
fof(f472,plain,
( ~ spl0_15
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f124,f469,f235]) ).
fof(f474,definition,
( spl0_65
<=> c3_1(a903) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f476,plain,
( ~ c3_1(a903)
| spl0_65 ),
inference(avatar_component_clause,[],[f474]) ).
fof(f477,plain,
( ~ spl0_56
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f123,f474,f428]) ).
fof(f479,definition,
( spl0_66
<=> c2_1(a903) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f481,plain,
( ~ c2_1(a903)
| spl0_66 ),
inference(avatar_component_clause,[],[f479]) ).
fof(f482,plain,
( ~ spl0_56
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f122,f479,f428]) ).
fof(f484,definition,
( spl0_67
<=> c2_1(a904) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f486,plain,
( ~ c2_1(a904)
| spl0_67 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f487,plain,
( ~ spl0_51
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f121,f484,f400]) ).
fof(f489,definition,
( spl0_68
<=> c1_1(a904) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f491,plain,
( ~ c1_1(a904)
| spl0_68 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f492,plain,
( ~ spl0_51
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f120,f489,f400]) ).
fof(f494,definition,
( spl0_69
<=> c2_1(a905) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f496,plain,
( ~ c2_1(a905)
| spl0_69 ),
inference(avatar_component_clause,[],[f494]) ).
fof(f497,plain,
( ~ spl0_58
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f119,f494,f439]) ).
fof(f499,definition,
( spl0_70
<=> c0_1(a905) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f502,plain,
( ~ spl0_58
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f118,f499,f439]) ).
fof(f504,definition,
( spl0_71
<=> c3_1(a906) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f506,plain,
( ~ c3_1(a906)
| spl0_71 ),
inference(avatar_component_clause,[],[f504]) ).
fof(f507,plain,
( ~ spl0_31
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f117,f504,f297]) ).
fof(f509,definition,
( spl0_72
<=> c2_1(a907) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f511,plain,
( ~ c2_1(a907)
| spl0_72 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f512,plain,
( ~ spl0_52
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f116,f509,f407]) ).
fof(f514,definition,
( spl0_73
<=> c3_1(a908) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f516,plain,
( ~ c3_1(a908)
| spl0_73 ),
inference(avatar_component_clause,[],[f514]) ).
fof(f517,plain,
( ~ spl0_47
| ~ spl0_73 ),
inference(avatar_split_clause,[],[f115,f514,f378]) ).
fof(f519,definition,
( spl0_74
<=> c2_1(a908) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f521,plain,
( ~ c2_1(a908)
| spl0_74 ),
inference(avatar_component_clause,[],[f519]) ).
fof(f522,plain,
( ~ spl0_47
| ~ spl0_74 ),
inference(avatar_split_clause,[],[f114,f519,f378]) ).
fof(f524,definition,
( spl0_75
<=> c3_1(a909) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f526,plain,
( ~ c3_1(a909)
| spl0_75 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f527,plain,
( ~ spl0_37
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f113,f524,f328]) ).
fof(f534,definition,
( spl0_77
<=> c3_1(a910) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f536,plain,
( ~ c3_1(a910)
| spl0_77 ),
inference(avatar_component_clause,[],[f534]) ).
fof(f537,plain,
( ~ spl0_28
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f111,f534,f285]) ).
fof(f539,definition,
( spl0_78
<=> c1_1(a910) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f541,plain,
( ~ c1_1(a910)
| spl0_78 ),
inference(avatar_component_clause,[],[f539]) ).
fof(f542,plain,
( ~ spl0_28
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f110,f539,f285]) ).
fof(f544,definition,
( spl0_79
<=> c0_1(a912) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f546,plain,
( ~ c0_1(a912)
| spl0_79 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( ~ spl0_46
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f109,f544,f372]) ).
fof(f549,definition,
( spl0_80
<=> c2_1(a914) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f551,plain,
( ~ c2_1(a914)
| spl0_80 ),
inference(avatar_component_clause,[],[f549]) ).
fof(f552,plain,
( ~ spl0_40
| ~ spl0_80 ),
inference(avatar_split_clause,[],[f108,f549,f343]) ).
fof(f554,definition,
( spl0_81
<=> c2_1(a917) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f556,plain,
( ~ c2_1(a917)
| spl0_81 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f557,plain,
( ~ spl0_39
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f107,f554,f339]) ).
fof(f559,definition,
( spl0_82
<=> c3_1(a921) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f561,plain,
( ~ c3_1(a921)
| spl0_82 ),
inference(avatar_component_clause,[],[f559]) ).
fof(f562,plain,
( ~ spl0_45
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f106,f559,f367]) ).
fof(f564,definition,
( spl0_83
<=> c0_1(a921) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f566,plain,
( ~ c0_1(a921)
| spl0_83 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f567,plain,
( ~ spl0_45
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f105,f564,f367]) ).
fof(f569,definition,
( spl0_84
<=> c1_1(a923) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f571,plain,
( ~ c1_1(a923)
| spl0_84 ),
inference(avatar_component_clause,[],[f569]) ).
fof(f572,plain,
( ~ spl0_50
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f104,f569,f395]) ).
fof(f574,definition,
( spl0_85
<=> c0_1(a923) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f576,plain,
( ~ c0_1(a923)
| spl0_85 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f577,plain,
( ~ spl0_50
| ~ spl0_85 ),
inference(avatar_split_clause,[],[f103,f574,f395]) ).
fof(f584,definition,
( spl0_87
<=> c0_1(a924) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f586,plain,
( ~ c0_1(a924)
| spl0_87 ),
inference(avatar_component_clause,[],[f584]) ).
fof(f587,plain,
( ~ spl0_17
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f101,f584,f243]) ).
fof(f589,definition,
( spl0_88
<=> c3_1(a926) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f591,plain,
( ~ c3_1(a926)
| spl0_88 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f592,plain,
( ~ spl0_24
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f100,f589,f269]) ).
fof(f594,definition,
( spl0_89
<=> c3_1(a936) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f596,plain,
( ~ c3_1(a936)
| spl0_89 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f597,plain,
( ~ spl0_43
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f99,f594,f358]) ).
fof(f599,definition,
( spl0_90
<=> c2_1(a936) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f601,plain,
( ~ c2_1(a936)
| spl0_90 ),
inference(avatar_component_clause,[],[f599]) ).
fof(f602,plain,
( ~ spl0_43
| ~ spl0_90 ),
inference(avatar_split_clause,[],[f98,f599,f358]) ).
fof(f604,definition,
( spl0_91
<=> c1_1(a936) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f606,plain,
( ~ c1_1(a936)
| spl0_91 ),
inference(avatar_component_clause,[],[f604]) ).
fof(f607,plain,
( ~ spl0_43
| ~ spl0_91 ),
inference(avatar_split_clause,[],[f97,f604,f358]) ).
fof(f624,definition,
( spl0_95
<=> c3_1(a939) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f626,plain,
( ~ c3_1(a939)
| spl0_95 ),
inference(avatar_component_clause,[],[f624]) ).
fof(f627,plain,
( ~ spl0_42
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f93,f624,f353]) ).
fof(f629,definition,
( spl0_96
<=> c1_1(a939) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f631,plain,
( ~ c1_1(a939)
| spl0_96 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f632,plain,
( ~ spl0_42
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f92,f629,f353]) ).
fof(f634,definition,
( spl0_97
<=> c3_1(a946) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f636,plain,
( ~ c3_1(a946)
| spl0_97 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f637,plain,
( ~ spl0_34
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f91,f634,f311]) ).
fof(f639,definition,
( spl0_98
<=> c2_1(a946) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f641,plain,
( ~ c2_1(a946)
| spl0_98 ),
inference(avatar_component_clause,[],[f639]) ).
fof(f642,plain,
( ~ spl0_34
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f90,f639,f311]) ).
fof(f644,definition,
( spl0_99
<=> c0_1(a946) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f647,plain,
( ~ spl0_34
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f89,f644,f311]) ).
fof(f654,definition,
( spl0_101
<=> c0_1(a954) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f657,plain,
( ~ spl0_41
| ~ spl0_101 ),
inference(avatar_split_clause,[],[f87,f654,f348]) ).
fof(f674,definition,
( spl0_105
<=> c1_1(a960) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f676,plain,
( ~ c1_1(a960)
| spl0_105 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f677,plain,
( ~ spl0_21
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f83,f674,f258]) ).
fof(f679,definition,
( spl0_106
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f683,definition,
( spl0_107
<=> c3_1(a979) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f685,plain,
( ~ c3_1(a979)
| spl0_107 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f686,plain,
( ~ spl0_106
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f82,f683,f679]) ).
fof(f688,definition,
( spl0_108
<=> c2_1(a902) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f690,plain,
( c2_1(a902)
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f688]) ).
fof(f691,plain,
( spl0_108
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f81,f235,f688]) ).
fof(f693,definition,
( spl0_109
<=> c0_1(a902) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f695,plain,
( c0_1(a902)
| ~ spl0_109 ),
inference(avatar_component_clause,[],[f693]) ).
fof(f696,plain,
( spl0_109
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f80,f235,f693]) ).
fof(f698,definition,
( spl0_110
<=> c0_1(a903) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f700,plain,
( c0_1(a903)
| ~ spl0_110 ),
inference(avatar_component_clause,[],[f698]) ).
fof(f701,plain,
( spl0_110
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f79,f428,f698]) ).
fof(f708,definition,
( spl0_112
<=> c3_1(a905) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f710,plain,
( c3_1(a905)
| ~ spl0_112 ),
inference(avatar_component_clause,[],[f708]) ).
fof(f711,plain,
( spl0_112
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f77,f439,f708]) ).
fof(f718,definition,
( spl0_114
<=> c0_1(a906) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f720,plain,
( c0_1(a906)
| ~ spl0_114 ),
inference(avatar_component_clause,[],[f718]) ).
fof(f721,plain,
( spl0_114
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f75,f297,f718]) ).
fof(f723,definition,
( spl0_115
<=> c1_1(a907) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f725,plain,
( c1_1(a907)
| ~ spl0_115 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f726,plain,
( spl0_115
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f74,f407,f723]) ).
fof(f728,definition,
( spl0_116
<=> c0_1(a907) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f730,plain,
( c0_1(a907)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f731,plain,
( spl0_116
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f73,f407,f728]) ).
fof(f733,definition,
( spl0_117
<=> c1_1(a908) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f735,plain,
( c1_1(a908)
| ~ spl0_117 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f736,plain,
( spl0_117
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f72,f378,f733]) ).
fof(f738,definition,
( spl0_118
<=> c1_1(a909) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f740,plain,
( c1_1(a909)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f738]) ).
fof(f741,plain,
( spl0_118
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f71,f328,f738]) ).
fof(f743,definition,
( spl0_119
<=> c2_1(a910) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f745,plain,
( c2_1(a910)
| ~ spl0_119 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f746,plain,
( spl0_119
| ~ spl0_28 ),
inference(avatar_split_clause,[],[f70,f285,f743]) ).
fof(f748,definition,
( spl0_120
<=> c2_1(a912) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f750,plain,
( c2_1(a912)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f748]) ).
fof(f751,plain,
( spl0_120
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f69,f372,f748]) ).
fof(f753,definition,
( spl0_121
<=> c1_1(a912) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f755,plain,
( c1_1(a912)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f756,plain,
( spl0_121
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f68,f372,f753]) ).
fof(f758,definition,
( spl0_122
<=> c3_1(a914) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f760,plain,
( c3_1(a914)
| ~ spl0_122 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f761,plain,
( spl0_122
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f67,f343,f758]) ).
fof(f763,definition,
( spl0_123
<=> c0_1(a914) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f765,plain,
( c0_1(a914)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f766,plain,
( spl0_123
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f66,f343,f763]) ).
fof(f768,definition,
( spl0_124
<=> c3_1(a917) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f769,plain,
( ~ c3_1(a917)
| spl0_124 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f770,plain,
( c3_1(a917)
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f768]) ).
fof(f771,plain,
( spl0_124
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f65,f339,f768]) ).
fof(f773,definition,
( spl0_125
<=> c1_1(a917) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f775,plain,
( c1_1(a917)
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f773]) ).
fof(f776,plain,
( spl0_125
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f64,f339,f773]) ).
fof(f778,definition,
( spl0_126
<=> c2_1(a921) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f780,plain,
( c2_1(a921)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f778]) ).
fof(f781,plain,
( spl0_126
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f63,f367,f778]) ).
fof(f783,definition,
( spl0_127
<=> c3_1(a923) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f785,plain,
( c3_1(a923)
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f783]) ).
fof(f786,plain,
( spl0_127
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f62,f395,f783]) ).
fof(f788,definition,
( spl0_128
<=> c2_1(a924) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f790,plain,
( c2_1(a924)
| ~ spl0_128 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f791,plain,
( spl0_128
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f61,f243,f788]) ).
fof(f793,definition,
( spl0_129
<=> c2_1(a926) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f795,plain,
( c2_1(a926)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f793]) ).
fof(f796,plain,
( spl0_129
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f60,f269,f793]) ).
fof(f798,definition,
( spl0_130
<=> c1_1(a926) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f800,plain,
( c1_1(a926)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f798]) ).
fof(f801,plain,
( spl0_130
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f59,f269,f798]) ).
fof(f818,definition,
( spl0_134
<=> c0_1(a939) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f820,plain,
( c0_1(a939)
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f821,plain,
( spl0_134
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f55,f353,f818]) ).
fof(f833,definition,
( spl0_137
<=> c3_1(a954) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f836,plain,
( spl0_137
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f52,f348,f833]) ).
fof(f838,definition,
( spl0_138
<=> c1_1(a954) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f840,plain,
( c1_1(a954)
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f838]) ).
fof(f841,plain,
( spl0_138
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f51,f348,f838]) ).
fof(f848,definition,
( spl0_140
<=> c0_1(a960) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f850,plain,
( c0_1(a960)
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f851,plain,
( spl0_140
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f49,f258,f848]) ).
fof(f858,definition,
( spl0_142
<=> c0_1(a979) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f861,plain,
( spl0_142
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f47,f679,f858]) ).
fof(f863,definition,
( spl0_143
<=> c3_1(a900) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f865,plain,
( c3_1(a900)
| ~ spl0_143 ),
inference(avatar_component_clause,[],[f863]) ).
fof(f866,plain,
( spl0_143
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f46,f316,f863]) ).
fof(f868,definition,
( spl0_144
<=> c2_1(a900) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f870,plain,
( c2_1(a900)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f868]) ).
fof(f871,plain,
( spl0_144
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f45,f316,f868]) ).
fof(f873,definition,
( spl0_145
<=> c1_1(a900) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f875,plain,
( c1_1(a900)
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f876,plain,
( spl0_145
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f44,f316,f873]) ).
fof(f878,definition,
( spl0_146
<=> c3_1(a916) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f880,plain,
( c3_1(a916)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f878]) ).
fof(f881,plain,
( spl0_146
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f43,f390,f878]) ).
fof(f883,definition,
( spl0_147
<=> c1_1(a916) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f885,plain,
( c1_1(a916)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f883]) ).
fof(f886,plain,
( spl0_147
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f42,f390,f883]) ).
fof(f888,definition,
( spl0_148
<=> c0_1(a916) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f890,plain,
( c0_1(a916)
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f891,plain,
( spl0_148
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f41,f390,f888]) ).
fof(f908,definition,
( spl0_152
<=> c2_1(a942) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f910,plain,
( c2_1(a942)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f908]) ).
fof(f911,plain,
( spl0_152
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f37,f362,f908]) ).
fof(f913,definition,
( spl0_153
<=> c1_1(a942) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f915,plain,
( c1_1(a942)
| ~ spl0_153 ),
inference(avatar_component_clause,[],[f913]) ).
fof(f916,plain,
( spl0_153
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f36,f362,f913]) ).
fof(f918,definition,
( spl0_154
<=> c0_1(a942) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f920,plain,
( c0_1(a942)
| ~ spl0_154 ),
inference(avatar_component_clause,[],[f918]) ).
fof(f921,plain,
( spl0_154
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f35,f362,f918]) ).
fof(f922,plain,
( spl0_34
| spl0_45
| spl0_39 ),
inference(avatar_split_clause,[],[f34,f339,f367,f311]) ).
fof(f923,plain,
( spl0_58
| spl0_50
| spl0_42 ),
inference(avatar_split_clause,[],[f33,f353,f395,f439]) ).
fof(f924,plain,
( spl0_34
| spl0_31
| spl0_106 ),
inference(avatar_split_clause,[],[f32,f679,f297,f311]) ).
fof(f926,plain,
( spl0_3
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f26,f297,f192]) ).
fof(f931,plain,
( spl0_3
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f10,f311,f192]) ).
fof(f932,plain,
( spl0_3
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f5,f679,f192]) ).
fof(f933,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_2
| ~ spl0_12 ),
inference(forward_subsumption_resolution,[],[f225,f190]) ).
fof(f934,plain,
( ! [X1] :
( ~ c2_1(X1)
| c3_1(X1) )
| ~ spl0_2
| ~ spl0_13 ),
inference(forward_subsumption_resolution,[],[f229,f190]) ).
fof(f935,plain,
( ! [X1] :
( c1_1(X1)
| ~ c0_1(X1) )
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f240,f232]) ).
fof(f936,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c2_1(X0) )
| ~ spl0_9
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f251,f214]) ).
fof(f937,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_14
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f266,f232]) ).
fof(f963,plain,
( ~ c0_1(a906)
| ~ spl0_2
| ~ spl0_12
| spl0_71 ),
inference(resolution,[],[f506,f933]) ).
fof(f964,plain,
( $false
| ~ spl0_2
| ~ spl0_12
| spl0_71
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f963,f720]) ).
fof(f965,plain,
( ~ spl0_2
| ~ spl0_12
| spl0_71
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f964]) ).
fof(f968,plain,
( ~ c0_1(a902)
| ~ spl0_14
| ~ spl0_16
| spl0_64 ),
inference(resolution,[],[f471,f935]) ).
fof(f969,plain,
( $false
| ~ spl0_14
| ~ spl0_16
| spl0_64
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f968,f695]) ).
fof(f970,plain,
( ~ spl0_14
| ~ spl0_16
| spl0_64
| ~ spl0_109 ),
inference(avatar_contradiction_clause,[],[f969]) ).
fof(f997,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7
| ~ spl0_19 ),
inference(forward_subsumption_resolution,[],[f251,f207]) ).
fof(f1006,plain,
( ! [X1] :
( c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_10
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f218,f263]) ).
fof(f1011,plain,
( ~ c0_1(a903)
| ~ spl0_14
| ~ spl0_23
| spl0_65 ),
inference(resolution,[],[f937,f476]) ).
fof(f1014,plain,
( $false
| ~ spl0_14
| ~ spl0_23
| spl0_65
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f1011,f700]) ).
fof(f1015,plain,
( ~ spl0_14
| ~ spl0_23
| spl0_65
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f1014]) ).
fof(f1019,plain,
( ~ c0_1(a903)
| ~ spl0_2
| ~ spl0_12
| spl0_65 ),
inference(resolution,[],[f933,f476]) ).
fof(f1025,plain,
( ~ c3_1(a954)
| ~ spl0_7
| ~ spl0_19
| ~ spl0_138 ),
inference(resolution,[],[f997,f840]) ).
fof(f1036,plain,
( ~ c3_1(a917)
| ~ spl0_10
| ~ spl0_22
| spl0_81 ),
inference(resolution,[],[f1006,f556]) ).
fof(f1046,plain,
( ! [X1] :
( c2_1(X1)
| c0_1(X1) )
| ~ spl0_10
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f218,f255]) ).
fof(f1048,plain,
( ~ c0_1(a960)
| ~ spl0_14
| ~ spl0_16
| spl0_105 ),
inference(resolution,[],[f676,f935]) ).
fof(f1052,plain,
( ! [X1] :
( ~ c3_1(X1)
| c0_1(X1) )
| ~ spl0_10
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f218,f248]) ).
fof(f1053,plain,
( $false
| ~ spl0_14
| ~ spl0_16
| spl0_105
| ~ spl0_140 ),
inference(forward_subsumption_resolution,[],[f1048,f850]) ).
fof(f1054,plain,
( ~ spl0_14
| ~ spl0_16
| spl0_105
| ~ spl0_140 ),
inference(avatar_contradiction_clause,[],[f1053]) ).
fof(f1056,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f197,f935]) ).
fof(f1138,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f225,f1056]) ).
fof(f1185,plain,
( ~ c0_1(a903)
| ~ spl0_4
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16
| spl0_66 ),
inference(resolution,[],[f1138,f481]) ).
fof(f1190,plain,
( $false
| ~ spl0_4
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16
| spl0_66
| ~ spl0_110 ),
inference(forward_subsumption_resolution,[],[f1185,f700]) ).
fof(f1191,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16
| spl0_66
| ~ spl0_110 ),
inference(avatar_contradiction_clause,[],[f1190]) ).
fof(f1198,plain,
( ! [X1] :
( ~ c2_1(X1)
| c0_1(X1) )
| ~ spl0_13
| ~ spl0_18 ),
inference(forward_subsumption_resolution,[],[f229,f248]) ).
fof(f1209,plain,
( c0_1(a912)
| ~ spl0_13
| ~ spl0_18
| ~ spl0_120 ),
inference(resolution,[],[f1198,f750]) ).
fof(f1221,plain,
( ! [X2] :
( c2_1(X2)
| c3_1(X2) )
| ~ spl0_1
| ~ spl0_60 ),
inference(forward_subsumption_resolution,[],[f187,f448]) ).
fof(f1252,plain,
( c3_1(a946)
| ~ spl0_1
| ~ spl0_60
| spl0_98 ),
inference(resolution,[],[f1221,f641]) ).
fof(f1258,plain,
( ! [X1] :
( c3_1(X1)
| c0_1(X1) )
| ~ spl0_13
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f229,f255]) ).
fof(f1286,plain,
( c0_1(a901)
| ~ spl0_13
| ~ spl0_20
| spl0_61 ),
inference(resolution,[],[f1258,f456]) ).
fof(f1313,plain,
( spl0_97
| ~ spl0_1
| ~ spl0_60
| spl0_98 ),
inference(avatar_split_clause,[],[f1252,f639,f447,f186,f634]) ).
fof(f1318,plain,
( spl0_63
| ~ spl0_13
| ~ spl0_20
| spl0_61 ),
inference(avatar_split_clause,[],[f1286,f454,f254,f228,f464]) ).
fof(f1325,plain,
( ! [X0] :
( ~ c1_1(X0)
| c2_1(X0) )
| ~ spl0_1
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f207,f187]) ).
fof(f1451,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2) )
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f211,f935]) ).
fof(f1496,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0) )
| ~ spl0_7
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f207,f1451]) ).
fof(f1518,plain,
( ~ c3_1(a914)
| ~ spl0_7
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16
| spl0_80 ),
inference(resolution,[],[f1496,f551]) ).
fof(f1528,plain,
( $false
| ~ spl0_7
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16
| spl0_80
| ~ spl0_122 ),
inference(forward_subsumption_resolution,[],[f1518,f760]) ).
fof(f1529,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16
| spl0_80
| ~ spl0_122 ),
inference(avatar_contradiction_clause,[],[f1528]) ).
fof(f1547,plain,
( ! [X2] :
( ~ c1_1(X2)
| c3_1(X2) )
| ~ spl0_1
| ~ spl0_9 ),
inference(forward_subsumption_resolution,[],[f187,f214]) ).
fof(f1559,plain,
( c3_1(a909)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_118 ),
inference(resolution,[],[f1547,f740]) ).
fof(f1566,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| spl0_75
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f1559,f526]) ).
fof(f1567,plain,
( ~ spl0_1
| ~ spl0_9
| spl0_75
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f1566]) ).
fof(f1609,plain,
( c0_1(a900)
| ~ c2_1(a900)
| ~ spl0_5
| ~ spl0_145 ),
inference(resolution,[],[f201,f875]) ).
fof(f1615,plain,
( c0_1(a926)
| ~ c2_1(a926)
| ~ spl0_5
| ~ spl0_130 ),
inference(resolution,[],[f201,f800]) ).
fof(f1617,plain,
( c0_1(a912)
| ~ c2_1(a912)
| ~ spl0_5
| ~ spl0_121 ),
inference(resolution,[],[f201,f755]) ).
fof(f1622,plain,
( c0_1(a926)
| ~ spl0_5
| ~ spl0_129
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f1615,f795]) ).
fof(f1635,plain,
( ~ spl0_124
| ~ spl0_10
| ~ spl0_22
| spl0_81 ),
inference(avatar_split_clause,[],[f1036,f554,f262,f217,f768]) ).
fof(f1679,plain,
( ! [X0] :
( ~ c1_1(X0)
| c0_1(X0) )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f333,f1547]) ).
fof(f1687,plain,
( ~ c3_1(a914)
| ~ spl0_10
| ~ spl0_22
| spl0_80 ),
inference(resolution,[],[f1006,f551]) ).
fof(f1708,plain,
( ~ spl0_137
| ~ spl0_7
| ~ spl0_19
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1025,f838,f250,f206,f833]) ).
fof(f1718,plain,
( ~ spl0_122
| ~ spl0_10
| ~ spl0_22
| spl0_80 ),
inference(avatar_split_clause,[],[f1687,f549,f262,f217,f758]) ).
fof(f1752,plain,
( ! [X1] :
( c2_1(X1)
| ~ c0_1(X1) )
| ~ spl0_27
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f294,f282]) ).
fof(f1753,plain,
( ! [X0] :
( c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_12
| ~ spl0_22 ),
inference(forward_subsumption_resolution,[],[f225,f263]) ).
fof(f1754,plain,
( ! [X0] :
( c1_1(X0)
| c0_1(X0) )
| ~ spl0_10
| ~ spl0_20
| ~ spl0_59 ),
inference(forward_subsumption_resolution,[],[f444,f1046]) ).
fof(f1800,plain,
( ~ c2_1(a942)
| ~ spl0_9
| ~ spl0_19
| ~ spl0_153 ),
inference(resolution,[],[f936,f915]) ).
fof(f1804,plain,
( ~ c2_1(a926)
| ~ spl0_9
| ~ spl0_19
| ~ spl0_130 ),
inference(resolution,[],[f936,f800]) ).
fof(f1806,plain,
( ~ spl0_129
| ~ spl0_9
| ~ spl0_19
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f1804,f798,f250,f213,f793]) ).
fof(f1809,plain,
( ~ spl0_152
| ~ spl0_9
| ~ spl0_19
| ~ spl0_153 ),
inference(avatar_split_clause,[],[f1800,f913,f250,f213,f908]) ).
fof(f1879,plain,
( c0_1(a923)
| ~ spl0_10
| ~ spl0_18
| ~ spl0_127 ),
inference(resolution,[],[f1052,f785]) ).
fof(f1881,plain,
( $false
| ~ spl0_10
| ~ spl0_18
| spl0_85
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f1879,f576]) ).
fof(f1882,plain,
( ~ spl0_10
| ~ spl0_18
| spl0_85
| ~ spl0_127 ),
inference(avatar_contradiction_clause,[],[f1881]) ).
fof(f1921,plain,
( c2_1(a907)
| ~ spl0_1
| ~ spl0_7
| ~ spl0_115 ),
inference(resolution,[],[f1325,f725]) ).
fof(f1922,plain,
( $false
| ~ spl0_1
| ~ spl0_7
| spl0_72
| ~ spl0_115 ),
inference(forward_subsumption_resolution,[],[f1921,f511]) ).
fof(f1923,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_72
| ~ spl0_115 ),
inference(avatar_contradiction_clause,[],[f1922]) ).
fof(f1930,plain,
( ! [X1] :
( c2_1(X1)
| c3_1(X1) )
| ~ spl0_12
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f255,f225]) ).
fof(f1954,plain,
( c0_1(a946)
| ~ spl0_10
| ~ spl0_20
| spl0_98 ),
inference(resolution,[],[f1046,f641]) ).
fof(f1980,plain,
( c0_1(a901)
| ~ spl0_10
| ~ spl0_20
| ~ spl0_59
| spl0_62 ),
inference(resolution,[],[f1754,f461]) ).
fof(f1981,plain,
( $false
| ~ spl0_10
| ~ spl0_20
| ~ spl0_59
| spl0_62
| spl0_63 ),
inference(forward_subsumption_resolution,[],[f1980,f466]) ).
fof(f1982,plain,
( ~ spl0_10
| ~ spl0_20
| ~ spl0_59
| spl0_62
| spl0_63 ),
inference(avatar_contradiction_clause,[],[f1981]) ).
fof(f1994,plain,
( c3_1(a917)
| ~ spl0_12
| ~ spl0_20
| spl0_81 ),
inference(resolution,[],[f1930,f556]) ).
fof(f1999,plain,
( c3_1(a903)
| ~ spl0_12
| ~ spl0_20
| spl0_66 ),
inference(resolution,[],[f1930,f481]) ).
fof(f2007,plain,
( $false
| ~ spl0_12
| ~ spl0_20
| spl0_65
| spl0_66 ),
inference(forward_subsumption_resolution,[],[f1999,f476]) ).
fof(f2008,plain,
( ~ spl0_12
| ~ spl0_20
| spl0_65
| spl0_66 ),
inference(avatar_contradiction_clause,[],[f2007]) ).
fof(f2030,plain,
( c0_1(a900)
| ~ spl0_5
| ~ spl0_144
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f1609,f870]) ).
fof(f2084,plain,
( ~ spl0_110
| ~ spl0_2
| ~ spl0_12
| spl0_65 ),
inference(avatar_split_clause,[],[f1019,f474,f224,f189,f698]) ).
fof(f2212,plain,
( ~ c3_1(a916)
| ~ spl0_7
| ~ spl0_19
| ~ spl0_147 ),
inference(resolution,[],[f997,f885]) ).
fof(f2242,plain,
( ~ c3_1(a900)
| ~ spl0_7
| ~ spl0_19
| ~ spl0_145 ),
inference(resolution,[],[f875,f997]) ).
fof(f2288,plain,
( ~ c3_1(a905)
| c0_1(a905)
| ~ spl0_10
| spl0_69 ),
inference(resolution,[],[f218,f496]) ).
fof(f2294,plain,
( c3_1(a936)
| ~ c0_1(a936)
| ~ spl0_12
| spl0_90 ),
inference(resolution,[],[f225,f601]) ).
fof(f2295,plain,
( ~ c0_1(a936)
| ~ spl0_12
| spl0_89
| spl0_90 ),
inference(forward_subsumption_resolution,[],[f2294,f596]) ).
fof(f2303,plain,
( ~ c0_1(a979)
| ~ spl0_2
| ~ spl0_12
| spl0_107 ),
inference(resolution,[],[f933,f685]) ).
fof(f2305,plain,
( ~ c0_1(a939)
| ~ spl0_2
| ~ spl0_12
| spl0_95 ),
inference(resolution,[],[f933,f626]) ).
fof(f2315,plain,
( $false
| ~ spl0_2
| ~ spl0_12
| spl0_95
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2305,f820]) ).
fof(f2316,plain,
( ~ spl0_2
| ~ spl0_12
| spl0_95
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2315]) ).
fof(f2341,plain,
( ~ c2_1(a912)
| ~ spl0_5
| spl0_79
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f1617,f546]) ).
fof(f2344,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14 ),
inference(forward_subsumption_resolution,[],[f232,f1547]) ).
fof(f2345,plain,
( $false
| ~ spl0_5
| spl0_79
| ~ spl0_120
| ~ spl0_121 ),
inference(forward_subsumption_resolution,[],[f2341,f750]) ).
fof(f2346,plain,
( ~ spl0_5
| spl0_79
| ~ spl0_120
| ~ spl0_121 ),
inference(avatar_contradiction_clause,[],[f2345]) ).
fof(f2384,plain,
( ~ c0_1(a906)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| spl0_71 ),
inference(resolution,[],[f2344,f506]) ).
fof(f2394,plain,
( $false
| ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| spl0_71
| ~ spl0_114 ),
inference(forward_subsumption_resolution,[],[f2384,f720]) ).
fof(f2395,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| spl0_71
| ~ spl0_114 ),
inference(avatar_contradiction_clause,[],[f2394]) ).
fof(f2404,plain,
( c3_1(a939)
| ~ c0_1(a939)
| ~ spl0_14
| spl0_96 ),
inference(resolution,[],[f232,f631]) ).
fof(f2434,plain,
( ~ c0_1(a939)
| ~ spl0_14
| spl0_95
| spl0_96 ),
inference(forward_subsumption_resolution,[],[f2404,f626]) ).
fof(f2438,plain,
( $false
| ~ spl0_14
| spl0_95
| spl0_96
| ~ spl0_134 ),
inference(forward_subsumption_resolution,[],[f2434,f820]) ).
fof(f2439,plain,
( ~ spl0_14
| spl0_95
| spl0_96
| ~ spl0_134 ),
inference(avatar_contradiction_clause,[],[f2438]) ).
fof(f2452,plain,
( ~ c3_1(a923)
| c0_1(a923)
| ~ spl0_32
| spl0_84 ),
inference(resolution,[],[f302,f571]) ).
fof(f2468,plain,
( c0_1(a923)
| ~ spl0_32
| spl0_84
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f2452,f785]) ).
fof(f2471,plain,
( $false
| ~ spl0_32
| spl0_84
| spl0_85
| ~ spl0_127 ),
inference(forward_subsumption_resolution,[],[f2468,f576]) ).
fof(f2472,plain,
( ~ spl0_32
| spl0_84
| spl0_85
| ~ spl0_127 ),
inference(avatar_contradiction_clause,[],[f2471]) ).
fof(f2475,plain,
( c3_1(a946)
| c0_1(a946)
| ~ spl0_20
| spl0_98 ),
inference(resolution,[],[f641,f255]) ).
fof(f2476,plain,
( c0_1(a946)
| ~ spl0_20
| spl0_97
| spl0_98 ),
inference(forward_subsumption_resolution,[],[f2475,f636]) ).
fof(f2539,plain,
( ! [X1] :
( ~ c2_1(X1)
| ~ c3_1(X1) )
| ~ spl0_18
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f248,f290]) ).
fof(f2540,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0) )
| ~ spl0_4
| ~ spl0_23 ),
inference(forward_subsumption_resolution,[],[f266,f197]) ).
fof(f2570,plain,
( ~ c3_1(a900)
| ~ spl0_18
| ~ spl0_29
| ~ spl0_144 ),
inference(resolution,[],[f2539,f870]) ).
fof(f2604,plain,
( ~ c0_1(a907)
| ~ spl0_4
| ~ spl0_23
| ~ spl0_115 ),
inference(resolution,[],[f2540,f725]) ).
fof(f2618,plain,
( ~ c0_1(a914)
| ~ spl0_27
| ~ spl0_30
| spl0_80 ),
inference(resolution,[],[f1752,f551]) ).
fof(f2620,plain,
( ~ c0_1(a907)
| ~ spl0_27
| ~ spl0_30
| spl0_72 ),
inference(resolution,[],[f1752,f511]) ).
fof(f2634,plain,
( $false
| ~ spl0_27
| ~ spl0_30
| spl0_72
| ~ spl0_116 ),
inference(forward_subsumption_resolution,[],[f2620,f730]) ).
fof(f2635,plain,
( ~ spl0_27
| ~ spl0_30
| spl0_72
| ~ spl0_116 ),
inference(avatar_contradiction_clause,[],[f2634]) ).
fof(f2646,plain,
( c3_1(a909)
| c2_1(a909)
| ~ spl0_1
| ~ spl0_118 ),
inference(resolution,[],[f187,f740]) ).
fof(f2672,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_1
| ~ spl0_8 ),
inference(resolution,[],[f211,f187]) ).
fof(f2684,plain,
( c2_1(a936)
| c0_1(a936)
| ~ spl0_8
| spl0_91 ),
inference(resolution,[],[f211,f606]) ).
fof(f2686,plain,
( ! [X0] :
( c2_1(X0)
| c0_1(X0)
| c3_1(X0) )
| ~ spl0_1
| ~ spl0_8 ),
inference(duplicate_literal_removal,[],[f2672]) ).
fof(f2688,plain,
( c0_1(a936)
| ~ spl0_8
| spl0_90
| spl0_91 ),
inference(forward_subsumption_resolution,[],[f2684,f601]) ).
fof(f2690,plain,
( spl0_20
| ~ spl0_1
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f2686,f210,f186,f254]) ).
fof(f2705,plain,
( c0_1(a954)
| ~ spl0_1
| ~ spl0_9
| ~ spl0_38
| ~ spl0_138 ),
inference(resolution,[],[f1679,f840]) ).
fof(f2729,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(resolution,[],[f222,f187]) ).
fof(f2738,plain,
( c3_1(a910)
| c0_1(a910)
| ~ spl0_11
| spl0_78 ),
inference(resolution,[],[f222,f541]) ).
fof(f2745,plain,
( c3_1(a901)
| c0_1(a901)
| ~ spl0_11
| spl0_62 ),
inference(resolution,[],[f222,f461]) ).
fof(f2746,plain,
( ! [X0] :
( c3_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_1
| ~ spl0_11 ),
inference(duplicate_literal_removal,[],[f2729]) ).
fof(f2750,plain,
( c0_1(a901)
| ~ spl0_11
| spl0_61
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f2745,f456]) ).
fof(f2753,plain,
( c0_1(a910)
| ~ spl0_11
| spl0_77
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f2738,f536]) ).
fof(f2781,plain,
( ~ spl0_116
| ~ spl0_4
| ~ spl0_23
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f2604,f723,f265,f196,f728]) ).
fof(f2783,plain,
( c3_1(a909)
| ~ spl0_1
| ~ spl0_2
| ~ spl0_13
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f2646,f934]) ).
fof(f2790,plain,
( $false
| ~ spl0_1
| ~ spl0_2
| ~ spl0_13
| spl0_75
| ~ spl0_118 ),
inference(forward_subsumption_resolution,[],[f2783,f526]) ).
fof(f2791,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_13
| spl0_75
| ~ spl0_118 ),
inference(avatar_contradiction_clause,[],[f2790]) ).
fof(f2817,plain,
( c3_1(a908)
| c2_1(a908)
| ~ spl0_1
| ~ spl0_117 ),
inference(resolution,[],[f735,f187]) ).
fof(f2818,plain,
( c2_1(a908)
| ~ spl0_1
| spl0_73
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f2817,f516]) ).
fof(f2819,plain,
( $false
| ~ spl0_1
| spl0_73
| spl0_74
| ~ spl0_117 ),
inference(forward_subsumption_resolution,[],[f2818,f521]) ).
fof(f2820,plain,
( ~ spl0_1
| spl0_73
| spl0_74
| ~ spl0_117 ),
inference(avatar_contradiction_clause,[],[f2819]) ).
fof(f2825,plain,
( c3_1(a942)
| ~ c0_1(a942)
| ~ spl0_2
| ~ spl0_152 ),
inference(resolution,[],[f190,f910]) ).
fof(f2831,plain,
( c3_1(a926)
| ~ c0_1(a926)
| ~ spl0_2
| ~ spl0_129 ),
inference(resolution,[],[f190,f795]) ).
fof(f2835,plain,
( c3_1(a910)
| ~ c0_1(a910)
| ~ spl0_2
| ~ spl0_119 ),
inference(resolution,[],[f190,f745]) ).
fof(f2842,plain,
( ~ c0_1(a910)
| ~ spl0_2
| spl0_77
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f2835,f536]) ).
fof(f2845,plain,
( c3_1(a942)
| ~ spl0_2
| ~ spl0_152
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f2825,f920]) ).
fof(f2848,plain,
( $false
| ~ spl0_2
| ~ spl0_11
| spl0_77
| spl0_78
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f2842,f2753]) ).
fof(f2849,plain,
( ~ spl0_2
| ~ spl0_11
| spl0_77
| spl0_78
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f2848]) ).
fof(f2854,definition,
( spl0_158
<=> c0_1(a936) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f2859,plain,
( $false
| ~ spl0_13
| ~ spl0_18
| spl0_79
| ~ spl0_120 ),
inference(forward_subsumption_resolution,[],[f1209,f546]) ).
fof(f2860,plain,
( ~ spl0_13
| ~ spl0_18
| spl0_79
| ~ spl0_120 ),
inference(avatar_contradiction_clause,[],[f2859]) ).
fof(f2863,plain,
( ~ spl0_143
| ~ spl0_18
| ~ spl0_29
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f2570,f868,f289,f247,f863]) ).
fof(f2870,plain,
( spl0_158
| ~ spl0_8
| spl0_90
| spl0_91 ),
inference(avatar_split_clause,[],[f2688,f604,f599,f210,f2854]) ).
fof(f2875,plain,
( spl0_101
| ~ spl0_1
| ~ spl0_9
| ~ spl0_38
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f2705,f838,f332,f213,f186,f654]) ).
fof(f2878,plain,
( ~ spl0_123
| ~ spl0_27
| ~ spl0_30
| spl0_80 ),
inference(avatar_split_clause,[],[f2618,f549,f293,f281,f763]) ).
fof(f2892,plain,
( ~ spl0_158
| ~ spl0_12
| spl0_89
| spl0_90 ),
inference(avatar_split_clause,[],[f2295,f599,f594,f224,f2854]) ).
fof(f2900,plain,
( c0_1(a924)
| ~ spl0_13
| ~ spl0_18
| ~ spl0_128 ),
inference(resolution,[],[f1198,f790]) ).
fof(f2909,plain,
( $false
| ~ spl0_13
| ~ spl0_18
| spl0_87
| ~ spl0_128 ),
inference(forward_subsumption_resolution,[],[f2900,f586]) ).
fof(f2910,plain,
( ~ spl0_13
| ~ spl0_18
| spl0_87
| ~ spl0_128 ),
inference(avatar_contradiction_clause,[],[f2909]) ).
fof(f2912,plain,
( c0_1(a905)
| ~ spl0_10
| spl0_69
| ~ spl0_112 ),
inference(forward_subsumption_resolution,[],[f2288,f710]) ).
fof(f3005,plain,
( c3_1(a926)
| c0_1(a926)
| ~ spl0_13
| ~ spl0_129 ),
inference(resolution,[],[f229,f795]) ).
fof(f3007,plain,
( c3_1(a921)
| c0_1(a921)
| ~ spl0_13
| ~ spl0_126 ),
inference(resolution,[],[f229,f780]) ).
fof(f3016,plain,
( c0_1(a921)
| ~ spl0_13
| spl0_82
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f3007,f561]) ).
fof(f3019,plain,
( $false
| ~ spl0_13
| spl0_82
| spl0_83
| ~ spl0_126 ),
inference(forward_subsumption_resolution,[],[f3016,f566]) ).
fof(f3020,plain,
( ~ spl0_13
| spl0_82
| spl0_83
| ~ spl0_126 ),
inference(avatar_contradiction_clause,[],[f3019]) ).
fof(f3023,plain,
( ~ spl0_142
| ~ spl0_2
| ~ spl0_12
| spl0_107 ),
inference(avatar_split_clause,[],[f2303,f683,f224,f189,f858]) ).
fof(f3048,plain,
( ~ c0_1(a914)
| ~ spl0_12
| ~ spl0_22
| spl0_80 ),
inference(resolution,[],[f1753,f551]) ).
fof(f3092,plain,
( $false
| ~ spl0_12
| ~ spl0_22
| spl0_80
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f3048,f765]) ).
fof(f3093,plain,
( ~ spl0_12
| ~ spl0_22
| spl0_80
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f3092]) ).
fof(f3095,plain,
( ! [X2] :
( c1_1(X2)
| c2_1(X2) )
| ~ spl0_8
| ~ spl0_30 ),
inference(forward_subsumption_resolution,[],[f211,f294]) ).
fof(f3106,plain,
( $false
| ~ spl0_12
| ~ spl0_20
| spl0_81
| spl0_124 ),
inference(forward_subsumption_resolution,[],[f1994,f769]) ).
fof(f3107,plain,
( ~ spl0_12
| ~ spl0_20
| spl0_81
| spl0_124 ),
inference(avatar_contradiction_clause,[],[f3106]) ).
fof(f3111,plain,
( ! [X0] :
( ~ c1_1(X0)
| ~ c3_1(X0) )
| ~ spl0_4
| ~ spl0_38 ),
inference(forward_subsumption_resolution,[],[f333,f197]) ).
fof(f3132,plain,
( c2_1(a904)
| ~ spl0_8
| ~ spl0_30
| spl0_68 ),
inference(resolution,[],[f3095,f491]) ).
fof(f3151,plain,
( ~ c3_1(a917)
| ~ spl0_4
| ~ spl0_38
| ~ spl0_125 ),
inference(resolution,[],[f3111,f775]) ).
fof(f3166,plain,
( $false
| ~ spl0_4
| ~ spl0_38
| ~ spl0_124
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f3151,f770]) ).
fof(f3167,plain,
( ~ spl0_4
| ~ spl0_38
| ~ spl0_124
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f3166]) ).
fof(f3184,plain,
( c3_1(a910)
| ~ c2_1(a910)
| ~ spl0_6
| spl0_78 ),
inference(resolution,[],[f204,f541]) ).
fof(f3187,plain,
( c3_1(a901)
| ~ c2_1(a901)
| ~ spl0_6
| spl0_62 ),
inference(resolution,[],[f204,f461]) ).
fof(f3189,plain,
( c3_1(a901)
| ~ spl0_6
| ~ spl0_12
| ~ spl0_20
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f3187,f1930]) ).
fof(f3195,plain,
( $false
| ~ spl0_6
| ~ spl0_12
| ~ spl0_20
| spl0_61
| spl0_62 ),
inference(forward_subsumption_resolution,[],[f3189,f456]) ).
fof(f3196,plain,
( ~ spl0_6
| ~ spl0_12
| ~ spl0_20
| spl0_61
| spl0_62 ),
inference(avatar_contradiction_clause,[],[f3195]) ).
fof(f3205,plain,
( spl0_20
| ~ spl0_1
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f2746,f221,f186,f254]) ).
fof(f3207,plain,
( spl0_63
| ~ spl0_11
| spl0_61
| spl0_62 ),
inference(avatar_split_clause,[],[f2750,f459,f454,f221,f464]) ).
fof(f3224,plain,
( ~ c2_1(a910)
| ~ spl0_6
| spl0_77
| spl0_78 ),
inference(forward_subsumption_resolution,[],[f3184,f536]) ).
fof(f3226,plain,
( $false
| ~ spl0_6
| spl0_77
| spl0_78
| ~ spl0_119 ),
inference(forward_subsumption_resolution,[],[f3224,f745]) ).
fof(f3227,plain,
( ~ spl0_6
| spl0_77
| spl0_78
| ~ spl0_119 ),
inference(avatar_contradiction_clause,[],[f3226]) ).
fof(f3270,plain,
( c3_1(a942)
| ~ c0_1(a942)
| ~ spl0_23
| ~ spl0_153 ),
inference(resolution,[],[f266,f915]) ).
fof(f3284,plain,
( c3_1(a942)
| ~ spl0_23
| ~ spl0_153
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f3270,f920]) ).
fof(f3296,plain,
( ~ c0_1(a902)
| ~ c2_1(a902)
| ~ spl0_26
| spl0_64 ),
inference(resolution,[],[f279,f471]) ).
fof(f3301,plain,
( ~ c3_1(a942)
| ~ c0_1(a942)
| ~ spl0_29
| ~ spl0_152 ),
inference(resolution,[],[f290,f910]) ).
fof(f3328,plain,
( ~ c0_1(a942)
| ~ spl0_23
| ~ spl0_29
| ~ spl0_152
| ~ spl0_153
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f3301,f3284]) ).
fof(f3341,plain,
( $false
| ~ spl0_23
| ~ spl0_29
| ~ spl0_152
| ~ spl0_153
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f3328,f920]) ).
fof(f3342,plain,
( ~ spl0_23
| ~ spl0_29
| ~ spl0_152
| ~ spl0_153
| ~ spl0_154 ),
inference(avatar_contradiction_clause,[],[f3341]) ).
fof(f3349,plain,
( ! [X1] :
( ~ c3_1(X1)
| ~ c0_1(X1) )
| ~ spl0_4
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f240,f197]) ).
fof(f3355,plain,
( ~ c2_1(a902)
| ~ spl0_26
| spl0_64
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f3296,f695]) ).
fof(f3364,plain,
( $false
| ~ spl0_26
| spl0_64
| ~ spl0_108
| ~ spl0_109 ),
inference(forward_subsumption_resolution,[],[f3355,f690]) ).
fof(f3365,plain,
( ~ spl0_26
| spl0_64
| ~ spl0_108
| ~ spl0_109 ),
inference(avatar_contradiction_clause,[],[f3364]) ).
fof(f3380,plain,
( ~ c0_1(a914)
| ~ spl0_4
| ~ spl0_16
| ~ spl0_122 ),
inference(resolution,[],[f3349,f760]) ).
fof(f3385,plain,
( $false
| ~ spl0_4
| ~ spl0_16
| ~ spl0_122
| ~ spl0_123 ),
inference(forward_subsumption_resolution,[],[f3380,f765]) ).
fof(f3386,plain,
( ~ spl0_4
| ~ spl0_16
| ~ spl0_122
| ~ spl0_123 ),
inference(avatar_contradiction_clause,[],[f3385]) ).
fof(f3437,plain,
( ~ c3_1(a916)
| ~ c0_1(a916)
| ~ spl0_4
| ~ spl0_147 ),
inference(resolution,[],[f197,f885]) ).
fof(f3438,plain,
( ~ c3_1(a900)
| ~ c0_1(a900)
| ~ spl0_4
| ~ spl0_145 ),
inference(resolution,[],[f197,f875]) ).
fof(f3457,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_7
| ~ spl0_8 ),
inference(resolution,[],[f207,f211]) ).
fof(f3464,plain,
( c2_1(a917)
| ~ c3_1(a917)
| ~ spl0_7
| ~ spl0_125 ),
inference(resolution,[],[f207,f775]) ).
fof(f3467,plain,
( ! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_7
| ~ spl0_8 ),
inference(duplicate_literal_removal,[],[f3457]) ).
fof(f3468,plain,
( ~ c3_1(a917)
| ~ spl0_7
| spl0_81
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f3464,f556]) ).
fof(f3474,plain,
( $false
| ~ spl0_7
| spl0_81
| ~ spl0_124
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f3468,f770]) ).
fof(f3475,plain,
( ~ spl0_7
| spl0_81
| ~ spl0_124
| ~ spl0_125 ),
inference(avatar_contradiction_clause,[],[f3474]) ).
fof(f3496,plain,
( $false
| ~ spl0_8
| ~ spl0_30
| spl0_67
| spl0_68 ),
inference(forward_subsumption_resolution,[],[f3132,f486]) ).
fof(f3497,plain,
( ~ spl0_8
| ~ spl0_30
| spl0_67
| spl0_68 ),
inference(avatar_contradiction_clause,[],[f3496]) ).
fof(f3499,plain,
( ~ c0_1(a900)
| ~ spl0_4
| ~ spl0_143
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f3438,f865]) ).
fof(f3503,plain,
( ~ c0_1(a916)
| ~ spl0_4
| ~ spl0_146
| ~ spl0_147 ),
inference(forward_subsumption_resolution,[],[f3437,f880]) ).
fof(f3505,plain,
( spl0_10
| ~ spl0_7
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f3467,f210,f206,f217]) ).
fof(f3507,plain,
( $false
| ~ spl0_4
| ~ spl0_5
| ~ spl0_143
| ~ spl0_144
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f3499,f2030]) ).
fof(f3508,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_143
| ~ spl0_144
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f3507]) ).
fof(f3511,plain,
( $false
| ~ spl0_4
| ~ spl0_146
| ~ spl0_147
| ~ spl0_148 ),
inference(forward_subsumption_resolution,[],[f3503,f890]) ).
fof(f3512,plain,
( ~ spl0_4
| ~ spl0_146
| ~ spl0_147
| ~ spl0_148 ),
inference(avatar_contradiction_clause,[],[f3511]) ).
fof(f3514,plain,
( ~ c0_1(a926)
| ~ spl0_2
| spl0_88
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f2831,f591]) ).
fof(f3520,plain,
( spl0_99
| ~ spl0_10
| ~ spl0_20
| spl0_98 ),
inference(avatar_split_clause,[],[f1954,f639,f254,f217,f644]) ).
fof(f3523,plain,
( spl0_70
| ~ spl0_10
| spl0_69
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f2912,f708,f494,f217,f499]) ).
fof(f3527,plain,
( spl0_99
| ~ spl0_20
| spl0_97
| spl0_98 ),
inference(avatar_split_clause,[],[f2476,f639,f634,f254,f644]) ).
fof(f3543,plain,
( $false
| ~ spl0_2
| ~ spl0_5
| spl0_88
| ~ spl0_129
| ~ spl0_130 ),
inference(forward_subsumption_resolution,[],[f3514,f1622]) ).
fof(f3544,plain,
( ~ spl0_2
| ~ spl0_5
| spl0_88
| ~ spl0_129
| ~ spl0_130 ),
inference(avatar_contradiction_clause,[],[f3543]) ).
fof(f3558,plain,
( c3_1(a926)
| ~ spl0_2
| ~ spl0_12
| ~ spl0_13
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f3005,f933]) ).
fof(f3563,plain,
( ~ spl0_146
| ~ spl0_7
| ~ spl0_19
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f2212,f883,f250,f206,f878]) ).
fof(f3564,plain,
( $false
| ~ spl0_7
| ~ spl0_19
| ~ spl0_143
| ~ spl0_145 ),
inference(forward_subsumption_resolution,[],[f2242,f865]) ).
fof(f3565,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_143
| ~ spl0_145 ),
inference(avatar_contradiction_clause,[],[f3564]) ).
fof(f3569,plain,
( ~ c0_1(a942)
| ~ spl0_2
| ~ spl0_29
| ~ spl0_152
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f3301,f2845]) ).
fof(f3577,plain,
( $false
| ~ spl0_2
| ~ spl0_12
| ~ spl0_13
| spl0_88
| ~ spl0_129 ),
inference(forward_subsumption_resolution,[],[f3558,f591]) ).
fof(f3578,plain,
( ~ spl0_2
| ~ spl0_12
| ~ spl0_13
| spl0_88
| ~ spl0_129 ),
inference(avatar_contradiction_clause,[],[f3577]) ).
fof(f3581,plain,
( $false
| ~ spl0_2
| ~ spl0_29
| ~ spl0_152
| ~ spl0_154 ),
inference(forward_subsumption_resolution,[],[f3569,f920]) ).
fof(f3582,plain,
( ~ spl0_2
| ~ spl0_29
| ~ spl0_152
| ~ spl0_154 ),
inference(avatar_contradiction_clause,[],[f3581]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| ~ spl0_3
| spl0_4 ),
inference(sat_conversion,[],[f198]) ).
cnf(s2,plain,
( ~ spl0_3
| spl0_5
| spl0_6
| spl0_7 ),
inference(sat_conversion,[],[f208]) ).
cnf(s3,plain,
( spl0_2
| ~ spl0_3
| spl0_8
| spl0_9 ),
inference(sat_conversion,[],[f215]) ).
cnf(s4,plain,
( ~ spl0_3
| spl0_4
| spl0_8
| spl0_10 ),
inference(sat_conversion,[],[f219]) ).
cnf(s5,plain,
( ~ spl0_3
| spl0_5
| spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f226]) ).
cnf(s6,plain,
( ~ spl0_3
| spl0_8
| spl0_13
| spl0_14 ),
inference(sat_conversion,[],[f233]) ).
cnf(s7,plain,
( ~ spl0_3
| spl0_4
| spl0_15
| spl0_16 ),
inference(sat_conversion,[],[f241]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_11
| spl0_12
| spl0_20 ),
inference(sat_conversion,[],[f256]) ).
cnf(s11,plain,
( spl0_1
| ~ spl0_3
| spl0_19
| spl0_24 ),
inference(sat_conversion,[],[f272]) ).
cnf(s12,plain,
( ~ spl0_3
| spl0_25
| spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f283]) ).
cnf(s13,plain,
( ~ spl0_3
| spl0_14
| spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f291]) ).
cnf(s14,plain,
( ~ spl0_3
| spl0_4
| spl0_17
| spl0_30 ),
inference(sat_conversion,[],[f295]) ).
cnf(s15,plain,
( ~ spl0_3
| spl0_19
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f303]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_12
| spl0_23
| spl0_25 ),
inference(sat_conversion,[],[f304]) ).
cnf(s18,plain,
( spl0_1
| ~ spl0_3
| spl0_16
| spl0_34 ),
inference(sat_conversion,[],[f314]) ).
cnf(s19,plain,
( spl0_1
| ~ spl0_3
| spl0_26
| spl0_35 ),
inference(sat_conversion,[],[f319]) ).
cnf(s21,plain,
( ~ spl0_3
| spl0_13
| spl0_18
| spl0_31 ),
inference(sat_conversion,[],[f325]) ).
cnf(s22,plain,
( spl0_1
| ~ spl0_3
| spl0_7 ),
inference(sat_conversion,[],[f326]) ).
cnf(s23,plain,
( ~ spl0_3
| spl0_20
| spl0_37
| spl0_38 ),
inference(sat_conversion,[],[f334]) ).
cnf(s24,plain,
( ~ spl0_3
| spl0_8
| spl0_22
| spl0_25 ),
inference(sat_conversion,[],[f335]) ).
cnf(s25,plain,
( ~ spl0_3
| spl0_8
| spl0_35
| spl0_38 ),
inference(sat_conversion,[],[f336]) ).
cnf(s26,plain,
( ~ spl0_3
| spl0_20
| spl0_28
| spl0_30 ),
inference(sat_conversion,[],[f337]) ).
cnf(s27,plain,
( ~ spl0_3
| spl0_19
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f346]) ).
cnf(s28,plain,
( ~ spl0_3
| spl0_17
| spl0_29
| spl0_41 ),
inference(sat_conversion,[],[f351]) ).
cnf(s29,plain,
( ~ spl0_3
| spl0_9
| spl0_37
| spl0_42 ),
inference(sat_conversion,[],[f356]) ).
cnf(s31,plain,
( ~ spl0_3
| spl0_23
| spl0_35
| spl0_45 ),
inference(sat_conversion,[],[f370]) ).
cnf(s32,plain,
( ~ spl0_3
| spl0_7
| spl0_34
| spl0_46 ),
inference(sat_conversion,[],[f375]) ).
cnf(s33,plain,
( ~ spl0_3
| spl0_7
| spl0_21
| spl0_34 ),
inference(sat_conversion,[],[f376]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_22
| spl0_31
| spl0_47 ),
inference(sat_conversion,[],[f381]) ).
cnf(s37,plain,
( ~ spl0_3
| spl0_18
| spl0_45
| spl0_47 ),
inference(sat_conversion,[],[f388]) ).
cnf(s38,plain,
( ~ spl0_3
| spl0_18
| spl0_24
| spl0_49 ),
inference(sat_conversion,[],[f393]) ).
cnf(s39,plain,
( ~ spl0_3
| spl0_5
| spl0_47
| spl0_50 ),
inference(sat_conversion,[],[f398]) ).
cnf(s40,plain,
( ~ spl0_3
| spl0_5
| spl0_45
| spl0_51 ),
inference(sat_conversion,[],[f403]) ).
cnf(s41,plain,
( spl0_1
| ~ spl0_3
| spl0_28
| spl0_44 ),
inference(sat_conversion,[],[f404]) ).
cnf(s42,plain,
( ~ spl0_3
| spl0_12
| spl0_15
| spl0_41 ),
inference(sat_conversion,[],[f405]) ).
cnf(s43,plain,
( ~ spl0_3
| spl0_12
| spl0_50
| spl0_52 ),
inference(sat_conversion,[],[f410]) ).
cnf(s44,plain,
( ~ spl0_3
| spl0_16
| spl0_49 ),
inference(sat_conversion,[],[f411]) ).
cnf(s45,plain,
( ~ spl0_3
| spl0_14
| spl0_44
| spl0_47 ),
inference(sat_conversion,[],[f412]) ).
cnf(s48,plain,
( ~ spl0_3
| spl0_30
| spl0_39
| spl0_43 ),
inference(sat_conversion,[],[f426]) ).
cnf(s49,plain,
( ~ spl0_3
| spl0_13
| spl0_25
| spl0_56 ),
inference(sat_conversion,[],[f431]) ).
cnf(s50,plain,
( ~ spl0_3
| spl0_13
| spl0_39
| spl0_49 ),
inference(sat_conversion,[],[f432]) ).
cnf(s52,plain,
( ~ spl0_3
| spl0_32
| spl0_47
| spl0_52 ),
inference(sat_conversion,[],[f437]) ).
cnf(s53,plain,
( ~ spl0_3
| spl0_51
| spl0_58
| spl0_59 ),
inference(sat_conversion,[],[f445]) ).
cnf(s55,plain,
( ~ spl0_3
| spl0_35
| spl0_40
| spl0_60 ),
inference(sat_conversion,[],[f450]) ).
cnf(s56,plain,
( ~ spl0_3
| spl0_20
| spl0_35
| spl0_46 ),
inference(sat_conversion,[],[f451]) ).
cnf(s57,plain,
( ~ spl0_3
| spl0_8
| spl0_15
| spl0_56 ),
inference(sat_conversion,[],[f452]) ).
cnf(s58,plain,
( ~ spl0_25
| ~ spl0_61 ),
inference(sat_conversion,[],[f457]) ).
cnf(s59,plain,
( ~ spl0_25
| ~ spl0_62 ),
inference(sat_conversion,[],[f462]) ).
cnf(s60,plain,
( ~ spl0_25
| ~ spl0_63 ),
inference(sat_conversion,[],[f467]) ).
cnf(s61,plain,
( ~ spl0_15
| ~ spl0_64 ),
inference(sat_conversion,[],[f472]) ).
cnf(s62,plain,
( ~ spl0_56
| ~ spl0_65 ),
inference(sat_conversion,[],[f477]) ).
cnf(s63,plain,
( ~ spl0_56
| ~ spl0_66 ),
inference(sat_conversion,[],[f482]) ).
cnf(s64,plain,
( ~ spl0_51
| ~ spl0_67 ),
inference(sat_conversion,[],[f487]) ).
cnf(s65,plain,
( ~ spl0_51
| ~ spl0_68 ),
inference(sat_conversion,[],[f492]) ).
cnf(s66,plain,
( ~ spl0_58
| ~ spl0_69 ),
inference(sat_conversion,[],[f497]) ).
cnf(s67,plain,
( ~ spl0_58
| ~ spl0_70 ),
inference(sat_conversion,[],[f502]) ).
cnf(s68,plain,
( ~ spl0_31
| ~ spl0_71 ),
inference(sat_conversion,[],[f507]) ).
cnf(s69,plain,
( ~ spl0_52
| ~ spl0_72 ),
inference(sat_conversion,[],[f512]) ).
cnf(s70,plain,
( ~ spl0_47
| ~ spl0_73 ),
inference(sat_conversion,[],[f517]) ).
cnf(s71,plain,
( ~ spl0_47
| ~ spl0_74 ),
inference(sat_conversion,[],[f522]) ).
cnf(s72,plain,
( ~ spl0_37
| ~ spl0_75 ),
inference(sat_conversion,[],[f527]) ).
cnf(s74,plain,
( ~ spl0_28
| ~ spl0_77 ),
inference(sat_conversion,[],[f537]) ).
cnf(s75,plain,
( ~ spl0_28
| ~ spl0_78 ),
inference(sat_conversion,[],[f542]) ).
cnf(s76,plain,
( ~ spl0_46
| ~ spl0_79 ),
inference(sat_conversion,[],[f547]) ).
cnf(s77,plain,
( ~ spl0_40
| ~ spl0_80 ),
inference(sat_conversion,[],[f552]) ).
cnf(s78,plain,
( ~ spl0_39
| ~ spl0_81 ),
inference(sat_conversion,[],[f557]) ).
cnf(s79,plain,
( ~ spl0_45
| ~ spl0_82 ),
inference(sat_conversion,[],[f562]) ).
cnf(s80,plain,
( ~ spl0_45
| ~ spl0_83 ),
inference(sat_conversion,[],[f567]) ).
cnf(s81,plain,
( ~ spl0_50
| ~ spl0_84 ),
inference(sat_conversion,[],[f572]) ).
cnf(s82,plain,
( ~ spl0_50
| ~ spl0_85 ),
inference(sat_conversion,[],[f577]) ).
cnf(s84,plain,
( ~ spl0_17
| ~ spl0_87 ),
inference(sat_conversion,[],[f587]) ).
cnf(s85,plain,
( ~ spl0_24
| ~ spl0_88 ),
inference(sat_conversion,[],[f592]) ).
cnf(s86,plain,
( ~ spl0_43
| ~ spl0_89 ),
inference(sat_conversion,[],[f597]) ).
cnf(s87,plain,
( ~ spl0_43
| ~ spl0_90 ),
inference(sat_conversion,[],[f602]) ).
cnf(s88,plain,
( ~ spl0_43
| ~ spl0_91 ),
inference(sat_conversion,[],[f607]) ).
cnf(s92,plain,
( ~ spl0_42
| ~ spl0_95 ),
inference(sat_conversion,[],[f627]) ).
cnf(s93,plain,
( ~ spl0_42
| ~ spl0_96 ),
inference(sat_conversion,[],[f632]) ).
cnf(s94,plain,
( ~ spl0_34
| ~ spl0_97 ),
inference(sat_conversion,[],[f637]) ).
cnf(s95,plain,
( ~ spl0_34
| ~ spl0_98 ),
inference(sat_conversion,[],[f642]) ).
cnf(s96,plain,
( ~ spl0_34
| ~ spl0_99 ),
inference(sat_conversion,[],[f647]) ).
cnf(s98,plain,
( ~ spl0_41
| ~ spl0_101 ),
inference(sat_conversion,[],[f657]) ).
cnf(s102,plain,
( ~ spl0_21
| ~ spl0_105 ),
inference(sat_conversion,[],[f677]) ).
cnf(s103,plain,
( ~ spl0_106
| ~ spl0_107 ),
inference(sat_conversion,[],[f686]) ).
cnf(s104,plain,
( ~ spl0_15
| spl0_108 ),
inference(sat_conversion,[],[f691]) ).
cnf(s105,plain,
( ~ spl0_15
| spl0_109 ),
inference(sat_conversion,[],[f696]) ).
cnf(s106,plain,
( ~ spl0_56
| spl0_110 ),
inference(sat_conversion,[],[f701]) ).
cnf(s108,plain,
( ~ spl0_58
| spl0_112 ),
inference(sat_conversion,[],[f711]) ).
cnf(s110,plain,
( ~ spl0_31
| spl0_114 ),
inference(sat_conversion,[],[f721]) ).
cnf(s111,plain,
( ~ spl0_52
| spl0_115 ),
inference(sat_conversion,[],[f726]) ).
cnf(s112,plain,
( ~ spl0_52
| spl0_116 ),
inference(sat_conversion,[],[f731]) ).
cnf(s113,plain,
( ~ spl0_47
| spl0_117 ),
inference(sat_conversion,[],[f736]) ).
cnf(s114,plain,
( ~ spl0_37
| spl0_118 ),
inference(sat_conversion,[],[f741]) ).
cnf(s115,plain,
( ~ spl0_28
| spl0_119 ),
inference(sat_conversion,[],[f746]) ).
cnf(s116,plain,
( ~ spl0_46
| spl0_120 ),
inference(sat_conversion,[],[f751]) ).
cnf(s117,plain,
( ~ spl0_46
| spl0_121 ),
inference(sat_conversion,[],[f756]) ).
cnf(s118,plain,
( ~ spl0_40
| spl0_122 ),
inference(sat_conversion,[],[f761]) ).
cnf(s119,plain,
( ~ spl0_40
| spl0_123 ),
inference(sat_conversion,[],[f766]) ).
cnf(s120,plain,
( ~ spl0_39
| spl0_124 ),
inference(sat_conversion,[],[f771]) ).
cnf(s121,plain,
( ~ spl0_39
| spl0_125 ),
inference(sat_conversion,[],[f776]) ).
cnf(s122,plain,
( ~ spl0_45
| spl0_126 ),
inference(sat_conversion,[],[f781]) ).
cnf(s123,plain,
( ~ spl0_50
| spl0_127 ),
inference(sat_conversion,[],[f786]) ).
cnf(s124,plain,
( ~ spl0_17
| spl0_128 ),
inference(sat_conversion,[],[f791]) ).
cnf(s125,plain,
( ~ spl0_24
| spl0_129 ),
inference(sat_conversion,[],[f796]) ).
cnf(s126,plain,
( ~ spl0_24
| spl0_130 ),
inference(sat_conversion,[],[f801]) ).
cnf(s130,plain,
( ~ spl0_42
| spl0_134 ),
inference(sat_conversion,[],[f821]) ).
cnf(s133,plain,
( ~ spl0_41
| spl0_137 ),
inference(sat_conversion,[],[f836]) ).
cnf(s134,plain,
( ~ spl0_41
| spl0_138 ),
inference(sat_conversion,[],[f841]) ).
cnf(s136,plain,
( ~ spl0_21
| spl0_140 ),
inference(sat_conversion,[],[f851]) ).
cnf(s138,plain,
( ~ spl0_106
| spl0_142 ),
inference(sat_conversion,[],[f861]) ).
cnf(s139,plain,
( ~ spl0_35
| spl0_143 ),
inference(sat_conversion,[],[f866]) ).
cnf(s140,plain,
( ~ spl0_35
| spl0_144 ),
inference(sat_conversion,[],[f871]) ).
cnf(s141,plain,
( ~ spl0_35
| spl0_145 ),
inference(sat_conversion,[],[f876]) ).
cnf(s142,plain,
( ~ spl0_49
| spl0_146 ),
inference(sat_conversion,[],[f881]) ).
cnf(s143,plain,
( ~ spl0_49
| spl0_147 ),
inference(sat_conversion,[],[f886]) ).
cnf(s144,plain,
( ~ spl0_49
| spl0_148 ),
inference(sat_conversion,[],[f891]) ).
cnf(s148,plain,
( ~ spl0_44
| spl0_152 ),
inference(sat_conversion,[],[f911]) ).
cnf(s149,plain,
( ~ spl0_44
| spl0_153 ),
inference(sat_conversion,[],[f916]) ).
cnf(s150,plain,
( ~ spl0_44
| spl0_154 ),
inference(sat_conversion,[],[f921]) ).
cnf(s151,plain,
( spl0_34
| spl0_39
| spl0_45 ),
inference(sat_conversion,[],[f922]) ).
cnf(s152,plain,
( spl0_42
| spl0_50
| spl0_58 ),
inference(sat_conversion,[],[f923]) ).
cnf(s153,plain,
( spl0_31
| spl0_34
| spl0_106 ),
inference(sat_conversion,[],[f924]) ).
cnf(s155,plain,
( spl0_3
| ~ spl0_31 ),
inference(sat_conversion,[],[f926]) ).
cnf(s160,plain,
( spl0_3
| ~ spl0_34 ),
inference(sat_conversion,[],[f931]) ).
cnf(s161,plain,
( spl0_3
| ~ spl0_106 ),
inference(sat_conversion,[],[f932]) ).
cnf(s165,plain,
( ~ spl0_2
| ~ spl0_12
| spl0_71
| ~ spl0_114 ),
inference(sat_conversion,[],[f965]) ).
cnf(s167,plain,
( ~ spl0_14
| ~ spl0_16
| spl0_64
| ~ spl0_109 ),
inference(sat_conversion,[],[f970]) ).
cnf(s178,plain,
( ~ spl0_14
| ~ spl0_23
| spl0_65
| ~ spl0_110 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s185,plain,
( ~ spl0_14
| ~ spl0_16
| spl0_105
| ~ spl0_140 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s213,plain,
( ~ spl0_4
| ~ spl0_12
| ~ spl0_14
| ~ spl0_16
| spl0_66
| ~ spl0_110 ),
inference(sat_conversion,[],[f1191]) ).
cnf(s239,plain,
( ~ spl0_1
| ~ spl0_60
| spl0_97
| spl0_98 ),
inference(sat_conversion,[],[f1313]) ).
cnf(s242,plain,
( ~ spl0_13
| ~ spl0_20
| spl0_61
| spl0_63 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s298,plain,
( ~ spl0_7
| ~ spl0_8
| ~ spl0_14
| ~ spl0_16
| spl0_80
| ~ spl0_122 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s303,plain,
( ~ spl0_1
| ~ spl0_9
| spl0_75
| ~ spl0_118 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s319,plain,
( ~ spl0_10
| ~ spl0_22
| spl0_81
| ~ spl0_124 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s347,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_137
| ~ spl0_138 ),
inference(sat_conversion,[],[f1708]) ).
cnf(s353,plain,
( ~ spl0_10
| ~ spl0_22
| spl0_80
| ~ spl0_122 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s383,plain,
( ~ spl0_9
| ~ spl0_19
| ~ spl0_129
| ~ spl0_130 ),
inference(sat_conversion,[],[f1806]) ).
cnf(s385,plain,
( ~ spl0_9
| ~ spl0_19
| ~ spl0_152
| ~ spl0_153 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s406,plain,
( ~ spl0_10
| ~ spl0_18
| spl0_85
| ~ spl0_127 ),
inference(sat_conversion,[],[f1882]) ).
cnf(s414,plain,
( ~ spl0_1
| ~ spl0_7
| spl0_72
| ~ spl0_115 ),
inference(sat_conversion,[],[f1923]) ).
cnf(s429,plain,
( ~ spl0_10
| ~ spl0_20
| ~ spl0_59
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f1982]) ).
cnf(s438,plain,
( ~ spl0_12
| ~ spl0_20
| spl0_65
| spl0_66 ),
inference(sat_conversion,[],[f2008]) ).
cnf(s458,plain,
( ~ spl0_2
| ~ spl0_12
| spl0_65
| ~ spl0_110 ),
inference(sat_conversion,[],[f2084]) ).
cnf(s539,plain,
( ~ spl0_2
| ~ spl0_12
| spl0_95
| ~ spl0_134 ),
inference(sat_conversion,[],[f2316]) ).
cnf(s551,plain,
( ~ spl0_5
| spl0_79
| ~ spl0_120
| ~ spl0_121 ),
inference(sat_conversion,[],[f2346]) ).
cnf(s561,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_14
| spl0_71
| ~ spl0_114 ),
inference(sat_conversion,[],[f2395]) ).
cnf(s566,plain,
( ~ spl0_14
| spl0_95
| spl0_96
| ~ spl0_134 ),
inference(sat_conversion,[],[f2439]) ).
cnf(s569,plain,
( ~ spl0_32
| spl0_84
| spl0_85
| ~ spl0_127 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s605,plain,
( ~ spl0_27
| ~ spl0_30
| spl0_72
| ~ spl0_116 ),
inference(sat_conversion,[],[f2635]) ).
cnf(s611,plain,
( ~ spl0_1
| ~ spl0_8
| spl0_20 ),
inference(sat_conversion,[],[f2690]) ).
cnf(s627,plain,
( ~ spl0_4
| ~ spl0_23
| ~ spl0_115
| ~ spl0_116 ),
inference(sat_conversion,[],[f2781]) ).
cnf(s629,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_13
| spl0_75
| ~ spl0_118 ),
inference(sat_conversion,[],[f2791]) ).
cnf(s638,plain,
( ~ spl0_1
| spl0_73
| spl0_74
| ~ spl0_117 ),
inference(sat_conversion,[],[f2820]) ).
cnf(s640,plain,
( ~ spl0_2
| ~ spl0_11
| spl0_77
| spl0_78
| ~ spl0_119 ),
inference(sat_conversion,[],[f2849]) ).
cnf(s643,plain,
( ~ spl0_13
| ~ spl0_18
| spl0_79
| ~ spl0_120 ),
inference(sat_conversion,[],[f2860]) ).
cnf(s646,plain,
( ~ spl0_18
| ~ spl0_29
| ~ spl0_143
| ~ spl0_144 ),
inference(sat_conversion,[],[f2863]) ).
cnf(s650,plain,
( ~ spl0_8
| spl0_90
| spl0_91
| spl0_158 ),
inference(sat_conversion,[],[f2870]) ).
cnf(s660,plain,
( ~ spl0_1
| ~ spl0_9
| ~ spl0_38
| spl0_101
| ~ spl0_138 ),
inference(sat_conversion,[],[f2875]) ).
cnf(s662,plain,
( ~ spl0_27
| ~ spl0_30
| spl0_80
| ~ spl0_123 ),
inference(sat_conversion,[],[f2878]) ).
cnf(s676,plain,
( ~ spl0_12
| spl0_89
| spl0_90
| ~ spl0_158 ),
inference(sat_conversion,[],[f2892]) ).
cnf(s679,plain,
( ~ spl0_13
| ~ spl0_18
| spl0_87
| ~ spl0_128 ),
inference(sat_conversion,[],[f2910]) ).
cnf(s693,plain,
( ~ spl0_13
| spl0_82
| spl0_83
| ~ spl0_126 ),
inference(sat_conversion,[],[f3020]) ).
cnf(s696,plain,
( ~ spl0_2
| ~ spl0_12
| spl0_107
| ~ spl0_142 ),
inference(sat_conversion,[],[f3023]) ).
cnf(s718,plain,
( ~ spl0_12
| ~ spl0_22
| spl0_80
| ~ spl0_123 ),
inference(sat_conversion,[],[f3093]) ).
cnf(s721,plain,
( ~ spl0_12
| ~ spl0_20
| spl0_81
| spl0_124 ),
inference(sat_conversion,[],[f3107]) ).
cnf(s736,plain,
( ~ spl0_4
| ~ spl0_38
| ~ spl0_124
| ~ spl0_125 ),
inference(sat_conversion,[],[f3167]) ).
cnf(s741,plain,
( ~ spl0_6
| ~ spl0_12
| ~ spl0_20
| spl0_61
| spl0_62 ),
inference(sat_conversion,[],[f3196]) ).
cnf(s744,plain,
( ~ spl0_1
| ~ spl0_11
| spl0_20 ),
inference(sat_conversion,[],[f3205]) ).
cnf(s745,plain,
( ~ spl0_11
| spl0_61
| spl0_62
| spl0_63 ),
inference(sat_conversion,[],[f3207]) ).
cnf(s751,plain,
( ~ spl0_6
| spl0_77
| spl0_78
| ~ spl0_119 ),
inference(sat_conversion,[],[f3227]) ).
cnf(s759,plain,
( ~ spl0_23
| ~ spl0_29
| ~ spl0_152
| ~ spl0_153
| ~ spl0_154 ),
inference(sat_conversion,[],[f3342]) ).
cnf(s763,plain,
( ~ spl0_26
| spl0_64
| ~ spl0_108
| ~ spl0_109 ),
inference(sat_conversion,[],[f3365]) ).
cnf(s766,plain,
( ~ spl0_4
| ~ spl0_16
| ~ spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f3386]) ).
cnf(s788,plain,
( ~ spl0_7
| spl0_81
| ~ spl0_124
| ~ spl0_125 ),
inference(sat_conversion,[],[f3475]) ).
cnf(s795,plain,
( ~ spl0_8
| ~ spl0_30
| spl0_67
| spl0_68 ),
inference(sat_conversion,[],[f3497]) ).
cnf(s796,plain,
( ~ spl0_7
| ~ spl0_8
| spl0_10 ),
inference(sat_conversion,[],[f3505]) ).
cnf(s798,plain,
( ~ spl0_4
| ~ spl0_5
| ~ spl0_143
| ~ spl0_144
| ~ spl0_145 ),
inference(sat_conversion,[],[f3508]) ).
cnf(s800,plain,
( ~ spl0_4
| ~ spl0_146
| ~ spl0_147
| ~ spl0_148 ),
inference(sat_conversion,[],[f3512]) ).
cnf(s802,plain,
( ~ spl0_10
| ~ spl0_20
| spl0_98
| spl0_99 ),
inference(sat_conversion,[],[f3520]) ).
cnf(s805,plain,
( ~ spl0_10
| spl0_69
| spl0_70
| ~ spl0_112 ),
inference(sat_conversion,[],[f3523]) ).
cnf(s809,plain,
( ~ spl0_20
| spl0_97
| spl0_98
| spl0_99 ),
inference(sat_conversion,[],[f3527]) ).
cnf(s814,plain,
( ~ spl0_2
| ~ spl0_5
| spl0_88
| ~ spl0_129
| ~ spl0_130 ),
inference(sat_conversion,[],[f3544]) ).
cnf(s838,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_146
| ~ spl0_147 ),
inference(sat_conversion,[],[f3563]) ).
cnf(s839,plain,
( ~ spl0_7
| ~ spl0_19
| ~ spl0_143
| ~ spl0_145 ),
inference(sat_conversion,[],[f3565]) ).
cnf(s842,plain,
( ~ spl0_2
| ~ spl0_12
| ~ spl0_13
| spl0_88
| ~ spl0_129 ),
inference(sat_conversion,[],[f3578]) ).
cnf(s844,plain,
( ~ spl0_2
| ~ spl0_29
| ~ spl0_152
| ~ spl0_154 ),
inference(sat_conversion,[],[f3582]) ).
cnf(s846,plain,
spl0_3,
inference(rat,[],[s153,s155,s160,s161]) ).
cnf(s847,plain,
( ~ spl0_49
| ~ spl0_4 ),
inference(rat,[],[s800,s142,s143,s144]) ).
cnf(s848,plain,
( ~ spl0_15
| ~ spl0_14
| ~ spl0_16 ),
inference(rat,[],[s167,s61,s105]) ).
cnf(s849,plain,
( ~ spl0_14
| ~ spl0_12
| spl0_8
| ~ spl0_4 ),
inference(rat,[],[s213,s63,s106,s57,s848,s44,s847,s846]) ).
cnf(s850,plain,
( ~ spl0_40
| ~ spl0_4 ),
inference(rat,[],[s766,s118,s119,s44,s847,s846]) ).
cnf(s851,plain,
( ~ spl0_39
| ~ spl0_7 ),
inference(rat,[],[s788,s78,s120,s121]) ).
cnf(s852,plain,
( ~ spl0_15
| ~ spl0_26 ),
inference(rat,[],[s763,s61,s104,s105]) ).
cnf(s853,plain,
( ~ spl0_24
| ~ spl0_9
| ~ spl0_19 ),
inference(rat,[],[s383,s125,s126]) ).
cnf(s855,plain,
( spl0_81
| ~ spl0_12
| ~ spl0_22
| ~ spl0_20
| ~ spl0_10 ),
inference(rat,[],[s319,s721]) ).
cnf(s856,plain,
( ~ spl0_25
| ~ spl0_20
| ~ spl0_13 ),
inference(rat,[],[s242,s58,s60]) ).
cnf(s857,plain,
( ~ spl0_41
| ~ spl0_19
| ~ spl0_7 ),
inference(rat,[],[s347,s133,s134]) ).
cnf(s859,plain,
( ~ spl0_44
| ~ spl0_9
| ~ spl0_19 ),
inference(rat,[],[s385,s148,s149]) ).
cnf(s860,plain,
( ~ spl0_35
| ~ spl0_19
| ~ spl0_7 ),
inference(rat,[],[s839,s139,s141]) ).
cnf(s861,plain,
( ~ spl0_43
| ~ spl0_8
| ~ spl0_12 ),
inference(rat,[],[s676,s650,s86,s87,s88]) ).
cnf(s862,plain,
( ~ spl0_45
| ~ spl0_13 ),
inference(rat,[],[s693,s79,s80,s122]) ).
cnf(s863,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s48,s795,s861,s3,s853,s64,s65,s38,s40,s643,s551,s76,s116,s117,s56,s809,s94,s95,s96,s151,s862,s42,s852,s19,s860,s857,s50,s27,s850,s847,s1,s851,s22,s846]) ).
cnf(s864,plain,
( ~ spl0_4
| spl0_1 ),
inference(rat,[],[s842,s85,s125,s38,s643,s76,s116,s56,s42,s809,s852,s94,s95,s96,s19,s151,s860,s857,s862,s27,s50,s850,s847,s851,s22,s863,s846]) ).
cnf(s865,plain,
( ~ spl0_58
| ~ spl0_10 ),
inference(rat,[],[s805,s66,s67,s108]) ).
cnf(s866,plain,
( ~ spl0_50
| ~ spl0_18
| ~ spl0_10 ),
inference(rat,[],[s406,s82,s123]) ).
cnf(s867,plain,
( ~ spl0_42
| ~ spl0_12
| ~ spl0_2 ),
inference(rat,[],[s539,s92,s130]) ).
cnf(s868,plain,
( spl0_8
| spl0_19
| spl0_1 ),
inference(rat,[],[s165,s68,s110,s21,s866,s152,s867,s865,s842,s5,s745,s58,s59,s60,s24,s353,s4,s864,s118,s77,s27,s851,s22,s814,s85,s863,s125,s126,s11,s846]) ).
cnf(s869,plain,
( ~ spl0_12
| ~ spl0_10
| spl0_88
| ~ spl0_129
| ~ spl0_2 ),
inference(rat,[],[s165,s68,s110,s21,s866,s152,s867,s842,s865,s846]) ).
cnf(s870,plain,
( ~ spl0_28
| ~ spl0_11
| ~ spl0_2 ),
inference(rat,[],[s640,s74,s75,s115]) ).
cnf(s871,plain,
( ~ spl0_25
| ~ spl0_11 ),
inference(rat,[],[s745,s58,s59,s60]) ).
cnf(s872,plain,
( spl0_19
| spl0_1 ),
inference(rat,[],[s662,s26,s12,s802,s852,s95,s96,s7,s18,s298,s13,s844,s871,s148,s150,s41,s870,s5,s869,s796,s868,s814,s77,s118,s119,s85,s125,s126,s27,s11,s851,s22,s863,s864,s846]) ).
cnf(s873,plain,
( ~ spl0_56
| spl0_1 ),
inference(rat,[],[s458,s62,s106,s863,s42,s852,s19,s860,s857,s872,s22,s846]) ).
cnf(s874,plain,
( ~ spl0_49
| spl0_1 ),
inference(rat,[],[s838,s142,s143,s22,s872,s846]) ).
cnf(s875,plain,
spl0_1,
inference(rat,[],[s869,s85,s125,s38,s874,s866,s152,s865,s796,s57,s873,s867,s42,s852,s19,s860,s857,s872,s863,s22,s846]) ).
cnf(s877,plain,
( ~ spl0_31
| ~ spl0_2
| ~ spl0_12 ),
inference(rat,[],[s165,s68,s110]) ).
cnf(s878,plain,
( ~ spl0_50
| ~ spl0_32 ),
inference(rat,[],[s569,s81,s82,s123]) ).
cnf(s879,plain,
~ spl0_47,
inference(rat,[],[s638,s70,s71,s113,s875]) ).
cnf(s880,plain,
( ~ spl0_40
| ~ spl0_22
| ~ spl0_12 ),
inference(rat,[],[s718,s77,s119]) ).
cnf(s881,plain,
( ~ spl0_34
| ~ spl0_20 ),
inference(rat,[],[s809,s94,s95,s96]) ).
cnf(s882,plain,
( ~ spl0_106
| ~ spl0_2
| ~ spl0_12 ),
inference(rat,[],[s696,s103,s138]) ).
cnf(s883,plain,
( ~ spl0_2
| spl0_19
| ~ spl0_12 ),
inference(rat,[],[s798,s139,s140,s141,s4,s55,s611,s239,s881,s94,s95,s153,s882,s880,s865,s39,s152,s878,s34,s15,s877,s867,s846,s875,s879]) ).
cnf(s885,plain,
( ~ spl0_50
| ~ spl0_9
| spl0_8
| ~ spl0_10
| spl0_19 ),
inference(rat,[],[s561,s6,s68,s110,s862,s15,s37,s878,s866,s875,s846,s879]) ).
cnf(s886,plain,
( ~ spl0_17
| ~ spl0_13 ),
inference(rat,[],[s679,s84,s124,s37,s862,s879,s846]) ).
cnf(s887,plain,
( ~ spl0_37
| ~ spl0_9 ),
inference(rat,[],[s303,s72,s114,s875]) ).
cnf(s888,plain,
( ~ spl0_41
| ~ spl0_38
| ~ spl0_9 ),
inference(rat,[],[s660,s98,s134,s875]) ).
cnf(s889,plain,
( ~ spl0_29
| ~ spl0_152
| ~ spl0_153
| ~ spl0_154
| spl0_45 ),
inference(rat,[],[s646,s139,s140,s31,s759,s37,s846,s879]) ).
cnf(s890,plain,
( spl0_8
| ~ spl0_10
| spl0_19
| ~ spl0_12 ),
inference(rat,[],[s855,s78,s24,s151,s856,s881,s23,s888,s28,s889,s887,s886,s148,s149,s150,s862,s45,s6,s566,s92,s93,s130,s152,s885,s3,s883,s865,s846,s879]) ).
cnf(s891,plain,
( ~ spl0_25
| ~ spl0_6
| ~ spl0_20
| ~ spl0_12 ),
inference(rat,[],[s741,s58,s59]) ).
cnf(s892,plain,
( ~ spl0_56
| ~ spl0_20
| ~ spl0_12 ),
inference(rat,[],[s438,s62,s63]) ).
cnf(s893,plain,
( ~ spl0_25
| ~ spl0_8
| ~ spl0_10
| ~ spl0_12 ),
inference(rat,[],[s551,s76,s116,s117,s2,s32,s851,s48,s795,s64,s65,s53,s429,s891,s59,s60,s865,s861,s881,s611,s846,s875]) ).
cnf(s894,plain,
( ~ spl0_10
| spl0_19
| ~ spl0_12 ),
inference(rat,[],[s551,s76,s116,s117,s32,s39,s851,s866,s151,s37,s862,s49,s893,s892,s881,s611,s890,s875,s879,s846]) ).
cnf(s895,plain,
( spl0_8
| spl0_19
| ~ spl0_12 ),
inference(rat,[],[s2,s751,s798,s74,s75,s115,s139,s140,s141,s13,s25,s889,s736,s148,s149,s150,s862,s851,s120,s121,s45,s6,s27,s849,s850,s4,s894,s846,s879]) ).
cnf(s896,plain,
( spl0_19
| ~ spl0_12 ),
inference(rat,[],[s37,s643,s862,s49,s891,s2,s551,s76,s116,s117,s32,s892,s881,s611,s796,s895,s894,s875,s879,s846]) ).
cnf(s898,plain,
( ~ spl0_2
| spl0_13
| ~ spl0_10
| ~ spl0_12 ),
inference(rat,[],[s866,s21,s152,s877,s867,s865,s846]) ).
cnf(s899,plain,
( ~ spl0_42
| ~ spl0_14 ),
inference(rat,[],[s566,s92,s93,s130]) ).
cnf(s900,plain,
( spl0_13
| ~ spl0_10
| spl0_8
| ~ spl0_12 ),
inference(rat,[],[s561,s68,s110,s21,s866,s152,s899,s3,s898,s6,s865,s875,s846]) ).
cnf(s901,plain,
( ~ spl0_42
| spl0_8
| ~ spl0_12 ),
inference(rat,[],[s859,s45,s3,s899,s867,s896,s846,s879]) ).
cnf(s902,plain,
( ~ spl0_10
| spl0_8
| ~ spl0_12 ),
inference(rat,[],[s37,s866,s862,s152,s900,s865,s901,s846,s879]) ).
cnf(s903,plain,
( spl0_8
| ~ spl0_12 ),
inference(rat,[],[s629,s72,s114,s29,s3,s859,s45,s6,s849,s4,s902,s901,s896,s875,s846,s879]) ).
cnf(s904,plain,
( ~ spl0_10
| ~ spl0_12 ),
inference(rat,[],[s551,s76,s116,s117,s32,s39,s851,s866,s151,s37,s862,s49,s893,s881,s892,s611,s903,s846,s879,s875]) ).
cnf(s905,plain,
~ spl0_12,
inference(rat,[],[s37,s643,s862,s49,s891,s2,s551,s76,s116,s117,s32,s796,s904,s892,s881,s611,s903,s846,s879,s875]) ).
cnf(s910,plain,
spl0_20,
inference(rat,[],[s744,s9,s875,s846,s905]) ).
cnf(s911,plain,
~ spl0_34,
inference(rat,[],[s881,s910]) ).
cnf(s913,plain,
spl0_50,
inference(rat,[],[s551,s76,s116,s117,s32,s414,s69,s111,s39,s43,s911,s846,s875,s879,s905]) ).
cnf(s917,plain,
~ spl0_32,
inference(rat,[],[s878,s913]) ).
cnf(s918,plain,
spl0_52,
inference(rat,[],[s52,s879,s846,s917]) ).
cnf(s919,plain,
spl0_116,
inference(rat,[],[s112,s918]) ).
cnf(s920,plain,
spl0_115,
inference(rat,[],[s111,s918]) ).
cnf(s921,plain,
~ spl0_72,
inference(rat,[],[s69,s918]) ).
cnf(s923,plain,
~ spl0_7,
inference(rat,[],[s414,s920,s875,s921]) ).
cnf(s925,plain,
spl0_21,
inference(rat,[],[s33,s846,s911,s923]) ).
cnf(s926,plain,
spl0_46,
inference(rat,[],[s32,s846,s911,s923]) ).
cnf(s930,plain,
spl0_140,
inference(rat,[],[s136,s925]) ).
cnf(s932,plain,
~ spl0_105,
inference(rat,[],[s102,s925]) ).
cnf(s933,plain,
spl0_121,
inference(rat,[],[s117,s926]) ).
cnf(s934,plain,
spl0_120,
inference(rat,[],[s116,s926]) ).
cnf(s935,plain,
~ spl0_79,
inference(rat,[],[s76,s926]) ).
cnf(s936,plain,
~ spl0_5,
inference(rat,[],[s551,s935,s933,s934]) ).
cnf(s937,plain,
spl0_6,
inference(rat,[],[s2,s923,s846,s936]) ).
cnf(s938,plain,
spl0_11,
inference(rat,[],[s5,s905,s846,s936]) ).
cnf(s939,plain,
~ spl0_25,
inference(rat,[],[s871,s938]) ).
cnf(s940,plain,
spl0_23,
inference(rat,[],[s16,s905,s846,s939]) ).
cnf(s941,plain,
~ spl0_4,
inference(rat,[],[s627,s919,s920,s940]) ).
cnf(s942,plain,
~ spl0_28,
inference(rat,[],[s751,s74,s75,s115,s937]) ).
cnf(s943,plain,
spl0_14,
inference(rat,[],[s759,s148,s149,s150,s13,s45,s940,s846,s942,s879]) ).
cnf(s945,plain,
~ spl0_16,
inference(rat,[],[s185,s930,s932,s943]) ).
cnf(s947,plain,
spl0_15,
inference(rat,[],[s7,s846,s941,s945]) ).
cnf(s954,plain,
~ spl0_26,
inference(rat,[],[s852,s947]) ).
cnf(s956,plain,
spl0_27,
inference(rat,[],[s12,s939,s846,s954]) ).
cnf(s957,plain,
~ spl0_30,
inference(rat,[],[s605,s919,s921,s956]) ).
cnf(s958,plain,
spl0_17,
inference(rat,[],[s14,s941,s846,s957]) ).
cnf(s963,plain,
~ spl0_13,
inference(rat,[],[s886,s958]) ).
cnf(s967,plain,
spl0_56,
inference(rat,[],[s49,s939,s846,s963]) ).
cnf(s968,plain,
spl0_110,
inference(rat,[],[s106,s967]) ).
cnf(s970,plain,
~ spl0_65,
inference(rat,[],[s62,s967]) ).
cnf(s971,plain,
$false,
inference(rat,[],[s178,s940,s943,s968,s970]) ).
fof(f3586,plain,
$false,
inference(avatar_sat_refutation,[],[s971]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN455-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 % Computer : n009.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Mon Sep 28 16:06:00 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.25 Running first-order model finding
% 0.09/0.25 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.30 % (3189582)Will run a generic schedule for satisfiability detection.
% 0.09/0.30 % (3189591)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1014337396:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.09/0.30 % (3189588)% WARNING: option uhcvi not known.
% 0.09/0.30 % (3189589)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3933691016:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.09/0.30 % (3189587)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1085240208_2999 on theBenchmark for (2999ds/0Mi)
% 0.09/0.30 % (3189588)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1537551799:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.09/0.30 % (3189590)dis+10_1_sil=32000:sp=arity:random_seed=1166663071:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.09/0.30 % (3189592)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2614786215:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.09/0.30 % (3189593)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=343824185:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.09/0.30 % Detected minimum model sizes of [1]
% 0.09/0.30 % Detected maximum model sizes of [31]
% 0.09/0.30 % TRYING [1]
% 0.09/0.30 % TRYING [2]
% 0.09/0.30 % TRYING [3]
% 0.09/0.30 % (3189591) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3189582-3189591"...
% 0.09/0.30 % TRYING [4]
% 0.09/0.30 % (3189591)...printing done.
% 0.09/0.30 % (3189591)Refutation found. Thanks to Tanya!
% 0.09/0.30 % SZS status Unsatisfiable for theBenchmark
% 0.09/0.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.25/0.32 % (3189591)------------------------------
% 0.25/0.32 % (3189591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.25/0.32 % (3189591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.25/0.32 % (3189591)CaDiCaL version: 2.1.3
% 0.25/0.32 % (3189591)Termination reason: Refutation
% 0.25/0.32 % (3189591)Time elapsed: 0.031 s
% 0.25/0.32 % (3189591)Peak memory usage: 13 MB
% 0.25/0.32 % (3189591)Instructions burned: 88 (million)
% 0.25/0.32 % (3189582)Success in time 0.05 s
% 0.25/0.32 % Vampire exiting
%------------------------------------------------------------------------------