%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN478+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 : Thu Sep 24 03:16:32 PM UTC 2026
% Result : Theorem 80.74s 10.83s
% Output : CNFRefutation 80.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 115
% Number of leaves : 1
% Syntax : Number of formulae : 747 ( 20 unt; 0 def)
% Number of atoms : 6236 ( 0 equ)
% Maximal formula atoms : 688 ( 8 avg)
% Number of connectives : 8866 (3377 ~;4487 |; 796 &)
% ( 0 <=>; 206 =>; 0 <=; 0 <~>)
% Maximal formula depth : 111 ( 7 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 33 prp; 0-1 aty)
% Number of functors : 31 ( 31 usr; 31 con; 0-0 aty)
% Number of variables : 747 ( 747 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ( ( hskp23
| hskp0
| hskp6 )
& ( hskp16
| hskp5
| hskp18 )
& ( hskp23
| hskp1
| hskp2 )
& ( hskp18
| hskp20 )
& ( hskp12
| hskp26 )
& ( hskp20
| hskp29
| hskp26 )
& ( hskp1
| hskp4
| hskp14 )
& ( hskp6
| hskp20
| hskp25 )
& ( hskp7
| hskp21
| hskp3 )
& ( hskp7
| hskp4
| hskp3 )
& ( hskp7
| hskp1
| hskp28 )
& ( hskp14
| hskp25
| hskp28 )
& ( hskp9
| hskp14
| hskp19 )
& ( hskp9
| hskp2
| hskp30 )
& ( hskp18
| hskp14
| hskp27 )
& ( hskp11
| hskp22
| ! [X97] :
( ndr1_0
=> ( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c1_1(X97) ) ) )
& ( hskp29
| ! [X96] :
( ndr1_0
=> ( ~ c3_1(X96)
| ~ c2_1(X96)
| ~ c1_1(X96) ) )
| ! [X95] :
( ndr1_0
=> ( ~ c3_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95) ) ) )
& ( hskp13
| ! [X94] :
( ndr1_0
=> ( ~ c2_1(X94)
| ~ c1_1(X94)
| ~ c0_1(X94) ) ) )
& ( hskp17
| ! [X93] :
( ndr1_0
=> ( ~ c3_1(X93)
| ~ c2_1(X93)
| ~ c1_1(X93) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c2_1(X92)
| ~ c1_1(X92)
| ~ c0_1(X92) ) ) )
& ( hskp5
| ! [X91] :
( ndr1_0
=> ( ~ c3_1(X91)
| ~ c1_1(X91)
| ~ c0_1(X91) ) )
| ! [X90] :
( ndr1_0
=> ( ~ c2_1(X90)
| ~ c1_1(X90)
| c3_1(X90) ) ) )
& ( hskp6
| hskp9
| ! [X89] :
( ndr1_0
=> ( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89) ) ) )
& ( hskp12
| hskp14
| ! [X88] :
( ndr1_0
=> ( ~ c2_1(X88)
| ~ c0_1(X88)
| c3_1(X88) ) ) )
& ( hskp18
| hskp30
| ! [X87] :
( ndr1_0
=> ( ~ c2_1(X87)
| ~ c0_1(X87)
| c3_1(X87) ) ) )
& ( hskp11
| ! [X86] :
( ndr1_0
=> ( ~ c3_1(X86)
| ~ c1_1(X86)
| ~ c0_1(X86) ) )
| ! [X85] :
( ndr1_0
=> ( ~ c2_1(X85)
| ~ c0_1(X85)
| c3_1(X85) ) ) )
& ( hskp24
| hskp20
| ! [X84] :
( ndr1_0
=> ( ~ c1_1(X84)
| ~ c0_1(X84)
| c3_1(X84) ) ) )
& ( hskp8
| hskp14
| ! [X83] :
( ndr1_0
=> ( ~ c1_1(X83)
| ~ c0_1(X83)
| c3_1(X83) ) ) )
& ( hskp13
| hskp14
| ! [X82] :
( ndr1_0
=> ( ~ c1_1(X82)
| c3_1(X82)
| c2_1(X82) ) ) )
& ( hskp16
| hskp14
| ! [X81] :
( ndr1_0
=> ( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81) ) ) )
& ( hskp17
| hskp4
| ! [X80] :
( ndr1_0
=> ( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80) ) ) )
& ( hskp27
| ! [X79] :
( ndr1_0
=> ( ~ c1_1(X79)
| ~ c0_1(X79)
| c3_1(X79) ) )
| ! [X78] :
( ndr1_0
=> ( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78) ) ) )
& ( hskp23
| hskp22
| ! [X77] :
( ndr1_0
=> ( ~ c3_1(X77)
| ~ c2_1(X77)
| c1_1(X77) ) ) )
& ( hskp2
| hskp22
| ! [X76] :
( ndr1_0
=> ( ~ c3_1(X76)
| ~ c2_1(X76)
| c1_1(X76) ) ) )
& ( hskp27
| ! [X75] :
( ndr1_0
=> ( ~ c3_1(X75)
| ~ c0_1(X75)
| c2_1(X75) ) )
| ! [X74] :
( ndr1_0
=> ( ~ c3_1(X74)
| ~ c2_1(X74)
| c1_1(X74) ) ) )
& ( hskp20
| ! [X73] :
( ndr1_0
=> ( ~ c1_1(X73)
| c3_1(X73)
| c2_1(X73) ) )
| ! [X72] :
( ndr1_0
=> ( ~ c3_1(X72)
| ~ c0_1(X72)
| c1_1(X72) ) ) )
& ( hskp0
| hskp21
| ! [X71] :
( ndr1_0
=> ( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71) ) ) )
& ( hskp0
| hskp12
| ! [X70] :
( ndr1_0
=> ( ~ c2_1(X70)
| ~ c0_1(X70)
| c1_1(X70) ) ) )
& ( hskp2
| hskp20
| ! [X69] :
( ndr1_0
=> ( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69) ) ) )
& ( hskp1
| hskp10
| ! [X68] :
( ndr1_0
=> ( ~ c2_1(X68)
| c3_1(X68)
| c1_1(X68) ) ) )
& ( hskp15
| hskp19
| ! [X67] :
( ndr1_0
=> ( ~ c0_1(X67)
| c3_1(X67)
| c1_1(X67) ) ) )
& ( hskp1
| hskp2
| ! [X66] :
( ndr1_0
=> ( ~ c3_1(X66)
| c2_1(X66)
| c1_1(X66) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( ~ c2_1(X65)
| ~ c1_1(X65)
| c3_1(X65) ) )
| ! [X64] :
( ndr1_0
=> ( ~ c1_1(X64)
| ~ c0_1(X64)
| c3_1(X64) ) )
| ! [X63] :
( ndr1_0
=> ( ~ c3_1(X63)
| c2_1(X63)
| c1_1(X63) ) ) )
& ( ! [X62] :
( ndr1_0
=> ( ~ c0_1(X62)
| c3_1(X62)
| c2_1(X62) ) )
| ! [X61] :
( ndr1_0
=> ( ~ c2_1(X61)
| ~ c0_1(X61)
| c1_1(X61) ) )
| ! [X60] :
( ndr1_0
=> ( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60) ) ) )
& ( hskp7
| hskp8
| ! [X59] :
( ndr1_0
=> ( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59) ) ) )
& ( hskp18
| hskp29
| ! [X58] :
( ndr1_0
=> ( ~ c0_1(X58)
| c2_1(X58)
| c1_1(X58) ) ) )
& ( hskp14
| ! [X57] :
( ndr1_0
=> ( ~ c2_1(X57)
| ~ c0_1(X57)
| c3_1(X57) ) )
| ! [X56] :
( ndr1_0
=> ( ~ c0_1(X56)
| c2_1(X56)
| c1_1(X56) ) ) )
& ( hskp15
| ! [X55] :
( ndr1_0
=> ( ~ c0_1(X55)
| c3_1(X55)
| c1_1(X55) ) )
| ! [X54] :
( ndr1_0
=> ( ~ c0_1(X54)
| c2_1(X54)
| c1_1(X54) ) ) )
& ( hskp0
| ! [X53] :
( ndr1_0
=> ( ~ c1_1(X53)
| ~ c0_1(X53)
| c2_1(X53) ) )
| ! [X52] :
( ndr1_0
=> ( ~ c3_1(X52)
| ~ c2_1(X52)
| c0_1(X52) ) ) )
& ( hskp17
| hskp16
| ! [X51] :
( ndr1_0
=> ( ~ c2_1(X51)
| ~ c1_1(X51)
| c0_1(X51) ) ) )
& ( hskp28
| ! [X50] :
( ndr1_0
=> ( ~ c3_1(X50)
| ~ c0_1(X50)
| c2_1(X50) ) )
| ! [X49] :
( ndr1_0
=> ( ~ c2_1(X49)
| ~ c1_1(X49)
| c0_1(X49) ) ) )
& ( hskp15
| hskp14
| ! [X48] :
( ndr1_0
=> ( ~ c2_1(X48)
| c3_1(X48)
| c0_1(X48) ) ) )
& ( ! [X47] :
( ndr1_0
=> ( ~ c3_1(X47)
| ~ c1_1(X47)
| ~ c0_1(X47) ) )
| ! [X46] :
( ndr1_0
=> ( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c2_1(X45)
| c3_1(X45)
| c0_1(X45) ) ) )
& ( ! [X44] :
( ndr1_0
=> ( ~ c2_1(X44)
| ~ c0_1(X44)
| c1_1(X44) ) )
| ! [X43] :
( ndr1_0
=> ( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43) ) )
| ! [X42] :
( ndr1_0
=> ( ~ c2_1(X42)
| c3_1(X42)
| c0_1(X42) ) ) )
& ( hskp4
| ! [X41] :
( ndr1_0
=> ( ~ c3_1(X41)
| ~ c1_1(X41)
| c0_1(X41) ) )
| ! [X40] :
( ndr1_0
=> ( ~ c2_1(X40)
| c3_1(X40)
| c0_1(X40) ) ) )
& ( hskp28
| ! [X39] :
( ndr1_0
=> ( ~ c1_1(X39)
| c3_1(X39)
| c0_1(X39) ) ) )
& ( hskp12
| ! [X38] :
( ndr1_0
=> ( ~ c2_1(X38)
| ~ c1_1(X38)
| ~ c0_1(X38) ) )
| ! [X37] :
( ndr1_0
=> ( ~ c1_1(X37)
| c3_1(X37)
| c0_1(X37) ) ) )
& ( ! [X36] :
( ndr1_0
=> ( ~ c1_1(X36)
| ~ c0_1(X36)
| c3_1(X36) ) )
| ! [X35] :
( ndr1_0
=> ( c3_1(X35)
| c2_1(X35)
| c1_1(X35) ) )
| ! [X34] :
( ndr1_0
=> ( ~ c1_1(X34)
| c3_1(X34)
| c0_1(X34) ) ) )
& ( hskp13
| ! [X33] :
( ndr1_0
=> ( ~ c0_1(X33)
| c3_1(X33)
| c1_1(X33) ) )
| ! [X32] :
( ndr1_0
=> ( ~ c3_1(X32)
| c2_1(X32)
| c0_1(X32) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( ~ c3_1(X31)
| ~ c0_1(X31)
| c1_1(X31) ) )
| ! [X30] :
( ndr1_0
=> ( ~ c3_1(X30)
| ~ c1_1(X30)
| c0_1(X30) ) )
| ! [X29] :
( ndr1_0
=> ( ~ c3_1(X29)
| c2_1(X29)
| c0_1(X29) ) ) )
& ( hskp12
| ! [X28] :
( ndr1_0
=> ( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X27] :
( ndr1_0
=> ( ~ c1_1(X27)
| c2_1(X27)
| c0_1(X27) ) ) )
& ( hskp11
| ! [X26] :
( ndr1_0
=> ( c3_1(X26)
| c2_1(X26)
| c1_1(X26) ) )
| ! [X25] :
( ndr1_0
=> ( ~ c1_1(X25)
| c2_1(X25)
| c0_1(X25) ) ) )
& ( hskp9
| ! [X24] :
( ndr1_0
=> ( ~ c1_1(X24)
| c3_1(X24)
| c0_1(X24) ) )
| ! [X23] :
( ndr1_0
=> ( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) ) ) )
& ( ! [X22] :
( ndr1_0
=> ( ~ c1_1(X22)
| c3_1(X22)
| c2_1(X22) ) )
| ! [X21] :
( ndr1_0
=> ( ~ c3_1(X21)
| c2_1(X21)
| c0_1(X21) ) )
| ! [X20] :
( ndr1_0
=> ( ~ c1_1(X20)
| c2_1(X20)
| c0_1(X20) ) ) )
& ( hskp6
| hskp10
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| c2_1(X19)
| c0_1(X19) ) ) )
& ( hskp9
| ! [X18] :
( ndr1_0
=> ( ~ c0_1(X18)
| c3_1(X18)
| c2_1(X18) ) )
| ! [X17] :
( ndr1_0
=> ( c3_1(X17)
| c2_1(X17)
| c0_1(X17) ) ) )
& ( hskp8
| ! [X16] :
( ndr1_0
=> ( ~ c3_1(X16)
| ~ c2_1(X16)
| c0_1(X16) ) )
| ! [X15] :
( ndr1_0
=> ( c3_1(X15)
| c2_1(X15)
| c0_1(X15) ) ) )
& ( hskp6
| ! [X14] :
( ndr1_0
=> ( ~ c2_1(X14)
| ~ c1_1(X14)
| c0_1(X14) ) )
| ! [X13] :
( ndr1_0
=> ( c3_1(X13)
| c2_1(X13)
| c0_1(X13) ) ) )
& ( hskp6
| ! [X12] :
( ndr1_0
=> ( ~ c2_1(X12)
| c3_1(X12)
| c0_1(X12) ) )
| ! [X11] :
( ndr1_0
=> ( c3_1(X11)
| c2_1(X11)
| c0_1(X11) ) ) )
& ( hskp7
| ! [X10] :
( ndr1_0
=> ( ~ c3_1(X10)
| ~ c1_1(X10)
| c2_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( ~ c3_1(X9)
| c1_1(X9)
| c0_1(X9) ) ) )
& ( hskp6
| hskp5
| ! [X8] :
( ndr1_0
=> ( ~ c2_1(X8)
| c1_1(X8)
| c0_1(X8) ) ) )
& ( hskp2
| hskp4
| ! [X7] :
( ndr1_0
=> ( ~ c2_1(X7)
| c1_1(X7)
| c0_1(X7) ) ) )
& ( hskp3
| ! [X6] :
( ndr1_0
=> ( ~ c3_1(X6)
| ~ c0_1(X6)
| c2_1(X6) ) )
| ! [X5] :
( ndr1_0
=> ( c3_1(X5)
| c1_1(X5)
| c0_1(X5) ) ) )
& ( ! [X4] :
( ndr1_0
=> ( ~ c2_1(X4)
| c3_1(X4)
| c1_1(X4) ) )
| ! [X3] :
( ndr1_0
=> ( ~ c2_1(X3)
| c1_1(X3)
| c0_1(X3) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ) )
& ( hskp1
| hskp2
| ! [X1] :
( ndr1_0
=> ( c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ) )
& ( hskp1
| hskp27
| ! [Z] :
( ndr1_0
=> ( c2_1(Z)
| c1_1(Z)
| c0_1(Z) ) ) )
& ( ! [Y] :
( ndr1_0
=> ( ~ c1_1(Y)
| ~ c0_1(Y)
| c3_1(Y) ) )
| ! [X] :
( ndr1_0
=> ( ~ c3_1(X)
| ~ c1_1(X)
| c2_1(X) ) )
| ! [W] :
( ndr1_0
=> ( c2_1(W)
| c1_1(W)
| c0_1(W) ) ) )
& ( hskp0
| ! [V] :
( ndr1_0
=> ( ~ c2_1(V)
| c3_1(V)
| c1_1(V) ) )
| ! [U] :
( ndr1_0
=> ( c2_1(U)
| c1_1(U)
| c0_1(U) ) ) )
& ( ( c3_1(a1372)
& c1_1(a1372)
& c0_1(a1372)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a1338)
& c2_1(a1338)
& c1_1(a1338)
& ndr1_0 )
| ~ hskp29 )
& ( ( c3_1(a1328)
& c2_1(a1328)
& c0_1(a1328)
& ndr1_0 )
| ~ hskp28 )
& ( ( c2_1(a1307)
& c1_1(a1307)
& c0_1(a1307)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a1411)
& ~ c2_1(a1411)
& c0_1(a1411)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c3_1(a1394)
& c2_1(a1394)
& c0_1(a1394)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c3_1(a1370)
& ~ c1_1(a1370)
& c2_1(a1370)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a1359)
& ~ c1_1(a1359)
& ~ c0_1(a1359)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c3_1(a1356)
& c1_1(a1356)
& c0_1(a1356)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c2_1(a1352)
& ~ c0_1(a1352)
& c3_1(a1352)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c0_1(a1348)
& c2_1(a1348)
& c1_1(a1348)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c2_1(a1344)
& c1_1(a1344)
& c0_1(a1344)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c2_1(a1339)
& ~ c0_1(a1339)
& c1_1(a1339)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c0_1(a1334)
& c3_1(a1334)
& c2_1(a1334)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a1333)
& ~ c2_1(a1333)
& c1_1(a1333)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c3_1(a1331)
& c2_1(a1331)
& c1_1(a1331)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c2_1(a1330)
& ~ c1_1(a1330)
& c0_1(a1330)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c3_1(a1326)
& ~ c2_1(a1326)
& ~ c1_1(a1326)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c0_1(a1325)
& c3_1(a1325)
& c1_1(a1325)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c1_1(a1324)
& c3_1(a1324)
& c0_1(a1324)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c2_1(a1321)
& c3_1(a1321)
& c0_1(a1321)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c1_1(a1320)
& ~ c0_1(a1320)
& c2_1(a1320)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c3_1(a1319)
& ~ c0_1(a1319)
& c2_1(a1319)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a1316)
& ~ c2_1(a1316)
& ~ c0_1(a1316)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a1315)
& ~ c0_1(a1315)
& c3_1(a1315)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a1314)
& ~ c0_1(a1314)
& c1_1(a1314)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c3_1(a1312)
& ~ c1_1(a1312)
& c0_1(a1312)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c1_1(a1311)
& c2_1(a1311)
& c0_1(a1311)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c2_1(a1309)
& c3_1(a1309)
& c1_1(a1309)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c2_1(a1308)
& ~ c1_1(a1308)
& c3_1(a1308)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c2_1(a1306)
& ~ c1_1(a1306)
& ~ c0_1(a1306)
& ndr1_0 )
| ~ hskp0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ( ( hskp23
| hskp0
| hskp6 )
& ( hskp16
| hskp5
| hskp18 )
& ( hskp23
| hskp1
| hskp2 )
& ( hskp18
| hskp20 )
& ( hskp12
| hskp26 )
& ( hskp20
| hskp29
| hskp26 )
& ( hskp1
| hskp4
| hskp14 )
& ( hskp6
| hskp20
| hskp25 )
& ( hskp7
| hskp21
| hskp3 )
& ( hskp7
| hskp4
| hskp3 )
& ( hskp7
| hskp1
| hskp28 )
& ( hskp14
| hskp25
| hskp28 )
& ( hskp9
| hskp14
| hskp19 )
& ( hskp9
| hskp2
| hskp30 )
& ( hskp18
| hskp14
| hskp27 )
& ( hskp11
| hskp22
| ! [X97] :
( ndr1_0
=> ( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c1_1(X97) ) ) )
& ( hskp29
| ! [X96] :
( ndr1_0
=> ( ~ c3_1(X96)
| ~ c2_1(X96)
| ~ c1_1(X96) ) )
| ! [X95] :
( ndr1_0
=> ( ~ c3_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95) ) ) )
& ( hskp13
| ! [X94] :
( ndr1_0
=> ( ~ c2_1(X94)
| ~ c1_1(X94)
| ~ c0_1(X94) ) ) )
& ( hskp17
| ! [X93] :
( ndr1_0
=> ( ~ c3_1(X93)
| ~ c2_1(X93)
| ~ c1_1(X93) ) )
| ! [X92] :
( ndr1_0
=> ( ~ c2_1(X92)
| ~ c1_1(X92)
| ~ c0_1(X92) ) ) )
& ( hskp5
| ! [X91] :
( ndr1_0
=> ( ~ c3_1(X91)
| ~ c1_1(X91)
| ~ c0_1(X91) ) )
| ! [X90] :
( ndr1_0
=> ( ~ c2_1(X90)
| ~ c1_1(X90)
| c3_1(X90) ) ) )
& ( hskp6
| hskp9
| ! [X89] :
( ndr1_0
=> ( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89) ) ) )
& ( hskp12
| hskp14
| ! [X88] :
( ndr1_0
=> ( ~ c2_1(X88)
| ~ c0_1(X88)
| c3_1(X88) ) ) )
& ( hskp18
| hskp30
| ! [X87] :
( ndr1_0
=> ( ~ c2_1(X87)
| ~ c0_1(X87)
| c3_1(X87) ) ) )
& ( hskp11
| ! [X86] :
( ndr1_0
=> ( ~ c3_1(X86)
| ~ c1_1(X86)
| ~ c0_1(X86) ) )
| ! [X85] :
( ndr1_0
=> ( ~ c2_1(X85)
| ~ c0_1(X85)
| c3_1(X85) ) ) )
& ( hskp24
| hskp20
| ! [X84] :
( ndr1_0
=> ( ~ c1_1(X84)
| ~ c0_1(X84)
| c3_1(X84) ) ) )
& ( hskp8
| hskp14
| ! [X83] :
( ndr1_0
=> ( ~ c1_1(X83)
| ~ c0_1(X83)
| c3_1(X83) ) ) )
& ( hskp13
| hskp14
| ! [X82] :
( ndr1_0
=> ( ~ c1_1(X82)
| c3_1(X82)
| c2_1(X82) ) ) )
& ( hskp16
| hskp14
| ! [X81] :
( ndr1_0
=> ( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81) ) ) )
& ( hskp17
| hskp4
| ! [X80] :
( ndr1_0
=> ( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80) ) ) )
& ( hskp27
| ! [X79] :
( ndr1_0
=> ( ~ c1_1(X79)
| ~ c0_1(X79)
| c3_1(X79) ) )
| ! [X78] :
( ndr1_0
=> ( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78) ) ) )
& ( hskp23
| hskp22
| ! [X77] :
( ndr1_0
=> ( ~ c3_1(X77)
| ~ c2_1(X77)
| c1_1(X77) ) ) )
& ( hskp2
| hskp22
| ! [X76] :
( ndr1_0
=> ( ~ c3_1(X76)
| ~ c2_1(X76)
| c1_1(X76) ) ) )
& ( hskp27
| ! [X75] :
( ndr1_0
=> ( ~ c3_1(X75)
| ~ c0_1(X75)
| c2_1(X75) ) )
| ! [X74] :
( ndr1_0
=> ( ~ c3_1(X74)
| ~ c2_1(X74)
| c1_1(X74) ) ) )
& ( hskp20
| ! [X73] :
( ndr1_0
=> ( ~ c1_1(X73)
| c3_1(X73)
| c2_1(X73) ) )
| ! [X72] :
( ndr1_0
=> ( ~ c3_1(X72)
| ~ c0_1(X72)
| c1_1(X72) ) ) )
& ( hskp0
| hskp21
| ! [X71] :
( ndr1_0
=> ( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71) ) ) )
& ( hskp0
| hskp12
| ! [X70] :
( ndr1_0
=> ( ~ c2_1(X70)
| ~ c0_1(X70)
| c1_1(X70) ) ) )
& ( hskp2
| hskp20
| ! [X69] :
( ndr1_0
=> ( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69) ) ) )
& ( hskp1
| hskp10
| ! [X68] :
( ndr1_0
=> ( ~ c2_1(X68)
| c3_1(X68)
| c1_1(X68) ) ) )
& ( hskp15
| hskp19
| ! [X67] :
( ndr1_0
=> ( ~ c0_1(X67)
| c3_1(X67)
| c1_1(X67) ) ) )
& ( hskp1
| hskp2
| ! [X66] :
( ndr1_0
=> ( ~ c3_1(X66)
| c2_1(X66)
| c1_1(X66) ) ) )
& ( ! [X65] :
( ndr1_0
=> ( ~ c2_1(X65)
| ~ c1_1(X65)
| c3_1(X65) ) )
| ! [X64] :
( ndr1_0
=> ( ~ c1_1(X64)
| ~ c0_1(X64)
| c3_1(X64) ) )
| ! [X63] :
( ndr1_0
=> ( ~ c3_1(X63)
| c2_1(X63)
| c1_1(X63) ) ) )
& ( ! [X62] :
( ndr1_0
=> ( ~ c0_1(X62)
| c3_1(X62)
| c2_1(X62) ) )
| ! [X61] :
( ndr1_0
=> ( ~ c2_1(X61)
| ~ c0_1(X61)
| c1_1(X61) ) )
| ! [X60] :
( ndr1_0
=> ( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60) ) ) )
& ( hskp7
| hskp8
| ! [X59] :
( ndr1_0
=> ( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59) ) ) )
& ( hskp18
| hskp29
| ! [X58] :
( ndr1_0
=> ( ~ c0_1(X58)
| c2_1(X58)
| c1_1(X58) ) ) )
& ( hskp14
| ! [X57] :
( ndr1_0
=> ( ~ c2_1(X57)
| ~ c0_1(X57)
| c3_1(X57) ) )
| ! [X56] :
( ndr1_0
=> ( ~ c0_1(X56)
| c2_1(X56)
| c1_1(X56) ) ) )
& ( hskp15
| ! [X55] :
( ndr1_0
=> ( ~ c0_1(X55)
| c3_1(X55)
| c1_1(X55) ) )
| ! [X54] :
( ndr1_0
=> ( ~ c0_1(X54)
| c2_1(X54)
| c1_1(X54) ) ) )
& ( hskp0
| ! [X53] :
( ndr1_0
=> ( ~ c1_1(X53)
| ~ c0_1(X53)
| c2_1(X53) ) )
| ! [X52] :
( ndr1_0
=> ( ~ c3_1(X52)
| ~ c2_1(X52)
| c0_1(X52) ) ) )
& ( hskp17
| hskp16
| ! [X51] :
( ndr1_0
=> ( ~ c2_1(X51)
| ~ c1_1(X51)
| c0_1(X51) ) ) )
& ( hskp28
| ! [X50] :
( ndr1_0
=> ( ~ c3_1(X50)
| ~ c0_1(X50)
| c2_1(X50) ) )
| ! [X49] :
( ndr1_0
=> ( ~ c2_1(X49)
| ~ c1_1(X49)
| c0_1(X49) ) ) )
& ( hskp15
| hskp14
| ! [X48] :
( ndr1_0
=> ( ~ c2_1(X48)
| c3_1(X48)
| c0_1(X48) ) ) )
& ( ! [X47] :
( ndr1_0
=> ( ~ c3_1(X47)
| ~ c1_1(X47)
| ~ c0_1(X47) ) )
| ! [X46] :
( ndr1_0
=> ( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46) ) )
| ! [X45] :
( ndr1_0
=> ( ~ c2_1(X45)
| c3_1(X45)
| c0_1(X45) ) ) )
& ( ! [X44] :
( ndr1_0
=> ( ~ c2_1(X44)
| ~ c0_1(X44)
| c1_1(X44) ) )
| ! [X43] :
( ndr1_0
=> ( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43) ) )
| ! [X42] :
( ndr1_0
=> ( ~ c2_1(X42)
| c3_1(X42)
| c0_1(X42) ) ) )
& ( hskp4
| ! [X41] :
( ndr1_0
=> ( ~ c3_1(X41)
| ~ c1_1(X41)
| c0_1(X41) ) )
| ! [X40] :
( ndr1_0
=> ( ~ c2_1(X40)
| c3_1(X40)
| c0_1(X40) ) ) )
& ( hskp28
| ! [X39] :
( ndr1_0
=> ( ~ c1_1(X39)
| c3_1(X39)
| c0_1(X39) ) ) )
& ( hskp12
| ! [X38] :
( ndr1_0
=> ( ~ c2_1(X38)
| ~ c1_1(X38)
| ~ c0_1(X38) ) )
| ! [X37] :
( ndr1_0
=> ( ~ c1_1(X37)
| c3_1(X37)
| c0_1(X37) ) ) )
& ( ! [X36] :
( ndr1_0
=> ( ~ c1_1(X36)
| ~ c0_1(X36)
| c3_1(X36) ) )
| ! [X35] :
( ndr1_0
=> ( c3_1(X35)
| c2_1(X35)
| c1_1(X35) ) )
| ! [X34] :
( ndr1_0
=> ( ~ c1_1(X34)
| c3_1(X34)
| c0_1(X34) ) ) )
& ( hskp13
| ! [X33] :
( ndr1_0
=> ( ~ c0_1(X33)
| c3_1(X33)
| c1_1(X33) ) )
| ! [X32] :
( ndr1_0
=> ( ~ c3_1(X32)
| c2_1(X32)
| c0_1(X32) ) ) )
& ( ! [X31] :
( ndr1_0
=> ( ~ c3_1(X31)
| ~ c0_1(X31)
| c1_1(X31) ) )
| ! [X30] :
( ndr1_0
=> ( ~ c3_1(X30)
| ~ c1_1(X30)
| c0_1(X30) ) )
| ! [X29] :
( ndr1_0
=> ( ~ c3_1(X29)
| c2_1(X29)
| c0_1(X29) ) ) )
& ( hskp12
| ! [X28] :
( ndr1_0
=> ( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28) ) )
| ! [X27] :
( ndr1_0
=> ( ~ c1_1(X27)
| c2_1(X27)
| c0_1(X27) ) ) )
& ( hskp11
| ! [X26] :
( ndr1_0
=> ( c3_1(X26)
| c2_1(X26)
| c1_1(X26) ) )
| ! [X25] :
( ndr1_0
=> ( ~ c1_1(X25)
| c2_1(X25)
| c0_1(X25) ) ) )
& ( hskp9
| ! [X24] :
( ndr1_0
=> ( ~ c1_1(X24)
| c3_1(X24)
| c0_1(X24) ) )
| ! [X23] :
( ndr1_0
=> ( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) ) ) )
& ( ! [X22] :
( ndr1_0
=> ( ~ c1_1(X22)
| c3_1(X22)
| c2_1(X22) ) )
| ! [X21] :
( ndr1_0
=> ( ~ c3_1(X21)
| c2_1(X21)
| c0_1(X21) ) )
| ! [X20] :
( ndr1_0
=> ( ~ c1_1(X20)
| c2_1(X20)
| c0_1(X20) ) ) )
& ( hskp6
| hskp10
| ! [X19] :
( ndr1_0
=> ( c3_1(X19)
| c2_1(X19)
| c0_1(X19) ) ) )
& ( hskp9
| ! [X18] :
( ndr1_0
=> ( ~ c0_1(X18)
| c3_1(X18)
| c2_1(X18) ) )
| ! [X17] :
( ndr1_0
=> ( c3_1(X17)
| c2_1(X17)
| c0_1(X17) ) ) )
& ( hskp8
| ! [X16] :
( ndr1_0
=> ( ~ c3_1(X16)
| ~ c2_1(X16)
| c0_1(X16) ) )
| ! [X15] :
( ndr1_0
=> ( c3_1(X15)
| c2_1(X15)
| c0_1(X15) ) ) )
& ( hskp6
| ! [X14] :
( ndr1_0
=> ( ~ c2_1(X14)
| ~ c1_1(X14)
| c0_1(X14) ) )
| ! [X13] :
( ndr1_0
=> ( c3_1(X13)
| c2_1(X13)
| c0_1(X13) ) ) )
& ( hskp6
| ! [X12] :
( ndr1_0
=> ( ~ c2_1(X12)
| c3_1(X12)
| c0_1(X12) ) )
| ! [X11] :
( ndr1_0
=> ( c3_1(X11)
| c2_1(X11)
| c0_1(X11) ) ) )
& ( hskp7
| ! [X10] :
( ndr1_0
=> ( ~ c3_1(X10)
| ~ c1_1(X10)
| c2_1(X10) ) )
| ! [X9] :
( ndr1_0
=> ( ~ c3_1(X9)
| c1_1(X9)
| c0_1(X9) ) ) )
& ( hskp6
| hskp5
| ! [X8] :
( ndr1_0
=> ( ~ c2_1(X8)
| c1_1(X8)
| c0_1(X8) ) ) )
& ( hskp2
| hskp4
| ! [X7] :
( ndr1_0
=> ( ~ c2_1(X7)
| c1_1(X7)
| c0_1(X7) ) ) )
& ( hskp3
| ! [X6] :
( ndr1_0
=> ( ~ c3_1(X6)
| ~ c0_1(X6)
| c2_1(X6) ) )
| ! [X5] :
( ndr1_0
=> ( c3_1(X5)
| c1_1(X5)
| c0_1(X5) ) ) )
& ( ! [X4] :
( ndr1_0
=> ( ~ c2_1(X4)
| c3_1(X4)
| c1_1(X4) ) )
| ! [X3] :
( ndr1_0
=> ( ~ c2_1(X3)
| c1_1(X3)
| c0_1(X3) ) )
| ! [X2] :
( ndr1_0
=> ( c3_1(X2)
| c1_1(X2)
| c0_1(X2) ) ) )
& ( hskp1
| hskp2
| ! [X1] :
( ndr1_0
=> ( c2_1(X1)
| c1_1(X1)
| c0_1(X1) ) ) )
& ( hskp1
| hskp27
| ! [Z] :
( ndr1_0
=> ( c2_1(Z)
| c1_1(Z)
| c0_1(Z) ) ) )
& ( ! [Y] :
( ndr1_0
=> ( ~ c1_1(Y)
| ~ c0_1(Y)
| c3_1(Y) ) )
| ! [X] :
( ndr1_0
=> ( ~ c3_1(X)
| ~ c1_1(X)
| c2_1(X) ) )
| ! [W] :
( ndr1_0
=> ( c2_1(W)
| c1_1(W)
| c0_1(W) ) ) )
& ( hskp0
| ! [V] :
( ndr1_0
=> ( ~ c2_1(V)
| c3_1(V)
| c1_1(V) ) )
| ! [U] :
( ndr1_0
=> ( c2_1(U)
| c1_1(U)
| c0_1(U) ) ) )
& ( ( c3_1(a1372)
& c1_1(a1372)
& c0_1(a1372)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a1338)
& c2_1(a1338)
& c1_1(a1338)
& ndr1_0 )
| ~ hskp29 )
& ( ( c3_1(a1328)
& c2_1(a1328)
& c0_1(a1328)
& ndr1_0 )
| ~ hskp28 )
& ( ( c2_1(a1307)
& c1_1(a1307)
& c0_1(a1307)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a1411)
& ~ c2_1(a1411)
& c0_1(a1411)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c3_1(a1394)
& c2_1(a1394)
& c0_1(a1394)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c3_1(a1370)
& ~ c1_1(a1370)
& c2_1(a1370)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a1359)
& ~ c1_1(a1359)
& ~ c0_1(a1359)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c3_1(a1356)
& c1_1(a1356)
& c0_1(a1356)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c2_1(a1352)
& ~ c0_1(a1352)
& c3_1(a1352)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c0_1(a1348)
& c2_1(a1348)
& c1_1(a1348)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c2_1(a1344)
& c1_1(a1344)
& c0_1(a1344)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c2_1(a1339)
& ~ c0_1(a1339)
& c1_1(a1339)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c0_1(a1334)
& c3_1(a1334)
& c2_1(a1334)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a1333)
& ~ c2_1(a1333)
& c1_1(a1333)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c3_1(a1331)
& c2_1(a1331)
& c1_1(a1331)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c2_1(a1330)
& ~ c1_1(a1330)
& c0_1(a1330)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c3_1(a1326)
& ~ c2_1(a1326)
& ~ c1_1(a1326)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c0_1(a1325)
& c3_1(a1325)
& c1_1(a1325)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c1_1(a1324)
& c3_1(a1324)
& c0_1(a1324)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c2_1(a1321)
& c3_1(a1321)
& c0_1(a1321)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c1_1(a1320)
& ~ c0_1(a1320)
& c2_1(a1320)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c3_1(a1319)
& ~ c0_1(a1319)
& c2_1(a1319)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a1316)
& ~ c2_1(a1316)
& ~ c0_1(a1316)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a1315)
& ~ c0_1(a1315)
& c3_1(a1315)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a1314)
& ~ c0_1(a1314)
& c1_1(a1314)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c3_1(a1312)
& ~ c1_1(a1312)
& c0_1(a1312)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c1_1(a1311)
& c2_1(a1311)
& c0_1(a1311)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c2_1(a1309)
& c3_1(a1309)
& c1_1(a1309)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c2_1(a1308)
& ~ c1_1(a1308)
& c3_1(a1308)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c2_1(a1306)
& ~ c1_1(a1306)
& ~ c0_1(a1306)
& ndr1_0 )
| ~ hskp0 ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
( ( hskp23
| hskp0
| hskp6 )
& ( hskp16
| hskp5
| hskp18 )
& ( hskp23
| hskp1
| hskp2 )
& ( hskp18
| hskp20 )
& ( hskp12
| hskp26 )
& ( hskp20
| hskp29
| hskp26 )
& ( hskp1
| hskp4
| hskp14 )
& ( hskp6
| hskp20
| hskp25 )
& ( hskp7
| hskp21
| hskp3 )
& ( hskp7
| hskp4
| hskp3 )
& ( hskp7
| hskp1
| hskp28 )
& ( hskp14
| hskp25
| hskp28 )
& ( hskp9
| hskp14
| hskp19 )
& ( hskp9
| hskp2
| hskp30 )
& ( hskp18
| hskp14
| hskp27 )
& ( hskp11
| hskp22
| ! [X97] :
( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c1_1(X97)
| ~ ndr1_0 ) )
& ( hskp29
| ! [X96] :
( ~ c3_1(X96)
| ~ c2_1(X96)
| ~ c1_1(X96)
| ~ ndr1_0 )
| ! [X95] :
( ~ c3_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95)
| ~ ndr1_0 ) )
& ( hskp13
| ! [X94] :
( ~ c2_1(X94)
| ~ c1_1(X94)
| ~ c0_1(X94)
| ~ ndr1_0 ) )
& ( hskp17
| ! [X93] :
( ~ c3_1(X93)
| ~ c2_1(X93)
| ~ c1_1(X93)
| ~ ndr1_0 )
| ! [X92] :
( ~ c2_1(X92)
| ~ c1_1(X92)
| ~ c0_1(X92)
| ~ ndr1_0 ) )
& ( hskp5
| ! [X91] :
( ~ c3_1(X91)
| ~ c1_1(X91)
| ~ c0_1(X91)
| ~ ndr1_0 )
| ! [X90] :
( ~ c2_1(X90)
| ~ c1_1(X90)
| c3_1(X90)
| ~ ndr1_0 ) )
& ( hskp6
| hskp9
| ! [X89] :
( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89)
| ~ ndr1_0 ) )
& ( hskp12
| hskp14
| ! [X88] :
( ~ c2_1(X88)
| ~ c0_1(X88)
| c3_1(X88)
| ~ ndr1_0 ) )
& ( hskp18
| hskp30
| ! [X87] :
( ~ c2_1(X87)
| ~ c0_1(X87)
| c3_1(X87)
| ~ ndr1_0 ) )
& ( hskp11
| ! [X86] :
( ~ c3_1(X86)
| ~ c1_1(X86)
| ~ c0_1(X86)
| ~ ndr1_0 )
| ! [X85] :
( ~ c2_1(X85)
| ~ c0_1(X85)
| c3_1(X85)
| ~ ndr1_0 ) )
& ( hskp24
| hskp20
| ! [X84] :
( ~ c1_1(X84)
| ~ c0_1(X84)
| c3_1(X84)
| ~ ndr1_0 ) )
& ( hskp8
| hskp14
| ! [X83] :
( ~ c1_1(X83)
| ~ c0_1(X83)
| c3_1(X83)
| ~ ndr1_0 ) )
& ( hskp13
| hskp14
| ! [X82] :
( ~ c1_1(X82)
| c3_1(X82)
| c2_1(X82)
| ~ ndr1_0 ) )
& ( hskp16
| hskp14
| ! [X81] :
( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81)
| ~ ndr1_0 ) )
& ( hskp17
| hskp4
| ! [X80] :
( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80)
| ~ ndr1_0 ) )
& ( hskp27
| ! [X79] :
( ~ c1_1(X79)
| ~ c0_1(X79)
| c3_1(X79)
| ~ ndr1_0 )
| ! [X78] :
( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78)
| ~ ndr1_0 ) )
& ( hskp23
| hskp22
| ! [X77] :
( ~ c3_1(X77)
| ~ c2_1(X77)
| c1_1(X77)
| ~ ndr1_0 ) )
& ( hskp2
| hskp22
| ! [X76] :
( ~ c3_1(X76)
| ~ c2_1(X76)
| c1_1(X76)
| ~ ndr1_0 ) )
& ( hskp27
| ! [X75] :
( ~ c3_1(X75)
| ~ c0_1(X75)
| c2_1(X75)
| ~ ndr1_0 )
| ! [X74] :
( ~ c3_1(X74)
| ~ c2_1(X74)
| c1_1(X74)
| ~ ndr1_0 ) )
& ( hskp20
| ! [X73] :
( ~ c1_1(X73)
| c3_1(X73)
| c2_1(X73)
| ~ ndr1_0 )
| ! [X72] :
( ~ c3_1(X72)
| ~ c0_1(X72)
| c1_1(X72)
| ~ ndr1_0 ) )
& ( hskp0
| hskp21
| ! [X71] :
( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71)
| ~ ndr1_0 ) )
& ( hskp0
| hskp12
| ! [X70] :
( ~ c2_1(X70)
| ~ c0_1(X70)
| c1_1(X70)
| ~ ndr1_0 ) )
& ( hskp2
| hskp20
| ! [X69] :
( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69)
| ~ ndr1_0 ) )
& ( hskp1
| hskp10
| ! [X68] :
( ~ c2_1(X68)
| c3_1(X68)
| c1_1(X68)
| ~ ndr1_0 ) )
& ( hskp15
| hskp19
| ! [X67] :
( ~ c0_1(X67)
| c3_1(X67)
| c1_1(X67)
| ~ ndr1_0 ) )
& ( hskp1
| hskp2
| ! [X66] :
( ~ c3_1(X66)
| c2_1(X66)
| c1_1(X66)
| ~ ndr1_0 ) )
& ( ! [X65] :
( ~ c2_1(X65)
| ~ c1_1(X65)
| c3_1(X65)
| ~ ndr1_0 )
| ! [X64] :
( ~ c1_1(X64)
| ~ c0_1(X64)
| c3_1(X64)
| ~ ndr1_0 )
| ! [X63] :
( ~ c3_1(X63)
| c2_1(X63)
| c1_1(X63)
| ~ ndr1_0 ) )
& ( ! [X62] :
( ~ c0_1(X62)
| c3_1(X62)
| c2_1(X62)
| ~ ndr1_0 )
| ! [X61] :
( ~ c2_1(X61)
| ~ c0_1(X61)
| c1_1(X61)
| ~ ndr1_0 )
| ! [X60] :
( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60)
| ~ ndr1_0 ) )
& ( hskp7
| hskp8
| ! [X59] :
( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59)
| ~ ndr1_0 ) )
& ( hskp18
| hskp29
| ! [X58] :
( ~ c0_1(X58)
| c2_1(X58)
| c1_1(X58)
| ~ ndr1_0 ) )
& ( hskp14
| ! [X57] :
( ~ c2_1(X57)
| ~ c0_1(X57)
| c3_1(X57)
| ~ ndr1_0 )
| ! [X56] :
( ~ c0_1(X56)
| c2_1(X56)
| c1_1(X56)
| ~ ndr1_0 ) )
& ( hskp15
| ! [X55] :
( ~ c0_1(X55)
| c3_1(X55)
| c1_1(X55)
| ~ ndr1_0 )
| ! [X54] :
( ~ c0_1(X54)
| c2_1(X54)
| c1_1(X54)
| ~ ndr1_0 ) )
& ( hskp0
| ! [X53] :
( ~ c1_1(X53)
| ~ c0_1(X53)
| c2_1(X53)
| ~ ndr1_0 )
| ! [X52] :
( ~ c3_1(X52)
| ~ c2_1(X52)
| c0_1(X52)
| ~ ndr1_0 ) )
& ( hskp17
| hskp16
| ! [X51] :
( ~ c2_1(X51)
| ~ c1_1(X51)
| c0_1(X51)
| ~ ndr1_0 ) )
& ( hskp28
| ! [X50] :
( ~ c3_1(X50)
| ~ c0_1(X50)
| c2_1(X50)
| ~ ndr1_0 )
| ! [X49] :
( ~ c2_1(X49)
| ~ c1_1(X49)
| c0_1(X49)
| ~ ndr1_0 ) )
& ( hskp15
| hskp14
| ! [X48] :
( ~ c2_1(X48)
| c3_1(X48)
| c0_1(X48)
| ~ ndr1_0 ) )
& ( ! [X47] :
( ~ c3_1(X47)
| ~ c1_1(X47)
| ~ c0_1(X47)
| ~ ndr1_0 )
| ! [X46] :
( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46)
| ~ ndr1_0 )
| ! [X45] :
( ~ c2_1(X45)
| c3_1(X45)
| c0_1(X45)
| ~ ndr1_0 ) )
& ( ! [X44] :
( ~ c2_1(X44)
| ~ c0_1(X44)
| c1_1(X44)
| ~ ndr1_0 )
| ! [X43] :
( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43)
| ~ ndr1_0 )
| ! [X42] :
( ~ c2_1(X42)
| c3_1(X42)
| c0_1(X42)
| ~ ndr1_0 ) )
& ( hskp4
| ! [X41] :
( ~ c3_1(X41)
| ~ c1_1(X41)
| c0_1(X41)
| ~ ndr1_0 )
| ! [X40] :
( ~ c2_1(X40)
| c3_1(X40)
| c0_1(X40)
| ~ ndr1_0 ) )
& ( hskp28
| ! [X39] :
( ~ c1_1(X39)
| c3_1(X39)
| c0_1(X39)
| ~ ndr1_0 ) )
& ( hskp12
| ! [X38] :
( ~ c2_1(X38)
| ~ c1_1(X38)
| ~ c0_1(X38)
| ~ ndr1_0 )
| ! [X37] :
( ~ c1_1(X37)
| c3_1(X37)
| c0_1(X37)
| ~ ndr1_0 ) )
& ( ! [X36] :
( ~ c1_1(X36)
| ~ c0_1(X36)
| c3_1(X36)
| ~ ndr1_0 )
| ! [X35] :
( c3_1(X35)
| c2_1(X35)
| c1_1(X35)
| ~ ndr1_0 )
| ! [X34] :
( ~ c1_1(X34)
| c3_1(X34)
| c0_1(X34)
| ~ ndr1_0 ) )
& ( hskp13
| ! [X33] :
( ~ c0_1(X33)
| c3_1(X33)
| c1_1(X33)
| ~ ndr1_0 )
| ! [X32] :
( ~ c3_1(X32)
| c2_1(X32)
| c0_1(X32)
| ~ ndr1_0 ) )
& ( ! [X31] :
( ~ c3_1(X31)
| ~ c0_1(X31)
| c1_1(X31)
| ~ ndr1_0 )
| ! [X30] :
( ~ c3_1(X30)
| ~ c1_1(X30)
| c0_1(X30)
| ~ ndr1_0 )
| ! [X29] :
( ~ c3_1(X29)
| c2_1(X29)
| c0_1(X29)
| ~ ndr1_0 ) )
& ( hskp12
| ! [X28] :
( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28)
| ~ ndr1_0 )
| ! [X27] :
( ~ c1_1(X27)
| c2_1(X27)
| c0_1(X27)
| ~ ndr1_0 ) )
& ( hskp11
| ! [X26] :
( c3_1(X26)
| c2_1(X26)
| c1_1(X26)
| ~ ndr1_0 )
| ! [X25] :
( ~ c1_1(X25)
| c2_1(X25)
| c0_1(X25)
| ~ ndr1_0 ) )
& ( hskp9
| ! [X24] :
( ~ c1_1(X24)
| c3_1(X24)
| c0_1(X24)
| ~ ndr1_0 )
| ! [X23] :
( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23)
| ~ ndr1_0 ) )
& ( ! [X22] :
( ~ c1_1(X22)
| c3_1(X22)
| c2_1(X22)
| ~ ndr1_0 )
| ! [X21] :
( ~ c3_1(X21)
| c2_1(X21)
| c0_1(X21)
| ~ ndr1_0 )
| ! [X20] :
( ~ c1_1(X20)
| c2_1(X20)
| c0_1(X20)
| ~ ndr1_0 ) )
& ( hskp6
| hskp10
| ! [X19] :
( c3_1(X19)
| c2_1(X19)
| c0_1(X19)
| ~ ndr1_0 ) )
& ( hskp9
| ! [X18] :
( ~ c0_1(X18)
| c3_1(X18)
| c2_1(X18)
| ~ ndr1_0 )
| ! [X17] :
( c3_1(X17)
| c2_1(X17)
| c0_1(X17)
| ~ ndr1_0 ) )
& ( hskp8
| ! [X16] :
( ~ c3_1(X16)
| ~ c2_1(X16)
| c0_1(X16)
| ~ ndr1_0 )
| ! [X15] :
( c3_1(X15)
| c2_1(X15)
| c0_1(X15)
| ~ ndr1_0 ) )
& ( hskp6
| ! [X14] :
( ~ c2_1(X14)
| ~ c1_1(X14)
| c0_1(X14)
| ~ ndr1_0 )
| ! [X13] :
( c3_1(X13)
| c2_1(X13)
| c0_1(X13)
| ~ ndr1_0 ) )
& ( hskp6
| ! [X12] :
( ~ c2_1(X12)
| c3_1(X12)
| c0_1(X12)
| ~ ndr1_0 )
| ! [X11] :
( c3_1(X11)
| c2_1(X11)
| c0_1(X11)
| ~ ndr1_0 ) )
& ( hskp7
| ! [X10] :
( ~ c3_1(X10)
| ~ c1_1(X10)
| c2_1(X10)
| ~ ndr1_0 )
| ! [X9] :
( ~ c3_1(X9)
| c1_1(X9)
| c0_1(X9)
| ~ ndr1_0 ) )
& ( hskp6
| hskp5
| ! [X8] :
( ~ c2_1(X8)
| c1_1(X8)
| c0_1(X8)
| ~ ndr1_0 ) )
& ( hskp2
| hskp4
| ! [X7] :
( ~ c2_1(X7)
| c1_1(X7)
| c0_1(X7)
| ~ ndr1_0 ) )
& ( hskp3
| ! [X6] :
( ~ c3_1(X6)
| ~ c0_1(X6)
| c2_1(X6)
| ~ ndr1_0 )
| ! [X5] :
( c3_1(X5)
| c1_1(X5)
| c0_1(X5)
| ~ ndr1_0 ) )
& ( ! [X4] :
( ~ c2_1(X4)
| c3_1(X4)
| c1_1(X4)
| ~ ndr1_0 )
| ! [X3] :
( ~ c2_1(X3)
| c1_1(X3)
| c0_1(X3)
| ~ ndr1_0 )
| ! [X2] :
( c3_1(X2)
| c1_1(X2)
| c0_1(X2)
| ~ ndr1_0 ) )
& ( hskp1
| hskp2
| ! [X1] :
( c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0 ) )
& ( hskp1
| hskp27
| ! [Z] :
( c2_1(Z)
| c1_1(Z)
| c0_1(Z)
| ~ ndr1_0 ) )
& ( ! [Y] :
( ~ c1_1(Y)
| ~ c0_1(Y)
| c3_1(Y)
| ~ ndr1_0 )
| ! [X] :
( ~ c3_1(X)
| ~ c1_1(X)
| c2_1(X)
| ~ ndr1_0 )
| ! [W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| ~ ndr1_0 ) )
& ( hskp0
| ! [V] :
( ~ c2_1(V)
| c3_1(V)
| c1_1(V)
| ~ ndr1_0 )
| ! [U] :
( c2_1(U)
| c1_1(U)
| c0_1(U)
| ~ ndr1_0 ) )
& ( ( c3_1(a1372)
& c1_1(a1372)
& c0_1(a1372)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a1338)
& c2_1(a1338)
& c1_1(a1338)
& ndr1_0 )
| ~ hskp29 )
& ( ( c3_1(a1328)
& c2_1(a1328)
& c0_1(a1328)
& ndr1_0 )
| ~ hskp28 )
& ( ( c2_1(a1307)
& c1_1(a1307)
& c0_1(a1307)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a1411)
& ~ c2_1(a1411)
& c0_1(a1411)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c3_1(a1394)
& c2_1(a1394)
& c0_1(a1394)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c3_1(a1370)
& ~ c1_1(a1370)
& c2_1(a1370)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a1359)
& ~ c1_1(a1359)
& ~ c0_1(a1359)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c3_1(a1356)
& c1_1(a1356)
& c0_1(a1356)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c2_1(a1352)
& ~ c0_1(a1352)
& c3_1(a1352)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c0_1(a1348)
& c2_1(a1348)
& c1_1(a1348)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c2_1(a1344)
& c1_1(a1344)
& c0_1(a1344)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c2_1(a1339)
& ~ c0_1(a1339)
& c1_1(a1339)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c0_1(a1334)
& c3_1(a1334)
& c2_1(a1334)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a1333)
& ~ c2_1(a1333)
& c1_1(a1333)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c3_1(a1331)
& c2_1(a1331)
& c1_1(a1331)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c2_1(a1330)
& ~ c1_1(a1330)
& c0_1(a1330)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c3_1(a1326)
& ~ c2_1(a1326)
& ~ c1_1(a1326)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c0_1(a1325)
& c3_1(a1325)
& c1_1(a1325)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c1_1(a1324)
& c3_1(a1324)
& c0_1(a1324)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c2_1(a1321)
& c3_1(a1321)
& c0_1(a1321)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c1_1(a1320)
& ~ c0_1(a1320)
& c2_1(a1320)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c3_1(a1319)
& ~ c0_1(a1319)
& c2_1(a1319)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a1316)
& ~ c2_1(a1316)
& ~ c0_1(a1316)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a1315)
& ~ c0_1(a1315)
& c3_1(a1315)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a1314)
& ~ c0_1(a1314)
& c1_1(a1314)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c3_1(a1312)
& ~ c1_1(a1312)
& c0_1(a1312)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c1_1(a1311)
& c2_1(a1311)
& c0_1(a1311)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c2_1(a1309)
& c3_1(a1309)
& c1_1(a1309)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c2_1(a1308)
& ~ c1_1(a1308)
& c3_1(a1308)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c2_1(a1306)
& ~ c1_1(a1306)
& ~ c0_1(a1306)
& ndr1_0 )
| ~ hskp0 ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,plain,
( ( hskp23
| hskp0
| hskp6 )
& ( hskp16
| hskp5
| hskp18 )
& ( hskp23
| hskp1
| hskp2 )
& ( hskp18
| hskp20 )
& ( hskp12
| hskp26 )
& ( hskp20
| hskp29
| hskp26 )
& ( hskp1
| hskp4
| hskp14 )
& ( hskp6
| hskp20
| hskp25 )
& ( hskp7
| hskp21
| hskp3 )
& ( hskp7
| hskp4
| hskp3 )
& ( hskp7
| hskp1
| hskp28 )
& ( hskp14
| hskp25
| hskp28 )
& ( hskp9
| hskp14
| hskp19 )
& ( hskp9
| hskp2
| hskp30 )
& ( hskp18
| hskp14
| hskp27 )
& ( hskp11
| hskp22
| ! [X97] :
( ~ c3_1(X97)
| ~ c2_1(X97)
| ~ c1_1(X97) )
| ~ ndr1_0 )
& ( hskp29
| ! [X96] :
( ~ c3_1(X96)
| ~ c2_1(X96)
| ~ c1_1(X96) )
| ~ ndr1_0
| ! [X95] :
( ~ c3_1(X95)
| ~ c1_1(X95)
| ~ c0_1(X95) )
| ~ ndr1_0 )
& ( hskp13
| ! [X94] :
( ~ c2_1(X94)
| ~ c1_1(X94)
| ~ c0_1(X94) )
| ~ ndr1_0 )
& ( hskp17
| ! [X93] :
( ~ c3_1(X93)
| ~ c2_1(X93)
| ~ c1_1(X93) )
| ~ ndr1_0
| ! [X92] :
( ~ c2_1(X92)
| ~ c1_1(X92)
| ~ c0_1(X92) )
| ~ ndr1_0 )
& ( hskp5
| ! [X91] :
( ~ c3_1(X91)
| ~ c1_1(X91)
| ~ c0_1(X91) )
| ~ ndr1_0
| ! [X90] :
( ~ c2_1(X90)
| ~ c1_1(X90)
| c3_1(X90) )
| ~ ndr1_0 )
& ( hskp6
| hskp9
| ! [X89] :
( ~ c2_1(X89)
| ~ c0_1(X89)
| c3_1(X89) )
| ~ ndr1_0 )
& ( hskp12
| hskp14
| ! [X88] :
( ~ c2_1(X88)
| ~ c0_1(X88)
| c3_1(X88) )
| ~ ndr1_0 )
& ( hskp18
| hskp30
| ! [X87] :
( ~ c2_1(X87)
| ~ c0_1(X87)
| c3_1(X87) )
| ~ ndr1_0 )
& ( hskp11
| ! [X86] :
( ~ c3_1(X86)
| ~ c1_1(X86)
| ~ c0_1(X86) )
| ~ ndr1_0
| ! [X85] :
( ~ c2_1(X85)
| ~ c0_1(X85)
| c3_1(X85) )
| ~ ndr1_0 )
& ( hskp24
| hskp20
| ! [X84] :
( ~ c1_1(X84)
| ~ c0_1(X84)
| c3_1(X84) )
| ~ ndr1_0 )
& ( hskp8
| hskp14
| ! [X83] :
( ~ c1_1(X83)
| ~ c0_1(X83)
| c3_1(X83) )
| ~ ndr1_0 )
& ( hskp13
| hskp14
| ! [X82] :
( ~ c1_1(X82)
| c3_1(X82)
| c2_1(X82) )
| ~ ndr1_0 )
& ( hskp16
| hskp14
| ! [X81] :
( ~ c1_1(X81)
| c3_1(X81)
| c2_1(X81) )
| ~ ndr1_0 )
& ( hskp17
| hskp4
| ! [X80] :
( ~ c0_1(X80)
| c3_1(X80)
| c2_1(X80) )
| ~ ndr1_0 )
& ( hskp27
| ! [X79] :
( ~ c1_1(X79)
| ~ c0_1(X79)
| c3_1(X79) )
| ~ ndr1_0
| ! [X78] :
( ~ c0_1(X78)
| c3_1(X78)
| c2_1(X78) )
| ~ ndr1_0 )
& ( hskp23
| hskp22
| ! [X77] :
( ~ c3_1(X77)
| ~ c2_1(X77)
| c1_1(X77) )
| ~ ndr1_0 )
& ( hskp2
| hskp22
| ! [X76] :
( ~ c3_1(X76)
| ~ c2_1(X76)
| c1_1(X76) )
| ~ ndr1_0 )
& ( hskp27
| ! [X75] :
( ~ c3_1(X75)
| ~ c0_1(X75)
| c2_1(X75) )
| ~ ndr1_0
| ! [X74] :
( ~ c3_1(X74)
| ~ c2_1(X74)
| c1_1(X74) )
| ~ ndr1_0 )
& ( hskp20
| ! [X73] :
( ~ c1_1(X73)
| c3_1(X73)
| c2_1(X73) )
| ~ ndr1_0
| ! [X72] :
( ~ c3_1(X72)
| ~ c0_1(X72)
| c1_1(X72) )
| ~ ndr1_0 )
& ( hskp0
| hskp21
| ! [X71] :
( ~ c2_1(X71)
| ~ c0_1(X71)
| c1_1(X71) )
| ~ ndr1_0 )
& ( hskp0
| hskp12
| ! [X70] :
( ~ c2_1(X70)
| ~ c0_1(X70)
| c1_1(X70) )
| ~ ndr1_0 )
& ( hskp2
| hskp20
| ! [X69] :
( ~ c2_1(X69)
| ~ c0_1(X69)
| c1_1(X69) )
| ~ ndr1_0 )
& ( hskp1
| hskp10
| ! [X68] :
( ~ c2_1(X68)
| c3_1(X68)
| c1_1(X68) )
| ~ ndr1_0 )
& ( hskp15
| hskp19
| ! [X67] :
( ~ c0_1(X67)
| c3_1(X67)
| c1_1(X67) )
| ~ ndr1_0 )
& ( hskp1
| hskp2
| ! [X66] :
( ~ c3_1(X66)
| c2_1(X66)
| c1_1(X66) )
| ~ ndr1_0 )
& ( ! [X65] :
( ~ c2_1(X65)
| ~ c1_1(X65)
| c3_1(X65) )
| ~ ndr1_0
| ! [X64] :
( ~ c1_1(X64)
| ~ c0_1(X64)
| c3_1(X64) )
| ~ ndr1_0
| ! [X63] :
( ~ c3_1(X63)
| c2_1(X63)
| c1_1(X63) )
| ~ ndr1_0 )
& ( ! [X62] :
( ~ c0_1(X62)
| c3_1(X62)
| c2_1(X62) )
| ~ ndr1_0
| ! [X61] :
( ~ c2_1(X61)
| ~ c0_1(X61)
| c1_1(X61) )
| ~ ndr1_0
| ! [X60] :
( ~ c3_1(X60)
| c2_1(X60)
| c1_1(X60) )
| ~ ndr1_0 )
& ( hskp7
| hskp8
| ! [X59] :
( ~ c0_1(X59)
| c2_1(X59)
| c1_1(X59) )
| ~ ndr1_0 )
& ( hskp18
| hskp29
| ! [X58] :
( ~ c0_1(X58)
| c2_1(X58)
| c1_1(X58) )
| ~ ndr1_0 )
& ( hskp14
| ! [X57] :
( ~ c2_1(X57)
| ~ c0_1(X57)
| c3_1(X57) )
| ~ ndr1_0
| ! [X56] :
( ~ c0_1(X56)
| c2_1(X56)
| c1_1(X56) )
| ~ ndr1_0 )
& ( hskp15
| ! [X55] :
( ~ c0_1(X55)
| c3_1(X55)
| c1_1(X55) )
| ~ ndr1_0
| ! [X54] :
( ~ c0_1(X54)
| c2_1(X54)
| c1_1(X54) )
| ~ ndr1_0 )
& ( hskp0
| ! [X53] :
( ~ c1_1(X53)
| ~ c0_1(X53)
| c2_1(X53) )
| ~ ndr1_0
| ! [X52] :
( ~ c3_1(X52)
| ~ c2_1(X52)
| c0_1(X52) )
| ~ ndr1_0 )
& ( hskp17
| hskp16
| ! [X51] :
( ~ c2_1(X51)
| ~ c1_1(X51)
| c0_1(X51) )
| ~ ndr1_0 )
& ( hskp28
| ! [X50] :
( ~ c3_1(X50)
| ~ c0_1(X50)
| c2_1(X50) )
| ~ ndr1_0
| ! [X49] :
( ~ c2_1(X49)
| ~ c1_1(X49)
| c0_1(X49) )
| ~ ndr1_0 )
& ( hskp15
| hskp14
| ! [X48] :
( ~ c2_1(X48)
| c3_1(X48)
| c0_1(X48) )
| ~ ndr1_0 )
& ( ! [X47] :
( ~ c3_1(X47)
| ~ c1_1(X47)
| ~ c0_1(X47) )
| ~ ndr1_0
| ! [X46] :
( ~ c3_1(X46)
| ~ c2_1(X46)
| c0_1(X46) )
| ~ ndr1_0
| ! [X45] :
( ~ c2_1(X45)
| c3_1(X45)
| c0_1(X45) )
| ~ ndr1_0 )
& ( ! [X44] :
( ~ c2_1(X44)
| ~ c0_1(X44)
| c1_1(X44) )
| ~ ndr1_0
| ! [X43] :
( ~ c3_1(X43)
| ~ c2_1(X43)
| c0_1(X43) )
| ~ ndr1_0
| ! [X42] :
( ~ c2_1(X42)
| c3_1(X42)
| c0_1(X42) )
| ~ ndr1_0 )
& ( hskp4
| ! [X41] :
( ~ c3_1(X41)
| ~ c1_1(X41)
| c0_1(X41) )
| ~ ndr1_0
| ! [X40] :
( ~ c2_1(X40)
| c3_1(X40)
| c0_1(X40) )
| ~ ndr1_0 )
& ( hskp28
| ! [X39] :
( ~ c1_1(X39)
| c3_1(X39)
| c0_1(X39) )
| ~ ndr1_0 )
& ( hskp12
| ! [X38] :
( ~ c2_1(X38)
| ~ c1_1(X38)
| ~ c0_1(X38) )
| ~ ndr1_0
| ! [X37] :
( ~ c1_1(X37)
| c3_1(X37)
| c0_1(X37) )
| ~ ndr1_0 )
& ( ! [X36] :
( ~ c1_1(X36)
| ~ c0_1(X36)
| c3_1(X36) )
| ~ ndr1_0
| ! [X35] :
( c3_1(X35)
| c2_1(X35)
| c1_1(X35) )
| ~ ndr1_0
| ! [X34] :
( ~ c1_1(X34)
| c3_1(X34)
| c0_1(X34) )
| ~ ndr1_0 )
& ( hskp13
| ! [X33] :
( ~ c0_1(X33)
| c3_1(X33)
| c1_1(X33) )
| ~ ndr1_0
| ! [X32] :
( ~ c3_1(X32)
| c2_1(X32)
| c0_1(X32) )
| ~ ndr1_0 )
& ( ! [X31] :
( ~ c3_1(X31)
| ~ c0_1(X31)
| c1_1(X31) )
| ~ ndr1_0
| ! [X30] :
( ~ c3_1(X30)
| ~ c1_1(X30)
| c0_1(X30) )
| ~ ndr1_0
| ! [X29] :
( ~ c3_1(X29)
| c2_1(X29)
| c0_1(X29) )
| ~ ndr1_0 )
& ( hskp12
| ! [X28] :
( ~ c3_1(X28)
| ~ c2_1(X28)
| ~ c1_1(X28) )
| ~ ndr1_0
| ! [X27] :
( ~ c1_1(X27)
| c2_1(X27)
| c0_1(X27) )
| ~ ndr1_0 )
& ( hskp11
| ! [X26] :
( c3_1(X26)
| c2_1(X26)
| c1_1(X26) )
| ~ ndr1_0
| ! [X25] :
( ~ c1_1(X25)
| c2_1(X25)
| c0_1(X25) )
| ~ ndr1_0 )
& ( hskp9
| ! [X24] :
( ~ c1_1(X24)
| c3_1(X24)
| c0_1(X24) )
| ~ ndr1_0
| ! [X23] :
( ~ c1_1(X23)
| c2_1(X23)
| c0_1(X23) )
| ~ ndr1_0 )
& ( ! [X22] :
( ~ c1_1(X22)
| c3_1(X22)
| c2_1(X22) )
| ~ ndr1_0
| ! [X21] :
( ~ c3_1(X21)
| c2_1(X21)
| c0_1(X21) )
| ~ ndr1_0
| ! [X20] :
( ~ c1_1(X20)
| c2_1(X20)
| c0_1(X20) )
| ~ ndr1_0 )
& ( hskp6
| hskp10
| ! [X19] :
( c3_1(X19)
| c2_1(X19)
| c0_1(X19) )
| ~ ndr1_0 )
& ( hskp9
| ! [X18] :
( ~ c0_1(X18)
| c3_1(X18)
| c2_1(X18) )
| ~ ndr1_0
| ! [X17] :
( c3_1(X17)
| c2_1(X17)
| c0_1(X17) )
| ~ ndr1_0 )
& ( hskp8
| ! [X16] :
( ~ c3_1(X16)
| ~ c2_1(X16)
| c0_1(X16) )
| ~ ndr1_0
| ! [X15] :
( c3_1(X15)
| c2_1(X15)
| c0_1(X15) )
| ~ ndr1_0 )
& ( hskp6
| ! [X14] :
( ~ c2_1(X14)
| ~ c1_1(X14)
| c0_1(X14) )
| ~ ndr1_0
| ! [X13] :
( c3_1(X13)
| c2_1(X13)
| c0_1(X13) )
| ~ ndr1_0 )
& ( hskp6
| ! [X12] :
( ~ c2_1(X12)
| c3_1(X12)
| c0_1(X12) )
| ~ ndr1_0
| ! [X11] :
( c3_1(X11)
| c2_1(X11)
| c0_1(X11) )
| ~ ndr1_0 )
& ( hskp7
| ! [X10] :
( ~ c3_1(X10)
| ~ c1_1(X10)
| c2_1(X10) )
| ~ ndr1_0
| ! [X9] :
( ~ c3_1(X9)
| c1_1(X9)
| c0_1(X9) )
| ~ ndr1_0 )
& ( hskp6
| hskp5
| ! [X8] :
( ~ c2_1(X8)
| c1_1(X8)
| c0_1(X8) )
| ~ ndr1_0 )
& ( hskp2
| hskp4
| ! [X7] :
( ~ c2_1(X7)
| c1_1(X7)
| c0_1(X7) )
| ~ ndr1_0 )
& ( hskp3
| ! [X6] :
( ~ c3_1(X6)
| ~ c0_1(X6)
| c2_1(X6) )
| ~ ndr1_0
| ! [X5] :
( c3_1(X5)
| c1_1(X5)
| c0_1(X5) )
| ~ ndr1_0 )
& ( ! [X4] :
( ~ c2_1(X4)
| c3_1(X4)
| c1_1(X4) )
| ~ ndr1_0
| ! [X3] :
( ~ c2_1(X3)
| c1_1(X3)
| c0_1(X3) )
| ~ ndr1_0
| ! [X2] :
( c3_1(X2)
| c1_1(X2)
| c0_1(X2) )
| ~ ndr1_0 )
& ( hskp1
| hskp2
| ! [X1] :
( c2_1(X1)
| c1_1(X1)
| c0_1(X1) )
| ~ ndr1_0 )
& ( hskp1
| hskp27
| ! [Z] :
( c2_1(Z)
| c1_1(Z)
| c0_1(Z) )
| ~ ndr1_0 )
& ( ! [Y] :
( ~ c1_1(Y)
| ~ c0_1(Y)
| c3_1(Y) )
| ~ ndr1_0
| ! [X] :
( ~ c3_1(X)
| ~ c1_1(X)
| c2_1(X) )
| ~ ndr1_0
| ! [W] :
( c2_1(W)
| c1_1(W)
| c0_1(W) )
| ~ ndr1_0 )
& ( hskp0
| ! [V] :
( ~ c2_1(V)
| c3_1(V)
| c1_1(V) )
| ~ ndr1_0
| ! [U] :
( c2_1(U)
| c1_1(U)
| c0_1(U) )
| ~ ndr1_0 )
& ( ( c3_1(a1372)
& c1_1(a1372)
& c0_1(a1372)
& ndr1_0 )
| ~ hskp30 )
& ( ( c3_1(a1338)
& c2_1(a1338)
& c1_1(a1338)
& ndr1_0 )
| ~ hskp29 )
& ( ( c3_1(a1328)
& c2_1(a1328)
& c0_1(a1328)
& ndr1_0 )
| ~ hskp28 )
& ( ( c2_1(a1307)
& c1_1(a1307)
& c0_1(a1307)
& ndr1_0 )
| ~ hskp27 )
& ( ( ~ c3_1(a1411)
& ~ c2_1(a1411)
& c0_1(a1411)
& ndr1_0 )
| ~ hskp26 )
& ( ( ~ c3_1(a1394)
& c2_1(a1394)
& c0_1(a1394)
& ndr1_0 )
| ~ hskp25 )
& ( ( ~ c3_1(a1370)
& ~ c1_1(a1370)
& c2_1(a1370)
& ndr1_0 )
| ~ hskp24 )
& ( ( ~ c3_1(a1359)
& ~ c1_1(a1359)
& ~ c0_1(a1359)
& ndr1_0 )
| ~ hskp23 )
& ( ( ~ c3_1(a1356)
& c1_1(a1356)
& c0_1(a1356)
& ndr1_0 )
| ~ hskp22 )
& ( ( ~ c2_1(a1352)
& ~ c0_1(a1352)
& c3_1(a1352)
& ndr1_0 )
| ~ hskp21 )
& ( ( ~ c0_1(a1348)
& c2_1(a1348)
& c1_1(a1348)
& ndr1_0 )
| ~ hskp20 )
& ( ( ~ c2_1(a1344)
& c1_1(a1344)
& c0_1(a1344)
& ndr1_0 )
| ~ hskp19 )
& ( ( ~ c2_1(a1339)
& ~ c0_1(a1339)
& c1_1(a1339)
& ndr1_0 )
| ~ hskp18 )
& ( ( ~ c0_1(a1334)
& c3_1(a1334)
& c2_1(a1334)
& ndr1_0 )
| ~ hskp17 )
& ( ( ~ c3_1(a1333)
& ~ c2_1(a1333)
& c1_1(a1333)
& ndr1_0 )
| ~ hskp16 )
& ( ( ~ c3_1(a1331)
& c2_1(a1331)
& c1_1(a1331)
& ndr1_0 )
| ~ hskp15 )
& ( ( ~ c2_1(a1330)
& ~ c1_1(a1330)
& c0_1(a1330)
& ndr1_0 )
| ~ hskp14 )
& ( ( ~ c3_1(a1326)
& ~ c2_1(a1326)
& ~ c1_1(a1326)
& ndr1_0 )
| ~ hskp13 )
& ( ( ~ c0_1(a1325)
& c3_1(a1325)
& c1_1(a1325)
& ndr1_0 )
| ~ hskp12 )
& ( ( ~ c1_1(a1324)
& c3_1(a1324)
& c0_1(a1324)
& ndr1_0 )
| ~ hskp11 )
& ( ( ~ c2_1(a1321)
& c3_1(a1321)
& c0_1(a1321)
& ndr1_0 )
| ~ hskp10 )
& ( ( ~ c1_1(a1320)
& ~ c0_1(a1320)
& c2_1(a1320)
& ndr1_0 )
| ~ hskp9 )
& ( ( ~ c3_1(a1319)
& ~ c0_1(a1319)
& c2_1(a1319)
& ndr1_0 )
| ~ hskp8 )
& ( ( ~ c3_1(a1316)
& ~ c2_1(a1316)
& ~ c0_1(a1316)
& ndr1_0 )
| ~ hskp7 )
& ( ( ~ c1_1(a1315)
& ~ c0_1(a1315)
& c3_1(a1315)
& ndr1_0 )
| ~ hskp6 )
& ( ( ~ c3_1(a1314)
& ~ c0_1(a1314)
& c1_1(a1314)
& ndr1_0 )
| ~ hskp5 )
& ( ( ~ c3_1(a1312)
& ~ c1_1(a1312)
& c0_1(a1312)
& ndr1_0 )
| ~ hskp4 )
& ( ( ~ c1_1(a1311)
& c2_1(a1311)
& c0_1(a1311)
& ndr1_0 )
| ~ hskp3 )
& ( ( ~ c2_1(a1309)
& c3_1(a1309)
& c1_1(a1309)
& ndr1_0 )
| ~ hskp2 )
& ( ( ~ c2_1(a1308)
& ~ c1_1(a1308)
& c3_1(a1308)
& ndr1_0 )
| ~ hskp1 )
& ( ( ~ c2_1(a1306)
& ~ c1_1(a1306)
& ~ c0_1(a1306)
& ndr1_0 )
| ~ hskp0 ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f5,plain,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f6,plain,
( ~ c0_1(a1306)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f7,plain,
( ~ c1_1(a1306)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f8,plain,
( ~ c2_1(a1306)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f9,plain,
( ndr1_0
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
( c3_1(a1308)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f11,plain,
( ~ c1_1(a1308)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f12,plain,
( ~ c2_1(a1308)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f13,plain,
( ndr1_0
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f14,plain,
( c1_1(a1309)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f15,plain,
( c3_1(a1309)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f16,plain,
( ~ c2_1(a1309)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f17,plain,
( ndr1_0
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f18,plain,
( c0_1(a1311)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f19,plain,
( c2_1(a1311)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f20,plain,
( ~ c1_1(a1311)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f21,plain,
( ndr1_0
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f22,plain,
( c0_1(a1312)
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f23,plain,
( ~ c1_1(a1312)
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
( ~ c3_1(a1312)
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f25,plain,
( ndr1_0
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f26,plain,
( c1_1(a1314)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f27,plain,
( ~ c0_1(a1314)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f28,plain,
( ~ c3_1(a1314)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f29,plain,
( ndr1_0
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f30,plain,
( c3_1(a1315)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f31,plain,
( ~ c0_1(a1315)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f32,plain,
( ~ c1_1(a1315)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f33,plain,
( ndr1_0
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f34,plain,
( ~ c0_1(a1316)
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f35,plain,
( ~ c2_1(a1316)
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f36,plain,
( ~ c3_1(a1316)
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f37,plain,
( ndr1_0
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f38,plain,
( c2_1(a1319)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f39,plain,
( ~ c0_1(a1319)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f40,plain,
( ~ c3_1(a1319)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f41,plain,
( ndr1_0
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f42,plain,
( c2_1(a1320)
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f43,plain,
( ~ c0_1(a1320)
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f44,plain,
( ~ c1_1(a1320)
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f49,plain,
( ndr1_0
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f50,plain,
( c0_1(a1324)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f51,plain,
( c3_1(a1324)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f52,plain,
( ~ c1_1(a1324)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f54,plain,
( c1_1(a1325)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f55,plain,
( c3_1(a1325)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f56,plain,
( ~ c0_1(a1325)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f57,plain,
( ndr1_0
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f58,plain,
( ~ c1_1(a1326)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f59,plain,
( ~ c2_1(a1326)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f60,plain,
( ~ c3_1(a1326)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f61,plain,
( ndr1_0
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f62,plain,
( c0_1(a1330)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f63,plain,
( ~ c1_1(a1330)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f64,plain,
( ~ c2_1(a1330)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f65,plain,
( ndr1_0
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f66,plain,
( c1_1(a1331)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f67,plain,
( c2_1(a1331)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f68,plain,
( ~ c3_1(a1331)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f69,plain,
( ndr1_0
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f70,plain,
( c1_1(a1333)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f71,plain,
( ~ c2_1(a1333)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f72,plain,
( ~ c3_1(a1333)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f74,plain,
( c2_1(a1334)
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f75,plain,
( c3_1(a1334)
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f76,plain,
( ~ c0_1(a1334)
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f77,plain,
( ndr1_0
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f78,plain,
( c1_1(a1339)
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f79,plain,
( ~ c0_1(a1339)
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f80,plain,
( ~ c2_1(a1339)
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f85,plain,
( ndr1_0
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f86,plain,
( c1_1(a1348)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f87,plain,
( c2_1(a1348)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f88,plain,
( ~ c0_1(a1348)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f93,plain,
( ndr1_0
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f94,plain,
( c0_1(a1356)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f95,plain,
( c1_1(a1356)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f96,plain,
( ~ c3_1(a1356)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f97,plain,
( ndr1_0
| ~ hskp23 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f98,plain,
( ~ c0_1(a1359)
| ~ hskp23 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f99,plain,
( ~ c1_1(a1359)
| ~ hskp23 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f100,plain,
( ~ c3_1(a1359)
| ~ hskp23 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f109,plain,
( ndr1_0
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f110,plain,
( c0_1(a1411)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f111,plain,
( ~ c2_1(a1411)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f112,plain,
( ~ c3_1(a1411)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f114,plain,
( c0_1(a1307)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f115,plain,
( c1_1(a1307)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f116,plain,
( c2_1(a1307)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f118,plain,
( c0_1(a1328)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f119,plain,
( c2_1(a1328)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f120,plain,
( c3_1(a1328)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f126,plain,
( c0_1(a1372)
| ~ hskp30 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f127,plain,
( c1_1(a1372)
| ~ hskp30 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f128,plain,
( c3_1(a1372)
| ~ hskp30 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f130,plain,
! [X0,X1,X2] :
( ~ c1_1(X2)
| ~ c0_1(X2)
| c3_1(X2)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f132,plain,
! [X0] :
( hskp1
| hskp2
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f133,plain,
! [X0,X1,X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c1_1(X2)
| ~ ndr1_0
| ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f136,plain,
! [X0] :
( hskp6
| hskp5
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f137,plain,
! [X0,X1] :
( hskp7
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f139,plain,
! [X0,X1] :
( hskp6
| ~ c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f140,plain,
! [X0,X1] :
( hskp8
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ ndr1_0
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f141,plain,
! [X0,X1] :
( hskp9
| ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ ndr1_0
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f143,plain,
! [X0,X1,X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c2_1(X2)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f144,plain,
! [X0,X1] :
( hskp9
| ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f145,plain,
! [X0,X1] :
( hskp11
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f147,plain,
! [X0,X1,X2] :
( ~ c3_1(X2)
| ~ c0_1(X2)
| c1_1(X2)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ~ c1_1(X2)
| ~ c0_1(X2)
| c3_1(X2)
| ~ ndr1_0
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f151,plain,
! [X0] :
( hskp28
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f152,plain,
! [X0,X1] :
( hskp4
| ~ c3_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f153,plain,
! [X0,X1,X2] :
( ~ c2_1(X2)
| ~ c0_1(X2)
| c1_1(X2)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f154,plain,
! [X0,X1,X2] :
( ~ c3_1(X2)
| ~ c1_1(X2)
| ~ c0_1(X2)
| ~ ndr1_0
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f155,plain,
! [X0] :
( hskp15
| hskp14
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f156,plain,
! [X0,X1] :
( hskp28
| ~ c3_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f157,plain,
! [X0] :
( hskp17
| hskp16
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f158,plain,
! [X0,X1] :
( hskp0
| ~ c1_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f159,plain,
! [X0,X1] :
( hskp15
| ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f160,plain,
! [X0,X1] :
( hskp14
| ~ c2_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f162,plain,
! [X0] :
( hskp7
| hskp8
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f164,plain,
! [X0,X1,X2] :
( ~ c2_1(X2)
| ~ c1_1(X2)
| c3_1(X2)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f173,plain,
! [X0] :
( hskp2
| hskp22
| ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f174,plain,
! [X0] :
( hskp23
| hskp22
| ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f175,plain,
! [X0,X1] :
( hskp27
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f176,plain,
! [X0] :
( hskp17
| hskp4
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f178,plain,
! [X0] :
( hskp13
| hskp14
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f179,plain,
! [X0] :
( hskp8
| hskp14
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f184,plain,
! [X0] :
( hskp6
| hskp9
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f185,plain,
! [X0,X1] :
( hskp5
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f187,plain,
! [X0] :
( hskp13
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f189,plain,
! [X0] :
( hskp11
| hskp22
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f190,plain,
( hskp18
| hskp14
| hskp27 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f191,plain,
( hskp9
| hskp2
| hskp30 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f195,plain,
( hskp7
| hskp4
| hskp3 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f200,plain,
( hskp12
| hskp26 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f201,plain,
( hskp18
| hskp20 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f202,plain,
( hskp23
| hskp1
| hskp2 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f203,plain,
( hskp16
| hskp5
| hskp18 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f204,plain,
( hskp23
| hskp0
| hskp6 ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f206,plain,
! [X0,X1,X2] :
( ~ c1_1(X2)
| ~ c0_1(X2)
| c3_1(X2)
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f130]) ).
fof(f207,plain,
! [X0,X1,X2] :
( ~ c2_1(X2)
| c3_1(X2)
| c1_1(X2)
| ~ c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f133]) ).
fof(f209,plain,
! [X0,X1] :
( hskp7
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f137]) ).
fof(f211,plain,
! [X0,X1] :
( hskp6
| ~ c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f139]) ).
fof(f212,plain,
! [X0,X1] :
( hskp8
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f140]) ).
fof(f213,plain,
! [X0,X1] :
( hskp9
| ~ c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f141]) ).
fof(f214,plain,
! [X0,X1,X2] :
( ~ c1_1(X2)
| c3_1(X2)
| c2_1(X2)
| ~ c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f143]) ).
fof(f215,plain,
! [X0,X1] :
( hskp9
| ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f144]) ).
fof(f216,plain,
! [X0,X1] :
( hskp11
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f145]) ).
fof(f218,plain,
! [X0,X1,X2] :
( ~ c3_1(X2)
| ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f147]) ).
fof(f220,plain,
! [X0,X1,X2] :
( ~ c1_1(X2)
| ~ c0_1(X2)
| c3_1(X2)
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f149]) ).
fof(f222,plain,
! [X0,X1] :
( hskp4
| ~ c3_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f152]) ).
fof(f223,plain,
! [X0,X1,X2] :
( ~ c2_1(X2)
| ~ c0_1(X2)
| c1_1(X2)
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f153]) ).
fof(f224,plain,
! [X0,X1,X2] :
( ~ c3_1(X2)
| ~ c1_1(X2)
| ~ c0_1(X2)
| ~ c3_1(X1)
| ~ c2_1(X1)
| c0_1(X1)
| ~ c2_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f154]) ).
fof(f225,plain,
! [X0,X1] :
( hskp28
| ~ c3_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f156]) ).
fof(f226,plain,
! [X0,X1] :
( hskp0
| ~ c1_1(X1)
| ~ c0_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f158]) ).
fof(f227,plain,
! [X0,X1] :
( hskp15
| ~ c0_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f159]) ).
fof(f228,plain,
! [X0,X1] :
( hskp14
| ~ c2_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c0_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f160]) ).
fof(f230,plain,
! [X0,X1,X2] :
( ~ c2_1(X2)
| ~ c1_1(X2)
| c3_1(X2)
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f164]) ).
fof(f233,plain,
! [X0,X1] :
( hskp27
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f175]) ).
fof(f235,plain,
! [X0,X1] :
( hskp5
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f185]) ).
fof(f258,plain,
( ~ hskp16
| hskp28
| ~ c1_1(a1333)
| c0_1(a1333)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f151,f72]) ).
fof(f259,plain,
( ~ hskp15
| hskp28
| ~ c1_1(a1331)
| c0_1(a1331)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f151,f68]) ).
fof(f263,plain,
( ~ hskp5
| hskp28
| ~ c1_1(a1314)
| c0_1(a1314)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f151,f28]) ).
fof(f265,plain,
( ~ hskp16
| hskp28
| ~ c1_1(a1333)
| c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f258,f69]) ).
fof(f266,plain,
( ~ hskp15
| hskp28
| ~ c1_1(a1331)
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f259,f65]) ).
fof(f269,plain,
( ~ hskp5
| hskp28
| ~ c1_1(a1314)
| c0_1(a1314) ),
inference(forward_subsumption_resolution,[status(thm)],[f263,f25]) ).
fof(f270,plain,
( ~ hskp16
| hskp28
| c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f265,f70]) ).
fof(f271,plain,
( ~ hskp15
| hskp28
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f266,f66]) ).
fof(f275,plain,
! [X0,X1] :
( ~ hskp23
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| c2_1(a1359)
| c0_1(a1359)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f206,f99]) ).
fof(f284,plain,
! [X0,X1] :
( ~ hskp0
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| c2_1(a1306)
| c0_1(a1306)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f206,f7]) ).
fof(f285,plain,
! [X0,X1] :
( ~ hskp23
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| c2_1(a1359)
| c0_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f275,f97]) ).
fof(f289,plain,
! [X0,X1] :
( ~ hskp0
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| c2_1(a1306)
| c0_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f284,f5]) ).
fof(f305,plain,
( ~ hskp5
| hskp28
| ~ c1_1(a1314) ),
inference(forward_subsumption_resolution,[status(thm)],[f269,f27]) ).
fof(f313,plain,
( ~ hskp23
| hskp1
| hskp2
| c2_1(a1359)
| c0_1(a1359)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f132,f99]) ).
fof(f323,plain,
( ~ hskp23
| hskp1
| hskp2
| c2_1(a1359)
| c0_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f313,f97]) ).
fof(f327,plain,
( ~ hskp23
| hskp1
| hskp2
| c2_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f323,f98]) ).
fof(f353,plain,
! [X0,X1] :
( ~ hskp23
| ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c3_1(a1359)
| c0_1(a1359)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f207,f99]) ).
fof(f357,plain,
! [X0,X1] :
( ~ hskp9
| ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c3_1(a1320)
| c0_1(a1320)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f207,f44]) ).
fof(f364,plain,
! [X0,X1] :
( ~ hskp23
| ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c3_1(a1359)
| c0_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f97]) ).
fof(f366,plain,
! [X0,X1] :
( ~ hskp9
| ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c3_1(a1320)
| c0_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f357,f41]) ).
fof(f389,plain,
( ~ hskp9
| hskp6
| hskp5
| ~ c2_1(a1320)
| c0_1(a1320)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f136,f44]) ).
fof(f397,plain,
( ~ hskp9
| hskp6
| hskp5
| ~ c2_1(a1320)
| c0_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f41]) ).
fof(f400,plain,
( ~ hskp9
| hskp6
| hskp5
| ~ c2_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f397,f43]) ).
fof(f425,plain,
! [X0] :
( ~ hskp9
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1320)
| c0_1(a1320)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f209,f44]) ).
fof(f426,plain,
! [X0] :
( ~ hskp6
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1315)
| c0_1(a1315)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f209,f32]) ).
fof(f430,plain,
! [X0] :
( ~ hskp0
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1306)
| c0_1(a1306)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f209,f7]) ).
fof(f431,plain,
! [X0] :
( ~ hskp9
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1320)
| c0_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f425,f41]) ).
fof(f432,plain,
! [X0] :
( ~ hskp6
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1315)
| c0_1(a1315) ),
inference(forward_subsumption_resolution,[status(thm)],[f426,f29]) ).
fof(f434,plain,
! [X0] :
( ~ hskp0
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1306)
| c0_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f430,f5]) ).
fof(f448,plain,
( ~ hskp8
| hskp15
| hskp14
| ~ c2_1(a1319)
| c0_1(a1319)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f155,f40]) ).
fof(f454,plain,
( ~ hskp8
| hskp15
| hskp14
| ~ c2_1(a1319)
| c0_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f448,f37]) ).
fof(f458,plain,
( ~ hskp8
| hskp15
| hskp14
| ~ c2_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f454,f39]) ).
fof(f462,plain,
( ~ hskp20
| hskp17
| hskp16
| ~ c2_1(a1348)
| ~ c1_1(a1348)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f157,f88]) ).
fof(f472,plain,
( ~ hskp20
| hskp17
| hskp16
| ~ c2_1(a1348)
| ~ c1_1(a1348) ),
inference(forward_subsumption_resolution,[status(thm)],[f462,f85]) ).
fof(f476,plain,
( ~ hskp20
| hskp17
| hskp16
| ~ c2_1(a1348) ),
inference(forward_subsumption_resolution,[status(thm)],[f472,f86]) ).
fof(f498,plain,
! [X0] :
( ~ hskp23
| hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| c2_1(a1359)
| c0_1(a1359)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f211,f100]) ).
fof(f507,plain,
! [X0] :
( ~ hskp23
| hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| c2_1(a1359)
| c0_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f498,f97]) ).
fof(f537,plain,
( ~ hskp14
| hskp7
| hskp8
| ~ c0_1(a1330)
| c2_1(a1330)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f162,f63]) ).
fof(f539,plain,
( ~ hskp11
| hskp7
| hskp8
| ~ c0_1(a1324)
| c2_1(a1324)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f162,f52]) ).
fof(f542,plain,
( ~ hskp4
| hskp7
| hskp8
| ~ c0_1(a1312)
| c2_1(a1312)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f162,f23]) ).
fof(f546,plain,
( ~ hskp14
| hskp7
| hskp8
| ~ c0_1(a1330)
| c2_1(a1330) ),
inference(forward_subsumption_resolution,[status(thm)],[f537,f61]) ).
fof(f548,plain,
( ~ hskp11
| hskp7
| hskp8
| ~ c0_1(a1324)
| c2_1(a1324) ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f49]) ).
fof(f549,plain,
( ~ hskp4
| hskp7
| hskp8
| ~ c0_1(a1312)
| c2_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f542,f21]) ).
fof(f551,plain,
( ~ hskp14
| hskp7
| hskp8
| ~ c0_1(a1330) ),
inference(forward_subsumption_resolution,[status(thm)],[f546,f64]) ).
fof(f553,plain,
( ~ hskp11
| hskp7
| hskp8
| c2_1(a1324) ),
inference(forward_subsumption_resolution,[status(thm)],[f548,f50]) ).
fof(f554,plain,
( ~ hskp4
| hskp7
| hskp8
| c2_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f549,f22]) ).
fof(f590,plain,
! [X0] :
( ~ hskp23
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1359)
| c0_1(a1359)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f212,f100]) ).
fof(f592,plain,
! [X0] :
( ~ hskp16
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1333)
| c0_1(a1333)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f212,f72]) ).
fof(f596,plain,
! [X0] :
( ~ hskp7
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1316)
| c0_1(a1316)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f212,f36]) ).
fof(f599,plain,
! [X0] :
( ~ hskp23
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1359)
| c0_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f590,f97]) ).
fof(f600,plain,
! [X0] :
( ~ hskp16
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1333)
| c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f592,f69]) ).
fof(f602,plain,
! [X0] :
( ~ hskp7
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1316)
| c0_1(a1316) ),
inference(forward_subsumption_resolution,[status(thm)],[f596,f33]) ).
fof(f611,plain,
! [X0] :
( ~ hskp13
| hskp9
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c2_1(a1326)
| c0_1(a1326)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f213,f60]) ).
fof(f613,plain,
! [X0] :
( ~ hskp7
| hskp9
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c2_1(a1316)
| c0_1(a1316)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f213,f36]) ).
fof(f618,plain,
! [X0] :
( ~ hskp13
| hskp9
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c2_1(a1326)
| c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f611,f57]) ).
fof(f619,plain,
! [X0] :
( ~ hskp7
| hskp9
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c2_1(a1316)
| c0_1(a1316) ),
inference(forward_subsumption_resolution,[status(thm)],[f613,f33]) ).
fof(f624,plain,
! [X0,X1] :
( ~ hskp18
| ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(a1339)
| c0_1(a1339)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f214,f80]) ).
fof(f630,plain,
! [X0,X1] :
( ~ hskp2
| ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(a1309)
| c0_1(a1309)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f214,f16]) ).
fof(f634,plain,
! [X0,X1] :
( ~ hskp18
| ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(a1339)
| c0_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f624,f77]) ).
fof(f637,plain,
! [X0,X1] :
( ~ hskp2
| ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(a1309)
| c0_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f630,f13]) ).
fof(f662,plain,
! [X0] :
( ~ hskp18
| hskp9
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(a1339)
| c0_1(a1339)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f215,f80]) ).
fof(f663,plain,
! [X0] :
( ~ hskp16
| hskp9
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(a1333)
| c0_1(a1333)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f215,f71]) ).
fof(f672,plain,
! [X0] :
( ~ hskp18
| hskp9
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(a1339)
| c0_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f662,f77]) ).
fof(f673,plain,
! [X0] :
( ~ hskp16
| hskp9
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(a1333)
| c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f663,f69]) ).
fof(f719,plain,
! [X0] :
( ~ hskp18
| hskp11
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1339)
| c0_1(a1339)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f216,f80]) ).
fof(f729,plain,
! [X0] :
( ~ hskp18
| hskp11
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1339)
| c0_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f719,f77]) ).
fof(f776,plain,
( ~ hskp11
| hskp2
| hskp22
| ~ c3_1(a1324)
| ~ c2_1(a1324)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f173,f52]) ).
fof(f777,plain,
( ~ hskp9
| hskp2
| hskp22
| ~ c3_1(a1320)
| ~ c2_1(a1320)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f173,f44]) ).
fof(f780,plain,
( ~ hskp3
| hskp2
| hskp22
| ~ c3_1(a1311)
| ~ c2_1(a1311)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f173,f20]) ).
fof(f783,plain,
( ~ hskp11
| hskp2
| hskp22
| ~ c3_1(a1324)
| ~ c2_1(a1324) ),
inference(forward_subsumption_resolution,[status(thm)],[f776,f49]) ).
fof(f784,plain,
( ~ hskp9
| hskp2
| hskp22
| ~ c3_1(a1320)
| ~ c2_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f41]) ).
fof(f786,plain,
( ~ hskp3
| hskp2
| hskp22
| ~ c3_1(a1311)
| ~ c2_1(a1311) ),
inference(forward_subsumption_resolution,[status(thm)],[f780,f17]) ).
fof(f787,plain,
( ~ hskp11
| hskp2
| hskp22
| ~ c2_1(a1324) ),
inference(forward_subsumption_resolution,[status(thm)],[f783,f51]) ).
fof(f788,plain,
( ~ hskp9
| hskp2
| hskp22
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f784,f42]) ).
fof(f790,plain,
( ~ hskp3
| hskp2
| hskp22
| ~ c3_1(a1311) ),
inference(forward_subsumption_resolution,[status(thm)],[f786,f19]) ).
fof(f795,plain,
( ~ hskp11
| hskp23
| hskp22
| ~ c3_1(a1324)
| ~ c2_1(a1324)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f174,f52]) ).
fof(f796,plain,
( ~ hskp9
| hskp23
| hskp22
| ~ c3_1(a1320)
| ~ c2_1(a1320)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f174,f44]) ).
fof(f799,plain,
( ~ hskp3
| hskp23
| hskp22
| ~ c3_1(a1311)
| ~ c2_1(a1311)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f174,f20]) ).
fof(f802,plain,
( ~ hskp11
| hskp23
| hskp22
| ~ c3_1(a1324)
| ~ c2_1(a1324) ),
inference(forward_subsumption_resolution,[status(thm)],[f795,f49]) ).
fof(f803,plain,
( ~ hskp9
| hskp23
| hskp22
| ~ c3_1(a1320)
| ~ c2_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f41]) ).
fof(f805,plain,
( ~ hskp3
| hskp23
| hskp22
| ~ c3_1(a1311)
| ~ c2_1(a1311) ),
inference(forward_subsumption_resolution,[status(thm)],[f799,f17]) ).
fof(f806,plain,
( ~ hskp11
| hskp23
| hskp22
| ~ c2_1(a1324) ),
inference(forward_subsumption_resolution,[status(thm)],[f802,f51]) ).
fof(f807,plain,
( ~ hskp9
| hskp23
| hskp22
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f803,f42]) ).
fof(f809,plain,
( ~ hskp3
| hskp23
| hskp22
| ~ c3_1(a1311) ),
inference(forward_subsumption_resolution,[status(thm)],[f805,f19]) ).
fof(f813,plain,
! [X0,X1] :
( ~ hskp18
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(a1339)
| c0_1(a1339)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f218,f80]) ).
fof(f823,plain,
! [X0,X1] :
( ~ hskp18
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(a1339)
| c0_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f813,f77]) ).
fof(f850,plain,
! [X0,X1] :
( ~ hskp15
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1331)
| c0_1(a1331)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f220,f68]) ).
fof(f854,plain,
! [X0,X1] :
( ~ hskp5
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1314)
| c0_1(a1314)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f220,f28]) ).
fof(f857,plain,
! [X0,X1] :
( ~ hskp15
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1331)
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f850,f65]) ).
fof(f860,plain,
! [X0,X1] :
( ~ hskp5
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1314)
| c0_1(a1314) ),
inference(forward_subsumption_resolution,[status(thm)],[f854,f25]) ).
fof(f861,plain,
( ~ hskp26
| hskp17
| hskp4
| ~ c0_1(a1411)
| c2_1(a1411)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f176,f112]) ).
fof(f873,plain,
( ~ hskp26
| hskp17
| hskp4
| ~ c0_1(a1411)
| c2_1(a1411) ),
inference(forward_subsumption_resolution,[status(thm)],[f861,f109]) ).
fof(f877,plain,
( ~ hskp26
| hskp17
| hskp4
| ~ c0_1(a1411) ),
inference(forward_subsumption_resolution,[status(thm)],[f873,f111]) ).
fof(f923,plain,
( ~ hskp16
| hskp13
| hskp14
| ~ c1_1(a1333)
| c2_1(a1333)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f178,f72]) ).
fof(f932,plain,
( ~ hskp16
| hskp13
| hskp14
| ~ c1_1(a1333)
| c2_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f923,f69]) ).
fof(f937,plain,
( ~ hskp16
| hskp13
| hskp14
| ~ c1_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f932,f71]) ).
fof(f944,plain,
( ~ hskp22
| hskp8
| hskp14
| ~ c1_1(a1356)
| ~ c0_1(a1356)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f179,f96]) ).
fof(f945,plain,
( ~ hskp16
| hskp8
| hskp14
| ~ c1_1(a1333)
| ~ c0_1(a1333)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f179,f72]) ).
fof(f954,plain,
( ~ hskp22
| hskp8
| hskp14
| ~ c1_1(a1356)
| ~ c0_1(a1356) ),
inference(forward_subsumption_resolution,[status(thm)],[f944,f93]) ).
fof(f955,plain,
( ~ hskp16
| hskp8
| hskp14
| ~ c1_1(a1333)
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f945,f69]) ).
fof(f966,plain,
! [X0] :
( ~ hskp8
| hskp4
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(a1319)
| c0_1(a1319)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f222,f40]) ).
fof(f973,plain,
! [X0] :
( ~ hskp8
| hskp4
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(a1319)
| c0_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f966,f37]) ).
fof(f983,plain,
! [X0,X1] :
( ~ hskp8
| ~ c2_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1319)
| c0_1(a1319)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f223,f40]) ).
fof(f990,plain,
! [X0,X1] :
( ~ hskp8
| ~ c2_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1319)
| c0_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f983,f37]) ).
fof(f993,plain,
( ~ hskp22
| hskp8
| hskp14
| ~ c1_1(a1356) ),
inference(forward_subsumption_resolution,[status(thm)],[f954,f94]) ).
fof(f994,plain,
( ~ hskp16
| hskp8
| hskp14
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f955,f70]) ).
fof(f1066,plain,
! [X0,X1] :
( ~ hskp8
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1319)
| c0_1(a1319)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f224,f40]) ).
fof(f1073,plain,
! [X0,X1] :
( ~ hskp8
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1319)
| c0_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f1066,f37]) ).
fof(f1077,plain,
! [X0] :
( ~ hskp20
| hskp28
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c2_1(a1348)
| ~ c1_1(a1348)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f225,f88]) ).
fof(f1087,plain,
! [X0] :
( ~ hskp20
| hskp28
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c2_1(a1348)
| ~ c1_1(a1348) ),
inference(forward_subsumption_resolution,[status(thm)],[f1077,f85]) ).
fof(f1096,plain,
! [X0] :
( ~ hskp9
| hskp0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(a1320)
| ~ c2_1(a1320)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f226,f43]) ).
fof(f1105,plain,
! [X0] :
( ~ hskp9
| hskp0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(a1320)
| ~ c2_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f1096,f41]) ).
fof(f1117,plain,
( ~ hskp15
| hskp6
| hskp9
| ~ c2_1(a1331)
| ~ c0_1(a1331)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f184,f68]) ).
fof(f1122,plain,
( ~ hskp4
| hskp6
| hskp9
| ~ c2_1(a1312)
| ~ c0_1(a1312)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f184,f24]) ).
fof(f1126,plain,
( ~ hskp15
| hskp6
| hskp9
| ~ c2_1(a1331)
| ~ c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f1117,f65]) ).
fof(f1127,plain,
( ~ hskp4
| hskp6
| hskp9
| ~ c2_1(a1312)
| ~ c0_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f1122,f21]) ).
fof(f1131,plain,
! [X0] :
( ~ hskp14
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1330)
| c2_1(a1330)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f227,f63]) ).
fof(f1132,plain,
! [X0] :
( ~ hskp13
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1326)
| c2_1(a1326)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f227,f58]) ).
fof(f1136,plain,
! [X0] :
( ~ hskp4
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1312)
| c2_1(a1312)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f227,f23]) ).
fof(f1140,plain,
! [X0] :
( ~ hskp14
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1330)
| c2_1(a1330) ),
inference(forward_subsumption_resolution,[status(thm)],[f1131,f61]) ).
fof(f1141,plain,
! [X0] :
( ~ hskp13
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1326)
| c2_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f1132,f57]) ).
fof(f1143,plain,
! [X0] :
( ~ hskp4
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1312)
| c2_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f1136,f21]) ).
fof(f1147,plain,
( ~ hskp15
| hskp6
| hskp9
| ~ c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f1126,f67]) ).
fof(f1148,plain,
( ~ hskp4
| hskp6
| hskp9
| ~ c2_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f1127,f22]) ).
fof(f1188,plain,
! [X0] :
( ~ hskp13
| hskp14
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(a1326)
| c2_1(a1326)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f228,f58]) ).
fof(f1196,plain,
! [X0] :
( ~ hskp13
| hskp14
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(a1326)
| c2_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f1188,f57]) ).
fof(f1280,plain,
! [X0,X1] :
( ~ hskp1
| ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1308)
| c2_1(a1308)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f230,f11]) ).
fof(f1285,plain,
! [X0,X1] :
( ~ hskp1
| ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1308)
| c2_1(a1308) ),
inference(forward_subsumption_resolution,[status(thm)],[f1280,f9]) ).
fof(f1343,plain,
! [X0] :
( ~ hskp16
| hskp27
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(a1333)
| c2_1(a1333)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f233,f72]) ).
fof(f1352,plain,
! [X0] :
( ~ hskp16
| hskp27
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(a1333)
| c2_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f1343,f69]) ).
fof(f1410,plain,
! [X0] :
( ~ hskp9
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f43]) ).
fof(f1414,plain,
( ~ hskp18
| ~ hskp9
| hskp7
| ~ c3_1(a1339)
| ~ c1_1(a1339)
| ~ c3_1(a1320) ),
inference(resolution,[status(thm)],[f1410,f80]) ).
fof(f1425,plain,
( ~ hskp18
| ~ hskp9
| hskp7
| ~ c3_1(a1339)
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f1414,f78]) ).
fof(f1429,plain,
! [X0] :
( ~ hskp6
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1315) ),
inference(forward_subsumption_resolution,[status(thm)],[f432,f31]) ).
fof(f1433,plain,
( ~ hskp18
| ~ hskp6
| hskp7
| ~ c3_1(a1339)
| ~ c1_1(a1339)
| ~ c3_1(a1315) ),
inference(resolution,[status(thm)],[f1429,f80]) ).
fof(f1439,plain,
( ~ hskp2
| ~ hskp6
| hskp7
| ~ c3_1(a1309)
| ~ c1_1(a1309)
| ~ c3_1(a1315) ),
inference(resolution,[status(thm)],[f1429,f16]) ).
fof(f1444,plain,
( ~ hskp18
| ~ hskp6
| hskp7
| ~ c3_1(a1339)
| ~ c1_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f1433,f30]) ).
fof(f1446,plain,
( ~ hskp2
| ~ hskp6
| hskp7
| ~ c3_1(a1309)
| ~ c1_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f1439,f30]) ).
fof(f1449,plain,
( ~ hskp18
| ~ hskp6
| hskp7
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f1444,f78]) ).
fof(f1451,plain,
( ~ hskp2
| ~ hskp6
| hskp7
| ~ c3_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f1446,f14]) ).
fof(f1471,plain,
! [X0,X1] :
( ~ hskp23
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| c2_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f285,f98]) ).
fof(f1490,plain,
! [X0] :
( ~ hskp0
| hskp7
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| ~ c3_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f434,f6]) ).
fof(f1494,plain,
( ~ hskp18
| ~ hskp0
| hskp7
| ~ c3_1(a1339)
| ~ c1_1(a1339)
| ~ c3_1(a1306) ),
inference(resolution,[status(thm)],[f1490,f80]) ).
fof(f1505,plain,
( ~ hskp18
| ~ hskp0
| hskp7
| ~ c3_1(a1339)
| ~ c3_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f1494,f78]) ).
fof(f1667,plain,
! [X0] :
( ~ hskp23
| hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| c2_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f507,f98]) ).
fof(f1668,plain,
! [X0,X1] :
( ~ hskp0
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0)
| c2_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f289,f6]) ).
fof(f1678,plain,
! [X0] :
( ~ hskp2
| ~ hskp0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1309)
| ~ c1_1(a1309)
| c2_1(a1306) ),
inference(resolution,[status(thm)],[f1668,f16]) ).
fof(f1685,plain,
! [X0] :
( ~ hskp2
| ~ hskp0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1309)
| ~ c1_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f1678,f8]) ).
fof(f1704,plain,
! [X0,X1] :
( ~ hskp23
| ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c3_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f364,f98]) ).
fof(f1706,plain,
! [X0] :
( ~ hskp23
| ~ hskp23
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a1359)
| c0_1(a1359)
| c3_1(a1359) ),
inference(resolution,[status(thm)],[f1704,f99]) ).
fof(f1717,plain,
! [X0] :
( ~ hskp23
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a1359)
| c0_1(a1359)
| c3_1(a1359) ),
inference(duplicate_literals_removal,[status(thm)],[f1706]) ).
fof(f1718,plain,
! [X0] :
( ~ hskp23
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a1359)
| c0_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f1717,f100]) ).
fof(f1763,plain,
! [X0] :
( ~ hskp23
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f1718,f98]) ).
fof(f1765,plain,
( ~ hskp23
| ~ hskp23
| ~ c2_1(a1359)
| c3_1(a1359)
| ~ c2_1(a1359) ),
inference(resolution,[status(thm)],[f1763,f99]) ).
fof(f1776,plain,
( ~ hskp23
| c3_1(a1359)
| ~ c2_1(a1359) ),
inference(duplicate_literals_removal,[status(thm)],[f1765]) ).
fof(f1777,plain,
( ~ hskp23
| ~ c2_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f1776,f100]) ).
fof(f1782,plain,
! [X0,X1] :
( ~ hskp23
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c2_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1471,f1777]) ).
fof(f1785,plain,
! [X0] :
( ~ hskp23
| hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1667,f1777]) ).
fof(f1792,plain,
( ~ hskp23
| hskp1
| hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f327,f1777]) ).
fof(f1810,plain,
( hskp1
| hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f1792,f202]) ).
fof(f1812,plain,
! [X0,X1] :
( ~ hskp9
| ~ c2_1(X1)
| c3_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f366,f43]) ).
fof(f1818,plain,
! [X0] :
( ~ hskp9
| ~ hskp9
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a1320)
| c0_1(a1320)
| c3_1(a1320) ),
inference(resolution,[status(thm)],[f1812,f44]) ).
fof(f1824,plain,
! [X0] :
( ~ hskp9
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a1320)
| c0_1(a1320)
| c3_1(a1320) ),
inference(duplicate_literals_removal,[status(thm)],[f1818]) ).
fof(f1825,plain,
! [X0] :
( ~ hskp9
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c2_1(a1320)
| c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f1824,f43]) ).
fof(f1869,plain,
( ~ hskp20
| ~ hskp23
| hskp6
| ~ c2_1(a1348)
| ~ c1_1(a1348) ),
inference(resolution,[status(thm)],[f1785,f88]) ).
fof(f1880,plain,
( ~ hskp20
| ~ hskp23
| hskp6
| ~ c2_1(a1348) ),
inference(forward_subsumption_resolution,[status(thm)],[f1869,f86]) ).
fof(f1883,plain,
( ~ hskp20
| ~ hskp23
| hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f1880,f87]) ).
fof(f1884,plain,
! [X0] :
( ~ hskp9
| ~ c2_1(X0)
| c3_1(X0)
| c1_1(X0)
| c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f1825,f42]) ).
fof(f1890,plain,
( ~ hskp9
| ~ hskp9
| ~ c2_1(a1320)
| c3_1(a1320)
| c3_1(a1320) ),
inference(resolution,[status(thm)],[f1884,f44]) ).
fof(f1897,plain,
( ~ hskp9
| ~ c2_1(a1320)
| c3_1(a1320) ),
inference(duplicate_literals_removal,[status(thm)],[f1890]) ).
fof(f1898,plain,
( ~ hskp9
| c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f1897,f42]) ).
fof(f1908,plain,
( ~ hskp18
| ~ hskp9
| hskp7
| ~ c3_1(a1339) ),
inference(backward_subsumption_resolution,[status(thm)],[f1425,f1898]) ).
fof(f1912,plain,
( ~ hskp9
| hskp23
| hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f807,f1898]) ).
fof(f1913,plain,
( ~ hskp9
| hskp2
| hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f788,f1898]) ).
fof(f1955,plain,
! [X0] :
( ~ hskp2
| ~ hskp23
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1309)
| ~ c1_1(a1309) ),
inference(resolution,[status(thm)],[f1782,f16]) ).
fof(f1963,plain,
! [X0] :
( ~ hskp2
| ~ hskp23
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f1955,f14]) ).
fof(f1982,plain,
! [X0] :
( ~ hskp23
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f599,f98]) ).
fof(f1983,plain,
! [X0] :
( ~ hskp23
| ~ hskp23
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(resolution,[status(thm)],[f1982,f1777]) ).
fof(f1984,plain,
! [X0] :
( ~ hskp23
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1983]) ).
fof(f1985,plain,
! [X0] :
( ~ hskp16
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f71]) ).
fof(f1992,plain,
( ~ hskp9
| ~ hskp23
| hskp8
| ~ c3_1(a1320)
| ~ c2_1(a1320) ),
inference(resolution,[status(thm)],[f1984,f43]) ).
fof(f2002,plain,
( ~ hskp9
| ~ hskp23
| hskp8
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f1992,f42]) ).
fof(f2005,plain,
( ~ hskp9
| ~ hskp23
| hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f2002,f1898]) ).
fof(f2397,plain,
! [X0] :
( ~ hskp7
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| c2_1(a1316) ),
inference(forward_subsumption_resolution,[status(thm)],[f602,f34]) ).
fof(f2398,plain,
! [X0] :
( ~ hskp7
| ~ hskp7
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(resolution,[status(thm)],[f2397,f35]) ).
fof(f2399,plain,
! [X0] :
( ~ hskp7
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2398]) ).
fof(f2405,plain,
( ~ hskp17
| ~ hskp7
| hskp8
| ~ c3_1(a1334)
| ~ c2_1(a1334) ),
inference(resolution,[status(thm)],[f2399,f76]) ).
fof(f2407,plain,
( ~ hskp9
| ~ hskp7
| hskp8
| ~ c3_1(a1320)
| ~ c2_1(a1320) ),
inference(resolution,[status(thm)],[f2399,f43]) ).
fof(f2414,plain,
( ~ hskp17
| ~ hskp7
| hskp8
| ~ c3_1(a1334) ),
inference(forward_subsumption_resolution,[status(thm)],[f2405,f74]) ).
fof(f2416,plain,
( ~ hskp9
| ~ hskp7
| hskp8
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f2407,f42]) ).
fof(f2419,plain,
( ~ hskp17
| ~ hskp7
| hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f2414,f75]) ).
fof(f2420,plain,
( ~ hskp9
| ~ hskp7
| hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f2416,f1898]) ).
fof(f2668,plain,
! [X0] :
( ~ hskp13
| hskp9
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f618,f59]) ).
fof(f2679,plain,
( ~ hskp16
| ~ hskp13
| hskp9
| ~ c0_1(a1333)
| c2_1(a1333)
| c0_1(a1326) ),
inference(resolution,[status(thm)],[f2668,f72]) ).
fof(f2689,plain,
( ~ hskp16
| ~ hskp13
| hskp9
| ~ c0_1(a1333)
| c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f2679,f71]) ).
fof(f2967,plain,
! [X0] :
( ~ hskp7
| hskp9
| ~ c0_1(X0)
| c3_1(X0)
| c2_1(X0)
| c2_1(a1316) ),
inference(forward_subsumption_resolution,[status(thm)],[f619,f34]) ).
fof(f2979,plain,
( ~ hskp16
| ~ hskp7
| hskp9
| ~ c0_1(a1333)
| c2_1(a1333)
| c2_1(a1316) ),
inference(resolution,[status(thm)],[f2967,f72]) ).
fof(f2989,plain,
( ~ hskp16
| ~ hskp7
| hskp9
| ~ c0_1(a1333)
| c2_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f2979,f35]) ).
fof(f3041,plain,
( ~ hskp16
| ~ hskp7
| hskp9
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f2989,f71]) ).
fof(f3045,plain,
! [X0,X1] :
( ~ hskp18
| ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f634,f79]) ).
fof(f3050,plain,
! [X0] :
( ~ hskp18
| ~ hskp18
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1339)
| c0_1(a1339)
| ~ c1_1(a1339) ),
inference(resolution,[status(thm)],[f3045,f80]) ).
fof(f3058,plain,
! [X0] :
( ~ hskp0
| ~ hskp18
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1306)
| c0_1(a1306)
| ~ c1_1(a1339) ),
inference(resolution,[status(thm)],[f3045,f8]) ).
fof(f3060,plain,
! [X0] :
( ~ hskp18
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1339)
| c0_1(a1339)
| ~ c1_1(a1339) ),
inference(duplicate_literals_removal,[status(thm)],[f3050]) ).
fof(f3061,plain,
! [X0] :
( ~ hskp18
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1339)
| c0_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f3060,f78]) ).
fof(f3064,plain,
! [X0] :
( ~ hskp0
| ~ hskp18
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1306)
| c0_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f3058,f78]) ).
fof(f3066,plain,
! [X0] :
( ~ hskp2
| ~ hskp23
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1963,f15]) ).
fof(f3077,plain,
( ~ hskp22
| ~ hskp2
| ~ hskp23
| ~ c1_1(a1356)
| ~ c0_1(a1356) ),
inference(resolution,[status(thm)],[f3066,f96]) ).
fof(f3097,plain,
( ~ hskp22
| ~ hskp2
| ~ hskp23
| ~ c1_1(a1356) ),
inference(forward_subsumption_resolution,[status(thm)],[f3077,f94]) ).
fof(f3177,plain,
( ~ hskp22
| ~ hskp2
| ~ hskp23 ),
inference(forward_subsumption_resolution,[status(thm)],[f3097,f95]) ).
fof(f3182,plain,
( hskp0
| hskp6
| ~ hskp22
| ~ hskp2 ),
inference(resolution,[status(thm)],[f3177,f204]) ).
fof(f3277,plain,
! [X0,X1] :
( ~ hskp2
| ~ c1_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| c0_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f637,f14]) ).
fof(f3288,plain,
! [X0] :
( ~ hskp2
| ~ hskp2
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1309)
| c0_1(a1309)
| c0_1(a1309) ),
inference(resolution,[status(thm)],[f3277,f16]) ).
fof(f3293,plain,
! [X0] :
( ~ hskp2
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1309)
| c0_1(a1309) ),
inference(duplicate_literals_removal,[status(thm)],[f3288]) ).
fof(f3294,plain,
! [X0] :
( ~ hskp2
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| c0_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f3293,f15]) ).
fof(f3321,plain,
! [X0] :
( ~ hskp18
| hskp9
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f672,f79]) ).
fof(f3356,plain,
! [X0] :
( ~ hskp16
| hskp9
| ~ c1_1(X0)
| c3_1(X0)
| c0_1(X0)
| c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f70]) ).
fof(f3368,plain,
( ~ hskp16
| ~ hskp16
| hskp9
| ~ c1_1(a1333)
| c0_1(a1333)
| c0_1(a1333) ),
inference(resolution,[status(thm)],[f3356,f72]) ).
fof(f3376,plain,
( ~ hskp16
| hskp9
| ~ c1_1(a1333)
| c0_1(a1333) ),
inference(duplicate_literals_removal,[status(thm)],[f3368]) ).
fof(f3377,plain,
( ~ hskp16
| hskp9
| c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f3376,f70]) ).
fof(f3383,plain,
( ~ hskp16
| ~ hskp7
| hskp9 ),
inference(backward_subsumption_resolution,[status(thm)],[f3041,f3377]) ).
fof(f3384,plain,
( ~ hskp16
| ~ hskp13
| hskp9
| c0_1(a1326) ),
inference(backward_subsumption_resolution,[status(thm)],[f2689,f3377]) ).
fof(f3455,plain,
( ~ hskp16
| ~ hskp2
| ~ c1_1(a1333)
| c2_1(a1333)
| c0_1(a1309) ),
inference(resolution,[status(thm)],[f3294,f72]) ).
fof(f3464,plain,
( ~ hskp16
| ~ hskp2
| ~ c1_1(a1333)
| c0_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f3455,f71]) ).
fof(f3510,plain,
! [X0] :
( ~ hskp18
| hskp11
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f729,f79]) ).
fof(f3528,plain,
( ~ hskp23
| ~ hskp18
| hskp11
| c3_1(a1359)
| c2_1(a1359)
| ~ c1_1(a1339) ),
inference(resolution,[status(thm)],[f3510,f99]) ).
fof(f3537,plain,
( ~ hskp0
| ~ hskp18
| hskp11
| c3_1(a1306)
| c2_1(a1306)
| ~ c1_1(a1339) ),
inference(resolution,[status(thm)],[f3510,f7]) ).
fof(f3545,plain,
( ~ hskp23
| ~ hskp18
| hskp11
| c3_1(a1359)
| c2_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f3528,f78]) ).
fof(f3549,plain,
( ~ hskp0
| ~ hskp18
| hskp11
| c3_1(a1306)
| c2_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f3537,f78]) ).
fof(f3588,plain,
( ~ hskp16
| ~ hskp2
| c0_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f3464,f70]) ).
fof(f3628,plain,
( ~ hskp23
| ~ hskp18
| hskp11
| c3_1(a1359) ),
inference(forward_subsumption_resolution,[status(thm)],[f3545,f1777]) ).
fof(f3629,plain,
( ~ hskp23
| ~ hskp23
| ~ hskp18
| hskp11 ),
inference(resolution,[status(thm)],[f3628,f100]) ).
fof(f3630,plain,
( ~ hskp23
| ~ hskp18
| hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f3629]) ).
fof(f3636,plain,
( ~ hskp0
| ~ hskp18
| hskp11
| c3_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f3549,f8]) ).
fof(f3734,plain,
! [X0,X1] :
( ~ hskp18
| ~ c3_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f823,f79]) ).
fof(f3740,plain,
! [X0] :
( ~ hskp18
| ~ hskp18
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1339)
| ~ c1_1(a1339)
| ~ c3_1(a1339) ),
inference(resolution,[status(thm)],[f3734,f79]) ).
fof(f3751,plain,
! [X0] :
( ~ hskp18
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c1_1(a1339)
| ~ c3_1(a1339) ),
inference(duplicate_literals_removal,[status(thm)],[f3740]) ).
fof(f3752,plain,
! [X0] :
( ~ hskp18
| ~ c3_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f3751,f78]) ).
fof(f4118,plain,
( ~ hskp11
| ~ hskp18
| ~ c3_1(a1324)
| ~ c0_1(a1324)
| ~ c3_1(a1339) ),
inference(resolution,[status(thm)],[f3752,f52]) ).
fof(f4128,plain,
( ~ hskp11
| ~ hskp18
| ~ c3_1(a1324)
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f4118,f50]) ).
fof(f4184,plain,
( ~ hskp11
| ~ hskp18
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f4128,f51]) ).
fof(f4187,plain,
( ~ hskp18
| hskp9
| ~ c1_1(a1339)
| c0_1(a1339)
| ~ c1_1(a1339)
| ~ hskp11
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4184,f3321]) ).
fof(f4227,plain,
( hskp9
| c0_1(a1339)
| ~ c1_1(a1339)
| ~ hskp11
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f4187]) ).
fof(f4228,plain,
( hskp9
| c0_1(a1339)
| ~ hskp11
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4227,f78]) ).
fof(f4240,plain,
( hskp9
| ~ hskp11
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4228,f79]) ).
fof(f4720,plain,
! [X0,X1] :
( ~ hskp15
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f857,f66]) ).
fof(f4741,plain,
! [X0] :
( ~ hskp13
| ~ hskp15
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| c3_1(a1326)
| c2_1(a1326)
| c0_1(a1331) ),
inference(resolution,[status(thm)],[f4720,f58]) ).
fof(f4751,plain,
! [X0] :
( ~ hskp13
| ~ hskp15
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| c3_1(a1326)
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f4741,f59]) ).
fof(f5310,plain,
! [X0,X1] :
( ~ hskp5
| ~ c1_1(X1)
| ~ c0_1(X1)
| c3_1(X1)
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a1314) ),
inference(forward_subsumption_resolution,[status(thm)],[f860,f27]) ).
fof(f5338,plain,
! [X0] :
( ~ hskp13
| ~ hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| c3_1(a1326)
| c2_1(a1326)
| ~ c1_1(a1314) ),
inference(resolution,[status(thm)],[f5310,f58]) ).
fof(f5349,plain,
! [X0] :
( ~ hskp13
| ~ hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| c3_1(a1326)
| c2_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f5338,f26]) ).
fof(f5459,plain,
! [X0] :
( ~ hskp18
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f3061,f79]) ).
fof(f5479,plain,
( ~ hskp7
| ~ hskp18
| ~ c1_1(a1316)
| c2_1(a1316)
| ~ c3_1(a1339) ),
inference(resolution,[status(thm)],[f5459,f36]) ).
fof(f5492,plain,
( ~ hskp7
| ~ hskp18
| ~ c1_1(a1316)
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f5479,f35]) ).
fof(f5636,plain,
( ~ hskp18
| hskp11
| c3_1(a1316)
| c2_1(a1316)
| ~ c1_1(a1339)
| ~ hskp7
| ~ hskp18
| ~ c3_1(a1339) ),
inference(resolution,[status(thm)],[f5492,f3510]) ).
fof(f5675,plain,
( hskp11
| c3_1(a1316)
| c2_1(a1316)
| ~ c1_1(a1339)
| ~ hskp7
| ~ hskp18
| ~ c3_1(a1339) ),
inference(duplicate_literals_removal,[status(thm)],[f5636]) ).
fof(f5676,plain,
( hskp11
| c3_1(a1316)
| c2_1(a1316)
| ~ hskp7
| ~ hskp18
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f5675,f78]) ).
fof(f5782,plain,
! [X0] :
( ~ hskp8
| hskp4
| ~ c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0)
| ~ c2_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f973,f39]) ).
fof(f5790,plain,
( ~ hskp12
| ~ hskp8
| hskp4
| ~ c3_1(a1325)
| ~ c1_1(a1325)
| ~ c2_1(a1319) ),
inference(resolution,[status(thm)],[f5782,f56]) ).
fof(f5801,plain,
( ~ hskp12
| ~ hskp8
| hskp4
| ~ c3_1(a1325)
| ~ c1_1(a1325) ),
inference(forward_subsumption_resolution,[status(thm)],[f5790,f38]) ).
fof(f5808,plain,
( ~ hskp12
| ~ hskp8
| hskp4
| ~ c3_1(a1325) ),
inference(forward_subsumption_resolution,[status(thm)],[f5801,f54]) ).
fof(f5809,plain,
( hskp11
| c3_1(a1316)
| ~ hskp7
| ~ hskp18
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f5676,f35]) ).
fof(f5810,plain,
( ~ hskp7
| hskp11
| ~ hskp7
| ~ hskp18
| ~ c3_1(a1339) ),
inference(resolution,[status(thm)],[f5809,f36]) ).
fof(f5811,plain,
( hskp11
| ~ hskp7
| ~ hskp18
| ~ c3_1(a1339) ),
inference(duplicate_literals_removal,[status(thm)],[f5810]) ).
fof(f5812,plain,
( ~ hskp7
| ~ hskp18
| ~ c3_1(a1339) ),
inference(forward_subsumption_resolution,[status(thm)],[f5811,f4184]) ).
fof(f5814,plain,
( ~ hskp18
| ~ hskp9
| ~ c3_1(a1339) ),
inference(backward_subsumption_resolution,[status(thm)],[f1908,f5812]) ).
fof(f5815,plain,
( ~ hskp18
| ~ hskp0
| ~ c3_1(a1339)
| ~ c3_1(a1306) ),
inference(backward_subsumption_resolution,[status(thm)],[f1505,f5812]) ).
fof(f5816,plain,
( ~ hskp18
| ~ hskp6
| ~ c3_1(a1339) ),
inference(backward_subsumption_resolution,[status(thm)],[f1449,f5812]) ).
fof(f5973,plain,
( hskp28
| ~ c1_1(a1339)
| c0_1(a1339)
| ~ ndr1_0
| ~ hskp18
| ~ hskp9 ),
inference(resolution,[status(thm)],[f5814,f151]) ).
fof(f5985,plain,
( hskp28
| ~ c1_1(a1339)
| c0_1(a1339)
| ~ hskp18
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f5973,f77]) ).
fof(f6011,plain,
( ~ hskp18
| hskp9
| ~ c1_1(a1339)
| c0_1(a1339)
| ~ c1_1(a1339)
| ~ hskp18
| ~ hskp6 ),
inference(resolution,[status(thm)],[f5816,f3321]) ).
fof(f6051,plain,
( hskp9
| c0_1(a1339)
| ~ c1_1(a1339)
| ~ hskp18
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f6011]) ).
fof(f6052,plain,
( hskp9
| c0_1(a1339)
| ~ hskp18
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f6051,f78]) ).
fof(f6063,plain,
( hskp9
| ~ hskp18
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f6052,f79]) ).
fof(f6127,plain,
( hskp28
| ~ c1_1(a1339)
| ~ hskp18
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f5985,f79]) ).
fof(f6154,plain,
! [X0,X1] :
( ~ hskp8
| ~ c2_1(X1)
| ~ c0_1(X1)
| c1_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f990,f39]) ).
fof(f6161,plain,
! [X0] :
( ~ hskp17
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1334)
| ~ c2_1(a1334)
| ~ c2_1(a1319) ),
inference(resolution,[status(thm)],[f6154,f76]) ).
fof(f6163,plain,
! [X0] :
( ~ hskp9
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1320)
| ~ c2_1(a1320)
| ~ c2_1(a1319) ),
inference(resolution,[status(thm)],[f6154,f43]) ).
fof(f6170,plain,
! [X0] :
( ~ hskp17
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1334)
| ~ c2_1(a1334) ),
inference(forward_subsumption_resolution,[status(thm)],[f6161,f38]) ).
fof(f6172,plain,
! [X0] :
( ~ hskp9
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1320)
| ~ c2_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f6163,f38]) ).
fof(f6228,plain,
! [X0,X1] :
( ~ hskp8
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1319) ),
inference(forward_subsumption_resolution,[status(thm)],[f1073,f39]) ).
fof(f6235,plain,
! [X0] :
( ~ hskp17
| ~ hskp8
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1334)
| ~ c2_1(a1334)
| ~ c2_1(a1319) ),
inference(resolution,[status(thm)],[f6228,f76]) ).
fof(f6237,plain,
! [X0] :
( ~ hskp9
| ~ hskp8
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1320)
| ~ c2_1(a1320)
| ~ c2_1(a1319) ),
inference(resolution,[status(thm)],[f6228,f43]) ).
fof(f6244,plain,
! [X0] :
( ~ hskp17
| ~ hskp8
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1334)
| ~ c2_1(a1334) ),
inference(forward_subsumption_resolution,[status(thm)],[f6235,f38]) ).
fof(f6246,plain,
! [X0] :
( ~ hskp9
| ~ hskp8
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1320)
| ~ c2_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f6237,f38]) ).
fof(f6273,plain,
! [X0] :
( ~ hskp20
| hskp28
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c2_1(a1348) ),
inference(forward_subsumption_resolution,[status(thm)],[f1087,f86]) ).
fof(f6280,plain,
( ~ hskp14
| ~ hskp20
| hskp28
| ~ c3_1(a1330)
| ~ c0_1(a1330)
| ~ c2_1(a1348) ),
inference(resolution,[status(thm)],[f6273,f64]) ).
fof(f6288,plain,
( ~ hskp14
| ~ hskp20
| hskp28
| ~ c3_1(a1330)
| ~ c0_1(a1330) ),
inference(forward_subsumption_resolution,[status(thm)],[f6280,f87]) ).
fof(f6293,plain,
( ~ hskp14
| ~ hskp20
| hskp28
| ~ c3_1(a1330) ),
inference(forward_subsumption_resolution,[status(thm)],[f6288,f62]) ).
fof(f6401,plain,
! [X0] :
( ~ hskp9
| hskp0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f1105,f42]) ).
fof(f6412,plain,
( ~ hskp2
| ~ hskp9
| hskp0
| ~ c1_1(a1309)
| ~ c0_1(a1309)
| ~ c3_1(a1320) ),
inference(resolution,[status(thm)],[f6401,f16]) ).
fof(f6419,plain,
( ~ hskp2
| ~ hskp9
| hskp0
| ~ c1_1(a1309)
| ~ c0_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f6412,f1898]) ).
fof(f6447,plain,
! [X0] :
( ~ hskp14
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1330) ),
inference(forward_subsumption_resolution,[status(thm)],[f1140,f64]) ).
fof(f6474,plain,
( ~ hskp14
| ~ hskp14
| hskp15
| ~ c0_1(a1330)
| c3_1(a1330)
| ~ c0_1(a1330) ),
inference(resolution,[status(thm)],[f6447,f63]) ).
fof(f6479,plain,
( ~ hskp4
| ~ hskp14
| hskp15
| ~ c0_1(a1312)
| c3_1(a1312)
| ~ c0_1(a1330) ),
inference(resolution,[status(thm)],[f6447,f23]) ).
fof(f6492,plain,
( ~ hskp14
| hskp15
| c3_1(a1330)
| ~ c0_1(a1330) ),
inference(duplicate_literals_removal,[status(thm)],[f6474]) ).
fof(f6493,plain,
( ~ hskp14
| hskp15
| c3_1(a1330) ),
inference(forward_subsumption_resolution,[status(thm)],[f6492,f62]) ).
fof(f6495,plain,
( ~ hskp4
| ~ hskp14
| hskp15
| ~ c0_1(a1312)
| c3_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f6479,f62]) ).
fof(f6498,plain,
( ~ hskp2
| ~ hskp9
| hskp0
| ~ c0_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f6419,f14]) ).
fof(f6502,plain,
( ~ hskp4
| ~ hskp14
| hskp15
| ~ c0_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f6495,f24]) ).
fof(f6506,plain,
! [X0] :
( ~ hskp13
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f1141,f59]) ).
fof(f6534,plain,
( ~ hskp13
| ~ hskp13
| hskp15
| ~ c0_1(a1326)
| c3_1(a1326)
| ~ c0_1(a1326) ),
inference(resolution,[status(thm)],[f6506,f58]) ).
fof(f6551,plain,
( ~ hskp13
| hskp15
| c3_1(a1326)
| ~ c0_1(a1326) ),
inference(duplicate_literals_removal,[status(thm)],[f6534]) ).
fof(f6552,plain,
( ~ hskp13
| hskp15
| ~ c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f6551,f60]) ).
fof(f6602,plain,
! [X0] :
( ~ hskp4
| hskp15
| ~ c0_1(X0)
| c3_1(X0)
| c1_1(X0)
| c2_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f1143,f22]) ).
fof(f6634,plain,
( ~ hskp4
| ~ hskp4
| hskp15
| ~ c0_1(a1312)
| c3_1(a1312)
| c2_1(a1312) ),
inference(resolution,[status(thm)],[f6602,f23]) ).
fof(f6646,plain,
( ~ hskp4
| hskp15
| ~ c0_1(a1312)
| c3_1(a1312)
| c2_1(a1312) ),
inference(duplicate_literals_removal,[status(thm)],[f6634]) ).
fof(f6647,plain,
( ~ hskp4
| hskp15
| ~ c0_1(a1312)
| c2_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f6646,f24]) ).
fof(f6696,plain,
( ~ hskp4
| hskp15
| c2_1(a1312) ),
inference(forward_subsumption_resolution,[status(thm)],[f6647,f22]) ).
fof(f6699,plain,
! [X0] :
( ~ hskp13
| hskp14
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f1196,f59]) ).
fof(f6721,plain,
( ~ hskp15
| ~ hskp13
| hskp14
| ~ c2_1(a1331)
| ~ c0_1(a1331)
| ~ c0_1(a1326) ),
inference(resolution,[status(thm)],[f6699,f68]) ).
fof(f6730,plain,
( ~ hskp15
| ~ hskp13
| hskp14
| ~ c0_1(a1331)
| ~ c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f6721,f67]) ).
fof(f6737,plain,
( ~ hskp13
| hskp14
| ~ c0_1(a1331)
| ~ c0_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f6730,f6552]) ).
fof(f7289,plain,
! [X0,X1] :
( ~ hskp1
| ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1308) ),
inference(forward_subsumption_resolution,[status(thm)],[f1285,f12]) ).
fof(f7626,plain,
! [X0] :
( ~ hskp16
| hskp27
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f1352,f71]) ).
fof(f7647,plain,
( ~ hskp16
| ~ hskp16
| hskp27
| ~ c1_1(a1333)
| ~ c0_1(a1333)
| ~ c0_1(a1333) ),
inference(resolution,[status(thm)],[f7626,f72]) ).
fof(f7661,plain,
( ~ hskp16
| hskp27
| ~ c1_1(a1333)
| ~ c0_1(a1333) ),
inference(duplicate_literals_removal,[status(thm)],[f7647]) ).
fof(f7662,plain,
( ~ hskp16
| hskp27
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f7661,f70]) ).
fof(f9346,plain,
! [X0] :
( ~ hskp2
| ~ hskp0
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1309) ),
inference(forward_subsumption_resolution,[status(thm)],[f1685,f14]) ).
fof(f9371,plain,
( ~ hskp22
| ~ hskp2
| ~ hskp0
| ~ c1_1(a1356)
| ~ c0_1(a1356)
| ~ c3_1(a1309) ),
inference(resolution,[status(thm)],[f9346,f96]) ).
fof(f9372,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp0
| ~ c1_1(a1333)
| ~ c0_1(a1333)
| ~ c3_1(a1309) ),
inference(resolution,[status(thm)],[f9346,f72]) ).
fof(f9390,plain,
( ~ hskp22
| ~ hskp2
| ~ hskp0
| ~ c1_1(a1356)
| ~ c0_1(a1356) ),
inference(forward_subsumption_resolution,[status(thm)],[f9371,f15]) ).
fof(f9391,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp0
| ~ c1_1(a1333)
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f9372,f15]) ).
fof(f9551,plain,
( ~ hskp22
| ~ hskp2
| ~ hskp0
| ~ c1_1(a1356) ),
inference(forward_subsumption_resolution,[status(thm)],[f9390,f94]) ).
fof(f9552,plain,
( ~ hskp22
| ~ hskp22
| ~ hskp2
| ~ hskp0 ),
inference(resolution,[status(thm)],[f9551,f95]) ).
fof(f9608,plain,
( ~ hskp22
| ~ hskp2
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f9552]) ).
fof(f9638,plain,
( hskp6
| ~ hskp22
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f3182,f9608]) ).
fof(f9646,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp0
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f9391,f70]) ).
fof(f9651,plain,
( ~ hskp16
| hskp9
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(resolution,[status(thm)],[f9646,f3377]) ).
fof(f9652,plain,
! [X0] :
( ~ hskp16
| hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(resolution,[status(thm)],[f9646,f1985]) ).
fof(f9658,plain,
( ~ hskp16
| hskp28
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(resolution,[status(thm)],[f9646,f270]) ).
fof(f9682,plain,
( hskp9
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f9651]) ).
fof(f9683,plain,
! [X0] :
( hskp8
| ~ c3_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f9652]) ).
fof(f9689,plain,
( hskp28
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f9658]) ).
fof(f10563,plain,
( ~ hskp9
| hskp8
| ~ c3_1(a1320)
| ~ c2_1(a1320)
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(resolution,[status(thm)],[f9683,f43]) ).
fof(f10576,plain,
( ~ hskp9
| hskp8
| ~ c3_1(a1320)
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f10563,f42]) ).
fof(f10580,plain,
( ~ hskp9
| hskp8
| ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f10576,f1898]) ).
fof(f11227,plain,
! [X0] :
( ~ hskp0
| ~ hskp18
| ~ c1_1(X0)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f3064,f6]) ).
fof(f11230,plain,
( ~ hskp18
| ~ hskp0
| ~ c3_1(a1306)
| ~ hskp0
| ~ hskp18
| ~ c1_1(a1339)
| c2_1(a1339)
| ~ c3_1(a1306) ),
inference(resolution,[status(thm)],[f11227,f5815]) ).
fof(f11264,plain,
( ~ hskp0
| ~ hskp18
| ~ c1_1(a1339)
| c2_1(a1339)
| ~ c3_1(a1306) ),
inference(duplicate_literals_removal,[status(thm)],[f11230]) ).
fof(f11265,plain,
( ~ hskp0
| ~ hskp18
| ~ c1_1(a1339)
| ~ c3_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f11264,f80]) ).
fof(f11355,plain,
( ~ hskp0
| ~ hskp18
| hskp11 ),
inference(backward_subsumption_resolution,[status(thm)],[f3636,f11356]) ).
fof(f11356,plain,
( ~ hskp0
| ~ hskp18
| ~ c3_1(a1306) ),
inference(forward_subsumption_resolution,[status(thm)],[f11265,f78]) ).
fof(f16445,plain,
! [X0] :
( ~ hskp13
| ~ hskp15
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f4751,f60]) ).
fof(f16486,plain,
( ~ hskp16
| ~ hskp13
| ~ hskp15
| ~ c1_1(a1333)
| ~ c0_1(a1333)
| c0_1(a1331) ),
inference(resolution,[status(thm)],[f16445,f72]) ).
fof(f16502,plain,
( ~ hskp16
| ~ hskp13
| ~ hskp15
| ~ c0_1(a1333)
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f16486,f70]) ).
fof(f20713,plain,
! [X0] :
( ~ hskp13
| ~ hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| c3_1(a1326) ),
inference(forward_subsumption_resolution,[status(thm)],[f5349,f59]) ).
fof(f20714,plain,
! [X0] :
( ~ hskp13
| ~ hskp13
| ~ hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(resolution,[status(thm)],[f20713,f60]) ).
fof(f20715,plain,
! [X0] :
( ~ hskp13
| ~ hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f20714]) ).
fof(f21076,plain,
( ~ hskp22
| ~ hskp13
| ~ hskp5
| ~ c1_1(a1356)
| ~ c0_1(a1356) ),
inference(resolution,[status(thm)],[f20715,f96]) ).
fof(f21077,plain,
( ~ hskp16
| ~ hskp13
| ~ hskp5
| ~ c1_1(a1333)
| ~ c0_1(a1333) ),
inference(resolution,[status(thm)],[f20715,f72]) ).
fof(f21092,plain,
( ~ hskp22
| ~ hskp13
| ~ hskp5
| ~ c1_1(a1356) ),
inference(forward_subsumption_resolution,[status(thm)],[f21076,f94]) ).
fof(f21093,plain,
( ~ hskp16
| ~ hskp13
| ~ hskp5
| ~ c0_1(a1333) ),
inference(forward_subsumption_resolution,[status(thm)],[f21077,f70]) ).
fof(f21286,plain,
( ~ hskp22
| ~ hskp13
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f21092,f95]) ).
fof(f21310,plain,
( ~ hskp16
| hskp9
| ~ hskp16
| ~ hskp13
| ~ hskp5 ),
inference(resolution,[status(thm)],[f21093,f3377]) ).
fof(f21317,plain,
( ~ hskp16
| hskp28
| ~ hskp16
| ~ hskp13
| ~ hskp5 ),
inference(resolution,[status(thm)],[f21093,f270]) ).
fof(f21356,plain,
( hskp9
| ~ hskp16
| ~ hskp13
| ~ hskp5 ),
inference(duplicate_literals_removal,[status(thm)],[f21310]) ).
fof(f21363,plain,
( hskp28
| ~ hskp16
| ~ hskp13
| ~ hskp5 ),
inference(duplicate_literals_removal,[status(thm)],[f21317]) ).
fof(f22280,plain,
! [X0] :
( ~ hskp17
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1334) ),
inference(forward_subsumption_resolution,[status(thm)],[f6170,f74]) ).
fof(f22711,plain,
! [X0] :
( ~ hskp9
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| c1_1(X0)
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f6172,f42]) ).
fof(f24307,plain,
! [X0] :
( ~ hskp17
| ~ hskp8
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1334) ),
inference(forward_subsumption_resolution,[status(thm)],[f6244,f74]) ).
fof(f24328,plain,
! [X0] :
( ~ hskp17
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1334)
| ~ hskp17
| ~ hskp8
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1334) ),
inference(resolution,[status(thm)],[f24307,f22280]) ).
fof(f24429,plain,
! [X0] :
( ~ c2_1(X0)
| ~ hskp17
| ~ hskp8
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1334) ),
inference(duplicate_literals_removal,[status(thm)],[f24328]) ).
fof(f24430,plain,
! [X0] :
( ~ c2_1(X0)
| ~ hskp17
| ~ hskp8
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f24429,f75]) ).
fof(f24711,plain,
( ~ hskp30
| ~ c2_1(a1372)
| ~ hskp17
| ~ hskp8
| ~ c0_1(a1372) ),
inference(resolution,[status(thm)],[f24430,f128]) ).
fof(f24713,plain,
( ~ hskp28
| ~ c2_1(a1328)
| ~ hskp17
| ~ hskp8
| ~ c0_1(a1328) ),
inference(resolution,[status(thm)],[f24430,f120]) ).
fof(f24831,plain,
( ~ hskp30
| ~ c2_1(a1372)
| ~ hskp17
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f24711,f126]) ).
fof(f24833,plain,
( ~ hskp28
| ~ c2_1(a1328)
| ~ hskp17
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f24713,f118]) ).
fof(f25009,plain,
( ~ hskp28
| ~ hskp17
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f24833,f119]) ).
fof(f25019,plain,
( ~ hskp20
| hskp16
| ~ c2_1(a1348)
| ~ hskp28
| ~ hskp8 ),
inference(resolution,[status(thm)],[f25009,f476]) ).
fof(f25026,plain,
( ~ hskp20
| hskp16
| ~ hskp28
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f25019,f87]) ).
fof(f25027,plain,
! [X0] :
( ~ hskp9
| ~ hskp8
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1320) ),
inference(forward_subsumption_resolution,[status(thm)],[f6246,f42]) ).
fof(f25046,plain,
! [X0] :
( ~ hskp9
| ~ hskp8
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1320)
| ~ hskp9
| ~ hskp8
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1320) ),
inference(resolution,[status(thm)],[f25027,f22711]) ).
fof(f25144,plain,
! [X0] :
( ~ c2_1(X0)
| ~ hskp9
| ~ hskp8
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a1320) ),
inference(duplicate_literals_removal,[status(thm)],[f25046]) ).
fof(f25145,plain,
! [X0] :
( ~ c2_1(X0)
| ~ hskp9
| ~ hskp8
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f25144,f1898]) ).
fof(f25895,plain,
( ~ hskp28
| ~ c2_1(a1328)
| ~ hskp9
| ~ hskp8
| ~ c0_1(a1328) ),
inference(resolution,[status(thm)],[f25145,f120]) ).
fof(f26022,plain,
( ~ hskp28
| ~ c2_1(a1328)
| ~ hskp9
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f25895,f118]) ).
fof(f26198,plain,
( ~ hskp28
| ~ hskp9
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f26022,f119]) ).
fof(f26205,plain,
( ~ hskp9
| ~ hskp16
| ~ hskp2
| ~ hskp0
| ~ hskp28
| ~ hskp9 ),
inference(resolution,[status(thm)],[f26198,f10580]) ).
fof(f26213,plain,
( ~ hskp9
| ~ hskp7
| ~ hskp28
| ~ hskp9 ),
inference(resolution,[status(thm)],[f26198,f2420]) ).
fof(f26218,plain,
( ~ hskp9
| ~ hskp23
| ~ hskp28
| ~ hskp9 ),
inference(resolution,[status(thm)],[f26198,f2005]) ).
fof(f26224,plain,
( ~ hskp22
| hskp14
| ~ c1_1(a1356)
| ~ hskp28
| ~ hskp9 ),
inference(resolution,[status(thm)],[f26198,f993]) ).
fof(f26229,plain,
( ~ hskp14
| hskp7
| ~ c0_1(a1330)
| ~ hskp28
| ~ hskp9 ),
inference(resolution,[status(thm)],[f26198,f551]) ).
fof(f26234,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp0
| ~ hskp28
| ~ hskp9 ),
inference(duplicate_literals_removal,[status(thm)],[f26205]) ).
fof(f26235,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp0
| ~ hskp28 ),
inference(forward_subsumption_resolution,[status(thm)],[f26234,f9682]) ).
fof(f26241,plain,
( ~ hskp7
| ~ hskp28
| ~ hskp9 ),
inference(duplicate_literals_removal,[status(thm)],[f26213]) ).
fof(f26242,plain,
( ~ hskp23
| ~ hskp28
| ~ hskp9 ),
inference(duplicate_literals_removal,[status(thm)],[f26218]) ).
fof(f26243,plain,
( ~ hskp22
| hskp14
| ~ hskp28
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f26224,f95]) ).
fof(f26245,plain,
( ~ hskp14
| hskp7
| ~ hskp28
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f26229,f62]) ).
fof(f26335,plain,
( ~ hskp9
| hskp22
| ~ hskp28
| ~ hskp9 ),
inference(resolution,[status(thm)],[f26242,f1912]) ).
fof(f26340,plain,
( hskp22
| ~ hskp28
| ~ hskp9 ),
inference(duplicate_literals_removal,[status(thm)],[f26335]) ).
fof(f27060,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f26235,f9689]) ).
fof(f27086,plain,
( hskp14
| ~ hskp28
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f26243,f26340]) ).
fof(f27087,plain,
( ~ hskp28
| ~ hskp9 ),
inference(backward_subsumption_resolution,[status(thm)],[f27086,f27088]) ).
fof(f27088,plain,
( ~ hskp14
| ~ hskp28
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f26245,f26241]) ).
fof(f27316,plain,
( ~ c1_1(a1339)
| ~ hskp18
| ~ hskp9 ),
inference(backward_subsumption_resolution,[status(thm)],[f6127,f27087]) ).
fof(f27319,plain,
( ~ hskp16
| ~ hskp13
| ~ hskp5
| ~ hskp9 ),
inference(resolution,[status(thm)],[f27087,f21363]) ).
fof(f27352,plain,
( ~ hskp5
| ~ c1_1(a1314)
| ~ hskp9 ),
inference(resolution,[status(thm)],[f27087,f305]) ).
fof(f27355,plain,
( ~ hskp18
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f27316,f78]) ).
fof(f27356,plain,
( ~ hskp16
| ~ hskp13
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f27319,f21356]) ).
fof(f27372,plain,
( ~ hskp5
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f27352,f26]) ).
fof(f27379,plain,
( ~ hskp18
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f6063,f27355]) ).
fof(f27386,plain,
( ~ hskp11
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f4240,f27355]) ).
fof(f27405,plain,
( ~ hskp9
| hskp6
| ~ c2_1(a1320) ),
inference(backward_subsumption_resolution,[status(thm)],[f400,f27372]) ).
fof(f27410,plain,
( ~ hskp9
| hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f27405,f42]) ).
fof(f27457,plain,
( ~ hskp0
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f11355,f27386]) ).
fof(f27459,plain,
( ~ hskp23
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f3630,f27386]) ).
fof(f27477,plain,
! [X0] :
( hskp6
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f184,f27410]) ).
fof(f27479,plain,
( ~ hskp4
| hskp6
| ~ c2_1(a1312) ),
inference(backward_subsumption_resolution,[status(thm)],[f1148,f27410]) ).
fof(f27480,plain,
( ~ hskp15
| hskp6
| ~ c0_1(a1331) ),
inference(backward_subsumption_resolution,[status(thm)],[f1147,f27410]) ).
fof(f27657,plain,
( hskp0
| hskp6
| ~ hskp18 ),
inference(resolution,[status(thm)],[f27459,f204]) ).
fof(f27659,plain,
( hskp0
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f27657,f27379]) ).
fof(f27681,plain,
( hskp16
| hskp5 ),
inference(backward_subsumption_resolution,[status(thm)],[f203,f27684]) ).
fof(f27682,plain,
( hskp14
| hskp27 ),
inference(backward_subsumption_resolution,[status(thm)],[f190,f27684]) ).
fof(f27683,plain,
hskp20,
inference(backward_subsumption_resolution,[status(thm)],[f201,f27684]) ).
fof(f27684,plain,
~ hskp18,
inference(forward_subsumption_resolution,[status(thm)],[f27659,f27457]) ).
fof(f27688,plain,
( hskp16
| ~ hskp28
| ~ hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f25026,f27683]) ).
fof(f27708,plain,
( ~ hskp14
| hskp28
| ~ c3_1(a1330) ),
inference(backward_subsumption_resolution,[status(thm)],[f6293,f27683]) ).
fof(f27710,plain,
! [X0] :
( hskp28
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0)
| ~ c2_1(a1348) ),
inference(backward_subsumption_resolution,[status(thm)],[f6273,f27683]) ).
fof(f27715,plain,
( ~ hskp23
| hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f1883,f27683]) ).
fof(f27716,plain,
( hskp17
| hskp16
| ~ c2_1(a1348) ),
inference(backward_subsumption_resolution,[status(thm)],[f476,f27683]) ).
fof(f27718,plain,
c2_1(a1348),
inference(backward_subsumption_resolution,[status(thm)],[f87,f27683]) ).
fof(f27720,plain,
ndr1_0,
inference(backward_subsumption_resolution,[status(thm)],[f85,f27683]) ).
fof(f27723,plain,
! [X0] :
( hskp6
| ~ c2_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f27477,f27720]) ).
fof(f27726,plain,
! [X0,X1] :
( hskp5
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f235,f27720]) ).
fof(f27733,plain,
! [X0] :
( hskp11
| hskp22
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f189,f27720]) ).
fof(f27750,plain,
! [X0] :
( hskp2
| hskp22
| ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f173,f27720]) ).
fof(f27771,plain,
! [X0] :
( hskp13
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f187,f27720]) ).
fof(f27933,plain,
( ~ hskp2
| ~ hskp0
| hskp5 ),
inference(resolution,[status(thm)],[f27681,f27060]) ).
fof(f27945,plain,
( hskp0
| hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f204,f27715]) ).
fof(f28096,plain,
( ~ hskp2
| ~ hskp0
| ~ hskp28
| ~ hskp8 ),
inference(resolution,[status(thm)],[f27688,f27060]) ).
fof(f28097,plain,
( ~ hskp9
| ~ hskp2
| ~ hskp0 ),
inference(resolution,[status(thm)],[f27933,f27372]) ).
fof(f28189,plain,
( ~ hskp2
| ~ hskp9
| ~ c0_1(a1309) ),
inference(backward_subsumption_resolution,[status(thm)],[f6498,f28097]) ).
fof(f29364,plain,
( ~ hskp9
| ~ hskp14
| ~ c3_1(a1330) ),
inference(resolution,[status(thm)],[f27708,f27087]) ).
fof(f29367,plain,
( hskp17
| hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f27716,f27718]) ).
fof(f29605,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp2
| ~ hskp9 ),
inference(resolution,[status(thm)],[f28189,f3588]) ).
fof(f29643,plain,
( ~ hskp16
| ~ hskp2
| ~ hskp9 ),
inference(duplicate_literals_removal,[status(thm)],[f29605]) ).
fof(f29653,plain,
( hskp5
| ~ hskp2
| ~ hskp9 ),
inference(resolution,[status(thm)],[f29643,f27681]) ).
fof(f29657,plain,
( ~ hskp2
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f29653,f27372]) ).
fof(f29661,plain,
( ~ hskp9
| hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f1913,f29657]) ).
fof(f29666,plain,
( ~ hskp16
| ~ hskp7
| ~ hskp2 ),
inference(resolution,[status(thm)],[f29657,f3383]) ).
fof(f29735,plain,
( ~ hskp28
| ~ hskp8
| ~ hskp7
| ~ hskp2 ),
inference(resolution,[status(thm)],[f29666,f27688]) ).
fof(f29736,plain,
( hskp5
| ~ hskp7
| ~ hskp2 ),
inference(resolution,[status(thm)],[f29666,f27681]) ).
fof(f30018,plain,
( ~ hskp14
| hskp15
| ~ hskp9
| ~ hskp14 ),
inference(resolution,[status(thm)],[f29364,f6493]) ).
fof(f30092,plain,
( hskp15
| ~ hskp9
| ~ hskp14 ),
inference(duplicate_literals_removal,[status(thm)],[f30018]) ).
fof(f30453,plain,
( ~ hskp17
| ~ hskp7
| ~ hskp28
| ~ hskp7
| ~ hskp2 ),
inference(resolution,[status(thm)],[f29735,f2419]) ).
fof(f30471,plain,
( ~ hskp17
| ~ hskp28
| ~ hskp7
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f30453]) ).
fof(f30477,plain,
( hskp16
| ~ hskp28
| ~ hskp7
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30471,f29367]) ).
fof(f30484,plain,
( ~ hskp28
| ~ hskp7
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f30477,f29666]) ).
fof(f30495,plain,
( ~ hskp5
| ~ c1_1(a1314)
| ~ hskp7
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30484,f305]) ).
fof(f30505,plain,
( ~ hskp5
| ~ hskp7
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f30495,f26]) ).
fof(f30520,plain,
( ~ hskp2
| ~ hskp6
| ~ c3_1(a1309) ),
inference(backward_subsumption_resolution,[status(thm)],[f1451,f30521]) ).
fof(f30521,plain,
( ~ hskp7
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f30505,f29736]) ).
fof(f30529,plain,
( ~ hskp2
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f30520,f15]) ).
fof(f30532,plain,
( ~ hskp22
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f9638,f30529]) ).
fof(f30537,plain,
( ~ hskp15
| ~ c0_1(a1331)
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30529,f27480]) ).
fof(f30538,plain,
( ~ hskp4
| ~ c2_1(a1312)
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30529,f27479]) ).
fof(f30539,plain,
( ~ hskp23
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30529,f27715]) ).
fof(f30549,plain,
( ~ hskp3
| hskp22
| ~ c3_1(a1311)
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30539,f809]) ).
fof(f30551,plain,
( ~ hskp11
| hskp22
| ~ c2_1(a1324)
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30539,f806]) ).
fof(f30552,plain,
( ~ hskp3
| hskp22
| ~ c3_1(a1311) ),
inference(forward_subsumption_resolution,[status(thm)],[f30549,f790]) ).
fof(f30553,plain,
( ~ hskp11
| hskp22
| ~ c2_1(a1324) ),
inference(forward_subsumption_resolution,[status(thm)],[f30551,f787]) ).
fof(f30837,plain,
( ~ hskp15
| hskp28
| ~ hskp15
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30537,f271]) ).
fof(f30872,plain,
( hskp28
| ~ hskp15
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f30837]) ).
fof(f30892,plain,
( ~ hskp4
| hskp15
| ~ hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30538,f6696]) ).
fof(f30898,plain,
( ~ hskp4
| hskp7
| hskp8
| ~ hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30538,f554]) ).
fof(f30940,plain,
( hskp15
| ~ hskp4
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f30892]) ).
fof(f30947,plain,
( hskp7
| hskp8
| ~ hskp4
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f30898]) ).
fof(f30948,plain,
( hskp8
| ~ hskp4
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f30947,f30521]) ).
fof(f30952,plain,
( ~ hskp2
| ~ hskp0
| ~ hskp28
| ~ hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30948,f28096]) ).
fof(f30953,plain,
( ~ hskp0
| ~ hskp28
| ~ hskp4
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f30952]) ).
fof(f31076,plain,
( ~ hskp2
| ~ hskp3
| ~ c3_1(a1311) ),
inference(resolution,[status(thm)],[f30552,f30532]) ).
fof(f31079,plain,
( ~ hskp13
| ~ hskp5
| ~ hskp11
| ~ c2_1(a1324) ),
inference(resolution,[status(thm)],[f30553,f21286]) ).
fof(f31095,plain,
( ~ hskp15
| ~ hskp2
| ~ hskp0
| ~ hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f30953,f30872]) ).
fof(f31107,plain,
( ~ hskp15
| ~ hskp0
| ~ hskp4
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f31095]) ).
fof(f31108,plain,
( ~ hskp0
| ~ hskp4
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f31107,f30940]) ).
fof(f31168,plain,
( hskp6
| ~ c2_1(a1311)
| ~ c0_1(a1311)
| ~ hskp2
| ~ hskp3 ),
inference(resolution,[status(thm)],[f31076,f27723]) ).
fof(f31232,plain,
( hskp6
| ~ c2_1(a1311)
| ~ hskp2
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f31168,f18]) ).
fof(f33082,plain,
! [X0] :
( hskp28
| ~ c3_1(X0)
| ~ c0_1(X0)
| c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f27710,f27718]) ).
fof(f33776,plain,
( ~ hskp11
| hskp7
| hskp8
| ~ hskp13
| ~ hskp5
| ~ hskp11 ),
inference(resolution,[status(thm)],[f31079,f553]) ).
fof(f33814,plain,
( hskp7
| hskp8
| ~ hskp13
| ~ hskp5
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f33776]) ).
fof(f33916,plain,
( hskp6
| ~ hskp2
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f31232,f19]) ).
fof(f33917,plain,
( ~ hskp2
| ~ hskp2
| ~ hskp3 ),
inference(resolution,[status(thm)],[f33916,f30529]) ).
fof(f33918,plain,
( ~ hskp2
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f33917]) ).
fof(f33926,plain,
( hskp7
| hskp4
| ~ hskp2 ),
inference(resolution,[status(thm)],[f33918,f195]) ).
fof(f33928,plain,
( hskp4
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f33926,f30521]) ).
fof(f33939,plain,
( ~ hskp0
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f31108,f33928]) ).
fof(f33949,plain,
( hskp6
| ~ hskp2 ),
inference(resolution,[status(thm)],[f33939,f27945]) ).
fof(f33976,plain,
~ hskp2,
inference(forward_subsumption_resolution,[status(thm)],[f33949,f30529]) ).
fof(f33979,plain,
! [X0] :
( hskp22
| ~ c3_1(X0)
| ~ c2_1(X0)
| c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f27750,f33976]) ).
fof(f33980,plain,
( hskp9
| hskp30 ),
inference(backward_subsumption_resolution,[status(thm)],[f191,f33976]) ).
fof(f33981,plain,
hskp1,
inference(backward_subsumption_resolution,[status(thm)],[f1810,f33976]) ).
fof(f34025,plain,
! [X0,X1] :
( ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0)
| ~ c3_1(a1308) ),
inference(backward_subsumption_resolution,[status(thm)],[f7289,f33981]) ).
fof(f34054,plain,
c3_1(a1308),
inference(backward_subsumption_resolution,[status(thm)],[f10,f33981]) ).
fof(f34243,plain,
! [X0] :
( hskp11
| hskp22
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f27733,f33979]) ).
fof(f34330,plain,
! [X0] :
( ~ hskp13
| ~ hskp5
| hskp11
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(resolution,[status(thm)],[f34243,f21286]) ).
fof(f34510,plain,
! [X0,X1] :
( hskp5
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f27726,f34511]) ).
fof(f34511,plain,
! [X0,X1] :
( ~ c2_1(X1)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(X0)
| c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f34025,f34054]) ).
fof(f34585,plain,
! [X0] :
( ~ hskp15
| hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(a1331)
| ~ c1_1(a1331) ),
inference(resolution,[status(thm)],[f34510,f68]) ).
fof(f34598,plain,
! [X0] :
( ~ hskp15
| hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ c2_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f34585,f66]) ).
fof(f35564,plain,
! [X0] :
( ~ hskp15
| hskp5
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f34598,f67]) ).
fof(f35565,plain,
! [X0] :
( ~ hskp9
| ~ hskp15
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f35564,f27372]) ).
fof(f35623,plain,
( ~ hskp22
| ~ hskp9
| ~ hskp15
| ~ c0_1(a1356) ),
inference(resolution,[status(thm)],[f35565,f95]) ).
fof(f35683,plain,
( ~ hskp22
| ~ hskp9
| ~ hskp15 ),
inference(forward_subsumption_resolution,[status(thm)],[f35623,f94]) ).
fof(f35821,plain,
( ~ hskp9
| ~ hskp14 ),
inference(backward_subsumption_resolution,[status(thm)],[f30092,f35822]) ).
fof(f35822,plain,
( ~ hskp9
| ~ hskp15 ),
inference(forward_subsumption_resolution,[status(thm)],[f35683,f29661]) ).
fof(f35835,plain,
( ~ hskp8
| hskp14
| ~ c2_1(a1319)
| ~ hskp9 ),
inference(resolution,[status(thm)],[f35822,f458]) ).
fof(f35839,plain,
( ~ hskp8
| hskp14
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f35835,f38]) ).
fof(f35985,plain,
( ~ hskp9
| ~ hskp7 ),
inference(backward_subsumption_resolution,[status(thm)],[f2420,f35986]) ).
fof(f35986,plain,
( ~ hskp8
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f35839,f35821]) ).
fof(f35999,plain,
( ~ hskp22
| hskp14
| ~ c1_1(a1356)
| ~ hskp9 ),
inference(resolution,[status(thm)],[f35986,f993]) ).
fof(f36005,plain,
( ~ hskp22
| hskp14
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f35999,f95]) ).
fof(f36013,plain,
( ~ hskp16
| ~ hskp7 ),
inference(backward_subsumption_resolution,[status(thm)],[f3383,f35985]) ).
fof(f36018,plain,
( ~ hskp28
| ~ hskp8
| ~ hskp7 ),
inference(resolution,[status(thm)],[f36013,f27688]) ).
fof(f36019,plain,
( hskp5
| ~ hskp7 ),
inference(resolution,[status(thm)],[f36013,f27681]) ).
fof(f36026,plain,
~ hskp9,
inference(backward_subsumption_resolution,[status(thm)],[f29661,f36027]) ).
fof(f36027,plain,
( ~ hskp22
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f36005,f35821]) ).
fof(f36034,plain,
hskp30,
inference(backward_subsumption_resolution,[status(thm)],[f33980,f36026]) ).
fof(f36037,plain,
( ~ hskp16
| ~ hskp13
| c0_1(a1326) ),
inference(backward_subsumption_resolution,[status(thm)],[f3384,f36026]) ).
fof(f36038,plain,
( ~ hskp16
| c0_1(a1333) ),
inference(backward_subsumption_resolution,[status(thm)],[f3377,f36026]) ).
fof(f36043,plain,
( ~ c2_1(a1372)
| ~ hskp17
| ~ hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f24831,f36034]) ).
fof(f36044,plain,
c3_1(a1372),
inference(backward_subsumption_resolution,[status(thm)],[f128,f36034]) ).
fof(f36045,plain,
c1_1(a1372),
inference(backward_subsumption_resolution,[status(thm)],[f127,f36034]) ).
fof(f36046,plain,
c0_1(a1372),
inference(backward_subsumption_resolution,[status(thm)],[f126,f36034]) ).
fof(f36069,plain,
( ~ hskp17
| ~ hskp7
| ~ hskp28
| ~ hskp7 ),
inference(resolution,[status(thm)],[f36018,f2419]) ).
fof(f36080,plain,
( ~ hskp17
| ~ hskp28
| ~ hskp7 ),
inference(duplicate_literals_removal,[status(thm)],[f36069]) ).
fof(f36135,plain,
( ~ hskp16
| ~ hskp13
| ~ hskp15
| c0_1(a1331) ),
inference(backward_subsumption_resolution,[status(thm)],[f16502,f36038]) ).
fof(f36142,plain,
( ~ hskp16
| hskp27 ),
inference(backward_subsumption_resolution,[status(thm)],[f7662,f36038]) ).
fof(f36145,plain,
( ~ hskp16
| hskp8
| hskp14 ),
inference(backward_subsumption_resolution,[status(thm)],[f994,f36038]) ).
fof(f36147,plain,
( hskp16
| ~ hskp28
| ~ hskp7 ),
inference(resolution,[status(thm)],[f36080,f29367]) ).
fof(f36151,plain,
( ~ hskp28
| ~ hskp7 ),
inference(forward_subsumption_resolution,[status(thm)],[f36147,f36013]) ).
fof(f36159,plain,
( ~ hskp5
| ~ c1_1(a1314)
| ~ hskp7 ),
inference(resolution,[status(thm)],[f36151,f305]) ).
fof(f36163,plain,
( ~ hskp5
| ~ hskp7 ),
inference(forward_subsumption_resolution,[status(thm)],[f36159,f26]) ).
fof(f36206,plain,
( hskp8
| ~ hskp13
| ~ hskp5
| ~ hskp11 ),
inference(backward_subsumption_resolution,[status(thm)],[f33814,f36221]) ).
fof(f36216,plain,
( ~ hskp14
| hskp8
| ~ c0_1(a1330) ),
inference(backward_subsumption_resolution,[status(thm)],[f551,f36221]) ).
fof(f36221,plain,
~ hskp7,
inference(forward_subsumption_resolution,[status(thm)],[f36163,f36019]) ).
fof(f36223,plain,
( ~ hskp14
| hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f36216,f62]) ).
fof(f36243,plain,
( ~ hskp16
| hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f36145,f36223]) ).
fof(f36478,plain,
( hskp28
| ~ c3_1(a1372)
| ~ c0_1(a1372)
| ~ hskp17
| ~ hskp8 ),
inference(resolution,[status(thm)],[f36043,f33082]) ).
fof(f36496,plain,
( hskp28
| ~ c3_1(a1372)
| ~ hskp17
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f36478,f36046]) ).
fof(f37168,plain,
( ~ hskp17
| ~ hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f25009,f37169]) ).
fof(f37169,plain,
( hskp28
| ~ hskp17
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f36496,f36044]) ).
fof(f37172,plain,
( hskp16
| ~ hskp8 ),
inference(resolution,[status(thm)],[f37168,f29367]) ).
fof(f37175,plain,
( ~ hskp26
| hskp4
| ~ c0_1(a1411)
| ~ hskp8 ),
inference(resolution,[status(thm)],[f37168,f877]) ).
fof(f37177,plain,
( ~ hskp26
| hskp4
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f37175,f110]) ).
fof(f37178,plain,
( ~ hskp13
| ~ hskp5
| ~ hskp8 ),
inference(resolution,[status(thm)],[f37172,f27356]) ).
fof(f37261,plain,
( ~ hskp13
| ~ hskp5
| ~ hskp11 ),
inference(backward_subsumption_resolution,[status(thm)],[f36206,f37178]) ).
fof(f39996,plain,
! [X0] :
( ~ hskp13
| ~ hskp5
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f34330,f37261]) ).
fof(f40023,plain,
( ~ hskp17
| ~ hskp13
| ~ hskp5
| ~ c2_1(a1334) ),
inference(resolution,[status(thm)],[f39996,f75]) ).
fof(f40095,plain,
! [X0] :
( ~ hskp13
| ~ hskp5
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp13
| ~ hskp5
| ~ c2_1(X0) ),
inference(resolution,[status(thm)],[f39996,f20715]) ).
fof(f40118,plain,
( ~ hskp17
| ~ hskp13
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f40023,f74]) ).
fof(f40153,plain,
! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp13
| ~ hskp5
| ~ c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f40095]) ).
fof(f40154,plain,
! [X0] :
( ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp5
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f40153,f27771]) ).
fof(f40206,plain,
( hskp16
| ~ hskp13
| ~ hskp5 ),
inference(resolution,[status(thm)],[f40118,f29367]) ).
fof(f40209,plain,
( hskp16
| ~ hskp13 ),
inference(forward_subsumption_resolution,[status(thm)],[f40206,f27681]) ).
fof(f40211,plain,
( ~ hskp13
| ~ hskp15
| c0_1(a1331) ),
inference(backward_subsumption_resolution,[status(thm)],[f36135,f40209]) ).
fof(f40212,plain,
( ~ hskp13
| c0_1(a1326) ),
inference(backward_subsumption_resolution,[status(thm)],[f36037,f40209]) ).
fof(f40238,plain,
( ~ hskp13
| hskp14
| ~ c0_1(a1331) ),
inference(backward_subsumption_resolution,[status(thm)],[f6737,f40212]) ).
fof(f40242,plain,
( ~ hskp13
| hskp15 ),
inference(backward_subsumption_resolution,[status(thm)],[f6552,f40212]) ).
fof(f40417,plain,
( ~ hskp13
| c0_1(a1331) ),
inference(forward_subsumption_resolution,[status(thm)],[f40211,f40242]) ).
fof(f40540,plain,
( ~ hskp16
| hskp14
| ~ c1_1(a1333) ),
inference(backward_subsumption_resolution,[status(thm)],[f937,f40542]) ).
fof(f40542,plain,
( ~ hskp13
| hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f40238,f40417]) ).
fof(f40543,plain,
( ~ hskp16
| hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f40540,f70]) ).
fof(f41214,plain,
( ~ hskp27
| ~ c0_1(a1307)
| ~ hskp5
| ~ c2_1(a1307) ),
inference(resolution,[status(thm)],[f40154,f115]) ).
fof(f41266,plain,
( ~ hskp27
| ~ c0_1(a1307)
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f41214,f116]) ).
fof(f41354,plain,
( ~ hskp27
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f41266,f114]) ).
fof(f41356,plain,
! [X0] :
( ~ hskp15
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp27 ),
inference(resolution,[status(thm)],[f41354,f35564]) ).
fof(f41408,plain,
( ~ hskp15
| ~ c0_1(a1372)
| ~ hskp27 ),
inference(resolution,[status(thm)],[f41356,f36045]) ).
fof(f41461,plain,
( ~ hskp15
| ~ hskp27 ),
inference(forward_subsumption_resolution,[status(thm)],[f41408,f36046]) ).
fof(f41504,plain,
( ~ hskp4
| ~ hskp14
| ~ c0_1(a1312)
| ~ hskp27 ),
inference(resolution,[status(thm)],[f41461,f6502]) ).
fof(f41510,plain,
( ~ hskp4
| ~ hskp14
| ~ hskp27 ),
inference(forward_subsumption_resolution,[status(thm)],[f41504,f22]) ).
fof(f41713,plain,
( ~ hskp16
| ~ hskp4
| ~ hskp14 ),
inference(resolution,[status(thm)],[f41510,f36142]) ).
fof(f41723,plain,
( ~ hskp16
| ~ hskp4 ),
inference(forward_subsumption_resolution,[status(thm)],[f41713,f40543]) ).
fof(f41828,plain,
( ~ hskp8
| ~ hskp4 ),
inference(resolution,[status(thm)],[f41723,f37172]) ).
fof(f41870,plain,
( ~ hskp26
| ~ hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f37177,f41828]) ).
fof(f41871,plain,
( ~ hskp12
| ~ hskp8
| ~ c3_1(a1325) ),
inference(backward_subsumption_resolution,[status(thm)],[f5808,f41828]) ).
fof(f41883,plain,
( ~ hskp12
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f41871,f55]) ).
fof(f41903,plain,
( hskp12
| ~ hskp8 ),
inference(resolution,[status(thm)],[f41870,f200]) ).
fof(f41953,plain,
~ hskp16,
inference(backward_subsumption_resolution,[status(thm)],[f36243,f41956]) ).
fof(f41954,plain,
~ hskp14,
inference(backward_subsumption_resolution,[status(thm)],[f36223,f41956]) ).
fof(f41956,plain,
~ hskp8,
inference(forward_subsumption_resolution,[status(thm)],[f41903,f41883]) ).
fof(f41959,plain,
hskp5,
inference(backward_subsumption_resolution,[status(thm)],[f27681,f41953]) ).
fof(f41968,plain,
hskp27,
inference(backward_subsumption_resolution,[status(thm)],[f27682,f41954]) ).
fof(f42080,plain,
~ hskp27,
inference(backward_subsumption_resolution,[status(thm)],[f41354,f41959]) ).
fof(f42128,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f42080,f41968]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN478+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n008.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 11:01:38 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.50 % Drodi V4.1.1
% 80.74/10.83 % Refutation found
% 80.74/10.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 80.74/10.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 80.74/10.89 % Elapsed time: 10.413092 seconds
% 80.74/10.89 % CPU time: 81.673565 seconds
% 80.74/10.89 % Total memory used: 77.603 MB
% 80.74/10.89 % Net memory used: 73.065 MB
%------------------------------------------------------------------------------