Drodi-SAT---4.1.1.THM-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : SYN485+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n015.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:19:47 PM UTC 2026

% Result   : Theorem 114.23s 16.07s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05  % Problem  : SYN485+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.07  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.49  % Computer : n015.cluster.edu
% 0.18/0.49  % Model    : x86_64 x86_64
% 0.18/0.49  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.49  % Memory   : 8046.5625MB
% 0.18/0.49  % OS       : Linux 6.8.0-71-generic
% 0.18/0.49  % CPULimit : 300
% 0.18/0.49  % WCLimit  : 300
% 0.18/0.49  % DateTime : Mon Sep 21 11:04:52 UTC 2026
% 0.18/0.49  % CPUTime  : 
% 0.22/0.54  % Drodi V4.1.1
% 114.23/16.07  % Refutation found
% 114.23/16.07  % SZS status Theorem for theBenchmark: Theorem is valid
% 114.23/16.07  % SZS output start CNFRefutation for theBenchmark
% 114.23/16.07  fof(f1,conjecture,(
% 114.23/16.07    ~ ( ( ~ hskp0| ( ndr1_0& c3_1(a2068)& ~ c0_1(a2068)& ~ c2_1(a2068) ) )& ( ~ hskp1| ( ndr1_0& c0_1(a2070)& c3_1(a2070)& ~ c2_1(a2070) ) )& ( ~ hskp2| ( ndr1_0& c0_1(a2071)& c2_1(a2071)& ~ c3_1(a2071) ) )& ( ~ hskp3| ( ndr1_0& ~ c0_1(a2072)& ~ c1_1(a2072)& ~ c3_1(a2072) ) )& ( ~ hskp4| ( ndr1_0& c1_1(a2074)& c3_1(a2074)& ~ c2_1(a2074) ) )& ( ~ hskp5| ( ndr1_0& c1_1(a2076)& c3_1(a2076)& ~ c0_1(a2076) ) )& ( ~ hskp6| ( ndr1_0& c0_1(a2078)& ~ c1_1(a2078)& ~ c2_1(a2078) ) )& ( ~ hskp7| ( ndr1_0& c0_1(a2079)& c1_1(a2079)& ~ c3_1(a2079) ) )& ( ~ hskp8| ( ndr1_0& c1_1(a2082)& c2_1(a2082)& ~ c0_1(a2082) ) )& ( ~ hskp9| ( ndr1_0& c2_1(a2084)& c3_1(a2084)& ~ c1_1(a2084) ) )& ( ~ hskp10| ( ndr1_0& c2_1(a2087)& ~ c1_1(a2087)& ~ c3_1(a2087) ) )& ( ~ hskp11| ( ndr1_0& c0_1(a2093)& ~ c1_1(a2093)& ~ c3_1(a2093) ) )& ( ~ hskp12| ( ndr1_0& c1_1(a2095)& ~ c0_1(a2095)& ~ c2_1(a2095) ) )& ( ~ hskp13| ( ndr1_0& c2_1(a2096)& ~ c0_1(a2096)& ~ c1_1(a2096) ) )& ( ~ hskp14| ( ndr1_0& ~ c0_1(a2097)& ~ c1_1(a2097)& ~ c2_1(a2097) ) )& ( ~ hskp15| ( ndr1_0& c0_1(a2099)& ~ c2_1(a2099)& ~ c3_1(a2099) ) )& ( ~ hskp16| ( ndr1_0& c3_1(a2104)& ~ c0_1(a2104)& ~ c1_1(a2104) ) )& ( ~ hskp17| ( ndr1_0& c0_1(a2110)& c2_1(a2110)& ~ c1_1(a2110) ) )& ( ~ hskp18| ( ndr1_0& c1_1(a2116)& ~ c2_1(a2116)& ~ c3_1(a2116) ) )& ( ~ hskp19| ( ndr1_0& c2_1(a2122)& ~ c0_1(a2122)& ~ c3_1(a2122) ) )& ( ~ hskp20| ( ndr1_0& ~ c1_1(a2130)& ~ c2_1(a2130)& ~ c3_1(a2130) ) )& ( ~ hskp21| ( ndr1_0& c0_1(a2136)& c1_1(a2136)& ~ c2_1(a2136) ) )& ( ~ hskp22| ( ndr1_0& c2_1(a2140)& c3_1(a2140)& ~ c0_1(a2140) ) )& ( ~ hskp23| ( ndr1_0& c0_1(a2149)& c3_1(a2149)& ~ c1_1(a2149) ) )& ( ~ hskp24| ( ndr1_0& c1_1(a2160)& c2_1(a2160)& ~ c3_1(a2160) ) )& ( ~ hskp25| ( ndr1_0& c1_1(a2172)& ~ c0_1(a2172)& ~ c3_1(a2172) ) )& ( ~ hskp26| ( ndr1_0& c0_1(a2069)& c2_1(a2069)& c3_1(a2069) ) )& ( ~ hskp27| ( ndr1_0& c0_1(a2073)& c1_1(a2073)& c3_1(a2073) ) )& ( ~ hskp28| ( ndr1_0& c0_1(a2075)& c1_1(a2075)& c2_1(a2075) ) )& ( ~ hskp29| ( ndr1_0& c1_1(a2077)& c2_1(a2077)& c3_1(a2077) ) )& ( (! [U] :( ndr1_0=> ( c0_1(U)| c1_1(U)| c2_1(U) ) ))| (! [V] :( ndr1_0=> ( c0_1(V)| c2_1(V)| ~ c1_1(V) ) ))| (! [W] :( ndr1_0=> ( c1_1(W)| c2_1(W)| c3_1(W) ) ) ))& ( (! [X] :( ndr1_0=> ( c0_1(X)| c1_1(X)| c2_1(X) ) ))| (! [Y] :( ndr1_0=> ( ~ c0_1(Y)| ~ c2_1(Y)| ~ c3_1(Y) ) ))| hskp0 )& ( (! [Z] :( ndr1_0=> ( c0_1(Z)| c1_1(Z)| c2_1(Z) ) ))| hskp26| hskp1 )& ( (! [X1] :( ndr1_0=> ( c0_1(X1)| c1_1(X1)| c2_1(X1) ) ))| hskp2| hskp3 )& ( (! [X2] :( ndr1_0=> ( c0_1(X2)| c1_1(X2)| c3_1(X2) ) ))| (! [X3] :( ndr1_0=> ( c0_1(X3)| c1_1(X3)| ~ c2_1(X3) ) ))| hskp27 )& ( (! [X4] :( ndr1_0=> ( c0_1(X4)| c1_1(X4)| c3_1(X4) ) ))| (! [X5] :( ndr1_0=> ( c1_1(X5)| c3_1(X5)| ~ c2_1(X5) ) ))| hskp4 )& ( (! [X6] :( ndr1_0=> ( c0_1(X6)| c1_1(X6)| c3_1(X6) ) ))| hskp28| hskp5 )& ( (! [X7] :( ndr1_0=> ( c0_1(X7)| c1_1(X7)| ~ c2_1(X7) ) ))| (! [X8] :( ndr1_0=> ( c0_1(X8)| ~ c2_1(X8)| ~ c3_1(X8) ) ))| (! [X9] :( ndr1_0=> ( c1_1(X9)| ~ c0_1(X9)| ~ c2_1(X9) ) ) ))& ( (! [X10] :( ndr1_0=> ( c0_1(X10)| c1_1(X10)| ~ c2_1(X10) ) ))| (! [X11] :( ndr1_0=> ( c2_1(X11)| ~ c0_1(X11)| ~ c1_1(X11) ) ))| hskp29 )& ( (! [X12] :( ndr1_0=> ( c0_1(X12)| c1_1(X12)| ~ c3_1(X12) ) ))| (! [X13] :( ndr1_0=> ( c1_1(X13)| ~ c0_1(X13)| ~ c3_1(X13) ) ))| hskp6 )& ( (! [X14] :( ndr1_0=> ( c0_1(X14)| c1_1(X14)| ~ c3_1(X14) ) ))| (! [X15] :( ndr1_0=> ( c1_1(X15)| ~ c2_1(X15)| ~ c3_1(X15) ) ))| (! [X16] :( ndr1_0=> ( c2_1(X16)| c3_1(X16)| ~ c1_1(X16) ) ) ))& ( (! [X17] :( ndr1_0=> ( c0_1(X17)| c1_1(X17)| ~ c3_1(X17) ) ))| (! [X18] :( ndr1_0=> ( ~ c0_1(X18)| ~ c1_1(X18)| ~ c3_1(X18) ) ))| hskp7 )& ( (! [X19] :( ndr1_0=> ( c0_1(X19)| c2_1(X19)| c3_1(X19) ) ))| (! [X20] :( ndr1_0=> ( c1_1(X20)| c3_1(X20)| ~ c2_1(X20) ) ))| (! [X21] :( ndr1_0=> ( c2_1(X21)| ~ c1_1(X21)| ~ c3_1(X21) ) ) ))& ( (! [X22] :( ndr1_0=> ( c0_1(X22)| c2_1(X22)| c3_1(X22) ) ))| hskp5| hskp4 )& ( (! [X23] :( ndr1_0=> ( c0_1(X23)| c2_1(X23)| ~ c1_1(X23) ) ))| (! [X24] :( ndr1_0=> ( c1_1(X24)| c3_1(X24)| ~ c2_1(X24) ) ))| hskp8 )& ( (! [X25] :( ndr1_0=> ( c0_1(X25)| c2_1(X25)| ~ c1_1(X25) ) ))| (! [X26] :( ndr1_0=> ( c1_1(X26)| ~ c0_1(X26)| ~ c3_1(X26) ) ))| hskp2 )& ( (! [X27] :( ndr1_0=> ( c0_1(X27)| c2_1(X27)| ~ c1_1(X27) ) ))| (! [X28] :( ndr1_0=> ( c2_1(X28)| ~ c0_1(X28)| ~ c1_1(X28) ) ))| hskp9 )& ( (! [X29] :( ndr1_0=> ( c0_1(X29)| c2_1(X29)| ~ c1_1(X29) ) ))| (! [X30] :( ndr1_0=> ( c2_1(X30)| ~ c0_1(X30)| ~ c3_1(X30) ) ))| hskp9 )& ( (! [X31] :( ndr1_0=> ( c0_1(X31)| c2_1(X31)| ~ c3_1(X31) ) ))| (! [X32] :( ndr1_0=> ( c0_1(X32)| c3_1(X32)| ~ c1_1(X32) ) ))| (! [X33] :( ndr1_0=> ( c2_1(X33)| c3_1(X33)| ~ c1_1(X33) ) ) ))& ( (! [X34] :( ndr1_0=> ( c0_1(X34)| c2_1(X34)| ~ c3_1(X34) ) ))| (! [X35] :( ndr1_0=> ( c1_1(X35)| c2_1(X35)| ~ c3_1(X35) ) ))| hskp4 )& ( (! [X36] :( ndr1_0=> ( c0_1(X36)| c2_1(X36)| ~ c3_1(X36) ) ))| (! [X37] :( ndr1_0=> ( ~ c0_1(X37)| ~ c2_1(X37)| ~ c3_1(X37) ) ))| hskp10 )& ( (! [X38] :( ndr1_0=> ( c0_1(X38)| c2_1(X38)| ~ c3_1(X38) ) ))| hskp27| hskp7 )& ( (! [X39] :( ndr1_0=> ( c0_1(X39)| c3_1(X39)| ~ c1_1(X39) ) ))| (! [X40] :( ndr1_0=> ( ~ c0_1(X40)| ~ c2_1(X40)| ~ c3_1(X40) ) ))| hskp4 )& ( (! [X41] :( ndr1_0=> ( c0_1(X41)| c3_1(X41)| ~ c1_1(X41) ) ))| (! [X42] :( ndr1_0=> ( ~ c1_1(X42)| ~ c2_1(X42)| ~ c3_1(X42) ) ))| hskp8 )& ( (! [X43] :( ndr1_0=> ( c0_1(X43)| c3_1(X43)| ~ c2_1(X43) ) ))| (! [X44] :( ndr1_0=> ( c0_1(X44)| ~ c1_1(X44)| ~ c2_1(X44) ) ))| hskp1 )& ( (! [X45] :( ndr1_0=> ( c0_1(X45)| c3_1(X45)| ~ c2_1(X45) ) ))| (! [X46] :( ndr1_0=> ( c1_1(X46)| c2_1(X46)| ~ c0_1(X46) ) ))| hskp11 )& ( (! [X47] :( ndr1_0=> ( c0_1(X47)| c3_1(X47)| ~ c2_1(X47) ) ))| (! [X48] :( ndr1_0=> ( c1_1(X48)| ~ c2_1(X48)| ~ c3_1(X48) ) ))| hskp10 )& ( (! [X49] :( ndr1_0=> ( c0_1(X49)| c3_1(X49)| ~ c2_1(X49) ) ))| (! [X50] :( ndr1_0=> ( c2_1(X50)| ~ c0_1(X50)| ~ c3_1(X50) ) ))| (! [X51] :( ndr1_0=> ( c2_1(X51)| ~ c1_1(X51)| ~ c3_1(X51) ) ) ))& ( (! [X52] :( ndr1_0=> ( c0_1(X52)| c3_1(X52)| ~ c2_1(X52) ) ))| hskp12| hskp13 )& ( (! [X53] :( ndr1_0=> ( c0_1(X53)| ~ c1_1(X53)| ~ c2_1(X53) ) ))| (! [X54] :( ndr1_0=> ( c1_1(X54)| c2_1(X54)| c3_1(X54) ) ))| hskp14 )& ( (! [X55] :( ndr1_0=> ( c0_1(X55)| ~ c1_1(X55)| ~ c2_1(X55) ) ))| (! [X56] :( ndr1_0=> ( c1_1(X56)| c3_1(X56)| ~ c2_1(X56) ) ))| hskp11 )& ( (! [X57] :( ndr1_0=> ( c0_1(X57)| ~ c1_1(X57)| ~ c3_1(X57) ) ))| (! [X58] :( ndr1_0=> ( c1_1(X58)| c2_1(X58)| ~ c3_1(X58) ) ))| hskp15 )& ( (! [X59] :( ndr1_0=> ( c0_1(X59)| ~ c1_1(X59)| ~ c3_1(X59) ) ))| (! [X60] :( ndr1_0=> ( c1_1(X60)| ~ c0_1(X60)| ~ c3_1(X60) ) ))| (! [X61] :( ndr1_0=> ( c2_1(X61)| ~ c0_1(X61)| ~ c1_1(X61) ) ) ))& ( (! [X62] :( ndr1_0=> ( c0_1(X62)| ~ c1_1(X62)| ~ c3_1(X62) ) ))| hskp28| hskp4 )& ( (! [X63] :( ndr1_0=> ( c0_1(X63)| ~ c1_1(X63)| ~ c3_1(X63) ) ))| hskp0 )& ( (! [X64] :( ndr1_0=> ( c0_1(X64)| ~ c2_1(X64)| ~ c3_1(X64) ) ))| (! [X65] :( ndr1_0=> ( c1_1(X65)| ~ c2_1(X65)| ~ c3_1(X65) ) ))| hskp27 )& ( (! [X66] :( ndr1_0=> ( c0_1(X66)| ~ c2_1(X66)| ~ c3_1(X66) ) ))| (! [X67] :( ndr1_0=> ( c2_1(X67)| c3_1(X67)| ~ c0_1(X67) ) ))| hskp16 )& ( (! [X68] :( ndr1_0=> ( c0_1(X68)| ~ c2_1(X68)| ~ c3_1(X68) ) ))| (! [X69] :( ndr1_0=> ( ~ c0_1(X69)| ~ c1_1(X69)| ~ c2_1(X69) ) ))| hskp26 )& ( (! [X70] :( ndr1_0=> ( c0_1(X70)| ~ c2_1(X70)| ~ c3_1(X70) ) ))| hskp27| hskp29 )& ( (! [X71] :( ndr1_0=> ( c0_1(X71)| ~ c2_1(X71)| ~ c3_1(X71) ) ))| hskp11| hskp0 )& ( (! [X72] :( ndr1_0=> ( c1_1(X72)| c2_1(X72)| c3_1(X72) ) ))| hskp17| hskp1 )& ( (! [X73] :( ndr1_0=> ( c1_1(X73)| c2_1(X73)| ~ c0_1(X73) ) ))| (! [X74] :( ndr1_0=> ( ~ c0_1(X74)| ~ c2_1(X74)| ~ c3_1(X74) ) ))| hskp26 )& ( (! [X75] :( ndr1_0=> ( c1_1(X75)| c2_1(X75)| ~ c3_1(X75) ) ))| (! [X76] :( ndr1_0=> ( c3_1(X76)| ~ c0_1(X76)| ~ c2_1(X76) ) ))| hskp16 )& ( (! [X77] :( ndr1_0=> ( c1_1(X77)| c2_1(X77)| ~ c3_1(X77) ) ))| (! [X78] :( ndr1_0=> ( ~ c1_1(X78)| ~ c2_1(X78)| ~ c3_1(X78) ) ))| hskp8 )& ( (! [X79] :( ndr1_0=> ( c1_1(X79)| c2_1(X79)| ~ c3_1(X79) ) ))| hskp26| hskp18 )& ( (! [X80] :( ndr1_0=> ( c1_1(X80)| c3_1(X80)| ~ c0_1(X80) ) ))| (! [X81] :( ndr1_0=> ( c1_1(X81)| ~ c2_1(X81)| ~ c3_1(X81) ) ))| hskp26 )& ( (! [X82] :( ndr1_0=> ( c1_1(X82)| c3_1(X82)| ~ c0_1(X82) ) ))| (! [X83] :( ndr1_0=> ( c2_1(X83)| ~ c1_1(X83)| ~ c3_1(X83) ) ))| hskp3 )& ( (! [X84] :( ndr1_0=> ( c1_1(X84)| c3_1(X84)| ~ c0_1(X84) ) ))| (! [X85] :( ndr1_0=> ( ~ c0_1(X85)| ~ c1_1(X85)| ~ c3_1(X85) ) ))| (! [X86] :( ndr1_0=> ( ~ c0_1(X86)| ~ c2_1(X86)| ~ c3_1(X86) ) ) ))& ( (! [X87] :( ndr1_0=> ( c1_1(X87)| c3_1(X87)| ~ c0_1(X87) ) ))| hskp1| hskp8 )& ( (! [X88] :( ndr1_0=> ( c1_1(X88)| c3_1(X88)| ~ c0_1(X88) ) ))| hskp11| hskp19 )& ( (! [X89] :( ndr1_0=> ( c1_1(X89)| ~ c0_1(X89)| ~ c3_1(X89) ) ))| (! [X90] :( ndr1_0=> ( c2_1(X90)| c3_1(X90)| ~ c1_1(X90) ) ))| hskp17 )& ( (! [X91] :( ndr1_0=> ( c1_1(X91)| ~ c0_1(X91)| ~ c3_1(X91) ) ))| (! [X92] :( ndr1_0=> ( c2_1(X92)| c3_1(X92)| ~ c1_1(X92) ) ))| hskp8 )& ( (! [X93] :( ndr1_0=> ( c1_1(X93)| ~ c0_1(X93)| ~ c3_1(X93) ) ))| hskp26| hskp5 )& ( (! [X94] :( ndr1_0=> ( c1_1(X94)| ~ c0_1(X94)| ~ c3_1(X94) ) ))| hskp11| hskp10 )& ( (! [X95] :( ndr1_0=> ( c1_1(X95)| ~ c2_1(X95)| ~ c3_1(X95) ) ))| (! [X96] :( ndr1_0=> ( c2_1(X96)| ~ c0_1(X96)| ~ c3_1(X96) ) ))| hskp3 )& ( (! [X97] :( ndr1_0=> ( c1_1(X97)| ~ c2_1(X97)| ~ c3_1(X97) ) ))| (! [X98] :( ndr1_0=> ( ~ c0_1(X98)| ~ c1_1(X98)| ~ c2_1(X98) ) ))| hskp20 )& ( (! [X99] :( ndr1_0=> ( c1_1(X99)| ~ c2_1(X99)| ~ c3_1(X99) ) ))| hskp7| hskp15 )& ( (! [X100] :( ndr1_0=> ( c2_1(X100)| c3_1(X100)| ~ c0_1(X100) ) ))| (! [X101] :( ndr1_0=> ( ~ c0_1(X101)| ~ c1_1(X101)| ~ c2_1(X101) ) ))| hskp11 )& ( (! [X102] :( ndr1_0=> ( c2_1(X102)| ~ c0_1(X102)| ~ c1_1(X102) ) ))| (! [X103] :( ndr1_0=> ( c2_1(X103)| ~ c1_1(X103)| ~ c3_1(X103) ) ))| hskp5 )& ( (! [X104] :( ndr1_0=> ( c2_1(X104)| ~ c0_1(X104)| ~ c1_1(X104) ) ))| (! [X105] :( ndr1_0=> ( c3_1(X105)| ~ c1_1(X105)| ~ c2_1(X105) ) ))| hskp12 )& ( (! [X106] :( ndr1_0=> ( c2_1(X106)| ~ c0_1(X106)| ~ c1_1(X106) ) ))| hskp21| hskp16 )& ( (! [X107] :( ndr1_0=> ( c2_1(X107)| ~ c0_1(X107)| ~ c1_1(X107) ) ))| hskp17| hskp20 )& ( (! [X108] :( ndr1_0=> ( c2_1(X108)| ~ c0_1(X108)| ~ c1_1(X108) ) ))| hskp22 )& ( (! [X109] :( ndr1_0=> ( c2_1(X109)| ~ c0_1(X109)| ~ c3_1(X109) ) ))| (! [X110] :( ndr1_0=> ( c3_1(X110)| ~ c0_1(X110)| ~ c2_1(X110) ) ))| hskp4 )& ( (! [X111] :( ndr1_0=> ( c2_1(X111)| ~ c0_1(X111)| ~ c3_1(X111) ) ))| hskp7| hskp16 )& ( (! [X112] :( ndr1_0=> ( ~ c0_1(X112)| ~ c1_1(X112)| ~ c2_1(X112) ) ))| hskp7| hskp4 )& ( (! [X113] :( ndr1_0=> ( ~ c0_1(X113)| ~ c1_1(X113)| ~ c3_1(X113) ) ))| hskp17| hskp22 )& ( hskp27| hskp23| hskp5 )& ( hskp7| hskp23| hskp15 )& ( hskp17| hskp2 )& ( hskp17| hskp23| hskp1 )& ( hskp23| hskp24| hskp5 )& ( hskp6| hskp5| hskp18 )& ( hskp29| hskp5| hskp3 )& ( hskp24| hskp12| hskp10 )& ( hskp12| hskp25| hskp18 ) ) ),
% 114.23/16.07    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 114.23/16.07  fof(f2,negated_conjecture,(
% 114.23/16.07    ~(~ ( ( ~ hskp0| ( ndr1_0& c3_1(a2068)& ~ c0_1(a2068)& ~ c2_1(a2068) ) )& ( ~ hskp1| ( ndr1_0& c0_1(a2070)& c3_1(a2070)& ~ c2_1(a2070) ) )& ( ~ hskp2| ( ndr1_0& c0_1(a2071)& c2_1(a2071)& ~ c3_1(a2071) ) )& ( ~ hskp3| ( ndr1_0& ~ c0_1(a2072)& ~ c1_1(a2072)& ~ c3_1(a2072) ) )& ( ~ hskp4| ( ndr1_0& c1_1(a2074)& c3_1(a2074)& ~ c2_1(a2074) ) )& ( ~ hskp5| ( ndr1_0& c1_1(a2076)& c3_1(a2076)& ~ c0_1(a2076) ) )& ( ~ hskp6| ( ndr1_0& c0_1(a2078)& ~ c1_1(a2078)& ~ c2_1(a2078) ) )& ( ~ hskp7| ( ndr1_0& c0_1(a2079)& c1_1(a2079)& ~ c3_1(a2079) ) )& ( ~ hskp8| ( ndr1_0& c1_1(a2082)& c2_1(a2082)& ~ c0_1(a2082) ) )& ( ~ hskp9| ( ndr1_0& c2_1(a2084)& c3_1(a2084)& ~ c1_1(a2084) ) )& ( ~ hskp10| ( ndr1_0& c2_1(a2087)& ~ c1_1(a2087)& ~ c3_1(a2087) ) )& ( ~ hskp11| ( ndr1_0& c0_1(a2093)& ~ c1_1(a2093)& ~ c3_1(a2093) ) )& ( ~ hskp12| ( ndr1_0& c1_1(a2095)& ~ c0_1(a2095)& ~ c2_1(a2095) ) )& ( ~ hskp13| ( ndr1_0& c2_1(a2096)& ~ c0_1(a2096)& ~ c1_1(a2096) ) )& ( ~ hskp14| ( ndr1_0& ~ c0_1(a2097)& ~ c1_1(a2097)& ~ c2_1(a2097) ) )& ( ~ hskp15| ( ndr1_0& c0_1(a2099)& ~ c2_1(a2099)& ~ c3_1(a2099) ) )& ( ~ hskp16| ( ndr1_0& c3_1(a2104)& ~ c0_1(a2104)& ~ c1_1(a2104) ) )& ( ~ hskp17| ( ndr1_0& c0_1(a2110)& c2_1(a2110)& ~ c1_1(a2110) ) )& ( ~ hskp18| ( ndr1_0& c1_1(a2116)& ~ c2_1(a2116)& ~ c3_1(a2116) ) )& ( ~ hskp19| ( ndr1_0& c2_1(a2122)& ~ c0_1(a2122)& ~ c3_1(a2122) ) )& ( ~ hskp20| ( ndr1_0& ~ c1_1(a2130)& ~ c2_1(a2130)& ~ c3_1(a2130) ) )& ( ~ hskp21| ( ndr1_0& c0_1(a2136)& c1_1(a2136)& ~ c2_1(a2136) ) )& ( ~ hskp22| ( ndr1_0& c2_1(a2140)& c3_1(a2140)& ~ c0_1(a2140) ) )& ( ~ hskp23| ( ndr1_0& c0_1(a2149)& c3_1(a2149)& ~ c1_1(a2149) ) )& ( ~ hskp24| ( ndr1_0& c1_1(a2160)& c2_1(a2160)& ~ c3_1(a2160) ) )& ( ~ hskp25| ( ndr1_0& c1_1(a2172)& ~ c0_1(a2172)& ~ c3_1(a2172) ) )& ( ~ hskp26| ( ndr1_0& c0_1(a2069)& c2_1(a2069)& c3_1(a2069) ) )& ( ~ hskp27| ( ndr1_0& c0_1(a2073)& c1_1(a2073)& c3_1(a2073) ) )& ( ~ hskp28| ( ndr1_0& c0_1(a2075)& c1_1(a2075)& c2_1(a2075) ) )& ( ~ hskp29| ( ndr1_0& c1_1(a2077)& c2_1(a2077)& c3_1(a2077) ) )& ( (! [U] :( ndr1_0=> ( c0_1(U)| c1_1(U)| c2_1(U) ) ))| (! [V] :( ndr1_0=> ( c0_1(V)| c2_1(V)| ~ c1_1(V) ) ))| (! [W] :( ndr1_0=> ( c1_1(W)| c2_1(W)| c3_1(W) ) ) ))& ( (! [X] :( ndr1_0=> ( c0_1(X)| c1_1(X)| c2_1(X) ) ))| (! [Y] :( ndr1_0=> ( ~ c0_1(Y)| ~ c2_1(Y)| ~ c3_1(Y) ) ))| hskp0 )& ( (! [Z] :( ndr1_0=> ( c0_1(Z)| c1_1(Z)| c2_1(Z) ) ))| hskp26| hskp1 )& ( (! [X1] :( ndr1_0=> ( c0_1(X1)| c1_1(X1)| c2_1(X1) ) ))| hskp2| hskp3 )& ( (! [X2] :( ndr1_0=> ( c0_1(X2)| c1_1(X2)| c3_1(X2) ) ))| (! [X3] :( ndr1_0=> ( c0_1(X3)| c1_1(X3)| ~ c2_1(X3) ) ))| hskp27 )& ( (! [X4] :( ndr1_0=> ( c0_1(X4)| c1_1(X4)| c3_1(X4) ) ))| (! [X5] :( ndr1_0=> ( c1_1(X5)| c3_1(X5)| ~ c2_1(X5) ) ))| hskp4 )& ( (! [X6] :( ndr1_0=> ( c0_1(X6)| c1_1(X6)| c3_1(X6) ) ))| hskp28| hskp5 )& ( (! [X7] :( ndr1_0=> ( c0_1(X7)| c1_1(X7)| ~ c2_1(X7) ) ))| (! [X8] :( ndr1_0=> ( c0_1(X8)| ~ c2_1(X8)| ~ c3_1(X8) ) ))| (! [X9] :( ndr1_0=> ( c1_1(X9)| ~ c0_1(X9)| ~ c2_1(X9) ) ) ))& ( (! [X10] :( ndr1_0=> ( c0_1(X10)| c1_1(X10)| ~ c2_1(X10) ) ))| (! [X11] :( ndr1_0=> ( c2_1(X11)| ~ c0_1(X11)| ~ c1_1(X11) ) ))| hskp29 )& ( (! [X12] :( ndr1_0=> ( c0_1(X12)| c1_1(X12)| ~ c3_1(X12) ) ))| (! [X13] :( ndr1_0=> ( c1_1(X13)| ~ c0_1(X13)| ~ c3_1(X13) ) ))| hskp6 )& ( (! [X14] :( ndr1_0=> ( c0_1(X14)| c1_1(X14)| ~ c3_1(X14) ) ))| (! [X15] :( ndr1_0=> ( c1_1(X15)| ~ c2_1(X15)| ~ c3_1(X15) ) ))| (! [X16] :( ndr1_0=> ( c2_1(X16)| c3_1(X16)| ~ c1_1(X16) ) ) ))& ( (! [X17] :( ndr1_0=> ( c0_1(X17)| c1_1(X17)| ~ c3_1(X17) ) ))| (! [X18] :( ndr1_0=> ( ~ c0_1(X18)| ~ c1_1(X18)| ~ c3_1(X18) ) ))| hskp7 )& ( (! [X19] :( ndr1_0=> ( c0_1(X19)| c2_1(X19)| c3_1(X19) ) ))| (! [X20] :( ndr1_0=> ( c1_1(X20)| c3_1(X20)| ~ c2_1(X20) ) ))| (! [X21] :( ndr1_0=> ( c2_1(X21)| ~ c1_1(X21)| ~ c3_1(X21) ) ) ))& ( (! [X22] :( ndr1_0=> ( c0_1(X22)| c2_1(X22)| c3_1(X22) ) ))| hskp5| hskp4 )& ( (! [X23] :( ndr1_0=> ( c0_1(X23)| c2_1(X23)| ~ c1_1(X23) ) ))| (! [X24] :( ndr1_0=> ( c1_1(X24)| c3_1(X24)| ~ c2_1(X24) ) ))| hskp8 )& ( (! [X25] :( ndr1_0=> ( c0_1(X25)| c2_1(X25)| ~ c1_1(X25) ) ))| (! [X26] :( ndr1_0=> ( c1_1(X26)| ~ c0_1(X26)| ~ c3_1(X26) ) ))| hskp2 )& ( (! [X27] :( ndr1_0=> ( c0_1(X27)| c2_1(X27)| ~ c1_1(X27) ) ))| (! [X28] :( ndr1_0=> ( c2_1(X28)| ~ c0_1(X28)| ~ c1_1(X28) ) ))| hskp9 )& ( (! [X29] :( ndr1_0=> ( c0_1(X29)| c2_1(X29)| ~ c1_1(X29) ) ))| (! [X30] :( ndr1_0=> ( c2_1(X30)| ~ c0_1(X30)| ~ c3_1(X30) ) ))| hskp9 )& ( (! [X31] :( ndr1_0=> ( c0_1(X31)| c2_1(X31)| ~ c3_1(X31) ) ))| (! [X32] :( ndr1_0=> ( c0_1(X32)| c3_1(X32)| ~ c1_1(X32) ) ))| (! [X33] :( ndr1_0=> ( c2_1(X33)| c3_1(X33)| ~ c1_1(X33) ) ) ))& ( (! [X34] :( ndr1_0=> ( c0_1(X34)| c2_1(X34)| ~ c3_1(X34) ) ))| (! [X35] :( ndr1_0=> ( c1_1(X35)| c2_1(X35)| ~ c3_1(X35) ) ))| hskp4 )& ( (! [X36] :( ndr1_0=> ( c0_1(X36)| c2_1(X36)| ~ c3_1(X36) ) ))| (! [X37] :( ndr1_0=> ( ~ c0_1(X37)| ~ c2_1(X37)| ~ c3_1(X37) ) ))| hskp10 )& ( (! [X38] :( ndr1_0=> ( c0_1(X38)| c2_1(X38)| ~ c3_1(X38) ) ))| hskp27| hskp7 )& ( (! [X39] :( ndr1_0=> ( c0_1(X39)| c3_1(X39)| ~ c1_1(X39) ) ))| (! [X40] :( ndr1_0=> ( ~ c0_1(X40)| ~ c2_1(X40)| ~ c3_1(X40) ) ))| hskp4 )& ( (! [X41] :( ndr1_0=> ( c0_1(X41)| c3_1(X41)| ~ c1_1(X41) ) ))| (! [X42] :( ndr1_0=> ( ~ c1_1(X42)| ~ c2_1(X42)| ~ c3_1(X42) ) ))| hskp8 )& ( (! [X43] :( ndr1_0=> ( c0_1(X43)| c3_1(X43)| ~ c2_1(X43) ) ))| (! [X44] :( ndr1_0=> ( c0_1(X44)| ~ c1_1(X44)| ~ c2_1(X44) ) ))| hskp1 )& ( (! [X45] :( ndr1_0=> ( c0_1(X45)| c3_1(X45)| ~ c2_1(X45) ) ))| (! [X46] :( ndr1_0=> ( c1_1(X46)| c2_1(X46)| ~ c0_1(X46) ) ))| hskp11 )& ( (! [X47] :( ndr1_0=> ( c0_1(X47)| c3_1(X47)| ~ c2_1(X47) ) ))| (! [X48] :( ndr1_0=> ( c1_1(X48)| ~ c2_1(X48)| ~ c3_1(X48) ) ))| hskp10 )& ( (! [X49] :( ndr1_0=> ( c0_1(X49)| c3_1(X49)| ~ c2_1(X49) ) ))| (! [X50] :( ndr1_0=> ( c2_1(X50)| ~ c0_1(X50)| ~ c3_1(X50) ) ))| (! [X51] :( ndr1_0=> ( c2_1(X51)| ~ c1_1(X51)| ~ c3_1(X51) ) ) ))& ( (! [X52] :( ndr1_0=> ( c0_1(X52)| c3_1(X52)| ~ c2_1(X52) ) ))| hskp12| hskp13 )& ( (! [X53] :( ndr1_0=> ( c0_1(X53)| ~ c1_1(X53)| ~ c2_1(X53) ) ))| (! [X54] :( ndr1_0=> ( c1_1(X54)| c2_1(X54)| c3_1(X54) ) ))| hskp14 )& ( (! [X55] :( ndr1_0=> ( c0_1(X55)| ~ c1_1(X55)| ~ c2_1(X55) ) ))| (! [X56] :( ndr1_0=> ( c1_1(X56)| c3_1(X56)| ~ c2_1(X56) ) ))| hskp11 )& ( (! [X57] :( ndr1_0=> ( c0_1(X57)| ~ c1_1(X57)| ~ c3_1(X57) ) ))| (! [X58] :( ndr1_0=> ( c1_1(X58)| c2_1(X58)| ~ c3_1(X58) ) ))| hskp15 )& ( (! [X59] :( ndr1_0=> ( c0_1(X59)| ~ c1_1(X59)| ~ c3_1(X59) ) ))| (! [X60] :( ndr1_0=> ( c1_1(X60)| ~ c0_1(X60)| ~ c3_1(X60) ) ))| (! [X61] :( ndr1_0=> ( c2_1(X61)| ~ c0_1(X61)| ~ c1_1(X61) ) ) ))& ( (! [X62] :( ndr1_0=> ( c0_1(X62)| ~ c1_1(X62)| ~ c3_1(X62) ) ))| hskp28| hskp4 )& ( (! [X63] :( ndr1_0=> ( c0_1(X63)| ~ c1_1(X63)| ~ c3_1(X63) ) ))| hskp0 )& ( (! [X64] :( ndr1_0=> ( c0_1(X64)| ~ c2_1(X64)| ~ c3_1(X64) ) ))| (! [X65] :( ndr1_0=> ( c1_1(X65)| ~ c2_1(X65)| ~ c3_1(X65) ) ))| hskp27 )& ( (! [X66] :( ndr1_0=> ( c0_1(X66)| ~ c2_1(X66)| ~ c3_1(X66) ) ))| (! [X67] :( ndr1_0=> ( c2_1(X67)| c3_1(X67)| ~ c0_1(X67) ) ))| hskp16 )& ( (! [X68] :( ndr1_0=> ( c0_1(X68)| ~ c2_1(X68)| ~ c3_1(X68) ) ))| (! [X69] :( ndr1_0=> ( ~ c0_1(X69)| ~ c1_1(X69)| ~ c2_1(X69) ) ))| hskp26 )& ( (! [X70] :( ndr1_0=> ( c0_1(X70)| ~ c2_1(X70)| ~ c3_1(X70) ) ))| hskp27| hskp29 )& ( (! [X71] :( ndr1_0=> ( c0_1(X71)| ~ c2_1(X71)| ~ c3_1(X71) ) ))| hskp11| hskp0 )& ( (! [X72] :( ndr1_0=> ( c1_1(X72)| c2_1(X72)| c3_1(X72) ) ))| hskp17| hskp1 )& ( (! [X73] :( ndr1_0=> ( c1_1(X73)| c2_1(X73)| ~ c0_1(X73) ) ))| (! [X74] :( ndr1_0=> ( ~ c0_1(X74)| ~ c2_1(X74)| ~ c3_1(X74) ) ))| hskp26 )& ( (! [X75] :( ndr1_0=> ( c1_1(X75)| c2_1(X75)| ~ c3_1(X75) ) ))| (! [X76] :( ndr1_0=> ( c3_1(X76)| ~ c0_1(X76)| ~ c2_1(X76) ) ))| hskp16 )& ( (! [X77] :( ndr1_0=> ( c1_1(X77)| c2_1(X77)| ~ c3_1(X77) ) ))| (! [X78] :( ndr1_0=> ( ~ c1_1(X78)| ~ c2_1(X78)| ~ c3_1(X78) ) ))| hskp8 )& ( (! [X79] :( ndr1_0=> ( c1_1(X79)| c2_1(X79)| ~ c3_1(X79) ) ))| hskp26| hskp18 )& ( (! [X80] :( ndr1_0=> ( c1_1(X80)| c3_1(X80)| ~ c0_1(X80) ) ))| (! [X81] :( ndr1_0=> ( c1_1(X81)| ~ c2_1(X81)| ~ c3_1(X81) ) ))| hskp26 )& ( (! [X82] :( ndr1_0=> ( c1_1(X82)| c3_1(X82)| ~ c0_1(X82) ) ))| (! [X83] :( ndr1_0=> ( c2_1(X83)| ~ c1_1(X83)| ~ c3_1(X83) ) ))| hskp3 )& ( (! [X84] :( ndr1_0=> ( c1_1(X84)| c3_1(X84)| ~ c0_1(X84) ) ))| (! [X85] :( ndr1_0=> ( ~ c0_1(X85)| ~ c1_1(X85)| ~ c3_1(X85) ) ))| (! [X86] :( ndr1_0=> ( ~ c0_1(X86)| ~ c2_1(X86)| ~ c3_1(X86) ) ) ))& ( (! [X87] :( ndr1_0=> ( c1_1(X87)| c3_1(X87)| ~ c0_1(X87) ) ))| hskp1| hskp8 )& ( (! [X88] :( ndr1_0=> ( c1_1(X88)| c3_1(X88)| ~ c0_1(X88) ) ))| hskp11| hskp19 )& ( (! [X89] :( ndr1_0=> ( c1_1(X89)| ~ c0_1(X89)| ~ c3_1(X89) ) ))| (! [X90] :( ndr1_0=> ( c2_1(X90)| c3_1(X90)| ~ c1_1(X90) ) ))| hskp17 )& ( (! [X91] :( ndr1_0=> ( c1_1(X91)| ~ c0_1(X91)| ~ c3_1(X91) ) ))| (! [X92] :( ndr1_0=> ( c2_1(X92)| c3_1(X92)| ~ c1_1(X92) ) ))| hskp8 )& ( (! [X93] :( ndr1_0=> ( c1_1(X93)| ~ c0_1(X93)| ~ c3_1(X93) ) ))| hskp26| hskp5 )& ( (! [X94] :( ndr1_0=> ( c1_1(X94)| ~ c0_1(X94)| ~ c3_1(X94) ) ))| hskp11| hskp10 )& ( (! [X95] :( ndr1_0=> ( c1_1(X95)| ~ c2_1(X95)| ~ c3_1(X95) ) ))| (! [X96] :( ndr1_0=> ( c2_1(X96)| ~ c0_1(X96)| ~ c3_1(X96) ) ))| hskp3 )& ( (! [X97] :( ndr1_0=> ( c1_1(X97)| ~ c2_1(X97)| ~ c3_1(X97) ) ))| (! [X98] :( ndr1_0=> ( ~ c0_1(X98)| ~ c1_1(X98)| ~ c2_1(X98) ) ))| hskp20 )& ( (! [X99] :( ndr1_0=> ( c1_1(X99)| ~ c2_1(X99)| ~ c3_1(X99) ) ))| hskp7| hskp15 )& ( (! [X100] :( ndr1_0=> ( c2_1(X100)| c3_1(X100)| ~ c0_1(X100) ) ))| (! [X101] :( ndr1_0=> ( ~ c0_1(X101)| ~ c1_1(X101)| ~ c2_1(X101) ) ))| hskp11 )& ( (! [X102] :( ndr1_0=> ( c2_1(X102)| ~ c0_1(X102)| ~ c1_1(X102) ) ))| (! [X103] :( ndr1_0=> ( c2_1(X103)| ~ c1_1(X103)| ~ c3_1(X103) ) ))| hskp5 )& ( (! [X104] :( ndr1_0=> ( c2_1(X104)| ~ c0_1(X104)| ~ c1_1(X104) ) ))| (! [X105] :( ndr1_0=> ( c3_1(X105)| ~ c1_1(X105)| ~ c2_1(X105) ) ))| hskp12 )& ( (! [X106] :( ndr1_0=> ( c2_1(X106)| ~ c0_1(X106)| ~ c1_1(X106) ) ))| hskp21| hskp16 )& ( (! [X107] :( ndr1_0=> ( c2_1(X107)| ~ c0_1(X107)| ~ c1_1(X107) ) ))| hskp17| hskp20 )& ( (! [X108] :( ndr1_0=> ( c2_1(X108)| ~ c0_1(X108)| ~ c1_1(X108) ) ))| hskp22 )& ( (! [X109] :( ndr1_0=> ( c2_1(X109)| ~ c0_1(X109)| ~ c3_1(X109) ) ))| (! [X110] :( ndr1_0=> ( c3_1(X110)| ~ c0_1(X110)| ~ c2_1(X110) ) ))| hskp4 )& ( (! [X111] :( ndr1_0=> ( c2_1(X111)| ~ c0_1(X111)| ~ c3_1(X111) ) ))| hskp7| hskp16 )& ( (! [X112] :( ndr1_0=> ( ~ c0_1(X112)| ~ c1_1(X112)| ~ c2_1(X112) ) ))| hskp7| hskp4 )& ( (! [X113] :( ndr1_0=> ( ~ c0_1(X113)| ~ c1_1(X113)| ~ c3_1(X113) ) ))| hskp17| hskp22 )& ( hskp27| hskp23| hskp5 )& ( hskp7| hskp23| hskp15 )& ( hskp17| hskp2 )& ( hskp17| hskp23| hskp1 )& ( hskp23| hskp24| hskp5 )& ( hskp6| hskp5| hskp18 )& ( hskp29| hskp5| hskp3 )& ( hskp24| hskp12| hskp10 )& ( hskp12| hskp25| hskp18 ) ) )),
% 114.23/16.07    inference(negated_conjecture,[status(cth)],[f1])).
% 114.23/16.07  fof(f3,plain,(
% 114.23/16.07    (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0|(((ndr1_0&c3_1(a2068))&~c0_1(a2068))&~c2_1(a2068)))&(~hskp1|(((ndr1_0&c0_1(a2070))&c3_1(a2070))&~c2_1(a2070))))&(~hskp2|(((ndr1_0&c0_1(a2071))&c2_1(a2071))&~c3_1(a2071))))&(~hskp3|(((ndr1_0&~c0_1(a2072))&~c1_1(a2072))&~c3_1(a2072))))&(~hskp4|(((ndr1_0&c1_1(a2074))&c3_1(a2074))&~c2_1(a2074))))&(~hskp5|(((ndr1_0&c1_1(a2076))&c3_1(a2076))&~c0_1(a2076))))&(~hskp6|(((ndr1_0&c0_1(a2078))&~c1_1(a2078))&~c2_1(a2078))))&(~hskp7|(((ndr1_0&c0_1(a2079))&c1_1(a2079))&~c3_1(a2079))))&(~hskp8|(((ndr1_0&c1_1(a2082))&c2_1(a2082))&~c0_1(a2082))))&(~hskp9|(((ndr1_0&c2_1(a2084))&c3_1(a2084))&~c1_1(a2084))))&(~hskp10|(((ndr1_0&c2_1(a2087))&~c1_1(a2087))&~c3_1(a2087))))&(~hskp11|(((ndr1_0&c0_1(a2093))&~c1_1(a2093))&~c3_1(a2093))))&(~hskp12|(((ndr1_0&c1_1(a2095))&~c0_1(a2095))&~c2_1(a2095))))&(~hskp13|(((ndr1_0&c2_1(a2096))&~c0_1(a2096))&~c1_1(a2096))))&(~hskp14|(((ndr1_0&~c0_1(a2097))&~c1_1(a2097))&~c2_1(a2097))))&(~hskp15|(((ndr1_0&c0_1(a2099))&~c2_1(a2099))&~c3_1(a2099))))&(~hskp16|(((ndr1_0&c3_1(a2104))&~c0_1(a2104))&~c1_1(a2104))))&(~hskp17|(((ndr1_0&c0_1(a2110))&c2_1(a2110))&~c1_1(a2110))))&(~hskp18|(((ndr1_0&c1_1(a2116))&~c2_1(a2116))&~c3_1(a2116))))&(~hskp19|(((ndr1_0&c2_1(a2122))&~c0_1(a2122))&~c3_1(a2122))))&(~hskp20|(((ndr1_0&~c1_1(a2130))&~c2_1(a2130))&~c3_1(a2130))))&(~hskp21|(((ndr1_0&c0_1(a2136))&c1_1(a2136))&~c2_1(a2136))))&(~hskp22|(((ndr1_0&c2_1(a2140))&c3_1(a2140))&~c0_1(a2140))))&(~hskp23|(((ndr1_0&c0_1(a2149))&c3_1(a2149))&~c1_1(a2149))))&(~hskp24|(((ndr1_0&c1_1(a2160))&c2_1(a2160))&~c3_1(a2160))))&(~hskp25|(((ndr1_0&c1_1(a2172))&~c0_1(a2172))&~c3_1(a2172))))&(~hskp26|(((ndr1_0&c0_1(a2069))&c2_1(a2069))&c3_1(a2069))))&(~hskp27|(((ndr1_0&c0_1(a2073))&c1_1(a2073))&c3_1(a2073))))&(~hskp28|(((ndr1_0&c0_1(a2075))&c1_1(a2075))&c2_1(a2075))))&(~hskp29|(((ndr1_0&c1_1(a2077))&c2_1(a2077))&c3_1(a2077))))&(((![U]: (~ndr1_0|((c0_1(U)|c1_1(U))|c2_1(U))))|(![V]: (~ndr1_0|((c0_1(V)|c2_1(V))|~c1_1(V)))))|(![W]: (~ndr1_0|((c1_1(W)|c2_1(W))|c3_1(W))))))&(((![X]: (~ndr1_0|((c0_1(X)|c1_1(X))|c2_1(X))))|(![Y]: (~ndr1_0|((~c0_1(Y)|~c2_1(Y))|~c3_1(Y)))))|hskp0))&(((![Z]: (~ndr1_0|((c0_1(Z)|c1_1(Z))|c2_1(Z))))|hskp26)|hskp1))&(((![X1]: (~ndr1_0|((c0_1(X1)|c1_1(X1))|c2_1(X1))))|hskp2)|hskp3))&(((![X2]: (~ndr1_0|((c0_1(X2)|c1_1(X2))|c3_1(X2))))|(![X3]: (~ndr1_0|((c0_1(X3)|c1_1(X3))|~c2_1(X3)))))|hskp27))&(((![X4]: (~ndr1_0|((c0_1(X4)|c1_1(X4))|c3_1(X4))))|(![X5]: (~ndr1_0|((c1_1(X5)|c3_1(X5))|~c2_1(X5)))))|hskp4))&(((![X6]: (~ndr1_0|((c0_1(X6)|c1_1(X6))|c3_1(X6))))|hskp28)|hskp5))&(((![X7]: (~ndr1_0|((c0_1(X7)|c1_1(X7))|~c2_1(X7))))|(![X8]: (~ndr1_0|((c0_1(X8)|~c2_1(X8))|~c3_1(X8)))))|(![X9]: (~ndr1_0|((c1_1(X9)|~c0_1(X9))|~c2_1(X9))))))&(((![X10]: (~ndr1_0|((c0_1(X10)|c1_1(X10))|~c2_1(X10))))|(![X11]: (~ndr1_0|((c2_1(X11)|~c0_1(X11))|~c1_1(X11)))))|hskp29))&(((![X12]: (~ndr1_0|((c0_1(X12)|c1_1(X12))|~c3_1(X12))))|(![X13]: (~ndr1_0|((c1_1(X13)|~c0_1(X13))|~c3_1(X13)))))|hskp6))&(((![X14]: (~ndr1_0|((c0_1(X14)|c1_1(X14))|~c3_1(X14))))|(![X15]: (~ndr1_0|((c1_1(X15)|~c2_1(X15))|~c3_1(X15)))))|(![X16]: (~ndr1_0|((c2_1(X16)|c3_1(X16))|~c1_1(X16))))))&(((![X17]: (~ndr1_0|((c0_1(X17)|c1_1(X17))|~c3_1(X17))))|(![X18]: (~ndr1_0|((~c0_1(X18)|~c1_1(X18))|~c3_1(X18)))))|hskp7))&(((![X19]: (~ndr1_0|((c0_1(X19)|c2_1(X19))|c3_1(X19))))|(![X20]: (~ndr1_0|((c1_1(X20)|c3_1(X20))|~c2_1(X20)))))|(![X21]: (~ndr1_0|((c2_1(X21)|~c1_1(X21))|~c3_1(X21))))))&(((![X22]: (~ndr1_0|((c0_1(X22)|c2_1(X22))|c3_1(X22))))|hskp5)|hskp4))&(((![X23]: (~ndr1_0|((c0_1(X23)|c2_1(X23))|~c1_1(X23))))|(![X24]: (~ndr1_0|((c1_1(X24)|c3_1(X24))|~c2_1(X24)))))|hskp8))&(((![X25]: (~ndr1_0|((c0_1(X25)|c2_1(X25))|~c1_1(X25))))|(![X26]: (~ndr1_0|((c1_1(X26)|~c0_1(X26))|~c3_1(X26)))))|hskp2))&(((![X27]: (~ndr1_0|((c0_1(X27)|c2_1(X27))|~c1_1(X27))))|(![X28]: (~ndr1_0|((c2_1(X28)|~c0_1(X28))|~c1_1(X28)))))|hskp9))&(((![X29]: (~ndr1_0|((c0_1(X29)|c2_1(X29))|~c1_1(X29))))|(![X30]: (~ndr1_0|((c2_1(X30)|~c0_1(X30))|~c3_1(X30)))))|hskp9))&(((![X31]: (~ndr1_0|((c0_1(X31)|c2_1(X31))|~c3_1(X31))))|(![X32]: (~ndr1_0|((c0_1(X32)|c3_1(X32))|~c1_1(X32)))))|(![X33]: (~ndr1_0|((c2_1(X33)|c3_1(X33))|~c1_1(X33))))))&(((![X34]: (~ndr1_0|((c0_1(X34)|c2_1(X34))|~c3_1(X34))))|(![X35]: (~ndr1_0|((c1_1(X35)|c2_1(X35))|~c3_1(X35)))))|hskp4))&(((![X36]: (~ndr1_0|((c0_1(X36)|c2_1(X36))|~c3_1(X36))))|(![X37]: (~ndr1_0|((~c0_1(X37)|~c2_1(X37))|~c3_1(X37)))))|hskp10))&(((![X38]: (~ndr1_0|((c0_1(X38)|c2_1(X38))|~c3_1(X38))))|hskp27)|hskp7))&(((![X39]: (~ndr1_0|((c0_1(X39)|c3_1(X39))|~c1_1(X39))))|(![X40]: (~ndr1_0|((~c0_1(X40)|~c2_1(X40))|~c3_1(X40)))))|hskp4))&(((![X41]: (~ndr1_0|((c0_1(X41)|c3_1(X41))|~c1_1(X41))))|(![X42]: (~ndr1_0|((~c1_1(X42)|~c2_1(X42))|~c3_1(X42)))))|hskp8))&(((![X43]: (~ndr1_0|((c0_1(X43)|c3_1(X43))|~c2_1(X43))))|(![X44]: (~ndr1_0|((c0_1(X44)|~c1_1(X44))|~c2_1(X44)))))|hskp1))&(((![X45]: (~ndr1_0|((c0_1(X45)|c3_1(X45))|~c2_1(X45))))|(![X46]: (~ndr1_0|((c1_1(X46)|c2_1(X46))|~c0_1(X46)))))|hskp11))&(((![X47]: (~ndr1_0|((c0_1(X47)|c3_1(X47))|~c2_1(X47))))|(![X48]: (~ndr1_0|((c1_1(X48)|~c2_1(X48))|~c3_1(X48)))))|hskp10))&(((![X49]: (~ndr1_0|((c0_1(X49)|c3_1(X49))|~c2_1(X49))))|(![X50]: (~ndr1_0|((c2_1(X50)|~c0_1(X50))|~c3_1(X50)))))|(![X51]: (~ndr1_0|((c2_1(X51)|~c1_1(X51))|~c3_1(X51))))))&(((![X52]: (~ndr1_0|((c0_1(X52)|c3_1(X52))|~c2_1(X52))))|hskp12)|hskp13))&(((![X53]: (~ndr1_0|((c0_1(X53)|~c1_1(X53))|~c2_1(X53))))|(![X54]: (~ndr1_0|((c1_1(X54)|c2_1(X54))|c3_1(X54)))))|hskp14))&(((![X55]: (~ndr1_0|((c0_1(X55)|~c1_1(X55))|~c2_1(X55))))|(![X56]: (~ndr1_0|((c1_1(X56)|c3_1(X56))|~c2_1(X56)))))|hskp11))&(((![X57]: (~ndr1_0|((c0_1(X57)|~c1_1(X57))|~c3_1(X57))))|(![X58]: (~ndr1_0|((c1_1(X58)|c2_1(X58))|~c3_1(X58)))))|hskp15))&(((![X59]: (~ndr1_0|((c0_1(X59)|~c1_1(X59))|~c3_1(X59))))|(![X60]: (~ndr1_0|((c1_1(X60)|~c0_1(X60))|~c3_1(X60)))))|(![X61]: (~ndr1_0|((c2_1(X61)|~c0_1(X61))|~c1_1(X61))))))&(((![X62]: (~ndr1_0|((c0_1(X62)|~c1_1(X62))|~c3_1(X62))))|hskp28)|hskp4))&((![X63]: (~ndr1_0|((c0_1(X63)|~c1_1(X63))|~c3_1(X63))))|hskp0))&(((![X64]: (~ndr1_0|((c0_1(X64)|~c2_1(X64))|~c3_1(X64))))|(![X65]: (~ndr1_0|((c1_1(X65)|~c2_1(X65))|~c3_1(X65)))))|hskp27))&(((![X66]: (~ndr1_0|((c0_1(X66)|~c2_1(X66))|~c3_1(X66))))|(![X67]: (~ndr1_0|((c2_1(X67)|c3_1(X67))|~c0_1(X67)))))|hskp16))&(((![X68]: (~ndr1_0|((c0_1(X68)|~c2_1(X68))|~c3_1(X68))))|(![X69]: (~ndr1_0|((~c0_1(X69)|~c1_1(X69))|~c2_1(X69)))))|hskp26))&(((![X70]: (~ndr1_0|((c0_1(X70)|~c2_1(X70))|~c3_1(X70))))|hskp27)|hskp29))&(((![X71]: (~ndr1_0|((c0_1(X71)|~c2_1(X71))|~c3_1(X71))))|hskp11)|hskp0))&(((![X72]: (~ndr1_0|((c1_1(X72)|c2_1(X72))|c3_1(X72))))|hskp17)|hskp1))&(((![X73]: (~ndr1_0|((c1_1(X73)|c2_1(X73))|~c0_1(X73))))|(![X74]: (~ndr1_0|((~c0_1(X74)|~c2_1(X74))|~c3_1(X74)))))|hskp26))&(((![X75]: (~ndr1_0|((c1_1(X75)|c2_1(X75))|~c3_1(X75))))|(![X76]: (~ndr1_0|((c3_1(X76)|~c0_1(X76))|~c2_1(X76)))))|hskp16))&(((![X77]: (~ndr1_0|((c1_1(X77)|c2_1(X77))|~c3_1(X77))))|(![X78]: (~ndr1_0|((~c1_1(X78)|~c2_1(X78))|~c3_1(X78)))))|hskp8))&(((![X79]: (~ndr1_0|((c1_1(X79)|c2_1(X79))|~c3_1(X79))))|hskp26)|hskp18))&(((![X80]: (~ndr1_0|((c1_1(X80)|c3_1(X80))|~c0_1(X80))))|(![X81]: (~ndr1_0|((c1_1(X81)|~c2_1(X81))|~c3_1(X81)))))|hskp26))&(((![X82]: (~ndr1_0|((c1_1(X82)|c3_1(X82))|~c0_1(X82))))|(![X83]: (~ndr1_0|((c2_1(X83)|~c1_1(X83))|~c3_1(X83)))))|hskp3))&(((![X84]: (~ndr1_0|((c1_1(X84)|c3_1(X84))|~c0_1(X84))))|(![X85]: (~ndr1_0|((~c0_1(X85)|~c1_1(X85))|~c3_1(X85)))))|(![X86]: (~ndr1_0|((~c0_1(X86)|~c2_1(X86))|~c3_1(X86))))))&(((![X87]: (~ndr1_0|((c1_1(X87)|c3_1(X87))|~c0_1(X87))))|hskp1)|hskp8))&(((![X88]: (~ndr1_0|((c1_1(X88)|c3_1(X88))|~c0_1(X88))))|hskp11)|hskp19))&(((![X89]: (~ndr1_0|((c1_1(X89)|~c0_1(X89))|~c3_1(X89))))|(![X90]: (~ndr1_0|((c2_1(X90)|c3_1(X90))|~c1_1(X90)))))|hskp17))&(((![X91]: (~ndr1_0|((c1_1(X91)|~c0_1(X91))|~c3_1(X91))))|(![X92]: (~ndr1_0|((c2_1(X92)|c3_1(X92))|~c1_1(X92)))))|hskp8))&(((![X93]: (~ndr1_0|((c1_1(X93)|~c0_1(X93))|~c3_1(X93))))|hskp26)|hskp5))&(((![X94]: (~ndr1_0|((c1_1(X94)|~c0_1(X94))|~c3_1(X94))))|hskp11)|hskp10))&(((![X95]: (~ndr1_0|((c1_1(X95)|~c2_1(X95))|~c3_1(X95))))|(![X96]: (~ndr1_0|((c2_1(X96)|~c0_1(X96))|~c3_1(X96)))))|hskp3))&(((![X97]: (~ndr1_0|((c1_1(X97)|~c2_1(X97))|~c3_1(X97))))|(![X98]: (~ndr1_0|((~c0_1(X98)|~c1_1(X98))|~c2_1(X98)))))|hskp20))&(((![X99]: (~ndr1_0|((c1_1(X99)|~c2_1(X99))|~c3_1(X99))))|hskp7)|hskp15))&(((![X100]: (~ndr1_0|((c2_1(X100)|c3_1(X100))|~c0_1(X100))))|(![X101]: (~ndr1_0|((~c0_1(X101)|~c1_1(X101))|~c2_1(X101)))))|hskp11))&(((![X102]: (~ndr1_0|((c2_1(X102)|~c0_1(X102))|~c1_1(X102))))|(![X103]: (~ndr1_0|((c2_1(X103)|~c1_1(X103))|~c3_1(X103)))))|hskp5))&(((![X104]: (~ndr1_0|((c2_1(X104)|~c0_1(X104))|~c1_1(X104))))|(![X105]: (~ndr1_0|((c3_1(X105)|~c1_1(X105))|~c2_1(X105)))))|hskp12))&(((![X106]: (~ndr1_0|((c2_1(X106)|~c0_1(X106))|~c1_1(X106))))|hskp21)|hskp16))&(((![X107]: (~ndr1_0|((c2_1(X107)|~c0_1(X107))|~c1_1(X107))))|hskp17)|hskp20))&((![X108]: (~ndr1_0|((c2_1(X108)|~c0_1(X108))|~c1_1(X108))))|hskp22))&(((![X109]: (~ndr1_0|((c2_1(X109)|~c0_1(X109))|~c3_1(X109))))|(![X110]: (~ndr1_0|((c3_1(X110)|~c0_1(X110))|~c2_1(X110)))))|hskp4))&(((![X111]: (~ndr1_0|((c2_1(X111)|~c0_1(X111))|~c3_1(X111))))|hskp7)|hskp16))&(((![X112]: (~ndr1_0|((~c0_1(X112)|~c1_1(X112))|~c2_1(X112))))|hskp7)|hskp4))&(((![X113]: (~ndr1_0|((~c0_1(X113)|~c1_1(X113))|~c3_1(X113))))|hskp17)|hskp22))&((hskp27|hskp23)|hskp5))&((hskp7|hskp23)|hskp15))&(hskp17|hskp2))&((hskp17|hskp23)|hskp1))&((hskp23|hskp24)|hskp5))&((hskp6|hskp5)|hskp18))&((hskp29|hskp5)|hskp3))&((hskp24|hskp12)|hskp10))&((hskp12|hskp25)|hskp18)),
% 114.23/16.07    inference(pre_NNF_transformation,[status(thm)],[f2])).
% 114.23/16.07  fof(f4,plain,(
% 114.23/16.07    (((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((~hskp0|(((ndr1_0&c3_1(a2068))&~c0_1(a2068))&~c2_1(a2068)))&(~hskp1|(((ndr1_0&c0_1(a2070))&c3_1(a2070))&~c2_1(a2070))))&(~hskp2|(((ndr1_0&c0_1(a2071))&c2_1(a2071))&~c3_1(a2071))))&(~hskp3|(((ndr1_0&~c0_1(a2072))&~c1_1(a2072))&~c3_1(a2072))))&(~hskp4|(((ndr1_0&c1_1(a2074))&c3_1(a2074))&~c2_1(a2074))))&(~hskp5|(((ndr1_0&c1_1(a2076))&c3_1(a2076))&~c0_1(a2076))))&(~hskp6|(((ndr1_0&c0_1(a2078))&~c1_1(a2078))&~c2_1(a2078))))&(~hskp7|(((ndr1_0&c0_1(a2079))&c1_1(a2079))&~c3_1(a2079))))&(~hskp8|(((ndr1_0&c1_1(a2082))&c2_1(a2082))&~c0_1(a2082))))&(~hskp9|(((ndr1_0&c2_1(a2084))&c3_1(a2084))&~c1_1(a2084))))&(~hskp10|(((ndr1_0&c2_1(a2087))&~c1_1(a2087))&~c3_1(a2087))))&(~hskp11|(((ndr1_0&c0_1(a2093))&~c1_1(a2093))&~c3_1(a2093))))&(~hskp12|(((ndr1_0&c1_1(a2095))&~c0_1(a2095))&~c2_1(a2095))))&(~hskp13|(((ndr1_0&c2_1(a2096))&~c0_1(a2096))&~c1_1(a2096))))&(~hskp14|(((ndr1_0&~c0_1(a2097))&~c1_1(a2097))&~c2_1(a2097))))&(~hskp15|(((ndr1_0&c0_1(a2099))&~c2_1(a2099))&~c3_1(a2099))))&(~hskp16|(((ndr1_0&c3_1(a2104))&~c0_1(a2104))&~c1_1(a2104))))&(~hskp17|(((ndr1_0&c0_1(a2110))&c2_1(a2110))&~c1_1(a2110))))&(~hskp18|(((ndr1_0&c1_1(a2116))&~c2_1(a2116))&~c3_1(a2116))))&(~hskp19|(((ndr1_0&c2_1(a2122))&~c0_1(a2122))&~c3_1(a2122))))&(~hskp20|(((ndr1_0&~c1_1(a2130))&~c2_1(a2130))&~c3_1(a2130))))&(~hskp21|(((ndr1_0&c0_1(a2136))&c1_1(a2136))&~c2_1(a2136))))&(~hskp22|(((ndr1_0&c2_1(a2140))&c3_1(a2140))&~c0_1(a2140))))&(~hskp23|(((ndr1_0&c0_1(a2149))&c3_1(a2149))&~c1_1(a2149))))&(~hskp24|(((ndr1_0&c1_1(a2160))&c2_1(a2160))&~c3_1(a2160))))&(~hskp25|(((ndr1_0&c1_1(a2172))&~c0_1(a2172))&~c3_1(a2172))))&(~hskp26|(((ndr1_0&c0_1(a2069))&c2_1(a2069))&c3_1(a2069))))&(~hskp27|(((ndr1_0&c0_1(a2073))&c1_1(a2073))&c3_1(a2073))))&(~hskp28|(((ndr1_0&c0_1(a2075))&c1_1(a2075))&c2_1(a2075))))&(~hskp29|(((ndr1_0&c1_1(a2077))&c2_1(a2077))&c3_1(a2077))))&(((~ndr1_0|(![U]: ((c0_1(U)|c1_1(U))|c2_1(U))))|(~ndr1_0|(![V]: ((c0_1(V)|c2_1(V))|~c1_1(V)))))|(~ndr1_0|(![W]: ((c1_1(W)|c2_1(W))|c3_1(W))))))&(((~ndr1_0|(![X]: ((c0_1(X)|c1_1(X))|c2_1(X))))|(~ndr1_0|(![Y]: ((~c0_1(Y)|~c2_1(Y))|~c3_1(Y)))))|hskp0))&(((~ndr1_0|(![Z]: ((c0_1(Z)|c1_1(Z))|c2_1(Z))))|hskp26)|hskp1))&(((~ndr1_0|(![X1]: ((c0_1(X1)|c1_1(X1))|c2_1(X1))))|hskp2)|hskp3))&(((~ndr1_0|(![X2]: ((c0_1(X2)|c1_1(X2))|c3_1(X2))))|(~ndr1_0|(![X3]: ((c0_1(X3)|c1_1(X3))|~c2_1(X3)))))|hskp27))&(((~ndr1_0|(![X4]: ((c0_1(X4)|c1_1(X4))|c3_1(X4))))|(~ndr1_0|(![X5]: ((c1_1(X5)|c3_1(X5))|~c2_1(X5)))))|hskp4))&(((~ndr1_0|(![X6]: ((c0_1(X6)|c1_1(X6))|c3_1(X6))))|hskp28)|hskp5))&(((~ndr1_0|(![X7]: ((c0_1(X7)|c1_1(X7))|~c2_1(X7))))|(~ndr1_0|(![X8]: ((c0_1(X8)|~c2_1(X8))|~c3_1(X8)))))|(~ndr1_0|(![X9]: ((c1_1(X9)|~c0_1(X9))|~c2_1(X9))))))&(((~ndr1_0|(![X10]: ((c0_1(X10)|c1_1(X10))|~c2_1(X10))))|(~ndr1_0|(![X11]: ((c2_1(X11)|~c0_1(X11))|~c1_1(X11)))))|hskp29))&(((~ndr1_0|(![X12]: ((c0_1(X12)|c1_1(X12))|~c3_1(X12))))|(~ndr1_0|(![X13]: ((c1_1(X13)|~c0_1(X13))|~c3_1(X13)))))|hskp6))&(((~ndr1_0|(![X14]: ((c0_1(X14)|c1_1(X14))|~c3_1(X14))))|(~ndr1_0|(![X15]: ((c1_1(X15)|~c2_1(X15))|~c3_1(X15)))))|(~ndr1_0|(![X16]: ((c2_1(X16)|c3_1(X16))|~c1_1(X16))))))&(((~ndr1_0|(![X17]: ((c0_1(X17)|c1_1(X17))|~c3_1(X17))))|(~ndr1_0|(![X18]: ((~c0_1(X18)|~c1_1(X18))|~c3_1(X18)))))|hskp7))&(((~ndr1_0|(![X19]: ((c0_1(X19)|c2_1(X19))|c3_1(X19))))|(~ndr1_0|(![X20]: ((c1_1(X20)|c3_1(X20))|~c2_1(X20)))))|(~ndr1_0|(![X21]: ((c2_1(X21)|~c1_1(X21))|~c3_1(X21))))))&(((~ndr1_0|(![X22]: ((c0_1(X22)|c2_1(X22))|c3_1(X22))))|hskp5)|hskp4))&(((~ndr1_0|(![X23]: ((c0_1(X23)|c2_1(X23))|~c1_1(X23))))|(~ndr1_0|(![X24]: ((c1_1(X24)|c3_1(X24))|~c2_1(X24)))))|hskp8))&(((~ndr1_0|(![X25]: ((c0_1(X25)|c2_1(X25))|~c1_1(X25))))|(~ndr1_0|(![X26]: ((c1_1(X26)|~c0_1(X26))|~c3_1(X26)))))|hskp2))&(((~ndr1_0|(![X27]: ((c0_1(X27)|c2_1(X27))|~c1_1(X27))))|(~ndr1_0|(![X28]: ((c2_1(X28)|~c0_1(X28))|~c1_1(X28)))))|hskp9))&(((~ndr1_0|(![X29]: ((c0_1(X29)|c2_1(X29))|~c1_1(X29))))|(~ndr1_0|(![X30]: ((c2_1(X30)|~c0_1(X30))|~c3_1(X30)))))|hskp9))&(((~ndr1_0|(![X31]: ((c0_1(X31)|c2_1(X31))|~c3_1(X31))))|(~ndr1_0|(![X32]: ((c0_1(X32)|c3_1(X32))|~c1_1(X32)))))|(~ndr1_0|(![X33]: ((c2_1(X33)|c3_1(X33))|~c1_1(X33))))))&(((~ndr1_0|(![X34]: ((c0_1(X34)|c2_1(X34))|~c3_1(X34))))|(~ndr1_0|(![X35]: ((c1_1(X35)|c2_1(X35))|~c3_1(X35)))))|hskp4))&(((~ndr1_0|(![X36]: ((c0_1(X36)|c2_1(X36))|~c3_1(X36))))|(~ndr1_0|(![X37]: ((~c0_1(X37)|~c2_1(X37))|~c3_1(X37)))))|hskp10))&(((~ndr1_0|(![X38]: ((c0_1(X38)|c2_1(X38))|~c3_1(X38))))|hskp27)|hskp7))&(((~ndr1_0|(![X39]: ((c0_1(X39)|c3_1(X39))|~c1_1(X39))))|(~ndr1_0|(![X40]: ((~c0_1(X40)|~c2_1(X40))|~c3_1(X40)))))|hskp4))&(((~ndr1_0|(![X41]: ((c0_1(X41)|c3_1(X41))|~c1_1(X41))))|(~ndr1_0|(![X42]: ((~c1_1(X42)|~c2_1(X42))|~c3_1(X42)))))|hskp8))&(((~ndr1_0|(![X43]: ((c0_1(X43)|c3_1(X43))|~c2_1(X43))))|(~ndr1_0|(![X44]: ((c0_1(X44)|~c1_1(X44))|~c2_1(X44)))))|hskp1))&(((~ndr1_0|(![X45]: ((c0_1(X45)|c3_1(X45))|~c2_1(X45))))|(~ndr1_0|(![X46]: ((c1_1(X46)|c2_1(X46))|~c0_1(X46)))))|hskp11))&(((~ndr1_0|(![X47]: ((c0_1(X47)|c3_1(X47))|~c2_1(X47))))|(~ndr1_0|(![X48]: ((c1_1(X48)|~c2_1(X48))|~c3_1(X48)))))|hskp10))&(((~ndr1_0|(![X49]: ((c0_1(X49)|c3_1(X49))|~c2_1(X49))))|(~ndr1_0|(![X50]: ((c2_1(X50)|~c0_1(X50))|~c3_1(X50)))))|(~ndr1_0|(![X51]: ((c2_1(X51)|~c1_1(X51))|~c3_1(X51))))))&(((~ndr1_0|(![X52]: ((c0_1(X52)|c3_1(X52))|~c2_1(X52))))|hskp12)|hskp13))&(((~ndr1_0|(![X53]: ((c0_1(X53)|~c1_1(X53))|~c2_1(X53))))|(~ndr1_0|(![X54]: ((c1_1(X54)|c2_1(X54))|c3_1(X54)))))|hskp14))&(((~ndr1_0|(![X55]: ((c0_1(X55)|~c1_1(X55))|~c2_1(X55))))|(~ndr1_0|(![X56]: ((c1_1(X56)|c3_1(X56))|~c2_1(X56)))))|hskp11))&(((~ndr1_0|(![X57]: ((c0_1(X57)|~c1_1(X57))|~c3_1(X57))))|(~ndr1_0|(![X58]: ((c1_1(X58)|c2_1(X58))|~c3_1(X58)))))|hskp15))&(((~ndr1_0|(![X59]: ((c0_1(X59)|~c1_1(X59))|~c3_1(X59))))|(~ndr1_0|(![X60]: ((c1_1(X60)|~c0_1(X60))|~c3_1(X60)))))|(~ndr1_0|(![X61]: ((c2_1(X61)|~c0_1(X61))|~c1_1(X61))))))&(((~ndr1_0|(![X62]: ((c0_1(X62)|~c1_1(X62))|~c3_1(X62))))|hskp28)|hskp4))&((~ndr1_0|(![X63]: ((c0_1(X63)|~c1_1(X63))|~c3_1(X63))))|hskp0))&(((~ndr1_0|(![X64]: ((c0_1(X64)|~c2_1(X64))|~c3_1(X64))))|(~ndr1_0|(![X65]: ((c1_1(X65)|~c2_1(X65))|~c3_1(X65)))))|hskp27))&(((~ndr1_0|(![X66]: ((c0_1(X66)|~c2_1(X66))|~c3_1(X66))))|(~ndr1_0|(![X67]: ((c2_1(X67)|c3_1(X67))|~c0_1(X67)))))|hskp16))&(((~ndr1_0|(![X68]: ((c0_1(X68)|~c2_1(X68))|~c3_1(X68))))|(~ndr1_0|(![X69]: ((~c0_1(X69)|~c1_1(X69))|~c2_1(X69)))))|hskp26))&(((~ndr1_0|(![X70]: ((c0_1(X70)|~c2_1(X70))|~c3_1(X70))))|hskp27)|hskp29))&(((~ndr1_0|(![X71]: ((c0_1(X71)|~c2_1(X71))|~c3_1(X71))))|hskp11)|hskp0))&(((~ndr1_0|(![X72]: ((c1_1(X72)|c2_1(X72))|c3_1(X72))))|hskp17)|hskp1))&(((~ndr1_0|(![X73]: ((c1_1(X73)|c2_1(X73))|~c0_1(X73))))|(~ndr1_0|(![X74]: ((~c0_1(X74)|~c2_1(X74))|~c3_1(X74)))))|hskp26))&(((~ndr1_0|(![X75]: ((c1_1(X75)|c2_1(X75))|~c3_1(X75))))|(~ndr1_0|(![X76]: ((c3_1(X76)|~c0_1(X76))|~c2_1(X76)))))|hskp16))&(((~ndr1_0|(![X77]: ((c1_1(X77)|c2_1(X77))|~c3_1(X77))))|(~ndr1_0|(![X78]: ((~c1_1(X78)|~c2_1(X78))|~c3_1(X78)))))|hskp8))&(((~ndr1_0|(![X79]: ((c1_1(X79)|c2_1(X79))|~c3_1(X79))))|hskp26)|hskp18))&(((~ndr1_0|(![X80]: ((c1_1(X80)|c3_1(X80))|~c0_1(X80))))|(~ndr1_0|(![X81]: ((c1_1(X81)|~c2_1(X81))|~c3_1(X81)))))|hskp26))&(((~ndr1_0|(![X82]: ((c1_1(X82)|c3_1(X82))|~c0_1(X82))))|(~ndr1_0|(![X83]: ((c2_1(X83)|~c1_1(X83))|~c3_1(X83)))))|hskp3))&(((~ndr1_0|(![X84]: ((c1_1(X84)|c3_1(X84))|~c0_1(X84))))|(~ndr1_0|(![X85]: ((~c0_1(X85)|~c1_1(X85))|~c3_1(X85)))))|(~ndr1_0|(![X86]: ((~c0_1(X86)|~c2_1(X86))|~c3_1(X86))))))&(((~ndr1_0|(![X87]: ((c1_1(X87)|c3_1(X87))|~c0_1(X87))))|hskp1)|hskp8))&(((~ndr1_0|(![X88]: ((c1_1(X88)|c3_1(X88))|~c0_1(X88))))|hskp11)|hskp19))&(((~ndr1_0|(![X89]: ((c1_1(X89)|~c0_1(X89))|~c3_1(X89))))|(~ndr1_0|(![X90]: ((c2_1(X90)|c3_1(X90))|~c1_1(X90)))))|hskp17))&(((~ndr1_0|(![X91]: ((c1_1(X91)|~c0_1(X91))|~c3_1(X91))))|(~ndr1_0|(![X92]: ((c2_1(X92)|c3_1(X92))|~c1_1(X92)))))|hskp8))&(((~ndr1_0|(![X93]: ((c1_1(X93)|~c0_1(X93))|~c3_1(X93))))|hskp26)|hskp5))&(((~ndr1_0|(![X94]: ((c1_1(X94)|~c0_1(X94))|~c3_1(X94))))|hskp11)|hskp10))&(((~ndr1_0|(![X95]: ((c1_1(X95)|~c2_1(X95))|~c3_1(X95))))|(~ndr1_0|(![X96]: ((c2_1(X96)|~c0_1(X96))|~c3_1(X96)))))|hskp3))&(((~ndr1_0|(![X97]: ((c1_1(X97)|~c2_1(X97))|~c3_1(X97))))|(~ndr1_0|(![X98]: ((~c0_1(X98)|~c1_1(X98))|~c2_1(X98)))))|hskp20))&(((~ndr1_0|(![X99]: ((c1_1(X99)|~c2_1(X99))|~c3_1(X99))))|hskp7)|hskp15))&(((~ndr1_0|(![X100]: ((c2_1(X100)|c3_1(X100))|~c0_1(X100))))|(~ndr1_0|(![X101]: ((~c0_1(X101)|~c1_1(X101))|~c2_1(X101)))))|hskp11))&(((~ndr1_0|(![X102]: ((c2_1(X102)|~c0_1(X102))|~c1_1(X102))))|(~ndr1_0|(![X103]: ((c2_1(X103)|~c1_1(X103))|~c3_1(X103)))))|hskp5))&(((~ndr1_0|(![X104]: ((c2_1(X104)|~c0_1(X104))|~c1_1(X104))))|(~ndr1_0|(![X105]: ((c3_1(X105)|~c1_1(X105))|~c2_1(X105)))))|hskp12))&(((~ndr1_0|(![X106]: ((c2_1(X106)|~c0_1(X106))|~c1_1(X106))))|hskp21)|hskp16))&(((~ndr1_0|(![X107]: ((c2_1(X107)|~c0_1(X107))|~c1_1(X107))))|hskp17)|hskp20))&((~ndr1_0|(![X108]: ((c2_1(X108)|~c0_1(X108))|~c1_1(X108))))|hskp22))&(((~ndr1_0|(![X109]: ((c2_1(X109)|~c0_1(X109))|~c3_1(X109))))|(~ndr1_0|(![X110]: ((c3_1(X110)|~c0_1(X110))|~c2_1(X110)))))|hskp4))&(((~ndr1_0|(![X111]: ((c2_1(X111)|~c0_1(X111))|~c3_1(X111))))|hskp7)|hskp16))&(((~ndr1_0|(![X112]: ((~c0_1(X112)|~c1_1(X112))|~c2_1(X112))))|hskp7)|hskp4))&(((~ndr1_0|(![X113]: ((~c0_1(X113)|~c1_1(X113))|~c3_1(X113))))|hskp17)|hskp22))&((hskp27|hskp23)|hskp5))&((hskp7|hskp23)|hskp15))&(hskp17|hskp2))&((hskp17|hskp23)|hskp1))&((hskp23|hskp24)|hskp5))&((hskp6|hskp5)|hskp18))&((hskp29|hskp5)|hskp3))&((hskp24|hskp12)|hskp10))&((hskp12|hskp25)|hskp18)),
% 114.23/16.07    inference(miniscoping,[status(thm)],[f3])).
% 114.23/16.07  fof(f6,plain,(
% 114.23/16.07    ~hskp0|c3_1(a2068)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f7,plain,(
% 114.23/16.07    ~hskp0|~c0_1(a2068)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f8,plain,(
% 114.23/16.07    ~hskp0|~c2_1(a2068)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f10,plain,(
% 114.23/16.07    ~hskp1|c0_1(a2070)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f11,plain,(
% 114.23/16.07    ~hskp1|c3_1(a2070)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f12,plain,(
% 114.23/16.07    ~hskp1|~c2_1(a2070)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f13,plain,(
% 114.23/16.07    ~hskp2|ndr1_0),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f18,plain,(
% 114.23/16.07    ~hskp3|~c0_1(a2072)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f19,plain,(
% 114.23/16.07    ~hskp3|~c1_1(a2072)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f20,plain,(
% 114.23/16.07    ~hskp3|~c3_1(a2072)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f22,plain,(
% 114.23/16.07    ~hskp4|c1_1(a2074)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f23,plain,(
% 114.23/16.07    ~hskp4|c3_1(a2074)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f24,plain,(
% 114.23/16.07    ~hskp4|~c2_1(a2074)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f26,plain,(
% 114.23/16.07    ~hskp5|c1_1(a2076)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f27,plain,(
% 114.23/16.07    ~hskp5|c3_1(a2076)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f28,plain,(
% 114.23/16.07    ~hskp5|~c0_1(a2076)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f34,plain,(
% 114.23/16.07    ~hskp7|c0_1(a2079)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f35,plain,(
% 114.23/16.07    ~hskp7|c1_1(a2079)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f36,plain,(
% 114.23/16.07    ~hskp7|~c3_1(a2079)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f38,plain,(
% 114.23/16.07    ~hskp8|c1_1(a2082)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f39,plain,(
% 114.23/16.07    ~hskp8|c2_1(a2082)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f40,plain,(
% 114.23/16.07    ~hskp8|~c0_1(a2082)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f42,plain,(
% 114.23/16.07    ~hskp9|c2_1(a2084)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f43,plain,(
% 114.23/16.07    ~hskp9|c3_1(a2084)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f44,plain,(
% 114.23/16.07    ~hskp9|~c1_1(a2084)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f46,plain,(
% 114.23/16.07    ~hskp10|c2_1(a2087)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f47,plain,(
% 114.23/16.07    ~hskp10|~c1_1(a2087)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f48,plain,(
% 114.23/16.07    ~hskp10|~c3_1(a2087)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f50,plain,(
% 114.23/16.07    ~hskp11|c0_1(a2093)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f51,plain,(
% 114.23/16.07    ~hskp11|~c1_1(a2093)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f52,plain,(
% 114.23/16.07    ~hskp11|~c3_1(a2093)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f54,plain,(
% 114.23/16.07    ~hskp12|c1_1(a2095)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f55,plain,(
% 114.23/16.07    ~hskp12|~c0_1(a2095)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f56,plain,(
% 114.23/16.07    ~hskp12|~c2_1(a2095)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f58,plain,(
% 114.23/16.07    ~hskp13|c2_1(a2096)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f59,plain,(
% 114.23/16.07    ~hskp13|~c0_1(a2096)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f60,plain,(
% 114.23/16.07    ~hskp13|~c1_1(a2096)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f66,plain,(
% 114.23/16.07    ~hskp15|c0_1(a2099)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f67,plain,(
% 114.23/16.07    ~hskp15|~c2_1(a2099)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f68,plain,(
% 114.23/16.07    ~hskp15|~c3_1(a2099)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f70,plain,(
% 114.23/16.07    ~hskp16|c3_1(a2104)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f71,plain,(
% 114.23/16.07    ~hskp16|~c0_1(a2104)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f72,plain,(
% 114.23/16.07    ~hskp16|~c1_1(a2104)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f73,plain,(
% 114.23/16.07    ~hskp17|ndr1_0),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f74,plain,(
% 114.23/16.07    ~hskp17|c0_1(a2110)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f76,plain,(
% 114.23/16.07    ~hskp17|~c1_1(a2110)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f78,plain,(
% 114.23/16.07    ~hskp18|c1_1(a2116)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f79,plain,(
% 114.23/16.07    ~hskp18|~c2_1(a2116)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f80,plain,(
% 114.23/16.07    ~hskp18|~c3_1(a2116)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f82,plain,(
% 114.23/16.07    ~hskp19|c2_1(a2122)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f83,plain,(
% 114.23/16.07    ~hskp19|~c0_1(a2122)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f84,plain,(
% 114.23/16.07    ~hskp19|~c3_1(a2122)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f94,plain,(
% 114.23/16.07    ~hskp22|c2_1(a2140)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f95,plain,(
% 114.23/16.07    ~hskp22|c3_1(a2140)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f96,plain,(
% 114.23/16.07    ~hskp22|~c0_1(a2140)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f98,plain,(
% 114.23/16.07    ~hskp23|c0_1(a2149)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f99,plain,(
% 114.23/16.07    ~hskp23|c3_1(a2149)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f100,plain,(
% 114.23/16.07    ~hskp23|~c1_1(a2149)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f102,plain,(
% 114.23/16.07    ~hskp24|c1_1(a2160)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f103,plain,(
% 114.23/16.07    ~hskp24|c2_1(a2160)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f104,plain,(
% 114.23/16.07    ~hskp24|~c3_1(a2160)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f106,plain,(
% 114.23/16.07    ~hskp25|c1_1(a2172)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f107,plain,(
% 114.23/16.07    ~hskp25|~c0_1(a2172)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f110,plain,(
% 114.23/16.07    ~hskp26|c0_1(a2069)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f111,plain,(
% 114.23/16.07    ~hskp26|c2_1(a2069)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f112,plain,(
% 114.23/16.07    ~hskp26|c3_1(a2069)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f114,plain,(
% 114.23/16.07    ~hskp27|c0_1(a2073)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f115,plain,(
% 114.23/16.07    ~hskp27|c1_1(a2073)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f116,plain,(
% 114.23/16.07    ~hskp27|c3_1(a2073)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f118,plain,(
% 114.23/16.07    ~hskp28|c0_1(a2075)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f119,plain,(
% 114.23/16.07    ~hskp28|c1_1(a2075)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f120,plain,(
% 114.23/16.07    ~hskp28|c2_1(a2075)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f122,plain,(
% 114.23/16.07    ~hskp29|c1_1(a2077)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f123,plain,(
% 114.23/16.07    ~hskp29|c2_1(a2077)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f124,plain,(
% 114.23/16.07    ~hskp29|c3_1(a2077)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f126,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|c2_1(X0)|~ndr1_0|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp0)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f127,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|c1_1(X0)|c2_1(X0)|hskp26|hskp1)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f130,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|c3_1(X0)|~ndr1_0|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f131,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|c1_1(X0)|c3_1(X0)|hskp28|hskp5)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f133,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|~c2_1(X0)|~ndr1_0|c2_1(X1)|~c0_1(X1)|~c1_1(X1)|hskp29)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f135,plain,(
% 114.23/16.07    ![X0,X1,X2]: (~ndr1_0|c0_1(X0)|c1_1(X0)|~c3_1(X0)|~ndr1_0|c1_1(X1)|~c2_1(X1)|~c3_1(X1)|~ndr1_0|c2_1(X2)|c3_1(X2)|~c1_1(X2))),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f136,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|~c3_1(X0)|~ndr1_0|~c0_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp7)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f137,plain,(
% 114.23/16.07    ![X0,X1,X2]: (~ndr1_0|c0_1(X0)|c2_1(X0)|c3_1(X0)|~ndr1_0|c1_1(X1)|c3_1(X1)|~c2_1(X1)|~ndr1_0|c2_1(X2)|~c1_1(X2)|~c3_1(X2))),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f138,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|c2_1(X0)|c3_1(X0)|hskp5|hskp4)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f139,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c1_1(X0)|~ndr1_0|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp8)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f141,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c1_1(X0)|~ndr1_0|c2_1(X1)|~c0_1(X1)|~c1_1(X1)|hskp9)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f142,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c1_1(X0)|~ndr1_0|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|hskp9)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f144,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c3_1(X0)|~ndr1_0|c1_1(X1)|c2_1(X1)|~c3_1(X1)|hskp4)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f145,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c3_1(X0)|~ndr1_0|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp10)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f146,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c3_1(X0)|hskp27|hskp7)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f147,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c3_1(X0)|~c1_1(X0)|~ndr1_0|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp4)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f149,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c3_1(X0)|~c2_1(X0)|~ndr1_0|c0_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp1)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f152,plain,(
% 114.23/16.07    ![X0,X1,X2]: (~ndr1_0|c0_1(X0)|c3_1(X0)|~c2_1(X0)|~ndr1_0|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|~ndr1_0|c2_1(X2)|~c1_1(X2)|~c3_1(X2))),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f153,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|c3_1(X0)|~c2_1(X0)|hskp12|hskp13)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f155,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|~c1_1(X0)|~c2_1(X0)|~ndr1_0|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp11)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f158,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|~c1_1(X0)|~c3_1(X0)|hskp28|hskp4)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f159,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|~c1_1(X0)|~c3_1(X0)|hskp0)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f161,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|~c2_1(X0)|~c3_1(X0)|~ndr1_0|c2_1(X1)|c3_1(X1)|~c0_1(X1)|hskp16)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f162,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|~c2_1(X0)|~c3_1(X0)|~ndr1_0|~c0_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp26)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f163,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp27|hskp29)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f164,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c0_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp11|hskp0)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f166,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c1_1(X0)|c2_1(X0)|~c0_1(X0)|~ndr1_0|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp26)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f168,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c1_1(X0)|c2_1(X0)|~c3_1(X0)|~ndr1_0|~c1_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp8)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f170,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c1_1(X0)|c3_1(X0)|~c0_1(X0)|~ndr1_0|c1_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp26)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f171,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c1_1(X0)|c3_1(X0)|~c0_1(X0)|~ndr1_0|c2_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp3)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f173,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp1|hskp8)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f174,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp11|hskp19)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f175,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c1_1(X0)|~c0_1(X0)|~c3_1(X0)|~ndr1_0|c2_1(X1)|c3_1(X1)|~c1_1(X1)|hskp17)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f178,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c1_1(X0)|~c0_1(X0)|~c3_1(X0)|hskp11|hskp10)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f179,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c1_1(X0)|~c2_1(X0)|~c3_1(X0)|~ndr1_0|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|hskp3)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f181,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c1_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp7|hskp15)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f183,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|~ndr1_0|c2_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp5)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f184,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|~ndr1_0|c3_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp12)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f187,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp22)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f188,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c3_1(X0)|~ndr1_0|c3_1(X1)|~c0_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f189,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c3_1(X0)|hskp7|hskp16)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f190,plain,(
% 114.23/16.07    ![X0]: (~ndr1_0|~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp7|hskp4)),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f193,plain,(
% 114.23/16.07    hskp7|hskp23|hskp15),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f194,plain,(
% 114.23/16.07    hskp17|hskp2),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f195,plain,(
% 114.23/16.07    hskp17|hskp23|hskp1),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f198,plain,(
% 114.23/16.07    hskp29|hskp5|hskp3),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f199,plain,(
% 114.23/16.07    hskp24|hskp12|hskp10),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f200,plain,(
% 114.23/16.07    hskp12|hskp25|hskp18),
% 114.23/16.07    inference(cnf_transformation,[status(thm)],[f4])).
% 114.23/16.07  fof(f202,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|c2_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp0)),
% 114.23/16.07    inference(duplicate_literals_removal,[status(thm)],[f126])).
% 114.23/16.07  fof(f204,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.07    inference(duplicate_literals_removal,[status(thm)],[f130])).
% 114.23/16.07  fof(f206,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c1_1(X1)|hskp29)),
% 114.23/16.07    inference(duplicate_literals_removal,[status(thm)],[f133])).
% 114.23/16.07  fof(f208,plain,(
% 114.23/16.07    ![X0,X1,X2]: (~ndr1_0|c0_1(X0)|c1_1(X0)|~c3_1(X0)|c1_1(X1)|~c2_1(X1)|~c3_1(X1)|c2_1(X2)|c3_1(X2)|~c1_1(X2))),
% 114.23/16.07    inference(duplicate_literals_removal,[status(thm)],[f135])).
% 114.23/16.07  fof(f209,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c1_1(X0)|~c3_1(X0)|~c0_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp7)),
% 114.23/16.07    inference(duplicate_literals_removal,[status(thm)],[f136])).
% 114.23/16.07  fof(f210,plain,(
% 114.23/16.07    ![X0,X1,X2]: (~ndr1_0|c0_1(X0)|c2_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|c2_1(X2)|~c1_1(X2)|~c3_1(X2))),
% 114.23/16.07    inference(duplicate_literals_removal,[status(thm)],[f137])).
% 114.23/16.07  fof(f211,plain,(
% 114.23/16.07    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c1_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp8)),
% 114.23/16.07    inference(duplicate_literals_removal,[status(thm)],[f139])).
% 114.23/16.08  fof(f213,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(X1)|~c0_1(X1)|~c1_1(X1)|hskp9)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f141])).
% 114.23/16.08  fof(f214,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|hskp9)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f142])).
% 114.23/16.08  fof(f216,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c3_1(X0)|c1_1(X1)|c2_1(X1)|~c3_1(X1)|hskp4)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f144])).
% 114.23/16.08  fof(f217,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|c2_1(X0)|~c3_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp10)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f145])).
% 114.23/16.08  fof(f218,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp4)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f147])).
% 114.23/16.08  fof(f220,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|c3_1(X0)|~c2_1(X0)|c0_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp1)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f149])).
% 114.23/16.08  fof(f223,plain,(
% 114.23/16.08    ![X0,X1,X2]: (~ndr1_0|c0_1(X0)|c3_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|c2_1(X2)|~c1_1(X2)|~c3_1(X2))),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f152])).
% 114.23/16.08  fof(f225,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|~c1_1(X0)|~c2_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp11)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f155])).
% 114.23/16.08  fof(f229,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|~c2_1(X0)|~c3_1(X0)|c2_1(X1)|c3_1(X1)|~c0_1(X1)|hskp16)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f161])).
% 114.23/16.08  fof(f230,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c0_1(X0)|~c2_1(X0)|~c3_1(X0)|~c0_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp26)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f162])).
% 114.23/16.08  fof(f231,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c1_1(X0)|c2_1(X0)|~c0_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp26)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f166])).
% 114.23/16.08  fof(f233,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c1_1(X0)|c2_1(X0)|~c3_1(X0)|~c1_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp8)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f168])).
% 114.23/16.08  fof(f234,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c1_1(X0)|c3_1(X0)|~c0_1(X0)|c1_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp26)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f170])).
% 114.23/16.08  fof(f235,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c1_1(X0)|c3_1(X0)|~c0_1(X0)|c2_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp3)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f171])).
% 114.23/16.08  fof(f237,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c1_1(X0)|~c0_1(X0)|~c3_1(X0)|c2_1(X1)|c3_1(X1)|~c1_1(X1)|hskp17)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f175])).
% 114.23/16.08  fof(f239,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c1_1(X0)|~c2_1(X0)|~c3_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|hskp3)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f179])).
% 114.23/16.08  fof(f242,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|c2_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp5)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f183])).
% 114.23/16.08  fof(f243,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|c3_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp12)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f184])).
% 114.23/16.08  fof(f244,plain,(
% 114.23/16.08    ![X0,X1]: (~ndr1_0|c2_1(X0)|~c0_1(X0)|~c3_1(X0)|c3_1(X1)|~c0_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f188])).
% 114.23/16.08  fof(f245,plain,(
% 114.23/16.08    hskp2|ndr1_0),
% 114.23/16.08    inference(resolution,[status(thm)],[f194,f73])).
% 114.23/16.08  fof(f246,plain,(
% 114.23/16.08    ndr1_0),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f245,f13])).
% 114.23/16.08  fof(f265,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c1_1(X0)|~c3_1(X0)|hskp0)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f159,f246])).
% 114.23/16.08  fof(f266,plain,(
% 114.23/16.08    c0_1(a2077)|~c1_1(a2077)|hskp0|~hskp29),
% 114.23/16.08    inference(resolution,[status(thm)],[f265,f124])).
% 114.23/16.08  fof(f270,plain,(
% 114.23/16.08    c0_1(a2140)|~c1_1(a2140)|hskp0|~hskp22),
% 114.23/16.08    inference(resolution,[status(thm)],[f265,f95])).
% 114.23/16.08  fof(f273,plain,(
% 114.23/16.08    c0_1(a2076)|~c1_1(a2076)|hskp0|~hskp5),
% 114.23/16.08    inference(resolution,[status(thm)],[f265,f27])).
% 114.23/16.08  fof(f274,plain,(
% 114.23/16.08    c0_1(a2074)|~c1_1(a2074)|hskp0|~hskp4),
% 114.23/16.08    inference(resolution,[status(thm)],[f265,f23])).
% 114.23/16.08  fof(f277,plain,(
% 114.23/16.08    c0_1(a2077)|hskp0|~hskp29),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f266,f122])).
% 114.23/16.08  fof(f278,plain,(
% 114.23/16.08    ~c1_1(a2140)|hskp0|~hskp22),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f270,f96])).
% 114.23/16.08  fof(f279,plain,(
% 114.23/16.08    ~c1_1(a2076)|hskp0|~hskp5),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f273,f28])).
% 114.23/16.08  fof(f280,plain,(
% 114.23/16.08    c0_1(a2074)|hskp0|~hskp4),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f274,f22])).
% 114.23/16.08  fof(f281,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c1_1(X0)|c2_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp0)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f202,f246])).
% 114.23/16.08  fof(f282,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c2_1(X0)|~c0_1(a2077)|~c2_1(a2077)|hskp0|~hskp29)),
% 114.23/16.08    inference(resolution,[status(thm)],[f281,f124])).
% 114.23/16.08  fof(f293,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c2_1(X0)|~c2_1(a2077)|hskp0|~hskp29)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f282,f277])).
% 114.23/16.08  fof(f298,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c2_1(X0)|hskp26|hskp1)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f127,f246])).
% 114.23/16.08  fof(f309,plain,(
% 114.23/16.08    c0_1(a2072)|c2_1(a2072)|hskp26|hskp1|~hskp3),
% 114.23/16.08    inference(resolution,[status(thm)],[f298,f19])).
% 114.23/16.08  fof(f314,plain,(
% 114.23/16.08    c2_1(a2072)|hskp26|hskp1|~hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f309,f18])).
% 114.23/16.08  fof(f316,plain,(
% 114.23/16.08    hskp0|~hskp5),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f279,f26])).
% 114.23/16.08  fof(f318,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp22)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f187,f246])).
% 114.23/16.08  fof(f325,plain,(
% 114.23/16.08    c2_1(a2116)|~c0_1(a2116)|hskp22|~hskp18),
% 114.23/16.08    inference(resolution,[status(thm)],[f318,f78])).
% 114.23/16.08  fof(f328,plain,(
% 114.23/16.08    c2_1(a2079)|~c0_1(a2079)|hskp22|~hskp7),
% 114.23/16.08    inference(resolution,[status(thm)],[f318,f35])).
% 114.23/16.08  fof(f330,plain,(
% 114.23/16.08    c2_1(a2074)|~c0_1(a2074)|hskp22|~hskp4),
% 114.23/16.08    inference(resolution,[status(thm)],[f318,f22])).
% 114.23/16.08  fof(f334,plain,(
% 114.23/16.08    ~c0_1(a2116)|hskp22|~hskp18),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f325,f79])).
% 114.23/16.08  fof(f335,plain,(
% 114.23/16.08    c2_1(a2079)|hskp22|~hskp7),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f328,f34])).
% 114.23/16.08  fof(f336,plain,(
% 114.23/16.08    ~c0_1(a2074)|hskp22|~hskp4),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f330,f24])).
% 114.23/16.08  fof(f380,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c1_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f204,f246])).
% 114.23/16.08  fof(f393,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c3_1(X0)|c1_1(a2087)|c3_1(a2087)|hskp4|~hskp10)),
% 114.23/16.08    inference(resolution,[status(thm)],[f380,f46])).
% 114.23/16.08  fof(f401,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c3_1(X0)|c3_1(a2087)|hskp4|~hskp10)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f393,f47])).
% 114.23/16.08  fof(f404,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c3_1(X0)|hskp28|hskp5)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f131,f246])).
% 114.23/16.08  fof(f415,plain,(
% 114.23/16.08    c0_1(a2072)|c3_1(a2072)|hskp28|hskp5|~hskp3),
% 114.23/16.08    inference(resolution,[status(thm)],[f404,f19])).
% 114.23/16.08  fof(f422,plain,(
% 114.23/16.08    c3_1(a2072)|hskp28|hskp5|~hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f415,f18])).
% 114.23/16.08  fof(f424,plain,(
% 114.23/16.08    hskp28|hskp5|~hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f422,f20])).
% 114.23/16.08  fof(f425,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|hskp5|hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f138,f246])).
% 114.23/16.08  fof(f428,plain,(
% 114.23/16.08    c0_1(a2116)|c3_1(a2116)|hskp5|hskp4|~hskp18),
% 114.23/16.08    inference(resolution,[status(thm)],[f425,f79])).
% 114.23/16.08  fof(f436,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c3_1(X0)|hskp5|hskp4|c0_1(X1)|c1_1(X1)|c3_1(X1)|c1_1(X0)|c3_1(X0)|hskp4)),
% 114.23/16.08    inference(resolution,[status(thm)],[f425,f380])).
% 114.23/16.08  fof(f439,plain,(
% 114.23/16.08    c0_1(a2116)|hskp5|hskp4|~hskp18),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f428,f80])).
% 114.23/16.08  fof(f442,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c3_1(X0)|hskp5|hskp4|c0_1(X1)|c1_1(X1)|c3_1(X1)|c1_1(X0))),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f436])).
% 114.23/16.08  fof(f444,plain,(
% 114.23/16.08    hskp5|hskp4|~hskp18|hskp22|~hskp18),
% 114.23/16.08    inference(resolution,[status(thm)],[f439,f334])).
% 114.23/16.08  fof(f445,plain,(
% 114.23/16.08    hskp5|hskp4|~hskp18|hskp22),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f444])).
% 114.23/16.08  fof(f463,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c1_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c1_1(X1)|hskp29)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f206,f246])).
% 114.23/16.08  fof(f469,plain,(
% 114.23/16.08    ![X0]: (c0_1(a2096)|~c2_1(a2096)|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp29|~hskp13)),
% 114.23/16.08    inference(resolution,[status(thm)],[f463,f60])).
% 114.23/16.08  fof(f478,plain,(
% 114.23/16.08    ![X0]: (~c2_1(a2096)|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp29|~hskp13)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f469,f59])).
% 114.23/16.08  fof(f495,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|hskp27|hskp7)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f146,f246])).
% 114.23/16.08  fof(f501,plain,(
% 114.23/16.08    c0_1(a2104)|c2_1(a2104)|hskp27|hskp7|~hskp16),
% 114.23/16.08    inference(resolution,[status(thm)],[f495,f70])).
% 114.23/16.08  fof(f504,plain,(
% 114.23/16.08    c0_1(a2074)|c2_1(a2074)|hskp27|hskp7|~hskp4),
% 114.23/16.08    inference(resolution,[status(thm)],[f495,f23])).
% 114.23/16.08  fof(f506,plain,(
% 114.23/16.08    c0_1(a2068)|c2_1(a2068)|hskp27|hskp7|~hskp0),
% 114.23/16.08    inference(resolution,[status(thm)],[f495,f6])).
% 114.23/16.08  fof(f507,plain,(
% 114.23/16.08    c2_1(a2104)|hskp27|hskp7|~hskp16),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f501,f71])).
% 114.23/16.08  fof(f509,plain,(
% 114.23/16.08    c0_1(a2074)|hskp27|hskp7|~hskp4),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f504,f24])).
% 114.23/16.08  fof(f510,plain,(
% 114.23/16.08    c2_1(a2068)|hskp27|hskp7|~hskp0),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f506,f7])).
% 114.23/16.08  fof(f511,plain,(
% 114.23/16.08    hskp27|hskp7|~hskp0),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f510,f8])).
% 114.23/16.08  fof(f528,plain,(
% 114.23/16.08    ![X0,X1,X2]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|c1_1(X1)|~c2_1(X1)|~c3_1(X1)|c2_1(X2)|c3_1(X2)|~c1_1(X2))),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f208,f246])).
% 114.23/16.08  fof(f535,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|c1_1(a2084)|~c2_1(a2084)|c2_1(X1)|c3_1(X1)|~c1_1(X1)|~hskp9)),
% 114.23/16.08    inference(resolution,[status(thm)],[f528,f43])).
% 114.23/16.08  fof(f544,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|~c2_1(a2084)|c2_1(X1)|c3_1(X1)|~c1_1(X1)|~hskp9)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f535,f44])).
% 114.23/16.08  fof(f545,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|~c0_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp7)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f209,f246])).
% 114.23/16.08  fof(f546,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|~c0_1(a2077)|~c1_1(a2077)|hskp7|~hskp29)),
% 114.23/16.08    inference(resolution,[status(thm)],[f545,f124])).
% 114.23/16.08  fof(f547,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|~c0_1(a2073)|~c1_1(a2073)|hskp7|~hskp27)),
% 114.23/16.08    inference(resolution,[status(thm)],[f545,f116])).
% 114.23/16.08  fof(f557,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|~c0_1(a2077)|hskp7|~hskp29)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f546,f122])).
% 114.23/16.08  fof(f558,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|~c1_1(a2073)|hskp7|~hskp27)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f547,f114])).
% 114.23/16.08  fof(f562,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|hskp12|hskp13)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f153,f246])).
% 114.23/16.08  fof(f575,plain,(
% 114.23/16.08    c0_1(a2087)|c3_1(a2087)|hskp12|hskp13|~hskp10),
% 114.23/16.08    inference(resolution,[status(thm)],[f562,f46])).
% 114.23/16.08  fof(f583,plain,(
% 114.23/16.08    c0_1(a2087)|hskp12|hskp13|~hskp10),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f575,f48])).
% 114.23/16.08  fof(f587,plain,(
% 114.23/16.08    ![X0,X1,X2]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|c2_1(X2)|~c1_1(X2)|~c3_1(X2))),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f210,f246])).
% 114.23/16.08  fof(f596,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|c2_1(a2074)|~c1_1(a2074)|~hskp4)),
% 114.23/16.08    inference(resolution,[status(thm)],[f587,f23])).
% 114.23/16.08  fof(f601,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|~c1_1(a2074)|~hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f596,f24])).
% 114.23/16.08  fof(f633,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp8)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f211,f246])).
% 114.23/16.08  fof(f643,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c3_1(a2087)|~c2_1(a2087)|hskp8|~hskp10)),
% 114.23/16.08    inference(resolution,[status(thm)],[f633,f47])).
% 114.23/16.08  fof(f652,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|~c2_1(a2087)|hskp8|~hskp10)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f643,f48])).
% 114.23/16.08  fof(f670,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c1_1(X0)|~c3_1(X0)|hskp28|hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f158,f246])).
% 114.23/16.08  fof(f671,plain,(
% 114.23/16.08    c0_1(a2077)|~c1_1(a2077)|hskp28|hskp4|~hskp29),
% 114.23/16.08    inference(resolution,[status(thm)],[f670,f124])).
% 114.23/16.08  fof(f678,plain,(
% 114.23/16.08    c0_1(a2076)|~c1_1(a2076)|hskp28|hskp4|~hskp5),
% 114.23/16.08    inference(resolution,[status(thm)],[f670,f27])).
% 114.23/16.08  fof(f681,plain,(
% 114.23/16.08    c0_1(a2068)|~c1_1(a2068)|hskp28|hskp4|~hskp0),
% 114.23/16.08    inference(resolution,[status(thm)],[f670,f6])).
% 114.23/16.08  fof(f682,plain,(
% 114.23/16.08    c0_1(a2077)|hskp28|hskp4|~hskp29),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f671,f122])).
% 114.23/16.08  fof(f684,plain,(
% 114.23/16.08    ~c1_1(a2076)|hskp28|hskp4|~hskp5),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f678,f28])).
% 114.23/16.08  fof(f685,plain,(
% 114.23/16.08    ~c1_1(a2068)|hskp28|hskp4|~hskp0),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f681,f7])).
% 114.23/16.08  fof(f692,plain,(
% 114.23/16.08    hskp28|hskp4|~hskp5),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f684,f26])).
% 114.23/16.08  fof(f713,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp27|hskp29)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f163,f246])).
% 114.23/16.08  fof(f719,plain,(
% 114.23/16.08    c0_1(a2104)|~c2_1(a2104)|hskp27|hskp29|~hskp16),
% 114.23/16.08    inference(resolution,[status(thm)],[f713,f70])).
% 114.23/16.08  fof(f726,plain,(
% 114.23/16.08    ~c2_1(a2104)|hskp27|hskp29|~hskp16),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f719,f71])).
% 114.23/16.08  fof(f729,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(X1)|~c0_1(X1)|~c1_1(X1)|hskp9)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f213,f246])).
% 114.23/16.08  fof(f739,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(a2079)|~c0_1(a2079)|hskp9|~hskp7)),
% 114.23/16.08    inference(resolution,[status(thm)],[f729,f35])).
% 114.23/16.08  fof(f750,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(a2079)|hskp9|~hskp7)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f739,f34])).
% 114.23/16.08  fof(f752,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|hskp9)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f214,f246])).
% 114.23/16.08  fof(f762,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(a2070)|~c0_1(a2070)|hskp9|~hskp1)),
% 114.23/16.08    inference(resolution,[status(thm)],[f752,f11])).
% 114.23/16.08  fof(f767,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|~c0_1(a2070)|hskp9|~hskp1)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f762,f12])).
% 114.23/16.08  fof(f785,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|c1_1(X1)|c2_1(X1)|~c3_1(X1)|hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f216,f246])).
% 114.23/16.08  fof(f796,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|c1_1(a2068)|c2_1(a2068)|hskp4|~hskp0)),
% 114.23/16.08    inference(resolution,[status(thm)],[f785,f6])).
% 114.23/16.08  fof(f800,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|c1_1(a2068)|hskp4|~hskp0)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f796,f8])).
% 114.23/16.08  fof(f801,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp11|hskp0)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f164,f246])).
% 114.23/16.08  fof(f806,plain,(
% 114.23/16.08    c0_1(a2140)|~c2_1(a2140)|hskp11|hskp0|~hskp22),
% 114.23/16.08    inference(resolution,[status(thm)],[f801,f95])).
% 114.23/16.08  fof(f813,plain,(
% 114.23/16.08    ~c2_1(a2140)|hskp11|hskp0|~hskp22),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f806,f96])).
% 114.23/16.08  fof(f816,plain,(
% 114.23/16.08    hskp11|hskp0|~hskp22),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f813,f94])).
% 114.23/16.08  fof(f829,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp10)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f217,f246])).
% 114.23/16.08  fof(f832,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|~c0_1(a2069)|~c2_1(a2069)|hskp10|~hskp26)),
% 114.23/16.08    inference(resolution,[status(thm)],[f829,f112])).
% 114.23/16.08  fof(f843,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|~c2_1(a2069)|hskp10|~hskp26)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f832,f110])).
% 114.23/16.08  fof(f846,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f218,f246])).
% 114.23/16.08  fof(f847,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c0_1(a2077)|~c2_1(a2077)|hskp4|~hskp29)),
% 114.23/16.08    inference(resolution,[status(thm)],[f846,f124])).
% 114.23/16.08  fof(f849,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c0_1(a2069)|~c2_1(a2069)|hskp4|~hskp26)),
% 114.23/16.08    inference(resolution,[status(thm)],[f846,f112])).
% 114.23/16.08  fof(f858,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c0_1(a2077)|hskp4|~hskp29)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f847,f123])).
% 114.23/16.08  fof(f860,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c2_1(a2069)|hskp4|~hskp26)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f849,f110])).
% 114.23/16.08  fof(f966,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c0_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp1)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f220,f246])).
% 114.23/16.08  fof(f975,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c0_1(a2082)|~c2_1(a2082)|hskp1|~hskp8)),
% 114.23/16.08    inference(resolution,[status(thm)],[f966,f38])).
% 114.23/16.08  fof(f1006,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|~c2_1(a2082)|hskp1|~hskp8)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f975,f40])).
% 114.23/16.08  fof(f1060,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp1|hskp8)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f173,f246])).
% 114.23/16.08  fof(f1067,plain,(
% 114.23/16.08    c3_1(a2110)|~c0_1(a2110)|hskp1|hskp8|~hskp17),
% 114.23/16.08    inference(resolution,[status(thm)],[f1060,f76])).
% 114.23/16.08  fof(f1071,plain,(
% 114.23/16.08    c3_1(a2093)|~c0_1(a2093)|hskp1|hskp8|~hskp11),
% 114.23/16.08    inference(resolution,[status(thm)],[f1060,f51])).
% 114.23/16.08  fof(f1072,plain,(
% 114.23/16.08    c3_1(a2087)|~c0_1(a2087)|hskp1|hskp8|~hskp10),
% 114.23/16.08    inference(resolution,[status(thm)],[f1060,f47])).
% 114.23/16.08  fof(f1082,plain,(
% 114.23/16.08    c3_1(a2110)|hskp1|hskp8|~hskp17),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1067,f74])).
% 114.23/16.08  fof(f1083,plain,(
% 114.23/16.08    ~c0_1(a2093)|hskp1|hskp8|~hskp11),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1071,f52])).
% 114.23/16.08  fof(f1084,plain,(
% 114.23/16.08    ~c0_1(a2087)|hskp1|hskp8|~hskp10),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1072,f48])).
% 114.23/16.08  fof(f1109,plain,(
% 114.23/16.08    hskp1|hskp8|~hskp11),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1083,f50])).
% 114.23/16.08  fof(f1168,plain,(
% 114.23/16.08    ![X0,X1,X2]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|c2_1(X2)|~c1_1(X2)|~c3_1(X2))),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f223,f246])).
% 114.23/16.08  fof(f1180,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|c2_1(a2074)|~c1_1(a2074)|~hskp4)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1168,f23])).
% 114.23/16.08  fof(f1186,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|~c1_1(a2074)|~hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1180,f24])).
% 114.23/16.08  fof(f1217,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp11|hskp19)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f174,f246])).
% 114.23/16.08  fof(f1224,plain,(
% 114.23/16.08    c3_1(a2110)|~c0_1(a2110)|hskp11|hskp19|~hskp17),
% 114.23/16.08    inference(resolution,[status(thm)],[f1217,f76])).
% 114.23/16.08  fof(f1240,plain,(
% 114.23/16.08    c3_1(a2110)|hskp11|hskp19|~hskp17),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1224,f74])).
% 114.23/16.08  fof(f1328,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|~c0_1(X0)|~c3_1(X0)|hskp11|hskp10)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f178,f246])).
% 114.23/16.08  fof(f1335,plain,(
% 114.23/16.08    c1_1(a2149)|~c0_1(a2149)|hskp11|hskp10|~hskp23),
% 114.23/16.08    inference(resolution,[status(thm)],[f1328,f99])).
% 114.23/16.08  fof(f1349,plain,(
% 114.23/16.08    ~c0_1(a2149)|hskp11|hskp10|~hskp23),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1335,f100])).
% 114.23/16.08  fof(f1355,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|~c1_1(X0)|~c2_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp11)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f225,f246])).
% 114.23/16.08  fof(f1367,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c1_1(X0)|~c2_1(X0)|c3_1(a2087)|~c2_1(a2087)|hskp11|~hskp10)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1355,f47])).
% 114.23/16.08  fof(f1377,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c1_1(X0)|~c2_1(X0)|~c2_1(a2087)|hskp11|~hskp10)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1367,f48])).
% 114.23/16.08  fof(f1425,plain,(
% 114.23/16.08    hskp11|hskp10|~hskp23),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1349,f98])).
% 114.23/16.08  fof(f1426,plain,(
% 114.23/16.08    hskp11|hskp10|hskp17|hskp1),
% 114.23/16.08    inference(resolution,[status(thm)],[f1425,f195])).
% 114.23/16.08  fof(f1428,plain,(
% 114.23/16.08    hskp11|hskp10|hskp1|c3_1(a2110)|hskp11|hskp19),
% 114.23/16.08    inference(resolution,[status(thm)],[f1426,f1240])).
% 114.23/16.08  fof(f1429,plain,(
% 114.23/16.08    hskp11|hskp10|hskp1|c3_1(a2110)|hskp1|hskp8),
% 114.23/16.08    inference(resolution,[status(thm)],[f1426,f1082])).
% 114.23/16.08  fof(f1430,plain,(
% 114.23/16.08    hskp11|hskp10|hskp1|c3_1(a2110)|hskp19),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f1428])).
% 114.23/16.08  fof(f1431,plain,(
% 114.23/16.08    hskp11|hskp10|hskp1|c3_1(a2110)|hskp8),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f1429])).
% 114.23/16.08  fof(f1432,plain,(
% 114.23/16.08    hskp10|hskp1|c3_1(a2110)|hskp8),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1431,f1109])).
% 114.23/16.08  fof(f1460,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8|c1_1(a2110)|~c0_1(a2110)|hskp11|hskp10),
% 114.23/16.08    inference(resolution,[status(thm)],[f1432,f1328])).
% 114.23/16.08  fof(f1483,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8|c1_1(a2110)|~c0_1(a2110)|hskp11),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f1460])).
% 114.23/16.08  fof(f1484,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8|c1_1(a2110)|~c0_1(a2110)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1483,f1109])).
% 114.23/16.08  fof(f1523,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8|c1_1(a2110)|~hskp17),
% 114.23/16.08    inference(resolution,[status(thm)],[f1484,f74])).
% 114.23/16.08  fof(f1525,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8|~hskp17),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1523,f76])).
% 114.23/16.08  fof(f1526,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8|hskp11|hskp10|hskp1),
% 114.23/16.08    inference(resolution,[status(thm)],[f1525,f1426])).
% 114.23/16.08  fof(f1528,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8|hskp11),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f1526])).
% 114.23/16.08  fof(f1529,plain,(
% 114.23/16.08    hskp10|hskp1|hskp8),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1528,f1109])).
% 114.23/16.08  fof(f1530,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|c2_1(X1)|c3_1(X1)|~c0_1(X1)|hskp16)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f229,f246])).
% 114.23/16.08  fof(f1534,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|c3_1(a2099)|~c0_1(a2099)|hskp16|~hskp15)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1530,f67])).
% 114.23/16.08  fof(f1549,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|~c0_1(a2099)|hskp16|~hskp15)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1534,f68])).
% 114.23/16.08  fof(f1552,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|~c0_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp26)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f230,f246])).
% 114.23/16.08  fof(f1564,plain,(
% 114.23/16.08    ![X0]: (c0_1(a2140)|~c2_1(a2140)|~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26|~hskp22)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1552,f95])).
% 114.23/16.08  fof(f1566,plain,(
% 114.23/16.08    ![X0]: (c0_1(a2084)|~c2_1(a2084)|~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26|~hskp9)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1552,f43])).
% 114.23/16.08  fof(f1572,plain,(
% 114.23/16.08    ![X0]: (~c2_1(a2140)|~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26|~hskp22)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1564,f96])).
% 114.23/16.08  fof(f1574,plain,(
% 114.23/16.08    ![X0]: (c0_1(a2084)|~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26|~hskp9)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1566,f42])).
% 114.23/16.08  fof(f1576,plain,(
% 114.23/16.08    ~c0_1(a2087)|hskp1|hskp8),
% 114.23/16.08    inference(backward_subsumption_resolution,[status(thm)],[f1084,f1529])).
% 114.23/16.08  fof(f1579,plain,(
% 114.23/16.08    hskp1|hskp8|hskp12|hskp13|~hskp10),
% 114.23/16.08    inference(resolution,[status(thm)],[f1576,f583])).
% 114.23/16.08  fof(f1582,plain,(
% 114.23/16.08    hskp1|hskp8|hskp12|hskp13),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1579,f1529])).
% 114.23/16.08  fof(f1585,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp7|hskp15)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f181,f246])).
% 114.23/16.08  fof(f1593,plain,(
% 114.23/16.08    c1_1(a2149)|~c2_1(a2149)|hskp7|hskp15|~hskp23),
% 114.23/16.08    inference(resolution,[status(thm)],[f1585,f99])).
% 114.23/16.08  fof(f1604,plain,(
% 114.23/16.08    ~c2_1(a2149)|hskp7|hskp15|~hskp23),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1593,f100])).
% 114.23/16.08  fof(f1615,plain,(
% 114.23/16.08    ~c2_1(a2149)|hskp7|hskp15),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1604,f193])).
% 114.23/16.08  fof(f1625,plain,(
% 114.23/16.08    ![X0,X1]: (c1_1(X0)|c2_1(X0)|~c0_1(X0)|~c0_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp26)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f231,f246])).
% 114.23/16.08  fof(f1638,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c2_1(X0)|~c0_1(X0)|~c0_1(a2084)|~c2_1(a2084)|hskp26|~hskp9)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1625,f43])).
% 114.23/16.08  fof(f1649,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c2_1(X0)|~c0_1(X0)|~c0_1(a2084)|hskp26|~hskp9)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1638,f42])).
% 114.23/16.08  fof(f1673,plain,(
% 114.23/16.08    ![X0,X1]: (c1_1(X0)|c2_1(X0)|~c3_1(X0)|~c1_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp8)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f233,f246])).
% 114.23/16.08  fof(f1678,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c2_1(X0)|~c3_1(X0)|~c1_1(a2077)|~c2_1(a2077)|hskp8|~hskp29)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1673,f124])).
% 114.23/16.08  fof(f1692,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c2_1(X0)|~c3_1(X0)|~c2_1(a2077)|hskp8|~hskp29)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1678,f122])).
% 114.23/16.08  fof(f1709,plain,(
% 114.23/16.08    ![X0,X1]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|c1_1(X1)|~c2_1(X1)|~c3_1(X1)|hskp26)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f234,f246])).
% 114.23/16.08  fof(f1722,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|c1_1(a2084)|~c2_1(a2084)|hskp26|~hskp9)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1709,f43])).
% 114.23/16.08  fof(f1730,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|~c2_1(a2084)|hskp26|~hskp9)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1722,f44])).
% 114.23/16.08  fof(f1753,plain,(
% 114.23/16.08    ![X0,X1]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|c2_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp3)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f235,f246])).
% 114.23/16.08  fof(f1768,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|c2_1(a2074)|~c1_1(a2074)|hskp3|~hskp4)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1753,f23])).
% 114.23/16.08  fof(f1770,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|c2_1(a2068)|~c1_1(a2068)|hskp3|~hskp0)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1753,f6])).
% 114.23/16.08  fof(f1773,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|~c1_1(a2074)|hskp3|~hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1768,f24])).
% 114.23/16.08  fof(f1775,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|~c1_1(a2068)|hskp3|~hskp0)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1770,f8])).
% 114.23/16.08  fof(f1892,plain,(
% 114.23/16.08    ![X0,X1]: (c1_1(X0)|~c0_1(X0)|~c3_1(X0)|c2_1(X1)|c3_1(X1)|~c1_1(X1)|hskp17)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f237,f246])).
% 114.23/16.08  fof(f1942,plain,(
% 114.23/16.08    ![X0,X1]: (c1_1(X0)|~c2_1(X0)|~c3_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|hskp3)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f239,f246])).
% 114.23/16.08  fof(f1958,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|~c2_1(X0)|~c3_1(X0)|c2_1(a2070)|~c0_1(a2070)|hskp3|~hskp1)),
% 114.23/16.08    inference(resolution,[status(thm)],[f1942,f11])).
% 114.23/16.08  fof(f1963,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|~c2_1(X0)|~c3_1(X0)|~c0_1(a2070)|hskp3|~hskp1)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f1958,f12])).
% 114.23/16.08  fof(f2059,plain,(
% 114.23/16.08    ![X0,X1]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|c2_1(X1)|~c1_1(X1)|~c3_1(X1)|hskp5)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f242,f246])).
% 114.23/16.08  fof(f2074,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|c2_1(a2074)|~c1_1(a2074)|hskp5|~hskp4)),
% 114.23/16.08    inference(resolution,[status(thm)],[f2059,f23])).
% 114.23/16.08  fof(f2076,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|c2_1(a2068)|~c1_1(a2068)|hskp5|~hskp0)),
% 114.23/16.08    inference(resolution,[status(thm)],[f2059,f6])).
% 114.23/16.08  fof(f2079,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|~c1_1(a2074)|hskp5|~hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2074,f24])).
% 114.23/16.08  fof(f2081,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|~c1_1(a2068)|hskp5|~hskp0)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2076,f8])).
% 114.23/16.08  fof(f2152,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c3_1(X0)|hskp7|hskp16)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f189,f246])).
% 114.23/16.08  fof(f2153,plain,(
% 114.23/16.08    ~c0_1(a2149)|~c3_1(a2149)|hskp7|hskp16|hskp7|hskp15),
% 114.23/16.08    inference(resolution,[status(thm)],[f2152,f1615])).
% 114.23/16.08  fof(f2161,plain,(
% 114.23/16.08    ~c0_1(a2074)|~c3_1(a2074)|hskp7|hskp16|~hskp4),
% 114.23/16.08    inference(resolution,[status(thm)],[f2152,f24])).
% 114.23/16.08  fof(f2162,plain,(
% 114.23/16.08    ~c0_1(a2070)|~c3_1(a2070)|hskp7|hskp16|~hskp1),
% 114.23/16.08    inference(resolution,[status(thm)],[f2152,f12])).
% 114.23/16.08  fof(f2169,plain,(
% 114.23/16.08    ~c0_1(a2149)|~c3_1(a2149)|hskp7|hskp16|hskp15),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f2153])).
% 114.23/16.08  fof(f2172,plain,(
% 114.23/16.08    ~c0_1(a2074)|hskp7|hskp16|~hskp4),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2161,f23])).
% 114.23/16.08  fof(f2173,plain,(
% 114.23/16.08    ~c3_1(a2070)|hskp7|hskp16|~hskp1),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2162,f10])).
% 114.23/16.08  fof(f2174,plain,(
% 114.23/16.08    ![X0,X1]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|c3_1(X1)|~c1_1(X1)|~c2_1(X1)|hskp12)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f243,f246])).
% 114.23/16.08  fof(f2182,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|c3_1(a2160)|~c2_1(a2160)|hskp12|~hskp24)),
% 114.23/16.08    inference(resolution,[status(thm)],[f2174,f102])).
% 114.23/16.08  fof(f2202,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|~c2_1(a2160)|hskp12|~hskp24)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2182,f104])).
% 114.23/16.08  fof(f2211,plain,(
% 114.23/16.08    ![X0,X1]: (c2_1(X0)|~c0_1(X0)|~c3_1(X0)|c3_1(X1)|~c0_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f244,f246])).
% 114.23/16.08  fof(f2221,plain,(
% 114.23/16.08    ![X0]: (~c0_1(a2070)|~c3_1(a2070)|c3_1(X0)|~c0_1(X0)|~c2_1(X0)|hskp4|~hskp1)),
% 114.23/16.08    inference(resolution,[status(thm)],[f2211,f12])).
% 114.23/16.08  fof(f2230,plain,(
% 114.23/16.08    ![X0]: (~c3_1(a2070)|c3_1(X0)|~c0_1(X0)|~c2_1(X0)|hskp4|~hskp1)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2221,f10])).
% 114.23/16.08  fof(f2231,plain,(
% 114.23/16.08    ![X0]: (~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp7|hskp4)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f190,f246])).
% 114.23/16.08  fof(f2235,plain,(
% 114.23/16.08    ~c0_1(a2077)|~c2_1(a2077)|hskp7|hskp4|~hskp29),
% 114.23/16.08    inference(resolution,[status(thm)],[f2231,f122])).
% 114.23/16.08  fof(f2236,plain,(
% 114.23/16.08    ~c0_1(a2075)|~c2_1(a2075)|hskp7|hskp4|~hskp28),
% 114.23/16.08    inference(resolution,[status(thm)],[f2231,f119])).
% 114.23/16.08  fof(f2260,plain,(
% 114.23/16.08    ~c0_1(a2077)|hskp7|hskp4|~hskp29),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2235,f123])).
% 114.23/16.08  fof(f2261,plain,(
% 114.23/16.08    ~c2_1(a2075)|hskp7|hskp4|~hskp28),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2236,f118])).
% 114.23/16.08  fof(f2269,plain,(
% 114.23/16.08    hskp7|hskp16|~hskp1),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2173,f11])).
% 114.23/16.08  fof(f2271,plain,(
% 114.23/16.08    ~c0_1(a2077)|hskp7|hskp4|hskp5|hskp3),
% 114.23/16.08    inference(resolution,[status(thm)],[f2260,f198])).
% 114.23/16.08  fof(f2273,plain,(
% 114.23/16.08    hskp7|hskp4|~hskp28),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2261,f120])).
% 114.23/16.08  fof(f2275,plain,(
% 114.23/16.08    hskp7|hskp4|hskp4|~hskp5),
% 114.23/16.08    inference(resolution,[status(thm)],[f2273,f692])).
% 114.23/16.08  fof(f2276,plain,(
% 114.23/16.08    hskp7|hskp4|hskp5|~hskp3),
% 114.23/16.08    inference(resolution,[status(thm)],[f2273,f424])).
% 114.23/16.08  fof(f2277,plain,(
% 114.23/16.08    hskp7|hskp4|~hskp5),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f2275])).
% 114.23/16.08  fof(f2306,plain,(
% 114.23/16.08    hskp7|hskp4|~hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2276,f2277])).
% 114.23/16.08  fof(f2405,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c2_1(X0)|hskp0|~hskp29)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f293,f123])).
% 114.23/16.08  fof(f2407,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c2_1(X0)|hskp0|hskp5|hskp3)),
% 114.23/16.08    inference(resolution,[status(thm)],[f2405,f198])).
% 114.23/16.08  fof(f2408,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c2_1(X0)|hskp0|hskp3)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2407,f316])).
% 114.23/16.08  fof(f2495,plain,(
% 114.23/16.08    ~c0_1(a2077)|hskp7|hskp4|hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2271,f2277])).
% 114.23/16.08  fof(f2496,plain,(
% 114.23/16.08    hskp7|hskp4|hskp3|hskp28|hskp4|~hskp29),
% 114.23/16.08    inference(resolution,[status(thm)],[f2495,f682])).
% 114.23/16.08  fof(f2499,plain,(
% 114.23/16.08    hskp7|hskp4|hskp3|hskp28|~hskp29),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f2496])).
% 114.23/16.08  fof(f2500,plain,(
% 114.23/16.08    hskp7|hskp4|hskp28|~hskp29),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2499,f2306])).
% 114.23/16.08  fof(f2504,plain,(
% 114.23/16.08    hskp7|hskp4|~hskp29),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2500,f2273])).
% 114.23/16.08  fof(f2506,plain,(
% 114.23/16.08    hskp7|hskp4|hskp5|hskp3),
% 114.23/16.08    inference(resolution,[status(thm)],[f2504,f198])).
% 114.23/16.08  fof(f2507,plain,(
% 114.23/16.08    hskp7|hskp4|hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2506,f2277])).
% 114.23/16.08  fof(f2508,plain,(
% 114.23/16.08    c0_1(a2074)|hskp27|hskp7),
% 114.23/16.08    inference(backward_subsumption_resolution,[status(thm)],[f509,f2510])).
% 114.23/16.08  fof(f2509,plain,(
% 114.23/16.08    ~c0_1(a2074)|hskp7|hskp16),
% 114.23/16.08    inference(backward_subsumption_resolution,[status(thm)],[f2172,f2510])).
% 114.23/16.08  fof(f2510,plain,(
% 114.23/16.08    hskp7|hskp4),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2507,f2306])).
% 114.23/16.08  fof(f2513,plain,(
% 114.23/16.08    hskp7|hskp16|hskp27|hskp7),
% 114.23/16.08    inference(resolution,[status(thm)],[f2509,f2508])).
% 114.23/16.08  fof(f2514,plain,(
% 114.23/16.08    hskp7|hskp16|hskp0|~hskp4),
% 114.23/16.08    inference(resolution,[status(thm)],[f2509,f280])).
% 114.23/16.08  fof(f2516,plain,(
% 114.23/16.08    hskp7|hskp16|hskp27),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f2513])).
% 114.23/16.08  fof(f2517,plain,(
% 114.23/16.08    hskp7|hskp16|hskp0),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2514,f2510])).
% 114.23/16.08  fof(f2518,plain,(
% 114.23/16.08    c2_1(a2104)|hskp27|hskp7),
% 114.23/16.08    inference(backward_subsumption_resolution,[status(thm)],[f507,f2516])).
% 114.23/16.08  fof(f2538,plain,(
% 114.23/16.08    hskp7|hskp0|~c2_1(a2104)|hskp27|hskp29),
% 114.23/16.08    inference(resolution,[status(thm)],[f2517,f726])).
% 114.23/16.08  fof(f2542,plain,(
% 114.23/16.08    hskp7|~c2_1(a2104)|hskp27|hskp29),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2538,f511])).
% 114.23/16.08  fof(f2635,plain,(
% 114.23/16.08    hskp7|hskp27|hskp29),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2542,f2518])).
% 114.23/16.08  fof(f2810,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c3_1(X0)|hskp4|~hskp10)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f401,f48])).
% 114.23/16.08  fof(f2811,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|c3_1(X0)|hskp4|hskp1|hskp8)),
% 114.23/16.08    inference(resolution,[status(thm)],[f2810,f1529])).
% 114.23/16.08  fof(f2812,plain,(
% 114.23/16.08    ![X0]: (c1_1(X0)|c3_1(X0)|hskp4|hskp1|hskp8)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f2811,f1060])).
% 114.23/16.08  fof(f3011,plain,(
% 114.23/16.08    c0_1(a2072)|c3_1(a2072)|hskp5|hskp4|c0_1(a2072)|c3_1(a2072)|~hskp3),
% 114.23/16.08    inference(resolution,[status(thm)],[f442,f19])).
% 114.23/16.08  fof(f3052,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|hskp5|hskp4|c0_1(X0)|c1_1(X0)|c3_1(X0))),
% 114.23/16.08    inference(factoring,[status(thm)],[f442])).
% 114.23/16.08  fof(f3081,plain,(
% 114.23/16.08    c0_1(a2072)|c3_1(a2072)|hskp5|hskp4|~hskp3),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f3011])).
% 114.23/16.08  fof(f3082,plain,(
% 114.23/16.08    c3_1(a2072)|hskp5|hskp4|~hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3081,f18])).
% 114.23/16.08  fof(f3107,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c3_1(X0)|hskp5|hskp4|c1_1(X0))),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f3052])).
% 114.23/16.08  fof(f3126,plain,(
% 114.23/16.08    hskp5|hskp4|~hskp3),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3082,f20])).
% 114.23/16.08  fof(f3433,plain,(
% 114.23/16.08    c3_1(a2087)|hskp4|hskp1|hskp8|~hskp10),
% 114.23/16.08    inference(resolution,[status(thm)],[f2812,f47])).
% 114.23/16.08  fof(f3449,plain,(
% 114.23/16.08    hskp4|hskp1|hskp8|~hskp10),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3433,f48])).
% 114.23/16.08  fof(f3459,plain,(
% 114.23/16.08    hskp4|hskp1|hskp8),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3449,f1529])).
% 114.23/16.08  fof(f3522,plain,(
% 114.23/16.08    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp29|~hskp13)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f478,f58])).
% 114.23/16.08  fof(f3702,plain,(
% 114.23/16.08    ~c0_1(a2149)|hskp7|hskp16|hskp15|~hskp23),
% 114.23/16.08    inference(resolution,[status(thm)],[f2169,f99])).
% 114.23/16.08  fof(f3703,plain,(
% 114.23/16.08    hskp7|hskp16|hskp15|~hskp23),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3702,f98])).
% 114.23/16.08  fof(f3705,plain,(
% 114.23/16.08    hskp7|hskp16|hskp15),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3703,f193])).
% 114.23/16.08  fof(f3890,plain,(
% 114.23/16.08    ![X0,X1]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|c2_1(X1)|c3_1(X1)|~c1_1(X1)|~hskp9)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f544,f42])).
% 114.23/16.08  fof(f3967,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|hskp7|~hskp29|hskp0|~hskp29)),
% 114.23/16.08    inference(resolution,[status(thm)],[f557,f277])).
% 114.23/16.08  fof(f3970,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|hskp7|~hskp29|hskp0)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f3967])).
% 114.23/16.08  fof(f3971,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c3_1(X0)|hskp7|~hskp29|hskp0)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3970,f265])).
% 114.23/16.08  fof(f3972,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|hskp7|~hskp27)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f558,f115])).
% 114.23/16.08  fof(f3983,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c3_1(X0)|hskp7|hskp0|hskp7|hskp27)),
% 114.23/16.08    inference(resolution,[status(thm)],[f3971,f2635])).
% 114.23/16.08  fof(f3986,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c3_1(X0)|hskp7|hskp0|hskp27)),
% 114.23/16.08    inference(duplicate_literals_removal,[status(thm)],[f3983])).
% 114.23/16.08  fof(f3987,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|~c3_1(X0)|hskp7|hskp27)),
% 114.23/16.08    inference(forward_subsumption_resolution,[status(thm)],[f3986,f511])).
% 114.23/16.08  fof(f3990,plain,(
% 114.23/16.08    ![X0]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|hskp7)),
% 114.23/16.08    inference(backward_subsumption_resolution,[status(thm)],[f3972,f3987])).
% 114.23/16.08  fof(f4049,plain,(
% 114.23/16.09    c0_1(a2104)|c1_1(a2104)|hskp7|~hskp16),
% 114.23/16.09    inference(resolution,[status(thm)],[f3990,f70])).
% 114.23/16.09  fof(f4058,plain,(
% 114.23/16.09    c1_1(a2104)|hskp7|~hskp16),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4049,f71])).
% 114.23/16.09  fof(f4071,plain,(
% 114.23/16.09    ~c0_1(a2074)|hskp7),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f2509,f4078])).
% 114.23/16.09  fof(f4072,plain,(
% 114.23/16.09    hskp7|~hskp1),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f2269,f4078])).
% 114.23/16.09  fof(f4076,plain,(
% 114.23/16.09    hskp7|hskp15),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f3705,f4078])).
% 114.23/16.09  fof(f4078,plain,(
% 114.23/16.09    hskp7|~hskp16),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4058,f72])).
% 114.23/16.09  fof(f4246,plain,(
% 114.23/16.09    ![X0,X1]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|~hskp4)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f601,f22])).
% 114.23/16.09  fof(f4304,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|hskp8|~hskp10)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f652,f46])).
% 114.23/16.09  fof(f4305,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|hskp8|hskp1|hskp8)),
% 114.23/16.09    inference(resolution,[status(thm)],[f4304,f1529])).
% 114.23/16.09  fof(f4306,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|hskp8|hskp1)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f4305])).
% 114.23/16.09  fof(f4320,plain,(
% 114.23/16.09    c0_1(a2095)|c2_1(a2095)|hskp8|hskp1|~hskp12),
% 114.23/16.09    inference(resolution,[status(thm)],[f4306,f54])).
% 114.23/16.09  fof(f4324,plain,(
% 114.23/16.09    c0_1(a2074)|c2_1(a2074)|hskp8|hskp1|~hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f4306,f22])).
% 114.23/16.09  fof(f4347,plain,(
% 114.23/16.09    c2_1(a2095)|hskp8|hskp1|~hskp12),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4320,f55])).
% 114.23/16.09  fof(f4349,plain,(
% 114.23/16.09    c0_1(a2074)|hskp8|hskp1|~hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4324,f24])).
% 114.23/16.09  fof(f4372,plain,(
% 114.23/16.09    hskp1|hskp8|hskp13),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f1582,f4373])).
% 114.23/16.09  fof(f4373,plain,(
% 114.23/16.09    hskp8|hskp1|~hskp12),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4347,f56])).
% 114.23/16.09  fof(f4385,plain,(
% 114.23/16.09    ![X0]: (hskp1|hskp8|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp29)),
% 114.23/16.09    inference(resolution,[status(thm)],[f4372,f3522])).
% 114.23/16.09  fof(f4391,plain,(
% 114.23/16.09    ![X0]: (hskp1|hskp8|c2_1(X0)|~c1_1(X0)|hskp29)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4385,f4306])).
% 114.23/16.09  fof(f4407,plain,(
% 114.23/16.09    c0_1(a2074)|hskp8|hskp1),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4349,f3459])).
% 114.23/16.09  fof(f4408,plain,(
% 114.23/16.09    hskp8|hskp1|hskp7),
% 114.23/16.09    inference(resolution,[status(thm)],[f4407,f4071])).
% 114.23/16.09  fof(f4409,plain,(
% 114.23/16.09    hskp8|hskp7),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4408,f4072])).
% 114.23/16.09  fof(f4626,plain,(
% 114.23/16.09    hskp1|hskp8|c2_1(a2074)|hskp29|~hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f4391,f22])).
% 114.23/16.09  fof(f4647,plain,(
% 114.23/16.09    hskp1|hskp8|hskp29|~hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4626,f24])).
% 114.23/16.09  fof(f4663,plain,(
% 114.23/16.09    hskp1|hskp8|hskp29),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f4647,f3459])).
% 114.23/16.09  fof(f4751,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|hskp9|~hskp1)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f767,f10])).
% 114.23/16.09  fof(f5154,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|hskp10|~hskp26)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f843,f111])).
% 114.23/16.09  fof(f5250,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|hskp4|~hskp29|hskp0|~hskp29)),
% 114.23/16.09    inference(resolution,[status(thm)],[f858,f277])).
% 114.23/16.09  fof(f5254,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|hskp4|~hskp29|hskp0)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f5250])).
% 114.23/16.09  fof(f5255,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|hskp4|~hskp29|hskp0)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5254,f265])).
% 114.23/16.09  fof(f5288,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|hskp4|hskp0|hskp5|hskp3)),
% 114.23/16.09    inference(resolution,[status(thm)],[f5255,f198])).
% 114.23/16.09  fof(f5289,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|hskp4|hskp0|hskp3)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5288,f316])).
% 114.23/16.09  fof(f5347,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|hskp4|~hskp26)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f860,f111])).
% 114.23/16.09  fof(f5363,plain,(
% 114.23/16.09    c0_1(a2172)|hskp4|hskp0|hskp3|~hskp25),
% 114.23/16.09    inference(resolution,[status(thm)],[f5289,f106])).
% 114.23/16.09  fof(f5367,plain,(
% 114.23/16.09    c0_1(a2095)|hskp4|hskp0|hskp3|~hskp12),
% 114.23/16.09    inference(resolution,[status(thm)],[f5289,f54])).
% 114.23/16.09  fof(f5369,plain,(
% 114.23/16.09    c0_1(a2082)|hskp4|hskp0|hskp3|~hskp8),
% 114.23/16.09    inference(resolution,[status(thm)],[f5289,f38])).
% 114.23/16.09  fof(f5375,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|hskp4|hskp0|hskp3|c0_1(X0)|c3_1(X0)|hskp5|hskp4)),
% 114.23/16.09    inference(resolution,[status(thm)],[f5289,f3107])).
% 114.23/16.09  fof(f5392,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|~hskp25),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5363,f107])).
% 114.23/16.09  fof(f5393,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|~hskp12),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5367,f55])).
% 114.23/16.09  fof(f5395,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|~hskp8),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5369,f40])).
% 114.23/16.09  fof(f5398,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|hskp4|hskp0|hskp3|c3_1(X0)|hskp5)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f5375])).
% 114.23/16.09  fof(f5399,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|hskp4|hskp0|c3_1(X0)|hskp5)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5398,f3126])).
% 114.23/16.09  fof(f5411,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|hskp12|hskp18),
% 114.23/16.09    inference(resolution,[status(thm)],[f5392,f200])).
% 114.23/16.09  fof(f5414,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|hskp4|hskp1),
% 114.23/16.09    inference(resolution,[status(thm)],[f5395,f3459])).
% 114.23/16.09  fof(f5416,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|hskp1),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f5414])).
% 114.23/16.09  fof(f5445,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|hskp18),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5411,f5393])).
% 114.23/16.09  fof(f5454,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|hskp5|hskp4|hskp22),
% 114.23/16.09    inference(resolution,[status(thm)],[f5445,f445])).
% 114.23/16.09  fof(f5461,plain,(
% 114.23/16.09    hskp4|hskp0|hskp3|hskp5|hskp22),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f5454])).
% 114.23/16.09  fof(f5462,plain,(
% 114.23/16.09    hskp4|hskp0|hskp5|hskp22),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5461,f3126])).
% 114.23/16.09  fof(f5466,plain,(
% 114.23/16.09    hskp4|hskp0|hskp22),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5462,f316])).
% 114.23/16.09  fof(f5731,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|hskp4|hskp0|c3_1(X0))),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5399,f316])).
% 114.23/16.09  fof(f5755,plain,(
% 114.23/16.09    hskp4|hskp0|c3_1(a2072)|~hskp3),
% 114.23/16.09    inference(resolution,[status(thm)],[f5731,f18])).
% 114.23/16.09  fof(f5766,plain,(
% 114.23/16.09    hskp4|hskp0|~hskp3),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5755,f20])).
% 114.23/16.09  fof(f5770,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|hskp1|~hskp8)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1006,f39])).
% 114.23/16.09  fof(f5772,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|hskp1|hskp7)),
% 114.23/16.09    inference(resolution,[status(thm)],[f5770,f4409])).
% 114.23/16.09  fof(f5775,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|hskp7)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f5772,f4072])).
% 114.23/16.09  fof(f5781,plain,(
% 114.23/16.09    hskp4|hskp0|hskp1),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f5416,f5766])).
% 114.23/16.09  fof(f5784,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|hskp4|hskp0)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f5289,f5766])).
% 114.23/16.09  fof(f5804,plain,(
% 114.23/16.09    hskp0|hskp1|~c0_1(a2074)|hskp22),
% 114.23/16.09    inference(resolution,[status(thm)],[f5781,f336])).
% 114.23/16.09  fof(f6034,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|hskp4|hskp0|c0_1(X0)|c2_1(X0)|hskp0|hskp3)),
% 114.23/16.09    inference(resolution,[status(thm)],[f5784,f2408])).
% 114.23/16.09  fof(f6054,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|hskp4|hskp0|c2_1(X0)|hskp3)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f6034])).
% 114.23/16.09  fof(f6055,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|hskp4|hskp0|c2_1(X0))),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f6054,f5766])).
% 114.23/16.09  fof(f6081,plain,(
% 114.23/16.09    hskp0|hskp1|hskp22|hskp0|~hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f5804,f280])).
% 114.23/16.09  fof(f6086,plain,(
% 114.23/16.09    hskp0|hskp1|hskp22|~hskp4),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f6081])).
% 114.23/16.09  fof(f6087,plain,(
% 114.23/16.09    hskp0|hskp1|hskp22),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f6086,f5466])).
% 114.23/16.09  fof(f6096,plain,(
% 114.23/16.09    hskp0|hskp1|hskp11|hskp0),
% 114.23/16.09    inference(resolution,[status(thm)],[f6087,f816])).
% 114.23/16.09  fof(f6103,plain,(
% 114.23/16.09    hskp0|hskp1|hskp11),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f6096])).
% 114.23/16.09  fof(f6106,plain,(
% 114.23/16.09    hskp0|hskp1|hskp1|hskp8),
% 114.23/16.09    inference(resolution,[status(thm)],[f6103,f1109])).
% 114.23/16.09  fof(f6108,plain,(
% 114.23/16.09    hskp0|hskp1|hskp8),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f6106])).
% 114.23/16.09  fof(f6113,plain,(
% 114.23/16.09    ![X0]: (hskp0|hskp1|c0_1(X0)|c3_1(X0)|~c2_1(X0)|hskp1)),
% 114.23/16.09    inference(resolution,[status(thm)],[f6108,f5770])).
% 114.23/16.09  fof(f6116,plain,(
% 114.23/16.09    ![X0]: (hskp0|hskp1|c0_1(X0)|c3_1(X0)|~c2_1(X0))),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f6113])).
% 114.23/16.09  fof(f6185,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|c1_1(a2068)|hskp4)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f800,f6055])).
% 114.23/16.09  fof(f7268,plain,(
% 114.23/16.09    ![X0,X1]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1)|~hskp4)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1186,f22])).
% 114.23/16.09  fof(f7299,plain,(
% 114.23/16.09    hskp0|hskp1|c0_1(a2082)|c3_1(a2082)|~hskp8),
% 114.23/16.09    inference(resolution,[status(thm)],[f6116,f39])).
% 114.23/16.09  fof(f7326,plain,(
% 114.23/16.09    hskp0|hskp1|c3_1(a2082)|~hskp8),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f7299,f40])).
% 114.23/16.09  fof(f7357,plain,(
% 114.23/16.09    hskp0|hskp1|c3_1(a2082)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f7326,f6108])).
% 114.23/16.09  fof(f7395,plain,(
% 114.23/16.09    hskp0|hskp1|c0_1(a2082)|~c1_1(a2082)|hskp0),
% 114.23/16.09    inference(resolution,[status(thm)],[f7357,f265])).
% 114.23/16.09  fof(f7410,plain,(
% 114.23/16.09    hskp0|hskp1|c0_1(a2082)|~c1_1(a2082)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f7395])).
% 114.23/16.09  fof(f7413,plain,(
% 114.23/16.09    hskp0|hskp1|c0_1(a2082)|~hskp8),
% 114.23/16.09    inference(resolution,[status(thm)],[f7410,f38])).
% 114.23/16.09  fof(f7432,plain,(
% 114.23/16.09    hskp0|hskp1|~hskp8),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f7413,f40])).
% 114.23/16.09  fof(f7445,plain,(
% 114.23/16.09    hskp0|hskp1),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f7432,f6108])).
% 114.23/16.09  fof(f7860,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp11|~hskp10)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1377,f46])).
% 114.23/16.09  fof(f7862,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp11|hskp1|hskp8)),
% 114.23/16.09    inference(resolution,[status(thm)],[f7860,f1529])).
% 114.23/16.09  fof(f7863,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|hskp11|hskp1|hskp8)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f7862,f4306])).
% 114.23/16.09  fof(f7864,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c1_1(X0)|hskp1|hskp8)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f7863,f1109])).
% 114.23/16.09  fof(f8819,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp16|~hskp15)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1549,f66])).
% 114.23/16.09  fof(f8820,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp16|hskp7)),
% 114.23/16.09    inference(resolution,[status(thm)],[f8819,f4076])).
% 114.23/16.09  fof(f8821,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c2_1(X0)|hskp16|hskp7)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f8820,f5775])).
% 114.23/16.09  fof(f8822,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|~c2_1(X0)|hskp7)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f8821,f4078])).
% 114.23/16.09  fof(f8854,plain,(
% 114.23/16.09    c0_1(a2082)|hskp7|~hskp8),
% 114.23/16.09    inference(resolution,[status(thm)],[f8822,f39])).
% 114.23/16.09  fof(f8885,plain,(
% 114.23/16.09    hskp7|~hskp8),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f8854,f40])).
% 114.23/16.09  fof(f8909,plain,(
% 114.23/16.09    c2_1(a2079)|hskp22),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f335,f8916])).
% 114.23/16.09  fof(f8910,plain,(
% 114.23/16.09    ~c3_1(a2079)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f36,f8916])).
% 114.23/16.09  fof(f8911,plain,(
% 114.23/16.09    c1_1(a2079)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f35,f8916])).
% 114.23/16.09  fof(f8912,plain,(
% 114.23/16.09    c0_1(a2079)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f34,f8916])).
% 114.23/16.09  fof(f8913,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|c2_1(a2079)|hskp9)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f750,f8916])).
% 114.23/16.09  fof(f8916,plain,(
% 114.23/16.09    hskp7),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f8885,f4409])).
% 114.23/16.09  fof(f8989,plain,(
% 114.23/16.09    ![X0]: (~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26|~hskp22)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1572,f94])).
% 114.23/16.09  fof(f9593,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c2_1(X0)|~c3_1(X0)|hskp8|~hskp29)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1692,f123])).
% 114.23/16.09  fof(f9594,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c2_1(X0)|~c3_1(X0)|hskp8|hskp1|hskp8)),
% 114.23/16.09    inference(resolution,[status(thm)],[f9593,f4663])).
% 114.23/16.09  fof(f9597,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c2_1(X0)|~c3_1(X0)|hskp8|hskp1)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f9594])).
% 114.23/16.09  fof(f9645,plain,(
% 114.23/16.09    c1_1(a2068)|c2_1(a2068)|hskp8|hskp1|~hskp0),
% 114.23/16.09    inference(resolution,[status(thm)],[f9597,f6])).
% 114.23/16.09  fof(f9655,plain,(
% 114.23/16.09    c1_1(a2068)|hskp8|hskp1|~hskp0),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9645,f8])).
% 114.23/16.09  fof(f9671,plain,(
% 114.23/16.09    c1_1(a2068)|hskp8|hskp1),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9655,f7445])).
% 114.23/16.09  fof(f9672,plain,(
% 114.23/16.09    hskp8|hskp1|c0_1(a2068)|hskp1|hskp8),
% 114.23/16.09    inference(resolution,[status(thm)],[f9671,f7864])).
% 114.23/16.09  fof(f9685,plain,(
% 114.23/16.09    hskp8|hskp1|c0_1(a2068)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f9672])).
% 114.23/16.09  fof(f9694,plain,(
% 114.23/16.09    hskp8|hskp1|~hskp0),
% 114.23/16.09    inference(resolution,[status(thm)],[f9685,f7])).
% 114.23/16.09  fof(f9697,plain,(
% 114.23/16.09    hskp8|hskp1),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9694,f7445])).
% 114.23/16.09  fof(f9698,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|hskp1)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f5770,f9697])).
% 114.23/16.09  fof(f9763,plain,(
% 114.23/16.09    c0_1(a2072)|c3_1(a2072)|hskp1|hskp26|hskp1|~hskp3),
% 114.23/16.09    inference(resolution,[status(thm)],[f9698,f314])).
% 114.23/16.09  fof(f9772,plain,(
% 114.23/16.09    c0_1(a2122)|c3_1(a2122)|hskp1|~hskp19),
% 114.23/16.09    inference(resolution,[status(thm)],[f9698,f82])).
% 114.23/16.09  fof(f9775,plain,(
% 114.23/16.09    c0_1(a2087)|c3_1(a2087)|hskp1|~hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f9698,f46])).
% 114.23/16.09  fof(f9800,plain,(
% 114.23/16.09    c0_1(a2072)|c3_1(a2072)|hskp1|hskp26|~hskp3),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f9763])).
% 114.23/16.09  fof(f9801,plain,(
% 114.23/16.09    c3_1(a2072)|hskp1|hskp26|~hskp3),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9800,f18])).
% 114.23/16.09  fof(f9806,plain,(
% 114.23/16.09    c3_1(a2122)|hskp1|~hskp19),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9772,f83])).
% 114.23/16.09  fof(f9808,plain,(
% 114.23/16.09    c0_1(a2087)|hskp1|~hskp10),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9775,f48])).
% 114.23/16.09  fof(f9819,plain,(
% 114.23/16.09    hskp11|hskp10|hskp1|c3_1(a2110)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f1430,f9820])).
% 114.23/16.09  fof(f9820,plain,(
% 114.23/16.09    hskp1|~hskp19),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9806,f84])).
% 114.23/16.09  fof(f9874,plain,(
% 114.23/16.09    hskp1|hskp26|~hskp3),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f9801,f20])).
% 114.23/16.09  fof(f9894,plain,(
% 114.23/16.09    hskp11|hskp10|hskp1|c1_1(a2110)|~c0_1(a2110)|hskp11|hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f9819,f1328])).
% 114.23/16.09  fof(f9922,plain,(
% 114.23/16.09    hskp11|hskp10|hskp1|c1_1(a2110)|~c0_1(a2110)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f9894])).
% 114.23/16.09  fof(f9949,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp26|~hskp9)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1730,f42])).
% 114.23/16.09  fof(f10055,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp3|~hskp4)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1773,f22])).
% 114.23/16.09  fof(f10318,plain,(
% 114.23/16.09    hskp11|hskp10|hskp1|c1_1(a2110)|~hskp17),
% 114.23/16.09    inference(resolution,[status(thm)],[f9922,f74])).
% 114.23/16.09  fof(f10327,plain,(
% 114.23/16.09    hskp11|hskp10|hskp1|~hskp17),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f10318,f76])).
% 114.23/16.09  fof(f10330,plain,(
% 114.23/16.09    hskp11|hskp10|hskp1),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f10327,f1426])).
% 114.23/16.09  fof(f11572,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp3|~hskp1)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f1963,f10])).
% 114.23/16.09  fof(f11573,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp3|hskp0)),
% 114.23/16.09    inference(resolution,[status(thm)],[f11572,f7445])).
% 114.23/16.09  fof(f11604,plain,(
% 114.23/16.09    c1_1(a2140)|~c2_1(a2140)|hskp3|hskp0|~hskp22),
% 114.23/16.09    inference(resolution,[status(thm)],[f11573,f95])).
% 114.23/16.09  fof(f11617,plain,(
% 114.23/16.09    ~c2_1(a2140)|hskp3|hskp0|~hskp22),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f11604,f278])).
% 114.23/16.09  fof(f11669,plain,(
% 114.23/16.09    hskp3|hskp0|~hskp22),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f11617,f94])).
% 114.23/16.09  fof(f11678,plain,(
% 114.23/16.09    hskp3|hskp0|hskp4|hskp0),
% 114.23/16.09    inference(resolution,[status(thm)],[f11669,f5466])).
% 114.23/16.09  fof(f11690,plain,(
% 114.23/16.09    hskp3|hskp0|hskp4),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f11678])).
% 114.23/16.09  fof(f11691,plain,(
% 114.23/16.09    hskp0|hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f11690,f5766])).
% 114.23/16.09  fof(f11696,plain,(
% 114.23/16.09    ~c1_1(a2068)|hskp28|hskp4),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f685,f11691])).
% 114.23/16.09  fof(f11697,plain,(
% 114.23/16.09    c0_1(a2074)|hskp0),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f280,f11691])).
% 114.23/16.09  fof(f11707,plain,(
% 114.23/16.09    hskp0|~c0_1(a2074)|hskp22),
% 114.23/16.09    inference(resolution,[status(thm)],[f11691,f336])).
% 114.23/16.09  fof(f11809,plain,(
% 114.23/16.09    hskp3|hskp0),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f11669,f11813])).
% 114.23/16.09  fof(f11813,plain,(
% 114.23/16.09    hskp0|hskp22),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f11707,f11697])).
% 114.23/16.09  fof(f11831,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|~c1_1(a2068)|hskp3)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f1775,f11809])).
% 114.23/16.09  fof(f12240,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp5|~hskp4)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f2079,f22])).
% 114.23/16.09  fof(f12241,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp5|hskp0)),
% 114.23/16.09    inference(resolution,[status(thm)],[f12240,f11691])).
% 114.23/16.09  fof(f12242,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp0)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f12241,f316])).
% 114.23/16.09  fof(f12265,plain,(
% 114.23/16.09    c2_1(a2074)|~c0_1(a2074)|hskp0|~hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f12242,f22])).
% 114.23/16.09  fof(f12288,plain,(
% 114.23/16.09    ~c0_1(a2074)|hskp0|~hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f12265,f24])).
% 114.23/16.09  fof(f12308,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|~c1_1(a2068)|hskp5)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f2081,f12242])).
% 114.23/16.09  fof(f12399,plain,(
% 114.23/16.09    hskp0),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f11691,f12400])).
% 114.23/16.09  fof(f12400,plain,(
% 114.23/16.09    hskp0|~hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f12288,f11697])).
% 114.23/16.09  fof(f12401,plain,(
% 114.23/16.09    ~c2_1(a2068)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f8,f12399])).
% 114.23/16.09  fof(f12402,plain,(
% 114.23/16.09    ~c0_1(a2068)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f7,f12399])).
% 114.23/16.09  fof(f12403,plain,(
% 114.23/16.09    c3_1(a2068)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f6,f12399])).
% 114.23/16.09  fof(f12507,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp12|~hskp24)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f2202,f103])).
% 114.23/16.09  fof(f12508,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp12|hskp12|hskp10)),
% 114.23/16.09    inference(resolution,[status(thm)],[f12507,f199])).
% 114.23/16.09  fof(f12510,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp12|hskp10)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f12508])).
% 114.23/16.09  fof(f12627,plain,(
% 114.23/16.09    c2_1(a2079)|~c0_1(a2079)|hskp12|hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f12510,f8911])).
% 114.23/16.09  fof(f12645,plain,(
% 114.23/16.09    c2_1(a2074)|~c0_1(a2074)|hskp12|hskp10|~hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f12510,f22])).
% 114.23/16.09  fof(f12660,plain,(
% 114.23/16.09    c2_1(a2079)|hskp12|hskp10),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f12627,f8912])).
% 114.23/16.09  fof(f12666,plain,(
% 114.23/16.09    ~c0_1(a2074)|hskp12|hskp10|~hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f12645,f24])).
% 114.23/16.09  fof(f13150,plain,(
% 114.23/16.09    ![X0]: (c3_1(X0)|~c0_1(X0)|~c2_1(X0)|hskp4|~hskp1)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f2230,f11])).
% 114.23/16.09  fof(f13336,plain,(
% 114.23/16.09    c0_1(a2068)|c2_1(a2068)|c1_1(a2068)|hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f6185,f12403])).
% 114.23/16.09  fof(f13351,plain,(
% 114.23/16.09    c2_1(a2068)|c1_1(a2068)|hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13336,f12402])).
% 114.23/16.09  fof(f13409,plain,(
% 114.23/16.09    hskp28|hskp4),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f11696,f13410])).
% 114.23/16.09  fof(f13410,plain,(
% 114.23/16.09    c1_1(a2068)|hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13351,f12401])).
% 114.23/16.09  fof(f13411,plain,(
% 114.23/16.09    ![X0]: (hskp4|c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp5)),
% 114.23/16.09    inference(resolution,[status(thm)],[f13410,f12308])).
% 114.23/16.09  fof(f13412,plain,(
% 114.23/16.09    hskp4|c0_1(a2068)|c2_1(a2068)|c2_1(a2079)|hskp9),
% 114.23/16.09    inference(resolution,[status(thm)],[f13410,f8913])).
% 114.23/16.09  fof(f13429,plain,(
% 114.23/16.09    ![X0]: (c2_1(X0)|~c0_1(X0)|~c1_1(X0)|hskp5)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13411,f12240])).
% 114.23/16.09  fof(f13430,plain,(
% 114.23/16.09    hskp4|c2_1(a2068)|c2_1(a2079)|hskp9),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13412,f12402])).
% 114.23/16.09  fof(f13621,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp3|hskp4)),
% 114.23/16.09    inference(resolution,[status(thm)],[f11831,f13410])).
% 114.23/16.09  fof(f13639,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp3)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13621,f10055])).
% 114.23/16.09  fof(f13882,plain,(
% 114.23/16.09    c3_1(a2093)|~c0_1(a2093)|hskp3|~hskp11),
% 114.23/16.09    inference(resolution,[status(thm)],[f13639,f51])).
% 114.23/16.09  fof(f13883,plain,(
% 114.23/16.09    c3_1(a2087)|~c0_1(a2087)|hskp3|~hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f13639,f47])).
% 114.23/16.09  fof(f13903,plain,(
% 114.23/16.09    ~c0_1(a2093)|hskp3|~hskp11),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13882,f52])).
% 114.23/16.09  fof(f13904,plain,(
% 114.23/16.09    ~c0_1(a2087)|hskp3|~hskp10),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13883,f48])).
% 114.23/16.09  fof(f14006,plain,(
% 114.23/16.09    hskp3|~hskp11),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13903,f50])).
% 114.23/16.09  fof(f14007,plain,(
% 114.23/16.09    hskp3|hskp10|hskp1),
% 114.23/16.09    inference(resolution,[status(thm)],[f14006,f10330])).
% 114.23/16.09  fof(f14008,plain,(
% 114.23/16.09    hskp3|hskp1|c0_1(a2087)|hskp1),
% 114.23/16.09    inference(resolution,[status(thm)],[f14007,f9808])).
% 114.23/16.09  fof(f14016,plain,(
% 114.23/16.09    hskp3|hskp1|c0_1(a2087)),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f14008])).
% 114.23/16.09  fof(f14022,plain,(
% 114.23/16.09    ~c0_1(a2087)|hskp3|hskp3|hskp1),
% 114.23/16.09    inference(resolution,[status(thm)],[f13904,f14007])).
% 114.23/16.09  fof(f14023,plain,(
% 114.23/16.09    ~c0_1(a2087)|hskp3|hskp1),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f14022])).
% 114.23/16.09  fof(f14067,plain,(
% 114.23/16.09    hskp1|hskp26),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f9874,f14069])).
% 114.23/16.09  fof(f14068,plain,(
% 114.23/16.09    ![X0]: (c1_1(X0)|~c2_1(X0)|~c3_1(X0)|hskp3)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f11572,f14069])).
% 114.23/16.09  fof(f14069,plain,(
% 114.23/16.09    hskp3|hskp1),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f14023,f14016])).
% 114.23/16.09  fof(f14093,plain,(
% 114.23/16.09    ![X0]: (hskp1|c0_1(X0)|c3_1(X0)|~c1_1(X0)|hskp4)),
% 114.23/16.09    inference(resolution,[status(thm)],[f14067,f5347])).
% 114.23/16.09  fof(f14094,plain,(
% 114.23/16.09    ![X0]: (hskp1|c0_1(X0)|c2_1(X0)|~c3_1(X0)|hskp10)),
% 114.23/16.09    inference(resolution,[status(thm)],[f14067,f5154])).
% 114.23/16.09  fof(f14426,plain,(
% 114.23/16.09    c1_1(a2084)|~c2_1(a2084)|hskp3|~hskp9),
% 114.23/16.09    inference(resolution,[status(thm)],[f14068,f43])).
% 114.23/16.09  fof(f14441,plain,(
% 114.23/16.09    ~c2_1(a2084)|hskp3|~hskp9),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f14426,f44])).
% 114.23/16.09  fof(f14462,plain,(
% 114.23/16.09    hskp3|~hskp9),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f14441,f42])).
% 114.23/16.09  fof(f14636,plain,(
% 114.23/16.09    hskp4|c2_1(a2079)|hskp9),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f13430,f12401])).
% 114.23/16.09  fof(f15124,plain,(
% 114.23/16.09    hskp1|c0_1(a2068)|~c3_1(a2068)|hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f14094,f12401])).
% 114.23/16.09  fof(f15141,plain,(
% 114.23/16.09    hskp1|~c3_1(a2068)|hskp10),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15124,f12402])).
% 114.23/16.09  fof(f15147,plain,(
% 114.23/16.09    hskp1|hskp10),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15141,f12403])).
% 114.23/16.09  fof(f15153,plain,(
% 114.23/16.09    ![X0]: (hskp1|c0_1(X0)|c1_1(X0)|c3_1(X0)|hskp4)),
% 114.23/16.09    inference(resolution,[status(thm)],[f15147,f2810])).
% 114.23/16.09  fof(f15156,plain,(
% 114.23/16.09    ![X0]: (hskp1|c0_1(X0)|c3_1(X0)|hskp4)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15153,f14093])).
% 114.23/16.09  fof(f15514,plain,(
% 114.23/16.09    hskp1|c3_1(a2072)|hskp4|~hskp3),
% 114.23/16.09    inference(resolution,[status(thm)],[f15156,f18])).
% 114.23/16.09  fof(f15521,plain,(
% 114.23/16.09    hskp1|hskp4|~hskp3),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15514,f20])).
% 114.23/16.09  fof(f15522,plain,(
% 114.23/16.09    ![X0]: (c3_1(X0)|~c0_1(X0)|~c2_1(X0)|hskp4)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f13150,f15524])).
% 114.23/16.09  fof(f15524,plain,(
% 114.23/16.09    hskp1|hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15521,f14069])).
% 114.23/16.09  fof(f15535,plain,(
% 114.23/16.09    ![X0,X1]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c0_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f846,f15522])).
% 114.23/16.09  fof(f15536,plain,(
% 114.23/16.09    c3_1(a2079)|~c2_1(a2079)|hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f15522,f8912])).
% 114.23/16.09  fof(f15560,plain,(
% 114.23/16.09    ~c2_1(a2079)|hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15536,f8910])).
% 114.23/16.09  fof(f15573,plain,(
% 114.23/16.09    hskp4|hskp9),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f14636,f15560])).
% 114.23/16.09  fof(f15580,plain,(
% 114.23/16.09    hskp4|hskp12|hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f15560,f12660])).
% 114.23/16.09  fof(f15583,plain,(
% 114.23/16.09    hskp4|hskp22),
% 114.23/16.09    inference(resolution,[status(thm)],[f15560,f8909])).
% 114.23/16.09  fof(f15612,plain,(
% 114.23/16.09    hskp4|hskp3),
% 114.23/16.09    inference(resolution,[status(thm)],[f15573,f14462])).
% 114.23/16.09  fof(f15647,plain,(
% 114.23/16.09    ![X0]: (hskp4|~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26)),
% 114.23/16.09    inference(resolution,[status(thm)],[f15583,f8989])).
% 114.23/16.09  fof(f15671,plain,(
% 114.23/16.09    ~c0_1(a2074)|hskp12|hskp10),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f12666,f15580])).
% 114.23/16.09  fof(f15695,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|~c2_1(a2075)|hskp4|~hskp28)),
% 114.23/16.09    inference(resolution,[status(thm)],[f15535,f118])).
% 114.23/16.09  fof(f15710,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|hskp4|~hskp28)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15695,f120])).
% 114.23/16.09  fof(f15909,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|hskp4|~hskp10)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f2810,f15912])).
% 114.23/16.09  fof(f15911,plain,(
% 114.23/16.09    ![X0,X1]: (c0_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1)|hskp4)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f380,f15912])).
% 114.23/16.09  fof(f15912,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c1_1(X0)|hskp4)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f15710,f13409])).
% 114.23/16.09  fof(f15983,plain,(
% 114.23/16.09    ![X0,X1]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|c1_1(X1)|c3_1(X1)|~c2_1(X1))),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f4246,f15911])).
% 114.23/16.09  fof(f16447,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|c1_1(a2087)|c3_1(a2087)|~hskp10)),
% 114.23/16.09    inference(resolution,[status(thm)],[f15983,f46])).
% 114.23/16.09  fof(f16467,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|c3_1(a2087)|~hskp10)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f16447,f47])).
% 114.23/16.09  fof(f16987,plain,(
% 114.23/16.09    hskp4|~c1_1(a2075)|~c2_1(a2075)|hskp26|~hskp28),
% 114.23/16.09    inference(resolution,[status(thm)],[f15647,f118])).
% 114.23/16.09  fof(f17000,plain,(
% 114.23/16.09    hskp4|~c2_1(a2075)|hskp26|~hskp28),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f16987,f119])).
% 114.23/16.09  fof(f17003,plain,(
% 114.23/16.09    hskp4|hskp26|~hskp28),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f17000,f120])).
% 114.23/16.09  fof(f17005,plain,(
% 114.23/16.09    hskp4|hskp26|hskp4),
% 114.23/16.09    inference(resolution,[status(thm)],[f17003,f13409])).
% 114.23/16.09  fof(f17006,plain,(
% 114.23/16.09    hskp4|hskp26),
% 114.23/16.09    inference(duplicate_literals_removal,[status(thm)],[f17005])).
% 114.23/16.09  fof(f17017,plain,(
% 114.23/16.09    ![X0]: (hskp4|c0_1(X0)|c2_1(X0)|~c3_1(X0)|hskp10)),
% 114.23/16.09    inference(resolution,[status(thm)],[f17006,f5154])).
% 114.23/16.09  fof(f17284,plain,(
% 114.23/16.09    hskp4|c0_1(a2068)|c2_1(a2068)|hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f17017,f12403])).
% 114.23/16.09  fof(f17291,plain,(
% 114.23/16.09    hskp4|c2_1(a2068)|hskp10),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f17284,f12402])).
% 114.23/16.09  fof(f17293,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|hskp4)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f15909,f17294])).
% 114.23/16.09  fof(f17294,plain,(
% 114.23/16.09    hskp4|hskp10),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f17291,f12401])).
% 114.23/16.09  fof(f17314,plain,(
% 114.23/16.09    ![X0,X1]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1))),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f7268,f17293])).
% 114.23/16.09  fof(f17336,plain,(
% 114.23/16.09    c3_1(a2072)|hskp4|~hskp3),
% 114.23/16.09    inference(resolution,[status(thm)],[f17293,f18])).
% 114.23/16.09  fof(f17342,plain,(
% 114.23/16.09    hskp4|~hskp3),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f17336,f20])).
% 114.23/16.09  fof(f17344,plain,(
% 114.23/16.09    ~c2_1(a2074)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f24,f17348])).
% 114.23/16.09  fof(f17345,plain,(
% 114.23/16.09    c3_1(a2074)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f23,f17348])).
% 114.23/16.09  fof(f17346,plain,(
% 114.23/16.09    c1_1(a2074)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f22,f17348])).
% 114.23/16.09  fof(f17348,plain,(
% 114.23/16.09    hskp4),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f17342,f15612])).
% 114.23/16.09  fof(f17411,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|c2_1(a2074)|~c0_1(a2074))),
% 114.23/16.09    inference(resolution,[status(thm)],[f17314,f17345])).
% 114.23/16.09  fof(f17425,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|~c2_1(X0)|~c0_1(a2074))),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f17411,f17344])).
% 114.23/16.09  fof(f20270,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|~hskp10)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f16467,f48])).
% 114.23/16.09  fof(f20272,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|c3_1(X0)|hskp1)),
% 114.23/16.09    inference(resolution,[status(thm)],[f20270,f15147])).
% 114.23/16.09  fof(f20273,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c3_1(X0)|hskp1)),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f20272,f9698])).
% 114.23/16.09  fof(f20308,plain,(
% 114.23/16.09    c3_1(a2072)|hskp1|~hskp3),
% 114.23/16.09    inference(resolution,[status(thm)],[f20273,f18])).
% 114.23/16.09  fof(f20321,plain,(
% 114.23/16.09    hskp1|~hskp3),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f20308,f20])).
% 114.23/16.09  fof(f20326,plain,(
% 114.23/16.09    ~c2_1(a2070)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f12,f20337])).
% 114.23/16.09  fof(f20327,plain,(
% 114.23/16.09    c3_1(a2070)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f11,f20337])).
% 114.23/16.09  fof(f20328,plain,(
% 114.23/16.09    c0_1(a2070)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f10,f20337])).
% 114.23/16.09  fof(f20334,plain,(
% 114.23/16.09    ![X0]: (c0_1(X0)|c2_1(X0)|~c1_1(X0)|hskp9)),
% 114.23/16.09    inference(backward_subsumption_resolution,[status(thm)],[f4751,f20337])).
% 114.23/16.09  fof(f20337,plain,(
% 114.23/16.09    hskp1),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f20321,f14069])).
% 114.23/16.09  fof(f20594,plain,(
% 114.23/16.09    c0_1(a2074)|c2_1(a2074)|hskp9),
% 114.23/16.09    inference(resolution,[status(thm)],[f20334,f17346])).
% 114.23/16.09  fof(f20618,plain,(
% 114.23/16.09    c0_1(a2095)|c2_1(a2095)|hskp9|~hskp12),
% 114.23/16.09    inference(resolution,[status(thm)],[f20334,f54])).
% 114.23/16.09  fof(f20640,plain,(
% 114.23/16.09    c0_1(a2074)|hskp9),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f20594,f17344])).
% 114.23/16.09  fof(f20649,plain,(
% 114.23/16.09    c2_1(a2095)|hskp9|~hskp12),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f20618,f55])).
% 114.23/16.09  fof(f20663,plain,(
% 114.23/16.09    ![X0]: (hskp9|c0_1(X0)|c3_1(X0)|~c2_1(X0))),
% 114.23/16.09    inference(resolution,[status(thm)],[f20640,f17425])).
% 114.23/16.09  fof(f20665,plain,(
% 114.23/16.09    hskp9|hskp12|hskp10),
% 114.23/16.09    inference(resolution,[status(thm)],[f20640,f15671])).
% 114.23/16.09  fof(f20673,plain,(
% 114.23/16.09    hskp9|c2_1(a2074)|~c1_1(a2074)|hskp5),
% 114.23/16.09    inference(resolution,[status(thm)],[f20640,f13429])).
% 114.23/16.09  fof(f20675,plain,(
% 114.23/16.09    hskp9|~c1_1(a2074)|hskp5),
% 114.23/16.09    inference(forward_subsumption_resolution,[status(thm)],[f20673,f17344])).
% 114.23/16.10  fof(f20815,plain,(
% 114.23/16.10    hskp9|hskp10),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f20665,f20816])).
% 114.23/16.10  fof(f20816,plain,(
% 114.23/16.10    hskp9|~hskp12),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f20649,f56])).
% 114.23/16.10  fof(f20821,plain,(
% 114.23/16.10    ![X0]: (hskp9|c0_1(X0)|c2_1(X0)|c3_1(X0))),
% 114.23/16.10    inference(resolution,[status(thm)],[f20815,f20270])).
% 114.23/16.10  fof(f20823,plain,(
% 114.23/16.10    ![X0]: (hskp9|c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp11)),
% 114.23/16.10    inference(resolution,[status(thm)],[f20815,f7860])).
% 114.23/16.10  fof(f20830,plain,(
% 114.23/16.10    ![X0]: (hskp9|c0_1(X0)|~c1_1(X0)|hskp11)),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f20823,f20334])).
% 114.23/16.10  fof(f20886,plain,(
% 114.23/16.10    hskp9|hskp5),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f20675,f17346])).
% 114.23/16.10  fof(f21328,plain,(
% 114.23/16.10    hskp9|c0_1(a2076)|hskp11|~hskp5),
% 114.23/16.10    inference(resolution,[status(thm)],[f20830,f26])).
% 114.23/16.10  fof(f21350,plain,(
% 114.23/16.10    hskp9|hskp11|~hskp5),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f21328,f28])).
% 114.23/16.10  fof(f21362,plain,(
% 114.23/16.10    hskp9|hskp11),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f21350,f20886])).
% 114.23/16.10  fof(f21363,plain,(
% 114.23/16.10    hskp9|hskp3),
% 114.23/16.10    inference(resolution,[status(thm)],[f21362,f14006])).
% 114.23/16.10  fof(f21366,plain,(
% 114.23/16.10    hskp3),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f21363,f14462])).
% 114.23/16.10  fof(f21421,plain,(
% 114.23/16.10    ~c3_1(a2072)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f20,f21366])).
% 114.23/16.10  fof(f21423,plain,(
% 114.23/16.10    ~c0_1(a2072)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f18,f21366])).
% 114.23/16.10  fof(f21924,plain,(
% 114.23/16.10    ![X0]: (hskp9|c0_1(X0)|c3_1(X0))),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f20821,f20663])).
% 114.23/16.10  fof(f21926,plain,(
% 114.23/16.10    hskp9|c3_1(a2072)),
% 114.23/16.10    inference(resolution,[status(thm)],[f21924,f21423])).
% 114.23/16.10  fof(f21952,plain,(
% 114.23/16.10    hskp9),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f21926,f21421])).
% 114.23/16.10  fof(f21955,plain,(
% 114.23/16.10    ~c1_1(a2084)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f44,f21952])).
% 114.23/16.10  fof(f21956,plain,(
% 114.23/16.10    c3_1(a2084)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f43,f21952])).
% 114.23/16.10  fof(f21962,plain,(
% 114.23/16.10    ![X0]: (c1_1(X0)|c3_1(X0)|~c0_1(X0)|hskp26)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f9949,f21952])).
% 114.23/16.10  fof(f21963,plain,(
% 114.23/16.10    ![X0]: (c1_1(X0)|c2_1(X0)|~c0_1(X0)|~c0_1(a2084)|hskp26)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f1649,f21952])).
% 114.23/16.10  fof(f21964,plain,(
% 114.23/16.10    ![X0]: (c0_1(a2084)|~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f1574,f21952])).
% 114.23/16.10  fof(f21967,plain,(
% 114.23/16.10    ![X0,X1]: (c0_1(X0)|c1_1(X0)|~c3_1(X0)|c2_1(X1)|c3_1(X1)|~c1_1(X1))),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f3890,f21952])).
% 114.23/16.10  fof(f22365,plain,(
% 114.23/16.10    c1_1(a2110)|c3_1(a2110)|hskp26|~hskp17),
% 114.23/16.10    inference(resolution,[status(thm)],[f21962,f74])).
% 114.23/16.10  fof(f22367,plain,(
% 114.23/16.10    c1_1(a2093)|c3_1(a2093)|hskp26|~hskp11),
% 114.23/16.10    inference(resolution,[status(thm)],[f21962,f50])).
% 114.23/16.10  fof(f22370,plain,(
% 114.23/16.10    c3_1(a2110)|hskp26|~hskp17),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f22365,f76])).
% 114.23/16.10  fof(f22372,plain,(
% 114.23/16.10    c3_1(a2093)|hskp26|~hskp11),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f22367,f51])).
% 114.23/16.10  fof(f22387,plain,(
% 114.23/16.10    hskp26|~hskp11),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f22372,f52])).
% 114.23/16.10  fof(f22400,plain,(
% 114.23/16.10    c0_1(a2084)|~c1_1(a2079)|~c2_1(a2079)|hskp26),
% 114.23/16.10    inference(resolution,[status(thm)],[f21964,f8912])).
% 114.23/16.10  fof(f22413,plain,(
% 114.23/16.10    c0_1(a2084)|~c2_1(a2079)|hskp26),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f22400,f8911])).
% 114.23/16.10  fof(f22632,plain,(
% 114.23/16.10    ![X0,X1]: (c1_1(X0)|~c3_1(X0)|c2_1(X1)|c3_1(X1)|~c1_1(X1)|hskp17)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f1892,f21967])).
% 114.23/16.10  fof(f22680,plain,(
% 114.23/16.10    ![X0]: (c1_1(a2084)|c2_1(X0)|c3_1(X0)|~c1_1(X0)|hskp17)),
% 114.23/16.10    inference(resolution,[status(thm)],[f22632,f21956])).
% 114.23/16.10  fof(f22699,plain,(
% 114.23/16.10    ![X0]: (c2_1(X0)|c3_1(X0)|~c1_1(X0)|hskp17)),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f22680,f21955])).
% 114.23/16.10  fof(f22706,plain,(
% 114.23/16.10    c0_1(a2084)|hskp26|hskp22),
% 114.23/16.10    inference(resolution,[status(thm)],[f22413,f8909])).
% 114.23/16.10  fof(f22723,plain,(
% 114.23/16.10    ![X0]: (hskp26|hskp22|c1_1(X0)|c2_1(X0)|~c0_1(X0)|hskp26)),
% 114.23/16.10    inference(resolution,[status(thm)],[f22706,f21963])).
% 114.23/16.10  fof(f22735,plain,(
% 114.23/16.10    ![X0]: (hskp26|hskp22|c1_1(X0)|c2_1(X0)|~c0_1(X0))),
% 114.23/16.10    inference(duplicate_literals_removal,[status(thm)],[f22723])).
% 114.23/16.10  fof(f22736,plain,(
% 114.23/16.10    ![X0]: (hskp26|hskp22|c2_1(X0)|~c0_1(X0))),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f22735,f318])).
% 114.23/16.10  fof(f22803,plain,(
% 114.23/16.10    hskp26|hskp22|c2_1(a2070)),
% 114.23/16.10    inference(resolution,[status(thm)],[f22736,f20328])).
% 114.23/16.10  fof(f22824,plain,(
% 114.23/16.10    hskp26|hskp22),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f22803,f20326])).
% 114.23/16.10  fof(f22827,plain,(
% 114.23/16.10    ![X0]: (~c0_1(X0)|~c1_1(X0)|~c2_1(X0)|hskp26)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f8989,f22824])).
% 114.23/16.10  fof(f23394,plain,(
% 114.23/16.10    c2_1(a2079)|c3_1(a2079)|hskp17),
% 114.23/16.10    inference(resolution,[status(thm)],[f22699,f8911])).
% 114.23/16.10  fof(f23430,plain,(
% 114.23/16.10    c2_1(a2079)|hskp17),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f23394,f8910])).
% 114.23/16.10  fof(f23621,plain,(
% 114.23/16.10    ~c1_1(a2079)|~c2_1(a2079)|hskp26),
% 114.23/16.10    inference(resolution,[status(thm)],[f22827,f8912])).
% 114.23/16.10  fof(f23639,plain,(
% 114.23/16.10    ~c2_1(a2079)|hskp26),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f23621,f8911])).
% 114.23/16.10  fof(f23644,plain,(
% 114.23/16.10    hskp26|hskp17),
% 114.23/16.10    inference(resolution,[status(thm)],[f23639,f23430])).
% 114.23/16.10  fof(f23666,plain,(
% 114.23/16.10    c3_1(a2110)|hskp26),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f22370,f23644])).
% 114.23/16.10  fof(f23730,plain,(
% 114.23/16.10    hskp26|c1_1(a2110)|~c0_1(a2110)|hskp11|hskp10),
% 114.23/16.10    inference(resolution,[status(thm)],[f23666,f1328])).
% 114.23/16.10  fof(f23740,plain,(
% 114.23/16.10    hskp26|c1_1(a2110)|~c0_1(a2110)|hskp10),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f23730,f22387])).
% 114.23/16.10  fof(f24722,plain,(
% 114.23/16.10    hskp26|c1_1(a2110)|hskp10|~hskp17),
% 114.23/16.10    inference(resolution,[status(thm)],[f23740,f74])).
% 114.23/16.10  fof(f24723,plain,(
% 114.23/16.10    hskp26|hskp10|~hskp17),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f24722,f76])).
% 114.23/16.10  fof(f24724,plain,(
% 114.23/16.10    ![X0]: (c0_1(X0)|c2_1(X0)|~c3_1(X0)|hskp10)),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f5154,f24726])).
% 114.23/16.10  fof(f24726,plain,(
% 114.23/16.10    hskp26|hskp10),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f24723,f23644])).
% 114.23/16.10  fof(f24813,plain,(
% 114.23/16.10    c0_1(a2068)|c2_1(a2068)|hskp10),
% 114.23/16.10    inference(resolution,[status(thm)],[f24724,f12403])).
% 114.23/16.10  fof(f24824,plain,(
% 114.23/16.10    c2_1(a2068)|hskp10),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f24813,f12402])).
% 114.23/16.10  fof(f24828,plain,(
% 114.23/16.10    ![X0]: (c0_1(X0)|c2_1(X0)|c3_1(X0))),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f20270,f24834])).
% 114.23/16.10  fof(f24834,plain,(
% 114.23/16.10    hskp10),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f24824,f12401])).
% 114.23/16.10  fof(f24886,plain,(
% 114.23/16.10    ![X0,X1]: (c0_1(X0)|c3_1(X0)|c2_1(X1)|~c0_1(X1)|~c3_1(X1))),
% 114.23/16.10    inference(backward_subsumption_resolution,[status(thm)],[f17314,f24828])).
% 114.23/16.10  fof(f25778,plain,(
% 114.23/16.10    ![X0]: (c0_1(X0)|c3_1(X0)|c2_1(a2070)|~c0_1(a2070))),
% 114.23/16.10    inference(resolution,[status(thm)],[f24886,f20327])).
% 114.23/16.10  fof(f25788,plain,(
% 114.23/16.10    ![X0]: (c0_1(X0)|c3_1(X0)|~c0_1(a2070))),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f25778,f20326])).
% 114.23/16.10  fof(f25853,plain,(
% 114.23/16.10    ![X0]: (c0_1(X0)|c3_1(X0))),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f25788,f20328])).
% 114.23/16.10  fof(f25855,plain,(
% 114.23/16.10    c3_1(a2072)),
% 114.23/16.10    inference(resolution,[status(thm)],[f25853,f21423])).
% 114.23/16.10  fof(f25874,plain,(
% 114.23/16.10    $false),
% 114.23/16.10    inference(forward_subsumption_resolution,[status(thm)],[f25855,f21421])).
% 114.23/16.10  % SZS output end CNFRefutation for theBenchmark.p
% 114.23/16.11  % Elapsed time: 15.589804 seconds
% 114.23/16.11  % CPU time: 122.762999 seconds
% 114.23/16.11  % Total memory used: 70.923 MB
% 114.23/16.11  % Net memory used: 67.009 MB
%------------------------------------------------------------------------------