%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN445+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:51:43 PM UTC 2026
% Result : Theorem 1.30s 1.13s
% Output : Refutation 3.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 104
% Syntax : Number of formulae : 588 ( 15 unt; 103 def)
% Number of atoms : 4904 ( 0 equ)
% Maximal formula atoms : 606 ( 8 avg)
% Number of connectives : 6532 (2216 ~;3036 |; 895 &)
% ( 103 <=>; 282 =>; 0 <=; 0 <~>)
% Maximal formula depth : 97 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 139 ( 138 usr; 135 prp; 0-1 aty)
% Number of functors : 30 ( 30 usr; 30 con; 0-0 aty)
% Number of variables : 596 ( 0 sgn 596 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( ~ hskp0
| ( ndr1_0
& ~ c0_1(a294)
& ~ c2_1(a294)
& ~ c3_1(a294) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a295)
& c2_1(a295)
& ~ c1_1(a295) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a297)
& ~ c0_1(a297)
& ~ c3_1(a297) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a299)
& c3_1(a299)
& ~ c2_1(a299) ) )
& ( ~ hskp4
| ( ndr1_0
& ~ c0_1(a300)
& ~ c1_1(a300)
& ~ c2_1(a300) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a301)
& ~ c1_1(a301)
& ~ c3_1(a301) ) )
& ( ~ hskp6
| ( ndr1_0
& c0_1(a302)
& ~ c1_1(a302)
& ~ c2_1(a302) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a303)
& c1_1(a303)
& ~ c2_1(a303) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a305)
& ~ c0_1(a305)
& ~ c1_1(a305) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a307)
& ~ c1_1(a307)
& ~ c3_1(a307) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a308)
& c3_1(a308)
& ~ c0_1(a308) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a309)
& c3_1(a309)
& ~ c2_1(a309) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a310)
& ~ c0_1(a310)
& ~ c2_1(a310) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a313)
& c3_1(a313)
& ~ c1_1(a313) ) )
& ( ~ hskp14
| ( ndr1_0
& c1_1(a315)
& c2_1(a315)
& ~ c0_1(a315) ) )
& ( ~ hskp15
| ( ndr1_0
& c1_1(a320)
& ~ c0_1(a320)
& ~ c2_1(a320) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a321)
& c3_1(a321)
& ~ c1_1(a321) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a323)
& c2_1(a323)
& ~ c3_1(a323) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a329)
& ~ c0_1(a329)
& ~ c3_1(a329) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a330)
& c2_1(a330)
& ~ c3_1(a330) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a333)
& ~ c2_1(a333)
& ~ c3_1(a333) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a336)
& ~ c0_1(a336)
& ~ c1_1(a336) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c1_1(a338)
& ~ c2_1(a338)
& ~ c3_1(a338) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a341)
& c3_1(a341)
& ~ c0_1(a341) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a342)
& ~ c1_1(a342)
& ~ c2_1(a342) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c0_1(a346)
& ~ c1_1(a346)
& ~ c3_1(a346) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a349)
& ~ c2_1(a349)
& ~ c3_1(a349) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a334)
& c2_1(a334)
& c3_1(a334) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a353)
& c2_1(a353)
& c3_1(a353) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a354)
& c1_1(a354)
& c2_1(a354) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c1_1(X4)
| c2_1(X4)
| c3_1(X4) ) )
| ! [X5] :
( ndr1_0
=> ( c2_1(X5)
| ~ c1_1(X5)
| ~ c3_1(X5) ) ) )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c2_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c1_1(X7)
| ~ c0_1(X7)
| ~ c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( ~ c0_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c2_1(X10)
| ~ c0_1(X10)
| ~ c1_1(X10) ) )
| hskp0 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c2_1(X12)
| c3_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c2_1(X15)
| ~ c1_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c3_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16) ) ) )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c2_1(X18)
| ~ c1_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21) ) )
| hskp1 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c2_1(X23)
| ~ c1_1(X23)
| ~ c3_1(X23) ) )
| hskp0 )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24) ) )
| hskp2
| hskp0 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c2_1(X25)
| c3_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| ~ c1_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27) ) ) )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c3_1(X29)
| ~ c1_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| ~ c1_1(X30)
| ~ c3_1(X30) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c2_1(X31)
| ~ c1_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c3_1(X32)
| ~ c1_1(X32) ) )
| hskp3 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c0_1(X34)
| ~ c2_1(X34) ) )
| hskp4 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c1_1(X36)
| ~ c0_1(X36)
| ~ c3_1(X36) ) )
| hskp5 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c3_1(X38)
| ~ c0_1(X38)
| ~ c1_1(X38) ) )
| hskp6 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39) ) )
| hskp7
| hskp4 )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| ~ c1_1(X40) ) )
| hskp8
| hskp5 )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c2_1(X41)
| ~ c3_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c3_1(X42)
| ~ c0_1(X42)
| ~ c2_1(X42) ) )
| hskp9 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c2_1(X43)
| ~ c3_1(X43) ) )
| hskp10
| hskp11 )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c2_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| hskp12 )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c2_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c3_1(X47)
| ~ c1_1(X47)
| ~ c2_1(X47) ) )
| hskp8 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c2_1(X49)
| c3_1(X49)
| ~ c0_1(X49) ) )
| hskp12 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| ~ c1_1(X50)
| ~ c2_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51) ) )
| hskp13 )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52) ) )
| ! [X53] :
( ndr1_0
=> ( c2_1(X53)
| c3_1(X53)
| ~ c1_1(X53) ) )
| hskp3 )
& ( ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| ~ c2_1(X54)
| ~ c3_1(X54) ) )
| hskp14
| hskp0 )
& ( ! [X55] :
( ndr1_0
=> ( c1_1(X55)
| c2_1(X55)
| ~ c0_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c2_1(X56)
| ~ c1_1(X56)
| ~ c3_1(X56) ) )
| hskp14 )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c2_1(X58)
| ~ c0_1(X58)
| ~ c1_1(X58) ) )
| hskp7 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| ~ c3_1(X59) ) )
| hskp6
| hskp15 )
& ( ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| c2_1(X60)
| ~ c3_1(X60) ) )
| hskp16 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c3_1(X61)
| ~ c0_1(X61) ) )
| ! [X62] :
( ndr1_0
=> ( c1_1(X62)
| c3_1(X62)
| ~ c2_1(X62) ) )
| hskp13 )
& ( ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| c3_1(X63)
| ~ c0_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| c3_1(X64)
| ~ c1_1(X64) ) )
| hskp17 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c3_1(X65)
| ~ c2_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66) ) )
| hskp5 )
& ( ! [X67] :
( ndr1_0
=> ( c1_1(X67)
| c3_1(X67)
| ~ c2_1(X67) ) )
| hskp11
| hskp16 )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| ~ c0_1(X68)
| ~ c2_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c1_1(X69)
| ~ c0_1(X69)
| ~ c3_1(X69) ) )
| hskp4 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| ~ c0_1(X70)
| ~ c2_1(X70) ) )
| hskp17
| hskp18 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71) ) )
| hskp19
| hskp12 )
& ( ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72) ) )
| hskp11
| hskp20 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73) ) )
| hskp27
| hskp3 )
& ( ! [X74] :
( ndr1_0
=> ( c2_1(X74)
| c3_1(X74)
| ~ c0_1(X74) ) )
| hskp21 )
& ( ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( ~ c0_1(X77)
| ~ c1_1(X77)
| ~ c3_1(X77) ) ) )
& ( ! [X78] :
( ndr1_0
=> ( c2_1(X78)
| c3_1(X78)
| ~ c1_1(X78) ) )
| ! [X79] :
( ndr1_0
=> ( ~ c0_1(X79)
| ~ c1_1(X79)
| ~ c3_1(X79) ) )
| hskp17 )
& ( ! [X80] :
( ndr1_0
=> ( c2_1(X80)
| c3_1(X80)
| ~ c1_1(X80) ) )
| hskp22 )
& ( ! [X81] :
( ndr1_0
=> ( c2_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) )
| ! [X82] :
( ndr1_0
=> ( ~ c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82) ) ) )
& ( ! [X83] :
( ndr1_0
=> ( c3_1(X83)
| ~ c0_1(X83)
| ~ c1_1(X83) ) )
| hskp17
| hskp4 )
& ( ! [X84] :
( ndr1_0
=> ( c3_1(X84)
| ~ c0_1(X84)
| ~ c1_1(X84) ) )
| hskp23
| hskp24 )
& ( ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c2_1(X85) ) )
| ! [X86] :
( ndr1_0
=> ( ~ c0_1(X86)
| ~ c2_1(X86)
| ~ c3_1(X86) ) )
| hskp11 )
& ( ! [X87] :
( ndr1_0
=> ( c3_1(X87)
| ~ c1_1(X87)
| ~ c2_1(X87) ) )
| ! [X88] :
( ndr1_0
=> ( ~ c1_1(X88)
| ~ c2_1(X88)
| ~ c3_1(X88) ) )
| hskp4 )
& ( ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c1_1(X89)
| ~ c2_1(X89) ) )
| hskp15
| hskp25 )
& ( ! [X90] :
( ndr1_0
=> ( ~ c0_1(X90)
| ~ c1_1(X90)
| ~ c2_1(X90) ) )
| hskp6
| hskp8 )
& ( ! [X91] :
( ndr1_0
=> ( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c2_1(X91) ) )
| hskp26
| hskp23 )
& ( ! [X92] :
( ndr1_0
=> ( ~ c0_1(X92)
| ~ c1_1(X92)
| ~ c3_1(X92) ) )
| hskp17
| hskp21 )
& ( ! [X93] :
( ndr1_0
=> ( ~ c1_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93) ) )
| hskp28 )
& ( hskp29
| hskp27
| hskp10 )
& ( hskp7
| hskp1
| hskp10 )
& ( hskp17
| hskp5
| hskp24 )
& ( hskp6
| hskp15
| hskp23 )
& ( hskp26
| hskp11
| hskp12 )
& ( hskp26
| hskp16 )
& ( hskp20
| hskp12
| hskp25 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
fof(f2,negated_conjecture,
~ ~ ( ( ~ hskp0
| ( ndr1_0
& ~ c0_1(a294)
& ~ c2_1(a294)
& ~ c3_1(a294) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a295)
& c2_1(a295)
& ~ c1_1(a295) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a297)
& ~ c0_1(a297)
& ~ c3_1(a297) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a299)
& c3_1(a299)
& ~ c2_1(a299) ) )
& ( ~ hskp4
| ( ndr1_0
& ~ c0_1(a300)
& ~ c1_1(a300)
& ~ c2_1(a300) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a301)
& ~ c1_1(a301)
& ~ c3_1(a301) ) )
& ( ~ hskp6
| ( ndr1_0
& c0_1(a302)
& ~ c1_1(a302)
& ~ c2_1(a302) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a303)
& c1_1(a303)
& ~ c2_1(a303) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a305)
& ~ c0_1(a305)
& ~ c1_1(a305) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a307)
& ~ c1_1(a307)
& ~ c3_1(a307) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a308)
& c3_1(a308)
& ~ c0_1(a308) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a309)
& c3_1(a309)
& ~ c2_1(a309) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a310)
& ~ c0_1(a310)
& ~ c2_1(a310) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a313)
& c3_1(a313)
& ~ c1_1(a313) ) )
& ( ~ hskp14
| ( ndr1_0
& c1_1(a315)
& c2_1(a315)
& ~ c0_1(a315) ) )
& ( ~ hskp15
| ( ndr1_0
& c1_1(a320)
& ~ c0_1(a320)
& ~ c2_1(a320) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a321)
& c3_1(a321)
& ~ c1_1(a321) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a323)
& c2_1(a323)
& ~ c3_1(a323) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a329)
& ~ c0_1(a329)
& ~ c3_1(a329) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a330)
& c2_1(a330)
& ~ c3_1(a330) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a333)
& ~ c2_1(a333)
& ~ c3_1(a333) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a336)
& ~ c0_1(a336)
& ~ c1_1(a336) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c1_1(a338)
& ~ c2_1(a338)
& ~ c3_1(a338) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a341)
& c3_1(a341)
& ~ c0_1(a341) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a342)
& ~ c1_1(a342)
& ~ c2_1(a342) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c0_1(a346)
& ~ c1_1(a346)
& ~ c3_1(a346) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a349)
& ~ c2_1(a349)
& ~ c3_1(a349) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a334)
& c2_1(a334)
& c3_1(a334) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a353)
& c2_1(a353)
& c3_1(a353) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a354)
& c1_1(a354)
& c2_1(a354) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c1_1(X4)
| c2_1(X4)
| c3_1(X4) ) )
| ! [X5] :
( ndr1_0
=> ( c2_1(X5)
| ~ c1_1(X5)
| ~ c3_1(X5) ) ) )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c2_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c1_1(X7)
| ~ c0_1(X7)
| ~ c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( ~ c0_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c2_1(X10)
| ~ c0_1(X10)
| ~ c1_1(X10) ) )
| hskp0 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c2_1(X12)
| c3_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c2_1(X15)
| ~ c1_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c3_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16) ) ) )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c2_1(X18)
| ~ c1_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21) ) )
| hskp1 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c2_1(X23)
| ~ c1_1(X23)
| ~ c3_1(X23) ) )
| hskp0 )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24) ) )
| hskp2
| hskp0 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c2_1(X25)
| c3_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| ~ c1_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27) ) ) )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c3_1(X29)
| ~ c1_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| ~ c1_1(X30)
| ~ c3_1(X30) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c2_1(X31)
| ~ c1_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c3_1(X32)
| ~ c1_1(X32) ) )
| hskp3 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c0_1(X34)
| ~ c2_1(X34) ) )
| hskp4 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c1_1(X36)
| ~ c0_1(X36)
| ~ c3_1(X36) ) )
| hskp5 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c3_1(X38)
| ~ c0_1(X38)
| ~ c1_1(X38) ) )
| hskp6 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39) ) )
| hskp7
| hskp4 )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| ~ c1_1(X40) ) )
| hskp8
| hskp5 )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c2_1(X41)
| ~ c3_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c3_1(X42)
| ~ c0_1(X42)
| ~ c2_1(X42) ) )
| hskp9 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c2_1(X43)
| ~ c3_1(X43) ) )
| hskp10
| hskp11 )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c2_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| hskp12 )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c2_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c3_1(X47)
| ~ c1_1(X47)
| ~ c2_1(X47) ) )
| hskp8 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c2_1(X49)
| c3_1(X49)
| ~ c0_1(X49) ) )
| hskp12 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| ~ c1_1(X50)
| ~ c2_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51) ) )
| hskp13 )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52) ) )
| ! [X53] :
( ndr1_0
=> ( c2_1(X53)
| c3_1(X53)
| ~ c1_1(X53) ) )
| hskp3 )
& ( ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| ~ c2_1(X54)
| ~ c3_1(X54) ) )
| hskp14
| hskp0 )
& ( ! [X55] :
( ndr1_0
=> ( c1_1(X55)
| c2_1(X55)
| ~ c0_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c2_1(X56)
| ~ c1_1(X56)
| ~ c3_1(X56) ) )
| hskp14 )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c2_1(X58)
| ~ c0_1(X58)
| ~ c1_1(X58) ) )
| hskp7 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| ~ c3_1(X59) ) )
| hskp6
| hskp15 )
& ( ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| c2_1(X60)
| ~ c3_1(X60) ) )
| hskp16 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c3_1(X61)
| ~ c0_1(X61) ) )
| ! [X62] :
( ndr1_0
=> ( c1_1(X62)
| c3_1(X62)
| ~ c2_1(X62) ) )
| hskp13 )
& ( ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| c3_1(X63)
| ~ c0_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| c3_1(X64)
| ~ c1_1(X64) ) )
| hskp17 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c3_1(X65)
| ~ c2_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66) ) )
| hskp5 )
& ( ! [X67] :
( ndr1_0
=> ( c1_1(X67)
| c3_1(X67)
| ~ c2_1(X67) ) )
| hskp11
| hskp16 )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| ~ c0_1(X68)
| ~ c2_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c1_1(X69)
| ~ c0_1(X69)
| ~ c3_1(X69) ) )
| hskp4 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| ~ c0_1(X70)
| ~ c2_1(X70) ) )
| hskp17
| hskp18 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71) ) )
| hskp19
| hskp12 )
& ( ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72) ) )
| hskp11
| hskp20 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73) ) )
| hskp27
| hskp3 )
& ( ! [X74] :
( ndr1_0
=> ( c2_1(X74)
| c3_1(X74)
| ~ c0_1(X74) ) )
| hskp21 )
& ( ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( ~ c0_1(X77)
| ~ c1_1(X77)
| ~ c3_1(X77) ) ) )
& ( ! [X78] :
( ndr1_0
=> ( c2_1(X78)
| c3_1(X78)
| ~ c1_1(X78) ) )
| ! [X79] :
( ndr1_0
=> ( ~ c0_1(X79)
| ~ c1_1(X79)
| ~ c3_1(X79) ) )
| hskp17 )
& ( ! [X80] :
( ndr1_0
=> ( c2_1(X80)
| c3_1(X80)
| ~ c1_1(X80) ) )
| hskp22 )
& ( ! [X81] :
( ndr1_0
=> ( c2_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) )
| ! [X82] :
( ndr1_0
=> ( ~ c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82) ) ) )
& ( ! [X83] :
( ndr1_0
=> ( c3_1(X83)
| ~ c0_1(X83)
| ~ c1_1(X83) ) )
| hskp17
| hskp4 )
& ( ! [X84] :
( ndr1_0
=> ( c3_1(X84)
| ~ c0_1(X84)
| ~ c1_1(X84) ) )
| hskp23
| hskp24 )
& ( ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c2_1(X85) ) )
| ! [X86] :
( ndr1_0
=> ( ~ c0_1(X86)
| ~ c2_1(X86)
| ~ c3_1(X86) ) )
| hskp11 )
& ( ! [X87] :
( ndr1_0
=> ( c3_1(X87)
| ~ c1_1(X87)
| ~ c2_1(X87) ) )
| ! [X88] :
( ndr1_0
=> ( ~ c1_1(X88)
| ~ c2_1(X88)
| ~ c3_1(X88) ) )
| hskp4 )
& ( ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c1_1(X89)
| ~ c2_1(X89) ) )
| hskp15
| hskp25 )
& ( ! [X90] :
( ndr1_0
=> ( ~ c0_1(X90)
| ~ c1_1(X90)
| ~ c2_1(X90) ) )
| hskp6
| hskp8 )
& ( ! [X91] :
( ndr1_0
=> ( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c2_1(X91) ) )
| hskp26
| hskp23 )
& ( ! [X92] :
( ndr1_0
=> ( ~ c0_1(X92)
| ~ c1_1(X92)
| ~ c3_1(X92) ) )
| hskp17
| hskp21 )
& ( ! [X93] :
( ndr1_0
=> ( ~ c1_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93) ) )
| hskp28 )
& ( hskp29
| hskp27
| hskp10 )
& ( hskp7
| hskp1
| hskp10 )
& ( hskp17
| hskp5
| hskp24 )
& ( hskp6
| hskp15
| hskp23 )
& ( hskp26
| hskp11
| hskp12 )
& ( hskp26
| hskp16 )
& ( hskp20
| hskp12
| hskp25 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( ~ hskp0
| ( ndr1_0
& ~ c0_1(a294)
& ~ c2_1(a294)
& ~ c3_1(a294) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a295)
& c2_1(a295)
& ~ c1_1(a295) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a297)
& ~ c0_1(a297)
& ~ c3_1(a297) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a299)
& c3_1(a299)
& ~ c2_1(a299) ) )
& ( ~ hskp4
| ( ndr1_0
& ~ c0_1(a300)
& ~ c1_1(a300)
& ~ c2_1(a300) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a301)
& ~ c1_1(a301)
& ~ c3_1(a301) ) )
& ( ~ hskp6
| ( ndr1_0
& c0_1(a302)
& ~ c1_1(a302)
& ~ c2_1(a302) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a303)
& c1_1(a303)
& ~ c2_1(a303) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a305)
& ~ c0_1(a305)
& ~ c1_1(a305) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a307)
& ~ c1_1(a307)
& ~ c3_1(a307) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a308)
& c3_1(a308)
& ~ c0_1(a308) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a309)
& c3_1(a309)
& ~ c2_1(a309) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a310)
& ~ c0_1(a310)
& ~ c2_1(a310) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a313)
& c3_1(a313)
& ~ c1_1(a313) ) )
& ( ~ hskp14
| ( ndr1_0
& c1_1(a315)
& c2_1(a315)
& ~ c0_1(a315) ) )
& ( ~ hskp15
| ( ndr1_0
& c1_1(a320)
& ~ c0_1(a320)
& ~ c2_1(a320) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a321)
& c3_1(a321)
& ~ c1_1(a321) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a323)
& c2_1(a323)
& ~ c3_1(a323) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a329)
& ~ c0_1(a329)
& ~ c3_1(a329) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a330)
& c2_1(a330)
& ~ c3_1(a330) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a333)
& ~ c2_1(a333)
& ~ c3_1(a333) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a336)
& ~ c0_1(a336)
& ~ c1_1(a336) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c1_1(a338)
& ~ c2_1(a338)
& ~ c3_1(a338) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a341)
& c3_1(a341)
& ~ c0_1(a341) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a342)
& ~ c1_1(a342)
& ~ c2_1(a342) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c0_1(a346)
& ~ c1_1(a346)
& ~ c3_1(a346) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a349)
& ~ c2_1(a349)
& ~ c3_1(a349) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a334)
& c2_1(a334)
& c3_1(a334) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a353)
& c2_1(a353)
& c3_1(a353) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a354)
& c1_1(a354)
& c2_1(a354) ) )
& ( ! [X0] :
( ndr1_0
=> ( c0_1(X0)
| c1_1(X0)
| c2_1(X0) ) )
| ! [X1] :
( ndr1_0
=> ( c0_1(X1)
| c2_1(X1)
| c3_1(X1) ) )
| ! [X2] :
( ndr1_0
=> ( c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ) ) )
& ( ! [X3] :
( ndr1_0
=> ( c0_1(X3)
| c1_1(X3)
| c2_1(X3) ) )
| ! [X4] :
( ndr1_0
=> ( c1_1(X4)
| c2_1(X4)
| c3_1(X4) ) )
| ! [X5] :
( ndr1_0
=> ( c2_1(X5)
| ~ c1_1(X5)
| ~ c3_1(X5) ) ) )
& ( ! [X6] :
( ndr1_0
=> ( c0_1(X6)
| c1_1(X6)
| c2_1(X6) ) )
| ! [X7] :
( ndr1_0
=> ( c1_1(X7)
| ~ c0_1(X7)
| ~ c2_1(X7) ) )
| ! [X8] :
( ndr1_0
=> ( ~ c0_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8) ) ) )
& ( ! [X9] :
( ndr1_0
=> ( c0_1(X9)
| c1_1(X9)
| c2_1(X9) ) )
| ! [X10] :
( ndr1_0
=> ( c2_1(X10)
| ~ c0_1(X10)
| ~ c1_1(X10) ) )
| hskp0 )
& ( ! [X11] :
( ndr1_0
=> ( c0_1(X11)
| c1_1(X11)
| c3_1(X11) ) )
| ! [X12] :
( ndr1_0
=> ( c0_1(X12)
| c2_1(X12)
| c3_1(X12) ) )
| ! [X13] :
( ndr1_0
=> ( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13) ) ) )
& ( ! [X14] :
( ndr1_0
=> ( c0_1(X14)
| c1_1(X14)
| c3_1(X14) ) )
| ! [X15] :
( ndr1_0
=> ( c0_1(X15)
| c2_1(X15)
| ~ c1_1(X15) ) )
| ! [X16] :
( ndr1_0
=> ( c3_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16) ) ) )
& ( ! [X17] :
( ndr1_0
=> ( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17) ) )
| ! [X18] :
( ndr1_0
=> ( c0_1(X18)
| c2_1(X18)
| ~ c1_1(X18) ) )
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19) ) ) )
& ( ! [X20] :
( ndr1_0
=> ( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20) ) )
| ! [X21] :
( ndr1_0
=> ( c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21) ) )
| hskp1 )
& ( ! [X22] :
( ndr1_0
=> ( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22) ) )
| ! [X23] :
( ndr1_0
=> ( c2_1(X23)
| ~ c1_1(X23)
| ~ c3_1(X23) ) )
| hskp0 )
& ( ! [X24] :
( ndr1_0
=> ( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24) ) )
| hskp2
| hskp0 )
& ( ! [X25] :
( ndr1_0
=> ( c0_1(X25)
| c2_1(X25)
| c3_1(X25) ) )
| ! [X26] :
( ndr1_0
=> ( c0_1(X26)
| c2_1(X26)
| ~ c1_1(X26) ) )
| ! [X27] :
( ndr1_0
=> ( c1_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27) ) ) )
& ( ! [X28] :
( ndr1_0
=> ( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X29] :
( ndr1_0
=> ( c0_1(X29)
| c3_1(X29)
| ~ c1_1(X29) ) )
| ! [X30] :
( ndr1_0
=> ( c0_1(X30)
| ~ c1_1(X30)
| ~ c3_1(X30) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( c0_1(X31)
| c2_1(X31)
| ~ c1_1(X31) ) )
| ! [X32] :
( ndr1_0
=> ( c0_1(X32)
| c3_1(X32)
| ~ c1_1(X32) ) )
| hskp3 )
& ( ! [X33] :
( ndr1_0
=> ( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33) ) )
| ! [X34] :
( ndr1_0
=> ( c1_1(X34)
| ~ c0_1(X34)
| ~ c2_1(X34) ) )
| hskp4 )
& ( ! [X35] :
( ndr1_0
=> ( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35) ) )
| ! [X36] :
( ndr1_0
=> ( c1_1(X36)
| ~ c0_1(X36)
| ~ c3_1(X36) ) )
| hskp5 )
& ( ! [X37] :
( ndr1_0
=> ( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37) ) )
| ! [X38] :
( ndr1_0
=> ( c3_1(X38)
| ~ c0_1(X38)
| ~ c1_1(X38) ) )
| hskp6 )
& ( ! [X39] :
( ndr1_0
=> ( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39) ) )
| hskp7
| hskp4 )
& ( ! [X40] :
( ndr1_0
=> ( c0_1(X40)
| c2_1(X40)
| ~ c1_1(X40) ) )
| hskp8
| hskp5 )
& ( ! [X41] :
( ndr1_0
=> ( c0_1(X41)
| c2_1(X41)
| ~ c3_1(X41) ) )
| ! [X42] :
( ndr1_0
=> ( c3_1(X42)
| ~ c0_1(X42)
| ~ c2_1(X42) ) )
| hskp9 )
& ( ! [X43] :
( ndr1_0
=> ( c0_1(X43)
| c2_1(X43)
| ~ c3_1(X43) ) )
| hskp10
| hskp11 )
& ( ! [X44] :
( ndr1_0
=> ( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44) ) )
| ! [X45] :
( ndr1_0
=> ( c2_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45) ) )
| hskp12 )
& ( ! [X46] :
( ndr1_0
=> ( c0_1(X46)
| c3_1(X46)
| ~ c2_1(X46) ) )
| ! [X47] :
( ndr1_0
=> ( c3_1(X47)
| ~ c1_1(X47)
| ~ c2_1(X47) ) )
| hskp8 )
& ( ! [X48] :
( ndr1_0
=> ( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48) ) )
| ! [X49] :
( ndr1_0
=> ( c2_1(X49)
| c3_1(X49)
| ~ c0_1(X49) ) )
| hskp12 )
& ( ! [X50] :
( ndr1_0
=> ( c0_1(X50)
| ~ c1_1(X50)
| ~ c2_1(X50) ) )
| ! [X51] :
( ndr1_0
=> ( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51) ) )
| hskp13 )
& ( ! [X52] :
( ndr1_0
=> ( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52) ) )
| ! [X53] :
( ndr1_0
=> ( c2_1(X53)
| c3_1(X53)
| ~ c1_1(X53) ) )
| hskp3 )
& ( ! [X54] :
( ndr1_0
=> ( c0_1(X54)
| ~ c2_1(X54)
| ~ c3_1(X54) ) )
| hskp14
| hskp0 )
& ( ! [X55] :
( ndr1_0
=> ( c1_1(X55)
| c2_1(X55)
| ~ c0_1(X55) ) )
| ! [X56] :
( ndr1_0
=> ( c2_1(X56)
| ~ c1_1(X56)
| ~ c3_1(X56) ) )
| hskp14 )
& ( ! [X57] :
( ndr1_0
=> ( c1_1(X57)
| c2_1(X57)
| ~ c3_1(X57) ) )
| ! [X58] :
( ndr1_0
=> ( c2_1(X58)
| ~ c0_1(X58)
| ~ c1_1(X58) ) )
| hskp7 )
& ( ! [X59] :
( ndr1_0
=> ( c1_1(X59)
| c2_1(X59)
| ~ c3_1(X59) ) )
| hskp6
| hskp15 )
& ( ! [X60] :
( ndr1_0
=> ( c1_1(X60)
| c2_1(X60)
| ~ c3_1(X60) ) )
| hskp16 )
& ( ! [X61] :
( ndr1_0
=> ( c1_1(X61)
| c3_1(X61)
| ~ c0_1(X61) ) )
| ! [X62] :
( ndr1_0
=> ( c1_1(X62)
| c3_1(X62)
| ~ c2_1(X62) ) )
| hskp13 )
& ( ! [X63] :
( ndr1_0
=> ( c1_1(X63)
| c3_1(X63)
| ~ c0_1(X63) ) )
| ! [X64] :
( ndr1_0
=> ( c2_1(X64)
| c3_1(X64)
| ~ c1_1(X64) ) )
| hskp17 )
& ( ! [X65] :
( ndr1_0
=> ( c1_1(X65)
| c3_1(X65)
| ~ c2_1(X65) ) )
| ! [X66] :
( ndr1_0
=> ( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66) ) )
| hskp5 )
& ( ! [X67] :
( ndr1_0
=> ( c1_1(X67)
| c3_1(X67)
| ~ c2_1(X67) ) )
| hskp11
| hskp16 )
& ( ! [X68] :
( ndr1_0
=> ( c1_1(X68)
| ~ c0_1(X68)
| ~ c2_1(X68) ) )
| ! [X69] :
( ndr1_0
=> ( c1_1(X69)
| ~ c0_1(X69)
| ~ c3_1(X69) ) )
| hskp4 )
& ( ! [X70] :
( ndr1_0
=> ( c1_1(X70)
| ~ c0_1(X70)
| ~ c2_1(X70) ) )
| hskp17
| hskp18 )
& ( ! [X71] :
( ndr1_0
=> ( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71) ) )
| hskp19
| hskp12 )
& ( ! [X72] :
( ndr1_0
=> ( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72) ) )
| hskp11
| hskp20 )
& ( ! [X73] :
( ndr1_0
=> ( c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73) ) )
| hskp27
| hskp3 )
& ( ! [X74] :
( ndr1_0
=> ( c2_1(X74)
| c3_1(X74)
| ~ c0_1(X74) ) )
| hskp21 )
& ( ! [X75] :
( ndr1_0
=> ( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75) ) )
| ! [X76] :
( ndr1_0
=> ( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76) ) )
| ! [X77] :
( ndr1_0
=> ( ~ c0_1(X77)
| ~ c1_1(X77)
| ~ c3_1(X77) ) ) )
& ( ! [X78] :
( ndr1_0
=> ( c2_1(X78)
| c3_1(X78)
| ~ c1_1(X78) ) )
| ! [X79] :
( ndr1_0
=> ( ~ c0_1(X79)
| ~ c1_1(X79)
| ~ c3_1(X79) ) )
| hskp17 )
& ( ! [X80] :
( ndr1_0
=> ( c2_1(X80)
| c3_1(X80)
| ~ c1_1(X80) ) )
| hskp22 )
& ( ! [X81] :
( ndr1_0
=> ( c2_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81) ) )
| ! [X82] :
( ndr1_0
=> ( ~ c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82) ) ) )
& ( ! [X83] :
( ndr1_0
=> ( c3_1(X83)
| ~ c0_1(X83)
| ~ c1_1(X83) ) )
| hskp17
| hskp4 )
& ( ! [X84] :
( ndr1_0
=> ( c3_1(X84)
| ~ c0_1(X84)
| ~ c1_1(X84) ) )
| hskp23
| hskp24 )
& ( ! [X85] :
( ndr1_0
=> ( c3_1(X85)
| ~ c0_1(X85)
| ~ c2_1(X85) ) )
| ! [X86] :
( ndr1_0
=> ( ~ c0_1(X86)
| ~ c2_1(X86)
| ~ c3_1(X86) ) )
| hskp11 )
& ( ! [X87] :
( ndr1_0
=> ( c3_1(X87)
| ~ c1_1(X87)
| ~ c2_1(X87) ) )
| ! [X88] :
( ndr1_0
=> ( ~ c1_1(X88)
| ~ c2_1(X88)
| ~ c3_1(X88) ) )
| hskp4 )
& ( ! [X89] :
( ndr1_0
=> ( c3_1(X89)
| ~ c1_1(X89)
| ~ c2_1(X89) ) )
| hskp15
| hskp25 )
& ( ! [X90] :
( ndr1_0
=> ( ~ c0_1(X90)
| ~ c1_1(X90)
| ~ c2_1(X90) ) )
| hskp6
| hskp8 )
& ( ! [X91] :
( ndr1_0
=> ( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c2_1(X91) ) )
| hskp26
| hskp23 )
& ( ! [X92] :
( ndr1_0
=> ( ~ c0_1(X92)
| ~ c1_1(X92)
| ~ c3_1(X92) ) )
| hskp17
| hskp21 )
& ( ! [X93] :
( ndr1_0
=> ( ~ c1_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93) ) )
| hskp28 )
& ( hskp29
| hskp27
| hskp10 )
& ( hskp7
| hskp1
| hskp10 )
& ( hskp17
| hskp5
| hskp24 )
& ( hskp6
| hskp15
| hskp23 )
& ( hskp26
| hskp11
| hskp12 )
& ( hskp26
| hskp16 )
& ( hskp20
| hskp12
| hskp25 ) ),
inference(flattening,[],[f2]) ).
fof(f4,plain,
( ( ~ hskp0
| ( ndr1_0
& ~ c0_1(a294)
& ~ c2_1(a294)
& ~ c3_1(a294) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a295)
& c2_1(a295)
& ~ c1_1(a295) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a297)
& ~ c0_1(a297)
& ~ c3_1(a297) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a299)
& c3_1(a299)
& ~ c2_1(a299) ) )
& ( ~ hskp4
| ( ndr1_0
& ~ c0_1(a300)
& ~ c1_1(a300)
& ~ c2_1(a300) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a301)
& ~ c1_1(a301)
& ~ c3_1(a301) ) )
& ( ~ hskp6
| ( ndr1_0
& c0_1(a302)
& ~ c1_1(a302)
& ~ c2_1(a302) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a303)
& c1_1(a303)
& ~ c2_1(a303) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a305)
& ~ c0_1(a305)
& ~ c1_1(a305) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a307)
& ~ c1_1(a307)
& ~ c3_1(a307) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a308)
& c3_1(a308)
& ~ c0_1(a308) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a309)
& c3_1(a309)
& ~ c2_1(a309) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a310)
& ~ c0_1(a310)
& ~ c2_1(a310) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a313)
& c3_1(a313)
& ~ c1_1(a313) ) )
& ( ~ hskp14
| ( ndr1_0
& c1_1(a315)
& c2_1(a315)
& ~ c0_1(a315) ) )
& ( ~ hskp15
| ( ndr1_0
& c1_1(a320)
& ~ c0_1(a320)
& ~ c2_1(a320) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a321)
& c3_1(a321)
& ~ c1_1(a321) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a323)
& c2_1(a323)
& ~ c3_1(a323) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a329)
& ~ c0_1(a329)
& ~ c3_1(a329) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a330)
& c2_1(a330)
& ~ c3_1(a330) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a333)
& ~ c2_1(a333)
& ~ c3_1(a333) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a336)
& ~ c0_1(a336)
& ~ c1_1(a336) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c1_1(a338)
& ~ c2_1(a338)
& ~ c3_1(a338) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a341)
& c3_1(a341)
& ~ c0_1(a341) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a342)
& ~ c1_1(a342)
& ~ c2_1(a342) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c0_1(a346)
& ~ c1_1(a346)
& ~ c3_1(a346) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a349)
& ~ c2_1(a349)
& ~ c3_1(a349) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a334)
& c2_1(a334)
& c3_1(a334) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a353)
& c2_1(a353)
& c3_1(a353) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a354)
& c1_1(a354)
& c2_1(a354) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c1_1(X4)
| c2_1(X4)
| c3_1(X4)
| ~ ndr1_0 )
| ! [X5] :
( c2_1(X5)
| ~ c1_1(X5)
| ~ c3_1(X5)
| ~ ndr1_0 ) )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c2_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c1_1(X7)
| ~ c0_1(X7)
| ~ c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( ~ c0_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c2_1(X10)
| ~ c0_1(X10)
| ~ c1_1(X10)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| c3_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c0_1(X12)
| c2_1(X12)
| c3_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0 ) )
& ( ! [X14] :
( c0_1(X14)
| c1_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| ! [X15] :
( c0_1(X15)
| c2_1(X15)
| ~ c1_1(X15)
| ~ ndr1_0 )
| ! [X16] :
( c3_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 ) )
& ( ! [X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0 )
| ! [X18] :
( c0_1(X18)
| c2_1(X18)
| ~ c1_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 ) )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0 )
| ! [X23] :
( c2_1(X23)
| ~ c1_1(X23)
| ~ c3_1(X23)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X24] :
( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| hskp2
| hskp0 )
& ( ! [X25] :
( c0_1(X25)
| c2_1(X25)
| c3_1(X25)
| ~ ndr1_0 )
| ! [X26] :
( c0_1(X26)
| c2_1(X26)
| ~ c1_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c1_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 ) )
& ( ! [X28] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( c0_1(X29)
| c3_1(X29)
| ~ c1_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( c0_1(X30)
| ~ c1_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 ) )
& ( ! [X31] :
( c0_1(X31)
| c2_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0 )
| ! [X32] :
( c0_1(X32)
| c3_1(X32)
| ~ c1_1(X32)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X33] :
( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| ~ c0_1(X34)
| ~ c2_1(X34)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c1_1(X36)
| ~ c0_1(X36)
| ~ c3_1(X36)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c3_1(X38)
| ~ c0_1(X38)
| ~ c1_1(X38)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X39] :
( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39)
| ~ ndr1_0 )
| hskp7
| hskp4 )
& ( ! [X40] :
( c0_1(X40)
| c2_1(X40)
| ~ c1_1(X40)
| ~ ndr1_0 )
| hskp8
| hskp5 )
& ( ! [X41] :
( c0_1(X41)
| c2_1(X41)
| ~ c3_1(X41)
| ~ ndr1_0 )
| ! [X42] :
( c3_1(X42)
| ~ c0_1(X42)
| ~ c2_1(X42)
| ~ ndr1_0 )
| hskp9 )
& ( ! [X43] :
( c0_1(X43)
| c2_1(X43)
| ~ c3_1(X43)
| ~ ndr1_0 )
| hskp10
| hskp11 )
& ( ! [X44] :
( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( c2_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X46] :
( c0_1(X46)
| c3_1(X46)
| ~ c2_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c3_1(X47)
| ~ c1_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X48] :
( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0 )
| ! [X49] :
( c2_1(X49)
| c3_1(X49)
| ~ c0_1(X49)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X50] :
( c0_1(X50)
| ~ c1_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X52] :
( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| ! [X53] :
( c2_1(X53)
| c3_1(X53)
| ~ c1_1(X53)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X54] :
( c0_1(X54)
| ~ c2_1(X54)
| ~ c3_1(X54)
| ~ ndr1_0 )
| hskp14
| hskp0 )
& ( ! [X55] :
( c1_1(X55)
| c2_1(X55)
| ~ c0_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( c2_1(X56)
| ~ c1_1(X56)
| ~ c3_1(X56)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X57] :
( c1_1(X57)
| c2_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c2_1(X58)
| ~ c0_1(X58)
| ~ c1_1(X58)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X59] :
( c1_1(X59)
| c2_1(X59)
| ~ c3_1(X59)
| ~ ndr1_0 )
| hskp6
| hskp15 )
& ( ! [X60] :
( c1_1(X60)
| c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X61] :
( c1_1(X61)
| c3_1(X61)
| ~ c0_1(X61)
| ~ ndr1_0 )
| ! [X62] :
( c1_1(X62)
| c3_1(X62)
| ~ c2_1(X62)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X63] :
( c1_1(X63)
| c3_1(X63)
| ~ c0_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c2_1(X64)
| c3_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X65] :
( c1_1(X65)
| c3_1(X65)
| ~ c2_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X67] :
( c1_1(X67)
| c3_1(X67)
| ~ c2_1(X67)
| ~ ndr1_0 )
| hskp11
| hskp16 )
& ( ! [X68] :
( c1_1(X68)
| ~ c0_1(X68)
| ~ c2_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c1_1(X69)
| ~ c0_1(X69)
| ~ c3_1(X69)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X70] :
( c1_1(X70)
| ~ c0_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0 )
| hskp17
| hskp18 )
& ( ! [X71] :
( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 )
| hskp19
| hskp12 )
& ( ! [X72] :
( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| hskp11
| hskp20 )
& ( ! [X73] :
( c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73)
| ~ ndr1_0 )
| hskp27
| hskp3 )
& ( ! [X74] :
( c2_1(X74)
| c3_1(X74)
| ~ c0_1(X74)
| ~ ndr1_0 )
| hskp21 )
& ( ! [X75] :
( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 )
| ! [X77] :
( ~ c0_1(X77)
| ~ c1_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0 ) )
& ( ! [X78] :
( c2_1(X78)
| c3_1(X78)
| ~ c1_1(X78)
| ~ ndr1_0 )
| ! [X79] :
( ~ c0_1(X79)
| ~ c1_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X80] :
( c2_1(X80)
| c3_1(X80)
| ~ c1_1(X80)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X81] :
( c2_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 )
| ! [X82] :
( ~ c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 ) )
& ( ! [X83] :
( c3_1(X83)
| ~ c0_1(X83)
| ~ c1_1(X83)
| ~ ndr1_0 )
| hskp17
| hskp4 )
& ( ! [X84] :
( c3_1(X84)
| ~ c0_1(X84)
| ~ c1_1(X84)
| ~ ndr1_0 )
| hskp23
| hskp24 )
& ( ! [X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c2_1(X85)
| ~ ndr1_0 )
| ! [X86] :
( ~ c0_1(X86)
| ~ c2_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X87] :
( c3_1(X87)
| ~ c1_1(X87)
| ~ c2_1(X87)
| ~ ndr1_0 )
| ! [X88] :
( ~ c1_1(X88)
| ~ c2_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X89] :
( c3_1(X89)
| ~ c1_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0 )
| hskp15
| hskp25 )
& ( ! [X90] :
( ~ c0_1(X90)
| ~ c1_1(X90)
| ~ c2_1(X90)
| ~ ndr1_0 )
| hskp6
| hskp8 )
& ( ! [X91] :
( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c2_1(X91)
| ~ ndr1_0 )
| hskp26
| hskp23 )
& ( ! [X92] :
( ~ c0_1(X92)
| ~ c1_1(X92)
| ~ c3_1(X92)
| ~ ndr1_0 )
| hskp17
| hskp21 )
& ( ! [X93] :
( ~ c1_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93)
| ~ ndr1_0 )
| hskp28 )
& ( hskp29
| hskp27
| hskp10 )
& ( hskp7
| hskp1
| hskp10 )
& ( hskp17
| hskp5
| hskp24 )
& ( hskp6
| hskp15
| hskp23 )
& ( hskp26
| hskp11
| hskp12 )
& ( hskp26
| hskp16 )
& ( hskp20
| hskp12
| hskp25 ) ),
inference(ennf_transformation,[],[f3]) ).
fof(f5,plain,
( ( ~ hskp0
| ( ndr1_0
& ~ c0_1(a294)
& ~ c2_1(a294)
& ~ c3_1(a294) ) )
& ( ~ hskp1
| ( ndr1_0
& c0_1(a295)
& c2_1(a295)
& ~ c1_1(a295) ) )
& ( ~ hskp2
| ( ndr1_0
& c1_1(a297)
& ~ c0_1(a297)
& ~ c3_1(a297) ) )
& ( ~ hskp3
| ( ndr1_0
& c0_1(a299)
& c3_1(a299)
& ~ c2_1(a299) ) )
& ( ~ hskp4
| ( ndr1_0
& ~ c0_1(a300)
& ~ c1_1(a300)
& ~ c2_1(a300) ) )
& ( ~ hskp5
| ( ndr1_0
& c2_1(a301)
& ~ c1_1(a301)
& ~ c3_1(a301) ) )
& ( ~ hskp6
| ( ndr1_0
& c0_1(a302)
& ~ c1_1(a302)
& ~ c2_1(a302) ) )
& ( ~ hskp7
| ( ndr1_0
& c0_1(a303)
& c1_1(a303)
& ~ c2_1(a303) ) )
& ( ~ hskp8
| ( ndr1_0
& c2_1(a305)
& ~ c0_1(a305)
& ~ c1_1(a305) ) )
& ( ~ hskp9
| ( ndr1_0
& c0_1(a307)
& ~ c1_1(a307)
& ~ c3_1(a307) ) )
& ( ~ hskp10
| ( ndr1_0
& c1_1(a308)
& c3_1(a308)
& ~ c0_1(a308) ) )
& ( ~ hskp11
| ( ndr1_0
& c1_1(a309)
& c3_1(a309)
& ~ c2_1(a309) ) )
& ( ~ hskp12
| ( ndr1_0
& c3_1(a310)
& ~ c0_1(a310)
& ~ c2_1(a310) ) )
& ( ~ hskp13
| ( ndr1_0
& c0_1(a313)
& c3_1(a313)
& ~ c1_1(a313) ) )
& ( ~ hskp14
| ( ndr1_0
& c1_1(a315)
& c2_1(a315)
& ~ c0_1(a315) ) )
& ( ~ hskp15
| ( ndr1_0
& c1_1(a320)
& ~ c0_1(a320)
& ~ c2_1(a320) ) )
& ( ~ hskp16
| ( ndr1_0
& c2_1(a321)
& c3_1(a321)
& ~ c1_1(a321) ) )
& ( ~ hskp17
| ( ndr1_0
& c0_1(a323)
& c2_1(a323)
& ~ c3_1(a323) ) )
& ( ~ hskp18
| ( ndr1_0
& c2_1(a329)
& ~ c0_1(a329)
& ~ c3_1(a329) ) )
& ( ~ hskp19
| ( ndr1_0
& c1_1(a330)
& c2_1(a330)
& ~ c3_1(a330) ) )
& ( ~ hskp20
| ( ndr1_0
& c1_1(a333)
& ~ c2_1(a333)
& ~ c3_1(a333) ) )
& ( ~ hskp21
| ( ndr1_0
& c3_1(a336)
& ~ c0_1(a336)
& ~ c1_1(a336) ) )
& ( ~ hskp22
| ( ndr1_0
& ~ c1_1(a338)
& ~ c2_1(a338)
& ~ c3_1(a338) ) )
& ( ~ hskp23
| ( ndr1_0
& c2_1(a341)
& c3_1(a341)
& ~ c0_1(a341) ) )
& ( ~ hskp24
| ( ndr1_0
& c3_1(a342)
& ~ c1_1(a342)
& ~ c2_1(a342) ) )
& ( ~ hskp25
| ( ndr1_0
& ~ c0_1(a346)
& ~ c1_1(a346)
& ~ c3_1(a346) ) )
& ( ~ hskp26
| ( ndr1_0
& c0_1(a349)
& ~ c2_1(a349)
& ~ c3_1(a349) ) )
& ( ~ hskp27
| ( ndr1_0
& c0_1(a334)
& c2_1(a334)
& c3_1(a334) ) )
& ( ~ hskp28
| ( ndr1_0
& c1_1(a353)
& c2_1(a353)
& c3_1(a353) ) )
& ( ~ hskp29
| ( ndr1_0
& c0_1(a354)
& c1_1(a354)
& c2_1(a354) ) )
& ( ! [X0] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0 )
| ! [X1] :
( c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ ndr1_0 )
| ! [X2] :
( c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ) )
& ( ! [X3] :
( c0_1(X3)
| c1_1(X3)
| c2_1(X3)
| ~ ndr1_0 )
| ! [X4] :
( c1_1(X4)
| c2_1(X4)
| c3_1(X4)
| ~ ndr1_0 )
| ! [X5] :
( c2_1(X5)
| ~ c1_1(X5)
| ~ c3_1(X5)
| ~ ndr1_0 ) )
& ( ! [X6] :
( c0_1(X6)
| c1_1(X6)
| c2_1(X6)
| ~ ndr1_0 )
| ! [X7] :
( c1_1(X7)
| ~ c0_1(X7)
| ~ c2_1(X7)
| ~ ndr1_0 )
| ! [X8] :
( ~ c0_1(X8)
| ~ c1_1(X8)
| ~ c3_1(X8)
| ~ ndr1_0 ) )
& ( ! [X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0 )
| ! [X10] :
( c2_1(X10)
| ~ c0_1(X10)
| ~ c1_1(X10)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X11] :
( c0_1(X11)
| c1_1(X11)
| c3_1(X11)
| ~ ndr1_0 )
| ! [X12] :
( c0_1(X12)
| c2_1(X12)
| c3_1(X12)
| ~ ndr1_0 )
| ! [X13] :
( c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0 ) )
& ( ! [X14] :
( c0_1(X14)
| c1_1(X14)
| c3_1(X14)
| ~ ndr1_0 )
| ! [X15] :
( c0_1(X15)
| c2_1(X15)
| ~ c1_1(X15)
| ~ ndr1_0 )
| ! [X16] :
( c3_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 ) )
& ( ! [X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0 )
| ! [X18] :
( c0_1(X18)
| c2_1(X18)
| ~ c1_1(X18)
| ~ ndr1_0 )
| ! [X19] :
( c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 ) )
& ( ! [X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0 )
| ! [X21] :
( c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0 )
| hskp1 )
& ( ! [X22] :
( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0 )
| ! [X23] :
( c2_1(X23)
| ~ c1_1(X23)
| ~ c3_1(X23)
| ~ ndr1_0 )
| hskp0 )
& ( ! [X24] :
( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0 )
| hskp2
| hskp0 )
& ( ! [X25] :
( c0_1(X25)
| c2_1(X25)
| c3_1(X25)
| ~ ndr1_0 )
| ! [X26] :
( c0_1(X26)
| c2_1(X26)
| ~ c1_1(X26)
| ~ ndr1_0 )
| ! [X27] :
( c1_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 ) )
& ( ! [X28] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X29] :
( c0_1(X29)
| c3_1(X29)
| ~ c1_1(X29)
| ~ ndr1_0 )
| ! [X30] :
( c0_1(X30)
| ~ c1_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 ) )
& ( ! [X31] :
( c0_1(X31)
| c2_1(X31)
| ~ c1_1(X31)
| ~ ndr1_0 )
| ! [X32] :
( c0_1(X32)
| c3_1(X32)
| ~ c1_1(X32)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X33] :
( c0_1(X33)
| c2_1(X33)
| ~ c1_1(X33)
| ~ ndr1_0 )
| ! [X34] :
( c1_1(X34)
| ~ c0_1(X34)
| ~ c2_1(X34)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X35] :
( c0_1(X35)
| c2_1(X35)
| ~ c1_1(X35)
| ~ ndr1_0 )
| ! [X36] :
( c1_1(X36)
| ~ c0_1(X36)
| ~ c3_1(X36)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X37] :
( c0_1(X37)
| c2_1(X37)
| ~ c1_1(X37)
| ~ ndr1_0 )
| ! [X38] :
( c3_1(X38)
| ~ c0_1(X38)
| ~ c1_1(X38)
| ~ ndr1_0 )
| hskp6 )
& ( ! [X39] :
( c0_1(X39)
| c2_1(X39)
| ~ c1_1(X39)
| ~ ndr1_0 )
| hskp7
| hskp4 )
& ( ! [X40] :
( c0_1(X40)
| c2_1(X40)
| ~ c1_1(X40)
| ~ ndr1_0 )
| hskp8
| hskp5 )
& ( ! [X41] :
( c0_1(X41)
| c2_1(X41)
| ~ c3_1(X41)
| ~ ndr1_0 )
| ! [X42] :
( c3_1(X42)
| ~ c0_1(X42)
| ~ c2_1(X42)
| ~ ndr1_0 )
| hskp9 )
& ( ! [X43] :
( c0_1(X43)
| c2_1(X43)
| ~ c3_1(X43)
| ~ ndr1_0 )
| hskp10
| hskp11 )
& ( ! [X44] :
( c0_1(X44)
| c3_1(X44)
| ~ c1_1(X44)
| ~ ndr1_0 )
| ! [X45] :
( c2_1(X45)
| ~ c1_1(X45)
| ~ c3_1(X45)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X46] :
( c0_1(X46)
| c3_1(X46)
| ~ c2_1(X46)
| ~ ndr1_0 )
| ! [X47] :
( c3_1(X47)
| ~ c1_1(X47)
| ~ c2_1(X47)
| ~ ndr1_0 )
| hskp8 )
& ( ! [X48] :
( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0 )
| ! [X49] :
( c2_1(X49)
| c3_1(X49)
| ~ c0_1(X49)
| ~ ndr1_0 )
| hskp12 )
& ( ! [X50] :
( c0_1(X50)
| ~ c1_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0 )
| ! [X51] :
( c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X52] :
( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0 )
| ! [X53] :
( c2_1(X53)
| c3_1(X53)
| ~ c1_1(X53)
| ~ ndr1_0 )
| hskp3 )
& ( ! [X54] :
( c0_1(X54)
| ~ c2_1(X54)
| ~ c3_1(X54)
| ~ ndr1_0 )
| hskp14
| hskp0 )
& ( ! [X55] :
( c1_1(X55)
| c2_1(X55)
| ~ c0_1(X55)
| ~ ndr1_0 )
| ! [X56] :
( c2_1(X56)
| ~ c1_1(X56)
| ~ c3_1(X56)
| ~ ndr1_0 )
| hskp14 )
& ( ! [X57] :
( c1_1(X57)
| c2_1(X57)
| ~ c3_1(X57)
| ~ ndr1_0 )
| ! [X58] :
( c2_1(X58)
| ~ c0_1(X58)
| ~ c1_1(X58)
| ~ ndr1_0 )
| hskp7 )
& ( ! [X59] :
( c1_1(X59)
| c2_1(X59)
| ~ c3_1(X59)
| ~ ndr1_0 )
| hskp6
| hskp15 )
& ( ! [X60] :
( c1_1(X60)
| c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0 )
| hskp16 )
& ( ! [X61] :
( c1_1(X61)
| c3_1(X61)
| ~ c0_1(X61)
| ~ ndr1_0 )
| ! [X62] :
( c1_1(X62)
| c3_1(X62)
| ~ c2_1(X62)
| ~ ndr1_0 )
| hskp13 )
& ( ! [X63] :
( c1_1(X63)
| c3_1(X63)
| ~ c0_1(X63)
| ~ ndr1_0 )
| ! [X64] :
( c2_1(X64)
| c3_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X65] :
( c1_1(X65)
| c3_1(X65)
| ~ c2_1(X65)
| ~ ndr1_0 )
| ! [X66] :
( c2_1(X66)
| c3_1(X66)
| ~ c1_1(X66)
| ~ ndr1_0 )
| hskp5 )
& ( ! [X67] :
( c1_1(X67)
| c3_1(X67)
| ~ c2_1(X67)
| ~ ndr1_0 )
| hskp11
| hskp16 )
& ( ! [X68] :
( c1_1(X68)
| ~ c0_1(X68)
| ~ c2_1(X68)
| ~ ndr1_0 )
| ! [X69] :
( c1_1(X69)
| ~ c0_1(X69)
| ~ c3_1(X69)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X70] :
( c1_1(X70)
| ~ c0_1(X70)
| ~ c2_1(X70)
| ~ ndr1_0 )
| hskp17
| hskp18 )
& ( ! [X71] :
( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0 )
| hskp19
| hskp12 )
& ( ! [X72] :
( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0 )
| hskp11
| hskp20 )
& ( ! [X73] :
( c1_1(X73)
| ~ c2_1(X73)
| ~ c3_1(X73)
| ~ ndr1_0 )
| hskp27
| hskp3 )
& ( ! [X74] :
( c2_1(X74)
| c3_1(X74)
| ~ c0_1(X74)
| ~ ndr1_0 )
| hskp21 )
& ( ! [X75] :
( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0 )
| ! [X76] :
( c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0 )
| ! [X77] :
( ~ c0_1(X77)
| ~ c1_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0 ) )
& ( ! [X78] :
( c2_1(X78)
| c3_1(X78)
| ~ c1_1(X78)
| ~ ndr1_0 )
| ! [X79] :
( ~ c0_1(X79)
| ~ c1_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0 )
| hskp17 )
& ( ! [X80] :
( c2_1(X80)
| c3_1(X80)
| ~ c1_1(X80)
| ~ ndr1_0 )
| hskp22 )
& ( ! [X81] :
( c2_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0 )
| ! [X82] :
( ~ c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 ) )
& ( ! [X83] :
( c3_1(X83)
| ~ c0_1(X83)
| ~ c1_1(X83)
| ~ ndr1_0 )
| hskp17
| hskp4 )
& ( ! [X84] :
( c3_1(X84)
| ~ c0_1(X84)
| ~ c1_1(X84)
| ~ ndr1_0 )
| hskp23
| hskp24 )
& ( ! [X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c2_1(X85)
| ~ ndr1_0 )
| ! [X86] :
( ~ c0_1(X86)
| ~ c2_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0 )
| hskp11 )
& ( ! [X87] :
( c3_1(X87)
| ~ c1_1(X87)
| ~ c2_1(X87)
| ~ ndr1_0 )
| ! [X88] :
( ~ c1_1(X88)
| ~ c2_1(X88)
| ~ c3_1(X88)
| ~ ndr1_0 )
| hskp4 )
& ( ! [X89] :
( c3_1(X89)
| ~ c1_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0 )
| hskp15
| hskp25 )
& ( ! [X90] :
( ~ c0_1(X90)
| ~ c1_1(X90)
| ~ c2_1(X90)
| ~ ndr1_0 )
| hskp6
| hskp8 )
& ( ! [X91] :
( ~ c0_1(X91)
| ~ c1_1(X91)
| ~ c2_1(X91)
| ~ ndr1_0 )
| hskp26
| hskp23 )
& ( ! [X92] :
( ~ c0_1(X92)
| ~ c1_1(X92)
| ~ c3_1(X92)
| ~ ndr1_0 )
| hskp17
| hskp21 )
& ( ! [X93] :
( ~ c1_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93)
| ~ ndr1_0 )
| hskp28 )
& ( hskp29
| hskp27
| hskp10 )
& ( hskp7
| hskp1
| hskp10 )
& ( hskp17
| hskp5
| hskp24 )
& ( hskp6
| hskp15
| hskp23 )
& ( hskp26
| hskp11
| hskp12 )
& ( hskp26
| hskp16 )
& ( hskp20
| hskp12
| hskp25 ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
( hskp20
| hskp12
| hskp25 ),
inference(cnf_transformation,[],[f5]) ).
fof(f7,plain,
( hskp26
| hskp16 ),
inference(cnf_transformation,[],[f5]) ).
fof(f8,plain,
( hskp26
| hskp11
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f17,plain,
! [X89] :
( c3_1(X89)
| ~ c1_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0
| hskp15
| hskp25 ),
inference(cnf_transformation,[],[f5]) ).
fof(f19,plain,
! [X86,X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c2_1(X85)
| ~ ndr1_0
| ~ c0_1(X86)
| ~ c2_1(X86)
| ~ c3_1(X86)
| ~ ndr1_0
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f22,plain,
! [X82,X81] :
( c2_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0
| ~ c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f23,plain,
! [X80] :
( c2_1(X80)
| c3_1(X80)
| ~ c1_1(X80)
| ~ ndr1_0
| hskp22 ),
inference(cnf_transformation,[],[f5]) ).
fof(f25,plain,
! [X76,X77,X75] :
( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0
| c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ ndr1_0
| ~ c0_1(X77)
| ~ c1_1(X77)
| ~ c3_1(X77)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f26,plain,
! [X74] :
( c2_1(X74)
| c3_1(X74)
| ~ c0_1(X74)
| ~ ndr1_0
| hskp21 ),
inference(cnf_transformation,[],[f5]) ).
fof(f28,plain,
! [X72] :
( c1_1(X72)
| ~ c0_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0
| hskp11
| hskp20 ),
inference(cnf_transformation,[],[f5]) ).
fof(f29,plain,
! [X71] :
( c1_1(X71)
| ~ c0_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0
| hskp19
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f32,plain,
! [X67] :
( c1_1(X67)
| c3_1(X67)
| ~ c2_1(X67)
| ~ ndr1_0
| hskp11
| hskp16 ),
inference(cnf_transformation,[],[f5]) ).
fof(f34,plain,
! [X63,X64] :
( c1_1(X63)
| c3_1(X63)
| ~ c0_1(X63)
| ~ ndr1_0
| c2_1(X64)
| c3_1(X64)
| ~ c1_1(X64)
| ~ ndr1_0
| hskp17 ),
inference(cnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X60] :
( c1_1(X60)
| c2_1(X60)
| ~ c3_1(X60)
| ~ ndr1_0
| hskp16 ),
inference(cnf_transformation,[],[f5]) ).
fof(f40,plain,
! [X54] :
( c0_1(X54)
| ~ c2_1(X54)
| ~ c3_1(X54)
| ~ ndr1_0
| hskp14
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f41,plain,
! [X52,X53] :
( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0
| c2_1(X53)
| c3_1(X53)
| ~ c1_1(X53)
| ~ ndr1_0
| hskp3 ),
inference(cnf_transformation,[],[f5]) ).
fof(f43,plain,
! [X48,X49] :
( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0
| c2_1(X49)
| c3_1(X49)
| ~ c0_1(X49)
| ~ ndr1_0
| hskp12 ),
inference(cnf_transformation,[],[f5]) ).
fof(f46,plain,
! [X43] :
( c0_1(X43)
| c2_1(X43)
| ~ c3_1(X43)
| ~ ndr1_0
| hskp10
| hskp11 ),
inference(cnf_transformation,[],[f5]) ).
fof(f54,plain,
! [X28,X29,X30] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0
| c0_1(X29)
| c3_1(X29)
| ~ c1_1(X29)
| ~ ndr1_0
| c0_1(X30)
| ~ c1_1(X30)
| ~ c3_1(X30)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f55,plain,
! [X26,X27,X25] :
( c0_1(X25)
| c2_1(X25)
| c3_1(X25)
| ~ ndr1_0
| c0_1(X26)
| c2_1(X26)
| ~ c1_1(X26)
| ~ ndr1_0
| c1_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f56,plain,
! [X24] :
( c0_1(X24)
| c1_1(X24)
| ~ c3_1(X24)
| ~ ndr1_0
| hskp2
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f57,plain,
! [X22,X23] :
( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0
| c2_1(X23)
| ~ c1_1(X23)
| ~ c3_1(X23)
| ~ ndr1_0
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f58,plain,
! [X21,X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0
| c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| ~ ndr1_0
| hskp1 ),
inference(cnf_transformation,[],[f5]) ).
fof(f59,plain,
! [X18,X19,X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0
| c0_1(X18)
| c2_1(X18)
| ~ c1_1(X18)
| ~ ndr1_0
| c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f61,plain,
! [X11,X12,X13] :
( c0_1(X11)
| c1_1(X11)
| c3_1(X11)
| ~ ndr1_0
| c0_1(X12)
| c2_1(X12)
| c3_1(X12)
| ~ ndr1_0
| c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f62,plain,
! [X10,X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0
| c2_1(X10)
| ~ c0_1(X10)
| ~ c1_1(X10)
| ~ ndr1_0
| hskp0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f65,plain,
! [X2,X0,X1] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ ndr1_0
| c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2)
| ~ ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f78,plain,
( ~ hskp26
| ~ c3_1(a349) ),
inference(cnf_transformation,[],[f5]) ).
fof(f79,plain,
( ~ hskp26
| ~ c2_1(a349) ),
inference(cnf_transformation,[],[f5]) ).
fof(f80,plain,
( ~ hskp26
| c0_1(a349) ),
inference(cnf_transformation,[],[f5]) ).
fof(f82,plain,
( ~ hskp25
| ~ c3_1(a346) ),
inference(cnf_transformation,[],[f5]) ).
fof(f83,plain,
( ~ hskp25
| ~ c1_1(a346) ),
inference(cnf_transformation,[],[f5]) ).
fof(f84,plain,
( ~ hskp25
| ~ c0_1(a346) ),
inference(cnf_transformation,[],[f5]) ).
fof(f85,plain,
( ~ hskp25
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f94,plain,
( ~ hskp22
| ~ c3_1(a338) ),
inference(cnf_transformation,[],[f5]) ).
fof(f95,plain,
( ~ hskp22
| ~ c2_1(a338) ),
inference(cnf_transformation,[],[f5]) ).
fof(f96,plain,
( ~ hskp22
| ~ c1_1(a338) ),
inference(cnf_transformation,[],[f5]) ).
fof(f98,plain,
( ~ hskp21
| ~ c1_1(a336) ),
inference(cnf_transformation,[],[f5]) ).
fof(f99,plain,
( ~ hskp21
| ~ c0_1(a336) ),
inference(cnf_transformation,[],[f5]) ).
fof(f100,plain,
( ~ hskp21
| c3_1(a336) ),
inference(cnf_transformation,[],[f5]) ).
fof(f102,plain,
( ~ hskp20
| ~ c3_1(a333) ),
inference(cnf_transformation,[],[f5]) ).
fof(f103,plain,
( ~ hskp20
| ~ c2_1(a333) ),
inference(cnf_transformation,[],[f5]) ).
fof(f104,plain,
( ~ hskp20
| c1_1(a333) ),
inference(cnf_transformation,[],[f5]) ).
fof(f105,plain,
( ~ hskp20
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f106,plain,
( ~ hskp19
| ~ c3_1(a330) ),
inference(cnf_transformation,[],[f5]) ).
fof(f107,plain,
( ~ hskp19
| c2_1(a330) ),
inference(cnf_transformation,[],[f5]) ).
fof(f108,plain,
( ~ hskp19
| c1_1(a330) ),
inference(cnf_transformation,[],[f5]) ).
fof(f114,plain,
( ~ hskp17
| ~ c3_1(a323) ),
inference(cnf_transformation,[],[f5]) ).
fof(f115,plain,
( ~ hskp17
| c2_1(a323) ),
inference(cnf_transformation,[],[f5]) ).
fof(f116,plain,
( ~ hskp17
| c0_1(a323) ),
inference(cnf_transformation,[],[f5]) ).
fof(f118,plain,
( ~ hskp16
| ~ c1_1(a321) ),
inference(cnf_transformation,[],[f5]) ).
fof(f119,plain,
( ~ hskp16
| c3_1(a321) ),
inference(cnf_transformation,[],[f5]) ).
fof(f120,plain,
( ~ hskp16
| c2_1(a321) ),
inference(cnf_transformation,[],[f5]) ).
fof(f122,plain,
( ~ hskp15
| ~ c2_1(a320) ),
inference(cnf_transformation,[],[f5]) ).
fof(f123,plain,
( ~ hskp15
| ~ c0_1(a320) ),
inference(cnf_transformation,[],[f5]) ).
fof(f124,plain,
( ~ hskp15
| c1_1(a320) ),
inference(cnf_transformation,[],[f5]) ).
fof(f126,plain,
( ~ hskp14
| ~ c0_1(a315) ),
inference(cnf_transformation,[],[f5]) ).
fof(f127,plain,
( ~ hskp14
| c2_1(a315) ),
inference(cnf_transformation,[],[f5]) ).
fof(f128,plain,
( ~ hskp14
| c1_1(a315) ),
inference(cnf_transformation,[],[f5]) ).
fof(f134,plain,
( ~ hskp12
| ~ c2_1(a310) ),
inference(cnf_transformation,[],[f5]) ).
fof(f135,plain,
( ~ hskp12
| ~ c0_1(a310) ),
inference(cnf_transformation,[],[f5]) ).
fof(f136,plain,
( ~ hskp12
| c3_1(a310) ),
inference(cnf_transformation,[],[f5]) ).
fof(f137,plain,
( ~ hskp12
| ndr1_0 ),
inference(cnf_transformation,[],[f5]) ).
fof(f138,plain,
( ~ hskp11
| ~ c2_1(a309) ),
inference(cnf_transformation,[],[f5]) ).
fof(f139,plain,
( ~ hskp11
| c3_1(a309) ),
inference(cnf_transformation,[],[f5]) ).
fof(f140,plain,
( ~ hskp11
| c1_1(a309) ),
inference(cnf_transformation,[],[f5]) ).
fof(f142,plain,
( ~ hskp10
| ~ c0_1(a308) ),
inference(cnf_transformation,[],[f5]) ).
fof(f143,plain,
( ~ hskp10
| c3_1(a308) ),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
( ~ hskp10
| c1_1(a308) ),
inference(cnf_transformation,[],[f5]) ).
fof(f170,plain,
( ~ hskp3
| ~ c2_1(a299) ),
inference(cnf_transformation,[],[f5]) ).
fof(f171,plain,
( ~ hskp3
| c3_1(a299) ),
inference(cnf_transformation,[],[f5]) ).
fof(f172,plain,
( ~ hskp3
| c0_1(a299) ),
inference(cnf_transformation,[],[f5]) ).
fof(f174,plain,
( ~ hskp2
| ~ c3_1(a297) ),
inference(cnf_transformation,[],[f5]) ).
fof(f175,plain,
( ~ hskp2
| ~ c0_1(a297) ),
inference(cnf_transformation,[],[f5]) ).
fof(f176,plain,
( ~ hskp2
| c1_1(a297) ),
inference(cnf_transformation,[],[f5]) ).
fof(f178,plain,
( ~ hskp1
| ~ c1_1(a295) ),
inference(cnf_transformation,[],[f5]) ).
fof(f179,plain,
( ~ hskp1
| c2_1(a295) ),
inference(cnf_transformation,[],[f5]) ).
fof(f180,plain,
( ~ hskp1
| c0_1(a295) ),
inference(cnf_transformation,[],[f5]) ).
fof(f182,plain,
( ~ hskp0
| ~ c3_1(a294) ),
inference(cnf_transformation,[],[f5]) ).
fof(f183,plain,
( ~ hskp0
| ~ c2_1(a294) ),
inference(cnf_transformation,[],[f5]) ).
fof(f184,plain,
( ~ hskp0
| ~ c0_1(a294) ),
inference(cnf_transformation,[],[f5]) ).
fof(f187,plain,
! [X86,X85] :
( c3_1(X85)
| ~ c0_1(X85)
| ~ c2_1(X85)
| ~ ndr1_0
| ~ c0_1(X86)
| ~ c2_1(X86)
| ~ c3_1(X86)
| hskp11 ),
inference(duplicate_literal_removal,[],[f19]) ).
fof(f188,plain,
! [X82,X81] :
( c2_1(X81)
| ~ c1_1(X81)
| ~ c3_1(X81)
| ~ ndr1_0
| ~ c0_1(X82)
| ~ c2_1(X82)
| ~ c3_1(X82) ),
inference(duplicate_literal_removal,[],[f22]) ).
fof(f190,plain,
! [X76,X77,X75] :
( c2_1(X75)
| c3_1(X75)
| ~ c1_1(X75)
| ~ ndr1_0
| c2_1(X76)
| ~ c1_1(X76)
| ~ c3_1(X76)
| ~ c0_1(X77)
| ~ c1_1(X77)
| ~ c3_1(X77) ),
inference(duplicate_literal_removal,[],[f25]) ).
fof(f193,plain,
! [X63,X64] :
( c1_1(X63)
| c3_1(X63)
| ~ c0_1(X63)
| ~ ndr1_0
| c2_1(X64)
| c3_1(X64)
| ~ c1_1(X64)
| hskp17 ),
inference(duplicate_literal_removal,[],[f34]) ).
fof(f197,plain,
! [X52,X53] :
( c0_1(X52)
| ~ c2_1(X52)
| ~ c3_1(X52)
| ~ ndr1_0
| c2_1(X53)
| c3_1(X53)
| ~ c1_1(X53)
| hskp3 ),
inference(duplicate_literal_removal,[],[f41]) ).
fof(f199,plain,
! [X48,X49] :
( c0_1(X48)
| ~ c1_1(X48)
| ~ c2_1(X48)
| ~ ndr1_0
| c2_1(X49)
| c3_1(X49)
| ~ c0_1(X49)
| hskp12 ),
inference(duplicate_literal_removal,[],[f43]) ).
fof(f207,plain,
! [X28,X29,X30] :
( c0_1(X28)
| c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0
| c0_1(X29)
| c3_1(X29)
| ~ c1_1(X29)
| c0_1(X30)
| ~ c1_1(X30)
| ~ c3_1(X30) ),
inference(duplicate_literal_removal,[],[f54]) ).
fof(f208,plain,
! [X26,X27,X25] :
( c0_1(X25)
| c2_1(X25)
| c3_1(X25)
| ~ ndr1_0
| c0_1(X26)
| c2_1(X26)
| ~ c1_1(X26)
| c1_1(X27)
| ~ c2_1(X27)
| ~ c3_1(X27) ),
inference(duplicate_literal_removal,[],[f55]) ).
fof(f209,plain,
! [X22,X23] :
( c0_1(X22)
| c1_1(X22)
| ~ c3_1(X22)
| ~ ndr1_0
| c2_1(X23)
| ~ c1_1(X23)
| ~ c3_1(X23)
| hskp0 ),
inference(duplicate_literal_removal,[],[f57]) ).
fof(f210,plain,
! [X21,X20] :
( c0_1(X20)
| c1_1(X20)
| ~ c2_1(X20)
| ~ ndr1_0
| c1_1(X21)
| ~ c2_1(X21)
| ~ c3_1(X21)
| hskp1 ),
inference(duplicate_literal_removal,[],[f58]) ).
fof(f211,plain,
! [X18,X19,X17] :
( c0_1(X17)
| c1_1(X17)
| ~ c2_1(X17)
| ~ ndr1_0
| c0_1(X18)
| c2_1(X18)
| ~ c1_1(X18)
| c3_1(X19)
| ~ c1_1(X19)
| ~ c2_1(X19) ),
inference(duplicate_literal_removal,[],[f59]) ).
fof(f213,plain,
! [X11,X12,X13] :
( c0_1(X11)
| c1_1(X11)
| c3_1(X11)
| ~ ndr1_0
| c0_1(X12)
| c2_1(X12)
| c3_1(X12)
| c0_1(X13)
| ~ c2_1(X13)
| ~ c3_1(X13) ),
inference(duplicate_literal_removal,[],[f61]) ).
fof(f214,plain,
! [X10,X9] :
( c0_1(X9)
| c1_1(X9)
| c2_1(X9)
| ~ ndr1_0
| c2_1(X10)
| ~ c0_1(X10)
| ~ c1_1(X10)
| hskp0 ),
inference(duplicate_literal_removal,[],[f62]) ).
fof(f217,plain,
! [X2,X0,X1] :
( c0_1(X0)
| c1_1(X0)
| c2_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| c0_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X2) ),
inference(duplicate_literal_removal,[],[f65]) ).
fof(f219,definition,
( spl0_1
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f222,definition,
( spl0_2
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f225,definition,
( spl0_3
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f227,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f6,f225,f222,f219]) ).
fof(f229,definition,
( spl0_4
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f232,definition,
( spl0_5
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f234,plain,
( spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f7,f232,f229]) ).
fof(f236,definition,
( spl0_6
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f238,plain,
( spl0_2
| spl0_6
| spl0_5 ),
inference(avatar_split_clause,[],[f8,f232,f236,f222]) ).
fof(f243,definition,
( spl0_8
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f256,definition,
( spl0_12
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f260,definition,
( spl0_13
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f263,definition,
( spl0_14
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f280,definition,
( spl0_19
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f287,definition,
( spl0_21
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f290,definition,
( spl0_22
<=> ! [X92] :
( ~ c0_1(X92)
| ~ c3_1(X92)
| ~ c1_1(X92) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f291,plain,
( ! [X92] :
( ~ c3_1(X92)
| ~ c0_1(X92)
| ~ c1_1(X92) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f290]) ).
fof(f302,definition,
( spl0_25
<=> ! [X89] :
( c3_1(X89)
| ~ c2_1(X89)
| ~ c1_1(X89) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f303,plain,
( ! [X89] :
( c3_1(X89)
| ~ c2_1(X89)
| ~ c1_1(X89) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f302]) ).
fof(f304,plain,
( spl0_1
| spl0_8
| ~ spl0_19
| spl0_25 ),
inference(avatar_split_clause,[],[f17,f302,f280,f243,f219]) ).
fof(f310,definition,
( spl0_27
<=> ! [X86] :
( ~ c0_1(X86)
| ~ c3_1(X86)
| ~ c2_1(X86) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f311,plain,
( ! [X86] :
( ~ c3_1(X86)
| ~ c0_1(X86)
| ~ c2_1(X86) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f313,definition,
( spl0_28
<=> ! [X85] :
( c3_1(X85)
| ~ c2_1(X85)
| ~ c0_1(X85) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f314,plain,
( ! [X85] :
( c3_1(X85)
| ~ c2_1(X85)
| ~ c0_1(X85) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f313]) ).
fof(f315,plain,
( spl0_6
| spl0_27
| ~ spl0_19
| spl0_28 ),
inference(avatar_split_clause,[],[f187,f313,f280,f310,f236]) ).
fof(f322,definition,
( spl0_30
<=> ! [X81] :
( c2_1(X81)
| ~ c3_1(X81)
| ~ c1_1(X81) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f323,plain,
( ! [X81] :
( ~ c3_1(X81)
| c2_1(X81)
| ~ c1_1(X81) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f322]) ).
fof(f324,plain,
( spl0_27
| ~ spl0_19
| spl0_30 ),
inference(avatar_split_clause,[],[f188,f322,f280,f310]) ).
fof(f326,definition,
( spl0_31
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f329,definition,
( spl0_32
<=> ! [X80] :
( c2_1(X80)
| ~ c1_1(X80)
| c3_1(X80) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f330,plain,
( ! [X80] :
( c3_1(X80)
| ~ c1_1(X80)
| c2_1(X80) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f331,plain,
( spl0_31
| ~ spl0_19
| spl0_32 ),
inference(avatar_split_clause,[],[f23,f329,f280,f326]) ).
fof(f333,plain,
( spl0_22
| spl0_30
| ~ spl0_19
| spl0_32 ),
inference(avatar_split_clause,[],[f190,f329,f280,f322,f290]) ).
fof(f335,definition,
( spl0_33
<=> ! [X74] :
( c2_1(X74)
| ~ c0_1(X74)
| c3_1(X74) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f336,plain,
( ! [X74] :
( c3_1(X74)
| ~ c0_1(X74)
| c2_1(X74) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f337,plain,
( spl0_21
| ~ spl0_19
| spl0_33 ),
inference(avatar_split_clause,[],[f26,f335,f280,f287]) ).
fof(f339,definition,
( spl0_34
<=> hskp3 ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f342,definition,
( spl0_35
<=> ! [X73] :
( c1_1(X73)
| ~ c3_1(X73)
| ~ c2_1(X73) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f343,plain,
( ! [X73] :
( ~ c3_1(X73)
| c1_1(X73)
| ~ c2_1(X73) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f342]) ).
fof(f346,definition,
( spl0_36
<=> ! [X72] :
( c1_1(X72)
| ~ c2_1(X72)
| ~ c0_1(X72) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f347,plain,
( ! [X72] :
( ~ c0_1(X72)
| ~ c2_1(X72)
| c1_1(X72) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f346]) ).
fof(f348,plain,
( spl0_3
| spl0_6
| ~ spl0_19
| spl0_36 ),
inference(avatar_split_clause,[],[f28,f346,f280,f236,f225]) ).
fof(f350,definition,
( spl0_37
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f352,plain,
( spl0_2
| spl0_37
| ~ spl0_19
| spl0_36 ),
inference(avatar_split_clause,[],[f29,f346,f280,f350,f222]) ).
fof(f362,definition,
( spl0_40
<=> ! [X67] :
( c1_1(X67)
| ~ c2_1(X67)
| c3_1(X67) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f363,plain,
( ! [X67] :
( c3_1(X67)
| ~ c2_1(X67)
| c1_1(X67) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f362]) ).
fof(f364,plain,
( spl0_4
| spl0_6
| ~ spl0_19
| spl0_40 ),
inference(avatar_split_clause,[],[f32,f362,f280,f236,f229]) ).
fof(f367,definition,
( spl0_41
<=> ! [X63] :
( c1_1(X63)
| ~ c0_1(X63)
| c3_1(X63) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f368,plain,
( ! [X63] :
( c3_1(X63)
| ~ c0_1(X63)
| c1_1(X63) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f369,plain,
( spl0_12
| spl0_32
| ~ spl0_19
| spl0_41 ),
inference(avatar_split_clause,[],[f193,f367,f280,f329,f256]) ).
fof(f375,definition,
( spl0_43
<=> ! [X60] :
( c1_1(X60)
| ~ c3_1(X60)
| c2_1(X60) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f376,plain,
( ! [X60] :
( ~ c3_1(X60)
| c1_1(X60)
| c2_1(X60) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f377,plain,
( spl0_4
| ~ spl0_19
| spl0_43 ),
inference(avatar_split_clause,[],[f36,f375,f280,f229]) ).
fof(f380,definition,
( spl0_44
<=> ! [X58] :
( c2_1(X58)
| ~ c1_1(X58)
| ~ c0_1(X58) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f381,plain,
( ! [X58] :
( ~ c0_1(X58)
| ~ c1_1(X58)
| c2_1(X58) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f384,definition,
( spl0_45
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f391,definition,
( spl0_47
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f394,definition,
( spl0_48
<=> ! [X54] :
( c0_1(X54)
| ~ c3_1(X54)
| ~ c2_1(X54) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f395,plain,
( ! [X54] :
( ~ c3_1(X54)
| c0_1(X54)
| ~ c2_1(X54) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f396,plain,
( spl0_47
| spl0_45
| ~ spl0_19
| spl0_48 ),
inference(avatar_split_clause,[],[f40,f394,f280,f384,f391]) ).
fof(f397,plain,
( spl0_34
| spl0_32
| ~ spl0_19
| spl0_48 ),
inference(avatar_split_clause,[],[f197,f394,f280,f329,f339]) ).
fof(f399,definition,
( spl0_49
<=> ! [X50] :
( c0_1(X50)
| ~ c2_1(X50)
| ~ c1_1(X50) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f400,plain,
( ! [X50] :
( c0_1(X50)
| ~ c2_1(X50)
| ~ c1_1(X50) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f399]) ).
fof(f402,plain,
( spl0_2
| spl0_33
| ~ spl0_19
| spl0_49 ),
inference(avatar_split_clause,[],[f199,f399,f280,f335,f222]) ).
fof(f408,definition,
( spl0_51
<=> ! [X44] :
( c0_1(X44)
| ~ c1_1(X44)
| c3_1(X44) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f409,plain,
( ! [X44] :
( c3_1(X44)
| ~ c1_1(X44)
| c0_1(X44) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f412,definition,
( spl0_52
<=> ! [X43] :
( c0_1(X43)
| ~ c3_1(X43)
| c2_1(X43) ) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f413,plain,
( ! [X43] :
( ~ c3_1(X43)
| c0_1(X43)
| c2_1(X43) )
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f414,plain,
( spl0_6
| spl0_13
| ~ spl0_19
| spl0_52 ),
inference(avatar_split_clause,[],[f46,f412,f280,f260,f236]) ).
fof(f420,definition,
( spl0_54
<=> ! [X40] :
( c0_1(X40)
| ~ c1_1(X40)
| c2_1(X40) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f421,plain,
( ! [X40] :
( c0_1(X40)
| ~ c1_1(X40)
| c2_1(X40) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f429,definition,
( spl0_55
<=> ! [X30] :
( c0_1(X30)
| ~ c3_1(X30)
| ~ c1_1(X30) ) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f430,plain,
( ! [X30] :
( ~ c3_1(X30)
| c0_1(X30)
| ~ c1_1(X30) )
| ~ spl0_55 ),
inference(avatar_component_clause,[],[f429]) ).
fof(f431,plain,
( spl0_55
| spl0_51
| ~ spl0_19
| spl0_54 ),
inference(avatar_split_clause,[],[f207,f420,f280,f408,f429]) ).
fof(f433,definition,
( spl0_56
<=> ! [X25] :
( c0_1(X25)
| c3_1(X25)
| c2_1(X25) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f434,plain,
( ! [X25] :
( c3_1(X25)
| c0_1(X25)
| c2_1(X25) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f433]) ).
fof(f435,plain,
( spl0_35
| spl0_54
| ~ spl0_19
| spl0_56 ),
inference(avatar_split_clause,[],[f208,f433,f280,f420,f342]) ).
fof(f437,definition,
( spl0_57
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f440,definition,
( spl0_58
<=> ! [X24] :
( c0_1(X24)
| ~ c3_1(X24)
| c1_1(X24) ) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f441,plain,
( ! [X24] :
( ~ c3_1(X24)
| c0_1(X24)
| c1_1(X24) )
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f440]) ).
fof(f442,plain,
( spl0_47
| spl0_57
| ~ spl0_19
| spl0_58 ),
inference(avatar_split_clause,[],[f56,f440,f280,f437,f391]) ).
fof(f443,plain,
( spl0_47
| spl0_30
| ~ spl0_19
| spl0_58 ),
inference(avatar_split_clause,[],[f209,f440,f280,f322,f391]) ).
fof(f445,definition,
( spl0_59
<=> ! [X20] :
( c0_1(X20)
| ~ c2_1(X20)
| c1_1(X20) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f446,plain,
( ! [X20] :
( c0_1(X20)
| ~ c2_1(X20)
| c1_1(X20) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f445]) ).
fof(f447,plain,
( spl0_14
| spl0_35
| ~ spl0_19
| spl0_59 ),
inference(avatar_split_clause,[],[f210,f445,f280,f342,f263]) ).
fof(f448,plain,
( spl0_25
| spl0_54
| ~ spl0_19
| spl0_59 ),
inference(avatar_split_clause,[],[f211,f445,f280,f420,f302]) ).
fof(f450,definition,
( spl0_60
<=> ! [X14] :
( c0_1(X14)
| c3_1(X14)
| c1_1(X14) ) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f451,plain,
( ! [X14] :
( c3_1(X14)
| c0_1(X14)
| c1_1(X14) )
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f453,plain,
( spl0_48
| spl0_56
| ~ spl0_19
| spl0_60 ),
inference(avatar_split_clause,[],[f213,f450,f280,f433,f394]) ).
fof(f455,definition,
( spl0_61
<=> ! [X9] :
( c0_1(X9)
| c2_1(X9)
| c1_1(X9) ) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f456,plain,
( ! [X9] :
( c0_1(X9)
| c2_1(X9)
| c1_1(X9) )
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f457,plain,
( spl0_47
| spl0_44
| ~ spl0_19
| spl0_61 ),
inference(avatar_split_clause,[],[f214,f455,f280,f380,f391]) ).
fof(f463,plain,
( spl0_49
| spl0_56
| ~ spl0_19
| spl0_61 ),
inference(avatar_split_clause,[],[f217,f455,f280,f433,f399]) ).
fof(f508,definition,
( spl0_72
<=> c3_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f509,plain,
( ~ c3_1(a349)
| spl0_72 ),
inference(avatar_component_clause,[],[f508]) ).
fof(f511,plain,
( ~ spl0_72
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f78,f232,f508]) ).
fof(f513,definition,
( spl0_73
<=> c2_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f515,plain,
( ~ spl0_73
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f79,f232,f513]) ).
fof(f517,definition,
( spl0_74
<=> c0_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f519,plain,
( spl0_74
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f80,f232,f517]) ).
fof(f522,definition,
( spl0_75
<=> c3_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f523,plain,
( ~ c3_1(a346)
| spl0_75 ),
inference(avatar_component_clause,[],[f522]) ).
fof(f525,plain,
( ~ spl0_75
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f82,f219,f522]) ).
fof(f527,definition,
( spl0_76
<=> c1_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f529,plain,
( ~ spl0_76
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f83,f219,f527]) ).
fof(f531,definition,
( spl0_77
<=> c0_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f532,plain,
( ~ c0_1(a346)
| spl0_77 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f533,plain,
( ~ spl0_77
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f84,f219,f531]) ).
fof(f534,plain,
( spl0_19
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f85,f219,f280]) ).
fof(f564,definition,
( spl0_84
<=> c3_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f565,plain,
( ~ c3_1(a338)
| spl0_84 ),
inference(avatar_component_clause,[],[f564]) ).
fof(f567,plain,
( ~ spl0_84
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f94,f326,f564]) ).
fof(f569,definition,
( spl0_85
<=> c2_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f571,plain,
( ~ spl0_85
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f95,f326,f569]) ).
fof(f573,definition,
( spl0_86
<=> c1_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f575,plain,
( ~ spl0_86
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f96,f326,f573]) ).
fof(f578,definition,
( spl0_87
<=> c1_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f581,plain,
( ~ spl0_87
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f98,f287,f578]) ).
fof(f583,definition,
( spl0_88
<=> c0_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f584,plain,
( ~ c0_1(a336)
| spl0_88 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f585,plain,
( ~ spl0_88
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f99,f287,f583]) ).
fof(f587,definition,
( spl0_89
<=> c3_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f588,plain,
( c3_1(a336)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f587]) ).
fof(f589,plain,
( spl0_89
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f100,f287,f587]) ).
fof(f592,definition,
( spl0_90
<=> c3_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f593,plain,
( ~ c3_1(a333)
| spl0_90 ),
inference(avatar_component_clause,[],[f592]) ).
fof(f595,plain,
( ~ spl0_90
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f102,f225,f592]) ).
fof(f597,definition,
( spl0_91
<=> c2_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f599,plain,
( ~ spl0_91
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f103,f225,f597]) ).
fof(f601,definition,
( spl0_92
<=> c1_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f603,plain,
( spl0_92
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f104,f225,f601]) ).
fof(f604,plain,
( spl0_19
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f105,f225,f280]) ).
fof(f606,definition,
( spl0_93
<=> c3_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f607,plain,
( ~ c3_1(a330)
| spl0_93 ),
inference(avatar_component_clause,[],[f606]) ).
fof(f609,plain,
( ~ spl0_93
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f106,f350,f606]) ).
fof(f611,definition,
( spl0_94
<=> c2_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f613,plain,
( spl0_94
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f107,f350,f611]) ).
fof(f615,definition,
( spl0_95
<=> c1_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f617,plain,
( spl0_95
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f108,f350,f615]) ).
fof(f634,definition,
( spl0_99
<=> c3_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f635,plain,
( ~ c3_1(a323)
| spl0_99 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f637,plain,
( ~ spl0_99
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f114,f256,f634]) ).
fof(f639,definition,
( spl0_100
<=> c2_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f641,plain,
( spl0_100
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f115,f256,f639]) ).
fof(f643,definition,
( spl0_101
<=> c0_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f645,plain,
( spl0_101
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f116,f256,f643]) ).
fof(f648,definition,
( spl0_102
<=> c1_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f651,plain,
( ~ spl0_102
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f118,f229,f648]) ).
fof(f653,definition,
( spl0_103
<=> c3_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f654,plain,
( c3_1(a321)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f653]) ).
fof(f655,plain,
( spl0_103
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f119,f229,f653]) ).
fof(f657,definition,
( spl0_104
<=> c2_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f659,plain,
( spl0_104
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f120,f229,f657]) ).
fof(f662,definition,
( spl0_105
<=> c2_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f665,plain,
( ~ spl0_105
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f122,f243,f662]) ).
fof(f667,definition,
( spl0_106
<=> c0_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f668,plain,
( ~ c0_1(a320)
| spl0_106 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f669,plain,
( ~ spl0_106
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f123,f243,f667]) ).
fof(f671,definition,
( spl0_107
<=> c1_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f673,plain,
( spl0_107
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f124,f243,f671]) ).
fof(f676,definition,
( spl0_108
<=> c0_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f677,plain,
( ~ c0_1(a315)
| spl0_108 ),
inference(avatar_component_clause,[],[f676]) ).
fof(f679,plain,
( ~ spl0_108
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f126,f384,f676]) ).
fof(f681,definition,
( spl0_109
<=> c2_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f683,plain,
( spl0_109
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f127,f384,f681]) ).
fof(f685,definition,
( spl0_110
<=> c1_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f687,plain,
( spl0_110
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f128,f384,f685]) ).
fof(f704,definition,
( spl0_114
<=> c2_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f707,plain,
( ~ spl0_114
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f134,f222,f704]) ).
fof(f709,definition,
( spl0_115
<=> c0_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f710,plain,
( ~ c0_1(a310)
| spl0_115 ),
inference(avatar_component_clause,[],[f709]) ).
fof(f711,plain,
( ~ spl0_115
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f135,f222,f709]) ).
fof(f713,definition,
( spl0_116
<=> c3_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f714,plain,
( c3_1(a310)
| ~ spl0_116 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f715,plain,
( spl0_116
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f136,f222,f713]) ).
fof(f716,plain,
( spl0_19
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f137,f222,f280]) ).
fof(f718,definition,
( spl0_117
<=> c2_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f721,plain,
( ~ spl0_117
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f138,f236,f718]) ).
fof(f723,definition,
( spl0_118
<=> c3_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f724,plain,
( c3_1(a309)
| ~ spl0_118 ),
inference(avatar_component_clause,[],[f723]) ).
fof(f725,plain,
( spl0_118
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f139,f236,f723]) ).
fof(f727,definition,
( spl0_119
<=> c1_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f729,plain,
( spl0_119
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f140,f236,f727]) ).
fof(f732,definition,
( spl0_120
<=> c0_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f733,plain,
( ~ c0_1(a308)
| spl0_120 ),
inference(avatar_component_clause,[],[f732]) ).
fof(f735,plain,
( ~ spl0_120
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f142,f260,f732]) ).
fof(f737,definition,
( spl0_121
<=> c3_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f738,plain,
( c3_1(a308)
| ~ spl0_121 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f739,plain,
( spl0_121
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f143,f260,f737]) ).
fof(f741,definition,
( spl0_122
<=> c1_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f743,plain,
( spl0_122
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f144,f260,f741]) ).
fof(f830,definition,
( spl0_141
<=> c2_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_141])],[avatar_definition]) ).
fof(f833,plain,
( ~ spl0_141
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f170,f339,f830]) ).
fof(f835,definition,
( spl0_142
<=> c3_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f836,plain,
( c3_1(a299)
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f835]) ).
fof(f837,plain,
( spl0_142
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f171,f339,f835]) ).
fof(f839,definition,
( spl0_143
<=> c0_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f841,plain,
( spl0_143
| ~ spl0_34 ),
inference(avatar_split_clause,[],[f172,f339,f839]) ).
fof(f844,definition,
( spl0_144
<=> c3_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f845,plain,
( ~ c3_1(a297)
| spl0_144 ),
inference(avatar_component_clause,[],[f844]) ).
fof(f847,plain,
( ~ spl0_144
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f174,f437,f844]) ).
fof(f849,definition,
( spl0_145
<=> c0_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f851,plain,
( ~ spl0_145
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f175,f437,f849]) ).
fof(f853,definition,
( spl0_146
<=> c1_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f855,plain,
( spl0_146
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f176,f437,f853]) ).
fof(f858,definition,
( spl0_147
<=> c1_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f861,plain,
( ~ spl0_147
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f178,f263,f858]) ).
fof(f863,definition,
( spl0_148
<=> c2_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f865,plain,
( spl0_148
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f179,f263,f863]) ).
fof(f867,definition,
( spl0_149
<=> c0_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f868,plain,
( c0_1(a295)
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f867]) ).
fof(f869,plain,
( spl0_149
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f180,f263,f867]) ).
fof(f872,definition,
( spl0_150
<=> c3_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f873,plain,
( ~ c3_1(a294)
| spl0_150 ),
inference(avatar_component_clause,[],[f872]) ).
fof(f875,plain,
( ~ spl0_150
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f182,f391,f872]) ).
fof(f877,definition,
( spl0_151
<=> c2_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f879,plain,
( ~ spl0_151
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f183,f391,f877]) ).
fof(f881,definition,
( spl0_152
<=> c0_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f882,plain,
( ~ c0_1(a294)
| spl0_152 ),
inference(avatar_component_clause,[],[f881]) ).
fof(f883,plain,
( ~ spl0_152
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f184,f391,f881]) ).
fof(f889,definition,
( spl0_153
<=> c2_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_153])],[avatar_definition]) ).
fof(f919,plain,
( c2_1(a308)
| ~ c1_1(a308)
| ~ spl0_30
| ~ spl0_121 ),
inference(resolution,[],[f323,f738]) ).
fof(f961,definition,
( spl0_157
<=> c1_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f968,definition,
( spl0_158
<=> c0_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f975,plain,
( ~ c0_1(a333)
| c2_1(a333)
| ~ spl0_33
| spl0_90 ),
inference(resolution,[],[f336,f593]) ).
fof(f977,plain,
( ~ c0_1(a349)
| c2_1(a349)
| ~ spl0_33
| spl0_72 ),
inference(resolution,[],[f336,f509]) ).
fof(f981,plain,
( spl0_73
| ~ spl0_74
| ~ spl0_33
| spl0_72 ),
inference(avatar_split_clause,[],[f977,f508,f335,f517,f513]) ).
fof(f985,definition,
( spl0_159
<=> c0_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f986,plain,
( ~ c0_1(a333)
| spl0_159 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f987,plain,
( spl0_91
| ~ spl0_159
| ~ spl0_33
| spl0_90 ),
inference(avatar_split_clause,[],[f975,f592,f335,f985,f597]) ).
fof(f995,plain,
( c1_1(a336)
| ~ c2_1(a336)
| ~ spl0_35
| ~ spl0_89 ),
inference(resolution,[],[f343,f588]) ).
fof(f1007,definition,
( spl0_160
<=> c2_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1010,plain,
( ~ spl0_160
| spl0_87
| ~ spl0_35
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f995,f587,f342,f578,f1007]) ).
fof(f1028,definition,
( spl0_161
<=> c1_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1090,plain,
( ~ c0_1(a338)
| c1_1(a338)
| ~ spl0_41
| spl0_84 ),
inference(resolution,[],[f368,f565]) ).
fof(f1096,plain,
( spl0_86
| ~ spl0_158
| ~ spl0_41
| spl0_84 ),
inference(avatar_split_clause,[],[f1090,f564,f367,f968,f573]) ).
fof(f1102,plain,
( c1_1(a336)
| c2_1(a336)
| ~ spl0_43
| ~ spl0_89 ),
inference(resolution,[],[f376,f588]) ).
fof(f1112,plain,
( spl0_160
| spl0_87
| ~ spl0_43
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f1102,f587,f375,f578,f1007]) ).
fof(f1158,plain,
( c0_1(a321)
| ~ c2_1(a321)
| ~ spl0_48
| ~ spl0_103 ),
inference(resolution,[],[f395,f654]) ).
fof(f1159,plain,
( c0_1(a336)
| ~ c2_1(a336)
| ~ spl0_48
| ~ spl0_89 ),
inference(resolution,[],[f395,f588]) ).
fof(f1172,plain,
( ~ spl0_160
| spl0_88
| ~ spl0_48
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f1159,f587,f394,f583,f1007]) ).
fof(f1175,definition,
( spl0_168
<=> c0_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_168])],[avatar_definition]) ).
fof(f1177,plain,
( ~ spl0_104
| spl0_168
| ~ spl0_48
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f1158,f653,f394,f1175,f657]) ).
fof(f1180,plain,
( c1_1(a299)
| c2_1(a299)
| ~ spl0_43
| ~ spl0_142 ),
inference(resolution,[],[f836,f376]) ).
fof(f1181,plain,
( c2_1(a299)
| ~ c1_1(a299)
| ~ spl0_30
| ~ spl0_142 ),
inference(resolution,[],[f836,f323]) ).
fof(f1185,definition,
( spl0_169
<=> c1_1(a299) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1190,plain,
( ~ spl0_169
| spl0_141
| ~ spl0_30
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1181,f835,f322,f830,f1185]) ).
fof(f1192,plain,
( spl0_141
| spl0_169
| ~ spl0_43
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1180,f835,f375,f1185,f830]) ).
fof(f1217,definition,
( spl0_170
<=> c2_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1229,plain,
( ~ c1_1(a294)
| c2_1(a294)
| ~ spl0_32
| spl0_150 ),
inference(resolution,[],[f330,f873]) ).
fof(f1241,plain,
( spl0_151
| ~ spl0_157
| ~ spl0_32
| spl0_150 ),
inference(avatar_split_clause,[],[f1229,f872,f329,f961,f877]) ).
fof(f1288,plain,
( ~ c2_1(a346)
| c1_1(a346)
| ~ spl0_40
| spl0_75 ),
inference(resolution,[],[f363,f523]) ).
fof(f1293,plain,
( spl0_76
| ~ spl0_170
| ~ spl0_40
| spl0_75 ),
inference(avatar_split_clause,[],[f1288,f522,f362,f1217,f527]) ).
fof(f1298,plain,
( ~ c2_1(a308)
| ~ c1_1(a308)
| ~ spl0_49
| spl0_120 ),
inference(resolution,[],[f400,f733]) ).
fof(f1374,plain,
( c0_1(a333)
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f985]) ).
fof(f1457,plain,
( c0_1(a336)
| c2_1(a336)
| ~ spl0_52
| ~ spl0_89 ),
inference(resolution,[],[f413,f588]) ).
fof(f1466,plain,
( spl0_160
| spl0_88
| ~ spl0_52
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f1457,f587,f412,f583,f1007]) ).
fof(f1510,plain,
( ~ c2_1(a336)
| c1_1(a336)
| ~ spl0_59
| spl0_88 ),
inference(resolution,[],[f446,f584]) ).
fof(f1513,plain,
( ~ c2_1(a346)
| c1_1(a346)
| ~ spl0_59
| spl0_77 ),
inference(resolution,[],[f446,f532]) ).
fof(f1518,plain,
( spl0_76
| ~ spl0_170
| ~ spl0_59
| spl0_77 ),
inference(avatar_split_clause,[],[f1513,f531,f445,f1217,f527]) ).
fof(f1520,plain,
( spl0_87
| ~ spl0_160
| ~ spl0_59
| spl0_88 ),
inference(avatar_split_clause,[],[f1510,f583,f445,f1007,f578]) ).
fof(f1525,plain,
( ~ c2_1(a295)
| c1_1(a295)
| ~ spl0_36
| ~ spl0_149 ),
inference(resolution,[],[f868,f347]) ).
fof(f1617,plain,
( spl0_147
| ~ spl0_148
| ~ spl0_36
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1525,f867,f346,f863,f858]) ).
fof(f1619,plain,
( ~ spl0_122
| ~ spl0_153
| ~ spl0_49
| spl0_120 ),
inference(avatar_split_clause,[],[f1298,f732,f399,f889,f741]) ).
fof(f1720,plain,
( c1_1(a321)
| ~ c2_1(a321)
| ~ spl0_35
| ~ spl0_103 ),
inference(resolution,[],[f343,f654]) ).
fof(f1726,plain,
( ~ spl0_104
| spl0_102
| ~ spl0_35
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f1720,f653,f342,f648,f657]) ).
fof(f1777,plain,
( c2_1(a309)
| ~ c1_1(a309)
| ~ spl0_30
| ~ spl0_118 ),
inference(resolution,[],[f323,f724]) ).
fof(f1778,plain,
( c2_1(a310)
| ~ c1_1(a310)
| ~ spl0_30
| ~ spl0_116 ),
inference(resolution,[],[f323,f714]) ).
fof(f1786,plain,
( ~ spl0_161
| spl0_114
| ~ spl0_30
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1778,f713,f322,f704,f1028]) ).
fof(f1787,plain,
( ~ spl0_119
| spl0_117
| ~ spl0_30
| ~ spl0_118 ),
inference(avatar_split_clause,[],[f1777,f723,f322,f718,f727]) ).
fof(f1804,plain,
( ~ c2_1(a315)
| ~ c1_1(a315)
| ~ spl0_49
| spl0_108 ),
inference(resolution,[],[f400,f677]) ).
fof(f1815,plain,
( ~ spl0_110
| ~ spl0_109
| ~ spl0_49
| spl0_108 ),
inference(avatar_split_clause,[],[f1804,f676,f399,f681,f685]) ).
fof(f1825,plain,
( ~ c0_1(a321)
| ~ c2_1(a321)
| ~ spl0_27
| ~ spl0_103 ),
inference(resolution,[],[f311,f654]) ).
fof(f1830,plain,
( ~ spl0_104
| ~ spl0_168
| ~ spl0_27
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f1825,f653,f310,f1175,f657]) ).
fof(f1835,plain,
( c0_1(a310)
| c2_1(a310)
| ~ spl0_52
| ~ spl0_116 ),
inference(resolution,[],[f413,f714]) ).
fof(f1842,plain,
( spl0_114
| spl0_115
| ~ spl0_52
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1835,f713,f412,f709,f704]) ).
fof(f1844,plain,
( ~ c1_1(a294)
| c2_1(a294)
| ~ spl0_54
| spl0_152 ),
inference(resolution,[],[f421,f882]) ).
fof(f1851,plain,
( ~ c1_1(a333)
| c2_1(a333)
| ~ spl0_54
| spl0_159 ),
inference(resolution,[],[f421,f986]) ).
fof(f1862,plain,
( c0_1(a294)
| c1_1(a294)
| ~ spl0_60
| spl0_150 ),
inference(resolution,[],[f451,f873]) ).
fof(f1869,plain,
( c0_1(a346)
| c1_1(a346)
| ~ spl0_60
| spl0_75 ),
inference(resolution,[],[f451,f523]) ).
fof(f1872,plain,
( spl0_76
| spl0_77
| ~ spl0_60
| spl0_75 ),
inference(avatar_split_clause,[],[f1869,f522,f450,f531,f527]) ).
fof(f1895,plain,
( spl0_91
| ~ spl0_92
| ~ spl0_54
| spl0_159 ),
inference(avatar_split_clause,[],[f1851,f985,f420,f601,f597]) ).
fof(f1900,plain,
( ~ c2_1(a323)
| ~ c0_1(a323)
| ~ spl0_28
| spl0_99 ),
inference(resolution,[],[f314,f635]) ).
fof(f1909,plain,
( ~ spl0_101
| ~ spl0_100
| ~ spl0_28
| spl0_99 ),
inference(avatar_split_clause,[],[f1900,f634,f313,f639,f643]) ).
fof(f1916,plain,
( ~ c1_1(a333)
| c2_1(a333)
| ~ spl0_32
| spl0_90 ),
inference(resolution,[],[f330,f593]) ).
fof(f1919,plain,
( spl0_91
| ~ spl0_92
| ~ spl0_32
| spl0_90 ),
inference(avatar_split_clause,[],[f1916,f592,f329,f601,f597]) ).
fof(f1922,plain,
( c0_1(a294)
| c2_1(a294)
| ~ spl0_56
| spl0_150 ),
inference(resolution,[],[f434,f873]) ).
fof(f1938,plain,
( c0_1(a310)
| c1_1(a310)
| ~ spl0_58
| ~ spl0_116 ),
inference(resolution,[],[f441,f714]) ).
fof(f1940,plain,
( c0_1(a321)
| c1_1(a321)
| ~ spl0_58
| ~ spl0_103 ),
inference(resolution,[],[f441,f654]) ).
fof(f1941,plain,
( c0_1(a336)
| c1_1(a336)
| ~ spl0_58
| ~ spl0_89 ),
inference(resolution,[],[f441,f588]) ).
fof(f1945,plain,
( spl0_87
| spl0_88
| ~ spl0_58
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f1941,f587,f440,f583,f578]) ).
fof(f1946,plain,
( spl0_102
| spl0_168
| ~ spl0_58
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f1940,f653,f440,f1175,f648]) ).
fof(f1947,plain,
( spl0_161
| spl0_115
| ~ spl0_58
| ~ spl0_116 ),
inference(avatar_split_clause,[],[f1938,f713,f440,f709,f1028]) ).
fof(f1961,plain,
( spl0_157
| spl0_152
| ~ spl0_60
| spl0_150 ),
inference(avatar_split_clause,[],[f1862,f872,f450,f881,f961]) ).
fof(f1967,plain,
( spl0_151
| ~ spl0_157
| ~ spl0_54
| spl0_152 ),
inference(avatar_split_clause,[],[f1844,f881,f420,f961,f877]) ).
fof(f1968,plain,
( ~ spl0_122
| spl0_153
| ~ spl0_30
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f919,f737,f322,f889,f741]) ).
fof(f1977,plain,
( spl0_151
| spl0_152
| ~ spl0_56
| spl0_150 ),
inference(avatar_split_clause,[],[f1922,f872,f433,f881,f877]) ).
fof(f1984,plain,
( ~ c0_1(a299)
| ~ c1_1(a299)
| ~ spl0_22
| ~ spl0_142 ),
inference(resolution,[],[f291,f836]) ).
fof(f1993,plain,
( ~ spl0_169
| ~ spl0_143
| ~ spl0_22
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1984,f835,f290,f839,f1185]) ).
fof(f2009,plain,
( ~ c2_1(a297)
| ~ c1_1(a297)
| ~ spl0_25
| spl0_144 ),
inference(resolution,[],[f303,f845]) ).
fof(f2013,plain,
( ~ c2_1(a330)
| ~ c1_1(a330)
| ~ spl0_25
| spl0_93 ),
inference(resolution,[],[f303,f607]) ).
fof(f2019,plain,
( ~ spl0_95
| ~ spl0_94
| ~ spl0_25
| spl0_93 ),
inference(avatar_split_clause,[],[f2013,f606,f302,f611,f615]) ).
fof(f2023,definition,
( spl0_174
<=> c2_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f2025,plain,
( ~ spl0_146
| ~ spl0_174
| ~ spl0_25
| spl0_144 ),
inference(avatar_split_clause,[],[f2009,f844,f302,f2023,f853]) ).
fof(f2051,plain,
( c0_1(a308)
| ~ c1_1(a308)
| ~ spl0_55
| ~ spl0_121 ),
inference(resolution,[],[f430,f738]) ).
fof(f2061,plain,
( ~ spl0_122
| spl0_120
| ~ spl0_55
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f2051,f737,f429,f732,f741]) ).
fof(f2069,plain,
( ~ c1_1(a297)
| c0_1(a297)
| ~ spl0_51
| spl0_144 ),
inference(resolution,[],[f409,f845]) ).
fof(f2082,plain,
( spl0_145
| ~ spl0_146
| ~ spl0_51
| spl0_144 ),
inference(avatar_split_clause,[],[f2069,f844,f408,f853,f849]) ).
fof(f2095,plain,
( ~ c1_1(a320)
| c2_1(a320)
| ~ spl0_54
| spl0_106 ),
inference(resolution,[],[f421,f668]) ).
fof(f2101,plain,
( spl0_105
| ~ spl0_107
| ~ spl0_54
| spl0_106 ),
inference(avatar_split_clause,[],[f2095,f667,f420,f671,f662]) ).
fof(f2111,plain,
( c0_1(a297)
| c2_1(a297)
| ~ spl0_56
| spl0_144 ),
inference(resolution,[],[f434,f845]) ).
fof(f2116,plain,
( c0_1(a333)
| c2_1(a333)
| ~ spl0_56
| spl0_90 ),
inference(resolution,[],[f434,f593]) ).
fof(f2117,plain,
( c0_1(a338)
| c2_1(a338)
| ~ spl0_56
| spl0_84 ),
inference(resolution,[],[f434,f565]) ).
fof(f2118,plain,
( c0_1(a346)
| c2_1(a346)
| ~ spl0_56
| spl0_75 ),
inference(resolution,[],[f434,f523]) ).
fof(f2121,plain,
( spl0_170
| spl0_77
| ~ spl0_56
| spl0_75 ),
inference(avatar_split_clause,[],[f2118,f522,f433,f531,f1217]) ).
fof(f2122,plain,
( spl0_85
| spl0_158
| ~ spl0_56
| spl0_84 ),
inference(avatar_split_clause,[],[f2117,f564,f433,f968,f569]) ).
fof(f2123,plain,
( spl0_91
| spl0_159
| ~ spl0_56
| spl0_90 ),
inference(avatar_split_clause,[],[f2116,f592,f433,f985,f597]) ).
fof(f2124,plain,
( spl0_174
| spl0_145
| ~ spl0_56
| spl0_144 ),
inference(avatar_split_clause,[],[f2111,f844,f433,f849,f2023]) ).
fof(f2132,plain,
( c2_1(a310)
| c1_1(a310)
| ~ spl0_61
| spl0_115 ),
inference(resolution,[],[f456,f710]) ).
fof(f2142,plain,
( spl0_161
| spl0_114
| ~ spl0_61
| spl0_115 ),
inference(avatar_split_clause,[],[f2132,f709,f455,f704,f1028]) ).
fof(f2165,plain,
( ~ c1_1(a333)
| c2_1(a333)
| ~ spl0_44
| ~ spl0_159 ),
inference(resolution,[],[f1374,f381]) ).
fof(f2167,plain,
( spl0_91
| ~ spl0_92
| ~ spl0_44
| ~ spl0_159 ),
inference(avatar_split_clause,[],[f2165,f985,f380,f601,f597]) ).
cnf(s1,plain,
( spl0_1
| spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f227]) ).
cnf(s2,plain,
( spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f234]) ).
cnf(s3,plain,
( spl0_2
| spl0_5
| spl0_6 ),
inference(sat_conversion,[],[f238]) ).
cnf(s12,plain,
( spl0_1
| spl0_8
| ~ spl0_19
| spl0_25 ),
inference(sat_conversion,[],[f304]) ).
cnf(s14,plain,
( spl0_6
| ~ spl0_19
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f315]) ).
cnf(s17,plain,
( ~ spl0_19
| spl0_27
| spl0_30 ),
inference(sat_conversion,[],[f324]) ).
cnf(s18,plain,
( ~ spl0_19
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f331]) ).
cnf(s20,plain,
( ~ spl0_19
| spl0_22
| spl0_30
| spl0_32 ),
inference(sat_conversion,[],[f333]) ).
cnf(s21,plain,
( ~ spl0_19
| spl0_21
| spl0_33 ),
inference(sat_conversion,[],[f337]) ).
cnf(s23,plain,
( spl0_3
| spl0_6
| ~ spl0_19
| spl0_36 ),
inference(sat_conversion,[],[f348]) ).
cnf(s24,plain,
( spl0_2
| ~ spl0_19
| spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f352]) ).
cnf(s27,plain,
( spl0_4
| spl0_6
| ~ spl0_19
| spl0_40 ),
inference(sat_conversion,[],[f364]) ).
cnf(s29,plain,
( spl0_12
| ~ spl0_19
| spl0_32
| spl0_41 ),
inference(sat_conversion,[],[f369]) ).
cnf(s31,plain,
( spl0_4
| ~ spl0_19
| spl0_43 ),
inference(sat_conversion,[],[f377]) ).
cnf(s35,plain,
( ~ spl0_19
| spl0_45
| spl0_47
| spl0_48 ),
inference(sat_conversion,[],[f396]) ).
cnf(s36,plain,
( ~ spl0_19
| spl0_32
| spl0_34
| spl0_48 ),
inference(sat_conversion,[],[f397]) ).
cnf(s38,plain,
( spl0_2
| ~ spl0_19
| spl0_33
| spl0_49 ),
inference(sat_conversion,[],[f402]) ).
cnf(s41,plain,
( spl0_6
| spl0_13
| ~ spl0_19
| spl0_52 ),
inference(sat_conversion,[],[f414]) ).
cnf(s49,plain,
( ~ spl0_19
| spl0_51
| spl0_54
| spl0_55 ),
inference(sat_conversion,[],[f431]) ).
cnf(s50,plain,
( ~ spl0_19
| spl0_35
| spl0_54
| spl0_56 ),
inference(sat_conversion,[],[f435]) ).
cnf(s51,plain,
( ~ spl0_19
| spl0_47
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f442]) ).
cnf(s52,plain,
( ~ spl0_19
| spl0_30
| spl0_47
| spl0_58 ),
inference(sat_conversion,[],[f443]) ).
cnf(s53,plain,
( spl0_14
| ~ spl0_19
| spl0_35
| spl0_59 ),
inference(sat_conversion,[],[f447]) ).
cnf(s54,plain,
( ~ spl0_19
| spl0_25
| spl0_54
| spl0_59 ),
inference(sat_conversion,[],[f448]) ).
cnf(s56,plain,
( ~ spl0_19
| spl0_48
| spl0_56
| spl0_60 ),
inference(sat_conversion,[],[f453]) ).
cnf(s57,plain,
( ~ spl0_19
| spl0_44
| spl0_47
| spl0_61 ),
inference(sat_conversion,[],[f457]) ).
cnf(s60,plain,
( ~ spl0_19
| spl0_49
| spl0_56
| spl0_61 ),
inference(sat_conversion,[],[f463]) ).
cnf(s73,plain,
( ~ spl0_5
| ~ spl0_72 ),
inference(sat_conversion,[],[f511]) ).
cnf(s74,plain,
( ~ spl0_5
| ~ spl0_73 ),
inference(sat_conversion,[],[f515]) ).
cnf(s75,plain,
( ~ spl0_5
| spl0_74 ),
inference(sat_conversion,[],[f519]) ).
cnf(s77,plain,
( ~ spl0_1
| ~ spl0_75 ),
inference(sat_conversion,[],[f525]) ).
cnf(s78,plain,
( ~ spl0_1
| ~ spl0_76 ),
inference(sat_conversion,[],[f529]) ).
cnf(s79,plain,
( ~ spl0_1
| ~ spl0_77 ),
inference(sat_conversion,[],[f533]) ).
cnf(s80,plain,
( ~ spl0_1
| spl0_19 ),
inference(sat_conversion,[],[f534]) ).
cnf(s89,plain,
( ~ spl0_31
| ~ spl0_84 ),
inference(sat_conversion,[],[f567]) ).
cnf(s90,plain,
( ~ spl0_31
| ~ spl0_85 ),
inference(sat_conversion,[],[f571]) ).
cnf(s91,plain,
( ~ spl0_31
| ~ spl0_86 ),
inference(sat_conversion,[],[f575]) ).
cnf(s93,plain,
( ~ spl0_21
| ~ spl0_87 ),
inference(sat_conversion,[],[f581]) ).
cnf(s94,plain,
( ~ spl0_21
| ~ spl0_88 ),
inference(sat_conversion,[],[f585]) ).
cnf(s95,plain,
( ~ spl0_21
| spl0_89 ),
inference(sat_conversion,[],[f589]) ).
cnf(s97,plain,
( ~ spl0_3
| ~ spl0_90 ),
inference(sat_conversion,[],[f595]) ).
cnf(s98,plain,
( ~ spl0_3
| ~ spl0_91 ),
inference(sat_conversion,[],[f599]) ).
cnf(s99,plain,
( ~ spl0_3
| spl0_92 ),
inference(sat_conversion,[],[f603]) ).
cnf(s100,plain,
( ~ spl0_3
| spl0_19 ),
inference(sat_conversion,[],[f604]) ).
cnf(s101,plain,
( ~ spl0_37
| ~ spl0_93 ),
inference(sat_conversion,[],[f609]) ).
cnf(s102,plain,
( ~ spl0_37
| spl0_94 ),
inference(sat_conversion,[],[f613]) ).
cnf(s103,plain,
( ~ spl0_37
| spl0_95 ),
inference(sat_conversion,[],[f617]) ).
cnf(s109,plain,
( ~ spl0_12
| ~ spl0_99 ),
inference(sat_conversion,[],[f637]) ).
cnf(s110,plain,
( ~ spl0_12
| spl0_100 ),
inference(sat_conversion,[],[f641]) ).
cnf(s111,plain,
( ~ spl0_12
| spl0_101 ),
inference(sat_conversion,[],[f645]) ).
cnf(s113,plain,
( ~ spl0_4
| ~ spl0_102 ),
inference(sat_conversion,[],[f651]) ).
cnf(s114,plain,
( ~ spl0_4
| spl0_103 ),
inference(sat_conversion,[],[f655]) ).
cnf(s115,plain,
( ~ spl0_4
| spl0_104 ),
inference(sat_conversion,[],[f659]) ).
cnf(s117,plain,
( ~ spl0_8
| ~ spl0_105 ),
inference(sat_conversion,[],[f665]) ).
cnf(s118,plain,
( ~ spl0_8
| ~ spl0_106 ),
inference(sat_conversion,[],[f669]) ).
cnf(s119,plain,
( ~ spl0_8
| spl0_107 ),
inference(sat_conversion,[],[f673]) ).
cnf(s121,plain,
( ~ spl0_45
| ~ spl0_108 ),
inference(sat_conversion,[],[f679]) ).
cnf(s122,plain,
( ~ spl0_45
| spl0_109 ),
inference(sat_conversion,[],[f683]) ).
cnf(s123,plain,
( ~ spl0_45
| spl0_110 ),
inference(sat_conversion,[],[f687]) ).
cnf(s129,plain,
( ~ spl0_2
| ~ spl0_114 ),
inference(sat_conversion,[],[f707]) ).
cnf(s130,plain,
( ~ spl0_2
| ~ spl0_115 ),
inference(sat_conversion,[],[f711]) ).
cnf(s131,plain,
( ~ spl0_2
| spl0_116 ),
inference(sat_conversion,[],[f715]) ).
cnf(s132,plain,
( ~ spl0_2
| spl0_19 ),
inference(sat_conversion,[],[f716]) ).
cnf(s133,plain,
( ~ spl0_6
| ~ spl0_117 ),
inference(sat_conversion,[],[f721]) ).
cnf(s134,plain,
( ~ spl0_6
| spl0_118 ),
inference(sat_conversion,[],[f725]) ).
cnf(s135,plain,
( ~ spl0_6
| spl0_119 ),
inference(sat_conversion,[],[f729]) ).
cnf(s137,plain,
( ~ spl0_13
| ~ spl0_120 ),
inference(sat_conversion,[],[f735]) ).
cnf(s138,plain,
( ~ spl0_13
| spl0_121 ),
inference(sat_conversion,[],[f739]) ).
cnf(s139,plain,
( ~ spl0_13
| spl0_122 ),
inference(sat_conversion,[],[f743]) ).
cnf(s165,plain,
( ~ spl0_34
| ~ spl0_141 ),
inference(sat_conversion,[],[f833]) ).
cnf(s166,plain,
( ~ spl0_34
| spl0_142 ),
inference(sat_conversion,[],[f837]) ).
cnf(s167,plain,
( ~ spl0_34
| spl0_143 ),
inference(sat_conversion,[],[f841]) ).
cnf(s169,plain,
( ~ spl0_57
| ~ spl0_144 ),
inference(sat_conversion,[],[f847]) ).
cnf(s170,plain,
( ~ spl0_57
| ~ spl0_145 ),
inference(sat_conversion,[],[f851]) ).
cnf(s171,plain,
( ~ spl0_57
| spl0_146 ),
inference(sat_conversion,[],[f855]) ).
cnf(s173,plain,
( ~ spl0_14
| ~ spl0_147 ),
inference(sat_conversion,[],[f861]) ).
cnf(s174,plain,
( ~ spl0_14
| spl0_148 ),
inference(sat_conversion,[],[f865]) ).
cnf(s175,plain,
( ~ spl0_14
| spl0_149 ),
inference(sat_conversion,[],[f869]) ).
cnf(s177,plain,
( ~ spl0_47
| ~ spl0_150 ),
inference(sat_conversion,[],[f875]) ).
cnf(s178,plain,
( ~ spl0_47
| ~ spl0_151 ),
inference(sat_conversion,[],[f879]) ).
cnf(s179,plain,
( ~ spl0_47
| ~ spl0_152 ),
inference(sat_conversion,[],[f883]) ).
cnf(s193,plain,
( ~ spl0_33
| spl0_72
| spl0_73
| ~ spl0_74 ),
inference(sat_conversion,[],[f981]) ).
cnf(s195,plain,
( ~ spl0_33
| spl0_90
| spl0_91
| ~ spl0_159 ),
inference(sat_conversion,[],[f987]) ).
cnf(s200,plain,
( ~ spl0_35
| spl0_87
| ~ spl0_89
| ~ spl0_160 ),
inference(sat_conversion,[],[f1010]) ).
cnf(s212,plain,
( ~ spl0_41
| spl0_84
| spl0_86
| ~ spl0_158 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s214,plain,
( ~ spl0_43
| spl0_87
| ~ spl0_89
| spl0_160 ),
inference(sat_conversion,[],[f1112]) ).
cnf(s227,plain,
( ~ spl0_48
| spl0_88
| ~ spl0_89
| ~ spl0_160 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s228,plain,
( ~ spl0_48
| ~ spl0_103
| ~ spl0_104
| spl0_168 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s231,plain,
( ~ spl0_30
| spl0_141
| ~ spl0_142
| ~ spl0_169 ),
inference(sat_conversion,[],[f1190]) ).
cnf(s232,plain,
( ~ spl0_43
| spl0_141
| ~ spl0_142
| spl0_169 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s250,plain,
( ~ spl0_32
| spl0_150
| spl0_151
| ~ spl0_157 ),
inference(sat_conversion,[],[f1241]) ).
cnf(s260,plain,
( ~ spl0_40
| spl0_75
| spl0_76
| ~ spl0_170 ),
inference(sat_conversion,[],[f1293]) ).
cnf(s321,plain,
( ~ spl0_52
| spl0_88
| ~ spl0_89
| spl0_160 ),
inference(sat_conversion,[],[f1466]) ).
cnf(s332,plain,
( ~ spl0_59
| spl0_76
| spl0_77
| ~ spl0_170 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s334,plain,
( ~ spl0_59
| spl0_87
| spl0_88
| ~ spl0_160 ),
inference(sat_conversion,[],[f1520]) ).
cnf(s383,plain,
( ~ spl0_36
| spl0_147
| ~ spl0_148
| ~ spl0_149 ),
inference(sat_conversion,[],[f1617]) ).
cnf(s385,plain,
( ~ spl0_49
| spl0_120
| ~ spl0_122
| ~ spl0_153 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s416,plain,
( ~ spl0_35
| spl0_102
| ~ spl0_103
| ~ spl0_104 ),
inference(sat_conversion,[],[f1726]) ).
cnf(s455,plain,
( ~ spl0_30
| spl0_114
| ~ spl0_116
| ~ spl0_161 ),
inference(sat_conversion,[],[f1786]) ).
cnf(s456,plain,
( ~ spl0_30
| spl0_117
| ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f1787]) ).
cnf(s463,plain,
( ~ spl0_49
| spl0_108
| ~ spl0_109
| ~ spl0_110 ),
inference(sat_conversion,[],[f1815]) ).
cnf(s469,plain,
( ~ spl0_27
| ~ spl0_103
| ~ spl0_104
| ~ spl0_168 ),
inference(sat_conversion,[],[f1830]) ).
cnf(s472,plain,
( ~ spl0_52
| spl0_114
| spl0_115
| ~ spl0_116 ),
inference(sat_conversion,[],[f1842]) ).
cnf(s477,plain,
( ~ spl0_60
| spl0_75
| spl0_76
| spl0_77 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s499,plain,
( ~ spl0_54
| spl0_91
| ~ spl0_92
| spl0_159 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s502,plain,
( ~ spl0_28
| spl0_99
| ~ spl0_100
| ~ spl0_101 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s503,plain,
( ~ spl0_32
| spl0_90
| spl0_91
| ~ spl0_92 ),
inference(sat_conversion,[],[f1919]) ).
cnf(s507,plain,
( ~ spl0_58
| spl0_87
| spl0_88
| ~ spl0_89 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s508,plain,
( ~ spl0_58
| spl0_102
| ~ spl0_103
| spl0_168 ),
inference(sat_conversion,[],[f1946]) ).
cnf(s509,plain,
( ~ spl0_58
| spl0_115
| ~ spl0_116
| spl0_161 ),
inference(sat_conversion,[],[f1947]) ).
cnf(s527,plain,
( ~ spl0_60
| spl0_150
| spl0_152
| spl0_157 ),
inference(sat_conversion,[],[f1961]) ).
cnf(s533,plain,
( ~ spl0_54
| spl0_151
| spl0_152
| ~ spl0_157 ),
inference(sat_conversion,[],[f1967]) ).
cnf(s534,plain,
( ~ spl0_30
| ~ spl0_121
| ~ spl0_122
| spl0_153 ),
inference(sat_conversion,[],[f1968]) ).
cnf(s543,plain,
( ~ spl0_56
| spl0_150
| spl0_151
| spl0_152 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s550,plain,
( ~ spl0_22
| ~ spl0_142
| ~ spl0_143
| ~ spl0_169 ),
inference(sat_conversion,[],[f1993]) ).
cnf(s552,plain,
( ~ spl0_25
| spl0_93
| ~ spl0_94
| ~ spl0_95 ),
inference(sat_conversion,[],[f2019]) ).
cnf(s554,plain,
( ~ spl0_25
| spl0_144
| ~ spl0_146
| ~ spl0_174 ),
inference(sat_conversion,[],[f2025]) ).
cnf(s558,plain,
( ~ spl0_55
| spl0_120
| ~ spl0_121
| ~ spl0_122 ),
inference(sat_conversion,[],[f2061]) ).
cnf(s564,plain,
( ~ spl0_51
| spl0_144
| spl0_145
| ~ spl0_146 ),
inference(sat_conversion,[],[f2082]) ).
cnf(s568,plain,
( ~ spl0_54
| spl0_105
| spl0_106
| ~ spl0_107 ),
inference(sat_conversion,[],[f2101]) ).
cnf(s573,plain,
( ~ spl0_56
| spl0_75
| spl0_77
| spl0_170 ),
inference(sat_conversion,[],[f2121]) ).
cnf(s574,plain,
( ~ spl0_56
| spl0_84
| spl0_85
| spl0_158 ),
inference(sat_conversion,[],[f2122]) ).
cnf(s575,plain,
( ~ spl0_56
| spl0_90
| spl0_91
| spl0_159 ),
inference(sat_conversion,[],[f2123]) ).
cnf(s576,plain,
( ~ spl0_56
| spl0_144
| spl0_145
| spl0_174 ),
inference(sat_conversion,[],[f2124]) ).
cnf(s579,plain,
( ~ spl0_61
| spl0_114
| spl0_115
| spl0_161 ),
inference(sat_conversion,[],[f2142]) ).
cnf(s585,plain,
( ~ spl0_44
| spl0_91
| ~ spl0_92
| ~ spl0_159 ),
inference(sat_conversion,[],[f2167]) ).
cnf(s586,plain,
( spl0_4
| ~ spl0_3 ),
inference(rat,[],[s20,s550,s231,s232,s165,s166,s167,s36,s227,s214,s93,s94,s95,s21,s193,s73,s74,s75,s2,s31,s100,s503,s97,s98,s99]) ).
cnf(s587,plain,
( spl0_59
| spl0_2
| spl0_1 ),
inference(rat,[],[s568,s117,s118,s119,s12,s54,s552,s101,s102,s103,s24,s383,s173,s174,s175,s53,s100,s416,s113,s114,s115,s586,s1]) ).
cnf(s588,plain,
( ~ spl0_47
| ~ spl0_56 ),
inference(rat,[],[s543,s177,s178,s179]) ).
cnf(s589,plain,
( ~ spl0_14
| ~ spl0_36 ),
inference(rat,[],[s383,s173,s174,s175]) ).
cnf(s590,plain,
( ~ spl0_45
| ~ spl0_49 ),
inference(rat,[],[s463,s121,s122,s123]) ).
cnf(s591,plain,
( ~ spl0_56
| spl0_45
| spl0_58
| ~ spl0_3 ),
inference(rat,[],[s456,s133,s134,s135,s14,s469,s228,s35,s52,s588,s502,s109,s110,s111,s29,s212,s574,s91,s90,s89,s18,s503,s97,s98,s99,s100,s115,s114,s586]) ).
cnf(s592,plain,
( ~ spl0_6
| ~ spl0_30 ),
inference(rat,[],[s456,s133,s134,s135]) ).
cnf(s593,plain,
( ~ spl0_30
| spl0_52
| ~ spl0_49
| ~ spl0_19 ),
inference(rat,[],[s385,s534,s137,s138,s139,s41,s592]) ).
cnf(s594,plain,
( spl0_33
| ~ spl0_59
| ~ spl0_3
| spl0_2 ),
inference(rat,[],[s527,s56,s533,s228,s177,s178,s179,s469,s52,s17,s593,s50,s591,s590,s321,s334,s507,s93,s94,s95,s21,s38,s100,s416,s113,s114,s115,s586]) ).
cnf(s595,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s50,s575,s499,s195,s594,s587,s416,s113,s114,s115,s586,s97,s98,s99,s100,s1]) ).
cnf(s596,plain,
( ~ spl0_56
| spl0_58
| ~ spl0_3
| ~ spl0_2 ),
inference(rat,[],[s579,s455,s57,s52,s585,s588,s575,s132,s131,s130,s129,s99,s98,s97]) ).
cnf(s597,plain,
( ~ spl0_30
| spl0_56
| ~ spl0_2 ),
inference(rat,[],[s579,s60,s455,s593,s132,s472,s129,s130,s131]) ).
cnf(s598,plain,
( spl0_58
| ~ spl0_3
| ~ spl0_2 ),
inference(rat,[],[s527,s56,s533,s228,s177,s178,s179,s469,s52,s17,s597,s50,s596,s132,s416,s113,s114,s115,s586]) ).
cnf(s599,plain,
( ~ spl0_3
| ~ spl0_2 ),
inference(rat,[],[s17,s469,s455,s508,s509,s598,s113,s114,s115,s586,s132,s131,s130,s129]) ).
cnf(s600,plain,
( ~ spl0_30
| spl0_1 ),
inference(rat,[],[s568,s117,s118,s119,s12,s49,s554,s564,s576,s169,s170,s171,s558,s51,s137,s138,s139,s588,s509,s41,s597,s455,s592,s132,s472,s129,s130,s131,s595]) ).
cnf(s601,plain,
( ~ spl0_21
| ~ spl0_58 ),
inference(rat,[],[s507,s93,s94,s95]) ).
cnf(s602,plain,
( ~ spl0_5
| ~ spl0_33 ),
inference(rat,[],[s193,s73,s74,s75]) ).
cnf(s603,plain,
( ~ spl0_103
| spl0_102
| ~ spl0_104
| ~ spl0_58
| ~ spl0_27 ),
inference(rat,[],[s508,s469]) ).
cnf(s604,plain,
( ~ spl0_58
| spl0_1 ),
inference(rat,[],[s114,s603,s113,s115,s2,s602,s21,s601,s17,s600,s132,s595]) ).
cnf(s605,plain,
( ~ spl0_104
| ~ spl0_103
| spl0_1 ),
inference(rat,[],[s31,s232,s113,s550,s416,s165,s166,s167,s50,s36,s20,s533,s250,s527,s56,s228,s469,s17,s179,s178,s177,s588,s52,s604,s132,s595,s600]) ).
cnf(s606,plain,
( spl0_4
| spl0_1 ),
inference(rat,[],[s527,s533,s56,s50,s227,s200,s214,s93,s94,s95,s21,s602,s2,s31,s179,s178,s177,s588,s52,s604,s132,s595,s600]) ).
cnf(s607,plain,
spl0_1,
inference(rat,[],[s605,s114,s115,s606]) ).
cnf(s608,plain,
spl0_19,
inference(rat,[],[s80,s607]) ).
cnf(s609,plain,
~ spl0_77,
inference(rat,[],[s79,s607]) ).
cnf(s610,plain,
~ spl0_76,
inference(rat,[],[s78,s607]) ).
cnf(s611,plain,
~ spl0_75,
inference(rat,[],[s77,s607]) ).
cnf(s612,plain,
~ spl0_60,
inference(rat,[],[s477,s609,s610,s611]) ).
cnf(s613,plain,
( ~ spl0_3
| ~ spl0_56 ),
inference(rat,[],[s591,s601,s590,s21,s38,s195,s575,s599,s97,s98,s608]) ).
cnf(s614,plain,
( spl0_6
| ~ spl0_56 ),
inference(rat,[],[s53,s416,s589,s113,s114,s115,s23,s27,s332,s260,s573,s613,s608,s611,s610,s609]) ).
cnf(s615,plain,
~ spl0_56,
inference(rat,[],[s603,s113,s114,s115,s2,s602,s21,s601,s52,s17,s592,s614,s588,s608]) ).
cnf(s616,plain,
spl0_48,
inference(rat,[],[s56,s612,s608,s615]) ).
cnf(s617,plain,
( ~ spl0_52
| spl0_88
| ~ spl0_89 ),
inference(rat,[],[s227,s321,s616]) ).
cnf(s618,plain,
~ spl0_30,
inference(rat,[],[s617,s94,s95,s593,s21,s38,s602,s3,s597,s592,s608,s615]) ).
cnf(s619,plain,
spl0_27,
inference(rat,[],[s17,s608,s618]) ).
cnf(s620,plain,
( ~ spl0_104
| ~ spl0_103 ),
inference(rat,[],[s228,s469,s619,s616]) ).
cnf(s621,plain,
spl0_4,
inference(rat,[],[s227,s214,s93,s94,s95,s21,s602,s2,s31,s616,s608]) ).
cnf(s622,plain,
spl0_104,
inference(rat,[],[s115,s621]) ).
cnf(s623,plain,
spl0_103,
inference(rat,[],[s114,s621]) ).
cnf(s625,plain,
$false,
inference(rat,[],[s620,s623,s622]) ).
fof(f2168,plain,
$false,
inference(avatar_sat_refutation,[],[s625]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN445+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n009.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 16:04:04 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.23 Running first-order theorem proving
% 0.07/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.30/1.13 % (3186147)Detected formulas, will run a generic FOF schedule.
% 1.30/1.13 % (3186152)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2613682185:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 1.30/1.13 % (3186156)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3862379510:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 1.30/1.13 % (3186154)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1452629088:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 1.30/1.13 % (3186155)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1223118988:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 1.30/1.13 % (3186157)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=967059035:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 1.30/1.13 % (3186153)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1201848692:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 1.30/1.13 % (3186158)dis-21_1_sil=8000:lcm=predicate:random_seed=3765309476:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 1.30/1.13 % (3186158)First to succeed.
% 1.30/1.13 % (3186158)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3186147"
% 1.30/1.13 % (3186157)Also succeeded, but the first one will report.
% 1.30/1.13 % (3186155)Also succeeded, but the first one will report.
% 1.30/1.13 % (3186156)Instruction limit reached!
% 1.30/1.13 % (3186156)------------------------------
% 1.30/1.13 % (3186156)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.30/1.13 % (3186156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.30/1.13 % (3186156)CaDiCaL version: 2.1.3
% 1.30/1.13 % (3186156)Termination reason: Instruction limit
% 1.30/1.13 % (3186156)Termination phase: Saturation
% 1.30/1.13 % (3186156)Time elapsed: 0.059 s
% 1.30/1.13 % (3186156)Peak memory usage: 87 MB
% 1.30/1.13 % (3186156)Instructions burned: 121 (million)
% 1.30/1.13 % (3186166)lrs+10_1_sil=8000:sp=occurrence:random_seed=4010971634:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 1.30/1.13 % (3186166)Also succeeded, but the first one will report.
% 1.30/1.13 % (3186158)Refutation found. Thanks to Tanya!
% 1.30/1.13 % SZS status Theorem for theBenchmark
% 1.30/1.13 % SZS output start Proof for theBenchmark
% See solution above
% 3.92/1.32 % (3186158)------------------------------
% 3.92/1.32 % (3186158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.92/1.32 % (3186158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.32 % (3186158)CaDiCaL version: 2.1.3
% 3.92/1.32 % (3186158)Termination reason: Refutation
% 3.92/1.32 % (3186158)Time elapsed: 0.031 s
% 3.92/1.32 % (3186158)Peak memory usage: 90 MB
% 3.92/1.32 % (3186158)Instructions burned: 51 (million)
% 3.92/1.32 % (3186158)------------------------------
% 3.92/1.32 % (3186158)------------------------------
% 3.92/1.32 % (3186147)Success in time 0.462 s
% 3.92/1.32 % Vampire exiting
%------------------------------------------------------------------------------