%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN505-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:39 PM UTC 2026
% Result : Unsatisfiable 195.85s 25.25s
% Output : CNFRefutation 195.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 124
% Number of leaves : 138
% Syntax : Number of formulae : 1037 ( 18 unt; 0 def)
% Number of atoms : 4662 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 6481 (2856 ~;3625 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 28 prp; 0-1 aty)
% Number of functors : 26 ( 26 usr; 26 con; 0-0 aty)
% Number of variables : 475 ( 475 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,negated_conjecture,
( ndr1_0
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
( ndr1_0
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
( ndr1_0
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
( ndr1_0
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,negated_conjecture,
( ndr1_0
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
( ndr1_0
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
( ndr1_0
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
( ndr1_0
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
( ndr1_0
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
( ndr1_0
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
( ndr1_0
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
( ndr1_0
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
( ndr1_0
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
( ndr1_0
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
( ndr1_0
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
( ndr1_0
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
( ndr1_0
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
( ndr1_0
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
( ndr1_0
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
( hskp3
| hskp12
| hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
( hskp13
| hskp16
| hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
( hskp10
| hskp30
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
( hskp25
| hskp14
| hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
( hskp27
| hskp8
| hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
( hskp13
| hskp1
| hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
( c1_1(a488)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,negated_conjecture,
( c2_1(a488)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,negated_conjecture,
( c3_1(a488)
| ~ hskp30 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
( c0_1(a474)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,negated_conjecture,
( c1_1(a474)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
( c2_1(a474)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
( c0_1(a469)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
( c2_1(a469)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,negated_conjecture,
( c3_1(a469)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
( c0_1(a559)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
( c1_1(a559)
| ~ hskp26 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
( c1_1(a545)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,negated_conjecture,
( c3_1(a545)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,negated_conjecture,
( c1_1(a519)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,negated_conjecture,
( c1_1(a506)
| ~ hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,negated_conjecture,
( c2_1(a506)
| ~ hskp20 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,negated_conjecture,
( c1_1(a500)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,negated_conjecture,
( c0_1(a494)
| ~ hskp18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,negated_conjecture,
( c2_1(a493)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,negated_conjecture,
( c3_1(a493)
| ~ hskp17 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,negated_conjecture,
( c0_1(a487)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,negated_conjecture,
( c0_1(a484)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,negated_conjecture,
( c2_1(a484)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,negated_conjecture,
( c1_1(a483)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,negated_conjecture,
( c2_1(a483)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,negated_conjecture,
( c3_1(a482)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,negated_conjecture,
( c1_1(a481)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,negated_conjecture,
( c0_1(a479)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,negated_conjecture,
( c3_1(a479)
| ~ hskp11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,negated_conjecture,
( c2_1(a478)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,negated_conjecture,
( c1_1(a472)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,negated_conjecture,
( c3_1(a472)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,negated_conjecture,
( c0_1(a471)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,negated_conjecture,
( c3_1(a471)
| ~ hskp7 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,negated_conjecture,
( c0_1(a467)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,negated_conjecture,
( c3_1(a465)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,negated_conjecture,
( c3_1(a464)
| ~ hskp2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
( c2_1(a463)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
( c0_1(a462)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,negated_conjecture,
( c2_1(a462)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,negated_conjecture,
( ~ hskp27
| ~ c1_1(a576) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,negated_conjecture,
( ~ hskp27
| ~ c2_1(a576) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,negated_conjecture,
( ~ hskp27
| ~ c3_1(a576) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,negated_conjecture,
( ~ hskp26
| ~ c3_1(a559) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
( ~ hskp25
| ~ c0_1(a545) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,negated_conjecture,
( ~ hskp22
| ~ c0_1(a519) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,negated_conjecture,
( ~ hskp22
| ~ c2_1(a519) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,negated_conjecture,
( ~ hskp20
| ~ c3_1(a506) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,negated_conjecture,
( ~ hskp19
| ~ c2_1(a500) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,negated_conjecture,
( ~ hskp19
| ~ c3_1(a500) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,negated_conjecture,
( ~ hskp18
| ~ c2_1(a494) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f109,negated_conjecture,
( ~ hskp18
| ~ c3_1(a494) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,negated_conjecture,
( ~ hskp17
| ~ c0_1(a493) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,negated_conjecture,
( ~ hskp16
| ~ c1_1(a487) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,negated_conjecture,
( ~ hskp16
| ~ c2_1(a487) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,negated_conjecture,
( ~ hskp15
| ~ c3_1(a484) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,negated_conjecture,
( ~ hskp14
| ~ c0_1(a483) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f115,negated_conjecture,
( ~ hskp13
| ~ c1_1(a482) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f116,negated_conjecture,
( ~ hskp13
| ~ c2_1(a482) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,negated_conjecture,
( ~ hskp12
| ~ c0_1(a481) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,negated_conjecture,
( ~ hskp12
| ~ c3_1(a481) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,negated_conjecture,
( ~ hskp11
| ~ c1_1(a479) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,negated_conjecture,
( ~ hskp10
| ~ c0_1(a478) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,negated_conjecture,
( ~ hskp10
| ~ c3_1(a478) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f123,negated_conjecture,
( ~ hskp8
| ~ c2_1(a472) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,negated_conjecture,
( ~ hskp7
| ~ c2_1(a471) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,negated_conjecture,
( ~ hskp6
| ~ c0_1(a470) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,negated_conjecture,
( ~ hskp6
| ~ c1_1(a470) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,negated_conjecture,
( ~ hskp6
| ~ c2_1(a470) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,negated_conjecture,
( ~ hskp5
| ~ c1_1(a467) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f129,negated_conjecture,
( ~ hskp5
| ~ c3_1(a467) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,negated_conjecture,
( ~ hskp3
| ~ c0_1(a465) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,negated_conjecture,
( ~ hskp3
| ~ c1_1(a465) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,negated_conjecture,
( ~ hskp2
| ~ c0_1(a464) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f136,negated_conjecture,
( ~ hskp2
| ~ c2_1(a464) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,negated_conjecture,
( ~ hskp1
| ~ c1_1(a463) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,negated_conjecture,
( ~ hskp1
| ~ c3_1(a463) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,negated_conjecture,
( ~ hskp0
| ~ c1_1(a462) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,negated_conjecture,
! [U] :
( hskp8
| hskp7
| c3_1(U)
| c2_1(U)
| c0_1(U)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f144,negated_conjecture,
! [U] :
( hskp12
| hskp5
| c2_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f145,negated_conjecture,
! [U] :
( hskp1
| hskp15
| c3_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f146,negated_conjecture,
! [U] :
( hskp16
| hskp7
| c3_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,negated_conjecture,
! [U] :
( hskp19
| hskp18
| c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,negated_conjecture,
! [U] :
( hskp1
| hskp18
| c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f153,negated_conjecture,
! [U] :
( hskp22
| hskp20
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,negated_conjecture,
! [U] :
( hskp1
| hskp30
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,negated_conjecture,
! [U] :
( hskp17
| hskp7
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,negated_conjecture,
! [U] :
( hskp17
| hskp5
| c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f161,negated_conjecture,
! [U] :
( hskp12
| hskp30
| c3_1(U)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,negated_conjecture,
! [U] :
( hskp25
| hskp14
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f172,negated_conjecture,
! [U,V] :
( hskp16
| c3_1(V)
| c2_1(V)
| c1_1(V)
| c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,negated_conjecture,
! [U,V] :
( hskp14
| c3_1(V)
| c2_1(V)
| c1_1(V)
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,negated_conjecture,
! [U,V] :
( hskp5
| c1_1(V)
| c0_1(V)
| c3_1(U)
| c2_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,negated_conjecture,
! [U,V] :
( hskp6
| c2_1(V)
| c0_1(V)
| c3_1(U)
| c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f177,negated_conjecture,
! [U,V] :
( hskp29
| c2_1(V)
| c0_1(V)
| c2_1(U)
| c1_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,negated_conjecture,
! [U,V] :
( c0_1(V)
| c2_1(U)
| c1_1(U)
| ~ c2_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f180,negated_conjecture,
! [U,V] :
( hskp2
| c3_1(V)
| c2_1(V)
| c1_1(V)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,negated_conjecture,
! [U,V] :
( hskp10
| c2_1(V)
| c0_1(V)
| c2_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f184,negated_conjecture,
! [U,V] :
( hskp13
| c3_1(V)
| c0_1(V)
| c1_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f185,negated_conjecture,
! [U,V] :
( hskp14
| c3_1(V)
| c0_1(V)
| c0_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f187,negated_conjecture,
! [U,V] :
( c3_1(V)
| c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f188,negated_conjecture,
! [U,V] :
( hskp28
| c1_1(V)
| c0_1(V)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
! [U,V] :
( hskp11
| c2_1(V)
| c0_1(V)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
! [U,V] :
( hskp2
| c3_1(V)
| c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f191,negated_conjecture,
! [U,V] :
( hskp12
| c1_1(V)
| c2_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
! [U,V] :
( hskp29
| c2_1(V)
| c3_1(U)
| ~ c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f194,negated_conjecture,
! [U,V] :
( hskp16
| c0_1(V)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,negated_conjecture,
! [U,V] :
( hskp18
| c1_1(V)
| ~ c3_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f198,negated_conjecture,
! [U,V,W] :
( c3_1(W)
| c1_1(W)
| c0_1(W)
| c2_1(V)
| c0_1(V)
| c3_1(U)
| c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
! [U,V,W] :
( c3_1(W)
| c2_1(W)
| c0_1(W)
| c2_1(V)
| c0_1(V)
| c3_1(U)
| c0_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f201,negated_conjecture,
! [U,V,W] :
( c1_1(W)
| c0_1(W)
| c2_1(V)
| c0_1(V)
| c3_1(U)
| c2_1(U)
| ~ c3_1(W)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f204,negated_conjecture,
! [U,V,W] :
( c3_1(W)
| c0_1(W)
| c3_1(V)
| c1_1(V)
| c2_1(U)
| ~ c1_1(W)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f210,plain,
( ndr1_0
| ~ hskp30 ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f213,plain,
( ndr1_0
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f215,plain,
( ndr1_0
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f218,plain,
( ndr1_0
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f221,plain,
( ndr1_0
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f222,plain,
( ndr1_0
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f223,plain,
( ndr1_0
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f224,plain,
( ndr1_0
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f225,plain,
( ndr1_0
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f226,plain,
( ndr1_0
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f227,plain,
( ndr1_0
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f228,plain,
( ndr1_0
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f229,plain,
( ndr1_0
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f230,plain,
( ndr1_0
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f232,plain,
( ndr1_0
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f233,plain,
( ndr1_0
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f235,plain,
( ndr1_0
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f237,plain,
( ndr1_0
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f238,plain,
( ndr1_0
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f240,plain,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f242,plain,
( hskp3
| hskp12
| hskp29 ),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f244,plain,
( hskp13
| hskp16
| hskp26 ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f246,plain,
( hskp10
| hskp30
| hskp0 ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f247,plain,
( hskp25
| hskp14
| hskp0 ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f249,plain,
( hskp27
| hskp8
| hskp7 ),
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f251,plain,
( hskp13
| hskp1
| hskp22 ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f255,plain,
( c1_1(a488)
| ~ hskp30 ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f256,plain,
( c2_1(a488)
| ~ hskp30 ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f257,plain,
( c3_1(a488)
| ~ hskp30 ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f258,plain,
( c0_1(a474)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f259,plain,
( c1_1(a474)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f260,plain,
( c2_1(a474)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f261,plain,
( c0_1(a469)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f262,plain,
( c2_1(a469)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f263,plain,
( c3_1(a469)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f264,plain,
( c0_1(a559)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f265,plain,
( c1_1(a559)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f266,plain,
( c1_1(a545)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f267,plain,
( c3_1(a545)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f270,plain,
( c1_1(a519)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f272,plain,
( c1_1(a506)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f273,plain,
( c2_1(a506)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f274,plain,
( c1_1(a500)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f275,plain,
( c0_1(a494)
| ~ hskp18 ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f276,plain,
( c2_1(a493)
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f277,plain,
( c3_1(a493)
| ~ hskp17 ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f278,plain,
( c0_1(a487)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f279,plain,
( c0_1(a484)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f280,plain,
( c2_1(a484)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f281,plain,
( c1_1(a483)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f282,plain,
( c2_1(a483)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f283,plain,
( c3_1(a482)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f284,plain,
( c1_1(a481)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f285,plain,
( c0_1(a479)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f286,plain,
( c3_1(a479)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f287,plain,
( c2_1(a478)
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f290,plain,
( c1_1(a472)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f291,plain,
( c3_1(a472)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f292,plain,
( c0_1(a471)
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f293,plain,
( c3_1(a471)
| ~ hskp7 ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f294,plain,
( c0_1(a467)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f295,plain,
( c3_1(a465)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f296,plain,
( c3_1(a464)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f297,plain,
( c2_1(a463)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f298,plain,
( c0_1(a462)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f299,plain,
( c2_1(a462)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f300,plain,
( ~ hskp27
| ~ c1_1(a576) ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f301,plain,
( ~ hskp27
| ~ c2_1(a576) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f302,plain,
( ~ hskp27
| ~ c3_1(a576) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f303,plain,
( ~ hskp26
| ~ c3_1(a559) ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f304,plain,
( ~ hskp25
| ~ c0_1(a545) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f309,plain,
( ~ hskp22
| ~ c0_1(a519) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f310,plain,
( ~ hskp22
| ~ c2_1(a519) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f313,plain,
( ~ hskp20
| ~ c3_1(a506) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f314,plain,
( ~ hskp19
| ~ c2_1(a500) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f315,plain,
( ~ hskp19
| ~ c3_1(a500) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f316,plain,
( ~ hskp18
| ~ c2_1(a494) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f317,plain,
( ~ hskp18
| ~ c3_1(a494) ),
inference(cnf_transformation,[status(thm)],[f109]) ).
fof(f318,plain,
( ~ hskp17
| ~ c0_1(a493) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f319,plain,
( ~ hskp16
| ~ c1_1(a487) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f320,plain,
( ~ hskp16
| ~ c2_1(a487) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f321,plain,
( ~ hskp15
| ~ c3_1(a484) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f322,plain,
( ~ hskp14
| ~ c0_1(a483) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f323,plain,
( ~ hskp13
| ~ c1_1(a482) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f324,plain,
( ~ hskp13
| ~ c2_1(a482) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f325,plain,
( ~ hskp12
| ~ c0_1(a481) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f326,plain,
( ~ hskp12
| ~ c3_1(a481) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f327,plain,
( ~ hskp11
| ~ c1_1(a479) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f328,plain,
( ~ hskp10
| ~ c0_1(a478) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f329,plain,
( ~ hskp10
| ~ c3_1(a478) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f331,plain,
( ~ hskp8
| ~ c2_1(a472) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f332,plain,
( ~ hskp7
| ~ c2_1(a471) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f333,plain,
( ~ hskp6
| ~ c0_1(a470) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f334,plain,
( ~ hskp6
| ~ c1_1(a470) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f335,plain,
( ~ hskp6
| ~ c2_1(a470) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f336,plain,
( ~ hskp5
| ~ c1_1(a467) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f337,plain,
( ~ hskp5
| ~ c3_1(a467) ),
inference(cnf_transformation,[status(thm)],[f129]) ).
fof(f341,plain,
( ~ hskp3
| ~ c0_1(a465) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f342,plain,
( ~ hskp3
| ~ c1_1(a465) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f343,plain,
( ~ hskp2
| ~ c0_1(a464) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f344,plain,
( ~ hskp2
| ~ c2_1(a464) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f345,plain,
( ~ hskp1
| ~ c1_1(a463) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f346,plain,
( ~ hskp1
| ~ c3_1(a463) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f347,plain,
( ~ hskp0
| ~ c1_1(a462) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f352,plain,
( hskp8
| hskp7
| ! [U] :
( c3_1(U)
| c2_1(U)
| c0_1(U)
| ~ ndr1_0 ) ),
inference(miniscoping,[status(thm)],[f142]) ).
fof(f353,plain,
! [X0] :
( hskp8
| hskp7
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f352]) ).
fof(f356,plain,
( hskp12
| hskp5
| ! [U] :
( c2_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f357,plain,
! [X0] :
( hskp12
| hskp5
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f356]) ).
fof(f358,plain,
( hskp1
| hskp15
| ! [U] :
( c3_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U) ) ),
inference(miniscoping,[status(thm)],[f145]) ).
fof(f359,plain,
! [X0] :
( hskp1
| hskp15
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f360,plain,
( hskp16
| hskp7
| ! [U] :
( c3_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U) ) ),
inference(miniscoping,[status(thm)],[f146]) ).
fof(f361,plain,
! [X0] :
( hskp16
| hskp7
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f362,plain,
( hskp19
| hskp18
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f147]) ).
fof(f363,plain,
! [X0] :
( hskp19
| hskp18
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f366,plain,
( hskp1
| hskp18
| ! [U] :
( c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f367,plain,
! [X0] :
( hskp1
| hskp18
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f366]) ).
fof(f374,plain,
( hskp22
| hskp20
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f153]) ).
fof(f375,plain,
! [X0] :
( hskp22
| hskp20
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f378,plain,
( hskp1
| hskp30
| ! [U] :
( c0_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f155]) ).
fof(f379,plain,
! [X0] :
( hskp1
| hskp30
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f380,plain,
( hskp17
| hskp7
| ! [U] :
( c0_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f381,plain,
! [X0] :
( hskp17
| hskp7
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f386,plain,
( hskp17
| hskp5
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f159]) ).
fof(f387,plain,
! [X0] :
( hskp17
| hskp5
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f386]) ).
fof(f390,plain,
( hskp12
| hskp30
| ! [U] :
( c3_1(U)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f391,plain,
! [X0] :
( hskp12
| hskp30
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f404,plain,
( hskp25
| hskp14
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f168]) ).
fof(f405,plain,
! [X0] :
( hskp25
| hskp14
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f412,plain,
( hskp16
| ! [V] :
( c3_1(V)
| c2_1(V)
| c1_1(V)
| ! [U] :
( c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f172]) ).
fof(f413,plain,
! [X0,X1] :
( hskp16
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f412]) ).
fof(f414,plain,
( hskp14
| ! [V] :
( c3_1(V)
| c2_1(V)
| c1_1(V)
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f415,plain,
! [X0,X1] :
( hskp14
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f418,plain,
( hskp5
| ! [V] :
( c1_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f175]) ).
fof(f419,plain,
! [X0,X1] :
( hskp5
| c1_1(X1)
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f420,plain,
( hskp6
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f421,plain,
! [X0,X1] :
( hskp6
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f422,plain,
( hskp29
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f423,plain,
! [X0,X1] :
( hskp29
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f426,plain,
! [V] :
( c0_1(V)
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ c2_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f427,plain,
! [X0,X1] :
( c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f426]) ).
fof(f428,plain,
( hskp2
| ! [V] :
( c3_1(V)
| c2_1(V)
| c1_1(V)
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f180]) ).
fof(f429,plain,
! [X0,X1] :
( hskp2
| c3_1(X1)
| c2_1(X1)
| c1_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f428]) ).
fof(f434,plain,
( hskp10
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f183]) ).
fof(f435,plain,
! [X0,X1] :
( hskp10
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f434]) ).
fof(f436,plain,
( hskp13
| ! [V] :
( c3_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f437,plain,
! [X0,X1] :
( hskp13
| c3_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f438,plain,
( hskp14
| ! [V] :
( c3_1(V)
| c0_1(V)
| ! [U] :
( c0_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f185]) ).
fof(f439,plain,
! [X0,X1] :
( hskp14
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f438]) ).
fof(f442,plain,
! [V] :
( c3_1(V)
| c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c2_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f187]) ).
fof(f443,plain,
! [X0,X1] :
( c3_1(X1)
| c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f444,plain,
( hskp28
| ! [V] :
( c1_1(V)
| c0_1(V)
| ~ c3_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f188]) ).
fof(f445,plain,
! [X0,X1] :
( hskp28
| c1_1(X1)
| c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f444]) ).
fof(f446,plain,
( hskp11
| ! [V] :
( c2_1(V)
| c0_1(V)
| ~ c3_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f189]) ).
fof(f447,plain,
! [X0,X1] :
( hskp11
| c2_1(X1)
| c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f446]) ).
fof(f448,plain,
( hskp2
| ! [V] :
( c3_1(V)
| c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f190]) ).
fof(f449,plain,
! [X0,X1] :
( hskp2
| c3_1(X1)
| c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f448]) ).
fof(f450,plain,
( hskp12
| ! [V] :
( c1_1(V)
| ! [U] :
( c2_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f191]) ).
fof(f451,plain,
! [X0,X1] :
( hskp12
| c1_1(X1)
| c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f454,plain,
( hskp29
| ! [V] :
( c2_1(V)
| ! [U] :
( c3_1(U)
| ~ c1_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f193]) ).
fof(f455,plain,
! [X0,X1] :
( hskp29
| c2_1(X1)
| c3_1(X0)
| ~ c1_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f454]) ).
fof(f456,plain,
( hskp16
| ! [V] :
( c0_1(V)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f194]) ).
fof(f457,plain,
! [X0,X1] :
( hskp16
| c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f456]) ).
fof(f458,plain,
( hskp18
| ! [V] :
( c1_1(V)
| ~ c3_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c2_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f195]) ).
fof(f459,plain,
! [X0,X1] :
( hskp18
| c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f458]) ).
fof(f464,plain,
! [W] :
( c3_1(W)
| c1_1(W)
| c0_1(W)
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f198]) ).
fof(f465,plain,
! [X0,X1,X2] :
( c3_1(X2)
| c1_1(X2)
| c0_1(X2)
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f464]) ).
fof(f466,plain,
! [W] :
( c3_1(W)
| c2_1(W)
| c0_1(W)
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| c0_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f467,plain,
! [X0,X1,X2] :
( c3_1(X2)
| c2_1(X2)
| c0_1(X2)
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f466]) ).
fof(f470,plain,
! [W] :
( c1_1(W)
| c0_1(W)
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ c3_1(W)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f201]) ).
fof(f471,plain,
! [X0,X1,X2] :
( c1_1(X2)
| c0_1(X2)
| c2_1(X1)
| c0_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c3_1(X2)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f470]) ).
fof(f476,plain,
! [W] :
( c3_1(W)
| c0_1(W)
| ! [V] :
( c3_1(V)
| c1_1(V)
| ! [U] :
( c2_1(U)
| ~ c1_1(W)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f204]) ).
fof(f477,plain,
! [X0,X1,X2] :
( c3_1(X2)
| c0_1(X2)
| c3_1(X1)
| c1_1(X1)
| c2_1(X0)
| ~ c1_1(X2)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f476]) ).
fof(f536,plain,
( ~ hskp27
| hskp8
| hskp7
| c3_1(a576)
| c0_1(a576)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f353,f301]) ).
fof(f541,plain,
( ~ hskp27
| hskp8
| hskp7
| c3_1(a576)
| c0_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f536,f213]) ).
fof(f555,plain,
( ~ hskp27
| hskp8
| hskp7
| c0_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f541,f302]) ).
fof(f587,plain,
( ~ hskp22
| hskp12
| hskp5
| c0_1(a519)
| ~ ndr1_0
| ~ c3_1(a519) ),
inference(resolution,[status(thm)],[f357,f310]) ).
fof(f595,plain,
( ~ hskp22
| hskp12
| hskp5
| c0_1(a519)
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f587,f218]) ).
fof(f615,plain,
( ~ hskp10
| hskp16
| hskp7
| c0_1(a478)
| ~ ndr1_0
| ~ c2_1(a478) ),
inference(resolution,[status(thm)],[f361,f329]) ).
fof(f616,plain,
( ~ hskp12
| hskp16
| hskp7
| c0_1(a481)
| ~ ndr1_0
| ~ c2_1(a481) ),
inference(resolution,[status(thm)],[f361,f326]) ).
fof(f626,plain,
( ~ hskp10
| hskp16
| hskp7
| c0_1(a478)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f615,f287]) ).
fof(f627,plain,
( ~ hskp12
| hskp16
| hskp7
| c0_1(a481)
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f616,f228]) ).
fof(f639,plain,
( ~ hskp7
| hskp19
| hskp18
| c1_1(a471)
| ~ ndr1_0
| ~ c0_1(a471) ),
inference(resolution,[status(thm)],[f363,f332]) ).
fof(f641,plain,
( ~ hskp13
| hskp19
| hskp18
| c1_1(a482)
| ~ ndr1_0
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f363,f324]) ).
fof(f642,plain,
( ~ hskp16
| hskp19
| hskp18
| c1_1(a487)
| ~ ndr1_0
| ~ c0_1(a487) ),
inference(resolution,[status(thm)],[f363,f320]) ).
fof(f649,plain,
( ~ hskp7
| hskp19
| hskp18
| c1_1(a471)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f639,f292]) ).
fof(f650,plain,
( ~ hskp13
| hskp19
| hskp18
| c1_1(a482)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f641,f227]) ).
fof(f651,plain,
( ~ hskp16
| hskp19
| hskp18
| c1_1(a487)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f642,f278]) ).
fof(f655,plain,
( ~ hskp10
| hskp16
| hskp7
| c0_1(a478) ),
inference(forward_subsumption_resolution,[status(thm)],[f626,f230]) ).
fof(f656,plain,
( ~ hskp10
| ~ hskp10
| hskp16
| hskp7 ),
inference(resolution,[status(thm)],[f655,f328]) ).
fof(f657,plain,
( ~ hskp10
| hskp16
| hskp7 ),
inference(duplicate_literals_removal,[status(thm)],[f656]) ).
fof(f659,plain,
( ~ hskp7
| hskp19
| hskp18
| c1_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f649,f233]) ).
fof(f660,plain,
( ~ hskp16
| hskp19
| hskp18
| c1_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f651,f224]) ).
fof(f661,plain,
( ~ hskp16
| ~ hskp16
| hskp19
| hskp18 ),
inference(resolution,[status(thm)],[f660,f319]) ).
fof(f662,plain,
( ~ hskp16
| hskp19
| hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f661]) ).
fof(f665,plain,
( ~ hskp22
| hskp12
| hskp5
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f595,f309]) ).
fof(f686,plain,
( ~ hskp5
| hskp1
| hskp18
| c1_1(a467)
| ~ ndr1_0
| ~ c0_1(a467) ),
inference(resolution,[status(thm)],[f367,f337]) ).
fof(f689,plain,
( ~ hskp15
| hskp1
| hskp18
| c1_1(a484)
| ~ ndr1_0
| ~ c0_1(a484) ),
inference(resolution,[status(thm)],[f367,f321]) ).
fof(f696,plain,
( ~ hskp5
| hskp1
| hskp18
| c1_1(a467)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f686,f294]) ).
fof(f697,plain,
( ~ hskp15
| hskp1
| hskp18
| c1_1(a484)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f689,f279]) ).
fof(f704,plain,
( ~ hskp5
| hskp1
| hskp18
| c1_1(a467) ),
inference(forward_subsumption_resolution,[status(thm)],[f696,f235]) ).
fof(f705,plain,
( ~ hskp5
| ~ hskp5
| hskp1
| hskp18 ),
inference(resolution,[status(thm)],[f704,f336]) ).
fof(f706,plain,
( ~ hskp5
| hskp1
| hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f705]) ).
fof(f707,plain,
( ~ hskp15
| hskp1
| hskp18
| c1_1(a484) ),
inference(forward_subsumption_resolution,[status(thm)],[f697,f225]) ).
fof(f710,plain,
( ~ hskp12
| hskp16
| hskp7
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f627,f325]) ).
fof(f711,plain,
( ~ hskp13
| hskp19
| hskp18
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f323]) ).
fof(f776,plain,
( ~ hskp18
| hskp22
| hskp20
| c3_1(a494)
| ~ ndr1_0
| ~ c1_1(a494) ),
inference(resolution,[status(thm)],[f375,f316]) ).
fof(f777,plain,
( ~ hskp19
| hskp22
| hskp20
| c3_1(a500)
| ~ ndr1_0
| ~ c1_1(a500) ),
inference(resolution,[status(thm)],[f375,f314]) ).
fof(f782,plain,
( ~ hskp18
| hskp22
| hskp20
| c3_1(a494)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f776,f222]) ).
fof(f783,plain,
( ~ hskp19
| hskp22
| hskp20
| c3_1(a500)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f274]) ).
fof(f814,plain,
( ~ hskp19
| hskp22
| hskp20
| c3_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f783,f221]) ).
fof(f815,plain,
( ~ hskp19
| ~ hskp19
| hskp22
| hskp20 ),
inference(resolution,[status(thm)],[f814,f315]) ).
fof(f816,plain,
( ~ hskp19
| hskp22
| hskp20 ),
inference(duplicate_literals_removal,[status(thm)],[f815]) ).
fof(f830,plain,
( ~ hskp14
| hskp1
| hskp30
| ~ ndr1_0
| ~ c2_1(a483)
| ~ c1_1(a483) ),
inference(resolution,[status(thm)],[f379,f322]) ).
fof(f838,plain,
( ~ hskp14
| hskp1
| hskp30
| ~ ndr1_0
| ~ c2_1(a483) ),
inference(forward_subsumption_resolution,[status(thm)],[f830,f281]) ).
fof(f859,plain,
( ~ hskp14
| hskp1
| hskp30
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f838,f282]) ).
fof(f871,plain,
( ~ hskp18
| hskp22
| hskp20
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f782,f317]) ).
fof(f912,plain,
( ~ hskp13
| hskp17
| hskp5
| ~ ndr1_0
| ~ c3_1(a482)
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f387,f324]) ).
fof(f922,plain,
( ~ hskp13
| hskp17
| hskp5
| ~ ndr1_0
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f912,f283]) ).
fof(f958,plain,
( ~ hskp26
| hskp12
| hskp30
| ~ ndr1_0
| ~ c1_1(a559)
| ~ c0_1(a559) ),
inference(resolution,[status(thm)],[f391,f303]) ).
fof(f964,plain,
( ~ hskp26
| hskp12
| hskp30
| ~ ndr1_0
| ~ c1_1(a559) ),
inference(forward_subsumption_resolution,[status(thm)],[f958,f264]) ).
fof(f971,plain,
( ~ hskp13
| hskp17
| hskp5
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f922,f227]) ).
fof(f1000,plain,
( ~ hskp26
| hskp12
| hskp30
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f964,f265]) ).
fof(f1025,plain,
! [X0] :
( ~ hskp5
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a467)
| ~ ndr1_0
| ~ c0_1(a467) ),
inference(resolution,[status(thm)],[f413,f337]) ).
fof(f1029,plain,
! [X0] :
( ~ hskp18
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a494)
| ~ ndr1_0
| ~ c0_1(a494) ),
inference(resolution,[status(thm)],[f413,f317]) ).
fof(f1034,plain,
! [X0] :
( ~ hskp27
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a576)
| ~ ndr1_0
| ~ c0_1(a576) ),
inference(resolution,[status(thm)],[f413,f302]) ).
fof(f1036,plain,
! [X0] :
( ~ hskp5
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a467)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1025,f294]) ).
fof(f1038,plain,
! [X0] :
( ~ hskp18
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a494)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1029,f275]) ).
fof(f1039,plain,
! [X0] :
( ~ hskp27
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a576)
| ~ c0_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f1034,f213]) ).
fof(f1065,plain,
! [X0] :
( ~ hskp18
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a494)
| ~ ndr1_0
| ~ c1_1(a494) ),
inference(resolution,[status(thm)],[f415,f316]) ).
fof(f1066,plain,
! [X0] :
( ~ hskp19
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a500)
| ~ ndr1_0
| ~ c1_1(a500) ),
inference(resolution,[status(thm)],[f415,f314]) ).
fof(f1067,plain,
! [X0] :
( ~ hskp22
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a519)
| ~ ndr1_0
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f415,f310]) ).
fof(f1071,plain,
! [X0] :
( ~ hskp18
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a494)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f1065,f222]) ).
fof(f1072,plain,
! [X0] :
( ~ hskp19
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a500)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1066,f274]) ).
fof(f1073,plain,
! [X0] :
( ~ hskp22
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a519)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1067,f270]) ).
fof(f1145,plain,
! [X0] :
( ~ hskp22
| hskp5
| c1_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f419,f310]) ).
fof(f1151,plain,
! [X0] :
( ~ hskp22
| hskp5
| c1_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1145,f270]) ).
fof(f1155,plain,
! [X0] :
( ~ hskp5
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a467) ),
inference(forward_subsumption_resolution,[status(thm)],[f1036,f235]) ).
fof(f1196,plain,
! [X0] :
( ~ hskp18
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f1038,f222]) ).
fof(f1203,plain,
( ~ hskp18
| ~ hskp18
| hskp16
| c3_1(a494)
| c1_1(a494)
| c1_1(a494) ),
inference(resolution,[status(thm)],[f1196,f316]) ).
fof(f1210,plain,
( ~ hskp18
| hskp16
| c3_1(a494)
| c1_1(a494) ),
inference(duplicate_literals_removal,[status(thm)],[f1203]) ).
fof(f1211,plain,
( ~ hskp18
| hskp16
| c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f1210,f317]) ).
fof(f1214,plain,
! [X0] :
( ~ hskp19
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f1072,f221]) ).
fof(f1216,plain,
( ~ hskp6
| ~ hskp19
| hskp14
| c3_1(a470)
| c1_1(a470)
| c3_1(a500) ),
inference(resolution,[status(thm)],[f1214,f335]) ).
fof(f1220,plain,
( ~ hskp16
| ~ hskp19
| hskp14
| c3_1(a487)
| c1_1(a487)
| c3_1(a500) ),
inference(resolution,[status(thm)],[f1214,f320]) ).
fof(f1227,plain,
( ~ hskp6
| ~ hskp19
| hskp14
| c3_1(a470)
| c1_1(a470) ),
inference(forward_subsumption_resolution,[status(thm)],[f1216,f315]) ).
fof(f1228,plain,
( ~ hskp16
| ~ hskp19
| hskp14
| c3_1(a487)
| c1_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f1220,f315]) ).
fof(f1239,plain,
! [X0] :
( ~ hskp18
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a494)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a494) ),
inference(resolution,[status(thm)],[f421,f316]) ).
fof(f1240,plain,
! [X0] :
( ~ hskp19
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a500) ),
inference(resolution,[status(thm)],[f421,f314]) ).
fof(f1241,plain,
! [X0] :
( ~ hskp22
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f421,f310]) ).
fof(f1245,plain,
! [X0] :
( ~ hskp18
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a494)
| ~ c1_1(X0)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f1239,f222]) ).
fof(f1246,plain,
! [X0] :
( ~ hskp19
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1240,f274]) ).
fof(f1247,plain,
! [X0] :
( ~ hskp22
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1241,f270]) ).
fof(f1254,plain,
! [X0] :
( ~ hskp13
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a482)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f423,f324]) ).
fof(f1255,plain,
! [X0] :
( ~ hskp16
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a487)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(a487) ),
inference(resolution,[status(thm)],[f423,f320]) ).
fof(f1256,plain,
! [X0] :
( ~ hskp18
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a494)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c0_1(a494) ),
inference(resolution,[status(thm)],[f423,f316]) ).
fof(f1263,plain,
! [X0] :
( ~ hskp13
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a482)
| ~ c3_1(X0)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f1254,f227]) ).
fof(f1264,plain,
! [X0] :
( ~ hskp16
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a487)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1255,f278]) ).
fof(f1265,plain,
! [X0] :
( ~ hskp18
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a494)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1256,f275]) ).
fof(f1284,plain,
( ~ hskp6
| ~ hskp19
| hskp14
| c3_1(a470) ),
inference(forward_subsumption_resolution,[status(thm)],[f1227,f334]) ).
fof(f1285,plain,
( ~ hskp16
| ~ hskp19
| hskp14
| c3_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f1228,f319]) ).
fof(f1295,plain,
! [X0] :
( ~ hskp13
| c0_1(X0)
| c1_1(a482)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f427,f324]) ).
fof(f1296,plain,
! [X0] :
( ~ hskp16
| c0_1(X0)
| c1_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a487) ),
inference(resolution,[status(thm)],[f427,f320]) ).
fof(f1297,plain,
! [X0] :
( ~ hskp18
| c0_1(X0)
| c1_1(a494)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a494) ),
inference(resolution,[status(thm)],[f427,f316]) ).
fof(f1304,plain,
! [X0] :
( ~ hskp13
| c0_1(X0)
| c1_1(a482)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f1295,f227]) ).
fof(f1305,plain,
! [X0] :
( ~ hskp16
| c0_1(X0)
| c1_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1296,f278]) ).
fof(f1306,plain,
! [X0] :
( ~ hskp18
| c0_1(X0)
| c1_1(a494)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1297,f275]) ).
fof(f1309,plain,
! [X0] :
( ~ hskp16
| c0_1(X0)
| c1_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1305,f224]) ).
fof(f1310,plain,
! [X0] :
( ~ hskp16
| ~ hskp16
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f1309,f319]) ).
fof(f1311,plain,
! [X0] :
( ~ hskp16
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1310]) ).
fof(f1317,plain,
( ~ hskp12
| ~ hskp16
| ~ c2_1(a481)
| ~ c1_1(a481) ),
inference(resolution,[status(thm)],[f1311,f325]) ).
fof(f1318,plain,
( ~ hskp14
| ~ hskp16
| ~ c2_1(a483)
| ~ c1_1(a483) ),
inference(resolution,[status(thm)],[f1311,f322]) ).
fof(f1323,plain,
( ~ hskp25
| ~ hskp16
| ~ c2_1(a545)
| ~ c1_1(a545) ),
inference(resolution,[status(thm)],[f1311,f304]) ).
fof(f1325,plain,
( ~ hskp12
| ~ hskp16
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f1317,f284]) ).
fof(f1326,plain,
( ~ hskp14
| ~ hskp16
| ~ c2_1(a483) ),
inference(forward_subsumption_resolution,[status(thm)],[f1318,f281]) ).
fof(f1328,plain,
( ~ hskp25
| ~ hskp16
| ~ c2_1(a545) ),
inference(forward_subsumption_resolution,[status(thm)],[f1323,f266]) ).
fof(f1338,plain,
( ~ hskp12
| hskp7
| ~ c2_1(a481) ),
inference(backward_subsumption_resolution,[status(thm)],[f710,f1325]) ).
fof(f1351,plain,
( hskp22
| hskp20
| c3_1(a481)
| ~ ndr1_0
| ~ c1_1(a481)
| ~ hskp12
| ~ hskp16 ),
inference(resolution,[status(thm)],[f1325,f375]) ).
fof(f1365,plain,
( hskp22
| hskp20
| c3_1(a481)
| ~ ndr1_0
| ~ hskp12
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f1351,f284]) ).
fof(f1369,plain,
( ~ hskp16
| ~ hskp19
| c3_1(a487) ),
inference(backward_subsumption_resolution,[status(thm)],[f1285,f1370]) ).
fof(f1370,plain,
( ~ hskp14
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f1326,f282]) ).
fof(f1404,plain,
! [X0] :
( ~ hskp3
| hskp2
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(a465)
| ~ c2_1(a465) ),
inference(resolution,[status(thm)],[f429,f342]) ).
fof(f1416,plain,
! [X0] :
( ~ hskp3
| hskp2
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(a465) ),
inference(forward_subsumption_resolution,[status(thm)],[f1404,f295]) ).
fof(f1443,plain,
( hskp22
| hskp20
| c3_1(a481)
| ~ hskp12
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f1365,f228]) ).
fof(f1444,plain,
( ~ hskp12
| hskp22
| hskp20
| ~ hskp12
| ~ hskp16 ),
inference(resolution,[status(thm)],[f1443,f326]) ).
fof(f1445,plain,
( hskp22
| hskp20
| ~ hskp12
| ~ hskp16 ),
inference(duplicate_literals_removal,[status(thm)],[f1444]) ).
fof(f1482,plain,
! [X0] :
( ~ hskp7
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a471)
| ~ c1_1(a471) ),
inference(resolution,[status(thm)],[f435,f332]) ).
fof(f1483,plain,
! [X0] :
( ~ hskp8
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a472)
| ~ c1_1(a472) ),
inference(resolution,[status(thm)],[f435,f331]) ).
fof(f1488,plain,
! [X0] :
( ~ hskp22
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a519)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f435,f310]) ).
fof(f1494,plain,
! [X0] :
( ~ hskp7
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c1_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f1482,f293]) ).
fof(f1495,plain,
! [X0] :
( ~ hskp8
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a472) ),
inference(forward_subsumption_resolution,[status(thm)],[f1483,f290]) ).
fof(f1496,plain,
! [X0] :
( ~ hskp22
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1488,f270]) ).
fof(f1500,plain,
! [X0] :
( ~ hskp0
| hskp13
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(a462)
| ~ c0_1(a462) ),
inference(resolution,[status(thm)],[f437,f347]) ).
fof(f1512,plain,
! [X0] :
( ~ hskp0
| hskp13
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c2_1(a462) ),
inference(forward_subsumption_resolution,[status(thm)],[f1500,f298]) ).
fof(f1520,plain,
! [X0] :
( ~ hskp18
| c0_1(X0)
| c1_1(a494)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1306,f222]) ).
fof(f1521,plain,
! [X0] :
( ~ hskp22
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1073,f218]) ).
fof(f1530,plain,
( ~ hskp18
| ~ hskp22
| hskp14
| c3_1(a494)
| c1_1(a494)
| c3_1(a519) ),
inference(resolution,[status(thm)],[f1521,f316]) ).
fof(f1538,plain,
( ~ hskp18
| ~ hskp22
| hskp14
| c1_1(a494)
| c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1530,f317]) ).
fof(f1552,plain,
! [X0] :
( ~ hskp22
| hskp14
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(a519)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f439,f309]) ).
fof(f1554,plain,
! [X0] :
( ~ hskp25
| hskp14
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(a545)
| ~ c1_1(a545) ),
inference(resolution,[status(thm)],[f439,f304]) ).
fof(f1557,plain,
! [X0] :
( ~ hskp22
| hskp14
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1552,f270]) ).
fof(f1558,plain,
! [X0] :
( ~ hskp25
| hskp14
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c3_1(a545) ),
inference(forward_subsumption_resolution,[status(thm)],[f1554,f266]) ).
fof(f1630,plain,
! [X0] :
( ~ hskp16
| c3_1(a487)
| ~ c0_1(a487)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f443,f320]) ).
fof(f1631,plain,
! [X0] :
( ~ hskp18
| c3_1(a494)
| ~ c0_1(a494)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f443,f316]) ).
fof(f1632,plain,
! [X0] :
( ~ hskp19
| c3_1(a500)
| ~ c0_1(a500)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f443,f314]) ).
fof(f1637,plain,
! [X0] :
( ~ hskp16
| c3_1(a487)
| ~ c0_1(a487)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1630,f1311]) ).
fof(f1638,plain,
! [X0] :
( ~ hskp18
| c3_1(a494)
| ~ c0_1(a494)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1631,f222]) ).
fof(f1639,plain,
! [X0] :
( ~ hskp19
| c3_1(a500)
| ~ c0_1(a500)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1632,f221]) ).
fof(f1642,plain,
! [X0] :
( ~ hskp16
| c3_1(a487)
| ~ c0_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1637,f224]) ).
fof(f1737,plain,
! [X0] :
( ~ hskp13
| hskp11
| c0_1(a482)
| ~ c3_1(a482)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f447,f324]) ).
fof(f1749,plain,
! [X0] :
( ~ hskp13
| hskp11
| c0_1(a482)
| ~ c3_1(a482)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1737,f227]) ).
fof(f1753,plain,
! [X0] :
( ~ hskp5
| hskp2
| c1_1(a467)
| ~ c0_1(a467)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f449,f337]) ).
fof(f1757,plain,
! [X0] :
( ~ hskp18
| hskp2
| c1_1(a494)
| ~ c0_1(a494)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f449,f317]) ).
fof(f1764,plain,
! [X0] :
( ~ hskp5
| hskp2
| c1_1(a467)
| ~ c0_1(a467)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1753,f235]) ).
fof(f1766,plain,
! [X0] :
( ~ hskp18
| hskp2
| c1_1(a494)
| ~ c0_1(a494)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1757,f222]) ).
fof(f1793,plain,
! [X0] :
( ~ hskp7
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a471)
| ~ c0_1(a471) ),
inference(resolution,[status(thm)],[f451,f332]) ).
fof(f1795,plain,
! [X0] :
( ~ hskp13
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a482)
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f451,f324]) ).
fof(f1796,plain,
! [X0] :
( ~ hskp16
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a487)
| ~ c0_1(a487) ),
inference(resolution,[status(thm)],[f451,f320]) ).
fof(f1803,plain,
! [X0] :
( ~ hskp7
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f1793,f292]) ).
fof(f1805,plain,
! [X0] :
( ~ hskp13
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f1795,f283]) ).
fof(f1806,plain,
! [X0] :
( ~ hskp16
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f1796,f278]) ).
fof(f1861,plain,
! [X0] :
( ~ hskp20
| hskp29
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a506)
| ~ c1_1(a506) ),
inference(resolution,[status(thm)],[f455,f313]) ).
fof(f1868,plain,
! [X0] :
( ~ hskp20
| hskp29
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a506) ),
inference(forward_subsumption_resolution,[status(thm)],[f1861,f272]) ).
fof(f1887,plain,
! [X0] :
( ~ hskp22
| hskp5
| c1_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1151,f218]) ).
fof(f1889,plain,
! [X0] :
( ~ hskp19
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1246,f221]) ).
fof(f1891,plain,
( ~ hskp12
| ~ hskp16
| ~ hskp19
| hskp6
| c0_1(a481)
| c3_1(a500)
| ~ c1_1(a481) ),
inference(resolution,[status(thm)],[f1889,f1325]) ).
fof(f1900,plain,
( ~ hskp22
| ~ hskp19
| hskp6
| c0_1(a519)
| c3_1(a500)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f1889,f310]) ).
fof(f1905,plain,
( ~ hskp12
| ~ hskp16
| ~ hskp19
| hskp6
| c0_1(a481)
| c3_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f1891,f284]) ).
fof(f1910,plain,
( ~ hskp22
| ~ hskp19
| hskp6
| c0_1(a519)
| c3_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f1900,f270]) ).
fof(f1916,plain,
( ~ hskp22
| ~ hskp19
| hskp6
| c0_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1910,f315]) ).
fof(f1917,plain,
( ~ hskp22
| ~ hskp22
| ~ hskp19
| hskp6 ),
inference(resolution,[status(thm)],[f1916,f309]) ).
fof(f1918,plain,
( ~ hskp22
| ~ hskp19
| hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f1917]) ).
fof(f1923,plain,
( ~ hskp12
| ~ hskp16
| ~ hskp19
| hskp6
| c0_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f1905,f315]) ).
fof(f1924,plain,
( ~ hskp12
| ~ hskp12
| ~ hskp16
| ~ hskp19
| hskp6 ),
inference(resolution,[status(thm)],[f1923,f325]) ).
fof(f1925,plain,
( ~ hskp12
| ~ hskp16
| ~ hskp19
| hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f1924]) ).
fof(f1932,plain,
! [X0] :
( ~ hskp14
| hskp16
| ~ c3_1(a483)
| ~ c1_1(a483)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f457,f322]) ).
fof(f1933,plain,
! [X0] :
( ~ hskp17
| hskp16
| ~ c3_1(a493)
| ~ c1_1(a493)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f457,f318]) ).
fof(f1935,plain,
! [X0] :
( ~ hskp22
| hskp16
| ~ c3_1(a519)
| ~ c1_1(a519)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f457,f309]) ).
fof(f1937,plain,
! [X0] :
( ~ hskp25
| hskp16
| ~ c3_1(a545)
| ~ c1_1(a545)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f457,f304]) ).
fof(f1939,plain,
! [X0] :
( ~ hskp14
| hskp16
| ~ c3_1(a483)
| ~ c1_1(a483)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1932,f226]) ).
fof(f1940,plain,
! [X0] :
( ~ hskp17
| hskp16
| ~ c3_1(a493)
| ~ c1_1(a493)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1933,f223]) ).
fof(f1941,plain,
! [X0] :
( ~ hskp22
| hskp16
| ~ c3_1(a519)
| ~ c1_1(a519)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1935,f218]) ).
fof(f1942,plain,
! [X0] :
( ~ hskp25
| hskp16
| ~ c3_1(a545)
| ~ c1_1(a545)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1937,f215]) ).
fof(f1954,plain,
! [X0] :
( ~ hskp16
| hskp18
| ~ c3_1(a487)
| ~ c0_1(a487)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f459,f319]) ).
fof(f1961,plain,
! [X0] :
( ~ hskp16
| hskp18
| ~ c3_1(a487)
| ~ c0_1(a487)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1954,f1311]) ).
fof(f1979,plain,
! [X0] :
( ~ hskp22
| hskp6
| c2_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1247,f218]) ).
fof(f1990,plain,
( ~ hskp22
| ~ hskp22
| hskp6
| c0_1(a519)
| c3_1(a519)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f1979,f310]) ).
fof(f1998,plain,
( ~ hskp22
| hskp6
| c0_1(a519)
| c3_1(a519)
| ~ c1_1(a519) ),
inference(duplicate_literals_removal,[status(thm)],[f1990]) ).
fof(f1999,plain,
( ~ hskp22
| hskp6
| c0_1(a519)
| c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1998,f270]) ).
fof(f2002,plain,
( ~ hskp22
| hskp6
| c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1999,f309]) ).
fof(f2076,plain,
! [X0,X1] :
( ~ hskp18
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a494)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a494) ),
inference(resolution,[status(thm)],[f465,f316]) ).
fof(f2077,plain,
! [X0,X1] :
( ~ hskp19
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a500) ),
inference(resolution,[status(thm)],[f465,f314]) ).
fof(f2078,plain,
! [X0,X1] :
( ~ hskp22
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f465,f310]) ).
fof(f2083,plain,
! [X0,X1] :
( ~ hskp18
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a494)
| ~ c1_1(X0)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f2076,f222]) ).
fof(f2084,plain,
! [X0,X1] :
( ~ hskp19
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2077,f274]) ).
fof(f2085,plain,
! [X0,X1] :
( ~ hskp22
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2078,f270]) ).
fof(f2092,plain,
! [X0,X1] :
( ~ hskp12
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c0_1(a481)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a481) ),
inference(resolution,[status(thm)],[f467,f326]) ).
fof(f2095,plain,
! [X0,X1] :
( ~ hskp19
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c0_1(a500)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a500) ),
inference(resolution,[status(thm)],[f467,f315]) ).
fof(f2101,plain,
! [X0,X1] :
( ~ hskp12
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c0_1(a481)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2092,f284]) ).
fof(f2102,plain,
! [X0,X1] :
( ~ hskp19
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c0_1(a500)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2095,f274]) ).
fof(f2106,plain,
! [X0] :
( ~ hskp16
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a487)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1264,f224]) ).
fof(f2107,plain,
( ~ hskp25
| ~ hskp16
| ~ hskp16
| hskp29
| c0_1(a545)
| c1_1(a487)
| ~ c3_1(a545) ),
inference(resolution,[status(thm)],[f2106,f1328]) ).
fof(f2109,plain,
( ~ hskp2
| ~ hskp16
| hskp29
| c0_1(a464)
| c1_1(a487)
| ~ c3_1(a464) ),
inference(resolution,[status(thm)],[f2106,f344]) ).
fof(f2110,plain,
( ~ hskp6
| ~ hskp16
| hskp29
| c0_1(a470)
| c1_1(a487)
| ~ c3_1(a470) ),
inference(resolution,[status(thm)],[f2106,f335]) ).
fof(f2117,plain,
( ~ hskp22
| ~ hskp16
| hskp29
| c0_1(a519)
| c1_1(a487)
| ~ c3_1(a519) ),
inference(resolution,[status(thm)],[f2106,f310]) ).
fof(f2121,plain,
( ~ hskp25
| ~ hskp16
| hskp29
| c0_1(a545)
| c1_1(a487)
| ~ c3_1(a545) ),
inference(duplicate_literals_removal,[status(thm)],[f2107]) ).
fof(f2122,plain,
( ~ hskp25
| ~ hskp16
| hskp29
| c0_1(a545)
| c1_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f2121,f267]) ).
fof(f2124,plain,
( ~ hskp2
| ~ hskp16
| hskp29
| c0_1(a464)
| c1_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f2109,f296]) ).
fof(f2125,plain,
( ~ hskp6
| ~ hskp16
| hskp29
| c0_1(a470)
| ~ c3_1(a470) ),
inference(forward_subsumption_resolution,[status(thm)],[f2110,f319]) ).
fof(f2129,plain,
( ~ hskp22
| ~ hskp16
| hskp29
| c0_1(a519)
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f2117,f319]) ).
fof(f2130,plain,
( ~ hskp25
| ~ hskp16
| hskp29
| c0_1(a545) ),
inference(forward_subsumption_resolution,[status(thm)],[f2122,f319]) ).
fof(f2131,plain,
( ~ hskp25
| ~ hskp25
| ~ hskp16
| hskp29 ),
inference(resolution,[status(thm)],[f2130,f304]) ).
fof(f2132,plain,
( ~ hskp25
| ~ hskp16
| hskp29 ),
inference(duplicate_literals_removal,[status(thm)],[f2131]) ).
fof(f2133,plain,
( ~ hskp2
| ~ hskp16
| hskp29
| c0_1(a464) ),
inference(forward_subsumption_resolution,[status(thm)],[f2124,f319]) ).
fof(f2134,plain,
( ~ hskp2
| ~ hskp2
| ~ hskp16
| hskp29 ),
inference(resolution,[status(thm)],[f2133,f343]) ).
fof(f2135,plain,
( ~ hskp2
| ~ hskp16
| hskp29 ),
inference(duplicate_literals_removal,[status(thm)],[f2134]) ).
fof(f2136,plain,
( ~ hskp6
| ~ hskp16
| hskp29
| ~ c3_1(a470) ),
inference(forward_subsumption_resolution,[status(thm)],[f2125,f333]) ).
fof(f2139,plain,
( ~ hskp22
| ~ hskp16
| hskp29
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f2129,f309]) ).
fof(f2140,plain,
! [X0] :
( ~ hskp18
| hskp29
| c2_1(X0)
| c0_1(X0)
| c1_1(a494)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1265,f222]) ).
fof(f2143,plain,
( ~ hskp2
| ~ hskp18
| hskp29
| c0_1(a464)
| c1_1(a494)
| ~ c3_1(a464) ),
inference(resolution,[status(thm)],[f2140,f344]) ).
fof(f2155,plain,
( ~ hskp2
| ~ hskp18
| hskp29
| c0_1(a464)
| c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f2143,f296]) ).
fof(f2161,plain,
( ~ hskp2
| ~ hskp18
| hskp29
| c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f2155,f343]) ).
fof(f2170,plain,
! [X0,X1] :
( ~ hskp18
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a494)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a494) ),
inference(resolution,[status(thm)],[f471,f316]) ).
fof(f2171,plain,
! [X0,X1] :
( ~ hskp19
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a500) ),
inference(resolution,[status(thm)],[f471,f314]) ).
fof(f2177,plain,
! [X0,X1] :
( ~ hskp18
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a494)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2170,f275]) ).
fof(f2178,plain,
! [X0,X1] :
( ~ hskp19
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c3_1(X1)
| ~ c1_1(X0)
| ~ c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f2171,f221]) ).
fof(f2302,plain,
! [X0,X1] :
( ~ hskp7
| c3_1(X1)
| c0_1(X1)
| c3_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(a471)
| ~ c0_1(a471) ),
inference(resolution,[status(thm)],[f477,f332]) ).
fof(f2312,plain,
! [X0,X1] :
( ~ hskp7
| c3_1(X1)
| c0_1(X1)
| c3_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ ndr1_0
| ~ c1_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f2302,f292]) ).
fof(f2335,plain,
! [X0] :
( ~ hskp13
| c0_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f1304,f323]) ).
fof(f2341,plain,
( ~ hskp12
| ~ hskp13
| ~ c2_1(a481)
| ~ c1_1(a481)
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f2335,f325]) ).
fof(f2342,plain,
( ~ hskp14
| ~ hskp13
| ~ c2_1(a483)
| ~ c1_1(a483)
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f2335,f322]) ).
fof(f2349,plain,
( ~ hskp12
| ~ hskp13
| ~ c2_1(a481)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f2341,f284]) ).
fof(f2350,plain,
( ~ hskp14
| ~ hskp13
| ~ c2_1(a483)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f2342,f281]) ).
fof(f2405,plain,
( hskp22
| hskp20
| c3_1(a481)
| ~ ndr1_0
| ~ c1_1(a481)
| ~ hskp12
| ~ hskp13
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f2349,f375]) ).
fof(f2424,plain,
( hskp22
| hskp20
| c3_1(a481)
| ~ ndr1_0
| ~ hskp12
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f2405,f284]) ).
fof(f2428,plain,
( ~ hskp14
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f2350,f282]) ).
fof(f2615,plain,
( hskp22
| hskp20
| c3_1(a481)
| ~ hskp12
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f2424,f228]) ).
fof(f2616,plain,
( ~ hskp12
| hskp22
| hskp20
| ~ hskp12
| ~ hskp13
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f2615,f326]) ).
fof(f2617,plain,
( hskp22
| hskp20
| ~ hskp12
| ~ hskp13
| ~ c0_1(a482) ),
inference(duplicate_literals_removal,[status(thm)],[f2616]) ).
fof(f2742,plain,
! [X0] :
( ~ hskp27
| hskp16
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f1039,f300]) ).
fof(f2758,plain,
( ~ hskp27
| ~ hskp27
| hskp16
| c3_1(a576)
| c1_1(a576)
| ~ c0_1(a576) ),
inference(resolution,[status(thm)],[f2742,f301]) ).
fof(f2761,plain,
( ~ hskp27
| hskp16
| c3_1(a576)
| c1_1(a576)
| ~ c0_1(a576) ),
inference(duplicate_literals_removal,[status(thm)],[f2758]) ).
fof(f2762,plain,
( ~ hskp27
| hskp16
| c3_1(a576)
| ~ c0_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f2761,f300]) ).
fof(f2763,plain,
! [X0] :
( ~ hskp18
| hskp14
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f1071,f317]) ).
fof(f2769,plain,
( ~ hskp6
| ~ hskp18
| hskp14
| c3_1(a470)
| c1_1(a470)
| ~ c1_1(a494) ),
inference(resolution,[status(thm)],[f2763,f335]) ).
fof(f2780,plain,
( ~ hskp6
| ~ hskp18
| hskp14
| c3_1(a470)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f2769,f334]) ).
fof(f2805,plain,
( ~ hskp27
| hskp16
| ~ c0_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f2762,f302]) ).
fof(f2936,plain,
! [X0] :
( ~ hskp18
| hskp6
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f1245,f317]) ).
fof(f2949,plain,
( ~ hskp22
| ~ hskp18
| hskp6
| c0_1(a519)
| ~ c1_1(a519)
| ~ c1_1(a494) ),
inference(resolution,[status(thm)],[f2936,f310]) ).
fof(f2960,plain,
( ~ hskp22
| ~ hskp18
| hskp6
| c0_1(a519)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f2949,f270]) ).
fof(f3032,plain,
! [X0] :
( ~ hskp13
| hskp29
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f1263,f323]) ).
fof(f3038,plain,
( ~ hskp6
| ~ hskp13
| hskp29
| c0_1(a470)
| ~ c3_1(a470)
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f3032,f335]) ).
fof(f3045,plain,
( ~ hskp22
| ~ hskp13
| hskp29
| c0_1(a519)
| ~ c3_1(a519)
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f3032,f310]) ).
fof(f3053,plain,
( ~ hskp6
| ~ hskp13
| hskp29
| ~ c3_1(a470)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f3038,f333]) ).
fof(f3055,plain,
( ~ hskp22
| ~ hskp13
| hskp29
| ~ c3_1(a519)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f3045,f309]) ).
fof(f3362,plain,
( ~ hskp22
| ~ hskp18
| hskp6
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f2960,f309]) ).
fof(f3387,plain,
! [X0] :
( ~ hskp3
| hskp2
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ c2_1(a465) ),
inference(forward_subsumption_resolution,[status(thm)],[f1416,f237]) ).
fof(f3400,plain,
( ~ hskp18
| ~ hskp3
| hskp2
| c3_1(a494)
| c1_1(a494)
| ~ c2_1(a465) ),
inference(resolution,[status(thm)],[f3387,f316]) ).
fof(f3408,plain,
( ~ hskp18
| ~ hskp3
| hskp2
| c1_1(a494)
| ~ c2_1(a465) ),
inference(forward_subsumption_resolution,[status(thm)],[f3400,f317]) ).
fof(f3686,plain,
! [X0] :
( ~ hskp7
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f1494,f233]) ).
fof(f3697,plain,
( ~ hskp13
| ~ hskp7
| hskp10
| c0_1(a482)
| ~ c3_1(a482)
| ~ c1_1(a471) ),
inference(resolution,[status(thm)],[f3686,f324]) ).
fof(f3712,plain,
( ~ hskp13
| ~ hskp7
| hskp10
| c0_1(a482)
| ~ c1_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f3697,f283]) ).
fof(f3715,plain,
! [X0] :
( ~ hskp8
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1495,f291]) ).
fof(f3726,plain,
( ~ hskp13
| ~ hskp8
| hskp10
| c0_1(a482)
| ~ c3_1(a482)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3715,f324]) ).
fof(f3741,plain,
( ~ hskp13
| ~ hskp8
| hskp10
| c0_1(a482)
| ~ c3_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f3726,f232]) ).
fof(f3743,plain,
! [X0] :
( ~ hskp22
| hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0)
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1496,f218]) ).
fof(f3758,plain,
( ~ hskp22
| ~ hskp22
| hskp10
| c0_1(a519)
| ~ c3_1(a519)
| ~ c3_1(a519) ),
inference(resolution,[status(thm)],[f3743,f310]) ).
fof(f3769,plain,
( ~ hskp22
| hskp10
| c0_1(a519)
| ~ c3_1(a519) ),
inference(duplicate_literals_removal,[status(thm)],[f3758]) ).
fof(f3770,plain,
( ~ hskp22
| hskp10
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f3769,f309]) ).
fof(f3786,plain,
( ~ hskp13
| ~ hskp8
| hskp10
| c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f3741,f283]) ).
fof(f3815,plain,
! [X0] :
( ~ hskp0
| hskp13
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1512,f299]) ).
fof(f3820,plain,
( ~ hskp12
| ~ hskp0
| hskp13
| c0_1(a481)
| ~ c1_1(a481)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3815,f326]) ).
fof(f3829,plain,
( ~ hskp12
| ~ hskp0
| hskp13
| c0_1(a481)
| ~ c1_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f3820,f240]) ).
fof(f3874,plain,
( ~ hskp12
| ~ hskp0
| hskp13
| c0_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f3829,f284]) ).
fof(f3875,plain,
( ~ hskp12
| ~ hskp12
| ~ hskp0
| hskp13 ),
inference(resolution,[status(thm)],[f3874,f325]) ).
fof(f3876,plain,
( ~ hskp12
| ~ hskp0
| hskp13 ),
inference(duplicate_literals_removal,[status(thm)],[f3875]) ).
fof(f3958,plain,
! [X0] :
( ~ hskp22
| hskp14
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f1557,f218]) ).
fof(f3962,plain,
( ~ hskp10
| ~ hskp22
| hskp14
| c0_1(a478)
| ~ c2_1(a478)
| ~ c3_1(a519) ),
inference(resolution,[status(thm)],[f3958,f329]) ).
fof(f3963,plain,
( ~ hskp12
| ~ hskp22
| hskp14
| c0_1(a481)
| ~ c2_1(a481)
| ~ c3_1(a519) ),
inference(resolution,[status(thm)],[f3958,f326]) ).
fof(f3973,plain,
( ~ hskp10
| ~ hskp22
| hskp14
| c0_1(a478)
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f3962,f287]) ).
fof(f3974,plain,
( ~ hskp12
| ~ hskp22
| hskp14
| ~ c2_1(a481)
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f3963,f325]) ).
fof(f3979,plain,
! [X0] :
( ~ hskp25
| hskp14
| c3_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1558,f267]) ).
fof(f3983,plain,
( ~ hskp10
| ~ hskp25
| hskp14
| c0_1(a478)
| ~ c2_1(a478)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3979,f329]) ).
fof(f3994,plain,
( ~ hskp10
| ~ hskp25
| hskp14
| c0_1(a478)
| ~ c2_1(a478) ),
inference(forward_subsumption_resolution,[status(thm)],[f3983,f230]) ).
fof(f3999,plain,
( ~ hskp10
| ~ hskp22
| hskp14
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f3973,f328]) ).
fof(f4003,plain,
( ~ hskp10
| ~ hskp25
| hskp14
| c0_1(a478) ),
inference(forward_subsumption_resolution,[status(thm)],[f3994,f287]) ).
fof(f4004,plain,
( ~ hskp10
| ~ hskp10
| ~ hskp25
| hskp14 ),
inference(resolution,[status(thm)],[f4003,f328]) ).
fof(f4005,plain,
( ~ hskp10
| ~ hskp25
| hskp14 ),
inference(duplicate_literals_removal,[status(thm)],[f4004]) ).
fof(f4080,plain,
! [X0] :
( ~ hskp18
| c3_1(a494)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1638,f275]) ).
fof(f4081,plain,
! [X0] :
( ~ hskp18
| ~ hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f4080,f317]) ).
fof(f4082,plain,
! [X0] :
( ~ hskp18
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f4081]) ).
fof(f4083,plain,
! [X0] :
( ~ hskp18
| c1_1(a494)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1520,f4082]) ).
fof(f4084,plain,
! [X0,X1] :
( c1_1(X1)
| ~ c3_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f459,f4082]) ).
fof(f4093,plain,
( ~ hskp20
| ~ hskp18
| ~ c1_1(a506)
| ~ c0_1(a506) ),
inference(resolution,[status(thm)],[f4082,f273]) ).
fof(f4096,plain,
( ~ hskp29
| ~ hskp18
| ~ c1_1(a474)
| ~ c0_1(a474) ),
inference(resolution,[status(thm)],[f4082,f260]) ).
fof(f4167,plain,
( ~ hskp20
| ~ hskp18
| ~ c0_1(a506) ),
inference(forward_subsumption_resolution,[status(thm)],[f4093,f272]) ).
fof(f4169,plain,
( ~ hskp29
| ~ hskp18
| ~ c1_1(a474) ),
inference(forward_subsumption_resolution,[status(thm)],[f4096,f258]) ).
fof(f4243,plain,
( ~ hskp16
| ~ c2_1(a506)
| ~ c1_1(a506)
| ~ hskp20
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4167,f1311]) ).
fof(f4260,plain,
( ~ hskp16
| ~ c2_1(a506)
| ~ hskp20
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4243,f272]) ).
fof(f4278,plain,
( ~ hskp2
| ~ hskp18
| c1_1(a494) ),
inference(backward_subsumption_resolution,[status(thm)],[f2161,f4280]) ).
fof(f4280,plain,
( ~ hskp29
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4169,f259]) ).
fof(f4286,plain,
( ~ hskp6
| ~ hskp13
| ~ c3_1(a470)
| ~ c0_1(a482)
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4280,f3053]) ).
fof(f4289,plain,
( ~ hskp22
| ~ hskp16
| ~ c3_1(a519)
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4280,f2139]) ).
fof(f4290,plain,
( ~ hskp6
| ~ hskp16
| ~ c3_1(a470)
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4280,f2136]) ).
fof(f4291,plain,
( ~ hskp2
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4280,f2135]) ).
fof(f4292,plain,
( ~ hskp25
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4280,f2132]) ).
fof(f4304,plain,
( hskp14
| hskp0
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4292,f247]) ).
fof(f4307,plain,
( hskp0
| ~ hskp16
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4304,f1370]) ).
fof(f4349,plain,
! [X0] :
( ~ hskp11
| ~ c3_1(a479)
| ~ c0_1(a479)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f4084,f327]) ).
fof(f4350,plain,
! [X0] :
( ~ hskp13
| ~ c3_1(a482)
| ~ c0_1(a482)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f4084,f323]) ).
fof(f4356,plain,
! [X0] :
( ~ hskp11
| ~ c3_1(a479)
| ~ c0_1(a479)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4349,f229]) ).
fof(f4357,plain,
! [X0] :
( ~ hskp13
| ~ c3_1(a482)
| ~ c0_1(a482)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4350,f2335]) ).
fof(f4364,plain,
( ~ hskp18
| ~ hskp3
| c1_1(a494)
| ~ c2_1(a465) ),
inference(backward_subsumption_resolution,[status(thm)],[f3408,f4278]) ).
fof(f4376,plain,
( ~ hskp16
| ~ hskp20
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4260,f273]) ).
fof(f4379,plain,
( hskp22
| ~ hskp12
| ~ hskp16
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4376,f1445]) ).
fof(f4381,plain,
( ~ hskp18
| hskp22
| ~ c1_1(a494)
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4376,f871]) ).
fof(f4387,plain,
( hskp22
| ~ hskp12
| ~ hskp16
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f4379]) ).
fof(f4388,plain,
( hskp22
| ~ c1_1(a494)
| ~ hskp16
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f4381]) ).
fof(f4412,plain,
! [X0] :
( ~ hskp19
| ~ c0_1(a500)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1639,f315]) ).
fof(f4423,plain,
( ~ hskp29
| ~ hskp19
| ~ c0_1(a500)
| ~ c1_1(a474)
| ~ c0_1(a474) ),
inference(resolution,[status(thm)],[f4412,f260]) ).
fof(f4494,plain,
( ~ hskp29
| ~ hskp19
| ~ c0_1(a500)
| ~ c1_1(a474) ),
inference(forward_subsumption_resolution,[status(thm)],[f4423,f258]) ).
fof(f4730,plain,
( ~ hskp22
| hskp6
| ~ hskp22
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4289,f2002]) ).
fof(f4733,plain,
( ~ hskp18
| ~ hskp22
| hskp14
| c1_1(a494)
| ~ hskp22
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4289,f1538]) ).
fof(f4768,plain,
( hskp6
| ~ hskp22
| ~ hskp16
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f4730]) ).
fof(f4773,plain,
( hskp14
| c1_1(a494)
| ~ hskp22
| ~ hskp16
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f4733]) ).
fof(f4774,plain,
( hskp14
| c1_1(a494)
| ~ hskp22
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4773,f1211]) ).
fof(f4793,plain,
( ~ hskp6
| ~ hskp18
| hskp14
| ~ c1_1(a494)
| ~ hskp6
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4290,f2780]) ).
fof(f4841,plain,
( hskp14
| ~ c1_1(a494)
| ~ hskp6
| ~ hskp16
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f4793]) ).
fof(f4842,plain,
( ~ c1_1(a494)
| ~ hskp6
| ~ hskp16
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4841,f1370]) ).
fof(f4894,plain,
( hskp14
| ~ hskp22
| ~ hskp18
| ~ hskp6
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4842,f4774]) ).
fof(f4911,plain,
( hskp14
| ~ hskp22
| ~ hskp6
| ~ hskp16
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f4894]) ).
fof(f4912,plain,
( hskp14
| ~ hskp22
| ~ hskp16
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4911,f4768]) ).
fof(f4923,plain,
( ~ c1_1(a494)
| ~ hskp16
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f4388,f4926]) ).
fof(f4925,plain,
( ~ hskp12
| ~ hskp16
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f4387,f4926]) ).
fof(f4926,plain,
( ~ hskp22
| ~ hskp16
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f4912,f1370]) ).
fof(f5018,plain,
! [X0] :
( ~ hskp13
| hskp11
| c0_1(a482)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1749,f283]) ).
fof(f5147,plain,
! [X0] :
( ~ hskp5
| hskp2
| c1_1(a467)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1764,f294]) ).
fof(f5148,plain,
! [X0] :
( ~ hskp5
| ~ hskp5
| hskp2
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f5147,f336]) ).
fof(f5149,plain,
! [X0] :
( ~ hskp5
| hskp2
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5148]) ).
fof(f5153,plain,
! [X0] :
( ~ hskp16
| ~ hskp18
| ~ hskp18
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f4083,f4923]) ).
fof(f5154,plain,
! [X0] :
( ~ hskp16
| ~ hskp18
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5153]) ).
fof(f5224,plain,
! [X0] :
( hskp22
| hskp20
| c3_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ hskp16
| ~ hskp18
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f5154,f375]) ).
fof(f5271,plain,
! [X0] :
( hskp22
| hskp20
| c3_1(X0)
| ~ ndr1_0
| ~ hskp16
| ~ hskp18
| ~ c1_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5224]) ).
fof(f5272,plain,
! [X0] :
( hskp22
| hskp20
| c3_1(X0)
| ~ hskp16
| ~ hskp18
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5271,f224]) ).
fof(f5296,plain,
! [X0] :
( ~ hskp18
| hskp2
| c1_1(a494)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1766,f275]) ).
fof(f5297,plain,
! [X0] :
( ~ hskp16
| ~ hskp18
| ~ hskp18
| hskp2
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f5296,f4923]) ).
fof(f5298,plain,
! [X0] :
( ~ hskp16
| ~ hskp18
| hskp2
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5297]) ).
fof(f5299,plain,
! [X0] :
( ~ hskp16
| ~ hskp18
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5298,f4291]) ).
fof(f5303,plain,
! [X0] :
( ~ hskp7
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1803,f293]) ).
fof(f5729,plain,
( ~ hskp16
| ~ hskp18
| ~ hskp18
| ~ hskp3
| ~ c2_1(a465) ),
inference(resolution,[status(thm)],[f4364,f4923]) ).
fof(f5730,plain,
( ~ hskp16
| ~ hskp18
| ~ hskp3
| ~ c2_1(a465) ),
inference(duplicate_literals_removal,[status(thm)],[f5729]) ).
fof(f5855,plain,
! [X0] :
( ~ hskp13
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f1805,f227]) ).
fof(f5872,plain,
( ~ hskp5
| ~ hskp13
| hskp12
| ~ c2_1(a467)
| ~ c0_1(a467)
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f5855,f336]) ).
fof(f5886,plain,
( ~ hskp5
| ~ hskp13
| hskp12
| ~ c2_1(a467)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f5872,f294]) ).
fof(f5890,plain,
! [X0] :
( ~ hskp16
| hskp12
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f1806,f224]) ).
fof(f5903,plain,
( ~ hskp0
| ~ hskp16
| hskp12
| ~ c2_1(a462)
| ~ c0_1(a462)
| ~ c3_1(a487) ),
inference(resolution,[status(thm)],[f5890,f347]) ).
fof(f5921,plain,
( ~ hskp0
| ~ hskp16
| hskp12
| ~ c2_1(a462)
| ~ c3_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f5903,f298]) ).
fof(f6008,plain,
( ~ hskp29
| ~ hskp19
| ~ c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f4494,f259]) ).
fof(f6569,plain,
! [X0] :
( ~ hskp20
| hskp29
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1868,f273]) ).
fof(f6584,plain,
( ~ hskp19
| ~ hskp20
| hskp29
| ~ c1_1(a500)
| ~ c0_1(a500)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f6569,f314]) ).
fof(f6592,plain,
! [X0] :
( ~ hskp18
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp20
| hskp29
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f6569,f4082]) ).
fof(f6596,plain,
( ~ hskp19
| ~ hskp20
| hskp29
| ~ c1_1(a500)
| ~ c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f6584,f221]) ).
fof(f6602,plain,
! [X0] :
( ~ hskp18
| ~ hskp20
| hskp29
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(duplicate_literals_removal,[status(thm)],[f6592]) ).
fof(f6603,plain,
! [X0] :
( ~ hskp18
| ~ hskp20
| hskp29
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6602,f222]) ).
fof(f6745,plain,
! [X0] :
( ~ hskp14
| hskp16
| ~ c3_1(a483)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1939,f281]) ).
fof(f6751,plain,
! [X0] :
( ~ hskp17
| hskp16
| ~ c1_1(a493)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1940,f277]) ).
fof(f6756,plain,
! [X0] :
( ~ hskp22
| hskp16
| ~ c3_1(a519)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1941,f270]) ).
fof(f6761,plain,
! [X0] :
( ~ hskp25
| hskp16
| ~ c3_1(a545)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1942,f266]) ).
fof(f6889,plain,
! [X0] :
( ~ hskp18
| ~ hskp20
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6603,f4280]) ).
fof(f6917,plain,
( ~ hskp18
| hskp16
| ~ hskp18
| ~ hskp20
| ~ c0_1(a494) ),
inference(resolution,[status(thm)],[f6889,f1211]) ).
fof(f7014,plain,
( hskp16
| ~ hskp18
| ~ hskp20
| ~ c0_1(a494) ),
inference(duplicate_literals_removal,[status(thm)],[f6917]) ).
fof(f7015,plain,
( hskp16
| ~ hskp18
| ~ hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f7014,f275]) ).
fof(f7052,plain,
! [X0] :
( ~ hskp16
| hskp18
| ~ c3_1(a487)
| ~ c0_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1961,f224]) ).
fof(f7083,plain,
( ~ hskp18
| hskp22
| ~ c1_1(a494) ),
inference(backward_subsumption_resolution,[status(thm)],[f871,f7084]) ).
fof(f7084,plain,
( ~ hskp18
| ~ hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f7015,f4376]) ).
fof(f7104,plain,
( ~ hskp18
| hskp6
| ~ c1_1(a494) ),
inference(backward_subsumption_resolution,[status(thm)],[f3362,f7083]) ).
fof(f7107,plain,
( ~ hskp18
| hskp14
| c3_1(a470)
| ~ c1_1(a494) ),
inference(backward_subsumption_resolution,[status(thm)],[f2780,f7104]) ).
fof(f7369,plain,
! [X0,X1] :
( ~ hskp18
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f2083,f317]) ).
fof(f7385,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| ~ c1_1(a519)
| ~ c1_1(a494) ),
inference(resolution,[status(thm)],[f7369,f310]) ).
fof(f7400,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| ~ c1_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f7385,f270]) ).
fof(f7404,plain,
! [X0,X1] :
( ~ hskp19
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2084,f221]) ).
fof(f7475,plain,
! [X0,X1] :
( ~ hskp22
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a519)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2085,f218]) ).
fof(f7491,plain,
! [X0] :
( ~ hskp22
| ~ hskp22
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a519)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f7475,f310]) ).
fof(f7506,plain,
! [X0] :
( ~ hskp22
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a519)
| ~ c1_1(a519) ),
inference(duplicate_literals_removal,[status(thm)],[f7491]) ).
fof(f7507,plain,
! [X0] :
( ~ hskp22
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f7506,f270]) ).
fof(f7938,plain,
( ~ hskp18
| hskp14
| ~ c1_1(a494)
| ~ hskp6
| ~ hskp13
| ~ c0_1(a482)
| ~ hskp18 ),
inference(resolution,[status(thm)],[f4286,f7107]) ).
fof(f7980,plain,
( hskp14
| ~ c1_1(a494)
| ~ hskp6
| ~ hskp13
| ~ c0_1(a482)
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f7938]) ).
fof(f7981,plain,
( hskp14
| ~ c1_1(a494)
| ~ hskp13
| ~ c0_1(a482)
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f7980,f7104]) ).
fof(f8138,plain,
! [X0,X1] :
( ~ hskp12
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c0_1(a481)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2101,f228]) ).
fof(f8154,plain,
! [X0] :
( ~ hskp22
| ~ hskp12
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| c0_1(a519)
| c0_1(a481)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f8138,f310]) ).
fof(f8174,plain,
! [X0] :
( ~ hskp22
| ~ hskp12
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| c0_1(a519)
| c0_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f8154,f270]) ).
fof(f8181,plain,
! [X0,X1] :
( ~ hskp19
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c0_1(a500)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2102,f221]) ).
fof(f8196,plain,
! [X0] :
( ~ hskp19
| ~ hskp19
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| c0_1(a500)
| c0_1(a500)
| ~ c1_1(a500) ),
inference(resolution,[status(thm)],[f8181,f314]) ).
fof(f8213,plain,
! [X0] :
( ~ hskp19
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| c0_1(a500)
| ~ c1_1(a500) ),
inference(duplicate_literals_removal,[status(thm)],[f8196]) ).
fof(f8214,plain,
! [X0] :
( ~ hskp19
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f8213,f274]) ).
fof(f8395,plain,
! [X0,X1] :
( ~ hskp18
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a494)
| ~ c3_1(X1)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2177,f222]) ).
fof(f8411,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a494)
| ~ c3_1(X0)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f8395,f310]) ).
fof(f8427,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a494)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8411,f270]) ).
fof(f8435,plain,
! [X0,X1] :
( ~ hskp19
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c0_1(X0)
| c3_1(a500)
| ~ c1_1(X0)
| ~ c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f2178,f7404]) ).
fof(f8451,plain,
! [X0] :
( ~ hskp22
| ~ hskp19
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a500)
| ~ c1_1(a519)
| ~ c0_1(a500) ),
inference(resolution,[status(thm)],[f8435,f310]) ).
fof(f8467,plain,
! [X0] :
( ~ hskp22
| ~ hskp19
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a500)
| ~ c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f8451,f270]) ).
fof(f8578,plain,
! [X0] :
( hskp22
| c3_1(X0)
| ~ hskp16
| ~ hskp18
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5272,f7084]) ).
fof(f8599,plain,
! [X0] :
( ~ hskp16
| ~ hskp18
| ~ c1_1(X0)
| ~ c0_1(X0)
| hskp22
| ~ hskp16
| ~ hskp18
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f8578,f5299]) ).
fof(f8608,plain,
! [X0] :
( ~ c0_1(X0)
| hskp22
| ~ hskp16
| ~ hskp18
| ~ c1_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f8599]) ).
fof(f8609,plain,
! [X0] :
( ~ c0_1(X0)
| ~ hskp16
| ~ hskp18
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8608,f4926]) ).
fof(f8775,plain,
! [X0] :
( ~ hskp16
| hskp12
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ c3_1(a487)
| ~ c0_1(X0)
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f8609,f5890]) ).
fof(f8809,plain,
! [X0] :
( hskp12
| ~ c2_1(X0)
| ~ c3_1(a487)
| ~ c0_1(X0)
| ~ hskp16
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f8775]) ).
fof(f8810,plain,
! [X0] :
( ~ c2_1(X0)
| ~ c3_1(a487)
| ~ c0_1(X0)
| ~ hskp16
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f8809,f4925]) ).
fof(f8932,plain,
( ~ hskp0
| ~ hskp16
| hskp12
| ~ c3_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f5921,f299]) ).
fof(f9577,plain,
! [X0,X1] :
( ~ hskp7
| c3_1(X1)
| c0_1(X1)
| c3_1(X0)
| c1_1(X0)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c1_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f2312,f233]) ).
fof(f9586,plain,
! [X0] :
( ~ hskp1
| ~ hskp7
| c3_1(X0)
| c0_1(X0)
| c1_1(a463)
| ~ c1_1(X0)
| ~ c2_1(a463)
| ~ c1_1(a471) ),
inference(resolution,[status(thm)],[f9577,f346]) ).
fof(f9598,plain,
! [X0] :
( ~ hskp1
| ~ hskp7
| c3_1(X0)
| c0_1(X0)
| c1_1(a463)
| ~ c1_1(X0)
| ~ c1_1(a471) ),
inference(forward_subsumption_resolution,[status(thm)],[f9586,f297]) ).
fof(f10743,plain,
( ~ hskp19
| ~ hskp20
| hskp29
| ~ c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f6596,f274]) ).
fof(f11939,plain,
( ~ c1_1(a494)
| ~ hskp13
| ~ c0_1(a482)
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f7981,f2428]) ).
fof(f11958,plain,
( ~ hskp18
| hskp16
| ~ hskp13
| ~ c0_1(a482)
| ~ hskp18 ),
inference(resolution,[status(thm)],[f11939,f1211]) ).
fof(f11999,plain,
( hskp16
| ~ hskp13
| ~ c0_1(a482)
| ~ hskp18 ),
inference(duplicate_literals_removal,[status(thm)],[f11958]) ).
fof(f15146,plain,
( ~ hskp0
| ~ c3_1(a487)
| ~ c0_1(a462)
| ~ hskp16
| ~ hskp18 ),
inference(resolution,[status(thm)],[f8810,f299]) ).
fof(f15246,plain,
( ~ hskp0
| ~ c3_1(a487)
| ~ hskp16
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f15146,f298]) ).
fof(f15276,plain,
! [X0] :
( ~ hskp16
| ~ c3_1(a487)
| ~ c0_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f7052,f15277]) ).
fof(f15277,plain,
( ~ c3_1(a487)
| ~ hskp16
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f15246,f4307]) ).
fof(f15325,plain,
! [X0] :
( ~ hskp16
| ~ c3_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15276,f278]) ).
fof(f15342,plain,
! [X0] :
( ~ hskp16
| ~ c0_1(a487)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1642,f15325]) ).
fof(f15443,plain,
! [X0] :
( ~ hskp16
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15342,f278]) ).
fof(f15523,plain,
! [X0,X1] :
( c0_1(X1)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f457,f15443]) ).
fof(f15524,plain,
! [X0] :
( ~ hskp25
| ~ c3_1(a545)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6761,f15443]) ).
fof(f15525,plain,
! [X0] :
( ~ hskp22
| ~ c3_1(a519)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6756,f15443]) ).
fof(f15526,plain,
! [X0] :
( ~ hskp17
| ~ c1_1(a493)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6751,f15443]) ).
fof(f15527,plain,
! [X0] :
( ~ hskp14
| ~ c3_1(a483)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6745,f15443]) ).
fof(f15539,plain,
( ~ hskp29
| ~ hskp16
| ~ c1_1(a474) ),
inference(resolution,[status(thm)],[f15443,f260]) ).
fof(f15629,plain,
! [X0] :
( ~ hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15524,f267]) ).
fof(f15631,plain,
( ~ hskp29
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f15539,f259]) ).
fof(f15711,plain,
! [X0] :
( ~ hskp16
| c2_1(X0)
| c0_1(X0)
| c1_1(a487)
| ~ c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2106,f15631]) ).
fof(f15714,plain,
( ~ hskp6
| ~ hskp16
| ~ c3_1(a470) ),
inference(backward_subsumption_resolution,[status(thm)],[f2136,f15631]) ).
fof(f15716,plain,
( ~ hskp25
| ~ hskp16 ),
inference(backward_subsumption_resolution,[status(thm)],[f2132,f15631]) ).
fof(f15724,plain,
! [X0] :
( ~ hskp16
| c2_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15711,f319]) ).
fof(f15765,plain,
( hskp14
| hskp0
| ~ hskp16 ),
inference(resolution,[status(thm)],[f15716,f247]) ).
fof(f15768,plain,
( hskp0
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f15765,f1370]) ).
fof(f15769,plain,
( ~ hskp16
| hskp12
| ~ c3_1(a487) ),
inference(backward_subsumption_resolution,[status(thm)],[f8932,f15768]) ).
fof(f15772,plain,
! [X0,X1] :
( hskp28
| c0_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f445,f15523]) ).
fof(f15851,plain,
! [X0] :
( ~ hskp2
| hskp28
| ~ c3_1(a464)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f15772,f343]) ).
fof(f15858,plain,
! [X0] :
( ~ hskp17
| hskp28
| ~ c3_1(a493)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f15772,f318]) ).
fof(f15873,plain,
! [X0] :
( ~ hskp2
| hskp28
| ~ c3_1(a464)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15851,f238]) ).
fof(f15875,plain,
! [X0] :
( ~ hskp17
| hskp28
| ~ c3_1(a493)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15858,f223]) ).
fof(f17359,plain,
( ~ hskp6
| ~ hskp19
| hskp14
| ~ hskp6
| ~ hskp16 ),
inference(resolution,[status(thm)],[f15714,f1284]) ).
fof(f17411,plain,
( ~ hskp19
| hskp14
| ~ hskp6
| ~ hskp16 ),
inference(duplicate_literals_removal,[status(thm)],[f17359]) ).
fof(f17412,plain,
( ~ hskp19
| ~ hskp6
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f17411,f1370]) ).
fof(f17422,plain,
( ~ hskp12
| ~ hskp16
| ~ hskp19 ),
inference(backward_subsumption_resolution,[status(thm)],[f1925,f17412]) ).
fof(f17432,plain,
( ~ hskp16
| hskp18
| ~ hskp12
| ~ hskp16 ),
inference(resolution,[status(thm)],[f17422,f662]) ).
fof(f17436,plain,
( hskp18
| ~ hskp12
| ~ hskp16 ),
inference(duplicate_literals_removal,[status(thm)],[f17432]) ).
fof(f17437,plain,
( ~ hskp12
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f17436,f4925]) ).
fof(f17745,plain,
! [X0] :
( ~ hskp11
| ~ c3_1(a479)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4356,f285]) ).
fof(f17751,plain,
( ~ hskp15
| ~ hskp11
| ~ c3_1(a479)
| ~ c1_1(a484)
| ~ c0_1(a484) ),
inference(resolution,[status(thm)],[f17745,f280]) ).
fof(f17756,plain,
( ~ hskp29
| ~ hskp11
| ~ c3_1(a479)
| ~ c1_1(a474)
| ~ c0_1(a474) ),
inference(resolution,[status(thm)],[f17745,f260]) ).
fof(f17845,plain,
( ~ hskp15
| ~ hskp11
| ~ c3_1(a479)
| ~ c1_1(a484) ),
inference(forward_subsumption_resolution,[status(thm)],[f17751,f279]) ).
fof(f17848,plain,
( ~ hskp29
| ~ hskp11
| ~ c3_1(a479)
| ~ c1_1(a474) ),
inference(forward_subsumption_resolution,[status(thm)],[f17756,f258]) ).
fof(f17901,plain,
( ~ hskp16
| ~ hskp19 ),
inference(backward_subsumption_resolution,[status(thm)],[f1369,f17902]) ).
fof(f17902,plain,
( ~ hskp16
| ~ c3_1(a487) ),
inference(forward_subsumption_resolution,[status(thm)],[f15769,f17437]) ).
fof(f17953,plain,
( ~ hskp16
| hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f662,f17901]) ).
fof(f17976,plain,
( ~ hskp16
| ~ hskp3
| ~ c2_1(a465) ),
inference(backward_subsumption_resolution,[status(thm)],[f5730,f17953]) ).
fof(f17981,plain,
! [X0] :
( ~ hskp13
| ~ c3_1(a482)
| ~ c0_1(a482)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4357,f227]) ).
fof(f17989,plain,
( ~ hskp20
| ~ hskp13
| ~ c3_1(a482)
| ~ c0_1(a482)
| ~ c1_1(a506) ),
inference(resolution,[status(thm)],[f17981,f273]) ).
fof(f17992,plain,
( ~ hskp29
| ~ hskp13
| ~ c3_1(a482)
| ~ c0_1(a482)
| ~ c1_1(a474) ),
inference(resolution,[status(thm)],[f17981,f260]) ).
fof(f18081,plain,
( ~ hskp20
| ~ hskp13
| ~ c3_1(a482)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f17989,f272]) ).
fof(f18083,plain,
( ~ hskp29
| ~ hskp13
| ~ c3_1(a482)
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f17992,f259]) ).
fof(f21163,plain,
( ~ hskp30
| ~ hskp25
| ~ c3_1(a488)
| ~ c1_1(a488) ),
inference(resolution,[status(thm)],[f15629,f256]) ).
fof(f21253,plain,
( ~ hskp30
| ~ hskp25
| ~ c3_1(a488) ),
inference(forward_subsumption_resolution,[status(thm)],[f21163,f255]) ).
fof(f21402,plain,
( ~ hskp30
| ~ hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f21253,f257]) ).
fof(f21404,plain,
! [X0] :
( hskp14
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f21402,f405]) ).
fof(f21405,plain,
( hskp14
| hskp0
| ~ hskp30 ),
inference(resolution,[status(thm)],[f21402,f247]) ).
fof(f21407,plain,
! [X0] :
( hskp14
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f21404,f210]) ).
fof(f21488,plain,
( ~ hskp30
| ~ hskp22
| ~ c3_1(a519)
| ~ c3_1(a488)
| ~ c1_1(a488) ),
inference(resolution,[status(thm)],[f15525,f256]) ).
fof(f21579,plain,
( ~ hskp30
| ~ hskp22
| ~ c3_1(a519)
| ~ c3_1(a488) ),
inference(forward_subsumption_resolution,[status(thm)],[f21488,f255]) ).
fof(f21634,plain,
( ~ hskp17
| ~ hskp17
| ~ c1_1(a493)
| ~ c3_1(a493)
| ~ c1_1(a493) ),
inference(resolution,[status(thm)],[f15526,f276]) ).
fof(f21727,plain,
( ~ hskp17
| ~ c3_1(a493)
| ~ c1_1(a493) ),
inference(duplicate_literals_removal,[status(thm)],[f21634]) ).
fof(f21728,plain,
( ~ hskp17
| ~ c1_1(a493) ),
inference(forward_subsumption_resolution,[status(thm)],[f21727,f277]) ).
fof(f21795,plain,
( ~ hskp14
| ~ hskp14
| ~ c3_1(a483)
| ~ c3_1(a483)
| ~ c1_1(a483) ),
inference(resolution,[status(thm)],[f15527,f282]) ).
fof(f21889,plain,
( ~ hskp14
| ~ c3_1(a483)
| ~ c1_1(a483) ),
inference(duplicate_literals_removal,[status(thm)],[f21795]) ).
fof(f21890,plain,
( ~ hskp14
| ~ c3_1(a483) ),
inference(forward_subsumption_resolution,[status(thm)],[f21889,f281]) ).
fof(f22001,plain,
( hskp1
| hskp15
| c0_1(a483)
| ~ ndr1_0
| ~ c2_1(a483)
| ~ hskp14 ),
inference(resolution,[status(thm)],[f21890,f359]) ).
fof(f22011,plain,
( hskp1
| hskp15
| c0_1(a483)
| ~ ndr1_0
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f22001,f282]) ).
fof(f22292,plain,
( ~ hskp16
| ~ hskp3
| ~ hskp16
| c0_1(a465)
| ~ c3_1(a465) ),
inference(resolution,[status(thm)],[f15724,f17976]) ).
fof(f22351,plain,
( ~ hskp3
| ~ hskp16
| c0_1(a465)
| ~ c3_1(a465) ),
inference(duplicate_literals_removal,[status(thm)],[f22292]) ).
fof(f22352,plain,
( ~ hskp3
| ~ hskp16
| c0_1(a465) ),
inference(forward_subsumption_resolution,[status(thm)],[f22351,f295]) ).
fof(f22367,plain,
( ~ hskp3
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f22352,f341]) ).
fof(f22368,plain,
( hskp12
| hskp29
| ~ hskp16 ),
inference(resolution,[status(thm)],[f22367,f242]) ).
fof(f22369,plain,
( hskp12
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f22368,f15631]) ).
fof(f22373,plain,
( ~ hskp18
| c1_1(a494) ),
inference(backward_subsumption_resolution,[status(thm)],[f1211,f22392]) ).
fof(f22380,plain,
! [X0] :
( ~ hskp5
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| c1_1(a467) ),
inference(backward_subsumption_resolution,[status(thm)],[f1155,f22392]) ).
fof(f22383,plain,
! [X0] :
( hskp7
| c3_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f361,f22392]) ).
fof(f22384,plain,
( hskp13
| hskp26 ),
inference(backward_subsumption_resolution,[status(thm)],[f244,f22392]) ).
fof(f22385,plain,
( ~ hskp13
| ~ c0_1(a482)
| ~ hskp18 ),
inference(backward_subsumption_resolution,[status(thm)],[f11999,f22392]) ).
fof(f22387,plain,
( ~ hskp27
| ~ c0_1(a576) ),
inference(backward_subsumption_resolution,[status(thm)],[f2805,f22392]) ).
fof(f22391,plain,
( ~ hskp10
| hskp7 ),
inference(backward_subsumption_resolution,[status(thm)],[f657,f22392]) ).
fof(f22392,plain,
~ hskp16,
inference(forward_subsumption_resolution,[status(thm)],[f22369,f17437]) ).
fof(f22393,plain,
! [X0] :
( ~ hskp5
| c3_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f22380,f336]) ).
fof(f22409,plain,
( ~ hskp18
| hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f7104,f22373]) ).
fof(f22410,plain,
( ~ hskp18
| hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f7083,f22373]) ).
fof(f22441,plain,
( ~ hskp27
| hskp8
| hskp7 ),
inference(backward_subsumption_resolution,[status(thm)],[f555,f22387]) ).
fof(f22456,plain,
( hskp8
| hskp7 ),
inference(forward_subsumption_resolution,[status(thm)],[f22441,f249]) ).
fof(f22492,plain,
! [X0] :
( hskp17
| hskp7
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f381,f22383]) ).
fof(f22494,plain,
( ~ hskp14
| hskp7
| c0_1(a483)
| ~ ndr1_0
| ~ c2_1(a483) ),
inference(resolution,[status(thm)],[f22383,f21890]) ).
fof(f22512,plain,
( ~ hskp14
| hskp7
| c0_1(a483)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f22494,f282]) ).
fof(f22668,plain,
( ~ hskp13
| hskp19
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f711,f22385]) ).
fof(f22852,plain,
! [X0] :
( ~ hskp2
| hskp28
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15873,f296]) ).
fof(f22855,plain,
( ~ hskp14
| hskp7
| c0_1(a483) ),
inference(forward_subsumption_resolution,[status(thm)],[f22512,f226]) ).
fof(f22856,plain,
( ~ hskp14
| ~ hskp14
| hskp7 ),
inference(resolution,[status(thm)],[f22855,f322]) ).
fof(f22857,plain,
( ~ hskp14
| hskp7 ),
inference(duplicate_literals_removal,[status(thm)],[f22856]) ).
fof(f22859,plain,
! [X0] :
( ~ hskp17
| hskp28
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f15875,f277]) ).
fof(f23270,plain,
( ~ hskp15
| ~ hskp11
| ~ c1_1(a484) ),
inference(forward_subsumption_resolution,[status(thm)],[f17845,f286]) ).
fof(f23275,plain,
( ~ hskp15
| hskp1
| hskp18
| ~ hskp15
| ~ hskp11 ),
inference(resolution,[status(thm)],[f23270,f707]) ).
fof(f23295,plain,
( hskp1
| hskp18
| ~ hskp15
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f23275]) ).
fof(f23420,plain,
( ~ hskp29
| ~ hskp11
| ~ c3_1(a479) ),
inference(forward_subsumption_resolution,[status(thm)],[f17848,f259]) ).
fof(f23421,plain,
( ~ hskp11
| ~ hskp29
| ~ hskp11 ),
inference(resolution,[status(thm)],[f23420,f286]) ).
fof(f23454,plain,
( ~ hskp29
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f23421]) ).
fof(f24005,plain,
( hskp22
| ~ hskp12
| ~ hskp13
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f2617,f24006]) ).
fof(f24006,plain,
( ~ hskp20
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f18081,f283]) ).
fof(f24211,plain,
( ~ hskp22
| ~ hskp13
| ~ c3_1(a519)
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f3055,f24215]) ).
fof(f24212,plain,
( ~ hskp6
| ~ hskp13
| ~ c3_1(a470)
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f3053,f24215]) ).
fof(f24215,plain,
( ~ hskp29
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f18083,f283]) ).
fof(f24216,plain,
! [X0] :
( ~ hskp13
| hskp11
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ hskp29
| ~ hskp13 ),
inference(resolution,[status(thm)],[f24215,f5018]) ).
fof(f24242,plain,
! [X0] :
( hskp11
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ hskp29
| ~ hskp13 ),
inference(duplicate_literals_removal,[status(thm)],[f24216]) ).
fof(f24243,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ hskp29
| ~ hskp13 ),
inference(forward_subsumption_resolution,[status(thm)],[f24242,f23454]) ).
fof(f24661,plain,
( ~ hskp30
| ~ hskp22
| ~ c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f21579,f257]) ).
fof(f24662,plain,
( ~ hskp22
| hskp6
| ~ hskp30
| ~ hskp22 ),
inference(resolution,[status(thm)],[f24661,f2002]) ).
fof(f24700,plain,
( hskp6
| ~ hskp30
| ~ hskp22 ),
inference(duplicate_literals_removal,[status(thm)],[f24662]) ).
fof(f24715,plain,
( hskp1
| hskp15
| c0_1(a483)
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f22011,f226]) ).
fof(f24716,plain,
( ~ hskp14
| hskp1
| hskp15
| ~ hskp14 ),
inference(resolution,[status(thm)],[f24715,f322]) ).
fof(f24717,plain,
( hskp1
| hskp15
| ~ hskp14 ),
inference(duplicate_literals_removal,[status(thm)],[f24716]) ).
fof(f24911,plain,
( ~ hskp22
| hskp6
| ~ hskp22
| ~ hskp13
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f24211,f2002]) ).
fof(f24949,plain,
( hskp6
| ~ hskp22
| ~ hskp13
| ~ c0_1(a482) ),
inference(duplicate_literals_removal,[status(thm)],[f24911]) ).
fof(f24983,plain,
( ~ hskp6
| ~ hskp19
| hskp14
| ~ hskp6
| ~ hskp13
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f24212,f1284]) ).
fof(f25033,plain,
( ~ hskp19
| hskp14
| ~ hskp6
| ~ hskp13
| ~ c0_1(a482) ),
inference(duplicate_literals_removal,[status(thm)],[f24983]) ).
fof(f25034,plain,
( ~ hskp19
| ~ hskp6
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f25033,f2428]) ).
fof(f25163,plain,
( ~ hskp22
| ~ hskp13
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f24949,f25164]) ).
fof(f25164,plain,
( ~ hskp6
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f25034,f22668]) ).
fof(f25277,plain,
( ~ hskp12
| ~ hskp13
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f24005,f25163]) ).
fof(f25324,plain,
( ~ hskp5
| ~ hskp13
| ~ c2_1(a467)
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f5886,f25277]) ).
fof(f25902,plain,
( ~ hskp5
| c3_1(a467)
| c1_1(a467)
| ~ hskp5
| ~ hskp13
| ~ c0_1(a482) ),
inference(resolution,[status(thm)],[f25324,f22393]) ).
fof(f25979,plain,
( c3_1(a467)
| c1_1(a467)
| ~ hskp5
| ~ hskp13
| ~ c0_1(a482) ),
inference(duplicate_literals_removal,[status(thm)],[f25902]) ).
fof(f25980,plain,
( c3_1(a467)
| ~ hskp5
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f25979,f336]) ).
fof(f26107,plain,
( ~ hskp13
| hskp17
| ~ c0_1(a482) ),
inference(backward_subsumption_resolution,[status(thm)],[f971,f26108]) ).
fof(f26108,plain,
( ~ hskp5
| ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f25980,f337]) ).
fof(f26530,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c0_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f7400,f22373]) ).
fof(f26744,plain,
( ~ hskp30
| ~ c3_1(a488)
| ~ c1_1(a488)
| ~ hskp29
| ~ hskp13 ),
inference(resolution,[status(thm)],[f24243,f256]) ).
fof(f26829,plain,
( ~ hskp30
| ~ c3_1(a488)
| ~ hskp29
| ~ hskp13 ),
inference(forward_subsumption_resolution,[status(thm)],[f26744,f255]) ).
fof(f26941,plain,
( ~ hskp30
| ~ hskp29
| ~ hskp13 ),
inference(forward_subsumption_resolution,[status(thm)],[f26829,f257]) ).
fof(f27783,plain,
! [X0] :
( ~ hskp22
| hskp5
| c1_1(X0)
| c0_1(X0)
| c3_1(a519) ),
inference(backward_subsumption_resolution,[status(thm)],[f1887,f27784]) ).
fof(f27784,plain,
! [X0] :
( ~ hskp22
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f7507,f309]) ).
fof(f27795,plain,
! [X0] :
( ~ hskp30
| ~ hskp22
| ~ hskp22
| hskp5
| c1_1(X0)
| c0_1(X0) ),
inference(resolution,[status(thm)],[f27783,f24661]) ).
fof(f27802,plain,
! [X0] :
( ~ hskp30
| ~ hskp22
| hskp5
| c1_1(X0)
| c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f27795]) ).
fof(f27871,plain,
( ~ hskp6
| ~ hskp30
| ~ hskp22
| hskp5
| c0_1(a470) ),
inference(resolution,[status(thm)],[f27802,f334]) ).
fof(f27884,plain,
( ~ hskp6
| ~ hskp30
| ~ hskp22
| hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f27871,f333]) ).
fof(f27887,plain,
( ~ hskp30
| ~ hskp22
| hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f27884,f24700]) ).
fof(f29228,plain,
! [X0] :
( ~ hskp22
| ~ hskp12
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| c0_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f8174,f325]) ).
fof(f29247,plain,
( ~ hskp22
| ~ hskp22
| ~ hskp12
| c3_1(a519)
| c0_1(a519)
| c0_1(a519) ),
inference(resolution,[status(thm)],[f29228,f310]) ).
fof(f29293,plain,
( ~ hskp22
| ~ hskp12
| c3_1(a519)
| c0_1(a519) ),
inference(duplicate_literals_removal,[status(thm)],[f29247]) ).
fof(f29294,plain,
( ~ hskp22
| ~ hskp12
| c3_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f29293,f309]) ).
fof(f29296,plain,
( ~ hskp12
| ~ hskp22
| hskp14
| ~ c2_1(a481) ),
inference(backward_subsumption_resolution,[status(thm)],[f3974,f29294]) ).
fof(f29786,plain,
( ~ hskp19
| ~ hskp19
| c3_1(a500)
| c0_1(a500)
| c0_1(a500) ),
inference(resolution,[status(thm)],[f8214,f314]) ).
fof(f29832,plain,
( ~ hskp19
| c3_1(a500)
| c0_1(a500) ),
inference(duplicate_literals_removal,[status(thm)],[f29786]) ).
fof(f29833,plain,
( ~ hskp19
| c0_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f29832,f315]) ).
fof(f29845,plain,
( ~ hskp19
| ~ hskp20
| hskp29 ),
inference(backward_subsumption_resolution,[status(thm)],[f10743,f29833]) ).
fof(f29859,plain,
( ~ hskp29
| ~ hskp19 ),
inference(backward_subsumption_resolution,[status(thm)],[f6008,f29833]) ).
fof(f29869,plain,
( ~ hskp19
| hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f816,f29870]) ).
fof(f29870,plain,
( ~ hskp19
| ~ hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f29845,f29859]) ).
fof(f29877,plain,
( ~ hskp19
| hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f1918,f29869]) ).
fof(f31871,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a494) ),
inference(forward_subsumption_resolution,[status(thm)],[f8427,f26530]) ).
fof(f31872,plain,
! [X0] :
( ~ hskp18
| ~ hskp22
| ~ hskp18
| c1_1(X0)
| c0_1(X0)
| c0_1(a519) ),
inference(resolution,[status(thm)],[f31871,f317]) ).
fof(f31877,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c1_1(X0)
| c0_1(X0)
| c0_1(a519) ),
inference(duplicate_literals_removal,[status(thm)],[f31872]) ).
fof(f31878,plain,
! [X0] :
( ~ hskp22
| ~ hskp18
| c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f31877,f309]) ).
fof(f31959,plain,
! [X0] :
( ~ hskp18
| c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f31878,f22410]) ).
fof(f31988,plain,
( ~ hskp6
| ~ hskp18
| c0_1(a470) ),
inference(resolution,[status(thm)],[f31959,f334]) ).
fof(f32005,plain,
( ~ hskp6
| ~ hskp18 ),
inference(forward_subsumption_resolution,[status(thm)],[f31988,f333]) ).
fof(f32125,plain,
( hskp1
| ~ hskp15
| ~ hskp11 ),
inference(backward_subsumption_resolution,[status(thm)],[f23295,f32132]) ).
fof(f32128,plain,
( ~ hskp5
| hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f706,f32132]) ).
fof(f32129,plain,
! [X0] :
( hskp1
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f367,f32132]) ).
fof(f32130,plain,
( ~ hskp7
| hskp19
| c1_1(a471) ),
inference(backward_subsumption_resolution,[status(thm)],[f659,f32132]) ).
fof(f32131,plain,
! [X0] :
( hskp19
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f363,f32132]) ).
fof(f32132,plain,
~ hskp18,
inference(forward_subsumption_resolution,[status(thm)],[f32005,f22409]) ).
fof(f32360,plain,
! [X0] :
( ~ hskp22
| ~ hskp19
| c1_1(X0)
| c0_1(X0)
| c0_1(a519)
| c3_1(a500) ),
inference(forward_subsumption_resolution,[status(thm)],[f8467,f29833]) ).
fof(f32361,plain,
! [X0] :
( ~ hskp19
| ~ hskp22
| ~ hskp19
| c1_1(X0)
| c0_1(X0)
| c0_1(a519) ),
inference(resolution,[status(thm)],[f32360,f315]) ).
fof(f32366,plain,
! [X0] :
( ~ hskp22
| ~ hskp19
| c1_1(X0)
| c0_1(X0)
| c0_1(a519) ),
inference(duplicate_literals_removal,[status(thm)],[f32361]) ).
fof(f32367,plain,
! [X0] :
( ~ hskp22
| ~ hskp19
| c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f32366,f309]) ).
fof(f32370,plain,
! [X0] :
( ~ hskp19
| c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f32367,f29869]) ).
fof(f32386,plain,
( ~ hskp17
| ~ hskp19
| c0_1(a493) ),
inference(resolution,[status(thm)],[f32370,f21728]) ).
fof(f32395,plain,
( ~ hskp6
| ~ hskp19
| c0_1(a470) ),
inference(resolution,[status(thm)],[f32370,f334]) ).
fof(f32405,plain,
( ~ hskp17
| ~ hskp19 ),
inference(forward_subsumption_resolution,[status(thm)],[f32386,f318]) ).
fof(f32411,plain,
( ~ hskp6
| ~ hskp19 ),
inference(forward_subsumption_resolution,[status(thm)],[f32395,f333]) ).
fof(f32417,plain,
( ~ hskp13
| ~ c0_1(a482)
| ~ hskp17 ),
inference(resolution,[status(thm)],[f32405,f22668]) ).
fof(f32419,plain,
( ~ hskp13
| ~ c0_1(a482) ),
inference(forward_subsumption_resolution,[status(thm)],[f32417,f26107]) ).
fof(f32426,plain,
( ~ hskp7
| c1_1(a471) ),
inference(backward_subsumption_resolution,[status(thm)],[f32130,f32430]) ).
fof(f32427,plain,
! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f32131,f32430]) ).
fof(f32430,plain,
~ hskp19,
inference(forward_subsumption_resolution,[status(thm)],[f32411,f29877]) ).
fof(f32437,plain,
! [X0,X1] :
( hskp29
| c2_1(X1)
| c3_1(X0)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f455,f32427]) ).
fof(f32438,plain,
! [X0] :
( ~ hskp7
| hskp12
| c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f5303,f32427]) ).
fof(f32440,plain,
! [X0,X1] :
( hskp13
| c3_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f437,f32427]) ).
fof(f32485,plain,
! [X0] :
( ~ hskp7
| hskp12
| c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f32438,f233]) ).
fof(f32497,plain,
! [X0] :
( ~ hskp13
| hskp11
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5018,f32419]) ).
fof(f32500,plain,
( ~ hskp13
| ~ hskp8
| hskp10 ),
inference(backward_subsumption_resolution,[status(thm)],[f3786,f32419]) ).
fof(f32501,plain,
( ~ hskp13
| ~ hskp7
| hskp10
| ~ c1_1(a471) ),
inference(backward_subsumption_resolution,[status(thm)],[f3712,f32419]) ).
fof(f32772,plain,
! [X0] :
( ~ hskp12
| hskp29
| c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a481)
| ~ c1_1(a481) ),
inference(resolution,[status(thm)],[f32437,f326]) ).
fof(f32784,plain,
! [X0] :
( ~ hskp12
| hskp29
| c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f32772,f284]) ).
fof(f33017,plain,
( ~ hskp0
| ~ hskp7
| hskp12
| ~ c0_1(a462) ),
inference(resolution,[status(thm)],[f32485,f347]) ).
fof(f33033,plain,
( ~ hskp0
| ~ hskp7
| hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f33017,f298]) ).
fof(f33055,plain,
! [X0] :
( ~ hskp5
| hskp13
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c0_1(a467) ),
inference(resolution,[status(thm)],[f32440,f336]) ).
fof(f33067,plain,
! [X0] :
( ~ hskp5
| hskp13
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f33055,f294]) ).
fof(f33069,plain,
( ~ hskp13
| ~ hskp7
| hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f32501,f32426]) ).
fof(f33552,plain,
! [X0] :
( ~ hskp12
| hskp29
| c2_1(X0)
| ~ c0_1(X0)
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f32784,f228]) ).
fof(f33561,plain,
( ~ hskp7
| ~ hskp12
| hskp29
| ~ c0_1(a471)
| ~ c2_1(a481) ),
inference(resolution,[status(thm)],[f33552,f332]) ).
fof(f33596,plain,
( ~ hskp7
| ~ hskp12
| hskp29
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f33561,f292]) ).
fof(f33696,plain,
( ~ hskp12
| hskp29
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f33596,f1338]) ).
fof(f33838,plain,
! [X0] :
( ~ hskp5
| hskp13
| c3_1(X0)
| c0_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f33067,f235]) ).
fof(f33841,plain,
( ~ hskp30
| ~ hskp22
| ~ hskp5
| hskp13
| c0_1(a519)
| ~ c1_1(a519) ),
inference(resolution,[status(thm)],[f33838,f24661]) ).
fof(f33868,plain,
( ~ hskp30
| ~ hskp22
| ~ hskp5
| hskp13
| c0_1(a519) ),
inference(forward_subsumption_resolution,[status(thm)],[f33841,f270]) ).
fof(f33968,plain,
( ~ hskp30
| ~ hskp22
| ~ hskp5
| hskp13 ),
inference(forward_subsumption_resolution,[status(thm)],[f33868,f309]) ).
fof(f33969,plain,
( ~ hskp30
| ~ hskp29
| ~ hskp30
| ~ hskp22
| ~ hskp5 ),
inference(resolution,[status(thm)],[f33968,f26941]) ).
fof(f33970,plain,
( ~ hskp29
| ~ hskp30
| ~ hskp22
| ~ hskp5 ),
inference(duplicate_literals_removal,[status(thm)],[f33969]) ).
fof(f33971,plain,
( ~ hskp29
| ~ hskp30
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f33970,f27887]) ).
fof(f33972,plain,
( hskp13
| hskp1
| ~ hskp29
| ~ hskp30 ),
inference(resolution,[status(thm)],[f33971,f251]) ).
fof(f33973,plain,
( hskp1
| ~ hskp29
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f33972,f26941]) ).
fof(f34605,plain,
! [X0] :
( ~ hskp1
| ~ hskp7
| c3_1(X0)
| c0_1(X0)
| c1_1(a463)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9598,f32426]) ).
fof(f34621,plain,
( ~ hskp14
| ~ hskp1
| ~ hskp7
| c0_1(a483)
| c1_1(a463)
| ~ c1_1(a483) ),
inference(resolution,[status(thm)],[f34605,f21890]) ).
fof(f34626,plain,
( ~ hskp12
| ~ hskp1
| ~ hskp7
| c0_1(a481)
| c1_1(a463)
| ~ c1_1(a481) ),
inference(resolution,[status(thm)],[f34605,f326]) ).
fof(f34639,plain,
( ~ hskp14
| ~ hskp1
| ~ hskp7
| c0_1(a483)
| c1_1(a463) ),
inference(forward_subsumption_resolution,[status(thm)],[f34621,f281]) ).
fof(f34641,plain,
( ~ hskp12
| ~ hskp1
| ~ hskp7
| c0_1(a481)
| c1_1(a463) ),
inference(forward_subsumption_resolution,[status(thm)],[f34626,f284]) ).
fof(f36941,plain,
( ~ hskp14
| ~ hskp1
| ~ hskp7
| c0_1(a483) ),
inference(forward_subsumption_resolution,[status(thm)],[f34639,f345]) ).
fof(f36942,plain,
( ~ hskp14
| ~ hskp14
| ~ hskp1
| ~ hskp7 ),
inference(resolution,[status(thm)],[f36941,f322]) ).
fof(f36943,plain,
( ~ hskp14
| ~ hskp1
| ~ hskp7 ),
inference(duplicate_literals_removal,[status(thm)],[f36942]) ).
fof(f36944,plain,
( ~ hskp14
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f36943,f22857]) ).
fof(f36945,plain,
( hskp15
| ~ hskp14 ),
inference(backward_subsumption_resolution,[status(thm)],[f24717,f36944]) ).
fof(f36946,plain,
( ~ hskp14
| hskp30
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f859,f36944]) ).
fof(f36954,plain,
( ~ hskp29
| ~ hskp30
| ~ hskp14 ),
inference(resolution,[status(thm)],[f36944,f33973]) ).
fof(f36958,plain,
( ~ hskp15
| ~ hskp11
| ~ hskp14 ),
inference(resolution,[status(thm)],[f36944,f32125]) ).
fof(f36959,plain,
( ~ hskp5
| ~ hskp14 ),
inference(resolution,[status(thm)],[f36944,f32128]) ).
fof(f36963,plain,
( ~ hskp14
| hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f36946,f226]) ).
fof(f36979,plain,
( ~ hskp10
| ~ hskp22
| ~ c3_1(a519)
| ~ hskp5 ),
inference(resolution,[status(thm)],[f36959,f3999]) ).
fof(f36984,plain,
( ~ hskp22
| ~ c3_1(a519)
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f36979,f3770]) ).
fof(f36993,plain,
( ~ hskp29
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f36954,f36963]) ).
fof(f36994,plain,
( ~ hskp12
| ~ hskp22
| ~ c2_1(a481)
| ~ hskp29 ),
inference(resolution,[status(thm)],[f36993,f29296]) ).
fof(f37005,plain,
( ~ hskp12
| ~ hskp22
| ~ c2_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f36994,f33696]) ).
fof(f37011,plain,
( ~ hskp11
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f36958,f36945]) ).
fof(f37012,plain,
! [X0] :
( ~ hskp13
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ hskp14 ),
inference(resolution,[status(thm)],[f37011,f32497]) ).
fof(f37176,plain,
( ~ hskp22
| hskp12
| ~ c3_1(a519) ),
inference(backward_subsumption_resolution,[status(thm)],[f665,f36984]) ).
fof(f37209,plain,
( ~ hskp5
| hskp13
| c0_1(a519)
| ~ c1_1(a519)
| ~ hskp22
| ~ hskp5 ),
inference(resolution,[status(thm)],[f36984,f33838]) ).
fof(f37268,plain,
( hskp13
| c0_1(a519)
| ~ c1_1(a519)
| ~ hskp22
| ~ hskp5 ),
inference(duplicate_literals_removal,[status(thm)],[f37209]) ).
fof(f37269,plain,
( hskp13
| c0_1(a519)
| ~ hskp22
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f37268,f270]) ).
fof(f37320,plain,
( ~ hskp22
| ~ hskp12
| c3_1(a481)
| c0_1(a481)
| c0_1(a519)
| ~ hskp12
| ~ hskp22 ),
inference(resolution,[status(thm)],[f37005,f29228]) ).
fof(f37371,plain,
( c3_1(a481)
| c0_1(a481)
| c0_1(a519)
| ~ hskp12
| ~ hskp22 ),
inference(duplicate_literals_removal,[status(thm)],[f37320]) ).
fof(f37372,plain,
( c3_1(a481)
| c0_1(a481)
| ~ hskp12
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f37371,f309]) ).
fof(f38092,plain,
( hskp13
| ~ hskp22
| ~ hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f37269,f309]) ).
fof(f38590,plain,
( c3_1(a481)
| ~ hskp12
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f37372,f325]) ).
fof(f38591,plain,
( ~ hskp12
| ~ hskp12
| ~ hskp22 ),
inference(resolution,[status(thm)],[f38590,f326]) ).
fof(f38596,plain,
( ~ hskp12
| ~ hskp22 ),
inference(duplicate_literals_removal,[status(thm)],[f38591]) ).
fof(f38597,plain,
( ~ hskp22
| ~ c3_1(a519) ),
inference(backward_subsumption_resolution,[status(thm)],[f37176,f38596]) ).
fof(f38605,plain,
! [X0] :
( ~ hskp22
| hskp5
| c1_1(X0)
| c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f27783,f38597]) ).
fof(f38607,plain,
( ~ hskp22
| hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f2002,f38597]) ).
fof(f38763,plain,
( ~ hskp6
| ~ hskp22
| hskp5
| c0_1(a470) ),
inference(resolution,[status(thm)],[f38605,f334]) ).
fof(f38778,plain,
( ~ hskp6
| ~ hskp22
| hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f38763,f333]) ).
fof(f38782,plain,
( hskp13
| ~ hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f38092,f38783]) ).
fof(f38783,plain,
( ~ hskp22
| hskp5 ),
inference(forward_subsumption_resolution,[status(thm)],[f38778,f38607]) ).
fof(f38784,plain,
( hskp13
| hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f251,f38782]) ).
fof(f39546,plain,
( ~ hskp30
| ~ hskp13
| ~ c3_1(a488)
| ~ c1_1(a488)
| ~ hskp14 ),
inference(resolution,[status(thm)],[f37012,f256]) ).
fof(f39607,plain,
( ~ hskp30
| ~ hskp13
| ~ c3_1(a488)
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f39546,f255]) ).
fof(f39650,plain,
( ~ hskp30
| ~ hskp13
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f39607,f257]) ).
fof(f39653,plain,
( hskp1
| ~ hskp30
| ~ hskp14 ),
inference(resolution,[status(thm)],[f39650,f38784]) ).
fof(f39670,plain,
( hskp1
| ~ hskp14 ),
inference(forward_subsumption_resolution,[status(thm)],[f39653,f36963]) ).
fof(f39681,plain,
( hskp0
| ~ hskp30 ),
inference(backward_subsumption_resolution,[status(thm)],[f21405,f39699]) ).
fof(f39692,plain,
! [X0] :
( hskp25
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f405,f39699]) ).
fof(f39694,plain,
( hskp25
| hskp0 ),
inference(backward_subsumption_resolution,[status(thm)],[f247,f39699]) ).
fof(f39695,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(backward_subsumption_resolution,[status(thm)],[f21407,f39699]) ).
fof(f39696,plain,
( ~ hskp10
| ~ hskp25 ),
inference(backward_subsumption_resolution,[status(thm)],[f4005,f39699]) ).
fof(f39699,plain,
~ hskp14,
inference(forward_subsumption_resolution,[status(thm)],[f39670,f36944]) ).
fof(f39702,plain,
( hskp10
| hskp0 ),
inference(backward_subsumption_resolution,[status(thm)],[f246,f39681]) ).
fof(f39712,plain,
( hskp0
| ~ hskp10 ),
inference(resolution,[status(thm)],[f39696,f39694]) ).
fof(f39730,plain,
( ~ hskp7
| hskp12 ),
inference(backward_subsumption_resolution,[status(thm)],[f33033,f39752]) ).
fof(f39741,plain,
( ~ hskp12
| hskp13 ),
inference(backward_subsumption_resolution,[status(thm)],[f3876,f39752]) ).
fof(f39748,plain,
~ c1_1(a462),
inference(backward_subsumption_resolution,[status(thm)],[f347,f39752]) ).
fof(f39749,plain,
c2_1(a462),
inference(backward_subsumption_resolution,[status(thm)],[f299,f39752]) ).
fof(f39750,plain,
c0_1(a462),
inference(backward_subsumption_resolution,[status(thm)],[f298,f39752]) ).
fof(f39751,plain,
ndr1_0,
inference(backward_subsumption_resolution,[status(thm)],[f240,f39752]) ).
fof(f39752,plain,
hskp0,
inference(forward_subsumption_resolution,[status(thm)],[f39712,f39702]) ).
fof(f39776,plain,
! [X0] :
( c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f32427,f39751]) ).
fof(f39778,plain,
! [X0] :
( hskp1
| c3_1(X0)
| c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f32129,f39751]) ).
fof(f39783,plain,
! [X0] :
( hskp17
| hskp7
| c0_1(X0)
| ~ c2_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f22492,f39751]) ).
fof(f39820,plain,
( ~ hskp26
| hskp12
| hskp30 ),
inference(backward_subsumption_resolution,[status(thm)],[f1000,f39751]) ).
fof(f39826,plain,
! [X0] :
( hskp17
| hskp5
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f387,f39751]) ).
fof(f39944,plain,
! [X0] :
( hskp25
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f39692,f39751]) ).
fof(f39945,plain,
! [X0] :
( ~ hskp10
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f39944,f39696]) ).
fof(f41209,plain,
( ~ hskp28
| ~ c3_1(a469)
| ~ c0_1(a469)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f39695,f262]) ).
fof(f41211,plain,
( ~ hskp30
| ~ c3_1(a488)
| ~ c0_1(a488)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f39695,f256]) ).
fof(f41214,plain,
! [X0] :
( c1_1(X0)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f39695,f39776]) ).
fof(f41242,plain,
( ~ hskp28
| ~ c3_1(a469)
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f41209,f261]) ).
fof(f41243,plain,
( ~ c3_1(a488)
| ~ c0_1(a488)
| ~ hskp30 ),
inference(duplicate_literals_removal,[status(thm)],[f41211]) ).
fof(f41244,plain,
( ~ c0_1(a488)
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f41243,f257]) ).
fof(f41245,plain,
! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(duplicate_literals_removal,[status(thm)],[f41214]) ).
fof(f41288,plain,
( hskp17
| hskp7
| ~ c2_1(a488)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f41244,f39783]) ).
fof(f41294,plain,
( hskp17
| hskp7
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f41288,f256]) ).
fof(f41312,plain,
( ~ hskp28
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f41242,f263]) ).
fof(f41314,plain,
! [X0] :
( ~ hskp17
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f41312,f22859]) ).
fof(f41315,plain,
! [X0] :
( ~ hskp2
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f41312,f22852]) ).
fof(f41360,plain,
( ~ hskp10
| ~ c3_1(a462)
| ~ c0_1(a462) ),
inference(resolution,[status(thm)],[f39945,f39749]) ).
fof(f41399,plain,
( ~ hskp10
| ~ c3_1(a462) ),
inference(forward_subsumption_resolution,[status(thm)],[f41360,f39750]) ).
fof(f41415,plain,
( hskp1
| c1_1(a462)
| ~ c0_1(a462)
| ~ hskp10 ),
inference(resolution,[status(thm)],[f41399,f39778]) ).
fof(f41443,plain,
( hskp1
| c1_1(a462)
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f41415,f39750]) ).
fof(f41628,plain,
( hskp1
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f41443,f39748]) ).
fof(f43761,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ hskp30
| hskp17
| hskp5
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f39826,f39695]) ).
fof(f43791,plain,
! [X0] :
( ~ hskp30
| hskp17
| hskp5
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f43761]) ).
fof(f44646,plain,
( ~ hskp30
| ~ hskp17
| ~ c3_1(a488)
| ~ c1_1(a488)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f41314,f256]) ).
fof(f44696,plain,
( ~ hskp17
| ~ c3_1(a488)
| ~ c1_1(a488)
| ~ hskp30 ),
inference(duplicate_literals_removal,[status(thm)],[f44646]) ).
fof(f44697,plain,
( ~ hskp17
| ~ c3_1(a488)
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f44696,f255]) ).
fof(f44717,plain,
! [X0] :
( ~ hskp30
| hskp5
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f43791,f44720]) ).
fof(f44718,plain,
( hskp7
| ~ hskp30 ),
inference(backward_subsumption_resolution,[status(thm)],[f41294,f44720]) ).
fof(f44720,plain,
( ~ hskp17
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f44697,f257]) ).
fof(f45352,plain,
( ~ hskp30
| ~ hskp2
| ~ c3_1(a488)
| ~ c1_1(a488)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f41315,f256]) ).
fof(f45402,plain,
( ~ hskp2
| ~ c3_1(a488)
| ~ c1_1(a488)
| ~ hskp30 ),
inference(duplicate_literals_removal,[status(thm)],[f45352]) ).
fof(f45403,plain,
( ~ hskp2
| ~ c3_1(a488)
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f45402,f255]) ).
fof(f45423,plain,
( ~ hskp2
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f45403,f257]) ).
fof(f45433,plain,
! [X0] :
( ~ hskp5
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f45423,f5149]) ).
fof(f45439,plain,
! [X0] :
( ~ hskp5
| ~ c3_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f45433,f41245]) ).
fof(f45480,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0)
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f45439,f44717]) ).
fof(f45505,plain,
( ~ hskp7
| ~ c0_1(a471)
| ~ hskp30 ),
inference(resolution,[status(thm)],[f45480,f293]) ).
fof(f45562,plain,
( ~ hskp7
| ~ hskp30 ),
inference(forward_subsumption_resolution,[status(thm)],[f45505,f292]) ).
fof(f45580,plain,
( ~ hskp26
| hskp12 ),
inference(backward_subsumption_resolution,[status(thm)],[f39820,f45581]) ).
fof(f45581,plain,
~ hskp30,
inference(forward_subsumption_resolution,[status(thm)],[f45562,f44718]) ).
fof(f47179,plain,
( ~ hskp12
| ~ hskp1
| ~ hskp7
| c0_1(a481) ),
inference(forward_subsumption_resolution,[status(thm)],[f34641,f345]) ).
fof(f47180,plain,
( ~ hskp12
| ~ hskp12
| ~ hskp1
| ~ hskp7 ),
inference(resolution,[status(thm)],[f47179,f325]) ).
fof(f47181,plain,
( ~ hskp12
| ~ hskp1
| ~ hskp7 ),
inference(duplicate_literals_removal,[status(thm)],[f47180]) ).
fof(f47182,plain,
( ~ hskp1
| ~ hskp7 ),
inference(forward_subsumption_resolution,[status(thm)],[f47181,f39730]) ).
fof(f47195,plain,
( ~ hskp10
| ~ hskp7 ),
inference(resolution,[status(thm)],[f47182,f41628]) ).
fof(f47204,plain,
~ hskp10,
inference(forward_subsumption_resolution,[status(thm)],[f47195,f22391]) ).
fof(f47214,plain,
( ~ hskp13
| ~ hskp7 ),
inference(backward_subsumption_resolution,[status(thm)],[f33069,f47204]) ).
fof(f47217,plain,
( ~ hskp13
| ~ hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f32500,f47204]) ).
fof(f47489,plain,
( ~ hskp12
| ~ hskp7 ),
inference(resolution,[status(thm)],[f47214,f39741]) ).
fof(f47494,plain,
~ hskp7,
inference(forward_subsumption_resolution,[status(thm)],[f47489,f39730]) ).
fof(f47504,plain,
hskp8,
inference(backward_subsumption_resolution,[status(thm)],[f22456,f47494]) ).
fof(f47598,plain,
hskp26,
inference(backward_subsumption_resolution,[status(thm)],[f22384,f47602]) ).
fof(f47599,plain,
~ hskp12,
inference(backward_subsumption_resolution,[status(thm)],[f39741,f47602]) ).
fof(f47602,plain,
~ hskp13,
inference(forward_subsumption_resolution,[status(thm)],[f47217,f47504]) ).
fof(f47603,plain,
hskp12,
inference(backward_subsumption_resolution,[status(thm)],[f45580,f47598]) ).
fof(f47631,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f47603,f47599]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN505-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n004.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 11:04:04 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.48 % Drodi V4.1.1
% 195.85/25.25 % Refutation found
% 195.85/25.25 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 195.85/25.25 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 195.85/25.28 % Elapsed time: 24.818460 seconds
% 195.85/25.28 % CPU time: 196.248545 seconds
% 195.85/25.28 % Total memory used: 92.210 MB
% 195.85/25.28 % Net memory used: 86.052 MB
%------------------------------------------------------------------------------