%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN445+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:08:35 PM UTC 2026
% Result : Theorem 0.08s 0.19s
% Output : Refutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 110
% Syntax : Number of formulae : 695 ( 17 unt; 109 def)
% Number of atoms : 5313 ( 0 equ)
% Maximal formula atoms : 606 ( 7 avg)
% Number of connectives : 7092 (2474 ~;3332 |; 895 &)
% ( 109 <=>; 282 =>; 0 <=; 0 <~>)
% Maximal formula depth : 97 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 145 ( 144 usr; 141 prp; 0-1 aty)
% Number of functors : 30 ( 30 usr; 30 con; 0-0 aty)
% Number of variables : 653 ( 0 sgn 653 !; 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/sandbox/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(f13,plain,
! [X93] :
( ~ c1_1(X93)
| ~ c2_1(X93)
| ~ c3_1(X93)
| ~ ndr1_0
| hskp28 ),
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(f21,plain,
! [X83] :
( c3_1(X83)
| ~ c0_1(X83)
| ~ c1_1(X83)
| ~ ndr1_0
| hskp17
| hskp4 ),
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(f24,plain,
! [X78,X79] :
( c2_1(X78)
| c3_1(X78)
| ~ c1_1(X78)
| ~ ndr1_0
| ~ c0_1(X79)
| ~ c1_1(X79)
| ~ c3_1(X79)
| ~ ndr1_0
| hskp17 ),
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(f31,plain,
! [X68,X69] :
( c1_1(X68)
| ~ c0_1(X68)
| ~ c2_1(X68)
| ~ ndr1_0
| c1_1(X69)
| ~ c0_1(X69)
| ~ c3_1(X69)
| ~ ndr1_0
| hskp4 ),
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(f42,plain,
! [X50,X51] :
( c0_1(X50)
| ~ c1_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0
| c3_1(X51)
| ~ c0_1(X51)
| ~ c1_1(X51)
| ~ ndr1_0
| hskp13 ),
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(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(f60,plain,
! [X16,X14,X15] :
( c0_1(X14)
| c1_1(X14)
| c3_1(X14)
| ~ ndr1_0
| c0_1(X15)
| c2_1(X15)
| ~ c1_1(X15)
| ~ ndr1_0
| c3_1(X16)
| ~ c0_1(X16)
| ~ c2_1(X16)
| ~ 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(f70,plain,
( ~ hskp28
| c3_1(a353) ),
inference(cnf_transformation,[],[f5]) ).
fof(f71,plain,
( ~ hskp28
| c2_1(a353) ),
inference(cnf_transformation,[],[f5]) ).
fof(f72,plain,
( ~ hskp28
| c1_1(a353) ),
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(f130,plain,
( ~ hskp13
| ~ c1_1(a313) ),
inference(cnf_transformation,[],[f5]) ).
fof(f131,plain,
( ~ hskp13
| c3_1(a313) ),
inference(cnf_transformation,[],[f5]) ).
fof(f132,plain,
( ~ hskp13
| c0_1(a313) ),
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(f143,plain,
( ~ hskp10
| c3_1(a308) ),
inference(cnf_transformation,[],[f5]) ).
fof(f144,plain,
( ~ hskp10
| c1_1(a308) ),
inference(cnf_transformation,[],[f5]) ).
fof(f166,plain,
( ~ hskp4
| ~ c2_1(a300) ),
inference(cnf_transformation,[],[f5]) ).
fof(f167,plain,
( ~ hskp4
| ~ c1_1(a300) ),
inference(cnf_transformation,[],[f5]) ).
fof(f168,plain,
( ~ hskp4
| ~ c0_1(a300) ),
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,
( hskp0
| c0_1(a294) ),
inference(consistent_polarity_flipping,[],[f184]) ).
fof(f188,plain,
( hskp0
| ~ c2_1(a294) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f189,plain,
( hskp0
| c3_1(a294) ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f190,plain,
( ~ hskp1
| ~ c0_1(a295) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f191,plain,
( ~ hskp1
| c1_1(a295) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f192,plain,
( ~ hskp2
| ~ c1_1(a297) ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f193,plain,
( ~ hskp2
| c0_1(a297) ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f194,plain,
( ~ hskp2
| c3_1(a297) ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f197,plain,
( ~ hskp4
| c0_1(a300) ),
inference(consistent_polarity_flipping,[],[f168]) ).
fof(f198,plain,
( ~ hskp4
| c1_1(a300) ),
inference(consistent_polarity_flipping,[],[f167]) ).
fof(f212,plain,
( ~ hskp10
| ~ c1_1(a308) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f213,plain,
( ~ hskp10
| ~ c3_1(a308) ),
inference(consistent_polarity_flipping,[],[f143]) ).
fof(f216,plain,
( hskp11
| ~ c1_1(a309) ),
inference(consistent_polarity_flipping,[],[f140]) ).
fof(f217,plain,
( hskp11
| ~ c3_1(a309) ),
inference(consistent_polarity_flipping,[],[f139]) ).
fof(f218,plain,
( hskp11
| ~ c2_1(a309) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f219,plain,
( hskp12
| ndr1_0 ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f220,plain,
( hskp12
| ~ c3_1(a310) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f221,plain,
( hskp12
| c0_1(a310) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f222,plain,
( hskp12
| ~ c2_1(a310) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f223,plain,
( ~ hskp13
| ~ c0_1(a313) ),
inference(consistent_polarity_flipping,[],[f132]) ).
fof(f224,plain,
( ~ hskp13
| ~ c3_1(a313) ),
inference(consistent_polarity_flipping,[],[f131]) ).
fof(f225,plain,
( ~ hskp13
| c1_1(a313) ),
inference(consistent_polarity_flipping,[],[f130]) ).
fof(f227,plain,
( hskp14
| ~ c1_1(a315) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f228,plain,
( hskp14
| c2_1(a315) ),
inference(consistent_polarity_flipping,[],[f127]) ).
fof(f229,plain,
( hskp14
| c0_1(a315) ),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f231,plain,
( hskp15
| ~ c1_1(a320) ),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f232,plain,
( hskp15
| c0_1(a320) ),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f233,plain,
( hskp15
| ~ c2_1(a320) ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f234,plain,
( ~ hskp16
| ~ c3_1(a321) ),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f235,plain,
( ~ hskp16
| c1_1(a321) ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f237,plain,
( hskp17
| ~ c0_1(a323) ),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f238,plain,
( hskp17
| c2_1(a323) ),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f239,plain,
( hskp17
| c3_1(a323) ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f244,plain,
( ~ hskp19
| ~ c1_1(a330) ),
inference(consistent_polarity_flipping,[],[f108]) ).
fof(f245,plain,
( ~ hskp19
| c3_1(a330) ),
inference(consistent_polarity_flipping,[],[f106]) ).
fof(f246,plain,
( ~ hskp20
| ~ c1_1(a333) ),
inference(consistent_polarity_flipping,[],[f104]) ).
fof(f247,plain,
( ~ hskp20
| c3_1(a333) ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f249,plain,
( hskp21
| ~ c3_1(a336) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f250,plain,
( hskp21
| c0_1(a336) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f251,plain,
( hskp21
| c1_1(a336) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f252,plain,
( ~ hskp22
| c1_1(a338) ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f253,plain,
( ~ hskp22
| c3_1(a338) ),
inference(consistent_polarity_flipping,[],[f94]) ).
fof(f262,plain,
( ~ hskp25
| c0_1(a346) ),
inference(consistent_polarity_flipping,[],[f84]) ).
fof(f263,plain,
( ~ hskp25
| c1_1(a346) ),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f264,plain,
( ~ hskp25
| c3_1(a346) ),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f265,plain,
( ~ hskp26
| ~ c0_1(a349) ),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f266,plain,
( ~ hskp26
| c3_1(a349) ),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f269,plain,
( ~ hskp28
| ~ c1_1(a353) ),
inference(consistent_polarity_flipping,[],[f72]) ).
fof(f270,plain,
( ~ hskp28
| ~ c3_1(a353) ),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f273,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(consistent_polarity_flipping,[],[f65]) ).
fof(f276,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(consistent_polarity_flipping,[],[f62]) ).
fof(f277,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(consistent_polarity_flipping,[],[f61]) ).
fof(f278,plain,
! [X16,X14,X15] :
( ~ c0_1(X14)
| ~ c1_1(X14)
| ~ c3_1(X14)
| ~ ndr1_0
| ~ c0_1(X15)
| c2_1(X15)
| c1_1(X15)
| ~ ndr1_0
| ~ c3_1(X16)
| c0_1(X16)
| ~ c2_1(X16)
| ~ ndr1_0 ),
inference(consistent_polarity_flipping,[],[f60]) ).
fof(f279,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(consistent_polarity_flipping,[],[f59]) ).
fof(f280,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(consistent_polarity_flipping,[],[f58]) ).
fof(f281,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(consistent_polarity_flipping,[],[f57]) ).
fof(f282,plain,
! [X24] :
( ~ c0_1(X24)
| ~ c1_1(X24)
| c3_1(X24)
| ~ ndr1_0
| hskp2
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f56]) ).
fof(f283,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(consistent_polarity_flipping,[],[f55]) ).
fof(f292,plain,
! [X43] :
( ~ c0_1(X43)
| c2_1(X43)
| c3_1(X43)
| ~ ndr1_0
| hskp10
| ~ hskp11 ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f295,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(consistent_polarity_flipping,[],[f43]) ).
fof(f296,plain,
! [X50,X51] :
( ~ c0_1(X50)
| c1_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0
| ~ c3_1(X51)
| c0_1(X51)
| c1_1(X51)
| ~ ndr1_0
| hskp13 ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f298,plain,
! [X54] :
( ~ c0_1(X54)
| ~ c2_1(X54)
| c3_1(X54)
| ~ ndr1_0
| ~ hskp14
| ~ hskp0 ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f302,plain,
! [X60] :
( ~ c1_1(X60)
| c2_1(X60)
| c3_1(X60)
| ~ ndr1_0
| hskp16 ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f304,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(consistent_polarity_flipping,[],[f34]) ).
fof(f306,plain,
! [X67] :
( ~ c1_1(X67)
| ~ c3_1(X67)
| ~ c2_1(X67)
| ~ ndr1_0
| ~ hskp11
| hskp16 ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f307,plain,
! [X68,X69] :
( ~ c1_1(X68)
| c0_1(X68)
| ~ c2_1(X68)
| ~ ndr1_0
| ~ c1_1(X69)
| c0_1(X69)
| c3_1(X69)
| ~ ndr1_0
| hskp4 ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f309,plain,
! [X71] :
( ~ c1_1(X71)
| c0_1(X71)
| ~ c2_1(X71)
| ~ ndr1_0
| hskp19
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f310,plain,
! [X72] :
( ~ c1_1(X72)
| c0_1(X72)
| ~ c2_1(X72)
| ~ ndr1_0
| ~ hskp11
| hskp20 ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f312,plain,
! [X74] :
( c2_1(X74)
| ~ c3_1(X74)
| c0_1(X74)
| ~ ndr1_0
| ~ hskp21 ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f314,plain,
! [X78,X79] :
( c2_1(X78)
| ~ c3_1(X78)
| c1_1(X78)
| ~ ndr1_0
| c0_1(X79)
| c1_1(X79)
| c3_1(X79)
| ~ ndr1_0
| ~ hskp17 ),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f315,plain,
! [X80] :
( c2_1(X80)
| ~ c3_1(X80)
| c1_1(X80)
| ~ ndr1_0
| hskp22 ),
inference(consistent_polarity_flipping,[],[f23]) ).
fof(f316,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(consistent_polarity_flipping,[],[f22]) ).
fof(f317,plain,
! [X83] :
( ~ c3_1(X83)
| c0_1(X83)
| c1_1(X83)
| ~ ndr1_0
| ~ hskp17
| hskp4 ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f319,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(consistent_polarity_flipping,[],[f19]) ).
fof(f321,plain,
! [X89] :
( ~ c3_1(X89)
| c1_1(X89)
| ~ c2_1(X89)
| ~ ndr1_0
| ~ hskp15
| hskp25 ),
inference(consistent_polarity_flipping,[],[f17]) ).
fof(f325,plain,
! [X93] :
( c1_1(X93)
| ~ c2_1(X93)
| c3_1(X93)
| ~ ndr1_0
| hskp28 ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f329,plain,
( hskp26
| ~ hskp11
| ~ hskp12 ),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f330,plain,
( hskp20
| ~ hskp12
| hskp25 ),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f332,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,[],[f319]) ).
fof(f333,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,[],[f316]) ).
fof(f334,plain,
! [X78,X79] :
( c2_1(X78)
| ~ c3_1(X78)
| c1_1(X78)
| ~ ndr1_0
| c0_1(X79)
| c1_1(X79)
| c3_1(X79)
| ~ hskp17 ),
inference(duplicate_literal_removal,[],[f314]) ).
fof(f336,plain,
! [X68,X69] :
( ~ c1_1(X68)
| c0_1(X68)
| ~ c2_1(X68)
| ~ ndr1_0
| ~ c1_1(X69)
| c0_1(X69)
| c3_1(X69)
| hskp4 ),
inference(duplicate_literal_removal,[],[f307]) ).
fof(f338,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,[],[f304]) ).
fof(f343,plain,
! [X50,X51] :
( ~ c0_1(X50)
| c1_1(X50)
| ~ c2_1(X50)
| ~ ndr1_0
| ~ c3_1(X51)
| c0_1(X51)
| c1_1(X51)
| hskp13 ),
inference(duplicate_literal_removal,[],[f296]) ).
fof(f344,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,[],[f295]) ).
fof(f353,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,[],[f283]) ).
fof(f354,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,[],[f281]) ).
fof(f355,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,[],[f280]) ).
fof(f356,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,[],[f279]) ).
fof(f357,plain,
! [X16,X14,X15] :
( ~ c0_1(X14)
| ~ c1_1(X14)
| ~ c3_1(X14)
| ~ ndr1_0
| ~ c0_1(X15)
| c2_1(X15)
| c1_1(X15)
| ~ c3_1(X16)
| c0_1(X16)
| ~ c2_1(X16) ),
inference(duplicate_literal_removal,[],[f278]) ).
fof(f358,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,[],[f277]) ).
fof(f359,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,[],[f276]) ).
fof(f362,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,[],[f273]) ).
fof(f364,definition,
( spl0_1
<=> hskp25 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f368,definition,
( spl0_2
<=> hskp12 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f372,definition,
( spl0_3
<=> hskp20 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f375,plain,
( spl0_1
| ~ spl0_2
| spl0_3 ),
inference(avatar_split_clause,[],[f330,f372,f368,f364]) ).
fof(f377,definition,
( spl0_4
<=> hskp16 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f381,definition,
( spl0_5
<=> hskp26 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f384,plain,
( spl0_4
| spl0_5 ),
inference(avatar_split_clause,[],[f7,f381,f377]) ).
fof(f386,definition,
( spl0_6
<=> hskp11 ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f389,plain,
( ~ spl0_2
| ~ spl0_6
| spl0_5 ),
inference(avatar_split_clause,[],[f329,f381,f386,f368]) ).
fof(f395,definition,
( spl0_8
<=> hskp15 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f412,definition,
( spl0_12
<=> hskp17 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f417,definition,
( spl0_13
<=> hskp10 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f421,definition,
( spl0_14
<=> hskp1 ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f439,definition,
( spl0_18
<=> hskp28 ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f443,definition,
( spl0_19
<=> ndr1_0 ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f447,definition,
( spl0_20
<=> ! [X93] :
( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f448,plain,
( ! [X93] :
( c1_1(X93)
| c3_1(X93)
| ~ c2_1(X93) )
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f449,plain,
( spl0_18
| ~ spl0_19
| spl0_20 ),
inference(avatar_split_clause,[],[f325,f447,f443,f439]) ).
fof(f451,definition,
( spl0_21
<=> hskp21 ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f455,definition,
( spl0_22
<=> ! [X92] :
( c0_1(X92)
| c3_1(X92)
| c1_1(X92) ) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f456,plain,
( ! [X92] :
( c1_1(X92)
| c3_1(X92)
| c0_1(X92) )
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f455]) ).
fof(f468,definition,
( spl0_25
<=> ! [X89] :
( ~ c3_1(X89)
| ~ c2_1(X89)
| c1_1(X89) ) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f469,plain,
( ! [X89] :
( c1_1(X89)
| ~ c2_1(X89)
| ~ c3_1(X89) )
| ~ spl0_25 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f470,plain,
( spl0_1
| ~ spl0_8
| ~ spl0_19
| spl0_25 ),
inference(avatar_split_clause,[],[f321,f468,f443,f395,f364]) ).
fof(f472,definition,
( spl0_26
<=> hskp4 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f477,definition,
( spl0_27
<=> ! [X86] :
( c0_1(X86)
| c3_1(X86)
| ~ c2_1(X86) ) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f478,plain,
( ! [X86] :
( c3_1(X86)
| c0_1(X86)
| ~ c2_1(X86) )
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f477]) ).
fof(f480,definition,
( spl0_28
<=> ! [X85] :
( ~ c3_1(X85)
| ~ c2_1(X85)
| c0_1(X85) ) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f481,plain,
( ! [X85] :
( ~ c3_1(X85)
| ~ c2_1(X85)
| c0_1(X85) )
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f480]) ).
fof(f482,plain,
( ~ spl0_6
| spl0_27
| ~ spl0_19
| spl0_28 ),
inference(avatar_split_clause,[],[f332,f480,f443,f477,f386]) ).
fof(f484,definition,
( spl0_29
<=> ! [X84] :
( ~ c3_1(X84)
| c1_1(X84)
| c0_1(X84) ) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f485,plain,
( ! [X84] :
( c1_1(X84)
| ~ c3_1(X84)
| c0_1(X84) )
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f484]) ).
fof(f487,plain,
( spl0_26
| ~ spl0_12
| ~ spl0_19
| spl0_29 ),
inference(avatar_split_clause,[],[f317,f484,f443,f412,f472]) ).
fof(f489,definition,
( spl0_30
<=> ! [X81] :
( c2_1(X81)
| c3_1(X81)
| c1_1(X81) ) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f490,plain,
( ! [X81] :
( c1_1(X81)
| c3_1(X81)
| c2_1(X81) )
| ~ spl0_30 ),
inference(avatar_component_clause,[],[f489]) ).
fof(f491,plain,
( spl0_27
| ~ spl0_19
| spl0_30 ),
inference(avatar_split_clause,[],[f333,f489,f443,f477]) ).
fof(f493,definition,
( spl0_31
<=> hskp22 ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f497,definition,
( spl0_32
<=> ! [X80] :
( c2_1(X80)
| c1_1(X80)
| ~ c3_1(X80) ) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f498,plain,
( ! [X80] :
( c1_1(X80)
| c2_1(X80)
| ~ c3_1(X80) )
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f497]) ).
fof(f499,plain,
( spl0_31
| ~ spl0_19
| spl0_32 ),
inference(avatar_split_clause,[],[f315,f497,f443,f493]) ).
fof(f500,plain,
( ~ spl0_12
| spl0_22
| ~ spl0_19
| spl0_32 ),
inference(avatar_split_clause,[],[f334,f497,f443,f455,f412]) ).
fof(f503,definition,
( spl0_33
<=> ! [X74] :
( c2_1(X74)
| c0_1(X74)
| ~ c3_1(X74) ) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f504,plain,
( ! [X74] :
( ~ c3_1(X74)
| c0_1(X74)
| c2_1(X74) )
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f503]) ).
fof(f505,plain,
( ~ spl0_21
| ~ spl0_19
| spl0_33 ),
inference(avatar_split_clause,[],[f312,f503,f443,f451]) ).
fof(f511,definition,
( spl0_35
<=> ! [X73] :
( ~ c1_1(X73)
| c3_1(X73)
| ~ c2_1(X73) ) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f512,plain,
( ! [X73] :
( ~ c1_1(X73)
| c3_1(X73)
| ~ c2_1(X73) )
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f511]) ).
fof(f515,definition,
( spl0_36
<=> ! [X72] :
( ~ c1_1(X72)
| ~ c2_1(X72)
| c0_1(X72) ) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f516,plain,
( ! [X72] :
( ~ c1_1(X72)
| ~ c2_1(X72)
| c0_1(X72) )
| ~ spl0_36 ),
inference(avatar_component_clause,[],[f515]) ).
fof(f517,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_19
| spl0_36 ),
inference(avatar_split_clause,[],[f310,f515,f443,f386,f372]) ).
fof(f519,definition,
( spl0_37
<=> hskp19 ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f522,plain,
( ~ spl0_2
| spl0_37
| ~ spl0_19
| spl0_36 ),
inference(avatar_split_clause,[],[f309,f515,f443,f519,f368]) ).
fof(f529,definition,
( spl0_39
<=> ! [X69] :
( ~ c1_1(X69)
| c3_1(X69)
| c0_1(X69) ) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f530,plain,
( ! [X69] :
( ~ c1_1(X69)
| c3_1(X69)
| c0_1(X69) )
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f529]) ).
fof(f531,plain,
( spl0_26
| spl0_39
| ~ spl0_19
| spl0_36 ),
inference(avatar_split_clause,[],[f336,f515,f443,f529,f472]) ).
fof(f533,definition,
( spl0_40
<=> ! [X67] :
( ~ c1_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67) ) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f534,plain,
( ! [X67] :
( ~ c1_1(X67)
| ~ c2_1(X67)
| ~ c3_1(X67) )
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f533]) ).
fof(f535,plain,
( spl0_4
| ~ spl0_6
| ~ spl0_19
| spl0_40 ),
inference(avatar_split_clause,[],[f306,f533,f443,f386,f377]) ).
fof(f538,definition,
( spl0_41
<=> ! [X63] :
( ~ c1_1(X63)
| c0_1(X63)
| ~ c3_1(X63) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f539,plain,
( ! [X63] :
( ~ c1_1(X63)
| c0_1(X63)
| ~ c3_1(X63) )
| ~ spl0_41 ),
inference(avatar_component_clause,[],[f538]) ).
fof(f540,plain,
( ~ spl0_12
| spl0_32
| ~ spl0_19
| spl0_41 ),
inference(avatar_split_clause,[],[f338,f538,f443,f497,f412]) ).
fof(f542,definition,
( spl0_42
<=> hskp13 ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f547,definition,
( spl0_43
<=> ! [X60] :
( ~ c1_1(X60)
| c3_1(X60)
| c2_1(X60) ) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f548,plain,
( ! [X60] :
( ~ c1_1(X60)
| c3_1(X60)
| c2_1(X60) )
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f547]) ).
fof(f549,plain,
( spl0_4
| ~ spl0_19
| spl0_43 ),
inference(avatar_split_clause,[],[f302,f547,f443,f377]) ).
fof(f552,definition,
( spl0_44
<=> ! [X58] :
( c2_1(X58)
| c1_1(X58)
| c0_1(X58) ) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f553,plain,
( ! [X58] :
( c1_1(X58)
| c2_1(X58)
| c0_1(X58) )
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f552]) ).
fof(f556,definition,
( spl0_45
<=> hskp14 ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f564,definition,
( spl0_47
<=> hskp0 ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f568,definition,
( spl0_48
<=> ! [X54] :
( ~ c0_1(X54)
| c3_1(X54)
| ~ c2_1(X54) ) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f569,plain,
( ! [X54] :
( c3_1(X54)
| ~ c0_1(X54)
| ~ c2_1(X54) )
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f568]) ).
fof(f570,plain,
( ~ spl0_47
| ~ spl0_45
| ~ spl0_19
| spl0_48 ),
inference(avatar_split_clause,[],[f298,f568,f443,f556,f564]) ).
fof(f573,definition,
( spl0_49
<=> ! [X50] :
( ~ c0_1(X50)
| ~ c2_1(X50)
| c1_1(X50) ) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f574,plain,
( ! [X50] :
( c1_1(X50)
| ~ c2_1(X50)
| ~ c0_1(X50) )
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f573]) ).
fof(f575,plain,
( spl0_42
| spl0_29
| ~ spl0_19
| spl0_49 ),
inference(avatar_split_clause,[],[f343,f573,f443,f484,f542]) ).
fof(f576,plain,
( ~ spl0_2
| spl0_33
| ~ spl0_19
| spl0_49 ),
inference(avatar_split_clause,[],[f344,f573,f443,f503,f368]) ).
fof(f586,definition,
( spl0_52
<=> ! [X43] :
( ~ c0_1(X43)
| c3_1(X43)
| c2_1(X43) ) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f587,plain,
( ! [X43] :
( c3_1(X43)
| ~ c0_1(X43)
| c2_1(X43) )
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f586]) ).
fof(f588,plain,
( ~ spl0_6
| spl0_13
| ~ spl0_19
| spl0_52 ),
inference(avatar_split_clause,[],[f292,f586,f443,f417,f386]) ).
fof(f595,definition,
( spl0_54
<=> ! [X40] :
( ~ c0_1(X40)
| c1_1(X40)
| c2_1(X40) ) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f596,plain,
( ! [X40] :
( c1_1(X40)
| ~ c0_1(X40)
| c2_1(X40) )
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f595]) ).
fof(f608,definition,
( spl0_56
<=> ! [X25] :
( ~ c0_1(X25)
| ~ c3_1(X25)
| c2_1(X25) ) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f609,plain,
( ! [X25] :
( ~ c3_1(X25)
| ~ c0_1(X25)
| c2_1(X25) )
| ~ spl0_56 ),
inference(avatar_component_clause,[],[f608]) ).
fof(f610,plain,
( spl0_35
| spl0_54
| ~ spl0_19
| spl0_56 ),
inference(avatar_split_clause,[],[f353,f608,f443,f595,f511]) ).
fof(f612,definition,
( spl0_57
<=> hskp2 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f616,definition,
( spl0_58
<=> ! [X24] :
( ~ c0_1(X24)
| c3_1(X24)
| ~ c1_1(X24) ) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f617,plain,
( ! [X24] :
( ~ c1_1(X24)
| c3_1(X24)
| ~ c0_1(X24) )
| ~ spl0_58 ),
inference(avatar_component_clause,[],[f616]) ).
fof(f618,plain,
( ~ spl0_47
| spl0_57
| ~ spl0_19
| spl0_58 ),
inference(avatar_split_clause,[],[f282,f616,f443,f612,f564]) ).
fof(f619,plain,
( ~ spl0_47
| spl0_30
| ~ spl0_19
| spl0_58 ),
inference(avatar_split_clause,[],[f354,f616,f443,f489,f564]) ).
fof(f621,definition,
( spl0_59
<=> ! [X20] :
( ~ c0_1(X20)
| ~ c2_1(X20)
| ~ c1_1(X20) ) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f622,plain,
( ! [X20] :
( ~ c1_1(X20)
| ~ c2_1(X20)
| ~ c0_1(X20) )
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( spl0_14
| spl0_35
| ~ spl0_19
| spl0_59 ),
inference(avatar_split_clause,[],[f355,f621,f443,f511,f421]) ).
fof(f624,plain,
( spl0_25
| spl0_54
| ~ spl0_19
| spl0_59 ),
inference(avatar_split_clause,[],[f356,f621,f443,f595,f468]) ).
fof(f626,definition,
( spl0_60
<=> ! [X14] :
( ~ c0_1(X14)
| ~ c3_1(X14)
| ~ c1_1(X14) ) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f627,plain,
( ! [X14] :
( ~ c1_1(X14)
| ~ c3_1(X14)
| ~ c0_1(X14) )
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f626]) ).
fof(f628,plain,
( spl0_28
| spl0_54
| ~ spl0_19
| spl0_60 ),
inference(avatar_split_clause,[],[f357,f626,f443,f595,f480]) ).
fof(f629,plain,
( spl0_48
| spl0_56
| ~ spl0_19
| spl0_60 ),
inference(avatar_split_clause,[],[f358,f626,f443,f608,f568]) ).
fof(f631,definition,
( spl0_61
<=> ! [X9] :
( ~ c0_1(X9)
| c2_1(X9)
| ~ c1_1(X9) ) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f632,plain,
( ! [X9] :
( ~ c1_1(X9)
| c2_1(X9)
| ~ c0_1(X9) )
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f631]) ).
fof(f633,plain,
( ~ spl0_47
| spl0_44
| ~ spl0_19
| spl0_61 ),
inference(avatar_split_clause,[],[f359,f631,f443,f552,f564]) ).
fof(f639,plain,
( spl0_49
| spl0_56
| ~ spl0_19
| spl0_61 ),
inference(avatar_split_clause,[],[f362,f631,f443,f608,f573]) ).
fof(f657,definition,
( spl0_66
<=> c3_1(a353) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f659,plain,
( ~ c3_1(a353)
| spl0_66 ),
inference(avatar_component_clause,[],[f657]) ).
fof(f660,plain,
( ~ spl0_66
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f270,f439,f657]) ).
fof(f662,definition,
( spl0_67
<=> c2_1(a353) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f665,plain,
( spl0_67
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f71,f439,f662]) ).
fof(f667,definition,
( spl0_68
<=> c1_1(a353) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f669,plain,
( ~ c1_1(a353)
| spl0_68 ),
inference(avatar_component_clause,[],[f667]) ).
fof(f670,plain,
( ~ spl0_68
| ~ spl0_18 ),
inference(avatar_split_clause,[],[f269,f439,f667]) ).
fof(f689,definition,
( spl0_72
<=> c3_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f691,plain,
( c3_1(a349)
| ~ spl0_72 ),
inference(avatar_component_clause,[],[f689]) ).
fof(f692,plain,
( spl0_72
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f266,f381,f689]) ).
fof(f694,definition,
( spl0_73
<=> c2_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f697,plain,
( ~ spl0_73
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f79,f381,f694]) ).
fof(f699,definition,
( spl0_74
<=> c0_1(a349) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f702,plain,
( ~ spl0_74
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f265,f381,f699]) ).
fof(f705,definition,
( spl0_75
<=> c3_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f707,plain,
( c3_1(a346)
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f705]) ).
fof(f708,plain,
( spl0_75
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f264,f364,f705]) ).
fof(f710,definition,
( spl0_76
<=> c1_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f712,plain,
( c1_1(a346)
| ~ spl0_76 ),
inference(avatar_component_clause,[],[f710]) ).
fof(f713,plain,
( spl0_76
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f263,f364,f710]) ).
fof(f715,definition,
( spl0_77
<=> c0_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f718,plain,
( spl0_77
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f262,f364,f715]) ).
fof(f719,plain,
( spl0_19
| ~ spl0_1 ),
inference(avatar_split_clause,[],[f85,f364,f443]) ).
fof(f753,definition,
( spl0_84
<=> c3_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f755,plain,
( c3_1(a338)
| ~ spl0_84 ),
inference(avatar_component_clause,[],[f753]) ).
fof(f756,plain,
( spl0_84
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f253,f493,f753]) ).
fof(f758,definition,
( spl0_85
<=> c2_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f761,plain,
( ~ spl0_85
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f95,f493,f758]) ).
fof(f763,definition,
( spl0_86
<=> c1_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f765,plain,
( c1_1(a338)
| ~ spl0_86 ),
inference(avatar_component_clause,[],[f763]) ).
fof(f766,plain,
( spl0_86
| ~ spl0_31 ),
inference(avatar_split_clause,[],[f252,f493,f763]) ).
fof(f769,definition,
( spl0_87
<=> c1_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f771,plain,
( c1_1(a336)
| ~ spl0_87 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f772,plain,
( spl0_87
| spl0_21 ),
inference(avatar_split_clause,[],[f251,f451,f769]) ).
fof(f774,definition,
( spl0_88
<=> c0_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f777,plain,
( spl0_88
| spl0_21 ),
inference(avatar_split_clause,[],[f250,f451,f774]) ).
fof(f779,definition,
( spl0_89
<=> c3_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f781,plain,
( ~ c3_1(a336)
| spl0_89 ),
inference(avatar_component_clause,[],[f779]) ).
fof(f782,plain,
( ~ spl0_89
| spl0_21 ),
inference(avatar_split_clause,[],[f249,f451,f779]) ).
fof(f785,definition,
( spl0_90
<=> c3_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f788,plain,
( spl0_90
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f247,f372,f785]) ).
fof(f790,definition,
( spl0_91
<=> c2_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f793,plain,
( ~ spl0_91
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f103,f372,f790]) ).
fof(f795,definition,
( spl0_92
<=> c1_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f797,plain,
( ~ c1_1(a333)
| spl0_92 ),
inference(avatar_component_clause,[],[f795]) ).
fof(f798,plain,
( ~ spl0_92
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f246,f372,f795]) ).
fof(f799,plain,
( spl0_19
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f105,f372,f443]) ).
fof(f801,definition,
( spl0_93
<=> c3_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f804,plain,
( spl0_93
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f245,f519,f801]) ).
fof(f806,definition,
( spl0_94
<=> c2_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f809,plain,
( spl0_94
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f107,f519,f806]) ).
fof(f811,definition,
( spl0_95
<=> c1_1(a330) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f813,plain,
( ~ c1_1(a330)
| spl0_95 ),
inference(avatar_component_clause,[],[f811]) ).
fof(f814,plain,
( ~ spl0_95
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f244,f519,f811]) ).
fof(f833,definition,
( spl0_99
<=> c3_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f835,plain,
( c3_1(a323)
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f833]) ).
fof(f836,plain,
( spl0_99
| spl0_12 ),
inference(avatar_split_clause,[],[f239,f412,f833]) ).
fof(f838,definition,
( spl0_100
<=> c2_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f841,plain,
( spl0_100
| spl0_12 ),
inference(avatar_split_clause,[],[f238,f412,f838]) ).
fof(f843,definition,
( spl0_101
<=> c0_1(a323) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f846,plain,
( ~ spl0_101
| spl0_12 ),
inference(avatar_split_clause,[],[f237,f412,f843]) ).
fof(f849,definition,
( spl0_102
<=> c1_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f851,plain,
( c1_1(a321)
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f849]) ).
fof(f852,plain,
( spl0_102
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f235,f377,f849]) ).
fof(f854,definition,
( spl0_103
<=> c3_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f856,plain,
( ~ c3_1(a321)
| spl0_103 ),
inference(avatar_component_clause,[],[f854]) ).
fof(f857,plain,
( ~ spl0_103
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f234,f377,f854]) ).
fof(f859,definition,
( spl0_104
<=> c2_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f862,plain,
( spl0_104
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f120,f377,f859]) ).
fof(f865,definition,
( spl0_105
<=> c2_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f868,plain,
( ~ spl0_105
| spl0_8 ),
inference(avatar_split_clause,[],[f233,f395,f865]) ).
fof(f870,definition,
( spl0_106
<=> c0_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f873,plain,
( spl0_106
| spl0_8 ),
inference(avatar_split_clause,[],[f232,f395,f870]) ).
fof(f875,definition,
( spl0_107
<=> c1_1(a320) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f877,plain,
( ~ c1_1(a320)
| spl0_107 ),
inference(avatar_component_clause,[],[f875]) ).
fof(f878,plain,
( ~ spl0_107
| spl0_8 ),
inference(avatar_split_clause,[],[f231,f395,f875]) ).
fof(f881,definition,
( spl0_108
<=> c0_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f884,plain,
( spl0_108
| spl0_45 ),
inference(avatar_split_clause,[],[f229,f556,f881]) ).
fof(f886,definition,
( spl0_109
<=> c2_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f889,plain,
( spl0_109
| spl0_45 ),
inference(avatar_split_clause,[],[f228,f556,f886]) ).
fof(f891,definition,
( spl0_110
<=> c1_1(a315) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f893,plain,
( ~ c1_1(a315)
| spl0_110 ),
inference(avatar_component_clause,[],[f891]) ).
fof(f894,plain,
( ~ spl0_110
| spl0_45 ),
inference(avatar_split_clause,[],[f227,f556,f891]) ).
fof(f897,definition,
( spl0_111
<=> c1_1(a313) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f899,plain,
( c1_1(a313)
| ~ spl0_111 ),
inference(avatar_component_clause,[],[f897]) ).
fof(f900,plain,
( spl0_111
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f225,f542,f897]) ).
fof(f902,definition,
( spl0_112
<=> c3_1(a313) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f905,plain,
( ~ spl0_112
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f224,f542,f902]) ).
fof(f907,definition,
( spl0_113
<=> c0_1(a313) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f910,plain,
( ~ spl0_113
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f223,f542,f907]) ).
fof(f913,definition,
( spl0_114
<=> c2_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f916,plain,
( ~ spl0_114
| spl0_2 ),
inference(avatar_split_clause,[],[f222,f368,f913]) ).
fof(f918,definition,
( spl0_115
<=> c0_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f921,plain,
( spl0_115
| spl0_2 ),
inference(avatar_split_clause,[],[f221,f368,f918]) ).
fof(f923,definition,
( spl0_116
<=> c3_1(a310) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f925,plain,
( ~ c3_1(a310)
| spl0_116 ),
inference(avatar_component_clause,[],[f923]) ).
fof(f926,plain,
( ~ spl0_116
| spl0_2 ),
inference(avatar_split_clause,[],[f220,f368,f923]) ).
fof(f927,plain,
( spl0_19
| spl0_2 ),
inference(avatar_split_clause,[],[f219,f368,f443]) ).
fof(f929,definition,
( spl0_117
<=> c2_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f932,plain,
( ~ spl0_117
| spl0_6 ),
inference(avatar_split_clause,[],[f218,f386,f929]) ).
fof(f934,definition,
( spl0_118
<=> c3_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f937,plain,
( ~ spl0_118
| spl0_6 ),
inference(avatar_split_clause,[],[f217,f386,f934]) ).
fof(f939,definition,
( spl0_119
<=> c1_1(a309) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f941,plain,
( ~ c1_1(a309)
| spl0_119 ),
inference(avatar_component_clause,[],[f939]) ).
fof(f942,plain,
( ~ spl0_119
| spl0_6 ),
inference(avatar_split_clause,[],[f216,f386,f939]) ).
fof(f950,definition,
( spl0_121
<=> c3_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f953,plain,
( ~ spl0_121
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f213,f417,f950]) ).
fof(f955,definition,
( spl0_122
<=> c1_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f957,plain,
( ~ c1_1(a308)
| spl0_122 ),
inference(avatar_component_clause,[],[f955]) ).
fof(f958,plain,
( ~ spl0_122
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f212,f417,f955]) ).
fof(f1041,definition,
( spl0_138
<=> c2_1(a300) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1044,plain,
( ~ spl0_138
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f166,f472,f1041]) ).
fof(f1046,definition,
( spl0_139
<=> c1_1(a300) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1048,plain,
( c1_1(a300)
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f1046]) ).
fof(f1049,plain,
( spl0_139
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f198,f472,f1046]) ).
fof(f1051,definition,
( spl0_140
<=> c0_1(a300) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1054,plain,
( spl0_140
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f197,f472,f1051]) ).
fof(f1073,definition,
( spl0_144
<=> c3_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1075,plain,
( c3_1(a297)
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f1073]) ).
fof(f1076,plain,
( spl0_144
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f194,f612,f1073]) ).
fof(f1078,definition,
( spl0_145
<=> c0_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1081,plain,
( spl0_145
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f193,f612,f1078]) ).
fof(f1083,definition,
( spl0_146
<=> c1_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_146])],[avatar_definition]) ).
fof(f1085,plain,
( ~ c1_1(a297)
| spl0_146 ),
inference(avatar_component_clause,[],[f1083]) ).
fof(f1086,plain,
( ~ spl0_146
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f192,f612,f1083]) ).
fof(f1089,definition,
( spl0_147
<=> c1_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1091,plain,
( c1_1(a295)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f1089]) ).
fof(f1092,plain,
( spl0_147
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f191,f421,f1089]) ).
fof(f1094,definition,
( spl0_148
<=> c2_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1097,plain,
( spl0_148
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f179,f421,f1094]) ).
fof(f1099,definition,
( spl0_149
<=> c0_1(a295) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1102,plain,
( ~ spl0_149
| ~ spl0_14 ),
inference(avatar_split_clause,[],[f190,f421,f1099]) ).
fof(f1105,definition,
( spl0_150
<=> c3_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1107,plain,
( c3_1(a294)
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f1105]) ).
fof(f1108,plain,
( spl0_150
| spl0_47 ),
inference(avatar_split_clause,[],[f189,f564,f1105]) ).
fof(f1110,definition,
( spl0_151
<=> c2_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f1113,plain,
( ~ spl0_151
| spl0_47 ),
inference(avatar_split_clause,[],[f188,f564,f1110]) ).
fof(f1115,definition,
( spl0_152
<=> c0_1(a294) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f1118,plain,
( spl0_152
| spl0_47 ),
inference(avatar_split_clause,[],[f187,f564,f1115]) ).
fof(f1128,plain,
( c3_1(a308)
| ~ c2_1(a308)
| ~ spl0_20
| spl0_122 ),
inference(resolution,[],[f448,f957]) ).
fof(f1147,definition,
( spl0_154
<=> c2_1(a346) ),
introduced(definition,[new_symbols(definition,[spl0_154])],[avatar_definition]) ).
fof(f1152,definition,
( spl0_155
<=> c2_1(a336) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1162,definition,
( spl0_157
<=> c2_1(a308) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1165,plain,
( ~ spl0_157
| spl0_121
| ~ spl0_20
| spl0_122 ),
inference(avatar_split_clause,[],[f1128,f955,f447,f950,f1162]) ).
fof(f1172,definition,
( spl0_159
<=> c2_1(a297) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1199,definition,
( spl0_160
<=> c0_1(a353) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1205,definition,
( spl0_161
<=> c0_1(a338) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1216,definition,
( spl0_163
<=> c0_1(a321) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1312,plain,
( ~ c2_1(a297)
| ~ c3_1(a297)
| ~ spl0_25
| spl0_146 ),
inference(resolution,[],[f469,f1085]) ).
fof(f1325,plain,
( ~ c2_1(a330)
| ~ c3_1(a330)
| ~ spl0_25
| spl0_95 ),
inference(resolution,[],[f469,f813]) ).
fof(f1347,plain,
( ~ c3_1(a333)
| c0_1(a333)
| ~ spl0_29
| spl0_92 ),
inference(resolution,[],[f485,f797]) ).
fof(f1352,definition,
( spl0_173
<=> c0_1(a333) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1364,plain,
( c3_1(a308)
| c2_1(a308)
| ~ spl0_30
| spl0_122 ),
inference(resolution,[],[f490,f957]) ).
fof(f1365,plain,
( c3_1(a309)
| c2_1(a309)
| ~ spl0_30
| spl0_119 ),
inference(resolution,[],[f490,f941]) ).
fof(f1384,plain,
( spl0_157
| spl0_121
| ~ spl0_30
| spl0_122 ),
inference(avatar_split_clause,[],[f1364,f955,f489,f950,f1162]) ).
fof(f1416,plain,
( ~ c2_1(a323)
| c0_1(a323)
| ~ spl0_28
| ~ spl0_99 ),
inference(resolution,[],[f835,f481]) ).
fof(f1417,plain,
( spl0_101
| ~ spl0_100
| ~ spl0_28
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f1416,f833,f480,f838,f843]) ).
fof(f1436,plain,
( c2_1(a333)
| ~ c3_1(a333)
| ~ spl0_32
| spl0_92 ),
inference(resolution,[],[f498,f797]) ).
fof(f1481,plain,
( c0_1(a338)
| c2_1(a338)
| ~ spl0_33
| ~ spl0_84 ),
inference(resolution,[],[f504,f755]) ).
fof(f1482,plain,
( c0_1(a349)
| c2_1(a349)
| ~ spl0_33
| ~ spl0_72 ),
inference(resolution,[],[f504,f691]) ).
fof(f1485,plain,
( spl0_73
| spl0_74
| ~ spl0_33
| ~ spl0_72 ),
inference(avatar_split_clause,[],[f1482,f689,f503,f699,f694]) ).
fof(f1486,plain,
( spl0_85
| spl0_161
| ~ spl0_33
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f1481,f753,f503,f1205,f758]) ).
fof(f1528,plain,
( ~ c2_1(a295)
| c0_1(a295)
| ~ spl0_36
| ~ spl0_147 ),
inference(resolution,[],[f516,f1091]) ).
fof(f1533,plain,
( ~ c2_1(a321)
| c0_1(a321)
| ~ spl0_36
| ~ spl0_102 ),
inference(resolution,[],[f516,f851]) ).
fof(f1546,plain,
( spl0_149
| ~ spl0_148
| ~ spl0_36
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1528,f1089,f515,f1094,f1099]) ).
fof(f1607,plain,
( ~ c2_1(a346)
| ~ c3_1(a346)
| ~ spl0_40
| ~ spl0_76 ),
inference(resolution,[],[f534,f712]) ).
fof(f1619,plain,
( c0_1(a338)
| ~ c3_1(a338)
| ~ spl0_41
| ~ spl0_86 ),
inference(resolution,[],[f539,f765]) ).
fof(f1623,plain,
( ~ spl0_84
| spl0_161
| ~ spl0_41
| ~ spl0_86 ),
inference(avatar_split_clause,[],[f1619,f763,f538,f1205,f753]) ).
fof(f1635,plain,
( c3_1(a336)
| c2_1(a336)
| ~ spl0_43
| ~ spl0_87 ),
inference(resolution,[],[f548,f771]) ).
fof(f1643,plain,
( spl0_155
| spl0_89
| ~ spl0_43
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f1635,f769,f547,f779,f1152]) ).
fof(f1646,plain,
( spl0_163
| ~ spl0_104
| ~ spl0_36
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1533,f849,f515,f859,f1216]) ).
fof(f1660,plain,
( c2_1(a333)
| c0_1(a333)
| ~ spl0_44
| spl0_92 ),
inference(resolution,[],[f553,f797]) ).
fof(f1682,plain,
( ~ c0_1(a321)
| ~ c2_1(a321)
| ~ spl0_48
| spl0_103 ),
inference(resolution,[],[f569,f856]) ).
fof(f1685,plain,
( ~ c0_1(a336)
| ~ c2_1(a336)
| ~ spl0_48
| spl0_89 ),
inference(resolution,[],[f569,f781]) ).
fof(f1689,plain,
( ~ spl0_104
| ~ spl0_163
| ~ spl0_48
| spl0_103 ),
inference(avatar_split_clause,[],[f1682,f854,f568,f1216,f859]) ).
fof(f1706,plain,
( ~ c2_1(a353)
| ~ c0_1(a353)
| ~ spl0_49
| spl0_68 ),
inference(resolution,[],[f574,f669]) ).
fof(f1734,plain,
( ~ c0_1(a310)
| c2_1(a310)
| ~ spl0_52
| spl0_116 ),
inference(resolution,[],[f587,f925]) ).
fof(f1740,plain,
( ~ c0_1(a336)
| c2_1(a336)
| ~ spl0_52
| spl0_89 ),
inference(resolution,[],[f587,f781]) ).
fof(f1749,plain,
( spl0_155
| ~ spl0_88
| ~ spl0_52
| spl0_89 ),
inference(avatar_split_clause,[],[f1740,f779,f586,f774,f1152]) ).
fof(f1762,plain,
( ~ c0_1(a333)
| c2_1(a333)
| ~ spl0_54
| spl0_92 ),
inference(resolution,[],[f596,f797]) ).
fof(f1765,plain,
( spl0_91
| ~ spl0_173
| ~ spl0_54
| spl0_92 ),
inference(avatar_split_clause,[],[f1762,f795,f595,f1352,f790]) ).
fof(f1769,plain,
( ~ c0_1(a294)
| c2_1(a294)
| ~ spl0_56
| ~ spl0_150 ),
inference(resolution,[],[f609,f1107]) ).
fof(f1771,plain,
( ~ c0_1(a297)
| c2_1(a297)
| ~ spl0_56
| ~ spl0_144 ),
inference(resolution,[],[f609,f1075]) ).
fof(f1781,plain,
( ~ c0_1(a338)
| c2_1(a338)
| ~ spl0_56
| ~ spl0_84 ),
inference(resolution,[],[f609,f755]) ).
fof(f1782,plain,
( ~ c0_1(a346)
| c2_1(a346)
| ~ spl0_56
| ~ spl0_75 ),
inference(resolution,[],[f609,f707]) ).
fof(f1788,plain,
( spl0_154
| ~ spl0_77
| ~ spl0_56
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f1782,f705,f608,f715,f1147]) ).
fof(f1789,plain,
( spl0_85
| ~ spl0_161
| ~ spl0_56
| ~ spl0_84 ),
inference(avatar_split_clause,[],[f1781,f753,f608,f1205,f758]) ).
fof(f1802,plain,
( c3_1(a321)
| ~ c0_1(a321)
| ~ spl0_58
| ~ spl0_102 ),
inference(resolution,[],[f617,f851]) ).
fof(f1803,plain,
( c3_1(a336)
| ~ c0_1(a336)
| ~ spl0_58
| ~ spl0_87 ),
inference(resolution,[],[f617,f771]) ).
fof(f1812,plain,
( ~ spl0_88
| spl0_89
| ~ spl0_58
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f1803,f769,f616,f779,f774]) ).
fof(f1813,plain,
( ~ spl0_163
| spl0_103
| ~ spl0_58
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1802,f849,f616,f854,f1216]) ).
fof(f1829,plain,
( ~ c2_1(a321)
| ~ c0_1(a321)
| ~ spl0_59
| ~ spl0_102 ),
inference(resolution,[],[f622,f851]) ).
fof(f1830,plain,
( ~ c2_1(a336)
| ~ c0_1(a336)
| ~ spl0_59
| ~ spl0_87 ),
inference(resolution,[],[f622,f771]) ).
fof(f1837,plain,
( ~ spl0_88
| ~ spl0_155
| ~ spl0_59
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f1830,f769,f621,f1152,f774]) ).
fof(f1838,plain,
( ~ spl0_163
| ~ spl0_104
| ~ spl0_59
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1829,f849,f621,f859,f1216]) ).
fof(f1847,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_35
| ~ spl0_49 ),
inference(resolution,[],[f512,f574]) ).
fof(f1856,plain,
( c3_1(a321)
| ~ c2_1(a321)
| ~ spl0_35
| ~ spl0_102 ),
inference(resolution,[],[f512,f851]) ).
fof(f1857,plain,
( c3_1(a336)
| ~ c2_1(a336)
| ~ spl0_35
| ~ spl0_87 ),
inference(resolution,[],[f512,f771]) ).
fof(f1864,plain,
( ! [X0] :
( c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) )
| ~ spl0_35
| ~ spl0_49 ),
inference(duplicate_literal_removal,[],[f1847]) ).
fof(f1885,plain,
( ~ spl0_155
| spl0_89
| ~ spl0_35
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f1857,f769,f511,f779,f1152]) ).
fof(f1886,plain,
( ~ spl0_104
| spl0_103
| ~ spl0_35
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f1856,f849,f511,f854,f859]) ).
fof(f1887,plain,
( spl0_48
| ~ spl0_35
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f1864,f573,f511,f568]) ).
fof(f1888,plain,
( spl0_114
| ~ spl0_115
| ~ spl0_52
| spl0_116 ),
inference(avatar_split_clause,[],[f1734,f923,f586,f918,f913]) ).
fof(f1889,plain,
( ~ spl0_160
| ~ spl0_67
| ~ spl0_49
| spl0_68 ),
inference(avatar_split_clause,[],[f1706,f667,f573,f662,f1199]) ).
fof(f1891,plain,
( c0_1(a353)
| ~ c2_1(a353)
| ~ spl0_27
| spl0_66 ),
inference(resolution,[],[f659,f478]) ).
fof(f1892,plain,
( ~ spl0_67
| spl0_160
| ~ spl0_27
| spl0_66 ),
inference(avatar_split_clause,[],[f1891,f657,f477,f1199,f662]) ).
fof(f1937,plain,
( c3_1(a353)
| c0_1(a353)
| ~ spl0_22
| spl0_68 ),
inference(resolution,[],[f456,f669]) ).
fof(f1948,plain,
( c0_1(a321)
| ~ c2_1(a321)
| ~ spl0_27
| spl0_103 ),
inference(resolution,[],[f478,f856]) ).
fof(f1966,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_54
| ~ spl0_60 ),
inference(resolution,[],[f627,f596]) ).
fof(f1981,plain,
( ~ c3_1(a346)
| ~ c0_1(a346)
| ~ spl0_60
| ~ spl0_76 ),
inference(resolution,[],[f627,f712]) ).
fof(f1982,plain,
( ! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) )
| ~ spl0_54
| ~ spl0_60 ),
inference(duplicate_literal_removal,[],[f1966]) ).
fof(f1984,plain,
( ~ spl0_77
| ~ spl0_75
| ~ spl0_60
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1981,f710,f626,f705,f715]) ).
fof(f1989,plain,
( spl0_56
| ~ spl0_54
| ~ spl0_60 ),
inference(avatar_split_clause,[],[f1982,f626,f595,f608]) ).
fof(f1991,plain,
( ~ spl0_75
| ~ spl0_154
| ~ spl0_40
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f1607,f710,f533,f1147,f705]) ).
fof(f2004,plain,
( ~ c0_1(a320)
| c2_1(a320)
| ~ spl0_54
| spl0_107 ),
inference(resolution,[],[f877,f596]) ).
fof(f2006,plain,
( ~ c2_1(a315)
| ~ c0_1(a315)
| ~ spl0_49
| spl0_110 ),
inference(resolution,[],[f893,f574]) ).
fof(f2011,plain,
( ~ spl0_108
| ~ spl0_109
| ~ spl0_49
| spl0_110 ),
inference(avatar_split_clause,[],[f2006,f891,f573,f886,f881]) ).
fof(f2014,plain,
( spl0_173
| ~ spl0_90
| ~ spl0_29
| spl0_92 ),
inference(avatar_split_clause,[],[f1347,f795,f484,f785,f1352]) ).
fof(f2018,plain,
( ~ spl0_90
| spl0_91
| ~ spl0_32
| spl0_92 ),
inference(avatar_split_clause,[],[f1436,f795,f497,f790,f785]) ).
fof(f2024,plain,
( ~ spl0_155
| ~ spl0_88
| ~ spl0_48
| spl0_89 ),
inference(avatar_split_clause,[],[f1685,f779,f568,f774,f1152]) ).
fof(f2037,plain,
( spl0_105
| ~ spl0_106
| ~ spl0_54
| spl0_107 ),
inference(avatar_split_clause,[],[f2004,f875,f595,f870,f865]) ).
fof(f2049,plain,
( spl0_160
| spl0_66
| ~ spl0_22
| spl0_68 ),
inference(avatar_split_clause,[],[f1937,f667,f455,f657,f1199]) ).
fof(f2051,plain,
( ~ spl0_144
| ~ spl0_159
| ~ spl0_25
| spl0_146 ),
inference(avatar_split_clause,[],[f1312,f1083,f468,f1172,f1073]) ).
fof(f2053,plain,
( ~ spl0_93
| ~ spl0_94
| ~ spl0_25
| spl0_95 ),
inference(avatar_split_clause,[],[f1325,f811,f468,f806,f801]) ).
fof(f2056,plain,
( spl0_117
| spl0_118
| ~ spl0_30
| spl0_119 ),
inference(avatar_split_clause,[],[f1365,f939,f489,f934,f929]) ).
fof(f2059,plain,
( spl0_151
| ~ spl0_152
| ~ spl0_56
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f1769,f1105,f608,f1115,f1110]) ).
fof(f2060,plain,
( spl0_159
| ~ spl0_145
| ~ spl0_56
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1771,f1073,f608,f1078,f1172]) ).
fof(f2063,plain,
( ~ spl0_104
| spl0_163
| ~ spl0_27
| spl0_103 ),
inference(avatar_split_clause,[],[f1948,f854,f477,f1216,f859]) ).
fof(f2065,plain,
( spl0_173
| spl0_91
| ~ spl0_44
| spl0_92 ),
inference(avatar_split_clause,[],[f1660,f795,f552,f790,f1352]) ).
fof(f2109,plain,
( c3_1(a313)
| c0_1(a313)
| ~ spl0_39
| ~ spl0_111 ),
inference(resolution,[],[f530,f899]) ).
fof(f2117,plain,
( spl0_113
| spl0_112
| ~ spl0_39
| ~ spl0_111 ),
inference(avatar_split_clause,[],[f2109,f897,f529,f902,f907]) ).
fof(f2176,plain,
( c2_1(a300)
| ~ c0_1(a300)
| ~ spl0_61
| ~ spl0_139 ),
inference(resolution,[],[f632,f1048]) ).
fof(f2189,plain,
( ~ spl0_140
| spl0_138
| ~ spl0_61
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f2176,f1046,f631,f1041,f1051]) ).
cnf(s1,plain,
( spl0_1
| ~ spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f375]) ).
cnf(s2,plain,
( spl0_4
| spl0_5 ),
inference(sat_conversion,[],[f384]) ).
cnf(s3,plain,
( ~ spl0_2
| spl0_5
| ~ spl0_6 ),
inference(sat_conversion,[],[f389]) ).
cnf(s8,plain,
( spl0_18
| ~ spl0_19
| spl0_20 ),
inference(sat_conversion,[],[f449]) ).
cnf(s12,plain,
( spl0_1
| ~ spl0_8
| ~ spl0_19
| spl0_25 ),
inference(sat_conversion,[],[f470]) ).
cnf(s14,plain,
( ~ spl0_6
| ~ spl0_19
| spl0_27
| spl0_28 ),
inference(sat_conversion,[],[f482]) ).
cnf(s16,plain,
( ~ spl0_12
| ~ spl0_19
| spl0_26
| spl0_29 ),
inference(sat_conversion,[],[f487]) ).
cnf(s17,plain,
( ~ spl0_19
| spl0_27
| spl0_30 ),
inference(sat_conversion,[],[f491]) ).
cnf(s18,plain,
( ~ spl0_19
| spl0_31
| spl0_32 ),
inference(sat_conversion,[],[f499]) ).
cnf(s19,plain,
( ~ spl0_12
| ~ spl0_19
| spl0_22
| spl0_32 ),
inference(sat_conversion,[],[f500]) ).
cnf(s21,plain,
( ~ spl0_19
| ~ spl0_21
| spl0_33 ),
inference(sat_conversion,[],[f505]) ).
cnf(s23,plain,
( spl0_3
| ~ spl0_6
| ~ spl0_19
| spl0_36 ),
inference(sat_conversion,[],[f517]) ).
cnf(s24,plain,
( ~ spl0_2
| ~ spl0_19
| spl0_36
| spl0_37 ),
inference(sat_conversion,[],[f522]) ).
cnf(s26,plain,
( ~ spl0_19
| spl0_26
| spl0_36
| spl0_39 ),
inference(sat_conversion,[],[f531]) ).
cnf(s27,plain,
( spl0_4
| ~ spl0_6
| ~ spl0_19
| spl0_40 ),
inference(sat_conversion,[],[f535]) ).
cnf(s29,plain,
( ~ spl0_12
| ~ spl0_19
| spl0_32
| spl0_41 ),
inference(sat_conversion,[],[f540]) ).
cnf(s31,plain,
( spl0_4
| ~ spl0_19
| spl0_43 ),
inference(sat_conversion,[],[f549]) ).
cnf(s35,plain,
( ~ spl0_19
| ~ spl0_45
| ~ spl0_47
| spl0_48 ),
inference(sat_conversion,[],[f570]) ).
cnf(s37,plain,
( ~ spl0_19
| spl0_29
| spl0_42
| spl0_49 ),
inference(sat_conversion,[],[f575]) ).
cnf(s38,plain,
( ~ spl0_2
| ~ spl0_19
| spl0_33
| spl0_49 ),
inference(sat_conversion,[],[f576]) ).
cnf(s41,plain,
( ~ spl0_6
| spl0_13
| ~ spl0_19
| spl0_52 ),
inference(sat_conversion,[],[f588]) ).
cnf(s50,plain,
( ~ spl0_19
| spl0_35
| spl0_54
| spl0_56 ),
inference(sat_conversion,[],[f610]) ).
cnf(s51,plain,
( ~ spl0_19
| ~ spl0_47
| spl0_57
| spl0_58 ),
inference(sat_conversion,[],[f618]) ).
cnf(s52,plain,
( ~ spl0_19
| spl0_30
| ~ spl0_47
| spl0_58 ),
inference(sat_conversion,[],[f619]) ).
cnf(s53,plain,
( spl0_14
| ~ spl0_19
| spl0_35
| spl0_59 ),
inference(sat_conversion,[],[f623]) ).
cnf(s54,plain,
( ~ spl0_19
| spl0_25
| spl0_54
| spl0_59 ),
inference(sat_conversion,[],[f624]) ).
cnf(s55,plain,
( ~ spl0_19
| spl0_28
| spl0_54
| spl0_60 ),
inference(sat_conversion,[],[f628]) ).
cnf(s56,plain,
( ~ spl0_19
| spl0_48
| spl0_56
| spl0_60 ),
inference(sat_conversion,[],[f629]) ).
cnf(s57,plain,
( ~ spl0_19
| spl0_44
| ~ spl0_47
| spl0_61 ),
inference(sat_conversion,[],[f633]) ).
cnf(s60,plain,
( ~ spl0_19
| spl0_49
| spl0_56
| spl0_61 ),
inference(sat_conversion,[],[f639]) ).
cnf(s65,plain,
( ~ spl0_18
| ~ spl0_66 ),
inference(sat_conversion,[],[f660]) ).
cnf(s66,plain,
( ~ spl0_18
| spl0_67 ),
inference(sat_conversion,[],[f665]) ).
cnf(s67,plain,
( ~ spl0_18
| ~ spl0_68 ),
inference(sat_conversion,[],[f670]) ).
cnf(s73,plain,
( ~ spl0_5
| spl0_72 ),
inference(sat_conversion,[],[f692]) ).
cnf(s74,plain,
( ~ spl0_5
| ~ spl0_73 ),
inference(sat_conversion,[],[f697]) ).
cnf(s75,plain,
( ~ spl0_5
| ~ spl0_74 ),
inference(sat_conversion,[],[f702]) ).
cnf(s77,plain,
( ~ spl0_1
| spl0_75 ),
inference(sat_conversion,[],[f708]) ).
cnf(s78,plain,
( ~ spl0_1
| spl0_76 ),
inference(sat_conversion,[],[f713]) ).
cnf(s79,plain,
( ~ spl0_1
| spl0_77 ),
inference(sat_conversion,[],[f718]) ).
cnf(s80,plain,
( ~ spl0_1
| spl0_19 ),
inference(sat_conversion,[],[f719]) ).
cnf(s89,plain,
( ~ spl0_31
| spl0_84 ),
inference(sat_conversion,[],[f756]) ).
cnf(s90,plain,
( ~ spl0_31
| ~ spl0_85 ),
inference(sat_conversion,[],[f761]) ).
cnf(s91,plain,
( ~ spl0_31
| spl0_86 ),
inference(sat_conversion,[],[f766]) ).
cnf(s93,plain,
( spl0_21
| spl0_87 ),
inference(sat_conversion,[],[f772]) ).
cnf(s94,plain,
( spl0_21
| spl0_88 ),
inference(sat_conversion,[],[f777]) ).
cnf(s95,plain,
( spl0_21
| ~ spl0_89 ),
inference(sat_conversion,[],[f782]) ).
cnf(s97,plain,
( ~ spl0_3
| spl0_90 ),
inference(sat_conversion,[],[f788]) ).
cnf(s98,plain,
( ~ spl0_3
| ~ spl0_91 ),
inference(sat_conversion,[],[f793]) ).
cnf(s99,plain,
( ~ spl0_3
| ~ spl0_92 ),
inference(sat_conversion,[],[f798]) ).
cnf(s100,plain,
( ~ spl0_3
| spl0_19 ),
inference(sat_conversion,[],[f799]) ).
cnf(s101,plain,
( ~ spl0_37
| spl0_93 ),
inference(sat_conversion,[],[f804]) ).
cnf(s102,plain,
( ~ spl0_37
| spl0_94 ),
inference(sat_conversion,[],[f809]) ).
cnf(s103,plain,
( ~ spl0_37
| ~ spl0_95 ),
inference(sat_conversion,[],[f814]) ).
cnf(s109,plain,
( spl0_12
| spl0_99 ),
inference(sat_conversion,[],[f836]) ).
cnf(s110,plain,
( spl0_12
| spl0_100 ),
inference(sat_conversion,[],[f841]) ).
cnf(s111,plain,
( spl0_12
| ~ spl0_101 ),
inference(sat_conversion,[],[f846]) ).
cnf(s113,plain,
( ~ spl0_4
| spl0_102 ),
inference(sat_conversion,[],[f852]) ).
cnf(s114,plain,
( ~ spl0_4
| ~ spl0_103 ),
inference(sat_conversion,[],[f857]) ).
cnf(s115,plain,
( ~ spl0_4
| spl0_104 ),
inference(sat_conversion,[],[f862]) ).
cnf(s117,plain,
( spl0_8
| ~ spl0_105 ),
inference(sat_conversion,[],[f868]) ).
cnf(s118,plain,
( spl0_8
| spl0_106 ),
inference(sat_conversion,[],[f873]) ).
cnf(s119,plain,
( spl0_8
| ~ spl0_107 ),
inference(sat_conversion,[],[f878]) ).
cnf(s121,plain,
( spl0_45
| spl0_108 ),
inference(sat_conversion,[],[f884]) ).
cnf(s122,plain,
( spl0_45
| spl0_109 ),
inference(sat_conversion,[],[f889]) ).
cnf(s123,plain,
( spl0_45
| ~ spl0_110 ),
inference(sat_conversion,[],[f894]) ).
cnf(s125,plain,
( ~ spl0_42
| spl0_111 ),
inference(sat_conversion,[],[f900]) ).
cnf(s126,plain,
( ~ spl0_42
| ~ spl0_112 ),
inference(sat_conversion,[],[f905]) ).
cnf(s127,plain,
( ~ spl0_42
| ~ spl0_113 ),
inference(sat_conversion,[],[f910]) ).
cnf(s129,plain,
( spl0_2
| ~ spl0_114 ),
inference(sat_conversion,[],[f916]) ).
cnf(s130,plain,
( spl0_2
| spl0_115 ),
inference(sat_conversion,[],[f921]) ).
cnf(s131,plain,
( spl0_2
| ~ spl0_116 ),
inference(sat_conversion,[],[f926]) ).
cnf(s132,plain,
( spl0_2
| spl0_19 ),
inference(sat_conversion,[],[f927]) ).
cnf(s133,plain,
( spl0_6
| ~ spl0_117 ),
inference(sat_conversion,[],[f932]) ).
cnf(s134,plain,
( spl0_6
| ~ spl0_118 ),
inference(sat_conversion,[],[f937]) ).
cnf(s135,plain,
( spl0_6
| ~ spl0_119 ),
inference(sat_conversion,[],[f942]) ).
cnf(s138,plain,
( ~ spl0_13
| ~ spl0_121 ),
inference(sat_conversion,[],[f953]) ).
cnf(s139,plain,
( ~ spl0_13
| ~ spl0_122 ),
inference(sat_conversion,[],[f958]) ).
cnf(s161,plain,
( ~ spl0_26
| ~ spl0_138 ),
inference(sat_conversion,[],[f1044]) ).
cnf(s162,plain,
( ~ spl0_26
| spl0_139 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s163,plain,
( ~ spl0_26
| spl0_140 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s169,plain,
( ~ spl0_57
| spl0_144 ),
inference(sat_conversion,[],[f1076]) ).
cnf(s170,plain,
( ~ spl0_57
| spl0_145 ),
inference(sat_conversion,[],[f1081]) ).
cnf(s171,plain,
( ~ spl0_57
| ~ spl0_146 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s173,plain,
( ~ spl0_14
| spl0_147 ),
inference(sat_conversion,[],[f1092]) ).
cnf(s174,plain,
( ~ spl0_14
| spl0_148 ),
inference(sat_conversion,[],[f1097]) ).
cnf(s175,plain,
( ~ spl0_14
| ~ spl0_149 ),
inference(sat_conversion,[],[f1102]) ).
cnf(s177,plain,
( spl0_47
| spl0_150 ),
inference(sat_conversion,[],[f1108]) ).
cnf(s178,plain,
( spl0_47
| ~ spl0_151 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s179,plain,
( spl0_47
| spl0_152 ),
inference(sat_conversion,[],[f1118]) ).
cnf(s185,plain,
( ~ spl0_20
| spl0_121
| spl0_122
| ~ spl0_157 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s221,plain,
( ~ spl0_30
| spl0_121
| spl0_122
| spl0_157 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s250,plain,
( ~ spl0_28
| ~ spl0_99
| ~ spl0_100
| spl0_101 ),
inference(sat_conversion,[],[f1417]) ).
cnf(s268,plain,
( ~ spl0_33
| ~ spl0_72
| spl0_73
| spl0_74 ),
inference(sat_conversion,[],[f1485]) ).
cnf(s269,plain,
( ~ spl0_33
| ~ spl0_84
| spl0_85
| spl0_161 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s289,plain,
( ~ spl0_36
| ~ spl0_147
| ~ spl0_148
| spl0_149 ),
inference(sat_conversion,[],[f1546]) ).
cnf(s305,plain,
( ~ spl0_41
| ~ spl0_84
| ~ spl0_86
| spl0_161 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s308,plain,
( ~ spl0_43
| ~ spl0_87
| spl0_89
| spl0_155 ),
inference(sat_conversion,[],[f1643]) ).
cnf(s311,plain,
( ~ spl0_36
| ~ spl0_102
| ~ spl0_104
| spl0_163 ),
inference(sat_conversion,[],[f1646]) ).
cnf(s324,plain,
( ~ spl0_48
| spl0_103
| ~ spl0_104
| ~ spl0_163 ),
inference(sat_conversion,[],[f1689]) ).
cnf(s329,plain,
( ~ spl0_52
| ~ spl0_88
| spl0_89
| spl0_155 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s330,plain,
( ~ spl0_54
| spl0_91
| spl0_92
| ~ spl0_173 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s332,plain,
( ~ spl0_56
| ~ spl0_75
| ~ spl0_77
| spl0_154 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s333,plain,
( ~ spl0_56
| ~ spl0_84
| spl0_85
| ~ spl0_161 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s336,plain,
( ~ spl0_58
| ~ spl0_87
| ~ spl0_88
| spl0_89 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s337,plain,
( ~ spl0_58
| ~ spl0_102
| spl0_103
| ~ spl0_163 ),
inference(sat_conversion,[],[f1813]) ).
cnf(s343,plain,
( ~ spl0_59
| ~ spl0_87
| ~ spl0_88
| ~ spl0_155 ),
inference(sat_conversion,[],[f1837]) ).
cnf(s344,plain,
( ~ spl0_59
| ~ spl0_102
| ~ spl0_104
| ~ spl0_163 ),
inference(sat_conversion,[],[f1838]) ).
cnf(s358,plain,
( ~ spl0_35
| ~ spl0_87
| spl0_89
| ~ spl0_155 ),
inference(sat_conversion,[],[f1885]) ).
cnf(s359,plain,
( ~ spl0_35
| ~ spl0_102
| spl0_103
| ~ spl0_104 ),
inference(sat_conversion,[],[f1886]) ).
cnf(s360,plain,
( ~ spl0_35
| spl0_48
| ~ spl0_49 ),
inference(sat_conversion,[],[f1887]) ).
cnf(s361,plain,
( ~ spl0_52
| spl0_114
| ~ spl0_115
| spl0_116 ),
inference(sat_conversion,[],[f1888]) ).
cnf(s362,plain,
( ~ spl0_49
| ~ spl0_67
| spl0_68
| ~ spl0_160 ),
inference(sat_conversion,[],[f1889]) ).
cnf(s363,plain,
( ~ spl0_27
| spl0_66
| ~ spl0_67
| spl0_160 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s382,plain,
( ~ spl0_60
| ~ spl0_75
| ~ spl0_76
| ~ spl0_77 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s387,plain,
( ~ spl0_54
| spl0_56
| ~ spl0_60 ),
inference(sat_conversion,[],[f1989]) ).
cnf(s389,plain,
( ~ spl0_40
| ~ spl0_75
| ~ spl0_76
| ~ spl0_154 ),
inference(sat_conversion,[],[f1991]) ).
cnf(s398,plain,
( ~ spl0_49
| ~ spl0_108
| ~ spl0_109
| spl0_110 ),
inference(sat_conversion,[],[f2011]) ).
cnf(s401,plain,
( ~ spl0_29
| ~ spl0_90
| spl0_92
| spl0_173 ),
inference(sat_conversion,[],[f2014]) ).
cnf(s405,plain,
( ~ spl0_32
| ~ spl0_90
| spl0_91
| spl0_92 ),
inference(sat_conversion,[],[f2018]) ).
cnf(s411,plain,
( ~ spl0_48
| ~ spl0_88
| spl0_89
| ~ spl0_155 ),
inference(sat_conversion,[],[f2024]) ).
cnf(s424,plain,
( ~ spl0_54
| spl0_105
| ~ spl0_106
| spl0_107 ),
inference(sat_conversion,[],[f2037]) ).
cnf(s436,plain,
( ~ spl0_22
| spl0_66
| spl0_68
| spl0_160 ),
inference(sat_conversion,[],[f2049]) ).
cnf(s438,plain,
( ~ spl0_25
| ~ spl0_144
| spl0_146
| ~ spl0_159 ),
inference(sat_conversion,[],[f2051]) ).
cnf(s440,plain,
( ~ spl0_25
| ~ spl0_93
| ~ spl0_94
| spl0_95 ),
inference(sat_conversion,[],[f2053]) ).
cnf(s443,plain,
( ~ spl0_30
| spl0_117
| spl0_118
| spl0_119 ),
inference(sat_conversion,[],[f2056]) ).
cnf(s446,plain,
( ~ spl0_56
| ~ spl0_150
| spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s447,plain,
( ~ spl0_56
| ~ spl0_144
| ~ spl0_145
| spl0_159 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s450,plain,
( ~ spl0_27
| spl0_103
| ~ spl0_104
| spl0_163 ),
inference(sat_conversion,[],[f2063]) ).
cnf(s452,plain,
( ~ spl0_44
| spl0_91
| spl0_92
| spl0_173 ),
inference(sat_conversion,[],[f2065]) ).
cnf(s457,plain,
( ~ spl0_39
| ~ spl0_111
| spl0_112
| spl0_113 ),
inference(sat_conversion,[],[f2117]) ).
cnf(s465,plain,
( ~ spl0_61
| spl0_138
| ~ spl0_139
| ~ spl0_140 ),
inference(sat_conversion,[],[f2189]) ).
cnf(s466,plain,
( spl0_4
| spl0_3
| ~ spl0_19 ),
inference(rat,[],[s387,s50,s56,s446,s177,s178,s179,s52,s443,s133,s134,s135,s23,s289,s173,s174,s175,s53,s411,s358,s343,s308,s336,s93,s94,s95,s21,s268,s73,s74,s75,s2,s31]) ).
cnf(s467,plain,
( spl0_30
| spl0_58
| ~ spl0_4
| ~ spl0_19 ),
inference(rat,[],[s387,s50,s56,s324,s446,s450,s177,s178,s179,s17,s52,s359,s113,s114,s115]) ).
cnf(s468,plain,
( spl0_6
| ~ spl0_30 ),
inference(rat,[],[s443,s133,s134,s135]) ).
cnf(s469,plain,
( ~ spl0_36
| ~ spl0_4
| ~ spl0_19 ),
inference(rat,[],[s289,s173,s174,s175,s53,s344,s311,s359,s113,s114,s115]) ).
cnf(s470,plain,
( spl0_3
| ~ spl0_19 ),
inference(rat,[],[s337,s450,s467,s17,s468,s23,s469,s113,s114,s115,s466]) ).
cnf(s471,plain,
( spl0_30
| ~ spl0_4
| ~ spl0_19 ),
inference(rat,[],[s337,s450,s467,s17,s115,s114,s113]) ).
cnf(s472,plain,
( spl0_56
| spl0_48
| spl0_35
| ~ spl0_19 ),
inference(rat,[],[s387,s50,s56]) ).
cnf(s473,plain,
( spl0_47
| ~ spl0_56 ),
inference(rat,[],[s446,s177,s178,s179]) ).
cnf(s474,plain,
( ~ spl0_163
| spl0_58
| ~ spl0_4
| ~ spl0_19
| spl0_1 ),
inference(rat,[],[s424,s117,s118,s119,s12,s54,s438,s447,s169,s170,s171,s51,s473,s472,s344,s324,s359,s113,s114,s115]) ).
cnf(s475,plain,
( spl0_8
| ~ spl0_54 ),
inference(rat,[],[s424,s117,s118,s119]) ).
cnf(s479,plain,
( spl0_12
| ~ spl0_28 ),
inference(rat,[],[s250,s109,s110,s111]) ).
cnf(s480,plain,
( spl0_56
| spl0_49
| ~ spl0_12
| spl0_35
| ~ spl0_19 ),
inference(rat,[],[s60,s465,s161,s162,s163,s16,s401,s330,s50,s99,s98,s97,s470]) ).
cnf(s481,plain,
( ~ spl0_12
| spl0_66
| ~ spl0_67
| spl0_68
| spl0_35
| ~ spl0_19 ),
inference(rat,[],[s333,s480,s362,s436,s305,s19,s29,s91,s90,s89,s18,s405,s97,s98,s99,s470]) ).
cnf(s482,plain,
( ~ spl0_4
| spl0_2
| spl0_1 ),
inference(rat,[],[s474,s337,s450,s14,s479,s481,s65,s66,s67,s8,s185,s221,s138,s139,s41,s468,s471,s359,s113,s114,s115,s132,s361,s129,s130,s131]) ).
cnf(s483,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s475,s12,s54,s438,s447,s169,s170,s171,s51,s473,s472,s358,s343,s411,s308,s336,s93,s94,s95,s21,s268,s73,s74,s75,s2,s31,s482,s132]) ).
cnf(s484,plain,
( spl0_56
| ~ spl0_102
| spl0_103
| spl0_35
| ~ spl0_104
| spl0_1 ),
inference(rat,[],[s440,s101,s102,s103,s24,s311,s12,s324,s475,s472,s50,s100,s1,s483]) ).
cnf(s485,plain,
( ~ spl0_102
| spl0_103
| spl0_35
| ~ spl0_104
| spl0_1 ),
inference(rat,[],[s54,s475,s344,s12,s450,s438,s14,s447,s468,s169,s170,s171,s52,s51,s336,s93,s94,s95,s479,s21,s29,s269,s305,s473,s333,s484,s91,s90,s89,s18,s405,s97,s98,s99,s100,s1,s483]) ).
cnf(s486,plain,
( spl0_4
| spl0_35
| spl0_1 ),
inference(rat,[],[s398,s121,s122,s123,s35,s473,s472,s411,s308,s93,s94,s95,s21,s38,s268,s73,s74,s75,s2,s31,s100,s1,s483]) ).
cnf(s487,plain,
( spl0_35
| ~ spl0_104
| spl0_1 ),
inference(rat,[],[s485,s113,s114,s486]) ).
cnf(s488,plain,
( spl0_4
| ~ spl0_35
| spl0_1 ),
inference(rat,[],[s308,s411,s93,s94,s95,s360,s21,s38,s268,s73,s74,s75,s2,s31,s100,s1,s483]) ).
cnf(s489,plain,
( ~ spl0_104
| spl0_1 ),
inference(rat,[],[s359,s113,s114,s488,s487]) ).
cnf(s490,plain,
( spl0_4
| spl0_1 ),
inference(rat,[],[s488,s486]) ).
cnf(s491,plain,
spl0_1,
inference(rat,[],[s490,s115,s489]) ).
cnf(s492,plain,
spl0_19,
inference(rat,[],[s80,s491]) ).
cnf(s493,plain,
spl0_77,
inference(rat,[],[s79,s491]) ).
cnf(s494,plain,
spl0_76,
inference(rat,[],[s78,s491]) ).
cnf(s495,plain,
spl0_75,
inference(rat,[],[s77,s491]) ).
cnf(s496,plain,
spl0_3,
inference(rat,[],[s470,s492]) ).
cnf(s497,plain,
~ spl0_60,
inference(rat,[],[s382,s493,s494,s495]) ).
cnf(s498,plain,
~ spl0_92,
inference(rat,[],[s99,s496]) ).
cnf(s499,plain,
~ spl0_91,
inference(rat,[],[s98,s496]) ).
cnf(s500,plain,
spl0_90,
inference(rat,[],[s97,s496]) ).
cnf(s506,plain,
( ~ spl0_4
| spl0_52
| spl0_103
| ~ spl0_104
| spl0_35 ),
inference(rat,[],[s465,s161,s162,s163,s26,s457,s57,s125,s126,s127,s473,s37,s472,s362,s324,s401,s452,s363,s450,s330,s14,s55,s479,s481,s65,s66,s67,s8,s185,s221,s138,s139,s41,s468,s471,s469,s492,s498,s500,s499,s497]) ).
cnf(s507,plain,
( spl0_4
| spl0_35 ),
inference(rat,[],[s27,s468,s389,s52,s332,s473,s472,s411,s308,s336,s93,s94,s95,s21,s268,s73,s74,s75,s2,s31,s492,s494,s495,s493]) ).
cnf(s508,plain,
( spl0_2
| ~ spl0_52 ),
inference(rat,[],[s361,s129,s130,s131]) ).
cnf(s509,plain,
( ~ spl0_52
| spl0_35 ),
inference(rat,[],[s398,s121,s122,s123,s35,s473,s472,s411,s329,s94,s95,s21,s38,s268,s73,s74,s75,s3,s508,s468,s471,s507,s492]) ).
cnf(s510,plain,
spl0_35,
inference(rat,[],[s506,s115,s509,s114,s507]) ).
cnf(s511,plain,
spl0_4,
inference(rat,[],[s308,s358,s93,s95,s21,s268,s73,s74,s75,s2,s31,s510,s492]) ).
cnf(s512,plain,
~ spl0_103,
inference(rat,[],[s114,s511]) ).
cnf(s513,plain,
spl0_102,
inference(rat,[],[s113,s511]) ).
cnf(s516,plain,
~ spl0_104,
inference(rat,[],[s359,s513,s510,s512]) ).
cnf(s517,plain,
$false,
inference(rat,[],[s115,s516,s511]) ).
fof(f2190,plain,
$false,
inference(avatar_sat_refutation,[],[s517]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN445+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 16:03:38 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.13 Running first-order model finding
% 0.08/0.13 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.19 % (3484573)Will run a generic schedule for satisfiability detection.
% 0.08/0.19 % (3484579)% WARNING: option uhcvi not known.
% 0.08/0.19 % (3484580)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1869355182:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.08/0.19 % (3484578)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1050631843_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.19 % (3484579)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=254587463:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.08/0.19 % (3484583)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3888333183:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.08/0.19 % (3484581)dis+10_1_sil=32000:sp=arity:random_seed=2287054147:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.08/0.19 % (3484582)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=89920908:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.08/0.19 % (3484584)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2784295317:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.08/0.19 % Detected minimum model sizes of [1]
% 0.08/0.19 % Detected maximum model sizes of [30]
% 0.08/0.19 % TRYING [1]
% 0.08/0.19 % TRYING [2]
% 0.08/0.19 % TRYING [3]
% 0.08/0.19 % (3484584) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3484573-3484584"...
% 0.08/0.19 % TRYING [4]
% 0.08/0.19 % (3484584)...printing done.
% 0.08/0.19 % (3484581) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3484573-3484581"...
% 0.08/0.19 % (3484584)Refutation found. Thanks to Tanya!
% 0.08/0.19 % SZS status Theorem for theBenchmark
% 0.08/0.19 % SZS output start Proof for theBenchmark
% See solution above
% 0.08/0.19 % (3484584)------------------------------
% 0.08/0.19 % (3484584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.19 % (3484584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.19 % (3484584)CaDiCaL version: 2.1.3
% 0.08/0.19 % (3484584)Termination reason: Refutation
% 0.08/0.19 % (3484584)Time elapsed: 0.015 s
% 0.08/0.19 % (3484584)Peak memory usage: 13 MB
% 0.08/0.19 % (3484584)Instructions burned: 47 (million)
% 0.08/0.19 % (3484573)Success in time 0.053 s
% 0.08/0.19 % Vampire exiting
%------------------------------------------------------------------------------