%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN432-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 21 02:50:46 EDT 2022
% Result : Satisfiable 10.40s 10.80s
% Output : Saturation 10.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SYN432-1 : TPTP v8.1.0. Released v2.1.0.
% 0.06/0.12 % Command : bliksem %s
% 0.13/0.33 % Computer : n009.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % DateTime : Mon Jul 11 14:31:07 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.43/1.08 *** allocated 10000 integers for termspace/termends
% 0.43/1.08 *** allocated 10000 integers for clauses
% 0.43/1.08 *** allocated 10000 integers for justifications
% 0.43/1.08 Bliksem 1.12
% 0.43/1.08
% 0.43/1.08
% 0.43/1.08 Automatic Strategy Selection
% 0.43/1.08
% 0.43/1.08 Clauses:
% 0.43/1.08 [
% 0.43/1.08 [ ~( hskp29 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp28 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp27 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp26 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp25 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp24 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp23 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp22 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp21 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp20 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp19 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp18 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp17 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp16 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp15 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp14 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp13 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp12 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp11 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp10 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp9 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp8 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp7 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp6 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp5 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp4 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp3 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp2 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp1 ), 'ndr1_0' ],
% 0.43/1.08 [ ~( hskp0 ), 'ndr1_0' ],
% 0.43/1.08 [ hskp5, hskp20, hskp21 ],
% 0.43/1.08 [ hskp6, hskp17, hskp22 ],
% 0.43/1.08 [ hskp28, hskp21, hskp8 ],
% 0.43/1.08 [ ~( hskp29 ), 'c2_1'( a193 ) ],
% 0.43/1.08 [ ~( hskp29 ), 'c3_1'( a193 ) ],
% 0.43/1.08 [ ~( hskp29 ), 'c0_1'( a193 ) ],
% 0.43/1.08 [ ~( hskp28 ), 'c2_1'( a190 ) ],
% 0.43/1.08 [ ~( hskp28 ), 'c0_1'( a190 ) ],
% 0.43/1.08 [ ~( hskp27 ), 'c1_1'( a188 ) ],
% 0.43/1.08 [ ~( hskp27 ), 'c0_1'( a188 ) ],
% 0.43/1.08 [ ~( hskp26 ), 'c3_1'( a187 ) ],
% 0.43/1.08 [ ~( hskp25 ), 'c1_1'( a186 ) ],
% 0.43/1.08 [ ~( hskp24 ), 'c1_1'( a185 ) ],
% 0.43/1.08 [ ~( hskp24 ), 'c3_1'( a185 ) ],
% 0.43/1.08 [ ~( hskp24 ), 'c0_1'( a185 ) ],
% 0.43/1.08 [ ~( hskp23 ), 'c1_1'( a184 ) ],
% 0.43/1.08 [ ~( hskp23 ), 'c2_1'( a184 ) ],
% 0.43/1.08 [ ~( hskp23 ), 'c0_1'( a184 ) ],
% 0.43/1.08 [ ~( hskp22 ), 'c2_1'( a183 ) ],
% 0.43/1.08 [ ~( hskp22 ), 'c0_1'( a183 ) ],
% 0.43/1.08 [ ~( hskp21 ), 'c3_1'( a180 ) ],
% 0.43/1.08 [ ~( hskp20 ), 'c3_1'( a179 ) ],
% 0.43/1.08 [ ~( hskp20 ), 'c2_1'( a179 ) ],
% 0.43/1.08 [ ~( hskp20 ), 'c0_1'( a179 ) ],
% 0.43/1.08 [ ~( hskp19 ), 'c3_1'( a177 ) ],
% 0.43/1.08 [ ~( hskp19 ), 'c1_1'( a177 ) ],
% 0.43/1.08 [ ~( hskp18 ), 'c1_1'( a175 ) ],
% 0.43/1.08 [ ~( hskp18 ), 'c3_1'( a175 ) ],
% 0.43/1.08 [ ~( hskp18 ), 'c2_1'( a175 ) ],
% 0.43/1.08 [ ~( hskp17 ), 'c0_1'( a174 ) ],
% 0.43/1.08 [ ~( hskp17 ), 'c2_1'( a174 ) ],
% 0.43/1.08 [ ~( hskp16 ), 'c1_1'( a171 ) ],
% 0.43/1.08 [ ~( hskp16 ), 'c0_1'( a171 ) ],
% 0.43/1.08 [ ~( hskp15 ), 'c1_1'( a170 ) ],
% 0.43/1.08 [ ~( hskp15 ), 'c0_1'( a170 ) ],
% 0.43/1.08 [ ~( hskp15 ), 'c2_1'( a170 ) ],
% 0.43/1.08 [ ~( hskp14 ), 'c0_1'( a167 ) ],
% 0.43/1.08 [ ~( hskp14 ), 'c3_1'( a167 ) ],
% 0.43/1.08 [ ~( hskp13 ), 'c1_1'( a166 ) ],
% 0.43/1.08 [ ~( hskp13 ), 'c3_1'( a166 ) ],
% 0.43/1.08 [ ~( hskp12 ), 'c2_1'( a164 ) ],
% 0.43/1.08 [ ~( hskp11 ), 'c0_1'( a163 ) ],
% 0.43/1.08 [ ~( hskp11 ), 'c3_1'( a163 ) ],
% 0.43/1.08 [ ~( hskp10 ), 'c2_1'( a162 ) ],
% 0.43/1.08 [ ~( hskp9 ), 'c3_1'( a195 ) ],
% 0.43/1.08 [ ~( hskp9 ), 'c2_1'( a195 ) ],
% 0.43/1.08 [ ~( hskp8 ), 'c3_1'( a192 ) ],
% 0.43/1.08 [ ~( hskp7 ), 'c2_1'( a189 ) ],
% 0.43/1.08 [ ~( hskp7 ), 'c1_1'( a189 ) ],
% 0.43/1.08 [ ~( hskp6 ), 'c0_1'( a181 ) ],
% 0.43/1.08 [ ~( hskp3 ), 'c3_1'( a173 ) ],
% 0.43/1.08 [ ~( hskp2 ), 'c3_1'( a172 ) ],
% 0.43/1.08 [ ~( hskp1 ), 'c3_1'( a169 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a190 ) ), ~( hskp28 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a188 ) ), ~( hskp27 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a187 ) ), ~( hskp26 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a187 ) ), ~( hskp26 ) ],
% 0.43/1.08 [ ~( 'c0_1'( a186 ) ), ~( hskp25 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a186 ) ), ~( hskp25 ) ],
% 0.43/1.08 [ ~( 'c3_1'( a183 ) ), ~( hskp22 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a180 ) ), ~( hskp21 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a180 ) ), ~( hskp21 ) ],
% 0.43/1.08 [ ~( 'c0_1'( a177 ) ), ~( hskp19 ) ],
% 0.43/1.08 [ ~( 'c3_1'( a174 ) ), ~( hskp17 ) ],
% 0.43/1.08 [ ~( 'c3_1'( a171 ) ), ~( hskp16 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a167 ) ), ~( hskp14 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a166 ) ), ~( hskp13 ) ],
% 0.43/1.08 [ ~( 'c0_1'( a164 ) ), ~( hskp12 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a164 ) ), ~( hskp12 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a163 ) ), ~( hskp11 ) ],
% 0.43/1.08 [ ~( 'c0_1'( a162 ) ), ~( hskp10 ) ],
% 0.43/1.08 [ ~( 'c3_1'( a162 ) ), ~( hskp10 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a195 ) ), ~( hskp9 ) ],
% 0.43/1.08 [ ~( 'c0_1'( a192 ) ), ~( hskp8 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a192 ) ), ~( hskp8 ) ],
% 0.43/1.08 [ ~( 'c3_1'( a189 ) ), ~( hskp7 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a181 ) ), ~( hskp6 ) ],
% 0.43/1.08 [ ~( 'c2_1'( a181 ) ), ~( hskp6 ) ],
% 0.43/1.08 [ ~( 'c3_1'( a178 ) ), ~( hskp5 ) ],
% 0.43/1.08 [ ~( 'c0_1'( a178 ) ), ~( hskp5 ) ],
% 0.43/1.08 [ ~( 'c1_1'( a178 ) ), ~( hskp5 ) ],
% 0.73/1.36 [ ~( 'c1_1'( a176 ) ), ~( hskp4 ) ],
% 0.73/1.36 [ ~( 'c3_1'( a176 ) ), ~( hskp4 ) ],
% 0.73/1.36 [ ~( 'c0_1'( a176 ) ), ~( hskp4 ) ],
% 0.73/1.36 [ ~( 'c1_1'( a173 ) ), ~( hskp3 ) ],
% 0.73/1.36 [ ~( 'c2_1'( a173 ) ), ~( hskp3 ) ],
% 0.73/1.36 [ ~( 'c2_1'( a172 ) ), ~( hskp2 ) ],
% 0.73/1.36 [ ~( 'c1_1'( a172 ) ), ~( hskp2 ) ],
% 0.73/1.36 [ ~( 'c1_1'( a169 ) ), ~( hskp1 ) ],
% 0.73/1.36 [ ~( 'c0_1'( a169 ) ), ~( hskp1 ) ],
% 0.73/1.36 [ ~( 'c0_1'( a168 ) ), ~( hskp0 ) ],
% 0.73/1.36 [ ~( 'c2_1'( a168 ) ), ~( hskp0 ) ],
% 0.73/1.36 [ ~( 'c1_1'( a168 ) ), ~( hskp0 ) ],
% 0.73/1.36 [ ~( 'ndr1_0' ), 'c1_1'( X ), 'c2_1'( X ), 'c0_1'( X ), hskp12, hskp11 ]
% 0.73/1.36 ,
% 0.73/1.36 [ ~( 'c3_1'( X ) ), ~( 'ndr1_0' ), 'c2_1'( X ), 'c1_1'( X ), hskp1,
% 0.73/1.36 hskp15 ],
% 0.73/1.36 [ ~( 'c1_1'( X ) ), ~( 'ndr1_0' ), 'c3_1'( X ), 'c0_1'( X ), hskp4,
% 0.73/1.36 hskp19 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), 'c1_1'( X ), 'c3_1'( X ), hskp23,
% 0.73/1.36 hskp24 ],
% 0.73/1.36 [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), 'c3_1'( X ), hskp16
% 0.73/1.36 , hskp2 ],
% 0.73/1.36 [ ~( 'c0_1'( X ) ), ~( 'c1_1'( X ) ), ~( 'ndr1_0' ), 'c3_1'( X ), hskp25
% 0.73/1.36 , hskp26 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'c1_1'( X ) ), ~( 'ndr1_0' ), 'c3_1'( X ), hskp27
% 0.73/1.36 , hskp7 ],
% 0.73/1.36 [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), 'c0_1'( X ), hskp29
% 0.73/1.36 , hskp25 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'c0_1'( X ) ), ~( 'c1_1'( X ) ), ~( 'ndr1_0' ),
% 0.73/1.36 hskp14, hskp0 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), 'c3_1'( X ), 'c1_1'( X ), 'c2_1'( Y )
% 0.73/1.36 , 'c1_1'( Y ), 'c3_1'( Y ), hskp10 ],
% 0.73/1.36 [ ~( 'c0_1'( X ) ), ~( 'ndr1_0' ), ~( 'c1_1'( Y ) ), 'c3_1'( X ), 'c2_1'(
% 0.73/1.36 X ), 'c3_1'( Y ), 'c2_1'( Y ), hskp3 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'c3_1'( X ) ), ~( 'ndr1_0' ), ~( 'c3_1'( Y ) ),
% 0.73/1.36 'c1_1'( X ), 'c2_1'( Y ), 'c0_1'( Y ), hskp17 ],
% 0.73/1.36 [ ~( 'c3_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), ~( 'c0_1'( Y ) ),
% 0.73/1.36 'c1_1'( X ), 'c2_1'( Y ), 'c1_1'( Y ), hskp18 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), ~( 'c3_1'( Y ) ), ~( 'c1_1'( Y ) ),
% 0.73/1.36 'c1_1'( X ), 'c0_1'( X ), 'c0_1'( Y ), hskp9 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), ~( 'c3_1'( Y ) ), ~( 'c0_1'( Y ) ),
% 0.73/1.36 ~( 'c2_1'( Y ) ), 'c3_1'( X ), 'c1_1'( X ), hskp13 ],
% 0.73/1.36 [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'c0_1'( X ) ), ~( 'ndr1_0' ),
% 0.73/1.36 ~( 'c3_1'( Y ) ), ~( 'c1_1'( Y ) ), ~( 'c0_1'( Y ) ), hskp11 ],
% 0.73/1.36 [ ~( 'c2_1'( X ) ), ~( 'ndr1_0' ), ~( 'c1_1'( Y ) ), ~( 'c2_1'( Y ) ),
% 0.73/1.36 ~( 'c1_1'( Z ) ), 'c0_1'( X ), 'c3_1'( X ), 'c3_1'( Y ), 'c2_1'( Z ),
% 0.73/1.36 'c3_1'( Z ) ]
% 0.73/1.36 ] .
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 percentage equality = 0.000000, percentage horn = 0.864286
% 0.73/1.36 This a non-horn, non-equality problem
% 0.73/1.36
% 0.73/1.36
% 0.73/1.36 Options Used:
% 0.73/1.36
% 0.73/1.36 useres = 1
% 0.73/1.36 useparamod = 0
% 0.73/1.36 useeqrefl = 0
% 0.73/1.36 useeqfact = 0
% 0.73/1.36 usefactor = 1
% 0.73/1.36 usesimpsplitting = 0
% 0.73/1.36 usesimpdemod = 0
% 0.73/1.36 usesimpres = 3
% 0.73/1.36
% 0.73/1.36 resimpinuse = 1000
% 0.73/1.36 resimpclauses = 20000
% 0.73/1.36 substype = standard
% 0.73/1.36 backwardsubs = 1
% 0.73/1.36 selectoldest = 5
% 0.73/1.36
% 0.73/1.36 litorderings [0] = split
% 0.73/1.36 litorderings [1] = liftord
% 0.73/1.36
% 0.73/1.36 termordering = none
% 0.73/1.36
% 0.73/1.36 litapriori = 1
% 0.73/1.36 termapriori = 0
% 0.73/1.36 litaposteriori = 0
% 0.73/1.36 termaposteriori = 0
% 0.73/1.36 demodaposteriori = 0
% 0.73/1.36 ordereqreflfact = 0
% 0.73/1.36
% 0.73/1.36 litselect = none
% 0.73/1.36
% 0.73/1.36 maxweight = 15
% 0.73/1.36 maxdepth = 30000
% 0.73/1.36 maxlength = 115
% 0.73/1.36 maxnrvars = 195
% 0.73/1.36 excuselevel = 1
% 0.73/1.36 increasemaxweight = 1
% 0.73/1.36
% 0.73/1.36 maxselected = 10000000
% 0.73/1.36 maxnrclauses = 10000000
% 0.73/1.36
% 0.73/1.36 showgenerated = 0
% 0.73/1.36 showkept = 0
% 0.73/1.36 showselected = 0
% 0.73/1.36 showdeleted = 0
% 0.73/1.36 showresimp = 1
% 0.73/1.36 showstatus = 2000
% 0.73/1.36
% 0.73/1.36 prologoutput = 1
% 0.73/1.36 nrgoals = 5000000
% 0.73/1.36 totalproof = 1
% 0.73/1.36
% 0.73/1.36 Symbols occurring in the translation:
% 0.73/1.36
% 0.73/1.36 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.73/1.36 . [1, 2] (w:1, o:82, a:1, s:1, b:0),
% 0.73/1.36 ! [4, 1] (w:0, o:73, a:1, s:1, b:0),
% 0.73/1.36 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.36 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.73/1.36 hskp29 [39, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.73/1.36 'ndr1_0' [40, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.73/1.36 hskp28 [41, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.73/1.36 hskp27 [42, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.73/1.36 hskp26 [43, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.73/1.36 hskp25 [44, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.73/1.36 hskp24 [45, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.73/1.36 hskp23 [46, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.73/1.36 hskp22 [47, 0] (w:1, o:23, a:1, s:1, b:0),
% 5.29/5.70 hskp21 [48, 0] (w:1, o:22, a:1, s:1, b:0),
% 5.29/5.70 hskp20 [49, 0] (w:1, o:21, a:1, s:1, b:0),
% 5.29/5.70 hskp19 [50, 0] (w:1, o:19, a:1, s:1, b:0),
% 5.29/5.70 hskp18 [51, 0] (w:1, o:18, a:1, s:1, b:0),
% 5.29/5.70 hskp17 [52, 0] (w:1, o:17, a:1, s:1, b:0),
% 5.29/5.70 hskp16 [53, 0] (w:1, o:16, a:1, s:1, b:0),
% 5.29/5.70 hskp15 [54, 0] (w:1, o:15, a:1, s:1, b:0),
% 5.29/5.70 hskp14 [55, 0] (w:1, o:14, a:1, s:1, b:0),
% 5.29/5.70 hskp13 [56, 0] (w:1, o:13, a:1, s:1, b:0),
% 5.29/5.70 hskp12 [57, 0] (w:1, o:12, a:1, s:1, b:0),
% 5.29/5.70 hskp11 [58, 0] (w:1, o:11, a:1, s:1, b:0),
% 5.29/5.70 hskp10 [59, 0] (w:1, o:10, a:1, s:1, b:0),
% 5.29/5.70 hskp9 [60, 0] (w:1, o:39, a:1, s:1, b:0),
% 5.29/5.70 hskp8 [61, 0] (w:1, o:38, a:1, s:1, b:0),
% 5.29/5.70 hskp7 [62, 0] (w:1, o:37, a:1, s:1, b:0),
% 5.29/5.70 hskp6 [63, 0] (w:1, o:36, a:1, s:1, b:0),
% 5.29/5.70 hskp5 [64, 0] (w:1, o:35, a:1, s:1, b:0),
% 5.29/5.70 hskp4 [65, 0] (w:1, o:34, a:1, s:1, b:0),
% 5.29/5.70 hskp3 [66, 0] (w:1, o:33, a:1, s:1, b:0),
% 5.29/5.70 hskp2 [67, 0] (w:1, o:32, a:1, s:1, b:0),
% 5.29/5.70 hskp1 [68, 0] (w:1, o:20, a:1, s:1, b:0),
% 5.29/5.70 hskp0 [69, 0] (w:1, o:9, a:1, s:1, b:0),
% 5.29/5.70 a193 [70, 0] (w:1, o:67, a:1, s:1, b:0),
% 5.29/5.70 'c2_1' [71, 1] (w:1, o:79, a:1, s:1, b:0),
% 5.29/5.70 'c3_1' [72, 1] (w:1, o:80, a:1, s:1, b:0),
% 5.29/5.70 'c0_1' [73, 1] (w:1, o:81, a:1, s:1, b:0),
% 5.29/5.70 a190 [74, 0] (w:1, o:68, a:1, s:1, b:0),
% 5.29/5.70 a188 [75, 0] (w:1, o:62, a:1, s:1, b:0),
% 5.29/5.70 'c1_1' [76, 1] (w:1, o:78, a:1, s:1, b:0),
% 5.29/5.70 a187 [77, 0] (w:1, o:61, a:1, s:1, b:0),
% 5.29/5.70 a186 [78, 0] (w:1, o:60, a:1, s:1, b:0),
% 5.29/5.70 a185 [79, 0] (w:1, o:59, a:1, s:1, b:0),
% 5.29/5.70 a184 [80, 0] (w:1, o:58, a:1, s:1, b:0),
% 5.29/5.70 a183 [81, 0] (w:1, o:57, a:1, s:1, b:0),
% 5.29/5.70 a180 [82, 0] (w:1, o:63, a:1, s:1, b:0),
% 5.29/5.70 a179 [83, 0] (w:1, o:48, a:1, s:1, b:0),
% 5.29/5.70 a177 [84, 0] (w:1, o:50, a:1, s:1, b:0),
% 5.29/5.70 a175 [85, 0] (w:1, o:54, a:1, s:1, b:0),
% 5.29/5.70 a174 [86, 0] (w:1, o:53, a:1, s:1, b:0),
% 5.29/5.70 a171 [87, 0] (w:1, o:56, a:1, s:1, b:0),
% 5.29/5.70 a170 [88, 0] (w:1, o:55, a:1, s:1, b:0),
% 5.29/5.70 a167 [89, 0] (w:1, o:41, a:1, s:1, b:0),
% 5.29/5.70 a166 [90, 0] (w:1, o:40, a:1, s:1, b:0),
% 5.29/5.70 a164 [91, 0] (w:1, o:44, a:1, s:1, b:0),
% 5.29/5.70 a163 [92, 0] (w:1, o:43, a:1, s:1, b:0),
% 5.29/5.70 a162 [93, 0] (w:1, o:42, a:1, s:1, b:0),
% 5.29/5.70 a195 [94, 0] (w:1, o:69, a:1, s:1, b:0),
% 5.29/5.70 a192 [95, 0] (w:1, o:66, a:1, s:1, b:0),
% 5.29/5.70 a189 [96, 0] (w:1, o:64, a:1, s:1, b:0),
% 5.29/5.70 a181 [97, 0] (w:1, o:65, a:1, s:1, b:0),
% 5.29/5.70 a173 [98, 0] (w:1, o:52, a:1, s:1, b:0),
% 5.29/5.70 a172 [99, 0] (w:1, o:51, a:1, s:1, b:0),
% 5.29/5.70 a169 [100, 0] (w:1, o:46, a:1, s:1, b:0),
% 5.29/5.70 a178 [101, 0] (w:1, o:47, a:1, s:1, b:0),
% 5.29/5.70 a176 [102, 0] (w:1, o:49, a:1, s:1, b:0),
% 5.29/5.70 a168 [103, 0] (w:1, o:45, a:1, s:1, b:0).
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 Starting Search:
% 5.29/5.70
% 5.29/5.70 Resimplifying inuse:
% 5.29/5.70 Done
% 5.29/5.70
% 5.29/5.70 Failed to find proof!
% 5.29/5.70 maxweight = 15
% 5.29/5.70 maxnrclauses = 10000000
% 5.29/5.70 Generated: 1512
% 5.29/5.70 Kept: 300
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 The strategy used was not complete!
% 5.29/5.70
% 5.29/5.70 Increased maxweight to 16
% 5.29/5.70
% 5.29/5.70 Starting Search:
% 5.29/5.70
% 5.29/5.70 Resimplifying inuse:
% 5.29/5.70 Done
% 5.29/5.70
% 5.29/5.70 Failed to find proof!
% 5.29/5.70 maxweight = 16
% 5.29/5.70 maxnrclauses = 10000000
% 5.29/5.70 Generated: 1985
% 5.29/5.70 Kept: 321
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 The strategy used was not complete!
% 5.29/5.70
% 5.29/5.70 Increased maxweight to 17
% 5.29/5.70
% 5.29/5.70 Starting Search:
% 5.29/5.70
% 5.29/5.70 Resimplifying inuse:
% 5.29/5.70 Done
% 5.29/5.70
% 5.29/5.70 Failed to find proof!
% 5.29/5.70 maxweight = 17
% 5.29/5.70 maxnrclauses = 10000000
% 5.29/5.70 Generated: 2450
% 5.29/5.70 Kept: 341
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 The strategy used was not complete!
% 5.29/5.70
% 5.29/5.70 Increased maxweight to 18
% 5.29/5.70
% 5.29/5.70 Starting Search:
% 5.29/5.70
% 5.29/5.70 Resimplifying inuse:
% 5.29/5.70 Done
% 5.29/5.70
% 5.29/5.70 Failed to find proof!
% 5.29/5.70 maxweight = 18
% 5.29/5.70 maxnrclauses = 10000000
% 5.29/5.70 Generated: 3910
% 5.29/5.70 Kept: 394
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 The strategy used was not complete!
% 5.29/5.70
% 5.29/5.70 Increased maxweight to 19
% 5.29/5.70
% 5.29/5.70 Starting Search:
% 5.29/5.70
% 5.29/5.70 Resimplifying inuse:
% 5.29/5.70 Done
% 5.29/5.70
% 5.29/5.70 Failed to find proof!
% 5.29/5.70 maxweight = 19
% 5.29/5.70 maxnrclauses = 10000000
% 5.29/5.70 Generated: 4232
% 5.29/5.70 Kept: 411
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 The strategy used was not complete!
% 5.29/5.70
% 5.29/5.70 Increased maxweight to 20
% 5.29/5.70
% 5.29/5.70 Starting Search:
% 5.29/5.70
% 5.29/5.70 Resimplifying inuse:
% 5.29/5.70 Done
% 5.29/5.70
% 5.29/5.70 Failed to find proof!
% 5.29/5.70 maxweight = 20
% 5.29/5.70 maxnrclauses = 10000000
% 5.29/5.70 Generated: 6003
% 5.29/5.70 Kept: 452
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 The strategy used was not complete!
% 5.29/5.70
% 5.29/5.70 Increased maxweight to 21
% 5.29/5.70
% 5.29/5.70 Starting Search:
% 5.29/5.70
% 5.29/5.70 Resimplifying inuse:
% 5.29/5.70 Done
% 5.29/5.70
% 5.29/5.70 Failed to find proof!
% 5.29/5.70 maxweight = 21
% 5.29/5.70 maxnrclauses = 10000000
% 5.29/5.70 Generated: 7463
% 5.29/5.70 Kept: 466
% 5.29/5.70
% 5.29/5.70
% 5.29/5.70 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 22
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 22
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 9349
% 10.40/10.80 Kept: 489
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 23
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 23
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 9593
% 10.40/10.80 Kept: 498
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 24
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 24
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 10256
% 10.40/10.80 Kept: 509
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 25
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 25
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 11694
% 10.40/10.80 Kept: 525
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 26
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 26
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 14619
% 10.40/10.80 Kept: 545
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 27
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 27
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 16253
% 10.40/10.80 Kept: 560
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 28
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 28
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 17301
% 10.40/10.80 Kept: 568
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 29
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 29
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 18028
% 10.40/10.80 Kept: 571
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 30
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 30
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 19771
% 10.40/10.80 Kept: 580
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 31
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 31
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 22508
% 10.40/10.80 Kept: 592
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 32
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 32
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 23818
% 10.40/10.80 Kept: 596
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 33
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 33
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 24966
% 10.40/10.80 Kept: 602
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 34
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 34
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25372
% 10.40/10.80 Kept: 605
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 35
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 35
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25392
% 10.40/10.80 Kept: 607
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 36
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 36
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 26213
% 10.40/10.80 Kept: 613
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 37
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 37
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25253
% 10.40/10.80 Kept: 619
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 38
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 38
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 26179
% 10.40/10.80 Kept: 622
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 39
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 39
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 26179
% 10.40/10.80 Kept: 622
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 40
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 40
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 26614
% 10.40/10.80 Kept: 626
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 41
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 41
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25739
% 10.40/10.80 Kept: 627
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 42
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 42
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 43
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 43
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 44
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 44
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 45
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 45
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 46
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 46
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 47
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 47
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 48
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 48
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 49
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 49
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 50
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 50
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 51
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 51
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 52
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 52
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 53
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 53
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 54
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 54
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 55
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80 Failed to find proof!
% 10.40/10.80 maxweight = 55
% 10.40/10.80 maxnrclauses = 10000000
% 10.40/10.80 Generated: 25764
% 10.40/10.80 Kept: 629
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 The strategy used was not complete!
% 10.40/10.80
% 10.40/10.80 Increased maxweight to 56
% 10.40/10.80
% 10.40/10.80 Starting Search:
% 10.40/10.80
% 10.40/10.80 Resimplifying inuse:
% 10.40/10.80 Done
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80
% 10.40/10.80 found a saturation!
% 10.40/10.80 % SZS status Satisfiable
% 10.40/10.80 % SZS output start Saturation
% 10.40/10.80
% 10.40/10.80 clause( 626, [ hskp11, hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( a183 ), ~(
% 10.40/10.80 'c1_1'( Y ) ), 'c1_1'( Z ), ~( 'c1_1'( T ) ), 'c2_1'( Y ), ~( 'c2_1'(
% 10.40/10.80 a183 ) ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), hskp10, hskp15, hskp1,
% 10.40/10.80 hskp17, hskp20, hskp12, hskp21, 'c3_1'( Y ), ~( 'c3_1'( Z ) ), ~( 'c3_1'(
% 10.40/10.80 T ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 617, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( a183 )
% 10.40/10.80 , hskp10, hskp15, hskp1, hskp17, hskp20, hskp12, hskp11, hskp21, ~(
% 10.40/10.80 'c2_1'( X ) ), ~( 'c2_1'( Y ) ), ~( 'c2_1'( a183 ) ), ~( 'c1_1'( a185 ) )
% 10.40/10.80 , hskp23, ~( 'c1_1'( Z ) ), 'c2_1'( Z ), 'c3_1'( Z ), ~( 'c3_1'( Y ) ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 558, [ hskp13, hskp9, ~( 'c1_1'( Y ) ), 'c1_1'( Z ), 'c1_1'( X ),
% 10.40/10.80 ~( 'c1_1'( T ) ), hskp11, hskp29, hskp25, ~( 'c2_1'( X ) ), ~( 'c2_1'( Z
% 10.40/10.80 ) ), ~( 'c2_1'( T ) ), hskp3, 'c1_1'( U ), hskp12, 'c2_1'( U ), 'c2_1'(
% 10.40/10.80 Y ), hskp1, hskp15, 'c3_1'( X ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 559, [ hskp13, hskp9, ~( 'c1_1'( Y ) ), 'c1_1'( Z ), 'c1_1'( X ),
% 10.40/10.80 ~( 'c1_1'( T ) ), hskp11, hskp29, hskp25, ~( 'c2_1'( X ) ), ~( 'c2_1'( Z
% 10.40/10.80 ) ), ~( 'c2_1'( T ) ), 'c2_1'( U ), 'c2_1'( Y ), hskp3, 'c1_1'( U ),
% 10.40/10.80 hskp12, 'c3_1'( X ), 'c3_1'( U ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 611, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( a183 )
% 10.40/10.80 , ~( 'c1_1'( Z ) ), hskp25, hskp26, ~( 'c2_1'( Y ) ), ~( 'c2_1'( a183 ) )
% 10.40/10.80 , ~( 'c2_1'( X ) ), 'c2_1'( Z ), hskp10, hskp15, hskp1, hskp17, hskp20,
% 10.40/10.80 hskp12, hskp11, hskp21, 'c3_1'( Z ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 613, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( a183 )
% 10.40/10.80 , ~( 'c1_1'( Z ) ), hskp14, hskp0, ~( 'c2_1'( Y ) ), ~( 'c2_1'( a183 ) )
% 10.40/10.80 , ~( 'c2_1'( X ) ), 'c2_1'( Z ), hskp10, hskp15, hskp1, hskp17, hskp20,
% 10.40/10.80 hskp12, hskp11, hskp21, 'c3_1'( Z ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 578, [ hskp17, hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), 'c1_1'(
% 10.40/10.80 X ), ~( 'c1_1'( T ) ), ~( 'c2_1'( X ) ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( T ), hskp12, hskp20, hskp21, ~( 'c2_1'( a190 ) ), hskp13, 'c3_1'(
% 10.40/10.80 Y ), 'c3_1'( T ), ~( 'c3_1'( a190 ) ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 614, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp12, hskp20, hskp21, hskp13, 'c2_1'( X ), ~(
% 10.40/10.80 'c2_1'( Z ) ), ~( 'c2_1'( a190 ) ), ~( 'c2_1'( Y ) ), hskp3, 'c1_1'( T )
% 10.40/10.80 , 'c2_1'( T ), hskp1, hskp15, ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 615, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp12, hskp20, hskp21, hskp13, 'c2_1'( X ), ~(
% 10.40/10.80 'c2_1'( Z ) ), ~( 'c2_1'( a190 ) ), ~( 'c2_1'( Y ) ), 'c2_1'( T ), hskp3
% 10.40/10.80 , 'c1_1'( T ), 'c3_1'( T ), ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 579, [ hskp17, hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), 'c1_1'(
% 10.40/10.80 X ), ~( 'c1_1'( T ) ), ~( 'c2_1'( X ) ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( T ), hskp13, hskp12, hskp20, hskp21, hskp23, ~( 'c2_1'( a185 ) )
% 10.40/10.80 , 'c3_1'( T ), ~( 'c3_1'( Z ) ), 'c3_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 580, [ hskp17, hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), 'c1_1'(
% 10.40/10.80 X ), ~( 'c1_1'( T ) ), ~( 'c2_1'( X ) ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( T ), 'c1_1'( U ), hskp10, 'c2_1'( U ), hskp1, hskp15, 'c3_1'( Y )
% 10.40/10.80 , 'c3_1'( T ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 582, [ hskp17, hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), 'c1_1'(
% 10.40/10.80 X ), ~( 'c1_1'( T ) ), ~( 'c2_1'( X ) ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( T ), 'c2_1'( U ), 'c1_1'( U ), hskp10, 'c3_1'( T ), ~( 'c3_1'( Z
% 10.40/10.80 ) ), 'c3_1'( U ), 'c3_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 560, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( a183 )
% 10.40/10.80 , ~( 'c1_1'( Z ) ), hskp11, hskp29, hskp25, ~( 'c2_1'( a183 ) ), ~(
% 10.40/10.80 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), hskp10, hskp15, hskp1, hskp17, hskp20,
% 10.40/10.80 hskp12, hskp21, ~( 'c3_1'( X ) ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 596, [ hskp11, hskp13, hskp19, hskp4, hskp9, ~( 'c1_1'( X ) ), ~(
% 10.40/10.80 'c1_1'( Y ) ), 'c1_1'( Z ), 'c1_1'( a183 ), ~( 'c2_1'( Z ) ), ~( 'c2_1'(
% 10.40/10.80 X ) ), ~( 'c2_1'( a183 ) ), hskp10, hskp15, hskp1, hskp17, hskp20, hskp12
% 10.40/10.80 , hskp21, ~( 'c3_1'( Y ) ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 628, [ hskp11, hskp25, hskp17, hskp29, hskp13, hskp12, hskp20,
% 10.40/10.80 hskp21, hskp23, hskp3, hskp1, hskp15, 'c1_1'( Z ), ~( 'c1_1'( X ) ), ~(
% 10.40/10.80 'c1_1'( Y ) ), 'c2_1'( Z ), 'c2_1'( Y ), ~( 'c2_1'( a185 ) ), ~( 'c2_1'(
% 10.40/10.80 X ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 608, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp13, hskp12, hskp20, hskp21, hskp23, hskp3,
% 10.40/10.80 'c1_1'( T ), 'c2_1'( X ), ~( 'c2_1'( a185 ) ), 'c2_1'( T ), ~( 'c2_1'( Z
% 10.40/10.80 ) ), ~( 'c2_1'( Y ) ), 'c3_1'( T ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 581, [ hskp17, hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), 'c1_1'(
% 10.40/10.80 X ), ~( 'c1_1'( T ) ), ~( 'c2_1'( X ) ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( T ), hskp10, 'c2_1'( a178 ), hskp20, hskp21, ~( 'c3_1'( Z ) ),
% 10.40/10.80 'c3_1'( Y ), 'c3_1'( T ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 606, [ hskp11, hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), ~(
% 10.40/10.80 'c1_1'( Z ) ), 'c1_1'( T ), ~( 'c1_1'( U ) ), 'c2_1'( Z ), ~( 'c2_1'( Y )
% 10.40/10.80 ), ~( 'c2_1'( T ) ), ~( 'c2_1'( X ) ), ~( 'c3_1'( T ) ), ~( 'c3_1'( U )
% 10.40/10.80 ), 'c3_1'( Z ), 'c3_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 609, [ hskp11, hskp19, hskp17, hskp4, hskp3, 'c1_1'( X ), ~( 'c1_1'(
% 10.40/10.80 Y ) ), ~( 'c1_1'( a183 ) ), hskp10, hskp15, hskp1, hskp20, hskp12, hskp21
% 10.40/10.80 , hskp13, ~( 'c2_1'( X ) ), ~( 'c2_1'( a183 ) ), ~( 'c2_1'( a190 ) ),
% 10.40/10.80 'c2_1'( Y ), ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 573, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp3, hskp22, hskp1, hskp15, hskp12, hskp20,
% 10.40/10.80 hskp21, hskp13, ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ), ~( 'c2_1'( a190 ) ),
% 10.40/10.80 'c2_1'( X ), ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 567, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp3, hskp22, ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( X ), hskp12, hskp20, hskp21, ~( 'c2_1'( a190 ) ), hskp13, 'c3_1'(
% 10.40/10.80 a181 ), ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 624, [ hskp11, hskp25, hskp17, hskp29, hskp3, hskp22, hskp1, hskp15
% 10.40/10.80 , hskp13, hskp12, hskp20, hskp21, hskp23, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X
% 10.40/10.80 ) ), ~( 'c2_1'( a185 ) ), ~( 'c2_1'( X ) ), 'c2_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 526, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp4, hskp19,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 hskp12, hskp20, hskp21, ~( 'c2_1'( a190 ) ), hskp13, 'c3_1'( X ), ~(
% 10.40/10.80 'c3_1'( a190 ) ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 562, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp3, hskp4, hskp19, hskp12, hskp20, hskp21,
% 10.40/10.80 hskp13, 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( a190 ) ), ~( 'c2_1'( Y
% 10.40/10.80 ) ), ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 568, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp3, hskp22, ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( X ), hskp13, hskp12, hskp20, hskp21, hskp23, ~( 'c2_1'( a185 ) )
% 10.40/10.80 , 'c3_1'( a181 ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 586, [ hskp17, hskp11, ~( 'c1_1'( a183 ) ), ~( 'c1_1'( Y ) ),
% 10.40/10.80 'c1_1'( X ), hskp10, hskp15, hskp1, hskp20, hskp12, hskp21, ~( 'c2_1'(
% 10.40/10.80 a183 ) ), ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( a190 ) ), hskp13, ~(
% 10.40/10.80 'c3_1'( a190 ) ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 530, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp4, hskp19,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 hskp13, hskp12, hskp20, hskp21, hskp23, ~( 'c2_1'( a185 ) ), ~( 'c3_1'( Y
% 10.40/10.80 ) ), 'c3_1'( X ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 549, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z )
% 10.40/10.80 , ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y )
% 10.40/10.80 ), hskp12, hskp20, hskp21, ~( 'c2_1'( a190 ) ), hskp13, ~( 'c3_1'( a190
% 10.40/10.80 ) ), 'c3_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 532, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp4, hskp19,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 'c1_1'( T ), hskp10, 'c2_1'( T ), hskp1, hskp15, 'c3_1'( X ), ~( 'c3_1'(
% 10.40/10.80 Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 519, [ hskp11, hskp12, hskp20, hskp21, hskp23, ~( 'c1_1'( a185 ) )
% 10.40/10.80 , ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), ~( 'c2_1'( X ) ), 'c2_1'( Y ),
% 10.40/10.80 hskp13, hskp9, 'c1_1'( Z ), 'c1_1'( T ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( T )
% 10.40/10.80 ), 'c3_1'( T ), ~( 'c3_1'( Z ) ), 'c3_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 535, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp4, hskp19,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 'c2_1'( T ), 'c1_1'( T ), hskp10, 'c3_1'( X ), 'c3_1'( T ), ~( 'c3_1'( Y
% 10.40/10.80 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 622, [ hskp11, hskp25, hskp17, hskp29, hskp3, hskp4, hskp19, hskp13
% 10.40/10.80 , hskp12, hskp20, hskp21, hskp23, ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ),
% 10.40/10.80 'c2_1'( Y ), ~( 'c2_1'( a185 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 512, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( a183 )
% 10.40/10.80 , ~( 'c2_1'( Y ) ), ~( 'c2_1'( a183 ) ), ~( 'c2_1'( X ) ), hskp10, hskp15
% 10.40/10.80 , hskp1, hskp17, hskp20, hskp12, hskp11, hskp21, ~( 'c3_1'( X ) ), ~(
% 10.40/10.80 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 550, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z )
% 10.40/10.80 , ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y )
% 10.40/10.80 ), hskp13, hskp12, hskp20, hskp21, hskp23, ~( 'c2_1'( a185 ) ), 'c3_1'(
% 10.40/10.80 Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 520, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp23, hskp24, hskp3, 'c1_1'( T ), hskp12, hskp1,
% 10.40/10.80 hskp15, 'c2_1'( T ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ), 'c2_1'( X ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 564, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp3, hskp4, hskp19, 'c1_1'( T ), hskp10, hskp1,
% 10.40/10.80 hskp15, 'c2_1'( T ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ), 'c2_1'( X ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 521, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp23, hskp24, hskp3, 'c1_1'( T ), hskp12, 'c2_1'(
% 10.40/10.80 T ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ), 'c2_1'( X ), 'c3_1'( T ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 476, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 hskp3, 'c1_1'( T ), hskp12, 'c2_1'( T ), hskp1, hskp15, ~( 'c3_1'( Z ) )
% 10.40/10.80 ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 551, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z )
% 10.40/10.80 , ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y )
% 10.40/10.80 ), 'c1_1'( T ), hskp10, 'c2_1'( T ), hskp1, hskp15, 'c3_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 566, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp3, hskp4, hskp19, 'c1_1'( T ), hskp10, ~(
% 10.40/10.80 'c2_1'( Z ) ), 'c2_1'( T ), ~( 'c2_1'( Y ) ), 'c2_1'( X ), 'c3_1'( T ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 477, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 'c2_1'( T ), hskp3, 'c1_1'( T ), hskp12, 'c3_1'( T ), ~( 'c3_1'( Z ) ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 554, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z )
% 10.40/10.80 , ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y )
% 10.40/10.80 ), 'c2_1'( T ), 'c1_1'( T ), hskp10, 'c3_1'( T ), 'c3_1'( Y ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 475, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 hskp12, hskp20, hskp21, ~( 'c2_1'( a190 ) ), hskp13, ~( 'c3_1'( a190 ) )
% 10.40/10.80 , ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 597, [ hskp11, hskp13, hskp19, hskp4, hskp9, ~( 'c1_1'( X ) ), ~(
% 10.40/10.80 'c1_1'( Y ) ), 'c1_1'( Z ), 'c1_1'( T ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X )
% 10.40/10.80 ), ~( 'c2_1'( T ) ), hskp3, 'c2_1'( Y ), 'c3_1'( T ), ~( 'c3_1'( Z ) ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 511, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( Z ),
% 10.40/10.80 ~( 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( T ) ),
% 10.40/10.80 hskp14, hskp0, 'c2_1'( T ), ~( 'c3_1'( Y ) ), 'c3_1'( T ), 'c3_1'( Z ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 510, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( Z ),
% 10.40/10.80 ~( 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( T ) ),
% 10.40/10.80 hskp25, hskp26, 'c2_1'( T ), ~( 'c3_1'( Y ) ), 'c3_1'( T ), 'c3_1'( Z ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 583, [ hskp17, hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), 'c1_1'(
% 10.40/10.80 X ), ~( 'c1_1'( T ) ), ~( 'c2_1'( X ) ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ),
% 10.40/10.80 'c2_1'( T ), hskp23, hskp24, 'c3_1'( Y ), 'c3_1'( T ), ~( 'c3_1'( Z ) ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 552, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( a183 ) ), 'c1_1'(
% 10.40/10.80 Y ), ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), ~( 'c2_1'( Y ) ), ~( 'c2_1'(
% 10.40/10.80 a183 ) ), hskp10, hskp15, hskp1, hskp20, hskp12, hskp21, ~( 'c3_1'( Y ) )
% 10.40/10.80 ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 478, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 hskp13, hskp12, hskp20, hskp21, hskp23, ~( 'c2_1'( a185 ) ), ~( 'c3_1'( Y
% 10.40/10.80 ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 601, [ hskp11, hskp17, hskp25, hskp10, hskp29, hskp3, hskp12,
% 10.40/10.80 'c1_1'( Z ), ~( 'c1_1'( T ) ), 'c1_1'( X ), ~( 'c1_1'( Y ) ), hskp1,
% 10.40/10.80 hskp15, 'c2_1'( Z ), ~( 'c2_1'( T ) ), 'c2_1'( Y ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 534, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp4, hskp19,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 hskp10, 'c2_1'( a178 ), hskp20, hskp21, ~( 'c3_1'( Y ) ), 'c3_1'( X ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 480, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 'c1_1'( T ), hskp10, 'c2_1'( T ), hskp1, hskp15, ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 600, [ hskp11, hskp25, hskp17, hskp29, hskp10, 'c1_1'( Y ), ~(
% 10.40/10.80 'c1_1'( Z ) ), 'c1_1'( T ), ~( 'c1_1'( X ) ), hskp3, hskp12, ~( 'c2_1'( X
% 10.40/10.80 ) ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ), 'c2_1'( T ), 'c3_1'( T ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 483, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.80 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.80 'c2_1'( T ), 'c1_1'( T ), hskp10, 'c3_1'( T ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 547, [ hskp13, hskp11, hskp4, hskp19, hskp9, ~( 'c1_1'( X ) ), ~(
% 10.40/10.80 'c1_1'( Y ) ), 'c1_1'( Z ), 'c1_1'( T ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X )
% 10.40/10.80 ), ~( 'c2_1'( T ) ), ~( 'c3_1'( Y ) ), ~( 'c3_1'( Z ) ), 'c3_1'( T ) ]
% 10.40/10.80 )
% 10.40/10.80 .
% 10.40/10.80 clause( 592, [ hskp11, hskp17, hskp25, hskp29, hskp19, hskp10, hskp20,
% 10.40/10.80 hskp21, hskp3, hskp4, hskp9, 'c1_1'( X ), ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z
% 10.40/10.80 ) ), 'c2_1'( Y ), ~( 'c2_1'( X ) ), ~( 'c2_1'( Z ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 565, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.80 ), ~( 'c1_1'( X ) ), hskp3, hskp4, hskp19, hskp10, hskp20, hskp21,
% 10.40/10.80 'c2_1'( a178 ), 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 585, [ hskp17, hskp11, ~( 'c1_1'( a183 ) ), ~( 'c1_1'( Y ) ),
% 10.40/10.80 'c1_1'( X ), hskp10, hskp15, hskp1, hskp20, hskp12, hskp21, ~( 'c2_1'(
% 10.40/10.80 a183 ) ), ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( a178 ) ), ~( 'c3_1'(
% 10.40/10.80 X ) ) ] )
% 10.40/10.80 .
% 10.40/10.80 clause( 553, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z )
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y )
% 10.40/10.81 ), hskp10, 'c2_1'( a178 ), hskp20, hskp21, 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 538, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z )
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp20, hskp21, ~( 'c2_1'( Z ) ), ~( 'c2_1'( a178 ) )
% 10.40/10.81 , ~( 'c2_1'( Y ) ), 'c2_1'( X ), 'c3_1'( Y ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 589, [ hskp11, hskp17, hskp22, hskp25, hskp10, hskp29, hskp3, hskp1
% 10.40/10.81 , hskp15, ~( 'c1_1'( Z ) ), ~( 'c1_1'( X ) ), 'c1_1'( Y ), ~( 'c2_1'( X )
% 10.40/10.81 ), 'c2_1'( Z ), ~( 'c2_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 482, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.81 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.81 hskp10, 'c2_1'( a178 ), hskp20, hskp21, ~( 'c3_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 587, [ hskp11, hskp17, hskp25, hskp29, hskp22, hskp3, hskp10, ~(
% 10.40/10.81 'c1_1'( X ) ), 'c1_1'( Y ), ~( 'c1_1'( Z ) ), 'c2_1'( Z ), ~( 'c2_1'( Y )
% 10.40/10.81 ), ~( 'c2_1'( X ) ), 'c3_1'( a181 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 423, [ hskp10, hskp15, hskp17, hskp12, hskp11, hskp1, hskp20,
% 10.40/10.81 hskp21, ~( 'c1_1'( a183 ) ), ~( 'c1_1'( X ) ), ~( 'c2_1'( a183 ) ), ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), 'c1_1'( Y ), hskp13, 'c1_1'( Z ), hskp9
% 10.40/10.81 , 'c3_1'( Y ), ~( 'c3_1'( Z ) ), ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 419, [ 'c1_1'( X ), hskp17, ~( 'c1_1'( a183 ) ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp11, ~( 'c2_1'( a183 ) ), ~( 'c2_1'( X ) ), 'c2_1'( Y ), hskp10,
% 10.40/10.81 hskp15, hskp1, hskp20, hskp12, hskp21, ~( 'c3_1'( X ) ), ~( 'c3_1'( Y ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 440, [ hskp11, hskp25, hskp29, hskp20, hskp21, hskp9, ~( 'c1_1'( X
% 10.40/10.81 ) ), ~( 'c1_1'( Y ) ), hskp18, hskp17, hskp22, 'c1_1'( Z ), hskp10,
% 10.40/10.81 'c2_1'( Y ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 498, [ hskp11, hskp20, hskp21, hskp19, hskp4, hskp9, ~( 'c1_1'( X )
% 10.40/10.81 ), ~( 'c1_1'( Y ) ), hskp18, hskp17, hskp22, 'c1_1'( Z ), hskp10, 'c2_1'(
% 10.40/10.81 Y ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 522, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.81 ), ~( 'c1_1'( X ) ), hskp23, hskp24, hskp3, hskp22, hskp1, hskp15,
% 10.40/10.81 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 418, [ 'c1_1'( X ), hskp17, ~( 'c1_1'( Z ) ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp11, ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c1_1'( T ) )
% 10.40/10.81 , 'c2_1'( T ), ~( 'c3_1'( X ) ), 'c3_1'( Z ), 'c3_1'( T ), ~( 'c3_1'( Y )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 479, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.81 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.81 hskp3, hskp22, hskp1, hskp15, ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 523, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.81 ), ~( 'c1_1'( X ) ), hskp23, hskp24, hskp3, hskp22, 'c2_1'( X ), ~(
% 10.40/10.81 'c2_1'( Z ) ), ~( 'c2_1'( Y ) ), 'c3_1'( a181 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 481, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.81 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.81 hskp3, hskp22, 'c3_1'( a181 ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 486, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.81 ), ~( 'c1_1'( X ) ), hskp20, hskp21, ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y ) )
% 10.40/10.81 , 'c2_1'( X ), ~( 'c2_1'( a178 ) ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 515, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( Z ),
% 10.40/10.81 ~( 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), hskp25, hskp26,
% 10.40/10.81 hskp4, hskp19, ~( 'c3_1'( Y ) ), 'c3_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 513, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( Z ),
% 10.40/10.81 ~( 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), hskp14, hskp0,
% 10.40/10.81 hskp4, hskp19, ~( 'c3_1'( Y ) ), 'c3_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 537, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp4, hskp19,
% 10.40/10.81 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.81 hskp23, hskp24, ~( 'c3_1'( Y ) ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 442, [ hskp11, hskp25, hskp29, hskp20, hskp21, hskp9, ~( 'c1_1'( X
% 10.40/10.81 ) ), ~( 'c1_1'( Y ) ), hskp17, hskp28, 'c1_1'( Z ), hskp10, ~( 'c2_1'( X
% 10.40/10.81 ) ), ~( 'c2_1'( Z ) ), 'c2_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 500, [ hskp11, hskp20, hskp21, hskp19, hskp4, hskp9, ~( 'c1_1'( X )
% 10.40/10.81 ), ~( 'c1_1'( Y ) ), hskp17, hskp28, 'c1_1'( Z ), hskp10, ~( 'c2_1'( X )
% 10.40/10.81 ), ~( 'c2_1'( Z ) ), 'c2_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 524, [ hskp11, hskp29, hskp25, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z
% 10.40/10.81 ), ~( 'c1_1'( X ) ), hskp23, hskp24, hskp3, hskp4, hskp19, ~( 'c2_1'( Y
% 10.40/10.81 ) ), 'c2_1'( X ), ~( 'c2_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 406, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp27, hskp7, hskp17, 'c1_1'( Z ), hskp18, ~( 'c2_1'( X ) ), ~( 'c2_1'(
% 10.40/10.81 Y ) ), 'c2_1'( Z ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 409, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp16, hskp2, hskp17, 'c1_1'( Z ), hskp18, ~( 'c2_1'( X ) ), ~( 'c2_1'(
% 10.40/10.81 Y ) ), 'c2_1'( Z ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 484, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.81 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.81 hskp3, hskp4, hskp19, ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 364, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Z ) ), 'c1_1'( Y ), hskp9,
% 10.40/10.81 ~( 'c2_1'( Y ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( T ) ), ~( 'c2_1'( T ) ),
% 10.40/10.81 hskp11, hskp29, hskp25, 'c3_1'( X ), ~( 'c3_1'( Z ) ), ~( 'c3_1'( Y ) ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 555, [ hskp11, hskp4, hskp19, hskp17, ~( 'c1_1'( Y ) ), 'c1_1'( Z )
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( Y )
% 10.40/10.81 ), hskp23, hskp24, 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 370, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Y ) ), hskp29, hskp25, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ), hskp17, 'c1_1'( Z ), hskp18, 'c2_1'( Z )
% 10.40/10.81 , ~( 'c3_1'( Z ) ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 536, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp4, hskp19,
% 10.40/10.81 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.81 hskp3, ~( 'c3_1'( Z ) ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 359, [ hskp13, hskp20, hskp21, hskp9, hskp25, hskp26, hskp4, hskp19
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp18, hskp17, hskp22, 'c1_1'( Y ), hskp10, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 427, [ ~( 'c1_1'( a183 ) ), ~( 'c1_1'( X ) ), ~( 'c2_1'( a178 ) ),
% 10.40/10.81 hskp20, hskp21, ~( 'c2_1'( a183 ) ), 'c2_1'( X ), hskp10, hskp15, hskp1,
% 10.40/10.81 hskp17, hskp12, hskp11, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 354, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c2_1'( X ) )
% 10.40/10.81 , hskp4, hskp19, ~( 'c2_1'( Z ) ), 'c1_1'( Z ), 'c2_1'( Y ), hskp17, ~(
% 10.40/10.81 'c3_1'( Z ) ), 'c3_1'( X ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 398, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp26, hskp17, 'c1_1'( Z ), hskp18, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X ) ),
% 10.40/10.81 'c2_1'( Z ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 485, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp29, hskp25,
% 10.40/10.81 'c1_1'( Z ), hskp17, ~( 'c2_1'( X ) ), 'c2_1'( Y ), ~( 'c2_1'( Z ) ),
% 10.40/10.81 hskp23, hskp24, ~( 'c3_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 518, [ hskp11, ~( 'c1_1'( a185 ) ), ~( 'c1_1'( X ) ), hskp12,
% 10.40/10.81 hskp20, hskp21, hskp23, ~( 'c1_1'( Y ) ), ~( 'c2_1'( X ) ), 'c2_1'( Y ),
% 10.40/10.81 'c3_1'( Y ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 337, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c2_1'( X ) )
% 10.40/10.81 , ~( 'c2_1'( Z ) ), 'c1_1'( Z ), hskp9, ~( 'c3_1'( Y ) ), 'c3_1'( X ),
% 10.40/10.81 hskp4, hskp19, 'c0_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 516, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( Z ),
% 10.40/10.81 ~( 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), hskp16, hskp2, ~(
% 10.40/10.81 'c3_1'( Y ) ), 'c3_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 336, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c2_1'( X ) )
% 10.40/10.81 , ~( 'c2_1'( Z ) ), 'c1_1'( Z ), hskp9, ~( 'c3_1'( Y ) ), ~( 'c2_1'( T )
% 10.40/10.81 ), ~( 'c3_1'( Z ) ), 'c3_1'( T ), 'c1_1'( T ), hskp13, ~( 'c0_1'( X ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 514, [ hskp13, hskp9, ~( 'c1_1'( X ) ), 'c1_1'( Y ), 'c1_1'( Z ),
% 10.40/10.81 ~( 'c2_1'( Y ) ), ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), hskp27, hskp7, ~(
% 10.40/10.81 'c3_1'( Y ) ), 'c3_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 366, [ hskp13, hskp9, ~( 'c1_1'( Y ) ), 'c1_1'( Z ), 'c1_1'( X ),
% 10.40/10.81 ~( 'c2_1'( Z ) ), ~( 'c2_1'( X ) ), ~( 'c2_1'( Y ) ), 'c3_1'( X ), ~(
% 10.40/10.81 'c3_1'( Z ) ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 335, [ ~( 'c1_1'( a183 ) ), ~( 'c1_1'( X ) ), hskp11, ~( 'c2_1'(
% 10.40/10.81 a183 ) ), ~( 'c2_1'( Y ) ), 'c1_1'( Y ), hskp9, ~( 'c3_1'( X ) ), hskp10
% 10.40/10.81 , hskp15, hskp1, hskp17, hskp20, hskp12, hskp21, 'c0_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 360, [ hskp13, hskp20, hskp21, hskp9, hskp25, hskp26, hskp4, hskp19
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp17, hskp28, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) )
% 10.40/10.81 , ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 334, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c2_1'( X ) )
% 10.40/10.81 , ~( 'c2_1'( Z ) ), 'c1_1'( Z ), hskp9, ~( 'c3_1'( Y ) ), ~( 'c1_1'( T )
% 10.40/10.81 ), 'c2_1'( T ), 'c3_1'( X ), 'c3_1'( T ), 'c0_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 508, [ hskp11, hskp20, hskp21, hskp10, hskp15, hskp1, hskp17,
% 10.40/10.81 hskp12, hskp9, ~( 'c1_1'( X ) ), ~( 'c1_1'( a183 ) ), 'c2_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 325, [ ~( 'c1_1'( a183 ) ), ~( 'c1_1'( X ) ), hskp11, ~( 'c2_1'(
% 10.40/10.81 a183 ) ), ~( 'c2_1'( a178 ) ), hskp9, hskp20, hskp21, hskp10, hskp15,
% 10.40/10.81 hskp1, hskp17, hskp12, ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 322, [ hskp9, hskp20, hskp21, hskp11, hskp25, hskp26, hskp4, hskp19
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp17, hskp28, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) )
% 10.40/10.81 , ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 431, [ hskp12, hskp11, hskp17, hskp20, hskp21, 'c1_1'( X ), hskp13
% 10.40/10.81 , ~( 'c2_1'( X ) ), ~( 'c2_1'( a190 ) ), 'c2_1'( Y ), 'c1_1'( Y ), hskp18
% 10.40/10.81 , ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 332, [ hskp17, hskp18, 'c1_1'( Y ), 'c1_1'( X ), 'c2_1'( Y ), ~(
% 10.40/10.81 'c2_1'( X ) ), ~( 'c2_1'( Z ) ), 'c1_1'( Z ), hskp10, 'c3_1'( Z ), ~(
% 10.40/10.81 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 331, [ hskp17, hskp18, 'c1_1'( Y ), 'c1_1'( X ), 'c2_1'( Y ), ~(
% 10.40/10.81 'c2_1'( X ) ), 'c2_1'( Z ), 'c1_1'( Z ), hskp10, 'c3_1'( Z ), ~( 'c3_1'(
% 10.40/10.81 Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 320, [ hskp9, hskp20, hskp21, hskp11, hskp25, hskp26, hskp4, hskp19
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp18, hskp17, hskp22, 'c1_1'( Y ), hskp10, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 317, [ hskp9, hskp20, hskp21, hskp14, hskp0, hskp16, hskp2, ~(
% 10.40/10.81 'c1_1'( X ) ), hskp18, hskp17, hskp22, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y
% 10.40/10.81 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 318, [ hskp9, hskp20, hskp21, hskp14, hskp0, hskp16, hskp2, ~(
% 10.40/10.81 'c1_1'( X ) ), hskp17, hskp28, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 347, [ hskp13, hskp20, hskp21, hskp9, hskp27, hskp7, ~( 'c1_1'( X )
% 10.40/10.81 ), hskp18, hskp17, hskp22, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 349, [ hskp13, hskp20, hskp21, hskp9, hskp16, hskp2, ~( 'c1_1'( X )
% 10.40/10.81 ), hskp18, hskp17, hskp22, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 316, [ hskp9, hskp20, hskp21, hskp14, hskp0, hskp27, hskp7, ~(
% 10.40/10.81 'c1_1'( X ) ), hskp17, hskp28, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 315, [ hskp9, hskp20, hskp21, hskp14, hskp0, hskp27, hskp7, ~(
% 10.40/10.81 'c1_1'( X ) ), hskp18, hskp17, hskp22, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y
% 10.40/10.81 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 312, [ hskp9, hskp20, hskp21, hskp14, hskp0, hskp4, hskp19, ~(
% 10.40/10.81 'c1_1'( X ) ), hskp17, hskp28, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 502, [ hskp11, hskp20, hskp21, hskp19, hskp4, hskp9, ~( 'c1_1'( X )
% 10.40/10.81 ), ~( 'c1_1'( Y ) ), hskp12, 'c2_1'( Y ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 310, [ hskp9, hskp20, hskp21, hskp14, hskp0, hskp4, hskp19, ~(
% 10.40/10.81 'c1_1'( X ) ), hskp18, hskp17, hskp22, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y
% 10.40/10.81 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 494, [ hskp11, hskp20, hskp21, hskp4, hskp19, hskp9, ~( 'c1_1'( X )
% 10.40/10.81 ), ~( 'c1_1'( Y ) ), 'c2_1'( Y ), ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 489, [ hskp11, ~( 'c1_1'( Y ) ), ~( 'c1_1'( X ) ), hskp9, hskp20,
% 10.40/10.81 hskp21, hskp4, hskp19, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ), ~( 'c3_1'(
% 10.40/10.81 Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 305, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c2_1'( X ) )
% 10.40/10.81 , hskp29, hskp25, ~( 'c2_1'( Z ) ), 'c1_1'( Z ), 'c2_1'( Y ), hskp17, ~(
% 10.40/10.81 'c3_1'( Y ) ), ~( 'c3_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 307, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c2_1'( X ) )
% 10.40/10.81 , hskp29, hskp25, ~( 'c2_1'( Z ) ), 'c1_1'( Z ), hskp9, ~( 'c3_1'( Y ) )
% 10.40/10.81 , 'c0_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 296, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), hskp11
% 10.40/10.81 , ~( 'c2_1'( X ) ), 'c2_1'( Y ), 'c3_1'( X ), ~( 'c3_1'( Z ) ), 'c3_1'( Y
% 10.40/10.81 ), ~( 'c0_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 472, [ hskp11, hskp12, hskp20, hskp21, hskp23, hskp10, hskp15,
% 10.40/10.81 hskp1, hskp17, ~( 'c1_1'( a183 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 432, [ hskp12, hskp11, hskp17, hskp20, hskp21, ~( 'c2_1'( a183 ) )
% 10.40/10.81 , 'c1_1'( a183 ), hskp13, ~( 'c2_1'( a190 ) ), hskp10, hskp15, hskp1, ~(
% 10.40/10.81 'c3_1'( a190 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 348, [ hskp13, hskp20, hskp21, hskp9, hskp27, hskp7, ~( 'c1_1'( X )
% 10.40/10.81 ), hskp17, hskp28, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 350, [ hskp13, hskp20, hskp21, hskp9, hskp16, hskp2, ~( 'c1_1'( X )
% 10.40/10.81 ), hskp17, hskp28, 'c1_1'( Y ), hskp10, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 465, [ hskp11, hskp12, hskp20, hskp21, hskp23, hskp19, hskp4, hskp9
% 10.40/10.81 , ~( 'c1_1'( X ) ), ~( 'c1_1'( a185 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 457, [ hskp11, ~( 'c1_1'( a185 ) ), ~( 'c1_1'( X ) ), hskp12,
% 10.40/10.81 hskp20, hskp21, hskp23, hskp4, hskp19, ~( 'c2_1'( X ) ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 289, [ hskp17, hskp18, hskp22, hskp10, hskp20, hskp21, 'c1_1'( X )
% 10.40/10.81 , hskp9, ~( 'c1_1'( Y ) ), hskp11, hskp27, hskp7, ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 447, [ hskp11, hskp12, hskp13, hskp20, hskp21, hskp23, hskp18,
% 10.40/10.81 'c1_1'( X ), 'c2_1'( X ), ~( 'c2_1'( a185 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 324, [ hskp14, hskp0, ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), ~( 'c2_1'(
% 10.40/10.81 X ) ), 'c2_1'( Y ), hskp9, ~( 'c2_1'( a178 ) ), hskp20, hskp21, 'c3_1'( Y
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 288, [ hskp17, hskp18, hskp22, hskp10, hskp20, hskp21, 'c1_1'( X )
% 10.40/10.81 , hskp9, ~( 'c1_1'( Y ) ), hskp11, hskp16, hskp2, ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 330, [ hskp17, hskp18, 'c1_1'( Y ), 'c1_1'( X ), 'c2_1'( Y ), ~(
% 10.40/10.81 'c2_1'( X ) ), hskp10, ~( 'c2_1'( a178 ) ), hskp20, hskp21, ~( 'c3_1'( X
% 10.40/10.81 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 329, [ hskp17, hskp18, 'c1_1'( Y ), 'c1_1'( X ), 'c2_1'( Y ), ~(
% 10.40/10.81 'c2_1'( X ) ), hskp10, 'c2_1'( a178 ), hskp20, hskp21, ~( 'c3_1'( Y ) ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 429, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp20, hskp21, 'c2_1'(
% 10.40/10.81 Y ), ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ), hskp11, hskp29, hskp25,
% 10.40/10.81 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 425, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp20, hskp21, 'c2_1'(
% 10.40/10.81 Y ), ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ), hskp13, hskp29, hskp25,
% 10.40/10.81 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 282, [ hskp17, hskp21, hskp28, hskp10, hskp20, 'c1_1'( X ), hskp9,
% 10.40/10.81 ~( 'c1_1'( Y ) ), hskp11, hskp27, hskp7, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 403, [ hskp13, hskp11, hskp12, hskp20, hskp21, hskp23, 'c1_1'( a183
% 10.40/10.81 ), ~( 'c2_1'( a183 ) ), hskp10, hskp15, hskp1, hskp17, ~( 'c2_1'( a185 )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 433, [ hskp12, hskp11, hskp17, hskp20, hskp21, 'c1_1'( X ), hskp13
% 10.40/10.81 , ~( 'c2_1'( X ) ), ~( 'c2_1'( a190 ) ), hskp18, hskp22, ~( 'c3_1'( a190
% 10.40/10.81 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 281, [ hskp17, hskp21, hskp28, hskp10, hskp20, 'c1_1'( X ), hskp9,
% 10.40/10.81 ~( 'c1_1'( Y ) ), hskp11, hskp16, hskp2, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 408, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp27, hskp7, hskp18, hskp17, hskp22, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 407, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp27, hskp7, hskp17, hskp21, hskp28, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 411, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp16, hskp2, hskp18, hskp17, hskp22, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 410, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp16, hskp2, hskp17, hskp21, hskp28, ~( 'c2_1'( Y ) ), ~( 'c2_1'( X ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 444, [ hskp11, hskp25, hskp29, hskp20, hskp21, hskp9, ~( 'c1_1'( X
% 10.40/10.81 ) ), ~( 'c1_1'( Y ) ), hskp12, 'c2_1'( Y ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 437, [ hskp11, hskp29, hskp25, hskp9, hskp20, hskp21, ~( 'c1_1'( Y
% 10.40/10.81 ) ), ~( 'c1_1'( X ) ), 'c2_1'( X ), ~( 'c2_1'( Y ) ), ~( 'c2_1'( a178 )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 306, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c2_1'( X ) )
% 10.40/10.81 , hskp29, hskp25, ~( 'c2_1'( a178 ) ), hskp9, hskp20, hskp21, ~( 'c3_1'(
% 10.40/10.81 Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 434, [ hskp12, hskp11, hskp17, hskp20, hskp21, ~( 'c2_1'( a178 ) )
% 10.40/10.81 , hskp13, ~( 'c2_1'( a190 ) ), ~( 'c3_1'( a190 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 277, [ hskp17, hskp12, hskp11, hskp20, hskp21, ~( 'c2_1'( X ) ),
% 10.40/10.81 ~( 'c2_1'( a190 ) ), 'c1_1'( X ), hskp13, 'c3_1'( X ), ~( 'c3_1'( a190 )
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 373, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Y ) ), hskp29, hskp25, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ), hskp18, hskp17, hskp22, ~( 'c3_1'( Y ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 372, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Y ) ), hskp29, hskp25, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ), hskp17, hskp21, hskp28, ~( 'c3_1'( Y ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 428, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp20, hskp21, 'c2_1'(
% 10.40/10.81 Y ), ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ), hskp9, hskp11, 'c3_1'( Y ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 426, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp20, hskp21, 'c2_1'(
% 10.40/10.81 Y ), ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ), hskp13, hskp9, 'c3_1'( Y ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 293, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), ~( 'c2_1'( X ) ), ~(
% 10.40/10.81 'c2_1'( a178 ) ), 'c2_1'( Y ), hskp20, hskp21, 'c3_1'( Y ), 'c3_1'( X ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 253, [ hskp10, hskp15, hskp17, hskp1, hskp12, hskp11, hskp20,
% 10.40/10.81 hskp21, ~( 'c1_1'( a183 ) ), ~( 'c2_1'( a183 ) ), ~( 'c1_1'( X ) ), ~(
% 10.40/10.81 'c3_1'( X ) ), ~( 'c0_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 422, [ hskp11, hskp12, hskp13, hskp20, hskp21, hskp18, hskp17,
% 10.40/10.81 hskp22, hskp23, ~( 'c2_1'( a185 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 417, [ hskp11, ~( 'c1_1'( a185 ) ), ~( 'c1_1'( X ) ), hskp29,
% 10.40/10.81 hskp25, hskp12, hskp20, hskp21, hskp23, ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 247, [ 'c1_1'( X ), ~( 'c2_1'( X ) ), 'c2_1'( Y ), hskp17, ~(
% 10.40/10.81 'c1_1'( Z ) ), ~( 'c2_1'( Z ) ), ~( 'c1_1'( Y ) ), hskp11, ~( 'c3_1'( Y )
% 10.40/10.81 ), ~( 'c3_1'( X ) ), ~( 'c0_1'( Z ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 400, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp26, hskp18, hskp17, hskp22, ~( 'c2_1'( X ) ), ~( 'c2_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 399, [ hskp13, hskp29, hskp25, 'c1_1'( X ), ~( 'c1_1'( Y ) ),
% 10.40/10.81 hskp26, hskp17, hskp21, hskp28, ~( 'c2_1'( X ) ), ~( 'c2_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 376, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Y ) ), hskp29, hskp25, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ), hskp16, hskp2, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 375, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Y ) ), hskp29, hskp25, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ), hskp27, hskp7, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 405, [ ~( 'c1_1'( X ) ), hskp3, 'c1_1'( Y ), hskp12, hskp11, 'c2_1'(
% 10.40/10.81 Y ), 'c2_1'( X ), hskp1, hskp15, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 240, [ ~( 'c1_1'( X ) ), 'c2_1'( Y ), 'c2_1'( X ), hskp3, 'c1_1'( Y
% 10.40/10.81 ), hskp12, hskp11, 'c3_1'( Y ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 227, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Y ) ), hskp9, ~( 'c2_1'( X )
% 10.40/10.81 ), ~( 'c2_1'( Y ) ), ~( 'c3_1'( Y ) ), 'c3_1'( X ), 'c0_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 395, [ 'c1_1'( X ), hskp13, hskp11, hskp12, hskp20, hskp21, hskp23
% 10.40/10.81 , ~( 'c2_1'( a185 ) ), ~( 'c2_1'( X ) ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 374, [ 'c1_1'( X ), hskp13, ~( 'c1_1'( Y ) ), hskp29, hskp25, ~(
% 10.40/10.81 'c2_1'( Y ) ), ~( 'c2_1'( X ) ), hskp26, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 397, [ hskp13, hskp11, hskp12, hskp20, hskp21, hskp23, ~( 'c2_1'(
% 10.40/10.81 a178 ) ), ~( 'c2_1'( a185 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 381, [ hskp13, hskp29, hskp25, ~( 'c1_1'( X ) ), hskp20, hskp21,
% 10.40/10.81 hskp16, hskp2, ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 380, [ hskp13, hskp29, hskp25, ~( 'c1_1'( X ) ), hskp20, hskp21,
% 10.40/10.81 hskp27, hskp7, ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 379, [ hskp13, hskp29, hskp25, ~( 'c1_1'( X ) ), hskp20, hskp21,
% 10.40/10.81 hskp26, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 377, [ hskp13, ~( 'c1_1'( X ) ), hskp29, hskp25, ~( 'c2_1'( a178 )
% 10.40/10.81 ), ~( 'c2_1'( X ) ), hskp20, hskp21, ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 225, [ ~( 'c2_1'( X ) ), ~( 'c2_1'( Y ) ), 'c1_1'( X ), hskp13, ~(
% 10.40/10.81 'c1_1'( Y ) ), hskp29, hskp25, ~( 'c3_1'( Y ) ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 224, [ ~( 'c2_1'( X ) ), ~( 'c2_1'( Y ) ), 'c1_1'( X ), hskp13, ~(
% 10.40/10.81 'c2_1'( Z ) ), ~( 'c1_1'( Y ) ), 'c1_1'( Z ), hskp9, ~( 'c3_1'( Y ) ),
% 10.40/10.81 'c3_1'( X ), 'c0_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 369, [ hskp10, hskp15, hskp17, hskp12, hskp11, hskp1, hskp20,
% 10.40/10.81 hskp21, hskp25, hskp26, ~( 'c1_1'( a183 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 367, [ hskp10, hskp15, hskp17, hskp12, hskp11, hskp1, hskp20,
% 10.40/10.81 hskp21, hskp14, hskp0, ~( 'c1_1'( a183 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 223, [ ~( 'c2_1'( X ) ), ~( 'c2_1'( Y ) ), 'c1_1'( X ), hskp13, ~(
% 10.40/10.81 'c1_1'( Z ) ), 'c1_1'( Y ), hskp9, 'c3_1'( X ), ~( 'c3_1'( Z ) ), ~(
% 10.40/10.81 'c3_1'( Y ) ), 'c0_1'( Z ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 362, [ hskp10, hskp15, hskp17, hskp12, hskp11, hskp1, hskp20,
% 10.40/10.81 hskp21, hskp16, hskp2, ~( 'c1_1'( a183 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 361, [ hskp10, hskp15, hskp17, hskp12, hskp11, hskp1, hskp20,
% 10.40/10.81 hskp21, hskp27, hskp7, ~( 'c1_1'( a183 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 342, [ hskp13, hskp20, hskp21, hskp9, ~( 'c1_1'( X ) ), hskp25,
% 10.40/10.81 hskp26, hskp4, hskp19, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 357, [ hskp18, hskp12, hskp11, hskp20, hskp21, hskp28, 'c1_1'( a195
% 10.40/10.81 ), 'c1_1'( X ), 'c2_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 356, [ hskp10, hskp1, hskp15, hskp18, hskp17, hskp22, 'c1_1'( X ),
% 10.40/10.81 ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 221, [ ~( 'c2_1'( X ) ), ~( 'c2_1'( Y ) ), 'c1_1'( X ), hskp13, ~(
% 10.40/10.81 'c1_1'( a192 ) ), 'c1_1'( Y ), hskp9, hskp21, hskp28, ~( 'c3_1'( Y ) ),
% 10.40/10.81 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 355, [ hskp10, hskp1, hskp15, hskp17, hskp21, hskp28, 'c1_1'( X ),
% 10.40/10.81 hskp22, ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 297, [ hskp10, 'c1_1'( Y ), 'c1_1'( X ), hskp1, hskp15, hskp17,
% 10.40/10.81 hskp21, hskp28, ~( 'c2_1'( X ) ), 'c2_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 220, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11
% 10.40/10.81 , ~( 'c3_1'( Y ) ), 'c3_1'( X ), hskp4, hskp19, ~( 'c0_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 304, [ hskp18, hskp12, hskp11, hskp10, hskp1, hskp15, 'c1_1'( X ),
% 10.40/10.81 'c1_1'( Y ), 'c2_1'( Y ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 343, [ hskp13, hskp20, hskp21, hskp9, ~( 'c1_1'( X ) ), hskp16,
% 10.40/10.81 hskp2, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 341, [ hskp13, hskp20, hskp21, hskp9, ~( 'c1_1'( X ) ), hskp27,
% 10.40/10.81 hskp7, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 219, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( a185 ) ),
% 10.40/10.81 hskp11, ~( 'c3_1'( a185 ) ), hskp12, hskp20, hskp21, hskp23, ~( 'c0_1'( X
% 10.40/10.81 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 338, [ hskp13, hskp9, hskp20, hskp21, ~( 'c1_1'( X ) ), ~( 'c2_1'(
% 10.40/10.81 X ) ), ~( 'c2_1'( a178 ) ), ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 237, [ hskp18, hskp17, hskp22, 'c1_1'( X ), 'c1_1'( Y ), hskp10,
% 10.40/10.81 ~( 'c2_1'( X ) ), 'c2_1'( Y ), 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 267, [ hskp17, hskp21, hskp28, 'c1_1'( X ), 'c1_1'( Y ), hskp10,
% 10.40/10.81 ~( 'c2_1'( X ) ), 'c2_1'( Y ), 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 217, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11
% 10.40/10.81 , ~( 'c3_1'( Y ) ), ~( 'c2_1'( Z ) ), 'c1_1'( Z ), hskp9, 'c0_1'( Z ),
% 10.40/10.81 ~( 'c0_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 303, [ hskp18, hskp12, hskp11, hskp10, 'c1_1'( X ), 'c1_1'( Y ),
% 10.40/10.81 'c2_1'( Y ), ~( 'c2_1'( X ) ), 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 333, [ hskp17, hskp18, 'c1_1'( Y ), 'c1_1'( X ), 'c2_1'( Y ), ~(
% 10.40/10.81 'c2_1'( X ) ), hskp23, hskp24, ~( 'c3_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 249, [ 'c1_1'( X ), hskp17, 'c1_1'( Y ), hskp18, 'c2_1'( Y ), ~(
% 10.40/10.81 'c2_1'( X ) ), ~( 'c3_1'( X ) ), ~( 'c3_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 294, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp25, hskp26, ~(
% 10.40/10.81 'c2_1'( X ) ), 'c2_1'( Y ), 'c3_1'( Y ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 216, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11
% 10.40/10.81 , ~( 'c3_1'( Y ) ), ~( 'c2_1'( a178 ) ), hskp9, hskp20, hskp21, ~( 'c0_1'(
% 10.40/10.81 X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 295, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), hskp14, hskp0, ~( 'c2_1'(
% 10.40/10.81 X ) ), 'c2_1'( Y ), 'c3_1'( Y ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 323, [ hskp9, hskp20, hskp21, hskp11, hskp25, hskp26, hskp4, hskp19
% 10.40/10.81 , ~( 'c1_1'( X ) ), hskp12, ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 212, [ hskp9, ~( 'c1_1'( X ) ), hskp20, hskp21, hskp11, hskp25,
% 10.40/10.81 hskp26, hskp4, hskp19, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 314, [ hskp9, hskp20, hskp21, hskp14, hskp0, hskp4, hskp19, ~(
% 10.40/10.81 'c1_1'( X ) ), hskp12, hskp11, ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 286, [ hskp9, ~( 'c1_1'( X ) ), hskp20, hskp21, hskp14, hskp0,
% 10.40/10.81 hskp16, hskp2, ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 285, [ hskp9, ~( 'c1_1'( X ) ), hskp20, hskp21, hskp14, hskp0,
% 10.40/10.81 hskp27, hskp7, ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 284, [ hskp9, ~( 'c1_1'( X ) ), hskp20, hskp21, hskp14, hskp0,
% 10.40/10.81 hskp4, hskp19, ~( 'c2_1'( X ) ), ~( 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 309, [ hskp3, hskp17, hskp22, ~( 'c1_1'( X ) ), hskp1, hskp15,
% 10.40/10.81 'c2_1'( X ), 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 209, [ ~( 'c1_1'( X ) ), ~( 'c1_1'( Y ) ), ~( 'c2_1'( X ) ), 'c2_1'(
% 10.40/10.81 Y ), 'c3_1'( X ), 'c3_1'( Y ), 'c0_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 302, [ 'c1_1'( X ), 'c1_1'( Y ), hskp18, hskp12, hskp11, hskp23,
% 10.40/10.81 hskp24, 'c2_1'( Y ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 218, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'c1_1'( Y ) ), hskp11
% 10.40/10.81 , ~( 'c3_1'( Y ) ), hskp29, hskp25, ~( 'c0_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 229, [ ~( 'c2_1'( X ) ), 'c1_1'( X ), 'c2_1'( Y ), 'c1_1'( Y ),
% 10.40/10.81 hskp18, hskp12, hskp11, ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 231, [ 'c1_1'( X ), 'c1_1'( Y ), hskp10, ~( 'c2_1'( X ) ), 'c2_1'(
% 10.40/10.81 Y ), hskp1, hskp15, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 208, [ ~( 'c1_1'( Y ) ), ~( 'c1_1'( Z ) ), ~( 'c2_1'( Y ) ), ~(
% 10.40/10.81 'c2_1'( X ) ), 'c3_1'( X ), 'c3_1'( Y ), 'c2_1'( Z ), 'c3_1'( Z ), 'c0_1'(
% 10.40/10.81 X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 236, [ hskp18, hskp17, hskp22, 'c1_1'( X ), hskp10, hskp20, hskp21
% 10.40/10.81 , 'c2_1'( a178 ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 200, [ ~( 'c1_1'( X ) ), hskp9, ~( 'c2_1'( a178 ) ), hskp20, hskp21
% 10.40/10.81 , ~( 'c2_1'( X ) ), hskp14, hskp0, ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 283, [ hskp17, hskp21, hskp28, hskp10, hskp20, 'c1_1'( X ), ~(
% 10.40/10.81 'c1_1'( a192 ) ), hskp9, ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 243, [ hskp10, hskp20, hskp21, hskp1, hskp15, 'c1_1'( X ), hskp12,
% 10.40/10.81 hskp11, 'c2_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 266, [ hskp17, hskp21, hskp28, 'c1_1'( X ), hskp10, hskp20, ~(
% 10.40/10.81 'c2_1'( X ) ), 'c2_1'( a178 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 276, [ hskp17, hskp20, hskp12, hskp11, hskp21, 'c2_1'( a190 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 195, [ ~( 'c1_1'( Y ) ), 'c1_1'( X ), ~( 'c2_1'( X ) ), hskp9, ~(
% 10.40/10.81 'c3_1'( Y ) ), ~( 'c2_1'( Y ) ), hskp14, hskp0, 'c0_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 275, [ hskp17, hskp20, hskp12, hskp11, hskp21, 'c0_1'( a190 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 274, [ hskp17, hskp20, hskp12, hskp11, hskp21, ~( 'c1_1'( a190 ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 273, [ hskp17, hskp21, hskp20, hskp12, hskp11, hskp28 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 194, [ ~( 'c1_1'( Y ) ), 'c1_1'( X ), ~( 'c2_1'( X ) ), hskp9, ~(
% 10.40/10.81 'c3_1'( Y ) ), ~( 'c2_1'( Y ) ), hskp11, 'c0_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 269, [ hskp17, hskp21, hskp28, 'c1_1'( X ), hskp23, hskp24, ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 265, [ 'c1_1'( X ), hskp17, hskp21, hskp28, ~( 'c2_1'( X ) ), ~(
% 10.40/10.81 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 252, [ hskp10, hskp15, hskp1, hskp17, hskp20, hskp12, hskp11,
% 10.40/10.81 hskp21, ~( 'c3_1'( a183 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 251, [ hskp10, hskp15, hskp1, hskp17, hskp20, hskp12, hskp11,
% 10.40/10.81 hskp21, 'c2_1'( a183 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 250, [ hskp10, hskp15, hskp1, hskp17, hskp20, hskp12, hskp11,
% 10.40/10.81 hskp21, 'c0_1'( a183 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 245, [ hskp10, hskp1, hskp15, hskp20, hskp17, hskp21, hskp12,
% 10.40/10.81 hskp11, hskp22 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 187, [ ~( 'c2_1'( X ) ), 'c1_1'( X ), 'c2_1'( Y ), ~( 'c3_1'( X ) )
% 10.40/10.81 , ~( 'c3_1'( Y ) ), hskp17, 'c0_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 244, [ hskp10, hskp20, hskp1, hskp15, hskp21, hskp17, hskp22, ~(
% 10.40/10.81 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 234, [ hskp10, 'c1_1'( X ), hskp20, hskp21, hskp1, hskp15, 'c2_1'(
% 10.40/10.81 X ), ~( 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 241, [ ~( 'c1_1'( X ) ), 'c2_1'( X ), hskp3, hskp17, hskp22, 'c3_1'(
% 10.40/10.81 X ), 'c3_1'( a181 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 239, [ hskp18, hskp17, hskp22, 'c1_1'( X ), hskp23, hskp24, ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 178, [ ~( 'c1_1'( Y ) ), 'c3_1'( X ), 'c2_1'( X ), 'c3_1'( Y ),
% 10.40/10.81 'c2_1'( Y ), hskp3, ~( 'c0_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 235, [ 'c1_1'( X ), hskp18, hskp17, hskp22, ~( 'c2_1'( X ) ), ~(
% 10.40/10.81 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 233, [ 'c1_1'( X ), hskp10, 'c2_1'( a178 ), ~( 'c2_1'( X ) ),
% 10.40/10.81 hskp20, hskp21, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 232, [ 'c1_1'( X ), hskp10, ~( 'c2_1'( a178 ) ), 'c2_1'( X ),
% 10.40/10.81 hskp20, hskp21, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 174, [ ~( 'c2_1'( X ) ), 'c1_1'( X ), 'c2_1'( Y ), 'c1_1'( Y ),
% 10.40/10.81 hskp10, 'c3_1'( X ), 'c3_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 188, [ ~( 'c2_1'( X ) ), ~( 'c3_1'( X ) ), 'c1_1'( X ), 'c2_1'( Y )
% 10.40/10.81 , 'c1_1'( Y ), hskp18, ~( 'c0_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 198, [ ~( 'c2_1'( X ) ), ~( 'c3_1'( Y ) ), ~( 'c2_1'( Y ) ), 'c3_1'(
% 10.40/10.81 X ), 'c1_1'( X ), hskp13, ~( 'c0_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 207, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), ~( 'c3_1'( Y ) ), ~(
% 10.40/10.81 'c1_1'( Y ) ), hskp11, ~( 'c0_1'( X ) ), ~( 'c0_1'( Y ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 215, [ hskp9, hskp20, hskp21, hskp11, hskp16, hskp2, ~( 'c1_1'( X )
% 10.40/10.81 ), hskp12, ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 213, [ hskp9, ~( 'c1_1'( X ) ), hskp20, hskp21, hskp11, hskp16,
% 10.40/10.81 hskp2, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 214, [ hskp9, hskp20, hskp21, hskp11, hskp27, hskp7, ~( 'c1_1'( X )
% 10.40/10.81 ), hskp12, ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 211, [ hskp9, ~( 'c1_1'( X ) ), hskp20, hskp21, hskp11, hskp27,
% 10.40/10.81 hskp7, ~( 'c2_1'( a178 ) ), ~( 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 199, [ ~( 'c1_1'( X ) ), hskp9, ~( 'c2_1'( a178 ) ), hskp20, hskp21
% 10.40/10.81 , ~( 'c2_1'( X ) ), hskp11, ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 197, [ ~( 'c1_1'( a192 ) ), 'c1_1'( X ), hskp9, ~( 'c2_1'( X ) ),
% 10.40/10.81 hskp21, hskp28, 'c0_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 206, [ hskp20, hskp21, hskp12, hskp11, hskp28, ~( 'c1_1'( a195 ) )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 205, [ hskp20, hskp21, hskp12, hskp11, hskp28, 'c2_1'( a195 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 204, [ hskp20, hskp21, hskp12, hskp11, hskp28, 'c3_1'( a195 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 203, [ hskp20, hskp21, hskp28, hskp12, hskp11, hskp9 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 201, [ ~( 'c1_1'( a192 ) ), hskp9, hskp20, hskp21, hskp28, ~(
% 10.40/10.81 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 196, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( a178 ) ), hskp9, ~( 'c3_1'( X )
% 10.40/10.81 ), hskp20, hskp21, 'c0_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 193, [ ~( 'c2_1'( X ) ), ~( 'c1_1'( Y ) ), 'c1_1'( X ), ~( 'c3_1'(
% 10.40/10.81 Y ) ), hskp9, 'c0_1'( X ), 'c0_1'( Y ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 192, [ hskp11, ~( 'c1_1'( a185 ) ), hskp12, hskp20, hskp21, hskp23
% 10.40/10.81 , ~( 'c2_1'( a185 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 172, [ ~( 'c1_1'( X ) ), hskp14, hskp0, ~( 'c2_1'( X ) ), hskp4,
% 10.40/10.81 hskp19, 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 185, [ hskp11, ~( 'c1_1'( X ) ), hskp29, hskp25, hskp16, hskp2, ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 184, [ hskp11, ~( 'c1_1'( X ) ), hskp29, hskp25, hskp27, hskp7, ~(
% 10.40/10.81 'c2_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 180, [ ~( 'c1_1'( X ) ), hskp3, 'c2_1'( X ), hskp4, hskp19, 'c3_1'(
% 10.40/10.81 X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 183, [ hskp11, ~( 'c1_1'( X ) ), hskp29, hskp25, hskp26, ~( 'c2_1'(
% 10.40/10.81 X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 181, [ ~( 'c1_1'( X ) ), hskp11, ~( 'c2_1'( X ) ), hskp29, hskp25,
% 10.40/10.81 ~( 'c3_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 177, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), hskp11, ~( 'c3_1'( X ) )
% 10.40/10.81 , ~( 'c0_1'( X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 179, [ ~( 'c1_1'( X ) ), 'c2_1'( X ), hskp3, 'c3_1'( X ), ~( 'c0_1'(
% 10.40/10.81 X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 176, [ ~( 'c1_1'( X ) ), hskp29, hskp25, ~( 'c2_1'( X ) ), hskp26,
% 10.40/10.81 'c3_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 175, [ ~( 'c1_1'( X ) ), hskp29, hskp25, hskp14, hskp0, ~( 'c2_1'(
% 10.40/10.81 X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 173, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), hskp29, hskp25, 'c0_1'(
% 10.40/10.81 X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 170, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), hskp14, hskp0, ~( 'c0_1'(
% 10.40/10.81 X ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 169, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), hskp27, hskp7, 'c3_1'( X
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 168, [ ~( 'c1_1'( X ) ), hskp25, hskp26, hskp4, hskp19, 'c3_1'( X )
% 10.40/10.81 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 163, [ ~( 'c1_1'( X ) ), ~( 'c2_1'( X ) ), hskp16, hskp2, 'c3_1'( X
% 10.40/10.81 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 167, [ ~( 'c1_1'( X ) ), 'c3_1'( X ), hskp25, hskp26, ~( 'c0_1'( X
% 10.40/10.81 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 166, [ hskp11, hskp12, hskp20, hskp21, hskp23, 'c1_1'( a185 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 165, [ hskp11, hskp12, hskp20, hskp21, hskp23, 'c3_1'( a185 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 164, [ hskp11, hskp12, hskp20, hskp21, hskp23, 'c0_1'( a185 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 161, [ hskp12, hskp11, hskp21, hskp28, 'c1_1'( a192 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 162, [ hskp11, hskp12, hskp20, hskp21, hskp23, hskp24 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 160, [ hskp12, hskp11, hskp20, hskp21, 'c2_1'( a178 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 154, [ 'c1_1'( X ), 'c2_1'( X ), hskp12, hskp11, 'c0_1'( X ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 159, [ hskp23, hskp24, hskp20, hskp21, ~( 'c2_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 158, [ 'c1_1'( X ), ~( 'c2_1'( X ) ), hskp23, hskp24, 'c3_1'( X ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 157, [ hskp1, hskp15, hskp21, hskp28, 'c1_1'( a192 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 155, [ 'c2_1'( X ), 'c1_1'( X ), hskp1, hskp15, ~( 'c3_1'( X ) ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 156, [ ~( 'c1_1'( X ) ), 'c3_1'( X ), hskp4, hskp19, 'c0_1'( X ) ]
% 10.40/10.81 )
% 10.40/10.81 .
% 10.40/10.81 clause( 145, [ hskp20, hskp21, ~( 'c1_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 146, [ hskp20, hskp21, ~( 'c0_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 147, [ hskp20, hskp21, ~( 'c3_1'( a178 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 148, [ hskp17, hskp22, ~( 'c2_1'( a181 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 149, [ hskp17, hskp22, ~( 'c1_1'( a181 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 150, [ hskp21, hskp28, ~( 'c2_1'( a192 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 151, [ hskp21, hskp28, ~( 'c0_1'( a192 ) ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 152, [ hskp17, hskp22, 'c0_1'( a181 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 153, [ hskp21, hskp28, 'c3_1'( a192 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 51, [ 'c3_1'( a179 ), ~( hskp20 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 52, [ 'c2_1'( a179 ), ~( hskp20 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 53, [ 'c0_1'( a179 ), ~( hskp20 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 54, [ 'c3_1'( a177 ), ~( hskp19 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 50, [ 'c3_1'( a180 ), ~( hskp21 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 55, [ 'c1_1'( a177 ), ~( hskp19 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 56, [ 'c1_1'( a175 ), ~( hskp18 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 57, [ 'c3_1'( a175 ), ~( hskp18 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 58, [ 'c2_1'( a175 ), ~( hskp18 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 49, [ 'c0_1'( a183 ), ~( hskp22 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 59, [ 'c0_1'( a174 ), ~( hskp17 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 60, [ 'c2_1'( a174 ), ~( hskp17 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 61, [ 'c1_1'( a171 ), ~( hskp16 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 62, [ 'c0_1'( a171 ), ~( hskp16 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 48, [ 'c2_1'( a183 ), ~( hskp22 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 63, [ 'c1_1'( a170 ), ~( hskp15 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 64, [ 'c0_1'( a170 ), ~( hskp15 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 65, [ 'c2_1'( a170 ), ~( hskp15 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 66, [ 'c0_1'( a167 ), ~( hskp14 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 47, [ 'c0_1'( a184 ), ~( hskp23 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 67, [ 'c3_1'( a167 ), ~( hskp14 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 68, [ 'c1_1'( a166 ), ~( hskp13 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 69, [ 'c3_1'( a166 ), ~( hskp13 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 70, [ 'c2_1'( a164 ), ~( hskp12 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 46, [ 'c2_1'( a184 ), ~( hskp23 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 71, [ 'c0_1'( a163 ), ~( hskp11 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 72, [ 'c3_1'( a163 ), ~( hskp11 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 73, [ 'c2_1'( a162 ), ~( hskp10 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 74, [ 'c3_1'( a195 ), ~( hskp9 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 45, [ 'c1_1'( a184 ), ~( hskp23 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 75, [ 'c2_1'( a195 ), ~( hskp9 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 76, [ 'c3_1'( a192 ), ~( hskp8 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 77, [ 'c2_1'( a189 ), ~( hskp7 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 78, [ 'c1_1'( a189 ), ~( hskp7 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 44, [ 'c0_1'( a185 ), ~( hskp24 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 79, [ 'c0_1'( a181 ), ~( hskp6 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 80, [ 'c3_1'( a173 ), ~( hskp3 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 81, [ 'c3_1'( a172 ), ~( hskp2 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 82, [ 'c3_1'( a169 ), ~( hskp1 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 43, [ 'c3_1'( a185 ), ~( hskp24 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 83, [ ~( 'c1_1'( a190 ) ), ~( hskp28 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 84, [ ~( 'c2_1'( a188 ) ), ~( hskp27 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 85, [ ~( 'c2_1'( a187 ) ), ~( hskp26 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 86, [ ~( 'c1_1'( a187 ) ), ~( hskp26 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 42, [ 'c1_1'( a185 ), ~( hskp24 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 87, [ ~( 'c0_1'( a186 ) ), ~( hskp25 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 88, [ ~( 'c2_1'( a186 ) ), ~( hskp25 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 89, [ ~( 'c3_1'( a183 ) ), ~( hskp22 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 90, [ ~( 'c1_1'( a180 ) ), ~( hskp21 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 41, [ 'c1_1'( a186 ), ~( hskp25 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 91, [ ~( 'c2_1'( a180 ) ), ~( hskp21 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 92, [ ~( 'c0_1'( a177 ) ), ~( hskp19 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 93, [ ~( 'c3_1'( a174 ) ), ~( hskp17 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 94, [ ~( 'c3_1'( a171 ) ), ~( hskp16 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 40, [ 'c3_1'( a187 ), ~( hskp26 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 95, [ ~( 'c2_1'( a167 ) ), ~( hskp14 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 96, [ ~( 'c2_1'( a166 ) ), ~( hskp13 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 97, [ ~( 'c0_1'( a164 ) ), ~( hskp12 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 98, [ ~( 'c1_1'( a164 ) ), ~( hskp12 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 39, [ 'c0_1'( a188 ), ~( hskp27 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 99, [ ~( 'c1_1'( a163 ) ), ~( hskp11 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 100, [ ~( 'c0_1'( a162 ) ), ~( hskp10 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 101, [ ~( 'c3_1'( a162 ) ), ~( hskp10 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 102, [ ~( 'c1_1'( a195 ) ), ~( hskp9 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 38, [ 'c1_1'( a188 ), ~( hskp27 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 103, [ ~( 'c0_1'( a192 ) ), ~( hskp8 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 104, [ ~( 'c2_1'( a192 ) ), ~( hskp8 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 105, [ ~( 'c3_1'( a189 ) ), ~( hskp7 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 106, [ ~( 'c1_1'( a181 ) ), ~( hskp6 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 37, [ 'c0_1'( a190 ), ~( hskp28 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 107, [ ~( 'c2_1'( a181 ) ), ~( hskp6 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 108, [ ~( 'c3_1'( a178 ) ), ~( hskp5 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 109, [ ~( 'c0_1'( a178 ) ), ~( hskp5 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 110, [ ~( 'c1_1'( a178 ) ), ~( hskp5 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 36, [ 'c2_1'( a190 ), ~( hskp28 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 111, [ ~( 'c1_1'( a176 ) ), ~( hskp4 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 112, [ ~( 'c3_1'( a176 ) ), ~( hskp4 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 113, [ ~( 'c0_1'( a176 ) ), ~( hskp4 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 114, [ ~( 'c1_1'( a173 ) ), ~( hskp3 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 35, [ 'c0_1'( a193 ), ~( hskp29 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 115, [ ~( 'c2_1'( a173 ) ), ~( hskp3 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 116, [ ~( 'c2_1'( a172 ) ), ~( hskp2 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 117, [ ~( 'c1_1'( a172 ) ), ~( hskp2 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 118, [ ~( 'c1_1'( a169 ) ), ~( hskp1 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 34, [ 'c3_1'( a193 ), ~( hskp29 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 119, [ ~( 'c0_1'( a169 ) ), ~( hskp1 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 120, [ ~( 'c0_1'( a168 ) ), ~( hskp0 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 121, [ ~( 'c2_1'( a168 ) ), ~( hskp0 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 122, [ ~( 'c1_1'( a168 ) ), ~( hskp0 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 33, [ 'c2_1'( a193 ), ~( hskp29 ) ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 31, [ hskp17, hskp22, hskp6 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 32, [ hskp21, hskp28, hskp8 ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 144, [ 'ndr1_0' ] )
% 10.40/10.81 .
% 10.40/10.81 clause( 30, [ hskp20, hskp21, hskp5 ] )
% 10.40/10.81 .
% 10.40/10.81
% 10.40/10.81
% 10.40/10.81 % SZS output end Saturation
% 10.40/10.81 end of saturation!
% 10.40/10.81
% 10.40/10.81 Memory use:
% 10.40/10.81
% 10.40/10.81 space for terms: 14100
% 10.40/10.81 space for clauses: 27288
% 10.40/10.81
% 10.40/10.81
% 10.40/10.81 clauses generated: 25764
% 10.40/10.81 clauses kept: 629
% 10.40/10.81 clauses selected: 459
% 10.40/10.81 clauses deleted: 242
% 10.40/10.81 clauses inuse deleted: 72
% 10.40/10.81
% 10.40/10.81 subsentry: 41611
% 10.40/10.81 literals s-matched: 38093
% 10.40/10.81 literals matched: 38093
% 10.40/10.81 full subsumption: 32533
% 10.40/10.81
% 10.40/10.81 checksum: 684773263
% 10.40/10.81
% 10.40/10.81
% 10.40/10.81 Bliksem ended
%------------------------------------------------------------------------------