%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT082+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 8 06:04:24 AM UTC 2026
% Result : Theorem 60.65s 60.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT082+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n014.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 7 14:17:11 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.25/0.51 start to proof:theBenchmark
% 60.52/60.69 %-------------------------------------------
% 60.52/60.69 % File :CSE---1.7
% 60.52/60.69 % Problem :theBenchmark
% 60.52/60.69 % Transform :cnf
% 60.52/60.69 % Format :tptp:raw
% 60.52/60.69 % Command :java -jar mcs_scs.jar %d %s
% 60.52/60.69
% 60.52/60.69 % Result :Theorem 60.193680s
% 60.52/60.69 % Output :CNFRefutation 60.193680s
% 60.52/60.69 %-------------------------------------------
% 60.52/60.69 %--------------------------------------------------------------------------
% 60.52/60.69 % File : MGT082+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 60.52/60.69 % Domain : Management
% 60.52/60.69 % Problem : 3D eq conflict via distinctness (7 constants)
% 60.52/60.69 % Version : Especial.
% 60.52/60.69 % English : Width: eq 600 intersection eq 601 = {600}intersection{601} =
% 60.52/60.69 % null Conflict (distinct)
% 60.52/60.69 % Height: gt 300 intersection lt 500 = (300,500) Compatible
% 60.52/60.69 % Depth: gteq 16 intersection lteq 32 = [16,32] Compatible
% 60.52/60.69 % Conflict proved by X distinctness - no density needed.
% 60.52/60.69
% 60.52/60.69 % Refs : [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 60.52/60.69 % Source : [MC+26]
% 60.52/60.69 % Names : ODRL411-1.p [MC+26]
% 60.52/60.69
% 60.52/60.69 % Status : Theorem
% 60.52/60.69 % Rating : ? v9.3.1
% 60.52/60.69 % Syntax : Number of formulae : 57 ( 35 unt; 0 def)
% 60.52/60.69 % Number of atoms : 132 ( 44 equ)
% 60.52/60.69 % Maximal formula atoms : 21 ( 2 avg)
% 60.52/60.69 % Number of connectives : 104 ( 29 ~; 9 |; 46 &)
% 60.52/60.69 % ( 8 <=>; 12 =>; 0 <=; 0 <~>)
% 60.52/60.69 % Maximal formula depth : 22 ( 3 avg)
% 60.52/60.69 % Maximal term depth : 2 ( 1 avg)
% 60.52/60.69 % Number of predicates : 12 ( 11 usr; 0 prp; 1-4 aty)
% 60.52/60.69 % Number of functors : 11 ( 11 usr; 10 con; 0-2 aty)
% 60.52/60.69 % Number of variables : 60 ( 55 !; 5 ?)
% 60.52/60.69 % SPC : FOF_THM_RFO_SEQ
% 60.52/60.69
% 60.52/60.69 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 60.52/60.69 % Bugfixes : v9.3.1 - $distinct expanded to inequalities.
% 60.52/60.69 %--------------------------------------------------------------------------
% 60.52/60.69 include('Axioms/MGT002+0.ax').
% 60.52/60.69 include('Axioms/MGT002+2.ax').
% 60.52/60.69 %--------------------------------------------------------------------------
% 60.52/60.69 %----Named constants and ordering
% 60.52/60.69 fof(val_v0,axiom,
% 60.52/60.69 val(v0) ).
% 60.52/60.69
% 60.52/60.70 fof(val_v16,axiom,
% 60.52/60.70 val(v16) ).
% 60.52/60.70
% 60.52/60.70 fof(val_v32,axiom,
% 60.52/60.70 val(v32) ).
% 60.52/60.70
% 60.52/60.70 fof(val_v300,axiom,
% 60.52/60.70 val(v300) ).
% 60.52/60.70
% 60.52/60.70 fof(val_v500,axiom,
% 60.52/60.70 val(v500) ).
% 60.52/60.70
% 60.52/60.70 fof(val_v600,axiom,
% 60.52/60.70 val(v600) ).
% 60.52/60.70
% 60.52/60.70 fof(val_v601,axiom,
% 60.52/60.70 val(v601) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v0_v16,axiom,
% 60.52/60.70 less(v0,v16) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v0_v32,axiom,
% 60.52/60.70 less(v0,v32) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v0_v300,axiom,
% 60.52/60.70 less(v0,v300) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v0_v500,axiom,
% 60.52/60.70 less(v0,v500) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v0_v600,axiom,
% 60.52/60.70 less(v0,v600) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v0_v601,axiom,
% 60.52/60.70 less(v0,v601) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v16_v32,axiom,
% 60.52/60.70 less(v16,v32) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v16_v300,axiom,
% 60.52/60.70 less(v16,v300) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v16_v500,axiom,
% 60.52/60.70 less(v16,v500) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v16_v600,axiom,
% 60.52/60.70 less(v16,v600) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v16_v601,axiom,
% 60.52/60.70 less(v16,v601) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v32_v300,axiom,
% 60.52/60.70 less(v32,v300) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v32_v500,axiom,
% 60.52/60.70 less(v32,v500) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v32_v600,axiom,
% 60.52/60.70 less(v32,v600) ).
% 60.52/60.70
% 60.52/60.70 fof(ord_v32_v601,axiom,
% 60.52/60.70 less(v32,v601) ).
% 60.52/60.70
% 60.65/60.70 fof(ord_v300_v500,axiom,
% 60.65/60.70 less(v300,v500) ).
% 60.65/60.70
% 60.65/60.70 fof(ord_v300_v600,axiom,
% 60.65/60.70 less(v300,v600) ).
% 60.65/60.70
% 60.65/60.70 fof(ord_v300_v601,axiom,
% 60.65/60.70 less(v300,v601) ).
% 60.65/60.70
% 60.65/60.70 fof(ord_v500_v600,axiom,
% 60.65/60.70 less(v500,v600) ).
% 60.65/60.70
% 60.65/60.70 fof(ord_v500_v601,axiom,
% 60.65/60.70 less(v500,v601) ).
% 60.65/60.70
% 60.65/60.70 fof(ord_v600_v601,axiom,
% 60.65/60.70 less(v600,v601) ).
% 60.65/60.70
% 60.65/60.70 fof(distinct,axiom,
% 60.65/60.70 ( v0 != v16
% 60.65/60.70 & v0 != v32
% 60.65/60.70 & v0 != v300
% 60.65/60.70 & v0 != v500
% 60.65/60.70 & v0 != v600
% 60.65/60.70 & v0 != v601
% 60.65/60.70 & v16 != v32
% 60.65/60.70 & v16 != v300
% 60.65/60.70 & v16 != v500
% 60.65/60.70 & v16 != v600
% 60.65/60.70 & v16 != v601
% 60.65/60.70 & v32 != v300
% 60.65/60.70 & v32 != v500
% 60.65/60.70 & v32 != v600
% 60.65/60.70 & v32 != v601
% 60.65/60.70 & v300 != v500
% 60.65/60.70 & v300 != v600
% 60.65/60.70 & v300 != v601
% 60.65/60.70 & v500 != v600
% 60.65/60.70 & v500 != v601
% 60.65/60.70 & v600 != v601 ) ).
% 60.65/60.70
% 60.65/60.70 fof(odrl411,conjecture,
% 60.65/60.70 ~ ? [X,Y,Z] :
% 60.65/60.70 ( in_closed(X,v600,v600)
% 60.65/60.70 & in_closed(X,v601,v601)
% 60.65/60.70 & less(v300,Y)
% 60.65/60.70 & in_open(Y,v0,v500)
% 60.65/60.70 & leq(v16,Z)
% 60.65/60.70 & in_lopen(Z,v0,v32) ) ).
% 60.65/60.70
% 60.65/60.70 %--------------------------------------------------------------------------
% 60.65/60.70 %-------------------------------------------
% 60.65/60.70 % Proof found
% 60.65/60.70 % SZS status Theorem for theBenchmark
% 60.65/60.70 % SZS output start Proof
% 60.65/60.70 %ClaNum:147(EqnAxiom:47)
% 60.65/60.70 %VarNum:252(SingletonVarNum:111)
% 60.65/60.70 %MaxLitNum:6
% 60.65/60.70 %MaxfuncDepth:1
% 60.65/60.70 %SharedTerms:74
% 60.65/60.70 %goalClause: 76 80 81 82 83 84
% 60.65/60.70 %singleGoalClaCount:6
% 60.65/60.70 [48]P1(a1)
% 60.65/60.70 [49]P1(a2)
% 60.65/60.70 [50]P1(a4)
% 60.65/60.70 [51]P9(a11)
% 60.65/60.70 [52]P9(a12)
% 60.65/60.70 [53]P9(a13)
% 60.65/60.70 [54]P9(a14)
% 60.65/60.70 [55]P9(a15)
% 60.65/60.70 [56]P9(a16)
% 60.65/60.70 [57]P9(a17)
% 60.65/60.70 [58]P10(a11,a12)
% 60.65/60.70 [59]P10(a11,a13)
% 60.65/60.70 [60]P10(a11,a14)
% 60.65/60.70 [61]P10(a11,a15)
% 60.65/60.70 [62]P10(a11,a16)
% 60.65/60.70 [63]P10(a11,a17)
% 60.65/60.70 [64]P10(a12,a13)
% 60.65/60.70 [65]P10(a12,a14)
% 60.65/60.70 [66]P10(a12,a15)
% 60.65/60.70 [67]P10(a12,a16)
% 60.65/60.70 [68]P10(a12,a17)
% 60.65/60.70 [69]P10(a13,a14)
% 60.65/60.70 [70]P10(a13,a15)
% 60.65/60.70 [71]P10(a13,a16)
% 60.65/60.70 [72]P10(a13,a17)
% 60.65/60.70 [73]P10(a14,a15)
% 60.65/60.70 [74]P10(a14,a16)
% 60.65/60.70 [75]P10(a14,a17)
% 60.65/60.70 [76]P10(a14,a5)
% 60.65/60.70 [77]P10(a15,a16)
% 60.65/60.70 [78]P10(a15,a17)
% 60.65/60.70 [79]P10(a16,a17)
% 60.65/60.70 [80]P11(a12,a10)
% 60.65/60.70 [81]P2(a6,a16,a16)
% 60.65/60.70 [82]P2(a6,a17,a17)
% 60.65/60.70 [83]P6(a10,a11,a13)
% 60.65/60.70 [84]P7(a5,a11,a15)
% 60.65/60.70 [85]~E(a1,a2)
% 60.65/60.70 [86]~E(a1,a4)
% 60.65/60.70 [87]~E(a4,a2)
% 60.65/60.70 [88]~E(a12,a11)
% 60.65/60.70 [89]~E(a13,a11)
% 60.65/60.70 [90]~E(a13,a12)
% 60.65/60.70 [91]~E(a14,a11)
% 60.65/60.70 [92]~E(a14,a12)
% 60.65/60.70 [93]~E(a14,a13)
% 60.65/60.70 [94]~E(a15,a11)
% 60.65/60.70 [95]~E(a15,a12)
% 60.65/60.70 [96]~E(a15,a13)
% 60.65/60.70 [97]~E(a15,a14)
% 60.65/60.70 [98]~E(a16,a11)
% 60.65/60.70 [99]~E(a16,a12)
% 60.65/60.70 [100]~E(a16,a13)
% 60.65/60.70 [101]~E(a16,a14)
% 60.65/60.70 [102]~E(a16,a15)
% 60.65/60.70 [103]~E(a17,a11)
% 60.65/60.70 [104]~E(a17,a12)
% 60.65/60.70 [105]~E(a17,a13)
% 60.65/60.70 [106]~E(a17,a14)
% 60.65/60.70 [107]~E(a17,a15)
% 60.65/60.70 [108]~E(a17,a16)
% 60.65/60.70 [109]~P10(x1091,x1091)
% 60.65/60.70 [111]~E(x1111,x1112)+P11(x1111,x1112)
% 60.65/60.70 [119]~P10(x1191,x1192)+P11(x1191,x1192)
% 60.65/60.70 [131]P10(x1311,x1312)+~P6(x1312,x1311,x1313)
% 60.65/60.70 [132]P10(x1321,x1322)+~P8(x1321,x1323,x1322)
% 60.65/60.70 [133]P10(x1331,x1332)+~P7(x1332,x1331,x1333)
% 60.65/60.70 [134]P10(x1341,x1342)+~P7(x1341,x1343,x1342)
% 60.65/60.70 [135]P11(x1351,x1352)+~P2(x1352,x1351,x1353)
% 60.65/60.70 [136]P11(x1361,x1362)+~P2(x1361,x1363,x1362)
% 60.65/60.70 [137]P11(x1371,x1372)+~P6(x1371,x1373,x1372)
% 60.65/60.70 [138]P11(x1381,x1382)+~P8(x1382,x1381,x1383)
% 60.65/60.70 [142]P5(x1421,x1422,x1423,x1424)+P2(f7(x1421,x1422,x1423,x1424),x1423,x1424)
% 60.65/60.70 [143]P5(x1431,x1432,x1433,x1434)+P2(f7(x1431,x1432,x1433,x1434),x1431,x1432)
% 60.65/60.70 [144]P4(x1441,x1442,x1443,x1444)+P2(f8(x1441,x1442,x1443,x1444),x1441,x1442)
% 60.65/60.70 [145]~P3(x1451,x1452,x1453,x1454)+P2(f9(x1451,x1452,x1453,x1454),x1453,x1454)
% 60.65/60.70 [146]~P3(x1461,x1462,x1463,x1464)+P2(f9(x1461,x1462,x1463,x1464),x1461,x1462)
% 60.65/60.70 [147]P4(x1471,x1472,x1473,x1474)+~P2(f8(x1471,x1472,x1473,x1474),x1473,x1474)
% 60.65/60.70 [112]P10(x1122,x1121)+P10(x1121,x1122)+E(x1121,x1122)
% 60.65/60.70 [120]P10(x1201,x1202)+~P11(x1201,x1202)+E(x1201,x1202)
% 60.65/60.70 [121]~P11(x1212,x1211)+~P11(x1211,x1212)+E(x1211,x1212)
% 60.65/60.71 [123]~P10(x1231,x1233)+P10(x1231,x1232)+~P10(x1233,x1232)
% 60.65/60.71 [124]~P11(x1241,x1243)+P10(x1241,x1242)+~P10(x1243,x1242)
% 60.65/60.71 [125]~P11(x1253,x1252)+P10(x1251,x1252)+~P10(x1251,x1253)
% 60.65/60.71 [126]~P11(x1261,x1263)+P11(x1261,x1262)+~P11(x1263,x1262)
% 60.65/60.71 [127]~P11(x1271,x1273)+~P11(x1272,x1271)+P2(x1271,x1272,x1273)
% 60.65/60.71 [128]~P10(x1282,x1281)+~P11(x1281,x1283)+P6(x1281,x1282,x1283)
% 60.65/60.71 [129]~P10(x1291,x1293)+~P11(x1292,x1291)+P8(x1291,x1292,x1293)
% 60.65/60.71 [130]~P10(x1301,x1303)+~P10(x1302,x1301)+P7(x1301,x1302,x1303)
% 60.65/60.71 [139]~P2(x1395,x1391,x1392)+P3(x1391,x1392,x1393,x1394)+~P2(x1395,x1393,x1394)
% 60.65/60.71 [140]~P4(x1404,x1405,x1402,x1403)+P2(x1401,x1402,x1403)+~P2(x1401,x1404,x1405)
% 60.65/60.71 [141]~P5(x1414,x1415,x1412,x1413)+~P2(x1411,x1412,x1413)+~P2(x1411,x1414,x1415)
% 60.65/60.71 [110]~P1(x1101)+E(x1101,a2)+E(x1101,a4)+E(x1101,a1)
% 60.65/60.71 [113]~P1(x1131)+~P1(x1132)+~E(x1132,a1)+E(f3(x1131,x1132),a1)
% 60.65/60.71 [114]~P1(x1142)+~P1(x1141)+~E(x1141,a1)+E(f3(x1141,x1142),a1)
% 60.65/60.71 [115]~P1(x1152)+~P1(x1151)+~E(x1152,a2)+~E(x1151,a2)+E(f3(x1151,x1152),a2)
% 60.65/60.71 [122]~P1(x1222)+~P1(x1221)+E(f3(x1221,x1222),a1)+E(f3(x1221,x1222),a2)+E(f3(x1221,x1222),a4)
% 60.65/60.71 [116]~P1(x1161)+~P1(x1162)+~E(x1162,a4)+E(x1161,a1)+E(x1162,a1)+E(f3(x1161,x1162),a4)
% 60.65/60.71 [117]~P1(x1171)+~P1(x1172)+~E(x1172,a4)+E(x1171,a1)+E(x1172,a1)+E(f3(x1172,x1171),a4)
% 60.65/60.71 %EqnAxiom
% 60.65/60.71 [1]E(x11,x11)
% 60.65/60.71 [2]E(x22,x21)+~E(x21,x22)
% 60.65/60.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.65/60.71 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 60.65/60.71 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 60.65/60.71 [6]~E(x61,x62)+E(f8(x61,x63,x64,x65),f8(x62,x63,x64,x65))
% 60.65/60.71 [7]~E(x71,x72)+E(f8(x73,x71,x74,x75),f8(x73,x72,x74,x75))
% 60.65/60.71 [8]~E(x81,x82)+E(f8(x83,x84,x81,x85),f8(x83,x84,x82,x85))
% 60.65/60.71 [9]~E(x91,x92)+E(f8(x93,x94,x95,x91),f8(x93,x94,x95,x92))
% 60.65/60.71 [10]~E(x101,x102)+E(f9(x101,x103,x104,x105),f9(x102,x103,x104,x105))
% 60.65/60.71 [11]~E(x111,x112)+E(f9(x113,x111,x114,x115),f9(x113,x112,x114,x115))
% 60.65/60.71 [12]~E(x121,x122)+E(f9(x123,x124,x121,x125),f9(x123,x124,x122,x125))
% 60.65/60.71 [13]~E(x131,x132)+E(f9(x133,x134,x135,x131),f9(x133,x134,x135,x132))
% 60.65/60.71 [14]~E(x141,x142)+E(f7(x141,x143,x144,x145),f7(x142,x143,x144,x145))
% 60.65/60.71 [15]~E(x151,x152)+E(f7(x153,x151,x154,x155),f7(x153,x152,x154,x155))
% 60.65/60.71 [16]~E(x161,x162)+E(f7(x163,x164,x161,x165),f7(x163,x164,x162,x165))
% 60.65/60.71 [17]~E(x171,x172)+E(f7(x173,x174,x175,x171),f7(x173,x174,x175,x172))
% 60.65/60.71 [18]~P1(x181)+P1(x182)+~E(x181,x182)
% 60.65/60.71 [19]P2(x192,x193,x194)+~E(x191,x192)+~P2(x191,x193,x194)
% 60.65/60.71 [20]P2(x203,x202,x204)+~E(x201,x202)+~P2(x203,x201,x204)
% 60.65/60.71 [21]P2(x213,x214,x212)+~E(x211,x212)+~P2(x213,x214,x211)
% 60.65/60.71 [22]P4(x222,x223,x224,x225)+~E(x221,x222)+~P4(x221,x223,x224,x225)
% 60.65/60.71 [23]P4(x233,x232,x234,x235)+~E(x231,x232)+~P4(x233,x231,x234,x235)
% 60.65/60.71 [24]P4(x243,x244,x242,x245)+~E(x241,x242)+~P4(x243,x244,x241,x245)
% 60.65/60.71 [25]P4(x253,x254,x255,x252)+~E(x251,x252)+~P4(x253,x254,x255,x251)
% 60.65/60.71 [26]~P9(x261)+P9(x262)+~E(x261,x262)
% 60.65/60.71 [27]P8(x272,x273,x274)+~E(x271,x272)+~P8(x271,x273,x274)
% 60.65/60.71 [28]P8(x283,x282,x284)+~E(x281,x282)+~P8(x283,x281,x284)
% 60.65/60.71 [29]P8(x293,x294,x292)+~E(x291,x292)+~P8(x293,x294,x291)
% 60.65/60.71 [30]P10(x302,x303)+~E(x301,x302)+~P10(x301,x303)
% 60.65/60.71 [31]P10(x313,x312)+~E(x311,x312)+~P10(x313,x311)
% 60.65/60.71 [32]P6(x322,x323,x324)+~E(x321,x322)+~P6(x321,x323,x324)
% 60.65/60.71 [33]P6(x333,x332,x334)+~E(x331,x332)+~P6(x333,x331,x334)
% 60.65/60.71 [34]P6(x343,x344,x342)+~E(x341,x342)+~P6(x343,x344,x341)
% 60.65/60.71 [35]P11(x352,x353)+~E(x351,x352)+~P11(x351,x353)
% 60.65/60.71 [36]P11(x363,x362)+~E(x361,x362)+~P11(x363,x361)
% 60.65/60.71 [37]P7(x372,x373,x374)+~E(x371,x372)+~P7(x371,x373,x374)
% 60.65/60.71 [38]P7(x383,x382,x384)+~E(x381,x382)+~P7(x383,x381,x384)
% 60.65/60.71 [39]P7(x393,x394,x392)+~E(x391,x392)+~P7(x393,x394,x391)
% 60.65/60.71 [40]P5(x402,x403,x404,x405)+~E(x401,x402)+~P5(x401,x403,x404,x405)
% 60.65/60.71 [41]P5(x413,x412,x414,x415)+~E(x411,x412)+~P5(x413,x411,x414,x415)
% 60.65/60.71 [42]P5(x423,x424,x422,x425)+~E(x421,x422)+~P5(x423,x424,x421,x425)
% 60.65/60.71 [43]P5(x433,x434,x435,x432)+~E(x431,x432)+~P5(x433,x434,x435,x431)
% 60.65/60.71 [44]P3(x442,x443,x444,x445)+~E(x441,x442)+~P3(x441,x443,x444,x445)
% 60.65/60.71 [45]P3(x453,x452,x454,x455)+~E(x451,x452)+~P3(x453,x451,x454,x455)
% 60.65/60.71 [46]P3(x463,x464,x462,x465)+~E(x461,x462)+~P3(x463,x464,x461,x465)
% 60.65/60.71 [47]P3(x473,x474,x475,x472)+~E(x471,x472)+~P3(x473,x474,x475,x471)
% 60.65/60.71
% 60.65/60.71 %-------------------------------------------
% 60.65/60.71 cnf(148,plain,
% 60.65/60.71 (P11(x1481,x1481)),
% 60.65/60.71 inference(equality_inference,[],[111])).
% 60.65/60.71 cnf(149,plain,
% 60.65/60.71 (~P1(x1491)+~P1(a1)+E(f3(x1491,a1),a1)),
% 60.65/60.71 inference(equality_inference,[],[113])).
% 60.65/60.71 cnf(150,plain,
% 60.65/60.71 (~P1(x1501)+~P1(a1)+E(f3(a1,x1501),a1)),
% 60.65/60.71 inference(equality_inference,[],[114])).
% 60.65/60.71 cnf(151,plain,
% 60.65/60.71 (~P1(x1511)+~P1(a4)+E(x1511,a1)+E(a4,a1)+E(f3(x1511,a4),a4)),
% 60.65/60.71 inference(equality_inference,[],[116])).
% 60.65/60.71 cnf(153,plain,
% 60.65/60.71 (~P1(x1531)+E(f3(x1531,a1),a1)),
% 60.65/60.71 inference(scs_inference,[],[48,149])).
% 60.65/60.71 cnf(154,plain,
% 60.65/60.71 (~P1(x1541)+E(f3(a1,x1541),a1)),
% 60.65/60.71 inference(scs_inference,[],[48,150])).
% 60.65/60.71 cnf(155,plain,
% 60.65/60.71 (~P1(x1551)+E(x1551,a1)+E(a4,a1)+E(f3(x1551,a4),a4)),
% 60.65/60.71 inference(scs_inference,[],[50,151])).
% 60.65/60.71 cnf(157,plain,
% 60.65/60.71 (~P6(x1571,x1571,x1572)),
% 60.65/60.71 inference(scs_inference,[],[109,131])).
% 60.65/60.71 cnf(159,plain,
% 60.65/60.71 (~P7(x1591,x1591,x1592)),
% 60.65/60.71 inference(scs_inference,[],[109,131,133])).
% 60.65/60.71 cnf(161,plain,
% 60.65/60.71 (~P7(x1611,x1612,x1611)),
% 60.65/60.71 inference(scs_inference,[],[109,131,133,134])).
% 60.65/60.71 cnf(163,plain,
% 60.65/60.71 (~P8(x1631,x1632,x1631)),
% 60.65/60.71 inference(scs_inference,[],[109,131,133,134,132])).
% 60.65/60.71 cnf(165,plain,
% 60.65/60.71 (P10(a11,a5)),
% 60.65/60.71 inference(scs_inference,[],[76,109,60,131,133,134,132,123])).
% 60.65/60.71 cnf(167,plain,
% 60.65/60.71 (P10(a11,a10)),
% 60.65/60.71 inference(scs_inference,[],[76,80,58,109,60,131,133,134,132,123,125])).
% 60.65/60.71 cnf(169,plain,
% 60.65/60.71 (P3(a16,a16,a16,a16)),
% 60.65/60.71 inference(scs_inference,[],[76,80,81,58,109,60,131,133,134,132,123,125,139])).
% 60.65/60.71 cnf(171,plain,
% 60.65/60.71 (~P5(a16,a16,a16,a16)),
% 60.65/60.71 inference(scs_inference,[],[76,80,81,58,109,60,131,133,134,132,123,125,139,141])).
% 60.65/60.71 cnf(174,plain,
% 60.65/60.71 (~P10(x1741,x1741)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(175,plain,
% 60.65/60.71 (~E(a5,a14)),
% 60.65/60.71 inference(scs_inference,[],[76,80,81,58,109,174,60,131,133,134,132,123,125,139,141,30,31])).
% 60.65/60.71 cnf(178,plain,
% 60.65/60.71 (~E(a15,a5)),
% 60.65/60.71 inference(scs_inference,[],[76,80,81,84,58,109,174,60,131,133,134,132,123,125,139,141,30,31,38,39])).
% 60.65/60.71 cnf(191,plain,
% 60.65/60.71 (P10(a12,a5)),
% 60.65/60.71 inference(scs_inference,[],[76,84,159,65,37,123])).
% 60.65/60.71 cnf(193,plain,
% 60.65/60.71 (P3(a17,a17,a17,a17)),
% 60.65/60.71 inference(scs_inference,[],[76,82,84,159,65,37,123,139])).
% 60.65/60.71 cnf(215,plain,
% 60.65/60.71 (P10(a13,a5)),
% 60.65/60.71 inference(scs_inference,[],[76,69,123])).
% 60.65/60.71 cnf(220,plain,
% 60.65/60.71 (~P10(x2201,x2201)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(224,plain,
% 60.65/60.71 (P3(a17,a17,x2241,a17)+~E(a17,x2241)),
% 60.65/60.71 inference(scs_inference,[],[76,80,84,161,191,193,69,109,220,123,37,30,31,36,46])).
% 60.65/60.71 cnf(225,plain,
% 60.65/60.71 (P3(a17,a17,a17,x2251)+~E(a17,x2251)),
% 60.65/60.71 inference(scs_inference,[],[76,80,84,161,191,193,69,109,220,123,37,30,31,36,46,47])).
% 60.65/60.71 cnf(228,plain,
% 60.65/60.71 (P3(x2281,a17,a17,a17)+~E(a17,x2281)),
% 60.65/60.71 inference(scs_inference,[],[76,80,84,82,161,191,193,69,109,220,123,37,30,31,36,46,47,140,44])).
% 60.65/60.71 cnf(229,plain,
% 60.65/60.71 (P2(a6,x2291,a17)+~E(a17,x2291)),
% 60.65/60.71 inference(scs_inference,[],[76,80,84,82,161,191,193,69,109,220,123,37,30,31,36,46,47,140,44,20])).
% 60.65/60.71 cnf(235,plain,
% 60.65/60.71 (~P10(a12,a11)),
% 60.65/60.71 inference(scs_inference,[],[58,109,123])).
% 60.65/60.71 cnf(236,plain,
% 60.65/60.71 (~P10(x2361,x2361)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(248,plain,
% 60.65/60.71 (P2(x2481,a17,a17)+~E(a6,x2481)),
% 60.65/60.71 inference(scs_inference,[],[82,58,215,109,236,123,30,132,134,133,131,19])).
% 60.65/60.71 cnf(249,plain,
% 60.65/60.71 (P4(x2491,x2492,a17,a17)+~E(a6,f8(x2491,x2492,a17,a17))),
% 60.65/60.71 inference(scs_inference,[],[82,58,215,109,236,123,30,132,134,133,131,19,147])).
% 60.65/60.71 cnf(254,plain,
% 60.65/60.71 (~P10(x2541,x2541)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(266,plain,
% 60.65/60.71 (P2(a6,a17,x2661)+~E(a17,x2661)),
% 60.65/60.71 inference(scs_inference,[],[82,167,59,109,254,123,30,134,132,133,131,21])).
% 60.65/60.71 cnf(267,plain,
% 60.65/60.71 (~P5(a17,x2671,a17,a17)+~E(a17,x2671)),
% 60.65/60.71 inference(scs_inference,[],[82,167,59,109,254,123,30,134,132,133,131,21,141])).
% 60.65/60.71 cnf(274,plain,
% 60.65/60.71 (~P10(x2741,x2741)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(286,plain,
% 60.65/60.71 (P3(a16,a16,a16,x2861)+~E(a16,x2861)),
% 60.65/60.71 inference(scs_inference,[],[165,169,61,109,274,123,30,132,134,133,131,47])).
% 60.65/60.71 cnf(287,plain,
% 60.65/60.71 (P3(a16,a16,x2871,a16)+~E(a16,x2871)),
% 60.65/60.71 inference(scs_inference,[],[165,169,61,109,274,123,30,132,134,133,131,47,46])).
% 60.65/60.71 cnf(290,plain,
% 60.65/60.71 (~P5(x2901,x2902,a16,a16)+~P4(a16,a16,x2901,x2902)),
% 60.65/60.71 inference(scs_inference,[],[81,165,169,61,109,274,123,30,132,134,133,131,47,46,140,141])).
% 60.65/60.71 cnf(295,plain,
% 60.65/60.71 (~P10(a16,a11)),
% 60.65/60.71 inference(scs_inference,[],[62,109,123])).
% 60.65/60.71 cnf(296,plain,
% 60.65/60.71 (~P10(x2961,x2961)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(300,plain,
% 60.65/60.71 (~P7(a16,x3001,a11)),
% 60.65/60.71 inference(scs_inference,[],[62,109,296,123,30,134])).
% 60.65/60.71 cnf(302,plain,
% 60.65/60.71 (~P8(a16,x3021,a11)),
% 60.65/60.71 inference(scs_inference,[],[62,109,296,123,30,134,132])).
% 60.65/60.71 cnf(308,plain,
% 60.65/60.71 (P2(a6,a16,x3081)+~E(a16,x3081)),
% 60.65/60.71 inference(scs_inference,[],[81,62,109,296,123,30,134,132,133,131,21])).
% 60.65/60.71 cnf(309,plain,
% 60.65/60.71 (~P5(a16,x3091,a17,a17)+~E(a16,x3091)),
% 60.65/60.71 inference(scs_inference,[],[82,81,62,109,296,123,30,134,132,133,131,21,141])).
% 60.65/60.71 cnf(311,plain,
% 60.65/60.71 (P3(a17,a17,a16,x3111)+~E(a16,x3111)),
% 60.65/60.71 inference(scs_inference,[],[82,81,62,109,296,123,30,134,132,133,131,21,141,139])).
% 60.65/60.71 cnf(316,plain,
% 60.65/60.71 (~P5(a16,a16,a17,a17)),
% 60.65/60.71 inference(equality_inference,[],[309])).
% 60.65/60.71 cnf(317,plain,
% 60.65/60.71 (P3(a17,a17,a16,a16)),
% 60.65/60.71 inference(equality_inference,[],[311])).
% 60.65/60.71 cnf(319,plain,
% 60.65/60.71 (~P10(x3191,x3191)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(331,plain,
% 60.65/60.71 (P2(a6,x3311,a16)+~E(a16,x3311)),
% 60.65/60.71 inference(scs_inference,[],[81,63,109,319,123,30,132,134,133,131,20])).
% 60.65/60.71 cnf(332,plain,
% 60.65/60.71 (~P5(x3321,a16,a17,a17)+~E(a16,x3321)),
% 60.65/60.71 inference(scs_inference,[],[82,81,63,109,319,123,30,132,134,133,131,20,141])).
% 60.65/60.71 cnf(334,plain,
% 60.65/60.71 (P3(a17,a17,x3341,a16)+~E(a16,x3341)),
% 60.65/60.71 inference(scs_inference,[],[82,81,63,109,319,123,30,132,134,133,131,20,141,139])).
% 60.65/60.71 cnf(342,plain,
% 60.65/60.71 (~P10(x3421,x3421)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(354,plain,
% 60.65/60.71 (P3(a17,x3541,a17,a17)+~E(a17,x3541)),
% 60.65/60.71 inference(scs_inference,[],[193,64,59,109,342,123,30,134,132,133,131,45])).
% 60.65/60.71 cnf(360,plain,
% 60.65/60.71 (~P10(x3601,x3601)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(373,plain,
% 60.65/60.71 (P3(x3731,a17,a16,a16)+~E(a17,x3731)),
% 60.65/60.71 inference(scs_inference,[],[83,317,68,61,109,360,123,30,132,134,133,131,34,44])).
% 60.65/60.71 cnf(374,plain,
% 60.65/60.71 (P11(x3741,a10)+~E(a12,x3741)),
% 60.65/60.71 inference(scs_inference,[],[83,80,317,68,61,109,360,123,30,132,134,133,131,34,44,35])).
% 60.65/60.71 cnf(382,plain,
% 60.65/60.71 (~P10(x3821,x3821)),
% 60.65/60.71 inference(rename_variables,[],[109])).
% 60.65/60.71 cnf(394,plain,
% 60.65/60.71 (P3(a17,x3941,a16,a16)+~E(a17,x3941)),
% 60.65/60.71 inference(scs_inference,[],[317,67,60,109,382,123,30,134,132,133,131,45])).
% 60.65/60.71 cnf(401,plain,
% 60.65/60.71 (P3(x4011,a16,a16,a16)+~E(a16,x4011)),
% 60.65/60.71 inference(scs_inference,[],[169,66,109,30,44])).
% 60.65/60.71 cnf(402,plain,
% 60.65/60.71 (P11(x4021,x4022)+~E(x4022,x4021)),
% 60.65/60.71 inference(scs_inference,[],[169,148,66,109,30,44,35])).
% 60.65/60.71 cnf(410,plain,
% 60.65/60.71 (~E(a13,a17)),
% 60.65/60.71 inference(scs_inference,[],[72,109,30])).
% 60.65/60.71 cnf(419,plain,
% 60.65/60.71 (P3(a16,x4191,a16,a16)+~E(a16,x4191)),
% 60.65/60.71 inference(scs_inference,[],[169,71,109,30,45])).
% 60.65/60.71 cnf(426,plain,
% 60.65/60.71 (~E(a14,a17)),
% 60.65/60.71 inference(scs_inference,[],[75,109,30])).
% 60.65/60.71 cnf(447,plain,
% 60.65/60.71 (~P11(a5,a14)),
% 60.65/60.71 inference(scs_inference,[],[76,175,119,121])).
% 60.65/60.71 cnf(450,plain,
% 60.65/60.71 (~P2(a14,a5,x4501)),
% 60.65/60.71 inference(scs_inference,[],[447,119,135])).
% 60.65/60.71 cnf(473,plain,
% 60.65/60.71 (~E(a1,x4731)+E(f3(x4731,a1),a1)),
% 60.65/60.71 inference(scs_inference,[],[48,153,18])).
% 60.65/60.71 cnf(474,plain,
% 60.65/60.71 (E(f3(a1,a1),a1)),
% 60.65/60.71 inference(equality_inference,[],[473])).
% 60.65/60.71 cnf(475,plain,
% 60.65/60.71 (P11(a1,f3(a1,a1))),
% 60.65/60.71 inference(scs_inference,[],[474,402])).
% 60.65/60.71 cnf(476,plain,
% 60.65/60.71 (E(a1,f3(a1,a1))),
% 60.65/60.71 inference(scs_inference,[],[474,402,2])).
% 60.65/60.71 cnf(477,plain,
% 60.65/60.71 (P1(f3(a1,a1))),
% 60.65/60.71 inference(scs_inference,[],[474,48,402,2,18])).
% 60.65/60.71 cnf(480,plain,
% 60.65/60.71 (P11(f3(a1,a1),a1)),
% 60.65/60.71 inference(scs_inference,[],[476,402])).
% 60.65/60.71 cnf(493,plain,
% 60.65/60.71 (E(a1,f3(a1,f3(a1,a1)))),
% 60.65/60.71 inference(scs_inference,[],[477,154,2])).
% 60.65/60.71 cnf(495,plain,
% 60.65/60.71 (E(f3(a1,f3(a1,a1)),a1)),
% 60.65/60.71 inference(scs_inference,[],[493,402,2])).
% 60.65/60.71 cnf(496,plain,
% 60.65/60.71 (E(f3(a1,a1),f3(a1,f3(a1,a1)))),
% 60.65/60.71 inference(scs_inference,[],[474,493,402,2,3])).
% 60.65/60.71 cnf(582,plain,
% 60.65/60.71 (E(f3(a1,x5821),f3(f3(a1,a1),x5821))),
% 60.65/60.71 inference(scs_inference,[],[474,4,2])).
% 60.65/60.71 cnf(603,plain,
% 60.65/60.71 (~P5(a17,a17,a16,a16)+~E(a6,f8(a16,a16,a17,a17))),
% 60.65/60.71 inference(scs_inference,[],[290,249])).
% 60.65/60.71 cnf(625,plain,
% 60.65/60.71 (~E(f8(a16,a16,a17,a17),a6)+~P5(a17,a17,a16,a16)),
% 60.65/60.71 inference(scs_inference,[],[603,2])).
% 60.65/60.71 cnf(630,plain,
% 60.65/60.71 (~E(x6301,a6)+~E(f8(a16,a16,a17,a17),x6301)+~P5(a17,a17,a16,a16)),
% 60.65/60.71 inference(scs_inference,[],[625,3])).
% 60.65/60.72 cnf(631,plain,
% 60.65/60.72 (P2(f7(a17,a17,a17,a17),a17,a17)),
% 60.65/60.72 inference(scs_inference,[],[82,142,141])).
% 60.65/60.72 cnf(653,plain,
% 60.65/60.72 (E(f3(a1,a1),f3(f3(a1,a1),f3(a1,a1)))),
% 60.65/60.72 inference(scs_inference,[],[496,582,3])).
% 60.65/60.72 cnf(655,plain,
% 60.65/60.72 (E(f3(f3(a1,a1),f3(a1,a1)),f3(a1,a1))),
% 60.65/60.72 inference(scs_inference,[],[496,582,3,2])).
% 60.65/60.72 cnf(662,plain,
% 60.65/60.72 (~P5(a5,a17,a5,a17)+~E(a17,a5)),
% 60.65/60.72 inference(scs_inference,[],[82,450,496,582,631,3,2,402,20,19,139,140,141])).
% 60.65/60.72 cnf(673,plain,
% 60.65/60.72 (P2(x6731,a17,a17)+~E(f7(a17,a17,a17,a17),x6731)),
% 60.65/60.72 inference(scs_inference,[],[475,476,655,653,631,402,126,3,2,19])).
% 60.65/60.72 cnf(686,plain,
% 60.65/60.72 (~E(a5,a17)+~P5(a5,a17,a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[662,2])).
% 60.65/60.72 cnf(688,plain,
% 60.65/60.72 (~P11(a5,a17)+P10(a5,a17)+~P5(a5,a17,a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[686,120])).
% 60.65/60.72 cnf(693,plain,
% 60.65/60.72 (P11(a16,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[171,143,135])).
% 60.65/60.72 cnf(696,plain,
% 60.65/60.72 (P10(a11,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[58,693,67,125,123])).
% 60.65/60.72 cnf(719,plain,
% 60.65/60.72 (P2(f9(a17,a17,a17,a17),a17,a17)),
% 60.65/60.72 inference(scs_inference,[],[82,146,139])).
% 60.65/60.72 cnf(720,plain,
% 60.65/60.72 (P10(a13,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[693,71,125])).
% 60.65/60.72 cnf(723,plain,
% 60.65/60.72 (~P10(x7231,x7231)),
% 60.65/60.72 inference(rename_variables,[],[109])).
% 60.65/60.72 cnf(727,plain,
% 60.65/60.72 (~P7(f7(a16,a16,a16,a16),x7271,a11)),
% 60.65/60.72 inference(scs_inference,[],[693,696,71,109,723,125,123,30,134])).
% 60.65/60.72 cnf(745,plain,
% 60.65/60.72 (P10(a14,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[693,74,125])).
% 60.65/60.72 cnf(756,plain,
% 60.65/60.72 (P3(a17,a17,a16,f7(a16,a16,a16,a16))+~P11(f7(a16,a16,a16,a16),a16)),
% 60.65/60.72 inference(scs_inference,[],[317,81,169,693,720,74,109,125,30,121,21,20,46,44,45,47])).
% 60.65/60.72 cnf(766,plain,
% 60.65/60.72 (P10(a15,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[693,77,125])).
% 60.65/60.72 cnf(768,plain,
% 60.65/60.72 (~E(a14,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[693,745,77,109,125,30])).
% 60.65/60.72 cnf(785,plain,
% 60.65/60.72 (P11(a16,x7851)+~E(f7(a16,a16,a16,a16),x7851)),
% 60.65/60.72 inference(scs_inference,[],[693,36])).
% 60.65/60.72 cnf(799,plain,
% 60.65/60.72 (P2(x7991,a17,a17)+~E(f9(a17,a17,a17,a17),x7991)),
% 60.65/60.72 inference(scs_inference,[],[719,19])).
% 60.65/60.72 cnf(881,plain,
% 60.65/60.72 (~P2(f7(a16,a16,a16,a16),x8811,a16)+P3(a17,a17,a16,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[756,136])).
% 60.65/60.72 cnf(914,plain,
% 60.65/60.72 (P2(f9(a17,a17,a16,f7(a16,a16,a16,a16)),a17,a17)+~P2(f7(a16,a16,a16,a16),x9141,a16)),
% 60.65/60.72 inference(scs_inference,[],[881,146])).
% 60.65/60.72 cnf(1153,plain,
% 60.65/60.72 (P2(f7(a5,a17,a5,a17),a5,a17)+~P11(a5,a17)+P10(a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[688,142])).
% 60.65/60.72 cnf(1165,plain,
% 60.65/60.72 (P4(x11651,x11652,f3(a1,f3(a1,a1)),x11653)+~E(f3(a1,a1),f3(a1,f3(a1,a1)))+P2(f8(x11651,x11652,f3(a1,a1),x11653),x11651,x11652)),
% 60.65/60.72 inference(scs_inference,[],[496,24,144])).
% 60.65/60.72 cnf(1166,plain,
% 60.65/60.72 (P2(f8(x11661,x11662,f3(a1,a1),x11663),x11661,x11662)+P4(x11661,x11662,f3(a1,f3(a1,a1)),x11663)),
% 60.65/60.72 inference(scs_inference,[],[496,1165])).
% 60.65/60.72 cnf(1196,plain,
% 60.65/60.72 (~E(x11961,a16)+P2(f7(a16,x11961,a17,a17),a16,x11961)),
% 60.65/60.72 inference(scs_inference,[],[316,41,143])).
% 60.65/60.72 cnf(1197,plain,
% 60.65/60.72 (P2(f7(a16,a16,a17,a17),a16,a16)),
% 60.65/60.72 inference(equality_inference,[],[1196])).
% 60.65/60.72 cnf(1213,plain,
% 60.65/60.72 (P3(a5,a16,a5,a16)+~E(a16,a5)),
% 60.65/60.72 inference(scs_inference,[],[450,1197,20,19,139])).
% 60.65/60.72 cnf(1221,plain,
% 60.65/60.72 (~E(a5,a16)+P3(a5,a16,a5,a16)),
% 60.65/60.72 inference(scs_inference,[],[1213,2])).
% 60.65/60.72 cnf(1224,plain,
% 60.65/60.72 (~P5(a16,x12241,a16,a16)+~E(a16,x12241)),
% 60.65/60.72 inference(scs_inference,[],[1197,21,140,141])).
% 60.65/60.72 cnf(1231,plain,
% 60.65/60.72 (P2(x12311,a16,a16)+~E(f7(a16,a16,a17,a17),x12311)),
% 60.65/60.72 inference(scs_inference,[],[1197,19])).
% 60.65/60.72 cnf(1239,plain,
% 60.65/60.72 (~E(x12391,a16)+~E(a5,x12391)+P3(a5,a16,a5,a16)),
% 60.65/60.72 inference(scs_inference,[],[1221,3])).
% 60.65/60.72 cnf(1293,plain,
% 60.65/60.72 (~E(x12931,a16)+P2(f7(a16,a16,x12931,a16),x12931,a16)),
% 60.65/60.72 inference(scs_inference,[],[171,42,142])).
% 60.65/60.72 cnf(1294,plain,
% 60.65/60.72 (P2(f7(a16,a16,a16,a16),a16,a16)),
% 60.65/60.72 inference(equality_inference,[],[1293])).
% 60.65/60.72 cnf(1295,plain,
% 60.65/60.72 (P3(a17,a17,a16,f7(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[1294,881])).
% 60.65/60.72 cnf(1296,plain,
% 60.65/60.72 (P2(f9(a17,a17,a16,f7(a16,a16,a16,a16)),a17,a17)),
% 60.65/60.72 inference(scs_inference,[],[1294,914])).
% 60.65/60.72 cnf(1299,plain,
% 60.65/60.72 (P2(f7(a16,a16,a16,a16),f3(a1,f3(a1,a1)),x12991)+~P4(a16,a16,f3(a1,a1),x12991)),
% 60.65/60.72 inference(scs_inference,[],[496,1294,140,20])).
% 60.65/60.72 cnf(1315,plain,
% 60.65/60.72 (~P5(x13151,a16,a16,a16)+~E(a16,x13151)),
% 60.65/60.72 inference(scs_inference,[],[1294,20,140,141])).
% 60.65/60.72 cnf(1337,plain,
% 60.65/60.72 (P3(a17,x13371,a16,f7(a16,a16,a16,a16))+~E(a17,x13371)),
% 60.65/60.72 inference(scs_inference,[],[1295,45])).
% 60.65/60.72 cnf(1339,plain,
% 60.65/60.72 (P3(a17,a17,x13391,f7(a16,a16,a16,a16))+~E(a16,x13391)),
% 60.65/60.72 inference(scs_inference,[],[1296,1295,45,21,46])).
% 60.65/60.72 cnf(1340,plain,
% 60.65/60.72 (P3(x13401,a17,a16,f7(a16,a16,a16,a16))+~E(a17,x13401)),
% 60.65/60.72 inference(scs_inference,[],[1296,1295,45,21,46,44])).
% 60.65/60.72 cnf(1341,plain,
% 60.65/60.72 (P3(a17,a17,a16,x13411)+~E(f7(a16,a16,a16,a16),x13411)),
% 60.65/60.72 inference(scs_inference,[],[1296,1295,45,21,46,44,47])).
% 60.65/60.72 cnf(1342,plain,
% 60.65/60.72 (P2(x13421,a16,a16)+~E(f7(a16,a16,a16,a16),x13421)),
% 60.65/60.72 inference(scs_inference,[],[1294,1296,1295,45,21,46,44,47,19])).
% 60.65/60.72 cnf(1375,plain,
% 60.65/60.72 (P11(f7(a16,a16,a16,a16),x13751)+~P4(a16,a16,f3(a1,a1),x13751)),
% 60.65/60.72 inference(scs_inference,[],[1299,136])).
% 60.65/60.72 cnf(1426,plain,
% 60.65/60.72 (~E(a5,a17)+P10(a5,a17)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[1153,111])).
% 60.65/60.72 cnf(1433,plain,
% 60.65/60.72 (P10(a5,a17)+P10(a17,a5)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[1426,112])).
% 60.65/60.72 cnf(1435,plain,
% 60.65/60.72 (P6(a17,a5,a17)+P10(a17,a5)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[148,1433,128])).
% 60.65/60.72 cnf(1436,plain,
% 60.65/60.72 (~E(f8(a16,a16,a17,a17),x14361)+P2(f7(a17,a17,a16,a16),a16,a16)+~E(x14361,a6)),
% 60.65/60.72 inference(scs_inference,[],[630,142])).
% 60.65/60.72 cnf(1446,plain,
% 60.65/60.72 (P8(a17,a17,a5)+P6(a17,a5,a17)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[148,1435,129])).
% 60.65/60.72 cnf(1462,plain,
% 60.65/60.72 (~E(a17,a5)+P6(a17,a5,a17)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[163,1446,27])).
% 60.65/60.72 cnf(1463,plain,
% 60.65/60.72 (~E(a5,a17)+P6(a17,a5,a17)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[1462,2])).
% 60.65/60.72 cnf(1464,plain,
% 60.65/60.72 (~E(a5,a17)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[157,1463,33])).
% 60.65/60.72 cnf(1465,plain,
% 60.65/60.72 (~E(a17,a5)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[1464,2])).
% 60.65/60.72 cnf(1466,plain,
% 60.65/60.72 (~E(x14661,a5)+~E(a17,x14661)+P2(f7(a5,a17,a5,a17),a5,a17)),
% 60.65/60.72 inference(scs_inference,[],[1465,3])).
% 60.65/60.72 cnf(1467,plain,
% 60.65/60.72 (P3(a5,a17,a5,a17)+~E(a17,x14671)+~E(x14671,a5)),
% 60.65/60.72 inference(scs_inference,[],[1466,139])).
% 60.65/60.72 cnf(1495,plain,
% 60.65/60.72 (~E(f8(a16,a16,a17,a17),a6)+P2(f7(a17,a17,a16,a16),a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[148,109,1436,120])).
% 60.65/60.72 cnf(1496,plain,
% 60.65/60.72 (~E(a6,f8(a16,a16,a17,a17))+P2(f7(a17,a17,a16,a16),a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[1495,2])).
% 60.65/60.72 cnf(1497,plain,
% 60.65/60.72 (~E(x14971,f8(a16,a16,a17,a17))+~E(a6,x14971)+P2(f7(a17,a17,a16,a16),a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[1496,3])).
% 60.65/60.72 cnf(1618,plain,
% 60.65/60.72 (~P2(a11,f7(a16,a16,a16,a16),x16181)),
% 60.65/60.72 inference(scs_inference,[],[696,109,125,137,135])).
% 60.65/60.72 cnf(1624,plain,
% 60.65/60.72 (~P4(a16,a16,x16241,a11)),
% 60.65/60.72 inference(scs_inference,[],[696,109,1294,125,137,135,138,136,140])).
% 60.65/60.72 cnf(1626,plain,
% 60.65/60.72 (P2(f8(a16,a16,f3(a1,a1),a11),a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[696,109,1294,125,137,135,138,136,140,1166])).
% 60.65/60.72 cnf(1634,plain,
% 60.65/60.72 (~P11(a16,a11)),
% 60.65/60.72 inference(scs_inference,[],[235,67,125])).
% 60.65/60.72 cnf(1636,plain,
% 60.65/60.72 (~P2(a11,a16,x16361)),
% 60.65/60.72 inference(scs_inference,[],[235,67,125,135])).
% 60.65/60.72 cnf(1638,plain,
% 60.65/60.72 (~P6(a16,x16381,a11)),
% 60.65/60.72 inference(scs_inference,[],[235,67,125,135,137])).
% 60.65/60.72 cnf(1640,plain,
% 60.65/60.72 (~P8(a11,a16,x16401)),
% 60.65/60.72 inference(scs_inference,[],[235,67,125,135,137,138])).
% 60.65/60.72 cnf(1642,plain,
% 60.65/60.72 (~P2(a16,x16421,a11)),
% 60.65/60.72 inference(scs_inference,[],[235,67,125,135,137,138,136])).
% 60.65/60.72 cnf(1646,plain,
% 60.65/60.72 (~E(a6,a11)),
% 60.65/60.72 inference(scs_inference,[],[81,235,67,1626,125,135,137,138,136,140,19])).
% 60.65/60.72 cnf(1678,plain,
% 60.65/60.72 (~P2(a11,a17,x16781)),
% 60.65/60.72 inference(scs_inference,[],[235,68,125,135])).
% 60.65/60.72 cnf(1682,plain,
% 60.65/60.72 (~P8(a11,a17,x16821)),
% 60.65/60.72 inference(scs_inference,[],[235,68,125,135,137,138])).
% 60.65/60.72 cnf(1716,plain,
% 60.65/60.72 (~E(f7(a17,a17,a17,a17),a11)),
% 60.65/60.72 inference(scs_inference,[],[1678,673])).
% 60.65/60.72 cnf(1717,plain,
% 60.65/60.72 (~P2(a11,a17,x17171)),
% 60.65/60.72 inference(rename_variables,[],[1678])).
% 60.65/60.72 cnf(1718,plain,
% 60.65/60.72 (~E(f9(a17,a17,a17,a17),a11)),
% 60.65/60.72 inference(scs_inference,[],[1678,1717,673,799])).
% 60.65/60.72 cnf(1734,plain,
% 60.65/60.72 (~P2(a11,a14,x17341)),
% 60.65/60.72 inference(scs_inference,[],[235,65,125,135])).
% 60.65/60.72 cnf(1738,plain,
% 60.65/60.72 (~P2(a14,x17381,a11)),
% 60.65/60.72 inference(scs_inference,[],[235,65,125,135,137,136])).
% 60.65/60.72 cnf(1863,plain,
% 60.65/60.72 (E(a1,f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[50,2,153])).
% 60.65/60.72 cnf(1864,plain,
% 60.65/60.72 (E(f3(a4,a1),a1)),
% 60.65/60.72 inference(scs_inference,[],[1863,2])).
% 60.65/60.72 cnf(1865,plain,
% 60.65/60.72 (P11(f3(a4,a1),a1)),
% 60.65/60.72 inference(scs_inference,[],[1863,2,402])).
% 60.65/60.72 cnf(1866,plain,
% 60.65/60.72 (E(f3(a1,f3(a1,a1)),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[495,1863,2,402,3])).
% 60.65/60.72 cnf(1868,plain,
% 60.65/60.72 (P11(f3(a4,a1),f3(a1,a1))),
% 60.65/60.72 inference(scs_inference,[],[495,476,1863,48,2,402,3,18,36])).
% 60.65/60.72 cnf(1876,plain,
% 60.65/60.72 (P11(a1,f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[1864,1866,2,402])).
% 60.65/60.72 cnf(1877,plain,
% 60.65/60.72 (P11(f3(a1,a1),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[480,1864,1866,2,402,126])).
% 60.65/60.72 cnf(1879,plain,
% 60.65/60.72 (E(f3(a1,a1),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[480,496,1864,1866,2,402,126,3])).
% 60.65/60.72 cnf(1880,plain,
% 60.65/60.72 (E(f3(a4,a1),f3(a1,a1))),
% 60.65/60.72 inference(scs_inference,[],[480,1868,496,1864,1866,2,402,126,3,121])).
% 60.65/60.72 cnf(1897,plain,
% 60.65/60.72 (E(f3(a2,a1),a1)),
% 60.65/60.72 inference(scs_inference,[],[49,153])).
% 60.65/60.72 cnf(1899,plain,
% 60.65/60.72 (E(f3(a1,a2),a1)),
% 60.65/60.72 inference(scs_inference,[],[49,153,154])).
% 60.65/60.72 cnf(1901,plain,
% 60.65/60.72 (P2(f7(a16,a16,a17,a17),a17,a17)),
% 60.65/60.72 inference(scs_inference,[],[49,316,153,154,142])).
% 60.65/60.72 cnf(1905,plain,
% 60.65/60.72 (P2(f9(a16,a16,a16,a16),a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[49,316,1624,169,153,154,142,144,145])).
% 60.65/60.72 cnf(1907,plain,
% 60.65/60.72 (P2(f9(a17,a17,a16,a16),a17,a17)),
% 60.65/60.72 inference(scs_inference,[],[49,316,1624,169,317,153,154,142,144,145,146])).
% 60.65/60.72 cnf(1909,plain,
% 60.65/60.72 (P11(f3(a2,a1),a1)),
% 60.65/60.72 inference(scs_inference,[],[49,316,1624,169,317,153,154,142,144,145,146,111])).
% 60.65/60.72 cnf(1911,plain,
% 60.65/60.72 (P11(a14,a5)),
% 60.65/60.72 inference(scs_inference,[],[76,49,316,1624,169,317,153,154,142,144,145,146,111,119])).
% 60.65/60.72 cnf(1913,plain,
% 60.65/60.72 (P10(a5,a15)),
% 60.65/60.72 inference(scs_inference,[],[76,49,316,1624,169,84,317,153,154,142,144,145,146,111,119,134])).
% 60.65/60.72 cnf(1915,plain,
% 60.65/60.72 (~P2(f8(a16,a16,x19151,a11),x19151,a11)),
% 60.65/60.72 inference(scs_inference,[],[76,49,316,1624,169,84,317,153,154,142,144,145,146,111,119,134,147])).
% 60.65/60.72 cnf(1917,plain,
% 60.65/60.72 (P11(a10,a13)),
% 60.65/60.72 inference(scs_inference,[],[76,49,316,1624,169,84,317,83,153,154,142,144,145,146,111,119,134,147,137])).
% 60.65/60.72 cnf(1919,plain,
% 60.65/60.72 (P11(a16,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[76,49,316,1624,1197,169,84,317,83,153,154,142,144,145,146,111,119,134,147,137,135])).
% 60.65/60.72 cnf(1921,plain,
% 60.65/60.72 (P11(f7(a16,a16,a17,a17),a16)),
% 60.65/60.72 inference(scs_inference,[],[76,49,316,1624,1197,169,84,317,83,153,154,142,144,145,146,111,119,134,147,137,135,136])).
% 60.65/60.72 cnf(1923,plain,
% 60.65/60.72 (~E(a11,a6)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,316,1624,1197,169,84,317,83,153,154,142,144,145,146,111,119,134,147,137,135,136,2])).
% 60.65/60.72 cnf(1924,plain,
% 60.65/60.72 (~P10(f3(a4,a1),a1)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1876,316,1624,1197,169,84,317,83,109,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124])).
% 60.65/60.72 cnf(1925,plain,
% 60.65/60.72 (~P10(x19251,x19251)),
% 60.65/60.72 inference(rename_variables,[],[109])).
% 60.65/60.72 cnf(1927,plain,
% 60.65/60.72 (~P8(f3(a1,a1),x19271,f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1879,1876,316,1624,1197,169,84,163,317,83,109,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27])).
% 60.65/60.72 cnf(1929,plain,
% 60.65/60.72 (P2(f3(a4,a1),a1,a1)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1879,1876,1865,316,1624,1197,169,84,163,317,83,109,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127])).
% 60.65/60.72 cnf(1938,plain,
% 60.65/60.72 (~P7(f3(a4,a1),f3(a1,a1),x19381)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1879,1876,1865,316,1624,71,159,69,1197,169,84,163,317,693,83,109,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38])).
% 60.65/60.72 cnf(1939,plain,
% 60.65/60.72 (~P7(x19391,x19391,x19392)),
% 60.65/60.72 inference(rename_variables,[],[159])).
% 60.65/60.72 cnf(1940,plain,
% 60.65/60.72 (~P7(f3(a1,a1),f3(a4,a1),x19401)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1879,1876,1865,316,1624,71,159,1939,69,1197,169,84,163,317,693,83,109,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37])).
% 60.65/60.72 cnf(1942,plain,
% 60.65/60.72 (~P6(f3(a1,a1),f3(a4,a1),x19421)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1879,1876,1865,316,1624,71,159,1939,69,1197,169,84,163,317,693,83,157,109,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32])).
% 60.65/60.72 cnf(1944,plain,
% 60.65/60.72 (~P10(f3(a4,a1),f3(a1,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1879,1876,1877,1865,316,1624,71,159,1939,69,1197,169,84,163,317,693,83,157,109,1925,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125])).
% 60.65/60.72 cnf(1945,plain,
% 60.65/60.72 (~P10(x19451,x19451)),
% 60.65/60.72 inference(rename_variables,[],[109])).
% 60.65/60.72 cnf(1947,plain,
% 60.65/60.72 (~P10(a1,f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,1879,1876,1877,1865,316,1624,1864,71,159,1939,69,1197,169,84,163,317,693,83,157,109,1925,1945,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125,31])).
% 60.65/60.72 cnf(1949,plain,
% 60.65/60.72 (~E(f3(a4,a1),a2)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,85,1879,1876,1877,1865,316,1624,1864,71,159,1939,69,1863,1197,169,84,163,317,693,83,157,109,1925,1945,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125,31,3])).
% 60.65/60.72 cnf(1950,plain,
% 60.65/60.72 (E(f7(a16,a16,a17,a17),a16)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,85,1879,1876,1877,1865,316,1624,1864,71,159,1939,69,1863,1197,169,84,163,317,693,83,157,109,1925,1945,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125,31,3,121])).
% 60.65/60.72 cnf(1953,plain,
% 60.65/60.72 (~P2(f7(a16,a16,a17,a17),x19531,a11)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,85,1642,1879,1876,1877,1865,1634,316,1624,1864,71,159,1939,69,1863,1197,169,84,163,317,693,83,157,109,1925,1945,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125,31,3,121,35,19])).
% 60.65/60.72 cnf(1954,plain,
% 60.65/60.72 (~P10(f7(a16,a16,a17,a17),a11)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,85,1642,1879,1876,1877,1865,1634,316,1624,1864,71,295,159,1939,69,1863,1197,169,84,163,317,693,83,157,109,1925,1945,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125,31,3,121,35,19,30])).
% 60.65/60.72 cnf(1956,plain,
% 60.65/60.72 (~E(a11,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,85,1642,1879,1876,1877,1865,1634,316,1624,1864,71,295,159,1939,69,1863,1197,169,84,163,317,693,83,157,109,1925,1945,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125,31,3,121,35,19,30,1231,402])).
% 60.65/60.72 cnf(1957,plain,
% 60.65/60.72 (~P8(a11,f7(a16,a16,a17,a17),x19571)),
% 60.65/60.72 inference(scs_inference,[],[76,1646,49,85,1640,1642,1879,1876,1877,1865,1634,316,1624,1864,71,295,159,1939,69,1863,1197,169,84,163,317,693,83,157,109,1925,1945,148,153,154,142,144,145,146,111,119,134,147,137,135,136,2,124,27,127,128,129,130,38,37,32,125,31,3,121,35,19,30,1231,402,28])).
% 60.65/60.72 cnf(1982,plain,
% 60.65/60.72 (E(f3(a1,a4),a1)),
% 60.65/60.72 inference(scs_inference,[],[50,154])).
% 60.65/60.72 cnf(1984,plain,
% 60.65/60.72 (P11(f3(a1,a2),a1)),
% 60.65/60.72 inference(scs_inference,[],[1899,50,154,111])).
% 60.65/60.72 cnf(1986,plain,
% 60.65/60.72 (P2(f9(a17,a17,a16,a16),a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[1899,50,317,154,111,145])).
% 60.65/60.72 cnf(1988,plain,
% 60.65/60.72 (P11(a5,a15)),
% 60.65/60.72 inference(scs_inference,[],[1913,1899,50,317,154,111,145,119])).
% 60.65/60.72 cnf(1990,plain,
% 60.65/60.72 (P11(a16,f9(a16,a16,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[1913,1905,1899,50,317,154,111,145,119,135])).
% 60.65/60.72 cnf(1992,plain,
% 60.65/60.72 (P11(f9(a16,a16,a16,a16),a16)),
% 60.65/60.72 inference(scs_inference,[],[1913,1905,1899,50,317,154,111,145,119,135,136])).
% 60.65/60.72 cnf(1994,plain,
% 60.65/60.72 (~E(a4,a1)),
% 60.65/60.72 inference(scs_inference,[],[86,1913,1905,1899,50,317,154,111,145,119,135,136,2])).
% 60.65/60.72 cnf(1995,plain,
% 60.65/60.72 (~P5(a16,a16,f7(a16,a16,a17,a17),a16)),
% 60.65/60.72 inference(scs_inference,[],[86,1913,1905,1950,1899,50,171,317,154,111,145,119,135,136,2,42])).
% 60.65/60.72 cnf(1996,plain,
% 60.65/60.72 (~P10(a1,f3(a1,a1))),
% 60.65/60.72 inference(scs_inference,[],[86,1913,1944,1905,1950,1899,50,1865,171,317,154,111,145,119,135,136,2,42,124])).
% 60.65/60.72 cnf(2001,plain,
% 60.65/60.72 (P2(a5,a14,a5)),
% 60.65/60.72 inference(scs_inference,[],[1911,86,1913,1944,1905,1950,1899,50,1865,316,171,60,317,148,154,111,145,119,135,136,2,42,124,40,128,127])).
% 60.65/60.72 cnf(2002,plain,
% 60.65/60.72 (P11(x20021,x20021)),
% 60.65/60.72 inference(rename_variables,[],[148])).
% 60.65/60.72 cnf(2005,plain,
% 60.65/60.72 (~P8(f3(a1,a1),x20051,a1)),
% 60.65/60.72 inference(scs_inference,[],[1911,86,1913,1944,1927,1905,1950,1899,302,50,1865,316,171,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29])).
% 60.65/60.72 cnf(2006,plain,
% 60.65/60.72 (~P5(a16,a16,a16,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[1911,86,1913,1944,1927,1905,1950,1899,302,50,1865,316,171,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43])).
% 60.65/60.72 cnf(2007,plain,
% 60.65/60.72 (~P5(a16,f7(a16,a16,a17,a17),a17,a17)),
% 60.65/60.72 inference(scs_inference,[],[1911,86,1913,1944,1927,1905,1950,1899,302,50,1865,316,171,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41])).
% 60.65/60.72 cnf(2008,plain,
% 60.65/60.72 (P10(a11,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[1911,86,1913,1944,1927,1954,1905,1956,1950,1899,302,50,1865,316,171,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112])).
% 60.65/60.72 cnf(2014,plain,
% 60.65/60.72 (~P7(f3(a1,a1),a1,x20141)),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1940,1954,1905,1956,1950,1899,302,50,1865,316,171,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38])).
% 60.65/60.72 cnf(2015,plain,
% 60.65/60.72 (~P7(a1,f3(a1,a1),x20151)),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1954,1905,1956,1950,1899,302,50,1865,316,171,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37])).
% 60.65/60.72 cnf(2016,plain,
% 60.65/60.72 (~P4(f7(a16,a16,a17,a17),a16,x20161,a11)),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1954,1905,1956,1950,1899,302,50,1865,316,171,1624,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22])).
% 60.65/60.72 cnf(2017,plain,
% 60.65/60.72 (~P6(f3(a1,a1),a1,x20171)),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1942,1954,1905,1956,1950,1899,302,50,1865,316,171,1624,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33])).
% 60.65/60.72 cnf(2018,plain,
% 60.65/60.72 (~P4(a16,f7(a16,a16,a17,a17),x20181,a11)),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1942,1954,1905,1956,1950,1899,302,50,1865,316,171,1624,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23])).
% 60.65/60.72 cnf(2020,plain,
% 60.65/60.72 (~P10(f3(a4,a1),f3(a2,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1950,1899,1638,302,50,1865,316,171,1624,60,1863,317,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125])).
% 60.65/60.72 cnf(2022,plain,
% 60.65/60.72 (~P10(a16,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1950,1899,1638,302,50,1865,316,171,1624,60,1863,317,109,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31])).
% 60.65/60.72 cnf(2024,plain,
% 60.65/60.72 (E(f3(a2,a1),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1950,1897,1899,1638,302,50,1865,316,171,1624,60,1863,317,109,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3])).
% 60.65/60.72 cnf(2025,plain,
% 60.65/60.72 (E(a16,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[76,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1638,302,50,1865,316,171,1624,60,1863,317,109,148,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120])).
% 60.65/60.72 cnf(2029,plain,
% 60.65/60.72 (P11(a1,f3(a1,a2))),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1638,302,50,1865,316,171,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35])).
% 60.65/60.72 cnf(2032,plain,
% 60.65/60.72 (~P10(f3(a2,a1),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1947,1929,1638,302,50,1865,316,171,1880,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35,19,30])).
% 60.65/60.72 cnf(2033,plain,
% 60.65/60.72 (E(f3(a4,a4),a4)),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1947,1929,1638,302,50,1865,316,171,1880,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35,19,30,155])).
% 60.65/60.72 cnf(2035,plain,
% 60.65/60.72 (P2(a6,a16,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1947,1929,1638,302,50,1865,316,171,1880,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35,19,30,155,308])).
% 60.65/60.72 cnf(2036,plain,
% 60.65/60.72 (P2(a6,f7(a16,a16,a17,a17),a16)),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1947,1929,1638,302,50,1865,316,171,1880,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35,19,30,155,308,331])).
% 60.65/60.72 cnf(2045,plain,
% 60.65/60.72 (~P5(a16,f7(a16,a16,a17,a17),a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1947,1929,1638,302,50,1865,316,171,1880,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35,19,30,155,308,331,286,287,311,334,401,419,1224])).
% 60.65/60.72 cnf(2047,plain,
% 60.65/60.72 (~P5(f7(a16,a16,a17,a17),a16,a16,a16)),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1924,1956,1919,1950,1897,1899,1947,1929,1638,302,50,1865,316,171,1880,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35,19,30,155,308,331,286,287,311,334,401,419,1224,1315])).
% 60.65/60.72 cnf(2056,plain,
% 60.65/60.72 (~P2(f8(a17,a17,x20561,a11),x20561,a11)),
% 60.65/60.72 inference(scs_inference,[],[76,178,1911,86,1913,1944,1927,1938,1940,1942,1954,1909,1905,1953,1924,1956,1919,1950,1901,1897,1899,1947,1929,1638,302,50,1865,316,171,1880,1624,60,1863,317,109,148,2002,154,111,145,119,135,136,2,42,124,40,128,127,27,29,43,41,112,129,130,38,37,22,33,23,32,125,31,3,120,121,35,19,30,155,308,331,286,287,311,334,401,419,1224,1315,1339,1239,140,144,147])).
% 60.65/60.72 cnf(2069,plain,
% 60.65/60.72 (P11(f3(a2,a1),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[2024,111])).
% 60.65/60.72 cnf(2071,plain,
% 60.65/60.72 (P11(a11,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[2024,2008,111,119])).
% 60.65/60.72 cnf(2073,plain,
% 60.65/60.72 (P11(a17,f9(a17,a17,a16,a16))),
% 60.65/60.72 inference(scs_inference,[],[1907,2024,2008,111,119,135])).
% 60.65/60.72 cnf(2077,plain,
% 60.65/60.72 (~E(a2,a4)),
% 60.65/60.72 inference(scs_inference,[],[87,1907,2024,2008,111,119,135,136,2])).
% 60.65/60.72 cnf(2080,plain,
% 60.65/60.72 (P2(a13,a10,a13)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2024,2008,148,111,119,135,136,2,128,127])).
% 60.65/60.72 cnf(2081,plain,
% 60.65/60.72 (P11(x20811,x20811)),
% 60.65/60.72 inference(rename_variables,[],[148])).
% 60.65/60.72 cnf(2084,plain,
% 60.65/60.72 (~P10(a1,f3(a1,a2))),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,1984,1950,109,148,111,119,135,136,2,128,127,40,124])).
% 60.65/60.72 cnf(2085,plain,
% 60.65/60.72 (~P10(x20851,x20851)),
% 60.65/60.72 inference(rename_variables,[],[109])).
% 60.65/60.72 cnf(2089,plain,
% 60.65/60.72 (~P5(a16,a16,f7(a16,a16,a17,a17),f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,70,1950,109,148,111,119,135,136,2,128,127,40,124,129,42])).
% 60.65/60.72 cnf(2090,plain,
% 60.65/60.72 (~P8(f3(a2,a1),x20901,f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,70,1950,163,109,148,111,119,135,136,2,128,127,40,124,129,42,27])).
% 60.65/60.72 cnf(2092,plain,
% 60.65/60.72 (~P8(f3(a1,a1),x20921,f3(a1,a4))),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,1982,70,1950,163,109,148,111,119,135,136,2,128,127,40,124,129,42,27,29])).
% 60.65/60.72 cnf(2095,plain,
% 60.65/60.72 (~P5(a16,f7(a16,a16,a17,a17),a16,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,1990,1982,2045,1634,70,1950,163,109,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43])).
% 60.65/60.72 cnf(2098,plain,
% 60.65/60.72 (~P7(f3(a1,a1),f3(a1,a4),x20981)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,2014,1990,1982,2045,1634,70,65,1950,163,109,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38])).
% 60.65/60.72 cnf(2099,plain,
% 60.65/60.72 (~P7(f3(a2,a1),f3(a1,a1),x20991)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,2014,1990,1982,2045,1938,1634,70,65,1950,163,109,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37])).
% 60.65/60.72 cnf(2100,plain,
% 60.65/60.72 (~P4(f7(a16,a16,a17,a17),f7(a16,a16,a17,a17),x21001,a11)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,2014,2018,1990,1982,2045,1938,1634,70,65,1950,163,109,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22])).
% 60.65/60.72 cnf(2101,plain,
% 60.65/60.72 (~P6(f3(a1,a1),f3(a1,a4),x21011)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,2014,2017,2018,1990,1982,2045,1938,1634,70,65,1950,163,109,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33])).
% 60.65/60.72 cnf(2104,plain,
% 60.65/60.72 (~P6(f3(a2,a1),f3(a4,a1),x21041)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,2014,2017,2018,2022,1990,1982,2045,1938,1634,70,65,79,1950,163,157,109,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32])).
% 60.65/60.72 cnf(2106,plain,
% 60.65/60.72 (~P10(a13,a10)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2006,1984,2005,2014,2017,2018,2022,1990,1982,2045,1938,1634,70,65,79,1950,163,157,109,2085,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32,125])).
% 60.65/60.72 cnf(2107,plain,
% 60.65/60.72 (~P10(x21071,x21071)),
% 60.65/60.72 inference(rename_variables,[],[109])).
% 60.65/60.72 cnf(2111,plain,
% 60.65/60.72 (E(f3(a1,a4),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,1907,2007,2024,2008,2033,2006,1984,2005,2014,2017,2018,2022,1990,1982,2045,1938,1634,70,65,79,1950,1863,163,157,109,2085,2107,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32,125,31,3])).
% 60.65/60.72 cnf(2114,plain,
% 60.65/60.72 (~P2(f8(a16,a16,a4,a11),f3(a4,a4),a11)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,2001,1907,2007,2024,2008,2033,2006,1984,2005,2014,2017,1915,2018,2022,1990,1982,2045,1938,1634,70,65,79,1950,1863,163,157,109,2085,2107,148,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32,125,31,3,141,20])).
% 60.65/60.72 cnf(2119,plain,
% 60.65/60.72 (~E(f9(a17,a17,a16,a16),a11)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,2001,1907,2007,2024,2008,2033,2006,1984,2005,2014,2017,1915,2018,2022,1990,1982,2045,1938,1678,1634,70,65,79,1950,1863,163,157,109,2085,2107,148,2081,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32,125,31,3,141,20,35,36,19])).
% 60.65/60.72 cnf(2121,plain,
% 60.65/60.72 (~P10(f3(a1,a4),f3(a1,a1))),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,2001,1907,2007,2024,2008,2033,2006,1984,2005,2014,2017,1915,1996,2018,2022,1990,1982,2045,1938,1678,1634,70,65,79,1950,1863,163,157,109,2085,2107,148,2081,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32,125,31,3,141,20,35,36,19,30])).
% 60.65/60.72 cnf(2122,plain,
% 60.65/60.72 (P2(f7(a14,a5,a14,a5),a14,a5)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,2001,1907,2007,2024,2008,2033,2006,1984,2005,2014,2017,1915,1996,2018,2022,1990,1982,2045,1938,1678,1634,70,65,79,1950,1863,163,157,109,2085,2107,148,2081,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32,125,31,3,141,20,35,36,19,30,143])).
% 60.65/60.72 cnf(2125,plain,
% 60.65/60.72 (~P5(a16,f7(a16,a16,a17,a17),f7(a16,a16,a17,a17),a16)),
% 60.65/60.72 inference(scs_inference,[],[76,1917,87,1988,2001,1907,2007,2024,2008,2033,2006,1984,2005,2014,2017,1915,1996,2018,2022,1990,1982,1995,2045,1682,1938,1678,1634,70,65,79,1950,1863,163,157,109,2085,2107,148,2081,111,119,135,136,2,128,127,40,124,129,42,27,29,126,43,130,38,37,22,33,123,32,125,31,3,141,20,35,36,19,30,143,28,41])).
% 60.65/60.72 cnf(2132,plain,
% 60.65/60.72 (P11(f3(a1,a4),f3(a4,a1))),
% 60.65/60.72 inference(scs_inference,[],[2111,111])).
% 60.65/60.72 cnf(2134,plain,
% 60.65/60.72 (P11(a13,a17)),
% 60.65/60.72 inference(scs_inference,[],[2111,72,111,119])).
% 60.65/60.72 cnf(2136,plain,
% 60.65/60.72 (P11(a16,a6)),
% 60.65/60.72 inference(scs_inference,[],[2111,2035,72,111,119,135])).
% 60.65/60.72 cnf(2138,plain,
% 60.65/60.72 (P11(a6,f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[2111,2035,72,111,119,135,136])).
% 60.65/60.72 cnf(2144,plain,
% 60.65/60.72 (P11(x21441,x21441)),
% 60.65/60.72 inference(rename_variables,[],[148])).
% 60.65/60.72 cnf(2147,plain,
% 60.65/60.72 (P11(x21471,x21471)),
% 60.65/60.72 inference(rename_variables,[],[148])).
% 60.65/60.72 cnf(2149,plain,
% 60.65/60.72 (~P10(a1,f3(a2,a1))),
% 60.65/60.72 inference(scs_inference,[],[1716,2069,2111,2035,2020,1921,2008,72,1865,148,2144,111,119,135,136,2,128,127,129,124])).
% 60.65/60.72 cnf(2151,plain,
% 60.65/60.72 (~P5(f7(a16,a16,a17,a17),a16,f7(a16,a16,a17,a17),f7(a16,a16,a17,a17))),
% 60.65/60.72 inference(scs_inference,[],[1716,2069,2111,2035,2020,2089,1921,2008,72,1865,1950,148,2144,111,119,135,136,2,128,127,129,124,40])).
% 60.65/60.72 cnf(2153,plain,
% 60.65/60.72 (P11(a11,a16)),
% 60.65/60.72 inference(scs_inference,[],[1716,2047,2069,2111,2035,2020,2089,1921,2071,2008,72,1865,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126])).
% 60.65/60.72 cnf(2160,plain,
% 60.65/60.73 (~P5(f7(a16,a16,a17,a17),a16,a16,f7(a16,a16,a17,a17))),
% 60.65/60.73 inference(scs_inference,[],[1716,2092,2090,2047,2069,2111,2035,2020,2089,1921,2071,2008,72,215,1865,1913,1880,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43])).
% 60.65/60.73 cnf(2162,plain,
% 60.65/60.73 (~P7(f3(a2,a1),f3(a4,a1),x21621)),
% 60.65/60.73 inference(scs_inference,[],[1716,2099,2092,2098,2090,2047,2069,2111,2035,2020,2089,1921,2071,2008,72,215,1865,1913,1880,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38])).
% 60.65/60.73 cnf(2164,plain,
% 60.65/60.73 (~P10(a17,a10)),
% 60.65/60.73 inference(scs_inference,[],[2106,1716,2099,2092,2098,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2008,72,215,1865,1913,1880,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123])).
% 60.65/60.73 cnf(2171,plain,
% 60.65/60.73 (~E(a17,a10)),
% 60.65/60.73 inference(scs_inference,[],[2080,2106,1716,2099,2092,2098,2101,2121,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2008,72,215,1865,1868,1913,1880,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123,139,32,125,31])).
% 60.65/60.73 cnf(2172,plain,
% 60.65/60.73 (~E(f7(a16,a16,a17,a17),a14)),
% 60.65/60.73 inference(scs_inference,[],[101,2080,2106,1716,2099,2092,2098,2101,2121,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2025,2008,72,215,1865,1868,1913,1880,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123,139,32,125,31,3])).
% 60.65/60.73 cnf(2173,plain,
% 60.65/60.73 (E(a1,f3(a1,a2))),
% 60.65/60.73 inference(scs_inference,[],[101,2080,2106,1716,2099,2092,2098,2101,2121,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2029,2084,2025,2008,72,215,1865,1868,1913,1880,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123,139,32,125,31,3,120])).
% 60.65/60.73 cnf(2175,plain,
% 60.65/60.73 (~P11(a17,a13)),
% 60.65/60.73 inference(scs_inference,[],[410,101,2080,2106,1716,2099,2092,2098,2101,2121,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2029,2084,2025,2008,72,215,1865,1868,1913,1880,1950,148,2144,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123,139,32,125,31,3,120,121])).
% 60.65/60.73 cnf(2178,plain,
% 60.65/60.73 (P11(f3(a4,a1),f3(a1,a4))),
% 60.65/60.73 inference(scs_inference,[],[410,101,2080,2106,1716,2099,2092,2098,2101,2121,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2029,2084,2025,1636,2008,72,215,1865,1868,1913,1880,1950,148,2144,2147,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123,139,32,125,31,3,120,121,20,35])).
% 60.65/60.73 cnf(2179,plain,
% 60.65/60.73 (P11(x21791,x21791)),
% 60.65/60.73 inference(rename_variables,[],[148])).
% 60.65/60.73 cnf(2184,plain,
% 60.65/60.73 (P2(f9(a10,a13,a10,a13),a10,a13)),
% 60.65/60.73 inference(scs_inference,[],[410,101,2080,2106,1716,2099,2092,2098,2101,2121,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2029,2084,2025,1636,2008,72,215,2033,1897,1865,1868,1913,1880,1950,148,2144,2147,2179,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123,139,32,125,31,3,120,121,20,35,36,19,30,146])).
% 60.65/60.73 cnf(2186,plain,
% 60.65/60.73 (P10(a11,a6)+P10(a6,a11)),
% 60.65/60.73 inference(scs_inference,[],[410,101,1923,2080,2106,1716,2099,2092,2098,2101,2121,2090,2104,2047,2069,2111,2035,2020,2089,1921,2071,2029,2084,2025,1636,2008,72,215,2033,1897,1865,1868,1913,1880,1950,148,2144,2147,2179,111,119,135,136,2,128,127,129,124,40,42,126,27,41,130,29,43,37,38,33,123,139,32,125,31,3,120,121,20,35,36,19,30,146,112])).
% 60.65/60.73 cnf(2197,plain,
% 60.65/60.73 (P11(f3(a1,a4),a1)),
% 60.65/60.73 inference(scs_inference,[],[1982,111])).
% 60.65/60.73 cnf(2199,plain,
% 60.65/60.73 (P11(a14,a17)),
% 60.65/60.73 inference(scs_inference,[],[75,1982,111,119])).
% 60.65/60.73 cnf(2212,plain,
% 60.65/60.73 (P10(a10,a17)),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2122,2073,75,74,1982,79,111,119,135,136,2,128,127,129,112])).
% 60.65/60.73 cnf(2214,plain,
% 60.65/60.73 (~P10(a6,f7(a16,a16,a17,a17))),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2122,2073,2022,75,74,1982,79,111,119,135,136,2,128,127,129,112,124])).
% 60.65/60.73 cnf(2216,plain,
% 60.65/60.73 (~P11(f9(a17,a17,a16,a16),a13)),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2175,2122,2073,2022,75,74,1982,79,111,119,135,136,2,128,127,129,112,124,126])).
% 60.65/60.73 cnf(2222,plain,
% 60.65/60.73 (~P8(f3(a1,a1),x22221,f3(a1,a2))),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2175,2122,2095,2151,2073,2005,2022,75,1899,74,1982,69,79,1950,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29])).
% 60.65/60.73 cnf(2227,plain,
% 60.65/60.73 (~P7(a1,f3(a1,a2),x22271)),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2175,2122,2095,2151,2173,2073,2005,2022,75,1899,74,2025,159,1982,69,79,1950,163,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37])).
% 60.65/60.73 cnf(2230,plain,
% 60.65/60.73 (~P6(f3(a1,a1),f3(a2,a1),x22301)),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2175,2122,2095,2151,2015,2173,2073,1942,2005,2022,75,1899,74,2024,2025,159,1982,69,79,1880,1950,163,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37,38,33])).
% 60.65/60.73 cnf(2231,plain,
% 60.65/60.73 (~P6(a1,f3(a1,a2),x22311)),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2175,2122,2095,2151,2015,2173,2073,1942,2005,2022,75,1899,74,2024,2025,159,1982,69,79,1880,1950,163,157,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37,38,33,32])).
% 60.65/60.73 cnf(2233,plain,
% 60.65/60.73 (~P10(a6,a16)),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2175,2122,2095,2151,2015,2173,2073,1942,2005,2022,75,1899,74,2024,2025,159,1982,69,79,1880,1950,163,157,109,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37,38,33,32,125])).
% 60.65/60.73 cnf(2236,plain,
% 60.65/60.73 (~P10(f3(a4,a1),f3(a1,a2))),
% 60.65/60.73 inference(scs_inference,[],[2136,2134,2153,2164,2171,2175,2122,2095,2151,2015,2173,2073,1942,2005,1924,2022,75,1899,74,2024,2025,159,1982,69,79,1880,1950,163,157,109,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37,38,33,32,125,31])).
% 60.65/60.73 cnf(2238,plain,
% 60.65/60.73 (~P11(a17,a10)),
% 60.65/60.73 inference(scs_inference,[],[2136,1994,2134,2153,2164,2171,2175,2122,2095,2151,2015,2173,2073,1942,2005,1924,2022,75,1899,74,2024,2025,159,1982,69,79,1880,1950,163,157,109,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37,38,33,32,125,31,3,120])).
% 60.65/60.73 cnf(2240,plain,
% 60.65/60.73 (E(f3(a4,a1),f3(a1,a4))),
% 60.65/60.73 inference(scs_inference,[],[2136,1994,2134,2153,2164,2171,2175,2122,2132,2178,2095,2151,2015,2173,2073,1942,2005,1924,2022,75,1899,74,2024,2025,159,1982,69,79,1880,1950,163,157,109,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37,38,33,32,125,31,3,120,121])).
% 60.65/60.73 cnf(2248,plain,
% 60.65/60.73 (~P10(f3(a1,a2),f3(a2,a1))),
% 60.65/60.73 inference(scs_inference,[],[2136,1994,2134,2153,2164,2171,2175,2122,2132,2178,2095,2151,2015,2149,2173,2073,2056,1734,1942,2005,1924,2022,75,1899,74,1917,2024,2025,159,1982,69,79,1880,1950,163,157,109,111,119,135,136,2,128,127,129,112,124,126,42,130,41,29,40,27,43,37,38,33,32,125,31,3,120,121,20,35,36,19,30])).
% 60.65/60.73 cnf(2255,plain,
% 60.65/60.73 (P11(a10,a17)),
% 60.65/60.73 inference(scs_inference,[],[2212,119])).
% 60.65/60.73 cnf(2259,plain,
% 60.65/60.73 (P11(a6,a16)),
% 60.65/60.73 inference(scs_inference,[],[2212,2036,119,135,136])).
% 60.65/60.73 cnf(2264,plain,
% 60.65/60.73 (P2(a14,a14,a17)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,1718,2036,2073,148,119,135,136,2,128,127])).
% 60.65/60.73 cnf(2265,plain,
% 60.65/60.73 (P11(x22651,x22651)),
% 60.65/60.73 inference(rename_variables,[],[148])).
% 60.65/60.73 cnf(2270,plain,
% 60.65/60.73 (P11(f3(a1,a4),f3(a1,a2))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,1718,2036,2197,2029,2073,148,2265,119,135,136,2,128,127,129,126])).
% 60.65/60.73 cnf(2272,plain,
% 60.65/60.73 (~P10(f7(a16,a16,a17,a17),a16)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2036,2138,2197,2029,2073,148,2265,119,135,136,2,128,127,129,126,124])).
% 60.65/60.73 cnf(2276,plain,
% 60.65/60.73 (~P8(f3(a4,a1),x22761,f3(a1,a2))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2222,2036,2138,2197,2029,78,73,2073,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27])).
% 60.65/60.73 cnf(2278,plain,
% 60.65/60.73 (~P7(f3(a2,a1),f3(a1,a2),x22781)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2222,2036,2162,2227,2138,2197,2029,78,73,2073,1897,2111,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37])).
% 60.65/60.73 cnf(2280,plain,
% 60.65/60.73 (~P10(a6,f9(a16,a16,a16,a16))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2162,2227,2138,2197,1992,2029,78,73,2073,1897,2111,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125])).
% 60.65/60.73 cnf(2282,plain,
% 60.65/60.73 (~P10(f3(a2,a1),f3(a1,a4))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2162,2032,2227,2138,2197,1992,2029,78,73,2073,1897,2111,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31])).
% 60.65/60.73 cnf(2284,plain,
% 60.65/60.73 (E(a6,a16)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,2029,78,73,2073,1897,2111,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120])).
% 60.65/60.73 cnf(2286,plain,
% 60.65/60.73 (~P11(a17,a14)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2029,78,73,2073,1897,2111,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121])).
% 60.65/60.73 cnf(2288,plain,
% 60.65/60.73 (P11(a1,f3(a1,a4))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,78,73,2073,1897,1864,2111,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35])).
% 60.65/60.73 cnf(2289,plain,
% 60.65/60.73 (P11(f9(a16,a16,a16,a16),f7(a16,a16,a17,a17))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36])).
% 60.65/60.73 cnf(2291,plain,
% 60.65/60.73 (~P10(f3(a2,a1),f3(a1,a1))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30])).
% 60.65/60.73 cnf(2294,plain,
% 60.65/60.73 (E(f8(a6,x22941,x22942,x22943),f8(a16,x22941,x22942,x22943))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6])).
% 60.65/60.73 cnf(2295,plain,
% 60.65/60.73 (E(f8(x22951,a6,x22952,x22953),f8(x22951,a16,x22952,x22953))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7])).
% 60.65/60.73 cnf(2298,plain,
% 60.65/60.73 (E(f9(a6,x22981,x22982,x22983),f9(a16,x22981,x22982,x22983))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10])).
% 60.65/60.73 cnf(2300,plain,
% 60.65/60.73 (E(f9(x23001,x23002,a6,x23003),f9(x23001,x23002,a16,x23003))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12])).
% 60.65/60.73 cnf(2302,plain,
% 60.65/60.73 (E(f7(a6,x23021,x23022,x23023),f7(a16,x23021,x23022,x23023))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14])).
% 60.65/60.73 cnf(2303,plain,
% 60.65/60.73 (E(f7(x23031,a6,x23032,x23033),f7(x23031,a16,x23032,x23033))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14,15])).
% 60.65/60.73 cnf(2306,plain,
% 60.65/60.73 (P2(a16,a17,a17)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14,15,16,17,248])).
% 60.65/60.73 cnf(2311,plain,
% 60.65/60.73 (~P5(f7(a16,a16,a17,a17),a6,a16,f7(a16,a16,a17,a17))),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2160,2032,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14,15,16,17,248,111,1497,41])).
% 60.65/60.73 cnf(2312,plain,
% 60.65/60.73 (~P5(a16,f7(a16,a16,a17,a17),f7(a16,a16,a17,a17),a6)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2160,2032,2125,2227,2138,2197,1992,1949,426,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14,15,16,17,248,111,1497,41,43])).
% 60.65/60.73 cnf(2313,plain,
% 60.65/60.73 (~P4(f7(a16,a16,a17,a17),a6,x23131,a11)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2160,2032,2125,2227,2138,2197,1992,1949,426,2016,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14,15,16,17,248,111,1497,41,43,23])).
% 60.65/60.73 cnf(2314,plain,
% 60.65/60.73 (~P4(a16,a6,x23141,a11)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2160,2032,2125,2227,2138,2197,1992,1949,426,2016,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14,15,16,17,248,111,1497,41,43,23,22])).
% 60.65/60.73 cnf(2318,plain,
% 60.65/60.73 (~P2(f8(a16,a6,x23181,a11),x23181,a11)),
% 60.65/60.73 inference(scs_inference,[],[2199,2212,2233,1718,2230,2222,2036,2240,2162,2160,2032,2125,2227,2138,2197,1992,1949,426,2016,1618,2178,2029,1996,1929,78,73,2073,1897,1864,2111,2025,1880,148,2265,119,135,136,2,128,127,129,126,124,130,27,38,37,32,125,31,3,120,121,35,36,19,30,4,5,6,7,8,9,10,11,12,13,14,15,16,17,248,111,1497,41,43,23,22,20,144,147])).
% 60.65/60.73 cnf(2322,plain,
% 60.65/60.73 (P11(f8(a6,x23221,x23222,x23223),f8(a16,x23221,x23222,x23223))),
% 60.65/60.73 inference(scs_inference,[],[2294,111])).
% 60.65/60.73 cnf(2326,plain,
% 60.65/60.73 (P11(a17,a16)),
% 60.65/60.73 inference(scs_inference,[],[2306,2294,766,111,119,135])).
% 60.65/60.73 cnf(2328,plain,
% 60.65/60.73 (P11(a16,a17)),
% 60.65/60.73 inference(scs_inference,[],[2306,2294,766,111,119,135,136])).
% 60.65/60.73 cnf(2332,plain,
% 60.65/60.73 (E(f7(a6,x23321,x23322,x23323),f7(a16,x23321,x23322,x23323))),
% 60.65/60.73 inference(rename_variables,[],[2302])).
% 60.65/60.73 cnf(2341,plain,
% 60.65/60.73 (~P5(f7(a16,a16,a17,a17),a6,a6,f7(a16,a16,a17,a17))),
% 60.65/60.73 inference(scs_inference,[],[2259,2255,2284,2286,2306,2119,2294,2302,2311,1957,1919,766,2073,167,79,111,119,135,136,2,28,127,128,129,126,42])).
% 60.65/60.73 cnf(2342,plain,
% 60.65/60.73 (~P10(f7(a16,a16,a17,a17),f9(a16,a16,a16,a16))),
% 60.65/60.73 inference(scs_inference,[],[2259,2255,2284,2286,2306,2289,2119,2294,2302,2311,1957,1919,766,2073,167,79,109,111,119,135,136,2,28,127,128,129,126,42,124])).
% 60.65/60.73 cnf(2343,plain,
% 60.65/60.73 (~P10(x23431,x23431)),
% 60.65/60.73 inference(rename_variables,[],[109])).
% 60.65/60.73 cnf(2346,plain,
% 60.65/60.73 (E(f7(a6,x23461,x23462,x23463),f7(a16,x23461,x23462,x23463))),
% 60.65/60.73 inference(rename_variables,[],[2302])).
% 60.65/60.73 cnf(2347,plain,
% 60.65/60.73 (~P7(a16,x23471,a6)),
% 60.65/60.73 inference(scs_inference,[],[2259,2255,2284,2286,2306,2289,2119,2294,2302,2332,2311,1957,1919,766,2073,167,161,79,109,111,119,135,136,2,28,127,128,129,126,42,124,40,39])).
% 60.65/60.73 cnf(2349,plain,
% 60.65/60.73 (~P8(f3(a4,a1),x23491,a1)),
% 60.65/60.73 inference(scs_inference,[],[2259,2255,2284,2286,2306,2289,2276,2119,2294,2302,2332,2311,1957,1919,766,2073,2173,167,161,79,109,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29])).
% 60.65/60.73 cnf(2352,plain,
% 60.65/60.73 (~P5(a16,f7(a6,a16,a17,a17),f7(a16,a16,a17,a17),a6)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2255,2284,2286,2306,2289,2276,2119,2294,2302,2332,2346,2311,2312,1957,1919,766,2073,2173,167,60,161,79,109,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41])).
% 60.65/60.73 cnf(2353,plain,
% 60.65/60.73 (E(f7(a6,x23531,x23532,x23533),f7(a16,x23531,x23532,x23533))),
% 60.65/60.73 inference(rename_variables,[],[2302])).
% 60.65/60.73 cnf(2356,plain,
% 60.65/60.73 (E(f7(a6,x23561,x23562,x23563),f7(a16,x23561,x23562,x23563))),
% 60.65/60.73 inference(rename_variables,[],[2302])).
% 60.65/60.73 cnf(2357,plain,
% 60.65/60.73 (~P4(f7(a16,a16,a17,a17),f7(a6,a16,a17,a17),x23571,a11)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2255,2284,2286,2306,2289,2276,2119,2294,2302,2332,2346,2353,2356,2311,2312,1957,2100,1919,302,766,2073,2173,167,60,161,79,109,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23])).
% 60.65/60.73 cnf(2359,plain,
% 60.65/60.73 (~P4(a6,a6,x23591,a11)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2255,2284,2286,2306,2289,2276,2119,2294,2302,2332,2346,2353,2356,2311,2312,1957,2100,1919,302,766,2073,2173,167,60,161,79,109,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22])).
% 60.65/60.73 cnf(2365,plain,
% 60.65/60.73 (~P10(f8(a16,x23651,x23652,x23653),f8(a6,x23651,x23652,x23653))),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2255,2284,2286,2306,2278,2289,2276,2119,2294,2302,2332,2346,2353,2356,2272,2311,2312,1957,2100,300,1919,1638,302,766,2073,2173,167,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31])).
% 60.65/60.73 cnf(2368,plain,
% 60.65/60.73 (P10(a17,a16)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2119,2294,2302,2332,2346,2353,2356,2272,2311,2312,108,1957,2100,300,1919,1638,302,766,2033,2073,2173,167,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120])).
% 60.65/60.73 cnf(2370,plain,
% 60.65/60.73 (E(a16,a6)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2119,2294,2302,2332,2346,2353,2356,2272,2311,2312,108,1957,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121])).
% 60.65/60.73 cnf(2373,plain,
% 60.65/60.73 (~P2(f8(a16,a6,x23731,a11),x23731,a11)),
% 60.65/60.73 inference(rename_variables,[],[2318])).
% 60.65/60.73 cnf(2374,plain,
% 60.65/60.73 (~P11(f9(a17,a17,a6,a16),a13)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2119,2294,2300,2302,2332,2346,2353,2356,2318,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35])).
% 60.65/60.73 cnf(2377,plain,
% 60.65/60.73 (~P2(f8(a6,a6,x23771,a11),x23771,a11)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19])).
% 60.65/60.73 cnf(2380,plain,
% 60.65/60.73 (~P10(f3(a2,a1),f3(a1,a2))),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30])).
% 60.65/60.73 cnf(2381,plain,
% 60.65/60.73 (~P5(a16,a6,a17,a17)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309])).
% 60.65/60.73 cnf(2383,plain,
% 60.65/60.73 (~P5(a6,a16,a17,a17)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332])).
% 60.65/60.73 cnf(2385,plain,
% 60.65/60.73 (~P5(a6,a16,a16,a16)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315])).
% 60.65/60.73 cnf(2391,plain,
% 60.65/60.73 (E(f8(x23911,x23912,a16,x23913),f8(x23911,x23912,a6,x23913))),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8])).
% 60.65/60.73 cnf(2394,plain,
% 60.65/60.73 (E(f7(a16,x23941,x23942,x23943),f7(a6,x23941,x23942,x23943))),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14])).
% 60.65/60.73 cnf(2396,plain,
% 60.65/60.73 (E(f8(x23961,a16,x23962,x23963),f8(x23961,a6,x23962,x23963))),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7])).
% 60.65/60.73 cnf(2399,plain,
% 60.65/60.73 (P3(a16,a6,a16,a16)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419])).
% 60.65/60.73 cnf(2401,plain,
% 60.65/60.73 (P3(a17,a17,a16,a6)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419,13,311])).
% 60.65/60.73 cnf(2404,plain,
% 60.65/60.73 (~P5(a16,a6,a16,a16)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419,13,311,5,1224])).
% 60.65/60.73 cnf(2406,plain,
% 60.65/60.73 (P3(a16,a16,a6,a16)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419,13,311,5,1224,287])).
% 60.65/60.73 cnf(2417,plain,
% 60.65/60.73 (E(f7(x24171,a16,x24172,x24173),f7(x24171,a6,x24172,x24173))),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419,13,311,5,1224,287,144,9,11,17,145,286,401,1339,15])).
% 60.65/60.73 cnf(2418,plain,
% 60.65/60.73 (E(f7(x24181,x24182,a16,x24183),f7(x24181,x24182,a6,x24183))),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419,13,311,5,1224,287,144,9,11,17,145,286,401,1339,15,16])).
% 60.65/60.73 cnf(2421,plain,
% 60.65/60.73 (P2(a6,a16,a6)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419,13,311,5,1224,287,144,9,11,17,145,286,401,1339,15,16,12,10,308])).
% 60.65/60.73 cnf(2422,plain,
% 60.65/60.73 (P2(f7(a6,a16,a17,a17),a16,a16)),
% 60.65/60.73 inference(scs_inference,[],[76,2259,2314,2077,2255,2284,2286,2306,2278,2289,2276,2236,2119,2294,2300,2302,2332,2346,2353,2356,2318,2373,2272,2311,2312,108,1957,2216,2100,300,1919,1638,302,766,2136,2033,2073,2173,167,2024,60,161,79,109,2343,111,119,135,136,2,28,127,128,129,126,42,124,40,39,29,130,41,27,43,23,22,38,37,125,32,31,3,120,121,20,35,36,19,30,309,332,1315,142,143,8,4,6,14,331,7,334,419,13,311,5,1224,287,144,9,11,17,145,286,401,1339,15,16,12,10,308,1231])).
% 60.65/60.73 cnf(2435,plain,
% 60.65/60.73 (E(f7(a16,x24351,x24352,x24353),f7(a6,x24351,x24352,x24353))),
% 60.65/60.73 inference(rename_variables,[],[2394])).
% 60.65/60.73 cnf(2441,plain,
% 60.65/60.73 (E(f7(a16,x24411,x24412,x24413),f7(a6,x24411,x24412,x24413))),
% 60.65/60.73 inference(rename_variables,[],[2394])).
% 60.65/60.73 cnf(2442,plain,
% 60.65/60.73 (P11(a16,f7(a6,a16,a16,a16))),
% 60.65/60.73 inference(scs_inference,[],[2383,2394,2435,2441,1341,142,143,1342,785])).
% 60.65/60.73 cnf(2448,plain,
% 60.65/60.73 (P11(f8(x24481,x24482,a16,x24483),f8(x24481,x24482,a6,x24483))),
% 60.65/60.73 inference(scs_inference,[],[2383,2399,2391,2394,2435,2441,1341,142,143,1342,785,146,145,111])).
% 60.65/60.73 cnf(2468,plain,
% 60.65/60.73 (~P11(a16,a10)),
% 60.65/60.73 inference(scs_inference,[],[2368,2326,2328,2383,2399,2282,2184,2391,2394,2435,2441,2417,2172,2374,2238,2069,745,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126])).
% 60.65/60.73 cnf(2471,plain,
% 60.65/60.73 (E(f7(x24711,a6,x24712,x24713),f7(x24711,a16,x24712,x24713))),
% 60.65/60.73 inference(rename_variables,[],[2303])).
% 60.65/60.73 cnf(2472,plain,
% 60.65/60.73 (P7(a16,a17,a17)),
% 60.65/60.73 inference(scs_inference,[],[2368,2326,2328,2383,2399,2282,2184,2391,2394,2435,2441,2417,2172,2352,2374,2238,2303,2069,745,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130])).
% 60.65/60.73 cnf(2476,plain,
% 60.65/60.73 (E(f7(x24761,a6,x24762,x24763),f7(x24761,a16,x24762,x24763))),
% 60.65/60.73 inference(rename_variables,[],[2303])).
% 60.65/60.73 cnf(2478,plain,
% 60.65/60.73 (E(f7(x24781,a6,x24782,x24783),f7(x24781,a16,x24782,x24783))),
% 60.65/60.73 inference(rename_variables,[],[2303])).
% 60.65/60.73 cnf(2479,plain,
% 60.65/60.73 (~P8(f3(a2,a1),x24791,a1)),
% 60.65/60.73 inference(scs_inference,[],[2368,2326,2328,2383,2399,2282,2184,2391,2394,2435,2441,2417,2349,2172,2341,2352,2374,2238,2303,2471,2476,2069,1927,745,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27])).
% 60.65/60.73 cnf(2483,plain,
% 60.65/60.73 (E(f7(x24831,a6,x24832,x24833),f7(x24831,a16,x24832,x24833))),
% 60.65/60.73 inference(rename_variables,[],[2303])).
% 60.65/60.73 cnf(2489,plain,
% 60.65/60.73 (~P4(a14,a17,x24891,a11)),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,2282,2184,2391,2394,2435,2441,2417,2357,2231,2349,2172,2288,2341,2352,2374,2238,2303,2471,2476,2478,2483,1738,727,2069,1927,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140])).
% 60.65/60.73 cnf(2493,plain,
% 60.65/60.73 (~E(a6,a15)),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,2342,2282,2184,2391,2394,2435,2441,2417,2357,2231,2349,2172,2288,2341,2352,2374,102,2238,2298,2303,2471,2476,2478,2483,1738,727,2069,1927,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140,31,3])).
% 60.65/60.73 cnf(2494,plain,
% 60.65/60.73 (E(a6,f7(a16,a16,a17,a17))),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,2342,2282,2184,2391,2394,2435,2441,2417,2214,2357,2231,2349,2172,2288,2341,2352,2374,102,2238,2298,2303,2471,2476,2478,2483,1738,727,2069,2138,1927,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140,31,3,120])).
% 60.65/60.73 cnf(2499,plain,
% 60.65/60.73 (~P2(f8(a6,a6,x24991,a11),x24991,a11)),
% 60.65/60.73 inference(rename_variables,[],[2377])).
% 60.65/60.73 cnf(2501,plain,
% 60.65/60.73 (P11(a6,a17)),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,768,2342,2282,2184,2391,2394,2435,2441,2417,2214,2357,2231,2349,2172,2377,2288,2341,2352,2374,102,2238,2298,2303,2471,2476,2478,2483,1738,727,2069,2138,1927,56,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140,31,3,120,121,20,26,35])).
% 60.65/60.73 cnf(2502,plain,
% 60.65/60.73 (P11(a17,a6)),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,768,2342,2282,2184,2391,2394,2435,2441,2417,2214,2357,2231,2349,2172,2377,2288,2341,2352,2374,102,2238,2298,2303,2471,2476,2478,2483,1738,727,2069,2138,1927,56,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140,31,3,120,121,20,26,35,36])).
% 60.65/60.73 cnf(2504,plain,
% 60.65/60.73 (E(f8(x25041,x25042,a16,x25043),f8(x25041,x25042,a6,x25043))),
% 60.65/60.73 inference(rename_variables,[],[2391])).
% 60.65/60.73 cnf(2506,plain,
% 60.65/60.73 (~P10(f8(a16,x25061,a16,x25062),f8(a6,x25061,a6,x25062))),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,768,2342,2282,2184,2365,2391,2504,2394,2435,2441,2417,2214,2357,2231,2349,2172,2377,2499,2288,2341,2352,2374,102,2238,2298,2303,2471,2476,2478,2483,1738,727,2069,2138,1927,56,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140,31,3,120,121,20,26,35,36,19,30])).
% 60.65/60.73 cnf(2509,plain,
% 60.65/60.73 (~P4(a16,a16,f3(a1,a1),a14)),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,768,2342,2282,2184,2365,2391,2504,2394,2435,2441,2417,2214,2357,2231,2349,2172,2377,2499,2288,2341,2352,2374,102,2238,2298,2303,2471,2476,2478,2483,1738,727,2069,2138,1927,56,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140,31,3,120,121,20,26,35,36,19,30,1375])).
% 60.65/60.73 cnf(2513,plain,
% 60.65/60.73 (~P2(f8(a6,a16,x25131,a11),x25131,a11)),
% 60.65/60.73 inference(scs_inference,[],[2368,2359,2264,2326,2328,2370,2383,2399,768,2342,2282,2184,2365,2391,2504,2394,2435,2441,2417,2214,2357,2231,2349,2172,2377,2499,2288,2341,2352,2374,102,2238,2298,2303,2471,2476,2478,2483,1738,727,2069,2138,1927,56,745,1864,2024,79,1341,142,143,1342,785,146,145,111,119,1231,135,136,402,2,127,128,129,124,126,42,130,29,40,41,27,43,23,22,37,125,32,140,31,3,120,121,20,26,35,36,19,30,1375,144,147])).
% 60.65/60.73 cnf(2526,plain,
% 60.65/60.73 (E(f7(x25261,x25262,a16,x25263),f7(x25261,x25262,a6,x25263))),
% 60.65/60.73 inference(rename_variables,[],[2418])).
% 60.65/60.73 cnf(2532,plain,
% 60.65/60.73 (E(f7(x25321,x25322,a16,x25323),f7(x25321,x25322,a6,x25323))),
% 60.65/60.73 inference(rename_variables,[],[2418])).
% 60.65/60.73 cnf(2547,plain,
% 60.65/60.73 (~E(a10,a16)),
% 60.65/60.73 inference(scs_inference,[],[2385,2401,2404,2489,2468,1986,2396,2418,2526,2532,720,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402])).
% 60.65/60.73 cnf(2549,plain,
% 60.65/60.73 (E(f3(a1,a2),f3(a2,a1))),
% 60.65/60.73 inference(scs_inference,[],[2385,2401,2404,2489,2468,2493,2380,2248,1986,2396,2418,2526,2532,720,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112])).
% 60.65/60.73 cnf(2562,plain,
% 60.65/60.73 (~P5(a6,a16,a6,a16)),
% 60.65/60.73 inference(scs_inference,[],[2385,2401,2404,2489,2468,2493,2501,2502,2380,2248,1986,2509,2280,2442,2396,2418,2526,2532,720,63,2368,2284,1880,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42])).
% 60.65/60.73 cnf(2565,plain,
% 60.65/60.73 (~P5(a6,a6,a17,a17)),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2489,2468,2493,2501,2502,2380,2248,1986,2509,2280,2442,2396,2418,2526,2532,720,59,63,2368,2284,1880,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40])).
% 60.65/60.73 cnf(2578,plain,
% 60.65/60.73 (~P10(a17,a6)),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2489,2468,2493,2501,2502,2380,2248,1986,2509,2280,2479,2313,2494,2442,2396,2418,2526,2532,2214,2303,720,59,63,2368,2008,159,2284,1899,1880,163,109,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40,29,41,27,43,123,23,22,37,125])).
% 60.65/60.73 cnf(2591,plain,
% 60.65/60.73 (E(a17,a6)),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2421,2489,2468,2493,2501,2502,2380,2248,1986,2509,2280,2506,2479,2313,2494,2442,2396,2418,2526,2532,1646,2214,2303,720,59,63,2368,2008,159,2284,1899,1880,163,157,109,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40,29,41,27,43,123,23,22,37,125,32,141,31,3,120,121])).
% 60.65/60.73 cnf(2595,plain,
% 60.65/60.73 (~P11(a6,a10)),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2421,2489,2468,2493,2501,2502,2380,2248,1986,2509,2280,2506,2479,2513,2313,2494,2442,2396,2418,2526,2532,1646,2214,2303,720,59,63,2368,2008,2033,159,2284,1899,1880,163,157,109,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40,29,41,27,43,123,23,22,37,125,32,141,31,3,120,121,20,35])).
% 60.65/60.73 cnf(2622,plain,
% 60.65/60.73 (E(f9(x26221,a17,x26222,x26223),f9(x26221,a6,x26222,x26223))),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2421,2489,2468,2493,2501,2502,2291,2380,2248,1986,2509,2280,2506,2479,2513,2114,2313,2494,2442,2396,2418,2526,2532,2295,1646,2214,2303,720,59,63,2368,2008,2033,159,2284,1899,1880,163,157,109,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40,29,41,27,43,123,23,22,37,125,32,141,31,3,120,121,20,35,36,19,30,229,266,224,225,228,267,354,373,394,1337,1340,374,4,8,13,5,9,6,14,7,799,11])).
% 60.65/60.73 cnf(2623,plain,
% 60.65/60.73 (E(f7(x26231,a17,x26232,x26233),f7(x26231,a6,x26232,x26233))),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2421,2489,2468,2493,2501,2502,2291,2380,2248,1986,2509,2280,2506,2479,2513,2114,2313,2494,2442,2396,2418,2526,2532,2295,1646,2214,2303,720,59,63,2368,2008,2033,159,2284,1899,1880,163,157,109,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40,29,41,27,43,123,23,22,37,125,32,141,31,3,120,121,20,35,36,19,30,229,266,224,225,228,267,354,373,394,1337,1340,374,4,8,13,5,9,6,14,7,799,11,15])).
% 60.65/60.73 cnf(2626,plain,
% 60.65/60.73 (E(f7(x26261,x26262,x26263,a17),f7(x26261,x26262,x26263,a6))),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2421,2489,2468,2493,2501,2502,2291,2380,2248,1986,2509,2280,2506,2479,2513,2114,2313,2494,2442,2396,2418,2526,2532,2295,1646,2214,2303,720,59,63,2368,2008,2033,159,2284,1899,1880,163,157,109,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40,29,41,27,43,123,23,22,37,125,32,141,31,3,120,121,20,35,36,19,30,229,266,224,225,228,267,354,373,394,1337,1340,374,4,8,13,5,9,6,14,7,799,11,15,16,12,17])).
% 60.65/60.73 cnf(2632,plain,
% 60.65/60.73 (P10(a11,a6)),
% 60.65/60.73 inference(scs_inference,[],[2381,2385,2401,2404,2421,2347,2489,2468,2472,2493,2501,2502,2291,2380,2248,1986,2509,2280,2506,2479,2513,2114,2313,2494,2442,2396,2418,2526,2532,2295,1646,2214,2303,720,59,63,2368,2008,2033,159,2284,1899,1880,163,157,109,142,143,1341,146,145,785,144,1342,111,119,147,135,136,402,2,112,127,128,129,24,124,126,42,130,40,29,41,27,43,123,23,22,37,125,32,141,31,3,120,121,20,35,36,19,30,229,266,224,225,228,267,354,373,394,1337,1340,374,4,8,13,5,9,6,14,7,799,11,15,16,12,17,10,1231,1467,39,2186])).
% 60.65/60.73 cnf(2644,plain,
% 60.65/60.73 (E(f7(x26441,a16,x26442,x26443),f7(x26441,a6,x26442,x26443))),
% 60.65/60.73 inference(rename_variables,[],[2417])).
% 60.65/60.73 cnf(2682,plain,
% 60.65/60.73 ($false),
% 60.65/60.73 inference(scs_inference,[],[2632,2406,2562,2547,2578,2565,2591,2595,2549,2270,2422,2322,2448,2622,2623,2626,2347,2288,2472,2417,2644,2138,61,78,2326,148,374,142,143,673,1341,146,145,799,785,111,119,1231,135,136,402,2,127,128,129,124,126,130,42,40,39]),
% 60.65/60.73 ['proof']).
% 60.65/60.73 % SZS output end Proof
% 60.65/60.73 % Total time :60.193680s
%------------------------------------------------------------------------------