%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN445-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:07 PM UTC 2026
% Result : Unsatisfiable 225.49s 29.05s
% Output : CNFRefutation 225.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 81
% Syntax : Number of formulae : 559 ( 15 unt; 0 def)
% Number of atoms : 2576 ( 0 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 3598 (1581 ~;2017 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 17 prp; 0-1 aty)
% Number of functors : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 252 ( 252 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
( hskp16
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
( ndr1_0
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
( ndr1_0
| ~ hskp25 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
( ndr1_0
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,negated_conjecture,
( ndr1_0
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
( ndr1_0
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
( ndr1_0
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,negated_conjecture,
( ndr1_0
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
( ndr1_0
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
( ndr1_0
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
( ndr1_0
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
( ndr1_0
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
( ndr1_0
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
( ndr1_0
| ~ hskp0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
( hskp12
| hskp11
| hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
( c0_1(a349)
| ~ hskp26 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,negated_conjecture,
( c3_1(a336)
| ~ hskp21 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
( c1_1(a333)
| ~ hskp20 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
( c1_1(a330)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
( c2_1(a330)
| ~ hskp19 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,negated_conjecture,
( c2_1(a321)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,negated_conjecture,
( c3_1(a321)
| ~ hskp16 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f60,negated_conjecture,
( c1_1(a320)
| ~ hskp15 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f65,negated_conjecture,
( c3_1(a310)
| ~ hskp12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,negated_conjecture,
( c1_1(a309)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,negated_conjecture,
( c3_1(a309)
| ~ hskp11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,negated_conjecture,
( c1_1(a308)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,negated_conjecture,
( c3_1(a308)
| ~ hskp10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,negated_conjecture,
( c2_1(a305)
| ~ hskp8 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,negated_conjecture,
( c1_1(a297)
| ~ hskp2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,negated_conjecture,
( c0_1(a295)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,negated_conjecture,
( c2_1(a295)
| ~ hskp1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,negated_conjecture,
( ~ hskp26
| ~ c2_1(a349) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,negated_conjecture,
( ~ hskp26
| ~ c3_1(a349) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,negated_conjecture,
( ~ hskp25
| ~ c0_1(a346) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,negated_conjecture,
( ~ hskp25
| ~ c1_1(a346) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,negated_conjecture,
( ~ hskp25
| ~ c3_1(a346) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
( ~ hskp22
| ~ c1_1(a338) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
( ~ hskp22
| ~ c2_1(a338) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91,negated_conjecture,
( ~ hskp22
| ~ c3_1(a338) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f92,negated_conjecture,
( ~ hskp21
| ~ c0_1(a336) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f93,negated_conjecture,
( ~ hskp21
| ~ c1_1(a336) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,negated_conjecture,
( ~ hskp20
| ~ c2_1(a333) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f95,negated_conjecture,
( ~ hskp20
| ~ c3_1(a333) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,negated_conjecture,
( ~ hskp19
| ~ c3_1(a330) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,negated_conjecture,
( ~ hskp16
| ~ c1_1(a321) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,negated_conjecture,
( ~ hskp15
| ~ c0_1(a320) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f102,negated_conjecture,
( ~ hskp15
| ~ c2_1(a320) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f105,negated_conjecture,
( ~ hskp12
| ~ c0_1(a310) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f106,negated_conjecture,
( ~ hskp12
| ~ c2_1(a310) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f107,negated_conjecture,
( ~ hskp11
| ~ c2_1(a309) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,negated_conjecture,
( ~ hskp10
| ~ c0_1(a308) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f111,negated_conjecture,
( ~ hskp8
| ~ c0_1(a305) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f112,negated_conjecture,
( ~ hskp8
| ~ c1_1(a305) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f122,negated_conjecture,
( ~ hskp2
| ~ c0_1(a297) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f123,negated_conjecture,
( ~ hskp2
| ~ c3_1(a297) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f124,negated_conjecture,
( ~ hskp1
| ~ c1_1(a295) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f125,negated_conjecture,
( ~ hskp0
| ~ c0_1(a294) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,negated_conjecture,
( ~ hskp0
| ~ c2_1(a294) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,negated_conjecture,
( ~ hskp0
| ~ c3_1(a294) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f128,negated_conjecture,
! [U] :
( hskp16
| c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f129,negated_conjecture,
! [U] :
( hskp21
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f130,negated_conjecture,
! [U] :
( hskp22
| c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f131,negated_conjecture,
! [U] :
( hskp0
| hskp2
| c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f134,negated_conjecture,
! [U] :
( hskp11
| hskp10
| c2_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f136,negated_conjecture,
! [U] :
( hskp16
| hskp11
| c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f139,negated_conjecture,
! [U] :
( hskp12
| hskp19
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f140,negated_conjecture,
! [U] :
( hskp20
| hskp11
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f144,negated_conjecture,
! [U] :
( hskp25
| hskp15
| c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f149,negated_conjecture,
! [U,V] :
( hskp0
| c2_1(V)
| c1_1(V)
| c0_1(V)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,negated_conjecture,
! [U,V] :
( hskp1
| c1_1(V)
| c0_1(V)
| c1_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f155,negated_conjecture,
! [U,V] :
( hskp0
| c1_1(V)
| c0_1(V)
| c2_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f160,negated_conjecture,
! [U,V] :
( hskp12
| c3_1(V)
| c0_1(V)
| c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f161,negated_conjecture,
! [U,V] :
( hskp8
| c3_1(V)
| c0_1(V)
| c3_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f162,negated_conjecture,
! [U,V] :
( hskp12
| c0_1(V)
| c3_1(U)
| c2_1(U)
| ~ c2_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f169,negated_conjecture,
! [U,V] :
( c2_1(V)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f172,negated_conjecture,
! [U,V,W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| c3_1(V)
| c2_1(V)
| c0_1(V)
| c0_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f173,negated_conjecture,
! [U,V,W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| c3_1(V)
| c2_1(V)
| c1_1(V)
| c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f174,negated_conjecture,
! [U,V,W] :
( c3_1(W)
| c1_1(W)
| c0_1(W)
| c3_1(V)
| c2_1(V)
| c0_1(V)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f176,negated_conjecture,
! [U,V,W] :
( c3_1(W)
| c2_1(W)
| c0_1(W)
| c2_1(V)
| c0_1(V)
| c1_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f178,negated_conjecture,
! [U,V,W] :
( c2_1(W)
| c0_1(W)
| c3_1(V)
| c0_1(V)
| c0_1(U)
| ~ c1_1(W)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f181,plain,
( hskp16
| hskp26 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f185,plain,
( ndr1_0
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f186,plain,
( ndr1_0
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f190,plain,
( ndr1_0
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f191,plain,
( ~ hskp20
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f192,plain,
( ~ hskp19
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f196,plain,
( ndr1_0
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f199,plain,
( ndr1_0
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f200,plain,
( ndr1_0
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f201,plain,
( ~ hskp10
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f203,plain,
( ~ hskp8
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f209,plain,
( ~ hskp2
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f210,plain,
( ~ hskp1
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f211,plain,
( ~ hskp0
| ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f216,plain,
( hskp26
| hskp11
| hskp12 ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f227,plain,
( ~ hskp26
| c0_1(a349) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f231,plain,
( c3_1(a336)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f232,plain,
( ~ hskp20
| c1_1(a333) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f233,plain,
( c1_1(a330)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f234,plain,
( c2_1(a330)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f238,plain,
( c2_1(a321)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f239,plain,
( ~ hskp16
| c3_1(a321) ),
inference(cnf_transformation,[status(thm)],[f59]) ).
fof(f240,plain,
( c1_1(a320)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f245,plain,
( c3_1(a310)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f246,plain,
( ~ hskp11
| c1_1(a309) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f247,plain,
( c3_1(a309)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f248,plain,
( ~ hskp10
| c1_1(a308) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f249,plain,
( ~ hskp10
| c3_1(a308) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f251,plain,
( c2_1(a305)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f258,plain,
( ~ hskp2
| c1_1(a297) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f259,plain,
( c0_1(a295)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f260,plain,
( ~ hskp1
| c2_1(a295) ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f261,plain,
( ~ hskp26
| ~ c2_1(a349) ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f262,plain,
( ~ c3_1(a349)
| ~ hskp26 ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f263,plain,
( ~ c0_1(a346)
| ~ hskp25 ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f264,plain,
( ~ hskp25
| ~ c1_1(a346) ),
inference(cnf_transformation,[status(thm)],[f84]) ).
fof(f265,plain,
( ~ hskp25
| ~ c3_1(a346) ),
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f269,plain,
( ~ c1_1(a338)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f270,plain,
( ~ hskp22
| ~ c2_1(a338) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f271,plain,
( ~ c3_1(a338)
| ~ hskp22 ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f272,plain,
( ~ c0_1(a336)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f273,plain,
( ~ c1_1(a336)
| ~ hskp21 ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f274,plain,
( ~ c2_1(a333)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f275,plain,
( ~ c3_1(a333)
| ~ hskp20 ),
inference(cnf_transformation,[status(thm)],[f95]) ).
fof(f276,plain,
( ~ c3_1(a330)
| ~ hskp19 ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f280,plain,
( ~ c1_1(a321)
| ~ hskp16 ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f281,plain,
( ~ c0_1(a320)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f282,plain,
( ~ c2_1(a320)
| ~ hskp15 ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f285,plain,
( ~ hskp12
| ~ c0_1(a310) ),
inference(cnf_transformation,[status(thm)],[f105]) ).
fof(f286,plain,
( ~ c2_1(a310)
| ~ hskp12 ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f287,plain,
( ~ c2_1(a309)
| ~ hskp11 ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f288,plain,
( ~ c0_1(a308)
| ~ hskp10 ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f291,plain,
( ~ c0_1(a305)
| ~ hskp8 ),
inference(cnf_transformation,[status(thm)],[f111]) ).
fof(f292,plain,
( ~ hskp8
| ~ c1_1(a305) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f302,plain,
( ~ hskp2
| ~ c0_1(a297) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f303,plain,
( ~ c3_1(a297)
| ~ hskp2 ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f304,plain,
( ~ c1_1(a295)
| ~ hskp1 ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f305,plain,
( ~ hskp0
| ~ c0_1(a294) ),
inference(cnf_transformation,[status(thm)],[f125]) ).
fof(f306,plain,
( ~ c2_1(a294)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f307,plain,
( ~ c3_1(a294)
| ~ hskp0 ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f308,plain,
( hskp16
| ! [U] :
( c2_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ),
inference(miniscoping,[status(thm)],[f128]) ).
fof(f309,plain,
! [X0] :
( ~ c3_1(X0)
| ~ ndr1_0
| hskp16
| c2_1(X0)
| c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f310,plain,
( hskp21
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f129]) ).
fof(f311,plain,
! [X0] :
( ~ ndr1_0
| hskp21
| c3_1(X0)
| c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f312,plain,
( hskp22
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ ndr1_0
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f130]) ).
fof(f313,plain,
! [X0] :
( hskp22
| ~ ndr1_0
| c2_1(X0)
| ~ c1_1(X0)
| c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f312]) ).
fof(f314,plain,
( hskp0
| hskp2
| ! [U] :
( c1_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ),
inference(miniscoping,[status(thm)],[f131]) ).
fof(f315,plain,
! [X0] :
( ~ c3_1(X0)
| c1_1(X0)
| c0_1(X0)
| hskp2
| hskp0
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f314]) ).
fof(f320,plain,
( hskp11
| hskp10
| ! [U] :
( c2_1(U)
| c0_1(U)
| ~ ndr1_0
| ~ c3_1(U) ) ),
inference(miniscoping,[status(thm)],[f134]) ).
fof(f321,plain,
! [X0] :
( ~ c3_1(X0)
| hskp11
| c2_1(X0)
| hskp10
| ~ ndr1_0
| c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f320]) ).
fof(f324,plain,
( hskp16
| hskp11
| ! [U] :
( c3_1(U)
| c1_1(U)
| ~ ndr1_0
| ~ c2_1(U) ) ),
inference(miniscoping,[status(thm)],[f136]) ).
fof(f325,plain,
! [X0] :
( hskp11
| hskp16
| c3_1(X0)
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f324]) ).
fof(f330,plain,
( hskp12
| hskp19
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f139]) ).
fof(f331,plain,
! [X0] :
( ~ ndr1_0
| hskp12
| ~ c2_1(X0)
| c1_1(X0)
| hskp19
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f330]) ).
fof(f332,plain,
( hskp20
| hskp11
| ! [U] :
( c1_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f140]) ).
fof(f333,plain,
! [X0] :
( hskp11
| ~ ndr1_0
| c1_1(X0)
| ~ c0_1(X0)
| hskp20
| ~ c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f332]) ).
fof(f340,plain,
( hskp25
| hskp15
| ! [U] :
( c3_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ),
inference(miniscoping,[status(thm)],[f144]) ).
fof(f341,plain,
! [X0] :
( hskp25
| ~ c1_1(X0)
| hskp15
| ~ c2_1(X0)
| ~ ndr1_0
| c3_1(X0) ),
inference(cnf_transformation,[status(thm)],[f340]) ).
fof(f350,plain,
( hskp0
| ! [V] :
( c2_1(V)
| c1_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c1_1(U)
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f351,plain,
! [X0,X1] :
( ~ c0_1(X1)
| c2_1(X1)
| hskp0
| ~ c1_1(X1)
| ~ ndr1_0
| c2_1(X0)
| c0_1(X0)
| c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f350]) ).
fof(f360,plain,
( hskp1
| ! [V] :
( c1_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f154]) ).
fof(f361,plain,
! [X0,X1] :
( c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(X1)
| c1_1(X1)
| ~ ndr1_0
| ~ c3_1(X1)
| c1_1(X0)
| hskp1 ),
inference(cnf_transformation,[status(thm)],[f360]) ).
fof(f362,plain,
( hskp0
| ! [V] :
( c1_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| ~ c3_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f155]) ).
fof(f363,plain,
! [X0,X1] :
( c0_1(X0)
| ~ c3_1(X1)
| ~ c1_1(X1)
| c2_1(X1)
| ~ ndr1_0
| ~ c3_1(X0)
| hskp0
| c1_1(X0) ),
inference(cnf_transformation,[status(thm)],[f362]) ).
fof(f372,plain,
( hskp12
| ! [V] :
( c3_1(V)
| c0_1(V)
| ! [U] :
( c2_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f160]) ).
fof(f373,plain,
! [X0,X1] :
( c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(X1)
| ~ c3_1(X1)
| c2_1(X1)
| c0_1(X0)
| hskp12 ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f374,plain,
( hskp8
| ! [V] :
( c3_1(V)
| c0_1(V)
| ! [U] :
( c3_1(U)
| ~ c2_1(V)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f161]) ).
fof(f375,plain,
! [X0,X1] :
( c0_1(X0)
| ~ c1_1(X1)
| hskp8
| ~ c2_1(X1)
| c3_1(X1)
| c3_1(X0)
| ~ c2_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f374]) ).
fof(f376,plain,
( hskp12
| ! [V] :
( c0_1(V)
| ! [U] :
( c3_1(U)
| c2_1(U)
| ~ c2_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c0_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f162]) ).
fof(f377,plain,
! [X0,X1] :
( hskp12
| c0_1(X1)
| ~ c1_1(X1)
| c3_1(X0)
| c2_1(X0)
| ~ c2_1(X1)
| ~ c0_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f376]) ).
fof(f390,plain,
! [V] :
( c2_1(V)
| ~ c3_1(V)
| ~ c1_1(V)
| ~ ndr1_0
| ! [U] :
( ~ c3_1(U)
| ~ c2_1(U)
| ~ c0_1(U) ) ),
inference(miniscoping,[status(thm)],[f169]) ).
fof(f391,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(X1)
| c2_1(X1)
| ~ c1_1(X1)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f390]) ).
fof(f396,plain,
! [W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| ! [V] :
( c3_1(V)
| c2_1(V)
| c0_1(V)
| ! [U] :
( c0_1(U)
| ~ ndr1_0
| ~ c2_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f172]) ).
fof(f397,plain,
! [X0,X1,X2] :
( c0_1(X1)
| c1_1(X2)
| c2_1(X0)
| ~ c2_1(X1)
| c2_1(X2)
| c0_1(X2)
| ~ ndr1_0
| ~ c1_1(X1)
| c3_1(X0)
| c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f396]) ).
fof(f398,plain,
! [W] :
( c2_1(W)
| c1_1(W)
| c0_1(W)
| ! [V] :
( c3_1(V)
| c2_1(V)
| c1_1(V)
| ! [U] :
( c2_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f399,plain,
! [X0,X1,X2] :
( c3_1(X0)
| c2_1(X2)
| c2_1(X1)
| c0_1(X2)
| ~ c1_1(X1)
| c1_1(X2)
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(cnf_transformation,[status(thm)],[f398]) ).
fof(f400,plain,
! [W] :
( c3_1(W)
| c1_1(W)
| c0_1(W)
| ! [V] :
( c3_1(V)
| c2_1(V)
| c0_1(V)
| ! [U] :
( c0_1(U)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f174]) ).
fof(f401,plain,
! [X0,X1,X2] :
( ~ c3_1(X2)
| c1_1(X0)
| c2_1(X1)
| c3_1(X1)
| ~ c2_1(X2)
| c0_1(X2)
| c0_1(X1)
| ~ ndr1_0
| c3_1(X0)
| c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f400]) ).
fof(f404,plain,
! [W] :
( c3_1(W)
| c2_1(W)
| c0_1(W)
| ! [V] :
( c2_1(V)
| c0_1(V)
| ! [U] :
( c1_1(U)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c2_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f176]) ).
fof(f405,plain,
! [X0,X1,X2] :
( c1_1(X1)
| ~ c3_1(X1)
| ~ ndr1_0
| c0_1(X2)
| c3_1(X2)
| c2_1(X2)
| ~ c2_1(X1)
| ~ c1_1(X0)
| c0_1(X0)
| c2_1(X0) ),
inference(cnf_transformation,[status(thm)],[f404]) ).
fof(f408,plain,
! [W] :
( c2_1(W)
| c0_1(W)
| ! [V] :
( c3_1(V)
| c0_1(V)
| ! [U] :
( c0_1(U)
| ~ c1_1(W)
| ~ c1_1(V)
| ~ ndr1_0
| ~ c3_1(U)
| ~ c1_1(U) ) ) ),
inference(miniscoping,[status(thm)],[f178]) ).
fof(f409,plain,
! [X0,X1,X2] :
( ~ ndr1_0
| c2_1(X1)
| ~ c1_1(X0)
| c0_1(X1)
| c0_1(X2)
| c3_1(X2)
| ~ c3_1(X0)
| ~ c1_1(X2)
| ~ c1_1(X1)
| c0_1(X0) ),
inference(cnf_transformation,[status(thm)],[f408]) ).
fof(f419,plain,
! [X0,X1] :
( ~ hskp0
| c3_1(X0)
| c2_1(a294)
| c2_1(X1)
| ~ c1_1(X1)
| c1_1(a294)
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f399,f305]) ).
fof(f421,plain,
! [X0,X1] :
( ~ hskp12
| c3_1(X0)
| c2_1(a310)
| c2_1(X1)
| ~ c1_1(X1)
| c1_1(a310)
| ~ c3_1(X1)
| c2_1(X0)
| c1_1(X0)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f399,f285]) ).
fof(f423,plain,
! [X0,X1] :
( c1_1(X1)
| c2_1(X1)
| ~ c1_1(X0)
| c1_1(a294)
| ~ hskp0
| c3_1(X1)
| c2_1(a294)
| c2_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f419,f211]) ).
fof(f427,plain,
! [X0,X1] :
( c2_1(X0)
| ~ c3_1(X0)
| c2_1(X1)
| c2_1(a310)
| c3_1(X1)
| c1_1(X1)
| c1_1(a310)
| ~ c1_1(X0)
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f421,f199]) ).
fof(f447,plain,
! [X0,X1] :
( ~ hskp0
| c0_1(X0)
| c1_1(X1)
| c2_1(a294)
| ~ c2_1(X0)
| c2_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| c0_1(a294) ),
inference(resolution,[status(thm)],[f397,f307]) ).
fof(f453,plain,
! [X0,X1] :
( ~ ndr1_0
| ~ hskp0
| c0_1(X0)
| c0_1(X1)
| c2_1(X1)
| c1_1(X1)
| ~ c1_1(X0)
| c2_1(a294)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f447,f305]) ).
fof(f480,plain,
( ~ hskp1
| ~ ndr1_0
| hskp12
| ~ c2_1(a295)
| hskp19
| ~ c0_1(a295) ),
inference(resolution,[status(thm)],[f331,f304]) ).
fof(f483,plain,
( ~ c0_1(a295)
| ~ hskp1
| hskp12
| hskp19
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f480,f260]) ).
fof(f558,plain,
! [X0,X1] :
( c0_1(X0)
| c1_1(X1)
| c2_1(a333)
| ~ c2_1(X0)
| c2_1(X1)
| c0_1(X1)
| ~ ndr1_0
| ~ c1_1(X0)
| c0_1(a333)
| ~ hskp20 ),
inference(resolution,[status(thm)],[f275,f397]) ).
fof(f559,plain,
! [X0,X1] :
( c0_1(a333)
| c2_1(X0)
| ~ hskp20
| c2_1(a333)
| ~ c2_1(X1)
| ~ c1_1(X1)
| c0_1(X1)
| c0_1(X0)
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f558,f191]) ).
fof(f562,plain,
! [X0,X1] :
( ~ hskp2
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(a297)
| c2_1(a297) ),
inference(resolution,[status(thm)],[f405,f302]) ).
fof(f563,plain,
! [X0,X1] :
( ~ hskp15
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(a320)
| c2_1(a320) ),
inference(resolution,[status(thm)],[f405,f281]) ).
fof(f567,plain,
! [X0,X1] :
( ~ hskp0
| c1_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| c0_1(X1)
| c3_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c1_1(a294)
| c2_1(a294) ),
inference(resolution,[status(thm)],[f405,f305]) ).
fof(f572,plain,
! [X0,X1] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| c2_1(a297)
| ~ hskp2
| ~ c1_1(a297)
| c3_1(X1)
| c2_1(X1)
| c0_1(X1)
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f562,f209]) ).
fof(f574,plain,
! [X0,X1] :
( ~ c2_1(X0)
| c0_1(X1)
| c2_1(X1)
| ~ c1_1(a320)
| c3_1(X1)
| c2_1(a320)
| ~ hskp15
| ~ c3_1(X0)
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f563,f196]) ).
fof(f575,plain,
! [X0,X1] :
( ~ ndr1_0
| c3_1(X1)
| c1_1(X0)
| c0_1(X1)
| ~ c2_1(X0)
| c2_1(X1)
| ~ hskp0
| ~ c3_1(X0)
| ~ c1_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f567,f306]) ).
fof(f595,plain,
! [X0,X1] :
( ~ hskp10
| ~ ndr1_0
| c2_1(X0)
| ~ c1_1(a308)
| c0_1(X0)
| c0_1(X1)
| c3_1(X1)
| ~ c3_1(a308)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f409,f288]) ).
fof(f596,plain,
! [X0,X1] :
( ~ hskp12
| ~ ndr1_0
| c2_1(X0)
| ~ c1_1(a310)
| c0_1(X0)
| c0_1(X1)
| c3_1(X1)
| ~ c3_1(a310)
| ~ c1_1(X1)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f409,f285]) ).
fof(f599,plain,
! [X0,X1] :
( ~ hskp12
| ~ c1_1(a310)
| ~ c1_1(X0)
| ~ c1_1(X1)
| c3_1(X1)
| c0_1(X1)
| c0_1(X0)
| c2_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f596,f245]) ).
fof(f600,plain,
! [X0,X1] :
( c0_1(X0)
| ~ c1_1(X1)
| c2_1(X0)
| ~ c1_1(a308)
| ~ ndr1_0
| c0_1(X1)
| ~ hskp10
| c3_1(X1)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f595,f249]) ).
fof(f631,plain,
( ~ hskp21
| ~ c3_1(a336)
| c1_1(a336)
| hskp2
| hskp0
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f315,f272]) ).
fof(f639,plain,
( ~ hskp12
| ~ c3_1(a310)
| c1_1(a310)
| hskp2
| hskp0
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f315,f285]) ).
fof(f644,plain,
( hskp2
| ~ hskp12
| hskp0
| c1_1(a310)
| ~ c3_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f639,f199]) ).
fof(f646,plain,
( ~ hskp21
| ~ c3_1(a336)
| hskp0
| hskp2
| c1_1(a336) ),
inference(forward_subsumption_resolution,[status(thm)],[f631,f190]) ).
fof(f663,plain,
( ~ hskp12
| ~ c3_1(a310)
| ~ ndr1_0
| hskp16
| c1_1(a310) ),
inference(resolution,[status(thm)],[f309,f286]) ).
fof(f673,plain,
( c1_1(a310)
| hskp16
| ~ hskp12
| ~ c3_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f663,f199]) ).
fof(f705,plain,
! [X0,X1] :
( ~ c3_1(X1)
| c1_1(a346)
| c2_1(X0)
| c3_1(X0)
| ~ c2_1(X1)
| c0_1(X1)
| c0_1(X0)
| ~ ndr1_0
| c0_1(a346)
| ~ hskp25 ),
inference(resolution,[status(thm)],[f265,f401]) ).
fof(f709,plain,
! [X0,X1] :
( c1_1(a346)
| ~ hskp25
| c0_1(X0)
| ~ c3_1(X0)
| c0_1(X1)
| c2_1(X1)
| c3_1(X1)
| ~ c2_1(X0)
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f705,f263]) ).
fof(f713,plain,
( ~ c0_1(a295)
| ~ hskp1
| hskp12
| hskp19 ),
inference(forward_subsumption_resolution,[status(thm)],[f483,f210]) ).
fof(f717,plain,
! [X0] :
( ~ hskp15
| c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a320)
| ~ c3_1(a320)
| c0_1(X0)
| hskp12 ),
inference(resolution,[status(thm)],[f373,f282]) ).
fof(f721,plain,
! [X0] :
( ~ hskp11
| c3_1(X0)
| ~ c1_1(X0)
| ~ ndr1_0
| ~ c1_1(a309)
| ~ c3_1(a309)
| c0_1(X0)
| hskp12 ),
inference(resolution,[status(thm)],[f373,f287]) ).
fof(f728,plain,
! [X0] :
( ~ c1_1(a309)
| ~ ndr1_0
| c3_1(X0)
| hskp12
| ~ hskp11
| ~ c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f721,f247]) ).
fof(f731,plain,
! [X0] :
( c3_1(X0)
| hskp12
| ~ hskp15
| c0_1(X0)
| ~ ndr1_0
| ~ c1_1(X0)
| ~ c3_1(a320) ),
inference(forward_subsumption_resolution,[status(thm)],[f717,f240]) ).
fof(f733,plain,
( hskp16
| ~ hskp12
| c1_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f673,f245]) ).
fof(f738,plain,
( ~ hskp20
| hskp22
| ~ ndr1_0
| c2_1(a333)
| ~ c1_1(a333) ),
inference(resolution,[status(thm)],[f313,f275]) ).
fof(f742,plain,
( ~ hskp0
| hskp22
| ~ ndr1_0
| c2_1(a294)
| ~ c1_1(a294) ),
inference(resolution,[status(thm)],[f313,f307]) ).
fof(f747,plain,
( ~ ndr1_0
| ~ hskp20
| c2_1(a333)
| hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f738,f232]) ).
fof(f749,plain,
( ~ hskp0
| ~ ndr1_0
| hskp22
| ~ c1_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f742,f306]) ).
fof(f751,plain,
( ~ hskp20
| ~ ndr1_0
| hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f747,f274]) ).
fof(f753,plain,
( ~ hskp0
| hskp22
| ~ c1_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f749,f211]) ).
fof(f757,plain,
( ~ hskp20
| ~ ndr1_0
| hskp21
| c2_1(a333)
| ~ c0_1(a333) ),
inference(resolution,[status(thm)],[f311,f275]) ).
fof(f758,plain,
( ~ hskp26
| ~ ndr1_0
| hskp21
| c2_1(a349)
| ~ c0_1(a349) ),
inference(resolution,[status(thm)],[f311,f262]) ).
fof(f766,plain,
( ~ ndr1_0
| ~ hskp26
| c2_1(a349)
| hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f758,f227]) ).
fof(f767,plain,
( hskp21
| ~ hskp20
| ~ ndr1_0
| ~ c0_1(a333) ),
inference(forward_subsumption_resolution,[status(thm)],[f757,f274]) ).
fof(f770,plain,
( ~ hskp26
| hskp21
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f766,f261]) ).
fof(f771,plain,
( hskp21
| ~ hskp20
| ~ c0_1(a333) ),
inference(forward_subsumption_resolution,[status(thm)],[f767,f191]) ).
fof(f856,plain,
( ~ hskp21
| ~ c3_1(a336)
| hskp11
| c2_1(a336)
| hskp10
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f321,f272]) ).
fof(f864,plain,
( ~ hskp12
| ~ c3_1(a310)
| hskp11
| c2_1(a310)
| hskp10
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f321,f285]) ).
fof(f866,plain,
( ~ hskp12
| c2_1(a310)
| hskp11
| ~ c3_1(a310)
| hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f864,f199]) ).
fof(f867,plain,
( hskp10
| c2_1(a336)
| ~ c3_1(a336)
| hskp11
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f856,f190]) ).
fof(f885,plain,
( hskp0
| c1_1(a310)
| ~ hskp12
| hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f644,f245]) ).
fof(f887,plain,
( hskp2
| hskp0
| ~ c3_1(a336)
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f646,f273]) ).
fof(f891,plain,
( hskp11
| c2_1(a310)
| ~ hskp12
| hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f866,f245]) ).
fof(f892,plain,
( ~ hskp12
| hskp11
| ~ hskp12
| hskp10 ),
inference(resolution,[status(thm)],[f891,f286]) ).
fof(f893,plain,
( hskp10
| hskp11
| ~ hskp12 ),
inference(duplicate_literals_removal,[status(thm)],[f892]) ).
fof(f894,plain,
( hskp11
| hskp10
| c2_1(a336)
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f867,f231]) ).
fof(f899,plain,
( ~ hskp19
| hskp25
| ~ c1_1(a330)
| hskp15
| ~ c2_1(a330)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f341,f276]) ).
fof(f909,plain,
( ~ c2_1(a330)
| ~ c1_1(a330)
| ~ hskp19
| hskp15
| hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f899,f192]) ).
fof(f932,plain,
( hskp15
| hskp25
| ~ c2_1(a330)
| ~ hskp19 ),
inference(forward_subsumption_resolution,[status(thm)],[f909,f233]) ).
fof(f944,plain,
( ~ hskp1
| hskp11
| ~ ndr1_0
| ~ c0_1(a295)
| hskp20
| ~ c2_1(a295) ),
inference(resolution,[status(thm)],[f333,f304]) ).
fof(f948,plain,
( hskp11
| ~ hskp1
| hskp20
| ~ ndr1_0
| ~ c0_1(a295) ),
inference(forward_subsumption_resolution,[status(thm)],[f944,f260]) ).
fof(f953,plain,
( hskp20
| hskp11
| ~ ndr1_0
| ~ hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f948,f259]) ).
fof(f989,plain,
! [X0] :
( ~ hskp15
| c0_1(X0)
| ~ c3_1(a320)
| ~ c1_1(a320)
| ~ ndr1_0
| ~ c3_1(X0)
| hskp0
| c1_1(X0) ),
inference(resolution,[status(thm)],[f363,f282]) ).
fof(f990,plain,
! [X0] :
( ~ hskp12
| c0_1(X0)
| ~ c3_1(a310)
| ~ c1_1(a310)
| ~ ndr1_0
| ~ c3_1(X0)
| hskp0
| c1_1(X0) ),
inference(resolution,[status(thm)],[f363,f286]) ).
fof(f993,plain,
! [X0] :
( ~ hskp11
| c0_1(X0)
| ~ c3_1(a309)
| ~ c1_1(a309)
| ~ ndr1_0
| ~ c3_1(X0)
| hskp0
| c1_1(X0) ),
inference(resolution,[status(thm)],[f363,f287]) ).
fof(f1000,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c3_1(a320)
| hskp0
| c1_1(X0)
| c0_1(X0)
| ~ c1_1(a320)
| ~ hskp15 ),
inference(forward_subsumption_resolution,[status(thm)],[f989,f196]) ).
fof(f1002,plain,
! [X0] :
( c1_1(X0)
| ~ c3_1(a310)
| ~ c3_1(X0)
| ~ c1_1(a310)
| hskp0
| c0_1(X0)
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f990,f199]) ).
fof(f1004,plain,
! [X0] :
( hskp0
| ~ c3_1(X0)
| c0_1(X0)
| c1_1(X0)
| ~ hskp11
| ~ c3_1(a309)
| ~ c1_1(a309) ),
inference(forward_subsumption_resolution,[status(thm)],[f993,f200]) ).
fof(f1262,plain,
! [X0] :
( ~ hskp12
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a310)
| ~ c1_1(a310)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f391,f286]) ).
fof(f1265,plain,
! [X0] :
( ~ hskp11
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c3_1(a309)
| ~ c1_1(a309)
| ~ c2_1(X0)
| ~ c0_1(X0) ),
inference(resolution,[status(thm)],[f391,f287]) ).
fof(f1274,plain,
! [X0] :
( ~ c3_1(a309)
| ~ ndr1_0
| ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp11
| ~ c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1265,f246]) ).
fof(f1276,plain,
! [X0] :
( ~ hskp12
| ~ c1_1(a310)
| ~ c0_1(X0)
| ~ c3_1(X0)
| ~ ndr1_0
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1262,f245]) ).
fof(f1504,plain,
! [X0] :
( ~ hskp21
| c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(a336)
| ~ ndr1_0
| ~ c3_1(a336)
| c1_1(X0)
| hskp1 ),
inference(resolution,[status(thm)],[f361,f273]) ).
fof(f1510,plain,
! [X0] :
( ~ hskp16
| c0_1(X0)
| ~ c2_1(X0)
| ~ c2_1(a321)
| ~ ndr1_0
| ~ c3_1(a321)
| c1_1(X0)
| hskp1 ),
inference(resolution,[status(thm)],[f361,f280]) ).
fof(f1512,plain,
! [X0] :
( ~ hskp21
| c1_1(X0)
| ~ ndr1_0
| ~ c2_1(X0)
| c0_1(X0)
| ~ c2_1(a336)
| hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1504,f231]) ).
fof(f1513,plain,
! [X0] :
( ~ hskp16
| ~ ndr1_0
| ~ c2_1(a321)
| c0_1(X0)
| ~ c2_1(X0)
| hskp1
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1510,f239]) ).
fof(f1526,plain,
! [X0] :
( ~ hskp12
| ~ c0_1(X0)
| c2_1(X0)
| hskp0
| ~ c1_1(X0)
| ~ ndr1_0
| c2_1(a310)
| c1_1(a310) ),
inference(resolution,[status(thm)],[f351,f285]) ).
fof(f1530,plain,
! [X0] :
( ~ hskp12
| ~ ndr1_0
| hskp0
| c1_1(a310)
| c2_1(X0)
| ~ c0_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1526,f286]) ).
fof(f1649,plain,
! [X0] :
( ~ hskp2
| c0_1(a297)
| ~ c1_1(X0)
| hskp8
| ~ c2_1(X0)
| c3_1(X0)
| ~ c2_1(a297)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f375,f303]) ).
fof(f1663,plain,
! [X0] :
( ~ hskp2
| c0_1(a297)
| c3_1(X0)
| ~ c2_1(X0)
| hskp8
| ~ c2_1(a297)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1649,f209]) ).
fof(f1793,plain,
! [X0] :
( ~ hskp26
| hskp12
| c0_1(X0)
| ~ c1_1(X0)
| c2_1(a349)
| ~ c2_1(X0)
| ~ c0_1(a349)
| ~ ndr1_0 ),
inference(resolution,[status(thm)],[f377,f262]) ).
fof(f1812,plain,
! [X0] :
( c2_1(a349)
| hskp12
| ~ hskp26
| ~ c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0)
| ~ c0_1(a349) ),
inference(forward_subsumption_resolution,[status(thm)],[f1793,f185]) ).
fof(f1825,plain,
! [X0] :
( ~ c0_1(X0)
| ~ c2_1(X0)
| ~ hskp11
| ~ c3_1(X0)
| ~ c3_1(a309) ),
inference(forward_subsumption_resolution,[status(thm)],[f1274,f200]) ).
fof(f1827,plain,
! [X0] :
( ~ hskp11
| ~ c0_1(X0)
| ~ c2_1(X0)
| ~ hskp11
| ~ c3_1(X0) ),
inference(resolution,[status(thm)],[f1825,f247]) ).
fof(f1911,plain,
! [X0] :
( ~ c2_1(X0)
| ~ c0_1(X0)
| ~ hskp11
| ~ c3_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1827]) ).
fof(f1944,plain,
( ~ hskp16
| ~ c2_1(a321)
| ~ c0_1(a321)
| ~ hskp11 ),
inference(resolution,[status(thm)],[f1911,f239]) ).
fof(f1972,plain,
( ~ hskp16
| ~ c0_1(a321)
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f1944,f238]) ).
fof(f2061,plain,
( ~ c3_1(a321)
| c1_1(a321)
| hskp2
| hskp0
| ~ ndr1_0
| ~ hskp16
| ~ hskp11 ),
inference(resolution,[status(thm)],[f1972,f315]) ).
fof(f2068,plain,
( ~ hskp16
| hskp0
| c1_1(a321)
| ~ c3_1(a321)
| ~ hskp11
| hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f2061,f200]) ).
fof(f2069,plain,
! [X0,X1] :
( c2_1(X0)
| ~ c3_1(X0)
| c3_1(X1)
| ~ hskp0
| c2_1(X1)
| c1_1(X1)
| c1_1(a294)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f423,f306]) ).
fof(f2088,plain,
! [X0] :
( ~ hskp0
| c2_1(X0)
| ~ c3_1(X0)
| ~ hskp0
| c2_1(a294)
| c1_1(a294)
| c1_1(a294)
| ~ c1_1(X0) ),
inference(resolution,[status(thm)],[f2069,f307]) ).
fof(f2101,plain,
! [X0] :
( c2_1(X0)
| ~ c3_1(X0)
| ~ hskp0
| c2_1(a294)
| c1_1(a294)
| ~ c1_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f2088]) ).
fof(f2102,plain,
! [X0] :
( ~ c3_1(X0)
| c1_1(a294)
| ~ hskp0
| ~ c1_1(X0)
| c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2101,f306]) ).
fof(f2172,plain,
! [X0,X1] :
( ~ c3_1(X0)
| c2_1(X1)
| c1_1(a310)
| c3_1(X1)
| c2_1(X0)
| ~ hskp12
| c1_1(X1)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f427,f286]) ).
fof(f2179,plain,
! [X0] :
( ~ hskp11
| ~ c3_1(a309)
| c2_1(X0)
| c1_1(a310)
| c3_1(X0)
| ~ hskp12
| c1_1(X0)
| ~ c1_1(a309) ),
inference(resolution,[status(thm)],[f2172,f287]) ).
fof(f2186,plain,
! [X0] :
( ~ hskp12
| c1_1(X0)
| ~ hskp11
| c3_1(X0)
| ~ c3_1(a309)
| c2_1(X0)
| c1_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f2179,f246]) ).
fof(f2213,plain,
( ~ hskp15
| ~ c3_1(a320)
| c1_1(a294)
| ~ hskp0
| ~ c1_1(a320) ),
inference(resolution,[status(thm)],[f2102,f282]) ).
fof(f2214,plain,
( ~ hskp12
| ~ c3_1(a310)
| c1_1(a294)
| ~ hskp0
| ~ c1_1(a310) ),
inference(resolution,[status(thm)],[f2102,f286]) ).
fof(f2217,plain,
( ~ hskp11
| ~ c3_1(a309)
| c1_1(a294)
| ~ hskp0
| ~ c1_1(a309) ),
inference(resolution,[status(thm)],[f2102,f287]) ).
fof(f2225,plain,
( ~ c3_1(a309)
| ~ hskp0
| c1_1(a294)
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f2217,f246]) ).
fof(f2227,plain,
( ~ c1_1(a310)
| ~ hskp12
| c1_1(a294)
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2214,f245]) ).
fof(f2228,plain,
( ~ c3_1(a320)
| c1_1(a294)
| ~ hskp15
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2213,f240]) ).
fof(f2229,plain,
( ~ hskp0
| c1_1(a294)
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f2225,f247]) ).
fof(f2300,plain,
( ~ hskp11
| ~ hskp16
| c1_1(a321)
| hskp0
| hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f2068,f239]) ).
fof(f2301,plain,
( ~ hskp16
| ~ hskp11
| ~ hskp16
| hskp0
| hskp2 ),
inference(resolution,[status(thm)],[f2300,f280]) ).
fof(f2302,plain,
( hskp0
| ~ hskp11
| hskp2
| ~ hskp16 ),
inference(duplicate_literals_removal,[status(thm)],[f2301]) ).
fof(f2456,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(a310)
| ~ c0_1(X0)
| ~ hskp12
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1276,f199]) ).
fof(f2462,plain,
( ~ hskp16
| ~ c1_1(a310)
| ~ c0_1(a321)
| ~ hskp12
| ~ c2_1(a321) ),
inference(resolution,[status(thm)],[f2456,f239]) ).
fof(f2493,plain,
( ~ c1_1(a310)
| ~ c0_1(a321)
| ~ hskp16
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f2462,f238]) ).
fof(f2518,plain,
( ~ c3_1(a321)
| c1_1(a321)
| hskp2
| hskp0
| ~ ndr1_0
| ~ c1_1(a310)
| ~ hskp16
| ~ hskp12 ),
inference(resolution,[status(thm)],[f2493,f315]) ).
fof(f2524,plain,
( ~ hskp12
| hskp2
| c1_1(a321)
| ~ hskp16
| ~ c3_1(a321)
| hskp0
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f2518,f885]) ).
fof(f2603,plain,
! [X0,X1] :
( c1_1(X1)
| ~ ndr1_0
| c0_1(X1)
| ~ hskp0
| c2_1(X1)
| ~ c1_1(X0)
| ~ c2_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f453,f306]) ).
fof(f2619,plain,
! [X0] :
( ~ hskp10
| c1_1(X0)
| ~ ndr1_0
| c0_1(X0)
| ~ hskp0
| c2_1(X0)
| ~ c1_1(a308)
| ~ c2_1(a308) ),
inference(resolution,[status(thm)],[f2603,f288]) ).
fof(f2622,plain,
! [X0] :
( ~ hskp10
| ~ c2_1(a308)
| ~ hskp0
| ~ ndr1_0
| c1_1(X0)
| c0_1(X0)
| c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2619,f248]) ).
fof(f3204,plain,
( hskp0
| ~ hskp16
| hskp2
| ~ hskp12
| c1_1(a321)
| ~ c3_1(a321) ),
inference(forward_subsumption_resolution,[status(thm)],[f2524,f199]) ).
fof(f3205,plain,
( ~ hskp16
| hskp0
| ~ hskp16
| hskp2
| ~ hskp12
| ~ c3_1(a321) ),
inference(resolution,[status(thm)],[f3204,f280]) ).
fof(f3206,plain,
( hskp0
| ~ hskp16
| hskp2
| ~ hskp12
| ~ c3_1(a321) ),
inference(duplicate_literals_removal,[status(thm)],[f3205]) ).
fof(f3207,plain,
( ~ hskp12
| hskp2
| hskp0
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f3206,f239]) ).
fof(f3640,plain,
! [X0,X1] :
( c2_1(X1)
| c1_1(X1)
| ~ c2_1(X0)
| ~ hskp20
| c0_1(X1)
| c0_1(a333)
| ~ c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f559,f274]) ).
fof(f3660,plain,
! [X0] :
( ~ hskp10
| c2_1(X0)
| c1_1(X0)
| ~ c2_1(a308)
| ~ hskp20
| c0_1(X0)
| c0_1(a333)
| ~ c1_1(a308) ),
inference(resolution,[status(thm)],[f3640,f288]) ).
fof(f3664,plain,
! [X0] :
( c0_1(X0)
| ~ hskp10
| c0_1(a333)
| ~ c2_1(a308)
| c2_1(X0)
| ~ hskp20
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3660,f248]) ).
fof(f3803,plain,
! [X0,X1] :
( c2_1(a297)
| ~ hskp2
| c3_1(X1)
| c2_1(X1)
| ~ c2_1(X0)
| ~ c3_1(X0)
| c0_1(X1)
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f572,f258]) ).
fof(f3810,plain,
! [X0] :
( ~ hskp21
| c2_1(a297)
| ~ hskp2
| c3_1(X0)
| c2_1(X0)
| ~ c2_1(a336)
| ~ c3_1(a336)
| c0_1(X0) ),
inference(resolution,[status(thm)],[f3803,f273]) ).
fof(f3821,plain,
! [X0] :
( c2_1(a297)
| c0_1(X0)
| ~ hskp21
| ~ c2_1(a336)
| c2_1(X0)
| ~ hskp2
| c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3810,f231]) ).
fof(f3826,plain,
! [X0,X1] :
( ~ hskp15
| c0_1(X0)
| ~ c2_1(X1)
| c3_1(X0)
| ~ c1_1(a320)
| c1_1(X1)
| ~ c3_1(X1)
| c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f574,f282]) ).
fof(f3833,plain,
! [X0] :
( ~ hskp21
| ~ hskp15
| c0_1(X0)
| ~ c2_1(a336)
| c3_1(X0)
| ~ c1_1(a320)
| ~ c3_1(a336)
| c2_1(X0) ),
inference(resolution,[status(thm)],[f3826,f273]) ).
fof(f3841,plain,
! [X0] :
( c2_1(X0)
| c3_1(X0)
| ~ hskp15
| ~ hskp21
| c0_1(X0)
| ~ c2_1(a336)
| ~ c1_1(a320) ),
inference(forward_subsumption_resolution,[status(thm)],[f3833,f231]) ).
fof(f3883,plain,
! [X0,X1] :
( ~ c3_1(X1)
| ~ c1_1(a294)
| c2_1(X0)
| ~ c2_1(X1)
| c1_1(X1)
| c3_1(X0)
| ~ hskp0
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f575,f211]) ).
fof(f3902,plain,
! [X0] :
( ~ hskp0
| ~ c3_1(X0)
| ~ c1_1(a294)
| c2_1(a294)
| ~ c2_1(X0)
| c1_1(X0)
| ~ hskp0
| c0_1(a294) ),
inference(resolution,[status(thm)],[f3883,f307]) ).
fof(f3921,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c1_1(a294)
| c2_1(a294)
| ~ c2_1(X0)
| c1_1(X0)
| ~ hskp0
| c0_1(a294) ),
inference(duplicate_literals_removal,[status(thm)],[f3902]) ).
fof(f3922,plain,
! [X0] :
( ~ c2_1(X0)
| ~ c1_1(a294)
| ~ c3_1(X0)
| c1_1(X0)
| ~ hskp0
| c2_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f3921,f305]) ).
fof(f4128,plain,
! [X0,X1] :
( c0_1(X1)
| c2_1(X0)
| ~ hskp12
| ~ c1_1(a310)
| ~ c1_1(X1)
| c3_1(X1)
| ~ c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f599,f199]) ).
fof(f4149,plain,
! [X0] :
( ~ hskp12
| c0_1(X0)
| c2_1(a310)
| ~ hskp12
| ~ c1_1(a310)
| ~ c1_1(X0)
| c3_1(X0)
| ~ c1_1(a310) ),
inference(resolution,[status(thm)],[f4128,f285]) ).
fof(f4152,plain,
! [X0] :
( c0_1(X0)
| c2_1(a310)
| ~ hskp12
| ~ c1_1(X0)
| c3_1(X0)
| ~ c1_1(a310) ),
inference(duplicate_literals_removal,[status(thm)],[f4149]) ).
fof(f4153,plain,
! [X0] :
( ~ hskp12
| ~ c1_1(a310)
| c3_1(X0)
| ~ c1_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4152,f286]) ).
fof(f4190,plain,
( ~ hskp20
| ~ hskp12
| ~ c1_1(a310)
| ~ c1_1(a333)
| c0_1(a333) ),
inference(resolution,[status(thm)],[f4153,f275]) ).
fof(f4193,plain,
( ~ hskp2
| ~ hskp12
| ~ c1_1(a310)
| ~ c1_1(a297)
| c0_1(a297) ),
inference(resolution,[status(thm)],[f4153,f303]) ).
fof(f4194,plain,
( ~ hskp0
| ~ hskp12
| ~ c1_1(a310)
| ~ c1_1(a294)
| c0_1(a294) ),
inference(resolution,[status(thm)],[f4153,f307]) ).
fof(f4208,plain,
( ~ c1_1(a297)
| ~ c1_1(a310)
| ~ hskp12
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4193,f302]) ).
fof(f4210,plain,
( ~ hskp12
| ~ hskp0
| ~ c1_1(a310)
| ~ c1_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f4194,f305]) ).
fof(f4212,plain,
( ~ hskp12
| ~ c1_1(a310)
| c0_1(a333)
| ~ hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f4190,f232]) ).
fof(f4213,plain,
( ~ hskp2
| ~ hskp12
| ~ c1_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f4208,f258]) ).
fof(f4242,plain,
! [X0,X1] :
( c0_1(X1)
| c3_1(X1)
| ~ c1_1(X1)
| ~ hskp10
| c2_1(X0)
| c0_1(X0)
| ~ c1_1(a308)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f600,f201]) ).
fof(f4256,plain,
! [X0] :
( ~ hskp2
| c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ hskp10
| c2_1(a297)
| ~ c1_1(a308)
| ~ c1_1(a297) ),
inference(resolution,[status(thm)],[f4242,f302]) ).
fof(f4261,plain,
! [X0] :
( ~ hskp0
| c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ hskp10
| c2_1(a294)
| ~ c1_1(a308)
| ~ c1_1(a294) ),
inference(resolution,[status(thm)],[f4242,f305]) ).
fof(f4262,plain,
! [X0] :
( ~ hskp10
| c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ hskp10
| c2_1(a308)
| ~ c1_1(a308)
| ~ c1_1(a308) ),
inference(resolution,[status(thm)],[f4242,f288]) ).
fof(f4265,plain,
! [X0] :
( c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ hskp10
| c2_1(a308)
| ~ c1_1(a308) ),
inference(duplicate_literals_removal,[status(thm)],[f4262]) ).
fof(f4266,plain,
! [X0] :
( c2_1(a308)
| ~ c1_1(X0)
| ~ hskp10
| c0_1(X0)
| c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4265,f248]) ).
fof(f4268,plain,
! [X0] :
( ~ hskp0
| ~ c1_1(a294)
| c0_1(X0)
| c2_1(a294)
| ~ c1_1(X0)
| ~ hskp10
| c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4261,f248]) ).
fof(f4269,plain,
! [X0] :
( ~ c1_1(a308)
| c2_1(a297)
| ~ c1_1(X0)
| c3_1(X0)
| ~ hskp2
| ~ hskp10
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4256,f258]) ).
fof(f4271,plain,
( ~ c1_1(a310)
| ~ hskp12
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f4210,f2227]) ).
fof(f4345,plain,
( ~ hskp20
| c2_1(a308)
| ~ c1_1(a333)
| ~ hskp10
| c0_1(a333) ),
inference(resolution,[status(thm)],[f4266,f275]) ).
fof(f4349,plain,
( ~ hskp0
| c2_1(a308)
| ~ c1_1(a294)
| ~ hskp10
| c0_1(a294) ),
inference(resolution,[status(thm)],[f4266,f307]) ).
fof(f4366,plain,
( ~ hskp20
| c0_1(a333)
| c2_1(a308)
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f4345,f232]) ).
fof(f4368,plain,
( c2_1(a308)
| ~ c1_1(a294)
| ~ hskp0
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f4349,f305]) ).
fof(f4378,plain,
! [X0] :
( ~ c1_1(a309)
| hskp12
| c3_1(X0)
| ~ hskp11
| c0_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f728,f200]) ).
fof(f4396,plain,
( ~ hskp2
| ~ c1_1(a309)
| hskp12
| ~ hskp11
| c0_1(a297)
| ~ c1_1(a297) ),
inference(resolution,[status(thm)],[f4378,f303]) ).
fof(f4397,plain,
( ~ hskp0
| ~ c1_1(a309)
| hskp12
| ~ hskp11
| c0_1(a294)
| ~ c1_1(a294) ),
inference(resolution,[status(thm)],[f4378,f307]) ).
fof(f4412,plain,
( c0_1(a297)
| hskp12
| ~ c1_1(a309)
| ~ hskp2
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f4396,f258]) ).
fof(f4413,plain,
( ~ c1_1(a309)
| ~ hskp11
| ~ hskp0
| hskp12
| c0_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f4397,f2229]) ).
fof(f4417,plain,
( ~ hskp11
| ~ hskp2
| hskp12
| c0_1(a297) ),
inference(forward_subsumption_resolution,[status(thm)],[f4412,f246]) ).
fof(f4418,plain,
( ~ hskp2
| ~ hskp11
| ~ hskp2
| hskp12 ),
inference(resolution,[status(thm)],[f4417,f302]) ).
fof(f4419,plain,
( ~ hskp2
| hskp12
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f4418]) ).
fof(f4420,plain,
( ~ hskp11
| ~ hskp0
| hskp12
| ~ c1_1(a309) ),
inference(forward_subsumption_resolution,[status(thm)],[f4413,f305]) ).
fof(f4594,plain,
! [X0] :
( ~ hskp15
| c3_1(X0)
| c0_1(X0)
| hskp12
| ~ c3_1(a320)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f196]) ).
fof(f4613,plain,
( ~ hskp0
| ~ hskp15
| c0_1(a294)
| hskp12
| ~ c3_1(a320)
| ~ c1_1(a294) ),
inference(resolution,[status(thm)],[f4594,f307]) ).
fof(f4630,plain,
( ~ hskp0
| ~ hskp15
| c0_1(a294)
| ~ c3_1(a320)
| hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f4613,f2228]) ).
fof(f4637,plain,
( ~ hskp0
| ~ hskp15
| hskp12
| ~ c3_1(a320) ),
inference(forward_subsumption_resolution,[status(thm)],[f4630,f305]) ).
fof(f5266,plain,
! [X0,X1] :
( ~ hskp25
| c2_1(X1)
| c0_1(X0)
| c3_1(X1)
| c0_1(X1)
| c1_1(a346)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f186]) ).
fof(f5285,plain,
! [X0] :
( ~ hskp0
| ~ hskp25
| c2_1(a294)
| c0_1(X0)
| c0_1(a294)
| c1_1(a346)
| ~ c3_1(X0)
| ~ c2_1(X0) ),
inference(resolution,[status(thm)],[f5266,f307]) ).
fof(f5300,plain,
! [X0] :
( ~ c3_1(X0)
| ~ c2_1(X0)
| ~ hskp25
| ~ hskp0
| c2_1(a294)
| c0_1(X0)
| c0_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f5285,f264]) ).
fof(f5933,plain,
! [X0] :
( ~ hskp15
| ~ c3_1(a320)
| c0_1(X0)
| hskp0
| c1_1(X0)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1000,f240]) ).
fof(f5946,plain,
( ~ hskp21
| ~ hskp15
| ~ c3_1(a320)
| hskp0
| c1_1(a336)
| ~ c3_1(a336) ),
inference(resolution,[status(thm)],[f5933,f272]) ).
fof(f5965,plain,
( ~ hskp15
| ~ c3_1(a320)
| hskp0
| ~ hskp21
| c1_1(a336) ),
inference(forward_subsumption_resolution,[status(thm)],[f5946,f231]) ).
fof(f6007,plain,
! [X0] :
( ~ c1_1(a310)
| c0_1(X0)
| ~ c3_1(a310)
| ~ c3_1(X0)
| c1_1(X0)
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f1002,f4271]) ).
fof(f6020,plain,
( ~ hskp21
| ~ c1_1(a310)
| ~ c3_1(a310)
| ~ c3_1(a336)
| c1_1(a336)
| ~ hskp12 ),
inference(resolution,[status(thm)],[f6007,f272]) ).
fof(f6023,plain,
( ~ hskp8
| ~ c1_1(a310)
| ~ c3_1(a310)
| ~ c3_1(a305)
| c1_1(a305)
| ~ hskp12 ),
inference(resolution,[status(thm)],[f6007,f291]) ).
fof(f6032,plain,
( ~ hskp12
| ~ c3_1(a310)
| ~ hskp21
| ~ c1_1(a310)
| ~ c3_1(a336) ),
inference(forward_subsumption_resolution,[status(thm)],[f6020,f273]) ).
fof(f6033,plain,
( ~ c3_1(a305)
| ~ c1_1(a310)
| ~ hskp12
| ~ hskp8
| ~ c3_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f6023,f292]) ).
fof(f6081,plain,
( hskp0
| ~ hskp21
| ~ hskp15
| ~ c3_1(a320) ),
inference(forward_subsumption_resolution,[status(thm)],[f5965,f273]) ).
fof(f6090,plain,
! [X0] :
( ~ c3_1(a309)
| c1_1(X0)
| ~ c3_1(X0)
| hskp0
| c0_1(X0)
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f1004,f246]) ).
fof(f6103,plain,
( ~ hskp21
| ~ c3_1(a309)
| c1_1(a336)
| ~ c3_1(a336)
| hskp0
| ~ hskp11 ),
inference(resolution,[status(thm)],[f6090,f272]) ).
fof(f6111,plain,
( ~ hskp12
| ~ c3_1(a309)
| c1_1(a310)
| ~ c3_1(a310)
| hskp0
| ~ hskp11 ),
inference(resolution,[status(thm)],[f6090,f285]) ).
fof(f6116,plain,
( ~ c3_1(a309)
| hskp0
| ~ hskp11
| ~ hskp12
| c1_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f6111,f245]) ).
fof(f6122,plain,
( c1_1(a336)
| ~ c3_1(a309)
| hskp0
| ~ hskp21
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f6103,f231]) ).
fof(f6242,plain,
( hskp0
| ~ hskp12
| c1_1(a310)
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f6116,f247]) ).
fof(f6244,plain,
( ~ hskp2
| ~ hskp12
| hskp0
| ~ hskp12
| ~ hskp11 ),
inference(resolution,[status(thm)],[f6242,f4213]) ).
fof(f6247,plain,
( ~ hskp2
| hskp0
| ~ hskp12
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f6244]) ).
fof(f6248,plain,
( ~ hskp11
| ~ hskp2
| hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f6247,f4419]) ).
fof(f6249,plain,
( ~ hskp11
| ~ hskp16
| hskp0 ),
inference(backward_subsumption_resolution,[status(thm)],[f2302,f6248]) ).
fof(f6347,plain,
( c1_1(a336)
| ~ hskp11
| hskp0
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f6122,f247]) ).
fof(f6348,plain,
( ~ hskp21
| ~ hskp11
| hskp0
| ~ hskp21 ),
inference(resolution,[status(thm)],[f6347,f273]) ).
fof(f6349,plain,
( hskp0
| ~ hskp21
| ~ hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f6348]) ).
fof(f6422,plain,
( ~ hskp21
| ~ c1_1(a310)
| ~ c3_1(a310)
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f6032,f231]) ).
fof(f6423,plain,
( ~ hskp12
| ~ hskp21
| ~ c1_1(a310)
| ~ hskp12 ),
inference(resolution,[status(thm)],[f6422,f245]) ).
fof(f6499,plain,
( ~ hskp21
| ~ hskp12
| ~ c1_1(a310) ),
inference(duplicate_literals_removal,[status(thm)],[f6423]) ).
fof(f7023,plain,
( ~ c3_1(a305)
| ~ hskp12
| ~ c1_1(a310)
| ~ hskp8 ),
inference(forward_subsumption_resolution,[status(thm)],[f6033,f245]) ).
fof(f7076,plain,
( hskp11
| hskp16
| c1_1(a305)
| ~ ndr1_0
| ~ c2_1(a305)
| ~ hskp12
| ~ c1_1(a310)
| ~ hskp8 ),
inference(resolution,[status(thm)],[f7023,f325]) ).
fof(f7089,plain,
( c1_1(a305)
| hskp11
| ~ hskp8
| ~ c2_1(a305)
| hskp16
| ~ hskp12
| ~ ndr1_0 ),
inference(forward_subsumption_resolution,[status(thm)],[f7076,f733]) ).
fof(f7822,plain,
( hskp16
| ~ c2_1(a305)
| ~ hskp12
| ~ hskp8
| c1_1(a305)
| hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f7089,f203]) ).
fof(f7823,plain,
( ~ hskp8
| hskp16
| ~ c2_1(a305)
| ~ hskp12
| ~ hskp8
| hskp11 ),
inference(resolution,[status(thm)],[f7822,f292]) ).
fof(f7824,plain,
( hskp16
| ~ c2_1(a305)
| ~ hskp12
| ~ hskp8
| hskp11 ),
inference(duplicate_literals_removal,[status(thm)],[f7823]) ).
fof(f7825,plain,
( hskp11
| ~ hskp8
| ~ hskp12
| hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f7824,f251]) ).
fof(f8245,plain,
! [X0] :
( ~ c2_1(a336)
| ~ hskp21
| hskp1
| c1_1(X0)
| c0_1(X0)
| ~ c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1512,f190]) ).
fof(f8265,plain,
( ~ hskp21
| ~ c2_1(a336)
| ~ hskp21
| hskp1
| c1_1(a336)
| ~ c2_1(a336) ),
inference(resolution,[status(thm)],[f8245,f272]) ).
fof(f8278,plain,
( ~ hskp21
| hskp1
| c1_1(a336)
| ~ c2_1(a336) ),
inference(duplicate_literals_removal,[status(thm)],[f8265]) ).
fof(f8279,plain,
( hskp1
| ~ c2_1(a336)
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f8278,f273]) ).
fof(f8289,plain,
! [X0] :
( ~ ndr1_0
| c0_1(X0)
| ~ hskp16
| c1_1(X0)
| ~ c2_1(X0)
| hskp1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1513,f238]) ).
fof(f8312,plain,
( ~ hskp8
| ~ ndr1_0
| ~ hskp16
| c1_1(a305)
| ~ c2_1(a305)
| hskp1 ),
inference(resolution,[status(thm)],[f8289,f291]) ).
fof(f8328,plain,
( hskp1
| ~ hskp8
| ~ ndr1_0
| ~ hskp16
| c1_1(a305) ),
inference(forward_subsumption_resolution,[status(thm)],[f8312,f251]) ).
fof(f8339,plain,
( ~ ndr1_0
| ~ hskp8
| hskp1
| ~ hskp16 ),
inference(forward_subsumption_resolution,[status(thm)],[f8328,f292]) ).
fof(f8539,plain,
! [X0] :
( ~ c1_1(X0)
| ~ hskp12
| hskp0
| ~ c0_1(X0)
| c1_1(a310)
| c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1530,f199]) ).
fof(f8549,plain,
( ~ hskp20
| ~ c1_1(a333)
| ~ hskp12
| hskp0
| ~ c0_1(a333)
| c1_1(a310) ),
inference(resolution,[status(thm)],[f8539,f274]) ).
fof(f8559,plain,
( hskp0
| ~ hskp12
| ~ hskp20
| c1_1(a310)
| ~ c0_1(a333) ),
inference(forward_subsumption_resolution,[status(thm)],[f8549,f232]) ).
fof(f8656,plain,
( ~ hskp21
| ~ hskp12
| hskp0
| ~ hskp12
| ~ hskp20
| ~ c0_1(a333) ),
inference(resolution,[status(thm)],[f8559,f6499]) ).
fof(f8661,plain,
( ~ hskp21
| hskp0
| ~ hskp12
| ~ hskp20
| ~ c0_1(a333) ),
inference(duplicate_literals_removal,[status(thm)],[f8656]) ).
fof(f8662,plain,
( ~ hskp20
| ~ hskp12
| hskp0
| ~ c0_1(a333) ),
inference(forward_subsumption_resolution,[status(thm)],[f8661,f771]) ).
fof(f8902,plain,
! [X0] :
( ~ hskp2
| hskp8
| ~ c2_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ c2_1(a297) ),
inference(forward_subsumption_resolution,[status(thm)],[f1663,f302]) ).
fof(f8922,plain,
( ~ hskp2
| ~ hskp2
| hskp8
| ~ c2_1(a297)
| ~ c1_1(a297)
| ~ c2_1(a297) ),
inference(resolution,[status(thm)],[f8902,f303]) ).
fof(f8945,plain,
( ~ hskp2
| hskp8
| ~ c1_1(a297)
| ~ c2_1(a297) ),
inference(duplicate_literals_removal,[status(thm)],[f8922]) ).
fof(f8946,plain,
( hskp8
| ~ hskp2
| ~ c2_1(a297) ),
inference(forward_subsumption_resolution,[status(thm)],[f8945,f258]) ).
fof(f9076,plain,
! [X0] :
( c2_1(a349)
| ~ c2_1(X0)
| ~ hskp26
| c0_1(X0)
| ~ c1_1(X0)
| hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f1812,f227]) ).
fof(f9097,plain,
( ~ hskp2
| c2_1(a349)
| ~ c2_1(a297)
| ~ hskp26
| ~ c1_1(a297)
| hskp12 ),
inference(resolution,[status(thm)],[f9076,f302]) ).
fof(f9112,plain,
( ~ hskp26
| c2_1(a349)
| ~ c2_1(a297)
| hskp12
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f9097,f258]) ).
fof(f9172,plain,
( hskp12
| ~ c2_1(a297)
| ~ hskp2
| ~ hskp26 ),
inference(forward_subsumption_resolution,[status(thm)],[f9112,f261]) ).
fof(f11167,plain,
! [X0] :
( ~ hskp10
| ~ c2_1(a308)
| ~ hskp0
| c0_1(X0)
| c2_1(X0)
| c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2622,f211]) ).
fof(f11189,plain,
( ~ hskp21
| ~ hskp10
| ~ c2_1(a308)
| ~ hskp0
| c2_1(a336)
| c1_1(a336) ),
inference(resolution,[status(thm)],[f11167,f272]) ).
fof(f11195,plain,
( ~ hskp0
| ~ hskp10
| ~ c2_1(a308)
| ~ hskp0
| c2_1(a294)
| c1_1(a294) ),
inference(resolution,[status(thm)],[f11167,f305]) ).
fof(f11197,plain,
( ~ hskp12
| ~ hskp10
| ~ c2_1(a308)
| ~ hskp0
| c2_1(a310)
| c1_1(a310) ),
inference(resolution,[status(thm)],[f11167,f285]) ).
fof(f11199,plain,
( ~ hskp10
| ~ c2_1(a308)
| ~ hskp0
| c2_1(a294)
| c1_1(a294) ),
inference(duplicate_literals_removal,[status(thm)],[f11195]) ).
fof(f11200,plain,
( ~ hskp10
| ~ hskp0
| c1_1(a294)
| ~ c2_1(a308) ),
inference(forward_subsumption_resolution,[status(thm)],[f11199,f306]) ).
fof(f11201,plain,
( ~ c2_1(a308)
| ~ hskp10
| c2_1(a310)
| ~ hskp0
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f11197,f4271]) ).
fof(f11203,plain,
( ~ c2_1(a308)
| ~ hskp21
| ~ hskp0
| ~ hskp10
| c2_1(a336) ),
inference(forward_subsumption_resolution,[status(thm)],[f11189,f273]) ).
fof(f11204,plain,
( ~ c2_1(a308)
| ~ hskp0
| ~ hskp12
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f11201,f286]) ).
fof(f11226,plain,
( ~ c1_1(a294)
| ~ hskp0
| ~ hskp10
| ~ hskp0
| ~ hskp12
| ~ hskp10 ),
inference(resolution,[status(thm)],[f11204,f4368]) ).
fof(f11246,plain,
( ~ c3_1(a308)
| c1_1(a294)
| ~ hskp0
| ~ c1_1(a308)
| ~ hskp0
| ~ hskp12
| ~ hskp10 ),
inference(resolution,[status(thm)],[f11204,f2102]) ).
fof(f11286,plain,
( ~ c3_1(a308)
| c1_1(a294)
| ~ c1_1(a308)
| ~ hskp0
| ~ hskp12
| ~ hskp10 ),
inference(duplicate_literals_removal,[status(thm)],[f11246]) ).
fof(f11287,plain,
( ~ c3_1(a308)
| ~ hskp12
| c1_1(a294)
| ~ hskp0
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f11286,f248]) ).
fof(f11293,plain,
( ~ hskp12
| ~ hskp0
| ~ hskp10
| ~ c1_1(a294) ),
inference(duplicate_literals_removal,[status(thm)],[f11226]) ).
fof(f12458,plain,
( ~ c3_1(a308)
| ~ hskp10
| ~ hskp12
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f11287,f11293]) ).
fof(f12459,plain,
( ~ hskp10
| ~ hskp10
| ~ hskp12
| ~ hskp0 ),
inference(resolution,[status(thm)],[f12458,f249]) ).
fof(f12563,plain,
( ~ hskp10
| ~ hskp0
| ~ hskp12 ),
inference(duplicate_literals_removal,[status(thm)],[f12459]) ).
fof(f12571,plain,
( hskp11
| ~ hskp12
| ~ hskp0
| ~ hskp12 ),
inference(resolution,[status(thm)],[f12563,f893]) ).
fof(f12573,plain,
( ~ hskp0
| hskp11
| ~ hskp12 ),
inference(duplicate_literals_removal,[status(thm)],[f12571]) ).
fof(f12789,plain,
! [X0] :
( c1_1(a310)
| c2_1(X0)
| ~ hskp11
| c1_1(X0)
| ~ hskp12
| c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2186,f247]) ).
fof(f12814,plain,
( ~ hskp22
| c1_1(a310)
| c2_1(a338)
| ~ hskp11
| c1_1(a338)
| ~ hskp12 ),
inference(resolution,[status(thm)],[f12789,f271]) ).
fof(f12838,plain,
( c1_1(a310)
| ~ hskp11
| ~ hskp12
| ~ hskp22
| c2_1(a338) ),
inference(forward_subsumption_resolution,[status(thm)],[f12814,f269]) ).
fof(f13162,plain,
( ~ hskp12
| c1_1(a310)
| ~ hskp11
| ~ hskp22 ),
inference(forward_subsumption_resolution,[status(thm)],[f12838,f270]) ).
fof(f13165,plain,
( ~ hskp12
| ~ hskp0
| ~ hskp12
| ~ hskp11
| ~ hskp22 ),
inference(resolution,[status(thm)],[f13162,f4271]) ).
fof(f13172,plain,
( ~ hskp0
| ~ hskp12
| ~ hskp11
| ~ hskp22 ),
inference(duplicate_literals_removal,[status(thm)],[f13165]) ).
fof(f13173,plain,
( ~ hskp0
| ~ hskp22
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f13172,f12573]) ).
fof(f13193,plain,
( ~ hskp0
| ~ c1_1(a294)
| ~ hskp0
| ~ hskp12 ),
inference(resolution,[status(thm)],[f13173,f753]) ).
fof(f13195,plain,
( ~ hskp20
| ~ ndr1_0
| ~ hskp0
| ~ hskp12 ),
inference(resolution,[status(thm)],[f13173,f751]) ).
fof(f13201,plain,
( ~ c1_1(a294)
| ~ hskp12
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f13193]) ).
fof(f13202,plain,
( ~ hskp20
| ~ hskp12
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13195,f199]) ).
fof(f13205,plain,
( ~ c0_1(a333)
| ~ hskp12
| ~ hskp20 ),
inference(backward_subsumption_resolution,[status(thm)],[f8662,f13202]) ).
fof(f13264,plain,
( ~ c3_1(a320)
| ~ hskp15
| ~ hskp0
| ~ hskp12
| ~ hskp0 ),
inference(resolution,[status(thm)],[f13201,f2228]) ).
fof(f13266,plain,
( ~ hskp0
| ~ hskp11
| ~ hskp12
| ~ hskp0 ),
inference(resolution,[status(thm)],[f13201,f2229]) ).
fof(f13293,plain,
( ~ hskp11
| ~ hskp12
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f13266]) ).
fof(f13294,plain,
( ~ hskp0
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f13293,f12573]) ).
fof(f13296,plain,
( ~ c3_1(a320)
| ~ hskp15
| ~ hskp12
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f13264]) ).
fof(f13297,plain,
( ~ hskp15
| ~ c3_1(a320)
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f13296,f4637]) ).
fof(f13305,plain,
( ~ hskp11
| ~ hskp0
| ~ c1_1(a309) ),
inference(backward_subsumption_resolution,[status(thm)],[f4420,f13294]) ).
fof(f13313,plain,
( ~ hskp16
| hskp2
| ~ hskp12 ),
inference(backward_subsumption_resolution,[status(thm)],[f3207,f13294]) ).
fof(f13354,plain,
( ~ hskp0
| ~ hskp11 ),
inference(forward_subsumption_resolution,[status(thm)],[f13305,f246]) ).
fof(f13365,plain,
( ~ hskp21
| ~ hskp11 ),
inference(backward_subsumption_resolution,[status(thm)],[f6349,f13354]) ).
fof(f13366,plain,
( ~ hskp11
| ~ hskp16 ),
inference(backward_subsumption_resolution,[status(thm)],[f6249,f13354]) ).
fof(f13420,plain,
( hskp26
| ~ hskp11 ),
inference(resolution,[status(thm)],[f13366,f181]) ).
fof(f13425,plain,
( ~ hskp21
| c2_1(a336)
| hskp10 ),
inference(backward_subsumption_resolution,[status(thm)],[f894,f13365]) ).
fof(f13435,plain,
( ~ hskp26
| ~ ndr1_0
| ~ hskp11 ),
inference(resolution,[status(thm)],[f13365,f770]) ).
fof(f13436,plain,
( ~ hskp11
| ~ hskp26 ),
inference(forward_subsumption_resolution,[status(thm)],[f13435,f185]) ).
fof(f13438,plain,
( hskp12
| hskp26 ),
inference(backward_subsumption_resolution,[status(thm)],[f216,f13420]) ).
fof(f13518,plain,
( hskp16
| ~ hskp8
| ~ hskp12 ),
inference(backward_subsumption_resolution,[status(thm)],[f7825,f13540]) ).
fof(f13528,plain,
( hskp20
| ~ ndr1_0
| ~ hskp1 ),
inference(backward_subsumption_resolution,[status(thm)],[f953,f13540]) ).
fof(f13533,plain,
( ~ hskp12
| hskp10 ),
inference(backward_subsumption_resolution,[status(thm)],[f893,f13540]) ).
fof(f13540,plain,
~ hskp11,
inference(forward_subsumption_resolution,[status(thm)],[f13436,f13420]) ).
fof(f13541,plain,
( ~ hskp1
| hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f13528,f210]) ).
fof(f13550,plain,
( ~ hskp2
| hskp12
| ~ c2_1(a297) ),
inference(backward_subsumption_resolution,[status(thm)],[f9172,f13438]) ).
fof(f13844,plain,
( ~ hskp0
| c2_1(a336)
| ~ c2_1(a308)
| ~ hskp21 ),
inference(backward_subsumption_resolution,[status(thm)],[f11203,f13425]) ).
fof(f13939,plain,
( ~ hskp12
| ~ c1_1(a310)
| ~ hskp20 ),
inference(backward_subsumption_resolution,[status(thm)],[f4212,f13205]) ).
fof(f14028,plain,
( ~ hskp21
| ~ hskp15
| ~ c3_1(a320) ),
inference(backward_subsumption_resolution,[status(thm)],[f6081,f13297]) ).
fof(f14676,plain,
( c2_1(a308)
| ~ c1_1(a320)
| ~ hskp10
| c0_1(a320)
| ~ hskp21
| ~ hskp15 ),
inference(resolution,[status(thm)],[f14028,f4266]) ).
fof(f14716,plain,
( ~ hskp10
| ~ c1_1(a320)
| c2_1(a308)
| ~ hskp21
| ~ hskp15 ),
inference(forward_subsumption_resolution,[status(thm)],[f14676,f281]) ).
fof(f23319,plain,
( ~ hskp21
| ~ hskp10
| c2_1(a308)
| ~ hskp15 ),
inference(forward_subsumption_resolution,[status(thm)],[f14716,f240]) ).
fof(f23954,plain,
! [X0] :
( ~ hskp10
| c0_1(X0)
| ~ hskp20
| c1_1(X0)
| c0_1(a333)
| c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3664,f4366]) ).
fof(f23962,plain,
! [X0] :
( ~ hskp12
| ~ hskp20
| ~ hskp10
| c0_1(X0)
| ~ hskp20
| c1_1(X0)
| c2_1(X0) ),
inference(resolution,[status(thm)],[f23954,f13205]) ).
fof(f23964,plain,
! [X0] :
( ~ hskp12
| ~ hskp10
| c0_1(X0)
| ~ hskp20
| c1_1(X0)
| c2_1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f23962]) ).
fof(f23965,plain,
! [X0] :
( c0_1(X0)
| ~ hskp20
| c1_1(X0)
| ~ hskp12
| c2_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f23964,f13533]) ).
fof(f24115,plain,
( ~ hskp12
| ~ hskp20
| c1_1(a310)
| ~ hskp12
| c2_1(a310) ),
inference(resolution,[status(thm)],[f23965,f285]) ).
fof(f24124,plain,
( ~ hskp20
| c1_1(a310)
| ~ hskp12
| c2_1(a310) ),
inference(duplicate_literals_removal,[status(thm)],[f24115]) ).
fof(f24125,plain,
( ~ hskp20
| ~ hskp12
| c1_1(a310) ),
inference(forward_subsumption_resolution,[status(thm)],[f24124,f286]) ).
fof(f24187,plain,
( ~ hskp12
| ~ hskp20 ),
inference(forward_subsumption_resolution,[status(thm)],[f24125,f13939]) ).
fof(f24192,plain,
( ~ hskp1
| ~ hskp12 ),
inference(resolution,[status(thm)],[f24187,f13541]) ).
fof(f24195,plain,
( ~ c0_1(a295)
| ~ hskp1
| hskp19 ),
inference(backward_subsumption_resolution,[status(thm)],[f713,f24192]) ).
fof(f24211,plain,
( ~ ndr1_0
| ~ hskp8
| ~ hskp16
| ~ hskp12 ),
inference(resolution,[status(thm)],[f24192,f8339]) ).
fof(f24214,plain,
( ~ hskp1
| hskp19 ),
inference(forward_subsumption_resolution,[status(thm)],[f24195,f259]) ).
fof(f24215,plain,
( ~ ndr1_0
| ~ hskp8
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f24211,f13518]) ).
fof(f24234,plain,
( ~ hskp8
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f24215,f203]) ).
fof(f24242,plain,
( ~ hskp2
| ~ c2_1(a297)
| ~ hskp12 ),
inference(resolution,[status(thm)],[f24234,f8946]) ).
fof(f24258,plain,
( ~ hskp2
| ~ c2_1(a297) ),
inference(forward_subsumption_resolution,[status(thm)],[f24242,f13550]) ).
fof(f27584,plain,
! [X0] :
( c2_1(X0)
| ~ c2_1(a336)
| ~ hskp2
| ~ hskp21
| c3_1(X0)
| c0_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3821,f24258]) ).
fof(f27635,plain,
( ~ hskp2
| c2_1(a297)
| ~ c2_1(a336)
| ~ hskp2
| ~ hskp21
| c0_1(a297) ),
inference(resolution,[status(thm)],[f27584,f303]) ).
fof(f27664,plain,
( c2_1(a297)
| ~ c2_1(a336)
| ~ hskp2
| ~ hskp21
| c0_1(a297) ),
inference(duplicate_literals_removal,[status(thm)],[f27635]) ).
fof(f27665,plain,
( ~ c2_1(a336)
| ~ hskp21
| ~ hskp2
| c2_1(a297) ),
inference(forward_subsumption_resolution,[status(thm)],[f27664,f302]) ).
fof(f27803,plain,
! [X0] :
( c3_1(X0)
| c0_1(X0)
| c2_1(X0)
| ~ hskp15
| ~ hskp21
| ~ c2_1(a336) ),
inference(forward_subsumption_resolution,[status(thm)],[f3841,f240]) ).
fof(f27841,plain,
( ~ hskp21
| ~ hskp15
| c0_1(a320)
| c2_1(a320)
| ~ hskp15
| ~ hskp21
| ~ c2_1(a336) ),
inference(resolution,[status(thm)],[f27803,f14028]) ).
fof(f27882,plain,
( c0_1(a320)
| c2_1(a320)
| ~ hskp15
| ~ hskp21
| ~ c2_1(a336) ),
inference(duplicate_literals_removal,[status(thm)],[f27841]) ).
fof(f27883,plain,
( ~ c2_1(a336)
| ~ hskp21
| c0_1(a320)
| ~ hskp15 ),
inference(forward_subsumption_resolution,[status(thm)],[f27882,f282]) ).
fof(f28638,plain,
! [X0] :
( ~ c2_1(X0)
| ~ hskp0
| c1_1(X0)
| ~ c1_1(a294)
| ~ c3_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3922,f306]) ).
fof(f28679,plain,
( ~ hskp21
| ~ c2_1(a336)
| ~ hskp0
| ~ c1_1(a294)
| ~ c3_1(a336) ),
inference(resolution,[status(thm)],[f28638,f273]) ).
fof(f28693,plain,
( ~ hskp21
| ~ c1_1(a294)
| ~ hskp0
| ~ c2_1(a336) ),
inference(forward_subsumption_resolution,[status(thm)],[f28679,f231]) ).
fof(f33263,plain,
! [X0] :
( ~ hskp10
| ~ c1_1(a294)
| ~ hskp0
| c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4268,f306]) ).
fof(f33329,plain,
( ~ hskp0
| ~ hskp10
| ~ c1_1(a294)
| ~ hskp0
| c0_1(a294)
| ~ c1_1(a294) ),
inference(resolution,[status(thm)],[f33263,f307]) ).
fof(f33361,plain,
( ~ hskp10
| ~ hskp0
| c0_1(a294)
| ~ c1_1(a294) ),
inference(duplicate_literals_removal,[status(thm)],[f33329]) ).
fof(f33362,plain,
( ~ hskp10
| ~ c1_1(a294)
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f33361,f305]) ).
fof(f33378,plain,
( ~ hskp10
| ~ hskp0
| ~ c2_1(a308) ),
inference(backward_subsumption_resolution,[status(thm)],[f11200,f33362]) ).
fof(f33449,plain,
! [X0] :
( ~ c1_1(a308)
| c0_1(X0)
| c3_1(X0)
| ~ c1_1(X0)
| ~ hskp10
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f4269,f24258]) ).
fof(f33514,plain,
( ~ hskp2
| ~ c1_1(a308)
| c0_1(a297)
| ~ c1_1(a297)
| ~ hskp10
| ~ hskp2 ),
inference(resolution,[status(thm)],[f33449,f303]) ).
fof(f33542,plain,
( ~ c1_1(a308)
| c0_1(a297)
| ~ c1_1(a297)
| ~ hskp10
| ~ hskp2 ),
inference(duplicate_literals_removal,[status(thm)],[f33514]) ).
fof(f33543,plain,
( c0_1(a297)
| ~ hskp10
| ~ c1_1(a308)
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f33542,f258]) ).
fof(f33608,plain,
( ~ c3_1(a308)
| c1_1(a294)
| ~ hskp0
| ~ c1_1(a308)
| ~ hskp10
| ~ hskp0 ),
inference(resolution,[status(thm)],[f33378,f2102]) ).
fof(f33626,plain,
( ~ c3_1(a308)
| c1_1(a294)
| ~ c1_1(a308)
| ~ hskp10
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f33608]) ).
fof(f33627,plain,
( ~ c3_1(a308)
| ~ hskp10
| c1_1(a294)
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f33626,f248]) ).
fof(f36907,plain,
( ~ hskp21
| ~ c2_1(a336)
| ~ hskp2 ),
inference(forward_subsumption_resolution,[status(thm)],[f27665,f24258]) ).
fof(f36909,plain,
( ~ hskp21
| hskp10
| ~ hskp21
| ~ hskp2 ),
inference(resolution,[status(thm)],[f36907,f13425]) ).
fof(f36946,plain,
( ~ hskp2
| ~ hskp21
| hskp10 ),
inference(duplicate_literals_removal,[status(thm)],[f36909]) ).
fof(f37358,plain,
( ~ hskp15
| ~ hskp21
| ~ c2_1(a336) ),
inference(forward_subsumption_resolution,[status(thm)],[f27883,f281]) ).
fof(f37359,plain,
( ~ hskp0
| ~ c2_1(a308)
| ~ hskp21
| ~ hskp15
| ~ hskp21 ),
inference(resolution,[status(thm)],[f37358,f13844]) ).
fof(f37360,plain,
( ~ hskp21
| hskp10
| ~ hskp15
| ~ hskp21 ),
inference(resolution,[status(thm)],[f37358,f13425]) ).
fof(f37396,plain,
( ~ hskp21
| hskp10
| ~ hskp15 ),
inference(duplicate_literals_removal,[status(thm)],[f37360]) ).
fof(f37400,plain,
( ~ c2_1(a308)
| ~ hskp21
| ~ hskp0
| ~ hskp15 ),
inference(duplicate_literals_removal,[status(thm)],[f37359]) ).
fof(f37409,plain,
( c2_1(a308)
| ~ hskp15
| ~ hskp21 ),
inference(backward_subsumption_resolution,[status(thm)],[f23319,f37396]) ).
fof(f38435,plain,
( ~ hskp0
| ~ hskp21
| ~ hskp15 ),
inference(forward_subsumption_resolution,[status(thm)],[f37400,f37409]) ).
fof(f38450,plain,
( ~ hskp26
| ~ ndr1_0
| ~ hskp0
| ~ hskp15 ),
inference(resolution,[status(thm)],[f38435,f770]) ).
fof(f38459,plain,
( ~ hskp15
| ~ hskp0
| ~ hskp26 ),
inference(forward_subsumption_resolution,[status(thm)],[f38450,f185]) ).
fof(f41258,plain,
( ~ hskp21
| hskp10
| ~ hskp21
| ~ c1_1(a294)
| ~ hskp0 ),
inference(resolution,[status(thm)],[f28693,f13425]) ).
fof(f41296,plain,
( hskp10
| ~ hskp21
| ~ c1_1(a294)
| ~ hskp0 ),
inference(duplicate_literals_removal,[status(thm)],[f41258]) ).
fof(f41297,plain,
( ~ hskp21
| ~ c1_1(a294)
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f41296,f33362]) ).
fof(f42226,plain,
! [X0] :
( ~ hskp0
| ~ c2_1(X0)
| c0_1(X0)
| ~ hskp25
| ~ c3_1(X0)
| c2_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f5300,f305]) ).
fof(f42259,plain,
( ~ hskp21
| ~ hskp0
| ~ c2_1(a336)
| ~ hskp25
| ~ c3_1(a336)
| c2_1(a294) ),
inference(resolution,[status(thm)],[f42226,f272]) ).
fof(f42270,plain,
( ~ hskp25
| ~ c3_1(a336)
| ~ c2_1(a336)
| ~ hskp0
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f42259,f306]) ).
fof(f45077,plain,
( c0_1(a297)
| ~ hskp2
| ~ hskp10 ),
inference(forward_subsumption_resolution,[status(thm)],[f33543,f248]) ).
fof(f45078,plain,
( ~ hskp2
| ~ hskp2
| ~ hskp10 ),
inference(resolution,[status(thm)],[f45077,f302]) ).
fof(f45086,plain,
( ~ hskp2
| ~ hskp10 ),
inference(duplicate_literals_removal,[status(thm)],[f45078]) ).
fof(f45093,plain,
( ~ hskp21
| ~ hskp2 ),
inference(backward_subsumption_resolution,[status(thm)],[f36946,f45086]) ).
fof(f45100,plain,
( ~ hskp16
| ~ hskp12
| ~ hskp10 ),
inference(resolution,[status(thm)],[f45086,f13313]) ).
fof(f45105,plain,
( ~ hskp16
| ~ hskp12 ),
inference(forward_subsumption_resolution,[status(thm)],[f45100,f13533]) ).
fof(f45154,plain,
( hskp26
| ~ hskp12 ),
inference(resolution,[status(thm)],[f45105,f181]) ).
fof(f45157,plain,
hskp26,
inference(forward_subsumption_resolution,[status(thm)],[f45154,f13438]) ).
fof(f45164,plain,
( ~ hskp0
| ~ hskp15 ),
inference(backward_subsumption_resolution,[status(thm)],[f38459,f45157]) ).
fof(f45196,plain,
( hskp21
| ~ ndr1_0 ),
inference(backward_subsumption_resolution,[status(thm)],[f770,f45157]) ).
fof(f45201,plain,
ndr1_0,
inference(backward_subsumption_resolution,[status(thm)],[f185,f45157]) ).
fof(f45365,plain,
( hskp0
| ~ c3_1(a336)
| ~ hskp21 ),
inference(backward_subsumption_resolution,[status(thm)],[f887,f45093]) ).
fof(f45368,plain,
( hskp0
| ~ hskp21 ),
inference(forward_subsumption_resolution,[status(thm)],[f45365,f231]) ).
fof(f45387,plain,
( ~ c1_1(a294)
| ~ hskp0 ),
inference(backward_subsumption_resolution,[status(thm)],[f41297,f45420]) ).
fof(f45405,plain,
( hskp10
| c2_1(a336) ),
inference(backward_subsumption_resolution,[status(thm)],[f13425,f45420]) ).
fof(f45408,plain,
( hskp1
| ~ c2_1(a336) ),
inference(backward_subsumption_resolution,[status(thm)],[f8279,f45420]) ).
fof(f45417,plain,
c3_1(a336),
inference(backward_subsumption_resolution,[status(thm)],[f231,f45420]) ).
fof(f45420,plain,
hskp21,
inference(forward_subsumption_resolution,[status(thm)],[f45196,f45201]) ).
fof(f45449,plain,
~ hskp15,
inference(backward_subsumption_resolution,[status(thm)],[f45164,f45498]) ).
fof(f45498,plain,
hskp0,
inference(forward_subsumption_resolution,[status(thm)],[f45368,f45420]) ).
fof(f45501,plain,
( hskp25
| ~ c2_1(a330)
| ~ hskp19 ),
inference(backward_subsumption_resolution,[status(thm)],[f932,f45449]) ).
fof(f45504,plain,
( ~ hskp19
| hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f45501,f234]) ).
fof(f46130,plain,
~ c1_1(a294),
inference(forward_subsumption_resolution,[status(thm)],[f45387,f45498]) ).
fof(f46850,plain,
( ~ c3_1(a308)
| ~ hskp10
| c1_1(a294) ),
inference(forward_subsumption_resolution,[status(thm)],[f33627,f45498]) ).
fof(f46851,plain,
( ~ c3_1(a308)
| ~ hskp10 ),
inference(resolution,[status(thm)],[f46850,f46130]) ).
fof(f46852,plain,
~ hskp10,
inference(forward_subsumption_resolution,[status(thm)],[f46851,f249]) ).
fof(f46854,plain,
c2_1(a336),
inference(backward_subsumption_resolution,[status(thm)],[f45405,f46852]) ).
fof(f46861,plain,
hskp1,
inference(backward_subsumption_resolution,[status(thm)],[f45408,f46854]) ).
fof(f46864,plain,
hskp19,
inference(backward_subsumption_resolution,[status(thm)],[f24214,f46861]) ).
fof(f46886,plain,
hskp25,
inference(backward_subsumption_resolution,[status(thm)],[f45504,f46864]) ).
fof(f47690,plain,
( ~ c2_1(a336)
| ~ hskp0
| ~ c3_1(a336)
| ~ hskp25 ),
inference(forward_subsumption_resolution,[status(thm)],[f42270,f45420]) ).
fof(f47691,plain,
( ~ c2_1(a336)
| ~ hskp0
| ~ hskp25 ),
inference(resolution,[status(thm)],[f47690,f45417]) ).
fof(f47699,plain,
( ~ c2_1(a336)
| ~ hskp0 ),
inference(forward_subsumption_resolution,[status(thm)],[f47691,f46886]) ).
fof(f47705,plain,
~ c2_1(a336),
inference(forward_subsumption_resolution,[status(thm)],[f47699,f45498]) ).
fof(f47706,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f46854,f47705]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYN445-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n005.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 10:57:18 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 225.49/29.05 % Refutation found
% 225.49/29.05 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 225.49/29.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 50.09/29.08 % Elapsed time: 28.638136 seconds
% 50.09/29.08 % CPU time: 226.664611 seconds
% 50.09/29.08 % Total memory used: 138.983 MB
% 50.09/29.08 % Net memory used: 130.473 MB
%------------------------------------------------------------------------------