%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN510-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 : n006.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:41 PM UTC 2026
% Result : Unsatisfiable 57.24s 7.83s
% Output : CNFRefutation 36.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 125
% Syntax : Number of formulae : 761 ( 20 unt; 0 def)
% Number of atoms : 3002 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 4055 (1814 ~;2241 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 27 prp; 0-1 aty)
% Number of functors : 25 ( 25 usr; 25 con; 0-0 aty)
% Number of variables : 239 ( 239 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(f8,negated_conjecture,
( ndr1_0
| ~ hskp24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
( ndr1_0
| ~ hskp23 ),
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(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(f22,negated_conjecture,
( ndr1_0
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
( ndr1_0
| ~ hskp9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
( ndr1_0
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
( ndr1_0
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
( ndr1_0
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
( ndr1_0
| ~ hskp4 ),
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(f31,negated_conjecture,
( ndr1_0
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
( hskp23
| hskp15
| hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
( hskp25
| hskp27
| hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
( hskp14
| hskp10
| hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
( hskp6
| hskp24
| hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
( hskp18
| hskp24
| hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
( c0_1(a552)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,negated_conjecture,
( c2_1(a552)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,negated_conjecture,
( c3_1(a552)
| ~ hskp29 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,negated_conjecture,
( c0_1(a541)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
( c1_1(a541)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f59,negated_conjecture,
( c2_1(a541)
| ~ hskp28 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f60,negated_conjecture,
( c0_1(a615)
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,negated_conjecture,
( c2_1(a615)
| ~ hskp27 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,negated_conjecture,
( c2_1(a594)
| ~ hskp25 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,negated_conjecture,
( c1_1(a590)
| ~ hskp24 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,negated_conjecture,
( c3_1(a584)
| ~ hskp22 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,negated_conjecture,
( c2_1(a582)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,negated_conjecture,
( c3_1(a582)
| ~ hskp21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,negated_conjecture,
( c0_1(a576)
| ~ hskp19 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,negated_conjecture,
( c1_1(a570)
| ~ hskp16 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,negated_conjecture,
( c0_1(a567)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,negated_conjecture,
( c1_1(a567)
| ~ hskp15 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,negated_conjecture,
( c2_1(a566)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,negated_conjecture,
( c3_1(a566)
| ~ hskp14 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,negated_conjecture,
( c0_1(a565)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,negated_conjecture,
( c3_1(a565)
| ~ hskp13 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,negated_conjecture,
( c0_1(a564)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,negated_conjecture,
( c3_1(a564)
| ~ hskp12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,negated_conjecture,
( c1_1(a551)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,negated_conjecture,
( c3_1(a551)
| ~ hskp10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,negated_conjecture,
( c1_1(a548)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,negated_conjecture,
( c2_1(a548)
| ~ hskp8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,negated_conjecture,
( c3_1(a546)
| ~ hskp6 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
( c0_1(a544)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
( c1_1(a544)
| ~ hskp5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f91,negated_conjecture,
( c3_1(a540)
| ~ hskp4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,negated_conjecture,
( c0_1(a539)
| ~ hskp3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,negated_conjecture,
( c2_1(a537)
| ~ hskp1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,negated_conjecture,
( c0_1(a536)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f95,negated_conjecture,
( c2_1(a536)
| ~ hskp0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
( ~ hskp27
| ~ c1_1(a615) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f98,negated_conjecture,
( ~ hskp25
| ~ c0_1(a594) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,negated_conjecture,
( ~ hskp25
| ~ c1_1(a594) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,negated_conjecture,
( ~ hskp24
| ~ c2_1(a590) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f102,negated_conjecture,
( ~ hskp23
| ~ c0_1(a587) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f103,negated_conjecture,
( ~ hskp23
| ~ c2_1(a587) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f104,negated_conjecture,
( ~ hskp23
| ~ c3_1(a587) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,negated_conjecture,
( ~ hskp22
| ~ c0_1(a584) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,negated_conjecture,
( ~ hskp22
| ~ c2_1(a584) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f107,negated_conjecture,
( ~ hskp21
| ~ c1_1(a582) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f110,negated_conjecture,
( ~ hskp19
| ~ c1_1(a576) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f111,negated_conjecture,
( ~ hskp19
| ~ c3_1(a576) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f112,negated_conjecture,
( ~ hskp18
| ~ c0_1(a573) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f113,negated_conjecture,
( ~ hskp18
| ~ c1_1(a573) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f114,negated_conjecture,
( ~ hskp18
| ~ c3_1(a573) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f117,negated_conjecture,
( ~ hskp16
| ~ c2_1(a570) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f118,negated_conjecture,
( ~ hskp16
| ~ c3_1(a570) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f119,negated_conjecture,
( ~ hskp15
| ~ c2_1(a567) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f120,negated_conjecture,
( ~ hskp14
| ~ c0_1(a566) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f121,negated_conjecture,
( ~ hskp13
| ~ c2_1(a565) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f122,negated_conjecture,
( ~ hskp12
| ~ c1_1(a564) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f124,negated_conjecture,
( ~ hskp10
| ~ c0_1(a551) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f125,negated_conjecture,
( ~ hskp9
| ~ c0_1(a549) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f126,negated_conjecture,
( ~ hskp9
| ~ c1_1(a549) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f127,negated_conjecture,
( ~ hskp9
| ~ c2_1(a549) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f128,negated_conjecture,
( ~ hskp8
| ~ c0_1(a548) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f131,negated_conjecture,
( ~ hskp6
| ~ c0_1(a546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f132,negated_conjecture,
( ~ hskp6
| ~ c1_1(a546) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,negated_conjecture,
( ~ hskp5
| ~ c3_1(a544) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,negated_conjecture,
( ~ hskp4
| ~ c1_1(a540) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f135,negated_conjecture,
( ~ hskp4
| ~ c2_1(a540) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f136,negated_conjecture,
( ~ hskp3
| ~ c2_1(a539) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f137,negated_conjecture,
( ~ hskp3
| ~ c3_1(a539) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f138,negated_conjecture,
( ~ hskp2
| ~ c1_1(a538) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f139,negated_conjecture,
( ~ hskp2
| ~ c2_1(a538) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,negated_conjecture,
( ~ hskp2
| ~ c3_1(a538) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f141,negated_conjecture,
( ~ hskp1
| ~ c1_1(a537) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,negated_conjecture,
( ~ hskp1
| ~ c3_1(a537) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,negated_conjecture,
( ~ hskp0
| ~ c3_1(a536) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f147,negated_conjecture,
! [U] :
( hskp16
| hskp3
| c3_1(U)
| c2_1(U)
| c1_1(U)
| ~ ndr1_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f148,negated_conjecture,
! [U] :
( hskp2
| hskp5
| c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,negated_conjecture,
! [U] :
( hskp10
| hskp8
| c2_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f155,negated_conjecture,
! [U] :
( hskp21
| hskp29
| c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f156,negated_conjecture,
! [U] :
( hskp22
| hskp21
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f157,negated_conjecture,
! [U] :
( hskp6
| hskp3
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f158,negated_conjecture,
! [U] :
( hskp4
| hskp25
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f159,negated_conjecture,
! [U] :
( hskp9
| hskp10
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f162,negated_conjecture,
! [U] :
( hskp0
| hskp15
| c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f163,negated_conjecture,
! [U] :
( hskp6
| hskp3
| c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f164,negated_conjecture,
! [U] :
( hskp21
| hskp12
| c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f168,negated_conjecture,
! [U] :
( hskp9
| hskp25
| c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f175,negated_conjecture,
! [U,V] :
( hskp0
| c2_1(V)
| c1_1(V)
| c0_1(V)
| c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f176,negated_conjecture,
! [U,V] :
( hskp3
| c3_1(V)
| c1_1(V)
| c0_1(V)
| c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f177,negated_conjecture,
! [U,V] :
( hskp1
| c2_1(V)
| c1_1(V)
| c0_1(V)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f178,negated_conjecture,
! [U,V] :
( hskp4
| c3_1(V)
| c1_1(V)
| c0_1(V)
| c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f179,negated_conjecture,
! [U,V] :
( hskp6
| c3_1(V)
| c2_1(V)
| c0_1(V)
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f181,negated_conjecture,
! [U,V] :
( hskp2
| c2_1(V)
| c1_1(V)
| c0_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f183,negated_conjecture,
! [U,V] :
( hskp12
| c2_1(V)
| c1_1(V)
| c3_1(U)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f186,negated_conjecture,
! [U,V] :
( c3_1(V)
| c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f189,negated_conjecture,
! [U,V] :
( hskp0
| c3_1(V)
| c0_1(V)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f190,negated_conjecture,
! [U,V] :
( hskp6
| c0_1(V)
| c2_1(U)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f193,negated_conjecture,
! [U,V] :
( hskp19
| c1_1(V)
| c1_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f199,negated_conjecture,
! [U,V] :
( hskp23
| c1_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(f203,negated_conjecture,
! [U,V,W] :
( c1_1(W)
| c0_1(W)
| c1_1(V)
| c0_1(V)
| c0_1(U)
| ~ c2_1(W)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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(f216,plain,
( ndr1_0
| ~ hskp24 ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f217,plain,
( ndr1_0
| ~ hskp23 ),
inference(cnf_transformation,[status(thm)],[f9]) ).
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(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(f230,plain,
( ndr1_0
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f231,plain,
( ndr1_0
| ~ hskp9 ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f232,plain,
( ndr1_0
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f234,plain,
( ndr1_0
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f235,plain,
( ndr1_0
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f236,plain,
( ndr1_0
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f28]) ).
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(f239,plain,
( ndr1_0
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f240,plain,
( ndr1_0
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f241,plain,
( hskp23
| hskp15
| hskp28 ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f245,plain,
( hskp25
| hskp27
| hskp5 ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f246,plain,
( hskp14
| hskp10
| hskp5 ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f248,plain,
( hskp6
| hskp24
| hskp13 ),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f251,plain,
( hskp18
| hskp24
| hskp3 ),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f262,plain,
( c0_1(a552)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f263,plain,
( c2_1(a552)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f55]) ).
fof(f264,plain,
( c3_1(a552)
| ~ hskp29 ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f265,plain,
( c0_1(a541)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f57]) ).
fof(f266,plain,
( c1_1(a541)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f267,plain,
( c2_1(a541)
| ~ hskp28 ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f268,plain,
( c0_1(a615)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f269,plain,
( c2_1(a615)
| ~ hskp27 ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f272,plain,
( c2_1(a594)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f273,plain,
( c1_1(a590)
| ~ hskp24 ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f274,plain,
( c3_1(a584)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f275,plain,
( c2_1(a582)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f276,plain,
( c3_1(a582)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f278,plain,
( c0_1(a576)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f280,plain,
( c1_1(a570)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f281,plain,
( c0_1(a567)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f282,plain,
( c1_1(a567)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f283,plain,
( c2_1(a566)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f284,plain,
( c3_1(a566)
| ~ hskp14 ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f285,plain,
( c0_1(a565)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f286,plain,
( c3_1(a565)
| ~ hskp13 ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f287,plain,
( c0_1(a564)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f288,plain,
( c3_1(a564)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f291,plain,
( c1_1(a551)
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f292,plain,
( c3_1(a551)
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f293,plain,
( c1_1(a548)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f294,plain,
( c2_1(a548)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f296,plain,
( c3_1(a546)
| ~ hskp6 ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f297,plain,
( c0_1(a544)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f298,plain,
( c1_1(a544)
| ~ hskp5 ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f299,plain,
( c3_1(a540)
| ~ hskp4 ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f300,plain,
( c0_1(a539)
| ~ hskp3 ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f301,plain,
( c2_1(a537)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f302,plain,
( c0_1(a536)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f303,plain,
( c2_1(a536)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f304,plain,
( ~ hskp27
| ~ c1_1(a615) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f306,plain,
( ~ hskp25
| ~ c0_1(a594) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f307,plain,
( ~ hskp25
| ~ c1_1(a594) ),
inference(cnf_transformation,[status(thm)],[f99]) ).
fof(f309,plain,
( ~ hskp24
| ~ c2_1(a590) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f310,plain,
( ~ hskp23
| ~ c0_1(a587) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f311,plain,
( ~ hskp23
| ~ c2_1(a587) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f312,plain,
( ~ hskp23
| ~ c3_1(a587) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f313,plain,
( ~ hskp22
| ~ c0_1(a584) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f314,plain,
( ~ hskp22
| ~ c2_1(a584) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f315,plain,
( ~ hskp21
| ~ c1_1(a582) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f318,plain,
( ~ hskp19
| ~ c1_1(a576) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f319,plain,
( ~ hskp19
| ~ c3_1(a576) ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f320,plain,
( ~ hskp18
| ~ c0_1(a573) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f321,plain,
( ~ hskp18
| ~ c1_1(a573) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f322,plain,
( ~ hskp18
| ~ c3_1(a573) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f325,plain,
( ~ hskp16
| ~ c2_1(a570) ),
inference(cnf_transformation,[status(thm)],[f117]) ).
fof(f326,plain,
( ~ hskp16
| ~ c3_1(a570) ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f327,plain,
( ~ hskp15
| ~ c2_1(a567) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f328,plain,
( ~ hskp14
| ~ c0_1(a566) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
fof(f329,plain,
( ~ hskp13
| ~ c2_1(a565) ),
inference(cnf_transformation,[status(thm)],[f121]) ).
fof(f330,plain,
( ~ hskp12
| ~ c1_1(a564) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f332,plain,
( ~ hskp10
| ~ c0_1(a551) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f333,plain,
( ~ hskp9
| ~ c0_1(a549) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f334,plain,
( ~ hskp9
| ~ c1_1(a549) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f335,plain,
( ~ hskp9
| ~ c2_1(a549) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f336,plain,
( ~ hskp8
| ~ c0_1(a548) ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f339,plain,
( ~ hskp6
| ~ c0_1(a546) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f340,plain,
( ~ hskp6
| ~ c1_1(a546) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f341,plain,
( ~ hskp5
| ~ c3_1(a544) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f342,plain,
( ~ hskp4
| ~ c1_1(a540) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f343,plain,
( ~ hskp4
| ~ c2_1(a540) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f344,plain,
( ~ hskp3
| ~ c2_1(a539) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f345,plain,
( ~ hskp3
| ~ c3_1(a539) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f346,plain,
( ~ hskp2
| ~ c1_1(a538) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f347,plain,
( ~ hskp2
| ~ c2_1(a538) ),
inference(cnf_transformation,[status(thm)],[f139]) ).
fof(f348,plain,
( ~ hskp2
| ~ c3_1(a538) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f349,plain,
( ~ hskp1
| ~ c1_1(a537) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f350,plain,
( ~ hskp1
| ~ c3_1(a537) ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f351,plain,
( ~ hskp0
| ~ c3_1(a536) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f358,plain,
( hskp16
| hskp3
| ! [U] :
( c3_1(U)
| c2_1(U)
| c1_1(U)
| ~ ndr1_0 ) ),
inference(miniscoping,[status(thm)],[f147]) ).
fof(f359,plain,
! [X0] :
( hskp16
| hskp3
| c3_1(X0)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f358]) ).
fof(f360,plain,
( hskp2
| hskp5
| ! [U] :
( c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ),
inference(miniscoping,[status(thm)],[f148]) ).
fof(f361,plain,
! [X0] :
( hskp2
| hskp5
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f362,plain,
( hskp10
| hskp8
| ! [U] :
( c2_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f363,plain,
! [X0] :
( hskp10
| hskp8
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f374,plain,
( hskp21
| hskp29
| ! [U] :
( c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U) ) ),
inference(miniscoping,[status(thm)],[f155]) ).
fof(f375,plain,
! [X0] :
( hskp21
| hskp29
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
( hskp22
| hskp21
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f156]) ).
fof(f377,plain,
! [X0] :
( hskp22
| hskp21
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f378,plain,
( hskp6
| hskp3
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f157]) ).
fof(f379,plain,
! [X0] :
( hskp6
| hskp3
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f378]) ).
fof(f380,plain,
( hskp4
| hskp25
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f158]) ).
fof(f381,plain,
! [X0] :
( hskp4
| hskp25
| c3_1(X0)
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f382,plain,
( hskp9
| hskp10
| ! [U] :
( c0_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f159]) ).
fof(f383,plain,
! [X0] :
( hskp9
| hskp10
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f382]) ).
fof(f388,plain,
( hskp0
| hskp15
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f162]) ).
fof(f389,plain,
! [X0] :
( hskp0
| hskp15
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f388]) ).
fof(f390,plain,
( hskp6
| hskp3
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f163]) ).
fof(f391,plain,
! [X0] :
( hskp6
| hskp3
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f392,plain,
( hskp21
| hskp12
| ! [U] :
( c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f164]) ).
fof(f393,plain,
! [X0] :
( hskp21
| hskp12
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f400,plain,
( hskp9
| hskp25
| ! [U] :
( c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f168]) ).
fof(f401,plain,
! [X0] :
( hskp9
| hskp25
| c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f414,plain,
( hskp0
| ! [V] :
( c2_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f175]) ).
fof(f415,plain,
! [X0,X1] :
( hskp0
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f416,plain,
( hskp3
| ! [V] :
( c3_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f417,plain,
! [X0,X1] :
( hskp3
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f416]) ).
fof(f418,plain,
( hskp1
| ! [V] :
( c2_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f177]) ).
fof(f419,plain,
! [X0,X1] :
( hskp1
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f420,plain,
( hskp4
| ! [V] :
( c3_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f178]) ).
fof(f421,plain,
! [X0,X1] :
( hskp4
| c3_1(X1)
| c1_1(X1)
| c0_1(X1)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f420]) ).
fof(f422,plain,
( hskp6
| ! [V] :
( c3_1(V)
| c2_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f179]) ).
fof(f423,plain,
! [X0,X1] :
( hskp6
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f426,plain,
( hskp2
| ! [V] :
( c2_1(V)
| c1_1(V)
| c0_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c2_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f181]) ).
fof(f427,plain,
! [X0,X1] :
( hskp2
| c2_1(X1)
| c1_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f426]) ).
fof(f430,plain,
( hskp12
| ! [V] :
( c2_1(V)
| c1_1(V)
| ! [U] :
( c3_1(U)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f183]) ).
fof(f431,plain,
! [X0,X1] :
( hskp12
| c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f430]) ).
fof(f436,plain,
! [V] :
( c3_1(V)
| c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f186]) ).
fof(f437,plain,
! [X0,X1] :
( c3_1(X1)
| c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f436]) ).
fof(f442,plain,
( hskp0
| ! [V] :
( c3_1(V)
| c0_1(V)
| ~ c2_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f189]) ).
fof(f443,plain,
! [X0,X1] :
( hskp0
| c3_1(X1)
| c0_1(X1)
| ~ c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f444,plain,
( hskp6
| ! [V] :
( c0_1(V)
| ! [U] :
( c2_1(U)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f190]) ).
fof(f445,plain,
! [X0,X1] :
( hskp6
| c0_1(X1)
| c2_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f444]) ).
fof(f450,plain,
( hskp19
| ! [V] :
( c1_1(V)
| ! [U] :
( c1_1(U)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f193]) ).
fof(f451,plain,
! [X0,X1] :
( hskp19
| c1_1(X1)
| c1_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f462,plain,
( hskp23
| ! [V] :
( c1_1(V)
| ~ c2_1(V)
| ~ c0_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c2_1(U)
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f463,plain,
! [X0,X1] :
( hskp23
| c1_1(X1)
| ~ c2_1(X1)
| ~ c0_1(X1)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f462]) ).
fof(f470,plain,
! [W] :
( c1_1(W)
| c0_1(W)
| ! [V] :
( c1_1(V)
| c0_1(V)
| ! [U] :
( c0_1(U)
| ~ c2_1(W)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f203]) ).
fof(f471,plain,
! [X0,X1,X2] :
( c1_1(X2)
| c0_1(X2)
| c1_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ c2_1(X2)
| ~ c3_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f470]) ).
fof(f537,plain,
( ~ hskp2
| hskp16
| hskp3
| c3_1(a538)
| c2_1(a538)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f359,f346]) ).
fof(f540,plain,
( ~ hskp9
| hskp16
| hskp3
| c3_1(a549)
| c2_1(a549)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f359,f334]) ).
fof(f548,plain,
( ~ hskp2
| hskp16
| hskp3
| c3_1(a538)
| c2_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f537,f238]) ).
fof(f549,plain,
( ~ hskp9
| hskp16
| hskp3
| c3_1(a549)
| c2_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f540,f231]) ).
fof(f556,plain,
( ~ hskp6
| hskp2
| hskp5
| c1_1(a546)
| ~ ndr1_0
| ~ c3_1(a546) ),
inference(resolution,[status(thm)],[f361,f339]) ).
fof(f568,plain,
( ~ hskp6
| hskp2
| hskp5
| c1_1(a546)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f556,f296]) ).
fof(f573,plain,
( ~ hskp6
| hskp2
| hskp5
| c1_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f568,f234]) ).
fof(f574,plain,
( ~ hskp6
| ~ hskp6
| hskp2
| hskp5 ),
inference(resolution,[status(thm)],[f573,f340]) ).
fof(f575,plain,
( ~ hskp6
| hskp2
| hskp5 ),
inference(duplicate_literals_removal,[status(thm)],[f574]) ).
fof(f591,plain,
( ~ hskp22
| hskp10
| hskp8
| c2_1(a584)
| ~ ndr1_0
| ~ c1_1(a584) ),
inference(resolution,[status(thm)],[f363,f313]) ).
fof(f596,plain,
( ~ hskp22
| hskp10
| hskp8
| c2_1(a584)
| ~ c1_1(a584) ),
inference(forward_subsumption_resolution,[status(thm)],[f591,f218]) ).
fof(f629,plain,
( ~ hskp2
| hskp16
| hskp3
| c3_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f548,f347]) ).
fof(f630,plain,
( ~ hskp2
| ~ hskp2
| hskp16
| hskp3 ),
inference(resolution,[status(thm)],[f629,f348]) ).
fof(f631,plain,
( ~ hskp2
| hskp16
| hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f630]) ).
fof(f712,plain,
( ~ hskp1
| hskp21
| hskp29
| c3_1(a537)
| ~ ndr1_0
| ~ c2_1(a537) ),
inference(resolution,[status(thm)],[f375,f349]) ).
fof(f720,plain,
( ~ hskp19
| hskp21
| hskp29
| c3_1(a576)
| ~ ndr1_0
| ~ c2_1(a576) ),
inference(resolution,[status(thm)],[f375,f318]) ).
fof(f722,plain,
( ~ hskp25
| hskp21
| hskp29
| c3_1(a594)
| ~ ndr1_0
| ~ c2_1(a594) ),
inference(resolution,[status(thm)],[f375,f307]) ).
fof(f723,plain,
( ~ hskp27
| hskp21
| hskp29
| c3_1(a615)
| ~ ndr1_0
| ~ c2_1(a615) ),
inference(resolution,[status(thm)],[f375,f304]) ).
fof(f724,plain,
( ~ hskp1
| hskp21
| hskp29
| c3_1(a537)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f712,f301]) ).
fof(f726,plain,
( ~ hskp19
| hskp21
| hskp29
| c3_1(a576)
| ~ c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f720,f221]) ).
fof(f727,plain,
( ~ hskp25
| hskp21
| hskp29
| c3_1(a594)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f722,f272]) ).
fof(f728,plain,
( ~ hskp27
| hskp21
| hskp29
| c3_1(a615)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f723,f269]) ).
fof(f732,plain,
( ~ hskp3
| hskp22
| hskp21
| c2_1(a539)
| ~ ndr1_0
| ~ c0_1(a539) ),
inference(resolution,[status(thm)],[f377,f345]) ).
fof(f742,plain,
( ~ hskp3
| hskp22
| hskp21
| c2_1(a539)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f732,f300]) ).
fof(f751,plain,
( ~ hskp1
| hskp21
| hskp29
| c3_1(a537) ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f239]) ).
fof(f752,plain,
( ~ hskp1
| ~ hskp1
| hskp21
| hskp29 ),
inference(resolution,[status(thm)],[f751,f350]) ).
fof(f753,plain,
( ~ hskp1
| hskp21
| hskp29 ),
inference(duplicate_literals_removal,[status(thm)],[f752]) ).
fof(f754,plain,
( ~ hskp25
| hskp21
| hskp29
| c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f727,f215]) ).
fof(f755,plain,
( ~ hskp27
| hskp21
| hskp29
| c3_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f728,f213]) ).
fof(f756,plain,
( ~ hskp3
| hskp22
| hskp21
| c2_1(a539) ),
inference(forward_subsumption_resolution,[status(thm)],[f742,f237]) ).
fof(f757,plain,
( ~ hskp3
| ~ hskp3
| hskp22
| hskp21 ),
inference(resolution,[status(thm)],[f756,f344]) ).
fof(f758,plain,
( ~ hskp3
| hskp22
| hskp21 ),
inference(duplicate_literals_removal,[status(thm)],[f757]) ).
fof(f765,plain,
( ~ hskp5
| hskp6
| hskp3
| c2_1(a544)
| ~ ndr1_0
| ~ c1_1(a544) ),
inference(resolution,[status(thm)],[f379,f341]) ).
fof(f767,plain,
( ~ hskp16
| hskp6
| hskp3
| c2_1(a570)
| ~ ndr1_0
| ~ c1_1(a570) ),
inference(resolution,[status(thm)],[f379,f326]) ).
fof(f773,plain,
( ~ hskp5
| hskp6
| hskp3
| c2_1(a544)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f765,f298]) ).
fof(f774,plain,
( ~ hskp16
| hskp6
| hskp3
| c2_1(a570)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f767,f280]) ).
fof(f781,plain,
( ~ hskp5
| hskp4
| hskp25
| c2_1(a544)
| ~ ndr1_0
| ~ c1_1(a544) ),
inference(resolution,[status(thm)],[f381,f341]) ).
fof(f790,plain,
( ~ hskp5
| hskp4
| hskp25
| c2_1(a544)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f781,f298]) ).
fof(f796,plain,
( ~ hskp8
| hskp9
| hskp10
| ~ ndr1_0
| ~ c2_1(a548)
| ~ c1_1(a548) ),
inference(resolution,[status(thm)],[f383,f336]) ).
fof(f807,plain,
( ~ hskp8
| hskp9
| hskp10
| ~ ndr1_0
| ~ c2_1(a548) ),
inference(forward_subsumption_resolution,[status(thm)],[f796,f293]) ).
fof(f810,plain,
( ~ hskp5
| hskp6
| hskp3
| c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f773,f235]) ).
fof(f811,plain,
( ~ hskp16
| hskp6
| hskp3
| c2_1(a570) ),
inference(forward_subsumption_resolution,[status(thm)],[f774,f224]) ).
fof(f812,plain,
( ~ hskp16
| ~ hskp16
| hskp6
| hskp3 ),
inference(resolution,[status(thm)],[f811,f325]) ).
fof(f813,plain,
( ~ hskp16
| hskp6
| hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f812]) ).
fof(f832,plain,
( ~ hskp5
| hskp4
| hskp25
| c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f790,f235]) ).
fof(f838,plain,
( ~ hskp8
| hskp9
| hskp10
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f807,f294]) ).
fof(f885,plain,
! [X0] :
( hskp6
| hskp3
| c2_1(X0)
| ~ ndr1_0
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f391,f379]) ).
fof(f897,plain,
( ~ hskp24
| hskp6
| hskp3
| ~ ndr1_0
| ~ c1_1(a590) ),
inference(resolution,[status(thm)],[f885,f309]) ).
fof(f903,plain,
( ~ hskp24
| hskp6
| hskp3
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f897,f273]) ).
fof(f904,plain,
( ~ hskp0
| hskp21
| hskp12
| ~ ndr1_0
| ~ c2_1(a536)
| ~ c0_1(a536) ),
inference(resolution,[status(thm)],[f393,f351]) ).
fof(f908,plain,
( ~ hskp5
| hskp21
| hskp12
| ~ ndr1_0
| ~ c2_1(a544)
| ~ c0_1(a544) ),
inference(resolution,[status(thm)],[f393,f341]) ).
fof(f916,plain,
( ~ hskp0
| hskp21
| hskp12
| ~ ndr1_0
| ~ c2_1(a536) ),
inference(forward_subsumption_resolution,[status(thm)],[f904,f302]) ).
fof(f918,plain,
( ~ hskp5
| hskp21
| hskp12
| ~ ndr1_0
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f908,f297]) ).
fof(f940,plain,
( ~ hskp24
| hskp6
| hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f903,f216]) ).
fof(f958,plain,
( ~ hskp0
| hskp21
| hskp12
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f916,f303]) ).
fof(f960,plain,
( ~ hskp5
| hskp21
| hskp12
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f918,f235]) ).
fof(f980,plain,
( ~ hskp0
| hskp9
| hskp25
| ~ ndr1_0
| ~ c2_1(a536)
| ~ c0_1(a536) ),
inference(resolution,[status(thm)],[f401,f351]) ).
fof(f984,plain,
( ~ hskp5
| hskp9
| hskp25
| ~ ndr1_0
| ~ c2_1(a544)
| ~ c0_1(a544) ),
inference(resolution,[status(thm)],[f401,f341]) ).
fof(f992,plain,
( ~ hskp0
| hskp9
| hskp25
| ~ ndr1_0
| ~ c2_1(a536) ),
inference(forward_subsumption_resolution,[status(thm)],[f980,f302]) ).
fof(f994,plain,
( ~ hskp5
| hskp9
| hskp25
| ~ ndr1_0
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f984,f297]) ).
fof(f1027,plain,
( ~ hskp0
| hskp9
| hskp25
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f992,f303]) ).
fof(f1029,plain,
( ~ hskp5
| hskp9
| hskp25
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f994,f235]) ).
fof(f1036,plain,
( ~ hskp9
| hskp16
| hskp3
| c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f549,f335]) ).
fof(f1042,plain,
( ~ hskp22
| hskp10
| hskp8
| ~ c1_1(a584) ),
inference(forward_subsumption_resolution,[status(thm)],[f596,f314]) ).
fof(f1049,plain,
( ~ hskp6
| hskp0
| c2_1(a546)
| c1_1(a546)
| c1_1(a546)
| ~ ndr1_0
| ~ c3_1(a546) ),
inference(resolution,[status(thm)],[f415,f339]) ).
fof(f1055,plain,
( ~ hskp9
| hskp0
| c2_1(a549)
| c1_1(a549)
| c1_1(a549)
| ~ ndr1_0
| ~ c3_1(a549) ),
inference(resolution,[status(thm)],[f415,f333]) ).
fof(f1076,plain,
! [X0] :
( ~ hskp9
| hskp0
| c2_1(a549)
| c1_1(a549)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(resolution,[status(thm)],[f415,f333]) ).
fof(f1085,plain,
! [X0] :
( hskp0
| c2_1(X0)
| c1_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(factoring,[status(thm)],[f415]) ).
fof(f1086,plain,
( ~ hskp6
| hskp0
| c2_1(a546)
| c1_1(a546)
| ~ ndr1_0
| ~ c3_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f1049]) ).
fof(f1087,plain,
( ~ hskp6
| hskp0
| c2_1(a546)
| c1_1(a546)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1086,f296]) ).
fof(f1091,plain,
( ~ hskp9
| hskp0
| c2_1(a549)
| c1_1(a549)
| ~ ndr1_0
| ~ c3_1(a549) ),
inference(duplicate_literals_removal,[status(thm)],[f1055]) ).
fof(f1092,plain,
( ~ hskp9
| hskp0
| c2_1(a549)
| c1_1(a549)
| ~ c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f1091,f231]) ).
fof(f1107,plain,
! [X0] :
( ~ hskp9
| hskp0
| c2_1(a549)
| c1_1(a549)
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1076,f231]) ).
fof(f1111,plain,
! [X0] :
( hskp0
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1085]) ).
fof(f1114,plain,
! [X0] :
( ~ hskp4
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a540)
| ~ ndr1_0
| ~ c3_1(a540) ),
inference(resolution,[status(thm)],[f417,f342]) ).
fof(f1115,plain,
! [X0] :
( ~ hskp6
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a546)
| ~ ndr1_0
| ~ c3_1(a546) ),
inference(resolution,[status(thm)],[f417,f340]) ).
fof(f1116,plain,
! [X0] :
( ~ hskp9
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a549)
| ~ ndr1_0
| ~ c3_1(a549) ),
inference(resolution,[status(thm)],[f417,f334]) ).
fof(f1117,plain,
! [X0] :
( ~ hskp12
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a564)
| ~ ndr1_0
| ~ c3_1(a564) ),
inference(resolution,[status(thm)],[f417,f330]) ).
fof(f1135,plain,
! [X0] :
( ~ hskp25
| hskp3
| c3_1(a594)
| c1_1(a594)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(resolution,[status(thm)],[f417,f306]) ).
fof(f1136,plain,
! [X0] :
( ~ hskp4
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a540)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f299]) ).
fof(f1137,plain,
! [X0] :
( ~ hskp6
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a546)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1115,f296]) ).
fof(f1138,plain,
! [X0] :
( ~ hskp9
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a549)
| ~ c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f1116,f231]) ).
fof(f1139,plain,
! [X0] :
( ~ hskp12
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a564)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1117,f288]) ).
fof(f1145,plain,
! [X0] :
( ~ hskp25
| hskp3
| c3_1(a594)
| c1_1(a594)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1135,f215]) ).
fof(f1151,plain,
! [X0] :
( ~ hskp12
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a564)
| ~ c0_1(a564) ),
inference(resolution,[status(thm)],[f419,f330]) ).
fof(f1171,plain,
! [X0] :
( ~ hskp12
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1151,f287]) ).
fof(f1189,plain,
! [X0] :
( ~ hskp13
| hskp4
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a565)
| ~ c0_1(a565) ),
inference(resolution,[status(thm)],[f421,f329]) ).
fof(f1207,plain,
! [X0] :
( ~ hskp25
| hskp4
| c3_1(a594)
| c1_1(a594)
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f421,f306]) ).
fof(f1209,plain,
! [X0] :
( ~ hskp13
| hskp4
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(a565) ),
inference(forward_subsumption_resolution,[status(thm)],[f1189,f285]) ).
fof(f1216,plain,
! [X0] :
( ~ hskp25
| hskp4
| c3_1(a594)
| c1_1(a594)
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1207,f215]) ).
fof(f1218,plain,
( ~ hskp19
| hskp21
| hskp29
| ~ c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f726,f319]) ).
fof(f1223,plain,
( ~ hskp6
| hskp0
| c2_1(a546)
| c1_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1087,f234]) ).
fof(f1224,plain,
( ~ hskp6
| ~ hskp6
| hskp0
| c2_1(a546) ),
inference(resolution,[status(thm)],[f1223,f340]) ).
fof(f1225,plain,
( ~ hskp6
| hskp0
| c2_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f1224]) ).
fof(f1231,plain,
! [X0] :
( ~ hskp12
| hskp6
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a564)
| ~ c0_1(a564) ),
inference(resolution,[status(thm)],[f423,f330]) ).
fof(f1237,plain,
! [X0] :
( ~ hskp27
| hskp6
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a615)
| ~ c0_1(a615) ),
inference(resolution,[status(thm)],[f423,f304]) ).
fof(f1251,plain,
! [X0] :
( ~ hskp12
| hskp6
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1231,f287]) ).
fof(f1254,plain,
! [X0] :
( ~ hskp27
| hskp6
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f1237,f268]) ).
fof(f1295,plain,
( ~ hskp9
| hskp0
| c2_1(a549)
| ~ c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f1092,f334]) ).
fof(f1296,plain,
( ~ hskp9
| ~ hskp9
| hskp0
| ~ c3_1(a549) ),
inference(resolution,[status(thm)],[f1295,f335]) ).
fof(f1297,plain,
( ~ hskp9
| hskp0
| ~ c3_1(a549) ),
inference(duplicate_literals_removal,[status(thm)],[f1296]) ).
fof(f1350,plain,
! [X0] :
( ~ hskp6
| hskp2
| c2_1(a546)
| c1_1(a546)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f427,f339]) ).
fof(f1362,plain,
! [X0] :
( ~ hskp6
| hskp2
| c2_1(a546)
| c1_1(a546)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1350,f234]) ).
fof(f1404,plain,
! [X0] :
( ~ hskp5
| hskp12
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(a544)
| ~ c0_1(a544) ),
inference(resolution,[status(thm)],[f431,f341]) ).
fof(f1426,plain,
! [X0] :
( ~ hskp5
| hskp12
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c1_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f1404,f297]) ).
fof(f1485,plain,
! [X0] :
( ~ hskp4
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a540) ),
inference(forward_subsumption_resolution,[status(thm)],[f1136,f236]) ).
fof(f1492,plain,
( ~ hskp18
| ~ hskp4
| hskp3
| c3_1(a573)
| c1_1(a573)
| c2_1(a540) ),
inference(resolution,[status(thm)],[f1485,f320]) ).
fof(f1497,plain,
( ~ hskp25
| ~ hskp4
| hskp3
| c3_1(a594)
| c1_1(a594)
| c2_1(a540) ),
inference(resolution,[status(thm)],[f1485,f306]) ).
fof(f1500,plain,
( ~ hskp18
| ~ hskp4
| hskp3
| c3_1(a573)
| c1_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f1492,f343]) ).
fof(f1502,plain,
( ~ hskp25
| ~ hskp4
| hskp3
| c3_1(a594)
| c1_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f1497,f343]) ).
fof(f1505,plain,
( ~ hskp18
| ~ hskp4
| hskp3
| c3_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f1500,f321]) ).
fof(f1506,plain,
( ~ hskp18
| ~ hskp18
| ~ hskp4
| hskp3 ),
inference(resolution,[status(thm)],[f1505,f322]) ).
fof(f1507,plain,
( ~ hskp18
| ~ hskp4
| hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f1506]) ).
fof(f1545,plain,
! [X0] :
( ~ hskp2
| c2_1(a538)
| ~ c0_1(a538)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f437,f348]) ).
fof(f1546,plain,
! [X0] :
( ~ hskp3
| c2_1(a539)
| ~ c0_1(a539)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f437,f345]) ).
fof(f1547,plain,
! [X0] :
( ~ hskp5
| c2_1(a544)
| ~ c0_1(a544)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f437,f341]) ).
fof(f1555,plain,
! [X0] :
( ~ hskp2
| c2_1(a538)
| ~ c0_1(a538)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1545,f238]) ).
fof(f1556,plain,
! [X0] :
( ~ hskp3
| c2_1(a539)
| ~ c0_1(a539)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1546,f237]) ).
fof(f1557,plain,
! [X0] :
( ~ hskp5
| c2_1(a544)
| ~ c0_1(a544)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1547,f235]) ).
fof(f1560,plain,
( ~ hskp25
| ~ hskp4
| hskp3
| c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f1502,f307]) ).
fof(f1561,plain,
! [X0] :
( ~ hskp6
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1137,f234]) ).
fof(f1573,plain,
( ~ hskp25
| ~ hskp6
| hskp3
| c3_1(a594)
| c1_1(a594)
| c2_1(a546) ),
inference(resolution,[status(thm)],[f1561,f306]) ).
fof(f1579,plain,
( ~ hskp25
| ~ hskp6
| hskp3
| c3_1(a594)
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1573,f307]) ).
fof(f1581,plain,
! [X0] :
( ~ hskp12
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1139,f228]) ).
fof(f1585,plain,
( ~ hskp9
| ~ hskp12
| hskp3
| c3_1(a549)
| c1_1(a549)
| c2_1(a564) ),
inference(resolution,[status(thm)],[f1581,f333]) ).
fof(f1595,plain,
( ~ hskp9
| ~ hskp12
| hskp3
| c3_1(a549)
| c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1585,f334]) ).
fof(f1645,plain,
! [X0] :
( ~ hskp25
| hskp0
| c3_1(a594)
| ~ c2_1(a594)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f443,f306]) ).
fof(f1650,plain,
! [X0] :
( ~ hskp25
| hskp0
| c3_1(a594)
| ~ c2_1(a594)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1645,f215]) ).
fof(f1676,plain,
! [X0] :
( ~ hskp15
| hskp6
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a567)
| ~ c0_1(a567) ),
inference(resolution,[status(thm)],[f445,f327]) ).
fof(f1686,plain,
! [X0] :
( ~ hskp10
| hskp6
| c2_1(X0)
| ~ c3_1(a551)
| ~ c1_1(a551)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f445,f332]) ).
fof(f1697,plain,
! [X0] :
( ~ hskp15
| hskp6
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a567) ),
inference(forward_subsumption_resolution,[status(thm)],[f1676,f281]) ).
fof(f1700,plain,
! [X0] :
( ~ hskp10
| hskp6
| c2_1(X0)
| ~ c3_1(a551)
| ~ c1_1(a551)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1686,f230]) ).
fof(f1704,plain,
! [X0] :
( ~ hskp12
| hskp1
| c2_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1171,f288]) ).
fof(f1705,plain,
( ~ hskp6
| ~ hskp12
| hskp1
| c2_1(a546)
| c1_1(a546)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f1704,f339]) ).
fof(f1708,plain,
( ~ hskp9
| ~ hskp12
| hskp1
| c2_1(a549)
| c1_1(a549)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f1704,f333]) ).
fof(f1717,plain,
( ~ hskp6
| ~ hskp12
| hskp1
| c2_1(a546)
| c1_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1705,f234]) ).
fof(f1718,plain,
( ~ hskp9
| ~ hskp12
| hskp1
| c2_1(a549)
| c1_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f1708,f231]) ).
fof(f1722,plain,
( ~ hskp6
| ~ hskp12
| hskp1
| c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f1717,f340]) ).
fof(f1723,plain,
( ~ hskp9
| ~ hskp12
| hskp1
| c2_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f1718,f334]) ).
fof(f1724,plain,
( ~ hskp9
| ~ hskp9
| ~ hskp12
| hskp1 ),
inference(resolution,[status(thm)],[f1723,f335]) ).
fof(f1725,plain,
( ~ hskp9
| ~ hskp12
| hskp1 ),
inference(duplicate_literals_removal,[status(thm)],[f1724]) ).
fof(f1854,plain,
! [X0] :
( hskp19
| c1_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(factoring,[status(thm)],[f451]) ).
fof(f1878,plain,
! [X0] :
( hskp19
| c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1854]) ).
fof(f2051,plain,
! [X0] :
( ~ hskp13
| hskp4
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1209,f286]) ).
fof(f2058,plain,
( ~ hskp18
| ~ hskp13
| hskp4
| c3_1(a573)
| c1_1(a573)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f2051,f320]) ).
fof(f2066,plain,
( ~ hskp18
| ~ hskp13
| hskp4
| c3_1(a573)
| c1_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f2058,f227]) ).
fof(f2071,plain,
( ~ hskp18
| ~ hskp13
| hskp4
| c3_1(a573) ),
inference(forward_subsumption_resolution,[status(thm)],[f2066,f321]) ).
fof(f2072,plain,
( ~ hskp18
| ~ hskp18
| ~ hskp13
| hskp4 ),
inference(resolution,[status(thm)],[f2071,f322]) ).
fof(f2073,plain,
( ~ hskp18
| ~ hskp13
| hskp4 ),
inference(duplicate_literals_removal,[status(thm)],[f2072]) ).
fof(f2086,plain,
! [X0] :
( ~ hskp27
| hskp23
| ~ c2_1(a615)
| ~ c0_1(a615)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f463,f304]) ).
fof(f2091,plain,
! [X0] :
( ~ hskp27
| hskp23
| ~ c2_1(a615)
| ~ c0_1(a615)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2086,f213]) ).
fof(f2262,plain,
( ~ hskp6
| c1_1(a546)
| c1_1(a546)
| ~ c2_1(a546)
| ~ c3_1(a546)
| ~ ndr1_0
| ~ c3_1(a546)
| ~ c2_1(a546) ),
inference(resolution,[status(thm)],[f471,f339]) ).
fof(f2284,plain,
( ~ hskp25
| c1_1(a594)
| c1_1(a594)
| ~ c2_1(a594)
| ~ c3_1(a594)
| ~ ndr1_0
| ~ c3_1(a594)
| ~ c2_1(a594) ),
inference(resolution,[status(thm)],[f471,f306]) ).
fof(f2296,plain,
! [X0] :
( ~ hskp14
| c1_1(a566)
| c1_1(a566)
| c0_1(X0)
| ~ c2_1(a566)
| ~ c3_1(a566)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(resolution,[status(thm)],[f471,f328]) ).
fof(f2322,plain,
! [X0] :
( c1_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(factoring,[status(thm)],[f471]) ).
fof(f2323,plain,
( ~ hskp6
| c1_1(a546)
| ~ ndr1_0
| ~ c3_1(a546)
| ~ c2_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f2262]) ).
fof(f2324,plain,
( ~ hskp6
| c1_1(a546)
| ~ ndr1_0
| ~ c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2323,f296]) ).
fof(f2340,plain,
( ~ hskp25
| c1_1(a594)
| ~ ndr1_0
| ~ c3_1(a594)
| ~ c2_1(a594) ),
inference(duplicate_literals_removal,[status(thm)],[f2284]) ).
fof(f2341,plain,
( ~ hskp25
| c1_1(a594)
| ~ ndr1_0
| ~ c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f2340,f272]) ).
fof(f2351,plain,
! [X0] :
( ~ hskp14
| c1_1(a566)
| c0_1(X0)
| ~ c2_1(a566)
| ~ c3_1(a566)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2296]) ).
fof(f2352,plain,
! [X0] :
( ~ hskp14
| c1_1(a566)
| c0_1(X0)
| ~ c2_1(a566)
| ~ c3_1(a566)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2351,f226]) ).
fof(f2368,plain,
! [X0] :
( c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2322]) ).
fof(f2403,plain,
( ~ hskp6
| c1_1(a546)
| ~ c2_1(a546) ),
inference(forward_subsumption_resolution,[status(thm)],[f2324,f234]) ).
fof(f2404,plain,
( ~ hskp6
| ~ hskp6
| ~ c2_1(a546) ),
inference(resolution,[status(thm)],[f2403,f340]) ).
fof(f2405,plain,
( ~ hskp6
| ~ c2_1(a546) ),
inference(duplicate_literals_removal,[status(thm)],[f2404]) ).
fof(f2406,plain,
( ~ hskp25
| ~ hskp6
| hskp3
| c3_1(a594) ),
inference(backward_subsumption_resolution,[status(thm)],[f1579,f2405]) ).
fof(f2410,plain,
! [X0] :
( ~ hskp6
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1561,f2405]) ).
fof(f2414,plain,
( ~ hskp6
| ~ hskp12
| hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f1722,f2405]) ).
fof(f2417,plain,
( ~ hskp6
| hskp0 ),
inference(backward_subsumption_resolution,[status(thm)],[f1225,f2405]) ).
fof(f2597,plain,
( ~ hskp25
| c1_1(a594)
| ~ c3_1(a594) ),
inference(forward_subsumption_resolution,[status(thm)],[f2341,f215]) ).
fof(f2598,plain,
( ~ hskp25
| ~ hskp25
| ~ c3_1(a594) ),
inference(resolution,[status(thm)],[f2597,f307]) ).
fof(f2599,plain,
( ~ hskp25
| ~ c3_1(a594) ),
inference(duplicate_literals_removal,[status(thm)],[f2598]) ).
fof(f2600,plain,
( ~ hskp25
| ~ hskp6
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f2406,f2599]) ).
fof(f2605,plain,
( ~ hskp25
| ~ hskp4
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1560,f2599]) ).
fof(f2606,plain,
( ~ hskp25
| hskp21
| hskp29 ),
inference(backward_subsumption_resolution,[status(thm)],[f754,f2599]) ).
fof(f2637,plain,
! [X0] :
( hskp0
| c1_1(X0)
| c0_1(X0)
| ~ ndr1_0
| ~ c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1111,f2368]) ).
fof(f2638,plain,
! [X0] :
( hskp19
| c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1878,f2368]) ).
fof(f2660,plain,
( ~ hskp22
| hskp0
| c1_1(a584)
| ~ ndr1_0
| ~ c3_1(a584) ),
inference(resolution,[status(thm)],[f2637,f313]) ).
fof(f2664,plain,
( ~ hskp22
| hskp0
| c1_1(a584)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2660,f274]) ).
fof(f2666,plain,
( ~ hskp22
| hskp0
| c1_1(a584) ),
inference(forward_subsumption_resolution,[status(thm)],[f2664,f218]) ).
fof(f2691,plain,
( ~ hskp21
| hskp19
| ~ ndr1_0
| ~ c3_1(a582)
| ~ c2_1(a582) ),
inference(resolution,[status(thm)],[f2638,f315]) ).
fof(f2695,plain,
( ~ hskp21
| hskp19
| ~ ndr1_0
| ~ c3_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f2691,f275]) ).
fof(f2714,plain,
! [X0] :
( ~ hskp9
| hskp0
| c2_1(a549)
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1107,f334]) ).
fof(f2729,plain,
( ~ hskp21
| hskp19
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2695,f276]) ).
fof(f2778,plain,
! [X0] :
( ~ hskp12
| hskp6
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f1251,f228]) ).
fof(f2816,plain,
! [X0] :
( ~ hskp9
| hskp3
| c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f1138,f335]) ).
fof(f2931,plain,
! [X0] :
( ~ hskp27
| hskp6
| c3_1(X0)
| c2_1(X0)
| c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1254,f269]) ).
fof(f2935,plain,
( ~ hskp9
| ~ hskp27
| hskp6
| c3_1(a549)
| c2_1(a549)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f2931,f333]) ).
fof(f2941,plain,
( ~ hskp23
| ~ hskp27
| hskp6
| c3_1(a587)
| c2_1(a587)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f2931,f310]) ).
fof(f2944,plain,
( ~ hskp9
| ~ hskp27
| hskp6
| c3_1(a549)
| c2_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f2935,f231]) ).
fof(f2947,plain,
( ~ hskp23
| ~ hskp27
| hskp6
| c3_1(a587)
| c2_1(a587) ),
inference(forward_subsumption_resolution,[status(thm)],[f2941,f217]) ).
fof(f2949,plain,
( ~ hskp9
| ~ hskp27
| hskp6
| c3_1(a549) ),
inference(forward_subsumption_resolution,[status(thm)],[f2944,f335]) ).
fof(f2952,plain,
( ~ hskp23
| ~ hskp27
| hskp6
| c3_1(a587) ),
inference(forward_subsumption_resolution,[status(thm)],[f2947,f311]) ).
fof(f2953,plain,
( ~ hskp23
| ~ hskp23
| ~ hskp27
| hskp6 ),
inference(resolution,[status(thm)],[f2952,f312]) ).
fof(f2954,plain,
( ~ hskp23
| ~ hskp27
| hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f2953]) ).
fof(f2955,plain,
! [X0] :
( ~ hskp25
| hskp3
| c3_1(a594)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1145,f307]) ).
fof(f3229,plain,
! [X0] :
( ~ hskp25
| hskp4
| c3_1(a594)
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1216,f307]) ).
fof(f3243,plain,
! [X0] :
( ~ hskp25
| ~ hskp25
| hskp4
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f3229,f2599]) ).
fof(f3244,plain,
! [X0] :
( ~ hskp25
| hskp4
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3243]) ).
fof(f3461,plain,
! [X0] :
( ~ hskp5
| hskp12
| c2_1(X0)
| c1_1(X0)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1426,f298]) ).
fof(f3470,plain,
( ~ hskp19
| ~ hskp5
| hskp12
| c2_1(a576)
| ~ c0_1(a576)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f3461,f318]) ).
fof(f3477,plain,
( ~ hskp19
| ~ hskp5
| hskp12
| c2_1(a576)
| ~ c0_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f3470,f235]) ).
fof(f3542,plain,
( ~ hskp19
| ~ hskp5
| hskp12
| c2_1(a576) ),
inference(forward_subsumption_resolution,[status(thm)],[f3477,f278]) ).
fof(f3543,plain,
! [X0] :
( ~ hskp6
| hskp2
| c2_1(a546)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1362,f340]) ).
fof(f3544,plain,
! [X0] :
( ~ hskp6
| ~ hskp6
| hskp2
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f3543,f2405]) ).
fof(f3545,plain,
! [X0] :
( ~ hskp6
| hskp2
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3544]) ).
fof(f3900,plain,
! [X0] :
( ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1555,f347]) ).
fof(f3904,plain,
( ~ hskp12
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(a564)
| ~ c2_1(a564) ),
inference(resolution,[status(thm)],[f3900,f287]) ).
fof(f3909,plain,
( ~ hskp27
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(a615)
| ~ c2_1(a615) ),
inference(resolution,[status(thm)],[f3900,f268]) ).
fof(f3911,plain,
( ~ hskp29
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(a552)
| ~ c2_1(a552) ),
inference(resolution,[status(thm)],[f3900,f262]) ).
fof(f3948,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(resolution,[status(thm)],[f3900,f2368]) ).
fof(f4107,plain,
( ~ hskp12
| ~ hskp2
| ~ c0_1(a538)
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f3904,f288]) ).
fof(f4108,plain,
( ~ hskp27
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f3909,f269]) ).
fof(f4110,plain,
( ~ hskp29
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(a552) ),
inference(forward_subsumption_resolution,[status(thm)],[f3911,f263]) ).
fof(f4126,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f3948]) ).
fof(f4127,plain,
! [X0] :
( c1_1(X0)
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4126,f238]) ).
fof(f4208,plain,
( ~ hskp12
| hskp6
| c3_1(a538)
| c2_1(a538)
| ~ c2_1(a564)
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(resolution,[status(thm)],[f4107,f2778]) ).
fof(f4216,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| c1_1(a538)
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(resolution,[status(thm)],[f4107,f2410]) ).
fof(f4277,plain,
( hskp6
| c3_1(a538)
| c2_1(a538)
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(duplicate_literals_removal,[status(thm)],[f4208]) ).
fof(f4278,plain,
( hskp6
| c3_1(a538)
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f4277,f347]) ).
fof(f4280,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f4216,f346]) ).
fof(f4324,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| c1_1(a538)
| ~ hskp27
| ~ hskp2
| ~ c3_1(a615) ),
inference(resolution,[status(thm)],[f4108,f2410]) ).
fof(f4388,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| ~ hskp27
| ~ hskp2
| ~ c3_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f4324,f346]) ).
fof(f4522,plain,
( ~ hskp29
| ~ hskp2
| ~ c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f4110,f264]) ).
fof(f4528,plain,
( ~ hskp27
| hskp6
| c3_1(a538)
| c2_1(a538)
| ~ ndr1_0
| ~ hskp29
| ~ hskp2 ),
inference(resolution,[status(thm)],[f4522,f2931]) ).
fof(f4531,plain,
( ~ hskp9
| hskp3
| c3_1(a538)
| c1_1(a538)
| ~ c3_1(a549)
| ~ hskp29
| ~ hskp2 ),
inference(resolution,[status(thm)],[f4522,f2816]) ).
fof(f4541,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| c1_1(a538)
| ~ hskp29
| ~ hskp2 ),
inference(resolution,[status(thm)],[f4522,f2410]) ).
fof(f4597,plain,
( ~ hskp27
| hskp6
| c3_1(a538)
| c2_1(a538)
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4528,f238]) ).
fof(f4600,plain,
( ~ hskp9
| hskp3
| c3_1(a538)
| ~ c3_1(a549)
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4531,f346]) ).
fof(f4604,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4541,f346]) ).
fof(f4779,plain,
( ~ hskp6
| hskp3
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4604,f348]) ).
fof(f4780,plain,
( hskp6
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f4278,f348]) ).
fof(f4791,plain,
( ~ hskp21
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(a582)
| ~ c2_1(a582) ),
inference(resolution,[status(thm)],[f4127,f315]) ).
fof(f4795,plain,
( ~ hskp21
| ~ hskp2
| ~ c0_1(a538)
| ~ c3_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f4791,f275]) ).
fof(f4815,plain,
( ~ hskp21
| ~ hskp2
| ~ c0_1(a538) ),
inference(forward_subsumption_resolution,[status(thm)],[f4795,f276]) ).
fof(f4834,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| c1_1(a538)
| ~ hskp21
| ~ hskp2 ),
inference(resolution,[status(thm)],[f4815,f2410]) ).
fof(f4897,plain,
( ~ hskp6
| hskp3
| c3_1(a538)
| ~ hskp21
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4834,f346]) ).
fof(f4923,plain,
( ~ hskp6
| hskp3
| ~ hskp21
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4897,f348]) ).
fof(f4963,plain,
( ~ hskp6
| hskp3
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f4280,f348]) ).
fof(f4964,plain,
( ~ hskp6
| hskp3
| ~ hskp27
| ~ hskp2
| ~ c3_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f4388,f348]) ).
fof(f5029,plain,
( ~ hskp27
| hskp6
| c3_1(a538)
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4597,f347]) ).
fof(f5030,plain,
( ~ hskp2
| ~ hskp27
| hskp6
| ~ hskp29
| ~ hskp2 ),
inference(resolution,[status(thm)],[f5029,f348]) ).
fof(f5031,plain,
( ~ hskp27
| hskp6
| ~ hskp29
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f5030]) ).
fof(f5033,plain,
( ~ hskp9
| hskp3
| ~ c3_1(a549)
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4600,f348]) ).
fof(f5034,plain,
! [X0] :
( ~ hskp3
| c2_1(a539)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1556,f300]) ).
fof(f5035,plain,
! [X0] :
( ~ hskp3
| ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f5034,f344]) ).
fof(f5036,plain,
! [X0] :
( ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5035]) ).
fof(f5037,plain,
! [X0] :
( ~ hskp5
| c2_1(a544)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1557,f297]) ).
fof(f5041,plain,
( ~ hskp12
| ~ hskp3
| ~ c3_1(a564)
| ~ c2_1(a564) ),
inference(resolution,[status(thm)],[f5036,f287]) ).
fof(f5046,plain,
( ~ hskp27
| ~ hskp3
| ~ c3_1(a615)
| ~ c2_1(a615) ),
inference(resolution,[status(thm)],[f5036,f268]) ).
fof(f5048,plain,
( ~ hskp29
| ~ hskp3
| ~ c3_1(a552)
| ~ c2_1(a552) ),
inference(resolution,[status(thm)],[f5036,f262]) ).
fof(f5067,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(resolution,[status(thm)],[f5036,f2368]) ).
fof(f5120,plain,
( ~ hskp12
| ~ hskp3
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f5041,f288]) ).
fof(f5121,plain,
( ~ hskp27
| ~ hskp3
| ~ c3_1(a615) ),
inference(forward_subsumption_resolution,[status(thm)],[f5046,f269]) ).
fof(f5123,plain,
( ~ hskp29
| ~ hskp3
| ~ c3_1(a552) ),
inference(forward_subsumption_resolution,[status(thm)],[f5048,f263]) ).
fof(f5133,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5067]) ).
fof(f5134,plain,
! [X0] :
( c1_1(X0)
| ~ hskp3
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5133,f237]) ).
fof(f5166,plain,
( ~ hskp6
| ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(backward_subsumption_resolution,[status(thm)],[f4963,f5120]) ).
fof(f5207,plain,
( ~ hskp12
| ~ hskp2
| ~ c2_1(a564) ),
inference(forward_subsumption_resolution,[status(thm)],[f5166,f4780]) ).
fof(f5236,plain,
( ~ hskp6
| ~ hskp27
| ~ hskp2
| ~ c3_1(a615) ),
inference(backward_subsumption_resolution,[status(thm)],[f4964,f5121]) ).
fof(f5237,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ hskp27
| ~ hskp3 ),
inference(resolution,[status(thm)],[f5121,f755]) ).
fof(f5268,plain,
( hskp21
| hskp29
| ~ hskp27
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f5237]) ).
fof(f5324,plain,
( ~ hskp9
| ~ c3_1(a549)
| ~ hskp29
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f5033,f5327]) ).
fof(f5326,plain,
( ~ hskp6
| ~ hskp29
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f4779,f5327]) ).
fof(f5327,plain,
( ~ hskp29
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f5123,f264]) ).
fof(f5328,plain,
( ~ hskp25
| hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f5327,f2606]) ).
fof(f5330,plain,
( ~ hskp19
| hskp21
| ~ c2_1(a576)
| ~ hskp3 ),
inference(resolution,[status(thm)],[f5327,f1218]) ).
fof(f5334,plain,
( ~ hskp1
| hskp21
| ~ hskp3 ),
inference(resolution,[status(thm)],[f5327,f753]) ).
fof(f5336,plain,
( ~ hskp27
| ~ hskp29
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f5031,f5326]) ).
fof(f5768,plain,
( hskp21
| ~ hskp27
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f5268,f5327]) ).
fof(f5771,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ hskp6
| ~ hskp27
| ~ hskp2 ),
inference(resolution,[status(thm)],[f5236,f755]) ).
fof(f5802,plain,
( hskp21
| hskp29
| ~ hskp6
| ~ hskp27
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f5771]) ).
fof(f5803,plain,
( hskp21
| ~ hskp6
| ~ hskp27
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f5802,f5336]) ).
fof(f5880,plain,
( ~ hskp9
| ~ hskp12
| hskp3
| c2_1(a564)
| ~ hskp9
| ~ hskp29
| ~ hskp2 ),
inference(resolution,[status(thm)],[f5324,f1595]) ).
fof(f5935,plain,
( ~ hskp12
| hskp3
| c2_1(a564)
| ~ hskp9
| ~ hskp29
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f5880]) ).
fof(f5936,plain,
( ~ hskp12
| hskp3
| ~ hskp9
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f5935,f5207]) ).
fof(f6005,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp29
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f5936,f5327]) ).
fof(f6012,plain,
( ~ hskp1
| hskp21
| ~ hskp12
| ~ hskp9
| ~ hskp2 ),
inference(resolution,[status(thm)],[f6005,f753]) ).
fof(f6016,plain,
( hskp21
| ~ hskp12
| ~ hskp9
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f6012,f1725]) ).
fof(f6028,plain,
( ~ hskp21
| ~ hskp3
| ~ c3_1(a582)
| ~ c2_1(a582) ),
inference(resolution,[status(thm)],[f5134,f315]) ).
fof(f6031,plain,
( ~ hskp21
| ~ hskp3
| ~ c3_1(a582) ),
inference(forward_subsumption_resolution,[status(thm)],[f6028,f275]) ).
fof(f6032,plain,
( ~ hskp6
| ~ hskp21
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f4923,f6039]) ).
fof(f6033,plain,
( ~ hskp3
| hskp22 ),
inference(backward_subsumption_resolution,[status(thm)],[f758,f6039]) ).
fof(f6035,plain,
( ~ hskp19
| ~ c2_1(a576)
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f5330,f6039]) ).
fof(f6036,plain,
( ~ hskp27
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f5768,f6039]) ).
fof(f6037,plain,
( ~ hskp1
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f5334,f6039]) ).
fof(f6038,plain,
( ~ hskp25
| ~ hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f5328,f6039]) ).
fof(f6039,plain,
( ~ hskp21
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f6031,f276]) ).
fof(f6044,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp2
| ~ hskp3 ),
inference(resolution,[status(thm)],[f6039,f6016]) ).
fof(f6059,plain,
( ~ hskp0
| hskp12
| ~ ndr1_0
| ~ hskp3 ),
inference(resolution,[status(thm)],[f6039,f958]) ).
fof(f6063,plain,
( ~ hskp0
| hskp12
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f6059,f240]) ).
fof(f6066,plain,
( hskp25
| hskp5
| ~ hskp3 ),
inference(resolution,[status(thm)],[f6036,f245]) ).
fof(f6077,plain,
( ~ hskp18
| ~ hskp4
| ~ hskp1 ),
inference(resolution,[status(thm)],[f6037,f1507]) ).
fof(f6078,plain,
! [X0] :
( ~ hskp25
| c3_1(a594)
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2955,f6038]) ).
fof(f6083,plain,
( ~ hskp25
| ~ hskp4 ),
inference(backward_subsumption_resolution,[status(thm)],[f2605,f6038]) ).
fof(f6084,plain,
( ~ hskp25
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f2600,f6038]) ).
fof(f6091,plain,
( ~ hskp0
| hskp9
| ~ ndr1_0
| ~ hskp3 ),
inference(resolution,[status(thm)],[f6038,f1027]) ).
fof(f6094,plain,
! [X0] :
( ~ hskp25
| c2_1(X0)
| c1_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f6078,f2599]) ).
fof(f6095,plain,
( ~ hskp0
| hskp9
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f6091,f240]) ).
fof(f6101,plain,
! [X0] :
( ~ hskp25
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f3244,f6083]) ).
fof(f6121,plain,
( ~ hskp0
| hskp9
| ~ ndr1_0
| ~ hskp6 ),
inference(resolution,[status(thm)],[f6084,f1027]) ).
fof(f6125,plain,
( ~ hskp0
| hskp9
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f6121,f240]) ).
fof(f6136,plain,
( ~ hskp6
| ~ hskp27
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f5803,f6032]) ).
fof(f6141,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp2
| ~ hskp6
| ~ hskp2 ),
inference(resolution,[status(thm)],[f6032,f6016]) ).
fof(f6153,plain,
( ~ hskp0
| hskp12
| ~ ndr1_0
| ~ hskp6
| ~ hskp2 ),
inference(resolution,[status(thm)],[f6032,f958]) ).
fof(f6156,plain,
( ~ hskp12
| ~ hskp9
| ~ hskp6
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f6141]) ).
fof(f6160,plain,
( ~ hskp0
| hskp12
| ~ hskp6
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f6153,f240]) ).
fof(f6162,plain,
( hskp5
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f6066,f6038]) ).
fof(f6212,plain,
! [X0] :
( ~ hskp25
| hskp0
| c3_1(a594)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1650,f272]) ).
fof(f6268,plain,
( hskp9
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f6125,f2417]) ).
fof(f6270,plain,
( hskp25
| hskp5
| ~ hskp6
| ~ hskp2 ),
inference(resolution,[status(thm)],[f6136,f245]) ).
fof(f6272,plain,
( hskp25
| hskp5
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f6270,f575]) ).
fof(f6355,plain,
! [X0] :
( ~ hskp15
| hskp6
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f1697,f282]) ).
fof(f6418,plain,
( hskp5
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f6272,f6084]) ).
fof(f6644,plain,
! [X0] :
( ~ hskp10
| hskp6
| c2_1(X0)
| ~ c3_1(a551)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1700,f291]) ).
fof(f6703,plain,
( ~ hskp19
| ~ hskp5
| hskp12
| ~ hskp19
| ~ hskp3 ),
inference(resolution,[status(thm)],[f6035,f3542]) ).
fof(f6753,plain,
( ~ hskp5
| hskp12
| ~ hskp19
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f6703]) ).
fof(f6754,plain,
( hskp12
| ~ hskp19
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f6753,f6162]) ).
fof(f6767,plain,
( ~ hskp0
| ~ hskp3
| ~ hskp9
| ~ hskp2
| ~ hskp3 ),
inference(resolution,[status(thm)],[f6044,f6063]) ).
fof(f6787,plain,
( ~ hskp0
| ~ hskp9
| ~ hskp2
| ~ hskp3 ),
inference(duplicate_literals_removal,[status(thm)],[f6767]) ).
fof(f6788,plain,
( ~ hskp0
| ~ hskp2
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f6787,f6095]) ).
fof(f7395,plain,
( ~ hskp12
| ~ hskp6
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f6156,f6268]) ).
fof(f7449,plain,
( ~ hskp0
| ~ hskp6
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f6160,f7395]) ).
fof(f7461,plain,
( ~ hskp16
| hskp3
| ~ hskp0
| ~ hskp2 ),
inference(resolution,[status(thm)],[f7449,f813]) ).
fof(f7468,plain,
( ~ hskp16
| ~ hskp0
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f7461,f6788]) ).
fof(f7582,plain,
( ~ hskp2
| hskp3
| ~ hskp0
| ~ hskp2 ),
inference(resolution,[status(thm)],[f7468,f631]) ).
fof(f7583,plain,
( hskp3
| ~ hskp0
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f7582]) ).
fof(f7584,plain,
( ~ hskp0
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f7583,f6788]) ).
fof(f7587,plain,
! [X0] :
( ~ hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0)
| ~ hskp0 ),
inference(resolution,[status(thm)],[f7584,f3545]) ).
fof(f7588,plain,
! [X0] :
( ~ hskp6
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f7587,f2417]) ).
fof(f10391,plain,
! [X0] :
( ~ hskp25
| hskp0
| c3_1(a594)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6212,f6101]) ).
fof(f10416,plain,
! [X0] :
( ~ hskp25
| hskp0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f10391,f2599]) ).
fof(f10420,plain,
( ~ hskp5
| ~ hskp6
| ~ c2_1(a544)
| ~ c1_1(a544) ),
inference(resolution,[status(thm)],[f7588,f297]) ).
fof(f10510,plain,
( ~ hskp5
| ~ hskp6
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f10420,f298]) ).
fof(f10649,plain,
( ~ hskp6
| ~ c2_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f10510,f6418]) ).
fof(f10651,plain,
! [X0] :
( ~ hskp5
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f10649,f5037]) ).
fof(f10702,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f10651,f6418]) ).
fof(f11473,plain,
( ~ hskp27
| ~ c3_1(a615)
| ~ c2_1(a615)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f10702,f268]) ).
fof(f11475,plain,
( ~ hskp29
| ~ c3_1(a552)
| ~ c2_1(a552)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f10702,f262]) ).
fof(f11504,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f10702,f2368]) ).
fof(f11557,plain,
( ~ hskp27
| ~ c3_1(a615)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f11473,f269]) ).
fof(f11558,plain,
( ~ hskp29
| ~ c3_1(a552)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f11475,f263]) ).
fof(f11570,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f11504]) ).
fof(f11571,plain,
! [X0] :
( c1_1(X0)
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f11570,f234]) ).
fof(f11596,plain,
! [X0] :
( ~ hskp27
| hskp23
| ~ c2_1(a615)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2091,f268]) ).
fof(f11833,plain,
( ~ hskp27
| hskp21
| hskp29
| ~ hskp27
| ~ hskp6 ),
inference(resolution,[status(thm)],[f11557,f755]) ).
fof(f11864,plain,
( hskp21
| hskp29
| ~ hskp27
| ~ hskp6 ),
inference(duplicate_literals_removal,[status(thm)],[f11833]) ).
fof(f11872,plain,
( ~ hskp29
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f11558,f264]) ).
fof(f11878,plain,
( ~ hskp1
| hskp21
| ~ hskp6 ),
inference(resolution,[status(thm)],[f11872,f753]) ).
fof(f12236,plain,
( hskp21
| ~ hskp27
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f11864,f11872]) ).
fof(f12648,plain,
( ~ hskp21
| ~ c3_1(a582)
| ~ c2_1(a582)
| ~ hskp6 ),
inference(resolution,[status(thm)],[f11571,f315]) ).
fof(f12653,plain,
( ~ hskp21
| ~ c3_1(a582)
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f12648,f275]) ).
fof(f12808,plain,
( ~ hskp27
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f12236,f12810]) ).
fof(f12809,plain,
( ~ hskp1
| ~ hskp6 ),
inference(backward_subsumption_resolution,[status(thm)],[f11878,f12810]) ).
fof(f12810,plain,
( ~ hskp21
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f12653,f276]) ).
fof(f12822,plain,
( ~ hskp0
| hskp12
| ~ ndr1_0
| ~ hskp6 ),
inference(resolution,[status(thm)],[f12810,f958]) ).
fof(f12825,plain,
( ~ hskp0
| hskp12
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f12822,f240]) ).
fof(f12829,plain,
( ~ hskp9
| ~ hskp27
| c3_1(a549) ),
inference(backward_subsumption_resolution,[status(thm)],[f2949,f12808]) ).
fof(f12831,plain,
( ~ hskp23
| ~ hskp27 ),
inference(backward_subsumption_resolution,[status(thm)],[f2954,f12808]) ).
fof(f12845,plain,
( ~ hskp6
| ~ hskp12 ),
inference(backward_subsumption_resolution,[status(thm)],[f2414,f12809]) ).
fof(f12852,plain,
( ~ hskp24
| hskp3
| ~ hskp1 ),
inference(resolution,[status(thm)],[f12809,f940]) ).
fof(f12861,plain,
( ~ hskp24
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f12852,f6037]) ).
fof(f12865,plain,
! [X0] :
( ~ hskp27
| ~ c2_1(a615)
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f11596,f12831]) ).
fof(f12868,plain,
! [X0] :
( ~ hskp27
| ~ c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f12865,f269]) ).
fof(f12907,plain,
( hskp18
| hskp3
| ~ hskp1 ),
inference(resolution,[status(thm)],[f12861,f251]) ).
fof(f12908,plain,
( hskp6
| hskp13
| ~ hskp1 ),
inference(resolution,[status(thm)],[f12861,f248]) ).
fof(f12910,plain,
( hskp18
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f12907,f6037]) ).
fof(f12911,plain,
( hskp13
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f12908,f12809]) ).
fof(f13163,plain,
( ~ hskp4
| ~ hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f6077,f12910]) ).
fof(f13247,plain,
( ~ hskp18
| ~ hskp13
| ~ hskp1 ),
inference(resolution,[status(thm)],[f13163,f2073]) ).
fof(f13250,plain,
( ~ hskp18
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f13247,f12911]) ).
fof(f13289,plain,
( ~ hskp9
| ~ hskp12 ),
inference(backward_subsumption_resolution,[status(thm)],[f1725,f13290]) ).
fof(f13290,plain,
~ hskp1,
inference(forward_subsumption_resolution,[status(thm)],[f13250,f12910]) ).
fof(f13305,plain,
( ~ hskp19
| ~ hskp3
| ~ hskp9 ),
inference(resolution,[status(thm)],[f13289,f6754]) ).
fof(f13306,plain,
( ~ hskp0
| ~ hskp3
| ~ hskp9 ),
inference(resolution,[status(thm)],[f13289,f6063]) ).
fof(f13324,plain,
( ~ hskp0
| ~ hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f13306,f6095]) ).
fof(f13444,plain,
~ hskp6,
inference(backward_subsumption_resolution,[status(thm)],[f2417,f13445]) ).
fof(f13445,plain,
( ~ hskp0
| ~ hskp6 ),
inference(forward_subsumption_resolution,[status(thm)],[f12825,f12845]) ).
fof(f13450,plain,
( ~ hskp24
| hskp3
| ~ hskp0 ),
inference(resolution,[status(thm)],[f13445,f940]) ).
fof(f13457,plain,
( ~ hskp24
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13450,f13324]) ).
fof(f13464,plain,
! [X0] :
( ~ hskp10
| c2_1(X0)
| ~ c3_1(a551)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6644,f13444]) ).
fof(f13467,plain,
! [X0] :
( ~ hskp15
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f6355,f13444]) ).
fof(f13482,plain,
( ~ hskp5
| hskp3
| c2_1(a544) ),
inference(backward_subsumption_resolution,[status(thm)],[f810,f13444]) ).
fof(f13484,plain,
( hskp24
| hskp13 ),
inference(backward_subsumption_resolution,[status(thm)],[f248,f13444]) ).
fof(f13489,plain,
( ~ hskp24
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f940,f13444]) ).
fof(f13492,plain,
( ~ hskp16
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f813,f13444]) ).
fof(f13493,plain,
! [X0] :
( ~ hskp10
| c2_1(X0)
| ~ c1_1(X0)
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13464,f292]) ).
fof(f13494,plain,
! [X0] :
( ~ hskp15
| c0_1(X0)
| ~ c3_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13467,f225]) ).
fof(f13503,plain,
( hskp18
| hskp3
| ~ hskp0 ),
inference(resolution,[status(thm)],[f13457,f251]) ).
fof(f13506,plain,
( hskp18
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13503,f13324]) ).
fof(f13537,plain,
( ~ hskp0
| hskp13 ),
inference(resolution,[status(thm)],[f13484,f13457]) ).
fof(f13538,plain,
( hskp18
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f251,f13489]) ).
fof(f13706,plain,
( ~ hskp9
| hskp3
| c3_1(a549) ),
inference(backward_subsumption_resolution,[status(thm)],[f1036,f13492]) ).
fof(f13715,plain,
( ~ hskp4
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f1507,f13538]) ).
fof(f13722,plain,
( ~ hskp0
| ~ hskp4 ),
inference(resolution,[status(thm)],[f13715,f13324]) ).
fof(f13734,plain,
( ~ hskp18
| ~ hskp13
| ~ hskp0 ),
inference(resolution,[status(thm)],[f13722,f2073]) ).
fof(f13737,plain,
( ~ hskp18
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13734,f13537]) ).
fof(f13747,plain,
! [X0] :
( ~ hskp9
| c2_1(a549)
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2714,f13766]) ).
fof(f13751,plain,
( ~ hskp22
| c1_1(a584) ),
inference(backward_subsumption_resolution,[status(thm)],[f2666,f13766]) ).
fof(f13761,plain,
! [X0] :
( hskp15
| c2_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f389,f13766]) ).
fof(f13762,plain,
! [X0] :
( ~ hskp25
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f10416,f13766]) ).
fof(f13765,plain,
( ~ hskp9
| ~ c3_1(a549) ),
inference(backward_subsumption_resolution,[status(thm)],[f1297,f13766]) ).
fof(f13766,plain,
~ hskp0,
inference(forward_subsumption_resolution,[status(thm)],[f13737,f13506]) ).
fof(f13768,plain,
! [X0] :
( ~ hskp9
| c1_1(X0)
| c0_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13747,f335]) ).
fof(f14916,plain,
( ~ hskp22
| hskp10
| hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f1042,f13751]) ).
fof(f15147,plain,
( ~ hskp9
| ~ hskp27 ),
inference(forward_subsumption_resolution,[status(thm)],[f12829,f13765]) ).
fof(f15149,plain,
( hskp25
| hskp5
| ~ hskp9 ),
inference(resolution,[status(thm)],[f15147,f245]) ).
fof(f16470,plain,
! [X0] :
( ~ hskp14
| c1_1(a566)
| c0_1(X0)
| ~ c2_1(a566)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2352,f284]) ).
fof(f16490,plain,
( ~ hskp14
| ~ hskp14
| c1_1(a566)
| ~ c2_1(a566)
| ~ c3_1(a566)
| ~ c2_1(a566) ),
inference(resolution,[status(thm)],[f16470,f328]) ).
fof(f16509,plain,
( ~ hskp14
| c1_1(a566)
| ~ c3_1(a566)
| ~ c2_1(a566) ),
inference(duplicate_literals_removal,[status(thm)],[f16490]) ).
fof(f16510,plain,
( ~ hskp14
| c1_1(a566)
| ~ c3_1(a566) ),
inference(forward_subsumption_resolution,[status(thm)],[f16509,f283]) ).
fof(f16684,plain,
( ~ hskp19
| ~ hskp9 ),
inference(backward_subsumption_resolution,[status(thm)],[f13305,f16685]) ).
fof(f16685,plain,
( ~ hskp9
| hskp3 ),
inference(forward_subsumption_resolution,[status(thm)],[f13706,f13765]) ).
fof(f16690,plain,
( ~ hskp21
| ~ ndr1_0
| ~ hskp9 ),
inference(resolution,[status(thm)],[f16684,f2729]) ).
fof(f16693,plain,
( ~ hskp21
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f16690,f231]) ).
fof(f16701,plain,
( ~ hskp5
| hskp12
| ~ c2_1(a544)
| ~ hskp9 ),
inference(resolution,[status(thm)],[f16693,f960]) ).
fof(f16703,plain,
( ~ hskp5
| ~ c2_1(a544)
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f16701,f13289]) ).
fof(f16717,plain,
( ~ hskp29
| ~ hskp25
| ~ c3_1(a552) ),
inference(resolution,[status(thm)],[f13762,f262]) ).
fof(f16785,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp25
| ~ c3_1(X0) ),
inference(resolution,[status(thm)],[f13762,f2368]) ).
fof(f16822,plain,
( ~ hskp29
| ~ hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f16717,f264]) ).
fof(f16901,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ hskp25
| ~ c3_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f16785]) ).
fof(f16902,plain,
! [X0] :
( c1_1(X0)
| ~ ndr1_0
| ~ hskp25
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f16901,f6094]) ).
fof(f16943,plain,
( ~ hskp25
| hskp21 ),
inference(backward_subsumption_resolution,[status(thm)],[f2606,f16822]) ).
fof(f16952,plain,
( ~ hskp9
| ~ hskp25 ),
inference(resolution,[status(thm)],[f16943,f16693]) ).
fof(f17099,plain,
( hskp5
| ~ hskp9 ),
inference(backward_subsumption_resolution,[status(thm)],[f15149,f16952]) ).
fof(f18197,plain,
( ~ hskp5
| hskp25
| ~ c2_1(a544) ),
inference(backward_subsumption_resolution,[status(thm)],[f1029,f18200]) ).
fof(f18200,plain,
( ~ c2_1(a544)
| ~ hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f16703,f17099]) ).
fof(f19707,plain,
( ~ hskp5
| hskp4
| hskp25 ),
inference(backward_subsumption_resolution,[status(thm)],[f832,f18197]) ).
fof(f20724,plain,
( ~ hskp14
| c1_1(a566) ),
inference(forward_subsumption_resolution,[status(thm)],[f16510,f284]) ).
fof(f20855,plain,
! [X0] :
( c1_1(X0)
| ~ hskp25
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f16902,f215]) ).
fof(f20863,plain,
( ~ hskp21
| ~ hskp25
| ~ c3_1(a582) ),
inference(resolution,[status(thm)],[f20855,f315]) ).
fof(f20866,plain,
( ~ hskp21
| ~ hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f20863,f276]) ).
fof(f20871,plain,
( hskp27
| hskp5 ),
inference(backward_subsumption_resolution,[status(thm)],[f245,f20879]) ).
fof(f20872,plain,
( ~ hskp5
| hskp4 ),
inference(backward_subsumption_resolution,[status(thm)],[f19707,f20879]) ).
fof(f20873,plain,
( ~ hskp5
| ~ c2_1(a544) ),
inference(backward_subsumption_resolution,[status(thm)],[f18197,f20879]) ).
fof(f20879,plain,
~ hskp25,
inference(forward_subsumption_resolution,[status(thm)],[f20866,f16943]) ).
fof(f20918,plain,
( ~ hskp5
| hskp3 ),
inference(backward_subsumption_resolution,[status(thm)],[f13482,f20873]) ).
fof(f23187,plain,
( ~ hskp28
| ~ hskp27
| ~ c2_1(a541)
| ~ c1_1(a541) ),
inference(resolution,[status(thm)],[f12868,f265]) ).
fof(f23310,plain,
( ~ hskp28
| ~ hskp27
| ~ c2_1(a541) ),
inference(forward_subsumption_resolution,[status(thm)],[f23187,f266]) ).
fof(f23356,plain,
( ~ hskp28
| ~ hskp27 ),
inference(forward_subsumption_resolution,[status(thm)],[f23310,f267]) ).
fof(f23359,plain,
( hskp23
| hskp15
| ~ hskp27 ),
inference(resolution,[status(thm)],[f23356,f241]) ).
fof(f23361,plain,
( hskp15
| ~ hskp27 ),
inference(forward_subsumption_resolution,[status(thm)],[f23359,f12831]) ).
fof(f23728,plain,
( ~ hskp5
| ~ hskp10
| ~ c1_1(a544)
| ~ c0_1(a544) ),
inference(resolution,[status(thm)],[f13493,f20873]) ).
fof(f23744,plain,
( ~ hskp15
| ~ hskp10
| ~ c1_1(a567)
| ~ c0_1(a567) ),
inference(resolution,[status(thm)],[f13493,f327]) ).
fof(f23750,plain,
( ~ hskp5
| ~ hskp10
| ~ c1_1(a544) ),
inference(forward_subsumption_resolution,[status(thm)],[f23728,f297]) ).
fof(f23756,plain,
( ~ hskp15
| ~ hskp10
| ~ c1_1(a567) ),
inference(forward_subsumption_resolution,[status(thm)],[f23744,f281]) ).
fof(f23758,plain,
( ~ hskp5
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f23750,f298]) ).
fof(f24155,plain,
( ~ hskp15
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f23756,f282]) ).
fof(f24156,plain,
( ~ hskp27
| ~ hskp10 ),
inference(resolution,[status(thm)],[f24155,f23361]) ).
fof(f24167,plain,
( hskp5
| ~ hskp10 ),
inference(resolution,[status(thm)],[f24156,f20871]) ).
fof(f24169,plain,
~ hskp10,
inference(forward_subsumption_resolution,[status(thm)],[f24167,f23758]) ).
fof(f24172,plain,
! [X0] :
( hskp9
| c0_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f383,f24169]) ).
fof(f24175,plain,
( hskp14
| hskp5 ),
inference(backward_subsumption_resolution,[status(thm)],[f246,f24169]) ).
fof(f24178,plain,
( ~ hskp22
| hskp8 ),
inference(backward_subsumption_resolution,[status(thm)],[f14916,f24169]) ).
fof(f24181,plain,
( ~ hskp8
| hskp9
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f838,f24169]) ).
fof(f24184,plain,
( ~ hskp8
| hskp9 ),
inference(forward_subsumption_resolution,[status(thm)],[f24181,f232]) ).
fof(f24208,plain,
! [X0] :
( ~ hskp27
| ~ c2_1(X0)
| ~ c1_1(X0)
| hskp9
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f24172,f12868]) ).
fof(f24229,plain,
! [X0] :
( ~ hskp27
| hskp9
| ~ ndr1_0
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f24208]) ).
fof(f24230,plain,
! [X0] :
( ~ hskp27
| hskp9
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f24229,f213]) ).
fof(f24497,plain,
! [X0] :
( ~ hskp27
| ~ c2_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f24230,f15147]) ).
fof(f24499,plain,
( ~ hskp14
| ~ hskp27
| ~ c2_1(a566) ),
inference(resolution,[status(thm)],[f24497,f20724]) ).
fof(f24601,plain,
( ~ hskp14
| ~ hskp27 ),
inference(forward_subsumption_resolution,[status(thm)],[f24499,f283]) ).
fof(f24664,plain,
( hskp5
| ~ hskp14 ),
inference(resolution,[status(thm)],[f24601,f20871]) ).
fof(f24666,plain,
hskp5,
inference(forward_subsumption_resolution,[status(thm)],[f24664,f24175]) ).
fof(f24671,plain,
hskp3,
inference(backward_subsumption_resolution,[status(thm)],[f20918,f24666]) ).
fof(f24673,plain,
hskp4,
inference(backward_subsumption_resolution,[status(thm)],[f20872,f24666]) ).
fof(f24680,plain,
ndr1_0,
inference(backward_subsumption_resolution,[status(thm)],[f235,f24666]) ).
fof(f24695,plain,
hskp22,
inference(backward_subsumption_resolution,[status(thm)],[f6033,f24671]) ).
fof(f24701,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f5036,f24671]) ).
fof(f24758,plain,
~ c1_1(a540),
inference(backward_subsumption_resolution,[status(thm)],[f342,f24673]) ).
fof(f24759,plain,
c3_1(a540),
inference(backward_subsumption_resolution,[status(thm)],[f299,f24673]) ).
fof(f24772,plain,
! [X0] :
( hskp15
| c2_1(X0)
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f13761,f24680]) ).
fof(f24843,plain,
hskp8,
inference(backward_subsumption_resolution,[status(thm)],[f24178,f24695]) ).
fof(f24847,plain,
c1_1(a584),
inference(backward_subsumption_resolution,[status(thm)],[f13751,f24695]) ).
fof(f24850,plain,
~ c0_1(a584),
inference(backward_subsumption_resolution,[status(thm)],[f313,f24695]) ).
fof(f24851,plain,
c3_1(a584),
inference(backward_subsumption_resolution,[status(thm)],[f274,f24695]) ).
fof(f24867,plain,
hskp9,
inference(backward_subsumption_resolution,[status(thm)],[f24184,f24843]) ).
fof(f25678,plain,
! [X0] :
( hskp15
| ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f24772,f24701]) ).
fof(f25869,plain,
( ~ hskp15
| ~ c3_1(a584)
| ~ c1_1(a584) ),
inference(resolution,[status(thm)],[f13494,f24850]) ).
fof(f25880,plain,
( ~ hskp15
| ~ c3_1(a584) ),
inference(forward_subsumption_resolution,[status(thm)],[f25869,f24847]) ).
fof(f25886,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c0_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f25678,f25891]) ).
fof(f25891,plain,
~ hskp15,
inference(forward_subsumption_resolution,[status(thm)],[f25880,f24851]) ).
fof(f26192,plain,
! [X0] :
( ~ hskp9
| c1_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f13768,f25886]) ).
fof(f26195,plain,
( ~ hskp9
| ~ c3_1(a540) ),
inference(resolution,[status(thm)],[f26192,f24758]) ).
fof(f26197,plain,
~ hskp9,
inference(forward_subsumption_resolution,[status(thm)],[f26195,f24759]) ).
fof(f26198,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f26197,f24867]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN510-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.43 % Computer : n006.cluster.edu
% 0.19/0.43 % Model : x86_64 x86_64
% 0.19/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.43 % Memory : 8046.5625MB
% 0.19/0.43 % OS : Linux 6.8.0-71-generic
% 0.19/0.43 % CPULimit : 300
% 0.19/0.43 % WCLimit : 300
% 0.19/0.43 % DateTime : Mon Sep 21 11:04:12 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 57.24/7.83 % Refutation found
% 57.24/7.83 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 57.24/7.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 36.42/7.88 % Elapsed time: 7.424434 seconds
% 36.42/7.88 % CPU time: 58.084376 seconds
% 36.42/7.88 % Total memory used: 65.735 MB
% 36.42/7.88 % Net memory used: 62.039 MB
%------------------------------------------------------------------------------