%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN445-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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 : Sun Sep 27 09:38:15 AM UTC 2026
% Result : Unsatisfiable 192.40s 25.91s
% Output : CNFRefutation 192.40s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(clause1,axiom,
( hskp16
| hskp26 ),
file('theBenchmark.p',clause1) ).
cnf(c_1,plain,
( hskp16
| hskp26 ),
inference(clausify,[status(thm)],[clause1]) ).
fof(clause5,axiom,
( ndr1_0
| ~ hskp26 ),
file('theBenchmark.p',clause5) ).
cnf(c_5,plain,
( ndr1_0
| ~ hskp26 ),
inference(clausify,[status(thm)],[clause5]) ).
fof(clause15,axiom,
( ndr1_0
| ~ hskp16 ),
file('theBenchmark.p',clause15) ).
cnf(c_15,plain,
( ndr1_0
| ~ hskp16 ),
inference(clausify,[status(thm)],[clause15]) ).
fof(clause36,axiom,
( hskp12
| hskp11
| hskp26 ),
file('theBenchmark.p',clause36) ).
cnf(c_36,plain,
( hskp12
| hskp11
| hskp26 ),
inference(clausify,[status(thm)],[clause36]) ).
fof(clause41,axiom,
( c1_1(a353)
| ~ hskp28 ),
file('theBenchmark.p',clause41) ).
cnf(c_41,plain,
( c1_1(a353)
| ~ hskp28 ),
inference(clausify,[status(thm)],[clause41]) ).
fof(clause42,axiom,
( c2_1(a353)
| ~ hskp28 ),
file('theBenchmark.p',clause42) ).
cnf(c_42,plain,
( c2_1(a353)
| ~ hskp28 ),
inference(clausify,[status(thm)],[clause42]) ).
fof(clause43,axiom,
( c3_1(a353)
| ~ hskp28 ),
file('theBenchmark.p',clause43) ).
cnf(c_43,plain,
( c3_1(a353)
| ~ hskp28 ),
inference(clausify,[status(thm)],[clause43]) ).
fof(clause47,axiom,
( c0_1(a349)
| ~ hskp26 ),
file('theBenchmark.p',clause47) ).
cnf(c_47,plain,
( c0_1(a349)
| ~ hskp26 ),
inference(clausify,[status(thm)],[clause47]) ).
fof(clause51,axiom,
( c3_1(a336)
| ~ hskp21 ),
file('theBenchmark.p',clause51) ).
cnf(c_51,plain,
( c3_1(a336)
| ~ hskp21 ),
inference(clausify,[status(thm)],[clause51]) ).
fof(clause52,axiom,
( c1_1(a333)
| ~ hskp20 ),
file('theBenchmark.p',clause52) ).
cnf(c_52,plain,
( c1_1(a333)
| ~ hskp20 ),
inference(clausify,[status(thm)],[clause52]) ).
fof(clause53,axiom,
( c1_1(a330)
| ~ hskp19 ),
file('theBenchmark.p',clause53) ).
cnf(c_53,plain,
( c1_1(a330)
| ~ hskp19 ),
inference(clausify,[status(thm)],[clause53]) ).
fof(clause54,axiom,
( c2_1(a330)
| ~ hskp19 ),
file('theBenchmark.p',clause54) ).
cnf(c_54,plain,
( c2_1(a330)
| ~ hskp19 ),
inference(clausify,[status(thm)],[clause54]) ).
fof(clause58,axiom,
( c2_1(a321)
| ~ hskp16 ),
file('theBenchmark.p',clause58) ).
cnf(c_58,plain,
( c2_1(a321)
| ~ hskp16 ),
inference(clausify,[status(thm)],[clause58]) ).
fof(clause59,axiom,
( c3_1(a321)
| ~ hskp16 ),
file('theBenchmark.p',clause59) ).
cnf(c_59,plain,
( c3_1(a321)
| ~ hskp16 ),
inference(clausify,[status(thm)],[clause59]) ).
fof(clause61,axiom,
( c1_1(a315)
| ~ hskp14 ),
file('theBenchmark.p',clause61) ).
cnf(c_61,plain,
( c1_1(a315)
| ~ hskp14 ),
inference(clausify,[status(thm)],[clause61]) ).
fof(clause62,axiom,
( c2_1(a315)
| ~ hskp14 ),
file('theBenchmark.p',clause62) ).
cnf(c_62,plain,
( c2_1(a315)
| ~ hskp14 ),
inference(clausify,[status(thm)],[clause62]) ).
fof(clause63,axiom,
( c0_1(a313)
| ~ hskp13 ),
file('theBenchmark.p',clause63) ).
cnf(c_63,plain,
( c0_1(a313)
| ~ hskp13 ),
inference(clausify,[status(thm)],[clause63]) ).
fof(clause64,axiom,
( c3_1(a313)
| ~ hskp13 ),
file('theBenchmark.p',clause64) ).
cnf(c_64,plain,
( c3_1(a313)
| ~ hskp13 ),
inference(clausify,[status(thm)],[clause64]) ).
fof(clause65,axiom,
( c3_1(a310)
| ~ hskp12 ),
file('theBenchmark.p',clause65) ).
cnf(c_65,plain,
( c3_1(a310)
| ~ hskp12 ),
inference(clausify,[status(thm)],[clause65]) ).
fof(clause66,axiom,
( c1_1(a309)
| ~ hskp11 ),
file('theBenchmark.p',clause66) ).
cnf(c_66,plain,
( c1_1(a309)
| ~ hskp11 ),
inference(clausify,[status(thm)],[clause66]) ).
fof(clause67,axiom,
( c3_1(a309)
| ~ hskp11 ),
file('theBenchmark.p',clause67) ).
cnf(c_67,plain,
( c3_1(a309)
| ~ hskp11 ),
inference(clausify,[status(thm)],[clause67]) ).
fof(clause68,axiom,
( c1_1(a308)
| ~ hskp10 ),
file('theBenchmark.p',clause68) ).
cnf(c_68,plain,
( c1_1(a308)
| ~ hskp10 ),
inference(clausify,[status(thm)],[clause68]) ).
fof(clause69,axiom,
( c3_1(a308)
| ~ hskp10 ),
file('theBenchmark.p',clause69) ).
cnf(c_69,plain,
( c3_1(a308)
| ~ hskp10 ),
inference(clausify,[status(thm)],[clause69]) ).
fof(clause71,axiom,
( c2_1(a305)
| ~ hskp8 ),
file('theBenchmark.p',clause71) ).
cnf(c_71,plain,
( c2_1(a305)
| ~ hskp8 ),
inference(clausify,[status(thm)],[clause71]) ).
fof(clause78,axiom,
( c1_1(a297)
| ~ hskp2 ),
file('theBenchmark.p',clause78) ).
cnf(c_78,plain,
( c1_1(a297)
| ~ hskp2 ),
inference(clausify,[status(thm)],[clause78]) ).
fof(clause79,axiom,
( c0_1(a295)
| ~ hskp1 ),
file('theBenchmark.p',clause79) ).
cnf(c_79,plain,
( c0_1(a295)
| ~ hskp1 ),
inference(clausify,[status(thm)],[clause79]) ).
fof(clause80,axiom,
( c2_1(a295)
| ~ hskp1 ),
file('theBenchmark.p',clause80) ).
cnf(c_80,plain,
( c2_1(a295)
| ~ hskp1 ),
inference(clausify,[status(thm)],[clause80]) ).
fof(clause81,axiom,
( ~ hskp26
| ~ c2_1(a349) ),
file('theBenchmark.p',clause81) ).
cnf(c_81,plain,
( ~ hskp26
| ~ c2_1(a349) ),
inference(clausify,[status(thm)],[clause81]) ).
fof(clause82,axiom,
( ~ hskp26
| ~ c3_1(a349) ),
file('theBenchmark.p',clause82) ).
cnf(c_82,plain,
( ~ hskp26
| ~ c3_1(a349) ),
inference(clausify,[status(thm)],[clause82]) ).
fof(clause92,axiom,
( ~ hskp21
| ~ c0_1(a336) ),
file('theBenchmark.p',clause92) ).
cnf(c_92,plain,
( ~ hskp21
| ~ c0_1(a336) ),
inference(clausify,[status(thm)],[clause92]) ).
fof(clause93,axiom,
( ~ hskp21
| ~ c1_1(a336) ),
file('theBenchmark.p',clause93) ).
cnf(c_93,plain,
( ~ hskp21
| ~ c1_1(a336) ),
inference(clausify,[status(thm)],[clause93]) ).
fof(clause94,axiom,
( ~ hskp20
| ~ c2_1(a333) ),
file('theBenchmark.p',clause94) ).
cnf(c_94,plain,
( ~ hskp20
| ~ c2_1(a333) ),
inference(clausify,[status(thm)],[clause94]) ).
fof(clause95,axiom,
( ~ hskp20
| ~ c3_1(a333) ),
file('theBenchmark.p',clause95) ).
cnf(c_95,plain,
( ~ hskp20
| ~ c3_1(a333) ),
inference(clausify,[status(thm)],[clause95]) ).
fof(clause96,axiom,
( ~ hskp19
| ~ c3_1(a330) ),
file('theBenchmark.p',clause96) ).
cnf(c_96,plain,
( ~ hskp19
| ~ c3_1(a330) ),
inference(clausify,[status(thm)],[clause96]) ).
fof(clause100,axiom,
( ~ hskp16
| ~ c1_1(a321) ),
file('theBenchmark.p',clause100) ).
cnf(c_100,plain,
( ~ hskp16
| ~ c1_1(a321) ),
inference(clausify,[status(thm)],[clause100]) ).
fof(clause103,axiom,
( ~ hskp14
| ~ c0_1(a315) ),
file('theBenchmark.p',clause103) ).
cnf(c_103,plain,
( ~ hskp14
| ~ c0_1(a315) ),
inference(clausify,[status(thm)],[clause103]) ).
fof(clause104,axiom,
( ~ hskp13
| ~ c1_1(a313) ),
file('theBenchmark.p',clause104) ).
cnf(c_104,plain,
( ~ hskp13
| ~ c1_1(a313) ),
inference(clausify,[status(thm)],[clause104]) ).
fof(clause105,axiom,
( ~ hskp12
| ~ c0_1(a310) ),
file('theBenchmark.p',clause105) ).
cnf(c_105,plain,
( ~ hskp12
| ~ c0_1(a310) ),
inference(clausify,[status(thm)],[clause105]) ).
fof(clause106,axiom,
( ~ hskp12
| ~ c2_1(a310) ),
file('theBenchmark.p',clause106) ).
cnf(c_106,plain,
( ~ hskp12
| ~ c2_1(a310) ),
inference(clausify,[status(thm)],[clause106]) ).
fof(clause107,axiom,
( ~ hskp11
| ~ c2_1(a309) ),
file('theBenchmark.p',clause107) ).
cnf(c_107,plain,
( ~ hskp11
| ~ c2_1(a309) ),
inference(clausify,[status(thm)],[clause107]) ).
fof(clause108,axiom,
( ~ hskp10
| ~ c0_1(a308) ),
file('theBenchmark.p',clause108) ).
cnf(c_108,plain,
( ~ hskp10
| ~ c0_1(a308) ),
inference(clausify,[status(thm)],[clause108]) ).
fof(clause111,axiom,
( ~ hskp8
| ~ c0_1(a305) ),
file('theBenchmark.p',clause111) ).
cnf(c_111,plain,
( ~ hskp8
| ~ c0_1(a305) ),
inference(clausify,[status(thm)],[clause111]) ).
fof(clause112,axiom,
( ~ hskp8
| ~ c1_1(a305) ),
file('theBenchmark.p',clause112) ).
cnf(c_112,plain,
( ~ hskp8
| ~ c1_1(a305) ),
inference(clausify,[status(thm)],[clause112]) ).
fof(clause118,axiom,
( ~ hskp4
| ~ c0_1(a300) ),
file('theBenchmark.p',clause118) ).
cnf(c_118,plain,
( ~ hskp4
| ~ c0_1(a300) ),
inference(clausify,[status(thm)],[clause118]) ).
fof(clause119,axiom,
( ~ hskp4
| ~ c1_1(a300) ),
file('theBenchmark.p',clause119) ).
cnf(c_119,plain,
( ~ hskp4
| ~ c1_1(a300) ),
inference(clausify,[status(thm)],[clause119]) ).
fof(clause120,axiom,
( ~ hskp4
| ~ c2_1(a300) ),
file('theBenchmark.p',clause120) ).
cnf(c_120,plain,
( ~ hskp4
| ~ c2_1(a300) ),
inference(clausify,[status(thm)],[clause120]) ).
fof(clause122,axiom,
( ~ hskp2
| ~ c0_1(a297) ),
file('theBenchmark.p',clause122) ).
cnf(c_122,plain,
( ~ hskp2
| ~ c0_1(a297) ),
inference(clausify,[status(thm)],[clause122]) ).
fof(clause123,axiom,
( ~ hskp2
| ~ c3_1(a297) ),
file('theBenchmark.p',clause123) ).
cnf(c_123,plain,
( ~ hskp2
| ~ c3_1(a297) ),
inference(clausify,[status(thm)],[clause123]) ).
fof(clause124,axiom,
( ~ hskp1
| ~ c1_1(a295) ),
file('theBenchmark.p',clause124) ).
cnf(c_124,plain,
( ~ hskp1
| ~ c1_1(a295) ),
inference(clausify,[status(thm)],[clause124]) ).
fof(clause125,axiom,
( ~ hskp0
| ~ c0_1(a294) ),
file('theBenchmark.p',clause125) ).
cnf(c_125,plain,
( ~ hskp0
| ~ c0_1(a294) ),
inference(clausify,[status(thm)],[clause125]) ).
fof(clause126,axiom,
( ~ hskp0
| ~ c2_1(a294) ),
file('theBenchmark.p',clause126) ).
cnf(c_126,plain,
( ~ hskp0
| ~ c2_1(a294) ),
inference(clausify,[status(thm)],[clause126]) ).
fof(clause127,axiom,
( ~ hskp0
| ~ c3_1(a294) ),
file('theBenchmark.p',clause127) ).
cnf(c_127,plain,
( ~ hskp0
| ~ c3_1(a294) ),
inference(clausify,[status(thm)],[clause127]) ).
fof(clause128,axiom,
! [VAR_0] :
( hskp16
| c2_1(VAR_0)
| c1_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0) ),
file('theBenchmark.p',clause128) ).
cnf(c_128,plain,
( hskp16
| c2_1(A)
| c1_1(A)
| ~ ndr1_0
| ~ c3_1(A) ),
inference(clausify,[status(thm)],[clause128]) ).
fof(clause129,axiom,
! [VAR_0] :
( hskp21
| c3_1(VAR_0)
| c2_1(VAR_0)
| ~ ndr1_0
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause129) ).
cnf(c_129,plain,
( hskp21
| c3_1(A)
| c2_1(A)
| ~ ndr1_0
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause129]) ).
fof(clause131,axiom,
! [VAR_0] :
( hskp0
| hskp2
| c1_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0) ),
file('theBenchmark.p',clause131) ).
cnf(c_131,plain,
( hskp0
| hskp2
| c1_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c3_1(A) ),
inference(clausify,[status(thm)],[clause131]) ).
fof(clause134,axiom,
! [VAR_0] :
( hskp11
| hskp10
| c2_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0) ),
file('theBenchmark.p',clause134) ).
cnf(c_134,plain,
( hskp11
| hskp10
| c2_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c3_1(A) ),
inference(clausify,[status(thm)],[clause134]) ).
fof(clause137,axiom,
! [VAR_0] :
( hskp0
| hskp14
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause137) ).
cnf(c_137,plain,
( hskp0
| hskp14
| c0_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause137]) ).
fof(clause139,axiom,
! [VAR_0] :
( hskp12
| hskp19
| c1_1(VAR_0)
| ~ ndr1_0
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause139) ).
cnf(c_139,plain,
( hskp12
| hskp19
| c1_1(A)
| ~ ndr1_0
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause139]) ).
fof(clause140,axiom,
! [VAR_0] :
( hskp20
| hskp11
| c1_1(VAR_0)
| ~ ndr1_0
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause140) ).
cnf(c_140,plain,
( hskp20
| hskp11
| c1_1(A)
| ~ ndr1_0
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause140]) ).
fof(clause145,axiom,
! [VAR_0] :
( hskp28
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause145) ).
cnf(c_145,plain,
( hskp28
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause145]) ).
fof(clause149,axiom,
! [VAR_0,VAR_1] :
( hskp0
| c2_1(VAR_1)
| c1_1(VAR_1)
| c0_1(VAR_1)
| c2_1(VAR_0)
| ~ ndr1_0
| ~ c1_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause149) ).
cnf(c_149,plain,
( hskp0
| c2_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ ndr1_0
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause149]) ).
fof(clause151,axiom,
! [VAR_0,VAR_1] :
( hskp13
| c3_1(VAR_1)
| c1_1(VAR_1)
| c3_1(VAR_0)
| c1_1(VAR_0)
| ~ c0_1(VAR_1)
| ~ ndr1_0
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause151) ).
cnf(c_151,plain,
( hskp13
| c3_1(B)
| c1_1(B)
| c3_1(A)
| c1_1(A)
| ~ c0_1(B)
| ~ ndr1_0
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause151]) ).
fof(clause154,axiom,
! [VAR_0,VAR_1] :
( hskp1
| c1_1(VAR_1)
| c0_1(VAR_1)
| c1_1(VAR_0)
| ~ c2_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause154) ).
cnf(c_154,plain,
( hskp1
| c1_1(B)
| c0_1(B)
| c1_1(A)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause154]) ).
fof(clause155,axiom,
! [VAR_0,VAR_1] :
( hskp0
| c1_1(VAR_1)
| c0_1(VAR_1)
| c2_1(VAR_0)
| ~ c3_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause155) ).
cnf(c_155,plain,
( hskp0
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause155]) ).
fof(clause161,axiom,
! [VAR_0,VAR_1] :
( hskp8
| c3_1(VAR_1)
| c0_1(VAR_1)
| c3_1(VAR_0)
| ~ c2_1(VAR_1)
| ~ ndr1_0
| ~ c2_1(VAR_0)
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause161) ).
cnf(c_161,plain,
( hskp8
| c3_1(B)
| c0_1(B)
| c3_1(A)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause161]) ).
fof(clause162,axiom,
! [VAR_0,VAR_1] :
( hskp12
| c0_1(VAR_1)
| c3_1(VAR_0)
| c2_1(VAR_0)
| ~ c2_1(VAR_1)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause162) ).
cnf(c_162,plain,
( hskp12
| c0_1(B)
| c3_1(A)
| c2_1(A)
| ~ c2_1(B)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause162]) ).
fof(clause167,axiom,
! [VAR_0,VAR_1] :
( hskp4
| c1_1(VAR_1)
| c1_1(VAR_0)
| ~ c2_1(VAR_1)
| ~ c0_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause167) ).
cnf(c_167,plain,
( hskp4
| c1_1(B)
| c1_1(A)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause167]) ).
fof(clause169,axiom,
! [VAR_0,VAR_1] :
( c2_1(VAR_1)
| ~ c3_1(VAR_1)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause169) ).
cnf(c_169,plain,
( c2_1(B)
| ~ c3_1(B)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause169]) ).
fof(clause170,axiom,
! [VAR_0,VAR_1] :
( hskp11
| c3_1(VAR_1)
| ~ c2_1(VAR_1)
| ~ c0_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause170) ).
cnf(c_170,plain,
( hskp11
| c3_1(B)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause170]) ).
fof(clause174,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c3_1(VAR_2)
| c1_1(VAR_2)
| c0_1(VAR_2)
| c3_1(VAR_1)
| c2_1(VAR_1)
| c0_1(VAR_1)
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause174) ).
cnf(c_174,plain,
( c3_1(C)
| c1_1(C)
| c0_1(C)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause174]) ).
fof(clause176,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c3_1(VAR_2)
| c2_1(VAR_2)
| c0_1(VAR_2)
| c2_1(VAR_1)
| c0_1(VAR_1)
| c1_1(VAR_0)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause176) ).
cnf(c_176,plain,
( c3_1(C)
| c2_1(C)
| c0_1(C)
| c2_1(B)
| c0_1(B)
| c1_1(A)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause176]) ).
cnf(c_36440,plain,
( hskp13
| c3_1(A)
| c3_1(A)
| c1_1(A)
| ~ c0_1(A)
| ~ ndr1_0
| ~ c2_1(A) ),
inference(factor,[status(thm)],[c_151]) ).
cnf(c_182,plain,
( hskp13
| c3_1(A)
| c1_1(A)
| ~ c0_1(A)
| ~ ndr1_0
| ~ c2_1(A) ),
inference(copy,[status(thm)],[c_36440]) ).
cnf(c_36441,plain,
( hskp1
| c1_1(A)
| c0_1(A)
| c1_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(factor,[status(thm)],[c_154]) ).
cnf(c_183,plain,
( hskp1
| c0_1(A)
| c1_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(copy,[status(thm)],[c_36441]) ).
cnf(c_36442,plain,
( hskp8
| c3_1(A)
| c0_1(A)
| c3_1(A)
| ~ ndr1_0
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(factor,[status(thm)],[c_161]) ).
cnf(c_184,plain,
( hskp8
| c0_1(A)
| c3_1(A)
| ~ ndr1_0
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(copy,[status(thm)],[c_36442]) ).
cnf(c_36443,plain,
( hskp4
| c1_1(A)
| c1_1(A)
| ~ c2_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(factor,[status(thm)],[c_167]) ).
cnf(c_185,plain,
( hskp4
| c1_1(A)
| ~ c2_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(copy,[status(thm)],[c_36443]) ).
cnf(c_36444,plain,
( c3_1(B)
| c1_1(B)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(factor,[status(thm)],[c_174]) ).
cnf(c_188,plain,
( c1_1(B)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(copy,[status(thm)],[c_36444]) ).
cnf(c_36445,plain,
( c3_1(B)
| c2_1(B)
| c2_1(B)
| c0_1(B)
| c1_1(A)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(factor,[status(thm)],[c_176]) ).
cnf(c_189,plain,
( c3_1(B)
| c2_1(B)
| c0_1(B)
| c1_1(A)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(copy,[status(thm)],[c_36445]) ).
cnf(c_193,plain,
( hskp16
| ndr1_0 ),
inference(resolve,[status(thm)],[c_5,c_1]) ).
cnf(c_203,plain,
( hskp12
| hskp11
| c0_1(a349) ),
inference(resolve,[status(thm)],[c_47,c_36]) ).
cnf(c_204,plain,
( hskp16
| c0_1(a349) ),
inference(resolve,[status(thm)],[c_47,c_1]) ).
cnf(c_36446,plain,
( ndr1_0
| ndr1_0 ),
inference(resolve,[status(thm)],[c_193,c_15]) ).
cnf(c_211,plain,
ndr1_0,
inference(copy,[status(thm)],[c_36446]) ).
cnf(c_215,plain,
( c3_1(B)
| c2_1(B)
| c0_1(B)
| c1_1(A)
| ~ c1_1(B)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_189]) ).
cnf(c_216,plain,
( c1_1(B)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_188]) ).
cnf(c_219,plain,
( hskp4
| c1_1(A)
| ~ c2_1(A)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_185]) ).
cnf(c_220,plain,
( hskp8
| c0_1(A)
| c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_211,c_184]) ).
cnf(c_221,plain,
( hskp1
| c0_1(A)
| c1_1(A)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_183]) ).
cnf(c_222,plain,
( hskp13
| c3_1(A)
| c1_1(A)
| ~ c0_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_182]) ).
cnf(c_228,plain,
( c3_1(C)
| c2_1(C)
| c0_1(C)
| c2_1(B)
| c0_1(B)
| c1_1(A)
| ~ c1_1(B)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_176]) ).
cnf(c_230,plain,
( c3_1(C)
| c1_1(C)
| c0_1(C)
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_174]) ).
cnf(c_234,plain,
( hskp11
| c3_1(B)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_170]) ).
cnf(c_235,plain,
( c2_1(B)
| ~ c3_1(B)
| ~ c1_1(B)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_169]) ).
cnf(c_237,plain,
( hskp4
| c1_1(B)
| c1_1(A)
| ~ c2_1(B)
| ~ c0_1(B)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_167]) ).
cnf(c_242,plain,
( hskp12
| c0_1(B)
| c3_1(A)
| c2_1(A)
| ~ c2_1(B)
| ~ c1_1(B)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_162]) ).
cnf(c_249,plain,
( hskp0
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_211,c_155]) ).
cnf(c_250,plain,
( hskp1
| c1_1(B)
| c0_1(B)
| c1_1(A)
| ~ c2_1(B)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_154]) ).
cnf(c_255,plain,
( hskp0
| c2_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_149]) ).
cnf(c_259,plain,
( hskp28
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_211,c_145]) ).
cnf(c_264,plain,
( hskp20
| hskp11
| c1_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_140]) ).
cnf(c_265,plain,
( hskp12
| hskp19
| c1_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_139]) ).
cnf(c_267,plain,
( hskp0
| hskp14
| c0_1(A)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_211,c_137]) ).
cnf(c_270,plain,
( hskp11
| hskp10
| c2_1(A)
| c0_1(A)
| ~ c3_1(A) ),
inference(resolve,[status(thm)],[c_211,c_134]) ).
cnf(c_273,plain,
( hskp0
| hskp2
| c1_1(A)
| c0_1(A)
| ~ c3_1(A) ),
inference(resolve,[status(thm)],[c_211,c_131]) ).
cnf(c_275,plain,
( hskp21
| c3_1(A)
| c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_211,c_129]) ).
cnf(c_276,plain,
( hskp16
| c2_1(A)
| c1_1(A)
| ~ c3_1(A) ),
inference(resolve,[status(thm)],[c_211,c_128]) ).
cnf(c_279,plain,
( hskp16
| hskp21
| c3_1(a349)
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_275,c_204]) ).
cnf(c_280,plain,
( hskp12
| hskp11
| hskp21
| c3_1(a349)
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_275,c_203]) ).
cnf(c_281,plain,
( ~ hskp26
| hskp16
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_279,c_82]) ).
cnf(c_36447,plain,
( hskp16
| hskp16
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_281,c_1]) ).
cnf(c_285,plain,
( hskp16
| hskp21
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36447]) ).
cnf(c_286,plain,
( ~ hskp26
| hskp16
| hskp21 ),
inference(resolve,[status(thm)],[c_285,c_81]) ).
cnf(c_36448,plain,
( hskp16
| hskp16
| hskp21 ),
inference(resolve,[status(thm)],[c_286,c_1]) ).
cnf(c_288,plain,
( hskp16
| hskp21 ),
inference(copy,[status(thm)],[c_36448]) ).
cnf(c_289,plain,
( c3_1(a336)
| hskp16 ),
inference(resolve,[status(thm)],[c_288,c_51]) ).
cnf(c_36449,plain,
( hskp16
| hskp16
| c2_1(a336)
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_276,c_289]) ).
cnf(c_294,plain,
( hskp16
| c2_1(a336)
| c1_1(a336) ),
inference(copy,[status(thm)],[c_36449]) ).
cnf(c_300,plain,
( ~ hskp26
| hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_280,c_82]) ).
cnf(c_36450,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_300,c_36]) ).
cnf(c_36451,plain,
( hskp12
| hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36450]) ).
cnf(c_301,plain,
( hskp12
| hskp11
| hskp21
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36451]) ).
cnf(c_304,plain,
( ~ hskp26
| hskp12
| hskp11
| hskp21 ),
inference(resolve,[status(thm)],[c_301,c_81]) ).
cnf(c_36452,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp21 ),
inference(resolve,[status(thm)],[c_304,c_36]) ).
cnf(c_36453,plain,
( hskp12
| hskp12
| hskp11
| hskp21 ),
inference(copy,[status(thm)],[c_36452]) ).
cnf(c_305,plain,
( hskp12
| hskp11
| hskp21 ),
inference(copy,[status(thm)],[c_36453]) ).
cnf(c_306,plain,
( c3_1(a336)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_305,c_51]) ).
cnf(c_312,plain,
( hskp12
| hskp11
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336)
| ~ c2_1(a336) ),
inference(resolve,[status(thm)],[c_216,c_306]) ).
cnf(c_313,plain,
( hskp16
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336)
| ~ c2_1(a336) ),
inference(resolve,[status(thm)],[c_216,c_289]) ).
cnf(c_354,plain,
( hskp16
| hskp1
| c0_1(a336)
| c1_1(a336)
| ~ c2_1(a336) ),
inference(resolve,[status(thm)],[c_221,c_289]) ).
cnf(c_394,plain,
( hskp12
| hskp11
| hskp0
| hskp14
| c0_1(a336)
| ~ c2_1(a336) ),
inference(resolve,[status(thm)],[c_267,c_306]) ).
cnf(c_36454,plain,
( hskp12
| hskp11
| hskp11
| hskp10
| c2_1(a336)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_270,c_306]) ).
cnf(c_462,plain,
( hskp12
| hskp11
| hskp10
| c2_1(a336)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36454]) ).
cnf(c_466,plain,
( ~ hskp21
| hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(resolve,[status(thm)],[c_462,c_92]) ).
cnf(c_36455,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(resolve,[status(thm)],[c_466,c_305]) ).
cnf(c_36456,plain,
( hskp12
| hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(copy,[status(thm)],[c_36455]) ).
cnf(c_467,plain,
( hskp12
| hskp11
| hskp10
| c2_1(a336) ),
inference(copy,[status(thm)],[c_36456]) ).
cnf(c_493,plain,
( hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_273,c_306]) ).
cnf(c_36457,plain,
( hskp12
| hskp11
| hskp12
| c0_1(A)
| c3_1(a349)
| c2_1(a349)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_242,c_203]) ).
cnf(c_616,plain,
( hskp11
| hskp12
| c0_1(A)
| c3_1(a349)
| c2_1(a349)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(copy,[status(thm)],[c_36457]) ).
cnf(c_36458,plain,
( hskp16
| c1_1(a336)
| hskp16
| hskp1
| c0_1(a336)
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_354,c_294]) ).
cnf(c_36459,plain,
( hskp16
| hskp16
| hskp1
| c0_1(a336)
| c1_1(a336) ),
inference(copy,[status(thm)],[c_36458]) ).
cnf(c_663,plain,
( hskp16
| hskp1
| c0_1(a336)
| c1_1(a336) ),
inference(copy,[status(thm)],[c_36459]) ).
cnf(c_668,plain,
( ~ hskp21
| hskp16
| hskp1
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_663,c_92]) ).
cnf(c_36460,plain,
( hskp16
| hskp16
| hskp1
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_668,c_288]) ).
cnf(c_670,plain,
( hskp16
| hskp1
| c1_1(a336) ),
inference(copy,[status(thm)],[c_36460]) ).
cnf(c_674,plain,
( ~ hskp21
| hskp16
| hskp1 ),
inference(resolve,[status(thm)],[c_670,c_93]) ).
cnf(c_36461,plain,
( hskp16
| hskp16
| hskp1 ),
inference(resolve,[status(thm)],[c_674,c_288]) ).
cnf(c_680,plain,
( hskp16
| hskp1 ),
inference(copy,[status(thm)],[c_36461]) ).
cnf(c_681,plain,
( c2_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_680,c_80]) ).
cnf(c_682,plain,
( c0_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_680,c_79]) ).
cnf(c_695,plain,
( hskp13
| c3_1(a295)
| c1_1(a295)
| ~ c2_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_682,c_222]) ).
cnf(c_36462,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_394,c_467]) ).
cnf(c_36463,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36462]) ).
cnf(c_882,plain,
( hskp10
| hskp12
| hskp11
| hskp0
| hskp14
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36463]) ).
cnf(c_888,plain,
( ~ hskp21
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(resolve,[status(thm)],[c_882,c_92]) ).
cnf(c_36464,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(resolve,[status(thm)],[c_888,c_305]) ).
cnf(c_36465,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(copy,[status(thm)],[c_36464]) ).
cnf(c_889,plain,
( hskp10
| hskp12
| hskp11
| hskp0
| hskp14 ),
inference(copy,[status(thm)],[c_36465]) ).
cnf(c_890,plain,
( c2_1(a315)
| hskp10
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_889,c_62]) ).
cnf(c_36466,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_312,c_467]) ).
cnf(c_36467,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36466]) ).
cnf(c_1048,plain,
( hskp10
| hskp12
| hskp11
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36467]) ).
cnf(c_1070,plain,
( ~ hskp21
| hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_493,c_92]) ).
cnf(c_36468,plain,
( hskp16
| c1_1(a336)
| hskp16
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_313,c_294]) ).
cnf(c_1072,plain,
( c1_1(a336)
| hskp16
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36468]) ).
cnf(c_36469,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(resolve,[status(thm)],[c_1070,c_305]) ).
cnf(c_36470,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(copy,[status(thm)],[c_36469]) ).
cnf(c_1073,plain,
( hskp12
| hskp11
| hskp0
| hskp2
| c1_1(a336) ),
inference(copy,[status(thm)],[c_36470]) ).
cnf(c_1079,plain,
( ~ hskp21
| hskp12
| hskp11
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_1073,c_93]) ).
cnf(c_36471,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_1079,c_305]) ).
cnf(c_36472,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| hskp2 ),
inference(copy,[status(thm)],[c_36471]) ).
cnf(c_1080,plain,
( hskp12
| hskp11
| hskp0
| hskp2 ),
inference(copy,[status(thm)],[c_36472]) ).
cnf(c_1081,plain,
( c1_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_1080,c_78]) ).
cnf(c_36473,plain,
( hskp16
| hskp13
| c3_1(a295)
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_695,c_681]) ).
cnf(c_1182,plain,
( hskp13
| c3_1(a295)
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_36473]) ).
cnf(c_36474,plain,
( hskp4
| c1_1(a295)
| ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_1182,c_219]) ).
cnf(c_1187,plain,
( hskp4
| ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_36474]) ).
cnf(c_36475,plain,
( hskp16
| hskp4
| ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_1187,c_682]) ).
cnf(c_2422,plain,
( hskp4
| ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_36475]) ).
cnf(c_36476,plain,
( hskp16
| hskp4
| hskp13
| c1_1(a295)
| hskp16 ),
inference(resolve,[status(thm)],[c_2422,c_681]) ).
cnf(c_2423,plain,
( hskp4
| hskp13
| c1_1(a295)
| hskp16 ),
inference(copy,[status(thm)],[c_36476]) ).
cnf(c_2438,plain,
( ~ hskp1
| hskp4
| hskp13
| hskp16 ),
inference(resolve,[status(thm)],[c_2423,c_124]) ).
cnf(c_36477,plain,
( hskp16
| hskp4
| hskp13
| hskp16 ),
inference(resolve,[status(thm)],[c_2438,c_680]) ).
cnf(c_2439,plain,
( hskp4
| hskp13
| hskp16 ),
inference(copy,[status(thm)],[c_36477]) ).
cnf(c_2440,plain,
( c3_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2439,c_64]) ).
cnf(c_2441,plain,
( c0_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2439,c_63]) ).
cnf(c_36478,plain,
( hskp16
| c2_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2440,c_276]) ).
cnf(c_2445,plain,
( c2_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36478]) ).
cnf(c_36479,plain,
( hskp4
| c1_1(a313)
| ~ c2_1(a313)
| ~ c0_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2440,c_219]) ).
cnf(c_2461,plain,
( c1_1(a313)
| ~ c2_1(a313)
| ~ c0_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36479]) ).
cnf(c_36480,plain,
( hskp4
| hskp16
| c1_1(a313)
| ~ c2_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2461,c_2441]) ).
cnf(c_36481,plain,
( hskp4
| c1_1(a313)
| ~ c2_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36480]) ).
cnf(c_2479,plain,
( c1_1(a313)
| ~ c2_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36481]) ).
cnf(c_36482,plain,
( c1_1(a313)
| hskp4
| hskp16
| c1_1(a313)
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2479,c_2445]) ).
cnf(c_36483,plain,
( c1_1(a313)
| hskp4
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36482]) ).
cnf(c_36484,plain,
( c1_1(a313)
| c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36483]) ).
cnf(c_2489,plain,
( c1_1(a313)
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36484]) ).
cnf(c_2490,plain,
( ~ hskp13
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2489,c_104]) ).
cnf(c_36485,plain,
( hskp4
| hskp16
| hskp4
| hskp16 ),
inference(resolve,[status(thm)],[c_2490,c_2439]) ).
cnf(c_36486,plain,
( hskp4
| hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36485]) ).
cnf(c_2491,plain,
( hskp4
| hskp16 ),
inference(copy,[status(thm)],[c_36486]) ).
cnf(c_36487,plain,
( hskp10
| hskp12
| hskp11
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a315) ),
inference(resolve,[status(thm)],[c_616,c_890]) ).
cnf(c_36488,plain,
( hskp10
| hskp12
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a315) ),
inference(copy,[status(thm)],[c_36487]) ).
cnf(c_4145,plain,
( hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a315) ),
inference(copy,[status(thm)],[c_36488]) ).
cnf(c_36489,plain,
( hskp11
| hskp10
| c2_1(A)
| c0_1(A)
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_1048,c_270]) ).
cnf(c_36490,plain,
( hskp11
| hskp10
| c2_1(A)
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36489]) ).
cnf(c_36491,plain,
( hskp11
| hskp10
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36490]) ).
cnf(c_36492,plain,
( hskp11
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36491]) ).
cnf(c_8016,plain,
( hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36492]) ).
cnf(c_36493,plain,
( hskp16
| c2_1(A)
| c1_1(A)
| c1_1(a336)
| hskp16
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(resolve,[status(thm)],[c_1072,c_276]) ).
cnf(c_36494,plain,
( hskp16
| c2_1(A)
| c1_1(a336)
| hskp16
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36493]) ).
cnf(c_36495,plain,
( hskp16
| c1_1(a336)
| hskp16
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36494]) ).
cnf(c_8192,plain,
( c1_1(a336)
| hskp16
| c1_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a336) ),
inference(copy,[status(thm)],[c_36495]) ).
cnf(c_11925,plain,
( ~ hskp21
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_8016,c_92]) ).
cnf(c_36496,plain,
( hskp12
| hskp11
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_11925,c_305]) ).
cnf(c_36497,plain,
( hskp12
| hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_36496]) ).
cnf(c_11954,plain,
( hskp10
| hskp12
| hskp11
| c1_1(A)
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_36497]) ).
cnf(c_11964,plain,
( ~ hskp0
| hskp10
| hskp12
| hskp11
| c1_1(a294)
| c2_1(a294) ),
inference(resolve,[status(thm)],[c_11954,c_125]) ).
cnf(c_13862,plain,
( ~ hskp21
| c1_1(a336)
| hskp16
| c1_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_8192,c_92]) ).
cnf(c_36498,plain,
( hskp16
| c1_1(a336)
| hskp16
| c1_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_13862,c_288]) ).
cnf(c_13873,plain,
( c1_1(a336)
| hskp16
| c1_1(A)
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_36498]) ).
cnf(c_13880,plain,
( ~ hskp4
| c1_1(a336)
| hskp16
| c1_1(a300)
| c2_1(a300) ),
inference(resolve,[status(thm)],[c_13873,c_118]) ).
cnf(c_36499,plain,
( hskp16
| c1_1(a336)
| hskp16
| c1_1(a300)
| c2_1(a300) ),
inference(resolve,[status(thm)],[c_13880,c_2491]) ).
cnf(c_13937,plain,
( c1_1(a336)
| hskp16
| c1_1(a300)
| c2_1(a300) ),
inference(copy,[status(thm)],[c_36499]) ).
cnf(c_13957,plain,
( ~ hskp4
| c1_1(a336)
| hskp16
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_13937,c_120]) ).
cnf(c_36500,plain,
( hskp16
| c1_1(a336)
| hskp16
| c1_1(a300) ),
inference(resolve,[status(thm)],[c_13957,c_2491]) ).
cnf(c_13967,plain,
( c1_1(a336)
| hskp16
| c1_1(a300) ),
inference(copy,[status(thm)],[c_36500]) ).
cnf(c_14000,plain,
( ~ hskp4
| c1_1(a336)
| hskp16 ),
inference(resolve,[status(thm)],[c_13967,c_119]) ).
cnf(c_36501,plain,
( hskp16
| c1_1(a336)
| hskp16 ),
inference(resolve,[status(thm)],[c_14000,c_2491]) ).
cnf(c_14001,plain,
( c1_1(a336)
| hskp16 ),
inference(copy,[status(thm)],[c_36501]) ).
cnf(c_14013,plain,
( ~ hskp21
| hskp16 ),
inference(resolve,[status(thm)],[c_14001,c_93]) ).
cnf(c_36502,plain,
( hskp16
| hskp16 ),
inference(resolve,[status(thm)],[c_14013,c_288]) ).
cnf(c_14018,plain,
hskp16,
inference(copy,[status(thm)],[c_36502]) ).
cnf(c_14019,plain,
~ c1_1(a321),
inference(resolve,[status(thm)],[c_14018,c_100]) ).
cnf(c_14020,plain,
c3_1(a321),
inference(resolve,[status(thm)],[c_14018,c_59]) ).
cnf(c_14021,plain,
c2_1(a321),
inference(resolve,[status(thm)],[c_14018,c_58]) ).
cnf(c_36503,plain,
( hskp0
| hskp2
| c1_1(a321)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_273]) ).
cnf(c_14158,plain,
( hskp0
| hskp2
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14019,c_36503]) ).
cnf(c_36504,plain,
( hskp1
| c1_1(A)
| c0_1(A)
| c1_1(a321)
| ~ c2_1(A)
| ~ c2_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_250]) ).
cnf(c_36505,plain,
( hskp1
| c1_1(A)
| c0_1(A)
| c1_1(a321)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_14021,c_36504]) ).
cnf(c_14161,plain,
( hskp1
| c1_1(A)
| c0_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_14019,c_36505]) ).
cnf(c_36506,plain,
( hskp0
| c1_1(a321)
| c0_1(a321)
| c2_1(A)
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_14020,c_249]) ).
cnf(c_14162,plain,
( hskp0
| c0_1(a321)
| c2_1(A)
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_14019,c_36506]) ).
cnf(c_36507,plain,
( c2_1(A)
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c2_1(a321)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_235]) ).
cnf(c_14166,plain,
( c2_1(A)
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14021,c_36507]) ).
cnf(c_36508,plain,
( hskp11
| c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| ~ c2_1(a321)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_234]) ).
cnf(c_14167,plain,
( hskp11
| c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14021,c_36508]) ).
cnf(c_36509,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a321)
| ~ c2_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_230]) ).
cnf(c_14168,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14021,c_36509]) ).
cnf(c_36510,plain,
( c3_1(B)
| c2_1(B)
| c0_1(B)
| c2_1(A)
| c0_1(A)
| c1_1(a321)
| ~ c1_1(A)
| ~ c2_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_228]) ).
cnf(c_36511,plain,
( c3_1(B)
| c2_1(B)
| c0_1(B)
| c2_1(A)
| c0_1(A)
| c1_1(a321)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_14021,c_36510]) ).
cnf(c_14169,plain,
( c3_1(B)
| c2_1(B)
| c0_1(B)
| c2_1(A)
| c0_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_14019,c_36511]) ).
cnf(c_36512,plain,
( hskp1
| c0_1(a321)
| c1_1(a321)
| ~ c2_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_221]) ).
cnf(c_36513,plain,
( hskp1
| c0_1(a321)
| c1_1(a321) ),
inference(resolve,[status(thm)],[c_14021,c_36512]) ).
cnf(c_14170,plain,
( hskp1
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14019,c_36513]) ).
cnf(c_36514,plain,
( hskp4
| c1_1(a321)
| ~ c2_1(a321)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_219]) ).
cnf(c_36515,plain,
( hskp4
| c1_1(a321)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14021,c_36514]) ).
cnf(c_14171,plain,
( hskp4
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_14019,c_36515]) ).
cnf(c_36516,plain,
( c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a321)
| ~ c2_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_216]) ).
cnf(c_14172,plain,
( c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14021,c_36516]) ).
cnf(c_36517,plain,
( c3_1(A)
| c2_1(A)
| c0_1(A)
| c1_1(a321)
| ~ c1_1(A)
| ~ c2_1(a321) ),
inference(resolve,[status(thm)],[c_14020,c_215]) ).
cnf(c_36518,plain,
( c3_1(A)
| c2_1(A)
| c0_1(A)
| c1_1(a321)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_14021,c_36517]) ).
cnf(c_14173,plain,
( c3_1(A)
| c2_1(A)
| c0_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_14019,c_36518]) ).
cnf(c_36519,plain,
( hskp12
| hskp19
| c1_1(a321)
| ~ c2_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_14170,c_265]) ).
cnf(c_36520,plain,
( hskp12
| hskp19
| c1_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_14021,c_36519]) ).
cnf(c_14197,plain,
( hskp12
| hskp19
| hskp1 ),
inference(resolve,[status(thm)],[c_14019,c_36520]) ).
cnf(c_36521,plain,
( hskp20
| hskp11
| c1_1(a321)
| ~ c2_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_14170,c_264]) ).
cnf(c_36522,plain,
( hskp20
| hskp11
| c1_1(a321)
| hskp1 ),
inference(resolve,[status(thm)],[c_14021,c_36521]) ).
cnf(c_14198,plain,
( hskp20
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_14019,c_36522]) ).
cnf(c_14200,plain,
( hskp1
| hskp4 ),
inference(resolve,[status(thm)],[c_14171,c_14170]) ).
cnf(c_14201,plain,
( c2_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_14200,c_80]) ).
cnf(c_14202,plain,
( c0_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_14200,c_79]) ).
cnf(c_14297,plain,
( c2_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_14197,c_54]) ).
cnf(c_14298,plain,
( c1_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_14197,c_53]) ).
cnf(c_14303,plain,
( c1_1(a333)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_14198,c_52]) ).
cnf(c_14350,plain,
( hskp13
| c3_1(a295)
| c1_1(a295)
| ~ c2_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_14202,c_222]) ).
cnf(c_36523,plain,
( hskp20
| hskp11
| c1_1(a321)
| ~ c2_1(a321)
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_14158,c_264]) ).
cnf(c_36524,plain,
( hskp20
| hskp11
| c1_1(a321)
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_14021,c_36523]) ).
cnf(c_14355,plain,
( hskp20
| hskp11
| hskp0
| hskp2 ),
inference(resolve,[status(thm)],[c_14019,c_36524]) ).
cnf(c_14417,plain,
( hskp8
| c0_1(a330)
| c3_1(a330)
| ~ c1_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_14297,c_220]) ).
cnf(c_14469,plain,
( c1_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_14355,c_78]) ).
cnf(c_15082,plain,
( hskp20
| hskp11
| hskp0
| c3_1(a297)
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_14173,c_14469]) ).
cnf(c_15086,plain,
( hskp11
| hskp1
| c3_1(a333)
| c2_1(a333)
| c0_1(a333) ),
inference(resolve,[status(thm)],[c_14173,c_14303]) ).
cnf(c_15093,plain,
( hskp12
| hskp11
| hskp0
| c3_1(a297)
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_14173,c_1081]) ).
cnf(c_36525,plain,
( hskp4
| hskp13
| c3_1(a295)
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_14350,c_14201]) ).
cnf(c_15098,plain,
( hskp13
| c3_1(a295)
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_36525]) ).
cnf(c_36526,plain,
( hskp4
| c1_1(a295)
| ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15098,c_219]) ).
cnf(c_36527,plain,
( hskp4
| ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_36526]) ).
cnf(c_15118,plain,
( ~ c2_1(a295)
| ~ c0_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_36527]) ).
cnf(c_15909,plain,
( ~ hskp20
| hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(resolve,[status(thm)],[c_15086,c_95]) ).
cnf(c_36528,plain,
( hskp11
| hskp1
| hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(resolve,[status(thm)],[c_15909,c_14198]) ).
cnf(c_36529,plain,
( hskp11
| hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(copy,[status(thm)],[c_36528]) ).
cnf(c_15916,plain,
( hskp11
| hskp1
| c2_1(a333)
| c0_1(a333) ),
inference(copy,[status(thm)],[c_36529]) ).
cnf(c_36530,plain,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp1
| c2_1(a333) ),
inference(resolve,[status(thm)],[c_15916,c_275]) ).
cnf(c_15918,plain,
( hskp21
| c3_1(a333)
| hskp11
| hskp1
| c2_1(a333) ),
inference(copy,[status(thm)],[c_36530]) ).
cnf(c_15937,plain,
( ~ hskp20
| hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(resolve,[status(thm)],[c_15918,c_95]) ).
cnf(c_36531,plain,
( hskp11
| hskp1
| hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(resolve,[status(thm)],[c_15937,c_14198]) ).
cnf(c_36532,plain,
( hskp11
| hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(copy,[status(thm)],[c_36531]) ).
cnf(c_15939,plain,
( hskp21
| hskp11
| hskp1
| c2_1(a333) ),
inference(copy,[status(thm)],[c_36532]) ).
cnf(c_15948,plain,
( ~ hskp20
| hskp21
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15939,c_94]) ).
cnf(c_36533,plain,
( hskp11
| hskp1
| hskp21
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15948,c_14198]) ).
cnf(c_36534,plain,
( hskp11
| hskp21
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36533]) ).
cnf(c_15950,plain,
( hskp21
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36534]) ).
cnf(c_15951,plain,
( c3_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15950,c_51]) ).
cnf(c_36535,plain,
( hskp11
| hskp10
| c2_1(a336)
| c0_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15951,c_270]) ).
cnf(c_15959,plain,
( hskp10
| c2_1(a336)
| c0_1(a336)
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36535]) ).
cnf(c_15984,plain,
( ~ hskp21
| hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15959,c_92]) ).
cnf(c_36536,plain,
( hskp11
| hskp1
| hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15984,c_15950]) ).
cnf(c_36537,plain,
( hskp11
| hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36536]) ).
cnf(c_15985,plain,
( hskp10
| c2_1(a336)
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36537]) ).
cnf(c_36538,plain,
( hskp1
| c1_1(a336)
| c0_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15985,c_14161]) ).
cnf(c_15986,plain,
( c1_1(a336)
| c0_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36538]) ).
cnf(c_15999,plain,
( ~ hskp21
| c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15986,c_92]) ).
cnf(c_36539,plain,
( hskp11
| hskp1
| c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_15999,c_15950]) ).
cnf(c_36540,plain,
( hskp11
| c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36539]) ).
cnf(c_16000,plain,
( c1_1(a336)
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36540]) ).
cnf(c_16008,plain,
( ~ hskp21
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16000,c_93]) ).
cnf(c_36541,plain,
( hskp11
| hskp1
| hskp10
| hskp11
| hskp1 ),
inference(resolve,[status(thm)],[c_16008,c_15950]) ).
cnf(c_36542,plain,
( hskp11
| hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36541]) ).
cnf(c_16012,plain,
( hskp10
| hskp11
| hskp1 ),
inference(copy,[status(thm)],[c_36542]) ).
cnf(c_16013,plain,
( c2_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16012,c_80]) ).
cnf(c_16014,plain,
( c0_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16012,c_79]) ).
cnf(c_36543,plain,
( hskp20
| hskp11
| c1_1(a295)
| ~ c2_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16014,c_264]) ).
cnf(c_16025,plain,
( hskp20
| c1_1(a295)
| ~ c2_1(a295)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36543]) ).
cnf(c_36544,plain,
( hskp10
| hskp11
| hskp20
| c1_1(a295)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16025,c_16013]) ).
cnf(c_36545,plain,
( hskp10
| hskp20
| c1_1(a295)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36544]) ).
cnf(c_16034,plain,
( hskp20
| c1_1(a295)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36545]) ).
cnf(c_16035,plain,
( ~ hskp1
| hskp20
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16034,c_124]) ).
cnf(c_36546,plain,
( hskp10
| hskp11
| hskp20
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16035,c_16012]) ).
cnf(c_36547,plain,
( hskp10
| hskp20
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36546]) ).
cnf(c_16040,plain,
( hskp20
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36547]) ).
cnf(c_16041,plain,
( c1_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16040,c_52]) ).
cnf(c_16042,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16041,c_14173]) ).
cnf(c_36548,plain,
( hskp4
| ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_15118,c_14202]) ).
cnf(c_16111,plain,
( ~ c2_1(a295)
| hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_36548]) ).
cnf(c_36549,plain,
( hskp4
| hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_16111,c_14201]) ).
cnf(c_16115,plain,
( hskp13
| c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_36549]) ).
cnf(c_16121,plain,
( ~ hskp1
| hskp13
| hskp4 ),
inference(resolve,[status(thm)],[c_16115,c_124]) ).
cnf(c_36550,plain,
( hskp4
| hskp13
| hskp4 ),
inference(resolve,[status(thm)],[c_16121,c_14200]) ).
cnf(c_16125,plain,
( hskp13
| hskp4 ),
inference(copy,[status(thm)],[c_36550]) ).
cnf(c_16126,plain,
( c3_1(a313)
| hskp4 ),
inference(resolve,[status(thm)],[c_16125,c_64]) ).
cnf(c_16127,plain,
( c0_1(a313)
| hskp4 ),
inference(resolve,[status(thm)],[c_16125,c_63]) ).
cnf(c_36551,plain,
( hskp4
| c1_1(A)
| c1_1(a313)
| ~ c2_1(A)
| ~ c0_1(A)
| ~ c0_1(a313)
| hskp4 ),
inference(resolve,[status(thm)],[c_16126,c_237]) ).
cnf(c_16174,plain,
( c1_1(A)
| c1_1(a313)
| ~ c2_1(A)
| ~ c0_1(A)
| ~ c0_1(a313)
| hskp4 ),
inference(copy,[status(thm)],[c_36551]) ).
cnf(c_36552,plain,
( hskp11
| hskp10
| c2_1(a333)
| c0_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16042,c_270]) ).
cnf(c_36553,plain,
( hskp11
| hskp10
| c2_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36552]) ).
cnf(c_36554,plain,
( hskp11
| hskp10
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36553]) ).
cnf(c_36555,plain,
( hskp11
| c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36554]) ).
cnf(c_16406,plain,
( c2_1(a333)
| c0_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36555]) ).
cnf(c_36556,plain,
( hskp21
| c3_1(a333)
| c2_1(a333)
| c2_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16406,c_275]) ).
cnf(c_16408,plain,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36556]) ).
cnf(c_16429,plain,
( ~ hskp20
| hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16408,c_95]) ).
cnf(c_36557,plain,
( hskp10
| hskp11
| hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16429,c_16040]) ).
cnf(c_36558,plain,
( hskp10
| hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36557]) ).
cnf(c_16430,plain,
( hskp21
| c2_1(a333)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36558]) ).
cnf(c_16444,plain,
( ~ hskp20
| hskp21
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16430,c_94]) ).
cnf(c_36559,plain,
( hskp10
| hskp11
| hskp21
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16444,c_16040]) ).
cnf(c_36560,plain,
( hskp10
| hskp21
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36559]) ).
cnf(c_16445,plain,
( hskp21
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36560]) ).
cnf(c_16449,plain,
( c3_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16445,c_51]) ).
cnf(c_36561,plain,
( hskp11
| hskp10
| c2_1(a336)
| c0_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16449,c_270]) ).
cnf(c_36562,plain,
( hskp11
| c2_1(a336)
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36561]) ).
cnf(c_16455,plain,
( c2_1(a336)
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36562]) ).
cnf(c_16457,plain,
( hskp0
| hskp14
| c0_1(a336)
| ~ c2_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16449,c_267]) ).
cnf(c_16477,plain,
( ~ hskp21
| c2_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16455,c_92]) ).
cnf(c_36563,plain,
( hskp10
| hskp11
| c2_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16477,c_16445]) ).
cnf(c_36564,plain,
( hskp10
| c2_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36563]) ).
cnf(c_16478,plain,
( c2_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36564]) ).
cnf(c_36565,plain,
( hskp10
| hskp11
| hskp0
| hskp14
| c0_1(a336)
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16457,c_16478]) ).
cnf(c_36566,plain,
( hskp10
| hskp0
| hskp14
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36565]) ).
cnf(c_16660,plain,
( hskp0
| hskp14
| c0_1(a336)
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36566]) ).
cnf(c_16663,plain,
( ~ hskp21
| hskp0
| hskp14
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16660,c_92]) ).
cnf(c_36567,plain,
( hskp10
| hskp11
| hskp0
| hskp14
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16663,c_16445]) ).
cnf(c_36568,plain,
( hskp10
| hskp0
| hskp14
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36567]) ).
cnf(c_16665,plain,
( hskp0
| hskp14
| hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36568]) ).
cnf(c_16667,plain,
( c1_1(a315)
| hskp0
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_16665,c_61]) ).
cnf(c_17196,plain,
( hskp1
| hskp11
| c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_14167,c_14170]) ).
cnf(c_36569,plain,
( hskp12
| hskp1
| hskp8
| c0_1(a330)
| c3_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_14417,c_14298]) ).
cnf(c_36570,plain,
( hskp12
| hskp8
| c0_1(a330)
| c3_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36569]) ).
cnf(c_17369,plain,
( hskp8
| c0_1(a330)
| c3_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36570]) ).
cnf(c_17376,plain,
( ~ hskp19
| hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17369,c_96]) ).
cnf(c_36571,plain,
( hskp12
| hskp1
| hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17376,c_14197]) ).
cnf(c_36572,plain,
( hskp12
| hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36571]) ).
cnf(c_17378,plain,
( hskp8
| c0_1(a330)
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36572]) ).
cnf(c_36573,plain,
( hskp1
| hskp11
| c3_1(a330)
| ~ c2_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17378,c_17196]) ).
cnf(c_17382,plain,
( hskp11
| c3_1(a330)
| ~ c2_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36573]) ).
cnf(c_36574,plain,
( hskp12
| hskp1
| hskp11
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17382,c_14297]) ).
cnf(c_36575,plain,
( hskp12
| hskp11
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36574]) ).
cnf(c_17392,plain,
( hskp11
| c3_1(a330)
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36575]) ).
cnf(c_17397,plain,
( ~ hskp19
| hskp11
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17392,c_96]) ).
cnf(c_36576,plain,
( hskp12
| hskp1
| hskp11
| hskp8
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17397,c_14197]) ).
cnf(c_36577,plain,
( hskp12
| hskp11
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36576]) ).
cnf(c_17399,plain,
( hskp11
| hskp8
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36577]) ).
cnf(c_17400,plain,
( c2_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17399,c_71]) ).
cnf(c_36578,plain,
( hskp1
| c1_1(a305)
| c0_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17400,c_14161]) ).
cnf(c_17401,plain,
( c1_1(a305)
| c0_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36578]) ).
cnf(c_17410,plain,
( ~ hskp8
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17401,c_111]) ).
cnf(c_36579,plain,
( hskp11
| hskp12
| hskp1
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17410,c_17399]) ).
cnf(c_36580,plain,
( hskp11
| hskp12
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36579]) ).
cnf(c_36581,plain,
( hskp11
| c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36580]) ).
cnf(c_17411,plain,
( c1_1(a305)
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36581]) ).
cnf(c_17417,plain,
( ~ hskp8
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17411,c_112]) ).
cnf(c_36582,plain,
( hskp11
| hskp12
| hskp1
| hskp11
| hskp12
| hskp1 ),
inference(resolve,[status(thm)],[c_17417,c_17399]) ).
cnf(c_36583,plain,
( hskp11
| hskp12
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36582]) ).
cnf(c_36584,plain,
( hskp11
| hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36583]) ).
cnf(c_17418,plain,
( hskp11
| hskp12
| hskp1 ),
inference(copy,[status(thm)],[c_36584]) ).
cnf(c_17419,plain,
( c2_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17418,c_80]) ).
cnf(c_17420,plain,
( c0_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17418,c_79]) ).
cnf(c_36585,plain,
( hskp20
| hskp11
| c1_1(a295)
| ~ c2_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17420,c_264]) ).
cnf(c_17433,plain,
( hskp20
| c1_1(a295)
| ~ c2_1(a295)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36585]) ).
cnf(c_36586,plain,
( hskp11
| hskp12
| hskp20
| c1_1(a295)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17433,c_17419]) ).
cnf(c_36587,plain,
( hskp11
| hskp20
| c1_1(a295)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36586]) ).
cnf(c_17467,plain,
( hskp20
| c1_1(a295)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36587]) ).
cnf(c_17468,plain,
( ~ hskp1
| hskp20
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17467,c_124]) ).
cnf(c_36588,plain,
( hskp11
| hskp12
| hskp20
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17468,c_17418]) ).
cnf(c_36589,plain,
( hskp11
| hskp20
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36588]) ).
cnf(c_17469,plain,
( hskp20
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36589]) ).
cnf(c_17470,plain,
( c1_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17469,c_52]) ).
cnf(c_17471,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17470,c_14173]) ).
cnf(c_17635,plain,
( ~ hskp20
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17471,c_95]) ).
cnf(c_36590,plain,
( hskp11
| hskp12
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17635,c_17469]) ).
cnf(c_36591,plain,
( hskp11
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36590]) ).
cnf(c_17638,plain,
( c2_1(a333)
| c0_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36591]) ).
cnf(c_36592,plain,
( hskp12
| c0_1(A)
| c3_1(a333)
| c2_1(a333)
| ~ c2_1(A)
| ~ c1_1(A)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17638,c_242]) ).
cnf(c_36593,plain,
( hskp12
| c0_1(A)
| c3_1(a333)
| ~ c2_1(A)
| ~ c1_1(A)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36592]) ).
cnf(c_17643,plain,
( c0_1(A)
| c3_1(a333)
| ~ c2_1(A)
| ~ c1_1(A)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36593]) ).
cnf(c_17910,plain,
( ~ hskp2
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_15082,c_123]) ).
cnf(c_36594,plain,
( hskp20
| hskp11
| hskp0
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_17910,c_14355]) ).
cnf(c_36595,plain,
( hskp20
| hskp11
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_36594]) ).
cnf(c_36596,plain,
( hskp20
| hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_36595]) ).
cnf(c_17911,plain,
( hskp20
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_36596]) ).
cnf(c_17917,plain,
( ~ hskp2
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_17911,c_122]) ).
cnf(c_36597,plain,
( hskp20
| hskp11
| hskp0
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_17917,c_14355]) ).
cnf(c_36598,plain,
( hskp20
| hskp11
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_36597]) ).
cnf(c_36599,plain,
( hskp20
| hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_36598]) ).
cnf(c_17918,plain,
( hskp20
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_36599]) ).
cnf(c_17924,plain,
( hskp8
| c0_1(a297)
| c3_1(a297)
| ~ c1_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_17918,c_220]) ).
cnf(c_17986,plain,
( ~ hskp2
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_15093,c_123]) ).
cnf(c_36600,plain,
( hskp12
| hskp11
| hskp0
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(resolve,[status(thm)],[c_17986,c_1080]) ).
cnf(c_36601,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_36600]) ).
cnf(c_36602,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_36601]) ).
cnf(c_18011,plain,
( hskp12
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297) ),
inference(copy,[status(thm)],[c_36602]) ).
cnf(c_18017,plain,
( ~ hskp2
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_18011,c_122]) ).
cnf(c_36603,plain,
( hskp12
| hskp11
| hskp0
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(resolve,[status(thm)],[c_18017,c_1080]) ).
cnf(c_36604,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_36603]) ).
cnf(c_36605,plain,
( hskp12
| hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_36604]) ).
cnf(c_18019,plain,
( hskp12
| hskp11
| hskp0
| c2_1(a297) ),
inference(copy,[status(thm)],[c_36605]) ).
cnf(c_36606,plain,
( hskp11
| hskp12
| c0_1(a297)
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_18019,c_616]) ).
cnf(c_36607,plain,
( hskp11
| c0_1(a297)
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36606]) ).
cnf(c_18022,plain,
( c0_1(a297)
| c3_1(a349)
| c2_1(a349)
| ~ c1_1(a297)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36607]) ).
cnf(c_36608,plain,
( hskp0
| hskp10
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c3_1(a349)
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_4145,c_16667]) ).
cnf(c_36609,plain,
( hskp0
| hskp10
| hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c3_1(a349)
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36608]) ).
cnf(c_36610,plain,
( hskp0
| hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c3_1(a349)
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36609]) ).
cnf(c_18572,plain,
( hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c3_1(a349)
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36610]) ).
cnf(c_19801,plain,
( ~ hskp0
| c1_1(a294)
| c2_1(a294)
| c0_1(a294)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14172,c_127]) ).
cnf(c_36611,plain,
( hskp20
| hskp11
| hskp0
| hskp8
| c0_1(a297)
| c3_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_17924,c_14469]) ).
cnf(c_36612,plain,
( hskp20
| hskp11
| hskp8
| c0_1(a297)
| c3_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36611]) ).
cnf(c_36613,plain,
( hskp20
| hskp8
| c0_1(a297)
| c3_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36612]) ).
cnf(c_20988,plain,
( hskp8
| c0_1(a297)
| c3_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36613]) ).
cnf(c_20994,plain,
( ~ hskp2
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_20988,c_123]) ).
cnf(c_36614,plain,
( hskp20
| hskp11
| hskp0
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_20994,c_14355]) ).
cnf(c_36615,plain,
( hskp20
| hskp11
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36614]) ).
cnf(c_36616,plain,
( hskp20
| hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36615]) ).
cnf(c_20995,plain,
( hskp8
| c0_1(a297)
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36616]) ).
cnf(c_21003,plain,
( ~ hskp2
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_20995,c_122]) ).
cnf(c_36617,plain,
( hskp20
| hskp11
| hskp0
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21003,c_14355]) ).
cnf(c_36618,plain,
( hskp20
| hskp11
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36617]) ).
cnf(c_36619,plain,
( hskp20
| hskp8
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36618]) ).
cnf(c_21004,plain,
( hskp8
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36619]) ).
cnf(c_21005,plain,
( c1_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21004,c_52]) ).
cnf(c_21007,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21005,c_14173]) ).
cnf(c_21047,plain,
( ~ hskp20
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21007,c_95]) ).
cnf(c_36620,plain,
( hskp8
| hskp11
| hskp0
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21047,c_21004]) ).
cnf(c_36621,plain,
( hskp8
| hskp11
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36620]) ).
cnf(c_36622,plain,
( hskp8
| c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36621]) ).
cnf(c_21048,plain,
( c2_1(a333)
| c0_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36622]) ).
cnf(c_36623,plain,
( hskp21
| c3_1(a333)
| c2_1(a333)
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21048,c_275]) ).
cnf(c_21049,plain,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36623]) ).
cnf(c_21069,plain,
( ~ hskp20
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21049,c_95]) ).
cnf(c_36624,plain,
( hskp8
| hskp11
| hskp0
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21069,c_21004]) ).
cnf(c_36625,plain,
( hskp8
| hskp11
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36624]) ).
cnf(c_36626,plain,
( hskp8
| hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36625]) ).
cnf(c_21070,plain,
( hskp21
| c2_1(a333)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36626]) ).
cnf(c_21078,plain,
( ~ hskp20
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21070,c_94]) ).
cnf(c_36627,plain,
( hskp8
| hskp11
| hskp0
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21078,c_21004]) ).
cnf(c_36628,plain,
( hskp8
| hskp11
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36627]) ).
cnf(c_36629,plain,
( hskp8
| hskp21
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36628]) ).
cnf(c_21079,plain,
( hskp21
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36629]) ).
cnf(c_21081,plain,
( c3_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21079,c_51]) ).
cnf(c_36630,plain,
( hskp0
| hskp2
| c1_1(a336)
| c0_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21081,c_273]) ).
cnf(c_21084,plain,
( hskp2
| c1_1(a336)
| c0_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36630]) ).
cnf(c_21105,plain,
( ~ hskp21
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21084,c_92]) ).
cnf(c_36631,plain,
( hskp8
| hskp11
| hskp0
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21105,c_21079]) ).
cnf(c_36632,plain,
( hskp8
| hskp11
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36631]) ).
cnf(c_36633,plain,
( hskp8
| hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36632]) ).
cnf(c_21106,plain,
( hskp2
| c1_1(a336)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36633]) ).
cnf(c_21118,plain,
( ~ hskp21
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21106,c_93]) ).
cnf(c_36634,plain,
( hskp8
| hskp11
| hskp0
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21118,c_21079]) ).
cnf(c_36635,plain,
( hskp8
| hskp11
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36634]) ).
cnf(c_36636,plain,
( hskp8
| hskp2
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36635]) ).
cnf(c_21119,plain,
( hskp2
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36636]) ).
cnf(c_21120,plain,
( c1_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21119,c_78]) ).
cnf(c_21121,plain,
( c3_1(a297)
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21120,c_14173]) ).
cnf(c_21147,plain,
( ~ hskp2
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21121,c_123]) ).
cnf(c_36637,plain,
( hskp8
| hskp11
| hskp0
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21147,c_21119]) ).
cnf(c_36638,plain,
( hskp8
| hskp11
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36637]) ).
cnf(c_36639,plain,
( hskp8
| c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36638]) ).
cnf(c_21148,plain,
( c2_1(a297)
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36639]) ).
cnf(c_21153,plain,
( ~ hskp2
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21148,c_122]) ).
cnf(c_36640,plain,
( hskp8
| hskp11
| hskp0
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21153,c_21119]) ).
cnf(c_36641,plain,
( hskp8
| hskp11
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36640]) ).
cnf(c_36642,plain,
( hskp8
| c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36641]) ).
cnf(c_21154,plain,
( c2_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36642]) ).
cnf(c_36643,plain,
( hskp8
| c0_1(a297)
| c3_1(a297)
| ~ c1_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21154,c_220]) ).
cnf(c_21160,plain,
( c0_1(a297)
| c3_1(a297)
| ~ c1_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36643]) ).
cnf(c_36644,plain,
( hskp8
| hskp11
| hskp0
| c0_1(a297)
| c3_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21160,c_21120]) ).
cnf(c_36645,plain,
( hskp8
| hskp11
| c0_1(a297)
| c3_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36644]) ).
cnf(c_36646,plain,
( hskp8
| c0_1(a297)
| c3_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36645]) ).
cnf(c_21175,plain,
( c0_1(a297)
| c3_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36646]) ).
cnf(c_21182,plain,
( ~ hskp2
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21175,c_123]) ).
cnf(c_36647,plain,
( hskp8
| hskp11
| hskp0
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21182,c_21119]) ).
cnf(c_36648,plain,
( hskp8
| hskp11
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36647]) ).
cnf(c_36649,plain,
( hskp8
| c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36648]) ).
cnf(c_21183,plain,
( c0_1(a297)
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36649]) ).
cnf(c_21196,plain,
( ~ hskp2
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21183,c_122]) ).
cnf(c_36650,plain,
( hskp8
| hskp11
| hskp0
| hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21196,c_21119]) ).
cnf(c_36651,plain,
( hskp8
| hskp11
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36650]) ).
cnf(c_36652,plain,
( hskp8
| hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36651]) ).
cnf(c_21197,plain,
( hskp8
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36652]) ).
cnf(c_21198,plain,
( c2_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21197,c_71]) ).
cnf(c_21199,plain,
( hskp1
| c1_1(a305)
| c0_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21198,c_14161]) ).
cnf(c_21219,plain,
( ~ hskp8
| hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21199,c_111]) ).
cnf(c_36653,plain,
( hskp11
| hskp0
| hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21219,c_21197]) ).
cnf(c_36654,plain,
( hskp11
| hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36653]) ).
cnf(c_21231,plain,
( hskp1
| c1_1(a305)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36654]) ).
cnf(c_21233,plain,
( ~ hskp8
| hskp1
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21231,c_112]) ).
cnf(c_36655,plain,
( hskp11
| hskp0
| hskp1
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21233,c_21197]) ).
cnf(c_36656,plain,
( hskp11
| hskp1
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36655]) ).
cnf(c_21234,plain,
( hskp1
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36656]) ).
cnf(c_21235,plain,
( c2_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21234,c_80]) ).
cnf(c_21236,plain,
( c0_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21234,c_79]) ).
cnf(c_36657,plain,
( hskp20
| hskp11
| c1_1(a295)
| ~ c2_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21236,c_264]) ).
cnf(c_21254,plain,
( hskp20
| c1_1(a295)
| ~ c2_1(a295)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36657]) ).
cnf(c_36658,plain,
( hskp11
| hskp0
| hskp20
| c1_1(a295)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21254,c_21235]) ).
cnf(c_36659,plain,
( hskp11
| hskp20
| c1_1(a295)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36658]) ).
cnf(c_21282,plain,
( hskp20
| c1_1(a295)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36659]) ).
cnf(c_21283,plain,
( ~ hskp1
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21282,c_124]) ).
cnf(c_36660,plain,
( hskp11
| hskp0
| hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21283,c_21234]) ).
cnf(c_36661,plain,
( hskp11
| hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36660]) ).
cnf(c_21284,plain,
( hskp20
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36661]) ).
cnf(c_21285,plain,
( c1_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21284,c_52]) ).
cnf(c_21287,plain,
( c3_1(a333)
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21285,c_14173]) ).
cnf(c_21334,plain,
( ~ hskp20
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21287,c_95]) ).
cnf(c_36662,plain,
( hskp11
| hskp0
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21334,c_21284]) ).
cnf(c_36663,plain,
( hskp11
| c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36662]) ).
cnf(c_21336,plain,
( c2_1(a333)
| c0_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36663]) ).
cnf(c_36664,plain,
( hskp21
| c3_1(a333)
| c2_1(a333)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21336,c_275]) ).
cnf(c_21337,plain,
( hskp21
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36664]) ).
cnf(c_36665,plain,
( hskp0
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| ~ c1_1(a333)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21336,c_255]) ).
cnf(c_36666,plain,
( hskp0
| c2_1(A)
| c1_1(A)
| c0_1(A)
| ~ c1_1(a333)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36665]) ).
cnf(c_21339,plain,
( c2_1(A)
| c1_1(A)
| c0_1(A)
| ~ c1_1(a333)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36666]) ).
cnf(c_21349,plain,
( ~ hskp20
| hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21337,c_95]) ).
cnf(c_36667,plain,
( hskp11
| hskp0
| hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21349,c_21284]) ).
cnf(c_36668,plain,
( hskp11
| hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36667]) ).
cnf(c_21350,plain,
( hskp21
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36668]) ).
cnf(c_21356,plain,
( ~ hskp20
| hskp21
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21350,c_94]) ).
cnf(c_36669,plain,
( hskp11
| hskp0
| hskp21
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21356,c_21284]) ).
cnf(c_36670,plain,
( hskp11
| hskp21
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36669]) ).
cnf(c_21357,plain,
( hskp21
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36670]) ).
cnf(c_21358,plain,
( c3_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21357,c_51]) ).
cnf(c_36671,plain,
( hskp0
| hskp2
| c1_1(a336)
| c0_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21358,c_273]) ).
cnf(c_21361,plain,
( hskp2
| c1_1(a336)
| c0_1(a336)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36671]) ).
cnf(c_21383,plain,
( ~ hskp21
| hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21361,c_92]) ).
cnf(c_36672,plain,
( hskp11
| hskp0
| hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21383,c_21357]) ).
cnf(c_36673,plain,
( hskp11
| hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36672]) ).
cnf(c_21384,plain,
( hskp2
| c1_1(a336)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36673]) ).
cnf(c_21387,plain,
( ~ hskp21
| hskp2
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21384,c_93]) ).
cnf(c_36674,plain,
( hskp11
| hskp0
| hskp2
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21387,c_21357]) ).
cnf(c_36675,plain,
( hskp11
| hskp2
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36674]) ).
cnf(c_21388,plain,
( hskp2
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36675]) ).
cnf(c_21389,plain,
( c1_1(a297)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21388,c_78]) ).
cnf(c_21662,plain,
( ~ hskp26
| hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_18572,c_82]) ).
cnf(c_36676,plain,
( hskp12
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_21662,c_36]) ).
cnf(c_36677,plain,
( hskp12
| hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36676]) ).
cnf(c_21665,plain,
( hskp10
| hskp0
| hskp11
| hskp12
| c0_1(a315)
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36677]) ).
cnf(c_21672,plain,
( ~ hskp14
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_21665,c_103]) ).
cnf(c_36678,plain,
( hskp0
| hskp10
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(resolve,[status(thm)],[c_21672,c_16665]) ).
cnf(c_36679,plain,
( hskp0
| hskp10
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36678]) ).
cnf(c_36680,plain,
( hskp0
| hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36679]) ).
cnf(c_21674,plain,
( hskp10
| hskp0
| hskp11
| hskp12
| c2_1(a349) ),
inference(copy,[status(thm)],[c_36680]) ).
cnf(c_21682,plain,
( ~ hskp26
| hskp10
| hskp0
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21674,c_81]) ).
cnf(c_36681,plain,
( hskp12
| hskp11
| hskp10
| hskp0
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21682,c_36]) ).
cnf(c_36682,plain,
( hskp12
| hskp10
| hskp0
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36681]) ).
cnf(c_21684,plain,
( hskp10
| hskp0
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36682]) ).
cnf(c_36683,plain,
( hskp10
| hskp12
| hskp11
| c1_1(a294)
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21684,c_11964]) ).
cnf(c_36684,plain,
( hskp10
| hskp12
| c1_1(a294)
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36683]) ).
cnf(c_36685,plain,
( hskp10
| c1_1(a294)
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36684]) ).
cnf(c_21685,plain,
( c1_1(a294)
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36685]) ).
cnf(c_21696,plain,
( ~ hskp0
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21685,c_126]) ).
cnf(c_36686,plain,
( hskp10
| hskp11
| hskp12
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21696,c_21684]) ).
cnf(c_36687,plain,
( hskp10
| hskp11
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36686]) ).
cnf(c_36688,plain,
( hskp10
| c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36687]) ).
cnf(c_21697,plain,
( c1_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36688]) ).
cnf(c_21698,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21697,c_14173]) ).
cnf(c_36689,plain,
( hskp11
| hskp10
| c2_1(a294)
| c0_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21698,c_270]) ).
cnf(c_36690,plain,
( hskp11
| hskp10
| c2_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36689]) ).
cnf(c_36691,plain,
( hskp11
| hskp10
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36690]) ).
cnf(c_36692,plain,
( hskp11
| c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36691]) ).
cnf(c_21730,plain,
( c2_1(a294)
| c0_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36692]) ).
cnf(c_21735,plain,
( ~ hskp0
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21730,c_125]) ).
cnf(c_36693,plain,
( hskp10
| hskp11
| hskp12
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21735,c_21684]) ).
cnf(c_36694,plain,
( hskp10
| hskp11
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36693]) ).
cnf(c_36695,plain,
( hskp10
| c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36694]) ).
cnf(c_21736,plain,
( c2_1(a294)
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36695]) ).
cnf(c_21752,plain,
( ~ hskp0
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21736,c_126]) ).
cnf(c_36696,plain,
( hskp10
| hskp11
| hskp12
| hskp10
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21752,c_21684]) ).
cnf(c_36697,plain,
( hskp10
| hskp11
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36696]) ).
cnf(c_36698,plain,
( hskp10
| hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36697]) ).
cnf(c_21753,plain,
( hskp10
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36698]) ).
cnf(c_21754,plain,
( c3_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21753,c_69]) ).
cnf(c_21755,plain,
( c1_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21753,c_68]) ).
cnf(c_21756,plain,
( c2_1(a308)
| ~ c1_1(a308)
| ~ c0_1(a321)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21754,c_14166]) ).
cnf(c_21763,plain,
( hskp28
| ~ c2_1(a308)
| ~ c1_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21754,c_259]) ).
cnf(c_21769,plain,
( c2_1(a308)
| ~ c1_1(a308)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21754,c_235]) ).
cnf(c_36699,plain,
( hskp4
| c1_1(A)
| c1_1(a313)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp4 ),
inference(resolve,[status(thm)],[c_16174,c_16127]) ).
cnf(c_23587,plain,
( c1_1(A)
| c1_1(a313)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp4 ),
inference(copy,[status(thm)],[c_36699]) ).
cnf(c_36700,plain,
( hskp4
| c1_1(a295)
| c1_1(a313)
| ~ c2_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_23587,c_14202]) ).
cnf(c_23603,plain,
( c1_1(a295)
| c1_1(a313)
| ~ c2_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_36700]) ).
cnf(c_36701,plain,
( hskp4
| c1_1(a295)
| c1_1(a313)
| hskp4 ),
inference(resolve,[status(thm)],[c_23603,c_14201]) ).
cnf(c_23611,plain,
( c1_1(a295)
| c1_1(a313)
| hskp4 ),
inference(copy,[status(thm)],[c_36701]) ).
cnf(c_23615,plain,
( ~ hskp13
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_23611,c_104]) ).
cnf(c_36702,plain,
( hskp4
| c1_1(a295)
| hskp4 ),
inference(resolve,[status(thm)],[c_23615,c_16125]) ).
cnf(c_23617,plain,
( c1_1(a295)
| hskp4 ),
inference(copy,[status(thm)],[c_36702]) ).
cnf(c_23630,plain,
( ~ hskp1
| hskp4 ),
inference(resolve,[status(thm)],[c_23617,c_124]) ).
cnf(c_36703,plain,
( hskp4
| hskp4 ),
inference(resolve,[status(thm)],[c_23630,c_14200]) ).
cnf(c_23636,plain,
hskp4,
inference(copy,[status(thm)],[c_36703]) ).
cnf(c_23641,plain,
~ c2_1(a300),
inference(resolve,[status(thm)],[c_23636,c_120]) ).
cnf(c_23642,plain,
~ c1_1(a300),
inference(resolve,[status(thm)],[c_23636,c_119]) ).
cnf(c_23643,plain,
~ c0_1(a300),
inference(resolve,[status(thm)],[c_23636,c_118]) ).
cnf(c_36704,plain,
( hskp11
| hskp0
| c0_1(a297)
| c3_1(a349)
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_18022,c_21389]) ).
cnf(c_36705,plain,
( hskp11
| c0_1(a297)
| c3_1(a349)
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36704]) ).
cnf(c_24619,plain,
( c0_1(a297)
| c3_1(a349)
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36705]) ).
cnf(c_24642,plain,
( ~ hskp26
| c0_1(a297)
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24619,c_82]) ).
cnf(c_36706,plain,
( hskp12
| hskp11
| c0_1(a297)
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24642,c_36]) ).
cnf(c_36707,plain,
( hskp12
| c0_1(a297)
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36706]) ).
cnf(c_24644,plain,
( c0_1(a297)
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36707]) ).
cnf(c_24656,plain,
( ~ hskp2
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24644,c_122]) ).
cnf(c_36708,plain,
( hskp11
| hskp0
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24656,c_21388]) ).
cnf(c_36709,plain,
( hskp11
| c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36708]) ).
cnf(c_24658,plain,
( c2_1(a349)
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36709]) ).
cnf(c_24699,plain,
( ~ hskp26
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24658,c_81]) ).
cnf(c_36710,plain,
( hskp12
| hskp11
| hskp12
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_24699,c_36]) ).
cnf(c_36711,plain,
( hskp12
| hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36710]) ).
cnf(c_24700,plain,
( hskp12
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36711]) ).
cnf(c_24701,plain,
( c1_1(a294)
| c2_1(a294)
| c0_1(a294)
| c0_1(a321)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24700,c_19801]) ).
cnf(c_24708,plain,
( ~ hskp0
| c1_1(a294)
| c2_1(a294)
| c0_1(a321)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24701,c_125]) ).
cnf(c_36712,plain,
( hskp12
| hskp11
| c1_1(a294)
| c2_1(a294)
| c0_1(a321)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24708,c_24700]) ).
cnf(c_36713,plain,
( hskp12
| c1_1(a294)
| c2_1(a294)
| c0_1(a321)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36712]) ).
cnf(c_24724,plain,
( c1_1(a294)
| c2_1(a294)
| c0_1(a321)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36713]) ).
cnf(c_36714,plain,
( c2_1(a308)
| ~ c1_1(a308)
| hskp11
| hskp12
| c1_1(a294)
| c2_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24724,c_21756]) ).
cnf(c_36715,plain,
( c2_1(a308)
| ~ c1_1(a308)
| hskp11
| c1_1(a294)
| c2_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36714]) ).
cnf(c_24730,plain,
( c2_1(a308)
| ~ c1_1(a308)
| c1_1(a294)
| c2_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36715]) ).
cnf(c_36716,plain,
( hskp11
| hskp12
| c2_1(a308)
| c1_1(a294)
| c2_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24730,c_21755]) ).
cnf(c_36717,plain,
( hskp11
| c2_1(a308)
| c1_1(a294)
| c2_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36716]) ).
cnf(c_24750,plain,
( c2_1(a308)
| c1_1(a294)
| c2_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36717]) ).
cnf(c_24757,plain,
( ~ hskp0
| c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24750,c_126]) ).
cnf(c_36718,plain,
( hskp12
| hskp11
| c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24757,c_24700]) ).
cnf(c_36719,plain,
( hskp12
| c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36718]) ).
cnf(c_24761,plain,
( c2_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36719]) ).
cnf(c_36720,plain,
( hskp28
| ~ c1_1(a308)
| hskp11
| hskp12
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24761,c_21763]) ).
cnf(c_36721,plain,
( hskp28
| ~ c1_1(a308)
| hskp11
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36720]) ).
cnf(c_24762,plain,
( hskp28
| ~ c1_1(a308)
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36721]) ).
cnf(c_36722,plain,
( hskp11
| hskp12
| hskp28
| c1_1(a294)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24762,c_21755]) ).
cnf(c_36723,plain,
( hskp11
| hskp28
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36722]) ).
cnf(c_24769,plain,
( hskp28
| c1_1(a294)
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36723]) ).
cnf(c_24771,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24769,c_14173]) ).
cnf(c_24800,plain,
( ~ hskp0
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24771,c_127]) ).
cnf(c_36724,plain,
( hskp12
| hskp11
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24800,c_24700]) ).
cnf(c_36725,plain,
( hskp12
| c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36724]) ).
cnf(c_24801,plain,
( c2_1(a294)
| c0_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36725]) ).
cnf(c_24806,plain,
( ~ hskp0
| c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24801,c_125]) ).
cnf(c_36726,plain,
( hskp12
| hskp11
| c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24806,c_24700]) ).
cnf(c_36727,plain,
( hskp12
| c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36726]) ).
cnf(c_24807,plain,
( c2_1(a294)
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36727]) ).
cnf(c_24818,plain,
( ~ hskp0
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24807,c_126]) ).
cnf(c_36728,plain,
( hskp12
| hskp11
| hskp28
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24818,c_24700]) ).
cnf(c_36729,plain,
( hskp12
| hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36728]) ).
cnf(c_24819,plain,
( hskp28
| hskp12
| hskp11 ),
inference(copy,[status(thm)],[c_36729]) ).
cnf(c_24820,plain,
( c3_1(a353)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24819,c_43]) ).
cnf(c_24821,plain,
( c2_1(a353)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24819,c_42]) ).
cnf(c_24822,plain,
( c1_1(a353)
| hskp12
| hskp11 ),
inference(resolve,[status(thm)],[c_24819,c_41]) ).
cnf(c_25395,plain,
( ~ hskp0
| c1_1(a294)
| c0_1(a294)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_14168,c_127]) ).
cnf(c_36730,plain,
( hskp12
| hskp11
| c0_1(a353)
| c3_1(a333)
| ~ c1_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_17643,c_24821]) ).
cnf(c_36731,plain,
( hskp12
| c0_1(a353)
| c3_1(a333)
| ~ c1_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36730]) ).
cnf(c_29402,plain,
( c0_1(a353)
| c3_1(a333)
| ~ c1_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36731]) ).
cnf(c_36732,plain,
( hskp12
| hskp11
| c0_1(a353)
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_29402,c_24822]) ).
cnf(c_36733,plain,
( hskp12
| c0_1(a353)
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36732]) ).
cnf(c_29409,plain,
( c0_1(a353)
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36733]) ).
cnf(c_29428,plain,
( ~ hskp20
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_29409,c_95]) ).
cnf(c_36734,plain,
( hskp11
| hskp12
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_29428,c_17469]) ).
cnf(c_36735,plain,
( hskp11
| c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36734]) ).
cnf(c_29431,plain,
( c0_1(a353)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36735]) ).
cnf(c_36736,plain,
( hskp11
| hskp0
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_21339,c_21285]) ).
cnf(c_36737,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36736]) ).
cnf(c_29867,plain,
( c2_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36737]) ).
cnf(c_36738,plain,
( c2_1(a300)
| c1_1(a300)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_29867,c_23643]) ).
cnf(c_36739,plain,
( c2_1(a300)
| c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_23642,c_36738]) ).
cnf(c_29868,plain,
( c2_1(a333)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_23641,c_36739]) ).
cnf(c_29878,plain,
( ~ hskp20
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_29868,c_94]) ).
cnf(c_36740,plain,
( hskp11
| hskp0
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_29878,c_21284]) ).
cnf(c_36741,plain,
( hskp11
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36740]) ).
cnf(c_29881,plain,
( hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_36741]) ).
cnf(c_29882,plain,
( c1_1(a294)
| c2_1(a294)
| c0_1(a294)
| c0_1(a321)
| hskp11 ),
inference(resolve,[status(thm)],[c_29881,c_19801]) ).
cnf(c_29889,plain,
( ~ hskp0
| c1_1(a294)
| c2_1(a294)
| c0_1(a321)
| hskp11 ),
inference(resolve,[status(thm)],[c_29882,c_125]) ).
cnf(c_36742,plain,
( hskp11
| c1_1(a294)
| c2_1(a294)
| c0_1(a321)
| hskp11 ),
inference(resolve,[status(thm)],[c_29889,c_29881]) ).
cnf(c_29890,plain,
( c1_1(a294)
| c2_1(a294)
| c0_1(a321)
| hskp11 ),
inference(copy,[status(thm)],[c_36742]) ).
cnf(c_36743,plain,
( hskp20
| hskp11
| c1_1(a321)
| ~ c2_1(a321)
| c1_1(a294)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_29890,c_264]) ).
cnf(c_36744,plain,
( hskp20
| c1_1(a321)
| ~ c2_1(a321)
| c1_1(a294)
| c2_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_36743]) ).
cnf(c_36745,plain,
( hskp20
| c1_1(a321)
| c1_1(a294)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_14021,c_36744]) ).
cnf(c_29915,plain,
( hskp20
| c1_1(a294)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_14019,c_36745]) ).
cnf(c_29921,plain,
( ~ hskp0
| hskp20
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_29915,c_126]) ).
cnf(c_36746,plain,
( hskp11
| hskp20
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_29921,c_29881]) ).
cnf(c_29922,plain,
( hskp20
| c1_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_36746]) ).
cnf(c_29926,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp20
| hskp11 ),
inference(resolve,[status(thm)],[c_29922,c_14173]) ).
cnf(c_29966,plain,
( ~ hskp0
| c2_1(a294)
| c0_1(a294)
| hskp20
| hskp11 ),
inference(resolve,[status(thm)],[c_29926,c_127]) ).
cnf(c_36747,plain,
( hskp11
| c2_1(a294)
| c0_1(a294)
| hskp20
| hskp11 ),
inference(resolve,[status(thm)],[c_29966,c_29881]) ).
cnf(c_29967,plain,
( c2_1(a294)
| c0_1(a294)
| hskp20
| hskp11 ),
inference(copy,[status(thm)],[c_36747]) ).
cnf(c_29971,plain,
( ~ hskp0
| c2_1(a294)
| hskp20
| hskp11 ),
inference(resolve,[status(thm)],[c_29967,c_125]) ).
cnf(c_36748,plain,
( hskp11
| c2_1(a294)
| hskp20
| hskp11 ),
inference(resolve,[status(thm)],[c_29971,c_29881]) ).
cnf(c_29972,plain,
( c2_1(a294)
| hskp20
| hskp11 ),
inference(copy,[status(thm)],[c_36748]) ).
cnf(c_29981,plain,
( ~ hskp0
| hskp20
| hskp11 ),
inference(resolve,[status(thm)],[c_29972,c_126]) ).
cnf(c_36749,plain,
( hskp11
| hskp20
| hskp11 ),
inference(resolve,[status(thm)],[c_29981,c_29881]) ).
cnf(c_29982,plain,
( hskp20
| hskp11 ),
inference(copy,[status(thm)],[c_36749]) ).
cnf(c_36750,plain,
( hskp12
| hskp11
| c2_1(a308)
| ~ c1_1(a308)
| ~ c2_1(a353)
| ~ c0_1(a353)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_21769,c_24820]) ).
cnf(c_36751,plain,
( hskp12
| c2_1(a308)
| ~ c1_1(a308)
| ~ c2_1(a353)
| ~ c0_1(a353)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36750]) ).
cnf(c_30367,plain,
( c2_1(a308)
| ~ c1_1(a308)
| ~ c2_1(a353)
| ~ c0_1(a353)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36751]) ).
cnf(c_36752,plain,
( c2_1(a333)
| hskp11
| hskp12
| c2_1(a308)
| ~ c1_1(a308)
| ~ c2_1(a353)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30367,c_29431]) ).
cnf(c_36753,plain,
( c2_1(a333)
| hskp11
| c2_1(a308)
| ~ c1_1(a308)
| ~ c2_1(a353)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36752]) ).
cnf(c_30372,plain,
( c2_1(a333)
| c2_1(a308)
| ~ c1_1(a308)
| ~ c2_1(a353)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36753]) ).
cnf(c_36754,plain,
( hskp12
| hskp11
| c2_1(a333)
| c2_1(a308)
| ~ c1_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30372,c_24821]) ).
cnf(c_36755,plain,
( hskp12
| c2_1(a333)
| c2_1(a308)
| ~ c1_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36754]) ).
cnf(c_30380,plain,
( c2_1(a333)
| c2_1(a308)
| ~ c1_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36755]) ).
cnf(c_36756,plain,
( hskp11
| hskp12
| c2_1(a333)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30380,c_21755]) ).
cnf(c_36757,plain,
( hskp11
| c2_1(a333)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36756]) ).
cnf(c_30381,plain,
( c2_1(a333)
| c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36757]) ).
cnf(c_30386,plain,
( ~ hskp20
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30381,c_94]) ).
cnf(c_36758,plain,
( hskp11
| c2_1(a308)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30386,c_29982]) ).
cnf(c_30390,plain,
( c2_1(a308)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36758]) ).
cnf(c_36759,plain,
( c0_1(a308)
| c3_1(a333)
| ~ c1_1(a308)
| c2_1(a333)
| hskp11
| hskp12
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30390,c_17643]) ).
cnf(c_36760,plain,
( c0_1(a308)
| c3_1(a333)
| ~ c1_1(a308)
| c2_1(a333)
| hskp11
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36759]) ).
cnf(c_30391,plain,
( c0_1(a308)
| c3_1(a333)
| ~ c1_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36760]) ).
cnf(c_36761,plain,
( hskp11
| hskp12
| c0_1(a308)
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30391,c_21755]) ).
cnf(c_36762,plain,
( hskp11
| c0_1(a308)
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36761]) ).
cnf(c_30398,plain,
( c0_1(a308)
| c3_1(a333)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36762]) ).
cnf(c_30415,plain,
( ~ hskp20
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30398,c_95]) ).
cnf(c_36763,plain,
( hskp11
| c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30415,c_29982]) ).
cnf(c_30416,plain,
( c0_1(a308)
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36763]) ).
cnf(c_30418,plain,
( ~ hskp10
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30416,c_108]) ).
cnf(c_36764,plain,
( hskp11
| hskp12
| c2_1(a333)
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30418,c_21753]) ).
cnf(c_36765,plain,
( hskp11
| c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36764]) ).
cnf(c_30420,plain,
( c2_1(a333)
| hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36765]) ).
cnf(c_30431,plain,
( ~ hskp20
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30420,c_94]) ).
cnf(c_36766,plain,
( hskp11
| hskp11
| hskp12 ),
inference(resolve,[status(thm)],[c_30431,c_29982]) ).
cnf(c_30432,plain,
( hskp11
| hskp12 ),
inference(copy,[status(thm)],[c_36766]) ).
cnf(c_30435,plain,
( c3_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30432,c_65]) ).
cnf(c_36767,plain,
( hskp11
| hskp10
| c2_1(a310)
| c0_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30435,c_270]) ).
cnf(c_30455,plain,
( hskp10
| c2_1(a310)
| c0_1(a310)
| hskp11 ),
inference(copy,[status(thm)],[c_36767]) ).
cnf(c_30477,plain,
( ~ hskp12
| hskp10
| c2_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30455,c_105]) ).
cnf(c_36768,plain,
( hskp11
| hskp10
| c2_1(a310)
| hskp11 ),
inference(resolve,[status(thm)],[c_30477,c_30432]) ).
cnf(c_30478,plain,
( hskp10
| c2_1(a310)
| hskp11 ),
inference(copy,[status(thm)],[c_36768]) ).
cnf(c_30488,plain,
( ~ hskp12
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_30478,c_106]) ).
cnf(c_36769,plain,
( hskp11
| hskp10
| hskp11 ),
inference(resolve,[status(thm)],[c_30488,c_30432]) ).
cnf(c_30489,plain,
( hskp10
| hskp11 ),
inference(copy,[status(thm)],[c_36769]) ).
cnf(c_30490,plain,
( c3_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30489,c_69]) ).
cnf(c_30491,plain,
( c1_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30489,c_68]) ).
cnf(c_30522,plain,
( c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a308)
| ~ c2_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30490,c_216]) ).
cnf(c_30535,plain,
( c3_1(A)
| c2_1(A)
| c0_1(A)
| c2_1(a308)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30491,c_14169]) ).
cnf(c_30971,plain,
( ~ hskp0
| c2_1(a294)
| c0_1(a294)
| c2_1(a308)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30535,c_127]) ).
cnf(c_36770,plain,
( hskp11
| c2_1(a294)
| c0_1(a294)
| c2_1(a308)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30971,c_29881]) ).
cnf(c_30975,plain,
( c2_1(a294)
| c0_1(a294)
| c2_1(a308)
| c0_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_36770]) ).
cnf(c_30979,plain,
( ~ hskp0
| c2_1(a294)
| c2_1(a308)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30975,c_125]) ).
cnf(c_36771,plain,
( hskp11
| c2_1(a294)
| c2_1(a308)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30979,c_29881]) ).
cnf(c_30981,plain,
( c2_1(a294)
| c2_1(a308)
| c0_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_36771]) ).
cnf(c_30983,plain,
( ~ hskp10
| c2_1(a294)
| c2_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30981,c_108]) ).
cnf(c_36772,plain,
( hskp11
| c2_1(a294)
| c2_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30983,c_30489]) ).
cnf(c_30985,plain,
( c2_1(a294)
| c2_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_36772]) ).
cnf(c_31001,plain,
( ~ hskp0
| c2_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30985,c_126]) ).
cnf(c_36773,plain,
( hskp11
| c2_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_31001,c_29881]) ).
cnf(c_31007,plain,
( c2_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_36773]) ).
cnf(c_36774,plain,
( hskp11
| c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_30522,c_31007]) ).
cnf(c_35999,plain,
( c1_1(A)
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_36774]) ).
cnf(c_36001,plain,
( ~ hskp0
| c1_1(a294)
| c2_1(a294)
| c0_1(a294)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_35999,c_127]) ).
cnf(c_36775,plain,
( hskp11
| c1_1(a294)
| c2_1(a294)
| c0_1(a294)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_36001,c_29881]) ).
cnf(c_36004,plain,
( c1_1(a294)
| c2_1(a294)
| c0_1(a294)
| c0_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_36775]) ).
cnf(c_36006,plain,
( ~ hskp0
| c1_1(a294)
| c2_1(a294)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_36004,c_125]) ).
cnf(c_36776,plain,
( hskp11
| c1_1(a294)
| c2_1(a294)
| c0_1(a308)
| hskp11 ),
inference(resolve,[status(thm)],[c_36006,c_29881]) ).
cnf(c_36009,plain,
( c1_1(a294)
| c2_1(a294)
| c0_1(a308)
| hskp11 ),
inference(copy,[status(thm)],[c_36776]) ).
cnf(c_36012,plain,
( ~ hskp10
| c1_1(a294)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36009,c_108]) ).
cnf(c_36777,plain,
( hskp11
| c1_1(a294)
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36012,c_30489]) ).
cnf(c_36013,plain,
( c1_1(a294)
| c2_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_36777]) ).
cnf(c_36022,plain,
( ~ hskp0
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36013,c_126]) ).
cnf(c_36778,plain,
( hskp11
| c1_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36022,c_29881]) ).
cnf(c_36025,plain,
( c1_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_36778]) ).
cnf(c_36044,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36025,c_14173]) ).
cnf(c_36103,plain,
( ~ hskp0
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36044,c_127]) ).
cnf(c_36779,plain,
( hskp11
| c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36103,c_29881]) ).
cnf(c_36104,plain,
( c2_1(a294)
| c0_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_36779]) ).
cnf(c_36105,plain,
( ~ hskp0
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36104,c_125]) ).
cnf(c_36780,plain,
( hskp11
| c2_1(a294)
| hskp11 ),
inference(resolve,[status(thm)],[c_36105,c_29881]) ).
cnf(c_36132,plain,
( c2_1(a294)
| hskp11 ),
inference(copy,[status(thm)],[c_36780]) ).
cnf(c_36145,plain,
( ~ hskp0
| hskp11 ),
inference(resolve,[status(thm)],[c_36132,c_126]) ).
cnf(c_36781,plain,
( hskp11
| hskp11 ),
inference(resolve,[status(thm)],[c_36145,c_29881]) ).
cnf(c_36146,plain,
hskp11,
inference(copy,[status(thm)],[c_36781]) ).
cnf(c_36147,plain,
~ c2_1(a309),
inference(resolve,[status(thm)],[c_36146,c_107]) ).
cnf(c_36148,plain,
c3_1(a309),
inference(resolve,[status(thm)],[c_36146,c_67]) ).
cnf(c_36149,plain,
c1_1(a309),
inference(resolve,[status(thm)],[c_36146,c_66]) ).
cnf(c_36782,plain,
( c2_1(a309)
| ~ c1_1(a309)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_36148,c_14166]) ).
cnf(c_36783,plain,
( c2_1(a309)
| ~ c0_1(a321) ),
inference(resolve,[status(thm)],[c_36149,c_36782]) ).
cnf(c_36210,plain,
~ c0_1(a321),
inference(resolve,[status(thm)],[c_36147,c_36783]) ).
cnf(c_36784,plain,
( hskp0
| c0_1(a321)
| c2_1(a309)
| ~ c1_1(a309) ),
inference(resolve,[status(thm)],[c_36148,c_14162]) ).
cnf(c_36785,plain,
( hskp0
| c0_1(a321)
| c2_1(a309) ),
inference(resolve,[status(thm)],[c_36149,c_36784]) ).
cnf(c_36786,plain,
( hskp0
| c0_1(a321) ),
inference(resolve,[status(thm)],[c_36147,c_36785]) ).
cnf(c_36211,plain,
hskp0,
inference(resolve,[status(thm)],[c_36210,c_36786]) ).
cnf(c_36787,plain,
( ~ hskp0
| c1_1(a294)
| c0_1(a294)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_36210,c_25395]) ).
cnf(c_36350,plain,
( c1_1(a294)
| c0_1(a294)
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_36211,c_36787]) ).
cnf(c_36373,plain,
~ c3_1(a294),
inference(resolve,[status(thm)],[c_36211,c_127]) ).
cnf(c_36374,plain,
~ c2_1(a294),
inference(resolve,[status(thm)],[c_36211,c_126]) ).
cnf(c_36375,plain,
~ c0_1(a294),
inference(resolve,[status(thm)],[c_36211,c_125]) ).
cnf(c_36788,plain,
( c1_1(a294)
| c3_1(a294)
| c2_1(a294)
| c0_1(a294) ),
inference(factor,[status(thm)],[c_36350]) ).
cnf(c_36789,plain,
( c1_1(a294)
| c3_1(a294)
| c2_1(a294) ),
inference(resolve,[status(thm)],[c_36375,c_36788]) ).
cnf(c_36790,plain,
( c1_1(a294)
| c3_1(a294) ),
inference(resolve,[status(thm)],[c_36374,c_36789]) ).
cnf(c_36377,plain,
c1_1(a294),
inference(resolve,[status(thm)],[c_36373,c_36790]) ).
cnf(c_36791,plain,
( c3_1(a294)
| c2_1(a294)
| c0_1(a294) ),
inference(resolve,[status(thm)],[c_36377,c_14173]) ).
cnf(c_36792,plain,
( c3_1(a294)
| c2_1(a294) ),
inference(resolve,[status(thm)],[c_36375,c_36791]) ).
cnf(c_36793,plain,
c3_1(a294),
inference(resolve,[status(thm)],[c_36374,c_36792]) ).
cnf(c_36439,plain,
$false,
inference(resolve,[status(thm)],[c_36373,c_36793]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN445-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n002.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 17:49:53 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 2329472 was started by sandbox2 on n002,
% 0.18/0.45 % Sat Sep 26 17:49:53 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.46
% 0.18/0.46 % From the command line: assign(max_seconds, 300).
% 192.40/25.91
% 192.40/25.91 % given #500 (T,wt=8): 516 hskp0 | hskp16 | c0_1(a297) | c2_1(a297) | hskp8 | hskp5. [resolve(513,c,271,a)].
% 192.40/25.91
% 192.40/25.91 % given #1000 (T,wt=6): 3188 hskp16 | hskp12 | hskp8 | hskp23 | hskp24 | -hskp19. [resolve(3163,d,96,a)].
% 192.40/25.91
% 192.40/25.91 % given #1500 (T,wt=7): 5639 hskp6 | hskp17 | hskp5 | hskp4 | hskp0 | c1_1(a297). [resolve(5631,e,78,a)].
% 192.40/25.91
% 192.40/25.91 % given #2000 (T,wt=9): 8064 hskp11 | hskp17 | hskp4 | hskp12 | c3_1(a330) | c0_1(a330) | hskp8. [resolve(2968,e,2959,e),merge(h),merge(i),merge(j),merge(k)].
% 192.40/25.91
% 192.40/25.91 % given #2500 (T,wt=4): 10627 hskp27 | hskp16 | hskp22 | -hskp0. [resolve(10606,c,126,a)].
% 192.40/25.91
% 192.40/25.91 % given #3000 (T,wt=7): 12973 hskp10 | hskp11 | hskp4 | hskp8 | hskp5 | hskp21 | -hskp20. [resolve(12962,d,94,a)].
% 192.40/25.91
% 192.40/25.91 % given #3500 (T,wt=4): 15951 hskp1 | hskp11 | c3_1(a336). [resolve(15950,c,51,a)].
% 192.40/25.91
% 192.40/25.91 % given #4000 (T,wt=8): 17978 c0_1(a297) | c2_1(a297) | hskp0 | hskp11 | hskp12 | hskp10. [resolve(15093,c,270,a),merge(f),merge(g),merge(i)].
% 192.40/25.91
% 192.40/25.91 % given #4500 (T,wt=10): 15712 c2_1(a333) | hskp4 | hskp11 | -c1_1(a333) | c3_1(a333) | hskp23 | hskp24. [resolve(15710,a,261,a)].
% 192.40/25.91
% 192.40/25.91 % given #5000 (T,wt=7): 21926 hskp12 | hskp11 | c2_1(a308) | c2_1(a333) | hskp3. [resolve(21795,c,21755,c),merge(f),merge(g)].
% 192.40/25.91
% 192.40/25.91 % given #5500 (T,wt=6): 23853 hskp10 | hskp11 | hskp27 | -c1_1(a354) | hskp28. [resolve(23730,e,202,a),merge(f),merge(g)].
% 192.40/25.91
% 192.40/25.91 % given #6000 (T,wt=10): 25985 hskp27 | -c1_1(A) | c1_1(a299) | c0_1(A) | c2_1(A) | hskp5. [resolve(14248,b,14185,b),merge(g)].
% 192.40/25.91
% 192.40/25.91 % given #6500 (T,wt=8): 27893 hskp11 | hskp7 | hskp23 | -c1_1(a342) | -c2_1(a342) | hskp28. [resolve(27888,d,259,c)].
% 192.40/25.91
% 192.40/25.91 % given #7000 (T,wt=6): 29942 hskp11 | hskp20 | c2_1(a294) | hskp22 | -hskp0. [resolve(29929,d,127,a)].
% 192.40/25.91
% 192.40/25.91 % given #7500 (T,wt=11): 31648 hskp12 | hskp7 | hskp10 | hskp2 | hskp0 | -c1_1(a330) | c3_1(a330) | hskp23 | hskp24. [resolve(31646,d,261,a)].
% 192.40/25.91
% 192.40/25.91 % given #8000 (T,wt=11): 33190 hskp11 | -c0_1(a299) | -c2_1(a299) | -c0_1(A) | -c2_1(A) | c3_1(A). [resolve(33167,b,234,c),merge(g)].
% 192.40/25.91
% 192.40/25.91 % given #8500 (T,wt=12): 34644 c0_1(a342) | c2_1(a342) | hskp9 | hskp17 | hskp5 | hskp27 | hskp10 | -c1_1(a354) | hskp21. [resolve(25489,h,200,a),merge(j),merge(k)].
% 192.40/25.91
% 192.40/25.91 % SZS status Unsatisfiable for theBenchmark
% 192.40/25.91
% 192.40/25.91 % Proof 1 at 20.97 (+ 4.24) seconds.
% 192.40/25.91 % Length of proof is 487.
% 192.40/25.91 % Level of proof is 184.
% 192.40/25.91 % Maximum clause weight is 19.000.
% 192.40/25.91 % Given clauses 8859.
% 192.40/25.91
% 192.40/25.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------