%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN461-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 03:16:30 PM UTC 2026
% Result : Unsatisfiable 120.33s 16.16s
% Output : CNFRefutation 120.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 94
% Number of leaves : 124
% Syntax : Number of formulae : 1030 ( 21 unt; 0 def)
% Number of atoms : 4696 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 6521 (2855 ~;3666 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 24 prp; 0-1 aty)
% Number of functors : 22 ( 22 usr; 22 con; 0-0 aty)
% Number of variables : 454 ( 454 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,negated_conjecture,
( ndr1_0
| ~ hskp23 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
( ndr1_0
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
( ndr1_0
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
( ndr1_0
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
( ndr1_0
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
( ndr1_0
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
( ndr1_0
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
( ndr1_0
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
( ndr1_0
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
( ndr1_0
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
( ndr1_0
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
( ndr1_0
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
( ndr1_0
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
( ndr1_0
| ~ hskp7 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
( ndr1_0
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
( ndr1_0
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
( ndr1_0
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
( ndr1_0
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
( hskp24
| hskp17
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
( hskp14
| hskp1
| hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
( hskp2
| hskp13
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
( hskp16
| hskp1
| hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
( hskp14
| hskp21
| hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
( hskp19
| hskp21
| hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
( c0_1(a1190)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
( c1_1(a1190)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
( c3_1(a1190)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
( c1_1(a1182)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
( c2_1(a1182)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,negated_conjecture,
( c3_1(a1182)
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,negated_conjecture,
( c3_1(a1232)
| ~ hskp24 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
( c0_1(a1211)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,negated_conjecture,
( c3_1(a1211)
| ~ hskp22 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
( c2_1(a1207)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
( c3_1(a1207)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
( c1_1(a1205)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,negated_conjecture,
( c3_1(a1205)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
( c3_1(a1204)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,negated_conjecture,
( c0_1(a1200)
| ~ hskp17 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,negated_conjecture,
( c2_1(a1199)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,negated_conjecture,
( c2_1(a1195)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,negated_conjecture,
( c2_1(a1194)
| ~ hskp14 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,negated_conjecture,
( c1_1(a1192)
| ~ hskp13 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,negated_conjecture,
( c0_1(a1186)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,negated_conjecture,
( c1_1(a1180)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,negated_conjecture,
( c1_1(a1178)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,negated_conjecture,
( c2_1(a1178)
| ~ hskp6 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f74,negated_conjecture,
( c0_1(a1174)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,negated_conjecture,
( c1_1(a1174)
| ~ hskp3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,negated_conjecture,
( c2_1(a1172)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,negated_conjecture,
( c3_1(a1172)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,negated_conjecture,
( c1_1(a1169)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,negated_conjecture,
( c0_1(a1168)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,negated_conjecture,
( c1_1(a1168)
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,negated_conjecture,
( ~ hskp24
| ~ c0_1(a1232) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,negated_conjecture,
( ~ hskp24
| ~ c1_1(a1232) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,negated_conjecture,
( ~ hskp23
| ~ c0_1(a1218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,negated_conjecture,
( ~ hskp23
| ~ c1_1(a1218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,negated_conjecture,
( ~ hskp23
| ~ c3_1(a1218) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,negated_conjecture,
( ~ hskp22
| ~ c1_1(a1211) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f87,negated_conjecture,
( ~ hskp21
| ~ c1_1(a1207) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,negated_conjecture,
( ~ hskp20
| ~ c2_1(a1205) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
( ~ hskp19
| ~ c1_1(a1204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
( ~ hskp19
| ~ c2_1(a1204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,negated_conjecture,
( ~ hskp17
| ~ c1_1(a1200) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,negated_conjecture,
( ~ hskp17
| ~ c2_1(a1200) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,negated_conjecture,
( ~ hskp16
| ~ c0_1(a1199) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,negated_conjecture,
( ~ hskp16
| ~ c3_1(a1199) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
( ~ hskp15
| ~ c1_1(a1195) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
( ~ hskp15
| ~ c3_1(a1195) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f98,negated_conjecture,
( ~ hskp14
| ~ c0_1(a1194) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f99,negated_conjecture,
( ~ hskp14
| ~ c1_1(a1194) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,negated_conjecture,
( ~ hskp13
| ~ c0_1(a1192) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,negated_conjecture,
( ~ hskp13
| ~ c2_1(a1192) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,negated_conjecture,
( ~ hskp12
| ~ c0_1(a1187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f103,negated_conjecture,
( ~ hskp12
| ~ c2_1(a1187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f104,negated_conjecture,
( ~ hskp12
| ~ c3_1(a1187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,negated_conjecture,
( ~ hskp11
| ~ c2_1(a1186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,negated_conjecture,
( ~ hskp11
| ~ c3_1(a1186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,negated_conjecture,
( ~ hskp8
| ~ c0_1(a1180) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,negated_conjecture,
( ~ hskp8
| ~ c3_1(a1180) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f113,negated_conjecture,
( ~ hskp7
| ~ c1_1(a1179) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f114,negated_conjecture,
( ~ hskp7
| ~ c2_1(a1179) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f115,negated_conjecture,
( ~ hskp7
| ~ c3_1(a1179) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,negated_conjecture,
( ~ hskp6
| ~ c3_1(a1178) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f119,negated_conjecture,
( ~ hskp3
| ~ c3_1(a1174) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f120,negated_conjecture,
( ~ hskp2
| ~ c0_1(a1172) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f121,negated_conjecture,
( ~ hskp1
| ~ c2_1(a1169) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,negated_conjecture,
( ~ hskp1
| ~ c3_1(a1169) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,negated_conjecture,
( ~ hskp0
| ~ c2_1(a1168) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,negated_conjecture,
! [U] :
( hskp3
| hskp0
| c3_1(U)
| c1_1(U)
| c0_1(U)
| ~ ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,negated_conjecture,
! [U] :
( hskp6
| hskp3
| c3_1(U)
| c2_1(U)
| c0_1(U)
| ~ ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,negated_conjecture,
! [U] :
( hskp15
| hskp14
| c3_1(U)
| c2_1(U)
| c1_1(U)
| ~ ndr1_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,negated_conjecture,
! [U] :
( hskp0
| c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,negated_conjecture,
! [U] :
( hskp17
| hskp22
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,negated_conjecture,
! [U] :
( hskp14
| hskp22
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f133,negated_conjecture,
! [U] :
( hskp23
| hskp19
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,negated_conjecture,
! [U] :
( hskp19
| hskp13
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f137,negated_conjecture,
! [U] :
( hskp12
| hskp20
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f138,negated_conjecture,
! [U] :
( hskp12
| hskp21
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,negated_conjecture,
! [U] :
( hskp14
| hskp22
| c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f142,negated_conjecture,
! [U] :
( hskp2
| hskp22
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,negated_conjecture,
! [U,V] :
( hskp0
| c2_1(V)
| c1_1(V)
| c0_1(V)
| c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f145,negated_conjecture,
! [U,V] :
( hskp0
| c3_1(V)
| c1_1(V)
| c0_1(V)
| c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f148,negated_conjecture,
! [U,V] :
( hskp26
| c3_1(V)
| c2_1(V)
| c1_1(V)
| c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,negated_conjecture,
! [U,V] :
( hskp1
| c2_1(V)
| c1_1(V)
| c0_1(V)
| c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f150,negated_conjecture,
! [U,V] :
( hskp0
| c2_1(V)
| c1_1(V)
| c0_1(V)
| c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f152,negated_conjecture,
! [U,V] :
( hskp7
| c2_1(V)
| c0_1(V)
| c2_1(U)
| c1_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f153,negated_conjecture,
! [U,V] :
( hskp6
| c3_1(V)
| c2_1(V)
| c1_1(V)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f156,negated_conjecture,
! [U,V] :
( hskp1
| c2_1(V)
| c0_1(V)
| c1_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f158,negated_conjecture,
! [U,V] :
( hskp3
| c3_1(V)
| c0_1(V)
| c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f159,negated_conjecture,
! [U,V] :
( hskp11
| c0_1(V)
| c2_1(U)
| c1_1(U)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,negated_conjecture,
! [U,V] :
( c2_1(V)
| c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,negated_conjecture,
! [U,V] :
( hskp11
| c2_1(V)
| c1_1(V)
| c3_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f163,negated_conjecture,
! [U,V] :
( hskp17
| c1_1(V)
| c3_1(U)
| c2_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f164,negated_conjecture,
! [U,V] :
( hskp12
| c0_1(V)
| c1_1(U)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f167,negated_conjecture,
! [U,V] :
( hskp25
| c2_1(V)
| c3_1(U)
| ~ c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f168,negated_conjecture,
! [U,V,W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| c2_1(V)
| c0_1(V)
| c3_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,negated_conjecture,
! [U,V,W] :
( c3_1(W)
| c1_1(W)
| c0_1(W)
| c3_1(V)
| c0_1(V)
| c0_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f170,negated_conjecture,
! [U,V,W] :
( c1_1(W)
| c0_1(W)
| c1_1(V)
| c0_1(V)
| c3_1(U)
| ~ c2_1(W)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f171,negated_conjecture,
! [U,V,W] :
( c3_1(W)
| c2_1(W)
| c0_1(W)
| c1_1(V)
| c1_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,negated_conjecture,
! [U,V,W] :
( c2_1(W)
| c1_1(W)
| c1_1(V)
| c2_1(U)
| ~ c0_1(W)
| ~ c3_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,negated_conjecture,
! [U,V,W] :
( c0_1(W)
| c3_1(V)
| c3_1(U)
| ~ c3_1(W)
| ~ c1_1(W)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f183,plain,
( ndr1_0
| ~ hskp23 ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f184,plain,
( ndr1_0
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f185,plain,
( ndr1_0
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f186,plain,
( ndr1_0
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f187,plain,
( ndr1_0
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f189,plain,
( ndr1_0
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f190,plain,
( ndr1_0
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f191,plain,
( ndr1_0
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f192,plain,
( ndr1_0
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f193,plain,
( ndr1_0
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f194,plain,
( ndr1_0
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f195,plain,
( ndr1_0
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f198,plain,
( ndr1_0
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f199,plain,
( ndr1_0
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f200,plain,
( ndr1_0
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f203,plain,
( ndr1_0
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f204,plain,
( ndr1_0
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f205,plain,
( ndr1_0
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f206,plain,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f207,plain,
( hskp24
| hskp17
| hskp26 ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f208,plain,
( hskp14
| hskp1
| hskp0 ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f209,plain,
( hskp2
| hskp13
| hskp17 ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f210,plain,
( hskp16
| hskp1
| hskp17 ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f211,plain,
( hskp14
| hskp21
| hskp6 ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f212,plain,
( hskp19
| hskp21
| hskp8 ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f219,plain,
( c0_1(a1190)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f220,plain,
( c1_1(a1190)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f221,plain,
( c3_1(a1190)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f222,plain,
( c1_1(a1182)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f223,plain,
( c2_1(a1182)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f224,plain,
( c3_1(a1182)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f225,plain,
( c3_1(a1232)
| ~ hskp24 ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f226,plain,
( c0_1(a1211)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f227,plain,
( c3_1(a1211)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f228,plain,
( c2_1(a1207)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f229,plain,
( c3_1(a1207)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f230,plain,
( c1_1(a1205)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f231,plain,
( c3_1(a1205)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f232,plain,
( c3_1(a1204)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f235,plain,
( c0_1(a1200)
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f236,plain,
( c2_1(a1199)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f237,plain,
( c2_1(a1195)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f238,plain,
( c2_1(a1194)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f239,plain,
( c1_1(a1192)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f240,plain,
( c0_1(a1186)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f243,plain,
( c1_1(a1180)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f244,plain,
( c1_1(a1178)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f245,plain,
( c2_1(a1178)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f250,plain,
( c0_1(a1174)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f251,plain,
( c1_1(a1174)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f252,plain,
( c2_1(a1172)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f253,plain,
( c3_1(a1172)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f254,plain,
( c1_1(a1169)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f255,plain,
( c0_1(a1168)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f256,plain,
( c1_1(a1168)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f257,plain,
( ~ hskp24
| ~ c0_1(a1232) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f258,plain,
( ~ hskp24
| ~ c1_1(a1232) ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f259,plain,
( ~ hskp23
| ~ c0_1(a1218) ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f260,plain,
( ~ hskp23
| ~ c1_1(a1218) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f261,plain,
( ~ hskp23
| ~ c3_1(a1218) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f262,plain,
( ~ hskp22
| ~ c1_1(a1211) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f263,plain,
( ~ hskp21
| ~ c1_1(a1207) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f264,plain,
( ~ hskp20
| ~ c2_1(a1205) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f265,plain,
( ~ hskp19
| ~ c1_1(a1204) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f266,plain,
( ~ hskp19
| ~ c2_1(a1204) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f268,plain,
( ~ hskp17
| ~ c1_1(a1200) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f269,plain,
( ~ hskp17
| ~ c2_1(a1200) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f270,plain,
( ~ hskp16
| ~ c0_1(a1199) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f271,plain,
( ~ hskp16
| ~ c3_1(a1199) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f272,plain,
( ~ hskp15
| ~ c1_1(a1195) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f273,plain,
( ~ hskp15
| ~ c3_1(a1195) ),
inference(cnf_transformation,[status(thm)],[f97]) ).
fof(f274,plain,
( ~ hskp14
| ~ c0_1(a1194) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f275,plain,
( ~ hskp14
| ~ c1_1(a1194) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f276,plain,
( ~ hskp13
| ~ c0_1(a1192) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f277,plain,
( ~ hskp13
| ~ c2_1(a1192) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f278,plain,
( ~ hskp12
| ~ c0_1(a1187) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f279,plain,
( ~ hskp12
| ~ c2_1(a1187) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f280,plain,
( ~ hskp12
| ~ c3_1(a1187) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f281,plain,
( ~ hskp11
| ~ c2_1(a1186) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f282,plain,
( ~ hskp11
| ~ c3_1(a1186) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f287,plain,
( ~ hskp8
| ~ c0_1(a1180) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f288,plain,
( ~ hskp8
| ~ c3_1(a1180) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f289,plain,
( ~ hskp7
| ~ c1_1(a1179) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f290,plain,
( ~ hskp7
| ~ c2_1(a1179) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f291,plain,
( ~ hskp7
| ~ c3_1(a1179) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f292,plain,
( ~ hskp6
| ~ c3_1(a1178) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f295,plain,
( ~ hskp3
| ~ c3_1(a1174) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f296,plain,
( ~ hskp2
| ~ c0_1(a1172) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f297,plain,
( ~ hskp1
| ~ c2_1(a1169) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f298,plain,
( ~ hskp1
| ~ c3_1(a1169) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f299,plain,
( ~ hskp0
| ~ c2_1(a1168) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f300,plain,
( hskp3
| hskp0
| ! [U] :
( c3_1(U)
| c1_1(U)
| c0_1(U)
| ~ ndr1_0 ) ),
inference(miniscoping,[status(thm)],[f124]) ).
fof(f301,plain,
! [X0] :
( hskp3
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f300]) ).
fof(f302,plain,
( hskp6
| hskp3
| ! [U] :
( c3_1(U)
| c2_1(U)
| c0_1(U)
| ~ ndr1_0 ) ),
inference(miniscoping,[status(thm)],[f125]) ).
fof(f303,plain,
! [X0] :
( hskp6
| hskp3
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f302]) ).
fof(f304,plain,
( hskp15
| hskp14
| ! [U] :
( c3_1(U)
| c2_1(U)
| c1_1(U)
| ~ ndr1_0 ) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f305,plain,
! [X0] :
( hskp15
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f306,plain,
( hskp0
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f127]) ).
fof(f307,plain,
! [X0] :
( hskp0
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f312,plain,
( hskp17
| hskp22
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f313,plain,
! [X0] :
( hskp17
| hskp22
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f314,plain,
( hskp14
| hskp22
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f131]) ).
fof(f315,plain,
! [X0] :
( hskp14
| hskp22
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f318,plain,
( hskp23
| hskp19
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f319,plain,
! [X0] :
( hskp23
| hskp19
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f318]) ).
fof(f324,plain,
( hskp19
| hskp13
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f325,plain,
! [X0] :
( hskp19
| hskp13
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f326,plain,
( hskp12
| hskp20
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f327,plain,
! [X0] :
( hskp12
| hskp20
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f326]) ).
fof(f328,plain,
( hskp12
| hskp21
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ),
inference(miniscoping,[status(thm)],[f138]) ).
fof(f329,plain,
! [X0] :
( hskp12
| hskp21
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f328]) ).
fof(f332,plain,
( hskp14
| hskp22
| ! [U] :
( c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f140]) ).
fof(f333,plain,
! [X0] :
( hskp14
| hskp22
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f336,plain,
( hskp2
| hskp22
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f142]) ).
fof(f337,plain,
! [X0] :
( hskp2
| hskp22
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f340,plain,
( hskp0
| ! [V] :
( c2_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f341,plain,
! [X0,X1] :
( hskp0
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f342,plain,
( hskp0
| ! [V] :
( c3_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f343,plain,
! [X0,X1] :
( hskp0
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f342]) ).
fof(f348,plain,
( hskp26
| ! [V] :
( c3_1(V)
| c2_1(V)
| c1_1(V)
| ! [U] :
( c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f349,plain,
! [X0,X1] :
( hskp26
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f348]) ).
fof(f350,plain,
( hskp1
| ! [V] :
( c2_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f351,plain,
! [X0,X1] :
( hskp1
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f352,plain,
( hskp0
| ! [V] :
( c2_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f150]) ).
fof(f353,plain,
! [X0,X1] :
( hskp0
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f356,plain,
( hskp7
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f152]) ).
fof(f357,plain,
! [X0,X1] :
( hskp7
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f358,plain,
( hskp6
| ! [V] :
( c3_1(V)
| c2_1(V)
| c1_1(V)
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f359,plain,
! [X0,X1] :
( hskp6
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f364,plain,
( hskp1
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f365,plain,
! [X0,X1] :
( hskp1
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f368,plain,
( hskp3
| ! [V] :
( c3_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f158]) ).
fof(f369,plain,
! [X0,X1] :
( hskp3
| c3_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f368]) ).
fof(f370,plain,
( hskp11
| ! [V] :
( c0_1(V)
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f159]) ).
fof(f371,plain,
! [X0,X1] :
( hskp11
| c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f370]) ).
fof(f374,plain,
! [V] :
( c2_1(V)
| c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f375,plain,
! [X0,X1] :
( c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
( hskp11
| ! [V] :
( c2_1(V)
| c1_1(V)
| ! [U] :
( c3_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f162]) ).
fof(f377,plain,
! [X0,X1] :
( hskp11
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
( hskp17
| ! [V] :
( c1_1(V)
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f163]) ).
fof(f379,plain,
! [X0,X1] :
( hskp17
| c1_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f380,plain,
( hskp12
| ! [V] :
( c0_1(V)
| ! [U] :
( c1_1(U)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f164]) ).
fof(f381,plain,
! [X0,X1] :
( hskp12
| c0_1(X1)
| c1_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f386,plain,
( hskp25
| ! [V] :
( c2_1(V)
| ! [U] :
( c3_1(U)
| ~ c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f167]) ).
fof(f387,plain,
! [X0,X1] :
( hskp25
| c2_1(X1)
| c3_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f388,plain,
! [W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f168]) ).
fof(f389,plain,
! [X0,X1,X2] :
( c2_1(X2)
| c1_1(X2)
| c0_1(X2)
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f390,plain,
! [W] :
( c3_1(W)
| c1_1(W)
| c0_1(W)
| ! [V] :
( c3_1(V)
| c0_1(V)
| ! [U] :
( c0_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f391,plain,
! [X0,X1,X2] :
( c3_1(X2)
| c1_1(X2)
| c0_1(X2)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f392,plain,
! [W] :
( c1_1(W)
| c0_1(W)
| ! [V] :
( c1_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| ~ c2_1(W)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f170]) ).
fof(f393,plain,
! [X0,X1,X2] :
( c1_1(X2)
| c0_1(X2)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| ~ c2_1(X2)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f394,plain,
! [W] :
( c3_1(W)
| c2_1(W)
| c0_1(W)
| ! [V] :
( c1_1(V)
| ! [U] :
( c1_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f171]) ).
fof(f395,plain,
! [X0,X1,X2] :
( c3_1(X2)
| c2_1(X2)
| c0_1(X2)
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f394]) ).
fof(f398,plain,
! [W] :
( c2_1(W)
| c1_1(W)
| ! [V] :
( c1_1(V)
| ! [U] :
( c2_1(U)
| ~ c0_1(W)
| ~ c3_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f399,plain,
! [X0,X1,X2] :
( c2_1(X2)
| c1_1(X2)
| c1_1(X1)
| c2_1(X0)
| ~ c0_1(X2)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f400,plain,
! [W] :
( c0_1(W)
| ! [V] :
( c3_1(V)
| ! [U] :
( c3_1(U)
| ~ c3_1(W)
| ~ c1_1(W)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f174]) ).
fof(f401,plain,
! [X0,X1,X2] :
( c0_1(X2)
| c3_1(X1)
| c3_1(X0)
| ~ c3_1(X2)
| ~ c1_1(X2)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f414,plain,
( ~ hskp23
| hskp3
| hskp0
| c3_1(a1218)
| c0_1(a1218)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f301,f260]) ).
fof(f420,plain,
( ~ hskp23
| hskp3
| hskp0
| c3_1(a1218)
| c0_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f414,f183]) ).
fof(f421,plain,
( ~ hskp1
| hskp6
| hskp3
| c2_1(a1169)
| c0_1(a1169)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f303,f298]) ).
fof(f425,plain,
( ~ hskp7
| hskp6
| hskp3
| c2_1(a1179)
| c0_1(a1179)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f303,f291]) ).
fof(f426,plain,
( ~ hskp8
| hskp6
| hskp3
| c2_1(a1180)
| c0_1(a1180)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f303,f288]) ).
fof(f428,plain,
( ~ hskp12
| hskp6
| hskp3
| c2_1(a1187)
| c0_1(a1187)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f303,f280]) ).
fof(f432,plain,
( ~ hskp1
| hskp6
| hskp3
| c2_1(a1169)
| c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f421,f205]) ).
fof(f433,plain,
( ~ hskp7
| hskp6
| hskp3
| c2_1(a1179)
| c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f425,f199]) ).
fof(f434,plain,
( ~ hskp8
| hskp6
| hskp3
| c2_1(a1180)
| c0_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f426,f198]) ).
fof(f435,plain,
( ~ hskp12
| hskp6
| hskp3
| c2_1(a1187)
| c0_1(a1187) ),
inference(forward_subsumption_resolution,[status(thm)],[f428,f194]) ).
fof(f441,plain,
( ~ hskp17
| hskp15
| hskp14
| c3_1(a1200)
| c2_1(a1200)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f305,f268]) ).
fof(f449,plain,
( ~ hskp17
| hskp15
| hskp14
| c3_1(a1200)
| c2_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f441,f189]) ).
fof(f451,plain,
( ~ hskp7
| hskp0
| c2_1(a1179)
| ~ ndr1_0
| ~ c0_1(a1179) ),
inference(resolution,[status(thm)],[f307,f289]) ).
fof(f455,plain,
( ~ hskp17
| hskp0
| c2_1(a1200)
| ~ ndr1_0
| ~ c0_1(a1200) ),
inference(resolution,[status(thm)],[f307,f268]) ).
fof(f458,plain,
( ~ hskp22
| hskp0
| c2_1(a1211)
| ~ ndr1_0
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f307,f262]) ).
fof(f461,plain,
( ~ hskp7
| hskp0
| c2_1(a1179)
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f451,f199]) ).
fof(f462,plain,
( ~ hskp17
| hskp0
| c2_1(a1200)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f455,f235]) ).
fof(f464,plain,
( ~ hskp22
| hskp0
| c2_1(a1211)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f458,f226]) ).
fof(f465,plain,
( ~ hskp17
| hskp0
| c2_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f462,f189]) ).
fof(f466,plain,
( ~ hskp17
| ~ hskp17
| hskp0 ),
inference(resolution,[status(thm)],[f465,f269]) ).
fof(f467,plain,
( ~ hskp17
| hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f466]) ).
fof(f468,plain,
( ~ hskp22
| hskp0
| c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f464,f184]) ).
fof(f469,plain,
( ~ hskp7
| hskp0
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f461,f290]) ).
fof(f497,plain,
( ~ hskp23
| hskp3
| hskp0
| c3_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f259]) ).
fof(f498,plain,
( ~ hskp23
| ~ hskp23
| hskp3
| hskp0 ),
inference(resolution,[status(thm)],[f497,f261]) ).
fof(f499,plain,
( ~ hskp23
| hskp3
| hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f498]) ).
fof(f500,plain,
( ~ hskp1
| hskp6
| hskp3
| c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f432,f297]) ).
fof(f514,plain,
( ~ hskp1
| hskp17
| hskp22
| c2_1(a1169)
| ~ ndr1_0
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f313,f298]) ).
fof(f515,plain,
( ~ hskp3
| hskp17
| hskp22
| c2_1(a1174)
| ~ ndr1_0
| ~ c0_1(a1174) ),
inference(resolution,[status(thm)],[f313,f295]) ).
fof(f518,plain,
( ~ hskp7
| hskp17
| hskp22
| c2_1(a1179)
| ~ ndr1_0
| ~ c0_1(a1179) ),
inference(resolution,[status(thm)],[f313,f291]) ).
fof(f520,plain,
( ~ hskp11
| hskp17
| hskp22
| c2_1(a1186)
| ~ ndr1_0
| ~ c0_1(a1186) ),
inference(resolution,[status(thm)],[f313,f282]) ).
fof(f525,plain,
( ~ hskp1
| hskp17
| hskp22
| c2_1(a1169)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f514,f205]) ).
fof(f526,plain,
( ~ hskp3
| hskp17
| hskp22
| c2_1(a1174)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f515,f250]) ).
fof(f527,plain,
( ~ hskp7
| hskp17
| hskp22
| c2_1(a1179)
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f518,f199]) ).
fof(f528,plain,
( ~ hskp11
| hskp17
| hskp22
| c2_1(a1186)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f520,f240]) ).
fof(f533,plain,
( ~ hskp3
| hskp17
| hskp22
| c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f526,f203]) ).
fof(f534,plain,
( ~ hskp11
| hskp17
| hskp22
| c2_1(a1186) ),
inference(forward_subsumption_resolution,[status(thm)],[f528,f195]) ).
fof(f535,plain,
( ~ hskp11
| ~ hskp11
| hskp17
| hskp22 ),
inference(resolution,[status(thm)],[f534,f281]) ).
fof(f536,plain,
( ~ hskp11
| hskp17
| hskp22 ),
inference(duplicate_literals_removal,[status(thm)],[f535]) ).
fof(f537,plain,
( ~ hskp7
| hskp6
| hskp3
| c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f433,f290]) ).
fof(f538,plain,
( ~ hskp8
| hskp6
| hskp3
| c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f434,f287]) ).
fof(f539,plain,
( ~ hskp12
| hskp6
| hskp3
| c2_1(a1187) ),
inference(forward_subsumption_resolution,[status(thm)],[f435,f278]) ).
fof(f540,plain,
( ~ hskp12
| ~ hskp12
| hskp6
| hskp3 ),
inference(resolution,[status(thm)],[f539,f279]) ).
fof(f541,plain,
( ~ hskp12
| hskp6
| hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f540]) ).
fof(f547,plain,
( ~ hskp17
| hskp15
| hskp14
| c3_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f449,f269]) ).
fof(f581,plain,
( ~ hskp1
| hskp23
| hskp19
| c2_1(a1169)
| ~ ndr1_0
| ~ c1_1(a1169) ),
inference(resolution,[status(thm)],[f319,f298]) ).
fof(f582,plain,
( ~ hskp3
| hskp23
| hskp19
| c2_1(a1174)
| ~ ndr1_0
| ~ c1_1(a1174) ),
inference(resolution,[status(thm)],[f319,f295]) ).
fof(f592,plain,
( ~ hskp1
| hskp23
| hskp19
| c2_1(a1169)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f581,f254]) ).
fof(f593,plain,
( ~ hskp3
| hskp23
| hskp19
| c2_1(a1174)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f582,f251]) ).
fof(f619,plain,
( ~ hskp1
| hskp23
| hskp19
| c2_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f592,f205]) ).
fof(f620,plain,
( ~ hskp1
| ~ hskp1
| hskp23
| hskp19 ),
inference(resolution,[status(thm)],[f619,f297]) ).
fof(f621,plain,
( ~ hskp1
| hskp23
| hskp19 ),
inference(duplicate_literals_removal,[status(thm)],[f620]) ).
fof(f622,plain,
( ~ hskp3
| hskp23
| hskp19
| c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f593,f203]) ).
fof(f627,plain,
( ~ hskp1
| hskp17
| hskp22
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f525,f297]) ).
fof(f628,plain,
( ~ hskp7
| hskp17
| hskp22
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f527,f290]) ).
fof(f651,plain,
( ~ hskp21
| hskp19
| hskp13
| ~ ndr1_0
| ~ c3_1(a1207)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f325,f263]) ).
fof(f652,plain,
( ~ hskp22
| hskp19
| hskp13
| ~ ndr1_0
| ~ c3_1(a1211)
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f325,f262]) ).
fof(f656,plain,
( ~ hskp21
| hskp19
| hskp13
| ~ ndr1_0
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f229]) ).
fof(f657,plain,
( ~ hskp22
| hskp19
| hskp13
| ~ ndr1_0
| ~ c3_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f652,f226]) ).
fof(f662,plain,
( ~ hskp21
| hskp19
| hskp13
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f656,f185]) ).
fof(f663,plain,
( ~ hskp22
| hskp19
| hskp13
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f657,f227]) ).
fof(f673,plain,
( ~ hskp21
| hskp12
| hskp20
| ~ ndr1_0
| ~ c3_1(a1207)
| ~ c2_1(a1207) ),
inference(resolution,[status(thm)],[f327,f263]) ).
fof(f678,plain,
( ~ hskp21
| hskp12
| hskp20
| ~ ndr1_0
| ~ c3_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f228]) ).
fof(f682,plain,
( ~ hskp21
| hskp12
| hskp20
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f678,f229]) ).
fof(f687,plain,
( ~ hskp14
| hskp12
| hskp21
| ~ ndr1_0
| ~ c3_1(a1194)
| ~ c2_1(a1194) ),
inference(resolution,[status(thm)],[f329,f275]) ).
fof(f692,plain,
( ~ hskp22
| hskp12
| hskp21
| ~ ndr1_0
| ~ c3_1(a1211)
| ~ c2_1(a1211) ),
inference(resolution,[status(thm)],[f329,f262]) ).
fof(f695,plain,
( ~ hskp14
| hskp12
| hskp21
| ~ ndr1_0
| ~ c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f687,f238]) ).
fof(f696,plain,
( ~ hskp22
| hskp12
| hskp21
| ~ ndr1_0
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f692,f227]) ).
fof(f698,plain,
( ~ hskp14
| hskp12
| hskp21
| ~ c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f695,f192]) ).
fof(f699,plain,
( ~ hskp22
| hskp12
| hskp21
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f696,f184]) ).
fof(f716,plain,
! [X0] :
( hskp14
| hskp22
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f333,f315]) ).
fof(f759,plain,
! [X0] :
( ~ hskp17
| c2_1(a1200)
| ~ c0_1(a1200)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f375,f268]) ).
fof(f760,plain,
! [X0] :
( ~ hskp19
| c2_1(a1204)
| ~ c0_1(a1204)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f375,f265]) ).
fof(f762,plain,
! [X0] :
( ~ hskp22
| c2_1(a1211)
| ~ c0_1(a1211)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f375,f262]) ).
fof(f766,plain,
! [X0] :
( ~ hskp17
| c2_1(a1200)
| ~ c0_1(a1200)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f759,f189]) ).
fof(f767,plain,
! [X0] :
( ~ hskp19
| c2_1(a1204)
| ~ c0_1(a1204)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f760,f187]) ).
fof(f768,plain,
! [X0] :
( ~ hskp22
| c2_1(a1211)
| ~ c0_1(a1211)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f762,f184]) ).
fof(f830,plain,
! [X0,X1] :
( hskp0
| c2_1(X1)
| c1_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f341,f307]) ).
fof(f836,plain,
! [X0] :
( ~ hskp19
| hskp0
| c2_1(X0)
| c1_1(X0)
| c2_1(a1204)
| ~ ndr1_0
| ~ c3_1(a1204) ),
inference(resolution,[status(thm)],[f830,f265]) ).
fof(f843,plain,
! [X0] :
( ~ hskp19
| hskp0
| c2_1(X0)
| c1_1(X0)
| c2_1(a1204)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f836,f232]) ).
fof(f848,plain,
! [X0] :
( ~ hskp14
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1194)
| ~ ndr1_0
| ~ c2_1(a1194) ),
inference(resolution,[status(thm)],[f343,f275]) ).
fof(f852,plain,
! [X0] :
( ~ hskp21
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ ndr1_0
| ~ c2_1(a1207) ),
inference(resolution,[status(thm)],[f343,f263]) ).
fof(f854,plain,
! [X0] :
( ~ hskp23
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1218)
| ~ ndr1_0
| ~ c2_1(a1218) ),
inference(resolution,[status(thm)],[f343,f260]) ).
fof(f857,plain,
! [X0] :
( ~ hskp14
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1194)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f848,f238]) ).
fof(f859,plain,
! [X0] :
( ~ hskp21
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f852,f228]) ).
fof(f860,plain,
! [X0] :
( ~ hskp23
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1218)
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f854,f183]) ).
fof(f870,plain,
! [X0] :
( ~ hskp19
| hskp0
| c2_1(X0)
| c1_1(X0)
| c2_1(a1204) ),
inference(forward_subsumption_resolution,[status(thm)],[f843,f187]) ).
fof(f876,plain,
( ~ hskp19
| ~ hskp19
| hskp0
| c2_1(a1204)
| c2_1(a1204) ),
inference(resolution,[status(thm)],[f870,f265]) ).
fof(f884,plain,
( ~ hskp19
| hskp0
| c2_1(a1204) ),
inference(duplicate_literals_removal,[status(thm)],[f876]) ).
fof(f885,plain,
( ~ hskp19
| hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f884,f266]) ).
fof(f934,plain,
! [X0] :
( ~ hskp14
| hskp26
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a1194)
| ~ ndr1_0
| ~ c2_1(a1194) ),
inference(resolution,[status(thm)],[f349,f275]) ).
fof(f935,plain,
! [X0] :
( ~ hskp15
| hskp26
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a1195)
| ~ ndr1_0
| ~ c2_1(a1195) ),
inference(resolution,[status(thm)],[f349,f272]) ).
fof(f943,plain,
! [X0] :
( ~ hskp14
| hskp26
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a1194)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f934,f238]) ).
fof(f944,plain,
! [X0] :
( ~ hskp15
| hskp26
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a1195)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f935,f237]) ).
fof(f965,plain,
! [X0] :
( ~ hskp0
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a1168)
| ~ c0_1(a1168) ),
inference(resolution,[status(thm)],[f351,f299]) ).
fof(f975,plain,
! [X0] :
( ~ hskp20
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a1205)
| ~ c0_1(a1205) ),
inference(resolution,[status(thm)],[f351,f264]) ).
fof(f976,plain,
! [X0] :
( ~ hskp0
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f965,f255]) ).
fof(f980,plain,
! [X0] :
( ~ hskp20
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a1205) ),
inference(forward_subsumption_resolution,[status(thm)],[f975,f231]) ).
fof(f982,plain,
! [X0] :
( ~ hskp17
| c2_1(a1200)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f766,f235]) ).
fof(f983,plain,
! [X0] :
( ~ hskp17
| ~ hskp17
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f982,f269]) ).
fof(f984,plain,
! [X0] :
( ~ hskp17
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f983]) ).
fof(f995,plain,
( ~ hskp26
| ~ hskp17
| ~ c3_1(a1190)
| ~ c0_1(a1190) ),
inference(resolution,[status(thm)],[f984,f220]) ).
fof(f1014,plain,
( ~ hskp26
| ~ hskp17
| ~ c3_1(a1190) ),
inference(forward_subsumption_resolution,[status(thm)],[f995,f219]) ).
fof(f1047,plain,
( ~ hskp26
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f1014,f221]) ).
fof(f1061,plain,
! [X0,X1] :
( hskp0
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f307]) ).
fof(f1067,plain,
! [X0] :
( ~ hskp3
| hskp0
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174)
| ~ c0_1(a1174) ),
inference(resolution,[status(thm)],[f1061,f295]) ).
fof(f1077,plain,
! [X0] :
( ~ hskp3
| hskp0
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1067,f250]) ).
fof(f1111,plain,
! [X0] :
( ~ hskp3
| hskp0
| c2_1(X0)
| c1_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1077,f203]) ).
fof(f1134,plain,
! [X0] :
( ~ hskp22
| hskp7
| c2_1(X0)
| c0_1(X0)
| c2_1(a1211)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f357,f262]) ).
fof(f1141,plain,
! [X0] :
( ~ hskp22
| hskp7
| c2_1(X0)
| c0_1(X0)
| c2_1(a1211)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1134,f226]) ).
fof(f1144,plain,
! [X0] :
( ~ hskp0
| hskp6
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a1168)
| ~ c0_1(a1168) ),
inference(resolution,[status(thm)],[f359,f299]) ).
fof(f1145,plain,
! [X0] :
( ~ hskp1
| hskp6
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a1169)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f359,f297]) ).
fof(f1155,plain,
! [X0] :
( ~ hskp0
| hskp6
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f1144,f255]) ).
fof(f1156,plain,
! [X0] :
( ~ hskp1
| hskp6
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f1145,f254]) ).
fof(f1248,plain,
! [X0] :
( ~ hskp19
| ~ c0_1(a1204)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f767,f266]) ).
fof(f1249,plain,
( ~ hskp0
| ~ hskp19
| ~ c0_1(a1204)
| ~ c3_1(a1168)
| ~ c0_1(a1168) ),
inference(resolution,[status(thm)],[f1248,f256]) ).
fof(f1257,plain,
( ~ hskp20
| ~ hskp19
| ~ c0_1(a1204)
| ~ c3_1(a1205)
| ~ c0_1(a1205) ),
inference(resolution,[status(thm)],[f1248,f230]) ).
fof(f1259,plain,
( ~ hskp26
| ~ hskp19
| ~ c0_1(a1204)
| ~ c3_1(a1190)
| ~ c0_1(a1190) ),
inference(resolution,[status(thm)],[f1248,f220]) ).
fof(f1281,plain,
( ~ hskp0
| ~ hskp19
| ~ c0_1(a1204)
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f1249,f255]) ).
fof(f1282,plain,
( ~ hskp20
| ~ hskp19
| ~ c0_1(a1204)
| ~ c0_1(a1205) ),
inference(forward_subsumption_resolution,[status(thm)],[f1257,f231]) ).
fof(f1284,plain,
( ~ hskp26
| ~ hskp19
| ~ c0_1(a1204)
| ~ c3_1(a1190) ),
inference(forward_subsumption_resolution,[status(thm)],[f1259,f219]) ).
fof(f1298,plain,
( ~ hskp19
| ~ c0_1(a1204)
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f1281,f885]) ).
fof(f1321,plain,
! [X0] :
( ~ hskp21
| hskp1
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a1207)
| ~ c2_1(a1207) ),
inference(resolution,[status(thm)],[f365,f263]) ).
fof(f1322,plain,
! [X0] :
( ~ hskp22
| hskp1
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a1211)
| ~ c2_1(a1211) ),
inference(resolution,[status(thm)],[f365,f262]) ).
fof(f1329,plain,
! [X0] :
( ~ hskp21
| hskp1
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f1321,f228]) ).
fof(f1330,plain,
! [X0] :
( ~ hskp22
| hskp1
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f1322,f227]) ).
fof(f1366,plain,
( ~ hskp26
| ~ hskp19
| ~ c0_1(a1204) ),
inference(forward_subsumption_resolution,[status(thm)],[f1284,f221]) ).
fof(f1390,plain,
! [X0] :
( ~ hskp22
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f768,f226]) ).
fof(f1391,plain,
! [X0] :
( ~ hskp14
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f857,f192]) ).
fof(f1394,plain,
( ~ hskp14
| ~ hskp14
| hskp0
| c3_1(a1194)
| c0_1(a1194)
| c0_1(a1194) ),
inference(resolution,[status(thm)],[f1391,f275]) ).
fof(f1407,plain,
( ~ hskp14
| hskp0
| c3_1(a1194)
| c0_1(a1194) ),
inference(duplicate_literals_removal,[status(thm)],[f1394]) ).
fof(f1408,plain,
( ~ hskp14
| hskp0
| c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f1407,f274]) ).
fof(f1411,plain,
! [X0] :
( ~ hskp0
| hskp3
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(a1168)
| ~ c1_1(a1168) ),
inference(resolution,[status(thm)],[f369,f299]) ).
fof(f1421,plain,
! [X0] :
( ~ hskp20
| hskp3
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(a1205)
| ~ c1_1(a1205) ),
inference(resolution,[status(thm)],[f369,f264]) ).
fof(f1422,plain,
! [X0] :
( ~ hskp0
| hskp3
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f1411,f256]) ).
fof(f1425,plain,
! [X0] :
( ~ hskp20
| hskp3
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(a1205) ),
inference(forward_subsumption_resolution,[status(thm)],[f1421,f230]) ).
fof(f1431,plain,
! [X0] :
( ~ hskp19
| hskp11
| c0_1(X0)
| c2_1(a1204)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(a1204) ),
inference(resolution,[status(thm)],[f371,f265]) ).
fof(f1433,plain,
! [X0] :
( ~ hskp22
| hskp11
| c0_1(X0)
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c3_1(a1211) ),
inference(resolution,[status(thm)],[f371,f262]) ).
fof(f1441,plain,
! [X0] :
( ~ hskp19
| hskp11
| c0_1(X0)
| c2_1(a1204)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1431,f232]) ).
fof(f1442,plain,
! [X0] :
( ~ hskp22
| hskp11
| c0_1(X0)
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1433,f227]) ).
fof(f1481,plain,
! [X0] :
( ~ hskp1
| hskp11
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(a1169)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f377,f298]) ).
fof(f1482,plain,
! [X0] :
( ~ hskp3
| hskp11
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(a1174)
| ~ c0_1(a1174) ),
inference(resolution,[status(thm)],[f377,f295]) ).
fof(f1498,plain,
! [X0] :
( ~ hskp1
| hskp11
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f1481,f254]) ).
fof(f1499,plain,
! [X0] :
( ~ hskp3
| hskp11
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1482,f250]) ).
fof(f1539,plain,
! [X0] :
( ~ hskp21
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f859,f185]) ).
fof(f1548,plain,
( ~ hskp23
| ~ hskp21
| hskp0
| c3_1(a1218)
| c0_1(a1218)
| c0_1(a1207) ),
inference(resolution,[status(thm)],[f1539,f260]) ).
fof(f1556,plain,
( ~ hskp23
| ~ hskp21
| hskp0
| c3_1(a1218)
| c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f1548,f259]) ).
fof(f1565,plain,
! [X0] :
( ~ hskp1
| hskp17
| c1_1(X0)
| c2_1(a1169)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f379,f298]) ).
fof(f1566,plain,
! [X0] :
( ~ hskp3
| hskp17
| c1_1(X0)
| c2_1(a1174)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a1174) ),
inference(resolution,[status(thm)],[f379,f295]) ).
fof(f1569,plain,
! [X0] :
( ~ hskp7
| hskp17
| c1_1(X0)
| c2_1(a1179)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a1179) ),
inference(resolution,[status(thm)],[f379,f291]) ).
fof(f1571,plain,
! [X0] :
( ~ hskp11
| hskp17
| c1_1(X0)
| c2_1(a1186)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a1186) ),
inference(resolution,[status(thm)],[f379,f282]) ).
fof(f1578,plain,
! [X0] :
( ~ hskp1
| hskp17
| c1_1(X0)
| c2_1(a1169)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f1565,f205]) ).
fof(f1579,plain,
! [X0] :
( ~ hskp3
| hskp17
| c1_1(X0)
| c2_1(a1174)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1566,f250]) ).
fof(f1580,plain,
! [X0] :
( ~ hskp7
| hskp17
| c1_1(X0)
| c2_1(a1179)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f1569,f199]) ).
fof(f1581,plain,
! [X0] :
( ~ hskp11
| hskp17
| c1_1(X0)
| c2_1(a1186)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1571,f240]) ).
fof(f1588,plain,
! [X0] :
( ~ hskp21
| hskp12
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(a1207)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f381,f263]) ).
fof(f1596,plain,
! [X0] :
( ~ hskp21
| hskp12
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f1588,f228]) ).
fof(f1604,plain,
( ~ hskp23
| ~ hskp21
| hskp0
| c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f1556,f261]) ).
fof(f1626,plain,
! [X0] :
( ~ hskp14
| hskp26
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f943,f192]) ).
fof(f1631,plain,
( ~ hskp17
| ~ hskp14
| hskp26
| c3_1(a1200)
| c2_1(a1200)
| c3_1(a1194) ),
inference(resolution,[status(thm)],[f1626,f268]) ).
fof(f1643,plain,
( ~ hskp17
| ~ hskp14
| hskp26
| c3_1(a1200)
| c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f1631,f269]) ).
fof(f1646,plain,
( ~ hskp17
| ~ hskp14
| c3_1(a1200)
| c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f1643,f1047]) ).
fof(f1647,plain,
! [X0] :
( ~ hskp15
| hskp26
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a1195) ),
inference(forward_subsumption_resolution,[status(thm)],[f944,f191]) ).
fof(f1652,plain,
( ~ hskp17
| ~ hskp15
| hskp26
| c3_1(a1200)
| c2_1(a1200)
| c3_1(a1195) ),
inference(resolution,[status(thm)],[f1647,f268]) ).
fof(f1664,plain,
( ~ hskp17
| ~ hskp15
| hskp26
| c3_1(a1200)
| c2_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f1652,f273]) ).
fof(f1671,plain,
( ~ hskp17
| ~ hskp15
| hskp26
| c3_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f1664,f269]) ).
fof(f1718,plain,
! [X0] :
( ~ hskp3
| hskp25
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(a1174)
| ~ c0_1(a1174) ),
inference(resolution,[status(thm)],[f387,f295]) ).
fof(f1735,plain,
! [X0] :
( ~ hskp3
| hskp25
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1718,f250]) ).
fof(f1740,plain,
! [X0] :
( ~ hskp0
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f976,f206]) ).
fof(f1746,plain,
( ~ hskp19
| ~ hskp0
| hskp1
| c2_1(a1204)
| c0_1(a1204)
| ~ c3_1(a1168) ),
inference(resolution,[status(thm)],[f1740,f265]) ).
fof(f1756,plain,
( ~ hskp19
| ~ hskp0
| hskp1
| c2_1(a1204)
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f1746,f1298]) ).
fof(f1761,plain,
( ~ hskp19
| ~ hskp0
| hskp1
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f1756,f266]) ).
fof(f1769,plain,
! [X0,X1] :
( ~ hskp3
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174)
| ~ c1_1(a1174) ),
inference(resolution,[status(thm)],[f389,f295]) ).
fof(f1771,plain,
! [X0,X1] :
( ~ hskp6
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1178)
| ~ c1_1(a1178) ),
inference(resolution,[status(thm)],[f389,f292]) ).
fof(f1773,plain,
! [X0,X1] :
( ~ hskp8
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1180)
| ~ c1_1(a1180) ),
inference(resolution,[status(thm)],[f389,f288]) ).
fof(f1777,plain,
! [X0,X1] :
( ~ hskp16
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1199)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f389,f271]) ).
fof(f1785,plain,
! [X0,X1] :
( ~ hskp3
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1769,f251]) ).
fof(f1787,plain,
! [X0,X1] :
( ~ hskp6
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1178) ),
inference(forward_subsumption_resolution,[status(thm)],[f1771,f244]) ).
fof(f1788,plain,
! [X0,X1] :
( ~ hskp8
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f1773,f243]) ).
fof(f1789,plain,
! [X0,X1] :
( ~ hskp16
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f1777,f236]) ).
fof(f1835,plain,
! [X0,X1] :
( ~ hskp2
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(a1172)
| ~ c2_1(a1172) ),
inference(resolution,[status(thm)],[f391,f296]) ).
fof(f1847,plain,
! [X0,X1] :
( ~ hskp2
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(a1172) ),
inference(forward_subsumption_resolution,[status(thm)],[f1835,f252]) ).
fof(f1859,plain,
! [X0,X1] :
( ~ hskp3
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174)
| ~ c1_1(a1174) ),
inference(resolution,[status(thm)],[f393,f295]) ).
fof(f1861,plain,
! [X0,X1] :
( ~ hskp6
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1178)
| ~ c1_1(a1178) ),
inference(resolution,[status(thm)],[f393,f292]) ).
fof(f1863,plain,
! [X0,X1] :
( ~ hskp8
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1180)
| ~ c1_1(a1180) ),
inference(resolution,[status(thm)],[f393,f288]) ).
fof(f1867,plain,
! [X0,X1] :
( ~ hskp16
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1199)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f393,f271]) ).
fof(f1875,plain,
! [X0,X1] :
( ~ hskp3
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1859,f251]) ).
fof(f1877,plain,
! [X0,X1] :
( ~ hskp6
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1178) ),
inference(forward_subsumption_resolution,[status(thm)],[f1861,f244]) ).
fof(f1878,plain,
! [X0,X1] :
( ~ hskp8
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f1863,f243]) ).
fof(f1879,plain,
! [X0,X1] :
( ~ hskp16
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f1867,f236]) ).
fof(f1940,plain,
! [X0] :
( ~ hskp20
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c0_1(a1205) ),
inference(forward_subsumption_resolution,[status(thm)],[f980,f186]) ).
fof(f1946,plain,
( ~ hskp19
| ~ hskp20
| hskp1
| c2_1(a1204)
| c0_1(a1204)
| ~ c0_1(a1205) ),
inference(resolution,[status(thm)],[f1940,f265]) ).
fof(f1956,plain,
( ~ hskp19
| ~ hskp20
| hskp1
| c2_1(a1204)
| ~ c0_1(a1205) ),
inference(forward_subsumption_resolution,[status(thm)],[f1946,f1282]) ).
fof(f1961,plain,
( ~ hskp19
| ~ hskp20
| hskp1
| ~ c0_1(a1205) ),
inference(forward_subsumption_resolution,[status(thm)],[f1956,f266]) ).
fof(f1968,plain,
! [X0,X1] :
( ~ hskp21
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a1207)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f395,f263]) ).
fof(f1969,plain,
! [X0,X1] :
( ~ hskp22
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a1211)
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f395,f262]) ).
fof(f1977,plain,
! [X0,X1] :
( ~ hskp21
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f1968,f229]) ).
fof(f1978,plain,
! [X0,X1] :
( ~ hskp22
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f1969,f226]) ).
fof(f2009,plain,
! [X0,X1,X2] :
( c2_1(X2)
| c1_1(X2)
| c2_1(X0)
| ~ c0_1(X2)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f375]) ).
fof(f2010,plain,
! [X0,X1] :
( ~ hskp0
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(a1168)
| ~ c0_1(a1168) ),
inference(resolution,[status(thm)],[f2009,f299]) ).
fof(f2011,plain,
! [X0,X1] :
( ~ hskp1
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(a1169)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f2009,f297]) ).
fof(f2021,plain,
! [X0,X1] :
( ~ hskp0
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f2010,f255]) ).
fof(f2022,plain,
! [X0,X1] :
( ~ hskp1
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f2011,f254]) ).
fof(f2060,plain,
! [X0,X1] :
( ~ hskp3
| c0_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174)
| ~ c1_1(a1174) ),
inference(resolution,[status(thm)],[f401,f295]) ).
fof(f2076,plain,
! [X0,X1] :
( ~ hskp3
| c0_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f2060,f251]) ).
fof(f2235,plain,
! [X0] :
( ~ hskp23
| hskp0
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f860,f259]) ).
fof(f2244,plain,
( ~ hskp23
| ~ hskp23
| hskp0
| c3_1(a1218)
| c0_1(a1218)
| ~ c2_1(a1218) ),
inference(resolution,[status(thm)],[f2235,f260]) ).
fof(f2251,plain,
( ~ hskp23
| hskp0
| c3_1(a1218)
| c0_1(a1218)
| ~ c2_1(a1218) ),
inference(duplicate_literals_removal,[status(thm)],[f2244]) ).
fof(f2252,plain,
( ~ hskp23
| hskp0
| c3_1(a1218)
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f2251,f259]) ).
fof(f2293,plain,
( ~ hskp23
| hskp0
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f2252,f261]) ).
fof(f2619,plain,
! [X0] :
( ~ hskp22
| hskp7
| c2_1(X0)
| c0_1(X0)
| c2_1(a1211)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1141,f184]) ).
fof(f2633,plain,
( ~ hskp13
| ~ hskp22
| hskp7
| c2_1(a1192)
| c2_1(a1211)
| ~ c1_1(a1192) ),
inference(resolution,[status(thm)],[f2619,f276]) ).
fof(f2641,plain,
( ~ hskp13
| ~ hskp22
| hskp7
| c2_1(a1192)
| c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f2633,f239]) ).
fof(f2643,plain,
! [X0] :
( ~ hskp0
| hskp6
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1155,f256]) ).
fof(f2645,plain,
( ~ hskp7
| ~ hskp0
| hskp6
| c3_1(a1179)
| c2_1(a1179)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f2643,f289]) ).
fof(f2649,plain,
( ~ hskp17
| ~ hskp0
| hskp6
| c3_1(a1200)
| c2_1(a1200)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f2643,f268]) ).
fof(f2653,plain,
( ~ hskp23
| ~ hskp0
| hskp6
| c3_1(a1218)
| c2_1(a1218)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f2643,f260]) ).
fof(f2659,plain,
( ~ hskp7
| ~ hskp0
| hskp6
| c3_1(a1179)
| c2_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f2645,f206]) ).
fof(f2661,plain,
( ~ hskp17
| ~ hskp0
| hskp6
| c3_1(a1200)
| c2_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f2649,f206]) ).
fof(f2662,plain,
( ~ hskp23
| ~ hskp0
| hskp6
| c3_1(a1218)
| c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f2653,f206]) ).
fof(f2663,plain,
! [X0] :
( ~ hskp1
| hskp6
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f1156,f205]) ).
fof(f2706,plain,
( ~ hskp13
| ~ hskp22
| hskp7
| c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f2641,f277]) ).
fof(f2707,plain,
( ~ hskp7
| ~ hskp0
| hskp6
| c3_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f2659,f290]) ).
fof(f2708,plain,
( ~ hskp7
| ~ hskp7
| ~ hskp0
| hskp6 ),
inference(resolution,[status(thm)],[f2707,f291]) ).
fof(f2709,plain,
( ~ hskp7
| ~ hskp0
| hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f2708]) ).
fof(f2711,plain,
( ~ hskp17
| ~ hskp0
| hskp6
| c3_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f2661,f269]) ).
fof(f2712,plain,
( ~ hskp23
| ~ hskp0
| hskp6
| c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f2662,f261]) ).
fof(f3174,plain,
! [X0] :
( ~ hskp21
| hskp1
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1329,f229]) ).
fof(f3175,plain,
( ~ hskp26
| ~ hskp19
| ~ hskp21
| hskp1
| c2_1(a1204)
| ~ c3_1(a1204)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3174,f1366]) ).
fof(f3188,plain,
( ~ hskp13
| ~ hskp21
| hskp1
| c2_1(a1192)
| ~ c3_1(a1192)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3174,f276]) ).
fof(f3194,plain,
( ~ hskp26
| ~ hskp19
| ~ hskp21
| hskp1
| c2_1(a1204)
| ~ c3_1(a1204) ),
inference(forward_subsumption_resolution,[status(thm)],[f3175,f187]) ).
fof(f3198,plain,
( ~ hskp13
| ~ hskp21
| hskp1
| c2_1(a1192)
| ~ c3_1(a1192) ),
inference(forward_subsumption_resolution,[status(thm)],[f3188,f193]) ).
fof(f3208,plain,
! [X0] :
( ~ hskp22
| hskp1
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f1330,f184]) ).
fof(f3298,plain,
( ~ hskp13
| ~ hskp21
| hskp1
| ~ c3_1(a1192) ),
inference(forward_subsumption_resolution,[status(thm)],[f3198,f277]) ).
fof(f3426,plain,
! [X0] :
( ~ hskp0
| hskp3
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f1422,f206]) ).
fof(f3434,plain,
( ~ hskp1
| ~ hskp0
| hskp3
| c0_1(a1169)
| ~ c1_1(a1169)
| ~ c3_1(a1168) ),
inference(resolution,[status(thm)],[f3426,f298]) ).
fof(f3439,plain,
( ~ hskp8
| ~ hskp0
| hskp3
| c0_1(a1180)
| ~ c1_1(a1180)
| ~ c3_1(a1168) ),
inference(resolution,[status(thm)],[f3426,f288]) ).
fof(f3446,plain,
( ~ hskp1
| ~ hskp0
| hskp3
| c0_1(a1169)
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f3434,f254]) ).
fof(f3448,plain,
( ~ hskp8
| ~ hskp0
| hskp3
| c0_1(a1180)
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f3439,f243]) ).
fof(f3476,plain,
( ~ hskp8
| ~ hskp0
| hskp3
| ~ c3_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f3448,f287]) ).
fof(f3480,plain,
( ~ hskp26
| ~ hskp19
| ~ hskp21
| hskp1
| c2_1(a1204) ),
inference(forward_subsumption_resolution,[status(thm)],[f3194,f232]) ).
fof(f3481,plain,
( ~ hskp19
| ~ hskp26
| ~ hskp19
| ~ hskp21
| hskp1 ),
inference(resolution,[status(thm)],[f3480,f266]) ).
fof(f3482,plain,
( ~ hskp26
| ~ hskp19
| ~ hskp21
| hskp1 ),
inference(duplicate_literals_removal,[status(thm)],[f3481]) ).
fof(f3512,plain,
! [X0] :
( ~ hskp20
| hskp3
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1425,f231]) ).
fof(f3520,plain,
( ~ hskp1
| ~ hskp20
| hskp3
| c0_1(a1169)
| ~ c1_1(a1169)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3512,f298]) ).
fof(f3535,plain,
( ~ hskp1
| ~ hskp20
| hskp3
| c0_1(a1169)
| ~ c1_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f3520,f205]) ).
fof(f3596,plain,
( ~ hskp1
| ~ hskp20
| hskp3
| c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f3535,f254]) ).
fof(f3606,plain,
! [X0] :
( ~ hskp19
| hskp11
| c0_1(X0)
| c2_1(a1204)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1441,f187]) ).
fof(f3635,plain,
! [X0] :
( ~ hskp22
| hskp11
| c0_1(X0)
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1442,f184]) ).
fof(f3739,plain,
! [X0] :
( ~ hskp1
| hskp11
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f1498,f205]) ).
fof(f3745,plain,
( ~ hskp19
| ~ hskp1
| hskp11
| c2_1(a1204)
| ~ c3_1(a1204)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f3739,f265]) ).
fof(f3755,plain,
( ~ hskp19
| ~ hskp1
| hskp11
| c2_1(a1204)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f3745,f232]) ).
fof(f3761,plain,
( ~ hskp19
| ~ hskp1
| hskp11
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f3755,f266]) ).
fof(f3780,plain,
! [X0] :
( ~ hskp3
| hskp11
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1499,f251]) ).
fof(f3786,plain,
( ~ hskp19
| ~ hskp3
| hskp11
| c2_1(a1204)
| ~ c3_1(a1204)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3780,f265]) ).
fof(f3788,plain,
( ~ hskp22
| ~ hskp3
| hskp11
| c2_1(a1211)
| ~ c3_1(a1211)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3780,f262]) ).
fof(f3796,plain,
( ~ hskp19
| ~ hskp3
| hskp11
| c2_1(a1204)
| ~ c3_1(a1204) ),
inference(forward_subsumption_resolution,[status(thm)],[f3786,f203]) ).
fof(f3797,plain,
( ~ hskp22
| ~ hskp3
| hskp11
| c2_1(a1211)
| ~ c3_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f3788,f203]) ).
fof(f3851,plain,
( ~ hskp19
| ~ hskp3
| hskp11
| c2_1(a1204) ),
inference(forward_subsumption_resolution,[status(thm)],[f3796,f232]) ).
fof(f3852,plain,
( ~ hskp19
| ~ hskp19
| ~ hskp3
| hskp11 ),
inference(resolution,[status(thm)],[f3851,f266]) ).
fof(f3853,plain,
( ~ hskp19
| ~ hskp3
| hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f3852]) ).
fof(f3854,plain,
( ~ hskp22
| ~ hskp3
| hskp11
| c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f3797,f227]) ).
fof(f3857,plain,
! [X0] :
( ~ hskp1
| hskp17
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f1578,f297]) ).
fof(f3864,plain,
( ~ hskp21
| ~ hskp1
| hskp17
| ~ c2_1(a1207)
| ~ c0_1(a1207)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f3857,f263]) ).
fof(f3865,plain,
( ~ hskp22
| ~ hskp1
| hskp17
| ~ c2_1(a1211)
| ~ c0_1(a1211)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f3857,f262]) ).
fof(f3872,plain,
( ~ hskp21
| ~ hskp1
| hskp17
| ~ c0_1(a1207)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f3864,f228]) ).
fof(f3873,plain,
( ~ hskp22
| ~ hskp1
| hskp17
| ~ c2_1(a1211)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f3865,f226]) ).
fof(f3888,plain,
! [X0] :
( ~ hskp3
| hskp17
| c1_1(X0)
| c2_1(a1174)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1579,f203]) ).
fof(f3896,plain,
( ~ hskp22
| ~ hskp3
| hskp17
| c2_1(a1174)
| ~ c2_1(a1211)
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f3888,f262]) ).
fof(f3904,plain,
( ~ hskp22
| ~ hskp3
| hskp17
| c2_1(a1174)
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f3896,f226]) ).
fof(f3908,plain,
! [X0] :
( ~ hskp7
| hskp17
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f1580,f290]) ).
fof(f3915,plain,
( ~ hskp21
| ~ hskp7
| hskp17
| ~ c2_1(a1207)
| ~ c0_1(a1207)
| ~ c0_1(a1179) ),
inference(resolution,[status(thm)],[f3908,f263]) ).
fof(f3924,plain,
( ~ hskp21
| ~ hskp7
| hskp17
| ~ c0_1(a1207)
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f3915,f228]) ).
fof(f3931,plain,
( ~ hskp1
| hskp17
| ~ c2_1(a1211)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f3873,f627]) ).
fof(f3932,plain,
( ~ hskp3
| hskp17
| c2_1(a1174)
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f3904,f533]) ).
fof(f3991,plain,
! [X0] :
( ~ hskp11
| hskp17
| c1_1(X0)
| c2_1(a1186)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1581,f195]) ).
fof(f3999,plain,
( ~ hskp22
| ~ hskp11
| hskp17
| c2_1(a1186)
| ~ c2_1(a1211)
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f3991,f262]) ).
fof(f4007,plain,
( ~ hskp22
| ~ hskp11
| hskp17
| c2_1(a1186)
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f3999,f226]) ).
fof(f4039,plain,
! [X0] :
( ~ hskp21
| hskp12
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f1596,f185]) ).
fof(f4054,plain,
( ~ hskp13
| ~ hskp21
| hskp12
| ~ c3_1(a1192)
| ~ c1_1(a1192)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f4039,f276]) ).
fof(f4064,plain,
( ~ hskp13
| ~ hskp21
| hskp12
| ~ c3_1(a1192)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f4054,f239]) ).
fof(f4068,plain,
( ~ hskp22
| ~ hskp11
| hskp17
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f4007,f281]) ).
fof(f4139,plain,
! [X0] :
( ~ hskp3
| hskp25
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1735,f251]) ).
fof(f4281,plain,
! [X0,X1] :
( ~ hskp3
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1785,f203]) ).
fof(f4301,plain,
! [X0] :
( ~ hskp24
| ~ hskp3
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c3_1(a1232)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f4281,f257]) ).
fof(f4309,plain,
! [X0] :
( ~ hskp24
| ~ hskp3
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f4301,f225]) ).
fof(f4339,plain,
! [X0,X1] :
( ~ hskp6
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1787,f245]) ).
fof(f4359,plain,
! [X0] :
( ~ hskp24
| ~ hskp6
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c3_1(a1232)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f4339,f257]) ).
fof(f4367,plain,
! [X0] :
( ~ hskp24
| ~ hskp6
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c3_1(a1232) ),
inference(forward_subsumption_resolution,[status(thm)],[f4359,f200]) ).
fof(f4388,plain,
! [X0,X1] :
( ~ hskp8
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f1788,f198]) ).
fof(f4408,plain,
! [X0] :
( ~ hskp24
| ~ hskp8
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c3_1(a1232)
| ~ c2_1(a1180) ),
inference(resolution,[status(thm)],[f4388,f257]) ).
fof(f4416,plain,
! [X0] :
( ~ hskp24
| ~ hskp8
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f4408,f225]) ).
fof(f4428,plain,
! [X0,X1] :
( ~ hskp16
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f1789,f190]) ).
fof(f4448,plain,
! [X0] :
( ~ hskp24
| ~ hskp16
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c3_1(a1232)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f4428,f257]) ).
fof(f4457,plain,
! [X0] :
( ~ hskp24
| ~ hskp16
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f4448,f225]) ).
fof(f4458,plain,
! [X0,X1] :
( ~ hskp2
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1847,f253]) ).
fof(f4475,plain,
! [X0] :
( ~ hskp16
| ~ hskp2
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1199)
| ~ c2_1(a1199)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f4458,f271]) ).
fof(f4476,plain,
! [X0] :
( ~ hskp23
| ~ hskp2
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1218)
| ~ c2_1(a1218)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f4458,f261]) ).
fof(f4485,plain,
! [X0] :
( ~ hskp16
| ~ hskp2
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1199)
| ~ c2_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f4475,f204]) ).
fof(f4486,plain,
! [X0] :
( ~ hskp23
| ~ hskp2
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1218)
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f4476,f204]) ).
fof(f4770,plain,
! [X0,X1] :
( ~ hskp3
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f1875,f203]) ).
fof(f4777,plain,
! [X0] :
( ~ hskp21
| ~ hskp3
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ c2_1(X0)
| ~ c3_1(a1207)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f4770,f263]) ).
fof(f4780,plain,
! [X0] :
( ~ hskp24
| ~ hskp3
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c3_1(a1232)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f4770,f258]) ).
fof(f4787,plain,
! [X0] :
( ~ hskp21
| ~ hskp3
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ c2_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f4777,f229]) ).
fof(f4788,plain,
! [X0] :
( ~ hskp24
| ~ hskp3
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f4780,f225]) ).
fof(f4889,plain,
! [X0,X1] :
( ~ hskp6
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1877,f245]) ).
fof(f4892,plain,
! [X0] :
( ~ hskp14
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1194)
| ~ c2_1(X0)
| ~ c3_1(a1194)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f4889,f275]) ).
fof(f4896,plain,
! [X0] :
( ~ hskp21
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ c2_1(X0)
| ~ c3_1(a1207)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f4889,f263]) ).
fof(f4899,plain,
! [X0] :
( ~ hskp24
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c3_1(a1232)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f4889,f258]) ).
fof(f4904,plain,
! [X0] :
( ~ hskp14
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1194)
| ~ c2_1(X0)
| ~ c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f4892,f200]) ).
fof(f4906,plain,
! [X0] :
( ~ hskp21
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ c2_1(X0)
| ~ c3_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f4896,f200]) ).
fof(f4907,plain,
! [X0] :
( ~ hskp24
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c3_1(a1232) ),
inference(forward_subsumption_resolution,[status(thm)],[f4899,f200]) ).
fof(f4908,plain,
! [X0,X1] :
( ~ hskp8
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f1878,f198]) ).
fof(f4918,plain,
! [X0] :
( ~ hskp24
| ~ hskp8
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c3_1(a1232)
| ~ c2_1(a1180) ),
inference(resolution,[status(thm)],[f4908,f258]) ).
fof(f4926,plain,
! [X0] :
( ~ hskp24
| ~ hskp8
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f4918,f225]) ).
fof(f4927,plain,
! [X0,X1] :
( ~ hskp16
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f1879,f190]) ).
fof(f4934,plain,
! [X0] :
( ~ hskp21
| ~ hskp16
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ c2_1(X0)
| ~ c3_1(a1207)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f4927,f263]) ).
fof(f4937,plain,
! [X0] :
( ~ hskp24
| ~ hskp16
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c3_1(a1232)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f4927,f258]) ).
fof(f4944,plain,
! [X0] :
( ~ hskp21
| ~ hskp16
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ c2_1(X0)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f4934,f229]) ).
fof(f4945,plain,
! [X0] :
( ~ hskp24
| ~ hskp16
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f4937,f225]) ).
fof(f5135,plain,
! [X0,X1] :
( ~ hskp21
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f1977,f185]) ).
fof(f5142,plain,
! [X0] :
( ~ hskp21
| ~ hskp21
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1207)
| ~ c0_1(a1207)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f5135,f263]) ).
fof(f5150,plain,
! [X0] :
( ~ hskp21
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1207)
| ~ c0_1(a1207) ),
inference(duplicate_literals_removal,[status(thm)],[f5142]) ).
fof(f5151,plain,
! [X0] :
( ~ hskp21
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5150,f228]) ).
fof(f5164,plain,
( ~ hskp1
| ~ hskp21
| c2_1(a1169)
| c0_1(a1169)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f5151,f298]) ).
fof(f5168,plain,
( ~ hskp7
| ~ hskp21
| c2_1(a1179)
| c0_1(a1179)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f5151,f291]) ).
fof(f5171,plain,
( ~ hskp12
| ~ hskp21
| c2_1(a1187)
| c0_1(a1187)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f5151,f280]) ).
fof(f5174,plain,
( ~ hskp23
| ~ hskp21
| c2_1(a1218)
| c0_1(a1218)
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f5151,f261]) ).
fof(f5177,plain,
( ~ hskp1
| ~ hskp21
| c0_1(a1169)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5164,f297]) ).
fof(f5178,plain,
( ~ hskp7
| ~ hskp21
| c0_1(a1179)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5168,f290]) ).
fof(f5180,plain,
( ~ hskp12
| ~ hskp21
| c2_1(a1187)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5171,f278]) ).
fof(f5181,plain,
( ~ hskp23
| ~ hskp21
| c2_1(a1218)
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5174,f259]) ).
fof(f5182,plain,
( ~ hskp21
| ~ hskp1
| hskp17
| ~ c0_1(a1207) ),
inference(backward_subsumption_resolution,[status(thm)],[f3872,f5177]) ).
fof(f5183,plain,
( ~ hskp21
| ~ hskp7
| hskp17
| ~ c0_1(a1207) ),
inference(backward_subsumption_resolution,[status(thm)],[f3924,f5178]) ).
fof(f5248,plain,
( ~ hskp13
| ~ hskp21
| ~ c3_1(a1192)
| ~ c0_1(a1207) ),
inference(backward_subsumption_resolution,[status(thm)],[f4064,f5251]) ).
fof(f5251,plain,
( ~ hskp12
| ~ hskp21
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5180,f279]) ).
fof(f5351,plain,
! [X0,X1] :
( ~ hskp22
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1978,f227]) ).
fof(f5359,plain,
! [X0] :
( ~ hskp22
| ~ hskp22
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1211)
| ~ c0_1(a1211)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f5351,f262]) ).
fof(f5366,plain,
! [X0] :
( ~ hskp22
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1211)
| ~ c0_1(a1211)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f5359]) ).
fof(f5367,plain,
! [X0] :
( ~ hskp22
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1211)
| ~ c0_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f5366,f184]) ).
fof(f5650,plain,
! [X0,X1] :
( ~ hskp0
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2021,f256]) ).
fof(f5651,plain,
! [X0] :
( ~ hskp7
| ~ hskp0
| c2_1(a1179)
| ~ c0_1(a1179)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f5650,f289]) ).
fof(f5655,plain,
! [X0] :
( ~ hskp17
| ~ hskp0
| c2_1(a1200)
| ~ c0_1(a1200)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f5650,f268]) ).
fof(f5658,plain,
! [X0] :
( ~ hskp22
| ~ hskp0
| c2_1(a1211)
| ~ c0_1(a1211)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f5650,f262]) ).
fof(f5664,plain,
! [X0] :
( ~ hskp7
| ~ hskp0
| c2_1(a1179)
| ~ c0_1(a1179)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5651,f206]) ).
fof(f5665,plain,
! [X0] :
( ~ hskp17
| ~ hskp0
| c2_1(a1200)
| ~ c0_1(a1200)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5655,f206]) ).
fof(f5667,plain,
! [X0] :
( ~ hskp22
| ~ hskp0
| c2_1(a1211)
| ~ c0_1(a1211)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5658,f206]) ).
fof(f5678,plain,
( ~ hskp21
| c2_1(a1192)
| c0_1(a1192)
| ~ c0_1(a1207)
| ~ hskp13
| ~ hskp21
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f5248,f5151]) ).
fof(f5708,plain,
( c2_1(a1192)
| c0_1(a1192)
| ~ hskp13
| ~ hskp21
| ~ c0_1(a1207) ),
inference(duplicate_literals_removal,[status(thm)],[f5678]) ).
fof(f5709,plain,
( c2_1(a1192)
| ~ hskp13
| ~ hskp21
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5708,f276]) ).
fof(f5852,plain,
( ~ hskp21
| hskp19
| ~ c0_1(a1207) ),
inference(backward_subsumption_resolution,[status(thm)],[f662,f5853]) ).
fof(f5853,plain,
( ~ hskp13
| ~ hskp21
| ~ c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f5709,f277]) ).
fof(f5955,plain,
! [X0,X1] :
( ~ hskp1
| c2_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f2022,f205]) ).
fof(f5964,plain,
! [X0] :
( ~ hskp22
| ~ hskp1
| c2_1(a1211)
| ~ c0_1(a1211)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f5955,f262]) ).
fof(f5973,plain,
! [X0] :
( ~ hskp22
| ~ hskp1
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f5964,f226]) ).
fof(f6244,plain,
! [X0,X1] :
( ~ hskp3
| c0_1(X1)
| c3_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f2076,f203]) ).
fof(f6255,plain,
! [X0] :
( ~ hskp3
| ~ hskp3
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(a1174)
| ~ c0_1(a1174)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f6244,f295]) ).
fof(f6273,plain,
! [X0] :
( ~ hskp3
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(a1174)
| ~ c2_1(a1174) ),
inference(duplicate_literals_removal,[status(thm)],[f6255]) ).
fof(f6274,plain,
! [X0] :
( ~ hskp3
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f6273,f250]) ).
fof(f6315,plain,
! [X0,X1] :
( ~ hskp3
| c1_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0)
| ~ c2_1(a1174) ),
inference(backward_subsumption_resolution,[status(thm)],[f4770,f6274]) ).
fof(f6335,plain,
( ~ hskp2
| ~ hskp3
| ~ c3_1(a1172)
| ~ c1_1(a1172)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f6274,f296]) ).
fof(f6348,plain,
( ~ hskp2
| ~ hskp3
| ~ c1_1(a1172)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f6335,f253]) ).
fof(f6983,plain,
! [X0] :
( ~ hskp7
| ~ hskp0
| ~ c0_1(a1179)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5664,f290]) ).
fof(f7039,plain,
( ~ hskp22
| ~ hskp7
| ~ hskp0
| ~ c0_1(a1179)
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f6983,f227]) ).
fof(f7091,plain,
( ~ hskp22
| ~ hskp7
| ~ hskp0
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f7039,f226]) ).
fof(f7219,plain,
( ~ hskp7
| hskp17
| ~ c0_1(a1179) ),
inference(backward_subsumption_resolution,[status(thm)],[f628,f7220]) ).
fof(f7220,plain,
( ~ hskp22
| ~ hskp7
| ~ c0_1(a1179) ),
inference(forward_subsumption_resolution,[status(thm)],[f7091,f469]) ).
fof(f7941,plain,
! [X0] :
( ~ hskp17
| ~ hskp0
| c2_1(a1200)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5665,f235]) ).
fof(f7942,plain,
! [X0] :
( ~ hskp17
| ~ hskp17
| ~ hskp0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f7941,f269]) ).
fof(f7943,plain,
! [X0] :
( ~ hskp17
| ~ hskp0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f7942]) ).
fof(f7944,plain,
! [X0] :
( ~ hskp17
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7943,f467]) ).
fof(f8059,plain,
( ~ hskp17
| ~ hskp0
| hskp6
| ~ hskp17
| ~ c0_1(a1200) ),
inference(resolution,[status(thm)],[f7944,f2711]) ).
fof(f8065,plain,
( ~ hskp17
| ~ hskp15
| hskp26
| ~ hskp17
| ~ c0_1(a1200) ),
inference(resolution,[status(thm)],[f7944,f1671]) ).
fof(f8069,plain,
( ~ hskp17
| hskp15
| hskp14
| ~ hskp17
| ~ c0_1(a1200) ),
inference(resolution,[status(thm)],[f7944,f547]) ).
fof(f8105,plain,
( ~ hskp21
| ~ hskp17
| ~ c0_1(a1207) ),
inference(resolution,[status(thm)],[f7944,f229]) ).
fof(f8106,plain,
( ~ hskp22
| ~ hskp17
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f7944,f227]) ).
fof(f8164,plain,
( ~ hskp0
| hskp6
| ~ hskp17
| ~ c0_1(a1200) ),
inference(duplicate_literals_removal,[status(thm)],[f8059]) ).
fof(f8165,plain,
( ~ hskp0
| hskp6
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f8164,f235]) ).
fof(f8176,plain,
( ~ hskp15
| hskp26
| ~ hskp17
| ~ c0_1(a1200) ),
inference(duplicate_literals_removal,[status(thm)],[f8065]) ).
fof(f8177,plain,
( ~ hskp15
| hskp26
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f8176,f235]) ).
fof(f8184,plain,
( hskp15
| hskp14
| ~ hskp17
| ~ c0_1(a1200) ),
inference(duplicate_literals_removal,[status(thm)],[f8069]) ).
fof(f8185,plain,
( hskp15
| hskp14
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f8184,f235]) ).
fof(f8189,plain,
( ~ hskp22
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f8106,f226]) ).
fof(f8228,plain,
( ~ hskp22
| ~ hskp11
| ~ c2_1(a1211) ),
inference(backward_subsumption_resolution,[status(thm)],[f4068,f8189]) ).
fof(f8277,plain,
( hskp6
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f8165,f467]) ).
fof(f8285,plain,
( ~ hskp15
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f8177,f1047]) ).
fof(f8302,plain,
( ~ hskp17
| c3_1(a1200)
| c3_1(a1194) ),
inference(backward_subsumption_resolution,[status(thm)],[f1646,f8303]) ).
fof(f8303,plain,
( hskp14
| ~ hskp17 ),
inference(forward_subsumption_resolution,[status(thm)],[f8185,f8285]) ).
fof(f8478,plain,
( ~ hskp21
| ~ hskp7
| ~ c0_1(a1207) ),
inference(backward_subsumption_resolution,[status(thm)],[f5183,f8105]) ).
fof(f8479,plain,
( ~ hskp21
| ~ hskp1
| ~ c0_1(a1207) ),
inference(backward_subsumption_resolution,[status(thm)],[f5182,f8105]) ).
fof(f8542,plain,
( ~ hskp13
| ~ hskp22
| hskp7
| ~ hskp22
| ~ hskp11 ),
inference(resolution,[status(thm)],[f8228,f2706]) ).
fof(f8544,plain,
! [X0] :
( ~ hskp22
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp22
| ~ hskp11 ),
inference(resolution,[status(thm)],[f8228,f1390]) ).
fof(f8545,plain,
( ~ hskp22
| hskp0
| ~ hskp22
| ~ hskp11 ),
inference(resolution,[status(thm)],[f8228,f468]) ).
fof(f8558,plain,
( ~ hskp13
| hskp7
| ~ hskp22
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f8542]) ).
fof(f8560,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp22
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f8544]) ).
fof(f8561,plain,
( hskp0
| ~ hskp22
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f8545]) ).
fof(f9371,plain,
( ~ hskp26
| ~ c3_1(a1190)
| ~ c0_1(a1190)
| ~ hskp22
| ~ hskp11 ),
inference(resolution,[status(thm)],[f8560,f220]) ).
fof(f9454,plain,
( ~ hskp26
| ~ c3_1(a1190)
| ~ hskp22
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f9371,f219]) ).
fof(f9673,plain,
( ~ hskp26
| ~ hskp22
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f9454,f221]) ).
fof(f9825,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp3
| c2_1(a1232)
| c0_1(a1232)
| c2_1(a1232)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f4309,f258]) ).
fof(f9834,plain,
( ~ hskp24
| ~ hskp3
| c0_1(a1232)
| c2_1(a1232)
| ~ c2_1(a1174) ),
inference(duplicate_literals_removal,[status(thm)],[f9825]) ).
fof(f9835,plain,
( ~ hskp24
| ~ hskp3
| c2_1(a1232)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f9834,f257]) ).
fof(f10314,plain,
! [X0] :
( ~ hskp24
| ~ hskp6
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a1232) ),
inference(forward_subsumption_resolution,[status(thm)],[f4367,f225]) ).
fof(f10327,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp6
| c2_1(a1232)
| c0_1(a1232)
| c2_1(a1232) ),
inference(resolution,[status(thm)],[f10314,f258]) ).
fof(f10336,plain,
( ~ hskp24
| ~ hskp6
| c0_1(a1232)
| c2_1(a1232) ),
inference(duplicate_literals_removal,[status(thm)],[f10327]) ).
fof(f10337,plain,
( ~ hskp24
| ~ hskp6
| c2_1(a1232) ),
inference(forward_subsumption_resolution,[status(thm)],[f10336,f257]) ).
fof(f10563,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp8
| c2_1(a1232)
| c0_1(a1232)
| c2_1(a1232)
| ~ c2_1(a1180) ),
inference(resolution,[status(thm)],[f4416,f258]) ).
fof(f10572,plain,
( ~ hskp24
| ~ hskp8
| c0_1(a1232)
| c2_1(a1232)
| ~ c2_1(a1180) ),
inference(duplicate_literals_removal,[status(thm)],[f10563]) ).
fof(f10573,plain,
( ~ hskp24
| ~ hskp8
| c2_1(a1232)
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f10572,f257]) ).
fof(f11087,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp16
| c2_1(a1232)
| c0_1(a1232)
| c2_1(a1232)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f4457,f258]) ).
fof(f11096,plain,
( ~ hskp24
| ~ hskp16
| c0_1(a1232)
| c2_1(a1232)
| ~ c1_1(a1199) ),
inference(duplicate_literals_removal,[status(thm)],[f11087]) ).
fof(f11097,plain,
( ~ hskp24
| ~ hskp16
| c2_1(a1232)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f11096,f257]) ).
fof(f11333,plain,
! [X0] :
( ~ hskp16
| ~ hskp2
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f4485,f236]) ).
fof(f11485,plain,
! [X0] :
( ~ hskp23
| ~ hskp2
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f4486,f259]) ).
fof(f11497,plain,
( ~ hskp23
| ~ hskp23
| ~ hskp2
| c3_1(a1218)
| c0_1(a1218)
| ~ c2_1(a1218) ),
inference(resolution,[status(thm)],[f11485,f260]) ).
fof(f11507,plain,
( ~ hskp23
| ~ hskp2
| c3_1(a1218)
| c0_1(a1218)
| ~ c2_1(a1218) ),
inference(duplicate_literals_removal,[status(thm)],[f11497]) ).
fof(f11508,plain,
( ~ hskp23
| ~ hskp2
| c3_1(a1218)
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f11507,f259]) ).
fof(f11531,plain,
( ~ hskp23
| ~ hskp2
| ~ c2_1(a1218) ),
inference(forward_subsumption_resolution,[status(thm)],[f11508,f261]) ).
fof(f11537,plain,
( ~ hskp23
| ~ hskp21
| ~ c0_1(a1207)
| ~ hskp23
| ~ hskp2 ),
inference(resolution,[status(thm)],[f11531,f5181]) ).
fof(f11546,plain,
( ~ hskp23
| ~ hskp0
| hskp6
| ~ hskp23
| ~ hskp2 ),
inference(resolution,[status(thm)],[f11531,f2712]) ).
fof(f11578,plain,
( ~ hskp21
| ~ c0_1(a1207)
| ~ hskp23
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f11537]) ).
fof(f11587,plain,
( ~ hskp0
| hskp6
| ~ hskp23
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f11546]) ).
fof(f11607,plain,
( ~ hskp23
| ~ hskp21
| hskp0
| ~ hskp21
| ~ hskp23
| ~ hskp2 ),
inference(resolution,[status(thm)],[f11578,f1604]) ).
fof(f11648,plain,
( hskp0
| ~ hskp21
| ~ hskp23
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f11607]) ).
fof(f13697,plain,
( ~ hskp21
| ~ hskp21
| ~ hskp3
| c0_1(a1207)
| c0_1(a1207)
| ~ c2_1(a1207)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f4787,f263]) ).
fof(f13708,plain,
( ~ hskp21
| ~ hskp3
| c0_1(a1207)
| ~ c2_1(a1207)
| ~ c2_1(a1174) ),
inference(duplicate_literals_removal,[status(thm)],[f13697]) ).
fof(f13709,plain,
( ~ hskp21
| ~ hskp3
| c0_1(a1207)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f13708,f228]) ).
fof(f13712,plain,
! [X0] :
( ~ hskp24
| ~ hskp3
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f4788,f257]) ).
fof(f13725,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp3
| c0_1(a1232)
| ~ c2_1(a1232)
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f13712,f258]) ).
fof(f13736,plain,
( ~ hskp24
| ~ hskp3
| c0_1(a1232)
| ~ c2_1(a1232)
| ~ c2_1(a1174) ),
inference(duplicate_literals_removal,[status(thm)],[f13725]) ).
fof(f13737,plain,
( ~ hskp24
| ~ hskp3
| c0_1(a1232)
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f13736,f9835]) ).
fof(f14478,plain,
( ~ hskp21
| ~ hskp7
| ~ hskp21
| ~ hskp3
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f13709,f8478]) ).
fof(f14480,plain,
( ~ hskp13
| ~ hskp21
| ~ hskp21
| ~ hskp3
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f13709,f5853]) ).
fof(f14482,plain,
( ~ hskp12
| ~ hskp21
| ~ hskp21
| ~ hskp3
| ~ c2_1(a1174) ),
inference(resolution,[status(thm)],[f13709,f5251]) ).
fof(f14489,plain,
( ~ hskp7
| ~ hskp21
| ~ hskp3
| ~ c2_1(a1174) ),
inference(duplicate_literals_removal,[status(thm)],[f14478]) ).
fof(f14491,plain,
( ~ hskp13
| ~ hskp21
| ~ hskp3
| ~ c2_1(a1174) ),
inference(duplicate_literals_removal,[status(thm)],[f14480]) ).
fof(f14493,plain,
( ~ hskp12
| ~ hskp21
| ~ hskp3
| ~ c2_1(a1174) ),
inference(duplicate_literals_removal,[status(thm)],[f14482]) ).
fof(f14657,plain,
( ~ hskp3
| hskp17
| ~ c2_1(a1211)
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f14489,f3932]) ).
fof(f14660,plain,
( ~ hskp3
| hskp17
| hskp22
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f14489,f533]) ).
fof(f14684,plain,
( hskp17
| ~ c2_1(a1211)
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f14657]) ).
fof(f14687,plain,
( hskp17
| hskp22
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f14660]) ).
fof(f14749,plain,
( ~ hskp3
| hskp17
| ~ c2_1(a1211)
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f14491,f3932]) ).
fof(f14752,plain,
( ~ hskp3
| hskp17
| hskp22
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f14491,f533]) ).
fof(f14774,plain,
( hskp17
| ~ c2_1(a1211)
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f14749]) ).
fof(f14777,plain,
( hskp17
| hskp22
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f14752]) ).
fof(f14793,plain,
( ~ hskp3
| hskp17
| hskp22
| ~ hskp12
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f14493,f533]) ).
fof(f14819,plain,
( hskp17
| hskp22
| ~ hskp12
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f14793]) ).
fof(f14869,plain,
( ~ hskp24
| ~ hskp3
| ~ c2_1(a1174) ),
inference(forward_subsumption_resolution,[status(thm)],[f13737,f257]) ).
fof(f14875,plain,
( ~ hskp3
| hskp17
| ~ c2_1(a1211)
| ~ hskp24
| ~ hskp3 ),
inference(resolution,[status(thm)],[f14869,f3932]) ).
fof(f14878,plain,
( ~ hskp3
| hskp17
| hskp22
| ~ hskp24
| ~ hskp3 ),
inference(resolution,[status(thm)],[f14869,f533]) ).
fof(f14901,plain,
( hskp17
| ~ c2_1(a1211)
| ~ hskp24
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f14875]) ).
fof(f14904,plain,
( hskp17
| hskp22
| ~ hskp24
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f14878]) ).
fof(f15048,plain,
! [X0] :
( ~ hskp14
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f4904,f274]) ).
fof(f15057,plain,
( ~ hskp14
| ~ hskp14
| ~ hskp6
| c0_1(a1194)
| ~ c2_1(a1194)
| ~ c3_1(a1194) ),
inference(resolution,[status(thm)],[f15048,f275]) ).
fof(f15071,plain,
( ~ hskp14
| ~ hskp6
| c0_1(a1194)
| ~ c2_1(a1194)
| ~ c3_1(a1194) ),
inference(duplicate_literals_removal,[status(thm)],[f15057]) ).
fof(f15072,plain,
( ~ hskp14
| ~ hskp6
| c0_1(a1194)
| ~ c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f15071,f238]) ).
fof(f15105,plain,
! [X0] :
( ~ hskp21
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1207)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4906,f229]) ).
fof(f15118,plain,
( ~ hskp21
| ~ hskp21
| ~ hskp6
| c0_1(a1207)
| c0_1(a1207)
| ~ c2_1(a1207) ),
inference(resolution,[status(thm)],[f15105,f263]) ).
fof(f15128,plain,
( ~ hskp21
| ~ hskp6
| c0_1(a1207)
| ~ c2_1(a1207) ),
inference(duplicate_literals_removal,[status(thm)],[f15118]) ).
fof(f15129,plain,
( ~ hskp21
| ~ hskp6
| c0_1(a1207) ),
inference(forward_subsumption_resolution,[status(thm)],[f15128,f228]) ).
fof(f15139,plain,
( ~ hskp21
| ~ hskp1
| ~ hskp21
| ~ hskp6 ),
inference(resolution,[status(thm)],[f15129,f8479]) ).
fof(f15141,plain,
( ~ hskp21
| ~ hskp17
| ~ hskp21
| ~ hskp6 ),
inference(resolution,[status(thm)],[f15129,f8105]) ).
fof(f15144,plain,
( ~ hskp12
| ~ hskp21
| ~ hskp21
| ~ hskp6 ),
inference(resolution,[status(thm)],[f15129,f5251]) ).
fof(f15149,plain,
( ~ hskp1
| ~ hskp21
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f15139]) ).
fof(f15151,plain,
( ~ hskp17
| ~ hskp21
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f15141]) ).
fof(f15152,plain,
( ~ hskp17
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f15151,f8277]) ).
fof(f15155,plain,
( ~ hskp12
| ~ hskp21
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f15144]) ).
fof(f15156,plain,
( hskp22
| ~ hskp12
| ~ hskp21
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f14819,f15152]) ).
fof(f15157,plain,
( hskp22
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f14777,f15152]) ).
fof(f15158,plain,
( hskp22
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f14687,f15152]) ).
fof(f15212,plain,
! [X0] :
( ~ hskp24
| ~ hskp6
| c1_1(X0)
| c0_1(X0)
| c0_1(a1232)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4907,f225]) ).
fof(f15228,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp6
| c0_1(a1232)
| c0_1(a1232)
| ~ c2_1(a1232) ),
inference(resolution,[status(thm)],[f15212,f258]) ).
fof(f15239,plain,
( ~ hskp24
| ~ hskp6
| c0_1(a1232)
| ~ c2_1(a1232) ),
inference(duplicate_literals_removal,[status(thm)],[f15228]) ).
fof(f15240,plain,
( ~ hskp24
| ~ hskp6
| c0_1(a1232) ),
inference(forward_subsumption_resolution,[status(thm)],[f15239,f10337]) ).
fof(f15273,plain,
( ~ hskp0
| ~ hskp23
| ~ hskp2
| ~ hskp1
| ~ hskp21 ),
inference(resolution,[status(thm)],[f15149,f11587]) ).
fof(f15294,plain,
( ~ hskp23
| ~ hskp2
| ~ hskp1
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f15273,f11648]) ).
fof(f15366,plain,
( ~ hskp12
| hskp3
| ~ hskp12
| ~ hskp21 ),
inference(resolution,[status(thm)],[f15155,f541]) ).
fof(f15370,plain,
( hskp3
| ~ hskp12
| ~ hskp21 ),
inference(duplicate_literals_removal,[status(thm)],[f15366]) ).
fof(f15423,plain,
( ~ hskp12
| ~ hskp21
| ~ c2_1(a1174) ),
inference(backward_subsumption_resolution,[status(thm)],[f14493,f15370]) ).
fof(f15507,plain,
( hskp22
| ~ hskp12
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f15156,f15370]) ).
fof(f15513,plain,
( ~ hskp24
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f15240,f257]) ).
fof(f15514,plain,
( hskp17
| hskp26
| ~ hskp6 ),
inference(resolution,[status(thm)],[f15513,f207]) ).
fof(f15515,plain,
( ~ hskp22
| ~ hskp11
| hskp17
| ~ hskp6 ),
inference(resolution,[status(thm)],[f15514,f9673]) ).
fof(f15517,plain,
( ~ hskp22
| ~ hskp11
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f15515,f8189]) ).
fof(f15537,plain,
( ~ hskp7
| ~ hskp0
| ~ hskp22
| ~ hskp11 ),
inference(resolution,[status(thm)],[f15517,f2709]) ).
fof(f15547,plain,
( ~ hskp7
| ~ hskp22
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f15537,f8561]) ).
fof(f15550,plain,
( ~ hskp13
| ~ hskp22
| ~ hskp11 ),
inference(backward_subsumption_resolution,[status(thm)],[f8558,f15547]) ).
fof(f15637,plain,
( ~ hskp1
| hskp19
| ~ hskp2
| ~ hskp1
| ~ hskp21 ),
inference(resolution,[status(thm)],[f15294,f621]) ).
fof(f15647,plain,
( hskp19
| ~ hskp2
| ~ hskp1
| ~ hskp21 ),
inference(duplicate_literals_removal,[status(thm)],[f15637]) ).
fof(f15700,plain,
! [X0] :
( ~ hskp24
| ~ hskp8
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f4926,f257]) ).
fof(f15716,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp8
| c0_1(a1232)
| ~ c2_1(a1232)
| ~ c2_1(a1180) ),
inference(resolution,[status(thm)],[f15700,f258]) ).
fof(f15727,plain,
( ~ hskp24
| ~ hskp8
| c0_1(a1232)
| ~ c2_1(a1232)
| ~ c2_1(a1180) ),
inference(duplicate_literals_removal,[status(thm)],[f15716]) ).
fof(f15728,plain,
( ~ hskp24
| ~ hskp8
| c0_1(a1232)
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f15727,f10573]) ).
fof(f15831,plain,
( ~ hskp3
| hskp17
| ~ c2_1(a1211)
| ~ hskp12
| ~ hskp21 ),
inference(resolution,[status(thm)],[f15423,f3932]) ).
fof(f15857,plain,
( ~ hskp3
| ~ c2_1(a1211)
| ~ hskp12
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f15831,f15152]) ).
fof(f16095,plain,
( ~ hskp21
| ~ hskp21
| ~ hskp16
| c0_1(a1207)
| c0_1(a1207)
| ~ c2_1(a1207)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f4944,f263]) ).
fof(f16105,plain,
( ~ hskp21
| ~ hskp16
| c0_1(a1207)
| ~ c2_1(a1207)
| ~ c1_1(a1199) ),
inference(duplicate_literals_removal,[status(thm)],[f16095]) ).
fof(f16106,plain,
( ~ hskp21
| ~ hskp16
| c0_1(a1207)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f16105,f228]) ).
fof(f16109,plain,
! [X0] :
( ~ hskp24
| ~ hskp16
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f4945,f257]) ).
fof(f16125,plain,
( ~ hskp24
| ~ hskp24
| ~ hskp16
| c0_1(a1232)
| ~ c2_1(a1232)
| ~ c1_1(a1199) ),
inference(resolution,[status(thm)],[f16109,f258]) ).
fof(f16136,plain,
( ~ hskp24
| ~ hskp16
| c0_1(a1232)
| ~ c2_1(a1232)
| ~ c1_1(a1199) ),
inference(duplicate_literals_removal,[status(thm)],[f16125]) ).
fof(f16137,plain,
( ~ hskp24
| ~ hskp16
| c0_1(a1232)
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f16136,f11097]) ).
fof(f16996,plain,
( ~ c2_1(a1211)
| ~ hskp12
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f15857,f15370]) ).
fof(f16999,plain,
( ~ hskp22
| ~ hskp3
| hskp11
| ~ hskp12
| ~ hskp21 ),
inference(resolution,[status(thm)],[f16996,f3854]) ).
fof(f17027,plain,
( ~ hskp22
| hskp11
| ~ hskp12
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f16999,f15370]) ).
fof(f17043,plain,
( hskp11
| ~ hskp12
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f17027,f15507]) ).
fof(f18882,plain,
! [X0] :
( ~ hskp22
| hskp1
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1211) ),
inference(backward_subsumption_resolution,[status(thm)],[f3208,f18883]) ).
fof(f18883,plain,
! [X0] :
( ~ hskp22
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f5367,f226]) ).
fof(f18917,plain,
( ~ hskp1
| ~ hskp22
| c2_1(a1169)
| c0_1(a1169)
| ~ c2_1(a1211) ),
inference(resolution,[status(thm)],[f18883,f298]) ).
fof(f18948,plain,
( ~ hskp1
| ~ hskp22
| c0_1(a1169)
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f18917,f297]) ).
fof(f19744,plain,
( ~ hskp12
| ~ hskp22
| hskp1
| c2_1(a1187)
| ~ c2_1(a1211) ),
inference(resolution,[status(thm)],[f18882,f278]) ).
fof(f19745,plain,
( ~ hskp13
| ~ hskp22
| hskp1
| c2_1(a1192)
| ~ c2_1(a1211) ),
inference(resolution,[status(thm)],[f18882,f276]) ).
fof(f19764,plain,
( ~ hskp12
| ~ hskp22
| hskp1
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f19744,f279]) ).
fof(f19765,plain,
( ~ hskp13
| ~ hskp22
| hskp1
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f19745,f277]) ).
fof(f19906,plain,
( ~ c2_1(a1211)
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f14684,f15152]) ).
fof(f19909,plain,
( ~ hskp22
| ~ hskp3
| hskp11
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f19906,f3854]) ).
fof(f19935,plain,
( ~ hskp22
| hskp11
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f19909]) ).
fof(f19936,plain,
( ~ hskp22
| ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f19935,f15547]) ).
fof(f19956,plain,
( ~ hskp7
| ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f19936,f15158]) ).
fof(f20390,plain,
( ~ c2_1(a1211)
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f14774,f15152]) ).
fof(f20393,plain,
( ~ hskp22
| ~ hskp3
| hskp11
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f20390,f3854]) ).
fof(f20419,plain,
( ~ hskp22
| hskp11
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f20393]) ).
fof(f20420,plain,
( ~ hskp22
| ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f20419,f15550]) ).
fof(f20435,plain,
( ~ hskp13
| ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f20420,f15157]) ).
fof(f20717,plain,
( ~ hskp14
| ~ hskp6
| ~ c3_1(a1194) ),
inference(forward_subsumption_resolution,[status(thm)],[f15072,f274]) ).
fof(f20719,plain,
( ~ hskp17
| c3_1(a1200)
| ~ hskp14
| ~ hskp6 ),
inference(resolution,[status(thm)],[f20717,f8302]) ).
fof(f20725,plain,
( ~ hskp14
| hskp0
| ~ hskp14
| ~ hskp6 ),
inference(resolution,[status(thm)],[f20717,f1408]) ).
fof(f20771,plain,
( ~ hskp17
| c3_1(a1200)
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f20719,f8277]) ).
fof(f20778,plain,
( hskp0
| ~ hskp14
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f20725]) ).
fof(f21217,plain,
( ~ hskp17
| c3_1(a1200) ),
inference(forward_subsumption_resolution,[status(thm)],[f20771,f8303]) ).
fof(f21219,plain,
( ~ hskp17
| ~ c0_1(a1200)
| ~ hskp17 ),
inference(resolution,[status(thm)],[f21217,f7944]) ).
fof(f21221,plain,
( ~ c0_1(a1200)
| ~ hskp17 ),
inference(duplicate_literals_removal,[status(thm)],[f21219]) ).
fof(f21222,plain,
~ hskp17,
inference(forward_subsumption_resolution,[status(thm)],[f21221,f235]) ).
fof(f21268,plain,
( hskp26
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f15514,f21222]) ).
fof(f21269,plain,
( hskp22
| ~ hskp24
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f14904,f21222]) ).
fof(f21277,plain,
( ~ hskp1
| hskp22
| ~ c0_1(a1169) ),
inference(backward_subsumption_resolution,[status(thm)],[f627,f21222]) ).
fof(f21278,plain,
( ~ hskp11
| hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f536,f21222]) ).
fof(f21279,plain,
( ~ hskp3
| hskp22
| c2_1(a1174) ),
inference(backward_subsumption_resolution,[status(thm)],[f533,f21222]) ).
fof(f21280,plain,
! [X0] :
( hskp22
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f313,f21222]) ).
fof(f21281,plain,
( hskp16
| hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f210,f21222]) ).
fof(f21282,plain,
( hskp2
| hskp13 ),
inference(backward_subsumption_resolution,[status(thm)],[f209,f21222]) ).
fof(f21283,plain,
( hskp24
| hskp26 ),
inference(backward_subsumption_resolution,[status(thm)],[f207,f21222]) ).
fof(f21284,plain,
( ~ c2_1(a1211)
| ~ hskp24
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f14901,f21222]) ).
fof(f21285,plain,
( ~ hskp7
| ~ c0_1(a1179) ),
inference(backward_subsumption_resolution,[status(thm)],[f7219,f21222]) ).
fof(f21287,plain,
( ~ hskp1
| ~ c2_1(a1211)
| ~ c0_1(a1169) ),
inference(backward_subsumption_resolution,[status(thm)],[f3931,f21222]) ).
fof(f21313,plain,
( hskp0
| ~ hskp11 ),
inference(backward_subsumption_resolution,[status(thm)],[f8561,f21278]) ).
fof(f21314,plain,
( ~ hskp11
| ~ c2_1(a1211) ),
inference(backward_subsumption_resolution,[status(thm)],[f8228,f21278]) ).
fof(f21522,plain,
( ~ hskp7
| hskp6
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f537,f21285]) ).
fof(f21868,plain,
( ~ hskp22
| ~ hskp3
| hskp11
| ~ hskp24
| ~ hskp3 ),
inference(resolution,[status(thm)],[f21284,f3854]) ).
fof(f21886,plain,
( ~ hskp22
| hskp11
| ~ hskp24
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f21868]) ).
fof(f21887,plain,
( hskp11
| ~ hskp24
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f21886,f21269]) ).
fof(f26821,plain,
( ~ hskp24
| ~ hskp8
| ~ c2_1(a1180) ),
inference(forward_subsumption_resolution,[status(thm)],[f15728,f257]) ).
fof(f26826,plain,
( ~ hskp8
| hskp6
| hskp3
| ~ hskp24
| ~ hskp8 ),
inference(resolution,[status(thm)],[f26821,f538]) ).
fof(f26841,plain,
( hskp6
| hskp3
| ~ hskp24
| ~ hskp8 ),
inference(duplicate_literals_removal,[status(thm)],[f26826]) ).
fof(f26842,plain,
( hskp3
| ~ hskp24
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f26841,f15513]) ).
fof(f28350,plain,
! [X0] :
( ~ hskp22
| ~ hskp0
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5667,f226]) ).
fof(f28355,plain,
! [X0] :
( ~ hskp11
| ~ hskp22
| ~ hskp0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f28350,f21314]) ).
fof(f28362,plain,
! [X0] :
( ~ hskp11
| ~ hskp22
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f28355,f21313]) ).
fof(f28380,plain,
! [X0] :
( ~ hskp11
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f28362,f21278]) ).
fof(f28413,plain,
( ~ hskp22
| ~ hskp11
| ~ c0_1(a1211) ),
inference(resolution,[status(thm)],[f28380,f227]) ).
fof(f28457,plain,
( ~ hskp22
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f28413,f226]) ).
fof(f28509,plain,
( ~ hskp22
| ~ hskp3
| c2_1(a1211) ),
inference(backward_subsumption_resolution,[status(thm)],[f3854,f28543]) ).
fof(f28512,plain,
! [X0] :
( ~ hskp1
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(a1169) ),
inference(backward_subsumption_resolution,[status(thm)],[f3739,f28543]) ).
fof(f28520,plain,
! [X0] :
( ~ hskp22
| c0_1(X0)
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3635,f28543]) ).
fof(f28521,plain,
! [X0] :
( ~ hskp19
| c0_1(X0)
| c2_1(a1204)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3606,f28543]) ).
fof(f28529,plain,
( ~ hskp24
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f21887,f28543]) ).
fof(f28532,plain,
( ~ hskp12
| ~ hskp21 ),
inference(backward_subsumption_resolution,[status(thm)],[f17043,f28543]) ).
fof(f28533,plain,
( ~ hskp19
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f3853,f28543]) ).
fof(f28535,plain,
( ~ hskp19
| ~ hskp1
| ~ c0_1(a1169) ),
inference(backward_subsumption_resolution,[status(thm)],[f3761,f28543]) ).
fof(f28543,plain,
~ hskp11,
inference(forward_subsumption_resolution,[status(thm)],[f28457,f21278]) ).
fof(f28545,plain,
! [X0] :
( ~ hskp22
| c2_1(a1211)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f28520,f1390]) ).
fof(f28546,plain,
! [X0] :
( ~ hskp19
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f28521,f266]) ).
fof(f28553,plain,
( ~ hskp24
| ~ hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f26842,f28529]) ).
fof(f28555,plain,
( ~ hskp21
| hskp20
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f682,f28532]) ).
fof(f28567,plain,
( ~ hskp21
| hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f28555,f185]) ).
fof(f28569,plain,
( ~ hskp3
| hskp23
| c2_1(a1174) ),
inference(backward_subsumption_resolution,[status(thm)],[f622,f28533]) ).
fof(f28571,plain,
( ~ hskp21
| ~ c0_1(a1207)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f28533,f5852]) ).
fof(f28572,plain,
( ~ hskp22
| hskp13
| ~ ndr1_0
| ~ hskp3 ),
inference(resolution,[status(thm)],[f28533,f663]) ).
fof(f28574,plain,
( ~ hskp22
| hskp13
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f28572,f203]) ).
fof(f28576,plain,
( hskp26
| ~ hskp8 ),
inference(resolution,[status(thm)],[f28553,f21283]) ).
fof(f28867,plain,
( ~ hskp1
| ~ hskp20
| hskp3
| ~ hskp19
| ~ hskp1 ),
inference(resolution,[status(thm)],[f28535,f3596]) ).
fof(f28870,plain,
( ~ hskp1
| ~ hskp0
| hskp3
| ~ c3_1(a1168)
| ~ hskp19
| ~ hskp1 ),
inference(resolution,[status(thm)],[f28535,f3446]) ).
fof(f28902,plain,
( ~ hskp20
| hskp3
| ~ hskp19
| ~ hskp1 ),
inference(duplicate_literals_removal,[status(thm)],[f28867]) ).
fof(f28903,plain,
( ~ hskp20
| ~ hskp19
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f28902,f28533]) ).
fof(f28907,plain,
( ~ hskp0
| hskp3
| ~ c3_1(a1168)
| ~ hskp19
| ~ hskp1 ),
inference(duplicate_literals_removal,[status(thm)],[f28870]) ).
fof(f28908,plain,
( ~ hskp0
| hskp3
| ~ c3_1(a1168)
| ~ hskp19 ),
inference(forward_subsumption_resolution,[status(thm)],[f28907,f1761]) ).
fof(f28915,plain,
( ~ hskp19
| ~ hskp20
| ~ c0_1(a1205) ),
inference(backward_subsumption_resolution,[status(thm)],[f1961,f28903]) ).
fof(f28916,plain,
( ~ hskp21
| ~ hskp19
| ~ hskp1 ),
inference(resolution,[status(thm)],[f28903,f28567]) ).
fof(f28927,plain,
( ~ hskp26
| ~ hskp19
| ~ hskp21 ),
inference(backward_subsumption_resolution,[status(thm)],[f3482,f28916]) ).
fof(f28928,plain,
( ~ hskp2
| ~ hskp1
| ~ hskp21 ),
inference(backward_subsumption_resolution,[status(thm)],[f15647,f28916]) ).
fof(f28934,plain,
! [X0] :
( ~ hskp1
| hskp6
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(a1169) ),
inference(backward_subsumption_resolution,[status(thm)],[f2663,f28512]) ).
fof(f29000,plain,
( ~ hskp21
| ~ c0_1(a1207)
| ~ hskp26
| ~ hskp21 ),
inference(resolution,[status(thm)],[f28927,f5852]) ).
fof(f29003,plain,
( ~ c0_1(a1207)
| ~ hskp26
| ~ hskp21 ),
inference(duplicate_literals_removal,[status(thm)],[f29000]) ).
fof(f29288,plain,
( ~ hskp21
| ~ hskp3
| ~ c2_1(a1174) ),
inference(backward_subsumption_resolution,[status(thm)],[f13709,f28571]) ).
fof(f29294,plain,
( ~ hskp23
| ~ hskp21
| hskp0
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f28571,f1604]) ).
fof(f29331,plain,
( ~ hskp23
| hskp0
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f29294]) ).
fof(f29332,plain,
( ~ hskp23
| hskp0
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f29331,f499]) ).
fof(f29443,plain,
( ~ hskp19
| ~ c3_1(a1205)
| ~ c1_1(a1205)
| ~ hskp19
| ~ hskp20 ),
inference(resolution,[status(thm)],[f28915,f28546]) ).
fof(f29475,plain,
( ~ c3_1(a1205)
| ~ c1_1(a1205)
| ~ hskp19
| ~ hskp20 ),
inference(duplicate_literals_removal,[status(thm)],[f29443]) ).
fof(f29476,plain,
( ~ c3_1(a1205)
| ~ hskp19
| ~ hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f29475,f230]) ).
fof(f29493,plain,
( ~ hskp21
| ~ hskp6
| ~ hskp26
| ~ hskp21 ),
inference(resolution,[status(thm)],[f29003,f15129]) ).
fof(f29531,plain,
( ~ hskp6
| ~ hskp26
| ~ hskp21 ),
inference(duplicate_literals_removal,[status(thm)],[f29493]) ).
fof(f29532,plain,
( ~ hskp6
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f29531,f21268]) ).
fof(f29543,plain,
( ~ hskp7
| hskp3
| ~ hskp21 ),
inference(resolution,[status(thm)],[f29532,f21522]) ).
fof(f29548,plain,
( ~ hskp0
| ~ hskp23
| ~ hskp2
| ~ hskp21 ),
inference(resolution,[status(thm)],[f29532,f11587]) ).
fof(f29558,plain,
( ~ hskp7
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f29543,f19956]) ).
fof(f29560,plain,
( ~ hskp23
| ~ hskp2
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f29548,f29332]) ).
fof(f29578,plain,
( ~ hskp3
| hskp23
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f29288,f28569]) ).
fof(f29595,plain,
( hskp23
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f29578]) ).
fof(f29608,plain,
( ~ hskp2
| ~ hskp21
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f29595,f29560]) ).
fof(f29610,plain,
( ~ hskp2
| ~ hskp21
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f29608]) ).
fof(f29613,plain,
( hskp13
| ~ hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f29610,f21282]) ).
fof(f29619,plain,
( ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f29613,f20435]) ).
fof(f29624,plain,
( ~ hskp19
| ~ hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f29476,f231]) ).
fof(f29625,plain,
( ~ hskp21
| ~ hskp19 ),
inference(resolution,[status(thm)],[f29624,f28567]) ).
fof(f29629,plain,
( ~ hskp21
| ~ c0_1(a1207) ),
inference(backward_subsumption_resolution,[status(thm)],[f5852,f29625]) ).
fof(f29635,plain,
( ~ hskp21
| ~ hskp16
| ~ c1_1(a1199) ),
inference(backward_subsumption_resolution,[status(thm)],[f16106,f29629]) ).
fof(f29729,plain,
( ~ hskp16
| ~ hskp2
| c3_1(a1199)
| c0_1(a1199)
| c0_1(a1199)
| ~ hskp21
| ~ hskp16 ),
inference(resolution,[status(thm)],[f29635,f11333]) ).
fof(f29805,plain,
( ~ hskp2
| c3_1(a1199)
| c0_1(a1199)
| ~ hskp21
| ~ hskp16 ),
inference(duplicate_literals_removal,[status(thm)],[f29729]) ).
fof(f29806,plain,
( ~ hskp2
| c3_1(a1199)
| ~ hskp21
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f29805,f270]) ).
fof(f30159,plain,
( ~ hskp22
| ~ hskp1
| hskp6
| c2_1(a1211)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f28934,f262]) ).
fof(f30164,plain,
( ~ hskp22
| ~ hskp1
| hskp6
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f30159,f21287]) ).
fof(f30367,plain,
( ~ hskp0
| ~ c3_1(a1168)
| ~ hskp19 ),
inference(forward_subsumption_resolution,[status(thm)],[f28908,f28533]) ).
fof(f30477,plain,
( ~ hskp2
| ~ hskp21
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f29806,f271]) ).
fof(f30478,plain,
( hskp1
| ~ hskp2
| ~ hskp21 ),
inference(resolution,[status(thm)],[f30477,f21281]) ).
fof(f30479,plain,
( ~ hskp2
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f30478,f28928]) ).
fof(f30480,plain,
( hskp13
| ~ hskp21 ),
inference(resolution,[status(thm)],[f30479,f21282]) ).
fof(f30487,plain,
( ~ hskp21
| hskp1
| ~ c3_1(a1192) ),
inference(backward_subsumption_resolution,[status(thm)],[f3298,f30480]) ).
fof(f30489,plain,
( ~ hskp1
| hskp6
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f500,f30490]) ).
fof(f30490,plain,
( ~ hskp1
| hskp6
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f30164,f21277]) ).
fof(f30492,plain,
( ~ hskp21
| ~ hskp1
| hskp3 ),
inference(resolution,[status(thm)],[f30489,f29532]) ).
fof(f30493,plain,
( ~ hskp21
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f30492,f29619]) ).
fof(f30497,plain,
( ~ hskp21
| ~ c3_1(a1192) ),
inference(backward_subsumption_resolution,[status(thm)],[f30487,f30493]) ).
fof(f30823,plain,
( ~ hskp24
| ~ hskp16
| ~ c1_1(a1199) ),
inference(forward_subsumption_resolution,[status(thm)],[f16137,f257]) ).
fof(f30856,plain,
( ~ hskp16
| ~ hskp2
| c3_1(a1199)
| c0_1(a1199)
| c0_1(a1199)
| ~ hskp24
| ~ hskp16 ),
inference(resolution,[status(thm)],[f30823,f11333]) ).
fof(f30932,plain,
( ~ hskp2
| c3_1(a1199)
| c0_1(a1199)
| ~ hskp24
| ~ hskp16 ),
inference(duplicate_literals_removal,[status(thm)],[f30856]) ).
fof(f30933,plain,
( ~ hskp2
| c3_1(a1199)
| ~ hskp24
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f30932,f270]) ).
fof(f30950,plain,
( ~ hskp2
| ~ hskp24
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f30933,f271]) ).
fof(f30951,plain,
( hskp26
| ~ hskp2
| ~ hskp16 ),
inference(resolution,[status(thm)],[f30950,f21283]) ).
fof(f30952,plain,
! [X0] :
( ~ hskp22
| ~ hskp1
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f5973,f21287]) ).
fof(f30981,plain,
( ~ hskp22
| ~ hskp22
| ~ hskp1
| ~ c0_1(a1211)
| ~ c0_1(a1169) ),
inference(resolution,[status(thm)],[f30952,f227]) ).
fof(f31024,plain,
( ~ hskp22
| ~ hskp1
| ~ c0_1(a1211)
| ~ c0_1(a1169) ),
inference(duplicate_literals_removal,[status(thm)],[f30981]) ).
fof(f31025,plain,
( ~ hskp22
| ~ hskp1
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f31024,f226]) ).
fof(f31058,plain,
( ~ hskp1
| ~ c0_1(a1169) ),
inference(forward_subsumption_resolution,[status(thm)],[f31025,f21277]) ).
fof(f31096,plain,
( ~ hskp13
| ~ hskp22
| ~ c2_1(a1211) ),
inference(backward_subsumption_resolution,[status(thm)],[f19765,f31100]) ).
fof(f31097,plain,
( ~ hskp12
| ~ hskp22
| ~ c2_1(a1211) ),
inference(backward_subsumption_resolution,[status(thm)],[f19764,f31100]) ).
fof(f31100,plain,
( ~ hskp1
| ~ hskp22
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f18948,f31058]) ).
fof(f31181,plain,
( ~ hskp13
| ~ hskp22
| hskp7 ),
inference(backward_subsumption_resolution,[status(thm)],[f2706,f31096]) ).
fof(f31184,plain,
( ~ hskp22
| ~ hskp3
| ~ hskp13
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31096,f28509]) ).
fof(f31200,plain,
( ~ hskp3
| ~ hskp13
| ~ hskp22 ),
inference(duplicate_literals_removal,[status(thm)],[f31184]) ).
fof(f31201,plain,
( ~ hskp3
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f31200,f28574]) ).
fof(f31207,plain,
( ~ hskp3
| c2_1(a1174) ),
inference(backward_subsumption_resolution,[status(thm)],[f21279,f31201]) ).
fof(f31234,plain,
( ~ hskp21
| ~ hskp13
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31181,f29558]) ).
fof(f31239,plain,
( ~ hskp21
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f31234,f30480]) ).
fof(f31241,plain,
( ~ hskp22
| hskp12
| ~ c2_1(a1211) ),
inference(backward_subsumption_resolution,[status(thm)],[f699,f31239]) ).
fof(f31267,plain,
! [X0,X1] :
( ~ hskp3
| c1_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X1)
| ~ c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6315,f31207]) ).
fof(f31272,plain,
( ~ hskp2
| ~ hskp3
| ~ c1_1(a1172) ),
inference(backward_subsumption_resolution,[status(thm)],[f6348,f31207]) ).
fof(f31273,plain,
! [X0] :
( ~ hskp3
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6274,f31207]) ).
fof(f31277,plain,
! [X0] :
( ~ hskp3
| hskp0
| c2_1(X0)
| c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1111,f31207]) ).
fof(f31313,plain,
! [X0] :
( ~ hskp22
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f28545,f31319]) ).
fof(f31319,plain,
( ~ hskp22
| ~ c2_1(a1211) ),
inference(forward_subsumption_resolution,[status(thm)],[f31097,f31241]) ).
fof(f31356,plain,
! [X0] :
( ~ hskp2
| ~ hskp3
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(a1172) ),
inference(resolution,[status(thm)],[f31267,f296]) ).
fof(f31367,plain,
! [X0] :
( ~ hskp2
| ~ hskp3
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f31356,f253]) ).
fof(f31650,plain,
( ~ hskp26
| ~ hskp22
| ~ c3_1(a1190) ),
inference(resolution,[status(thm)],[f31313,f220]) ).
fof(f31742,plain,
( ~ hskp26
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f31650,f221]) ).
fof(f31790,plain,
( ~ hskp2
| ~ hskp16
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31742,f30951]) ).
fof(f31798,plain,
( ~ hskp6
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31742,f21268]) ).
fof(f31842,plain,
( ~ hskp23
| ~ hskp3
| hskp0
| c2_1(a1218) ),
inference(resolution,[status(thm)],[f31277,f260]) ).
fof(f31848,plain,
( ~ hskp23
| ~ hskp3
| hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f31842,f2293]) ).
fof(f31900,plain,
( ~ hskp1
| hskp3
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31798,f30489]) ).
fof(f31903,plain,
( ~ hskp7
| hskp3
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31798,f21522]) ).
fof(f31912,plain,
( hskp14
| hskp21
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31798,f211]) ).
fof(f31913,plain,
( ~ hskp1
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f31900,f31201]) ).
fof(f31914,plain,
( ~ hskp7
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f31903,f31201]) ).
fof(f31919,plain,
( hskp14
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f31912,f31239]) ).
fof(f31943,plain,
( ~ hskp13
| ~ hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f31181,f31914]) ).
fof(f31956,plain,
! [X0] :
( hskp14
| c3_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f716,f31919]) ).
fof(f32013,plain,
( hskp1
| ~ hskp2
| ~ hskp22 ),
inference(resolution,[status(thm)],[f31790,f21281]) ).
fof(f32014,plain,
( ~ hskp2
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f32013,f31913]) ).
fof(f32015,plain,
( hskp13
| ~ hskp22 ),
inference(resolution,[status(thm)],[f32014,f21282]) ).
fof(f32020,plain,
~ hskp22,
inference(forward_subsumption_resolution,[status(thm)],[f32015,f31943]) ).
fof(f32021,plain,
! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f21280,f32020]) ).
fof(f32022,plain,
! [X0] :
( hskp2
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f337,f32020]) ).
fof(f32067,plain,
! [X0] :
( hskp6
| hskp3
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f303,f32021]) ).
fof(f32092,plain,
( ~ hskp0
| ~ hskp19
| c2_1(a1168)
| ~ ndr1_0
| ~ c0_1(a1168) ),
inference(resolution,[status(thm)],[f32021,f30367]) ).
fof(f32108,plain,
( ~ hskp0
| ~ hskp19
| c2_1(a1168)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f32092,f255]) ).
fof(f32121,plain,
( ~ hskp23
| hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f31848,f499]) ).
fof(f32220,plain,
( ~ hskp21
| hskp6
| hskp3
| c2_1(a1192)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f32067,f30497]) ).
fof(f32244,plain,
( ~ hskp21
| hskp6
| hskp3
| c2_1(a1192) ),
inference(forward_subsumption_resolution,[status(thm)],[f32220,f185]) ).
fof(f32703,plain,
( ~ hskp0
| ~ hskp19
| c2_1(a1168) ),
inference(forward_subsumption_resolution,[status(thm)],[f32108,f206]) ).
fof(f32704,plain,
( ~ hskp0
| ~ hskp0
| ~ hskp19 ),
inference(resolution,[status(thm)],[f32703,f299]) ).
fof(f32705,plain,
( ~ hskp0
| ~ hskp19 ),
inference(duplicate_literals_removal,[status(thm)],[f32704]) ).
fof(f32706,plain,
~ hskp19,
inference(forward_subsumption_resolution,[status(thm)],[f32705,f885]) ).
fof(f32710,plain,
( ~ hskp1
| hskp23 ),
inference(backward_subsumption_resolution,[status(thm)],[f621,f32706]) ).
fof(f32712,plain,
( hskp21
| hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f212,f32706]) ).
fof(f32773,plain,
( ~ hskp21
| hskp6
| c2_1(a1192) ),
inference(forward_subsumption_resolution,[status(thm)],[f32244,f29619]) ).
fof(f32774,plain,
( ~ hskp13
| ~ hskp21
| hskp6 ),
inference(resolution,[status(thm)],[f32773,f277]) ).
fof(f32775,plain,
( ~ hskp13
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f32774,f29532]) ).
fof(f32777,plain,
( ~ hskp14
| hskp12
| ~ c3_1(a1194) ),
inference(backward_subsumption_resolution,[status(thm)],[f698,f32781]) ).
fof(f32780,plain,
hskp8,
inference(backward_subsumption_resolution,[status(thm)],[f32712,f32781]) ).
fof(f32781,plain,
~ hskp21,
inference(forward_subsumption_resolution,[status(thm)],[f32775,f30480]) ).
fof(f32788,plain,
hskp26,
inference(backward_subsumption_resolution,[status(thm)],[f28576,f32780]) ).
fof(f32809,plain,
( ~ hskp0
| hskp3
| ~ c3_1(a1168) ),
inference(backward_subsumption_resolution,[status(thm)],[f3476,f32780]) ).
fof(f32815,plain,
ndr1_0,
inference(backward_subsumption_resolution,[status(thm)],[f198,f32780]) ).
fof(f32858,plain,
c3_1(a1190),
inference(backward_subsumption_resolution,[status(thm)],[f221,f32788]) ).
fof(f32859,plain,
c1_1(a1190),
inference(backward_subsumption_resolution,[status(thm)],[f220,f32788]) ).
fof(f32860,plain,
c0_1(a1190),
inference(backward_subsumption_resolution,[status(thm)],[f219,f32788]) ).
fof(f32872,plain,
! [X0] :
( hskp2
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f32022,f32815]) ).
fof(f32873,plain,
! [X0] :
( c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f32021,f32815]) ).
fof(f32874,plain,
! [X0] :
( hskp14
| c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f31956,f32815]) ).
fof(f32883,plain,
! [X0] :
( ~ hskp3
| hskp25
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f4139,f32815]) ).
fof(f34078,plain,
( ~ hskp2
| ~ hskp3
| ~ hskp2
| ~ hskp3
| c0_1(a1172)
| ~ c2_1(a1172) ),
inference(resolution,[status(thm)],[f31367,f31272]) ).
fof(f34085,plain,
( ~ hskp2
| ~ hskp3
| c0_1(a1172)
| ~ c2_1(a1172) ),
inference(duplicate_literals_removal,[status(thm)],[f34078]) ).
fof(f34086,plain,
( ~ hskp2
| ~ hskp3
| c0_1(a1172) ),
inference(forward_subsumption_resolution,[status(thm)],[f34085,f252]) ).
fof(f34089,plain,
( ~ hskp2
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f34086,f296]) ).
fof(f34093,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f34089,f32872]) ).
fof(f34355,plain,
( ~ c2_1(a1190)
| ~ c0_1(a1190)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f34093,f32858]) ).
fof(f34369,plain,
( ~ hskp25
| ~ c2_1(a1182)
| ~ c0_1(a1182)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f34093,f224]) ).
fof(f34393,plain,
( ~ c2_1(a1190)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f34355,f32860]) ).
fof(f34395,plain,
( ~ hskp25
| ~ c0_1(a1182)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f34369,f223]) ).
fof(f34438,plain,
( ~ hskp3
| hskp25
| ~ c1_1(a1190)
| ~ c0_1(a1190)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f34393,f32883]) ).
fof(f34445,plain,
( hskp25
| ~ c1_1(a1190)
| ~ c0_1(a1190)
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f34438]) ).
fof(f34446,plain,
( hskp25
| ~ c1_1(a1190)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f34445,f32860]) ).
fof(f34457,plain,
( ~ hskp3
| ~ c3_1(a1182)
| ~ c1_1(a1182)
| ~ hskp25
| ~ hskp3 ),
inference(resolution,[status(thm)],[f34395,f31273]) ).
fof(f34473,plain,
( ~ c3_1(a1182)
| ~ c1_1(a1182)
| ~ hskp25
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f34457]) ).
fof(f34474,plain,
( ~ c3_1(a1182)
| ~ hskp25
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f34473,f222]) ).
fof(f34481,plain,
( hskp25
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f34446,f32859]) ).
fof(f34507,plain,
( ~ c3_1(a1182)
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f34474,f34481]) ).
fof(f34508,plain,
( ~ hskp25
| ~ hskp3 ),
inference(resolution,[status(thm)],[f34507,f224]) ).
fof(f34531,plain,
~ hskp3,
inference(forward_subsumption_resolution,[status(thm)],[f34508,f34481]) ).
fof(f34539,plain,
( ~ hskp12
| hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f541,f34531]) ).
fof(f34540,plain,
( ~ hskp0
| ~ c3_1(a1168) ),
inference(backward_subsumption_resolution,[status(thm)],[f32809,f34531]) ).
fof(f34564,plain,
( c2_1(a1168)
| ~ c0_1(a1168)
| ~ hskp0 ),
inference(resolution,[status(thm)],[f34540,f32873]) ).
fof(f34567,plain,
( hskp14
| ~ c0_1(a1168)
| ~ hskp0 ),
inference(resolution,[status(thm)],[f34540,f32874]) ).
fof(f34582,plain,
( c2_1(a1168)
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f34564,f255]) ).
fof(f34583,plain,
( hskp14
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f34567,f255]) ).
fof(f34588,plain,
( hskp14
| hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f208,f34583]) ).
fof(f34719,plain,
( ~ hskp14
| c3_1(a1194) ),
inference(backward_subsumption_resolution,[status(thm)],[f1408,f34725]) ).
fof(f34721,plain,
~ hskp23,
inference(backward_subsumption_resolution,[status(thm)],[f32121,f34725]) ).
fof(f34724,plain,
( ~ hskp14
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f20778,f34725]) ).
fof(f34725,plain,
~ hskp0,
inference(forward_subsumption_resolution,[status(thm)],[f34582,f299]) ).
fof(f34734,plain,
~ hskp1,
inference(backward_subsumption_resolution,[status(thm)],[f32710,f34721]) ).
fof(f34747,plain,
hskp14,
inference(backward_subsumption_resolution,[status(thm)],[f34588,f34734]) ).
fof(f34773,plain,
( hskp12
| ~ c3_1(a1194) ),
inference(backward_subsumption_resolution,[status(thm)],[f32777,f34747]) ).
fof(f34783,plain,
~ hskp12,
inference(backward_subsumption_resolution,[status(thm)],[f34539,f34784]) ).
fof(f34784,plain,
~ hskp6,
inference(forward_subsumption_resolution,[status(thm)],[f34724,f34747]) ).
fof(f34845,plain,
c3_1(a1194),
inference(forward_subsumption_resolution,[status(thm)],[f34719,f34747]) ).
fof(f34847,plain,
hskp12,
inference(forward_subsumption_resolution,[status(thm)],[f34773,f34845]) ).
fof(f34848,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f34783,f34847]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN461-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 10:57:05 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 120.33/16.16 % Refutation found
% 120.33/16.16 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 120.33/16.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 120.33/16.21 % Elapsed time: 15.826724 seconds
% 120.33/16.21 % CPU time: 124.600285 seconds
% 120.33/16.21 % Total memory used: 98.821 MB
% 120.33/16.21 % Net memory used: 92.400 MB
%------------------------------------------------------------------------------