%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN466+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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:09:53 PM UTC 2026
% Result : Theorem 0.47s 0.30s
% Output : Refutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 129
% Syntax : Number of formulae : 933 ( 34 unt; 128 def)
% Number of atoms : 6548 ( 0 equ)
% Maximal formula atoms : 673 ( 7 avg)
% Number of connectives : 8489 (2874 ~;4200 |; 975 &)
% ( 128 <=>; 312 =>; 0 <=; 0 <~>)
% Maximal formula depth : 106 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 166 ( 165 usr; 162 prp; 0-1 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 765 ( 0 sgn 765 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ~ hskp0
| ( ndr1_0
& c2_1(a101)
& c3_1(a101)
& ~ c0_1(a101) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a102)
& ~ c0_1(a102)
& ~ c1_1(a102) ) )
& ( ~ hskp2
| ( ndr1_0
& c0_1(a103)
& c1_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a104)
& c2_1(a104)
& ~ c1_1(a104) ) )
& ( ~ hskp4
| ( ndr1_0
& c2_1(a105)
& c3_1(a105)
& ~ c1_1(a105) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a106)
& c1_1(a106)
& ~ c2_1(a106) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a107)
& c2_1(a107)
& ~ c0_1(a107) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a108)
& c3_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a109)
& ~ c0_1(a109)
& ~ c3_1(a109) ) )
& ( ~ hskp9
| ( ndr1_0
& c2_1(a110)
& ~ c1_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a111)
& ~ c2_1(a111)
& ~ c3_1(a111) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a112)
& ~ c2_1(a112)
& ~ c3_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a113)
& ~ c0_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a114)
& c2_1(a114)
& ~ c3_1(a114) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a116)
& c2_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp15
| ( ndr1_0
& c0_1(a117)
& c3_1(a117)
& ~ c1_1(a117) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a126)
& c3_1(a126)
& ~ c2_1(a126) ) )
& ( ~ hskp17
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c1_1(a132) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a134)
& c3_1(a134)
& ~ c2_1(a134) ) )
& ( ~ hskp19
| ( ndr1_0
& c0_1(a135)
& ~ c2_1(a135)
& ~ c3_1(a135) ) )
& ( ~ hskp20
| ( ndr1_0
& c0_1(a139)
& ~ c1_1(a139)
& ~ c3_1(a139) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a143)
& ~ c1_1(a143)
& ~ c2_1(a143) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c0_1(a145)
& ~ c1_1(a145)
& ~ c2_1(a145) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a153)
& ~ c1_1(a153)
& ~ c3_1(a153) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c1_1(a163)
& ~ c2_1(a163)
& ~ c3_1(a163) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a167)
& ~ c0_1(a167)
& ~ c2_1(a167) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a187)
& ~ c1_1(a187)
& ~ c2_1(a187) ) )
& ( ~ hskp27
| ( ndr1_0
& c2_1(a196)
& ~ c0_1(a196)
& ~ c3_1(a196) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a118)
& c2_1(a118)
& c3_1(a118) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& c2_1(a128) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a131)
& c2_1(a131)
& c3_1(a131) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a141)
& c1_1(a141)
& c3_1(a141) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c1_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| ~ c2_1(X6)
| ~ c3_1(X6) ) )
| hskp1 )
& ( ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c2_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8) ) )
| hskp2 )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| hskp3
| hskp4 )
& ( ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| c3_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c3_1(X12)
| ~ c0_1(X12)
| ~ c2_1(X12) ) ) )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| c3_1(X13) ) )
| hskp5 )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| hskp6
| hskp7 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| c3_1(X15) ) )
| hskp8
| hskp9 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| ~ c2_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( ~ c0_1(X17)
| ~ c1_1(X17)
| ~ c3_1(X17) ) )
| hskp10 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19) ) )
| ! [X20] :
( ndr1_0
=> ( ~ c0_1(X20)
| ~ c1_1(X20)
| ~ c3_1(X20) ) ) )
& ( ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21) ) )
| ! [X22] :
( ndr1_0
=> ( c1_1(X22)
| c2_1(X22)
| ~ c0_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c2_1(X23)
| ~ c0_1(X23)
| ~ c1_1(X23) ) ) )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c2_1(X25)
| c3_1(X25)
| ~ c1_1(X25) ) )
| hskp11 )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c1_1(X26)
| ~ c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c3_1(X27)
| ~ c0_1(X27)
| ~ c2_1(X27) ) )
| hskp12 )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c1_1(X28)
| ~ c3_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( ~ c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( ~ c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c2_1(X31)
| c3_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( ~ c0_1(X32)
| ~ c1_1(X32)
| ~ c3_1(X32) ) )
| hskp13 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| c2_1(X34)
| ~ c3_1(X34) ) )
| hskp6 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c1_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36) ) )
| hskp14 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37) ) )
| hskp15
| hskp28 )
& ( ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| c3_1(X38)
| ~ c1_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c1_1(X40)
| ~ c0_1(X40)
| ~ c3_1(X40) ) ) )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c3_1(X41)
| ~ c1_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c2_1(X42)
| c3_1(X42)
| ~ c0_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| ~ c1_1(X43)
| ~ c2_1(X43) ) ) )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| hskp8 )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46) ) )
| hskp15
| hskp10 )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c3_1(X47)
| ~ c2_1(X47) ) )
| hskp15
| hskp0 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48) ) )
| hskp2
| hskp7 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c1_1(X50)
| c2_1(X50)
| c3_1(X50) ) )
| hskp16 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| ~ c2_1(X51)
| ~ c3_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| ~ c0_1(X52)
| ~ c2_1(X52) ) )
| hskp10 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| ~ c2_1(X53)
| ~ c3_1(X53) ) )
| hskp29
| hskp11 )
& ( ! [X54] :
( ndr1_0
=> ( c1_1(X54)
| c2_1(X54)
| c3_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( c2_1(X55)
| c3_1(X55)
| ~ c0_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( ~ c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56) ) ) )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c1_1(X58)
| c2_1(X58)
| ~ c3_1(X58) ) )
| hskp16 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| ~ c0_1(X59) ) )
| ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60) ) )
| hskp30 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| ~ c0_1(X61) ) )
| ! [X62] :
( ndr1_0
=> ( c2_1(X62)
| ~ c0_1(X62)
| ~ c1_1(X62) ) )
| hskp17 )
& ( ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| c2_1(X63)
| ~ c0_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( ~ c0_1(X64)
| ~ c1_1(X64)
| ~ c2_1(X64) ) )
| hskp7 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c3_1(X65)
| ~ c0_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67) ) ) )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c3_1(X68)
| ~ c0_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c1_1(X69)
| ~ c2_1(X69) ) )
| hskp18 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70) ) )
| hskp19
| hskp17 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| c3_1(X71)
| ~ c2_1(X71) ) )
| hskp28
| hskp17 )
& ( ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72) ) )
| ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c0_1(X73)
| ~ c3_1(X73) ) )
| hskp20 )
& ( ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| ~ c0_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c0_1(X76)
| ~ c3_1(X76) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c2_1(X77) ) )
| ! [X78] :
( ndr1_0
=> ( c3_1(X78)
| ~ c0_1(X78)
| ~ c2_1(X78) ) )
| hskp17 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79) ) )
| ! [X80] :
( ndr1_0
=> ( ~ c0_1(X80)
| ~ c1_1(X80)
| ~ c2_1(X80) ) )
| hskp31 )
& ( ! [X81] :
( ndr1_0
=> ( c1_1(X81)
| ~ c0_1(X81)
| ~ c2_1(X81) ) )
| hskp29
| hskp21 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| ~ c0_1(X82)
| ~ c3_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( c1_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83) ) )
| hskp17 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85) ) )
| hskp22 )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| ~ c0_1(X86)
| ~ c3_1(X86) ) )
| hskp31
| hskp28 )
& ( ! [X87] :
( ndr1_0
=> ( c1_1(X87)
| ~ c0_1(X87)
| ~ c3_1(X87) ) )
| hskp15
| hskp28 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88) ) )
| hskp28
| hskp11 )
& ( ! [X89] :
( ndr1_0
=> ( c1_1(X89)
| ~ c0_1(X89)
| ~ c3_1(X89) ) )
| hskp4
| hskp23 )
& ( ! [X90] :
( ndr1_0
=> ( c1_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90) ) )
| hskp4
| hskp10 )
& ( ! [X91] :
( ndr1_0
=> ( c2_1(X91)
| c3_1(X91)
| ~ c0_1(X91) ) )
| hskp19
| hskp8 )
& ( ! [X92] :
( ndr1_0
=> ( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92) ) )
| hskp19 )
& ( ! [X93] :
( ndr1_0
=> ( c2_1(X93)
| ~ c0_1(X93)
| ~ c1_1(X93) ) )
| ! [X94] :
( ndr1_0
=> ( c3_1(X94)
| ~ c1_1(X94)
| ~ c2_1(X94) ) )
| hskp12 )
& ( ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| hskp29
| hskp4 )
& ( ! [X96] :
( ndr1_0
=> ( c2_1(X96)
| ~ c0_1(X96)
| ~ c1_1(X96) ) )
| hskp1
| hskp24 )
& ( ! [X97] :
( ndr1_0
=> ( c2_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97) ) )
| hskp6
| hskp16 )
& ( ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c1_1(X98)
| ~ c3_1(X98) ) )
| ! [X99] :
( ndr1_0
=> ( ~ c0_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99) ) )
| hskp1 )
& ( ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100) ) )
| hskp25
| hskp0 )
& ( ! [X101] :
( ndr1_0
=> ( c3_1(X101)
| ~ c1_1(X101)
| ~ c2_1(X101) ) )
| hskp13
| hskp4 )
& ( ! [X102] :
( ndr1_0
=> ( ~ c0_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102) ) )
| hskp19
| hskp11 )
& ( ! [X103] :
( ndr1_0
=> ( ~ c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103) ) )
| hskp25
| hskp0 )
& ( hskp31
| hskp30
| hskp24 )
& ( hskp5
| hskp15
| hskp13 )
& ( hskp5
| hskp16
| hskp25 )
& ( hskp5
| hskp4
| hskp9 )
& ( hskp26
| hskp7
| hskp0 )
& ( hskp26
| hskp11
| hskp4 )
& ( hskp25
| hskp8 )
& ( hskp25
| hskp27
| hskp24 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ~ ( ( ~ hskp0
| ( ndr1_0
& c2_1(a101)
& c3_1(a101)
& ~ c0_1(a101) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a102)
& ~ c0_1(a102)
& ~ c1_1(a102) ) )
& ( ~ hskp2
| ( ndr1_0
& c0_1(a103)
& c1_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a104)
& c2_1(a104)
& ~ c1_1(a104) ) )
& ( ~ hskp4
| ( ndr1_0
& c2_1(a105)
& c3_1(a105)
& ~ c1_1(a105) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a106)
& c1_1(a106)
& ~ c2_1(a106) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a107)
& c2_1(a107)
& ~ c0_1(a107) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a108)
& c3_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a109)
& ~ c0_1(a109)
& ~ c3_1(a109) ) )
& ( ~ hskp9
| ( ndr1_0
& c2_1(a110)
& ~ c1_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a111)
& ~ c2_1(a111)
& ~ c3_1(a111) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a112)
& ~ c2_1(a112)
& ~ c3_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a113)
& ~ c0_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a114)
& c2_1(a114)
& ~ c3_1(a114) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a116)
& c2_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp15
| ( ndr1_0
& c0_1(a117)
& c3_1(a117)
& ~ c1_1(a117) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a126)
& c3_1(a126)
& ~ c2_1(a126) ) )
& ( ~ hskp17
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c1_1(a132) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a134)
& c3_1(a134)
& ~ c2_1(a134) ) )
& ( ~ hskp19
| ( ndr1_0
& c0_1(a135)
& ~ c2_1(a135)
& ~ c3_1(a135) ) )
& ( ~ hskp20
| ( ndr1_0
& c0_1(a139)
& ~ c1_1(a139)
& ~ c3_1(a139) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a143)
& ~ c1_1(a143)
& ~ c2_1(a143) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c0_1(a145)
& ~ c1_1(a145)
& ~ c2_1(a145) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a153)
& ~ c1_1(a153)
& ~ c3_1(a153) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c1_1(a163)
& ~ c2_1(a163)
& ~ c3_1(a163) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a167)
& ~ c0_1(a167)
& ~ c2_1(a167) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a187)
& ~ c1_1(a187)
& ~ c2_1(a187) ) )
& ( ~ hskp27
| ( ndr1_0
& c2_1(a196)
& ~ c0_1(a196)
& ~ c3_1(a196) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a118)
& c2_1(a118)
& c3_1(a118) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& c2_1(a128) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a131)
& c2_1(a131)
& c3_1(a131) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a141)
& c1_1(a141)
& c3_1(a141) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c1_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| ~ c2_1(X6)
| ~ c3_1(X6) ) )
| hskp1 )
& ( ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c2_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8) ) )
| hskp2 )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| hskp3
| hskp4 )
& ( ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| c3_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c3_1(X12)
| ~ c0_1(X12)
| ~ c2_1(X12) ) ) )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| c3_1(X13) ) )
| hskp5 )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| hskp6
| hskp7 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| c3_1(X15) ) )
| hskp8
| hskp9 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| ~ c2_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( ~ c0_1(X17)
| ~ c1_1(X17)
| ~ c3_1(X17) ) )
| hskp10 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19) ) )
| ! [X20] :
( ndr1_0
=> ( ~ c0_1(X20)
| ~ c1_1(X20)
| ~ c3_1(X20) ) ) )
& ( ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21) ) )
| ! [X22] :
( ndr1_0
=> ( c1_1(X22)
| c2_1(X22)
| ~ c0_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c2_1(X23)
| ~ c0_1(X23)
| ~ c1_1(X23) ) ) )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c2_1(X25)
| c3_1(X25)
| ~ c1_1(X25) ) )
| hskp11 )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c1_1(X26)
| ~ c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c3_1(X27)
| ~ c0_1(X27)
| ~ c2_1(X27) ) )
| hskp12 )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c1_1(X28)
| ~ c3_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( ~ c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( ~ c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c2_1(X31)
| c3_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( ~ c0_1(X32)
| ~ c1_1(X32)
| ~ c3_1(X32) ) )
| hskp13 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| c2_1(X34)
| ~ c3_1(X34) ) )
| hskp6 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c1_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36) ) )
| hskp14 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37) ) )
| hskp15
| hskp28 )
& ( ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| c3_1(X38)
| ~ c1_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c1_1(X40)
| ~ c0_1(X40)
| ~ c3_1(X40) ) ) )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c3_1(X41)
| ~ c1_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c2_1(X42)
| c3_1(X42)
| ~ c0_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| ~ c1_1(X43)
| ~ c2_1(X43) ) ) )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| hskp8 )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46) ) )
| hskp15
| hskp10 )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c3_1(X47)
| ~ c2_1(X47) ) )
| hskp15
| hskp0 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48) ) )
| hskp2
| hskp7 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c1_1(X50)
| c2_1(X50)
| c3_1(X50) ) )
| hskp16 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| ~ c2_1(X51)
| ~ c3_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| ~ c0_1(X52)
| ~ c2_1(X52) ) )
| hskp10 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| ~ c2_1(X53)
| ~ c3_1(X53) ) )
| hskp29
| hskp11 )
& ( ! [X54] :
( ndr1_0
=> ( c1_1(X54)
| c2_1(X54)
| c3_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( c2_1(X55)
| c3_1(X55)
| ~ c0_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( ~ c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56) ) ) )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c1_1(X58)
| c2_1(X58)
| ~ c3_1(X58) ) )
| hskp16 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| ~ c0_1(X59) ) )
| ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60) ) )
| hskp30 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| ~ c0_1(X61) ) )
| ! [X62] :
( ndr1_0
=> ( c2_1(X62)
| ~ c0_1(X62)
| ~ c1_1(X62) ) )
| hskp17 )
& ( ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| c2_1(X63)
| ~ c0_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( ~ c0_1(X64)
| ~ c1_1(X64)
| ~ c2_1(X64) ) )
| hskp7 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c3_1(X65)
| ~ c0_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67) ) ) )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c3_1(X68)
| ~ c0_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c1_1(X69)
| ~ c2_1(X69) ) )
| hskp18 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70) ) )
| hskp19
| hskp17 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| c3_1(X71)
| ~ c2_1(X71) ) )
| hskp28
| hskp17 )
& ( ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72) ) )
| ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c0_1(X73)
| ~ c3_1(X73) ) )
| hskp20 )
& ( ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| ~ c0_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c0_1(X76)
| ~ c3_1(X76) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c2_1(X77) ) )
| ! [X78] :
( ndr1_0
=> ( c3_1(X78)
| ~ c0_1(X78)
| ~ c2_1(X78) ) )
| hskp17 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79) ) )
| ! [X80] :
( ndr1_0
=> ( ~ c0_1(X80)
| ~ c1_1(X80)
| ~ c2_1(X80) ) )
| hskp31 )
& ( ! [X81] :
( ndr1_0
=> ( c1_1(X81)
| ~ c0_1(X81)
| ~ c2_1(X81) ) )
| hskp29
| hskp21 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| ~ c0_1(X82)
| ~ c3_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( c1_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83) ) )
| hskp17 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85) ) )
| hskp22 )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| ~ c0_1(X86)
| ~ c3_1(X86) ) )
| hskp31
| hskp28 )
& ( ! [X87] :
( ndr1_0
=> ( c1_1(X87)
| ~ c0_1(X87)
| ~ c3_1(X87) ) )
| hskp15
| hskp28 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88) ) )
| hskp28
| hskp11 )
& ( ! [X89] :
( ndr1_0
=> ( c1_1(X89)
| ~ c0_1(X89)
| ~ c3_1(X89) ) )
| hskp4
| hskp23 )
& ( ! [X90] :
( ndr1_0
=> ( c1_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90) ) )
| hskp4
| hskp10 )
& ( ! [X91] :
( ndr1_0
=> ( c2_1(X91)
| c3_1(X91)
| ~ c0_1(X91) ) )
| hskp19
| hskp8 )
& ( ! [X92] :
( ndr1_0
=> ( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92) ) )
| hskp19 )
& ( ! [X93] :
( ndr1_0
=> ( c2_1(X93)
| ~ c0_1(X93)
| ~ c1_1(X93) ) )
| ! [X94] :
( ndr1_0
=> ( c3_1(X94)
| ~ c1_1(X94)
| ~ c2_1(X94) ) )
| hskp12 )
& ( ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| hskp29
| hskp4 )
& ( ! [X96] :
( ndr1_0
=> ( c2_1(X96)
| ~ c0_1(X96)
| ~ c1_1(X96) ) )
| hskp1
| hskp24 )
& ( ! [X97] :
( ndr1_0
=> ( c2_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97) ) )
| hskp6
| hskp16 )
& ( ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c1_1(X98)
| ~ c3_1(X98) ) )
| ! [X99] :
( ndr1_0
=> ( ~ c0_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99) ) )
| hskp1 )
& ( ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100) ) )
| hskp25
| hskp0 )
& ( ! [X101] :
( ndr1_0
=> ( c3_1(X101)
| ~ c1_1(X101)
| ~ c2_1(X101) ) )
| hskp13
| hskp4 )
& ( ! [X102] :
( ndr1_0
=> ( ~ c0_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102) ) )
| hskp19
| hskp11 )
& ( ! [X103] :
( ndr1_0
=> ( ~ c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103) ) )
| hskp25
| hskp0 )
& ( hskp31
| hskp30
| hskp24 )
& ( hskp5
| hskp15
| hskp13 )
& ( hskp5
| hskp16
| hskp25 )
& ( hskp5
| hskp4
| hskp9 )
& ( hskp26
| hskp7
| hskp0 )
& ( hskp26
| hskp11
| hskp4 )
& ( hskp25
| hskp8 )
& ( hskp25
| hskp27
| hskp24 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ~ hskp0
| ( ndr1_0
& c2_1(a101)
& c3_1(a101)
& ~ c0_1(a101) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a102)
& ~ c0_1(a102)
& ~ c1_1(a102) ) )
& ( ~ hskp2
| ( ndr1_0
& c0_1(a103)
& c1_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a104)
& c2_1(a104)
& ~ c1_1(a104) ) )
& ( ~ hskp4
| ( ndr1_0
& c2_1(a105)
& c3_1(a105)
& ~ c1_1(a105) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a106)
& c1_1(a106)
& ~ c2_1(a106) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a107)
& c2_1(a107)
& ~ c0_1(a107) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a108)
& c3_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a109)
& ~ c0_1(a109)
& ~ c3_1(a109) ) )
& ( ~ hskp9
| ( ndr1_0
& c2_1(a110)
& ~ c1_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a111)
& ~ c2_1(a111)
& ~ c3_1(a111) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a112)
& ~ c2_1(a112)
& ~ c3_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a113)
& ~ c0_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a114)
& c2_1(a114)
& ~ c3_1(a114) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a116)
& c2_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp15
| ( ndr1_0
& c0_1(a117)
& c3_1(a117)
& ~ c1_1(a117) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a126)
& c3_1(a126)
& ~ c2_1(a126) ) )
& ( ~ hskp17
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c1_1(a132) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a134)
& c3_1(a134)
& ~ c2_1(a134) ) )
& ( ~ hskp19
| ( ndr1_0
& c0_1(a135)
& ~ c2_1(a135)
& ~ c3_1(a135) ) )
& ( ~ hskp20
| ( ndr1_0
& c0_1(a139)
& ~ c1_1(a139)
& ~ c3_1(a139) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a143)
& ~ c1_1(a143)
& ~ c2_1(a143) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c0_1(a145)
& ~ c1_1(a145)
& ~ c2_1(a145) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a153)
& ~ c1_1(a153)
& ~ c3_1(a153) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c1_1(a163)
& ~ c2_1(a163)
& ~ c3_1(a163) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a167)
& ~ c0_1(a167)
& ~ c2_1(a167) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a187)
& ~ c1_1(a187)
& ~ c2_1(a187) ) )
& ( ~ hskp27
| ( ndr1_0
& c2_1(a196)
& ~ c0_1(a196)
& ~ c3_1(a196) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a118)
& c2_1(a118)
& c3_1(a118) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& c2_1(a128) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a131)
& c2_1(a131)
& c3_1(a131) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a141)
& c1_1(a141)
& c3_1(a141) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c1_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| ~ c2_1(X6)
| ~ c3_1(X6) ) )
| hskp1 )
& ( ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c2_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8) ) )
| hskp2 )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| hskp3
| hskp4 )
& ( ! [X10] :
( ndr1_0
=> ( c0_1(X10)
| c1_1(X10)
| c3_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c3_1(X12)
| ~ c0_1(X12)
| ~ c2_1(X12) ) ) )
& ( ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c1_1(X13)
| c3_1(X13) ) )
| hskp5 )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| hskp6
| hskp7 )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| c3_1(X15) ) )
| hskp8
| hskp9 )
& ( ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| c1_1(X16)
| ~ c2_1(X16) ) )
| ! [X17] :
( ndr1_0
=> ( ~ c0_1(X17)
| ~ c1_1(X17)
| ~ c3_1(X17) ) )
| hskp10 )
& ( ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19) ) )
| ! [X20] :
( ndr1_0
=> ( ~ c0_1(X20)
| ~ c1_1(X20)
| ~ c3_1(X20) ) ) )
& ( ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21) ) )
| ! [X22] :
( ndr1_0
=> ( c1_1(X22)
| c2_1(X22)
| ~ c0_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c2_1(X23)
| ~ c0_1(X23)
| ~ c1_1(X23) ) ) )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24) ) )
| ! [X25] :
( ndr1_0
=> ( c2_1(X25)
| c3_1(X25)
| ~ c1_1(X25) ) )
| hskp11 )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c1_1(X26)
| ~ c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c3_1(X27)
| ~ c0_1(X27)
| ~ c2_1(X27) ) )
| hskp12 )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c1_1(X28)
| ~ c3_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( ~ c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( ~ c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c2_1(X31)
| c3_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( ~ c0_1(X32)
| ~ c1_1(X32)
| ~ c3_1(X32) ) )
| hskp13 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| c2_1(X34)
| ~ c3_1(X34) ) )
| hskp6 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c1_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36) ) )
| hskp14 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37) ) )
| hskp15
| hskp28 )
& ( ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| c3_1(X38)
| ~ c1_1(X38) ) )
| ! [X39] :
( ndr1_0
=> ( c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c1_1(X40)
| ~ c0_1(X40)
| ~ c3_1(X40) ) ) )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c3_1(X41)
| ~ c1_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c2_1(X42)
| c3_1(X42)
| ~ c0_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c3_1(X43)
| ~ c1_1(X43)
| ~ c2_1(X43) ) ) )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| hskp8 )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46) ) )
| hskp15
| hskp10 )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c3_1(X47)
| ~ c2_1(X47) ) )
| hskp15
| hskp0 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48) ) )
| hskp2
| hskp7 )
& ( ! [X49] :
( ndr1_0
=> ( c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49) ) )
| ! [X50] :
( ndr1_0
=> ( c1_1(X50)
| c2_1(X50)
| c3_1(X50) ) )
| hskp16 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| ~ c2_1(X51)
| ~ c3_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c3_1(X52)
| ~ c0_1(X52)
| ~ c2_1(X52) ) )
| hskp10 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| ~ c2_1(X53)
| ~ c3_1(X53) ) )
| hskp29
| hskp11 )
& ( ! [X54] :
( ndr1_0
=> ( c1_1(X54)
| c2_1(X54)
| c3_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( c2_1(X55)
| c3_1(X55)
| ~ c0_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( ~ c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56) ) ) )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c1_1(X58)
| c2_1(X58)
| ~ c3_1(X58) ) )
| hskp16 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| ~ c0_1(X59) ) )
| ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60) ) )
| hskp30 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| ~ c0_1(X61) ) )
| ! [X62] :
( ndr1_0
=> ( c2_1(X62)
| ~ c0_1(X62)
| ~ c1_1(X62) ) )
| hskp17 )
& ( ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| c2_1(X63)
| ~ c0_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( ~ c0_1(X64)
| ~ c1_1(X64)
| ~ c2_1(X64) ) )
| hskp7 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c3_1(X65)
| ~ c0_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( ~ c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67) ) ) )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c3_1(X68)
| ~ c0_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c1_1(X69)
| ~ c2_1(X69) ) )
| hskp18 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70) ) )
| hskp19
| hskp17 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| c3_1(X71)
| ~ c2_1(X71) ) )
| hskp28
| hskp17 )
& ( ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72) ) )
| ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c0_1(X73)
| ~ c3_1(X73) ) )
| hskp20 )
& ( ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| ~ c0_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c0_1(X76)
| ~ c3_1(X76) ) ) )
& ( ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c2_1(X77) ) )
| ! [X78] :
( ndr1_0
=> ( c3_1(X78)
| ~ c0_1(X78)
| ~ c2_1(X78) ) )
| hskp17 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79) ) )
| ! [X80] :
( ndr1_0
=> ( ~ c0_1(X80)
| ~ c1_1(X80)
| ~ c2_1(X80) ) )
| hskp31 )
& ( ! [X81] :
( ndr1_0
=> ( c1_1(X81)
| ~ c0_1(X81)
| ~ c2_1(X81) ) )
| hskp29
| hskp21 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| ~ c0_1(X82)
| ~ c3_1(X82) ) )
| ! [X83] :
( ndr1_0
=> ( c1_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83) ) )
| hskp17 )
& ( ! [X84] :
( ndr1_0
=> ( c1_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85) ) )
| hskp22 )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| ~ c0_1(X86)
| ~ c3_1(X86) ) )
| hskp31
| hskp28 )
& ( ! [X87] :
( ndr1_0
=> ( c1_1(X87)
| ~ c0_1(X87)
| ~ c3_1(X87) ) )
| hskp15
| hskp28 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88) ) )
| hskp28
| hskp11 )
& ( ! [X89] :
( ndr1_0
=> ( c1_1(X89)
| ~ c0_1(X89)
| ~ c3_1(X89) ) )
| hskp4
| hskp23 )
& ( ! [X90] :
( ndr1_0
=> ( c1_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90) ) )
| hskp4
| hskp10 )
& ( ! [X91] :
( ndr1_0
=> ( c2_1(X91)
| c3_1(X91)
| ~ c0_1(X91) ) )
| hskp19
| hskp8 )
& ( ! [X92] :
( ndr1_0
=> ( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92) ) )
| hskp19 )
& ( ! [X93] :
( ndr1_0
=> ( c2_1(X93)
| ~ c0_1(X93)
| ~ c1_1(X93) ) )
| ! [X94] :
( ndr1_0
=> ( c3_1(X94)
| ~ c1_1(X94)
| ~ c2_1(X94) ) )
| hskp12 )
& ( ! [X95] :
( ndr1_0
=> ( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95) ) )
| hskp29
| hskp4 )
& ( ! [X96] :
( ndr1_0
=> ( c2_1(X96)
| ~ c0_1(X96)
| ~ c1_1(X96) ) )
| hskp1
| hskp24 )
& ( ! [X97] :
( ndr1_0
=> ( c2_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97) ) )
| hskp6
| hskp16 )
& ( ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c1_1(X98)
| ~ c3_1(X98) ) )
| ! [X99] :
( ndr1_0
=> ( ~ c0_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99) ) )
| hskp1 )
& ( ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100) ) )
| hskp25
| hskp0 )
& ( ! [X101] :
( ndr1_0
=> ( c3_1(X101)
| ~ c1_1(X101)
| ~ c2_1(X101) ) )
| hskp13
| hskp4 )
& ( ! [X102] :
( ndr1_0
=> ( ~ c0_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102) ) )
| hskp19
| hskp11 )
& ( ! [X103] :
( ndr1_0
=> ( ~ c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103) ) )
| hskp25
| hskp0 )
& ( hskp31
| hskp30
| hskp24 )
& ( hskp5
| hskp15
| hskp13 )
& ( hskp5
| hskp16
| hskp25 )
& ( hskp5
| hskp4
| hskp9 )
& ( hskp26
| hskp7
| hskp0 )
& ( hskp26
| hskp11
| hskp4 )
& ( hskp25
| hskp8 )
& ( hskp25
| hskp27
| hskp24 ) ),
inference(flattening,[],[f2]) ).
fof(f4,plain,
( ( ~ hskp0
| ( ndr1_0
& c2_1(a101)
& c3_1(a101)
& ~ c0_1(a101) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a102)
& ~ c0_1(a102)
& ~ c1_1(a102) ) )
& ( ~ hskp2
| ( ndr1_0
& c0_1(a103)
& c1_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a104)
& c2_1(a104)
& ~ c1_1(a104) ) )
& ( ~ hskp4
| ( ndr1_0
& c2_1(a105)
& c3_1(a105)
& ~ c1_1(a105) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a106)
& c1_1(a106)
& ~ c2_1(a106) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a107)
& c2_1(a107)
& ~ c0_1(a107) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a108)
& c3_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a109)
& ~ c0_1(a109)
& ~ c3_1(a109) ) )
& ( ~ hskp9
| ( ndr1_0
& c2_1(a110)
& ~ c1_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a111)
& ~ c2_1(a111)
& ~ c3_1(a111) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a112)
& ~ c2_1(a112)
& ~ c3_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a113)
& ~ c0_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a114)
& c2_1(a114)
& ~ c3_1(a114) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a116)
& c2_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp15
| ( ndr1_0
& c0_1(a117)
& c3_1(a117)
& ~ c1_1(a117) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a126)
& c3_1(a126)
& ~ c2_1(a126) ) )
& ( ~ hskp17
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c1_1(a132) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a134)
& c3_1(a134)
& ~ c2_1(a134) ) )
& ( ~ hskp19
| ( ndr1_0
& c0_1(a135)
& ~ c2_1(a135)
& ~ c3_1(a135) ) )
& ( ~ hskp20
| ( ndr1_0
& c0_1(a139)
& ~ c1_1(a139)
& ~ c3_1(a139) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a143)
& ~ c1_1(a143)
& ~ c2_1(a143) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c0_1(a145)
& ~ c1_1(a145)
& ~ c2_1(a145) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a153)
& ~ c1_1(a153)
& ~ c3_1(a153) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c1_1(a163)
& ~ c2_1(a163)
& ~ c3_1(a163) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a167)
& ~ c0_1(a167)
& ~ c2_1(a167) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a187)
& ~ c1_1(a187)
& ~ c2_1(a187) ) )
& ( ~ hskp27
| ( ndr1_0
& c2_1(a196)
& ~ c0_1(a196)
& ~ c3_1(a196) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a118)
& c2_1(a118)
& c3_1(a118) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& c2_1(a128) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a131)
& c2_1(a131)
& c3_1(a131) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a141)
& c1_1(a141)
& c3_1(a141) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c0_1(X4)
| c1_1(X4)
| ~ c3_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| ! [X6] :
( c0_1(X6)
| ~ c2_1(X6)
| ~ c3_1(X6)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X7] :
( c0_1(X7)
| c1_1(X7)
| c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c2_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8)
| ~ ndr1_0 )
| hskp2 )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0 )
| hskp3
| hskp4 )
& ( ! [X10] :
( c0_1(X10)
| c1_1(X10)
| c3_1(X10)
| ~ ndr1_0 )
| ! [X11] :
( c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c3_1(X12)
| ~ c0_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 ) )
& ( ! [X13] :
( c0_1(X13)
| c1_1(X13)
| c3_1(X13)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X14] :
( c0_1(X14)
| c1_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| hskp6
| hskp7 )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| c3_1(X15)
| ~ ndr1_0 )
| hskp8
| hskp9 )
& ( ! [X16] :
( c0_1(X16)
| c1_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 )
| ! [X17] :
( ~ c0_1(X17)
| ~ c1_1(X17)
| ~ c3_1(X17)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19)
| ~ ndr1_0 )
| ! [X20] :
( ~ c0_1(X20)
| ~ c1_1(X20)
| ~ c3_1(X20)
| ~ ndr1_0 ) )
& ( ! [X21] :
( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| ! [X22] :
( c1_1(X22)
| c2_1(X22)
| ~ c0_1(X22)
| ~ ndr1_0 )
| ! [X23] :
( c2_1(X23)
| ~ c0_1(X23)
| ~ c1_1(X23)
| ~ ndr1_0 ) )
& ( ! [X24] :
( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( c2_1(X25)
| c3_1(X25)
| ~ c1_1(X25)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X26] :
( c0_1(X26)
| c1_1(X26)
| ~ c3_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c3_1(X27)
| ~ c0_1(X27)
| ~ c2_1(X27)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X28] :
( c0_1(X28)
| c1_1(X28)
| ~ c3_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( ~ c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( ~ c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 ) )
& ( ! [X31] :
( c0_1(X31)
| c2_1(X31)
| c3_1(X31)
| ~ ndr1_0 )
| ! [X32] :
( ~ c0_1(X32)
| ~ c1_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X33] :
( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c1_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0 )
| hskp15
| hskp28 )
& ( ! [X38] :
( c0_1(X38)
| c3_1(X38)
| ~ c1_1(X38)
| ~ ndr1_0 )
| ! [X39] :
( c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39)
| ~ ndr1_0 )
| ! [X40] :
( c1_1(X40)
| ~ c0_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0 ) )
& ( ! [X41] :
( c0_1(X41)
| c3_1(X41)
| ~ c1_1(X41)
| ~ ndr1_0 )
| ! [X42] :
( c2_1(X42)
| c3_1(X42)
| ~ c0_1(X42)
| ~ ndr1_0 )
| ! [X43] :
( c3_1(X43)
| ~ c1_1(X43)
| ~ c2_1(X43)
| ~ ndr1_0 ) )
& ( ! [X44] :
( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( ~ c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X46] :
( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0 )
| hskp15
| hskp10 )
& ( ! [X47] :
( c0_1(X47)
| c3_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0 )
| hskp15
| hskp0 )
& ( ! [X48] :
( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0 )
| hskp2
| hskp7 )
& ( ! [X49] :
( c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49)
| ~ ndr1_0 )
| ! [X50] :
( c1_1(X50)
| c2_1(X50)
| c3_1(X50)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X51] :
( c0_1(X51)
| ~ c2_1(X51)
| ~ c3_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c3_1(X52)
| ~ c0_1(X52)
| ~ c2_1(X52)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X53] :
( c0_1(X53)
| ~ c2_1(X53)
| ~ c3_1(X53)
| ~ ndr1_0 )
| hskp29
| hskp11 )
& ( ! [X54] :
( c1_1(X54)
| c2_1(X54)
| c3_1(X54)
| ~ ndr1_0 )
| ! [X55] :
( c2_1(X55)
| c3_1(X55)
| ~ c0_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( ~ c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56)
| ~ ndr1_0 ) )
& ( ! [X57] :
( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c1_1(X58)
| c2_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X59] :
( c1_1(X59)
| c2_1(X59)
| ~ c0_1(X59)
| ~ ndr1_0 )
| ! [X60] :
( c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60)
| ~ ndr1_0 )
| hskp30 )
& ( ! [X61] :
( c1_1(X61)
| c2_1(X61)
| ~ c0_1(X61)
| ~ ndr1_0 )
| ! [X62] :
( c2_1(X62)
| ~ c0_1(X62)
| ~ c1_1(X62)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X63] :
( c1_1(X63)
| c2_1(X63)
| ~ c0_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( ~ c0_1(X64)
| ~ c1_1(X64)
| ~ c2_1(X64)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X65] :
( c1_1(X65)
| c3_1(X65)
| ~ c0_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c2_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 )
| ! [X67] :
( ~ c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67)
| ~ ndr1_0 ) )
& ( ! [X68] :
( c1_1(X68)
| c3_1(X68)
| ~ c0_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c3_1(X69)
| ~ c1_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0 )
| hskp18 )
& ( ! [X70] :
( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0 )
| hskp19
| hskp17 )
& ( ! [X71] :
( c1_1(X71)
| c3_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 )
| hskp28
| hskp17 )
& ( ! [X72] :
( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| ! [X73] :
( c1_1(X73)
| ~ c0_1(X73)
| ~ c3_1(X73)
| ~ ndr1_0 )
| hskp20 )
& ( ! [X74] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74)
| ~ ndr1_0 )
| ! [X75] :
( c2_1(X75)
| ~ c0_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c2_1(X76)
| ~ c0_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 ) )
& ( ! [X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0 )
| ! [X78] :
( c3_1(X78)
| ~ c0_1(X78)
| ~ c2_1(X78)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X79] :
( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79)
| ~ ndr1_0 )
| ! [X80] :
( ~ c0_1(X80)
| ~ c1_1(X80)
| ~ c2_1(X80)
| ~ ndr1_0 )
| hskp31 )
& ( ! [X81] :
( c1_1(X81)
| ~ c0_1(X81)
| ~ c2_1(X81)
| ~ ndr1_0 )
| hskp29
| hskp21 )
& ( ! [X82] :
( c1_1(X82)
| ~ c0_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 )
| ! [X83] :
( c1_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X84] :
( c1_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X86] :
( c1_1(X86)
| ~ c0_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0 )
| hskp31
| hskp28 )
& ( ! [X87] :
( c1_1(X87)
| ~ c0_1(X87)
| ~ c3_1(X87)
| ~ ndr1_0 )
| hskp15
| hskp28 )
& ( ! [X88] :
( c1_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| hskp28
| hskp11 )
& ( ! [X89] :
( c1_1(X89)
| ~ c0_1(X89)
| ~ c3_1(X89)
| ~ ndr1_0 )
| hskp4
| hskp23 )
& ( ! [X90] :
( c1_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 )
| hskp4
| hskp10 )
& ( ! [X91] :
( c2_1(X91)
| c3_1(X91)
| ~ c0_1(X91)
| ~ ndr1_0 )
| hskp19
| hskp8 )
& ( ! [X92] :
( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92)
| ~ ndr1_0 )
| hskp19 )
& ( ! [X93] :
( c2_1(X93)
| ~ c0_1(X93)
| ~ c1_1(X93)
| ~ ndr1_0 )
| ! [X94] :
( c3_1(X94)
| ~ c1_1(X94)
| ~ c2_1(X94)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0 )
| hskp29
| hskp4 )
& ( ! [X96] :
( c2_1(X96)
| ~ c0_1(X96)
| ~ c1_1(X96)
| ~ ndr1_0 )
| hskp1
| hskp24 )
& ( ! [X97] :
( c2_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97)
| ~ ndr1_0 )
| hskp6
| hskp16 )
& ( ! [X98] :
( c2_1(X98)
| ~ c1_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| ! [X99] :
( ~ c0_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100)
| ~ ndr1_0 )
| hskp25
| hskp0 )
& ( ! [X101] :
( c3_1(X101)
| ~ c1_1(X101)
| ~ c2_1(X101)
| ~ ndr1_0 )
| hskp13
| hskp4 )
& ( ! [X102] :
( ~ c0_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0 )
| hskp19
| hskp11 )
& ( ! [X103] :
( ~ c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp25
| hskp0 )
& ( hskp31
| hskp30
| hskp24 )
& ( hskp5
| hskp15
| hskp13 )
& ( hskp5
| hskp16
| hskp25 )
& ( hskp5
| hskp4
| hskp9 )
& ( hskp26
| hskp7
| hskp0 )
& ( hskp26
| hskp11
| hskp4 )
& ( hskp25
| hskp8 )
& ( hskp25
| hskp27
| hskp24 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ~ hskp0
| ( ndr1_0
& c2_1(a101)
& c3_1(a101)
& ~ c0_1(a101) ) )
& ( ~ hskp1
| ( ndr1_0
& c2_1(a102)
& ~ c0_1(a102)
& ~ c1_1(a102) ) )
& ( ~ hskp2
| ( ndr1_0
& c0_1(a103)
& c1_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a104)
& c2_1(a104)
& ~ c1_1(a104) ) )
& ( ~ hskp4
| ( ndr1_0
& c2_1(a105)
& c3_1(a105)
& ~ c1_1(a105) ) )
& ( ~ hskp5
| ( ndr1_0
& c0_1(a106)
& c1_1(a106)
& ~ c2_1(a106) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a107)
& c2_1(a107)
& ~ c0_1(a107) ) )
& ( ~ hskp7
| ( ndr1_0
& c1_1(a108)
& c3_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp8
| ( ndr1_0
& c1_1(a109)
& ~ c0_1(a109)
& ~ c3_1(a109) ) )
& ( ~ hskp9
| ( ndr1_0
& c2_1(a110)
& ~ c1_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp10
| ( ndr1_0
& ~ c0_1(a111)
& ~ c2_1(a111)
& ~ c3_1(a111) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a112)
& ~ c2_1(a112)
& ~ c3_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a113)
& ~ c0_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c1_1(a114)
& c2_1(a114)
& ~ c3_1(a114) ) )
& ( ~ hskp14
| ( ndr1_0
& c0_1(a116)
& c2_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp15
| ( ndr1_0
& c0_1(a117)
& c3_1(a117)
& ~ c1_1(a117) ) )
& ( ~ hskp16
| ( ndr1_0
& c1_1(a126)
& c3_1(a126)
& ~ c2_1(a126) ) )
& ( ~ hskp17
| ( ndr1_0
& c3_1(a132)
& ~ c0_1(a132)
& ~ c1_1(a132) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a134)
& c3_1(a134)
& ~ c2_1(a134) ) )
& ( ~ hskp19
| ( ndr1_0
& c0_1(a135)
& ~ c2_1(a135)
& ~ c3_1(a135) ) )
& ( ~ hskp20
| ( ndr1_0
& c0_1(a139)
& ~ c1_1(a139)
& ~ c3_1(a139) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a143)
& ~ c1_1(a143)
& ~ c2_1(a143) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c0_1(a145)
& ~ c1_1(a145)
& ~ c2_1(a145) ) )
& ( ~ hskp23
| ( ndr1_0
& ~ c0_1(a153)
& ~ c1_1(a153)
& ~ c3_1(a153) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c1_1(a163)
& ~ c2_1(a163)
& ~ c3_1(a163) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a167)
& ~ c0_1(a167)
& ~ c2_1(a167) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a187)
& ~ c1_1(a187)
& ~ c2_1(a187) ) )
& ( ~ hskp27
| ( ndr1_0
& c2_1(a196)
& ~ c0_1(a196)
& ~ c3_1(a196) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a118)
& c2_1(a118)
& c3_1(a118) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a128)
& c1_1(a128)
& c2_1(a128) ) )
& ( ~ hskp30
| ( ndr1_0
& c0_1(a131)
& c2_1(a131)
& c3_1(a131) ) )
& ( ~ hskp31
| ( ndr1_0
& c0_1(a141)
& c1_1(a141)
& c3_1(a141) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c1_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( ~ c1_1(X2)
| ~ c2_1(X2)
| ~ c3_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c0_1(X4)
| c1_1(X4)
| ~ c3_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| ! [X6] :
( c0_1(X6)
| ~ c2_1(X6)
| ~ c3_1(X6)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X7] :
( c0_1(X7)
| c1_1(X7)
| c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c2_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8)
| ~ ndr1_0 )
| hskp2 )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0 )
| hskp3
| hskp4 )
& ( ! [X10] :
( c0_1(X10)
| c1_1(X10)
| c3_1(X10)
| ~ ndr1_0 )
| ! [X11] :
( c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c3_1(X12)
| ~ c0_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 ) )
& ( ! [X13] :
( c0_1(X13)
| c1_1(X13)
| c3_1(X13)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X14] :
( c0_1(X14)
| c1_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| hskp6
| hskp7 )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| c3_1(X15)
| ~ ndr1_0 )
| hskp8
| hskp9 )
& ( ! [X16] :
( c0_1(X16)
| c1_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 )
| ! [X17] :
( ~ c0_1(X17)
| ~ c1_1(X17)
| ~ c3_1(X17)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X18] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19)
| ~ ndr1_0 )
| ! [X20] :
( ~ c0_1(X20)
| ~ c1_1(X20)
| ~ c3_1(X20)
| ~ ndr1_0 ) )
& ( ! [X21] :
( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| ! [X22] :
( c1_1(X22)
| c2_1(X22)
| ~ c0_1(X22)
| ~ ndr1_0 )
| ! [X23] :
( c2_1(X23)
| ~ c0_1(X23)
| ~ c1_1(X23)
| ~ ndr1_0 ) )
& ( ! [X24] :
( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| ! [X25] :
( c2_1(X25)
| c3_1(X25)
| ~ c1_1(X25)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X26] :
( c0_1(X26)
| c1_1(X26)
| ~ c3_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c3_1(X27)
| ~ c0_1(X27)
| ~ c2_1(X27)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X28] :
( c0_1(X28)
| c1_1(X28)
| ~ c3_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( ~ c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( ~ c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 ) )
& ( ! [X31] :
( c0_1(X31)
| c2_1(X31)
| c3_1(X31)
| ~ ndr1_0 )
| ! [X32] :
( ~ c0_1(X32)
| ~ c1_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X33] :
( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| c2_1(X34)
| ~ c3_1(X34)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c1_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0 )
| hskp15
| hskp28 )
& ( ! [X38] :
( c0_1(X38)
| c3_1(X38)
| ~ c1_1(X38)
| ~ ndr1_0 )
| ! [X39] :
( c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39)
| ~ ndr1_0 )
| ! [X40] :
( c1_1(X40)
| ~ c0_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0 ) )
& ( ! [X41] :
( c0_1(X41)
| c3_1(X41)
| ~ c1_1(X41)
| ~ ndr1_0 )
| ! [X42] :
( c2_1(X42)
| c3_1(X42)
| ~ c0_1(X42)
| ~ ndr1_0 )
| ! [X43] :
( c3_1(X43)
| ~ c1_1(X43)
| ~ c2_1(X43)
| ~ ndr1_0 ) )
& ( ! [X44] :
( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( ~ c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X46] :
( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0 )
| hskp15
| hskp10 )
& ( ! [X47] :
( c0_1(X47)
| c3_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0 )
| hskp15
| hskp0 )
& ( ! [X48] :
( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0 )
| hskp2
| hskp7 )
& ( ! [X49] :
( c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49)
| ~ ndr1_0 )
| ! [X50] :
( c1_1(X50)
| c2_1(X50)
| c3_1(X50)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X51] :
( c0_1(X51)
| ~ c2_1(X51)
| ~ c3_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c3_1(X52)
| ~ c0_1(X52)
| ~ c2_1(X52)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X53] :
( c0_1(X53)
| ~ c2_1(X53)
| ~ c3_1(X53)
| ~ ndr1_0 )
| hskp29
| hskp11 )
& ( ! [X54] :
( c1_1(X54)
| c2_1(X54)
| c3_1(X54)
| ~ ndr1_0 )
| ! [X55] :
( c2_1(X55)
| c3_1(X55)
| ~ c0_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( ~ c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56)
| ~ ndr1_0 ) )
& ( ! [X57] :
( c1_1(X57)
| c2_1(X57)
| ~ c0_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c1_1(X58)
| c2_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X59] :
( c1_1(X59)
| c2_1(X59)
| ~ c0_1(X59)
| ~ ndr1_0 )
| ! [X60] :
( c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60)
| ~ ndr1_0 )
| hskp30 )
& ( ! [X61] :
( c1_1(X61)
| c2_1(X61)
| ~ c0_1(X61)
| ~ ndr1_0 )
| ! [X62] :
( c2_1(X62)
| ~ c0_1(X62)
| ~ c1_1(X62)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X63] :
( c1_1(X63)
| c2_1(X63)
| ~ c0_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( ~ c0_1(X64)
| ~ c1_1(X64)
| ~ c2_1(X64)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X65] :
( c1_1(X65)
| c3_1(X65)
| ~ c0_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c2_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0 )
| ! [X67] :
( ~ c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67)
| ~ ndr1_0 ) )
& ( ! [X68] :
( c1_1(X68)
| c3_1(X68)
| ~ c0_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c3_1(X69)
| ~ c1_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0 )
| hskp18 )
& ( ! [X70] :
( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0 )
| hskp19
| hskp17 )
& ( ! [X71] :
( c1_1(X71)
| c3_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 )
| hskp28
| hskp17 )
& ( ! [X72] :
( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| ! [X73] :
( c1_1(X73)
| ~ c0_1(X73)
| ~ c3_1(X73)
| ~ ndr1_0 )
| hskp20 )
& ( ! [X74] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74)
| ~ ndr1_0 )
| ! [X75] :
( c2_1(X75)
| ~ c0_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c2_1(X76)
| ~ c0_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 ) )
& ( ! [X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0 )
| ! [X78] :
( c3_1(X78)
| ~ c0_1(X78)
| ~ c2_1(X78)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X79] :
( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79)
| ~ ndr1_0 )
| ! [X80] :
( ~ c0_1(X80)
| ~ c1_1(X80)
| ~ c2_1(X80)
| ~ ndr1_0 )
| hskp31 )
& ( ! [X81] :
( c1_1(X81)
| ~ c0_1(X81)
| ~ c2_1(X81)
| ~ ndr1_0 )
| hskp29
| hskp21 )
& ( ! [X82] :
( c1_1(X82)
| ~ c0_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 )
| ! [X83] :
( c1_1(X83)
| ~ c2_1(X83)
| ~ c3_1(X83)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X84] :
( c1_1(X84)
| ~ c0_1(X84)
| ~ c3_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c1_1(X85)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X86] :
( c1_1(X86)
| ~ c0_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0 )
| hskp31
| hskp28 )
& ( ! [X87] :
( c1_1(X87)
| ~ c0_1(X87)
| ~ c3_1(X87)
| ~ ndr1_0 )
| hskp15
| hskp28 )
& ( ! [X88] :
( c1_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| hskp28
| hskp11 )
& ( ! [X89] :
( c1_1(X89)
| ~ c0_1(X89)
| ~ c3_1(X89)
| ~ ndr1_0 )
| hskp4
| hskp23 )
& ( ! [X90] :
( c1_1(X90)
| ~ c0_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 )
| hskp4
| hskp10 )
& ( ! [X91] :
( c2_1(X91)
| c3_1(X91)
| ~ c0_1(X91)
| ~ ndr1_0 )
| hskp19
| hskp8 )
& ( ! [X92] :
( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92)
| ~ ndr1_0 )
| hskp19 )
& ( ! [X93] :
( c2_1(X93)
| ~ c0_1(X93)
| ~ c1_1(X93)
| ~ ndr1_0 )
| ! [X94] :
( c3_1(X94)
| ~ c1_1(X94)
| ~ c2_1(X94)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0 )
| hskp29
| hskp4 )
& ( ! [X96] :
( c2_1(X96)
| ~ c0_1(X96)
| ~ c1_1(X96)
| ~ ndr1_0 )
| hskp1
| hskp24 )
& ( ! [X97] :
( c2_1(X97)
| ~ c0_1(X97)
| ~ c3_1(X97)
| ~ ndr1_0 )
| hskp6
| hskp16 )
& ( ! [X98] :
( c2_1(X98)
| ~ c1_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| ! [X99] :
( ~ c0_1(X99)
| ~ c2_1(X99)
| ~ c3_1(X99)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100)
| ~ ndr1_0 )
| hskp25
| hskp0 )
& ( ! [X101] :
( c3_1(X101)
| ~ c1_1(X101)
| ~ c2_1(X101)
| ~ ndr1_0 )
| hskp13
| hskp4 )
& ( ! [X102] :
( ~ c0_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0 )
| hskp19
| hskp11 )
& ( ! [X103] :
( ~ c1_1(X103)
| ~ c2_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp25
| hskp0 )
& ( hskp31
| hskp30
| hskp24 )
& ( hskp5
| hskp15
| hskp13 )
& ( hskp5
| hskp16
| hskp25 )
& ( hskp5
| hskp4
| hskp9 )
& ( hskp26
| hskp7
| hskp0 )
& ( hskp26
| hskp11
| hskp4 )
& ( hskp25
| hskp8 )
& ( hskp25
| hskp27
| hskp24 ) ),
inference(flattening,[],[f4]) ).
fof(f7,plain,
( hskp25
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f10,plain,
( hskp5
| hskp4
| hskp9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f12,plain,
( hskp5
| hskp15
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f13,plain,
( hskp31
| hskp30
| hskp24 ),
inference(cnf_transformation,[],[f5]) ).
fof(f15,plain,
! [X102] :
( ~ c0_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0
| hskp19
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f20,plain,
! [X96] :
( c2_1(X96)
| ~ c0_1(X96)
| ~ c1_1(X96)
| ~ ndr1_0
| hskp1
| hskp24 ),
inference(cnf_transformation,[],[f5]) ).
fof(f21,plain,
! [X95] :
( c2_1(X95)
| ~ c0_1(X95)
| ~ c1_1(X95)
| ~ ndr1_0
| hskp29
| hskp4 ),
inference(cnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X92] :
( c2_1(X92)
| c3_1(X92)
| ~ c1_1(X92)
| ~ ndr1_0
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X88] :
( c1_1(X88)
| ~ c0_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0
| hskp28
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f29,plain,
! [X86] :
( c1_1(X86)
| ~ c0_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0
| hskp31
| hskp28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f32,plain,
! [X81] :
( c1_1(X81)
| ~ c0_1(X81)
| ~ c2_1(X81)
| ~ ndr1_0
| hskp29
| hskp21 ),
inference(cnf_transformation,[],[f5]) ).
fof(f33,plain,
! [X80,X79] :
( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79)
| ~ ndr1_0
| ~ c0_1(X80)
| ~ c1_1(X80)
| ~ c2_1(X80)
| ~ ndr1_0
| hskp31 ),
inference(cnf_transformation,[],[f5]) ).
fof(f34,plain,
! [X78,X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c2_1(X77)
| ~ ndr1_0
| c3_1(X78)
| ~ c0_1(X78)
| ~ c2_1(X78)
| ~ ndr1_0
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f35,plain,
! [X76,X74,X75] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74)
| ~ ndr1_0
| c2_1(X75)
| ~ c0_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0
| c2_1(X76)
| ~ c0_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f38,plain,
! [X70] :
( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0
| hskp19
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f39,plain,
! [X68,X69] :
( c1_1(X68)
| c3_1(X68)
| ~ c0_1(X68)
| ~ ndr1_0
| c3_1(X69)
| ~ c1_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0
| hskp18 ),
inference(cnf_transformation,[],[f5]) ).
fof(f40,plain,
! [X65,X66,X67] :
( c1_1(X65)
| c3_1(X65)
| ~ c0_1(X65)
| ~ ndr1_0
| c2_1(X66)
| ~ c1_1(X66)
| ~ c3_1(X66)
| ~ ndr1_0
| ~ c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f42,plain,
! [X62,X61] :
( c1_1(X61)
| c2_1(X61)
| ~ c0_1(X61)
| ~ ndr1_0
| c2_1(X62)
| ~ c0_1(X62)
| ~ c1_1(X62)
| ~ ndr1_0
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f43,plain,
! [X59,X60] :
( c1_1(X59)
| c2_1(X59)
| ~ c0_1(X59)
| ~ ndr1_0
| c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60)
| ~ ndr1_0
| hskp30 ),
inference(cnf_transformation,[],[f5]) ).
fof(f45,plain,
! [X56,X54,X55] :
( c1_1(X54)
| c2_1(X54)
| c3_1(X54)
| ~ ndr1_0
| c2_1(X55)
| c3_1(X55)
| ~ c0_1(X55)
| ~ ndr1_0
| ~ c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f46,plain,
! [X53] :
( c0_1(X53)
| ~ c2_1(X53)
| ~ c3_1(X53)
| ~ ndr1_0
| hskp29
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f48,plain,
! [X50,X49] :
( c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49)
| ~ ndr1_0
| c1_1(X50)
| c2_1(X50)
| c3_1(X50)
| ~ ndr1_0
| hskp16 ),
inference(cnf_transformation,[],[f5]) ).
fof(f50,plain,
! [X47] :
( c0_1(X47)
| c3_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0
| hskp15
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f51,plain,
! [X46] :
( c0_1(X46)
| c3_1(X46)
| ~ c1_1(X46)
| ~ ndr1_0
| hskp15
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f52,plain,
! [X44,X45] :
( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44)
| ~ ndr1_0
| ~ c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f53,plain,
! [X41,X42,X43] :
( c0_1(X41)
| c3_1(X41)
| ~ c1_1(X41)
| ~ ndr1_0
| c2_1(X42)
| c3_1(X42)
| ~ c0_1(X42)
| ~ ndr1_0
| c3_1(X43)
| ~ c1_1(X43)
| ~ c2_1(X43)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f54,plain,
! [X40,X38,X39] :
( c0_1(X38)
| c3_1(X38)
| ~ c1_1(X38)
| ~ ndr1_0
| c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39)
| ~ ndr1_0
| c1_1(X40)
| ~ c0_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f55,plain,
! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ~ ndr1_0
| hskp15
| hskp28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f56,plain,
! [X36,X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35)
| ~ ndr1_0
| c1_1(X36)
| ~ c0_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0
| hskp14 ),
inference(cnf_transformation,[],[f5]) ).
fof(f58,plain,
! [X31,X32] :
( c0_1(X31)
| c2_1(X31)
| c3_1(X31)
| ~ ndr1_0
| ~ c0_1(X32)
| ~ c1_1(X32)
| ~ c3_1(X32)
| ~ ndr1_0
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f59,plain,
! [X28,X29,X30] :
( c0_1(X28)
| c1_1(X28)
| ~ c3_1(X28)
| ~ ndr1_0
| ~ c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29)
| ~ ndr1_0
| ~ c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f61,plain,
! [X24,X25] :
( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0
| c2_1(X25)
| c3_1(X25)
| ~ c1_1(X25)
| ~ ndr1_0
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f62,plain,
! [X21,X22,X23] :
( c0_1(X21)
| c1_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0
| c1_1(X22)
| c2_1(X22)
| ~ c0_1(X22)
| ~ ndr1_0
| c2_1(X23)
| ~ c0_1(X23)
| ~ c1_1(X23)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f63,plain,
! [X18,X19,X20] :
( c0_1(X18)
| c1_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0
| c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19)
| ~ ndr1_0
| ~ c0_1(X20)
| ~ c1_1(X20)
| ~ c3_1(X20)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f64,plain,
! [X16,X17] :
( c0_1(X16)
| c1_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0
| ~ c0_1(X17)
| ~ c1_1(X17)
| ~ c3_1(X17)
| ~ ndr1_0
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f65,plain,
! [X15] :
( c0_1(X15)
| c1_1(X15)
| c3_1(X15)
| ~ ndr1_0
| hskp8
| hskp9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f67,plain,
! [X13] :
( c0_1(X13)
| c1_1(X13)
| c3_1(X13)
| ~ ndr1_0
| hskp5 ),
inference(cnf_transformation,[],[f5]) ).
fof(f68,plain,
! [X10,X11,X12] :
( c0_1(X10)
| c1_1(X10)
| c3_1(X10)
| ~ ndr1_0
| c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11)
| ~ ndr1_0
| c3_1(X12)
| ~ c0_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f74,plain,
( ~ hskp31
| c3_1(a141) ),
inference(cnf_transformation,[],[f5]) ).
fof(f75,plain,
( ~ hskp31
| c1_1(a141) ),
inference(cnf_transformation,[],[f5]) ).
fof(f76,plain,
( ~ hskp31
| c0_1(a141) ),
inference(cnf_transformation,[],[f5]) ).
fof(f78,plain,
( ~ hskp30
| c3_1(a131) ),
inference(cnf_transformation,[],[f5]) ).
fof(f79,plain,
( ~ hskp30
| c2_1(a131) ),
inference(cnf_transformation,[],[f5]) ).
fof(f80,plain,
( ~ hskp30
| c0_1(a131) ),
inference(cnf_transformation,[],[f5]) ).
fof(f82,plain,
( ~ hskp29
| c2_1(a128) ),
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
( ~ hskp29
| c1_1(a128) ),
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
( ~ hskp29
| c0_1(a128) ),
inference(cnf_transformation,[],[f5]) ).
fof(f86,plain,
( ~ hskp28
| c3_1(a118) ),
inference(cnf_transformation,[],[f5]) ).
fof(f87,plain,
( ~ hskp28
| c2_1(a118) ),
inference(cnf_transformation,[],[f5]) ).
fof(f88,plain,
( ~ hskp28
| c1_1(a118) ),
inference(cnf_transformation,[],[f5]) ).
fof(f98,plain,
( ~ hskp25
| ~ c2_1(a167) ),
inference(cnf_transformation,[],[f5]) ).
fof(f99,plain,
( ~ hskp25
| ~ c0_1(a167) ),
inference(cnf_transformation,[],[f5]) ).
fof(f100,plain,
( ~ hskp25
| c1_1(a167) ),
inference(cnf_transformation,[],[f5]) ).
fof(f101,plain,
( ~ hskp25
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f102,plain,
( ~ hskp24
| ~ c3_1(a163) ),
inference(cnf_transformation,[],[f5]) ).
fof(f103,plain,
( ~ hskp24
| ~ c2_1(a163) ),
inference(cnf_transformation,[],[f5]) ).
fof(f104,plain,
( ~ hskp24
| ~ c1_1(a163) ),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
( ~ hskp24
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f114,plain,
( ~ hskp21
| ~ c2_1(a143) ),
inference(cnf_transformation,[],[f5]) ).
fof(f115,plain,
( ~ hskp21
| ~ c1_1(a143) ),
inference(cnf_transformation,[],[f5]) ).
fof(f116,plain,
( ~ hskp21
| c3_1(a143) ),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
( ~ hskp19
| ~ c3_1(a135) ),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
( ~ hskp19
| ~ c2_1(a135) ),
inference(cnf_transformation,[],[f5]) ).
fof(f124,plain,
( ~ hskp19
| c0_1(a135) ),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
( ~ hskp18
| ~ c2_1(a134) ),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
( ~ hskp18
| c3_1(a134) ),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
( ~ hskp18
| c0_1(a134) ),
inference(cnf_transformation,[],[f5]) ).
fof(f130,plain,
( ~ hskp17
| ~ c1_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f131,plain,
( ~ hskp17
| ~ c0_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
( ~ hskp17
| c3_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
( ~ hskp16
| ~ c2_1(a126) ),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
( ~ hskp16
| c3_1(a126) ),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
( ~ hskp16
| c1_1(a126) ),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
( ~ hskp15
| ~ c1_1(a117) ),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
( ~ hskp15
| c3_1(a117) ),
inference(cnf_transformation,[],[f5]) ).
fof(f140,plain,
( ~ hskp15
| c0_1(a117) ),
inference(cnf_transformation,[],[f5]) ).
fof(f142,plain,
( ~ hskp14
| ~ c3_1(a116) ),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
( ~ hskp14
| c2_1(a116) ),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
( ~ hskp14
| c0_1(a116) ),
inference(cnf_transformation,[],[f5]) ).
fof(f146,plain,
( ~ hskp13
| ~ c3_1(a114) ),
inference(cnf_transformation,[],[f5]) ).
fof(f147,plain,
( ~ hskp13
| c2_1(a114) ),
inference(cnf_transformation,[],[f5]) ).
fof(f148,plain,
( ~ hskp13
| c1_1(a114) ),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
( ~ hskp11
| ~ c3_1(a112) ),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
( ~ hskp11
| ~ c2_1(a112) ),
inference(cnf_transformation,[],[f5]) ).
fof(f156,plain,
( ~ hskp11
| c1_1(a112) ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( ~ hskp10
| ~ c3_1(a111) ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( ~ hskp10
| ~ c2_1(a111) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( ~ hskp10
| ~ c0_1(a111) ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( ~ hskp9
| ~ c3_1(a110) ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( ~ hskp9
| ~ c1_1(a110) ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( ~ hskp9
| c2_1(a110) ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( ~ hskp8
| ~ c3_1(a109) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( ~ hskp8
| ~ c0_1(a109) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( ~ hskp8
| c1_1(a109) ),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
( ~ hskp8
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( ~ hskp5
| ~ c2_1(a106) ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( ~ hskp5
| c1_1(a106) ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( ~ hskp5
| c0_1(a106) ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( ~ hskp4
| ~ c1_1(a105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( ~ hskp4
| c3_1(a105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( ~ hskp4
| c2_1(a105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f194,plain,
( ~ hskp1
| ~ c1_1(a102) ),
inference(cnf_transformation,[],[f5]) ).
fof(f195,plain,
( ~ hskp1
| ~ c0_1(a102) ),
inference(cnf_transformation,[],[f5]) ).
fof(f196,plain,
( ~ hskp1
| c2_1(a102) ),
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
( ~ hskp0
| ~ c0_1(a101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
( ~ hskp0
| c3_1(a101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
( ~ hskp0
| c2_1(a101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f203,plain,
( ~ hskp0
| c0_1(a101) ),
inference(consistent_polarity_flipping,[],[f198]) ).
fof(f205,plain,
( ~ hskp1
| c0_1(a102) ),
inference(consistent_polarity_flipping,[],[f195]) ).
fof(f206,plain,
( ~ hskp1
| c1_1(a102) ),
inference(consistent_polarity_flipping,[],[f194]) ).
fof(f215,plain,
( ~ hskp4
| c1_1(a105) ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f217,plain,
( hskp5
| ~ c0_1(a106) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f218,plain,
( hskp5
| ~ c1_1(a106) ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f219,plain,
( hskp5
| ~ c2_1(a106) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f227,plain,
( hskp8
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f228,plain,
( hskp8
| ~ c1_1(a109) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f229,plain,
( hskp8
| c0_1(a109) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f230,plain,
( hskp8
| ~ c3_1(a109) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f232,plain,
( hskp9
| c2_1(a110) ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f233,plain,
( hskp9
| c1_1(a110) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f234,plain,
( hskp9
| ~ c3_1(a110) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f236,plain,
( hskp10
| c0_1(a111) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f237,plain,
( hskp10
| ~ c2_1(a111) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f238,plain,
( hskp10
| ~ c3_1(a111) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f240,plain,
( ~ hskp11
| ~ c1_1(a112) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f246,plain,
( hskp13
| ~ c1_1(a114) ),
inference(consistent_polarity_flipping,[],[f148]) ).
fof(f247,plain,
( hskp13
| c2_1(a114) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f248,plain,
( hskp13
| ~ c3_1(a114) ),
inference(consistent_polarity_flipping,[],[f146]) ).
fof(f250,plain,
( hskp14
| ~ c0_1(a116) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f251,plain,
( hskp14
| c2_1(a116) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f252,plain,
( hskp14
| ~ c3_1(a116) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f254,plain,
( hskp15
| ~ c0_1(a117) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f255,plain,
( hskp15
| c3_1(a117) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f256,plain,
( hskp15
| c1_1(a117) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f258,plain,
( hskp16
| ~ c1_1(a126) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f259,plain,
( hskp16
| c3_1(a126) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f260,plain,
( hskp16
| ~ c2_1(a126) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f262,plain,
( hskp17
| c3_1(a132) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f263,plain,
( hskp17
| c0_1(a132) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f264,plain,
( hskp17
| c1_1(a132) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f266,plain,
( hskp18
| ~ c0_1(a134) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f267,plain,
( hskp18
| c3_1(a134) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f268,plain,
( hskp18
| ~ c2_1(a134) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f270,plain,
( hskp19
| ~ c0_1(a135) ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f271,plain,
( hskp19
| ~ c2_1(a135) ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f272,plain,
( hskp19
| ~ c3_1(a135) ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f278,plain,
( ~ hskp21
| c1_1(a143) ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f286,plain,
( ~ hskp24
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f287,plain,
( ~ hskp24
| c1_1(a163) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f288,plain,
( hskp25
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f289,plain,
( hskp25
| ~ c1_1(a167) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f290,plain,
( hskp25
| c0_1(a167) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f291,plain,
( hskp25
| ~ c2_1(a167) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f298,plain,
( ~ hskp28
| ~ c1_1(a118) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f300,plain,
( hskp29
| ~ c0_1(a128) ),
inference(consistent_polarity_flipping,[],[f84]) ).
fof(f301,plain,
( hskp29
| ~ c1_1(a128) ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f302,plain,
( hskp29
| c2_1(a128) ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f304,plain,
( hskp30
| ~ c0_1(a131) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f305,plain,
( hskp30
| c2_1(a131) ),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f306,plain,
( hskp30
| c3_1(a131) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f308,plain,
( hskp31
| ~ c0_1(a141) ),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f309,plain,
( hskp31
| ~ c1_1(a141) ),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f310,plain,
( hskp31
| c3_1(a141) ),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f316,plain,
! [X10,X11,X12] :
( ~ c0_1(X10)
| ~ c1_1(X10)
| c3_1(X10)
| ndr1_0
| ~ c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11)
| ndr1_0
| c3_1(X12)
| c0_1(X12)
| ~ c2_1(X12)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f317,plain,
! [X13] :
( ~ c0_1(X13)
| ~ c1_1(X13)
| c3_1(X13)
| ndr1_0
| ~ hskp5 ),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f319,plain,
! [X15] :
( ~ c0_1(X15)
| ~ c1_1(X15)
| c3_1(X15)
| ndr1_0
| ~ hskp8
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f65]) ).
fof(f320,plain,
! [X16,X17] :
( ~ c0_1(X16)
| ~ c1_1(X16)
| ~ c2_1(X16)
| ndr1_0
| c0_1(X17)
| c1_1(X17)
| ~ c3_1(X17)
| ndr1_0
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f64]) ).
fof(f321,plain,
! [X18,X19,X20] :
( ~ c0_1(X18)
| ~ c1_1(X18)
| ~ c3_1(X18)
| ndr1_0
| ~ c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19)
| ndr1_0
| c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f63]) ).
fof(f322,plain,
! [X21,X22,X23] :
( ~ c0_1(X21)
| ~ c1_1(X21)
| ~ c3_1(X21)
| ndr1_0
| ~ c1_1(X22)
| c2_1(X22)
| c0_1(X22)
| ndr1_0
| c2_1(X23)
| c0_1(X23)
| c1_1(X23)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f62]) ).
fof(f323,plain,
! [X24,X25] :
( ~ c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24)
| ndr1_0
| c2_1(X25)
| c3_1(X25)
| c1_1(X25)
| ndr1_0
| hskp11 ),
inference(consistent_polarity_flipping,[],[f61]) ).
fof(f325,plain,
! [X28,X29,X30] :
( ~ c0_1(X28)
| ~ c1_1(X28)
| ~ c3_1(X28)
| ndr1_0
| c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29)
| ndr1_0
| c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f59]) ).
fof(f326,plain,
! [X31,X32] :
( ~ c0_1(X31)
| c2_1(X31)
| c3_1(X31)
| ndr1_0
| c0_1(X32)
| c1_1(X32)
| ~ c3_1(X32)
| ndr1_0
| ~ hskp13 ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f328,plain,
! [X36,X35] :
( ~ c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35)
| ndr1_0
| ~ c1_1(X36)
| c0_1(X36)
| ~ c2_1(X36)
| ndr1_0
| ~ hskp14 ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f329,plain,
! [X37] :
( ~ c0_1(X37)
| c2_1(X37)
| ~ c3_1(X37)
| ndr1_0
| ~ hskp15
| hskp28 ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f330,plain,
! [X40,X38,X39] :
( ~ c0_1(X38)
| c3_1(X38)
| c1_1(X38)
| ndr1_0
| ~ c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39)
| ndr1_0
| ~ c1_1(X40)
| c0_1(X40)
| ~ c3_1(X40)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f331,plain,
! [X41,X42,X43] :
( ~ c0_1(X41)
| c3_1(X41)
| c1_1(X41)
| ndr1_0
| c2_1(X42)
| c3_1(X42)
| c0_1(X42)
| ndr1_0
| c3_1(X43)
| c1_1(X43)
| ~ c2_1(X43)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f332,plain,
! [X44,X45] :
( ~ c0_1(X44)
| c3_1(X44)
| c1_1(X44)
| ndr1_0
| c0_1(X45)
| c1_1(X45)
| ~ c3_1(X45)
| ndr1_0
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f333,plain,
! [X46] :
( ~ c0_1(X46)
| c3_1(X46)
| c1_1(X46)
| ndr1_0
| ~ hskp15
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f334,plain,
! [X47] :
( ~ c0_1(X47)
| c3_1(X47)
| ~ c2_1(X47)
| ndr1_0
| ~ hskp15
| hskp0 ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f336,plain,
! [X50,X49] :
( ~ c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49)
| ndr1_0
| ~ c1_1(X50)
| c2_1(X50)
| c3_1(X50)
| ndr1_0
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f338,plain,
! [X53] :
( ~ c0_1(X53)
| ~ c2_1(X53)
| ~ c3_1(X53)
| ndr1_0
| ~ hskp29
| hskp11 ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f339,plain,
! [X56,X54,X55] :
( ~ c1_1(X54)
| c2_1(X54)
| c3_1(X54)
| ndr1_0
| c2_1(X55)
| c3_1(X55)
| c0_1(X55)
| ndr1_0
| c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f341,plain,
! [X59,X60] :
( ~ c1_1(X59)
| c2_1(X59)
| c0_1(X59)
| ndr1_0
| ~ c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60)
| ndr1_0
| ~ hskp30 ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f342,plain,
! [X62,X61] :
( ~ c1_1(X61)
| c2_1(X61)
| c0_1(X61)
| ndr1_0
| c2_1(X62)
| c0_1(X62)
| c1_1(X62)
| ndr1_0
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f344,plain,
! [X65,X66,X67] :
( ~ c1_1(X65)
| c3_1(X65)
| c0_1(X65)
| ndr1_0
| c2_1(X66)
| c1_1(X66)
| ~ c3_1(X66)
| ndr1_0
| c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f345,plain,
! [X68,X69] :
( ~ c1_1(X68)
| c3_1(X68)
| c0_1(X68)
| ndr1_0
| c3_1(X69)
| c1_1(X69)
| ~ c2_1(X69)
| ndr1_0
| ~ hskp18 ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f346,plain,
! [X70] :
( ~ c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70)
| ndr1_0
| ~ hskp19
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f349,plain,
! [X76,X74,X75] :
( ~ c1_1(X74)
| c0_1(X74)
| ~ c2_1(X74)
| ndr1_0
| c2_1(X75)
| c0_1(X75)
| c1_1(X75)
| ndr1_0
| c2_1(X76)
| c0_1(X76)
| ~ c3_1(X76)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f350,plain,
! [X78,X77] :
( ~ c1_1(X77)
| c0_1(X77)
| ~ c2_1(X77)
| ndr1_0
| c3_1(X78)
| c0_1(X78)
| ~ c2_1(X78)
| ndr1_0
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f34]) ).
fof(f351,plain,
! [X80,X79] :
( ~ c1_1(X79)
| c0_1(X79)
| ~ c2_1(X79)
| ndr1_0
| c0_1(X80)
| c1_1(X80)
| ~ c2_1(X80)
| ndr1_0
| ~ hskp31 ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f352,plain,
! [X81] :
( ~ c1_1(X81)
| c0_1(X81)
| ~ c2_1(X81)
| ndr1_0
| ~ hskp29
| hskp21 ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f355,plain,
! [X86] :
( ~ c1_1(X86)
| c0_1(X86)
| ~ c3_1(X86)
| ndr1_0
| ~ hskp31
| hskp28 ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f357,plain,
! [X88] :
( ~ c1_1(X88)
| c0_1(X88)
| ~ c3_1(X88)
| ndr1_0
| hskp28
| hskp11 ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f361,plain,
! [X92] :
( c2_1(X92)
| c3_1(X92)
| c1_1(X92)
| ndr1_0
| ~ hskp19 ),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f363,plain,
! [X95] :
( c2_1(X95)
| c0_1(X95)
| c1_1(X95)
| ndr1_0
| ~ hskp29
| hskp4 ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f364,plain,
! [X96] :
( c2_1(X96)
| c0_1(X96)
| c1_1(X96)
| ndr1_0
| hskp1
| hskp24 ),
inference(consistent_polarity_flipping,[],[f20]) ).
fof(f369,plain,
! [X102] :
( c0_1(X102)
| ~ c2_1(X102)
| ~ c3_1(X102)
| ndr1_0
| ~ hskp19
| hskp11 ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f371,plain,
( ~ hskp31
| ~ hskp30
| hskp24 ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f372,plain,
( ~ hskp5
| ~ hskp15
| ~ hskp13 ),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f374,plain,
( ~ hskp5
| hskp4
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f375,plain,
( ~ hskp25
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f7]) ).
fof(f381,plain,
! [X80,X79] :
( ~ c1_1(X79)
| c0_1(X79)
| ~ c2_1(X79)
| ndr1_0
| c0_1(X80)
| c1_1(X80)
| ~ c2_1(X80)
| ~ hskp31 ),
inference(duplicate_literal_removal,[],[f351]) ).
fof(f382,plain,
! [X78,X77] :
( ~ c1_1(X77)
| c0_1(X77)
| ~ c2_1(X77)
| ndr1_0
| c3_1(X78)
| c0_1(X78)
| ~ c2_1(X78)
| ~ hskp17 ),
inference(duplicate_literal_removal,[],[f350]) ).
fof(f383,plain,
! [X76,X74,X75] :
( ~ c1_1(X74)
| c0_1(X74)
| ~ c2_1(X74)
| ndr1_0
| c2_1(X75)
| c0_1(X75)
| c1_1(X75)
| c2_1(X76)
| c0_1(X76)
| ~ c3_1(X76) ),
inference(duplicate_literal_removal,[],[f349]) ).
fof(f385,plain,
! [X68,X69] :
( ~ c1_1(X68)
| c3_1(X68)
| c0_1(X68)
| ndr1_0
| c3_1(X69)
| c1_1(X69)
| ~ c2_1(X69)
| ~ hskp18 ),
inference(duplicate_literal_removal,[],[f345]) ).
fof(f386,plain,
! [X65,X66,X67] :
( ~ c1_1(X65)
| c3_1(X65)
| c0_1(X65)
| ndr1_0
| c2_1(X66)
| c1_1(X66)
| ~ c3_1(X66)
| c0_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67) ),
inference(duplicate_literal_removal,[],[f344]) ).
fof(f388,plain,
! [X62,X61] :
( ~ c1_1(X61)
| c2_1(X61)
| c0_1(X61)
| ndr1_0
| c2_1(X62)
| c0_1(X62)
| c1_1(X62)
| ~ hskp17 ),
inference(duplicate_literal_removal,[],[f342]) ).
fof(f389,plain,
! [X59,X60] :
( ~ c1_1(X59)
| c2_1(X59)
| c0_1(X59)
| ndr1_0
| ~ c1_1(X60)
| c3_1(X60)
| ~ c2_1(X60)
| ~ hskp30 ),
inference(duplicate_literal_removal,[],[f341]) ).
fof(f391,plain,
! [X56,X54,X55] :
( ~ c1_1(X54)
| c2_1(X54)
| c3_1(X54)
| ndr1_0
| c2_1(X55)
| c3_1(X55)
| c0_1(X55)
| c1_1(X56)
| ~ c2_1(X56)
| ~ c3_1(X56) ),
inference(duplicate_literal_removal,[],[f339]) ).
fof(f393,plain,
! [X50,X49] :
( ~ c0_1(X49)
| ~ c2_1(X49)
| ~ c3_1(X49)
| ndr1_0
| ~ c1_1(X50)
| c2_1(X50)
| c3_1(X50)
| ~ hskp16 ),
inference(duplicate_literal_removal,[],[f336]) ).
fof(f394,plain,
! [X44,X45] :
( ~ c0_1(X44)
| c3_1(X44)
| c1_1(X44)
| ndr1_0
| c0_1(X45)
| c1_1(X45)
| ~ c3_1(X45)
| ~ hskp8 ),
inference(duplicate_literal_removal,[],[f332]) ).
fof(f395,plain,
! [X41,X42,X43] :
( ~ c0_1(X41)
| c3_1(X41)
| c1_1(X41)
| ndr1_0
| c2_1(X42)
| c3_1(X42)
| c0_1(X42)
| c3_1(X43)
| c1_1(X43)
| ~ c2_1(X43) ),
inference(duplicate_literal_removal,[],[f331]) ).
fof(f396,plain,
! [X40,X38,X39] :
( ~ c0_1(X38)
| c3_1(X38)
| c1_1(X38)
| ndr1_0
| ~ c1_1(X39)
| c2_1(X39)
| ~ c3_1(X39)
| ~ c1_1(X40)
| c0_1(X40)
| ~ c3_1(X40) ),
inference(duplicate_literal_removal,[],[f330]) ).
fof(f397,plain,
! [X36,X35] :
( ~ c0_1(X35)
| c2_1(X35)
| ~ c3_1(X35)
| ndr1_0
| ~ c1_1(X36)
| c0_1(X36)
| ~ c2_1(X36)
| ~ hskp14 ),
inference(duplicate_literal_removal,[],[f328]) ).
fof(f399,plain,
! [X31,X32] :
( ~ c0_1(X31)
| c2_1(X31)
| c3_1(X31)
| ndr1_0
| c0_1(X32)
| c1_1(X32)
| ~ c3_1(X32)
| ~ hskp13 ),
inference(duplicate_literal_removal,[],[f326]) ).
fof(f400,plain,
! [X28,X29,X30] :
( ~ c0_1(X28)
| ~ c1_1(X28)
| ~ c3_1(X28)
| ndr1_0
| c0_1(X29)
| ~ c2_1(X29)
| ~ c3_1(X29)
| c1_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30) ),
inference(duplicate_literal_removal,[],[f325]) ).
fof(f402,plain,
! [X24,X25] :
( ~ c0_1(X24)
| ~ c1_1(X24)
| ~ c3_1(X24)
| ndr1_0
| c2_1(X25)
| c3_1(X25)
| c1_1(X25)
| hskp11 ),
inference(duplicate_literal_removal,[],[f323]) ).
fof(f403,plain,
! [X21,X22,X23] :
( ~ c0_1(X21)
| ~ c1_1(X21)
| ~ c3_1(X21)
| ndr1_0
| ~ c1_1(X22)
| c2_1(X22)
| c0_1(X22)
| c2_1(X23)
| c0_1(X23)
| c1_1(X23) ),
inference(duplicate_literal_removal,[],[f322]) ).
fof(f404,plain,
! [X18,X19,X20] :
( ~ c0_1(X18)
| ~ c1_1(X18)
| ~ c3_1(X18)
| ndr1_0
| ~ c0_1(X19)
| c2_1(X19)
| ~ c3_1(X19)
| c0_1(X20)
| c1_1(X20)
| ~ c3_1(X20) ),
inference(duplicate_literal_removal,[],[f321]) ).
fof(f405,plain,
! [X16,X17] :
( ~ c0_1(X16)
| ~ c1_1(X16)
| ~ c2_1(X16)
| ndr1_0
| c0_1(X17)
| c1_1(X17)
| ~ c3_1(X17)
| ~ hskp10 ),
inference(duplicate_literal_removal,[],[f320]) ).
fof(f406,plain,
! [X10,X11,X12] :
( ~ c0_1(X10)
| ~ c1_1(X10)
| c3_1(X10)
| ndr1_0
| ~ c0_1(X11)
| c3_1(X11)
| ~ c2_1(X11)
| c3_1(X12)
| c0_1(X12)
| ~ c2_1(X12) ),
inference(duplicate_literal_removal,[],[f316]) ).
fof(f412,definition,
( spl0_1
<=> hskp24 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f420,definition,
( spl0_3
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f425,definition,
( spl0_4
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f428,plain,
( ~ spl0_4
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f375,f420,f425]) ).
fof(f430,definition,
( spl0_5
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f434,definition,
( spl0_6
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f443,definition,
( spl0_8
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f452,definition,
( spl0_10
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f456,definition,
( spl0_11
<=> hskp5 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f459,plain,
( ~ spl0_10
| spl0_5
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f374,f456,f430,f452]) ).
fof(f461,definition,
( spl0_12
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f466,definition,
( spl0_13
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f470,definition,
( spl0_14
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f473,plain,
( ~ spl0_13
| ~ spl0_14
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f372,f456,f470,f466]) ).
fof(f475,definition,
( spl0_15
<=> hskp30 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f479,definition,
( spl0_16
<=> hskp31 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f482,plain,
( spl0_1
| ~ spl0_15
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f371,f479,f475,f412]) ).
fof(f484,definition,
( spl0_17
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f488,definition,
( spl0_18
<=> ! [X103] :
( c1_1(X103)
| ~ c3_1(X103)
| ~ c2_1(X103) ) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f489,plain,
( ! [X103] :
( c1_1(X103)
| ~ c3_1(X103)
| ~ c2_1(X103) )
| ~ spl0_18 ),
inference(avatar_component_clause,[],[f488]) ).
fof(f492,definition,
( spl0_19
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f496,definition,
( spl0_20
<=> ! [X102] :
( c0_1(X102)
| ~ c3_1(X102)
| ~ c2_1(X102) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f497,plain,
( ! [X102] :
( c0_1(X102)
| ~ c3_1(X102)
| ~ c2_1(X102) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f496]) ).
fof(f498,plain,
( spl0_6
| ~ spl0_19
| spl0_17
| spl0_20 ),
inference(avatar_split_clause,[],[f369,f496,f484,f492,f434]) ).
fof(f500,definition,
( spl0_21
<=> ! [X101] :
( c3_1(X101)
| ~ c2_1(X101)
| c1_1(X101) ) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f501,plain,
( ! [X101] :
( c1_1(X101)
| ~ c2_1(X101)
| c3_1(X101) )
| ~ spl0_21 ),
inference(avatar_component_clause,[],[f500]) ).
fof(f508,definition,
( spl0_23
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f512,definition,
( spl0_24
<=> ! [X98] :
( c2_1(X98)
| ~ c3_1(X98)
| c1_1(X98) ) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f513,plain,
( ! [X98] :
( c1_1(X98)
| ~ c3_1(X98)
| c2_1(X98) )
| ~ spl0_24 ),
inference(avatar_component_clause,[],[f512]) ).
fof(f520,definition,
( spl0_26
<=> ! [X97] :
( c2_1(X97)
| ~ c3_1(X97)
| c0_1(X97) ) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f521,plain,
( ! [X97] :
( c0_1(X97)
| ~ c3_1(X97)
| c2_1(X97) )
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f524,definition,
( spl0_27
<=> ! [X96] :
( c2_1(X96)
| c1_1(X96)
| c0_1(X96) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f525,plain,
( ! [X96] :
( c1_1(X96)
| c2_1(X96)
| c0_1(X96) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f524]) ).
fof(f526,plain,
( spl0_1
| spl0_23
| spl0_17
| spl0_27 ),
inference(avatar_split_clause,[],[f364,f524,f484,f508,f412]) ).
fof(f528,definition,
( spl0_28
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f531,plain,
( spl0_5
| ~ spl0_28
| spl0_17
| spl0_27 ),
inference(avatar_split_clause,[],[f363,f524,f484,f528,f430]) ).
fof(f538,definition,
( spl0_30
<=> ! [X92] :
( c2_1(X92)
| c1_1(X92)
| c3_1(X92) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f539,plain,
( ! [X92] :
( c1_1(X92)
| c2_1(X92)
| c3_1(X92) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( ~ spl0_19
| spl0_17
| spl0_30 ),
inference(avatar_split_clause,[],[f361,f538,f484,f492]) ).
fof(f542,definition,
( spl0_31
<=> ! [X91] :
( c2_1(X91)
| c0_1(X91)
| c3_1(X91) ) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f543,plain,
( ! [X91] :
( c0_1(X91)
| c2_1(X91)
| c3_1(X91) )
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f542]) ).
fof(f546,definition,
( spl0_32
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f550,definition,
( spl0_33
<=> ! [X90] :
( ~ c1_1(X90)
| ~ c3_1(X90)
| c0_1(X90) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f551,plain,
( ! [X90] :
( ~ c1_1(X90)
| ~ c3_1(X90)
| c0_1(X90) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f550]) ).
fof(f559,definition,
( spl0_35
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f562,plain,
( spl0_6
| spl0_35
| spl0_17
| spl0_33 ),
inference(avatar_split_clause,[],[f357,f550,f484,f559,f434]) ).
fof(f564,plain,
( spl0_35
| ~ spl0_16
| spl0_17
| spl0_33 ),
inference(avatar_split_clause,[],[f355,f550,f484,f479,f559]) ).
fof(f571,definition,
( spl0_37
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f579,definition,
( spl0_39
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f583,definition,
( spl0_40
<=> ! [X81] :
( ~ c1_1(X81)
| ~ c2_1(X81)
| c0_1(X81) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f584,plain,
( ! [X81] :
( ~ c1_1(X81)
| ~ c2_1(X81)
| c0_1(X81) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f585,plain,
( spl0_39
| ~ spl0_28
| spl0_17
| spl0_40 ),
inference(avatar_split_clause,[],[f352,f583,f484,f528,f579]) ).
fof(f587,definition,
( spl0_41
<=> ! [X80] :
( c0_1(X80)
| ~ c2_1(X80)
| c1_1(X80) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f588,plain,
( ! [X80] :
( c1_1(X80)
| ~ c2_1(X80)
| c0_1(X80) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f589,plain,
( ~ spl0_16
| spl0_41
| spl0_17
| spl0_40 ),
inference(avatar_split_clause,[],[f381,f583,f484,f587,f479]) ).
fof(f591,definition,
( spl0_42
<=> ! [X78] :
( c3_1(X78)
| ~ c2_1(X78)
| c0_1(X78) ) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f592,plain,
( ! [X78] :
( c0_1(X78)
| ~ c2_1(X78)
| c3_1(X78) )
| ~ spl0_42 ),
inference(avatar_component_clause,[],[f591]) ).
fof(f593,plain,
( ~ spl0_37
| spl0_42
| spl0_17
| spl0_40 ),
inference(avatar_split_clause,[],[f382,f583,f484,f591,f571]) ).
fof(f594,plain,
( spl0_26
| spl0_27
| spl0_17
| spl0_40 ),
inference(avatar_split_clause,[],[f383,f583,f484,f524,f520]) ).
fof(f601,definition,
( spl0_44
<=> ! [X71] :
( ~ c1_1(X71)
| ~ c2_1(X71)
| c3_1(X71) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f602,plain,
( ! [X71] :
( ~ c1_1(X71)
| ~ c2_1(X71)
| c3_1(X71) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f601]) ).
fof(f604,plain,
( ~ spl0_37
| ~ spl0_19
| spl0_17
| spl0_44 ),
inference(avatar_split_clause,[],[f346,f601,f484,f492,f571]) ).
fof(f606,definition,
( spl0_45
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f610,definition,
( spl0_46
<=> ! [X68] :
( ~ c1_1(X68)
| c0_1(X68)
| c3_1(X68) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f611,plain,
( ! [X68] :
( ~ c1_1(X68)
| c0_1(X68)
| c3_1(X68) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f612,plain,
( ~ spl0_45
| spl0_21
| spl0_17
| spl0_46 ),
inference(avatar_split_clause,[],[f385,f610,f484,f500,f606]) ).
fof(f613,plain,
( spl0_20
| spl0_24
| spl0_17
| spl0_46 ),
inference(avatar_split_clause,[],[f386,f610,f484,f512,f496]) ).
fof(f615,definition,
( spl0_47
<=> ! [X63] :
( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f616,plain,
( ! [X63] :
( ~ c1_1(X63)
| c0_1(X63)
| c2_1(X63) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f618,plain,
( ~ spl0_37
| spl0_27
| spl0_17
| spl0_47 ),
inference(avatar_split_clause,[],[f388,f615,f484,f524,f571]) ).
fof(f619,plain,
( ~ spl0_15
| spl0_44
| spl0_17
| spl0_47 ),
inference(avatar_split_clause,[],[f389,f615,f484,f601,f475]) ).
fof(f621,definition,
( spl0_48
<=> ! [X58] :
( ~ c1_1(X58)
| ~ c3_1(X58)
| c2_1(X58) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f622,plain,
( ! [X58] :
( ~ c1_1(X58)
| ~ c3_1(X58)
| c2_1(X58) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl0_49
<=> ! [X54] :
( ~ c1_1(X54)
| c3_1(X54)
| c2_1(X54) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f626,plain,
( ! [X54] :
( ~ c1_1(X54)
| c3_1(X54)
| c2_1(X54) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f627,plain,
( spl0_18
| spl0_31
| spl0_17
| spl0_49 ),
inference(avatar_split_clause,[],[f391,f625,f484,f542,f488]) ).
fof(f629,definition,
( spl0_50
<=> ! [X53] :
( ~ c0_1(X53)
| ~ c3_1(X53)
| ~ c2_1(X53) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f630,plain,
( ! [X53] :
( ~ c0_1(X53)
| ~ c3_1(X53)
| ~ c2_1(X53) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f631,plain,
( spl0_6
| ~ spl0_28
| spl0_17
| spl0_50 ),
inference(avatar_split_clause,[],[f338,f629,f484,f528,f434]) ).
fof(f633,plain,
( ~ spl0_12
| spl0_49
| spl0_17
| spl0_50 ),
inference(avatar_split_clause,[],[f393,f629,f484,f625,f461]) ).
fof(f643,definition,
( spl0_53
<=> ! [X47] :
( ~ c0_1(X47)
| ~ c2_1(X47)
| c3_1(X47) ) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f644,plain,
( ! [X47] :
( ~ c0_1(X47)
| ~ c2_1(X47)
| c3_1(X47) )
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f645,plain,
( spl0_8
| ~ spl0_14
| spl0_17
| spl0_53 ),
inference(avatar_split_clause,[],[f334,f643,f484,f470,f443]) ).
fof(f647,definition,
( spl0_54
<=> ! [X46] :
( ~ c0_1(X46)
| c1_1(X46)
| c3_1(X46) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f648,plain,
( ! [X46] :
( c1_1(X46)
| ~ c0_1(X46)
| c3_1(X46) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f647]) ).
fof(f649,plain,
( ~ spl0_32
| ~ spl0_14
| spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f333,f647,f484,f470,f546]) ).
fof(f651,definition,
( spl0_55
<=> ! [X45] :
( c0_1(X45)
| ~ c3_1(X45)
| c1_1(X45) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f652,plain,
( ! [X45] :
( c1_1(X45)
| ~ c3_1(X45)
| c0_1(X45) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f651]) ).
fof(f653,plain,
( ~ spl0_4
| spl0_55
| spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f394,f647,f484,f651,f425]) ).
fof(f654,plain,
( spl0_21
| spl0_31
| spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f395,f647,f484,f542,f500]) ).
fof(f655,plain,
( spl0_33
| spl0_48
| spl0_17
| spl0_54 ),
inference(avatar_split_clause,[],[f396,f647,f484,f621,f550]) ).
fof(f657,definition,
( spl0_56
<=> ! [X37] :
( ~ c0_1(X37)
| ~ c3_1(X37)
| c2_1(X37) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f658,plain,
( ! [X37] :
( ~ c0_1(X37)
| ~ c3_1(X37)
| c2_1(X37) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f659,plain,
( spl0_35
| ~ spl0_14
| spl0_17
| spl0_56 ),
inference(avatar_split_clause,[],[f329,f657,f484,f470,f559]) ).
fof(f661,definition,
( spl0_57
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f664,plain,
( ~ spl0_57
| spl0_40
| spl0_17
| spl0_56 ),
inference(avatar_split_clause,[],[f397,f657,f484,f583,f661]) ).
fof(f670,definition,
( spl0_59
<=> ! [X31] :
( ~ c0_1(X31)
| c3_1(X31)
| c2_1(X31) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f671,plain,
( ! [X31] :
( ~ c0_1(X31)
| c3_1(X31)
| c2_1(X31) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f670]) ).
fof(f672,plain,
( ~ spl0_13
| spl0_55
| spl0_17
| spl0_59 ),
inference(avatar_split_clause,[],[f399,f670,f484,f651,f466]) ).
fof(f674,definition,
( spl0_60
<=> ! [X28] :
( ~ c0_1(X28)
| ~ c3_1(X28)
| ~ c1_1(X28) ) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f675,plain,
( ! [X28] :
( ~ c1_1(X28)
| ~ c3_1(X28)
| ~ c0_1(X28) )
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f674]) ).
fof(f676,plain,
( spl0_18
| spl0_20
| spl0_17
| spl0_60 ),
inference(avatar_split_clause,[],[f400,f674,f484,f496,f488]) ).
fof(f678,plain,
( spl0_6
| spl0_30
| spl0_17
| spl0_60 ),
inference(avatar_split_clause,[],[f402,f674,f484,f538,f434]) ).
fof(f679,plain,
( spl0_27
| spl0_47
| spl0_17
| spl0_60 ),
inference(avatar_split_clause,[],[f403,f674,f484,f615,f524]) ).
fof(f680,plain,
( spl0_55
| spl0_56
| spl0_17
| spl0_60 ),
inference(avatar_split_clause,[],[f404,f674,f484,f657,f651]) ).
fof(f682,definition,
( spl0_61
<=> ! [X16] :
( ~ c0_1(X16)
| ~ c2_1(X16)
| ~ c1_1(X16) ) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f683,plain,
( ! [X16] :
( ~ c1_1(X16)
| ~ c2_1(X16)
| ~ c0_1(X16) )
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f682]) ).
fof(f684,plain,
( ~ spl0_32
| spl0_55
| spl0_17
| spl0_61 ),
inference(avatar_split_clause,[],[f405,f682,f484,f651,f546]) ).
fof(f686,definition,
( spl0_62
<=> ! [X15] :
( ~ c0_1(X15)
| c3_1(X15)
| ~ c1_1(X15) ) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f687,plain,
( ! [X15] :
( ~ c1_1(X15)
| c3_1(X15)
| ~ c0_1(X15) )
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f686]) ).
fof(f688,plain,
( ~ spl0_10
| ~ spl0_4
| spl0_17
| spl0_62 ),
inference(avatar_split_clause,[],[f319,f686,f484,f425,f452]) ).
fof(f690,plain,
( ~ spl0_11
| spl0_17
| spl0_62 ),
inference(avatar_split_clause,[],[f317,f686,f484,f456]) ).
fof(f691,plain,
( spl0_42
| spl0_53
| spl0_17
| spl0_62 ),
inference(avatar_split_clause,[],[f406,f686,f484,f643,f591]) ).
fof(f705,definition,
( spl0_65
<=> c3_1(a141) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f708,plain,
( spl0_65
| spl0_16 ),
inference(avatar_split_clause,[],[f310,f479,f705]) ).
fof(f710,definition,
( spl0_66
<=> c1_1(a141) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f712,plain,
( ~ c1_1(a141)
| spl0_66 ),
inference(avatar_component_clause,[],[f710]) ).
fof(f713,plain,
( ~ spl0_66
| spl0_16 ),
inference(avatar_split_clause,[],[f309,f479,f710]) ).
fof(f715,definition,
( spl0_67
<=> c0_1(a141) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f717,plain,
( ~ c0_1(a141)
| spl0_67 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f718,plain,
( ~ spl0_67
| spl0_16 ),
inference(avatar_split_clause,[],[f308,f479,f715]) ).
fof(f721,definition,
( spl0_68
<=> c3_1(a131) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f724,plain,
( spl0_68
| spl0_15 ),
inference(avatar_split_clause,[],[f306,f475,f721]) ).
fof(f726,definition,
( spl0_69
<=> c2_1(a131) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f729,plain,
( spl0_69
| spl0_15 ),
inference(avatar_split_clause,[],[f305,f475,f726]) ).
fof(f731,definition,
( spl0_70
<=> c0_1(a131) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f733,plain,
( ~ c0_1(a131)
| spl0_70 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f734,plain,
( ~ spl0_70
| spl0_15 ),
inference(avatar_split_clause,[],[f304,f475,f731]) ).
fof(f737,definition,
( spl0_71
<=> c2_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f740,plain,
( spl0_71
| spl0_28 ),
inference(avatar_split_clause,[],[f302,f528,f737]) ).
fof(f742,definition,
( spl0_72
<=> c1_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f744,plain,
( ~ c1_1(a128)
| spl0_72 ),
inference(avatar_component_clause,[],[f742]) ).
fof(f745,plain,
( ~ spl0_72
| spl0_28 ),
inference(avatar_split_clause,[],[f301,f528,f742]) ).
fof(f747,definition,
( spl0_73
<=> c0_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f749,plain,
( ~ c0_1(a128)
| spl0_73 ),
inference(avatar_component_clause,[],[f747]) ).
fof(f750,plain,
( ~ spl0_73
| spl0_28 ),
inference(avatar_split_clause,[],[f300,f528,f747]) ).
fof(f753,definition,
( spl0_74
<=> c3_1(a118) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f756,plain,
( spl0_74
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f86,f559,f753]) ).
fof(f758,definition,
( spl0_75
<=> c2_1(a118) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f761,plain,
( spl0_75
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f87,f559,f758]) ).
fof(f763,definition,
( spl0_76
<=> c1_1(a118) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f765,plain,
( ~ c1_1(a118)
| spl0_76 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f766,plain,
( ~ spl0_76
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f298,f559,f763]) ).
fof(f801,definition,
( spl0_83
<=> c2_1(a167) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f804,plain,
( ~ spl0_83
| spl0_3 ),
inference(avatar_split_clause,[],[f291,f420,f801]) ).
fof(f806,definition,
( spl0_84
<=> c0_1(a167) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f808,plain,
( c0_1(a167)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,plain,
( spl0_84
| spl0_3 ),
inference(avatar_split_clause,[],[f290,f420,f806]) ).
fof(f811,definition,
( spl0_85
<=> c1_1(a167) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f813,plain,
( ~ c1_1(a167)
| spl0_85 ),
inference(avatar_component_clause,[],[f811]) ).
fof(f814,plain,
( ~ spl0_85
| spl0_3 ),
inference(avatar_split_clause,[],[f289,f420,f811]) ).
fof(f815,plain,
( ~ spl0_17
| spl0_3 ),
inference(avatar_split_clause,[],[f288,f420,f484]) ).
fof(f817,definition,
( spl0_86
<=> c3_1(a163) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f820,plain,
( ~ spl0_86
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f102,f412,f817]) ).
fof(f822,definition,
( spl0_87
<=> c2_1(a163) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f825,plain,
( ~ spl0_87
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f103,f412,f822]) ).
fof(f827,definition,
( spl0_88
<=> c1_1(a163) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f829,plain,
( c1_1(a163)
| ~ spl0_88 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f830,plain,
( spl0_88
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f287,f412,f827]) ).
fof(f831,plain,
( ~ spl0_17
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f286,f412,f484]) ).
fof(f865,definition,
( spl0_95
<=> c2_1(a143) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f868,plain,
( ~ spl0_95
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f114,f579,f865]) ).
fof(f870,definition,
( spl0_96
<=> c1_1(a143) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f872,plain,
( c1_1(a143)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f873,plain,
( spl0_96
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f278,f579,f870]) ).
fof(f875,definition,
( spl0_97
<=> c3_1(a143) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f878,plain,
( spl0_97
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f116,f579,f875]) ).
fof(f897,definition,
( spl0_101
<=> c3_1(a135) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f900,plain,
( ~ spl0_101
| spl0_19 ),
inference(avatar_split_clause,[],[f272,f492,f897]) ).
fof(f902,definition,
( spl0_102
<=> c2_1(a135) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f905,plain,
( ~ spl0_102
| spl0_19 ),
inference(avatar_split_clause,[],[f271,f492,f902]) ).
fof(f907,definition,
( spl0_103
<=> c0_1(a135) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f909,plain,
( ~ c0_1(a135)
| spl0_103 ),
inference(avatar_component_clause,[],[f907]) ).
fof(f910,plain,
( ~ spl0_103
| spl0_19 ),
inference(avatar_split_clause,[],[f270,f492,f907]) ).
fof(f913,definition,
( spl0_104
<=> c2_1(a134) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f916,plain,
( ~ spl0_104
| spl0_45 ),
inference(avatar_split_clause,[],[f268,f606,f913]) ).
fof(f918,definition,
( spl0_105
<=> c3_1(a134) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f921,plain,
( spl0_105
| spl0_45 ),
inference(avatar_split_clause,[],[f267,f606,f918]) ).
fof(f923,definition,
( spl0_106
<=> c0_1(a134) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f925,plain,
( ~ c0_1(a134)
| spl0_106 ),
inference(avatar_component_clause,[],[f923]) ).
fof(f926,plain,
( ~ spl0_106
| spl0_45 ),
inference(avatar_split_clause,[],[f266,f606,f923]) ).
fof(f929,definition,
( spl0_107
<=> c1_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f931,plain,
( c1_1(a132)
| ~ spl0_107 ),
inference(avatar_component_clause,[],[f929]) ).
fof(f932,plain,
( spl0_107
| spl0_37 ),
inference(avatar_split_clause,[],[f264,f571,f929]) ).
fof(f934,definition,
( spl0_108
<=> c0_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f937,plain,
( spl0_108
| spl0_37 ),
inference(avatar_split_clause,[],[f263,f571,f934]) ).
fof(f939,definition,
( spl0_109
<=> c3_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f942,plain,
( spl0_109
| spl0_37 ),
inference(avatar_split_clause,[],[f262,f571,f939]) ).
fof(f945,definition,
( spl0_110
<=> c2_1(a126) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f948,plain,
( ~ spl0_110
| spl0_12 ),
inference(avatar_split_clause,[],[f260,f461,f945]) ).
fof(f950,definition,
( spl0_111
<=> c3_1(a126) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f953,plain,
( spl0_111
| spl0_12 ),
inference(avatar_split_clause,[],[f259,f461,f950]) ).
fof(f955,definition,
( spl0_112
<=> c1_1(a126) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f957,plain,
( ~ c1_1(a126)
| spl0_112 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f958,plain,
( ~ spl0_112
| spl0_12 ),
inference(avatar_split_clause,[],[f258,f461,f955]) ).
fof(f961,definition,
( spl0_113
<=> c1_1(a117) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f963,plain,
( c1_1(a117)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f961]) ).
fof(f964,plain,
( spl0_113
| spl0_14 ),
inference(avatar_split_clause,[],[f256,f470,f961]) ).
fof(f966,definition,
( spl0_114
<=> c3_1(a117) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f969,plain,
( spl0_114
| spl0_14 ),
inference(avatar_split_clause,[],[f255,f470,f966]) ).
fof(f971,definition,
( spl0_115
<=> c0_1(a117) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f973,plain,
( ~ c0_1(a117)
| spl0_115 ),
inference(avatar_component_clause,[],[f971]) ).
fof(f974,plain,
( ~ spl0_115
| spl0_14 ),
inference(avatar_split_clause,[],[f254,f470,f971]) ).
fof(f977,definition,
( spl0_116
<=> c3_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f980,plain,
( ~ spl0_116
| spl0_57 ),
inference(avatar_split_clause,[],[f252,f661,f977]) ).
fof(f982,definition,
( spl0_117
<=> c2_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f985,plain,
( spl0_117
| spl0_57 ),
inference(avatar_split_clause,[],[f251,f661,f982]) ).
fof(f987,definition,
( spl0_118
<=> c0_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f989,plain,
( ~ c0_1(a116)
| spl0_118 ),
inference(avatar_component_clause,[],[f987]) ).
fof(f990,plain,
( ~ spl0_118
| spl0_57 ),
inference(avatar_split_clause,[],[f250,f661,f987]) ).
fof(f993,definition,
( spl0_119
<=> c3_1(a114) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f996,plain,
( ~ spl0_119
| spl0_13 ),
inference(avatar_split_clause,[],[f248,f466,f993]) ).
fof(f998,definition,
( spl0_120
<=> c2_1(a114) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f1001,plain,
( spl0_120
| spl0_13 ),
inference(avatar_split_clause,[],[f247,f466,f998]) ).
fof(f1003,definition,
( spl0_121
<=> c1_1(a114) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1005,plain,
( ~ c1_1(a114)
| spl0_121 ),
inference(avatar_component_clause,[],[f1003]) ).
fof(f1006,plain,
( ~ spl0_121
| spl0_13 ),
inference(avatar_split_clause,[],[f246,f466,f1003]) ).
fof(f1025,definition,
( spl0_125
<=> c3_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f1028,plain,
( ~ spl0_125
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f154,f434,f1025]) ).
fof(f1030,definition,
( spl0_126
<=> c2_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f1033,plain,
( ~ spl0_126
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f155,f434,f1030]) ).
fof(f1035,definition,
( spl0_127
<=> c1_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f1037,plain,
( ~ c1_1(a112)
| spl0_127 ),
inference(avatar_component_clause,[],[f1035]) ).
fof(f1038,plain,
( ~ spl0_127
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f240,f434,f1035]) ).
fof(f1041,definition,
( spl0_128
<=> c3_1(a111) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f1044,plain,
( ~ spl0_128
| spl0_32 ),
inference(avatar_split_clause,[],[f238,f546,f1041]) ).
fof(f1046,definition,
( spl0_129
<=> c2_1(a111) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f1049,plain,
( ~ spl0_129
| spl0_32 ),
inference(avatar_split_clause,[],[f237,f546,f1046]) ).
fof(f1051,definition,
( spl0_130
<=> c0_1(a111) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f1053,plain,
( c0_1(a111)
| ~ spl0_130 ),
inference(avatar_component_clause,[],[f1051]) ).
fof(f1054,plain,
( spl0_130
| spl0_32 ),
inference(avatar_split_clause,[],[f236,f546,f1051]) ).
fof(f1057,definition,
( spl0_131
<=> c3_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1060,plain,
( ~ spl0_131
| spl0_10 ),
inference(avatar_split_clause,[],[f234,f452,f1057]) ).
fof(f1062,definition,
( spl0_132
<=> c1_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1064,plain,
( c1_1(a110)
| ~ spl0_132 ),
inference(avatar_component_clause,[],[f1062]) ).
fof(f1065,plain,
( spl0_132
| spl0_10 ),
inference(avatar_split_clause,[],[f233,f452,f1062]) ).
fof(f1067,definition,
( spl0_133
<=> c2_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1070,plain,
( spl0_133
| spl0_10 ),
inference(avatar_split_clause,[],[f232,f452,f1067]) ).
fof(f1073,definition,
( spl0_134
<=> c3_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f1076,plain,
( ~ spl0_134
| spl0_4 ),
inference(avatar_split_clause,[],[f230,f425,f1073]) ).
fof(f1078,definition,
( spl0_135
<=> c0_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f1080,plain,
( c0_1(a109)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f1078]) ).
fof(f1081,plain,
( spl0_135
| spl0_4 ),
inference(avatar_split_clause,[],[f229,f425,f1078]) ).
fof(f1083,definition,
( spl0_136
<=> c1_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f1085,plain,
( ~ c1_1(a109)
| spl0_136 ),
inference(avatar_component_clause,[],[f1083]) ).
fof(f1086,plain,
( ~ spl0_136
| spl0_4 ),
inference(avatar_split_clause,[],[f228,f425,f1083]) ).
fof(f1087,plain,
( ~ spl0_17
| spl0_4 ),
inference(avatar_split_clause,[],[f227,f425,f484]) ).
fof(f1121,definition,
( spl0_143
<=> c2_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1124,plain,
( ~ spl0_143
| spl0_11 ),
inference(avatar_split_clause,[],[f219,f456,f1121]) ).
fof(f1126,definition,
( spl0_144
<=> c1_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1128,plain,
( ~ c1_1(a106)
| spl0_144 ),
inference(avatar_component_clause,[],[f1126]) ).
fof(f1129,plain,
( ~ spl0_144
| spl0_11 ),
inference(avatar_split_clause,[],[f218,f456,f1126]) ).
fof(f1131,definition,
( spl0_145
<=> c0_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1133,plain,
( ~ c0_1(a106)
| spl0_145 ),
inference(avatar_component_clause,[],[f1131]) ).
fof(f1134,plain,
( ~ spl0_145
| spl0_11 ),
inference(avatar_split_clause,[],[f217,f456,f1131]) ).
fof(f1137,definition,
( spl0_146
<=> c1_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1139,plain,
( c1_1(a105)
| ~ spl0_146 ),
inference(avatar_component_clause,[],[f1137]) ).
fof(f1140,plain,
( spl0_146
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f215,f430,f1137]) ).
fof(f1142,definition,
( spl0_147
<=> c3_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1145,plain,
( spl0_147
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f183,f430,f1142]) ).
fof(f1147,definition,
( spl0_148
<=> c2_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1150,plain,
( spl0_148
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f184,f430,f1147]) ).
fof(f1185,definition,
( spl0_155
<=> c1_1(a102) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1187,plain,
( c1_1(a102)
| ~ spl0_155 ),
inference(avatar_component_clause,[],[f1185]) ).
fof(f1188,plain,
( spl0_155
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f206,f508,f1185]) ).
fof(f1190,definition,
( spl0_156
<=> c0_1(a102) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f1192,plain,
( c0_1(a102)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1193,plain,
( spl0_156
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f205,f508,f1190]) ).
fof(f1195,definition,
( spl0_157
<=> c2_1(a102) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1198,plain,
( spl0_157
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f196,f508,f1195]) ).
fof(f1201,definition,
( spl0_158
<=> c0_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f1203,plain,
( c0_1(a101)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f1201]) ).
fof(f1204,plain,
( spl0_158
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f203,f443,f1201]) ).
fof(f1206,definition,
( spl0_159
<=> c3_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1209,plain,
( spl0_159
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f199,f443,f1206]) ).
fof(f1211,definition,
( spl0_160
<=> c2_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1214,plain,
( spl0_160
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f200,f443,f1211]) ).
fof(f1237,plain,
( ~ c3_1(a131)
| ~ c2_1(a131)
| ~ spl0_20
| spl0_70 ),
inference(resolution,[],[f497,f733]) ).
fof(f1238,plain,
( ~ c3_1(a141)
| ~ c2_1(a141)
| ~ spl0_20
| spl0_67 ),
inference(resolution,[],[f497,f717]) ).
fof(f1240,definition,
( spl0_161
<=> c2_1(a141) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1265,plain,
( ~ c2_1(a128)
| c3_1(a128)
| ~ spl0_21
| spl0_72 ),
inference(resolution,[],[f501,f744]) ).
fof(f1283,definition,
( spl0_165
<=> c2_1(a117) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1288,definition,
( spl0_166
<=> c2_1(a109) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1306,plain,
( ~ c3_1(a106)
| c2_1(a106)
| ~ spl0_26
| spl0_145 ),
inference(resolution,[],[f521,f1133]) ).
fof(f1313,plain,
( ~ c3_1(a117)
| c2_1(a117)
| ~ spl0_26
| spl0_115 ),
inference(resolution,[],[f521,f973]) ).
fof(f1315,plain,
( ~ c3_1(a134)
| c2_1(a134)
| ~ spl0_26
| spl0_106 ),
inference(resolution,[],[f521,f925]) ).
fof(f1324,plain,
( ~ c3_1(a141)
| c2_1(a141)
| ~ spl0_26
| spl0_67 ),
inference(resolution,[],[f521,f717]) ).
fof(f1327,definition,
( spl0_169
<=> c3_1(a128) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1347,definition,
( spl0_173
<=> c3_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1357,definition,
( spl0_175
<=> c3_1(a102) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1381,plain,
( ~ c3_1(a167)
| c2_1(a167)
| ~ spl0_24
| spl0_85 ),
inference(resolution,[],[f513,f813]) ).
fof(f1386,definition,
( spl0_176
<=> c3_1(a167) ),
introduced(definition,[new_symbols(definition,[spl0_176])],[avatar_definition]) ).
fof(f1394,plain,
( c2_1(a106)
| c0_1(a106)
| ~ spl0_27
| spl0_144 ),
inference(resolution,[],[f525,f1128]) ).
fof(f1412,plain,
( c2_1(a141)
| c0_1(a141)
| ~ spl0_27
| spl0_66 ),
inference(resolution,[],[f525,f712]) ).
fof(f1413,plain,
( spl0_67
| spl0_161
| ~ spl0_27
| spl0_66 ),
inference(avatar_split_clause,[],[f1412,f710,f524,f1240,f715]) ).
fof(f1421,definition,
( spl0_178
<=> c0_1(a163) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f1422,plain,
( ~ c0_1(a163)
| spl0_178 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1423,plain,
( c0_1(a163)
| ~ spl0_178 ),
inference(avatar_component_clause,[],[f1421]) ).
fof(f1428,definition,
( spl0_179
<=> c0_1(a143) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f1429,plain,
( ~ c0_1(a143)
| spl0_179 ),
inference(avatar_component_clause,[],[f1428]) ).
fof(f1435,definition,
( spl0_180
<=> c0_1(a126) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f1437,plain,
( c0_1(a126)
| ~ spl0_180 ),
inference(avatar_component_clause,[],[f1435]) ).
fof(f1441,definition,
( spl0_181
<=> c0_1(a114) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1442,plain,
( ~ c0_1(a114)
| spl0_181 ),
inference(avatar_component_clause,[],[f1441]) ).
fof(f1451,definition,
( spl0_183
<=> c0_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1453,plain,
( c0_1(a110)
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1460,definition,
( spl0_184
<=> c0_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_184])],[avatar_definition]) ).
fof(f1462,plain,
( c0_1(a105)
| ~ spl0_184 ),
inference(avatar_component_clause,[],[f1460]) ).
fof(f1468,plain,
( spl0_165
| ~ spl0_114
| ~ spl0_26
| spl0_115 ),
inference(avatar_split_clause,[],[f1313,f971,f520,f966,f1283]) ).
fof(f1476,plain,
( ~ c3_1(a143)
| c2_1(a143)
| ~ spl0_26
| spl0_179 ),
inference(resolution,[],[f1429,f521]) ).
fof(f1484,plain,
( ~ c3_1(a117)
| c0_1(a117)
| ~ spl0_33
| ~ spl0_113 ),
inference(resolution,[],[f551,f963]) ).
fof(f1510,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_33
| ~ spl0_41 ),
inference(resolution,[],[f588,f551]) ).
fof(f1523,plain,
( ~ c2_1(a128)
| c0_1(a128)
| ~ spl0_41
| spl0_72 ),
inference(resolution,[],[f588,f744]) ).
fof(f1524,plain,
( ! [X0] :
( ~ c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_33
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f1510]) ).
fof(f1532,plain,
( spl0_20
| ~ spl0_33
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1524,f587,f550,f496]) ).
fof(f1540,plain,
( ~ c2_1(a116)
| c3_1(a116)
| ~ spl0_42
| spl0_118 ),
inference(resolution,[],[f592,f989]) ).
fof(f1554,plain,
( ~ c2_1(a128)
| c3_1(a128)
| ~ spl0_42
| spl0_73 ),
inference(resolution,[],[f592,f749]) ).
fof(f1565,plain,
( ~ c2_1(a102)
| c3_1(a102)
| ~ spl0_44
| ~ spl0_155 ),
inference(resolution,[],[f602,f1187]) ).
fof(f1568,plain,
( ~ c2_1(a110)
| c3_1(a110)
| ~ spl0_44
| ~ spl0_132 ),
inference(resolution,[],[f602,f1064]) ).
fof(f1578,plain,
( ~ c2_1(a105)
| c0_1(a105)
| ~ spl0_40
| ~ spl0_146 ),
inference(resolution,[],[f1139,f584]) ).
fof(f1579,plain,
( ~ c3_1(a105)
| c0_1(a105)
| ~ spl0_33
| ~ spl0_146 ),
inference(resolution,[],[f1139,f551]) ).
fof(f1580,plain,
( ! [X0] :
( c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_27
| ~ spl0_46 ),
inference(resolution,[],[f611,f525]) ).
fof(f1594,plain,
( ! [X0] :
( c0_1(X0)
| c3_1(X0)
| c2_1(X0) )
| ~ spl0_27
| ~ spl0_46 ),
inference(duplicate_literal_removal,[],[f1580]) ).
fof(f1605,plain,
( spl0_31
| ~ spl0_27
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f1594,f610,f524,f542]) ).
fof(f1607,plain,
( spl0_104
| ~ spl0_105
| ~ spl0_26
| spl0_106 ),
inference(avatar_split_clause,[],[f1315,f923,f520,f918,f913]) ).
fof(f1674,plain,
( c2_1(a135)
| c3_1(a135)
| ~ spl0_31
| spl0_103 ),
inference(resolution,[],[f543,f909]) ).
fof(f1677,plain,
( c2_1(a163)
| c3_1(a163)
| ~ spl0_31
| spl0_178 ),
inference(resolution,[],[f543,f1422]) ).
fof(f1684,plain,
( spl0_101
| spl0_102
| ~ spl0_31
| spl0_103 ),
inference(avatar_split_clause,[],[f1674,f907,f542,f902,f897]) ).
fof(f1698,plain,
( c2_1(a106)
| c3_1(a106)
| ~ spl0_30
| spl0_144 ),
inference(resolution,[],[f539,f1128]) ).
fof(f1701,plain,
( c2_1(a109)
| c3_1(a109)
| ~ spl0_30
| spl0_136 ),
inference(resolution,[],[f539,f1085]) ).
fof(f1702,plain,
( c2_1(a112)
| c3_1(a112)
| ~ spl0_30
| spl0_127 ),
inference(resolution,[],[f539,f1037]) ).
fof(f1709,plain,
( c2_1(a167)
| c3_1(a167)
| ~ spl0_30
| spl0_85 ),
inference(resolution,[],[f539,f813]) ).
fof(f1714,plain,
( spl0_176
| spl0_83
| ~ spl0_30
| spl0_85 ),
inference(avatar_split_clause,[],[f1709,f811,f538,f801,f1386]) ).
fof(f1717,plain,
( spl0_134
| spl0_166
| ~ spl0_30
| spl0_136 ),
inference(avatar_split_clause,[],[f1701,f1083,f538,f1288,f1073]) ).
fof(f1720,plain,
( spl0_173
| spl0_143
| ~ spl0_30
| spl0_144 ),
inference(avatar_split_clause,[],[f1698,f1126,f538,f1121,f1347]) ).
fof(f1734,plain,
( ~ c3_1(a117)
| ~ c2_1(a117)
| ~ spl0_20
| spl0_115 ),
inference(resolution,[],[f497,f973]) ).
fof(f1738,plain,
( ~ c3_1(a128)
| ~ c2_1(a128)
| ~ spl0_20
| spl0_73 ),
inference(resolution,[],[f497,f749]) ).
fof(f1745,plain,
( c0_1(a110)
| c3_1(a110)
| ~ spl0_46
| ~ spl0_132 ),
inference(resolution,[],[f611,f1064]) ).
fof(f1791,plain,
( c2_1(a126)
| c0_1(a126)
| ~ spl0_27
| spl0_112 ),
inference(resolution,[],[f957,f525]) ).
fof(f1793,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_27
| ~ spl0_49 ),
inference(resolution,[],[f626,f525]) ).
fof(f1803,plain,
( ! [X0] :
( c3_1(X0)
| c2_1(X0)
| c0_1(X0) )
| ~ spl0_27
| ~ spl0_49 ),
inference(duplicate_literal_removal,[],[f1793]) ).
fof(f1816,plain,
( ~ c3_1(a101)
| ~ c2_1(a101)
| ~ spl0_50
| ~ spl0_158 ),
inference(resolution,[],[f630,f1203]) ).
fof(f1819,plain,
( ~ c3_1(a105)
| ~ c2_1(a105)
| ~ spl0_50
| ~ spl0_184 ),
inference(resolution,[],[f630,f1462]) ).
fof(f1846,plain,
( ~ spl0_148
| ~ spl0_147
| ~ spl0_50
| ~ spl0_184 ),
inference(avatar_split_clause,[],[f1819,f1460,f629,f1142,f1147]) ).
fof(f1850,plain,
( spl0_116
| ~ spl0_117
| ~ spl0_42
| spl0_118 ),
inference(avatar_split_clause,[],[f1540,f987,f591,f982,f977]) ).
fof(f1854,plain,
( spl0_169
| ~ spl0_71
| ~ spl0_42
| spl0_73 ),
inference(avatar_split_clause,[],[f1554,f747,f591,f737,f1327]) ).
fof(f1892,plain,
( ~ c2_1(a102)
| c3_1(a102)
| ~ spl0_53
| ~ spl0_156 ),
inference(resolution,[],[f644,f1192]) ).
fof(f1898,plain,
( ~ c2_1(a109)
| c3_1(a109)
| ~ spl0_53
| ~ spl0_135 ),
inference(resolution,[],[f644,f1080]) ).
fof(f1899,plain,
( ~ c2_1(a110)
| c3_1(a110)
| ~ spl0_53
| ~ spl0_183 ),
inference(resolution,[],[f644,f1453]) ).
fof(f1931,plain,
( ~ c0_1(a109)
| c3_1(a109)
| ~ spl0_54
| spl0_136 ),
inference(resolution,[],[f648,f1085]) ).
fof(f1950,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| c0_1(X0) )
| ~ spl0_33
| ~ spl0_55 ),
inference(resolution,[],[f652,f551]) ).
fof(f1951,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_40
| ~ spl0_55 ),
inference(resolution,[],[f652,f584]) ).
fof(f1954,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_47
| ~ spl0_55 ),
inference(resolution,[],[f652,f616]) ).
fof(f1955,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| c2_1(X0) )
| ~ spl0_48
| ~ spl0_55 ),
inference(resolution,[],[f652,f622]) ).
fof(f1957,plain,
( ~ c3_1(a106)
| c0_1(a106)
| ~ spl0_55
| spl0_144 ),
inference(resolution,[],[f652,f1128]) ).
fof(f1963,plain,
( ~ c3_1(a126)
| c0_1(a126)
| ~ spl0_55
| spl0_112 ),
inference(resolution,[],[f652,f957]) ).
fof(f1970,plain,
( ~ c3_1(a128)
| c0_1(a128)
| ~ spl0_55
| spl0_72 ),
inference(resolution,[],[f652,f744]) ).
fof(f1971,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_48
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f1955]) ).
fof(f1972,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| c2_1(X0) )
| ~ spl0_47
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f1954]) ).
fof(f1974,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_40
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f1951]) ).
fof(f1975,plain,
( ! [X0] :
( c0_1(X0)
| ~ c3_1(X0) )
| ~ spl0_33
| ~ spl0_55 ),
inference(duplicate_literal_removal,[],[f1950]) ).
fof(f1979,plain,
( ~ c3_1(a117)
| ~ spl0_33
| ~ spl0_55
| spl0_115 ),
inference(resolution,[],[f1975,f973]) ).
fof(f2000,plain,
( ~ c3_1(a126)
| c2_1(a126)
| ~ spl0_56
| ~ spl0_180 ),
inference(resolution,[],[f658,f1437]) ).
fof(f2008,plain,
( ~ c3_1(a167)
| c2_1(a167)
| ~ spl0_56
| ~ spl0_84 ),
inference(resolution,[],[f658,f808]) ).
fof(f2029,plain,
( ~ spl0_114
| ~ spl0_33
| ~ spl0_55
| spl0_115 ),
inference(avatar_split_clause,[],[f1979,f971,f651,f550,f966]) ).
fof(f2036,plain,
( ~ c3_1(a102)
| ~ c0_1(a102)
| ~ spl0_60
| ~ spl0_155 ),
inference(resolution,[],[f675,f1187]) ).
fof(f2038,plain,
( ~ c3_1(a105)
| ~ c0_1(a105)
| ~ spl0_60
| ~ spl0_146 ),
inference(resolution,[],[f675,f1139]) ).
fof(f2053,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| c3_1(X0) )
| ~ spl0_30
| ~ spl0_62 ),
inference(resolution,[],[f687,f539]) ).
fof(f2055,plain,
( c3_1(a102)
| ~ c0_1(a102)
| ~ spl0_62
| ~ spl0_155 ),
inference(resolution,[],[f687,f1187]) ).
fof(f2059,plain,
( c3_1(a110)
| ~ c0_1(a110)
| ~ spl0_62
| ~ spl0_132 ),
inference(resolution,[],[f687,f1064]) ).
fof(f2061,plain,
( c3_1(a163)
| ~ c0_1(a163)
| ~ spl0_62
| ~ spl0_88 ),
inference(resolution,[],[f687,f829]) ).
fof(f2063,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_30
| ~ spl0_62 ),
inference(duplicate_literal_removal,[],[f2053]) ).
fof(f2071,plain,
( spl0_59
| ~ spl0_30
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f2063,f686,f538,f670]) ).
fof(f2078,plain,
( spl0_161
| ~ spl0_65
| ~ spl0_26
| spl0_67 ),
inference(avatar_split_clause,[],[f1324,f715,f520,f705,f1240]) ).
fof(f2091,plain,
( spl0_143
| ~ spl0_173
| ~ spl0_26
| spl0_145 ),
inference(avatar_split_clause,[],[f1306,f1131,f520,f1347,f1121]) ).
fof(f2098,plain,
( spl0_110
| ~ spl0_111
| ~ spl0_56
| ~ spl0_180 ),
inference(avatar_split_clause,[],[f2000,f1435,f657,f950,f945]) ).
fof(f2104,plain,
( spl0_20
| ~ spl0_40
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1974,f651,f583,f496]) ).
fof(f2112,plain,
( spl0_169
| ~ spl0_71
| ~ spl0_21
| spl0_72 ),
inference(avatar_split_clause,[],[f1265,f742,f500,f737,f1327]) ).
fof(f2116,plain,
( spl0_83
| ~ spl0_176
| ~ spl0_56
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f2008,f806,f657,f1386,f801]) ).
fof(f2133,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_18
| ~ spl0_40 ),
inference(resolution,[],[f489,f584]) ).
fof(f2154,plain,
( ~ c3_1(a118)
| ~ c2_1(a118)
| ~ spl0_18
| spl0_76 ),
inference(resolution,[],[f489,f765]) ).
fof(f2156,plain,
( ~ c3_1(a141)
| ~ c2_1(a141)
| ~ spl0_18
| spl0_66 ),
inference(resolution,[],[f489,f712]) ).
fof(f2158,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) )
| ~ spl0_18
| ~ spl0_40 ),
inference(duplicate_literal_removal,[],[f2133]) ).
fof(f2159,plain,
( ~ spl0_161
| ~ spl0_65
| ~ spl0_18
| spl0_66 ),
inference(avatar_split_clause,[],[f2156,f710,f488,f705,f1240]) ).
fof(f2161,plain,
( ~ spl0_75
| ~ spl0_74
| ~ spl0_18
| spl0_76 ),
inference(avatar_split_clause,[],[f2154,f763,f488,f753,f758]) ).
fof(f2170,plain,
( spl0_20
| ~ spl0_18
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f2158,f583,f488,f496]) ).
fof(f2171,plain,
( ~ spl0_156
| ~ spl0_175
| ~ spl0_60
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f2036,f1185,f674,f1357,f1190]) ).
fof(f2316,plain,
( c3_1(a109)
| c2_1(a109)
| ~ spl0_59
| ~ spl0_135 ),
inference(resolution,[],[f671,f1080]) ).
fof(f2318,plain,
( c3_1(a111)
| c2_1(a111)
| ~ spl0_59
| ~ spl0_130 ),
inference(resolution,[],[f671,f1053]) ).
fof(f2328,plain,
( c3_1(a163)
| c2_1(a163)
| ~ spl0_59
| ~ spl0_178 ),
inference(resolution,[],[f671,f1423]) ).
fof(f2358,plain,
( spl0_134
| ~ spl0_135
| ~ spl0_54
| spl0_136 ),
inference(avatar_split_clause,[],[f1931,f1083,f647,f1078,f1073]) ).
fof(f2361,plain,
( spl0_166
| spl0_134
| ~ spl0_59
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f2316,f1078,f670,f1073,f1288]) ).
fof(f2364,plain,
( spl0_87
| spl0_86
| ~ spl0_59
| ~ spl0_178 ),
inference(avatar_split_clause,[],[f2328,f1421,f670,f817,f822]) ).
fof(f2378,plain,
( ~ c2_1(a110)
| c0_1(a110)
| ~ spl0_40
| ~ spl0_132 ),
inference(resolution,[],[f584,f1064]) ).
fof(f2382,plain,
( ~ c2_1(a114)
| c3_1(a114)
| ~ spl0_42
| spl0_181 ),
inference(resolution,[],[f1442,f592]) ).
fof(f2384,plain,
( spl0_119
| ~ spl0_120
| ~ spl0_42
| spl0_181 ),
inference(avatar_split_clause,[],[f2382,f1441,f591,f998,f993]) ).
fof(f2389,plain,
( c0_1(a163)
| c2_1(a163)
| ~ spl0_47
| ~ spl0_88 ),
inference(resolution,[],[f829,f616]) ).
fof(f2390,plain,
( c3_1(a163)
| c2_1(a163)
| ~ spl0_49
| ~ spl0_88 ),
inference(resolution,[],[f829,f626]) ).
fof(f2401,plain,
( ~ c2_1(a109)
| c3_1(a109)
| ~ spl0_21
| spl0_136 ),
inference(resolution,[],[f501,f1085]) ).
fof(f2403,plain,
( ~ c2_1(a114)
| c3_1(a114)
| ~ spl0_21
| spl0_121 ),
inference(resolution,[],[f501,f1005]) ).
fof(f2428,plain,
( ~ c0_1(a114)
| c3_1(a114)
| ~ spl0_54
| spl0_121 ),
inference(resolution,[],[f648,f1005]) ).
fof(f2433,plain,
( ~ c0_1(a167)
| c3_1(a167)
| ~ spl0_54
| spl0_85 ),
inference(resolution,[],[f648,f813]) ).
fof(f2451,plain,
( c3_1(a111)
| c2_1(a111)
| ~ spl0_59
| ~ spl0_130 ),
inference(resolution,[],[f671,f1053]) ).
fof(f2471,plain,
( ~ c3_1(a132)
| ~ c0_1(a132)
| ~ spl0_60
| ~ spl0_107 ),
inference(resolution,[],[f675,f931]) ).
fof(f2473,plain,
( ~ c3_1(a143)
| ~ c0_1(a143)
| ~ spl0_60
| ~ spl0_96 ),
inference(resolution,[],[f675,f872]) ).
fof(f2481,plain,
( ~ c2_1(a102)
| ~ c0_1(a102)
| ~ spl0_61
| ~ spl0_155 ),
inference(resolution,[],[f683,f1187]) ).
fof(f2494,plain,
( ~ spl0_156
| ~ spl0_157
| ~ spl0_61
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f2481,f1185,f682,f1195,f1190]) ).
fof(f2503,plain,
( spl0_83
| ~ spl0_176
| ~ spl0_24
| spl0_85 ),
inference(avatar_split_clause,[],[f1381,f811,f512,f1386,f801]) ).
fof(f2507,plain,
( spl0_31
| ~ spl0_27
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f1803,f625,f524,f542]) ).
fof(f2512,plain,
( spl0_73
| ~ spl0_71
| ~ spl0_41
| spl0_72 ),
inference(avatar_split_clause,[],[f1523,f742,f587,f737,f747]) ).
fof(f2513,plain,
( ~ spl0_160
| ~ spl0_159
| ~ spl0_50
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f1816,f1201,f629,f1206,f1211]) ).
fof(f2522,plain,
( spl0_73
| ~ spl0_169
| ~ spl0_55
| spl0_72 ),
inference(avatar_split_clause,[],[f1970,f742,f651,f1327,f747]) ).
fof(f2528,plain,
( ~ spl0_179
| ~ spl0_97
| ~ spl0_60
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f2473,f870,f674,f875,f1428]) ).
fof(f2529,plain,
( ~ spl0_184
| ~ spl0_147
| ~ spl0_60
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f2038,f1137,f674,f1142,f1460]) ).
fof(f2531,plain,
( spl0_95
| ~ spl0_97
| ~ spl0_26
| spl0_179 ),
inference(avatar_split_clause,[],[f1476,f1428,f520,f875,f865]) ).
fof(f2532,plain,
( ~ spl0_108
| ~ spl0_109
| ~ spl0_60
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f2471,f929,f674,f939,f934]) ).
fof(f2541,plain,
( ~ spl0_69
| ~ spl0_68
| ~ spl0_20
| spl0_70 ),
inference(avatar_split_clause,[],[f1237,f731,f496,f721,f726]) ).
fof(f2542,plain,
( ~ spl0_165
| ~ spl0_114
| ~ spl0_20
| spl0_115 ),
inference(avatar_split_clause,[],[f1734,f971,f496,f966,f1283]) ).
fof(f2544,plain,
( ~ spl0_71
| ~ spl0_169
| ~ spl0_20
| spl0_73 ),
inference(avatar_split_clause,[],[f1738,f747,f496,f1327,f737]) ).
fof(f2545,plain,
( spl0_115
| ~ spl0_114
| ~ spl0_33
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f1484,f961,f550,f966,f971]) ).
fof(f2549,plain,
( spl0_184
| ~ spl0_147
| ~ spl0_33
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f1579,f1137,f550,f1142,f1460]) ).
fof(f2559,plain,
( spl0_184
| ~ spl0_148
| ~ spl0_40
| ~ spl0_146 ),
inference(avatar_split_clause,[],[f1578,f1137,f583,f1147,f1460]) ).
fof(f2564,plain,
( spl0_175
| ~ spl0_157
| ~ spl0_44
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f1565,f1185,f601,f1195,f1357]) ).
fof(f2574,plain,
( spl0_134
| ~ spl0_166
| ~ spl0_53
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1898,f1078,f643,f1288,f1073]) ).
fof(f2584,plain,
( spl0_119
| ~ spl0_181
| ~ spl0_54
| spl0_121 ),
inference(avatar_split_clause,[],[f2428,f1003,f647,f1441,f993]) ).
fof(f2587,plain,
( spl0_176
| ~ spl0_84
| ~ spl0_54
| spl0_85 ),
inference(avatar_split_clause,[],[f2433,f811,f647,f806,f1386]) ).
fof(f2591,plain,
( ~ spl0_156
| spl0_175
| ~ spl0_62
| ~ spl0_155 ),
inference(avatar_split_clause,[],[f2055,f1185,f686,f1357,f1190]) ).
fof(f2597,plain,
( spl0_87
| spl0_178
| ~ spl0_47
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f2389,f827,f615,f1421,f822]) ).
fof(f2607,plain,
( spl0_134
| ~ spl0_166
| ~ spl0_21
| spl0_136 ),
inference(avatar_split_clause,[],[f2401,f1083,f500,f1288,f1073]) ).
fof(f2608,plain,
( spl0_119
| ~ spl0_120
| ~ spl0_21
| spl0_121 ),
inference(avatar_split_clause,[],[f2403,f1003,f500,f998,f993]) ).
fof(f2616,plain,
( spl0_131
| spl0_183
| ~ spl0_46
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1745,f1062,f610,f1451,f1057]) ).
fof(f2625,plain,
( spl0_87
| spl0_86
| ~ spl0_49
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f2390,f827,f625,f817,f822]) ).
fof(f2627,plain,
( spl0_145
| ~ spl0_173
| ~ spl0_55
| spl0_144 ),
inference(avatar_split_clause,[],[f1957,f1126,f651,f1347,f1131]) ).
fof(f2628,plain,
( spl0_180
| ~ spl0_111
| ~ spl0_55
| spl0_112 ),
inference(avatar_split_clause,[],[f1963,f955,f651,f950,f1435]) ).
fof(f2629,plain,
( spl0_26
| ~ spl0_48
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1971,f651,f621,f520]) ).
fof(f2630,plain,
( spl0_26
| ~ spl0_47
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f1972,f651,f615,f520]) ).
fof(f2631,plain,
( ~ spl0_161
| ~ spl0_65
| ~ spl0_20
| spl0_67 ),
inference(avatar_split_clause,[],[f1238,f715,f496,f705,f1240]) ).
fof(f2635,plain,
( spl0_183
| ~ spl0_133
| ~ spl0_40
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f2378,f1062,f583,f1067,f1451]) ).
fof(f2636,plain,
( spl0_175
| ~ spl0_157
| ~ spl0_53
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f1892,f1190,f643,f1195,f1357]) ).
fof(f2638,plain,
( spl0_131
| ~ spl0_133
| ~ spl0_53
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f1899,f1451,f643,f1067,f1057]) ).
fof(f2640,plain,
( spl0_145
| spl0_143
| ~ spl0_27
| spl0_144 ),
inference(avatar_split_clause,[],[f1394,f1126,f524,f1121,f1131]) ).
fof(f2644,plain,
( spl0_180
| spl0_110
| ~ spl0_27
| spl0_112 ),
inference(avatar_split_clause,[],[f1791,f955,f524,f945,f1435]) ).
fof(f2645,plain,
( spl0_125
| spl0_126
| ~ spl0_30
| spl0_127 ),
inference(avatar_split_clause,[],[f1702,f1035,f538,f1030,f1025]) ).
fof(f2647,plain,
( spl0_86
| spl0_87
| ~ spl0_31
| spl0_178 ),
inference(avatar_split_clause,[],[f1677,f1421,f542,f822,f817]) ).
fof(f2649,plain,
( spl0_131
| ~ spl0_133
| ~ spl0_44
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f1568,f1062,f601,f1067,f1057]) ).
fof(f2655,plain,
( spl0_129
| spl0_128
| ~ spl0_59
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f2318,f1051,f670,f1041,f1046]) ).
fof(f2659,plain,
( spl0_129
| spl0_128
| ~ spl0_59
| ~ spl0_130 ),
inference(avatar_split_clause,[],[f2451,f1051,f670,f1041,f1046]) ).
fof(f2663,plain,
( ~ spl0_183
| spl0_131
| ~ spl0_62
| ~ spl0_132 ),
inference(avatar_split_clause,[],[f2059,f1062,f686,f1057,f1451]) ).
fof(f2665,plain,
( ~ spl0_178
| spl0_86
| ~ spl0_62
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f2061,f827,f686,f817,f1421]) ).
cnf(s2,plain,
( ~ spl0_3
| ~ spl0_4 ),
inference(sat_conversion,[],[f428]) ).
cnf(s5,plain,
( spl0_5
| ~ spl0_10
| ~ spl0_11 ),
inference(sat_conversion,[],[f459]) ).
cnf(s7,plain,
( ~ spl0_11
| ~ spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f473]) ).
cnf(s8,plain,
( spl0_1
| ~ spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f482]) ).
cnf(s10,plain,
( spl0_6
| spl0_17
| ~ spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f498]) ).
cnf(s15,plain,
( spl0_1
| spl0_17
| spl0_23
| spl0_27 ),
inference(sat_conversion,[],[f526]) ).
cnf(s16,plain,
( spl0_5
| spl0_17
| spl0_27
| ~ spl0_28 ),
inference(sat_conversion,[],[f531]) ).
cnf(s18,plain,
( spl0_17
| ~ spl0_19
| spl0_30 ),
inference(sat_conversion,[],[f540]) ).
cnf(s22,plain,
( spl0_6
| spl0_17
| spl0_33
| spl0_35 ),
inference(sat_conversion,[],[f562]) ).
cnf(s24,plain,
( ~ spl0_16
| spl0_17
| spl0_33
| spl0_35 ),
inference(sat_conversion,[],[f564]) ).
cnf(s27,plain,
( spl0_17
| ~ spl0_28
| spl0_39
| spl0_40 ),
inference(sat_conversion,[],[f585]) ).
cnf(s28,plain,
( ~ spl0_16
| spl0_17
| spl0_40
| spl0_41 ),
inference(sat_conversion,[],[f589]) ).
cnf(s29,plain,
( spl0_17
| ~ spl0_37
| spl0_40
| spl0_42 ),
inference(sat_conversion,[],[f593]) ).
cnf(s30,plain,
( spl0_17
| spl0_26
| spl0_27
| spl0_40 ),
inference(sat_conversion,[],[f594]) ).
cnf(s33,plain,
( spl0_17
| ~ spl0_19
| ~ spl0_37
| spl0_44 ),
inference(sat_conversion,[],[f604]) ).
cnf(s34,plain,
( spl0_17
| spl0_21
| ~ spl0_45
| spl0_46 ),
inference(sat_conversion,[],[f612]) ).
cnf(s35,plain,
( spl0_17
| spl0_20
| spl0_24
| spl0_46 ),
inference(sat_conversion,[],[f613]) ).
cnf(s37,plain,
( spl0_17
| spl0_27
| ~ spl0_37
| spl0_47 ),
inference(sat_conversion,[],[f618]) ).
cnf(s38,plain,
( ~ spl0_15
| spl0_17
| spl0_44
| spl0_47 ),
inference(sat_conversion,[],[f619]) ).
cnf(s40,plain,
( spl0_17
| spl0_18
| spl0_31
| spl0_49 ),
inference(sat_conversion,[],[f627]) ).
cnf(s41,plain,
( spl0_6
| spl0_17
| ~ spl0_28
| spl0_50 ),
inference(sat_conversion,[],[f631]) ).
cnf(s43,plain,
( ~ spl0_12
| spl0_17
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f633]) ).
cnf(s45,plain,
( spl0_8
| ~ spl0_14
| spl0_17
| spl0_53 ),
inference(sat_conversion,[],[f645]) ).
cnf(s46,plain,
( ~ spl0_14
| spl0_17
| ~ spl0_32
| spl0_54 ),
inference(sat_conversion,[],[f649]) ).
cnf(s47,plain,
( ~ spl0_4
| spl0_17
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f653]) ).
cnf(s48,plain,
( spl0_17
| spl0_21
| spl0_31
| spl0_54 ),
inference(sat_conversion,[],[f654]) ).
cnf(s49,plain,
( spl0_17
| spl0_33
| spl0_48
| spl0_54 ),
inference(sat_conversion,[],[f655]) ).
cnf(s50,plain,
( ~ spl0_14
| spl0_17
| spl0_35
| spl0_56 ),
inference(sat_conversion,[],[f659]) ).
cnf(s51,plain,
( spl0_17
| spl0_40
| spl0_56
| ~ spl0_57 ),
inference(sat_conversion,[],[f664]) ).
cnf(s53,plain,
( ~ spl0_13
| spl0_17
| spl0_55
| spl0_59 ),
inference(sat_conversion,[],[f672]) ).
cnf(s54,plain,
( spl0_17
| spl0_18
| spl0_20
| spl0_60 ),
inference(sat_conversion,[],[f676]) ).
cnf(s56,plain,
( spl0_6
| spl0_17
| spl0_30
| spl0_60 ),
inference(sat_conversion,[],[f678]) ).
cnf(s57,plain,
( spl0_17
| spl0_27
| spl0_47
| spl0_60 ),
inference(sat_conversion,[],[f679]) ).
cnf(s58,plain,
( spl0_17
| spl0_55
| spl0_56
| spl0_60 ),
inference(sat_conversion,[],[f680]) ).
cnf(s59,plain,
( spl0_17
| ~ spl0_32
| spl0_55
| spl0_61 ),
inference(sat_conversion,[],[f684]) ).
cnf(s60,plain,
( ~ spl0_4
| ~ spl0_10
| spl0_17
| spl0_62 ),
inference(sat_conversion,[],[f688]) ).
cnf(s62,plain,
( ~ spl0_11
| spl0_17
| spl0_62 ),
inference(sat_conversion,[],[f690]) ).
cnf(s63,plain,
( spl0_17
| spl0_42
| spl0_53
| spl0_62 ),
inference(sat_conversion,[],[f691]) ).
cnf(s69,plain,
( spl0_16
| spl0_65 ),
inference(sat_conversion,[],[f708]) ).
cnf(s70,plain,
( spl0_16
| ~ spl0_66 ),
inference(sat_conversion,[],[f713]) ).
cnf(s71,plain,
( spl0_16
| ~ spl0_67 ),
inference(sat_conversion,[],[f718]) ).
cnf(s73,plain,
( spl0_15
| spl0_68 ),
inference(sat_conversion,[],[f724]) ).
cnf(s74,plain,
( spl0_15
| spl0_69 ),
inference(sat_conversion,[],[f729]) ).
cnf(s75,plain,
( spl0_15
| ~ spl0_70 ),
inference(sat_conversion,[],[f734]) ).
cnf(s77,plain,
( spl0_28
| spl0_71 ),
inference(sat_conversion,[],[f740]) ).
cnf(s78,plain,
( spl0_28
| ~ spl0_72 ),
inference(sat_conversion,[],[f745]) ).
cnf(s79,plain,
( spl0_28
| ~ spl0_73 ),
inference(sat_conversion,[],[f750]) ).
cnf(s81,plain,
( ~ spl0_35
| spl0_74 ),
inference(sat_conversion,[],[f756]) ).
cnf(s82,plain,
( ~ spl0_35
| spl0_75 ),
inference(sat_conversion,[],[f761]) ).
cnf(s83,plain,
( ~ spl0_35
| ~ spl0_76 ),
inference(sat_conversion,[],[f766]) ).
cnf(s93,plain,
( spl0_3
| ~ spl0_83 ),
inference(sat_conversion,[],[f804]) ).
cnf(s94,plain,
( spl0_3
| spl0_84 ),
inference(sat_conversion,[],[f809]) ).
cnf(s95,plain,
( spl0_3
| ~ spl0_85 ),
inference(sat_conversion,[],[f814]) ).
cnf(s96,plain,
( spl0_3
| ~ spl0_17 ),
inference(sat_conversion,[],[f815]) ).
cnf(s97,plain,
( ~ spl0_1
| ~ spl0_86 ),
inference(sat_conversion,[],[f820]) ).
cnf(s98,plain,
( ~ spl0_1
| ~ spl0_87 ),
inference(sat_conversion,[],[f825]) ).
cnf(s99,plain,
( ~ spl0_1
| spl0_88 ),
inference(sat_conversion,[],[f830]) ).
cnf(s100,plain,
( ~ spl0_1
| ~ spl0_17 ),
inference(sat_conversion,[],[f831]) ).
cnf(s109,plain,
( ~ spl0_39
| ~ spl0_95 ),
inference(sat_conversion,[],[f868]) ).
cnf(s110,plain,
( ~ spl0_39
| spl0_96 ),
inference(sat_conversion,[],[f873]) ).
cnf(s111,plain,
( ~ spl0_39
| spl0_97 ),
inference(sat_conversion,[],[f878]) ).
cnf(s117,plain,
( spl0_19
| ~ spl0_101 ),
inference(sat_conversion,[],[f900]) ).
cnf(s118,plain,
( spl0_19
| ~ spl0_102 ),
inference(sat_conversion,[],[f905]) ).
cnf(s119,plain,
( spl0_19
| ~ spl0_103 ),
inference(sat_conversion,[],[f910]) ).
cnf(s121,plain,
( spl0_45
| ~ spl0_104 ),
inference(sat_conversion,[],[f916]) ).
cnf(s122,plain,
( spl0_45
| spl0_105 ),
inference(sat_conversion,[],[f921]) ).
cnf(s123,plain,
( spl0_45
| ~ spl0_106 ),
inference(sat_conversion,[],[f926]) ).
cnf(s125,plain,
( spl0_37
| spl0_107 ),
inference(sat_conversion,[],[f932]) ).
cnf(s126,plain,
( spl0_37
| spl0_108 ),
inference(sat_conversion,[],[f937]) ).
cnf(s127,plain,
( spl0_37
| spl0_109 ),
inference(sat_conversion,[],[f942]) ).
cnf(s129,plain,
( spl0_12
| ~ spl0_110 ),
inference(sat_conversion,[],[f948]) ).
cnf(s130,plain,
( spl0_12
| spl0_111 ),
inference(sat_conversion,[],[f953]) ).
cnf(s131,plain,
( spl0_12
| ~ spl0_112 ),
inference(sat_conversion,[],[f958]) ).
cnf(s133,plain,
( spl0_14
| spl0_113 ),
inference(sat_conversion,[],[f964]) ).
cnf(s134,plain,
( spl0_14
| spl0_114 ),
inference(sat_conversion,[],[f969]) ).
cnf(s135,plain,
( spl0_14
| ~ spl0_115 ),
inference(sat_conversion,[],[f974]) ).
cnf(s137,plain,
( spl0_57
| ~ spl0_116 ),
inference(sat_conversion,[],[f980]) ).
cnf(s138,plain,
( spl0_57
| spl0_117 ),
inference(sat_conversion,[],[f985]) ).
cnf(s139,plain,
( spl0_57
| ~ spl0_118 ),
inference(sat_conversion,[],[f990]) ).
cnf(s141,plain,
( spl0_13
| ~ spl0_119 ),
inference(sat_conversion,[],[f996]) ).
cnf(s142,plain,
( spl0_13
| spl0_120 ),
inference(sat_conversion,[],[f1001]) ).
cnf(s143,plain,
( spl0_13
| ~ spl0_121 ),
inference(sat_conversion,[],[f1006]) ).
cnf(s149,plain,
( ~ spl0_6
| ~ spl0_125 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s150,plain,
( ~ spl0_6
| ~ spl0_126 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s151,plain,
( ~ spl0_6
| ~ spl0_127 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s153,plain,
( spl0_32
| ~ spl0_128 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s154,plain,
( spl0_32
| ~ spl0_129 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s155,plain,
( spl0_32
| spl0_130 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s157,plain,
( spl0_10
| ~ spl0_131 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s158,plain,
( spl0_10
| spl0_132 ),
inference(sat_conversion,[],[f1065]) ).
cnf(s159,plain,
( spl0_10
| spl0_133 ),
inference(sat_conversion,[],[f1070]) ).
cnf(s161,plain,
( spl0_4
| ~ spl0_134 ),
inference(sat_conversion,[],[f1076]) ).
cnf(s162,plain,
( spl0_4
| spl0_135 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s163,plain,
( spl0_4
| ~ spl0_136 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s164,plain,
( spl0_4
| ~ spl0_17 ),
inference(sat_conversion,[],[f1087]) ).
cnf(s173,plain,
( spl0_11
| ~ spl0_143 ),
inference(sat_conversion,[],[f1124]) ).
cnf(s174,plain,
( spl0_11
| ~ spl0_144 ),
inference(sat_conversion,[],[f1129]) ).
cnf(s175,plain,
( spl0_11
| ~ spl0_145 ),
inference(sat_conversion,[],[f1134]) ).
cnf(s177,plain,
( ~ spl0_5
| spl0_146 ),
inference(sat_conversion,[],[f1140]) ).
cnf(s178,plain,
( ~ spl0_5
| spl0_147 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s179,plain,
( ~ spl0_5
| spl0_148 ),
inference(sat_conversion,[],[f1150]) ).
cnf(s189,plain,
( ~ spl0_23
| spl0_155 ),
inference(sat_conversion,[],[f1188]) ).
cnf(s190,plain,
( ~ spl0_23
| spl0_156 ),
inference(sat_conversion,[],[f1193]) ).
cnf(s191,plain,
( ~ spl0_23
| spl0_157 ),
inference(sat_conversion,[],[f1198]) ).
cnf(s193,plain,
( ~ spl0_8
| spl0_158 ),
inference(sat_conversion,[],[f1204]) ).
cnf(s194,plain,
( ~ spl0_8
| spl0_159 ),
inference(sat_conversion,[],[f1209]) ).
cnf(s195,plain,
( ~ spl0_8
| spl0_160 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s215,plain,
( ~ spl0_27
| spl0_66
| spl0_67
| spl0_161 ),
inference(sat_conversion,[],[f1413]) ).
cnf(s238,plain,
( ~ spl0_26
| ~ spl0_114
| spl0_115
| spl0_165 ),
inference(sat_conversion,[],[f1468]) ).
cnf(s251,plain,
( spl0_20
| ~ spl0_33
| ~ spl0_41 ),
inference(sat_conversion,[],[f1532]) ).
cnf(s269,plain,
( ~ spl0_27
| spl0_31
| ~ spl0_46 ),
inference(sat_conversion,[],[f1605]) ).
cnf(s271,plain,
( ~ spl0_26
| spl0_104
| ~ spl0_105
| spl0_106 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s300,plain,
( ~ spl0_31
| spl0_101
| spl0_102
| spl0_103 ),
inference(sat_conversion,[],[f1684]) ).
cnf(s310,plain,
( ~ spl0_30
| spl0_83
| spl0_85
| spl0_176 ),
inference(sat_conversion,[],[f1714]) ).
cnf(s313,plain,
( ~ spl0_30
| spl0_134
| spl0_136
| spl0_166 ),
inference(sat_conversion,[],[f1717]) ).
cnf(s316,plain,
( ~ spl0_30
| spl0_143
| spl0_144
| spl0_173 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s333,plain,
( ~ spl0_50
| ~ spl0_147
| ~ spl0_148
| ~ spl0_184 ),
inference(sat_conversion,[],[f1846]) ).
cnf(s337,plain,
( ~ spl0_42
| spl0_116
| ~ spl0_117
| spl0_118 ),
inference(sat_conversion,[],[f1850]) ).
cnf(s341,plain,
( ~ spl0_42
| ~ spl0_71
| spl0_73
| spl0_169 ),
inference(sat_conversion,[],[f1854]) ).
cnf(s371,plain,
( ~ spl0_33
| ~ spl0_55
| ~ spl0_114
| spl0_115 ),
inference(sat_conversion,[],[f2029]) ).
cnf(s382,plain,
( ~ spl0_30
| spl0_59
| ~ spl0_62 ),
inference(sat_conversion,[],[f2071]) ).
cnf(s389,plain,
( ~ spl0_26
| ~ spl0_65
| spl0_67
| spl0_161 ),
inference(sat_conversion,[],[f2078]) ).
cnf(s402,plain,
( ~ spl0_26
| spl0_143
| spl0_145
| ~ spl0_173 ),
inference(sat_conversion,[],[f2091]) ).
cnf(s409,plain,
( ~ spl0_56
| spl0_110
| ~ spl0_111
| ~ spl0_180 ),
inference(sat_conversion,[],[f2098]) ).
cnf(s415,plain,
( spl0_20
| ~ spl0_40
| ~ spl0_55 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s423,plain,
( ~ spl0_21
| ~ spl0_71
| spl0_72
| spl0_169 ),
inference(sat_conversion,[],[f2112]) ).
cnf(s427,plain,
( ~ spl0_56
| spl0_83
| ~ spl0_84
| ~ spl0_176 ),
inference(sat_conversion,[],[f2116]) ).
cnf(s432,plain,
( ~ spl0_18
| ~ spl0_65
| spl0_66
| ~ spl0_161 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s434,plain,
( ~ spl0_18
| ~ spl0_74
| ~ spl0_75
| spl0_76 ),
inference(sat_conversion,[],[f2161]) ).
cnf(s443,plain,
( ~ spl0_18
| spl0_20
| ~ spl0_40 ),
inference(sat_conversion,[],[f2170]) ).
cnf(s444,plain,
( ~ spl0_60
| ~ spl0_155
| ~ spl0_156
| ~ spl0_175 ),
inference(sat_conversion,[],[f2171]) ).
cnf(s477,plain,
( ~ spl0_54
| spl0_134
| ~ spl0_135
| spl0_136 ),
inference(sat_conversion,[],[f2358]) ).
cnf(s480,plain,
( ~ spl0_59
| spl0_134
| ~ spl0_135
| spl0_166 ),
inference(sat_conversion,[],[f2361]) ).
cnf(s483,plain,
( ~ spl0_59
| spl0_86
| spl0_87
| ~ spl0_178 ),
inference(sat_conversion,[],[f2364]) ).
cnf(s485,plain,
( ~ spl0_42
| spl0_119
| ~ spl0_120
| spl0_181 ),
inference(sat_conversion,[],[f2384]) ).
cnf(s493,plain,
( ~ spl0_61
| ~ spl0_155
| ~ spl0_156
| ~ spl0_157 ),
inference(sat_conversion,[],[f2494]) ).
cnf(s502,plain,
( ~ spl0_24
| spl0_83
| spl0_85
| ~ spl0_176 ),
inference(sat_conversion,[],[f2503]) ).
cnf(s506,plain,
( ~ spl0_27
| spl0_31
| ~ spl0_49 ),
inference(sat_conversion,[],[f2507]) ).
cnf(s511,plain,
( ~ spl0_41
| ~ spl0_71
| spl0_72
| spl0_73 ),
inference(sat_conversion,[],[f2512]) ).
cnf(s512,plain,
( ~ spl0_50
| ~ spl0_158
| ~ spl0_159
| ~ spl0_160 ),
inference(sat_conversion,[],[f2513]) ).
cnf(s521,plain,
( ~ spl0_55
| spl0_72
| spl0_73
| ~ spl0_169 ),
inference(sat_conversion,[],[f2522]) ).
cnf(s527,plain,
( ~ spl0_60
| ~ spl0_96
| ~ spl0_97
| ~ spl0_179 ),
inference(sat_conversion,[],[f2528]) ).
cnf(s528,plain,
( ~ spl0_60
| ~ spl0_146
| ~ spl0_147
| ~ spl0_184 ),
inference(sat_conversion,[],[f2529]) ).
cnf(s530,plain,
( ~ spl0_26
| spl0_95
| ~ spl0_97
| spl0_179 ),
inference(sat_conversion,[],[f2531]) ).
cnf(s531,plain,
( ~ spl0_60
| ~ spl0_107
| ~ spl0_108
| ~ spl0_109 ),
inference(sat_conversion,[],[f2532]) ).
cnf(s541,plain,
( ~ spl0_20
| ~ spl0_68
| ~ spl0_69
| spl0_70 ),
inference(sat_conversion,[],[f2541]) ).
cnf(s542,plain,
( ~ spl0_20
| ~ spl0_114
| spl0_115
| ~ spl0_165 ),
inference(sat_conversion,[],[f2542]) ).
cnf(s544,plain,
( ~ spl0_20
| ~ spl0_71
| spl0_73
| ~ spl0_169 ),
inference(sat_conversion,[],[f2544]) ).
cnf(s545,plain,
( ~ spl0_33
| ~ spl0_113
| ~ spl0_114
| spl0_115 ),
inference(sat_conversion,[],[f2545]) ).
cnf(s549,plain,
( ~ spl0_33
| ~ spl0_146
| ~ spl0_147
| spl0_184 ),
inference(sat_conversion,[],[f2549]) ).
cnf(s559,plain,
( ~ spl0_40
| ~ spl0_146
| ~ spl0_148
| spl0_184 ),
inference(sat_conversion,[],[f2559]) ).
cnf(s565,plain,
( ~ spl0_44
| ~ spl0_155
| ~ spl0_157
| spl0_175 ),
inference(sat_conversion,[],[f2564]) ).
cnf(s575,plain,
( ~ spl0_53
| spl0_134
| ~ spl0_135
| ~ spl0_166 ),
inference(sat_conversion,[],[f2574]) ).
cnf(s585,plain,
( ~ spl0_54
| spl0_119
| spl0_121
| ~ spl0_181 ),
inference(sat_conversion,[],[f2584]) ).
cnf(s588,plain,
( ~ spl0_54
| ~ spl0_84
| spl0_85
| spl0_176 ),
inference(sat_conversion,[],[f2587]) ).
cnf(s592,plain,
( ~ spl0_62
| ~ spl0_155
| ~ spl0_156
| spl0_175 ),
inference(sat_conversion,[],[f2591]) ).
cnf(s598,plain,
( ~ spl0_47
| spl0_87
| ~ spl0_88
| spl0_178 ),
inference(sat_conversion,[],[f2597]) ).
cnf(s609,plain,
( ~ spl0_21
| spl0_134
| spl0_136
| ~ spl0_166 ),
inference(sat_conversion,[],[f2607]) ).
cnf(s610,plain,
( ~ spl0_21
| spl0_119
| ~ spl0_120
| spl0_121 ),
inference(sat_conversion,[],[f2608]) ).
cnf(s618,plain,
( ~ spl0_46
| spl0_131
| ~ spl0_132
| spl0_183 ),
inference(sat_conversion,[],[f2616]) ).
cnf(s627,plain,
( ~ spl0_49
| spl0_86
| spl0_87
| ~ spl0_88 ),
inference(sat_conversion,[],[f2625]) ).
cnf(s629,plain,
( ~ spl0_55
| spl0_144
| spl0_145
| ~ spl0_173 ),
inference(sat_conversion,[],[f2627]) ).
cnf(s630,plain,
( ~ spl0_55
| ~ spl0_111
| spl0_112
| spl0_180 ),
inference(sat_conversion,[],[f2628]) ).
cnf(s631,plain,
( spl0_26
| ~ spl0_48
| ~ spl0_55 ),
inference(sat_conversion,[],[f2629]) ).
cnf(s632,plain,
( spl0_26
| ~ spl0_47
| ~ spl0_55 ),
inference(sat_conversion,[],[f2630]) ).
cnf(s633,plain,
( ~ spl0_20
| ~ spl0_65
| spl0_67
| ~ spl0_161 ),
inference(sat_conversion,[],[f2631]) ).
cnf(s637,plain,
( ~ spl0_40
| ~ spl0_132
| ~ spl0_133
| spl0_183 ),
inference(sat_conversion,[],[f2635]) ).
cnf(s638,plain,
( ~ spl0_53
| ~ spl0_156
| ~ spl0_157
| spl0_175 ),
inference(sat_conversion,[],[f2636]) ).
cnf(s640,plain,
( ~ spl0_53
| spl0_131
| ~ spl0_133
| ~ spl0_183 ),
inference(sat_conversion,[],[f2638]) ).
cnf(s642,plain,
( ~ spl0_27
| spl0_143
| spl0_144
| spl0_145 ),
inference(sat_conversion,[],[f2640]) ).
cnf(s646,plain,
( ~ spl0_27
| spl0_110
| spl0_112
| spl0_180 ),
inference(sat_conversion,[],[f2644]) ).
cnf(s647,plain,
( ~ spl0_30
| spl0_125
| spl0_126
| spl0_127 ),
inference(sat_conversion,[],[f2645]) ).
cnf(s650,plain,
( ~ spl0_31
| spl0_86
| spl0_87
| spl0_178 ),
inference(sat_conversion,[],[f2647]) ).
cnf(s652,plain,
( ~ spl0_44
| spl0_131
| ~ spl0_132
| ~ spl0_133 ),
inference(sat_conversion,[],[f2649]) ).
cnf(s658,plain,
( ~ spl0_59
| spl0_128
| spl0_129
| ~ spl0_130 ),
inference(sat_conversion,[],[f2655]) ).
cnf(s662,plain,
( ~ spl0_59
| spl0_128
| spl0_129
| ~ spl0_130 ),
inference(sat_conversion,[],[f2659]) ).
cnf(s666,plain,
( ~ spl0_62
| spl0_131
| ~ spl0_132
| ~ spl0_183 ),
inference(sat_conversion,[],[f2663]) ).
cnf(s668,plain,
( ~ spl0_62
| spl0_86
| ~ spl0_88
| ~ spl0_178 ),
inference(sat_conversion,[],[f2665]) ).
cnf(s672,plain,
( spl0_19
| ~ spl0_31 ),
inference(rat,[],[s300,s117,s118,s119]) ).
cnf(s673,plain,
( ~ spl0_19
| spl0_11
| spl0_44
| spl0_3 ),
inference(rat,[],[s58,s427,s629,s531,s310,s316,s125,s126,s127,s18,s33,s96,s95,s94,s93,s175,s174,s173]) ).
cnf(s674,plain,
( spl0_11
| spl0_44
| spl0_5
| spl0_4
| spl0_3 ),
inference(rat,[],[s610,s141,s142,s143,s53,s521,s480,s423,s609,s48,s672,s673,s77,s78,s79,s16,s642,s173,s174,s175,s96,s477,s161,s162,s163]) ).
cnf(s675,plain,
( spl0_13
| ~ spl0_21 ),
inference(rat,[],[s610,s141,s142,s143]) ).
cnf(s676,plain,
( spl0_31
| ~ spl0_11
| spl0_6
| spl0_4
| spl0_17
| spl0_1 ),
inference(rat,[],[s444,s592,s189,s190,s15,s506,s40,s434,s81,s82,s83,s22,s371,s134,s135,s7,s53,s675,s56,s480,s313,s609,s48,s477,s161,s162,s163,s62]) ).
cnf(s677,plain,
( spl0_10
| spl0_8
| spl0_6
| spl0_5
| spl0_4
| spl0_3
| spl0_1 ),
inference(rat,[],[s49,s631,s371,s271,s134,s135,s121,s122,s123,s45,s34,s58,s575,s609,s427,s531,s313,s310,s125,s126,s127,s18,s33,s672,s676,s618,s666,s62,s674,s652,s157,s158,s159,s96,s95,s94,s93,s477,s161,s162,s163]) ).
cnf(s678,plain,
( spl0_11
| spl0_6
| spl0_5
| spl0_4
| spl0_3
| spl0_1 ),
inference(rat,[],[s58,s629,s427,s316,s310,s56,s444,s565,s189,s190,s191,s15,s642,s674,s173,s174,s175,s96,s95,s94,s93]) ).
cnf(s679,plain,
( spl0_6
| spl0_5
| spl0_4
| spl0_3
| spl0_1 ),
inference(rat,[],[s215,s633,s30,s69,s70,s71,s271,s28,s121,s122,s123,s511,s34,s77,s78,s79,s609,s41,s313,s512,s10,s18,s618,s637,s193,s194,s195,s672,s666,s677,s157,s158,s159,s676,s62,s5,s678,s96,s163,s161]) ).
cnf(s680,plain,
( spl0_28
| ~ spl0_55
| ~ spl0_21 ),
inference(rat,[],[s423,s521,s77,s78,s79]) ).
cnf(s681,plain,
( spl0_11
| ~ spl0_27 ),
inference(rat,[],[s642,s173,s174,s175]) ).
cnf(s684,plain,
( spl0_16
| ~ spl0_18
| ~ spl0_27 ),
inference(rat,[],[s432,s215,s69,s70,s71]) ).
cnf(s685,plain,
( spl0_5
| spl0_4
| spl0_3
| spl0_1 ),
inference(rat,[],[s434,s81,s82,s83,s24,s684,s371,s134,s135,s7,s681,s40,s506,s16,s680,s53,s480,s675,s609,s48,s672,s18,s647,s149,s150,s151,s679,s96,s477,s161,s162,s163]) ).
cnf(s686,plain,
( ~ spl0_27
| spl0_31
| ~ spl0_55
| ~ spl0_13
| spl0_17 ),
inference(rat,[],[s434,s81,s82,s83,s24,s371,s134,s135,s684,s7,s40,s681,s506]) ).
cnf(s687,plain,
( spl0_16
| ~ spl0_18
| ~ spl0_26 ),
inference(rat,[],[s389,s432,s69,s70,s71]) ).
cnf(s689,plain,
( spl0_26
| spl0_27
| ~ spl0_55
| ~ spl0_5
| spl0_17 ),
inference(rat,[],[s528,s57,s559,s632,s30,s179,s178,s177]) ).
cnf(s690,plain,
( ~ spl0_18
| ~ spl0_26
| spl0_17
| spl0_1 ),
inference(rat,[],[s434,s81,s82,s83,s24,s251,s28,s443,s541,s73,s74,s75,s8,s687]) ).
cnf(s691,plain,
( spl0_20
| spl0_18
| ~ spl0_26
| ~ spl0_28
| ~ spl0_55
| spl0_17 ),
inference(rat,[],[s530,s527,s109,s110,s111,s27,s415,s54]) ).
cnf(s692,plain,
( spl0_16
| ~ spl0_20
| ~ spl0_26 ),
inference(rat,[],[s633,s389,s69,s71]) ).
cnf(s693,plain,
( ~ spl0_21
| ~ spl0_5
| spl0_134
| ~ spl0_135
| spl0_136
| spl0_17
| spl0_1 ),
inference(rat,[],[s541,s73,s74,s75,s8,s692,s691,s690,s689,s686,s672,s680,s18,s53,s480,s313,s675,s609]) ).
cnf(s694,plain,
( ~ spl0_6
| ~ spl0_30 ),
inference(rat,[],[s647,s149,s150,s151]) ).
cnf(s695,plain,
( spl0_14
| ~ spl0_55
| ~ spl0_20
| spl0_54
| spl0_17 ),
inference(rat,[],[s631,s238,s49,s542,s371,s134,s135]) ).
cnf(s696,plain,
( ~ spl0_55
| ~ spl0_20
| spl0_53
| ~ spl0_30
| spl0_54
| spl0_17 ),
inference(rat,[],[s521,s341,s77,s78,s79,s63,s41,s382,s512,s662,s193,s194,s195,s153,s154,s155,s45,s46,s695,s694]) ).
cnf(s697,plain,
( spl0_4
| spl0_3
| spl0_1 ),
inference(rat,[],[s531,s125,s126,s127,s29,s337,s137,s138,s139,s51,s559,s528,s58,s696,s10,s694,s575,s427,s313,s310,s18,s672,s48,s693,s177,s178,s179,s685,s477,s161,s162,s163,s96,s95,s94,s93]) ).
cnf(s698,plain,
( ~ spl0_27
| ~ spl0_55
| spl0_31
| spl0_3
| spl0_1 ),
inference(rat,[],[s35,s541,s502,s73,s74,s75,s588,s8,s48,s684,s675,s40,s686,s269,s506,s96,s95,s94,s93]) ).
cnf(s699,plain,
( ~ spl0_28
| spl0_27
| ~ spl0_55
| spl0_17
| spl0_1 ),
inference(rat,[],[s541,s73,s74,s75,s8,s692,s691,s690,s689,s16]) ).
cnf(s700,plain,
( spl0_20
| spl0_42
| spl0_41
| spl0_27
| ~ spl0_55
| spl0_17 ),
inference(rat,[],[s531,s54,s125,s126,s127,s687,s29,s30,s28,s415]) ).
cnf(s701,plain,
( spl0_47
| spl0_27
| spl0_17 ),
inference(rat,[],[s531,s125,s126,s127,s37,s57]) ).
cnf(s702,plain,
( spl0_27
| ~ spl0_55
| spl0_1
| spl0_17 ),
inference(rat,[],[s541,s73,s74,s75,s8,s692,s632,s701,s700,s341,s511,s521,s77,s78,s79,s699]) ).
cnf(s703,plain,
( ~ spl0_55
| spl0_31
| spl0_3
| spl0_1 ),
inference(rat,[],[s702,s698,s96]) ).
cnf(s704,plain,
( ~ spl0_27
| spl0_24
| spl0_31
| spl0_17
| spl0_1 ),
inference(rat,[],[s541,s73,s74,s75,s8,s684,s35,s40,s269,s506]) ).
cnf(s705,plain,
( spl0_31
| spl0_3
| spl0_1 ),
inference(rat,[],[s485,s585,s141,s142,s143,s53,s658,s63,s153,s154,s155,s638,s592,s59,s444,s493,s189,s190,s191,s15,s704,s58,s427,s502,s588,s47,s703,s96,s95,s94,s93,s697]) ).
cnf(s706,plain,
( spl0_16
| ~ spl0_27
| ~ spl0_20 ),
inference(rat,[],[s633,s215,s69,s70,s71]) ).
cnf(s707,plain,
( spl0_15
| ~ spl0_20 ),
inference(rat,[],[s541,s73,s74,s75]) ).
cnf(s708,plain,
( spl0_3
| spl0_1 ),
inference(rat,[],[s673,s62,s565,s592,s444,s58,s189,s190,s191,s702,s15,s706,s8,s707,s10,s427,s694,s310,s18,s672,s705,s93,s94,s95,s96]) ).
cnf(s709,plain,
( spl0_31
| spl0_1 ),
inference(rat,[],[s686,s702,s53,s480,s609,s675,s48,s164,s477,s161,s162,s163,s2,s708]) ).
cnf(s711,plain,
( ~ spl0_28
| spl0_1 ),
inference(rat,[],[s559,s333,s177,s178,s179,s41,s16,s30,s692,s706,s8,s707,s10,s694,s18,s164,s2,s708,s672,s709]) ).
cnf(s712,plain,
spl0_1,
inference(rat,[],[s341,s544,s77,s79,s711,s63,s382,s658,s153,s154,s155,s59,s493,s189,s190,s191,s15,s706,s8,s696,s707,s575,s10,s313,s694,s18,s672,s709,s477,s161,s162,s163,s164,s2,s708]) ).
cnf(s713,plain,
~ spl0_17,
inference(rat,[],[s100,s712]) ).
cnf(s714,plain,
spl0_88,
inference(rat,[],[s99,s712]) ).
cnf(s715,plain,
~ spl0_87,
inference(rat,[],[s98,s712]) ).
cnf(s716,plain,
~ spl0_86,
inference(rat,[],[s97,s712]) ).
cnf(s717,plain,
~ spl0_49,
inference(rat,[],[s627,s714,s715,s716]) ).
cnf(s718,plain,
( spl0_10
| ~ spl0_44 ),
inference(rat,[],[s652,s157,s158,s159]) ).
cnf(s721,plain,
( ~ spl0_35
| ~ spl0_18 ),
inference(rat,[],[s434,s81,s82,s83]) ).
cnf(s723,plain,
( spl0_20
| ~ spl0_27 ),
inference(rat,[],[s28,s251,s443,s24,s721,s684,s40,s650,s668,s62,s681,s713,s717,s716,s715,s714]) ).
cnf(s724,plain,
~ spl0_27,
inference(rat,[],[s371,s134,s135,s50,s58,s409,s646,s129,s130,s131,s43,s528,s333,s549,s177,s178,s179,s5,s718,s38,s707,s723,s24,s721,s684,s40,s650,s598,s668,s62,s681,s713,s717,s715,s716,s714]) ).
cnf(s725,plain,
spl0_47,
inference(rat,[],[s701,s713,s724]) ).
cnf(s726,plain,
spl0_178,
inference(rat,[],[s598,s715,s714,s725]) ).
cnf(s727,plain,
~ spl0_62,
inference(rat,[],[s668,s716,s714,s726]) ).
cnf(s728,plain,
~ spl0_59,
inference(rat,[],[s483,s716,s715,s726]) ).
cnf(s729,plain,
~ spl0_11,
inference(rat,[],[s62,s713,s727]) ).
cnf(s730,plain,
~ spl0_145,
inference(rat,[],[s175,s729]) ).
cnf(s731,plain,
~ spl0_144,
inference(rat,[],[s174,s729]) ).
cnf(s732,plain,
~ spl0_143,
inference(rat,[],[s173,s729]) ).
cnf(s733,plain,
( spl0_20
| ~ spl0_33
| ~ spl0_16
| ~ spl0_55 ),
inference(rat,[],[s28,s251,s415,s713]) ).
cnf(s734,plain,
( spl0_54
| ~ spl0_55
| spl0_31 ),
inference(rat,[],[s409,s630,s129,s130,s131,s43,s333,s549,s177,s178,s179,s16,s50,s680,s695,s48,s733,s24,s721,s687,s632,s40,s713,s717,s724,s725]) ).
cnf(s735,plain,
( ~ spl0_55
| spl0_3
| spl0_31 ),
inference(rat,[],[s371,s134,s135,s50,s427,s588,s734,s24,s687,s632,s721,s40,s95,s94,s93,s713,s725,s717]) ).
cnf(s736,plain,
( spl0_10
| ~ spl0_40
| ~ spl0_53 ),
inference(rat,[],[s640,s637,s157,s158,s159]) ).
cnf(s737,plain,
( spl0_3
| spl0_31 ),
inference(rat,[],[s477,s161,s162,s163,s60,s736,s30,s687,s24,s545,s133,s134,s135,s63,s50,s485,s427,s585,s588,s48,s675,s141,s142,s143,s53,s735,s93,s94,s95,s721,s40,s713,s727,s724,s728,s717]) ).
cnf(s738,plain,
( spl0_54
| spl0_31 ),
inference(rat,[],[s53,s675,s734,s48,s728,s713]) ).
cnf(s739,plain,
spl0_31,
inference(rat,[],[s738,s477,s161,s162,s163,s2,s737]) ).
cnf(s740,plain,
spl0_19,
inference(rat,[],[s672,s739]) ).
cnf(s741,plain,
spl0_30,
inference(rat,[],[s18,s713,s740]) ).
cnf(s742,plain,
~ spl0_6,
inference(rat,[],[s694,s741]) ).
cnf(s743,plain,
spl0_173,
inference(rat,[],[s316,s732,s731,s741]) ).
cnf(s744,plain,
spl0_20,
inference(rat,[],[s10,s740,s713,s742]) ).
cnf(s746,plain,
~ spl0_26,
inference(rat,[],[s402,s730,s732,s743]) ).
cnf(s749,plain,
spl0_40,
inference(rat,[],[s30,s724,s713,s746]) ).
cnf(s759,plain,
( spl0_28
| ~ spl0_42 ),
inference(rat,[],[s341,s544,s77,s79,s744]) ).
cnf(s760,plain,
~ spl0_28,
inference(rat,[],[s559,s333,s177,s178,s179,s41,s16,s749,s713,s742,s724]) ).
cnf(s764,plain,
~ spl0_42,
inference(rat,[],[s759,s760]) ).
cnf(s767,plain,
spl0_53,
inference(rat,[],[s63,s713,s727,s764]) ).
cnf(s769,plain,
spl0_10,
inference(rat,[],[s736,s749,s767]) ).
cnf(s770,plain,
~ spl0_4,
inference(rat,[],[s60,s727,s713,s769]) ).
cnf(s771,plain,
~ spl0_136,
inference(rat,[],[s163,s770]) ).
cnf(s772,plain,
spl0_135,
inference(rat,[],[s162,s770]) ).
cnf(s773,plain,
~ spl0_134,
inference(rat,[],[s161,s770]) ).
cnf(s774,plain,
spl0_166,
inference(rat,[],[s313,s741,s773,s771]) ).
cnf(s776,plain,
$false,
inference(rat,[],[s575,s767,s773,s772,s774]) ).
fof(f2669,plain,
$false,
inference(avatar_sat_refutation,[],[s776]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN466+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.18 % Computer : n014.cluster.edu
% 0.11/0.18 % Model : x86_64 x86_64
% 0.11/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.18 % Memory : 8046.5625MB
% 0.11/0.18 % OS : Linux 6.8.0-71-generic
% 0.11/0.18 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Mon Sep 28 16:09:01 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.22 Running first-order model finding
% 0.11/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.30 % (1901607)Will run a generic schedule for satisfiability detection.
% 0.47/0.30 % (1901613)% WARNING: option uhcvi not known.
% 0.47/0.30 % (1901618)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1767479413:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.47/0.30 % (1901612)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4062035769_2999 on theBenchmark for (2999ds/0Mi)
% 0.47/0.30 % (1901613)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1265651540:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.47/0.30 % (1901615)dis+10_1_sil=32000:sp=arity:random_seed=3501730103:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.47/0.30 % (1901614)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2331734483:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.47/0.30 % (1901616)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1623097857:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.47/0.30 % (1901617)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3019237566:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.47/0.30 % Detected minimum model sizes of [1]
% 0.47/0.30 % Detected maximum model sizes of [32]
% 0.47/0.30 % TRYING [1]
% 0.47/0.30 % TRYING [2]
% 0.47/0.30 % TRYING [3]
% 0.47/0.30 % TRYING [4]
% 0.47/0.30 % (1901618) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1901607-1901618"...
% 0.47/0.30 % (1901618)...printing done.
% 0.47/0.30 % (1901618)Refutation found. Thanks to Tanya!
% 0.47/0.30 % SZS status Theorem for theBenchmark
% 0.47/0.30 % SZS output start Proof for theBenchmark
% See solution above
% 0.47/0.30 % (1901618)------------------------------
% 0.47/0.30 % (1901618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.47/0.30 % (1901618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.47/0.30 % (1901618)CaDiCaL version: 2.1.3
% 0.47/0.30 % (1901618)Termination reason: Refutation
% 0.47/0.30 % (1901618)Time elapsed: 0.037 s
% 0.47/0.30 % (1901618)Peak memory usage: 13 MB
% 0.47/0.30 % (1901618)Instructions burned: 63 (million)
% 0.47/0.30 % (1901607)Success in time 0.074 s
% 0.47/0.30 % Vampire exiting
%------------------------------------------------------------------------------