%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN501+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:15:26 PM UTC 2026
% Result : Theorem 0.08s 0.26s
% Output : Refutation 0.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 123
% Syntax : Number of formulae : 807 ( 7 unt; 122 def)
% Number of atoms : 6480 ( 0 equ)
% Maximal formula atoms : 750 ( 8 avg)
% Number of connectives : 8505 (2832 ~;4193 |; 995 &)
% ( 122 <=>; 363 =>; 0 <=; 0 <~>)
% Maximal formula depth : 116 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 158 ( 157 usr; 154 prp; 0-1 aty)
% Number of functors : 30 ( 30 usr; 30 con; 0-0 aty)
% Number of variables : 827 ( 0 sgn 827 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a97)
& ~ c2_1(a97)
& ~ c3_1(a97) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a98)
& ~ c1_1(a98)
& ~ c3_1(a98) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a99)
& ~ c0_1(a99)
& ~ c1_1(a99) ) )
& ( ~ hskp3
| ( ndr1_0
& c2_1(a100)
& c3_1(a100)
& ~ c1_1(a100) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a103)
& c2_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a104)
& ~ c0_1(a104)
& ~ c3_1(a104) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a105)
& c2_1(a105)
& ~ c3_1(a105) ) )
& ( ~ hskp7
| ( ndr1_0
& c2_1(a106)
& c3_1(a106)
& ~ c0_1(a106) ) )
& ( ~ hskp8
| ( ndr1_0
& c3_1(a107)
& ~ c0_1(a107)
& ~ c2_1(a107) ) )
& ( ~ hskp9
| ( ndr1_0
& c1_1(a108)
& c2_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a110)
& ~ c2_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a112)
& ~ c0_1(a112)
& ~ c1_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a113)
& c1_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a116)
& c1_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a120)
& ~ c1_1(a120)
& ~ c2_1(a120) ) )
& ( ~ hskp15
| ( ndr1_0
& ~ c0_1(a121)
& ~ c2_1(a121)
& ~ c3_1(a121) ) )
& ( ~ hskp16
| ( ndr1_0
& c0_1(a122)
& ~ c1_1(a122)
& ~ c2_1(a122) ) )
& ( ~ hskp17
| ( ndr1_0
& c2_1(a124)
& ~ c1_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a129)
& c2_1(a129)
& ~ c1_1(a129) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a130)
& c3_1(a130)
& ~ c2_1(a130) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c1_1(a132)
& ~ c2_1(a132)
& ~ c3_1(a132) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a136)
& ~ c1_1(a136)
& ~ c2_1(a136) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a138)
& c3_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a145)
& c3_1(a145)
& ~ c0_1(a145) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a173)
& ~ c0_1(a173)
& ~ c3_1(a173) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a195)
& c3_1(a195)
& ~ c1_1(a195) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a101)
& c1_1(a101)
& c3_1(a101) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a137)
& c1_1(a137)
& c2_1(a137) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a166)
& c2_1(a166)
& c3_1(a166) ) )
& ( ! [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
=> ( c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c2_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| hskp1
| hskp2 )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c3_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| ~ c3_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c0_1(X8)
| c3_1(X8)
| ~ c1_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c1_1(X10)
| ~ c0_1(X10)
| ~ c3_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( c3_1(X11)
| ~ c0_1(X11)
| ~ c1_1(X11) ) ) )
& ( ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c1_1(X12)
| ~ c2_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c3_1(X13)
| ~ c1_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( ~ c1_1(X14)
| ~ c2_1(X14)
| ~ c3_1(X14) ) ) )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| ~ c2_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| ~ c1_1(X16)
| ~ c2_1(X16) ) )
| hskp3 )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c1_1(X18)
| c2_1(X18)
| ~ c3_1(X18) ) )
| hskp27 )
& ( ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c1_1(X19)
| ~ c2_1(X19) ) )
| ! [X20] :
( ndr1_0
=> ( c1_1(X20)
| c3_1(X20)
| ~ c2_1(X20) ) )
| hskp1 )
& ( ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c2_1(X21) ) )
| hskp4
| hskp5 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22) ) )
| hskp6
| hskp7 )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c1_1(X23)
| ~ c3_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c1_1(X24)
| c2_1(X24)
| ~ c3_1(X24) ) )
| hskp8 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c1_1(X25)
| ~ c3_1(X25) ) )
| hskp9
| hskp6 )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c2_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c2_1(X29)
| c3_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31) ) ) )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33) ) )
| hskp10 )
& ( ! [X34] :
( ndr1_0
=> ( c0_1(X34)
| c2_1(X34)
| c3_1(X34) ) )
| hskp5
| hskp11 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c0_1(X36)
| ~ c1_1(X36)
| ~ c2_1(X36) ) )
| hskp12 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| ~ c1_1(X38)
| ~ c2_1(X38) ) )
| hskp10 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c1_1(X40)
| c2_1(X40)
| ~ c3_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c1_1(X41)
| ~ c2_1(X41)
| ~ c3_1(X41) ) ) )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| ~ c1_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c1_1(X43)
| ~ c0_1(X43)
| ~ c3_1(X43) ) )
| hskp10 )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46) ) ) )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47) ) )
| hskp13
| hskp5 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c3_1(X49)
| ~ c0_1(X49)
| ~ c1_1(X49) ) )
| hskp11 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| c3_1(X50)
| ~ c2_1(X50) ) )
| hskp1
| hskp14 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52) ) )
| hskp15 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| ~ c1_1(X53)
| ~ c2_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c2_1(X54)
| ~ c0_1(X54)
| ~ c1_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c0_1(X55)
| ~ c1_1(X55)
| ~ c2_1(X55) ) ) )
& ( ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56) ) )
| ! [X57] :
( ndr1_0
=> ( c3_1(X57)
| ~ c0_1(X57)
| ~ c2_1(X57) ) )
| hskp16 )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59) ) )
| hskp0 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| c3_1(X61) ) )
| hskp17 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| ~ c2_1(X62)
| ~ c3_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( ~ c0_1(X63)
| ~ c2_1(X63)
| ~ c3_1(X63) ) )
| hskp1 )
& ( ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| ~ c2_1(X64)
| ~ c3_1(X64) ) )
| hskp9
| hskp17 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c2_1(X65)
| c3_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( c3_1(X67)
| ~ c1_1(X67)
| ~ c2_1(X67) ) ) )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c2_1(X68)
| c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c0_1(X69)
| ~ c2_1(X69) ) )
| hskp15 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| c3_1(X70) ) )
| hskp18
| hskp19 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| c2_1(X71)
| ~ c0_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| c3_1(X72)
| ~ c2_1(X72) ) )
| hskp4 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| c2_1(X73)
| ~ c0_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c3_1(X75)
| ~ c0_1(X75)
| ~ c2_1(X75) ) ) )
& ( ! [X76] :
( ndr1_0
=> ( c1_1(X76)
| c2_1(X76)
| ~ c0_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77) ) )
| hskp20 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78) ) )
| hskp6
| hskp20 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| c2_1(X79)
| ~ c0_1(X79) ) )
| hskp2
| hskp21 )
& ( ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c3_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81) ) )
| hskp28 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| c2_1(X82)
| ~ c3_1(X82) ) )
| hskp22
| hskp6 )
& ( ! [X83] :
( ndr1_0
=> ( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83) ) )
| ! [X84] :
( ndr1_0
=> ( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85) ) ) )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86) ) )
| ! [X87] :
( ndr1_0
=> ( ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87) ) )
| hskp18 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| c3_1(X88)
| ~ c2_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c1_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89) ) )
| ! [X90] :
( ndr1_0
=> ( ~ c1_1(X90)
| ~ c2_1(X90)
| ~ c3_1(X90) ) ) )
& ( ! [X91] :
( ndr1_0
=> ( c1_1(X91)
| c3_1(X91)
| ~ c2_1(X91) ) )
| hskp22
| hskp21 )
& ( ! [X92] :
( ndr1_0
=> ( c1_1(X92)
| c3_1(X92)
| ~ c2_1(X92) ) )
| hskp1
| hskp19 )
& ( ! [X93] :
( ndr1_0
=> ( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) ) )
| hskp23
| hskp17 )
& ( ! [X94] :
( ndr1_0
=> ( c1_1(X94)
| ~ c0_1(X94)
| ~ c2_1(X94) ) )
| ! [X95] :
( ndr1_0
=> ( c1_1(X95)
| ~ c2_1(X95)
| ~ c3_1(X95) ) )
| ! [X96] :
( ndr1_0
=> ( ~ c0_1(X96)
| ~ c2_1(X96)
| ~ c3_1(X96) ) ) )
& ( ! [X97] :
( ndr1_0
=> ( c1_1(X97)
| ~ c0_1(X97)
| ~ c2_1(X97) ) )
| ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp24 )
& ( ! [X99] :
( ndr1_0
=> ( c1_1(X99)
| ~ c0_1(X99)
| ~ c2_1(X99) ) )
| ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100) ) )
| hskp1 )
& ( ! [X101] :
( ndr1_0
=> ( c1_1(X101)
| ~ c0_1(X101)
| ~ c2_1(X101) ) )
| hskp4
| hskp7 )
& ( ! [X102] :
( ndr1_0
=> ( c1_1(X102)
| ~ c0_1(X102)
| ~ c3_1(X102) ) )
| ! [X103] :
( ndr1_0
=> ( c2_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103) ) )
| hskp19 )
& ( ! [X104] :
( ndr1_0
=> ( c1_1(X104)
| ~ c2_1(X104)
| ~ c3_1(X104) ) )
| hskp3
| hskp17 )
& ( ! [X105] :
( ndr1_0
=> ( c2_1(X105)
| c3_1(X105)
| ~ c0_1(X105) ) )
| hskp18
| hskp11 )
& ( ! [X106] :
( ndr1_0
=> ( c2_1(X106)
| c3_1(X106)
| ~ c0_1(X106) ) )
| hskp16
| hskp2 )
& ( ! [X107] :
( ndr1_0
=> ( c2_1(X107)
| ~ c0_1(X107)
| ~ c1_1(X107) ) )
| hskp7
| hskp20 )
& ( ! [X108] :
( ndr1_0
=> ( c2_1(X108)
| ~ c0_1(X108)
| ~ c3_1(X108) ) )
| hskp4
| hskp7 )
& ( ! [X109] :
( ndr1_0
=> ( c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109) ) )
| ! [X110] :
( ndr1_0
=> ( c3_1(X110)
| ~ c0_1(X110)
| ~ c2_1(X110) ) )
| hskp11 )
& ( ! [X111] :
( ndr1_0
=> ( c2_1(X111)
| ~ c1_1(X111)
| ~ c3_1(X111) ) )
| ! [X112] :
( ndr1_0
=> ( ~ c0_1(X112)
| ~ c1_1(X112)
| ~ c2_1(X112) ) )
| hskp2 )
& ( ! [X113] :
( ndr1_0
=> ( c3_1(X113)
| ~ c0_1(X113)
| ~ c1_1(X113) ) )
| hskp27
| hskp19 )
& ( ! [X114] :
( ndr1_0
=> ( c3_1(X114)
| ~ c0_1(X114)
| ~ c1_1(X114) ) )
| hskp29
| hskp0 )
& ( ! [X115] :
( ndr1_0
=> ( c3_1(X115)
| ~ c0_1(X115)
| ~ c1_1(X115) ) )
| hskp18
| hskp8 )
& ( ! [X116] :
( ndr1_0
=> ( c3_1(X116)
| ~ c0_1(X116)
| ~ c1_1(X116) ) )
| hskp0 )
& ( ! [X117] :
( ndr1_0
=> ( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117) ) )
| hskp6 )
& ( ! [X118] :
( ndr1_0
=> ( c3_1(X118)
| ~ c0_1(X118)
| ~ c2_1(X118) ) )
| hskp16
| hskp25 )
& ( ! [X119] :
( ndr1_0
=> ( ~ c0_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119) ) )
| hskp27
| hskp29 )
& ( ! [X120] :
( ndr1_0
=> ( ~ c0_1(X120)
| ~ c2_1(X120)
| ~ c3_1(X120) ) )
| hskp1
| hskp9 )
& ( hskp28
| hskp4
| hskp22 )
& ( hskp27
| hskp9
| hskp2 )
& ( hskp12
| hskp13 )
& ( hskp13
| hskp18
| hskp8 )
& ( hskp18
| hskp4
| hskp20 )
& ( hskp18
| hskp19
| hskp17 )
& ( hskp26
| hskp25
| hskp5 )
& ( hskp22
| hskp0
| hskp11 )
& ( hskp22
| hskp8
| hskp15 )
& ( hskp16
| hskp6
| hskp15 )
& ( hskp16
| hskp10
| hskp8 )
& ( hskp19
| hskp8
| hskp15 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ~ ( ( ~ hskp0
| ( ndr1_0
& c0_1(a97)
& ~ c2_1(a97)
& ~ c3_1(a97) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a98)
& ~ c1_1(a98)
& ~ c3_1(a98) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a99)
& ~ c0_1(a99)
& ~ c1_1(a99) ) )
& ( ~ hskp3
| ( ndr1_0
& c2_1(a100)
& c3_1(a100)
& ~ c1_1(a100) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a103)
& c2_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a104)
& ~ c0_1(a104)
& ~ c3_1(a104) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a105)
& c2_1(a105)
& ~ c3_1(a105) ) )
& ( ~ hskp7
| ( ndr1_0
& c2_1(a106)
& c3_1(a106)
& ~ c0_1(a106) ) )
& ( ~ hskp8
| ( ndr1_0
& c3_1(a107)
& ~ c0_1(a107)
& ~ c2_1(a107) ) )
& ( ~ hskp9
| ( ndr1_0
& c1_1(a108)
& c2_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a110)
& ~ c2_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a112)
& ~ c0_1(a112)
& ~ c1_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a113)
& c1_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a116)
& c1_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a120)
& ~ c1_1(a120)
& ~ c2_1(a120) ) )
& ( ~ hskp15
| ( ndr1_0
& ~ c0_1(a121)
& ~ c2_1(a121)
& ~ c3_1(a121) ) )
& ( ~ hskp16
| ( ndr1_0
& c0_1(a122)
& ~ c1_1(a122)
& ~ c2_1(a122) ) )
& ( ~ hskp17
| ( ndr1_0
& c2_1(a124)
& ~ c1_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a129)
& c2_1(a129)
& ~ c1_1(a129) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a130)
& c3_1(a130)
& ~ c2_1(a130) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c1_1(a132)
& ~ c2_1(a132)
& ~ c3_1(a132) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a136)
& ~ c1_1(a136)
& ~ c2_1(a136) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a138)
& c3_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a145)
& c3_1(a145)
& ~ c0_1(a145) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a173)
& ~ c0_1(a173)
& ~ c3_1(a173) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a195)
& c3_1(a195)
& ~ c1_1(a195) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a101)
& c1_1(a101)
& c3_1(a101) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a137)
& c1_1(a137)
& c2_1(a137) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a166)
& c2_1(a166)
& c3_1(a166) ) )
& ( ! [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
=> ( c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c2_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| hskp1
| hskp2 )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c3_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| ~ c3_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c0_1(X8)
| c3_1(X8)
| ~ c1_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c1_1(X10)
| ~ c0_1(X10)
| ~ c3_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( c3_1(X11)
| ~ c0_1(X11)
| ~ c1_1(X11) ) ) )
& ( ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c1_1(X12)
| ~ c2_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c3_1(X13)
| ~ c1_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( ~ c1_1(X14)
| ~ c2_1(X14)
| ~ c3_1(X14) ) ) )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| ~ c2_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| ~ c1_1(X16)
| ~ c2_1(X16) ) )
| hskp3 )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c1_1(X18)
| c2_1(X18)
| ~ c3_1(X18) ) )
| hskp27 )
& ( ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c1_1(X19)
| ~ c2_1(X19) ) )
| ! [X20] :
( ndr1_0
=> ( c1_1(X20)
| c3_1(X20)
| ~ c2_1(X20) ) )
| hskp1 )
& ( ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c2_1(X21) ) )
| hskp4
| hskp5 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22) ) )
| hskp6
| hskp7 )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c1_1(X23)
| ~ c3_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c1_1(X24)
| c2_1(X24)
| ~ c3_1(X24) ) )
| hskp8 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c1_1(X25)
| ~ c3_1(X25) ) )
| hskp9
| hskp6 )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c2_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c2_1(X29)
| c3_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31) ) ) )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33) ) )
| hskp10 )
& ( ! [X34] :
( ndr1_0
=> ( c0_1(X34)
| c2_1(X34)
| c3_1(X34) ) )
| hskp5
| hskp11 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c0_1(X36)
| ~ c1_1(X36)
| ~ c2_1(X36) ) )
| hskp12 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| ~ c1_1(X38)
| ~ c2_1(X38) ) )
| hskp10 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c1_1(X40)
| c2_1(X40)
| ~ c3_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c1_1(X41)
| ~ c2_1(X41)
| ~ c3_1(X41) ) ) )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| ~ c1_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c1_1(X43)
| ~ c0_1(X43)
| ~ c3_1(X43) ) )
| hskp10 )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46) ) ) )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47) ) )
| hskp13
| hskp5 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c3_1(X49)
| ~ c0_1(X49)
| ~ c1_1(X49) ) )
| hskp11 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| c3_1(X50)
| ~ c2_1(X50) ) )
| hskp1
| hskp14 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52) ) )
| hskp15 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| ~ c1_1(X53)
| ~ c2_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c2_1(X54)
| ~ c0_1(X54)
| ~ c1_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c0_1(X55)
| ~ c1_1(X55)
| ~ c2_1(X55) ) ) )
& ( ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56) ) )
| ! [X57] :
( ndr1_0
=> ( c3_1(X57)
| ~ c0_1(X57)
| ~ c2_1(X57) ) )
| hskp16 )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59) ) )
| hskp0 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| c3_1(X61) ) )
| hskp17 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| ~ c2_1(X62)
| ~ c3_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( ~ c0_1(X63)
| ~ c2_1(X63)
| ~ c3_1(X63) ) )
| hskp1 )
& ( ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| ~ c2_1(X64)
| ~ c3_1(X64) ) )
| hskp9
| hskp17 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c2_1(X65)
| c3_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( c3_1(X67)
| ~ c1_1(X67)
| ~ c2_1(X67) ) ) )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c2_1(X68)
| c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c0_1(X69)
| ~ c2_1(X69) ) )
| hskp15 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| c3_1(X70) ) )
| hskp18
| hskp19 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| c2_1(X71)
| ~ c0_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| c3_1(X72)
| ~ c2_1(X72) ) )
| hskp4 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| c2_1(X73)
| ~ c0_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c3_1(X75)
| ~ c0_1(X75)
| ~ c2_1(X75) ) ) )
& ( ! [X76] :
( ndr1_0
=> ( c1_1(X76)
| c2_1(X76)
| ~ c0_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77) ) )
| hskp20 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78) ) )
| hskp6
| hskp20 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| c2_1(X79)
| ~ c0_1(X79) ) )
| hskp2
| hskp21 )
& ( ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c3_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81) ) )
| hskp28 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| c2_1(X82)
| ~ c3_1(X82) ) )
| hskp22
| hskp6 )
& ( ! [X83] :
( ndr1_0
=> ( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83) ) )
| ! [X84] :
( ndr1_0
=> ( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85) ) ) )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86) ) )
| ! [X87] :
( ndr1_0
=> ( ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87) ) )
| hskp18 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| c3_1(X88)
| ~ c2_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c1_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89) ) )
| ! [X90] :
( ndr1_0
=> ( ~ c1_1(X90)
| ~ c2_1(X90)
| ~ c3_1(X90) ) ) )
& ( ! [X91] :
( ndr1_0
=> ( c1_1(X91)
| c3_1(X91)
| ~ c2_1(X91) ) )
| hskp22
| hskp21 )
& ( ! [X92] :
( ndr1_0
=> ( c1_1(X92)
| c3_1(X92)
| ~ c2_1(X92) ) )
| hskp1
| hskp19 )
& ( ! [X93] :
( ndr1_0
=> ( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) ) )
| hskp23
| hskp17 )
& ( ! [X94] :
( ndr1_0
=> ( c1_1(X94)
| ~ c0_1(X94)
| ~ c2_1(X94) ) )
| ! [X95] :
( ndr1_0
=> ( c1_1(X95)
| ~ c2_1(X95)
| ~ c3_1(X95) ) )
| ! [X96] :
( ndr1_0
=> ( ~ c0_1(X96)
| ~ c2_1(X96)
| ~ c3_1(X96) ) ) )
& ( ! [X97] :
( ndr1_0
=> ( c1_1(X97)
| ~ c0_1(X97)
| ~ c2_1(X97) ) )
| ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp24 )
& ( ! [X99] :
( ndr1_0
=> ( c1_1(X99)
| ~ c0_1(X99)
| ~ c2_1(X99) ) )
| ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100) ) )
| hskp1 )
& ( ! [X101] :
( ndr1_0
=> ( c1_1(X101)
| ~ c0_1(X101)
| ~ c2_1(X101) ) )
| hskp4
| hskp7 )
& ( ! [X102] :
( ndr1_0
=> ( c1_1(X102)
| ~ c0_1(X102)
| ~ c3_1(X102) ) )
| ! [X103] :
( ndr1_0
=> ( c2_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103) ) )
| hskp19 )
& ( ! [X104] :
( ndr1_0
=> ( c1_1(X104)
| ~ c2_1(X104)
| ~ c3_1(X104) ) )
| hskp3
| hskp17 )
& ( ! [X105] :
( ndr1_0
=> ( c2_1(X105)
| c3_1(X105)
| ~ c0_1(X105) ) )
| hskp18
| hskp11 )
& ( ! [X106] :
( ndr1_0
=> ( c2_1(X106)
| c3_1(X106)
| ~ c0_1(X106) ) )
| hskp16
| hskp2 )
& ( ! [X107] :
( ndr1_0
=> ( c2_1(X107)
| ~ c0_1(X107)
| ~ c1_1(X107) ) )
| hskp7
| hskp20 )
& ( ! [X108] :
( ndr1_0
=> ( c2_1(X108)
| ~ c0_1(X108)
| ~ c3_1(X108) ) )
| hskp4
| hskp7 )
& ( ! [X109] :
( ndr1_0
=> ( c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109) ) )
| ! [X110] :
( ndr1_0
=> ( c3_1(X110)
| ~ c0_1(X110)
| ~ c2_1(X110) ) )
| hskp11 )
& ( ! [X111] :
( ndr1_0
=> ( c2_1(X111)
| ~ c1_1(X111)
| ~ c3_1(X111) ) )
| ! [X112] :
( ndr1_0
=> ( ~ c0_1(X112)
| ~ c1_1(X112)
| ~ c2_1(X112) ) )
| hskp2 )
& ( ! [X113] :
( ndr1_0
=> ( c3_1(X113)
| ~ c0_1(X113)
| ~ c1_1(X113) ) )
| hskp27
| hskp19 )
& ( ! [X114] :
( ndr1_0
=> ( c3_1(X114)
| ~ c0_1(X114)
| ~ c1_1(X114) ) )
| hskp29
| hskp0 )
& ( ! [X115] :
( ndr1_0
=> ( c3_1(X115)
| ~ c0_1(X115)
| ~ c1_1(X115) ) )
| hskp18
| hskp8 )
& ( ! [X116] :
( ndr1_0
=> ( c3_1(X116)
| ~ c0_1(X116)
| ~ c1_1(X116) ) )
| hskp0 )
& ( ! [X117] :
( ndr1_0
=> ( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117) ) )
| hskp6 )
& ( ! [X118] :
( ndr1_0
=> ( c3_1(X118)
| ~ c0_1(X118)
| ~ c2_1(X118) ) )
| hskp16
| hskp25 )
& ( ! [X119] :
( ndr1_0
=> ( ~ c0_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119) ) )
| hskp27
| hskp29 )
& ( ! [X120] :
( ndr1_0
=> ( ~ c0_1(X120)
| ~ c2_1(X120)
| ~ c3_1(X120) ) )
| hskp1
| hskp9 )
& ( hskp28
| hskp4
| hskp22 )
& ( hskp27
| hskp9
| hskp2 )
& ( hskp12
| hskp13 )
& ( hskp13
| hskp18
| hskp8 )
& ( hskp18
| hskp4
| hskp20 )
& ( hskp18
| hskp19
| hskp17 )
& ( hskp26
| hskp25
| hskp5 )
& ( hskp22
| hskp0
| hskp11 )
& ( hskp22
| hskp8
| hskp15 )
& ( hskp16
| hskp6
| hskp15 )
& ( hskp16
| hskp10
| hskp8 )
& ( hskp19
| hskp8
| hskp15 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a97)
& ~ c2_1(a97)
& ~ c3_1(a97) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a98)
& ~ c1_1(a98)
& ~ c3_1(a98) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a99)
& ~ c0_1(a99)
& ~ c1_1(a99) ) )
& ( ~ hskp3
| ( ndr1_0
& c2_1(a100)
& c3_1(a100)
& ~ c1_1(a100) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a103)
& c2_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a104)
& ~ c0_1(a104)
& ~ c3_1(a104) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a105)
& c2_1(a105)
& ~ c3_1(a105) ) )
& ( ~ hskp7
| ( ndr1_0
& c2_1(a106)
& c3_1(a106)
& ~ c0_1(a106) ) )
& ( ~ hskp8
| ( ndr1_0
& c3_1(a107)
& ~ c0_1(a107)
& ~ c2_1(a107) ) )
& ( ~ hskp9
| ( ndr1_0
& c1_1(a108)
& c2_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a110)
& ~ c2_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a112)
& ~ c0_1(a112)
& ~ c1_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a113)
& c1_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a116)
& c1_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a120)
& ~ c1_1(a120)
& ~ c2_1(a120) ) )
& ( ~ hskp15
| ( ndr1_0
& ~ c0_1(a121)
& ~ c2_1(a121)
& ~ c3_1(a121) ) )
& ( ~ hskp16
| ( ndr1_0
& c0_1(a122)
& ~ c1_1(a122)
& ~ c2_1(a122) ) )
& ( ~ hskp17
| ( ndr1_0
& c2_1(a124)
& ~ c1_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a129)
& c2_1(a129)
& ~ c1_1(a129) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a130)
& c3_1(a130)
& ~ c2_1(a130) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c1_1(a132)
& ~ c2_1(a132)
& ~ c3_1(a132) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a136)
& ~ c1_1(a136)
& ~ c2_1(a136) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a138)
& c3_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a145)
& c3_1(a145)
& ~ c0_1(a145) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a173)
& ~ c0_1(a173)
& ~ c3_1(a173) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a195)
& c3_1(a195)
& ~ c1_1(a195) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a101)
& c1_1(a101)
& c3_1(a101) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a137)
& c1_1(a137)
& c2_1(a137) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a166)
& c2_1(a166)
& c3_1(a166) ) )
& ( ! [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
=> ( c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c0_1(X4)
| c2_1(X4)
| ~ c3_1(X4) ) )
| hskp0 )
& ( ! [X5] :
( ndr1_0
=> ( c0_1(X5)
| c1_1(X5)
| c2_1(X5) ) )
| hskp1
| hskp2 )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c3_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c0_1(X7)
| c1_1(X7)
| ~ c3_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( c0_1(X8)
| c3_1(X8)
| ~ c1_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c3_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c1_1(X10)
| ~ c0_1(X10)
| ~ c3_1(X10) ) )
| ! [X11] :
( ndr1_0
=> ( c3_1(X11)
| ~ c0_1(X11)
| ~ c1_1(X11) ) ) )
& ( ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c1_1(X12)
| ~ c2_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| c3_1(X13)
| ~ c1_1(X13) ) )
| ! [X14] :
( ndr1_0
=> ( ~ c1_1(X14)
| ~ c2_1(X14)
| ~ c3_1(X14) ) ) )
& ( ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c1_1(X15)
| ~ c2_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c0_1(X16)
| ~ c1_1(X16)
| ~ c2_1(X16) ) )
| hskp3 )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c1_1(X18)
| c2_1(X18)
| ~ c3_1(X18) ) )
| hskp27 )
& ( ! [X19] :
( ndr1_0
=> ( c0_1(X19)
| c1_1(X19)
| ~ c2_1(X19) ) )
| ! [X20] :
( ndr1_0
=> ( c1_1(X20)
| c3_1(X20)
| ~ c2_1(X20) ) )
| hskp1 )
& ( ! [X21] :
( ndr1_0
=> ( c0_1(X21)
| c1_1(X21)
| ~ c2_1(X21) ) )
| hskp4
| hskp5 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22) ) )
| hskp6
| hskp7 )
& ( ! [X23] :
( ndr1_0
=> ( c0_1(X23)
| c1_1(X23)
| ~ c3_1(X23) ) )
| ! [X24] :
( ndr1_0
=> ( c1_1(X24)
| c2_1(X24)
| ~ c3_1(X24) ) )
| hskp8 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c1_1(X25)
| ~ c3_1(X25) ) )
| hskp9
| hskp6 )
& ( ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| c3_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c0_1(X27)
| c2_1(X27)
| ~ c3_1(X27) ) )
| ! [X28] :
( ndr1_0
=> ( c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28) ) ) )
& ( ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c2_1(X29)
| c3_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30) ) )
| ! [X31] :
( ndr1_0
=> ( c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31) ) ) )
& ( ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c2_1(X32)
| c3_1(X32) ) )
| ! [X33] :
( ndr1_0
=> ( c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33) ) )
| hskp10 )
& ( ! [X34] :
( ndr1_0
=> ( c0_1(X34)
| c2_1(X34)
| c3_1(X34) ) )
| hskp5
| hskp11 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c0_1(X36)
| ~ c1_1(X36)
| ~ c2_1(X36) ) )
| hskp12 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c0_1(X38)
| ~ c1_1(X38)
| ~ c2_1(X38) ) )
| hskp10 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39) ) )
| ! [X40] :
( ndr1_0
=> ( c1_1(X40)
| c2_1(X40)
| ~ c3_1(X40) ) )
| ! [X41] :
( ndr1_0
=> ( ~ c1_1(X41)
| ~ c2_1(X41)
| ~ c3_1(X41) ) ) )
& ( ! [X42] :
( ndr1_0
=> ( c0_1(X42)
| c2_1(X42)
| ~ c1_1(X42) ) )
| ! [X43] :
( ndr1_0
=> ( c1_1(X43)
| ~ c0_1(X43)
| ~ c3_1(X43) ) )
| hskp10 )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| ! [X46] :
( ndr1_0
=> ( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46) ) ) )
& ( ! [X47] :
( ndr1_0
=> ( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47) ) )
| hskp13
| hskp5 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c3_1(X49)
| ~ c0_1(X49)
| ~ c1_1(X49) ) )
| hskp11 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| c3_1(X50)
| ~ c2_1(X50) ) )
| hskp1
| hskp14 )
& ( ! [X51] :
( ndr1_0
=> ( c0_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51) ) )
| ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52) ) )
| hskp15 )
& ( ! [X53] :
( ndr1_0
=> ( c0_1(X53)
| ~ c1_1(X53)
| ~ c2_1(X53) ) )
| ! [X54] :
( ndr1_0
=> ( c2_1(X54)
| ~ c0_1(X54)
| ~ c1_1(X54) ) )
| ! [X55] :
( ndr1_0
=> ( ~ c0_1(X55)
| ~ c1_1(X55)
| ~ c2_1(X55) ) ) )
& ( ! [X56] :
( ndr1_0
=> ( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56) ) )
| ! [X57] :
( ndr1_0
=> ( c3_1(X57)
| ~ c0_1(X57)
| ~ c2_1(X57) ) )
| hskp16 )
& ( ! [X58] :
( ndr1_0
=> ( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58) ) )
| ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59) ) )
| hskp0 )
& ( ! [X60] :
( ndr1_0
=> ( c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60) ) )
| ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c2_1(X61)
| c3_1(X61) ) )
| hskp17 )
& ( ! [X62] :
( ndr1_0
=> ( c0_1(X62)
| ~ c2_1(X62)
| ~ c3_1(X62) ) )
| ! [X63] :
( ndr1_0
=> ( ~ c0_1(X63)
| ~ c2_1(X63)
| ~ c3_1(X63) ) )
| hskp1 )
& ( ! [X64] :
( ndr1_0
=> ( c0_1(X64)
| ~ c2_1(X64)
| ~ c3_1(X64) ) )
| hskp9
| hskp17 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c2_1(X65)
| c3_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66) ) )
| ! [X67] :
( ndr1_0
=> ( c3_1(X67)
| ~ c1_1(X67)
| ~ c2_1(X67) ) ) )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| c2_1(X68)
| c3_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c3_1(X69)
| ~ c0_1(X69)
| ~ c2_1(X69) ) )
| hskp15 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| c2_1(X70)
| c3_1(X70) ) )
| hskp18
| hskp19 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| c2_1(X71)
| ~ c0_1(X71) ) )
| ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| c3_1(X72)
| ~ c2_1(X72) ) )
| hskp4 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| c2_1(X73)
| ~ c0_1(X73) ) )
| ! [X74] :
( ndr1_0
=> ( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74) ) )
| ! [X75] :
( ndr1_0
=> ( c3_1(X75)
| ~ c0_1(X75)
| ~ c2_1(X75) ) ) )
& ( ! [X76] :
( ndr1_0
=> ( c1_1(X76)
| c2_1(X76)
| ~ c0_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77) ) )
| hskp20 )
& ( ! [X78] :
( ndr1_0
=> ( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78) ) )
| hskp6
| hskp20 )
& ( ! [X79] :
( ndr1_0
=> ( c1_1(X79)
| c2_1(X79)
| ~ c0_1(X79) ) )
| hskp2
| hskp21 )
& ( ! [X80] :
( ndr1_0
=> ( c1_1(X80)
| c2_1(X80)
| ~ c3_1(X80) ) )
| ! [X81] :
( ndr1_0
=> ( c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81) ) )
| hskp28 )
& ( ! [X82] :
( ndr1_0
=> ( c1_1(X82)
| c2_1(X82)
| ~ c3_1(X82) ) )
| hskp22
| hskp6 )
& ( ! [X83] :
( ndr1_0
=> ( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83) ) )
| ! [X84] :
( ndr1_0
=> ( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84) ) )
| ! [X85] :
( ndr1_0
=> ( c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85) ) ) )
& ( ! [X86] :
( ndr1_0
=> ( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86) ) )
| ! [X87] :
( ndr1_0
=> ( ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87) ) )
| hskp18 )
& ( ! [X88] :
( ndr1_0
=> ( c1_1(X88)
| c3_1(X88)
| ~ c2_1(X88) ) )
| ! [X89] :
( ndr1_0
=> ( c1_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89) ) )
| ! [X90] :
( ndr1_0
=> ( ~ c1_1(X90)
| ~ c2_1(X90)
| ~ c3_1(X90) ) ) )
& ( ! [X91] :
( ndr1_0
=> ( c1_1(X91)
| c3_1(X91)
| ~ c2_1(X91) ) )
| hskp22
| hskp21 )
& ( ! [X92] :
( ndr1_0
=> ( c1_1(X92)
| c3_1(X92)
| ~ c2_1(X92) ) )
| hskp1
| hskp19 )
& ( ! [X93] :
( ndr1_0
=> ( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) ) )
| hskp23
| hskp17 )
& ( ! [X94] :
( ndr1_0
=> ( c1_1(X94)
| ~ c0_1(X94)
| ~ c2_1(X94) ) )
| ! [X95] :
( ndr1_0
=> ( c1_1(X95)
| ~ c2_1(X95)
| ~ c3_1(X95) ) )
| ! [X96] :
( ndr1_0
=> ( ~ c0_1(X96)
| ~ c2_1(X96)
| ~ c3_1(X96) ) ) )
& ( ! [X97] :
( ndr1_0
=> ( c1_1(X97)
| ~ c0_1(X97)
| ~ c2_1(X97) ) )
| ! [X98] :
( ndr1_0
=> ( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98) ) )
| hskp24 )
& ( ! [X99] :
( ndr1_0
=> ( c1_1(X99)
| ~ c0_1(X99)
| ~ c2_1(X99) ) )
| ! [X100] :
( ndr1_0
=> ( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100) ) )
| hskp1 )
& ( ! [X101] :
( ndr1_0
=> ( c1_1(X101)
| ~ c0_1(X101)
| ~ c2_1(X101) ) )
| hskp4
| hskp7 )
& ( ! [X102] :
( ndr1_0
=> ( c1_1(X102)
| ~ c0_1(X102)
| ~ c3_1(X102) ) )
| ! [X103] :
( ndr1_0
=> ( c2_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103) ) )
| hskp19 )
& ( ! [X104] :
( ndr1_0
=> ( c1_1(X104)
| ~ c2_1(X104)
| ~ c3_1(X104) ) )
| hskp3
| hskp17 )
& ( ! [X105] :
( ndr1_0
=> ( c2_1(X105)
| c3_1(X105)
| ~ c0_1(X105) ) )
| hskp18
| hskp11 )
& ( ! [X106] :
( ndr1_0
=> ( c2_1(X106)
| c3_1(X106)
| ~ c0_1(X106) ) )
| hskp16
| hskp2 )
& ( ! [X107] :
( ndr1_0
=> ( c2_1(X107)
| ~ c0_1(X107)
| ~ c1_1(X107) ) )
| hskp7
| hskp20 )
& ( ! [X108] :
( ndr1_0
=> ( c2_1(X108)
| ~ c0_1(X108)
| ~ c3_1(X108) ) )
| hskp4
| hskp7 )
& ( ! [X109] :
( ndr1_0
=> ( c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109) ) )
| ! [X110] :
( ndr1_0
=> ( c3_1(X110)
| ~ c0_1(X110)
| ~ c2_1(X110) ) )
| hskp11 )
& ( ! [X111] :
( ndr1_0
=> ( c2_1(X111)
| ~ c1_1(X111)
| ~ c3_1(X111) ) )
| ! [X112] :
( ndr1_0
=> ( ~ c0_1(X112)
| ~ c1_1(X112)
| ~ c2_1(X112) ) )
| hskp2 )
& ( ! [X113] :
( ndr1_0
=> ( c3_1(X113)
| ~ c0_1(X113)
| ~ c1_1(X113) ) )
| hskp27
| hskp19 )
& ( ! [X114] :
( ndr1_0
=> ( c3_1(X114)
| ~ c0_1(X114)
| ~ c1_1(X114) ) )
| hskp29
| hskp0 )
& ( ! [X115] :
( ndr1_0
=> ( c3_1(X115)
| ~ c0_1(X115)
| ~ c1_1(X115) ) )
| hskp18
| hskp8 )
& ( ! [X116] :
( ndr1_0
=> ( c3_1(X116)
| ~ c0_1(X116)
| ~ c1_1(X116) ) )
| hskp0 )
& ( ! [X117] :
( ndr1_0
=> ( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117) ) )
| hskp6 )
& ( ! [X118] :
( ndr1_0
=> ( c3_1(X118)
| ~ c0_1(X118)
| ~ c2_1(X118) ) )
| hskp16
| hskp25 )
& ( ! [X119] :
( ndr1_0
=> ( ~ c0_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119) ) )
| hskp27
| hskp29 )
& ( ! [X120] :
( ndr1_0
=> ( ~ c0_1(X120)
| ~ c2_1(X120)
| ~ c3_1(X120) ) )
| hskp1
| hskp9 )
& ( hskp28
| hskp4
| hskp22 )
& ( hskp27
| hskp9
| hskp2 )
& ( hskp12
| hskp13 )
& ( hskp13
| hskp18
| hskp8 )
& ( hskp18
| hskp4
| hskp20 )
& ( hskp18
| hskp19
| hskp17 )
& ( hskp26
| hskp25
| hskp5 )
& ( hskp22
| hskp0
| hskp11 )
& ( hskp22
| hskp8
| hskp15 )
& ( hskp16
| hskp6
| hskp15 )
& ( hskp16
| hskp10
| hskp8 )
& ( hskp19
| hskp8
| hskp15 ) ),
inference(flattening,[],[f2]) ).
fof(f4,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a97)
& ~ c2_1(a97)
& ~ c3_1(a97) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a98)
& ~ c1_1(a98)
& ~ c3_1(a98) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a99)
& ~ c0_1(a99)
& ~ c1_1(a99) ) )
& ( ~ hskp3
| ( ndr1_0
& c2_1(a100)
& c3_1(a100)
& ~ c1_1(a100) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a103)
& c2_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a104)
& ~ c0_1(a104)
& ~ c3_1(a104) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a105)
& c2_1(a105)
& ~ c3_1(a105) ) )
& ( ~ hskp7
| ( ndr1_0
& c2_1(a106)
& c3_1(a106)
& ~ c0_1(a106) ) )
& ( ~ hskp8
| ( ndr1_0
& c3_1(a107)
& ~ c0_1(a107)
& ~ c2_1(a107) ) )
& ( ~ hskp9
| ( ndr1_0
& c1_1(a108)
& c2_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a110)
& ~ c2_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a112)
& ~ c0_1(a112)
& ~ c1_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a113)
& c1_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a116)
& c1_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a120)
& ~ c1_1(a120)
& ~ c2_1(a120) ) )
& ( ~ hskp15
| ( ndr1_0
& ~ c0_1(a121)
& ~ c2_1(a121)
& ~ c3_1(a121) ) )
& ( ~ hskp16
| ( ndr1_0
& c0_1(a122)
& ~ c1_1(a122)
& ~ c2_1(a122) ) )
& ( ~ hskp17
| ( ndr1_0
& c2_1(a124)
& ~ c1_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a129)
& c2_1(a129)
& ~ c1_1(a129) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a130)
& c3_1(a130)
& ~ c2_1(a130) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c1_1(a132)
& ~ c2_1(a132)
& ~ c3_1(a132) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a136)
& ~ c1_1(a136)
& ~ c2_1(a136) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a138)
& c3_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a145)
& c3_1(a145)
& ~ c0_1(a145) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a173)
& ~ c0_1(a173)
& ~ c3_1(a173) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a195)
& c3_1(a195)
& ~ c1_1(a195) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a101)
& c1_1(a101)
& c3_1(a101) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a137)
& c1_1(a137)
& c2_1(a137) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a166)
& c2_1(a166)
& c3_1(a166) ) )
& ( ! [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] :
( c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c0_1(X4)
| c2_1(X4)
| ~ c3_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| hskp1
| hskp2 )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c3_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c0_1(X7)
| c1_1(X7)
| ~ c3_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c0_1(X8)
| c3_1(X8)
| ~ c1_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c1_1(X10)
| ~ c0_1(X10)
| ~ c3_1(X10)
| ~ ndr1_0 )
| ! [X11] :
( c3_1(X11)
| ~ c0_1(X11)
| ~ c1_1(X11)
| ~ ndr1_0 ) )
& ( ! [X12] :
( c0_1(X12)
| c1_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c0_1(X13)
| c3_1(X13)
| ~ c1_1(X13)
| ~ ndr1_0 )
| ! [X14] :
( ~ c1_1(X14)
| ~ c2_1(X14)
| ~ c3_1(X14)
| ~ ndr1_0 ) )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| ~ c2_1(X15)
| ~ ndr1_0 )
| ! [X16] :
( c0_1(X16)
| ~ c1_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0 )
| ! [X18] :
( c1_1(X18)
| c2_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| hskp27 )
& ( ! [X19] :
( c0_1(X19)
| c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 )
| ! [X20] :
( c1_1(X20)
| c3_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X21] :
( c0_1(X21)
| c1_1(X21)
| ~ c2_1(X21)
| ~ ndr1_0 )
| hskp4
| hskp5 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22)
| ~ ndr1_0 )
| hskp6
| hskp7 )
& ( ! [X23] :
( c0_1(X23)
| c1_1(X23)
| ~ c3_1(X23)
| ~ ndr1_0 )
| ! [X24] :
( c1_1(X24)
| c2_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X25] :
( c0_1(X25)
| c1_1(X25)
| ~ c3_1(X25)
| ~ ndr1_0 )
| hskp9
| hskp6 )
& ( ! [X26] :
( c0_1(X26)
| c2_1(X26)
| c3_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c0_1(X27)
| c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28)
| ~ ndr1_0 ) )
& ( ! [X29] :
( c0_1(X29)
| c2_1(X29)
| c3_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( c0_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0 ) )
& ( ! [X32] :
( c0_1(X32)
| c2_1(X32)
| c3_1(X32)
| ~ ndr1_0 )
| ! [X33] :
( c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X34] :
( c0_1(X34)
| c2_1(X34)
| c3_1(X34)
| ~ ndr1_0 )
| hskp5
| hskp11 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c0_1(X36)
| ~ c1_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c0_1(X38)
| ~ c1_1(X38)
| ~ c2_1(X38)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X39] :
( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39)
| ~ ndr1_0 )
| ! [X40] :
( c1_1(X40)
| c2_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0 )
| ! [X41] :
( ~ c1_1(X41)
| ~ c2_1(X41)
| ~ c3_1(X41)
| ~ ndr1_0 ) )
& ( ! [X42] :
( c0_1(X42)
| c2_1(X42)
| ~ c1_1(X42)
| ~ ndr1_0 )
| ! [X43] :
( c1_1(X43)
| ~ c0_1(X43)
| ~ c3_1(X43)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X44] :
( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| ! [X46] :
( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46)
| ~ ndr1_0 ) )
& ( ! [X47] :
( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47)
| ~ ndr1_0 )
| hskp13
| hskp5 )
& ( ! [X48] :
( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0 )
| ! [X49] :
( c3_1(X49)
| ~ c0_1(X49)
| ~ c1_1(X49)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X50] :
( c0_1(X50)
| c3_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0 )
| hskp1
| hskp14 )
& ( ! [X51] :
( c0_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| hskp15 )
& ( ! [X53] :
( c0_1(X53)
| ~ c1_1(X53)
| ~ c2_1(X53)
| ~ ndr1_0 )
| ! [X54] :
( c2_1(X54)
| ~ c0_1(X54)
| ~ c1_1(X54)
| ~ ndr1_0 )
| ! [X55] :
( ~ c0_1(X55)
| ~ c1_1(X55)
| ~ c2_1(X55)
| ~ ndr1_0 ) )
& ( ! [X56] :
( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0 )
| ! [X57] :
( c3_1(X57)
| ~ c0_1(X57)
| ~ c2_1(X57)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X58] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X60] :
( c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| ! [X61] :
( c1_1(X61)
| c2_1(X61)
| c3_1(X61)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X62] :
( c0_1(X62)
| ~ c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0 )
| ! [X63] :
( ~ c0_1(X63)
| ~ c2_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X64] :
( c0_1(X64)
| ~ c2_1(X64)
| ~ c3_1(X64)
| ~ ndr1_0 )
| hskp9
| hskp17 )
& ( ! [X65] :
( c1_1(X65)
| c2_1(X65)
| c3_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66)
| ~ ndr1_0 )
| ! [X67] :
( c3_1(X67)
| ~ c1_1(X67)
| ~ c2_1(X67)
| ~ ndr1_0 ) )
& ( ! [X68] :
( c1_1(X68)
| c2_1(X68)
| c3_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c3_1(X69)
| ~ c0_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0 )
| hskp15 )
& ( ! [X70] :
( c1_1(X70)
| c2_1(X70)
| c3_1(X70)
| ~ ndr1_0 )
| hskp18
| hskp19 )
& ( ! [X71] :
( c1_1(X71)
| c2_1(X71)
| ~ c0_1(X71)
| ~ ndr1_0 )
| ! [X72] :
( c1_1(X72)
| c3_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X73] :
( c1_1(X73)
| c2_1(X73)
| ~ c0_1(X73)
| ~ ndr1_0 )
| ! [X74] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74)
| ~ ndr1_0 )
| ! [X75] :
( c3_1(X75)
| ~ c0_1(X75)
| ~ c2_1(X75)
| ~ ndr1_0 ) )
& ( ! [X76] :
( c1_1(X76)
| c2_1(X76)
| ~ c0_1(X76)
| ~ ndr1_0 )
| ! [X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0 )
| hskp20 )
& ( ! [X78] :
( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78)
| ~ ndr1_0 )
| hskp6
| hskp20 )
& ( ! [X79] :
( c1_1(X79)
| c2_1(X79)
| ~ c0_1(X79)
| ~ ndr1_0 )
| hskp2
| hskp21 )
& ( ! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c3_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X82] :
( c1_1(X82)
| c2_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 )
| hskp22
| hskp6 )
& ( ! [X83] :
( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83)
| ~ ndr1_0 )
| ! [X84] :
( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85)
| ~ ndr1_0 ) )
& ( ! [X86] :
( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86)
| ~ ndr1_0 )
| ! [X87] :
( ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87)
| ~ ndr1_0 )
| hskp18 )
& ( ! [X88] :
( c1_1(X88)
| c3_1(X88)
| ~ c2_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c1_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0 )
| ! [X90] :
( ~ c1_1(X90)
| ~ c2_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 ) )
& ( ! [X91] :
( c1_1(X91)
| c3_1(X91)
| ~ c2_1(X91)
| ~ ndr1_0 )
| hskp22
| hskp21 )
& ( ! [X92] :
( c1_1(X92)
| c3_1(X92)
| ~ c2_1(X92)
| ~ ndr1_0 )
| hskp1
| hskp19 )
& ( ! [X93] :
( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93)
| ~ ndr1_0 )
| hskp23
| hskp17 )
& ( ! [X94] :
( c1_1(X94)
| ~ c0_1(X94)
| ~ c2_1(X94)
| ~ ndr1_0 )
| ! [X95] :
( c1_1(X95)
| ~ c2_1(X95)
| ~ c3_1(X95)
| ~ ndr1_0 )
| ! [X96] :
( ~ c0_1(X96)
| ~ c2_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0 ) )
& ( ! [X97] :
( c1_1(X97)
| ~ c0_1(X97)
| ~ c2_1(X97)
| ~ ndr1_0 )
| ! [X98] :
( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| hskp24 )
& ( ! [X99] :
( c1_1(X99)
| ~ c0_1(X99)
| ~ c2_1(X99)
| ~ ndr1_0 )
| ! [X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X101] :
( c1_1(X101)
| ~ c0_1(X101)
| ~ c2_1(X101)
| ~ ndr1_0 )
| hskp4
| hskp7 )
& ( ! [X102] :
( c1_1(X102)
| ~ c0_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0 )
| ! [X103] :
( c2_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp19 )
& ( ! [X104] :
( c1_1(X104)
| ~ c2_1(X104)
| ~ c3_1(X104)
| ~ ndr1_0 )
| hskp3
| hskp17 )
& ( ! [X105] :
( c2_1(X105)
| c3_1(X105)
| ~ c0_1(X105)
| ~ ndr1_0 )
| hskp18
| hskp11 )
& ( ! [X106] :
( c2_1(X106)
| c3_1(X106)
| ~ c0_1(X106)
| ~ ndr1_0 )
| hskp16
| hskp2 )
& ( ! [X107] :
( c2_1(X107)
| ~ c0_1(X107)
| ~ c1_1(X107)
| ~ ndr1_0 )
| hskp7
| hskp20 )
& ( ! [X108] :
( c2_1(X108)
| ~ c0_1(X108)
| ~ c3_1(X108)
| ~ ndr1_0 )
| hskp4
| hskp7 )
& ( ! [X109] :
( c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109)
| ~ ndr1_0 )
| ! [X110] :
( c3_1(X110)
| ~ c0_1(X110)
| ~ c2_1(X110)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X111] :
( c2_1(X111)
| ~ c1_1(X111)
| ~ c3_1(X111)
| ~ ndr1_0 )
| ! [X112] :
( ~ c0_1(X112)
| ~ c1_1(X112)
| ~ c2_1(X112)
| ~ ndr1_0 )
| hskp2 )
& ( ! [X113] :
( c3_1(X113)
| ~ c0_1(X113)
| ~ c1_1(X113)
| ~ ndr1_0 )
| hskp27
| hskp19 )
& ( ! [X114] :
( c3_1(X114)
| ~ c0_1(X114)
| ~ c1_1(X114)
| ~ ndr1_0 )
| hskp29
| hskp0 )
& ( ! [X115] :
( c3_1(X115)
| ~ c0_1(X115)
| ~ c1_1(X115)
| ~ ndr1_0 )
| hskp18
| hskp8 )
& ( ! [X116] :
( c3_1(X116)
| ~ c0_1(X116)
| ~ c1_1(X116)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X117] :
( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X118] :
( c3_1(X118)
| ~ c0_1(X118)
| ~ c2_1(X118)
| ~ ndr1_0 )
| hskp16
| hskp25 )
& ( ! [X119] :
( ~ c0_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119)
| ~ ndr1_0 )
| hskp27
| hskp29 )
& ( ! [X120] :
( ~ c0_1(X120)
| ~ c2_1(X120)
| ~ c3_1(X120)
| ~ ndr1_0 )
| hskp1
| hskp9 )
& ( hskp28
| hskp4
| hskp22 )
& ( hskp27
| hskp9
| hskp2 )
& ( hskp12
| hskp13 )
& ( hskp13
| hskp18
| hskp8 )
& ( hskp18
| hskp4
| hskp20 )
& ( hskp18
| hskp19
| hskp17 )
& ( hskp26
| hskp25
| hskp5 )
& ( hskp22
| hskp0
| hskp11 )
& ( hskp22
| hskp8
| hskp15 )
& ( hskp16
| hskp6
| hskp15 )
& ( hskp16
| hskp10
| hskp8 )
& ( hskp19
| hskp8
| hskp15 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ~ hskp0
| ( ndr1_0
& c0_1(a97)
& ~ c2_1(a97)
& ~ c3_1(a97) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a98)
& ~ c1_1(a98)
& ~ c3_1(a98) ) )
& ( ~ hskp2
| ( ndr1_0
& c2_1(a99)
& ~ c0_1(a99)
& ~ c1_1(a99) ) )
& ( ~ hskp3
| ( ndr1_0
& c2_1(a100)
& c3_1(a100)
& ~ c1_1(a100) ) )
& ( ~ hskp4
| ( ndr1_0
& c0_1(a103)
& c2_1(a103)
& ~ c3_1(a103) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a104)
& ~ c0_1(a104)
& ~ c3_1(a104) ) )
& ( ~ hskp6
| ( ndr1_0
& c1_1(a105)
& c2_1(a105)
& ~ c3_1(a105) ) )
& ( ~ hskp7
| ( ndr1_0
& c2_1(a106)
& c3_1(a106)
& ~ c0_1(a106) ) )
& ( ~ hskp8
| ( ndr1_0
& c3_1(a107)
& ~ c0_1(a107)
& ~ c2_1(a107) ) )
& ( ~ hskp9
| ( ndr1_0
& c1_1(a108)
& c2_1(a108)
& ~ c0_1(a108) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a110)
& ~ c2_1(a110)
& ~ c3_1(a110) ) )
& ( ~ hskp11
| ( ndr1_0
& c3_1(a112)
& ~ c0_1(a112)
& ~ c1_1(a112) ) )
& ( ~ hskp12
| ( ndr1_0
& c0_1(a113)
& c1_1(a113)
& ~ c2_1(a113) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a116)
& c1_1(a116)
& ~ c3_1(a116) ) )
& ( ~ hskp14
| ( ndr1_0
& ~ c0_1(a120)
& ~ c1_1(a120)
& ~ c2_1(a120) ) )
& ( ~ hskp15
| ( ndr1_0
& ~ c0_1(a121)
& ~ c2_1(a121)
& ~ c3_1(a121) ) )
& ( ~ hskp16
| ( ndr1_0
& c0_1(a122)
& ~ c1_1(a122)
& ~ c2_1(a122) ) )
& ( ~ hskp17
| ( ndr1_0
& c2_1(a124)
& ~ c1_1(a124)
& ~ c3_1(a124) ) )
& ( ~ hskp18
| ( ndr1_0
& c0_1(a129)
& c2_1(a129)
& ~ c1_1(a129) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a130)
& c3_1(a130)
& ~ c2_1(a130) ) )
& ( ~ hskp20
| ( ndr1_0
& ~ c1_1(a132)
& ~ c2_1(a132)
& ~ c3_1(a132) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a136)
& ~ c1_1(a136)
& ~ c2_1(a136) ) )
& ( ~ hskp22
| ( ndr1_0
& c0_1(a138)
& c3_1(a138)
& ~ c2_1(a138) ) )
& ( ~ hskp23
| ( ndr1_0
& c1_1(a145)
& c3_1(a145)
& ~ c0_1(a145) ) )
& ( ~ hskp24
| ( ndr1_0
& ~ c0_1(a147)
& ~ c1_1(a147)
& ~ c3_1(a147) ) )
& ( ~ hskp25
| ( ndr1_0
& c1_1(a173)
& ~ c0_1(a173)
& ~ c3_1(a173) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a195)
& c3_1(a195)
& ~ c1_1(a195) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a101)
& c1_1(a101)
& c3_1(a101) ) )
& ( ~ hskp28
| ( ndr1_0
& c0_1(a137)
& c1_1(a137)
& c2_1(a137) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a166)
& c2_1(a166)
& c3_1(a166) ) )
& ( ! [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] :
( c0_1(X2)
| c3_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c0_1(X4)
| c2_1(X4)
| ~ c3_1(X4)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X5] :
( c0_1(X5)
| c1_1(X5)
| c2_1(X5)
| ~ ndr1_0 )
| hskp1
| hskp2 )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c3_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c0_1(X7)
| c1_1(X7)
| ~ c3_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( c0_1(X8)
| c3_1(X8)
| ~ c1_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c3_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c1_1(X10)
| ~ c0_1(X10)
| ~ c3_1(X10)
| ~ ndr1_0 )
| ! [X11] :
( c3_1(X11)
| ~ c0_1(X11)
| ~ c1_1(X11)
| ~ ndr1_0 ) )
& ( ! [X12] :
( c0_1(X12)
| c1_1(X12)
| ~ c2_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c0_1(X13)
| c3_1(X13)
| ~ c1_1(X13)
| ~ ndr1_0 )
| ! [X14] :
( ~ c1_1(X14)
| ~ c2_1(X14)
| ~ c3_1(X14)
| ~ ndr1_0 ) )
& ( ! [X15] :
( c0_1(X15)
| c1_1(X15)
| ~ c2_1(X15)
| ~ ndr1_0 )
| ! [X16] :
( c0_1(X16)
| ~ c1_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0 )
| ! [X18] :
( c1_1(X18)
| c2_1(X18)
| ~ c3_1(X18)
| ~ ndr1_0 )
| hskp27 )
& ( ! [X19] :
( c0_1(X19)
| c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 )
| ! [X20] :
( c1_1(X20)
| c3_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X21] :
( c0_1(X21)
| c1_1(X21)
| ~ c2_1(X21)
| ~ ndr1_0 )
| hskp4
| hskp5 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c2_1(X22)
| ~ ndr1_0 )
| hskp6
| hskp7 )
& ( ! [X23] :
( c0_1(X23)
| c1_1(X23)
| ~ c3_1(X23)
| ~ ndr1_0 )
| ! [X24] :
( c1_1(X24)
| c2_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X25] :
( c0_1(X25)
| c1_1(X25)
| ~ c3_1(X25)
| ~ ndr1_0 )
| hskp9
| hskp6 )
& ( ! [X26] :
( c0_1(X26)
| c2_1(X26)
| c3_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c0_1(X27)
| c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 )
| ! [X28] :
( c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28)
| ~ ndr1_0 ) )
& ( ! [X29] :
( c0_1(X29)
| c2_1(X29)
| c3_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( c0_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 )
| ! [X31] :
( c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0 ) )
& ( ! [X32] :
( c0_1(X32)
| c2_1(X32)
| c3_1(X32)
| ~ ndr1_0 )
| ! [X33] :
( c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X34] :
( c0_1(X34)
| c2_1(X34)
| c3_1(X34)
| ~ ndr1_0 )
| hskp5
| hskp11 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c0_1(X36)
| ~ c1_1(X36)
| ~ c2_1(X36)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c0_1(X38)
| ~ c1_1(X38)
| ~ c2_1(X38)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X39] :
( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39)
| ~ ndr1_0 )
| ! [X40] :
( c1_1(X40)
| c2_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0 )
| ! [X41] :
( ~ c1_1(X41)
| ~ c2_1(X41)
| ~ c3_1(X41)
| ~ ndr1_0 ) )
& ( ! [X42] :
( c0_1(X42)
| c2_1(X42)
| ~ c1_1(X42)
| ~ ndr1_0 )
| ! [X43] :
( c1_1(X43)
| ~ c0_1(X43)
| ~ c3_1(X43)
| ~ ndr1_0 )
| hskp10 )
& ( ! [X44] :
( c0_1(X44)
| c2_1(X44)
| ~ c3_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( c0_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| ! [X46] :
( c1_1(X46)
| c2_1(X46)
| ~ c3_1(X46)
| ~ ndr1_0 ) )
& ( ! [X47] :
( c0_1(X47)
| c2_1(X47)
| ~ c3_1(X47)
| ~ ndr1_0 )
| hskp13
| hskp5 )
& ( ! [X48] :
( c0_1(X48)
| c3_1(X48)
| ~ c1_1(X48)
| ~ ndr1_0 )
| ! [X49] :
( c3_1(X49)
| ~ c0_1(X49)
| ~ c1_1(X49)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X50] :
( c0_1(X50)
| c3_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0 )
| hskp1
| hskp14 )
& ( ! [X51] :
( c0_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0 )
| ! [X52] :
( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| hskp15 )
& ( ! [X53] :
( c0_1(X53)
| ~ c1_1(X53)
| ~ c2_1(X53)
| ~ ndr1_0 )
| ! [X54] :
( c2_1(X54)
| ~ c0_1(X54)
| ~ c1_1(X54)
| ~ ndr1_0 )
| ! [X55] :
( ~ c0_1(X55)
| ~ c1_1(X55)
| ~ c2_1(X55)
| ~ ndr1_0 ) )
& ( ! [X56] :
( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0 )
| ! [X57] :
( c3_1(X57)
| ~ c0_1(X57)
| ~ c2_1(X57)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X58] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0 )
| ! [X59] :
( c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X60] :
( c0_1(X60)
| ~ c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| ! [X61] :
( c1_1(X61)
| c2_1(X61)
| c3_1(X61)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X62] :
( c0_1(X62)
| ~ c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0 )
| ! [X63] :
( ~ c0_1(X63)
| ~ c2_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X64] :
( c0_1(X64)
| ~ c2_1(X64)
| ~ c3_1(X64)
| ~ ndr1_0 )
| hskp9
| hskp17 )
& ( ! [X65] :
( c1_1(X65)
| c2_1(X65)
| c3_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66)
| ~ ndr1_0 )
| ! [X67] :
( c3_1(X67)
| ~ c1_1(X67)
| ~ c2_1(X67)
| ~ ndr1_0 ) )
& ( ! [X68] :
( c1_1(X68)
| c2_1(X68)
| c3_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c3_1(X69)
| ~ c0_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0 )
| hskp15 )
& ( ! [X70] :
( c1_1(X70)
| c2_1(X70)
| c3_1(X70)
| ~ ndr1_0 )
| hskp18
| hskp19 )
& ( ! [X71] :
( c1_1(X71)
| c2_1(X71)
| ~ c0_1(X71)
| ~ ndr1_0 )
| ! [X72] :
( c1_1(X72)
| c3_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X73] :
( c1_1(X73)
| c2_1(X73)
| ~ c0_1(X73)
| ~ ndr1_0 )
| ! [X74] :
( c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74)
| ~ ndr1_0 )
| ! [X75] :
( c3_1(X75)
| ~ c0_1(X75)
| ~ c2_1(X75)
| ~ ndr1_0 ) )
& ( ! [X76] :
( c1_1(X76)
| c2_1(X76)
| ~ c0_1(X76)
| ~ ndr1_0 )
| ! [X77] :
( c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0 )
| hskp20 )
& ( ! [X78] :
( c1_1(X78)
| c2_1(X78)
| ~ c0_1(X78)
| ~ ndr1_0 )
| hskp6
| hskp20 )
& ( ! [X79] :
( c1_1(X79)
| c2_1(X79)
| ~ c0_1(X79)
| ~ ndr1_0 )
| hskp2
| hskp21 )
& ( ! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c3_1(X80)
| ~ ndr1_0 )
| ! [X81] :
( c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81)
| ~ ndr1_0 )
| hskp28 )
& ( ! [X82] :
( c1_1(X82)
| c2_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 )
| hskp22
| hskp6 )
& ( ! [X83] :
( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83)
| ~ ndr1_0 )
| ! [X84] :
( c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ~ ndr1_0 )
| ! [X85] :
( c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85)
| ~ ndr1_0 ) )
& ( ! [X86] :
( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86)
| ~ ndr1_0 )
| ! [X87] :
( ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87)
| ~ ndr1_0 )
| hskp18 )
& ( ! [X88] :
( c1_1(X88)
| c3_1(X88)
| ~ c2_1(X88)
| ~ ndr1_0 )
| ! [X89] :
( c1_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0 )
| ! [X90] :
( ~ c1_1(X90)
| ~ c2_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 ) )
& ( ! [X91] :
( c1_1(X91)
| c3_1(X91)
| ~ c2_1(X91)
| ~ ndr1_0 )
| hskp22
| hskp21 )
& ( ! [X92] :
( c1_1(X92)
| c3_1(X92)
| ~ c2_1(X92)
| ~ ndr1_0 )
| hskp1
| hskp19 )
& ( ! [X93] :
( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93)
| ~ ndr1_0 )
| hskp23
| hskp17 )
& ( ! [X94] :
( c1_1(X94)
| ~ c0_1(X94)
| ~ c2_1(X94)
| ~ ndr1_0 )
| ! [X95] :
( c1_1(X95)
| ~ c2_1(X95)
| ~ c3_1(X95)
| ~ ndr1_0 )
| ! [X96] :
( ~ c0_1(X96)
| ~ c2_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0 ) )
& ( ! [X97] :
( c1_1(X97)
| ~ c0_1(X97)
| ~ c2_1(X97)
| ~ ndr1_0 )
| ! [X98] :
( c2_1(X98)
| ~ c0_1(X98)
| ~ c3_1(X98)
| ~ ndr1_0 )
| hskp24 )
& ( ! [X99] :
( c1_1(X99)
| ~ c0_1(X99)
| ~ c2_1(X99)
| ~ ndr1_0 )
| ! [X100] :
( c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X101] :
( c1_1(X101)
| ~ c0_1(X101)
| ~ c2_1(X101)
| ~ ndr1_0 )
| hskp4
| hskp7 )
& ( ! [X102] :
( c1_1(X102)
| ~ c0_1(X102)
| ~ c3_1(X102)
| ~ ndr1_0 )
| ! [X103] :
( c2_1(X103)
| ~ c1_1(X103)
| ~ c3_1(X103)
| ~ ndr1_0 )
| hskp19 )
& ( ! [X104] :
( c1_1(X104)
| ~ c2_1(X104)
| ~ c3_1(X104)
| ~ ndr1_0 )
| hskp3
| hskp17 )
& ( ! [X105] :
( c2_1(X105)
| c3_1(X105)
| ~ c0_1(X105)
| ~ ndr1_0 )
| hskp18
| hskp11 )
& ( ! [X106] :
( c2_1(X106)
| c3_1(X106)
| ~ c0_1(X106)
| ~ ndr1_0 )
| hskp16
| hskp2 )
& ( ! [X107] :
( c2_1(X107)
| ~ c0_1(X107)
| ~ c1_1(X107)
| ~ ndr1_0 )
| hskp7
| hskp20 )
& ( ! [X108] :
( c2_1(X108)
| ~ c0_1(X108)
| ~ c3_1(X108)
| ~ ndr1_0 )
| hskp4
| hskp7 )
& ( ! [X109] :
( c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109)
| ~ ndr1_0 )
| ! [X110] :
( c3_1(X110)
| ~ c0_1(X110)
| ~ c2_1(X110)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X111] :
( c2_1(X111)
| ~ c1_1(X111)
| ~ c3_1(X111)
| ~ ndr1_0 )
| ! [X112] :
( ~ c0_1(X112)
| ~ c1_1(X112)
| ~ c2_1(X112)
| ~ ndr1_0 )
| hskp2 )
& ( ! [X113] :
( c3_1(X113)
| ~ c0_1(X113)
| ~ c1_1(X113)
| ~ ndr1_0 )
| hskp27
| hskp19 )
& ( ! [X114] :
( c3_1(X114)
| ~ c0_1(X114)
| ~ c1_1(X114)
| ~ ndr1_0 )
| hskp29
| hskp0 )
& ( ! [X115] :
( c3_1(X115)
| ~ c0_1(X115)
| ~ c1_1(X115)
| ~ ndr1_0 )
| hskp18
| hskp8 )
& ( ! [X116] :
( c3_1(X116)
| ~ c0_1(X116)
| ~ c1_1(X116)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X117] :
( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X118] :
( c3_1(X118)
| ~ c0_1(X118)
| ~ c2_1(X118)
| ~ ndr1_0 )
| hskp16
| hskp25 )
& ( ! [X119] :
( ~ c0_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119)
| ~ ndr1_0 )
| hskp27
| hskp29 )
& ( ! [X120] :
( ~ c0_1(X120)
| ~ c2_1(X120)
| ~ c3_1(X120)
| ~ ndr1_0 )
| hskp1
| hskp9 )
& ( hskp28
| hskp4
| hskp22 )
& ( hskp27
| hskp9
| hskp2 )
& ( hskp12
| hskp13 )
& ( hskp13
| hskp18
| hskp8 )
& ( hskp18
| hskp4
| hskp20 )
& ( hskp18
| hskp19
| hskp17 )
& ( hskp26
| hskp25
| hskp5 )
& ( hskp22
| hskp0
| hskp11 )
& ( hskp22
| hskp8
| hskp15 )
& ( hskp16
| hskp6
| hskp15 )
& ( hskp16
| hskp10
| hskp8 )
& ( hskp19
| hskp8
| hskp15 ) ),
inference(flattening,[],[f4]) ).
fof(f8,plain,
( hskp16
| hskp6
| hskp15 ),
inference(cnf_transformation,[],[f5]) ).
fof(f12,plain,
( hskp18
| hskp19
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f13,plain,
( hskp18
| hskp4
| hskp20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f14,plain,
( hskp13
| hskp18
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f15,plain,
( hskp12
| hskp13 ),
inference(cnf_transformation,[],[f5]) ).
fof(f16,plain,
( hskp27
| hskp9
| hskp2 ),
inference(cnf_transformation,[],[f5]) ).
fof(f18,plain,
! [X120] :
( ~ c0_1(X120)
| ~ c2_1(X120)
| ~ c3_1(X120)
| ~ ndr1_0
| hskp1
| hskp9 ),
inference(cnf_transformation,[],[f5]) ).
fof(f19,plain,
! [X119] :
( ~ c0_1(X119)
| ~ c1_1(X119)
| ~ c2_1(X119)
| ~ ndr1_0
| hskp27
| hskp29 ),
inference(cnf_transformation,[],[f5]) ).
fof(f20,plain,
! [X118] :
( c3_1(X118)
| ~ c0_1(X118)
| ~ c2_1(X118)
| ~ ndr1_0
| hskp16
| hskp25 ),
inference(cnf_transformation,[],[f5]) ).
fof(f21,plain,
! [X117] :
( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117)
| ~ ndr1_0
| hskp6 ),
inference(cnf_transformation,[],[f5]) ).
fof(f22,plain,
! [X116] :
( c3_1(X116)
| ~ c0_1(X116)
| ~ c1_1(X116)
| ~ ndr1_0
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X115] :
( c3_1(X115)
| ~ c0_1(X115)
| ~ c1_1(X115)
| ~ ndr1_0
| hskp18
| hskp8 ),
inference(cnf_transformation,[],[f5]) ).
fof(f25,plain,
! [X113] :
( c3_1(X113)
| ~ c0_1(X113)
| ~ c1_1(X113)
| ~ ndr1_0
| hskp27
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X109,X110] :
( c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109)
| ~ ndr1_0
| c3_1(X110)
| ~ c0_1(X110)
| ~ c2_1(X110)
| ~ ndr1_0
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f28,plain,
! [X108] :
( c2_1(X108)
| ~ c0_1(X108)
| ~ c3_1(X108)
| ~ ndr1_0
| hskp4
| hskp7 ),
inference(cnf_transformation,[],[f5]) ).
fof(f29,plain,
! [X107] :
( c2_1(X107)
| ~ c0_1(X107)
| ~ c1_1(X107)
| ~ ndr1_0
| hskp7
| hskp20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f35,plain,
! [X99,X100] :
( c1_1(X99)
| ~ c0_1(X99)
| ~ c2_1(X99)
| ~ ndr1_0
| c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100)
| ~ ndr1_0
| hskp1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f37,plain,
! [X96,X94,X95] :
( c1_1(X94)
| ~ c0_1(X94)
| ~ c2_1(X94)
| ~ ndr1_0
| c1_1(X95)
| ~ c2_1(X95)
| ~ c3_1(X95)
| ~ ndr1_0
| ~ c0_1(X96)
| ~ c2_1(X96)
| ~ c3_1(X96)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f39,plain,
! [X92] :
( c1_1(X92)
| c3_1(X92)
| ~ c2_1(X92)
| ~ ndr1_0
| hskp1
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f41,plain,
! [X90,X88,X89] :
( c1_1(X88)
| c3_1(X88)
| ~ c2_1(X88)
| ~ ndr1_0
| c1_1(X89)
| ~ c0_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0
| ~ c1_1(X90)
| ~ c2_1(X90)
| ~ c3_1(X90)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f42,plain,
! [X86,X87] :
( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86)
| ~ ndr1_0
| ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87)
| ~ ndr1_0
| hskp18 ),
inference(cnf_transformation,[],[f5]) ).
fof(f43,plain,
! [X83,X84,X85] :
( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83)
| ~ ndr1_0
| c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ~ ndr1_0
| c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f45,plain,
! [X80,X81] :
( c1_1(X80)
| c2_1(X80)
| ~ c3_1(X80)
| ~ ndr1_0
| c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81)
| ~ ndr1_0
| hskp28 ),
inference(cnf_transformation,[],[f5]) ).
fof(f48,plain,
! [X76,X77] :
( c1_1(X76)
| c2_1(X76)
| ~ c0_1(X76)
| ~ ndr1_0
| c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0
| hskp20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f49,plain,
! [X73,X74,X75] :
( c1_1(X73)
| c2_1(X73)
| ~ c0_1(X73)
| ~ ndr1_0
| c1_1(X74)
| ~ c0_1(X74)
| ~ c2_1(X74)
| ~ ndr1_0
| c3_1(X75)
| ~ c0_1(X75)
| ~ c2_1(X75)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f51,plain,
! [X70] :
( c1_1(X70)
| c2_1(X70)
| c3_1(X70)
| ~ ndr1_0
| hskp18
| hskp19 ),
inference(cnf_transformation,[],[f5]) ).
fof(f52,plain,
! [X68,X69] :
( c1_1(X68)
| c2_1(X68)
| c3_1(X68)
| ~ ndr1_0
| c3_1(X69)
| ~ c0_1(X69)
| ~ c2_1(X69)
| ~ ndr1_0
| hskp15 ),
inference(cnf_transformation,[],[f5]) ).
fof(f53,plain,
! [X65,X66,X67] :
( c1_1(X65)
| c2_1(X65)
| c3_1(X65)
| ~ ndr1_0
| c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66)
| ~ ndr1_0
| c3_1(X67)
| ~ c1_1(X67)
| ~ c2_1(X67)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f55,plain,
! [X62,X63] :
( c0_1(X62)
| ~ c2_1(X62)
| ~ c3_1(X62)
| ~ ndr1_0
| ~ c0_1(X63)
| ~ c2_1(X63)
| ~ c3_1(X63)
| ~ ndr1_0
| hskp1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f57,plain,
! [X58,X59] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ~ ndr1_0
| c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59)
| ~ ndr1_0
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f58,plain,
! [X56,X57] :
( c0_1(X56)
| ~ c1_1(X56)
| ~ c2_1(X56)
| ~ ndr1_0
| c3_1(X57)
| ~ c0_1(X57)
| ~ c2_1(X57)
| ~ ndr1_0
| hskp16 ),
inference(cnf_transformation,[],[f5]) ).
fof(f60,plain,
! [X51,X52] :
( c0_1(X51)
| ~ c1_1(X51)
| ~ c2_1(X51)
| ~ ndr1_0
| c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0
| hskp15 ),
inference(cnf_transformation,[],[f5]) ).
fof(f66,plain,
! [X40,X41,X39] :
( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39)
| ~ ndr1_0
| c1_1(X40)
| c2_1(X40)
| ~ c3_1(X40)
| ~ ndr1_0
| ~ c1_1(X41)
| ~ c2_1(X41)
| ~ c3_1(X41)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f70,plain,
! [X32,X33] :
( c0_1(X32)
| c2_1(X32)
| c3_1(X32)
| ~ ndr1_0
| c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33)
| ~ ndr1_0
| hskp10 ),
inference(cnf_transformation,[],[f5]) ).
fof(f71,plain,
! [X31,X29,X30] :
( c0_1(X29)
| c2_1(X29)
| c3_1(X29)
| ~ ndr1_0
| c0_1(X30)
| ~ c2_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0
| c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f72,plain,
! [X28,X26,X27] :
( c0_1(X26)
| c2_1(X26)
| c3_1(X26)
| ~ ndr1_0
| c0_1(X27)
| c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0
| c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f86,plain,
( ~ hskp29
| c3_1(a166) ),
inference(cnf_transformation,[],[f5]) ).
fof(f87,plain,
( ~ hskp29
| c2_1(a166) ),
inference(cnf_transformation,[],[f5]) ).
fof(f88,plain,
( ~ hskp29
| c0_1(a166) ),
inference(cnf_transformation,[],[f5]) ).
fof(f90,plain,
( ~ hskp28
| c2_1(a137) ),
inference(cnf_transformation,[],[f5]) ).
fof(f91,plain,
( ~ hskp28
| c1_1(a137) ),
inference(cnf_transformation,[],[f5]) ).
fof(f92,plain,
( ~ hskp28
| c0_1(a137) ),
inference(cnf_transformation,[],[f5]) ).
fof(f94,plain,
( ~ hskp27
| c3_1(a101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f95,plain,
( ~ hskp27
| c1_1(a101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f96,plain,
( ~ hskp27
| c0_1(a101) ),
inference(cnf_transformation,[],[f5]) ).
fof(f97,plain,
( ~ hskp27
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f102,plain,
( ~ hskp25
| ~ c3_1(a173) ),
inference(cnf_transformation,[],[f5]) ).
fof(f103,plain,
( ~ hskp25
| ~ c0_1(a173) ),
inference(cnf_transformation,[],[f5]) ).
fof(f104,plain,
( ~ hskp25
| c1_1(a173) ),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
( ~ hskp20
| ~ c3_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
( ~ hskp20
| ~ c2_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f124,plain,
( ~ hskp20
| ~ c1_1(a132) ),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
( ~ hskp19
| ~ c2_1(a130) ),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
( ~ hskp19
| c3_1(a130) ),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
( ~ hskp19
| c1_1(a130) ),
inference(cnf_transformation,[],[f5]) ).
fof(f130,plain,
( ~ hskp18
| ~ c1_1(a129) ),
inference(cnf_transformation,[],[f5]) ).
fof(f131,plain,
( ~ hskp18
| c2_1(a129) ),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
( ~ hskp18
| c0_1(a129) ),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
( ~ hskp17
| ~ c3_1(a124) ),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
( ~ hskp17
| ~ c1_1(a124) ),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
( ~ hskp17
| c2_1(a124) ),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
( ~ hskp16
| ~ c2_1(a122) ),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
( ~ hskp16
| ~ c1_1(a122) ),
inference(cnf_transformation,[],[f5]) ).
fof(f140,plain,
( ~ hskp16
| c0_1(a122) ),
inference(cnf_transformation,[],[f5]) ).
fof(f142,plain,
( ~ hskp15
| ~ c3_1(a121) ),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
( ~ hskp15
| ~ c2_1(a121) ),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
( ~ hskp15
| ~ c0_1(a121) ),
inference(cnf_transformation,[],[f5]) ).
fof(f145,plain,
( ~ hskp15
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f150,plain,
( ~ hskp13
| ~ c3_1(a116) ),
inference(cnf_transformation,[],[f5]) ).
fof(f151,plain,
( ~ hskp13
| c1_1(a116) ),
inference(cnf_transformation,[],[f5]) ).
fof(f152,plain,
( ~ hskp13
| c0_1(a116) ),
inference(cnf_transformation,[],[f5]) ).
fof(f154,plain,
( ~ hskp12
| ~ c2_1(a113) ),
inference(cnf_transformation,[],[f5]) ).
fof(f155,plain,
( ~ hskp12
| c1_1(a113) ),
inference(cnf_transformation,[],[f5]) ).
fof(f156,plain,
( ~ hskp12
| c0_1(a113) ),
inference(cnf_transformation,[],[f5]) ).
fof(f158,plain,
( ~ hskp11
| ~ c1_1(a112) ),
inference(cnf_transformation,[],[f5]) ).
fof(f159,plain,
( ~ hskp11
| ~ c0_1(a112) ),
inference(cnf_transformation,[],[f5]) ).
fof(f160,plain,
( ~ hskp11
| c3_1(a112) ),
inference(cnf_transformation,[],[f5]) ).
fof(f162,plain,
( ~ hskp10
| ~ c3_1(a110) ),
inference(cnf_transformation,[],[f5]) ).
fof(f163,plain,
( ~ hskp10
| ~ c2_1(a110) ),
inference(cnf_transformation,[],[f5]) ).
fof(f164,plain,
( ~ hskp10
| c1_1(a110) ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( ~ hskp9
| ~ c0_1(a108) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( ~ hskp9
| c2_1(a108) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( ~ hskp9
| c1_1(a108) ),
inference(cnf_transformation,[],[f5]) ).
fof(f169,plain,
( ~ hskp9
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( ~ hskp8
| ~ c2_1(a107) ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( ~ hskp8
| ~ c0_1(a107) ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( ~ hskp8
| c3_1(a107) ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( ~ hskp7
| ~ c0_1(a106) ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( ~ hskp7
| c3_1(a106) ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( ~ hskp7
| c2_1(a106) ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( ~ hskp6
| ~ c3_1(a105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( ~ hskp6
| c2_1(a105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( ~ hskp6
| c1_1(a105) ),
inference(cnf_transformation,[],[f5]) ).
fof(f186,plain,
( ~ hskp4
| ~ c3_1(a103) ),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
( ~ hskp4
| c2_1(a103) ),
inference(cnf_transformation,[],[f5]) ).
fof(f188,plain,
( ~ hskp4
| c0_1(a103) ),
inference(cnf_transformation,[],[f5]) ).
fof(f197,plain,
( ~ hskp2
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f198,plain,
( ~ hskp1
| ~ c3_1(a98) ),
inference(cnf_transformation,[],[f5]) ).
fof(f199,plain,
( ~ hskp1
| ~ c1_1(a98) ),
inference(cnf_transformation,[],[f5]) ).
fof(f200,plain,
( ~ hskp1
| c0_1(a98) ),
inference(cnf_transformation,[],[f5]) ).
fof(f202,plain,
( ~ hskp0
| ~ c3_1(a97) ),
inference(cnf_transformation,[],[f5]) ).
fof(f203,plain,
( ~ hskp0
| ~ c2_1(a97) ),
inference(cnf_transformation,[],[f5]) ).
fof(f204,plain,
( ~ hskp0
| c0_1(a97) ),
inference(cnf_transformation,[],[f5]) ).
fof(f207,plain,
( hskp0
| c0_1(a97) ),
inference(consistent_polarity_flipping,[],[f204]) ).
fof(f208,plain,
( hskp0
| c2_1(a97) ),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f209,plain,
( hskp0
| ~ c3_1(a97) ),
inference(consistent_polarity_flipping,[],[f202]) ).
fof(f211,plain,
( ~ hskp2
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f197]) ).
fof(f216,plain,
( hskp4
| c0_1(a103) ),
inference(consistent_polarity_flipping,[],[f188]) ).
fof(f217,plain,
( hskp4
| ~ c2_1(a103) ),
inference(consistent_polarity_flipping,[],[f187]) ).
fof(f218,plain,
( hskp4
| ~ c3_1(a103) ),
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f224,plain,
( ~ hskp6
| ~ c2_1(a105) ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f226,plain,
( ~ hskp7
| ~ c2_1(a106) ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f228,plain,
( hskp8
| c3_1(a107) ),
inference(consistent_polarity_flipping,[],[f172]) ).
fof(f229,plain,
( hskp8
| ~ c0_1(a107) ),
inference(consistent_polarity_flipping,[],[f171]) ).
fof(f230,plain,
( hskp8
| c2_1(a107) ),
inference(consistent_polarity_flipping,[],[f170]) ).
fof(f231,plain,
( hskp9
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f232,plain,
( hskp9
| c1_1(a108) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f233,plain,
( hskp9
| ~ c2_1(a108) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f234,plain,
( hskp9
| ~ c0_1(a108) ),
inference(consistent_polarity_flipping,[],[f166]) ).
fof(f236,plain,
( hskp10
| c1_1(a110) ),
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f237,plain,
( hskp10
| c2_1(a110) ),
inference(consistent_polarity_flipping,[],[f163]) ).
fof(f238,plain,
( hskp10
| ~ c3_1(a110) ),
inference(consistent_polarity_flipping,[],[f162]) ).
fof(f240,plain,
( hskp11
| c3_1(a112) ),
inference(consistent_polarity_flipping,[],[f160]) ).
fof(f241,plain,
( hskp11
| ~ c0_1(a112) ),
inference(consistent_polarity_flipping,[],[f159]) ).
fof(f242,plain,
( hskp11
| ~ c1_1(a112) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f244,plain,
( hskp12
| c0_1(a113) ),
inference(consistent_polarity_flipping,[],[f156]) ).
fof(f245,plain,
( hskp12
| c1_1(a113) ),
inference(consistent_polarity_flipping,[],[f155]) ).
fof(f246,plain,
( hskp12
| c2_1(a113) ),
inference(consistent_polarity_flipping,[],[f154]) ).
fof(f248,plain,
( hskp13
| c0_1(a116) ),
inference(consistent_polarity_flipping,[],[f152]) ).
fof(f249,plain,
( hskp13
| c1_1(a116) ),
inference(consistent_polarity_flipping,[],[f151]) ).
fof(f250,plain,
( hskp13
| ~ c3_1(a116) ),
inference(consistent_polarity_flipping,[],[f150]) ).
fof(f253,plain,
( hskp15
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f145]) ).
fof(f254,plain,
( hskp15
| ~ c0_1(a121) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f255,plain,
( hskp15
| c2_1(a121) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f256,plain,
( hskp15
| ~ c3_1(a121) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f258,plain,
( hskp16
| c0_1(a122) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f259,plain,
( hskp16
| ~ c1_1(a122) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f260,plain,
( hskp16
| c2_1(a122) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f262,plain,
( hskp17
| ~ c2_1(a124) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f263,plain,
( hskp17
| ~ c1_1(a124) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f264,plain,
( hskp17
| ~ c3_1(a124) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f266,plain,
( hskp18
| c0_1(a129) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f267,plain,
( hskp18
| ~ c2_1(a129) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f268,plain,
( hskp18
| ~ c1_1(a129) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f270,plain,
( hskp19
| c1_1(a130) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f271,plain,
( hskp19
| c3_1(a130) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f272,plain,
( hskp19
| c2_1(a130) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f274,plain,
( ~ hskp20
| c2_1(a132) ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f285,plain,
( ~ hskp27
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f287,plain,
( ~ hskp28
| ~ c2_1(a137) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f289,plain,
( hskp29
| c0_1(a166) ),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f290,plain,
( hskp29
| ~ c2_1(a166) ),
inference(consistent_polarity_flipping,[],[f87]) ).
fof(f291,plain,
( hskp29
| c3_1(a166) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f305,plain,
! [X28,X26,X27] :
( c0_1(X26)
| ~ c2_1(X26)
| c3_1(X26)
| ndr1_0
| c0_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27)
| ndr1_0
| c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f306,plain,
! [X31,X29,X30] :
( c0_1(X29)
| ~ c2_1(X29)
| c3_1(X29)
| ndr1_0
| c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30)
| ndr1_0
| ~ c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f307,plain,
! [X32,X33] :
( c0_1(X32)
| ~ c2_1(X32)
| c3_1(X32)
| ndr1_0
| ~ c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33)
| ndr1_0
| ~ hskp10 ),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f311,plain,
! [X40,X41,X39] :
( c0_1(X39)
| ~ c2_1(X39)
| ~ c1_1(X39)
| ndr1_0
| c1_1(X40)
| ~ c2_1(X40)
| ~ c3_1(X40)
| ndr1_0
| ~ c1_1(X41)
| c2_1(X41)
| ~ c3_1(X41)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f317,plain,
! [X51,X52] :
( c0_1(X51)
| ~ c1_1(X51)
| c2_1(X51)
| ndr1_0
| c0_1(X52)
| c2_1(X52)
| ~ c3_1(X52)
| ndr1_0
| ~ hskp15 ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f319,plain,
! [X56,X57] :
( c0_1(X56)
| ~ c1_1(X56)
| c2_1(X56)
| ndr1_0
| c3_1(X57)
| ~ c0_1(X57)
| c2_1(X57)
| ndr1_0
| ~ hskp16 ),
inference(consistent_polarity_flipping,[],[f58]) ).
fof(f320,plain,
! [X58,X59] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ndr1_0
| c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59)
| ndr1_0
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f57]) ).
fof(f322,plain,
! [X62,X63] :
( c0_1(X62)
| c2_1(X62)
| ~ c3_1(X62)
| ndr1_0
| ~ c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63)
| ndr1_0
| hskp1 ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f324,plain,
! [X65,X66,X67] :
( c1_1(X65)
| ~ c2_1(X65)
| c3_1(X65)
| ndr1_0
| ~ c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66)
| ndr1_0
| c3_1(X67)
| ~ c1_1(X67)
| c2_1(X67)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f325,plain,
! [X68,X69] :
( c1_1(X68)
| ~ c2_1(X68)
| c3_1(X68)
| ndr1_0
| c3_1(X69)
| ~ c0_1(X69)
| c2_1(X69)
| ndr1_0
| ~ hskp15 ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f326,plain,
! [X70] :
( c1_1(X70)
| ~ c2_1(X70)
| c3_1(X70)
| ndr1_0
| ~ hskp18
| ~ hskp19 ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f328,plain,
! [X73,X74,X75] :
( c1_1(X73)
| ~ c2_1(X73)
| ~ c0_1(X73)
| ndr1_0
| c1_1(X74)
| ~ c0_1(X74)
| c2_1(X74)
| ndr1_0
| c3_1(X75)
| ~ c0_1(X75)
| c2_1(X75)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f329,plain,
! [X76,X77] :
( c1_1(X76)
| ~ c2_1(X76)
| ~ c0_1(X76)
| ndr1_0
| c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| ndr1_0
| hskp20 ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f332,plain,
! [X80,X81] :
( c1_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80)
| ndr1_0
| ~ c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81)
| ndr1_0
| hskp28 ),
inference(consistent_polarity_flipping,[],[f45]) ).
fof(f334,plain,
! [X83,X84,X85] :
( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83)
| ndr1_0
| ~ c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ndr1_0
| ~ c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f335,plain,
! [X86,X87] :
( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86)
| ndr1_0
| ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87)
| ndr1_0
| ~ hskp18 ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f336,plain,
! [X90,X88,X89] :
( c1_1(X88)
| c3_1(X88)
| c2_1(X88)
| ndr1_0
| c1_1(X89)
| ~ c0_1(X89)
| c2_1(X89)
| ndr1_0
| ~ c1_1(X90)
| c2_1(X90)
| ~ c3_1(X90)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f338,plain,
! [X92] :
( c1_1(X92)
| c3_1(X92)
| c2_1(X92)
| ndr1_0
| hskp1
| ~ hskp19 ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f340,plain,
! [X96,X94,X95] :
( c1_1(X94)
| ~ c0_1(X94)
| c2_1(X94)
| ndr1_0
| c1_1(X95)
| c2_1(X95)
| ~ c3_1(X95)
| ndr1_0
| ~ c0_1(X96)
| c2_1(X96)
| ~ c3_1(X96)
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f342,plain,
! [X99,X100] :
( c1_1(X99)
| ~ c0_1(X99)
| c2_1(X99)
| ndr1_0
| c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100)
| ndr1_0
| hskp1 ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f348,plain,
! [X107] :
( ~ c2_1(X107)
| ~ c0_1(X107)
| ~ c1_1(X107)
| ndr1_0
| hskp7
| hskp20 ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f349,plain,
! [X108] :
( ~ c2_1(X108)
| ~ c0_1(X108)
| ~ c3_1(X108)
| ndr1_0
| ~ hskp4
| hskp7 ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f350,plain,
! [X109,X110] :
( ~ c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109)
| ndr1_0
| c3_1(X110)
| ~ c0_1(X110)
| c2_1(X110)
| ndr1_0
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f352,plain,
! [X113] :
( c3_1(X113)
| ~ c0_1(X113)
| ~ c1_1(X113)
| ndr1_0
| hskp27
| ~ hskp19 ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f354,plain,
! [X115] :
( c3_1(X115)
| ~ c0_1(X115)
| ~ c1_1(X115)
| ndr1_0
| ~ hskp18
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f355,plain,
! [X116] :
( c3_1(X116)
| ~ c0_1(X116)
| ~ c1_1(X116)
| ndr1_0
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f22]) ).
fof(f356,plain,
! [X117] :
( c3_1(X117)
| ~ c0_1(X117)
| ~ c1_1(X117)
| ndr1_0
| hskp6 ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f357,plain,
! [X118] :
( c3_1(X118)
| ~ c0_1(X118)
| c2_1(X118)
| ndr1_0
| ~ hskp16
| hskp25 ),
inference(consistent_polarity_flipping,[],[f20]) ).
fof(f358,plain,
! [X119] :
( ~ c0_1(X119)
| ~ c1_1(X119)
| c2_1(X119)
| ndr1_0
| hskp27
| ~ hskp29 ),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f359,plain,
! [X120] :
( ~ c0_1(X120)
| c2_1(X120)
| ~ c3_1(X120)
| ndr1_0
| hskp1
| ~ hskp9 ),
inference(consistent_polarity_flipping,[],[f18]) ).
fof(f361,plain,
( hskp27
| ~ hskp9
| hskp2 ),
inference(consistent_polarity_flipping,[],[f16]) ).
fof(f362,plain,
( ~ hskp12
| ~ hskp13 ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f363,plain,
( ~ hskp13
| ~ hskp18
| ~ hskp8 ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f364,plain,
( ~ hskp18
| ~ hskp4
| hskp20 ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f365,plain,
( ~ hskp18
| ~ hskp19
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f369,plain,
( ~ hskp16
| hskp6
| ~ hskp15 ),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f373,plain,
! [X109,X110] :
( ~ c2_1(X109)
| ~ c1_1(X109)
| ~ c3_1(X109)
| ndr1_0
| c3_1(X110)
| ~ c0_1(X110)
| c2_1(X110)
| ~ hskp11 ),
inference(duplicate_literal_removal,[],[f350]) ).
fof(f375,plain,
! [X99,X100] :
( c1_1(X99)
| ~ c0_1(X99)
| c2_1(X99)
| ndr1_0
| c3_1(X100)
| ~ c0_1(X100)
| ~ c1_1(X100)
| hskp1 ),
inference(duplicate_literal_removal,[],[f342]) ).
fof(f377,plain,
! [X96,X94,X95] :
( c1_1(X94)
| ~ c0_1(X94)
| c2_1(X94)
| ndr1_0
| c1_1(X95)
| c2_1(X95)
| ~ c3_1(X95)
| ~ c0_1(X96)
| c2_1(X96)
| ~ c3_1(X96) ),
inference(duplicate_literal_removal,[],[f340]) ).
fof(f378,plain,
! [X90,X88,X89] :
( c1_1(X88)
| c3_1(X88)
| c2_1(X88)
| ndr1_0
| c1_1(X89)
| ~ c0_1(X89)
| c2_1(X89)
| ~ c1_1(X90)
| c2_1(X90)
| ~ c3_1(X90) ),
inference(duplicate_literal_removal,[],[f336]) ).
fof(f379,plain,
! [X86,X87] :
( c1_1(X86)
| c3_1(X86)
| ~ c0_1(X86)
| ndr1_0
| ~ c0_1(X87)
| ~ c1_1(X87)
| ~ c3_1(X87)
| ~ hskp18 ),
inference(duplicate_literal_removal,[],[f335]) ).
fof(f380,plain,
! [X83,X84,X85] :
( c1_1(X83)
| c3_1(X83)
| ~ c0_1(X83)
| ndr1_0
| ~ c2_1(X84)
| c3_1(X84)
| ~ c0_1(X84)
| ~ c2_1(X85)
| ~ c1_1(X85)
| ~ c3_1(X85) ),
inference(duplicate_literal_removal,[],[f334]) ).
fof(f381,plain,
! [X80,X81] :
( c1_1(X80)
| ~ c2_1(X80)
| ~ c3_1(X80)
| ndr1_0
| ~ c2_1(X81)
| ~ c0_1(X81)
| ~ c1_1(X81)
| hskp28 ),
inference(duplicate_literal_removal,[],[f332]) ).
fof(f382,plain,
! [X76,X77] :
( c1_1(X76)
| ~ c2_1(X76)
| ~ c0_1(X76)
| ndr1_0
| c1_1(X77)
| ~ c0_1(X77)
| ~ c3_1(X77)
| hskp20 ),
inference(duplicate_literal_removal,[],[f329]) ).
fof(f383,plain,
! [X73,X74,X75] :
( c1_1(X73)
| ~ c2_1(X73)
| ~ c0_1(X73)
| ndr1_0
| c1_1(X74)
| ~ c0_1(X74)
| c2_1(X74)
| c3_1(X75)
| ~ c0_1(X75)
| c2_1(X75) ),
inference(duplicate_literal_removal,[],[f328]) ).
fof(f385,plain,
! [X68,X69] :
( c1_1(X68)
| ~ c2_1(X68)
| c3_1(X68)
| ndr1_0
| c3_1(X69)
| ~ c0_1(X69)
| c2_1(X69)
| ~ hskp15 ),
inference(duplicate_literal_removal,[],[f325]) ).
fof(f386,plain,
! [X65,X66,X67] :
( c1_1(X65)
| ~ c2_1(X65)
| c3_1(X65)
| ndr1_0
| ~ c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66)
| c3_1(X67)
| ~ c1_1(X67)
| c2_1(X67) ),
inference(duplicate_literal_removal,[],[f324]) ).
fof(f387,plain,
! [X62,X63] :
( c0_1(X62)
| c2_1(X62)
| ~ c3_1(X62)
| ndr1_0
| ~ c0_1(X63)
| c2_1(X63)
| ~ c3_1(X63)
| hskp1 ),
inference(duplicate_literal_removal,[],[f322]) ).
fof(f389,plain,
! [X58,X59] :
( c0_1(X58)
| ~ c1_1(X58)
| ~ c3_1(X58)
| ndr1_0
| c1_1(X59)
| c3_1(X59)
| ~ c0_1(X59)
| ~ hskp0 ),
inference(duplicate_literal_removal,[],[f320]) ).
fof(f390,plain,
! [X56,X57] :
( c0_1(X56)
| ~ c1_1(X56)
| c2_1(X56)
| ndr1_0
| c3_1(X57)
| ~ c0_1(X57)
| c2_1(X57)
| ~ hskp16 ),
inference(duplicate_literal_removal,[],[f319]) ).
fof(f392,plain,
! [X51,X52] :
( c0_1(X51)
| ~ c1_1(X51)
| c2_1(X51)
| ndr1_0
| c0_1(X52)
| c2_1(X52)
| ~ c3_1(X52)
| ~ hskp15 ),
inference(duplicate_literal_removal,[],[f317]) ).
fof(f396,plain,
! [X40,X41,X39] :
( c0_1(X39)
| ~ c2_1(X39)
| ~ c1_1(X39)
| ndr1_0
| c1_1(X40)
| ~ c2_1(X40)
| ~ c3_1(X40)
| ~ c1_1(X41)
| c2_1(X41)
| ~ c3_1(X41) ),
inference(duplicate_literal_removal,[],[f311]) ).
fof(f399,plain,
! [X32,X33] :
( c0_1(X32)
| ~ c2_1(X32)
| c3_1(X32)
| ndr1_0
| ~ c2_1(X33)
| ~ c1_1(X33)
| ~ c3_1(X33)
| ~ hskp10 ),
inference(duplicate_literal_removal,[],[f307]) ).
fof(f400,plain,
! [X31,X29,X30] :
( c0_1(X29)
| ~ c2_1(X29)
| c3_1(X29)
| ndr1_0
| c0_1(X30)
| c2_1(X30)
| ~ c3_1(X30)
| ~ c2_1(X31)
| ~ c0_1(X31)
| ~ c1_1(X31) ),
inference(duplicate_literal_removal,[],[f306]) ).
fof(f401,plain,
! [X28,X26,X27] :
( c0_1(X26)
| ~ c2_1(X26)
| c3_1(X26)
| ndr1_0
| c0_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27)
| c1_1(X28)
| ~ c0_1(X28)
| ~ c3_1(X28) ),
inference(duplicate_literal_removal,[],[f305]) ).
fof(f412,definition,
( spl0_1
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f416,definition,
( spl0_2
<=> hskp8 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f420,definition,
( spl0_3
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f425,definition,
( spl0_4
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f429,definition,
( spl0_5
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f434,definition,
( spl0_6
<=> hskp6 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f437,plain,
( ~ spl0_1
| spl0_6
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f369,f429,f434,f412]) ).
fof(f444,definition,
( spl0_8
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f448,definition,
( spl0_9
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f457,definition,
( spl0_11
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f466,definition,
( spl0_13
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f470,definition,
( spl0_14
<=> hskp18 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f473,plain,
( ~ spl0_13
| ~ spl0_3
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f365,f470,f420,f466]) ).
fof(f475,definition,
( spl0_15
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f479,definition,
( spl0_16
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f482,plain,
( spl0_15
| ~ spl0_16
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f364,f470,f479,f475]) ).
fof(f484,definition,
( spl0_17
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f487,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f363,f484,f470,f416]) ).
fof(f489,definition,
( spl0_18
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f492,plain,
( ~ spl0_17
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f362,f489,f484]) ).
fof(f494,definition,
( spl0_19
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f498,definition,
( spl0_20
<=> hskp9 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f502,definition,
( spl0_21
<=> hskp27 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f505,plain,
( spl0_19
| ~ spl0_20
| spl0_21 ),
inference(avatar_split_clause,[],[f361,f502,f498,f494]) ).
fof(f507,definition,
( spl0_22
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f512,definition,
( spl0_23
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f516,definition,
( spl0_24
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f520,definition,
( spl0_25
<=> ! [X120] :
( ~ c0_1(X120)
| ~ c3_1(X120)
| c2_1(X120) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f521,plain,
( ! [X120] :
( ~ c3_1(X120)
| ~ c0_1(X120)
| c2_1(X120) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f520]) ).
fof(f522,plain,
( ~ spl0_20
| spl0_23
| spl0_24
| spl0_25 ),
inference(avatar_split_clause,[],[f359,f520,f516,f512,f498]) ).
fof(f524,definition,
( spl0_26
<=> hskp29 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f528,definition,
( spl0_27
<=> ! [X119] :
( ~ c0_1(X119)
| c2_1(X119)
| ~ c1_1(X119) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f529,plain,
( ! [X119] :
( ~ c1_1(X119)
| c2_1(X119)
| ~ c0_1(X119) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f528]) ).
fof(f530,plain,
( ~ spl0_26
| spl0_21
| spl0_24
| spl0_27 ),
inference(avatar_split_clause,[],[f358,f528,f516,f502,f524]) ).
fof(f532,definition,
( spl0_28
<=> ! [X118] :
( c3_1(X118)
| c2_1(X118)
| ~ c0_1(X118) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f533,plain,
( ! [X118] :
( c3_1(X118)
| c2_1(X118)
| ~ c0_1(X118) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f532]) ).
fof(f534,plain,
( spl0_11
| ~ spl0_5
| spl0_24
| spl0_28 ),
inference(avatar_split_clause,[],[f357,f532,f516,f429,f457]) ).
fof(f536,definition,
( spl0_29
<=> ! [X117] :
( c3_1(X117)
| ~ c1_1(X117)
| ~ c0_1(X117) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f537,plain,
( ! [X117] :
( ~ c1_1(X117)
| c3_1(X117)
| ~ c0_1(X117) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f536]) ).
fof(f538,plain,
( spl0_6
| spl0_24
| spl0_29 ),
inference(avatar_split_clause,[],[f356,f536,f516,f434]) ).
fof(f539,plain,
( ~ spl0_9
| spl0_24
| spl0_29 ),
inference(avatar_split_clause,[],[f355,f536,f516,f448]) ).
fof(f540,plain,
( ~ spl0_2
| ~ spl0_14
| spl0_24
| spl0_29 ),
inference(avatar_split_clause,[],[f354,f536,f516,f470,f416]) ).
fof(f542,plain,
( ~ spl0_3
| spl0_21
| spl0_24
| spl0_29 ),
inference(avatar_split_clause,[],[f352,f536,f516,f502,f420]) ).
fof(f544,definition,
( spl0_30
<=> ! [X111] :
( ~ c2_1(X111)
| ~ c3_1(X111)
| ~ c1_1(X111) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f545,plain,
( ! [X111] :
( ~ c1_1(X111)
| ~ c3_1(X111)
| ~ c2_1(X111) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f544]) ).
fof(f547,plain,
( ~ spl0_8
| spl0_28
| spl0_24
| spl0_30 ),
inference(avatar_split_clause,[],[f373,f544,f516,f532,f444]) ).
fof(f549,definition,
( spl0_31
<=> hskp7 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f553,definition,
( spl0_32
<=> ! [X108] :
( ~ c2_1(X108)
| ~ c3_1(X108)
| ~ c0_1(X108) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f554,plain,
( ! [X108] :
( ~ c3_1(X108)
| ~ c2_1(X108)
| ~ c0_1(X108) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f555,plain,
( spl0_31
| ~ spl0_16
| spl0_24
| spl0_32 ),
inference(avatar_split_clause,[],[f349,f553,f516,f479,f549]) ).
fof(f557,definition,
( spl0_33
<=> ! [X107] :
( ~ c2_1(X107)
| ~ c1_1(X107)
| ~ c0_1(X107) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f558,plain,
( ! [X107] :
( ~ c1_1(X107)
| ~ c2_1(X107)
| ~ c0_1(X107) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f559,plain,
( spl0_15
| spl0_31
| spl0_24
| spl0_33 ),
inference(avatar_split_clause,[],[f348,f557,f516,f549,f475]) ).
fof(f561,definition,
( spl0_34
<=> ! [X106] :
( ~ c2_1(X106)
| ~ c0_1(X106)
| c3_1(X106) ) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f562,plain,
( ! [X106] :
( c3_1(X106)
| ~ c0_1(X106)
| ~ c2_1(X106) )
| ~ spl0_34 ),
inference(avatar_component_clause,[],[f561]) ).
fof(f570,definition,
( spl0_36
<=> ! [X104] :
( c1_1(X104)
| ~ c3_1(X104)
| c2_1(X104) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f571,plain,
( ! [X104] :
( c1_1(X104)
| ~ c3_1(X104)
| c2_1(X104) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f574,definition,
( spl0_37
<=> ! [X102] :
( c1_1(X102)
| ~ c3_1(X102)
| ~ c0_1(X102) ) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f575,plain,
( ! [X102] :
( c1_1(X102)
| ~ c3_1(X102)
| ~ c0_1(X102) )
| ~ spl0_37 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f578,definition,
( spl0_38
<=> ! [X101] :
( c1_1(X101)
| c2_1(X101)
| ~ c0_1(X101) ) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f579,plain,
( ! [X101] :
( c1_1(X101)
| c2_1(X101)
| ~ c0_1(X101) )
| ~ spl0_38 ),
inference(avatar_component_clause,[],[f578]) ).
fof(f581,plain,
( spl0_23
| spl0_29
| spl0_24
| spl0_38 ),
inference(avatar_split_clause,[],[f375,f578,f516,f536,f512]) ).
fof(f587,plain,
( spl0_25
| spl0_36
| spl0_24
| spl0_38 ),
inference(avatar_split_clause,[],[f377,f578,f516,f570,f520]) ).
fof(f593,definition,
( spl0_41
<=> ! [X93] :
( c1_1(X93)
| c2_1(X93)
| c3_1(X93) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f594,plain,
( ! [X93] :
( c1_1(X93)
| c2_1(X93)
| c3_1(X93) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f596,plain,
( ~ spl0_3
| spl0_23
| spl0_24
| spl0_41 ),
inference(avatar_split_clause,[],[f338,f593,f516,f512,f420]) ).
fof(f603,definition,
( spl0_43
<=> ! [X90] :
( ~ c1_1(X90)
| ~ c3_1(X90)
| c2_1(X90) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f604,plain,
( ! [X90] :
( ~ c1_1(X90)
| ~ c3_1(X90)
| c2_1(X90) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f603]) ).
fof(f605,plain,
( spl0_43
| spl0_38
| spl0_24
| spl0_41 ),
inference(avatar_split_clause,[],[f378,f593,f516,f578,f603]) ).
fof(f607,definition,
( spl0_44
<=> ! [X87] :
( ~ c0_1(X87)
| ~ c3_1(X87)
| ~ c1_1(X87) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f608,plain,
( ! [X87] :
( ~ c1_1(X87)
| ~ c3_1(X87)
| ~ c0_1(X87) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,definition,
( spl0_45
<=> ! [X86] :
( c1_1(X86)
| ~ c0_1(X86)
| c3_1(X86) ) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f611,plain,
( ! [X86] :
( c1_1(X86)
| ~ c0_1(X86)
| c3_1(X86) )
| ~ spl0_45 ),
inference(avatar_component_clause,[],[f610]) ).
fof(f612,plain,
( ~ spl0_14
| spl0_44
| spl0_24
| spl0_45 ),
inference(avatar_split_clause,[],[f379,f610,f516,f607,f470]) ).
fof(f613,plain,
( spl0_30
| spl0_34
| spl0_24
| spl0_45 ),
inference(avatar_split_clause,[],[f380,f610,f516,f561,f544]) ).
fof(f615,definition,
( spl0_46
<=> ! [X82] :
( c1_1(X82)
| ~ c3_1(X82)
| ~ c2_1(X82) ) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f616,plain,
( ! [X82] :
( c1_1(X82)
| ~ c3_1(X82)
| ~ c2_1(X82) )
| ~ spl0_46 ),
inference(avatar_component_clause,[],[f615]) ).
fof(f618,plain,
( spl0_22
| spl0_33
| spl0_24
| spl0_46 ),
inference(avatar_split_clause,[],[f381,f615,f516,f557,f507]) ).
fof(f620,definition,
( spl0_47
<=> ! [X79] :
( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79) ) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f621,plain,
( ! [X79] :
( c1_1(X79)
| ~ c0_1(X79)
| ~ c2_1(X79) )
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f620]) ).
fof(f624,plain,
( spl0_15
| spl0_37
| spl0_24
| spl0_47 ),
inference(avatar_split_clause,[],[f382,f620,f516,f574,f475]) ).
fof(f625,plain,
( spl0_28
| spl0_38
| spl0_24
| spl0_47 ),
inference(avatar_split_clause,[],[f383,f620,f516,f578,f532]) ).
fof(f628,definition,
( spl0_48
<=> ! [X70] :
( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f629,plain,
( ! [X70] :
( c1_1(X70)
| c3_1(X70)
| ~ c2_1(X70) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f630,plain,
( ~ spl0_3
| ~ spl0_14
| spl0_24
| spl0_48 ),
inference(avatar_split_clause,[],[f326,f628,f516,f470,f420]) ).
fof(f631,plain,
( ~ spl0_1
| spl0_28
| spl0_24
| spl0_48 ),
inference(avatar_split_clause,[],[f385,f628,f516,f532,f412]) ).
fof(f633,definition,
( spl0_49
<=> ! [X67] :
( c3_1(X67)
| c2_1(X67)
| ~ c1_1(X67) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f634,plain,
( ! [X67] :
( ~ c1_1(X67)
| c2_1(X67)
| c3_1(X67) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f636,definition,
( spl0_50
<=> ! [X66] :
( ~ c2_1(X66)
| ~ c1_1(X66)
| c3_1(X66) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f637,plain,
( ! [X66] :
( ~ c1_1(X66)
| ~ c2_1(X66)
| c3_1(X66) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f636]) ).
fof(f638,plain,
( spl0_49
| spl0_50
| spl0_24
| spl0_48 ),
inference(avatar_split_clause,[],[f386,f628,f516,f636,f633]) ).
fof(f640,definition,
( spl0_51
<=> ! [X64] :
( c0_1(X64)
| ~ c3_1(X64)
| c2_1(X64) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f641,plain,
( ! [X64] :
( ~ c3_1(X64)
| c0_1(X64)
| c2_1(X64) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f640]) ).
fof(f643,plain,
( spl0_23
| spl0_25
| spl0_24
| spl0_51 ),
inference(avatar_split_clause,[],[f387,f640,f516,f520,f512]) ).
fof(f646,definition,
( spl0_52
<=> ! [X58] :
( c0_1(X58)
| ~ c3_1(X58)
| ~ c1_1(X58) ) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f647,plain,
( ! [X58] :
( ~ c1_1(X58)
| ~ c3_1(X58)
| c0_1(X58) )
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f648,plain,
( ~ spl0_9
| spl0_45
| spl0_24
| spl0_52 ),
inference(avatar_split_clause,[],[f389,f646,f516,f610,f448]) ).
fof(f650,definition,
( spl0_53
<=> ! [X56] :
( c0_1(X56)
| c2_1(X56)
| ~ c1_1(X56) ) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f651,plain,
( ! [X56] :
( ~ c1_1(X56)
| c2_1(X56)
| c0_1(X56) )
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f650]) ).
fof(f652,plain,
( ~ spl0_5
| spl0_28
| spl0_24
| spl0_53 ),
inference(avatar_split_clause,[],[f390,f650,f516,f532,f429]) ).
fof(f654,plain,
( ~ spl0_1
| spl0_51
| spl0_24
| spl0_53 ),
inference(avatar_split_clause,[],[f392,f650,f516,f640,f412]) ).
fof(f668,definition,
( spl0_57
<=> ! [X47] :
( c0_1(X47)
| ~ c3_1(X47)
| ~ c2_1(X47) ) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f669,plain,
( ! [X47] :
( ~ c3_1(X47)
| c0_1(X47)
| ~ c2_1(X47) )
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f668]) ).
fof(f673,definition,
( spl0_58
<=> ! [X42] :
( c0_1(X42)
| ~ c1_1(X42)
| ~ c2_1(X42) ) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f674,plain,
( ! [X42] :
( ~ c1_1(X42)
| c0_1(X42)
| ~ c2_1(X42) )
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f673]) ).
fof(f676,plain,
( spl0_43
| spl0_46
| spl0_24
| spl0_58 ),
inference(avatar_split_clause,[],[f396,f673,f516,f615,f603]) ).
fof(f680,definition,
( spl0_59
<=> ! [X34] :
( c0_1(X34)
| c3_1(X34)
| ~ c2_1(X34) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f681,plain,
( ! [X34] :
( c3_1(X34)
| c0_1(X34)
| ~ c2_1(X34) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f680]) ).
fof(f683,plain,
( ~ spl0_4
| spl0_30
| spl0_24
| spl0_59 ),
inference(avatar_split_clause,[],[f399,f680,f516,f544,f425]) ).
fof(f684,plain,
( spl0_33
| spl0_51
| spl0_24
| spl0_59 ),
inference(avatar_split_clause,[],[f400,f680,f516,f640,f557]) ).
fof(f685,plain,
( spl0_37
| spl0_57
| spl0_24
| spl0_59 ),
inference(avatar_split_clause,[],[f401,f680,f516,f668,f574]) ).
fof(f712,definition,
( spl0_64
<=> c3_1(a166) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f714,plain,
( c3_1(a166)
| ~ spl0_64 ),
inference(avatar_component_clause,[],[f712]) ).
fof(f715,plain,
( spl0_64
| spl0_26 ),
inference(avatar_split_clause,[],[f291,f524,f712]) ).
fof(f717,definition,
( spl0_65
<=> c2_1(a166) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f720,plain,
( ~ spl0_65
| spl0_26 ),
inference(avatar_split_clause,[],[f290,f524,f717]) ).
fof(f722,definition,
( spl0_66
<=> c0_1(a166) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f725,plain,
( spl0_66
| spl0_26 ),
inference(avatar_split_clause,[],[f289,f524,f722]) ).
fof(f728,definition,
( spl0_67
<=> c2_1(a137) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f731,plain,
( ~ spl0_67
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f287,f507,f728]) ).
fof(f733,definition,
( spl0_68
<=> c1_1(a137) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f735,plain,
( c1_1(a137)
| ~ spl0_68 ),
inference(avatar_component_clause,[],[f733]) ).
fof(f736,plain,
( spl0_68
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f91,f507,f733]) ).
fof(f738,definition,
( spl0_69
<=> c0_1(a137) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f741,plain,
( spl0_69
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f92,f507,f738]) ).
fof(f744,definition,
( spl0_70
<=> c3_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f746,plain,
( c3_1(a101)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f744]) ).
fof(f747,plain,
( spl0_70
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f94,f502,f744]) ).
fof(f749,definition,
( spl0_71
<=> c1_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f751,plain,
( c1_1(a101)
| ~ spl0_71 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f752,plain,
( spl0_71
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f95,f502,f749]) ).
fof(f754,definition,
( spl0_72
<=> c0_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f757,plain,
( spl0_72
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f96,f502,f754]) ).
fof(f758,plain,
( ~ spl0_24
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f285,f502,f516]) ).
fof(f776,definition,
( spl0_76
<=> c3_1(a173) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f778,plain,
( ~ c3_1(a173)
| spl0_76 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f779,plain,
( ~ spl0_76
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f102,f457,f776]) ).
fof(f781,definition,
( spl0_77
<=> c0_1(a173) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f784,plain,
( ~ spl0_77
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f103,f457,f781]) ).
fof(f786,definition,
( spl0_78
<=> c1_1(a173) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f788,plain,
( c1_1(a173)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f789,plain,
( spl0_78
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f104,f457,f786]) ).
fof(f856,definition,
( spl0_91
<=> c3_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f858,plain,
( ~ c3_1(a132)
| spl0_91 ),
inference(avatar_component_clause,[],[f856]) ).
fof(f859,plain,
( ~ spl0_91
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f122,f475,f856]) ).
fof(f861,definition,
( spl0_92
<=> c2_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f864,plain,
( spl0_92
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f274,f475,f861]) ).
fof(f866,definition,
( spl0_93
<=> c1_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f868,plain,
( ~ c1_1(a132)
| spl0_93 ),
inference(avatar_component_clause,[],[f866]) ).
fof(f869,plain,
( ~ spl0_93
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f124,f475,f866]) ).
fof(f872,definition,
( spl0_94
<=> c2_1(a130) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f875,plain,
( spl0_94
| spl0_3 ),
inference(avatar_split_clause,[],[f272,f420,f872]) ).
fof(f877,definition,
( spl0_95
<=> c3_1(a130) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f880,plain,
( spl0_95
| spl0_3 ),
inference(avatar_split_clause,[],[f271,f420,f877]) ).
fof(f882,definition,
( spl0_96
<=> c1_1(a130) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f884,plain,
( c1_1(a130)
| ~ spl0_96 ),
inference(avatar_component_clause,[],[f882]) ).
fof(f885,plain,
( spl0_96
| spl0_3 ),
inference(avatar_split_clause,[],[f270,f420,f882]) ).
fof(f888,definition,
( spl0_97
<=> c1_1(a129) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f890,plain,
( ~ c1_1(a129)
| spl0_97 ),
inference(avatar_component_clause,[],[f888]) ).
fof(f891,plain,
( ~ spl0_97
| spl0_14 ),
inference(avatar_split_clause,[],[f268,f470,f888]) ).
fof(f893,definition,
( spl0_98
<=> c2_1(a129) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f896,plain,
( ~ spl0_98
| spl0_14 ),
inference(avatar_split_clause,[],[f267,f470,f893]) ).
fof(f898,definition,
( spl0_99
<=> c0_1(a129) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f901,plain,
( spl0_99
| spl0_14 ),
inference(avatar_split_clause,[],[f266,f470,f898]) ).
fof(f904,definition,
( spl0_100
<=> c3_1(a124) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f907,plain,
( ~ spl0_100
| spl0_13 ),
inference(avatar_split_clause,[],[f264,f466,f904]) ).
fof(f909,definition,
( spl0_101
<=> c1_1(a124) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f911,plain,
( ~ c1_1(a124)
| spl0_101 ),
inference(avatar_component_clause,[],[f909]) ).
fof(f912,plain,
( ~ spl0_101
| spl0_13 ),
inference(avatar_split_clause,[],[f263,f466,f909]) ).
fof(f914,definition,
( spl0_102
<=> c2_1(a124) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f917,plain,
( ~ spl0_102
| spl0_13 ),
inference(avatar_split_clause,[],[f262,f466,f914]) ).
fof(f920,definition,
( spl0_103
<=> c2_1(a122) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f923,plain,
( spl0_103
| spl0_5 ),
inference(avatar_split_clause,[],[f260,f429,f920]) ).
fof(f925,definition,
( spl0_104
<=> c1_1(a122) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f927,plain,
( ~ c1_1(a122)
| spl0_104 ),
inference(avatar_component_clause,[],[f925]) ).
fof(f928,plain,
( ~ spl0_104
| spl0_5 ),
inference(avatar_split_clause,[],[f259,f429,f925]) ).
fof(f930,definition,
( spl0_105
<=> c0_1(a122) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f933,plain,
( spl0_105
| spl0_5 ),
inference(avatar_split_clause,[],[f258,f429,f930]) ).
fof(f936,definition,
( spl0_106
<=> c3_1(a121) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f938,plain,
( ~ c3_1(a121)
| spl0_106 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f939,plain,
( ~ spl0_106
| spl0_1 ),
inference(avatar_split_clause,[],[f256,f412,f936]) ).
fof(f941,definition,
( spl0_107
<=> c2_1(a121) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f944,plain,
( spl0_107
| spl0_1 ),
inference(avatar_split_clause,[],[f255,f412,f941]) ).
fof(f946,definition,
( spl0_108
<=> c0_1(a121) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f949,plain,
( ~ spl0_108
| spl0_1 ),
inference(avatar_split_clause,[],[f254,f412,f946]) ).
fof(f950,plain,
( ~ spl0_24
| spl0_1 ),
inference(avatar_split_clause,[],[f253,f412,f516]) ).
fof(f968,definition,
( spl0_112
<=> c3_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f971,plain,
( ~ spl0_112
| spl0_17 ),
inference(avatar_split_clause,[],[f250,f484,f968]) ).
fof(f973,definition,
( spl0_113
<=> c1_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f975,plain,
( c1_1(a116)
| ~ spl0_113 ),
inference(avatar_component_clause,[],[f973]) ).
fof(f976,plain,
( spl0_113
| spl0_17 ),
inference(avatar_split_clause,[],[f249,f484,f973]) ).
fof(f978,definition,
( spl0_114
<=> c0_1(a116) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f981,plain,
( spl0_114
| spl0_17 ),
inference(avatar_split_clause,[],[f248,f484,f978]) ).
fof(f984,definition,
( spl0_115
<=> c2_1(a113) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f987,plain,
( spl0_115
| spl0_18 ),
inference(avatar_split_clause,[],[f246,f489,f984]) ).
fof(f989,definition,
( spl0_116
<=> c1_1(a113) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f991,plain,
( c1_1(a113)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f989]) ).
fof(f992,plain,
( spl0_116
| spl0_18 ),
inference(avatar_split_clause,[],[f245,f489,f989]) ).
fof(f994,definition,
( spl0_117
<=> c0_1(a113) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f997,plain,
( spl0_117
| spl0_18 ),
inference(avatar_split_clause,[],[f244,f489,f994]) ).
fof(f1000,definition,
( spl0_118
<=> c1_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f1002,plain,
( ~ c1_1(a112)
| spl0_118 ),
inference(avatar_component_clause,[],[f1000]) ).
fof(f1003,plain,
( ~ spl0_118
| spl0_8 ),
inference(avatar_split_clause,[],[f242,f444,f1000]) ).
fof(f1005,definition,
( spl0_119
<=> c0_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f1008,plain,
( ~ spl0_119
| spl0_8 ),
inference(avatar_split_clause,[],[f241,f444,f1005]) ).
fof(f1010,definition,
( spl0_120
<=> c3_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f1012,plain,
( c3_1(a112)
| ~ spl0_120 ),
inference(avatar_component_clause,[],[f1010]) ).
fof(f1013,plain,
( spl0_120
| spl0_8 ),
inference(avatar_split_clause,[],[f240,f444,f1010]) ).
fof(f1016,definition,
( spl0_121
<=> c3_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1018,plain,
( ~ c3_1(a110)
| spl0_121 ),
inference(avatar_component_clause,[],[f1016]) ).
fof(f1019,plain,
( ~ spl0_121
| spl0_4 ),
inference(avatar_split_clause,[],[f238,f425,f1016]) ).
fof(f1021,definition,
( spl0_122
<=> c2_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f1024,plain,
( spl0_122
| spl0_4 ),
inference(avatar_split_clause,[],[f237,f425,f1021]) ).
fof(f1026,definition,
( spl0_123
<=> c1_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f1028,plain,
( c1_1(a110)
| ~ spl0_123 ),
inference(avatar_component_clause,[],[f1026]) ).
fof(f1029,plain,
( spl0_123
| spl0_4 ),
inference(avatar_split_clause,[],[f236,f425,f1026]) ).
fof(f1032,definition,
( spl0_124
<=> c0_1(a108) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f1035,plain,
( ~ spl0_124
| spl0_20 ),
inference(avatar_split_clause,[],[f234,f498,f1032]) ).
fof(f1037,definition,
( spl0_125
<=> c2_1(a108) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f1040,plain,
( ~ spl0_125
| spl0_20 ),
inference(avatar_split_clause,[],[f233,f498,f1037]) ).
fof(f1042,definition,
( spl0_126
<=> c1_1(a108) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f1044,plain,
( c1_1(a108)
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f1042]) ).
fof(f1045,plain,
( spl0_126
| spl0_20 ),
inference(avatar_split_clause,[],[f232,f498,f1042]) ).
fof(f1046,plain,
( ~ spl0_24
| spl0_20 ),
inference(avatar_split_clause,[],[f231,f498,f516]) ).
fof(f1048,definition,
( spl0_127
<=> c2_1(a107) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f1051,plain,
( spl0_127
| spl0_2 ),
inference(avatar_split_clause,[],[f230,f416,f1048]) ).
fof(f1053,definition,
( spl0_128
<=> c0_1(a107) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f1056,plain,
( ~ spl0_128
| spl0_2 ),
inference(avatar_split_clause,[],[f229,f416,f1053]) ).
fof(f1058,definition,
( spl0_129
<=> c3_1(a107) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f1060,plain,
( c3_1(a107)
| ~ spl0_129 ),
inference(avatar_component_clause,[],[f1058]) ).
fof(f1061,plain,
( spl0_129
| spl0_2 ),
inference(avatar_split_clause,[],[f228,f416,f1058]) ).
fof(f1064,definition,
( spl0_130
<=> c0_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_130])],[avatar_definition]) ).
fof(f1067,plain,
( ~ spl0_130
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f174,f549,f1064]) ).
fof(f1069,definition,
( spl0_131
<=> c3_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1071,plain,
( c3_1(a106)
| ~ spl0_131 ),
inference(avatar_component_clause,[],[f1069]) ).
fof(f1072,plain,
( spl0_131
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f175,f549,f1069]) ).
fof(f1074,definition,
( spl0_132
<=> c2_1(a106) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1077,plain,
( ~ spl0_132
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f226,f549,f1074]) ).
fof(f1080,definition,
( spl0_133
<=> c3_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1083,plain,
( ~ spl0_133
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f178,f434,f1080]) ).
fof(f1085,definition,
( spl0_134
<=> c2_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f1088,plain,
( ~ spl0_134
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f224,f434,f1085]) ).
fof(f1090,definition,
( spl0_135
<=> c1_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f1092,plain,
( c1_1(a105)
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f1090]) ).
fof(f1093,plain,
( spl0_135
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f180,f434,f1090]) ).
fof(f1112,definition,
( spl0_139
<=> c3_1(a103) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1114,plain,
( ~ c3_1(a103)
| spl0_139 ),
inference(avatar_component_clause,[],[f1112]) ).
fof(f1115,plain,
( ~ spl0_139
| spl0_16 ),
inference(avatar_split_clause,[],[f218,f479,f1112]) ).
fof(f1117,definition,
( spl0_140
<=> c2_1(a103) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1120,plain,
( ~ spl0_140
| spl0_16 ),
inference(avatar_split_clause,[],[f217,f479,f1117]) ).
fof(f1122,definition,
( spl0_141
<=> c0_1(a103) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f1125,plain,
( spl0_141
| spl0_16 ),
inference(avatar_split_clause,[],[f216,f479,f1122]) ).
fof(f1158,plain,
( ~ spl0_24
| ~ spl0_19 ),
inference(avatar_split_clause,[],[f211,f494,f516]) ).
fof(f1160,definition,
( spl0_148
<=> c3_1(a98) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1163,plain,
( ~ spl0_148
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f198,f512,f1160]) ).
fof(f1165,definition,
( spl0_149
<=> c1_1(a98) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1167,plain,
( ~ c1_1(a98)
| spl0_149 ),
inference(avatar_component_clause,[],[f1165]) ).
fof(f1168,plain,
( ~ spl0_149
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f199,f512,f1165]) ).
fof(f1170,definition,
( spl0_150
<=> c0_1(a98) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1173,plain,
( spl0_150
| ~ spl0_23 ),
inference(avatar_split_clause,[],[f200,f512,f1170]) ).
fof(f1176,definition,
( spl0_151
<=> c3_1(a97) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f1178,plain,
( ~ c3_1(a97)
| spl0_151 ),
inference(avatar_component_clause,[],[f1176]) ).
fof(f1179,plain,
( ~ spl0_151
| spl0_9 ),
inference(avatar_split_clause,[],[f209,f448,f1176]) ).
fof(f1181,definition,
( spl0_152
<=> c2_1(a97) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1184,plain,
( spl0_152
| spl0_9 ),
inference(avatar_split_clause,[],[f208,f448,f1181]) ).
fof(f1186,definition,
( spl0_153
<=> c0_1(a97) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f1189,plain,
( spl0_153
| spl0_9 ),
inference(avatar_split_clause,[],[f207,f448,f1186]) ).
fof(f1198,plain,
( ~ c0_1(a166)
| c2_1(a166)
| ~ spl0_25
| ~ spl0_64 ),
inference(resolution,[],[f714,f521]) ).
fof(f1199,plain,
( spl0_65
| ~ spl0_66
| ~ spl0_25
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f1198,f712,f520,f722,f717]) ).
fof(f1200,plain,
( ~ c0_1(a101)
| c2_1(a101)
| ~ spl0_25
| ~ spl0_70 ),
inference(resolution,[],[f746,f521]) ).
fof(f1202,definition,
( spl0_155
<=> c2_1(a101) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1206,plain,
( c3_1(a116)
| ~ c0_1(a116)
| ~ spl0_29
| ~ spl0_113 ),
inference(resolution,[],[f537,f975]) ).
fof(f1208,plain,
( ~ spl0_114
| spl0_112
| ~ spl0_29
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f1206,f973,f536,f968,f978]) ).
fof(f1209,plain,
( c3_1(a113)
| ~ c0_1(a113)
| ~ spl0_29
| ~ spl0_116 ),
inference(resolution,[],[f991,f537]) ).
fof(f1211,definition,
( spl0_156
<=> c3_1(a113) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f1213,plain,
( c3_1(a113)
| ~ spl0_156 ),
inference(avatar_component_clause,[],[f1211]) ).
fof(f1214,plain,
( ~ spl0_117
| spl0_156
| ~ spl0_29
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1209,f989,f536,f1211,f994]) ).
fof(f1216,plain,
( ~ c3_1(a101)
| ~ c2_1(a101)
| ~ spl0_30
| ~ spl0_71 ),
inference(resolution,[],[f545,f751]) ).
fof(f1217,plain,
( ~ c3_1(a113)
| ~ c2_1(a113)
| ~ spl0_30
| ~ spl0_116 ),
inference(resolution,[],[f545,f991]) ).
fof(f1218,plain,
( ~ spl0_115
| ~ spl0_156
| ~ spl0_30
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1217,f989,f544,f1211,f984]) ).
fof(f1219,plain,
( ~ spl0_155
| ~ spl0_70
| ~ spl0_30
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1216,f749,f544,f744,f1202]) ).
fof(f1222,plain,
( ~ c2_1(a113)
| ~ c0_1(a113)
| ~ spl0_32
| ~ spl0_156 ),
inference(resolution,[],[f554,f1213]) ).
fof(f1228,plain,
( ~ spl0_117
| ~ spl0_115
| ~ spl0_32
| ~ spl0_156 ),
inference(avatar_split_clause,[],[f1222,f1211,f553,f984,f994]) ).
fof(f1230,plain,
( ~ c2_1(a101)
| ~ c0_1(a101)
| ~ spl0_33
| ~ spl0_71 ),
inference(resolution,[],[f558,f751]) ).
fof(f1231,plain,
( ~ c2_1(a113)
| ~ c0_1(a113)
| ~ spl0_33
| ~ spl0_116 ),
inference(resolution,[],[f558,f991]) ).
fof(f1232,plain,
( ~ spl0_117
| ~ spl0_115
| ~ spl0_33
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1231,f989,f557,f984,f994]) ).
fof(f1233,plain,
( ~ spl0_72
| ~ spl0_155
| ~ spl0_33
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1230,f749,f557,f1202,f754]) ).
fof(f1255,definition,
( spl0_157
<=> c0_1(a132) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1269,plain,
( ~ c3_1(a122)
| ~ c0_1(a122)
| ~ spl0_37
| spl0_104 ),
inference(resolution,[],[f575,f927]) ).
fof(f1271,plain,
( ~ c3_1(a129)
| ~ c0_1(a129)
| ~ spl0_37
| spl0_97 ),
inference(resolution,[],[f575,f890]) ).
fof(f1282,definition,
( spl0_158
<=> c3_1(a129) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f1283,plain,
( c3_1(a129)
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f1282]) ).
fof(f1284,plain,
( ~ c3_1(a129)
| spl0_158 ),
inference(avatar_component_clause,[],[f1282]) ).
fof(f1287,definition,
( spl0_159
<=> c3_1(a122) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1289,plain,
( ~ c3_1(a122)
| spl0_159 ),
inference(avatar_component_clause,[],[f1287]) ).
fof(f1290,plain,
( ~ spl0_105
| ~ spl0_159
| ~ spl0_37
| spl0_104 ),
inference(avatar_split_clause,[],[f1269,f925,f574,f1287,f930]) ).
fof(f1304,plain,
( c2_1(a129)
| ~ c0_1(a129)
| ~ spl0_38
| spl0_97 ),
inference(resolution,[],[f579,f890]) ).
fof(f1332,definition,
( spl0_163
<=> c0_1(a110) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1337,definition,
( spl0_164
<=> c0_1(a105) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1347,plain,
( ~ c0_1(a122)
| ~ c2_1(a122)
| ~ spl0_34
| spl0_159 ),
inference(resolution,[],[f1289,f562]) ).
fof(f1348,plain,
( ~ spl0_103
| ~ spl0_105
| ~ spl0_34
| spl0_159 ),
inference(avatar_split_clause,[],[f1347,f1287,f561,f930,f920]) ).
fof(f1349,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_29
| ~ spl0_41 ),
inference(resolution,[],[f594,f537]) ).
fof(f1360,plain,
( c2_1(a124)
| c3_1(a124)
| ~ spl0_41
| spl0_101 ),
inference(resolution,[],[f594,f911]) ).
fof(f1361,plain,
( c2_1(a129)
| c3_1(a129)
| ~ spl0_41
| spl0_97 ),
inference(resolution,[],[f594,f890]) ).
fof(f1370,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_29
| ~ spl0_41 ),
inference(duplicate_literal_removal,[],[f1349]) ).
fof(f1372,definition,
( spl0_166
<=> c3_1(a137) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1382,definition,
( spl0_168
<=> c2_1(a173) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1398,plain,
( spl0_158
| spl0_98
| ~ spl0_41
| spl0_97 ),
inference(avatar_split_clause,[],[f1361,f888,f593,f893,f1282]) ).
fof(f1424,plain,
( spl0_28
| ~ spl0_29
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f1370,f593,f536,f532]) ).
fof(f1425,plain,
( ~ c3_1(a101)
| c2_1(a101)
| ~ spl0_43
| ~ spl0_71 ),
inference(resolution,[],[f604,f751]) ).
fof(f1430,plain,
( ! [X0] :
( ~ c0_1(X0)
| c3_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_29
| ~ spl0_45 ),
inference(resolution,[],[f611,f537]) ).
fof(f1431,plain,
( ~ c0_1(a98)
| c3_1(a98)
| ~ spl0_45
| spl0_149 ),
inference(resolution,[],[f611,f1167]) ).
fof(f1440,plain,
( ~ c0_1(a122)
| c3_1(a122)
| ~ spl0_45
| spl0_104 ),
inference(resolution,[],[f611,f927]) ).
fof(f1442,plain,
( ~ c0_1(a129)
| c3_1(a129)
| ~ spl0_45
| spl0_97 ),
inference(resolution,[],[f611,f890]) ).
fof(f1444,plain,
( ~ c0_1(a132)
| c3_1(a132)
| ~ spl0_45
| spl0_93 ),
inference(resolution,[],[f611,f868]) ).
fof(f1451,plain,
( ! [X0] :
( c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_29
| ~ spl0_45 ),
inference(duplicate_literal_removal,[],[f1430]) ).
fof(f1452,plain,
( spl0_158
| ~ spl0_99
| ~ spl0_45
| spl0_97 ),
inference(avatar_split_clause,[],[f1442,f888,f610,f898,f1282]) ).
fof(f1453,plain,
( spl0_159
| ~ spl0_105
| ~ spl0_45
| spl0_104 ),
inference(avatar_split_clause,[],[f1440,f925,f610,f930,f1287]) ).
fof(f1461,plain,
( ~ c0_1(a97)
| ~ c2_1(a97)
| ~ spl0_34
| spl0_151 ),
inference(resolution,[],[f562,f1178]) ).
fof(f1470,plain,
( ~ c0_1(a110)
| ~ c2_1(a110)
| ~ spl0_34
| spl0_121 ),
inference(resolution,[],[f562,f1018]) ).
fof(f1492,plain,
( ~ c3_1(a112)
| ~ c2_1(a112)
| ~ spl0_46
| spl0_118 ),
inference(resolution,[],[f616,f1002]) ).
fof(f1508,definition,
( spl0_175
<=> c2_1(a112) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1511,plain,
( ~ spl0_175
| ~ spl0_120
| ~ spl0_46
| spl0_118 ),
inference(avatar_split_clause,[],[f1492,f1000,f615,f1010,f1508]) ).
fof(f1512,plain,
( ~ c3_1(a137)
| c2_1(a137)
| ~ spl0_43
| ~ spl0_68 ),
inference(resolution,[],[f735,f604]) ).
fof(f1513,plain,
( c3_1(a137)
| ~ c0_1(a137)
| ~ spl0_29
| ~ spl0_68 ),
inference(resolution,[],[f735,f537]) ).
fof(f1514,plain,
( ~ spl0_69
| spl0_166
| ~ spl0_29
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f1513,f733,f536,f1372,f738]) ).
fof(f1535,plain,
( c2_1(a129)
| ~ c0_1(a129)
| ~ spl0_28
| spl0_158 ),
inference(resolution,[],[f533,f1284]) ).
fof(f1545,plain,
( ~ spl0_99
| spl0_98
| ~ spl0_28
| spl0_158 ),
inference(avatar_split_clause,[],[f1535,f1282,f532,f893,f898]) ).
fof(f1583,plain,
( ~ c0_1(a122)
| ~ c2_1(a122)
| ~ spl0_47
| spl0_104 ),
inference(resolution,[],[f621,f927]) ).
fof(f1607,plain,
( c3_1(a132)
| ~ c2_1(a132)
| ~ spl0_48
| spl0_93 ),
inference(resolution,[],[f629,f868]) ).
fof(f1614,plain,
( ~ spl0_92
| spl0_91
| ~ spl0_48
| spl0_93 ),
inference(avatar_split_clause,[],[f1607,f866,f628,f856,f861]) ).
fof(f1619,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0) )
| ~ spl0_46
| ~ spl0_52 ),
inference(resolution,[],[f647,f616]) ).
fof(f1625,plain,
( ! [X0] :
( ~ c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0) )
| ~ spl0_46
| ~ spl0_52 ),
inference(duplicate_literal_removal,[],[f1619]) ).
fof(f1628,plain,
( ~ spl0_152
| ~ spl0_153
| ~ spl0_34
| spl0_151 ),
inference(avatar_split_clause,[],[f1461,f1176,f561,f1186,f1181]) ).
fof(f1645,plain,
( c2_1(a173)
| c0_1(a173)
| ~ spl0_53
| ~ spl0_78 ),
inference(resolution,[],[f651,f788]) ).
fof(f1687,plain,
( c0_1(a107)
| ~ c2_1(a107)
| ~ spl0_57
| ~ spl0_129 ),
inference(resolution,[],[f669,f1060]) ).
fof(f1695,plain,
( ~ spl0_127
| spl0_128
| ~ spl0_57
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f1687,f1058,f668,f1053,f1048]) ).
fof(f1696,plain,
( spl0_57
| ~ spl0_46
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f1625,f646,f615,f668]) ).
fof(f1714,plain,
( c0_1(a110)
| ~ c2_1(a110)
| ~ spl0_58
| ~ spl0_123 ),
inference(resolution,[],[f674,f1028]) ).
fof(f1725,plain,
( ~ spl0_122
| spl0_163
| ~ spl0_58
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1714,f1026,f673,f1332,f1021]) ).
fof(f1740,plain,
( c0_1(a121)
| ~ c2_1(a121)
| ~ spl0_59
| spl0_106 ),
inference(resolution,[],[f681,f938]) ).
fof(f1744,plain,
( c0_1(a132)
| ~ c2_1(a132)
| ~ spl0_59
| spl0_91 ),
inference(resolution,[],[f681,f858]) ).
fof(f1748,plain,
( c0_1(a173)
| ~ c2_1(a173)
| ~ spl0_59
| spl0_76 ),
inference(resolution,[],[f681,f778]) ).
fof(f1752,plain,
( ~ spl0_168
| spl0_77
| ~ spl0_59
| spl0_76 ),
inference(avatar_split_clause,[],[f1748,f776,f680,f781,f1382]) ).
fof(f1753,plain,
( ~ spl0_92
| spl0_157
| ~ spl0_59
| spl0_91 ),
inference(avatar_split_clause,[],[f1744,f856,f680,f1255,f861]) ).
fof(f1759,plain,
( c0_1(a106)
| c2_1(a106)
| ~ spl0_51
| ~ spl0_131 ),
inference(resolution,[],[f641,f1071]) ).
fof(f1760,plain,
( c0_1(a112)
| c2_1(a112)
| ~ spl0_51
| ~ spl0_120 ),
inference(resolution,[],[f641,f1012]) ).
fof(f1774,plain,
( ~ spl0_122
| ~ spl0_163
| ~ spl0_34
| spl0_121 ),
inference(avatar_split_clause,[],[f1470,f1016,f561,f1332,f1021]) ).
fof(f1799,plain,
( c2_1(a105)
| c0_1(a105)
| ~ spl0_53
| ~ spl0_135 ),
inference(resolution,[],[f1092,f651]) ).
fof(f1800,plain,
( c3_1(a105)
| ~ c0_1(a105)
| ~ spl0_29
| ~ spl0_135 ),
inference(resolution,[],[f1092,f537]) ).
fof(f1807,plain,
( c2_1(a103)
| ~ c0_1(a103)
| ~ spl0_28
| spl0_139 ),
inference(resolution,[],[f533,f1114]) ).
fof(f1822,plain,
( ~ c0_1(a129)
| c2_1(a129)
| ~ spl0_25
| ~ spl0_158 ),
inference(resolution,[],[f1283,f521]) ).
fof(f1830,plain,
( ~ c0_1(a103)
| ~ spl0_29
| ~ spl0_45
| spl0_139 ),
inference(resolution,[],[f1451,f1114]) ).
fof(f1847,plain,
( ~ spl0_141
| ~ spl0_29
| ~ spl0_45
| spl0_139 ),
inference(avatar_split_clause,[],[f1830,f1112,f610,f536,f1122]) ).
fof(f1853,plain,
( spl0_100
| spl0_102
| ~ spl0_41
| spl0_101 ),
inference(avatar_split_clause,[],[f1360,f909,f593,f914,f904]) ).
fof(f1863,plain,
( ~ spl0_107
| spl0_108
| ~ spl0_59
| spl0_106 ),
inference(avatar_split_clause,[],[f1740,f936,f680,f946,f941]) ).
fof(f1867,plain,
( ~ spl0_103
| ~ spl0_105
| ~ spl0_47
| spl0_104 ),
inference(avatar_split_clause,[],[f1583,f925,f620,f930,f920]) ).
fof(f1873,plain,
( spl0_164
| spl0_134
| ~ spl0_53
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1799,f1090,f650,f1085,f1337]) ).
fof(f1874,plain,
( ~ spl0_164
| spl0_133
| ~ spl0_29
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1800,f1090,f536,f1080,f1337]) ).
fof(f1880,plain,
( spl0_132
| spl0_130
| ~ spl0_51
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f1759,f1069,f640,f1064,f1074]) ).
fof(f1881,plain,
( spl0_175
| spl0_119
| ~ spl0_51
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f1760,f1010,f640,f1005,f1508]) ).
fof(f1898,plain,
( c2_1(a108)
| c0_1(a108)
| ~ spl0_53
| ~ spl0_126 ),
inference(resolution,[],[f1044,f651]) ).
fof(f1899,plain,
( spl0_124
| spl0_125
| ~ spl0_53
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1898,f1042,f650,f1037,f1032]) ).
fof(f1913,plain,
( ~ c3_1(a130)
| ~ c2_1(a130)
| ~ spl0_30
| ~ spl0_96 ),
inference(resolution,[],[f545,f884]) ).
fof(f1916,plain,
( ~ spl0_94
| ~ spl0_95
| ~ spl0_30
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f1913,f882,f544,f877,f872]) ).
fof(f1927,plain,
( ~ spl0_141
| spl0_140
| ~ spl0_28
| spl0_139 ),
inference(avatar_split_clause,[],[f1807,f1112,f532,f1117,f1122]) ).
fof(f1928,plain,
( spl0_155
| ~ spl0_72
| ~ spl0_25
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f1200,f744,f520,f754,f1202]) ).
fof(f1930,plain,
( spl0_98
| ~ spl0_99
| ~ spl0_25
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f1822,f1282,f520,f898,f893]) ).
fof(f1931,plain,
( ~ spl0_99
| ~ spl0_158
| ~ spl0_37
| spl0_97 ),
inference(avatar_split_clause,[],[f1271,f888,f574,f1282,f898]) ).
fof(f1935,plain,
( ~ spl0_99
| spl0_98
| ~ spl0_38
| spl0_97 ),
inference(avatar_split_clause,[],[f1304,f888,f578,f893,f898]) ).
fof(f1936,plain,
( spl0_155
| ~ spl0_70
| ~ spl0_43
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f1425,f749,f603,f744,f1202]) ).
fof(f1937,plain,
( spl0_67
| ~ spl0_166
| ~ spl0_43
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f1512,f733,f603,f1372,f728]) ).
fof(f1939,plain,
( spl0_148
| ~ spl0_150
| ~ spl0_45
| spl0_149 ),
inference(avatar_split_clause,[],[f1431,f1165,f610,f1170,f1160]) ).
fof(f1942,plain,
( spl0_91
| ~ spl0_157
| ~ spl0_45
| spl0_93 ),
inference(avatar_split_clause,[],[f1444,f866,f610,f1255,f856]) ).
fof(f1944,plain,
( spl0_77
| spl0_168
| ~ spl0_53
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f1645,f786,f650,f1382,f781]) ).
fof(f1965,plain,
( c2_1(a105)
| ~ c0_1(a105)
| ~ spl0_27
| ~ spl0_135 ),
inference(resolution,[],[f529,f1092]) ).
fof(f1976,plain,
( ~ spl0_164
| spl0_134
| ~ spl0_27
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1965,f1090,f528,f1085,f1337]) ).
fof(f1985,plain,
( ~ c3_1(a129)
| c2_1(a129)
| ~ spl0_36
| spl0_97 ),
inference(resolution,[],[f571,f890]) ).
fof(f1993,plain,
( spl0_98
| ~ spl0_158
| ~ spl0_36
| spl0_97 ),
inference(avatar_split_clause,[],[f1985,f888,f570,f1282,f893]) ).
fof(f2041,plain,
( ~ c3_1(a113)
| ~ c0_1(a113)
| ~ spl0_44
| ~ spl0_116 ),
inference(resolution,[],[f608,f991]) ).
fof(f2047,plain,
( ~ c3_1(a101)
| ~ c0_1(a101)
| ~ spl0_44
| ~ spl0_71 ),
inference(resolution,[],[f608,f751]) ).
fof(f2051,plain,
( ~ spl0_72
| ~ spl0_70
| ~ spl0_44
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f2047,f749,f607,f744,f754]) ).
fof(f2054,plain,
( ~ spl0_117
| ~ spl0_156
| ~ spl0_44
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f2041,f989,f607,f1211,f994]) ).
fof(f2069,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_45
| ~ spl0_50 ),
inference(resolution,[],[f637,f611]) ).
fof(f2073,plain,
( ~ c2_1(a110)
| c3_1(a110)
| ~ spl0_50
| ~ spl0_123 ),
inference(resolution,[],[f637,f1028]) ).
fof(f2082,plain,
( ! [X0] :
( ~ c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_45
| ~ spl0_50 ),
inference(duplicate_literal_removal,[],[f2069]) ).
fof(f2086,plain,
( spl0_121
| ~ spl0_122
| ~ spl0_50
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f2073,f1026,f636,f1021,f1016]) ).
fof(f2087,plain,
( spl0_34
| ~ spl0_45
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f2082,f636,f610,f561]) ).
fof(f2088,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0)
| c3_1(X0) )
| ~ spl0_45
| ~ spl0_49 ),
inference(resolution,[],[f634,f611]) ).
fof(f2091,plain,
( c2_1(a105)
| c3_1(a105)
| ~ spl0_49
| ~ spl0_135 ),
inference(resolution,[],[f634,f1092]) ).
fof(f2102,plain,
( ! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ c0_1(X0) )
| ~ spl0_45
| ~ spl0_49 ),
inference(duplicate_literal_removal,[],[f2088]) ).
fof(f2104,plain,
( spl0_133
| spl0_134
| ~ spl0_49
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f2091,f1090,f633,f1085,f1080]) ).
fof(f2106,plain,
( spl0_28
| ~ spl0_45
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f2102,f633,f610,f532]) ).
cnf(s3,plain,
( ~ spl0_1
| ~ spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f437]) ).
cnf(s7,plain,
( ~ spl0_3
| ~ spl0_13
| ~ spl0_14 ),
inference(sat_conversion,[],[f473]) ).
cnf(s8,plain,
( ~ spl0_14
| spl0_15
| ~ spl0_16 ),
inference(sat_conversion,[],[f482]) ).
cnf(s9,plain,
( ~ spl0_2
| ~ spl0_14
| ~ spl0_17 ),
inference(sat_conversion,[],[f487]) ).
cnf(s10,plain,
( ~ spl0_17
| ~ spl0_18 ),
inference(sat_conversion,[],[f492]) ).
cnf(s11,plain,
( spl0_19
| ~ spl0_20
| spl0_21 ),
inference(sat_conversion,[],[f505]) ).
cnf(s13,plain,
( ~ spl0_20
| spl0_23
| spl0_24
| spl0_25 ),
inference(sat_conversion,[],[f522]) ).
cnf(s14,plain,
( spl0_21
| spl0_24
| ~ spl0_26
| spl0_27 ),
inference(sat_conversion,[],[f530]) ).
cnf(s15,plain,
( ~ spl0_5
| spl0_11
| spl0_24
| spl0_28 ),
inference(sat_conversion,[],[f534]) ).
cnf(s16,plain,
( spl0_6
| spl0_24
| spl0_29 ),
inference(sat_conversion,[],[f538]) ).
cnf(s17,plain,
( ~ spl0_9
| spl0_24
| spl0_29 ),
inference(sat_conversion,[],[f539]) ).
cnf(s18,plain,
( ~ spl0_2
| ~ spl0_14
| spl0_24
| spl0_29 ),
inference(sat_conversion,[],[f540]) ).
cnf(s20,plain,
( ~ spl0_3
| spl0_21
| spl0_24
| spl0_29 ),
inference(sat_conversion,[],[f542]) ).
cnf(s22,plain,
( ~ spl0_8
| spl0_24
| spl0_28
| spl0_30 ),
inference(sat_conversion,[],[f547]) ).
cnf(s23,plain,
( ~ spl0_16
| spl0_24
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f555]) ).
cnf(s24,plain,
( spl0_15
| spl0_24
| spl0_31
| spl0_33 ),
inference(sat_conversion,[],[f559]) ).
cnf(s30,plain,
( spl0_23
| spl0_24
| spl0_29
| spl0_38 ),
inference(sat_conversion,[],[f581]) ).
cnf(s32,plain,
( spl0_24
| spl0_25
| spl0_36
| spl0_38 ),
inference(sat_conversion,[],[f587]) ).
cnf(s34,plain,
( ~ spl0_3
| spl0_23
| spl0_24
| spl0_41 ),
inference(sat_conversion,[],[f596]) ).
cnf(s36,plain,
( spl0_24
| spl0_38
| spl0_41
| spl0_43 ),
inference(sat_conversion,[],[f605]) ).
cnf(s37,plain,
( ~ spl0_14
| spl0_24
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f612]) ).
cnf(s38,plain,
( spl0_24
| spl0_30
| spl0_34
| spl0_45 ),
inference(sat_conversion,[],[f613]) ).
cnf(s40,plain,
( spl0_22
| spl0_24
| spl0_33
| spl0_46 ),
inference(sat_conversion,[],[f618]) ).
cnf(s43,plain,
( spl0_15
| spl0_24
| spl0_37
| spl0_47 ),
inference(sat_conversion,[],[f624]) ).
cnf(s44,plain,
( spl0_24
| spl0_28
| spl0_38
| spl0_47 ),
inference(sat_conversion,[],[f625]) ).
cnf(s46,plain,
( ~ spl0_3
| ~ spl0_14
| spl0_24
| spl0_48 ),
inference(sat_conversion,[],[f630]) ).
cnf(s47,plain,
( ~ spl0_1
| spl0_24
| spl0_28
| spl0_48 ),
inference(sat_conversion,[],[f631]) ).
cnf(s48,plain,
( spl0_24
| spl0_48
| spl0_49
| spl0_50 ),
inference(sat_conversion,[],[f638]) ).
cnf(s50,plain,
( spl0_23
| spl0_24
| spl0_25
| spl0_51 ),
inference(sat_conversion,[],[f643]) ).
cnf(s52,plain,
( ~ spl0_9
| spl0_24
| spl0_45
| spl0_52 ),
inference(sat_conversion,[],[f648]) ).
cnf(s53,plain,
( ~ spl0_5
| spl0_24
| spl0_28
| spl0_53 ),
inference(sat_conversion,[],[f652]) ).
cnf(s55,plain,
( ~ spl0_1
| spl0_24
| spl0_51
| spl0_53 ),
inference(sat_conversion,[],[f654]) ).
cnf(s61,plain,
( spl0_24
| spl0_43
| spl0_46
| spl0_58 ),
inference(sat_conversion,[],[f676]) ).
cnf(s65,plain,
( ~ spl0_4
| spl0_24
| spl0_30
| spl0_59 ),
inference(sat_conversion,[],[f683]) ).
cnf(s66,plain,
( spl0_24
| spl0_33
| spl0_51
| spl0_59 ),
inference(sat_conversion,[],[f684]) ).
cnf(s67,plain,
( spl0_24
| spl0_37
| spl0_57
| spl0_59 ),
inference(sat_conversion,[],[f685]) ).
cnf(s81,plain,
( spl0_26
| spl0_64 ),
inference(sat_conversion,[],[f715]) ).
cnf(s82,plain,
( spl0_26
| ~ spl0_65 ),
inference(sat_conversion,[],[f720]) ).
cnf(s83,plain,
( spl0_26
| spl0_66 ),
inference(sat_conversion,[],[f725]) ).
cnf(s85,plain,
( ~ spl0_22
| ~ spl0_67 ),
inference(sat_conversion,[],[f731]) ).
cnf(s86,plain,
( ~ spl0_22
| spl0_68 ),
inference(sat_conversion,[],[f736]) ).
cnf(s87,plain,
( ~ spl0_22
| spl0_69 ),
inference(sat_conversion,[],[f741]) ).
cnf(s89,plain,
( ~ spl0_21
| spl0_70 ),
inference(sat_conversion,[],[f747]) ).
cnf(s90,plain,
( ~ spl0_21
| spl0_71 ),
inference(sat_conversion,[],[f752]) ).
cnf(s91,plain,
( ~ spl0_21
| spl0_72 ),
inference(sat_conversion,[],[f757]) ).
cnf(s92,plain,
( ~ spl0_21
| ~ spl0_24 ),
inference(sat_conversion,[],[f758]) ).
cnf(s97,plain,
( ~ spl0_11
| ~ spl0_76 ),
inference(sat_conversion,[],[f779]) ).
cnf(s98,plain,
( ~ spl0_11
| ~ spl0_77 ),
inference(sat_conversion,[],[f784]) ).
cnf(s99,plain,
( ~ spl0_11
| spl0_78 ),
inference(sat_conversion,[],[f789]) ).
cnf(s117,plain,
( ~ spl0_15
| ~ spl0_91 ),
inference(sat_conversion,[],[f859]) ).
cnf(s118,plain,
( ~ spl0_15
| spl0_92 ),
inference(sat_conversion,[],[f864]) ).
cnf(s119,plain,
( ~ spl0_15
| ~ spl0_93 ),
inference(sat_conversion,[],[f869]) ).
cnf(s121,plain,
( spl0_3
| spl0_94 ),
inference(sat_conversion,[],[f875]) ).
cnf(s122,plain,
( spl0_3
| spl0_95 ),
inference(sat_conversion,[],[f880]) ).
cnf(s123,plain,
( spl0_3
| spl0_96 ),
inference(sat_conversion,[],[f885]) ).
cnf(s125,plain,
( spl0_14
| ~ spl0_97 ),
inference(sat_conversion,[],[f891]) ).
cnf(s126,plain,
( spl0_14
| ~ spl0_98 ),
inference(sat_conversion,[],[f896]) ).
cnf(s127,plain,
( spl0_14
| spl0_99 ),
inference(sat_conversion,[],[f901]) ).
cnf(s129,plain,
( spl0_13
| ~ spl0_100 ),
inference(sat_conversion,[],[f907]) ).
cnf(s130,plain,
( spl0_13
| ~ spl0_101 ),
inference(sat_conversion,[],[f912]) ).
cnf(s131,plain,
( spl0_13
| ~ spl0_102 ),
inference(sat_conversion,[],[f917]) ).
cnf(s133,plain,
( spl0_5
| spl0_103 ),
inference(sat_conversion,[],[f923]) ).
cnf(s134,plain,
( spl0_5
| ~ spl0_104 ),
inference(sat_conversion,[],[f928]) ).
cnf(s135,plain,
( spl0_5
| spl0_105 ),
inference(sat_conversion,[],[f933]) ).
cnf(s137,plain,
( spl0_1
| ~ spl0_106 ),
inference(sat_conversion,[],[f939]) ).
cnf(s138,plain,
( spl0_1
| spl0_107 ),
inference(sat_conversion,[],[f944]) ).
cnf(s139,plain,
( spl0_1
| ~ spl0_108 ),
inference(sat_conversion,[],[f949]) ).
cnf(s140,plain,
( spl0_1
| ~ spl0_24 ),
inference(sat_conversion,[],[f950]) ).
cnf(s145,plain,
( spl0_17
| ~ spl0_112 ),
inference(sat_conversion,[],[f971]) ).
cnf(s146,plain,
( spl0_17
| spl0_113 ),
inference(sat_conversion,[],[f976]) ).
cnf(s147,plain,
( spl0_17
| spl0_114 ),
inference(sat_conversion,[],[f981]) ).
cnf(s149,plain,
( spl0_18
| spl0_115 ),
inference(sat_conversion,[],[f987]) ).
cnf(s150,plain,
( spl0_18
| spl0_116 ),
inference(sat_conversion,[],[f992]) ).
cnf(s151,plain,
( spl0_18
| spl0_117 ),
inference(sat_conversion,[],[f997]) ).
cnf(s153,plain,
( spl0_8
| ~ spl0_118 ),
inference(sat_conversion,[],[f1003]) ).
cnf(s154,plain,
( spl0_8
| ~ spl0_119 ),
inference(sat_conversion,[],[f1008]) ).
cnf(s155,plain,
( spl0_8
| spl0_120 ),
inference(sat_conversion,[],[f1013]) ).
cnf(s157,plain,
( spl0_4
| ~ spl0_121 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s158,plain,
( spl0_4
| spl0_122 ),
inference(sat_conversion,[],[f1024]) ).
cnf(s159,plain,
( spl0_4
| spl0_123 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s161,plain,
( spl0_20
| ~ spl0_124 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s162,plain,
( spl0_20
| ~ spl0_125 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s163,plain,
( spl0_20
| spl0_126 ),
inference(sat_conversion,[],[f1045]) ).
cnf(s164,plain,
( spl0_20
| ~ spl0_24 ),
inference(sat_conversion,[],[f1046]) ).
cnf(s165,plain,
( spl0_2
| spl0_127 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s166,plain,
( spl0_2
| ~ spl0_128 ),
inference(sat_conversion,[],[f1056]) ).
cnf(s167,plain,
( spl0_2
| spl0_129 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s169,plain,
( ~ spl0_31
| ~ spl0_130 ),
inference(sat_conversion,[],[f1067]) ).
cnf(s170,plain,
( ~ spl0_31
| spl0_131 ),
inference(sat_conversion,[],[f1072]) ).
cnf(s171,plain,
( ~ spl0_31
| ~ spl0_132 ),
inference(sat_conversion,[],[f1077]) ).
cnf(s173,plain,
( ~ spl0_6
| ~ spl0_133 ),
inference(sat_conversion,[],[f1083]) ).
cnf(s174,plain,
( ~ spl0_6
| ~ spl0_134 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s175,plain,
( ~ spl0_6
| spl0_135 ),
inference(sat_conversion,[],[f1093]) ).
cnf(s181,plain,
( spl0_16
| ~ spl0_139 ),
inference(sat_conversion,[],[f1115]) ).
cnf(s182,plain,
( spl0_16
| ~ spl0_140 ),
inference(sat_conversion,[],[f1120]) ).
cnf(s183,plain,
( spl0_16
| spl0_141 ),
inference(sat_conversion,[],[f1125]) ).
cnf(s192,plain,
( ~ spl0_19
| ~ spl0_24 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s193,plain,
( ~ spl0_23
| ~ spl0_148 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s194,plain,
( ~ spl0_23
| ~ spl0_149 ),
inference(sat_conversion,[],[f1168]) ).
cnf(s195,plain,
( ~ spl0_23
| spl0_150 ),
inference(sat_conversion,[],[f1173]) ).
cnf(s197,plain,
( spl0_9
| ~ spl0_151 ),
inference(sat_conversion,[],[f1179]) ).
cnf(s198,plain,
( spl0_9
| spl0_152 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s199,plain,
( spl0_9
| spl0_153 ),
inference(sat_conversion,[],[f1189]) ).
cnf(s202,plain,
( ~ spl0_25
| ~ spl0_64
| spl0_65
| ~ spl0_66 ),
inference(sat_conversion,[],[f1199]) ).
cnf(s204,plain,
( ~ spl0_29
| spl0_112
| ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s205,plain,
( ~ spl0_29
| ~ spl0_116
| ~ spl0_117
| spl0_156 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s206,plain,
( ~ spl0_30
| ~ spl0_115
| ~ spl0_116
| ~ spl0_156 ),
inference(sat_conversion,[],[f1218]) ).
cnf(s207,plain,
( ~ spl0_30
| ~ spl0_70
| ~ spl0_71
| ~ spl0_155 ),
inference(sat_conversion,[],[f1219]) ).
cnf(s210,plain,
( ~ spl0_32
| ~ spl0_115
| ~ spl0_117
| ~ spl0_156 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s211,plain,
( ~ spl0_33
| ~ spl0_115
| ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s212,plain,
( ~ spl0_33
| ~ spl0_71
| ~ spl0_72
| ~ spl0_155 ),
inference(sat_conversion,[],[f1233]) ).
cnf(s215,plain,
( ~ spl0_37
| spl0_104
| ~ spl0_105
| ~ spl0_159 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s225,plain,
( ~ spl0_34
| ~ spl0_103
| ~ spl0_105
| spl0_159 ),
inference(sat_conversion,[],[f1348]) ).
cnf(s233,plain,
( ~ spl0_41
| spl0_97
| spl0_98
| spl0_158 ),
inference(sat_conversion,[],[f1398]) ).
cnf(s243,plain,
( spl0_28
| ~ spl0_29
| ~ spl0_41 ),
inference(sat_conversion,[],[f1424]) ).
cnf(s244,plain,
( ~ spl0_45
| spl0_97
| ~ spl0_99
| spl0_158 ),
inference(sat_conversion,[],[f1452]) ).
cnf(s245,plain,
( ~ spl0_45
| spl0_104
| ~ spl0_105
| spl0_159 ),
inference(sat_conversion,[],[f1453]) ).
cnf(s249,plain,
( ~ spl0_46
| spl0_118
| ~ spl0_120
| ~ spl0_175 ),
inference(sat_conversion,[],[f1511]) ).
cnf(s250,plain,
( ~ spl0_29
| ~ spl0_68
| ~ spl0_69
| spl0_166 ),
inference(sat_conversion,[],[f1514]) ).
cnf(s254,plain,
( ~ spl0_28
| spl0_98
| ~ spl0_99
| spl0_158 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s258,plain,
( ~ spl0_48
| spl0_91
| ~ spl0_92
| spl0_93 ),
inference(sat_conversion,[],[f1614]) ).
cnf(s261,plain,
( ~ spl0_34
| spl0_151
| ~ spl0_152
| ~ spl0_153 ),
inference(sat_conversion,[],[f1628]) ).
cnf(s277,plain,
( ~ spl0_57
| ~ spl0_127
| spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f1695]) ).
cnf(s278,plain,
( ~ spl0_46
| ~ spl0_52
| spl0_57 ),
inference(sat_conversion,[],[f1696]) ).
cnf(s282,plain,
( ~ spl0_58
| ~ spl0_122
| ~ spl0_123
| spl0_163 ),
inference(sat_conversion,[],[f1725]) ).
cnf(s283,plain,
( ~ spl0_59
| spl0_76
| spl0_77
| ~ spl0_168 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s284,plain,
( ~ spl0_59
| spl0_91
| ~ spl0_92
| spl0_157 ),
inference(sat_conversion,[],[f1753]) ).
cnf(s297,plain,
( ~ spl0_34
| spl0_121
| ~ spl0_122
| ~ spl0_163 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s317,plain,
( ~ spl0_29
| ~ spl0_45
| spl0_139
| ~ spl0_141 ),
inference(sat_conversion,[],[f1847]) ).
cnf(s323,plain,
( ~ spl0_41
| spl0_100
| spl0_101
| spl0_102 ),
inference(sat_conversion,[],[f1853]) ).
cnf(s333,plain,
( ~ spl0_59
| spl0_106
| ~ spl0_107
| spl0_108 ),
inference(sat_conversion,[],[f1863]) ).
cnf(s337,plain,
( ~ spl0_47
| ~ spl0_103
| spl0_104
| ~ spl0_105 ),
inference(sat_conversion,[],[f1867]) ).
cnf(s343,plain,
( ~ spl0_53
| spl0_134
| ~ spl0_135
| spl0_164 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s344,plain,
( ~ spl0_29
| spl0_133
| ~ spl0_135
| ~ spl0_164 ),
inference(sat_conversion,[],[f1874]) ).
cnf(s350,plain,
( ~ spl0_51
| spl0_130
| ~ spl0_131
| spl0_132 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s351,plain,
( ~ spl0_51
| spl0_119
| ~ spl0_120
| spl0_175 ),
inference(sat_conversion,[],[f1881]) ).
cnf(s357,plain,
( ~ spl0_53
| spl0_124
| spl0_125
| ~ spl0_126 ),
inference(sat_conversion,[],[f1899]) ).
cnf(s359,plain,
( ~ spl0_30
| ~ spl0_94
| ~ spl0_95
| ~ spl0_96 ),
inference(sat_conversion,[],[f1916]) ).
cnf(s370,plain,
( ~ spl0_28
| spl0_139
| spl0_140
| ~ spl0_141 ),
inference(sat_conversion,[],[f1927]) ).
cnf(s371,plain,
( ~ spl0_25
| ~ spl0_70
| ~ spl0_72
| spl0_155 ),
inference(sat_conversion,[],[f1928]) ).
cnf(s373,plain,
( ~ spl0_25
| spl0_98
| ~ spl0_99
| ~ spl0_158 ),
inference(sat_conversion,[],[f1930]) ).
cnf(s374,plain,
( ~ spl0_37
| spl0_97
| ~ spl0_99
| ~ spl0_158 ),
inference(sat_conversion,[],[f1931]) ).
cnf(s378,plain,
( ~ spl0_38
| spl0_97
| spl0_98
| ~ spl0_99 ),
inference(sat_conversion,[],[f1935]) ).
cnf(s379,plain,
( ~ spl0_43
| ~ spl0_70
| ~ spl0_71
| spl0_155 ),
inference(sat_conversion,[],[f1936]) ).
cnf(s380,plain,
( ~ spl0_43
| spl0_67
| ~ spl0_68
| ~ spl0_166 ),
inference(sat_conversion,[],[f1937]) ).
cnf(s382,plain,
( ~ spl0_45
| spl0_148
| spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s385,plain,
( ~ spl0_45
| spl0_91
| spl0_93
| ~ spl0_157 ),
inference(sat_conversion,[],[f1942]) ).
cnf(s387,plain,
( ~ spl0_53
| spl0_77
| ~ spl0_78
| spl0_168 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s389,plain,
( ~ spl0_27
| spl0_134
| ~ spl0_135
| ~ spl0_164 ),
inference(sat_conversion,[],[f1976]) ).
cnf(s392,plain,
( ~ spl0_36
| spl0_97
| spl0_98
| ~ spl0_158 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s395,plain,
( ~ spl0_44
| ~ spl0_70
| ~ spl0_71
| ~ spl0_72 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s398,plain,
( ~ spl0_44
| ~ spl0_116
| ~ spl0_117
| ~ spl0_156 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s402,plain,
( ~ spl0_50
| spl0_121
| ~ spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f2086]) ).
cnf(s403,plain,
( spl0_34
| ~ spl0_45
| ~ spl0_50 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s405,plain,
( ~ spl0_49
| spl0_133
| spl0_134
| ~ spl0_135 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s407,plain,
( spl0_28
| ~ spl0_45
| ~ spl0_49 ),
inference(sat_conversion,[],[f2106]) ).
cnf(s408,plain,
( spl0_5
| spl0_30
| ~ spl0_37
| spl0_24 ),
inference(rat,[],[s38,s245,s225,s215,s133,s134,s135]) ).
cnf(s410,plain,
( spl0_14
| ~ spl0_28
| ~ spl0_37 ),
inference(rat,[],[s374,s254,s125,s126,s127]) ).
cnf(s412,plain,
( spl0_16
| ~ spl0_28 ),
inference(rat,[],[s370,s181,s182,s183]) ).
cnf(s413,plain,
( spl0_17
| ~ spl0_29 ),
inference(rat,[],[s204,s145,s146,s147]) ).
cnf(s414,plain,
( ~ spl0_29
| ~ spl0_16
| spl0_1 ),
inference(rat,[],[s350,s169,s170,s171,s23,s66,s210,s211,s205,s149,s150,s151,s10,s413,s140,s333,s137,s138,s139]) ).
cnf(s415,plain,
( ~ spl0_49
| ~ spl0_45
| spl0_1 ),
inference(rat,[],[s405,s173,s174,s175,s16,s414,s412,s407,s140]) ).
cnf(s416,plain,
( ~ spl0_15
| ~ spl0_48 ),
inference(rat,[],[s258,s117,s118,s119]) ).
cnf(s417,plain,
( ~ spl0_28
| spl0_15
| ~ spl0_37 ),
inference(rat,[],[s8,s412,s410]) ).
cnf(s418,plain,
( spl0_14
| ~ spl0_45
| ~ spl0_37 ),
inference(rat,[],[s244,s374,s125,s127]) ).
cnf(s419,plain,
( spl0_33
| spl0_15
| spl0_1 ),
inference(rat,[],[s350,s169,s170,s171,s24,s66,s140,s333,s137,s138,s139]) ).
cnf(s420,plain,
( spl0_18
| ~ spl0_33 ),
inference(rat,[],[s211,s149,s150,s151]) ).
cnf(s421,plain,
( spl0_20
| ~ spl0_53 ),
inference(rat,[],[s357,s161,s162,s163]) ).
cnf(s422,plain,
( ~ spl0_23
| ~ spl0_45 ),
inference(rat,[],[s382,s193,s194,s195]) ).
cnf(s424,plain,
( spl0_26
| ~ spl0_25 ),
inference(rat,[],[s202,s81,s82,s83]) ).
cnf(s425,plain,
( ~ spl0_45
| spl0_30
| ~ spl0_37
| spl0_1 ),
inference(rat,[],[s371,s212,s89,s90,s91,s14,s424,s13,s422,s421,s419,s389,s343,s174,s175,s16,s317,s181,s183,s8,s418,s53,s417,s416,s48,s415,s402,s157,s158,s159,s65,s333,s137,s138,s139,s408,s140]) ).
cnf(s426,plain,
( spl0_9
| ~ spl0_34 ),
inference(rat,[],[s261,s197,s198,s199]) ).
cnf(s427,plain,
( spl0_30
| spl0_57
| spl0_1 ),
inference(rat,[],[s380,s250,s85,s86,s87,s40,s420,s61,s10,s278,s413,s52,s17,s426,s282,s297,s38,s425,s157,s158,s159,s65,s67,s140,s333,s137,s138,s139]) ).
cnf(s428,plain,
( ~ spl0_3
| spl0_23
| ~ spl0_14
| spl0_24 ),
inference(rat,[],[s323,s129,s130,s131,s7,s34]) ).
cnf(s429,plain,
( spl0_3
| ~ spl0_30 ),
inference(rat,[],[s359,s121,s122,s123]) ).
cnf(s430,plain,
( ~ spl0_45
| ~ spl0_3
| ~ spl0_37
| spl0_24 ),
inference(rat,[],[s428,s422,s418]) ).
cnf(s431,plain,
( ~ spl0_14
| spl0_57
| spl0_1 ),
inference(rat,[],[s395,s89,s90,s91,s20,s413,s10,s420,s419,s416,s46,s37,s430,s429,s427,s67,s333,s137,s138,s139,s140]) ).
cnf(s433,plain,
( ~ spl0_21
| ~ spl0_43
| ~ spl0_30 ),
inference(rat,[],[s207,s379,s89,s90]) ).
cnf(s434,plain,
( spl0_57
| spl0_1 ),
inference(rat,[],[s206,s205,s149,s150,s151,s10,s413,s20,s433,s36,s233,s378,s374,s125,s126,s127,s431,s429,s427,s67,s140,s333,s137,s138,s139]) ).
cnf(s435,plain,
( spl0_14
| ~ spl0_38 ),
inference(rat,[],[s378,s125,s126,s127]) ).
cnf(s436,plain,
( spl0_2
| ~ spl0_57 ),
inference(rat,[],[s165,s277,s166,s167]) ).
cnf(s437,plain,
( ~ spl0_45
| spl0_50
| spl0_1 ),
inference(rat,[],[s435,s18,s30,s413,s10,s420,s419,s416,s48,s422,s415,s140,s436,s434]) ).
cnf(s438,plain,
( spl0_30
| spl0_1 ),
inference(rat,[],[s380,s250,s85,s86,s87,s40,s249,s351,s153,s154,s155,s36,s66,s243,s22,s435,s420,s412,s9,s10,s414,s413,s17,s426,s38,s437,s402,s157,s158,s159,s65,s140,s333,s137,s138,s139,s436,s434]) ).
cnf(s440,plain,
( ~ spl0_14
| spl0_24
| ~ spl0_2 ),
inference(rat,[],[s413,s9,s18]) ).
cnf(s441,plain,
( ~ spl0_21
| spl0_1 ),
inference(rat,[],[s392,s32,s233,s371,s36,s207,s433,s89,s90,s91,s438,s126,s125,s435,s440,s140,s436,s434]) ).
cnf(s442,plain,
spl0_1,
inference(rat,[],[s206,s205,s149,s150,s151,s10,s413,s20,s441,s429,s438,s140]) ).
cnf(s443,plain,
( ~ spl0_5
| spl0_28
| spl0_15
| spl0_23
| ~ spl0_6
| spl0_24 ),
inference(rat,[],[s350,s169,s170,s171,s24,s66,s212,s371,s89,s90,s91,s14,s424,s283,s387,s389,s13,s97,s98,s99,s343,s421,s15,s53,s175,s174]) ).
cnf(s444,plain,
( ~ spl0_45
| spl0_29
| spl0_24 ),
inference(rat,[],[s43,s337,s408,s133,s134,s135,s443,s412,s429,s8,s428,s416,s435,s48,s30,s403,s422,s426,s17,s405,s173,s174,s175,s16]) ).
cnf(s445,plain,
( spl0_29
| spl0_24 ),
inference(rat,[],[s233,s392,s36,s32,s435,s125,s126,s371,s37,s207,s395,s433,s89,s90,s91,s20,s429,s38,s444,s426,s17]) ).
cnf(s446,plain,
( ~ spl0_16
| ~ spl0_14
| ~ spl0_45
| spl0_24 ),
inference(rat,[],[s66,s350,s284,s385,s169,s170,s171,s117,s118,s119,s23,s8,s420,s210,s205,s150,s151,s149,s10,s413,s445]) ).
cnf(s447,plain,
( spl0_16
| ~ spl0_45
| ~ spl0_29 ),
inference(rat,[],[s317,s181,s183]) ).
cnf(s448,plain,
( ~ spl0_45
| spl0_24 ),
inference(rat,[],[s373,s50,s244,s350,s125,s126,s127,s169,s170,s171,s446,s23,s447,s422,s210,s205,s150,s151,s149,s10,s413,s445]) ).
cnf(s450,plain,
( ~ spl0_6
| ~ spl0_53
| ~ spl0_29 ),
inference(rat,[],[s344,s343,s173,s174,s175]) ).
cnf(s451,plain,
( spl0_28
| spl0_24 ),
inference(rat,[],[s337,s133,s134,s135,s3,s450,s55,s350,s169,s170,s171,s24,s416,s44,s47,s420,s435,s37,s448,s398,s205,s151,s150,s10,s413,s445,s442]) ).
cnf(s452,plain,
( spl0_45
| spl0_44
| spl0_24 ),
inference(rat,[],[s32,s392,s373,s254,s451,s435,s125,s126,s127,s37]) ).
cnf(s453,plain,
spl0_24,
inference(rat,[],[s452,s448,s398,s205,s150,s151,s10,s413,s445]) ).
cnf(s456,plain,
~ spl0_19,
inference(rat,[],[s192,s453]) ).
cnf(s463,plain,
spl0_20,
inference(rat,[],[s164,s453]) ).
cnf(s480,plain,
~ spl0_21,
inference(rat,[],[s92,s453]) ).
cnf(s483,plain,
$false,
inference(rat,[],[s11,s463,s480,s456]) ).
fof(f2107,plain,
$false,
inference(avatar_sat_refutation,[],[s483]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN501+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n003.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 16:19:43 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.26 % (1731003)Will run a generic schedule for satisfiability detection.
% 0.08/0.26 % (1731014)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3529152141:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.26 % (1731009)% WARNING: option uhcvi not known.
% 0.08/0.26 % (1731012)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2184529541:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.26 % (1731008)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=662808921_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.26 % (1731010)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1259695934:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.26 % (1731011)dis+10_1_sil=32000:sp=arity:random_seed=949463751:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.26 % (1731013)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1085881404:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.26 % (1731009)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2592356614:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.26 % (1731014) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1731003-1731014"...
% 0.08/0.26 % Detected minimum model sizes of [1]
% 0.08/0.26 % Detected maximum model sizes of [30]
% 0.08/0.26 % TRYING [1]
% 0.08/0.26 % TRYING [2]
% 0.08/0.26 % (1731014)...printing done.
% 0.08/0.26 % TRYING [3]
% 0.08/0.26 % (1731014)Refutation found. Thanks to Tanya!
% 0.08/0.26 % SZS status Theorem for theBenchmark
% 0.08/0.26 % SZS output start Proof for theBenchmark
% See solution above
% 0.43/0.27 % (1731014)------------------------------
% 0.43/0.27 % (1731014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.27 % (1731014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.27 % (1731014)CaDiCaL version: 2.1.3
% 0.43/0.27 % (1731014)Termination reason: Refutation
% 0.43/0.27 % (1731014)Time elapsed: 0.017 s
% 0.43/0.27 % (1731014)Peak memory usage: 13 MB
% 0.43/0.27 % (1731014)Instructions burned: 49 (million)
% 0.43/0.27 % (1731003)Success in time 0.048 s
% 0.43/0.27 % Vampire exiting
%------------------------------------------------------------------------------