%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN451-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:26 AM UTC 2026
% Result : Unsatisfiable 156.54s 21.15s
% Output : CNFRefutation 156.54s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(clause1,axiom,
( hskp8
| hskp0 ),
file('theBenchmark.p',clause1) ).
cnf(c_1,plain,
( hskp8
| hskp0 ),
inference(clausify,[status(thm)],[clause1]) ).
fof(clause22,axiom,
( ndr1_0
| ~ hskp8 ),
file('theBenchmark.p',clause22) ).
cnf(c_22,plain,
( ndr1_0
| ~ hskp8 ),
inference(clausify,[status(thm)],[clause22]) ).
fof(clause30,axiom,
( ndr1_0
| ~ hskp0 ),
file('theBenchmark.p',clause30) ).
cnf(c_30,plain,
( ndr1_0
| ~ hskp0 ),
inference(clausify,[status(thm)],[clause30]) ).
fof(clause32,axiom,
( hskp13
| hskp24
| hskp23 ),
file('theBenchmark.p',clause32) ).
cnf(c_32,plain,
( hskp13
| hskp24
| hskp23 ),
inference(clausify,[status(thm)],[clause32]) ).
fof(clause35,axiom,
( hskp4
| hskp1
| hskp7 ),
file('theBenchmark.p',clause35) ).
cnf(c_35,plain,
( hskp4
| hskp1
| hskp7 ),
inference(clausify,[status(thm)],[clause35]) ).
fof(clause36,axiom,
( c0_1(a784)
| ~ hskp28 ),
file('theBenchmark.p',clause36) ).
cnf(c_36,plain,
( c0_1(a784)
| ~ hskp28 ),
inference(clausify,[status(thm)],[clause36]) ).
fof(clause37,axiom,
( c1_1(a784)
| ~ hskp28 ),
file('theBenchmark.p',clause37) ).
cnf(c_37,plain,
( c1_1(a784)
| ~ hskp28 ),
inference(clausify,[status(thm)],[clause37]) ).
fof(clause38,axiom,
( c3_1(a784)
| ~ hskp28 ),
file('theBenchmark.p',clause38) ).
cnf(c_38,plain,
( c3_1(a784)
| ~ hskp28 ),
inference(clausify,[status(thm)],[clause38]) ).
fof(clause39,axiom,
( c0_1(a750)
| ~ hskp27 ),
file('theBenchmark.p',clause39) ).
cnf(c_39,plain,
( c0_1(a750)
| ~ hskp27 ),
inference(clausify,[status(thm)],[clause39]) ).
fof(clause40,axiom,
( c1_1(a750)
| ~ hskp27 ),
file('theBenchmark.p',clause40) ).
cnf(c_40,plain,
( c1_1(a750)
| ~ hskp27 ),
inference(clausify,[status(thm)],[clause40]) ).
fof(clause41,axiom,
( c2_1(a750)
| ~ hskp27 ),
file('theBenchmark.p',clause41) ).
cnf(c_41,plain,
( c2_1(a750)
| ~ hskp27 ),
inference(clausify,[status(thm)],[clause41]) ).
fof(clause45,axiom,
( c0_1(a729)
| ~ hskp25 ),
file('theBenchmark.p',clause45) ).
cnf(c_45,plain,
( c0_1(a729)
| ~ hskp25 ),
inference(clausify,[status(thm)],[clause45]) ).
fof(clause46,axiom,
( c2_1(a729)
| ~ hskp25 ),
file('theBenchmark.p',clause46) ).
cnf(c_46,plain,
( c2_1(a729)
| ~ hskp25 ),
inference(clausify,[status(thm)],[clause46]) ).
fof(clause47,axiom,
( c3_1(a729)
| ~ hskp25 ),
file('theBenchmark.p',clause47) ).
cnf(c_47,plain,
( c3_1(a729)
| ~ hskp25 ),
inference(clausify,[status(thm)],[clause47]) ).
fof(clause48,axiom,
( c0_1(a802)
| ~ hskp24 ),
file('theBenchmark.p',clause48) ).
cnf(c_48,plain,
( c0_1(a802)
| ~ hskp24 ),
inference(clausify,[status(thm)],[clause48]) ).
fof(clause49,axiom,
( c0_1(a798)
| ~ hskp23 ),
file('theBenchmark.p',clause49) ).
cnf(c_49,plain,
( c0_1(a798)
| ~ hskp23 ),
inference(clausify,[status(thm)],[clause49]) ).
fof(clause50,axiom,
( c1_1(a798)
| ~ hskp23 ),
file('theBenchmark.p',clause50) ).
cnf(c_50,plain,
( c1_1(a798)
| ~ hskp23 ),
inference(clausify,[status(thm)],[clause50]) ).
fof(clause52,axiom,
( c0_1(a793)
| ~ hskp21 ),
file('theBenchmark.p',clause52) ).
cnf(c_52,plain,
( c0_1(a793)
| ~ hskp21 ),
inference(clausify,[status(thm)],[clause52]) ).
fof(clause53,axiom,
( c3_1(a793)
| ~ hskp21 ),
file('theBenchmark.p',clause53) ).
cnf(c_53,plain,
( c3_1(a793)
| ~ hskp21 ),
inference(clausify,[status(thm)],[clause53]) ).
fof(clause54,axiom,
( c2_1(a779)
| ~ hskp20 ),
file('theBenchmark.p',clause54) ).
cnf(c_54,plain,
( c2_1(a779)
| ~ hskp20 ),
inference(clausify,[status(thm)],[clause54]) ).
fof(clause55,axiom,
( c2_1(a777)
| ~ hskp19 ),
file('theBenchmark.p',clause55) ).
cnf(c_55,plain,
( c2_1(a777)
| ~ hskp19 ),
inference(clausify,[status(thm)],[clause55]) ).
fof(clause59,axiom,
( c0_1(a764)
| ~ hskp16 ),
file('theBenchmark.p',clause59) ).
cnf(c_59,plain,
( c0_1(a764)
| ~ hskp16 ),
inference(clausify,[status(thm)],[clause59]) ).
fof(clause60,axiom,
( c2_1(a764)
| ~ hskp16 ),
file('theBenchmark.p',clause60) ).
cnf(c_60,plain,
( c2_1(a764)
| ~ hskp16 ),
inference(clausify,[status(thm)],[clause60]) ).
fof(clause61,axiom,
( c0_1(a763)
| ~ hskp15 ),
file('theBenchmark.p',clause61) ).
cnf(c_61,plain,
( c0_1(a763)
| ~ hskp15 ),
inference(clausify,[status(thm)],[clause61]) ).
fof(clause62,axiom,
( c1_1(a763)
| ~ hskp15 ),
file('theBenchmark.p',clause62) ).
cnf(c_62,plain,
( c1_1(a763)
| ~ hskp15 ),
inference(clausify,[status(thm)],[clause62]) ).
fof(clause64,axiom,
( c2_1(a759)
| ~ hskp13 ),
file('theBenchmark.p',clause64) ).
cnf(c_64,plain,
( c2_1(a759)
| ~ hskp13 ),
inference(clausify,[status(thm)],[clause64]) ).
fof(clause65,axiom,
( c3_1(a759)
| ~ hskp13 ),
file('theBenchmark.p',clause65) ).
cnf(c_65,plain,
( c3_1(a759)
| ~ hskp13 ),
inference(clausify,[status(thm)],[clause65]) ).
fof(clause68,axiom,
( c3_1(a746)
| ~ hskp9 ),
file('theBenchmark.p',clause68) ).
cnf(c_68,plain,
( c3_1(a746)
| ~ hskp9 ),
inference(clausify,[status(thm)],[clause68]) ).
fof(clause69,axiom,
( c3_1(a744)
| ~ hskp8 ),
file('theBenchmark.p',clause69) ).
cnf(c_69,plain,
( c3_1(a744)
| ~ hskp8 ),
inference(clausify,[status(thm)],[clause69]) ).
fof(clause70,axiom,
( c1_1(a741)
| ~ hskp7 ),
file('theBenchmark.p',clause70) ).
cnf(c_70,plain,
( c1_1(a741)
| ~ hskp7 ),
inference(clausify,[status(thm)],[clause70]) ).
fof(clause71,axiom,
( c3_1(a741)
| ~ hskp7 ),
file('theBenchmark.p',clause71) ).
cnf(c_71,plain,
( c3_1(a741)
| ~ hskp7 ),
inference(clausify,[status(thm)],[clause71]) ).
fof(clause72,axiom,
( c1_1(a738)
| ~ hskp6 ),
file('theBenchmark.p',clause72) ).
cnf(c_72,plain,
( c1_1(a738)
| ~ hskp6 ),
inference(clausify,[status(thm)],[clause72]) ).
fof(clause73,axiom,
( c2_1(a735)
| ~ hskp5 ),
file('theBenchmark.p',clause73) ).
cnf(c_73,plain,
( c2_1(a735)
| ~ hskp5 ),
inference(clausify,[status(thm)],[clause73]) ).
fof(clause74,axiom,
( c3_1(a735)
| ~ hskp5 ),
file('theBenchmark.p',clause74) ).
cnf(c_74,plain,
( c3_1(a735)
| ~ hskp5 ),
inference(clausify,[status(thm)],[clause74]) ).
fof(clause75,axiom,
( c1_1(a734)
| ~ hskp4 ),
file('theBenchmark.p',clause75) ).
cnf(c_75,plain,
( c1_1(a734)
| ~ hskp4 ),
inference(clausify,[status(thm)],[clause75]) ).
fof(clause77,axiom,
( c1_1(a731)
| ~ hskp1 ),
file('theBenchmark.p',clause77) ).
cnf(c_77,plain,
( c1_1(a731)
| ~ hskp1 ),
inference(clausify,[status(thm)],[clause77]) ).
fof(clause78,axiom,
( c3_1(a731)
| ~ hskp1 ),
file('theBenchmark.p',clause78) ).
cnf(c_78,plain,
( c3_1(a731)
| ~ hskp1 ),
inference(clausify,[status(thm)],[clause78]) ).
fof(clause79,axiom,
( c0_1(a730)
| ~ hskp0 ),
file('theBenchmark.p',clause79) ).
cnf(c_79,plain,
( c0_1(a730)
| ~ hskp0 ),
inference(clausify,[status(thm)],[clause79]) ).
fof(clause80,axiom,
( c3_1(a730)
| ~ hskp0 ),
file('theBenchmark.p',clause80) ).
cnf(c_80,plain,
( c3_1(a730)
| ~ hskp0 ),
inference(clausify,[status(thm)],[clause80]) ).
fof(clause81,axiom,
( ~ hskp24
| ~ c2_1(a802) ),
file('theBenchmark.p',clause81) ).
cnf(c_81,plain,
( ~ hskp24
| ~ c2_1(a802) ),
inference(clausify,[status(thm)],[clause81]) ).
fof(clause82,axiom,
( ~ hskp24
| ~ c3_1(a802) ),
file('theBenchmark.p',clause82) ).
cnf(c_82,plain,
( ~ hskp24
| ~ c3_1(a802) ),
inference(clausify,[status(thm)],[clause82]) ).
fof(clause83,axiom,
( ~ hskp23
| ~ c3_1(a798) ),
file('theBenchmark.p',clause83) ).
cnf(c_83,plain,
( ~ hskp23
| ~ c3_1(a798) ),
inference(clausify,[status(thm)],[clause83]) ).
fof(clause86,axiom,
( ~ hskp21
| ~ c2_1(a793) ),
file('theBenchmark.p',clause86) ).
cnf(c_86,plain,
( ~ hskp21
| ~ c2_1(a793) ),
inference(clausify,[status(thm)],[clause86]) ).
fof(clause87,axiom,
( ~ hskp20
| ~ c1_1(a779) ),
file('theBenchmark.p',clause87) ).
cnf(c_87,plain,
( ~ hskp20
| ~ c1_1(a779) ),
inference(clausify,[status(thm)],[clause87]) ).
fof(clause88,axiom,
( ~ hskp20
| ~ c3_1(a779) ),
file('theBenchmark.p',clause88) ).
cnf(c_88,plain,
( ~ hskp20
| ~ c3_1(a779) ),
inference(clausify,[status(thm)],[clause88]) ).
fof(clause89,axiom,
( ~ hskp19
| ~ c0_1(a777) ),
file('theBenchmark.p',clause89) ).
cnf(c_89,plain,
( ~ hskp19
| ~ c0_1(a777) ),
inference(clausify,[status(thm)],[clause89]) ).
fof(clause90,axiom,
( ~ hskp19
| ~ c3_1(a777) ),
file('theBenchmark.p',clause90) ).
cnf(c_90,plain,
( ~ hskp19
| ~ c3_1(a777) ),
inference(clausify,[status(thm)],[clause90]) ).
fof(clause91,axiom,
( ~ hskp18
| ~ c2_1(a775) ),
file('theBenchmark.p',clause91) ).
cnf(c_91,plain,
( ~ hskp18
| ~ c2_1(a775) ),
inference(clausify,[status(thm)],[clause91]) ).
fof(clause92,axiom,
( ~ hskp18
| ~ c3_1(a775) ),
file('theBenchmark.p',clause92) ).
cnf(c_92,plain,
( ~ hskp18
| ~ c3_1(a775) ),
inference(clausify,[status(thm)],[clause92]) ).
fof(clause94,axiom,
( ~ hskp16
| ~ c3_1(a764) ),
file('theBenchmark.p',clause94) ).
cnf(c_94,plain,
( ~ hskp16
| ~ c3_1(a764) ),
inference(clausify,[status(thm)],[clause94]) ).
fof(clause95,axiom,
( ~ hskp15
| ~ c2_1(a763) ),
file('theBenchmark.p',clause95) ).
cnf(c_95,plain,
( ~ hskp15
| ~ c2_1(a763) ),
inference(clausify,[status(thm)],[clause95]) ).
fof(clause98,axiom,
( ~ hskp13
| ~ c1_1(a759) ),
file('theBenchmark.p',clause98) ).
cnf(c_98,plain,
( ~ hskp13
| ~ c1_1(a759) ),
inference(clausify,[status(thm)],[clause98]) ).
fof(clause100,axiom,
( ~ hskp11
| ~ c0_1(a749) ),
file('theBenchmark.p',clause100) ).
cnf(c_100,plain,
( ~ hskp11
| ~ c0_1(a749) ),
inference(clausify,[status(thm)],[clause100]) ).
fof(clause101,axiom,
( ~ hskp11
| ~ c1_1(a749) ),
file('theBenchmark.p',clause101) ).
cnf(c_101,plain,
( ~ hskp11
| ~ c1_1(a749) ),
inference(clausify,[status(thm)],[clause101]) ).
fof(clause102,axiom,
( ~ hskp11
| ~ c3_1(a749) ),
file('theBenchmark.p',clause102) ).
cnf(c_102,plain,
( ~ hskp11
| ~ c3_1(a749) ),
inference(clausify,[status(thm)],[clause102]) ).
fof(clause103,axiom,
( ~ hskp10
| ~ c0_1(a748) ),
file('theBenchmark.p',clause103) ).
cnf(c_103,plain,
( ~ hskp10
| ~ c0_1(a748) ),
inference(clausify,[status(thm)],[clause103]) ).
fof(clause104,axiom,
( ~ hskp10
| ~ c1_1(a748) ),
file('theBenchmark.p',clause104) ).
cnf(c_104,plain,
( ~ hskp10
| ~ c1_1(a748) ),
inference(clausify,[status(thm)],[clause104]) ).
fof(clause105,axiom,
( ~ hskp10
| ~ c2_1(a748) ),
file('theBenchmark.p',clause105) ).
cnf(c_105,plain,
( ~ hskp10
| ~ c2_1(a748) ),
inference(clausify,[status(thm)],[clause105]) ).
fof(clause106,axiom,
( ~ hskp9
| ~ c0_1(a746) ),
file('theBenchmark.p',clause106) ).
cnf(c_106,plain,
( ~ hskp9
| ~ c0_1(a746) ),
inference(clausify,[status(thm)],[clause106]) ).
fof(clause107,axiom,
( ~ hskp9
| ~ c2_1(a746) ),
file('theBenchmark.p',clause107) ).
cnf(c_107,plain,
( ~ hskp9
| ~ c2_1(a746) ),
inference(clausify,[status(thm)],[clause107]) ).
fof(clause108,axiom,
( ~ hskp8
| ~ c0_1(a744) ),
file('theBenchmark.p',clause108) ).
cnf(c_108,plain,
( ~ hskp8
| ~ c0_1(a744) ),
inference(clausify,[status(thm)],[clause108]) ).
fof(clause109,axiom,
( ~ hskp8
| ~ c1_1(a744) ),
file('theBenchmark.p',clause109) ).
cnf(c_109,plain,
( ~ hskp8
| ~ c1_1(a744) ),
inference(clausify,[status(thm)],[clause109]) ).
fof(clause110,axiom,
( ~ hskp7
| ~ c0_1(a741) ),
file('theBenchmark.p',clause110) ).
cnf(c_110,plain,
( ~ hskp7
| ~ c0_1(a741) ),
inference(clausify,[status(thm)],[clause110]) ).
fof(clause111,axiom,
( ~ hskp6
| ~ c0_1(a738) ),
file('theBenchmark.p',clause111) ).
cnf(c_111,plain,
( ~ hskp6
| ~ c0_1(a738) ),
inference(clausify,[status(thm)],[clause111]) ).
fof(clause112,axiom,
( ~ hskp6
| ~ c2_1(a738) ),
file('theBenchmark.p',clause112) ).
cnf(c_112,plain,
( ~ hskp6
| ~ c2_1(a738) ),
inference(clausify,[status(thm)],[clause112]) ).
fof(clause113,axiom,
( ~ hskp5
| ~ c0_1(a735) ),
file('theBenchmark.p',clause113) ).
cnf(c_113,plain,
( ~ hskp5
| ~ c0_1(a735) ),
inference(clausify,[status(thm)],[clause113]) ).
fof(clause114,axiom,
( ~ hskp4
| ~ c0_1(a734) ),
file('theBenchmark.p',clause114) ).
cnf(c_114,plain,
( ~ hskp4
| ~ c0_1(a734) ),
inference(clausify,[status(thm)],[clause114]) ).
fof(clause115,axiom,
( ~ hskp4
| ~ c3_1(a734) ),
file('theBenchmark.p',clause115) ).
cnf(c_115,plain,
( ~ hskp4
| ~ c3_1(a734) ),
inference(clausify,[status(thm)],[clause115]) ).
fof(clause118,axiom,
( ~ hskp2
| ~ c0_1(a732) ),
file('theBenchmark.p',clause118) ).
cnf(c_118,plain,
( ~ hskp2
| ~ c0_1(a732) ),
inference(clausify,[status(thm)],[clause118]) ).
fof(clause119,axiom,
( ~ hskp2
| ~ c2_1(a732) ),
file('theBenchmark.p',clause119) ).
cnf(c_119,plain,
( ~ hskp2
| ~ c2_1(a732) ),
inference(clausify,[status(thm)],[clause119]) ).
fof(clause120,axiom,
( ~ hskp2
| ~ c3_1(a732) ),
file('theBenchmark.p',clause120) ).
cnf(c_120,plain,
( ~ hskp2
| ~ c3_1(a732) ),
inference(clausify,[status(thm)],[clause120]) ).
fof(clause121,axiom,
( ~ hskp1
| ~ c2_1(a731) ),
file('theBenchmark.p',clause121) ).
cnf(c_121,plain,
( ~ hskp1
| ~ c2_1(a731) ),
inference(clausify,[status(thm)],[clause121]) ).
fof(clause122,axiom,
( ~ hskp0
| ~ c1_1(a730) ),
file('theBenchmark.p',clause122) ).
cnf(c_122,plain,
( ~ hskp0
| ~ c1_1(a730) ),
inference(clausify,[status(thm)],[clause122]) ).
fof(clause123,axiom,
! [VAR_0] :
( hskp1
| hskp0
| c2_1(VAR_0)
| c1_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0 ),
file('theBenchmark.p',clause123) ).
cnf(c_123,plain,
( hskp1
| hskp0
| c2_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[clause123]) ).
fof(clause124,axiom,
! [VAR_0] :
( hskp5
| hskp4
| c3_1(VAR_0)
| c1_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0 ),
file('theBenchmark.p',clause124) ).
cnf(c_124,plain,
( hskp5
| hskp4
| c3_1(A)
| c1_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[clause124]) ).
fof(clause125,axiom,
! [VAR_0] :
( hskp9
| hskp5
| c3_1(VAR_0)
| c2_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0 ),
file('theBenchmark.p',clause125) ).
cnf(c_125,plain,
( hskp9
| hskp5
| c3_1(A)
| c2_1(A)
| c0_1(A)
| ~ ndr1_0 ),
inference(clausify,[status(thm)],[clause125]) ).
fof(clause128,axiom,
! [VAR_0] :
( hskp2
| hskp1
| c1_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause128) ).
cnf(c_128,plain,
( hskp2
| hskp1
| c1_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause128]) ).
fof(clause130,axiom,
! [VAR_0] :
( hskp6
| hskp25
| c2_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0) ),
file('theBenchmark.p',clause130) ).
cnf(c_130,plain,
( hskp6
| hskp25
| c2_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c3_1(A) ),
inference(clausify,[status(thm)],[clause130]) ).
fof(clause133,axiom,
! [VAR_0] :
( hskp9
| hskp0
| c3_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause133) ).
cnf(c_133,plain,
( hskp9
| hskp0
| c3_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause133]) ).
fof(clause135,axiom,
! [VAR_0] :
( hskp9
| hskp25
| c3_1(VAR_0)
| c2_1(VAR_0)
| ~ ndr1_0
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause135) ).
cnf(c_135,plain,
( hskp9
| hskp25
| c3_1(A)
| c2_1(A)
| ~ ndr1_0
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause135]) ).
fof(clause139,axiom,
! [VAR_0] :
( hskp19
| hskp27
| c1_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause139) ).
cnf(c_139,plain,
( hskp19
| hskp27
| c1_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause139]) ).
fof(clause140,axiom,
! [VAR_0] :
( hskp20
| hskp5
| c1_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause140) ).
cnf(c_140,plain,
( hskp20
| hskp5
| c1_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause140]) ).
fof(clause141,axiom,
! [VAR_0] :
( hskp11
| hskp18
| c3_1(VAR_0)
| ~ ndr1_0
| ~ c1_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause141) ).
cnf(c_141,plain,
( hskp11
| hskp18
| c3_1(A)
| ~ ndr1_0
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause141]) ).
fof(clause143,axiom,
! [VAR_0] :
( hskp21
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause143) ).
cnf(c_143,plain,
( hskp21
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause143]) ).
fof(clause144,axiom,
! [VAR_0] :
( hskp11
| hskp28
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause144) ).
cnf(c_144,plain,
( hskp11
| hskp28
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause144]) ).
fof(clause148,axiom,
! [VAR_0,VAR_1] :
( hskp8
| c3_1(VAR_1)
| c2_1(VAR_1)
| c0_1(VAR_1)
| c3_1(VAR_0)
| c0_1(VAR_0)
| ~ ndr1_0
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause148) ).
cnf(c_148,plain,
( hskp8
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause148]) ).
fof(clause149,axiom,
! [VAR_0,VAR_1] :
( hskp25
| c2_1(VAR_1)
| c1_1(VAR_1)
| c0_1(VAR_1)
| c1_1(VAR_0)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause149) ).
cnf(c_149,plain,
( hskp25
| c2_1(B)
| c1_1(B)
| c0_1(B)
| c1_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause149]) ).
fof(clause152,axiom,
! [VAR_0,VAR_1] :
( hskp5
| c2_1(VAR_1)
| c0_1(VAR_1)
| c3_1(VAR_0)
| c0_1(VAR_0)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause152) ).
cnf(c_152,plain,
( hskp5
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c0_1(A)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause152]) ).
fof(clause154,axiom,
! [VAR_0,VAR_1] :
( hskp5
| c1_1(VAR_1)
| c0_1(VAR_1)
| c0_1(VAR_0)
| ~ c3_1(VAR_1)
| ~ ndr1_0
| ~ c2_1(VAR_0)
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause154) ).
cnf(c_154,plain,
( hskp5
| c1_1(B)
| c0_1(B)
| c0_1(A)
| ~ c3_1(B)
| ~ ndr1_0
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause154]) ).
fof(clause156,axiom,
! [VAR_0,VAR_1] :
( hskp10
| c2_1(VAR_1)
| c0_1(VAR_1)
| c0_1(VAR_0)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0) ),
file('theBenchmark.p',clause156) ).
cnf(c_156,plain,
( hskp10
| c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(clausify,[status(thm)],[clause156]) ).
fof(clause158,axiom,
! [VAR_0,VAR_1] :
( hskp13
| c3_1(VAR_1)
| c0_1(VAR_1)
| c2_1(VAR_0)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c1_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause158) ).
cnf(c_158,plain,
( hskp13
| c3_1(B)
| c0_1(B)
| c2_1(A)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause158]) ).
fof(clause159,axiom,
! [VAR_0,VAR_1] :
( hskp2
| c0_1(VAR_1)
| c2_1(VAR_0)
| c1_1(VAR_0)
| ~ c3_1(VAR_1)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause159) ).
cnf(c_159,plain,
( hskp2
| c0_1(B)
| c2_1(A)
| c1_1(A)
| ~ c3_1(B)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause159]) ).
fof(clause160,axiom,
! [VAR_0,VAR_1] :
( hskp11
| c2_1(VAR_1)
| c1_1(VAR_1)
| c2_1(VAR_0)
| ~ c3_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause160) ).
cnf(c_160,plain,
( hskp11
| c2_1(B)
| c1_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause160]) ).
fof(clause161,axiom,
! [VAR_0,VAR_1] :
( hskp5
| c3_1(VAR_1)
| c1_1(VAR_1)
| c1_1(VAR_0)
| ~ c2_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause161) ).
cnf(c_161,plain,
( hskp5
| c3_1(B)
| c1_1(B)
| c1_1(A)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause161]) ).
fof(clause164,axiom,
! [VAR_0,VAR_1] :
( hskp15
| c3_1(VAR_1)
| c0_1(VAR_1)
| ~ c2_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c1_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause164) ).
cnf(c_164,plain,
( hskp15
| c3_1(B)
| c0_1(B)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause164]) ).
fof(clause166,axiom,
! [VAR_0,VAR_1] :
( hskp16
| c0_1(VAR_1)
| ~ c2_1(VAR_1)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause166) ).
cnf(c_166,plain,
( hskp16
| c0_1(B)
| ~ c2_1(B)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause166]) ).
fof(clause167,axiom,
! [VAR_0,VAR_1] :
( hskp1
| c3_1(VAR_1)
| ~ c1_1(VAR_1)
| ~ c0_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause167) ).
cnf(c_167,plain,
( hskp1
| c3_1(B)
| ~ c1_1(B)
| ~ c0_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause167]) ).
fof(clause171,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c3_1(VAR_2)
| c1_1(VAR_2)
| c0_1(VAR_2)
| c2_1(VAR_1)
| ~ c1_1(VAR_1)
| ~ c0_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c1_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause171) ).
cnf(c_171,plain,
( c3_1(C)
| c1_1(C)
| c0_1(C)
| c2_1(B)
| ~ c1_1(B)
| ~ c0_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause171]) ).
fof(clause172,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c2_1(VAR_2)
| c0_1(VAR_2)
| c0_1(VAR_1)
| c2_1(VAR_0)
| ~ c3_1(VAR_2)
| ~ c3_1(VAR_1)
| ~ c1_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause172) ).
cnf(c_172,plain,
( c2_1(C)
| c0_1(C)
| c0_1(B)
| c2_1(A)
| ~ c3_1(C)
| ~ c3_1(B)
| ~ c1_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause172]) ).
fof(clause173,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c3_1(VAR_2)
| c1_1(VAR_2)
| c3_1(VAR_1)
| c2_1(VAR_1)
| ~ c2_1(VAR_2)
| ~ c0_1(VAR_1)
| ~ ndr1_0
| ~ c2_1(VAR_0)
| ~ c1_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause173) ).
cnf(c_173,plain,
( c3_1(C)
| c1_1(C)
| c3_1(B)
| c2_1(B)
| ~ c2_1(C)
| ~ c0_1(B)
| ~ ndr1_0
| ~ c2_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause173]) ).
fof(clause174,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c2_1(VAR_2)
| c0_1(VAR_2)
| c0_1(VAR_1)
| ~ c3_1(VAR_2)
| ~ c3_1(VAR_1)
| ~ c2_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c2_1(VAR_0)
| ~ c1_1(VAR_0) ),
file('theBenchmark.p',clause174) ).
cnf(c_174,plain,
( c2_1(C)
| c0_1(C)
| c0_1(B)
| ~ c3_1(C)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(clausify,[status(thm)],[clause174]) ).
fof(clause175,axiom,
! [VAR_0,VAR_1,VAR_2] :
( c0_1(VAR_2)
| c1_1(VAR_1)
| c2_1(VAR_0)
| ~ c3_1(VAR_2)
| ~ c2_1(VAR_2)
| ~ c3_1(VAR_1)
| ~ c2_1(VAR_1)
| ~ ndr1_0
| ~ c3_1(VAR_0)
| ~ c0_1(VAR_0) ),
file('theBenchmark.p',clause175) ).
cnf(c_175,plain,
( c0_1(C)
| c1_1(B)
| c2_1(A)
| ~ c3_1(C)
| ~ c2_1(C)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(clausify,[status(thm)],[clause175]) ).
cnf(c_30582,plain,
( hskp5
| c2_1(A)
| c0_1(A)
| c3_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c1_1(A) ),
inference(factor,[status(thm)],[c_152]) ).
cnf(c_176,plain,
( hskp5
| c2_1(A)
| c3_1(A)
| c0_1(A)
| ~ ndr1_0
| ~ c1_1(A) ),
inference(copy,[status(thm)],[c_30582]) ).
cnf(c_30583,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c1_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(factor,[status(thm)],[c_171]) ).
cnf(c_178,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(copy,[status(thm)],[c_30583]) ).
cnf(c_30584,plain,
( c2_1(B)
| c0_1(B)
| c0_1(A)
| c2_1(A)
| ~ c3_1(B)
| ~ c3_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(factor,[status(thm)],[c_172]) ).
cnf(c_179,plain,
( c2_1(B)
| c0_1(B)
| c0_1(A)
| c2_1(A)
| ~ c3_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(copy,[status(thm)],[c_30584]) ).
cnf(c_30585,plain,
( c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ c3_1(B)
| ~ c3_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(factor,[status(thm)],[c_174]) ).
cnf(c_182,plain,
( c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ c3_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(copy,[status(thm)],[c_30585]) ).
cnf(c_30586,plain,
( c0_1(B)
| c1_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(factor,[status(thm)],[c_175]) ).
cnf(c_183,plain,
( c0_1(B)
| c1_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(copy,[status(thm)],[c_30586]) ).
cnf(c_30587,plain,
( c2_1(A)
| c0_1(A)
| c0_1(A)
| c2_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(factor,[status(thm)],[c_179]) ).
cnf(c_30588,plain,
( c2_1(A)
| c0_1(A)
| c2_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(copy,[status(thm)],[c_30587]) ).
cnf(c_184,plain,
( c0_1(A)
| c2_1(A)
| ~ ndr1_0
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(copy,[status(thm)],[c_30588]) ).
cnf(c_185,plain,
( hskp0
| ndr1_0 ),
inference(resolve,[status(thm)],[c_22,c_1]) ).
cnf(c_190,plain,
( hskp13
| hskp23
| c0_1(a802) ),
inference(resolve,[status(thm)],[c_48,c_32]) ).
cnf(c_195,plain,
( hskp0
| c3_1(a744) ),
inference(resolve,[status(thm)],[c_69,c_1]) ).
cnf(c_196,plain,
( hskp4
| hskp1
| c1_1(a741) ),
inference(resolve,[status(thm)],[c_70,c_35]) ).
cnf(c_197,plain,
( hskp4
| hskp1
| c3_1(a741) ),
inference(resolve,[status(thm)],[c_71,c_35]) ).
cnf(c_30589,plain,
( ndr1_0
| ndr1_0 ),
inference(resolve,[status(thm)],[c_185,c_30]) ).
cnf(c_200,plain,
ndr1_0,
inference(copy,[status(thm)],[c_30589]) ).
cnf(c_201,plain,
( c0_1(A)
| c2_1(A)
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_200,c_184]) ).
cnf(c_202,plain,
( c0_1(B)
| c1_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_183]) ).
cnf(c_203,plain,
( c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ c3_1(B)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_200,c_182]) ).
cnf(c_204,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_178]) ).
cnf(c_205,plain,
( hskp5
| c2_1(A)
| c3_1(A)
| c0_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_200,c_176]) ).
cnf(c_206,plain,
( c0_1(C)
| c1_1(B)
| c2_1(A)
| ~ c3_1(C)
| ~ c2_1(C)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_175]) ).
cnf(c_208,plain,
( c3_1(C)
| c1_1(C)
| c3_1(B)
| c2_1(B)
| ~ c2_1(C)
| ~ c0_1(B)
| ~ c2_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_173]) ).
cnf(c_210,plain,
( c3_1(C)
| c1_1(C)
| c0_1(C)
| c2_1(B)
| ~ c1_1(B)
| ~ c0_1(B)
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_171]) ).
cnf(c_214,plain,
( hskp1
| c3_1(B)
| ~ c1_1(B)
| ~ c0_1(B)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_167]) ).
cnf(c_215,plain,
( hskp16
| c0_1(B)
| ~ c2_1(B)
| ~ c1_1(B)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_166]) ).
cnf(c_217,plain,
( hskp15
| c3_1(B)
| c0_1(B)
| ~ c2_1(B)
| ~ c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_164]) ).
cnf(c_220,plain,
( hskp5
| c3_1(B)
| c1_1(B)
| c1_1(A)
| ~ c2_1(B)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_161]) ).
cnf(c_221,plain,
( hskp11
| c2_1(B)
| c1_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ c3_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_200,c_160]) ).
cnf(c_222,plain,
( hskp2
| c0_1(B)
| c2_1(A)
| c1_1(A)
| ~ c3_1(B)
| ~ c1_1(B)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_159]) ).
cnf(c_223,plain,
( hskp13
| c3_1(B)
| c0_1(B)
| c2_1(A)
| ~ c1_1(B)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_158]) ).
cnf(c_225,plain,
( hskp10
| c2_1(B)
| c0_1(B)
| c0_1(A)
| ~ c1_1(B)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_200,c_156]) ).
cnf(c_227,plain,
( hskp5
| c1_1(B)
| c0_1(B)
| c0_1(A)
| ~ c3_1(B)
| ~ c2_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_200,c_154]) ).
cnf(c_229,plain,
( hskp5
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c0_1(A)
| ~ c1_1(B)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_200,c_152]) ).
cnf(c_232,plain,
( hskp25
| c2_1(B)
| c1_1(B)
| c0_1(B)
| c1_1(A)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_149]) ).
cnf(c_233,plain,
( hskp8
| c3_1(B)
| c2_1(B)
| c0_1(B)
| c3_1(A)
| c0_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_200,c_148]) ).
cnf(c_237,plain,
( hskp11
| hskp28
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_144]) ).
cnf(c_238,plain,
( hskp21
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_143]) ).
cnf(c_240,plain,
( hskp11
| hskp18
| c3_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_141]) ).
cnf(c_241,plain,
( hskp20
| hskp5
| c1_1(A)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_200,c_140]) ).
cnf(c_242,plain,
( hskp19
| hskp27
| c1_1(A)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_139]) ).
cnf(c_246,plain,
( hskp9
| hskp25
| c3_1(A)
| c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_135]) ).
cnf(c_248,plain,
( hskp9
| hskp0
| c3_1(A)
| c0_1(A)
| ~ c1_1(A) ),
inference(resolve,[status(thm)],[c_200,c_133]) ).
cnf(c_251,plain,
( hskp6
| hskp25
| c2_1(A)
| c0_1(A)
| ~ c3_1(A) ),
inference(resolve,[status(thm)],[c_200,c_130]) ).
cnf(c_253,plain,
( hskp2
| hskp1
| c1_1(A)
| c0_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_200,c_128]) ).
cnf(c_256,plain,
( hskp9
| hskp5
| c3_1(A)
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_125]) ).
cnf(c_257,plain,
( hskp5
| hskp4
| c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_124]) ).
cnf(c_258,plain,
( hskp1
| hskp0
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_200,c_123]) ).
cnf(c_259,plain,
( hskp4
| hskp1
| c0_1(a741)
| c2_1(a741)
| ~ c3_1(a741) ),
inference(resolve,[status(thm)],[c_201,c_196]) ).
cnf(c_266,plain,
( hskp0
| c0_1(a744)
| c1_1(a744)
| c2_1(A)
| ~ c2_1(a744)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_202,c_195]) ).
cnf(c_271,plain,
( hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c3_1(A)
| ~ c3_1(a741)
| ~ c2_1(a741) ),
inference(resolve,[status(thm)],[c_203,c_196]) ).
cnf(c_281,plain,
( hskp13
| hskp23
| hskp9
| hskp25
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_246,c_190]) ).
cnf(c_328,plain,
( ~ hskp2
| hskp9
| hskp5
| c2_1(a732)
| c0_1(a732) ),
inference(resolve,[status(thm)],[c_256,c_120]) ).
cnf(c_330,plain,
( ~ hskp11
| hskp9
| hskp5
| c2_1(a749)
| c0_1(a749) ),
inference(resolve,[status(thm)],[c_256,c_102]) ).
cnf(c_331,plain,
( ~ hskp18
| hskp9
| hskp5
| c2_1(a775)
| c0_1(a775) ),
inference(resolve,[status(thm)],[c_256,c_92]) ).
cnf(c_30590,plain,
( hskp5
| c2_1(A)
| c3_1(A)
| c0_1(A)
| hskp5
| hskp4
| c3_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_257,c_205]) ).
cnf(c_30591,plain,
( hskp5
| c2_1(A)
| c3_1(A)
| hskp5
| hskp4
| c3_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30590]) ).
cnf(c_30592,plain,
( hskp5
| c2_1(A)
| hskp5
| hskp4
| c3_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30591]) ).
cnf(c_341,plain,
( c2_1(A)
| hskp5
| hskp4
| c3_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30592]) ).
cnf(c_344,plain,
( ~ hskp11
| hskp5
| hskp4
| c3_1(a749)
| c0_1(a749) ),
inference(resolve,[status(thm)],[c_257,c_101]) ).
cnf(c_30593,plain,
( hskp9
| hskp0
| c3_1(A)
| c0_1(A)
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_258,c_248]) ).
cnf(c_30594,plain,
( hskp9
| hskp0
| c3_1(A)
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30593]) ).
cnf(c_349,plain,
( hskp9
| c3_1(A)
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30594]) ).
cnf(c_30595,plain,
( c0_1(A)
| c2_1(A)
| ~ c3_1(A)
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_258,c_201]) ).
cnf(c_30596,plain,
( c0_1(A)
| ~ c3_1(A)
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30595]) ).
cnf(c_354,plain,
( ~ c3_1(A)
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30596]) ).
cnf(c_355,plain,
( ~ hskp8
| hskp1
| hskp0
| c2_1(a744)
| c0_1(a744) ),
inference(resolve,[status(thm)],[c_258,c_109]) ).
cnf(c_30597,plain,
( hskp0
| hskp1
| hskp0
| c2_1(a744)
| c0_1(a744) ),
inference(resolve,[status(thm)],[c_355,c_1]) ).
cnf(c_362,plain,
( hskp1
| hskp0
| c2_1(a744)
| c0_1(a744) ),
inference(copy,[status(thm)],[c_30597]) ).
cnf(c_30598,plain,
( hskp2
| hskp1
| c1_1(a744)
| c0_1(a744)
| hskp1
| hskp0
| c0_1(a744) ),
inference(resolve,[status(thm)],[c_362,c_253]) ).
cnf(c_30599,plain,
( hskp2
| hskp1
| c1_1(a744)
| hskp1
| hskp0
| c0_1(a744) ),
inference(copy,[status(thm)],[c_30598]) ).
cnf(c_365,plain,
( hskp2
| c1_1(a744)
| hskp1
| hskp0
| c0_1(a744) ),
inference(copy,[status(thm)],[c_30599]) ).
cnf(c_370,plain,
( ~ hskp8
| hskp2
| hskp1
| hskp0
| c0_1(a744) ),
inference(resolve,[status(thm)],[c_365,c_109]) ).
cnf(c_30600,plain,
( hskp0
| hskp2
| hskp1
| hskp0
| c0_1(a744) ),
inference(resolve,[status(thm)],[c_370,c_1]) ).
cnf(c_371,plain,
( hskp2
| hskp1
| hskp0
| c0_1(a744) ),
inference(copy,[status(thm)],[c_30600]) ).
cnf(c_373,plain,
( ~ hskp8
| hskp2
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_371,c_108]) ).
cnf(c_30601,plain,
( hskp0
| hskp2
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_373,c_1]) ).
cnf(c_375,plain,
( hskp2
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30601]) ).
cnf(c_30602,plain,
( hskp4
| hskp1
| hskp4
| hskp1
| c0_1(a741)
| c2_1(a741) ),
inference(resolve,[status(thm)],[c_259,c_197]) ).
cnf(c_30603,plain,
( hskp4
| hskp4
| hskp1
| c0_1(a741)
| c2_1(a741) ),
inference(copy,[status(thm)],[c_30602]) ).
cnf(c_378,plain,
( hskp4
| hskp1
| c0_1(a741)
| c2_1(a741) ),
inference(copy,[status(thm)],[c_30603]) ).
cnf(c_465,plain,
( hskp4
| hskp1
| hskp2
| c0_1(a741)
| c2_1(A)
| c1_1(A)
| ~ c3_1(a741)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_222,c_196]) ).
cnf(c_493,plain,
( ~ hskp24
| hskp13
| hskp23
| hskp9
| hskp25
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_281,c_82]) ).
cnf(c_30604,plain,
( hskp13
| hskp23
| hskp13
| hskp23
| hskp9
| hskp25
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_493,c_32]) ).
cnf(c_30605,plain,
( hskp13
| hskp13
| hskp23
| hskp9
| hskp25
| c2_1(a802) ),
inference(copy,[status(thm)],[c_30604]) ).
cnf(c_494,plain,
( hskp13
| hskp23
| hskp9
| hskp25
| c2_1(a802) ),
inference(copy,[status(thm)],[c_30605]) ).
cnf(c_495,plain,
( ~ hskp24
| hskp13
| hskp23
| hskp9
| hskp25 ),
inference(resolve,[status(thm)],[c_494,c_81]) ).
cnf(c_30606,plain,
( hskp13
| hskp23
| hskp13
| hskp23
| hskp9
| hskp25 ),
inference(resolve,[status(thm)],[c_495,c_32]) ).
cnf(c_30607,plain,
( hskp13
| hskp13
| hskp23
| hskp9
| hskp25 ),
inference(copy,[status(thm)],[c_30606]) ).
cnf(c_496,plain,
( hskp13
| hskp23
| hskp9
| hskp25 ),
inference(copy,[status(thm)],[c_30607]) ).
cnf(c_499,plain,
( c3_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_496,c_68]) ).
cnf(c_30608,plain,
( hskp6
| hskp25
| c2_1(a746)
| c0_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_499,c_251]) ).
cnf(c_501,plain,
( hskp6
| c2_1(a746)
| c0_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30608]) ).
cnf(c_30609,plain,
( hskp4
| hskp1
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c3_1(A)
| ~ c2_1(a741) ),
inference(resolve,[status(thm)],[c_271,c_197]) ).
cnf(c_30610,plain,
( hskp4
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c3_1(A)
| ~ c2_1(a741) ),
inference(copy,[status(thm)],[c_30609]) ).
cnf(c_781,plain,
( hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c3_1(A)
| ~ c2_1(a741) ),
inference(copy,[status(thm)],[c_30610]) ).
cnf(c_1100,plain,
( ~ hskp9
| hskp6
| c0_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_501,c_107]) ).
cnf(c_30611,plain,
( hskp13
| hskp23
| hskp25
| hskp6
| c0_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_1100,c_496]) ).
cnf(c_30612,plain,
( hskp13
| hskp23
| hskp6
| c0_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30611]) ).
cnf(c_30613,plain,
( hskp13
| hskp6
| c0_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30612]) ).
cnf(c_1107,plain,
( hskp6
| c0_1(a746)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30613]) ).
cnf(c_1108,plain,
( ~ hskp9
| hskp6
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_1107,c_106]) ).
cnf(c_30614,plain,
( hskp13
| hskp23
| hskp25
| hskp6
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_1108,c_496]) ).
cnf(c_30615,plain,
( hskp13
| hskp23
| hskp6
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30614]) ).
cnf(c_30616,plain,
( hskp13
| hskp6
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30615]) ).
cnf(c_1109,plain,
( hskp6
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30616]) ).
cnf(c_1110,plain,
( c1_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_1109,c_72]) ).
cnf(c_1157,plain,
( hskp5
| c2_1(a738)
| c3_1(a738)
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_1110,c_205]) ).
cnf(c_1160,plain,
( c0_1(a738)
| c2_1(a738)
| ~ c3_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_1110,c_201]) ).
cnf(c_30617,plain,
( hskp1
| hskp0
| c2_1(A)
| c0_1(A)
| hskp9
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_349,c_354]) ).
cnf(c_30618,plain,
( hskp1
| hskp0
| c2_1(A)
| hskp9
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30617]) ).
cnf(c_30619,plain,
( hskp1
| hskp0
| hskp9
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30618]) ).
cnf(c_30620,plain,
( hskp1
| hskp9
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30619]) ).
cnf(c_1429,plain,
( hskp9
| hskp1
| hskp0
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30620]) ).
cnf(c_1458,plain,
( ~ hskp2
| hskp9
| hskp1
| hskp0
| c0_1(a732) ),
inference(resolve,[status(thm)],[c_1429,c_119]) ).
cnf(c_30621,plain,
( hskp1
| hskp0
| hskp9
| hskp1
| hskp0
| c0_1(a732) ),
inference(resolve,[status(thm)],[c_1458,c_375]) ).
cnf(c_30622,plain,
( hskp1
| hskp9
| hskp1
| hskp0
| c0_1(a732) ),
inference(copy,[status(thm)],[c_30621]) ).
cnf(c_1463,plain,
( hskp9
| hskp1
| hskp0
| c0_1(a732) ),
inference(copy,[status(thm)],[c_30622]) ).
cnf(c_1469,plain,
( ~ hskp2
| hskp9
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1463,c_118]) ).
cnf(c_30623,plain,
( hskp1
| hskp0
| hskp9
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1469,c_375]) ).
cnf(c_30624,plain,
( hskp1
| hskp9
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30623]) ).
cnf(c_1470,plain,
( hskp9
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30624]) ).
cnf(c_1471,plain,
( c3_1(a746)
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1470,c_68]) ).
cnf(c_30625,plain,
( hskp1
| hskp0
| c2_1(a746)
| c0_1(a746)
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1471,c_354]) ).
cnf(c_30626,plain,
( hskp1
| c2_1(a746)
| c0_1(a746)
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30625]) ).
cnf(c_1472,plain,
( c2_1(a746)
| c0_1(a746)
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30626]) ).
cnf(c_1499,plain,
( ~ hskp9
| c0_1(a746)
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1472,c_107]) ).
cnf(c_30627,plain,
( hskp1
| hskp0
| c0_1(a746)
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1499,c_1470]) ).
cnf(c_30628,plain,
( hskp1
| c0_1(a746)
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30627]) ).
cnf(c_1500,plain,
( c0_1(a746)
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30628]) ).
cnf(c_1501,plain,
( ~ hskp9
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1500,c_106]) ).
cnf(c_30629,plain,
( hskp1
| hskp0
| hskp1
| hskp0 ),
inference(resolve,[status(thm)],[c_1501,c_1470]) ).
cnf(c_30630,plain,
( hskp1
| hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30629]) ).
cnf(c_1502,plain,
( hskp1
| hskp0 ),
inference(copy,[status(thm)],[c_30630]) ).
cnf(c_1510,plain,
( c3_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1502,c_78]) ).
cnf(c_1511,plain,
( c1_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1502,c_77]) ).
cnf(c_30631,plain,
( hskp0
| c0_1(a744)
| c1_1(a744)
| c2_1(a731)
| ~ c2_1(a744)
| ~ c0_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1510,c_266]) ).
cnf(c_1520,plain,
( c0_1(a744)
| c1_1(a744)
| c2_1(a731)
| ~ c2_1(a744)
| ~ c0_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30631]) ).
cnf(c_1546,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| c2_1(a731)
| ~ c3_1(A)
| ~ c3_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1511,c_221]) ).
cnf(c_1561,plain,
( c3_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a731)
| ~ c3_1(a731)
| ~ c0_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1511,c_204]) ).
cnf(c_1563,plain,
( c0_1(a731)
| c2_1(a731)
| ~ c3_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1511,c_201]) ).
cnf(c_30632,plain,
( hskp0
| c0_1(a731)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1563,c_1510]) ).
cnf(c_1601,plain,
( c0_1(a731)
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30632]) ).
cnf(c_1608,plain,
( ~ hskp1
| c0_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1601,c_121]) ).
cnf(c_30633,plain,
( hskp0
| c0_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1608,c_1502]) ).
cnf(c_1609,plain,
( c0_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30633]) ).
cnf(c_30634,plain,
( hskp4
| hskp1
| hskp4
| hskp1
| hskp2
| c0_1(a741)
| c2_1(A)
| c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_465,c_197]) ).
cnf(c_30635,plain,
( hskp4
| hskp4
| hskp1
| hskp2
| c0_1(a741)
| c2_1(A)
| c1_1(A)
| ~ c0_1(A) ),
inference(copy,[status(thm)],[c_30634]) ).
cnf(c_2397,plain,
( hskp4
| hskp1
| hskp2
| c0_1(a741)
| c2_1(A)
| c1_1(A)
| ~ c0_1(A) ),
inference(copy,[status(thm)],[c_30635]) ).
cnf(c_30636,plain,
( c0_1(a738)
| c2_1(a738)
| hskp13
| hskp23
| hskp25
| hskp5
| c2_1(a738)
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_1157,c_1160]) ).
cnf(c_30637,plain,
( c0_1(a738)
| c2_1(a738)
| hskp13
| hskp23
| hskp5
| c2_1(a738)
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30636]) ).
cnf(c_30638,plain,
( c0_1(a738)
| c2_1(a738)
| hskp13
| hskp5
| c2_1(a738)
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30637]) ).
cnf(c_30639,plain,
( c0_1(a738)
| c2_1(a738)
| hskp5
| c2_1(a738)
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30638]) ).
cnf(c_30640,plain,
( c0_1(a738)
| hskp5
| c2_1(a738)
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30639]) ).
cnf(c_5328,plain,
( hskp5
| c2_1(a738)
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30640]) ).
cnf(c_5335,plain,
( ~ hskp6
| hskp5
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_5328,c_112]) ).
cnf(c_30641,plain,
( hskp13
| hskp23
| hskp25
| hskp5
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_5335,c_1109]) ).
cnf(c_30642,plain,
( hskp13
| hskp23
| hskp5
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30641]) ).
cnf(c_30643,plain,
( hskp13
| hskp5
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30642]) ).
cnf(c_5337,plain,
( hskp5
| c0_1(a738)
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30643]) ).
cnf(c_5339,plain,
( ~ hskp6
| hskp5
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_5337,c_111]) ).
cnf(c_30644,plain,
( hskp13
| hskp23
| hskp25
| hskp5
| hskp13
| hskp23
| hskp25 ),
inference(resolve,[status(thm)],[c_5339,c_1109]) ).
cnf(c_30645,plain,
( hskp13
| hskp23
| hskp5
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30644]) ).
cnf(c_30646,plain,
( hskp13
| hskp5
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30645]) ).
cnf(c_5357,plain,
( hskp5
| hskp13
| hskp23
| hskp25 ),
inference(copy,[status(thm)],[c_30646]) ).
cnf(c_5358,plain,
( c1_1(a798)
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5357,c_50]) ).
cnf(c_5359,plain,
( c0_1(a798)
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5357,c_49]) ).
cnf(c_5363,plain,
( hskp11
| hskp18
| c3_1(a798)
| ~ c0_1(a798)
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5358,c_240]) ).
cnf(c_30647,plain,
( hskp5
| hskp13
| hskp25
| hskp11
| hskp18
| c3_1(a798)
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5363,c_5359]) ).
cnf(c_30648,plain,
( hskp5
| hskp13
| hskp11
| hskp18
| c3_1(a798)
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30647]) ).
cnf(c_30649,plain,
( hskp5
| hskp11
| hskp18
| c3_1(a798)
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30648]) ).
cnf(c_5406,plain,
( hskp11
| hskp18
| c3_1(a798)
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30649]) ).
cnf(c_5443,plain,
( ~ hskp23
| hskp11
| hskp18
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5406,c_83]) ).
cnf(c_30650,plain,
( hskp5
| hskp13
| hskp25
| hskp11
| hskp18
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5443,c_5357]) ).
cnf(c_30651,plain,
( hskp5
| hskp13
| hskp11
| hskp18
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30650]) ).
cnf(c_30652,plain,
( hskp5
| hskp11
| hskp18
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30651]) ).
cnf(c_5444,plain,
( hskp11
| hskp18
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30652]) ).
cnf(c_30653,plain,
( hskp9
| hskp5
| c2_1(a775)
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5444,c_331]) ).
cnf(c_5450,plain,
( hskp9
| c2_1(a775)
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30653]) ).
cnf(c_5564,plain,
( ~ hskp18
| hskp9
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5450,c_91]) ).
cnf(c_30654,plain,
( hskp11
| hskp5
| hskp13
| hskp25
| hskp9
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5564,c_5444]) ).
cnf(c_30655,plain,
( hskp11
| hskp5
| hskp13
| hskp9
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30654]) ).
cnf(c_30656,plain,
( hskp11
| hskp5
| hskp9
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30655]) ).
cnf(c_30657,plain,
( hskp11
| hskp9
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30656]) ).
cnf(c_5578,plain,
( hskp9
| c0_1(a775)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30657]) ).
cnf(c_30658,plain,
( hskp9
| hskp25
| c3_1(a775)
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5578,c_246]) ).
cnf(c_30659,plain,
( hskp9
| c3_1(a775)
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30658]) ).
cnf(c_5579,plain,
( c3_1(a775)
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30659]) ).
cnf(c_5586,plain,
( ~ hskp18
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5579,c_92]) ).
cnf(c_30660,plain,
( hskp11
| hskp5
| hskp13
| hskp25
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5586,c_5444]) ).
cnf(c_30661,plain,
( hskp11
| hskp5
| hskp13
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30660]) ).
cnf(c_30662,plain,
( hskp11
| hskp5
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30661]) ).
cnf(c_30663,plain,
( hskp11
| c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30662]) ).
cnf(c_5587,plain,
( c2_1(a775)
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30663]) ).
cnf(c_5616,plain,
( ~ hskp18
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5587,c_91]) ).
cnf(c_30664,plain,
( hskp11
| hskp5
| hskp13
| hskp25
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5616,c_5444]) ).
cnf(c_30665,plain,
( hskp11
| hskp5
| hskp13
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30664]) ).
cnf(c_30666,plain,
( hskp11
| hskp5
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30665]) ).
cnf(c_30667,plain,
( hskp11
| hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30666]) ).
cnf(c_5617,plain,
( hskp9
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30667]) ).
cnf(c_5620,plain,
( c3_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5617,c_68]) ).
cnf(c_30668,plain,
( hskp6
| hskp25
| c2_1(a746)
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5620,c_251]) ).
cnf(c_5644,plain,
( hskp6
| c2_1(a746)
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30668]) ).
cnf(c_5709,plain,
( ~ hskp9
| hskp6
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5644,c_107]) ).
cnf(c_30669,plain,
( hskp11
| hskp5
| hskp13
| hskp25
| hskp6
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5709,c_5617]) ).
cnf(c_30670,plain,
( hskp11
| hskp5
| hskp13
| hskp6
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30669]) ).
cnf(c_30671,plain,
( hskp11
| hskp5
| hskp6
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30670]) ).
cnf(c_30672,plain,
( hskp11
| hskp6
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30671]) ).
cnf(c_5710,plain,
( hskp6
| c0_1(a746)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30672]) ).
cnf(c_5711,plain,
( ~ hskp9
| hskp6
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5710,c_106]) ).
cnf(c_30673,plain,
( hskp11
| hskp5
| hskp13
| hskp25
| hskp6
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5711,c_5617]) ).
cnf(c_30674,plain,
( hskp11
| hskp5
| hskp13
| hskp6
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30673]) ).
cnf(c_30675,plain,
( hskp11
| hskp5
| hskp6
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30674]) ).
cnf(c_30676,plain,
( hskp11
| hskp6
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30675]) ).
cnf(c_5712,plain,
( hskp6
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30676]) ).
cnf(c_5713,plain,
( c1_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5712,c_72]) ).
cnf(c_30677,plain,
( hskp5
| c2_1(a738)
| c3_1(a738)
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5713,c_205]) ).
cnf(c_5745,plain,
( c2_1(a738)
| c3_1(a738)
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30677]) ).
cnf(c_5748,plain,
( c0_1(a738)
| c2_1(a738)
| ~ c3_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5713,c_201]) ).
cnf(c_30678,plain,
( c2_1(A)
| hskp5
| hskp4
| c0_1(A)
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c2_1(a741) ),
inference(resolve,[status(thm)],[c_781,c_341]) ).
cnf(c_30679,plain,
( c2_1(A)
| hskp5
| hskp4
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c2_1(a741) ),
inference(copy,[status(thm)],[c_30678]) ).
cnf(c_30680,plain,
( c2_1(A)
| hskp5
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c2_1(a741) ),
inference(copy,[status(thm)],[c_30679]) ).
cnf(c_5802,plain,
( hskp5
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741)
| ~ c2_1(a741) ),
inference(copy,[status(thm)],[c_30680]) ).
cnf(c_30681,plain,
( c2_1(a738)
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25
| c0_1(a738)
| c2_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_5748,c_5745]) ).
cnf(c_30682,plain,
( c2_1(a738)
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| c0_1(a738)
| c2_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30681]) ).
cnf(c_30683,plain,
( c2_1(a738)
| c0_1(a738)
| hskp11
| hskp5
| c0_1(a738)
| c2_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30682]) ).
cnf(c_30684,plain,
( c2_1(a738)
| c0_1(a738)
| hskp11
| c0_1(a738)
| c2_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30683]) ).
cnf(c_30685,plain,
( c2_1(a738)
| c0_1(a738)
| c0_1(a738)
| c2_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30684]) ).
cnf(c_30686,plain,
( c2_1(a738)
| c0_1(a738)
| c2_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30685]) ).
cnf(c_7632,plain,
( c0_1(a738)
| c2_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30686]) ).
cnf(c_7639,plain,
( ~ hskp6
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_7632,c_112]) ).
cnf(c_30687,plain,
( hskp11
| hskp5
| hskp13
| hskp25
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_7639,c_5712]) ).
cnf(c_30688,plain,
( hskp11
| hskp5
| hskp13
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30687]) ).
cnf(c_30689,plain,
( hskp11
| hskp5
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30688]) ).
cnf(c_30690,plain,
( hskp11
| c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30689]) ).
cnf(c_7640,plain,
( c0_1(a738)
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30690]) ).
cnf(c_7642,plain,
( ~ hskp6
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_7640,c_111]) ).
cnf(c_30691,plain,
( hskp11
| hskp5
| hskp13
| hskp25
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(resolve,[status(thm)],[c_7642,c_5712]) ).
cnf(c_30692,plain,
( hskp11
| hskp5
| hskp13
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30691]) ).
cnf(c_30693,plain,
( hskp11
| hskp5
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30692]) ).
cnf(c_30694,plain,
( hskp11
| hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30693]) ).
cnf(c_7643,plain,
( hskp11
| hskp5
| hskp13
| hskp25 ),
inference(copy,[status(thm)],[c_30694]) ).
cnf(c_7654,plain,
( c3_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(resolve,[status(thm)],[c_7643,c_65]) ).
cnf(c_7655,plain,
( c2_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(resolve,[status(thm)],[c_7643,c_64]) ).
cnf(c_30695,plain,
( hskp20
| hskp5
| c1_1(a759)
| ~ c2_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(resolve,[status(thm)],[c_7654,c_241]) ).
cnf(c_7688,plain,
( hskp20
| c1_1(a759)
| ~ c2_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(copy,[status(thm)],[c_30695]) ).
cnf(c_30696,plain,
( hskp11
| hskp5
| hskp25
| hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(resolve,[status(thm)],[c_7688,c_7655]) ).
cnf(c_30697,plain,
( hskp11
| hskp5
| hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(copy,[status(thm)],[c_30696]) ).
cnf(c_30698,plain,
( hskp11
| hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(copy,[status(thm)],[c_30697]) ).
cnf(c_7708,plain,
( hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp25 ),
inference(copy,[status(thm)],[c_30698]) ).
cnf(c_7723,plain,
( ~ hskp13
| hskp20
| hskp11
| hskp5
| hskp25 ),
inference(resolve,[status(thm)],[c_7708,c_98]) ).
cnf(c_30699,plain,
( hskp11
| hskp5
| hskp25
| hskp20
| hskp11
| hskp5
| hskp25 ),
inference(resolve,[status(thm)],[c_7723,c_7643]) ).
cnf(c_30700,plain,
( hskp11
| hskp5
| hskp20
| hskp11
| hskp5
| hskp25 ),
inference(copy,[status(thm)],[c_30699]) ).
cnf(c_30701,plain,
( hskp11
| hskp20
| hskp11
| hskp5
| hskp25 ),
inference(copy,[status(thm)],[c_30700]) ).
cnf(c_7724,plain,
( hskp20
| hskp11
| hskp5
| hskp25 ),
inference(copy,[status(thm)],[c_30701]) ).
cnf(c_7735,plain,
( c2_1(a779)
| hskp11
| hskp5
| hskp25 ),
inference(resolve,[status(thm)],[c_7724,c_54]) ).
cnf(c_30702,plain,
( hskp0
| hskp11
| c2_1(A)
| c1_1(A)
| c2_1(a731)
| ~ c3_1(A)
| hskp0 ),
inference(resolve,[status(thm)],[c_1546,c_1510]) ).
cnf(c_8833,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| c2_1(a731)
| ~ c3_1(A)
| hskp0 ),
inference(copy,[status(thm)],[c_30702]) ).
cnf(c_30703,plain,
( hskp0
| c3_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a731)
| ~ c0_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_1561,c_1510]) ).
cnf(c_9170,plain,
( c3_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a731)
| ~ c0_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30703]) ).
cnf(c_30704,plain,
( hskp0
| hskp11
| c2_1(a744)
| c1_1(a744)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_8833,c_195]) ).
cnf(c_9691,plain,
( hskp11
| c2_1(a744)
| c1_1(a744)
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30704]) ).
cnf(c_9741,plain,
( ~ hskp8
| hskp11
| c2_1(a744)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_9691,c_109]) ).
cnf(c_30705,plain,
( hskp0
| hskp11
| c2_1(a744)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_9741,c_1]) ).
cnf(c_9742,plain,
( hskp11
| c2_1(a744)
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30705]) ).
cnf(c_30706,plain,
( c0_1(a744)
| c1_1(a744)
| c2_1(a731)
| ~ c0_1(a731)
| hskp0
| hskp11
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_9742,c_1520]) ).
cnf(c_30707,plain,
( c0_1(a744)
| c1_1(a744)
| c2_1(a731)
| ~ c0_1(a731)
| hskp11
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30706]) ).
cnf(c_9743,plain,
( c0_1(a744)
| c1_1(a744)
| ~ c0_1(a731)
| hskp11
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30707]) ).
cnf(c_30708,plain,
( hskp0
| c0_1(a744)
| c1_1(a744)
| hskp11
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_9743,c_1609]) ).
cnf(c_10409,plain,
( c0_1(a744)
| c1_1(a744)
| hskp11
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30708]) ).
cnf(c_10423,plain,
( ~ hskp8
| c0_1(a744)
| hskp11
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_10409,c_109]) ).
cnf(c_30709,plain,
( hskp0
| c0_1(a744)
| hskp11
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_10423,c_1]) ).
cnf(c_10424,plain,
( c0_1(a744)
| hskp11
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30709]) ).
cnf(c_10434,plain,
( ~ hskp1
| c0_1(a744)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_10424,c_121]) ).
cnf(c_30710,plain,
( hskp0
| c0_1(a744)
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_10434,c_1502]) ).
cnf(c_10436,plain,
( c0_1(a744)
| hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_30710]) ).
cnf(c_10442,plain,
( ~ hskp8
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_10436,c_108]) ).
cnf(c_30711,plain,
( hskp0
| hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_10442,c_1]) ).
cnf(c_10443,plain,
( hskp11
| hskp0 ),
inference(copy,[status(thm)],[c_30711]) ).
cnf(c_30712,plain,
( hskp4
| hskp1
| c0_1(a741)
| hskp5
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741) ),
inference(resolve,[status(thm)],[c_5802,c_378]) ).
cnf(c_30713,plain,
( hskp4
| hskp1
| hskp5
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741) ),
inference(copy,[status(thm)],[c_30712]) ).
cnf(c_30714,plain,
( hskp4
| hskp5
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741) ),
inference(copy,[status(thm)],[c_30713]) ).
cnf(c_13019,plain,
( hskp5
| hskp4
| hskp1
| c2_1(A)
| c0_1(A)
| c0_1(a741) ),
inference(copy,[status(thm)],[c_30714]) ).
cnf(c_13023,plain,
( ~ hskp2
| hskp5
| hskp4
| hskp1
| c0_1(a732)
| c0_1(a741) ),
inference(resolve,[status(thm)],[c_13019,c_119]) ).
cnf(c_30715,plain,
( hskp0
| c3_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_9170,c_1609]) ).
cnf(c_14188,plain,
( c3_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30715]) ).
cnf(c_14209,plain,
( ~ hskp11
| c3_1(a749)
| c0_1(a749)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_14188,c_101]) ).
cnf(c_30716,plain,
( hskp0
| c3_1(a749)
| c0_1(a749)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_14209,c_10443]) ).
cnf(c_14294,plain,
( c3_1(a749)
| c0_1(a749)
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30716]) ).
cnf(c_14341,plain,
( ~ hskp11
| c0_1(a749)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_14294,c_102]) ).
cnf(c_30717,plain,
( hskp0
| c0_1(a749)
| c2_1(a731)
| hskp0 ),
inference(resolve,[status(thm)],[c_14341,c_10443]) ).
cnf(c_14343,plain,
( c0_1(a749)
| c2_1(a731)
| hskp0 ),
inference(copy,[status(thm)],[c_30717]) ).
cnf(c_14351,plain,
( ~ hskp1
| c0_1(a749)
| hskp0 ),
inference(resolve,[status(thm)],[c_14343,c_121]) ).
cnf(c_30718,plain,
( hskp0
| c0_1(a749)
| hskp0 ),
inference(resolve,[status(thm)],[c_14351,c_1502]) ).
cnf(c_14354,plain,
( c0_1(a749)
| hskp0 ),
inference(copy,[status(thm)],[c_30718]) ).
cnf(c_14358,plain,
( ~ hskp11
| hskp0 ),
inference(resolve,[status(thm)],[c_14354,c_100]) ).
cnf(c_30719,plain,
( hskp0
| hskp0 ),
inference(resolve,[status(thm)],[c_14358,c_10443]) ).
cnf(c_14359,plain,
hskp0,
inference(copy,[status(thm)],[c_30719]) ).
cnf(c_14360,plain,
~ c1_1(a730),
inference(resolve,[status(thm)],[c_14359,c_122]) ).
cnf(c_14361,plain,
c3_1(a730),
inference(resolve,[status(thm)],[c_14359,c_80]) ).
cnf(c_14362,plain,
c0_1(a730),
inference(resolve,[status(thm)],[c_14359,c_79]) ).
cnf(c_30720,plain,
( hskp19
| hskp27
| c1_1(a730)
| ~ c0_1(a730) ),
inference(resolve,[status(thm)],[c_14361,c_242]) ).
cnf(c_30721,plain,
( hskp19
| hskp27
| c1_1(a730) ),
inference(resolve,[status(thm)],[c_14362,c_30720]) ).
cnf(c_14429,plain,
( hskp19
| hskp27 ),
inference(resolve,[status(thm)],[c_14360,c_30721]) ).
cnf(c_30722,plain,
( hskp20
| hskp5
| c1_1(a730)
| ~ c2_1(a730) ),
inference(resolve,[status(thm)],[c_14361,c_241]) ).
cnf(c_14430,plain,
( hskp20
| hskp5
| ~ c2_1(a730) ),
inference(resolve,[status(thm)],[c_14360,c_30722]) ).
cnf(c_30723,plain,
( hskp21
| ~ c2_1(a730)
| ~ c0_1(a730) ),
inference(resolve,[status(thm)],[c_14361,c_238]) ).
cnf(c_14431,plain,
( hskp21
| ~ c2_1(a730) ),
inference(resolve,[status(thm)],[c_14362,c_30723]) ).
cnf(c_30724,plain,
( hskp25
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c1_1(a730)
| ~ c0_1(a730) ),
inference(resolve,[status(thm)],[c_14361,c_232]) ).
cnf(c_30725,plain,
( hskp25
| c2_1(A)
| c1_1(A)
| c0_1(A)
| c1_1(a730) ),
inference(resolve,[status(thm)],[c_14362,c_30724]) ).
cnf(c_14433,plain,
( hskp25
| c2_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14360,c_30725]) ).
cnf(c_30726,plain,
( hskp5
| c3_1(A)
| c1_1(A)
| c1_1(a730)
| ~ c2_1(A)
| ~ c0_1(a730) ),
inference(resolve,[status(thm)],[c_14361,c_220]) ).
cnf(c_30727,plain,
( hskp5
| c3_1(A)
| c1_1(A)
| c1_1(a730)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_14362,c_30726]) ).
cnf(c_14434,plain,
( hskp5
| c3_1(A)
| c1_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_14360,c_30727]) ).
cnf(c_30728,plain,
( c0_1(B)
| c1_1(a730)
| c2_1(A)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c2_1(a730)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_14361,c_206]) ).
cnf(c_14436,plain,
( c0_1(B)
| c2_1(A)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c2_1(a730)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_14360,c_30728]) ).
cnf(c_30729,plain,
( c0_1(B)
| c1_1(A)
| c2_1(a730)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(a730) ),
inference(resolve,[status(thm)],[c_14361,c_206]) ).
cnf(c_14437,plain,
( c0_1(B)
| c1_1(A)
| c2_1(a730)
| ~ c3_1(B)
| ~ c2_1(B)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_14362,c_30729]) ).
cnf(c_30730,plain,
( c0_1(A)
| c1_1(A)
| c2_1(a730)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(a730) ),
inference(resolve,[status(thm)],[c_14361,c_202]) ).
cnf(c_14438,plain,
( c0_1(A)
| c1_1(A)
| c2_1(a730)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_14362,c_30730]) ).
cnf(c_30731,plain,
( hskp4
| hskp1
| hskp2
| c0_1(a741)
| c2_1(a730)
| c1_1(a730) ),
inference(resolve,[status(thm)],[c_14362,c_2397]) ).
cnf(c_14439,plain,
( hskp4
| hskp1
| hskp2
| c0_1(a741)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_14360,c_30731]) ).
cnf(c_14449,plain,
( c2_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_14429,c_55]) ).
cnf(c_14479,plain,
( hskp8
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c3_1(a777)
| c0_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_14449,c_233]) ).
cnf(c_30732,plain,
( hskp10
| c2_1(A)
| c0_1(A)
| c0_1(B)
| ~ c3_1(B)
| ~ c2_1(B)
| hskp25
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_14433,c_225]) ).
cnf(c_30733,plain,
( hskp10
| c2_1(A)
| c0_1(B)
| ~ c3_1(B)
| ~ c2_1(B)
| hskp25
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30732]) ).
cnf(c_14561,plain,
( hskp10
| c0_1(B)
| ~ c3_1(B)
| ~ c2_1(B)
| hskp25
| c2_1(A)
| c0_1(A) ),
inference(copy,[status(thm)],[c_30733]) ).
cnf(c_14574,plain,
( ~ hskp10
| hskp25
| c2_1(a748)
| c0_1(a748) ),
inference(resolve,[status(thm)],[c_14433,c_104]) ).
cnf(c_30734,plain,
( hskp11
| hskp5
| hskp25
| hskp5
| c3_1(a779)
| c1_1(a779) ),
inference(resolve,[status(thm)],[c_14434,c_7735]) ).
cnf(c_14582,plain,
( hskp11
| hskp25
| hskp5
| c3_1(a779)
| c1_1(a779) ),
inference(copy,[status(thm)],[c_30734]) ).
cnf(c_14603,plain,
( hskp20
| hskp5
| hskp4
| hskp1
| hskp2
| c0_1(a741) ),
inference(resolve,[status(thm)],[c_14439,c_14430]) ).
cnf(c_14692,plain,
( ~ hskp20
| hskp11
| hskp25
| hskp5
| c3_1(a779) ),
inference(resolve,[status(thm)],[c_14582,c_87]) ).
cnf(c_30735,plain,
( hskp11
| hskp5
| hskp25
| hskp11
| hskp25
| hskp5
| c3_1(a779) ),
inference(resolve,[status(thm)],[c_14692,c_7724]) ).
cnf(c_30736,plain,
( hskp11
| hskp5
| hskp11
| hskp25
| hskp5
| c3_1(a779) ),
inference(copy,[status(thm)],[c_30735]) ).
cnf(c_30737,plain,
( hskp11
| hskp11
| hskp25
| hskp5
| c3_1(a779) ),
inference(copy,[status(thm)],[c_30736]) ).
cnf(c_14693,plain,
( hskp11
| hskp25
| hskp5
| c3_1(a779) ),
inference(copy,[status(thm)],[c_30737]) ).
cnf(c_14714,plain,
( ~ hskp20
| hskp11
| hskp25
| hskp5 ),
inference(resolve,[status(thm)],[c_14693,c_88]) ).
cnf(c_30738,plain,
( hskp11
| hskp5
| hskp25
| hskp11
| hskp25
| hskp5 ),
inference(resolve,[status(thm)],[c_14714,c_7724]) ).
cnf(c_30739,plain,
( hskp11
| hskp5
| hskp11
| hskp25
| hskp5 ),
inference(copy,[status(thm)],[c_30738]) ).
cnf(c_30740,plain,
( hskp11
| hskp11
| hskp25
| hskp5 ),
inference(copy,[status(thm)],[c_30739]) ).
cnf(c_14715,plain,
( hskp11
| hskp25
| hskp5 ),
inference(copy,[status(thm)],[c_30740]) ).
cnf(c_14719,plain,
( c3_1(a729)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14715,c_47]) ).
cnf(c_14720,plain,
( c2_1(a729)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14715,c_46]) ).
cnf(c_14721,plain,
( c0_1(a729)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14715,c_45]) ).
cnf(c_30741,plain,
( hskp11
| hskp28
| ~ c2_1(a729)
| ~ c0_1(a729)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14719,c_237]) ).
cnf(c_14734,plain,
( hskp28
| ~ c2_1(a729)
| ~ c0_1(a729)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30741]) ).
cnf(c_14786,plain,
( ~ hskp7
| hskp20
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_14603,c_110]) ).
cnf(c_30742,plain,
( hskp4
| hskp1
| hskp20
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_14786,c_35]) ).
cnf(c_30743,plain,
( hskp4
| hskp20
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30742]) ).
cnf(c_14787,plain,
( hskp20
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30743]) ).
cnf(c_14792,plain,
( c2_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_14787,c_54]) ).
cnf(c_30744,plain,
( hskp5
| c3_1(a779)
| c1_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_14792,c_14434]) ).
cnf(c_14793,plain,
( c3_1(a779)
| c1_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30744]) ).
cnf(c_30745,plain,
( hskp11
| hskp5
| hskp28
| ~ c0_1(a729)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14734,c_14720]) ).
cnf(c_30746,plain,
( hskp11
| hskp28
| ~ c0_1(a729)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30745]) ).
cnf(c_14925,plain,
( hskp28
| ~ c0_1(a729)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30746]) ).
cnf(c_30747,plain,
( hskp11
| hskp5
| hskp28
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14925,c_14721]) ).
cnf(c_30748,plain,
( hskp11
| hskp28
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30747]) ).
cnf(c_14926,plain,
( hskp28
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30748]) ).
cnf(c_14927,plain,
( c3_1(a784)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14926,c_38]) ).
cnf(c_14928,plain,
( c1_1(a784)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14926,c_37]) ).
cnf(c_14929,plain,
( c0_1(a784)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14926,c_36]) ).
cnf(c_14948,plain,
( hskp15
| c3_1(A)
| c0_1(A)
| ~ c2_1(A)
| ~ c3_1(a784)
| ~ c0_1(a784)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14928,c_217]) ).
cnf(c_15352,plain,
( ~ hskp20
| c3_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_14793,c_87]) ).
cnf(c_30749,plain,
( hskp5
| hskp4
| hskp1
| hskp2
| c3_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_15352,c_14787]) ).
cnf(c_30750,plain,
( hskp5
| hskp4
| hskp1
| c3_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30749]) ).
cnf(c_30751,plain,
( hskp5
| hskp4
| c3_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30750]) ).
cnf(c_30752,plain,
( hskp5
| c3_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30751]) ).
cnf(c_15353,plain,
( c3_1(a779)
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30752]) ).
cnf(c_15360,plain,
( ~ hskp20
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_15353,c_88]) ).
cnf(c_30753,plain,
( hskp5
| hskp4
| hskp1
| hskp2
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(resolve,[status(thm)],[c_15360,c_14787]) ).
cnf(c_30754,plain,
( hskp5
| hskp4
| hskp1
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30753]) ).
cnf(c_30755,plain,
( hskp5
| hskp4
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30754]) ).
cnf(c_30756,plain,
( hskp5
| hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30755]) ).
cnf(c_15375,plain,
( hskp5
| hskp4
| hskp1
| hskp2 ),
inference(copy,[status(thm)],[c_30756]) ).
cnf(c_30757,plain,
( hskp5
| hskp4
| hskp1
| c0_1(a732)
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(resolve,[status(thm)],[c_15375,c_13023]) ).
cnf(c_30758,plain,
( hskp5
| hskp4
| c0_1(a732)
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30757]) ).
cnf(c_30759,plain,
( hskp5
| c0_1(a732)
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30758]) ).
cnf(c_15377,plain,
( c0_1(a732)
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30759]) ).
cnf(c_15463,plain,
( ~ hskp2
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(resolve,[status(thm)],[c_15377,c_118]) ).
cnf(c_30760,plain,
( hskp5
| hskp4
| hskp1
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(resolve,[status(thm)],[c_15463,c_15375]) ).
cnf(c_30761,plain,
( hskp5
| hskp4
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30760]) ).
cnf(c_30762,plain,
( hskp5
| c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30761]) ).
cnf(c_15464,plain,
( c0_1(a741)
| hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30762]) ).
cnf(c_15469,plain,
( ~ hskp7
| hskp5
| hskp4
| hskp1 ),
inference(resolve,[status(thm)],[c_15464,c_110]) ).
cnf(c_30763,plain,
( hskp4
| hskp1
| hskp5
| hskp4
| hskp1 ),
inference(resolve,[status(thm)],[c_15469,c_35]) ).
cnf(c_30764,plain,
( hskp4
| hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30763]) ).
cnf(c_15470,plain,
( hskp5
| hskp4
| hskp1 ),
inference(copy,[status(thm)],[c_30764]) ).
cnf(c_15472,plain,
( c1_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15470,c_75]) ).
cnf(c_30765,plain,
( hskp5
| c2_1(A)
| c0_1(A)
| c3_1(a734)
| c0_1(a734)
| ~ c1_1(A)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15472,c_229]) ).
cnf(c_15480,plain,
( c2_1(A)
| c0_1(A)
| c3_1(a734)
| c0_1(a734)
| ~ c1_1(A)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30765]) ).
cnf(c_30766,plain,
( hskp5
| c1_1(A)
| c0_1(A)
| c0_1(a734)
| ~ c3_1(A)
| ~ c2_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15472,c_227]) ).
cnf(c_15482,plain,
( c1_1(A)
| c0_1(A)
| c0_1(a734)
| ~ c3_1(A)
| ~ c2_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30766]) ).
cnf(c_15486,plain,
( hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(A)
| ~ c1_1(A)
| ~ c0_1(A)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15472,c_223]) ).
cnf(c_30767,plain,
( hskp5
| c2_1(a734)
| c3_1(a734)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15472,c_205]) ).
cnf(c_15499,plain,
( c2_1(a734)
| c3_1(a734)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30767]) ).
cnf(c_15666,plain,
( ~ hskp4
| c2_1(a734)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15499,c_115]) ).
cnf(c_30768,plain,
( hskp5
| hskp1
| c2_1(a734)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15666,c_15470]) ).
cnf(c_30769,plain,
( hskp5
| c2_1(a734)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30768]) ).
cnf(c_15667,plain,
( c2_1(a734)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30769]) ).
cnf(c_17956,plain,
( ~ hskp19
| hskp8
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_14479,c_90]) ).
cnf(c_30770,plain,
( hskp27
| hskp8
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_17956,c_14429]) ).
cnf(c_17999,plain,
( hskp8
| c3_1(A)
| c2_1(A)
| c0_1(A)
| c0_1(a777)
| hskp27 ),
inference(copy,[status(thm)],[c_30770]) ).
cnf(c_18031,plain,
( ~ hskp2
| hskp8
| c2_1(a732)
| c0_1(a732)
| c0_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_17999,c_120]) ).
cnf(c_30771,plain,
( hskp11
| hskp5
| hskp15
| c3_1(A)
| c0_1(A)
| ~ c2_1(A)
| ~ c0_1(a784)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_14948,c_14927]) ).
cnf(c_30772,plain,
( hskp11
| hskp15
| c3_1(A)
| c0_1(A)
| ~ c2_1(A)
| ~ c0_1(a784)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30771]) ).
cnf(c_22236,plain,
( hskp15
| c3_1(A)
| c0_1(A)
| ~ c2_1(A)
| ~ c0_1(a784)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30772]) ).
cnf(c_30773,plain,
( c0_1(a734)
| hskp5
| hskp1
| hskp15
| c3_1(a734)
| c0_1(a734)
| ~ c0_1(a784)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_22236,c_15667]) ).
cnf(c_30774,plain,
( c0_1(a734)
| hskp1
| hskp15
| c3_1(a734)
| c0_1(a734)
| ~ c0_1(a784)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30773]) ).
cnf(c_23511,plain,
( hskp1
| hskp15
| c3_1(a734)
| c0_1(a734)
| ~ c0_1(a784)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30774]) ).
cnf(c_30775,plain,
( hskp11
| hskp5
| hskp1
| hskp15
| c3_1(a734)
| c0_1(a734)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_23511,c_14929]) ).
cnf(c_30776,plain,
( hskp11
| hskp1
| hskp15
| c3_1(a734)
| c0_1(a734)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30775]) ).
cnf(c_23515,plain,
( hskp1
| hskp15
| c3_1(a734)
| c0_1(a734)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30776]) ).
cnf(c_23527,plain,
( ~ hskp4
| hskp1
| hskp15
| c0_1(a734)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_23515,c_115]) ).
cnf(c_30777,plain,
( hskp5
| hskp1
| hskp1
| hskp15
| c0_1(a734)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_23527,c_15470]) ).
cnf(c_30778,plain,
( hskp5
| hskp1
| hskp15
| c0_1(a734)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30777]) ).
cnf(c_23528,plain,
( hskp1
| hskp15
| c0_1(a734)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30778]) ).
cnf(c_23530,plain,
( ~ hskp4
| hskp1
| hskp15
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_23528,c_114]) ).
cnf(c_30779,plain,
( hskp5
| hskp1
| hskp1
| hskp15
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_23530,c_15470]) ).
cnf(c_30780,plain,
( hskp5
| hskp1
| hskp15
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30779]) ).
cnf(c_23531,plain,
( hskp1
| hskp15
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30780]) ).
cnf(c_23533,plain,
( c1_1(a763)
| hskp1
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_23531,c_62]) ).
cnf(c_23534,plain,
( c0_1(a763)
| hskp1
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_23531,c_61]) ).
cnf(c_30781,plain,
( hskp1
| hskp11
| hskp5
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a763)
| ~ c0_1(a763)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_15486,c_23533]) ).
cnf(c_30782,plain,
( hskp1
| hskp11
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a763)
| ~ c0_1(a763)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30781]) ).
cnf(c_23818,plain,
( hskp11
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a763)
| ~ c0_1(a763)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30782]) ).
cnf(c_30783,plain,
( hskp1
| hskp11
| hskp5
| hskp11
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_23818,c_23534]) ).
cnf(c_30784,plain,
( hskp1
| hskp11
| hskp11
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30783]) ).
cnf(c_30785,plain,
( hskp1
| hskp11
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30784]) ).
cnf(c_27358,plain,
( hskp11
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30785]) ).
cnf(c_27367,plain,
( ~ hskp4
| hskp11
| hskp13
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27358,c_115]) ).
cnf(c_30786,plain,
( hskp5
| hskp1
| hskp11
| hskp13
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27367,c_15470]) ).
cnf(c_30787,plain,
( hskp5
| hskp11
| hskp13
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30786]) ).
cnf(c_27374,plain,
( hskp11
| hskp13
| c0_1(a734)
| c2_1(a763)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30787]) ).
cnf(c_27375,plain,
( ~ hskp15
| hskp11
| hskp13
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27374,c_95]) ).
cnf(c_30788,plain,
( hskp1
| hskp11
| hskp5
| hskp11
| hskp13
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27375,c_23531]) ).
cnf(c_30789,plain,
( hskp1
| hskp11
| hskp11
| hskp13
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30788]) ).
cnf(c_30790,plain,
( hskp1
| hskp11
| hskp13
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30789]) ).
cnf(c_27376,plain,
( hskp11
| hskp13
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30790]) ).
cnf(c_27381,plain,
( ~ hskp4
| hskp11
| hskp13
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27376,c_114]) ).
cnf(c_30791,plain,
( hskp5
| hskp1
| hskp11
| hskp13
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27381,c_15470]) ).
cnf(c_30792,plain,
( hskp5
| hskp11
| hskp13
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30791]) ).
cnf(c_27382,plain,
( hskp11
| hskp13
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30792]) ).
cnf(c_27385,plain,
( c3_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27382,c_65]) ).
cnf(c_27386,plain,
( c2_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27382,c_64]) ).
cnf(c_30793,plain,
( hskp20
| hskp5
| c1_1(a759)
| ~ c2_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27385,c_241]) ).
cnf(c_27406,plain,
( hskp20
| c1_1(a759)
| ~ c2_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30793]) ).
cnf(c_30794,plain,
( hskp11
| hskp5
| hskp1
| hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27406,c_27386]) ).
cnf(c_30795,plain,
( hskp11
| hskp5
| hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30794]) ).
cnf(c_30796,plain,
( hskp11
| hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30795]) ).
cnf(c_27414,plain,
( hskp20
| c1_1(a759)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30796]) ).
cnf(c_27424,plain,
( ~ hskp13
| hskp20
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27414,c_98]) ).
cnf(c_30797,plain,
( hskp11
| hskp5
| hskp1
| hskp20
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27424,c_27382]) ).
cnf(c_30798,plain,
( hskp11
| hskp5
| hskp20
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30797]) ).
cnf(c_30799,plain,
( hskp11
| hskp20
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30798]) ).
cnf(c_27425,plain,
( hskp20
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30799]) ).
cnf(c_27433,plain,
( c2_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27425,c_54]) ).
cnf(c_30800,plain,
( hskp5
| c3_1(a779)
| c1_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27433,c_14434]) ).
cnf(c_27436,plain,
( c3_1(a779)
| c1_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30800]) ).
cnf(c_27444,plain,
( ~ hskp20
| c3_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27436,c_87]) ).
cnf(c_30801,plain,
( hskp11
| hskp5
| hskp1
| c3_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27444,c_27425]) ).
cnf(c_30802,plain,
( hskp11
| hskp5
| c3_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30801]) ).
cnf(c_30803,plain,
( hskp11
| c3_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30802]) ).
cnf(c_27445,plain,
( c3_1(a779)
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30803]) ).
cnf(c_27469,plain,
( ~ hskp20
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27445,c_88]) ).
cnf(c_30804,plain,
( hskp11
| hskp5
| hskp1
| hskp11
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27469,c_27425]) ).
cnf(c_30805,plain,
( hskp11
| hskp5
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30804]) ).
cnf(c_30806,plain,
( hskp11
| hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30805]) ).
cnf(c_27470,plain,
( hskp11
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30806]) ).
cnf(c_30807,plain,
( hskp9
| hskp5
| c2_1(a749)
| c0_1(a749)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27470,c_330]) ).
cnf(c_27488,plain,
( hskp9
| c2_1(a749)
| c0_1(a749)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30807]) ).
cnf(c_30808,plain,
( hskp2
| hskp1
| c1_1(a749)
| c0_1(a749)
| hskp9
| c0_1(a749)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27488,c_253]) ).
cnf(c_30809,plain,
( hskp2
| hskp1
| c1_1(a749)
| hskp9
| c0_1(a749)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30808]) ).
cnf(c_27520,plain,
( hskp2
| c1_1(a749)
| hskp9
| c0_1(a749)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30809]) ).
cnf(c_27574,plain,
( ~ hskp11
| hskp2
| hskp9
| c0_1(a749)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27520,c_101]) ).
cnf(c_30810,plain,
( hskp5
| hskp1
| hskp2
| hskp9
| c0_1(a749)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27574,c_27470]) ).
cnf(c_30811,plain,
( hskp5
| hskp2
| hskp9
| c0_1(a749)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30810]) ).
cnf(c_27575,plain,
( hskp2
| hskp9
| c0_1(a749)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30811]) ).
cnf(c_27576,plain,
( ~ hskp11
| hskp2
| hskp9
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27575,c_100]) ).
cnf(c_30812,plain,
( hskp5
| hskp1
| hskp2
| hskp9
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27576,c_27470]) ).
cnf(c_30813,plain,
( hskp5
| hskp2
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30812]) ).
cnf(c_27593,plain,
( hskp2
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30813]) ).
cnf(c_30814,plain,
( hskp9
| hskp5
| c2_1(a732)
| c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27593,c_328]) ).
cnf(c_30815,plain,
( hskp9
| c2_1(a732)
| c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30814]) ).
cnf(c_27594,plain,
( c2_1(a732)
| c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30815]) ).
cnf(c_27600,plain,
( ~ hskp2
| c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27594,c_119]) ).
cnf(c_30816,plain,
( hskp9
| hskp5
| hskp1
| c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27600,c_27593]) ).
cnf(c_30817,plain,
( hskp9
| hskp5
| c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30816]) ).
cnf(c_30818,plain,
( hskp9
| c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30817]) ).
cnf(c_27601,plain,
( c0_1(a732)
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30818]) ).
cnf(c_27602,plain,
( ~ hskp2
| hskp9
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27601,c_118]) ).
cnf(c_30819,plain,
( hskp9
| hskp5
| hskp1
| hskp9
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27602,c_27593]) ).
cnf(c_30820,plain,
( hskp9
| hskp5
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30819]) ).
cnf(c_30821,plain,
( hskp9
| hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30820]) ).
cnf(c_27603,plain,
( hskp9
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30821]) ).
cnf(c_27604,plain,
( c3_1(a746)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27603,c_68]) ).
cnf(c_30822,plain,
( c1_1(a746)
| c0_1(a746)
| c0_1(a734)
| ~ c2_1(a734)
| hskp5
| hskp1
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27604,c_15482]) ).
cnf(c_30823,plain,
( c1_1(a746)
| c0_1(a746)
| c0_1(a734)
| ~ c2_1(a734)
| hskp5
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30822]) ).
cnf(c_27610,plain,
( c1_1(a746)
| c0_1(a746)
| c0_1(a734)
| ~ c2_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30823]) ).
cnf(c_30824,plain,
( c0_1(a734)
| hskp5
| hskp1
| c1_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27610,c_15667]) ).
cnf(c_30825,plain,
( c0_1(a734)
| hskp5
| c1_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30824]) ).
cnf(c_30826,plain,
( c0_1(a734)
| c1_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30825]) ).
cnf(c_27654,plain,
( c1_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30826]) ).
cnf(c_30827,plain,
( c2_1(a746)
| c0_1(a746)
| c3_1(a734)
| c0_1(a734)
| hskp5
| hskp1
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27654,c_15480]) ).
cnf(c_30828,plain,
( c2_1(a746)
| c0_1(a746)
| c3_1(a734)
| c0_1(a734)
| hskp5
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30827]) ).
cnf(c_30829,plain,
( c2_1(a746)
| c0_1(a746)
| c3_1(a734)
| c0_1(a734)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30828]) ).
cnf(c_30830,plain,
( c2_1(a746)
| c0_1(a746)
| c3_1(a734)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30829]) ).
cnf(c_27656,plain,
( c2_1(a746)
| c3_1(a734)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30830]) ).
cnf(c_27671,plain,
( ~ hskp4
| c2_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27656,c_115]) ).
cnf(c_30831,plain,
( hskp5
| hskp1
| c2_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27671,c_15470]) ).
cnf(c_30832,plain,
( hskp5
| c2_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30831]) ).
cnf(c_27672,plain,
( c2_1(a746)
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30832]) ).
cnf(c_27673,plain,
( ~ hskp9
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27672,c_107]) ).
cnf(c_30833,plain,
( hskp5
| hskp1
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27673,c_27603]) ).
cnf(c_30834,plain,
( hskp5
| c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30833]) ).
cnf(c_27674,plain,
( c0_1(a746)
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30834]) ).
cnf(c_27675,plain,
( ~ hskp9
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27674,c_106]) ).
cnf(c_30835,plain,
( hskp5
| hskp1
| c0_1(a734)
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27675,c_27603]) ).
cnf(c_30836,plain,
( hskp5
| c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30835]) ).
cnf(c_27676,plain,
( c0_1(a734)
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30836]) ).
cnf(c_27678,plain,
( ~ hskp4
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27676,c_114]) ).
cnf(c_30837,plain,
( hskp5
| hskp1
| hskp5
| hskp1 ),
inference(resolve,[status(thm)],[c_27678,c_15470]) ).
cnf(c_30838,plain,
( hskp5
| hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30837]) ).
cnf(c_27679,plain,
( hskp5
| hskp1 ),
inference(copy,[status(thm)],[c_30838]) ).
cnf(c_27686,plain,
( c3_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27679,c_78]) ).
cnf(c_27687,plain,
( c1_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27679,c_77]) ).
cnf(c_27730,plain,
( hskp13
| c3_1(A)
| c0_1(A)
| c2_1(a731)
| ~ c1_1(A)
| ~ c0_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27687,c_223]) ).
cnf(c_27732,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| c2_1(a731)
| ~ c3_1(A)
| ~ c3_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27687,c_221]) ).
cnf(c_27743,plain,
( c0_1(a731)
| c2_1(a731)
| ~ c3_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27687,c_201]) ).
cnf(c_30839,plain,
( hskp5
| c0_1(a731)
| c2_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27743,c_27686]) ).
cnf(c_27747,plain,
( c0_1(a731)
| c2_1(a731)
| hskp5 ),
inference(copy,[status(thm)],[c_30839]) ).
cnf(c_27748,plain,
( ~ hskp1
| c0_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27747,c_121]) ).
cnf(c_30840,plain,
( hskp5
| c0_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27748,c_27679]) ).
cnf(c_27749,plain,
( c0_1(a731)
| hskp5 ),
inference(copy,[status(thm)],[c_30840]) ).
cnf(c_30841,plain,
( hskp11
| c2_1(a730)
| c1_1(a730)
| c2_1(a731)
| ~ c3_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_27732,c_14361]) ).
cnf(c_28599,plain,
( hskp11
| c2_1(a730)
| c2_1(a731)
| ~ c3_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_14360,c_30841]) ).
cnf(c_30842,plain,
( hskp5
| hskp11
| c2_1(a730)
| c2_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_28599,c_27686]) ).
cnf(c_28604,plain,
( hskp11
| c2_1(a730)
| c2_1(a731)
| hskp5 ),
inference(copy,[status(thm)],[c_30842]) ).
cnf(c_28605,plain,
( ~ hskp1
| hskp11
| c2_1(a730)
| hskp5 ),
inference(resolve,[status(thm)],[c_28604,c_121]) ).
cnf(c_30843,plain,
( hskp5
| hskp11
| c2_1(a730)
| hskp5 ),
inference(resolve,[status(thm)],[c_28605,c_27679]) ).
cnf(c_28606,plain,
( hskp11
| c2_1(a730)
| hskp5 ),
inference(copy,[status(thm)],[c_30843]) ).
cnf(c_30844,plain,
( hskp20
| hskp5
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_28606,c_14430]) ).
cnf(c_28607,plain,
( hskp20
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30844]) ).
cnf(c_28622,plain,
( c2_1(a779)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_28607,c_54]) ).
cnf(c_30845,plain,
( hskp5
| c3_1(a779)
| c1_1(a779)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_28622,c_14434]) ).
cnf(c_28624,plain,
( c3_1(a779)
| c1_1(a779)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30845]) ).
cnf(c_28632,plain,
( ~ hskp20
| c3_1(a779)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_28624,c_87]) ).
cnf(c_30846,plain,
( hskp11
| hskp5
| c3_1(a779)
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_28632,c_28607]) ).
cnf(c_30847,plain,
( hskp11
| c3_1(a779)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30846]) ).
cnf(c_28633,plain,
( c3_1(a779)
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30847]) ).
cnf(c_28653,plain,
( ~ hskp20
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_28633,c_88]) ).
cnf(c_30848,plain,
( hskp11
| hskp5
| hskp11
| hskp5 ),
inference(resolve,[status(thm)],[c_28653,c_28607]) ).
cnf(c_30849,plain,
( hskp11
| hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30848]) ).
cnf(c_28654,plain,
( hskp11
| hskp5 ),
inference(copy,[status(thm)],[c_30849]) ).
cnf(c_30850,plain,
( hskp5
| hskp4
| c3_1(a749)
| c0_1(a749)
| hskp5 ),
inference(resolve,[status(thm)],[c_28654,c_344]) ).
cnf(c_28675,plain,
( hskp4
| c3_1(a749)
| c0_1(a749)
| hskp5 ),
inference(copy,[status(thm)],[c_30850]) ).
cnf(c_28778,plain,
( ~ hskp11
| hskp4
| c0_1(a749)
| hskp5 ),
inference(resolve,[status(thm)],[c_28675,c_102]) ).
cnf(c_30851,plain,
( hskp5
| hskp4
| c0_1(a749)
| hskp5 ),
inference(resolve,[status(thm)],[c_28778,c_28654]) ).
cnf(c_28779,plain,
( hskp4
| c0_1(a749)
| hskp5 ),
inference(copy,[status(thm)],[c_30851]) ).
cnf(c_28782,plain,
( ~ hskp11
| hskp4
| hskp5 ),
inference(resolve,[status(thm)],[c_28779,c_100]) ).
cnf(c_30852,plain,
( hskp5
| hskp4
| hskp5 ),
inference(resolve,[status(thm)],[c_28782,c_28654]) ).
cnf(c_28785,plain,
( hskp4
| hskp5 ),
inference(copy,[status(thm)],[c_30852]) ).
cnf(c_28790,plain,
( c1_1(a734)
| hskp5 ),
inference(resolve,[status(thm)],[c_28785,c_75]) ).
cnf(c_30853,plain,
( hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a731)
| ~ c0_1(a731)
| hskp5
| hskp5 ),
inference(resolve,[status(thm)],[c_28790,c_27730]) ).
cnf(c_28791,plain,
( hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a731)
| ~ c0_1(a731)
| hskp5 ),
inference(copy,[status(thm)],[c_30853]) ).
cnf(c_30854,plain,
( hskp5
| hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_28791,c_27749]) ).
cnf(c_29001,plain,
( hskp13
| c3_1(a734)
| c0_1(a734)
| c2_1(a731)
| hskp5 ),
inference(copy,[status(thm)],[c_30854]) ).
cnf(c_29005,plain,
( ~ hskp4
| hskp13
| c0_1(a734)
| c2_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_29001,c_115]) ).
cnf(c_30855,plain,
( hskp5
| hskp13
| c0_1(a734)
| c2_1(a731)
| hskp5 ),
inference(resolve,[status(thm)],[c_29005,c_28785]) ).
cnf(c_29008,plain,
( hskp13
| c0_1(a734)
| c2_1(a731)
| hskp5 ),
inference(copy,[status(thm)],[c_30855]) ).
cnf(c_29010,plain,
( ~ hskp1
| hskp13
| c0_1(a734)
| hskp5 ),
inference(resolve,[status(thm)],[c_29008,c_121]) ).
cnf(c_30856,plain,
( hskp5
| hskp13
| c0_1(a734)
| hskp5 ),
inference(resolve,[status(thm)],[c_29010,c_27679]) ).
cnf(c_29011,plain,
( hskp13
| c0_1(a734)
| hskp5 ),
inference(copy,[status(thm)],[c_30856]) ).
cnf(c_29012,plain,
( ~ hskp4
| hskp13
| hskp5 ),
inference(resolve,[status(thm)],[c_29011,c_114]) ).
cnf(c_30857,plain,
( hskp5
| hskp13
| hskp5 ),
inference(resolve,[status(thm)],[c_29012,c_28785]) ).
cnf(c_29013,plain,
( hskp13
| hskp5 ),
inference(copy,[status(thm)],[c_30857]) ).
cnf(c_29015,plain,
( c3_1(a759)
| hskp5 ),
inference(resolve,[status(thm)],[c_29013,c_65]) ).
cnf(c_29016,plain,
( c2_1(a759)
| hskp5 ),
inference(resolve,[status(thm)],[c_29013,c_64]) ).
cnf(c_30858,plain,
( hskp20
| hskp5
| c1_1(a759)
| ~ c2_1(a759)
| hskp5 ),
inference(resolve,[status(thm)],[c_29015,c_241]) ).
cnf(c_29021,plain,
( hskp20
| c1_1(a759)
| ~ c2_1(a759)
| hskp5 ),
inference(copy,[status(thm)],[c_30858]) ).
cnf(c_30859,plain,
( hskp5
| hskp20
| c1_1(a759)
| hskp5 ),
inference(resolve,[status(thm)],[c_29021,c_29016]) ).
cnf(c_29028,plain,
( hskp20
| c1_1(a759)
| hskp5 ),
inference(copy,[status(thm)],[c_30859]) ).
cnf(c_29042,plain,
( ~ hskp13
| hskp20
| hskp5 ),
inference(resolve,[status(thm)],[c_29028,c_98]) ).
cnf(c_30860,plain,
( hskp5
| hskp20
| hskp5 ),
inference(resolve,[status(thm)],[c_29042,c_29013]) ).
cnf(c_29043,plain,
( hskp20
| hskp5 ),
inference(copy,[status(thm)],[c_30860]) ).
cnf(c_29044,plain,
( c2_1(a779)
| hskp5 ),
inference(resolve,[status(thm)],[c_29043,c_54]) ).
cnf(c_30861,plain,
( hskp5
| c3_1(a779)
| c1_1(a779)
| hskp5 ),
inference(resolve,[status(thm)],[c_29044,c_14434]) ).
cnf(c_29045,plain,
( c3_1(a779)
| c1_1(a779)
| hskp5 ),
inference(copy,[status(thm)],[c_30861]) ).
cnf(c_29051,plain,
( ~ hskp20
| c3_1(a779)
| hskp5 ),
inference(resolve,[status(thm)],[c_29045,c_87]) ).
cnf(c_30862,plain,
( hskp5
| c3_1(a779)
| hskp5 ),
inference(resolve,[status(thm)],[c_29051,c_29043]) ).
cnf(c_29052,plain,
( c3_1(a779)
| hskp5 ),
inference(copy,[status(thm)],[c_30862]) ).
cnf(c_29062,plain,
( ~ hskp20
| hskp5 ),
inference(resolve,[status(thm)],[c_29052,c_88]) ).
cnf(c_30863,plain,
( hskp5
| hskp5 ),
inference(resolve,[status(thm)],[c_29062,c_29043]) ).
cnf(c_29063,plain,
hskp5,
inference(copy,[status(thm)],[c_30863]) ).
cnf(c_29065,plain,
~ c0_1(a735),
inference(resolve,[status(thm)],[c_29063,c_113]) ).
cnf(c_29066,plain,
c3_1(a735),
inference(resolve,[status(thm)],[c_29063,c_74]) ).
cnf(c_29067,plain,
c2_1(a735),
inference(resolve,[status(thm)],[c_29063,c_73]) ).
cnf(c_30864,plain,
( hskp10
| c0_1(a735)
| ~ c2_1(a735)
| hskp25
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_29066,c_14561]) ).
cnf(c_30865,plain,
( hskp10
| c0_1(a735)
| hskp25
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_29067,c_30864]) ).
cnf(c_29293,plain,
( hskp10
| hskp25
| c2_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_29065,c_30865]) ).
cnf(c_30866,plain,
( c0_1(a735)
| c1_1(a735)
| c2_1(a730)
| ~ c2_1(a735) ),
inference(resolve,[status(thm)],[c_29066,c_14438]) ).
cnf(c_30867,plain,
( c0_1(a735)
| c1_1(a735)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29067,c_30866]) ).
cnf(c_29294,plain,
( c1_1(a735)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29065,c_30867]) ).
cnf(c_30868,plain,
( c0_1(a735)
| c1_1(A)
| c2_1(a730)
| ~ c2_1(a735)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_29066,c_14437]) ).
cnf(c_30869,plain,
( c0_1(a735)
| c1_1(A)
| c2_1(a730)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_29067,c_30868]) ).
cnf(c_29295,plain,
( c1_1(A)
| c2_1(a730)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_29065,c_30869]) ).
cnf(c_30870,plain,
( c0_1(a735)
| c2_1(A)
| ~ c2_1(a735)
| ~ c2_1(a730)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_29066,c_14436]) ).
cnf(c_30871,plain,
( c0_1(a735)
| c2_1(A)
| ~ c2_1(a730)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_29067,c_30870]) ).
cnf(c_29296,plain,
( c2_1(A)
| ~ c2_1(a730)
| ~ c3_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_29065,c_30871]) ).
cnf(c_30872,plain,
( hskp2
| c0_1(a735)
| c2_1(A)
| c1_1(A)
| ~ c3_1(a735)
| ~ c0_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29294,c_222]) ).
cnf(c_30873,plain,
( hskp2
| c0_1(a735)
| c2_1(A)
| c1_1(A)
| ~ c0_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29066,c_30872]) ).
cnf(c_29353,plain,
( hskp2
| c2_1(A)
| c1_1(A)
| ~ c0_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29065,c_30873]) ).
cnf(c_30874,plain,
( hskp16
| c0_1(a735)
| ~ c2_1(a735)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29294,c_215]) ).
cnf(c_30875,plain,
( hskp16
| c0_1(a735)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29067,c_30874]) ).
cnf(c_29354,plain,
( hskp16
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29065,c_30875]) ).
cnf(c_30876,plain,
( c2_1(A)
| c0_1(A)
| c0_1(a735)
| ~ c3_1(A)
| ~ c3_1(a735)
| ~ c2_1(a735)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29294,c_203]) ).
cnf(c_30877,plain,
( c2_1(A)
| c0_1(A)
| c0_1(a735)
| ~ c3_1(A)
| ~ c3_1(a735)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29067,c_30876]) ).
cnf(c_30878,plain,
( c2_1(A)
| c0_1(A)
| c0_1(a735)
| ~ c3_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29066,c_30877]) ).
cnf(c_29357,plain,
( c2_1(A)
| c0_1(A)
| ~ c3_1(A)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_29065,c_30878]) ).
cnf(c_30879,plain,
( hskp2
| c1_1(a730)
| ~ c0_1(a730)
| c2_1(a730) ),
inference(factor,[status(thm)],[c_29353]) ).
cnf(c_30880,plain,
( hskp2
| c1_1(a730)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_14362,c_30879]) ).
cnf(c_29358,plain,
( hskp2
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_14360,c_30880]) ).
cnf(c_29373,plain,
( hskp21
| hskp2 ),
inference(resolve,[status(thm)],[c_29358,c_14431]) ).
cnf(c_29546,plain,
( ~ hskp2
| hskp10
| hskp25
| c0_1(a732) ),
inference(resolve,[status(thm)],[c_29293,c_119]) ).
cnf(c_29551,plain,
( hskp21
| hskp10
| hskp25
| c0_1(a732) ),
inference(resolve,[status(thm)],[c_29546,c_29373]) ).
cnf(c_29561,plain,
( ~ hskp2
| hskp21
| hskp10
| hskp25 ),
inference(resolve,[status(thm)],[c_29551,c_118]) ).
cnf(c_30881,plain,
( hskp21
| hskp21
| hskp10
| hskp25 ),
inference(resolve,[status(thm)],[c_29561,c_29373]) ).
cnf(c_29563,plain,
( hskp21
| hskp10
| hskp25 ),
inference(copy,[status(thm)],[c_30881]) ).
cnf(c_30882,plain,
( hskp25
| c2_1(a748)
| c0_1(a748)
| hskp21
| hskp25 ),
inference(resolve,[status(thm)],[c_29563,c_14574]) ).
cnf(c_29572,plain,
( c2_1(a748)
| c0_1(a748)
| hskp21
| hskp25 ),
inference(copy,[status(thm)],[c_30882]) ).
cnf(c_29623,plain,
( ~ hskp10
| c0_1(a748)
| hskp21
| hskp25 ),
inference(resolve,[status(thm)],[c_29572,c_105]) ).
cnf(c_30883,plain,
( hskp21
| hskp25
| c0_1(a748)
| hskp21
| hskp25 ),
inference(resolve,[status(thm)],[c_29623,c_29563]) ).
cnf(c_30884,plain,
( hskp21
| c0_1(a748)
| hskp21
| hskp25 ),
inference(copy,[status(thm)],[c_30883]) ).
cnf(c_29625,plain,
( c0_1(a748)
| hskp21
| hskp25 ),
inference(copy,[status(thm)],[c_30884]) ).
cnf(c_29628,plain,
( ~ hskp10
| hskp21
| hskp25 ),
inference(resolve,[status(thm)],[c_29625,c_103]) ).
cnf(c_30885,plain,
( hskp21
| hskp25
| hskp21
| hskp25 ),
inference(resolve,[status(thm)],[c_29628,c_29563]) ).
cnf(c_30886,plain,
( hskp21
| hskp21
| hskp25 ),
inference(copy,[status(thm)],[c_30885]) ).
cnf(c_29630,plain,
( hskp21
| hskp25 ),
inference(copy,[status(thm)],[c_30886]) ).
cnf(c_29631,plain,
( c3_1(a793)
| hskp25 ),
inference(resolve,[status(thm)],[c_29630,c_53]) ).
cnf(c_29632,plain,
( c0_1(a793)
| hskp25 ),
inference(resolve,[status(thm)],[c_29630,c_52]) ).
cnf(c_29837,plain,
( hskp25
| c2_1(a793)
| ~ c2_1(a730)
| ~ c0_1(a793) ),
inference(resolve,[status(thm)],[c_29296,c_29631]) ).
cnf(c_29873,plain,
( hskp2
| hskp25
| c2_1(a793)
| ~ c0_1(a793) ),
inference(resolve,[status(thm)],[c_29837,c_29358]) ).
cnf(c_30887,plain,
( hskp25
| hskp2
| hskp25
| c2_1(a793) ),
inference(resolve,[status(thm)],[c_29873,c_29632]) ).
cnf(c_29880,plain,
( hskp2
| hskp25
| c2_1(a793) ),
inference(copy,[status(thm)],[c_30887]) ).
cnf(c_29881,plain,
( ~ hskp21
| hskp2
| hskp25 ),
inference(resolve,[status(thm)],[c_29880,c_86]) ).
cnf(c_30888,plain,
( hskp25
| hskp2
| hskp25 ),
inference(resolve,[status(thm)],[c_29881,c_29630]) ).
cnf(c_29882,plain,
( hskp2
| hskp25 ),
inference(copy,[status(thm)],[c_30888]) ).
cnf(c_30889,plain,
( hskp10
| hskp25
| c0_1(a732)
| hskp25 ),
inference(resolve,[status(thm)],[c_29882,c_29546]) ).
cnf(c_29883,plain,
( hskp10
| c0_1(a732)
| hskp25 ),
inference(copy,[status(thm)],[c_30889]) ).
cnf(c_29906,plain,
( ~ hskp2
| hskp10
| hskp25 ),
inference(resolve,[status(thm)],[c_29883,c_118]) ).
cnf(c_30890,plain,
( hskp25
| hskp10
| hskp25 ),
inference(resolve,[status(thm)],[c_29906,c_29882]) ).
cnf(c_29907,plain,
( hskp10
| hskp25 ),
inference(copy,[status(thm)],[c_30890]) ).
cnf(c_30891,plain,
( hskp25
| c2_1(a748)
| c0_1(a748)
| hskp25 ),
inference(resolve,[status(thm)],[c_29907,c_14574]) ).
cnf(c_29922,plain,
( c2_1(a748)
| c0_1(a748)
| hskp25 ),
inference(copy,[status(thm)],[c_30891]) ).
cnf(c_30000,plain,
( ~ hskp10
| c0_1(a748)
| hskp25 ),
inference(resolve,[status(thm)],[c_29922,c_105]) ).
cnf(c_30892,plain,
( hskp25
| c0_1(a748)
| hskp25 ),
inference(resolve,[status(thm)],[c_30000,c_29907]) ).
cnf(c_30001,plain,
( c0_1(a748)
| hskp25 ),
inference(copy,[status(thm)],[c_30892]) ).
cnf(c_30010,plain,
( ~ hskp10
| hskp25 ),
inference(resolve,[status(thm)],[c_30001,c_103]) ).
cnf(c_30893,plain,
( hskp25
| hskp25 ),
inference(resolve,[status(thm)],[c_30010,c_29907]) ).
cnf(c_30014,plain,
hskp25,
inference(copy,[status(thm)],[c_30893]) ).
cnf(c_30015,plain,
c3_1(a729),
inference(resolve,[status(thm)],[c_30014,c_47]) ).
cnf(c_30016,plain,
c2_1(a729),
inference(resolve,[status(thm)],[c_30014,c_46]) ).
cnf(c_30017,plain,
c0_1(a729),
inference(resolve,[status(thm)],[c_30014,c_45]) ).
cnf(c_30894,plain,
( c1_1(a729)
| c2_1(a730)
| ~ c2_1(a729) ),
inference(resolve,[status(thm)],[c_30015,c_29295]) ).
cnf(c_30035,plain,
( c1_1(a729)
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_30016,c_30894]) ).
cnf(c_30895,plain,
( hskp21
| ~ c2_1(a729)
| ~ c0_1(a729) ),
inference(resolve,[status(thm)],[c_30015,c_238]) ).
cnf(c_30896,plain,
( hskp21
| ~ c2_1(a729) ),
inference(resolve,[status(thm)],[c_30017,c_30895]) ).
cnf(c_30045,plain,
hskp21,
inference(resolve,[status(thm)],[c_30016,c_30896]) ).
cnf(c_30048,plain,
~ c2_1(a793),
inference(resolve,[status(thm)],[c_30045,c_86]) ).
cnf(c_30049,plain,
c3_1(a793),
inference(resolve,[status(thm)],[c_30045,c_53]) ).
cnf(c_30050,plain,
c0_1(a793),
inference(resolve,[status(thm)],[c_30045,c_52]) ).
cnf(c_30897,plain,
( c2_1(a793)
| ~ c2_1(a730)
| ~ c0_1(a793) ),
inference(resolve,[status(thm)],[c_30049,c_29296]) ).
cnf(c_30898,plain,
( c2_1(a793)
| ~ c2_1(a730) ),
inference(resolve,[status(thm)],[c_30050,c_30897]) ).
cnf(c_30209,plain,
~ c2_1(a730),
inference(resolve,[status(thm)],[c_30048,c_30898]) ).
cnf(c_30216,plain,
c1_1(a729),
inference(resolve,[status(thm)],[c_30209,c_30035]) ).
cnf(c_30231,plain,
hskp2,
inference(resolve,[status(thm)],[c_30209,c_29358]) ).
cnf(c_30232,plain,
( c2_1(A)
| c0_1(A)
| ~ c3_1(A) ),
inference(resolve,[status(thm)],[c_30209,c_29357]) ).
cnf(c_30233,plain,
( hskp16
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_30209,c_29354]) ).
cnf(c_30236,plain,
( c1_1(A)
| ~ c3_1(A)
| ~ c2_1(A) ),
inference(resolve,[status(thm)],[c_30209,c_29295]) ).
cnf(c_30264,plain,
( hskp8
| c2_1(a732)
| c0_1(a732)
| c0_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_30231,c_18031]) ).
cnf(c_30271,plain,
~ c2_1(a732),
inference(resolve,[status(thm)],[c_30231,c_119]) ).
cnf(c_30272,plain,
~ c0_1(a732),
inference(resolve,[status(thm)],[c_30231,c_118]) ).
cnf(c_30899,plain,
( hskp8
| c2_1(a732)
| c0_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_30272,c_30264]) ).
cnf(c_30276,plain,
( hskp8
| c0_1(a777)
| hskp27 ),
inference(resolve,[status(thm)],[c_30271,c_30899]) ).
cnf(c_30900,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c1_1(A)
| ~ c0_1(A)
| ~ c3_1(a729)
| ~ c0_1(a729) ),
inference(resolve,[status(thm)],[c_30216,c_210]) ).
cnf(c_30901,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c1_1(A)
| ~ c0_1(A)
| ~ c3_1(a729) ),
inference(resolve,[status(thm)],[c_30017,c_30900]) ).
cnf(c_30287,plain,
( c3_1(B)
| c1_1(B)
| c0_1(B)
| c2_1(A)
| ~ c1_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_30015,c_30901]) ).
cnf(c_30902,plain,
( c3_1(B)
| c1_1(B)
| c3_1(A)
| c2_1(A)
| ~ c2_1(B)
| ~ c0_1(A)
| ~ c2_1(a729)
| ~ c0_1(a729) ),
inference(resolve,[status(thm)],[c_30216,c_208]) ).
cnf(c_30903,plain,
( c3_1(B)
| c1_1(B)
| c3_1(A)
| c2_1(A)
| ~ c2_1(B)
| ~ c0_1(A)
| ~ c2_1(a729) ),
inference(resolve,[status(thm)],[c_30017,c_30902]) ).
cnf(c_30288,plain,
( c3_1(B)
| c1_1(B)
| c3_1(A)
| c2_1(A)
| ~ c2_1(B)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_30016,c_30903]) ).
cnf(c_30307,plain,
( ~ hskp19
| hskp8
| hskp27 ),
inference(resolve,[status(thm)],[c_30276,c_89]) ).
cnf(c_30904,plain,
( hskp27
| hskp8
| hskp27 ),
inference(resolve,[status(thm)],[c_30307,c_14429]) ).
cnf(c_30308,plain,
( hskp8
| hskp27 ),
inference(copy,[status(thm)],[c_30904]) ).
cnf(c_30309,plain,
( c3_1(a744)
| hskp27 ),
inference(resolve,[status(thm)],[c_30308,c_69]) ).
cnf(c_30341,plain,
( hskp27
| c2_1(a744)
| c0_1(a744) ),
inference(resolve,[status(thm)],[c_30232,c_30309]) ).
cnf(c_30349,plain,
( hskp27
| c1_1(a744)
| ~ c2_1(a744) ),
inference(resolve,[status(thm)],[c_30236,c_30309]) ).
cnf(c_30905,plain,
( hskp27
| c0_1(a744)
| hskp27
| c1_1(a744) ),
inference(resolve,[status(thm)],[c_30349,c_30341]) ).
cnf(c_30351,plain,
( c0_1(a744)
| hskp27
| c1_1(a744) ),
inference(copy,[status(thm)],[c_30905]) ).
cnf(c_30353,plain,
( ~ hskp8
| c0_1(a744)
| hskp27 ),
inference(resolve,[status(thm)],[c_30351,c_109]) ).
cnf(c_30906,plain,
( hskp27
| c0_1(a744)
| hskp27 ),
inference(resolve,[status(thm)],[c_30353,c_30308]) ).
cnf(c_30355,plain,
( c0_1(a744)
| hskp27 ),
inference(copy,[status(thm)],[c_30906]) ).
cnf(c_30356,plain,
( ~ hskp8
| hskp27 ),
inference(resolve,[status(thm)],[c_30355,c_108]) ).
cnf(c_30907,plain,
( hskp27
| hskp27 ),
inference(resolve,[status(thm)],[c_30356,c_30308]) ).
cnf(c_30358,plain,
hskp27,
inference(copy,[status(thm)],[c_30907]) ).
cnf(c_30359,plain,
c2_1(a750),
inference(resolve,[status(thm)],[c_30358,c_41]) ).
cnf(c_30360,plain,
c1_1(a750),
inference(resolve,[status(thm)],[c_30358,c_40]) ).
cnf(c_30361,plain,
c0_1(a750),
inference(resolve,[status(thm)],[c_30358,c_39]) ).
cnf(c_30908,plain,
( hskp1
| c3_1(a750)
| ~ c0_1(a750)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_30360,c_214]) ).
cnf(c_30364,plain,
( hskp1
| c3_1(a750)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_30361,c_30908]) ).
cnf(c_30909,plain,
( hskp16
| ~ c2_1(a729)
| ~ c0_1(a729) ),
inference(resolve,[status(thm)],[c_30233,c_30015]) ).
cnf(c_30910,plain,
( hskp16
| ~ c2_1(a729) ),
inference(resolve,[status(thm)],[c_30017,c_30909]) ).
cnf(c_30435,plain,
hskp16,
inference(resolve,[status(thm)],[c_30016,c_30910]) ).
cnf(c_30436,plain,
~ c3_1(a764),
inference(resolve,[status(thm)],[c_30435,c_94]) ).
cnf(c_30437,plain,
c2_1(a764),
inference(resolve,[status(thm)],[c_30435,c_60]) ).
cnf(c_30438,plain,
c0_1(a764),
inference(resolve,[status(thm)],[c_30435,c_59]) ).
cnf(c_30911,plain,
( hskp1
| c3_1(a750)
| ~ c2_1(a729)
| ~ c0_1(a729) ),
inference(resolve,[status(thm)],[c_30364,c_30015]) ).
cnf(c_30912,plain,
( hskp1
| c3_1(a750)
| ~ c2_1(a729) ),
inference(resolve,[status(thm)],[c_30017,c_30911]) ).
cnf(c_30443,plain,
( hskp1
| c3_1(a750) ),
inference(resolve,[status(thm)],[c_30016,c_30912]) ).
cnf(c_30913,plain,
( c3_1(a764)
| c1_1(a764)
| c3_1(A)
| c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_30288,c_30437]) ).
cnf(c_30450,plain,
( c1_1(a764)
| c3_1(A)
| c2_1(A)
| ~ c0_1(A) ),
inference(resolve,[status(thm)],[c_30436,c_30913]) ).
cnf(c_30451,plain,
( hskp13
| hskp23
| c1_1(a764)
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30450,c_190]) ).
cnf(c_30914,plain,
( hskp1
| c3_1(a764)
| ~ c0_1(a764)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp13
| hskp23
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30451,c_214]) ).
cnf(c_30915,plain,
( hskp1
| c3_1(a764)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp13
| hskp23
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30438,c_30914]) ).
cnf(c_30453,plain,
( hskp1
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp13
| hskp23
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30436,c_30915]) ).
cnf(c_30916,plain,
( hskp1
| hskp1
| ~ c2_1(a750)
| ~ c0_1(a750)
| hskp13
| hskp23
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30453,c_30443]) ).
cnf(c_30917,plain,
( hskp1
| ~ c2_1(a750)
| ~ c0_1(a750)
| hskp13
| hskp23
| c3_1(a802)
| c2_1(a802) ),
inference(copy,[status(thm)],[c_30916]) ).
cnf(c_30918,plain,
( hskp1
| ~ c2_1(a750)
| hskp13
| hskp23
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30361,c_30917]) ).
cnf(c_30456,plain,
( hskp1
| hskp13
| hskp23
| c3_1(a802)
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30359,c_30918]) ).
cnf(c_30471,plain,
( ~ hskp24
| hskp1
| hskp13
| hskp23
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30456,c_82]) ).
cnf(c_30919,plain,
( hskp13
| hskp23
| hskp1
| hskp13
| hskp23
| c2_1(a802) ),
inference(resolve,[status(thm)],[c_30471,c_32]) ).
cnf(c_30920,plain,
( hskp13
| hskp1
| hskp13
| hskp23
| c2_1(a802) ),
inference(copy,[status(thm)],[c_30919]) ).
cnf(c_30473,plain,
( hskp1
| hskp13
| hskp23
| c2_1(a802) ),
inference(copy,[status(thm)],[c_30920]) ).
cnf(c_30475,plain,
( ~ hskp24
| hskp1
| hskp13
| hskp23 ),
inference(resolve,[status(thm)],[c_30473,c_81]) ).
cnf(c_30921,plain,
( hskp13
| hskp23
| hskp1
| hskp13
| hskp23 ),
inference(resolve,[status(thm)],[c_30475,c_32]) ).
cnf(c_30922,plain,
( hskp13
| hskp1
| hskp13
| hskp23 ),
inference(copy,[status(thm)],[c_30921]) ).
cnf(c_30476,plain,
( hskp1
| hskp13
| hskp23 ),
inference(copy,[status(thm)],[c_30922]) ).
cnf(c_30478,plain,
( c1_1(a798)
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30476,c_50]) ).
cnf(c_30479,plain,
( c0_1(a798)
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30476,c_49]) ).
cnf(c_30923,plain,
( hskp1
| c3_1(a798)
| ~ c0_1(a798)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30478,c_214]) ).
cnf(c_30487,plain,
( c3_1(a798)
| ~ c0_1(a798)
| ~ c3_1(A)
| ~ c2_1(A)
| ~ c0_1(A)
| hskp1
| hskp13 ),
inference(copy,[status(thm)],[c_30923]) ).
cnf(c_30924,plain,
( hskp1
| c3_1(a798)
| ~ c0_1(a798)
| ~ c2_1(a750)
| ~ c0_1(a750)
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30487,c_30443]) ).
cnf(c_30925,plain,
( c3_1(a798)
| ~ c0_1(a798)
| ~ c2_1(a750)
| ~ c0_1(a750)
| hskp1
| hskp13 ),
inference(copy,[status(thm)],[c_30924]) ).
cnf(c_30926,plain,
( c3_1(a798)
| ~ c0_1(a798)
| ~ c2_1(a750)
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30361,c_30925]) ).
cnf(c_30524,plain,
( c3_1(a798)
| ~ c0_1(a798)
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30359,c_30926]) ).
cnf(c_30927,plain,
( hskp1
| hskp13
| c3_1(a798)
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30524,c_30479]) ).
cnf(c_30928,plain,
( hskp1
| c3_1(a798)
| hskp1
| hskp13 ),
inference(copy,[status(thm)],[c_30927]) ).
cnf(c_30525,plain,
( c3_1(a798)
| hskp1
| hskp13 ),
inference(copy,[status(thm)],[c_30928]) ).
cnf(c_30526,plain,
( ~ hskp23
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30525,c_83]) ).
cnf(c_30929,plain,
( hskp1
| hskp13
| hskp1
| hskp13 ),
inference(resolve,[status(thm)],[c_30526,c_30476]) ).
cnf(c_30930,plain,
( hskp1
| hskp1
| hskp13 ),
inference(copy,[status(thm)],[c_30929]) ).
cnf(c_30527,plain,
( hskp1
| hskp13 ),
inference(copy,[status(thm)],[c_30930]) ).
cnf(c_30528,plain,
( c3_1(a759)
| hskp1 ),
inference(resolve,[status(thm)],[c_30527,c_65]) ).
cnf(c_30529,plain,
( c2_1(a759)
| hskp1 ),
inference(resolve,[status(thm)],[c_30527,c_64]) ).
cnf(c_30530,plain,
( c1_1(a759)
| ~ c2_1(a759)
| hskp1 ),
inference(resolve,[status(thm)],[c_30528,c_30236]) ).
cnf(c_30931,plain,
( hskp1
| c1_1(a759)
| hskp1 ),
inference(resolve,[status(thm)],[c_30530,c_30529]) ).
cnf(c_30540,plain,
( c1_1(a759)
| hskp1 ),
inference(copy,[status(thm)],[c_30931]) ).
cnf(c_30541,plain,
( ~ hskp13
| hskp1 ),
inference(resolve,[status(thm)],[c_30540,c_98]) ).
cnf(c_30932,plain,
( hskp1
| hskp1 ),
inference(resolve,[status(thm)],[c_30541,c_30527]) ).
cnf(c_30542,plain,
hskp1,
inference(copy,[status(thm)],[c_30932]) ).
cnf(c_30543,plain,
~ c2_1(a731),
inference(resolve,[status(thm)],[c_30542,c_121]) ).
cnf(c_30544,plain,
c3_1(a731),
inference(resolve,[status(thm)],[c_30542,c_78]) ).
cnf(c_30545,plain,
c1_1(a731),
inference(resolve,[status(thm)],[c_30542,c_77]) ).
cnf(c_30933,plain,
( c2_1(a731)
| c0_1(a731) ),
inference(resolve,[status(thm)],[c_30544,c_30232]) ).
cnf(c_30546,plain,
c0_1(a731),
inference(resolve,[status(thm)],[c_30543,c_30933]) ).
cnf(c_30934,plain,
( c3_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a731)
| ~ c0_1(a731) ),
inference(resolve,[status(thm)],[c_30545,c_30287]) ).
cnf(c_30935,plain,
( c3_1(A)
| c1_1(A)
| c0_1(A)
| c2_1(a731) ),
inference(resolve,[status(thm)],[c_30546,c_30934]) ).
cnf(c_30547,plain,
( c3_1(A)
| c1_1(A)
| c0_1(A) ),
inference(resolve,[status(thm)],[c_30543,c_30935]) ).
cnf(c_30936,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| c2_1(a731)
| ~ c3_1(A)
| ~ c3_1(a731) ),
inference(resolve,[status(thm)],[c_30545,c_221]) ).
cnf(c_30937,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| c2_1(a731)
| ~ c3_1(A) ),
inference(resolve,[status(thm)],[c_30544,c_30936]) ).
cnf(c_30550,plain,
( hskp11
| c2_1(A)
| c1_1(A)
| ~ c3_1(A) ),
inference(resolve,[status(thm)],[c_30543,c_30937]) ).
cnf(c_30559,plain,
( ~ hskp11
| c3_1(a749)
| c0_1(a749) ),
inference(resolve,[status(thm)],[c_30547,c_101]) ).
cnf(c_30938,plain,
( hskp11
| c2_1(a730)
| c1_1(a730) ),
inference(resolve,[status(thm)],[c_30550,c_14361]) ).
cnf(c_30939,plain,
( hskp11
| c2_1(a730) ),
inference(resolve,[status(thm)],[c_14360,c_30938]) ).
cnf(c_30576,plain,
hskp11,
inference(resolve,[status(thm)],[c_30209,c_30939]) ).
cnf(c_30577,plain,
( c3_1(a749)
| c0_1(a749) ),
inference(resolve,[status(thm)],[c_30576,c_30559]) ).
cnf(c_30578,plain,
~ c3_1(a749),
inference(resolve,[status(thm)],[c_30576,c_102]) ).
cnf(c_30580,plain,
~ c0_1(a749),
inference(resolve,[status(thm)],[c_30576,c_100]) ).
cnf(c_30940,plain,
c3_1(a749),
inference(resolve,[status(thm)],[c_30580,c_30577]) ).
cnf(c_30581,plain,
$false,
inference(resolve,[status(thm)],[c_30578,c_30940]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN451-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 17:49:15 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3859300 was started by sandbox on n010,
% 0.10/0.36 % Sat Sep 26 17:49:15 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 156.54/21.15
% 156.54/21.15 % given #500 (T,wt=7): 1288 c0_1(a732) | hskp4 | hskp5 | hskp27 | hskp11 | -hskp2. [resolve(826,d,119,a)].
% 156.54/21.15
% 156.54/21.15 % given #1000 (T,wt=7): 3152 hskp27 | hskp0 | hskp11 | -c2_1(a737) | hskp16 | hskp22. [resolve(1897,e,1885,d),merge(g),merge(h),merge(i)].
% 156.54/21.15
% 156.54/21.15 % given #1500 (T,wt=9): 5363 hskp25 | hskp13 | hskp5 | -c0_1(a798) | c3_1(a798) | hskp18 | hskp11. [resolve(5358,d,240,b)].
% 156.54/21.15
% 156.54/21.15 % given #2000 (T,wt=8): 7581 hskp25 | hskp13 | hskp5 | hskp11 | c0_1(a775) | c2_1(a775). [resolve(7580,g,5444,d),merge(g),merge(h),merge(i),merge(j)].
% 156.54/21.15
% 156.54/21.15 % given #2500 (T,wt=6): 10102 hskp0 | hskp27 | hskp16 | c2_1(a749) | hskp28. [resolve(10100,b,676,f),merge(e),merge(f),merge(h)].
% 156.54/21.15
% 156.54/21.15 % given #3000 (T,wt=10): 12539 c0_1(a744) | c2_1(a744) | c0_1(a749) | hskp2 | hskp0 | hskp9 | -hskp11. [resolve(5597,d,102,a)].
% 156.54/21.15
% 156.54/21.15 % given #3500 (T,wt=6): 14778 hskp2 | hskp1 | hskp4 | hskp28 | hskp11 | -hskp7. [resolve(14601,a,110,a)].
% 156.54/21.15
% 156.54/21.15 % given #4000 (T,wt=6): 16349 hskp5 | hskp16 | hskp13 | hskp11 | hskp3 | -hskp18. [resolve(16348,e,91,a)].
% 156.54/21.15
% 156.54/21.15 % given #4500 (T,wt=10): 18228 hskp27 | c0_1(a777) | c0_1(a732) | c2_1(a732) | hskp8 | hskp1 | hskp17. [resolve(18031,f,15279,c),merge(f)].
% 156.54/21.15
% 156.54/21.15 % given #5000 (T,wt=7): 20282 c0_1(a748) | hskp25 | hskp27 | hskp13 | hskp9 | -hskp10. [resolve(20273,b,105,a)].
% 156.54/21.15
% 156.54/21.15 % given #5500 (T,wt=8): 22014 hskp27 | hskp21 | hskp12 | hskp7 | c0_1(a744) | hskp26 | hskp6. [resolve(22013,h,21584,c),merge(h),merge(i)].
% 156.54/21.15
% 156.54/21.15 % given #6000 (T,wt=7): 23626 hskp27 | hskp25 | hskp16 | c0_1(a775) | hskp17 | -hskp18. [resolve(23617,e,91,a)].
% 156.54/21.15
% 156.54/21.15 % given #6500 (T,wt=11): 25301 hskp27 | c0_1(a777) | c0_1(a779) | hskp8 | hskp6 | hskp4 | hskp1 | hskp2 | -hskp20. [resolve(18366,g,87,a)].
% 156.54/21.15
% 156.54/21.15 % given #7000 (T,wt=7): 26828 hskp5 | hskp11 | c2_1(a784) | c0_1(a738) | -hskp6. [resolve(26820,e,112,a)].
% 156.54/21.15
% 156.54/21.15 % given #7500 (T,wt=9): 28321 hskp16 | hskp26 | hskp11 | hskp25 | hskp3 | c0_1(a797) | c2_1(a797). [resolve(28319,e,14576,d),merge(h)].
% 156.54/21.15
% 156.54/21.15 % given #8000 (T,wt=3): 30322 hskp8 | hskp16 | hskp18. [resolve(30320,d,33,c),merge(d),merge(e)].
% 156.54/21.15
% 156.54/21.15 % SZS status Unsatisfiable for theBenchmark
% 156.54/21.15
% 156.54/21.15 % Proof 1 at 16.85 (+ 3.71) seconds.
% 156.54/21.15 % Length of proof is 526.
% 156.54/21.15 % Level of proof is 220.
% 156.54/21.15 % Maximum clause weight is 19.000.
% 156.54/21.15 % Given clauses 8145.
% 156.54/21.15
% 156.54/21.15 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------