%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : MGT088+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 : n015.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.07s 60.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MGT088+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.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 7 14:24:45 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.24/0.52 start to proof:theBenchmark
% 60.07/60.22 %-------------------------------------------
% 60.07/60.22 % File :CSE---1.7
% 60.07/60.22 % Problem :theBenchmark
% 60.07/60.22 % Transform :cnf
% 60.07/60.22 % Format :tptp:raw
% 60.07/60.22 % Command :java -jar mcs_scs.jar %d %s
% 60.07/60.22
% 60.07/60.22 % Result :Theorem 59.704954s
% 60.07/60.22 % Output :CNFRefutation 59.704954s
% 60.07/60.22 %-------------------------------------------
% 60.07/60.23 %--------------------------------------------------------------------------
% 60.07/60.23 % File : MGT088+1 : TPTP v9.3.1. Bugfixed v9.3.1.
% 60.07/60.23 % Domain : Management
% 60.07/60.23 % Problem : aabb - half-open right-closed (l,u] is non-empty (density)
% 60.07/60.23 % Version : Especial.
% 60.07/60.23 % English :
% 60.07/60.23
% 60.07/60.23 % Refs [MC+26] Mustafa et al. (2026), Axis Decomposition for ODRL
% 60.07/60.23 % Source [MC+26]
% 60.07/60.23 % Names ODRL509-1.p [MC+26]
% 60.07/60.23
% 60.07/60.23 % Status : Theorem
% 60.07/60.23 % Rating : ? v9.3.1
% 60.07/60.23 % Syntax : Number of formulae : 40 ( 17 unt; 0 def)
% 60.07/60.23 % Number of atoms : 98 ( 29 equ)
% 60.07/60.23 % Maximal formula atoms : 7 ( 2 avg)
% 60.07/60.23 % Number of connectives : 71 ( 13 ~; 9 |; 28 &)
% 60.07/60.23 % ( 8 <=>; 13 =>; 0 <=; 0 <~>)
% 60.07/60.23 % Maximal formula depth : 9 ( 4 avg)
% 60.07/60.23 % Maximal term depth : 2 ( 1 avg)
% 60.07/60.23 % Number of predicates : 12 ( 11 usr; 0 prp; 1-4 aty)
% 60.07/60.23 % Number of functors : 8 ( 8 usr; 7 con; 0-2 aty)
% 60.07/60.23 % Number of variables : 61 ( 57 !; 4 ?)
% 60.07/60.23 % SPC : FOF_THM_RFO_SEQ
% 60.07/60.23
% 60.07/60.23 % Comments : Requires MGT002+0.ax + MGT002+2.ax.
% 60.07/60.23 % Bugfixes : v9.3.1 - $distinct expanded to inequalities.
% 60.07/60.23 %--------------------------------------------------------------------------
% 60.07/60.23 include('Axioms/MGT002+0.ax').
% 60.07/60.23 include('Axioms/MGT002+1.ax').
% 60.07/60.23 include('Axioms/MGT002+2.ax').
% 60.07/60.23 %--------------------------------------------------------------------------
% 60.07/60.23 %----Named constants and ordering
% 60.07/60.23 fof(val_v0,axiom,
% 60.07/60.23 val(v0) ).
% 60.07/60.23
% 60.07/60.23 fof(val_v200,axiom,
% 60.07/60.23 val(v200) ).
% 60.07/60.23
% 60.07/60.23 fof(val_v400,axiom,
% 60.07/60.23 val(v400) ).
% 60.07/60.23
% 60.07/60.23 fof(val_v600,axiom,
% 60.07/60.23 val(v600) ).
% 60.07/60.23
% 60.07/60.23 fof(ord_v0_v200,axiom,
% 60.07/60.23 less(v0,v200) ).
% 60.07/60.23
% 60.07/60.23 fof(ord_v0_v400,axiom,
% 60.07/60.23 less(v0,v400) ).
% 60.07/60.23
% 60.07/60.23 fof(ord_v0_v600,axiom,
% 60.07/60.23 less(v0,v600) ).
% 60.07/60.23
% 60.07/60.23 fof(ord_v200_v400,axiom,
% 60.07/60.23 less(v200,v400) ).
% 60.07/60.23
% 60.07/60.23 fof(ord_v200_v600,axiom,
% 60.07/60.23 less(v200,v600) ).
% 60.07/60.23
% 60.07/60.23 fof(ord_v400_v600,axiom,
% 60.07/60.23 less(v400,v600) ).
% 60.07/60.23
% 60.07/60.23 fof(distinct,axiom,
% 60.07/60.23 ( v0 != v200
% 60.07/60.23 & v0 != v400
% 60.07/60.23 & v0 != v600
% 60.07/60.23 & v200 != v400
% 60.07/60.23 & v200 != v600
% 60.07/60.23 & v400 != v600 ) ).
% 60.07/60.23
% 60.07/60.23 fof(odrl509,conjecture,
% 60.07/60.23 ? [X] :
% 60.07/60.23 ( less(v200,X)
% 60.07/60.23 & in_lopen(X,v0,v400) ) ).
% 60.07/60.23
% 60.07/60.23 %--------------------------------------------------------------------------
% 60.07/60.23 %-------------------------------------------
% 60.07/60.23 % Proof found
% 60.07/60.23 % SZS status Theorem for theBenchmark
% 60.07/60.23 % SZS output start Proof
% 60.07/60.23 %ClaNum:113(EqnAxiom:49)
% 60.07/60.23 %VarNum:264(SingletonVarNum:116)
% 60.07/60.23 %MaxLitNum:6
% 60.07/60.23 %MaxfuncDepth:1
% 60.07/60.23 %SharedTerms:29
% 60.07/60.23 %goalClause: 104
% 60.07/60.23 [50]P1(a1)
% 60.07/60.23 [51]P1(a2)
% 60.07/60.23 [52]P1(a4)
% 60.07/60.23 [53]P9(a9)
% 60.07/60.23 [54]P9(a10)
% 60.07/60.23 [55]P9(a11)
% 60.07/60.23 [56]P9(a12)
% 60.07/60.23 [57]P10(a9,a10)
% 60.07/60.23 [58]P10(a9,a11)
% 60.07/60.23 [59]P10(a9,a12)
% 60.07/60.23 [60]P10(a10,a11)
% 60.07/60.23 [61]P10(a10,a12)
% 60.07/60.23 [62]P10(a11,a12)
% 60.07/60.23 [63]~E(a1,a2)
% 60.07/60.23 [64]~E(a1,a4)
% 60.07/60.23 [65]~E(a4,a2)
% 60.07/60.23 [66]~E(a10,a9)
% 60.07/60.23 [67]~E(a11,a9)
% 60.07/60.23 [68]~E(a11,a10)
% 60.07/60.23 [69]~E(a12,a9)
% 60.07/60.23 [70]~E(a12,a10)
% 60.07/60.23 [71]~E(a12,a11)
% 60.07/60.23 [72]~P10(x721,x721)
% 60.07/60.23 [104]~P10(a10,x1041)+~P6(x1041,a9,a11)
% 60.07/60.23 [74]~E(x741,x742)+P11(x741,x742)
% 60.07/60.23 [82]~P10(x821,x822)+P11(x821,x822)
% 60.07/60.23 [90]~P10(x901,x902)+P10(x901,f5(x901,x902))
% 60.07/60.23 [91]~P10(x911,x912)+P10(f5(x911,x912),x912)
% 60.07/60.23 [96]P10(x961,x962)+~P6(x962,x961,x963)
% 60.07/60.23 [97]P10(x971,x972)+~P7(x971,x973,x972)
% 60.07/60.23 [98]P10(x981,x982)+~P8(x982,x981,x983)
% 60.07/60.23 [99]P10(x991,x992)+~P8(x991,x993,x992)
% 60.07/60.23 [100]P11(x1001,x1002)+~P2(x1002,x1001,x1003)
% 60.07/60.23 [101]P11(x1011,x1012)+~P2(x1011,x1013,x1012)
% 60.07/60.23 [102]P11(x1021,x1022)+~P6(x1021,x1023,x1022)
% 60.07/60.23 [103]P11(x1031,x1032)+~P7(x1032,x1031,x1033)
% 60.07/60.23 [108]P5(x1081,x1082,x1083,x1084)+P2(f6(x1081,x1082,x1083,x1084),x1083,x1084)
% 60.07/60.23 [109]P5(x1091,x1092,x1093,x1094)+P2(f6(x1091,x1092,x1093,x1094),x1091,x1092)
% 60.07/60.23 [110]P4(x1101,x1102,x1103,x1104)+P2(f7(x1101,x1102,x1103,x1104),x1101,x1102)
% 60.07/60.23 [111]~P3(x1111,x1112,x1113,x1114)+P2(f8(x1111,x1112,x1113,x1114),x1113,x1114)
% 60.07/60.23 [112]~P3(x1121,x1122,x1123,x1124)+P2(f8(x1121,x1122,x1123,x1124),x1121,x1122)
% 60.07/60.23 [113]P4(x1131,x1132,x1133,x1134)+~P2(f7(x1131,x1132,x1133,x1134),x1133,x1134)
% 60.07/60.23 [75]P10(x752,x751)+P10(x751,x752)+E(x751,x752)
% 60.07/60.23 [83]P10(x831,x832)+~P11(x831,x832)+E(x831,x832)
% 60.07/60.23 [84]~P11(x842,x841)+~P11(x841,x842)+E(x841,x842)
% 60.07/60.23 [86]~P10(x861,x863)+P10(x861,x862)+~P10(x863,x862)
% 60.07/60.23 [87]~P11(x871,x873)+P10(x871,x872)+~P10(x873,x872)
% 60.07/60.23 [88]~P11(x883,x882)+P10(x881,x882)+~P10(x881,x883)
% 60.07/60.23 [89]~P11(x891,x893)+P11(x891,x892)+~P11(x893,x892)
% 60.07/60.23 [92]~P11(x921,x923)+~P11(x922,x921)+P2(x921,x922,x923)
% 60.07/60.23 [93]~P10(x932,x931)+~P11(x931,x933)+P6(x931,x932,x933)
% 60.07/60.23 [94]~P10(x941,x943)+~P11(x942,x941)+P7(x941,x942,x943)
% 60.07/60.23 [95]~P10(x951,x953)+~P10(x952,x951)+P8(x951,x952,x953)
% 60.07/60.23 [105]~P2(x1055,x1051,x1052)+P3(x1051,x1052,x1053,x1054)+~P2(x1055,x1053,x1054)
% 60.07/60.23 [106]~P4(x1064,x1065,x1062,x1063)+P2(x1061,x1062,x1063)+~P2(x1061,x1064,x1065)
% 60.07/60.23 [107]~P5(x1074,x1075,x1072,x1073)+~P2(x1071,x1072,x1073)+~P2(x1071,x1074,x1075)
% 60.07/60.23 [73]~P1(x731)+E(x731,a2)+E(x731,a4)+E(x731,a1)
% 60.07/60.23 [76]~P1(x761)+~P1(x762)+~E(x762,a1)+E(f3(x761,x762),a1)
% 60.07/60.23 [77]~P1(x772)+~P1(x771)+~E(x771,a1)+E(f3(x771,x772),a1)
% 60.07/60.23 [78]~P1(x782)+~P1(x781)+~E(x782,a2)+~E(x781,a2)+E(f3(x781,x782),a2)
% 60.07/60.23 [85]~P1(x852)+~P1(x851)+E(f3(x851,x852),a1)+E(f3(x851,x852),a2)+E(f3(x851,x852),a4)
% 60.07/60.23 [79]~P1(x791)+~P1(x792)+~E(x792,a4)+E(x791,a1)+E(x792,a1)+E(f3(x791,x792),a4)
% 60.07/60.23 [80]~P1(x801)+~P1(x802)+~E(x802,a4)+E(x801,a1)+E(x802,a1)+E(f3(x802,x801),a4)
% 60.07/60.23 %EqnAxiom
% 60.07/60.23 [1]E(x11,x11)
% 60.07/60.23 [2]E(x22,x21)+~E(x21,x22)
% 60.07/60.23 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.07/60.24 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43))
% 60.07/60.24 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52))
% 60.07/60.24 [6]~E(x61,x62)+E(f7(x61,x63,x64,x65),f7(x62,x63,x64,x65))
% 60.07/60.24 [7]~E(x71,x72)+E(f7(x73,x71,x74,x75),f7(x73,x72,x74,x75))
% 60.07/60.24 [8]~E(x81,x82)+E(f7(x83,x84,x81,x85),f7(x83,x84,x82,x85))
% 60.07/60.24 [9]~E(x91,x92)+E(f7(x93,x94,x95,x91),f7(x93,x94,x95,x92))
% 60.07/60.24 [10]~E(x101,x102)+E(f8(x101,x103,x104,x105),f8(x102,x103,x104,x105))
% 60.07/60.24 [11]~E(x111,x112)+E(f8(x113,x111,x114,x115),f8(x113,x112,x114,x115))
% 60.07/60.24 [12]~E(x121,x122)+E(f8(x123,x124,x121,x125),f8(x123,x124,x122,x125))
% 60.07/60.24 [13]~E(x131,x132)+E(f8(x133,x134,x135,x131),f8(x133,x134,x135,x132))
% 60.07/60.24 [14]~E(x141,x142)+E(f5(x141,x143),f5(x142,x143))
% 60.07/60.24 [15]~E(x151,x152)+E(f5(x153,x151),f5(x153,x152))
% 60.07/60.24 [16]~E(x161,x162)+E(f6(x161,x163,x164,x165),f6(x162,x163,x164,x165))
% 60.07/60.24 [17]~E(x171,x172)+E(f6(x173,x171,x174,x175),f6(x173,x172,x174,x175))
% 60.07/60.24 [18]~E(x181,x182)+E(f6(x183,x184,x181,x185),f6(x183,x184,x182,x185))
% 60.07/60.24 [19]~E(x191,x192)+E(f6(x193,x194,x195,x191),f6(x193,x194,x195,x192))
% 60.07/60.24 [20]~P1(x201)+P1(x202)+~E(x201,x202)
% 60.07/60.24 [21]P2(x212,x213,x214)+~E(x211,x212)+~P2(x211,x213,x214)
% 60.07/60.24 [22]P2(x223,x222,x224)+~E(x221,x222)+~P2(x223,x221,x224)
% 60.07/60.24 [23]P2(x233,x234,x232)+~E(x231,x232)+~P2(x233,x234,x231)
% 60.07/60.24 [24]P4(x242,x243,x244,x245)+~E(x241,x242)+~P4(x241,x243,x244,x245)
% 60.07/60.24 [25]P4(x253,x252,x254,x255)+~E(x251,x252)+~P4(x253,x251,x254,x255)
% 60.07/60.24 [26]P4(x263,x264,x262,x265)+~E(x261,x262)+~P4(x263,x264,x261,x265)
% 60.07/60.24 [27]P4(x273,x274,x275,x272)+~E(x271,x272)+~P4(x273,x274,x275,x271)
% 60.07/60.24 [28]~P9(x281)+P9(x282)+~E(x281,x282)
% 60.07/60.24 [29]P8(x292,x293,x294)+~E(x291,x292)+~P8(x291,x293,x294)
% 60.07/60.24 [30]P8(x303,x302,x304)+~E(x301,x302)+~P8(x303,x301,x304)
% 60.07/60.24 [31]P8(x313,x314,x312)+~E(x311,x312)+~P8(x313,x314,x311)
% 60.07/60.24 [32]P10(x322,x323)+~E(x321,x322)+~P10(x321,x323)
% 60.07/60.24 [33]P10(x333,x332)+~E(x331,x332)+~P10(x333,x331)
% 60.07/60.24 [34]P6(x342,x343,x344)+~E(x341,x342)+~P6(x341,x343,x344)
% 60.07/60.24 [35]P6(x353,x352,x354)+~E(x351,x352)+~P6(x353,x351,x354)
% 60.07/60.24 [36]P6(x363,x364,x362)+~E(x361,x362)+~P6(x363,x364,x361)
% 60.07/60.24 [37]P7(x372,x373,x374)+~E(x371,x372)+~P7(x371,x373,x374)
% 60.07/60.24 [38]P7(x383,x382,x384)+~E(x381,x382)+~P7(x383,x381,x384)
% 60.07/60.24 [39]P7(x393,x394,x392)+~E(x391,x392)+~P7(x393,x394,x391)
% 60.07/60.24 [40]P11(x402,x403)+~E(x401,x402)+~P11(x401,x403)
% 60.07/60.24 [41]P11(x413,x412)+~E(x411,x412)+~P11(x413,x411)
% 60.07/60.24 [42]P5(x422,x423,x424,x425)+~E(x421,x422)+~P5(x421,x423,x424,x425)
% 60.07/60.24 [43]P5(x433,x432,x434,x435)+~E(x431,x432)+~P5(x433,x431,x434,x435)
% 60.07/60.24 [44]P5(x443,x444,x442,x445)+~E(x441,x442)+~P5(x443,x444,x441,x445)
% 60.07/60.24 [45]P5(x453,x454,x455,x452)+~E(x451,x452)+~P5(x453,x454,x455,x451)
% 60.07/60.24 [46]P3(x462,x463,x464,x465)+~E(x461,x462)+~P3(x461,x463,x464,x465)
% 60.07/60.24 [47]P3(x473,x472,x474,x475)+~E(x471,x472)+~P3(x473,x471,x474,x475)
% 60.07/60.24 [48]P3(x483,x484,x482,x485)+~E(x481,x482)+~P3(x483,x484,x481,x485)
% 60.07/60.24 [49]P3(x493,x494,x495,x492)+~E(x491,x492)+~P3(x493,x494,x495,x491)
% 60.07/60.24
% 60.07/60.24 %-------------------------------------------
% 60.07/60.24 cnf(114,plain,
% 60.07/60.24 (P11(x1141,x1141)),
% 60.07/60.24 inference(equality_inference,[],[74])).
% 60.07/60.24 cnf(115,plain,
% 60.07/60.24 (~P1(x1151)+~P1(a1)+E(f3(x1151,a1),a1)),
% 60.07/60.24 inference(equality_inference,[],[76])).
% 60.07/60.24 cnf(116,plain,
% 60.07/60.24 (~P1(x1161)+~P1(a1)+E(f3(a1,x1161),a1)),
% 60.07/60.24 inference(equality_inference,[],[77])).
% 60.07/60.24 cnf(117,plain,
% 60.07/60.24 (~P1(x1171)+~P1(a4)+E(x1171,a1)+E(a4,a1)+E(f3(x1171,a4),a4)),
% 60.07/60.24 inference(equality_inference,[],[79])).
% 60.07/60.24 cnf(118,plain,
% 60.07/60.24 (~P1(x1181)+~P1(a4)+E(x1181,a1)+E(a4,a1)+E(f3(a4,x1181),a4)),
% 60.07/60.24 inference(equality_inference,[],[80])).
% 60.07/60.24 cnf(119,plain,
% 60.07/60.24 (~P1(x1191)+E(f3(x1191,a1),a1)),
% 60.07/60.24 inference(scs_inference,[],[50,115])).
% 60.07/60.24 cnf(120,plain,
% 60.07/60.24 (~P1(x1201)+E(f3(a1,x1201),a1)),
% 60.07/60.24 inference(scs_inference,[],[50,116])).
% 60.07/60.24 cnf(121,plain,
% 60.07/60.24 (~P1(x1211)+E(x1211,a1)+E(a4,a1)+E(f3(x1211,a4),a4)),
% 60.07/60.24 inference(scs_inference,[],[52,117])).
% 60.07/60.24 cnf(122,plain,
% 60.07/60.24 (~P1(x1221)+E(x1221,a1)+E(a4,a1)+E(f3(a4,x1221),a4)),
% 60.07/60.24 inference(scs_inference,[],[52,118])).
% 60.07/60.24 cnf(123,plain,
% 60.07/60.24 (~P6(x1231,x1231,x1232)),
% 60.07/60.24 inference(scs_inference,[],[72,96])).
% 60.07/60.24 cnf(125,plain,
% 60.07/60.24 (~P7(x1251,x1252,x1251)),
% 60.07/60.24 inference(scs_inference,[],[72,96,97])).
% 60.07/60.24 cnf(127,plain,
% 60.07/60.24 (~P8(x1271,x1271,x1272)),
% 60.07/60.24 inference(scs_inference,[],[72,96,97,98])).
% 60.07/60.24 cnf(131,plain,
% 60.07/60.24 (~P10(a10,a9)),
% 60.07/60.24 inference(scs_inference,[],[72,57,96,97,98,99,86])).
% 60.07/60.24 cnf(132,plain,
% 60.07/60.24 (~P10(x1321,x1321)),
% 60.07/60.24 inference(rename_variables,[],[72])).
% 60.07/60.24 cnf(135,plain,
% 60.07/60.24 (~P10(x1351,x1351)),
% 60.07/60.24 inference(rename_variables,[],[72])).
% 60.07/60.24 cnf(136,plain,
% 60.07/60.24 (P11(x1361,x1362)+~E(x1362,x1361)),
% 60.07/60.24 inference(scs_inference,[],[60,72,132,114,57,96,97,98,99,86,32,40])).
% 60.07/60.24 cnf(140,plain,
% 60.07/60.24 (~P10(x1401,x1401)),
% 60.07/60.24 inference(rename_variables,[],[72])).
% 60.07/60.24 cnf(143,plain,
% 60.07/60.24 (~P10(x1431,x1431)),
% 60.07/60.24 inference(rename_variables,[],[72])).
% 60.07/60.24 cnf(145,plain,
% 60.07/60.24 (~E(a2,a1)),
% 60.07/60.24 inference(scs_inference,[],[60,61,72,132,135,140,143,114,57,63,96,97,98,99,86,32,40,83,87,88,33])).
% 60.07/60.24 cnf(157,plain,
% 60.07/60.24 (~P8(a10,x1571,a9)),
% 60.07/60.24 inference(scs_inference,[],[131,98,97,96,99])).
% 60.07/60.24 cnf(159,plain,
% 60.07/60.24 (~P10(a11,a9)),
% 60.07/60.24 inference(scs_inference,[],[131,58,72,98,97,96,99,86])).
% 60.07/60.24 cnf(172,plain,
% 60.07/60.24 (~P10(a12,a9)),
% 60.07/60.24 inference(scs_inference,[],[159,59,72,97,96,98,99,86])).
% 60.07/60.25 cnf(185,plain,
% 60.07/60.25 (~E(a11,a12)),
% 60.07/60.25 inference(scs_inference,[],[172,62,72,98,96,97,99,32])).
% 60.07/60.25 cnf(191,plain,
% 60.07/60.25 (E(a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[51,2,119])).
% 60.07/60.25 cnf(192,plain,
% 60.07/60.25 (E(f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[191,2])).
% 60.07/60.25 cnf(194,plain,
% 60.07/60.25 (~E(a2,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[145,191,2,136,3])).
% 60.07/60.25 cnf(199,plain,
% 60.07/60.25 (~P11(a11,a10)),
% 60.07/60.25 inference(scs_inference,[],[60,68,82,84])).
% 60.07/60.25 cnf(200,plain,
% 60.07/60.25 (~P10(a11,a10)),
% 60.07/60.25 inference(scs_inference,[],[199,82])).
% 60.07/60.25 cnf(202,plain,
% 60.07/60.25 (~P2(a10,a11,x2021)),
% 60.07/60.25 inference(scs_inference,[],[199,82,100])).
% 60.07/60.25 cnf(204,plain,
% 60.07/60.25 (~P2(a11,x2041,a10)),
% 60.07/60.25 inference(scs_inference,[],[199,82,100,101])).
% 60.07/60.25 cnf(212,plain,
% 60.07/60.25 (~P7(a11,x2121,a10)),
% 60.07/60.25 inference(scs_inference,[],[199,82,100,101,102,103,96,97])).
% 60.07/60.25 cnf(220,plain,
% 60.07/60.25 (~P6(f5(a10,a11),a9,a11)),
% 60.07/60.25 inference(scs_inference,[],[60,104,90])).
% 60.07/60.25 cnf(221,plain,
% 60.07/60.25 (~P10(a9,f5(a10,a11))+~P11(f5(a10,a11),a11)),
% 60.07/60.25 inference(scs_inference,[],[220,93])).
% 60.07/60.25 cnf(234,plain,
% 60.07/60.25 (E(f3(a1,f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[191,50,120,20])).
% 60.07/60.25 cnf(236,plain,
% 60.07/60.25 (E(a1,f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[234,136,2])).
% 60.07/60.25 cnf(238,plain,
% 60.07/60.25 (~E(a2,f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[145,191,234,136,2,40,3])).
% 60.07/60.25 cnf(239,plain,
% 60.07/60.25 (P1(f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[145,191,234,50,136,2,40,3,20])).
% 60.07/60.25 cnf(276,plain,
% 60.07/60.25 (P10(f5(a10,f5(a10,a11)),f5(a10,a11))),
% 60.07/60.25 inference(scs_inference,[],[60,91,90])).
% 60.07/60.25 cnf(278,plain,
% 60.07/60.25 (~P10(x2781,x2781)),
% 60.07/60.25 inference(rename_variables,[],[72])).
% 60.07/60.25 cnf(280,plain,
% 60.07/60.25 (~E(f5(a10,a11),f5(a10,f5(a10,a11)))),
% 60.07/60.25 inference(scs_inference,[],[72,278,276,86,33])).
% 60.07/60.25 cnf(294,plain,
% 60.07/60.25 (~E(a11,f5(a10,a11))),
% 60.07/60.25 inference(scs_inference,[],[280,15])).
% 60.07/60.25 cnf(295,plain,
% 60.07/60.25 (E(f3(f3(a2,a1),x2951),f3(a1,x2951))),
% 60.07/60.25 inference(scs_inference,[],[191,4,2])).
% 60.07/60.25 cnf(296,plain,
% 60.07/60.25 (E(f3(a1,x2961),f3(f3(a2,a1),x2961))),
% 60.07/60.25 inference(scs_inference,[],[295,2])).
% 60.07/60.25 cnf(297,plain,
% 60.07/60.25 (P11(f3(a1,x2971),f3(f3(a2,a1),x2971))),
% 60.07/60.25 inference(scs_inference,[],[295,2,136])).
% 60.07/60.25 cnf(298,plain,
% 60.07/60.25 (P11(a1,f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[234,295,2,136,40])).
% 60.07/60.25 cnf(301,plain,
% 60.07/60.25 (P1(f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[234,238,295,239,2,136,40,3,20])).
% 60.07/60.25 cnf(302,plain,
% 60.07/60.25 (E(a1,f3(f3(a2,a1),f3(a2,a1)))+~P11(f3(f3(a2,a1),f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[234,238,295,239,2,136,40,3,20,84])).
% 60.07/60.25 cnf(325,plain,
% 60.07/60.25 (P11(f3(f3(a2,a1),x3251),f3(a1,x3251))),
% 60.07/60.25 inference(scs_inference,[],[296,136])).
% 60.07/60.25 cnf(329,plain,
% 60.07/60.25 (E(f3(f3(a2,a1),f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[191,234,296,298,136,40,41,302,2])).
% 60.07/60.25 cnf(367,plain,
% 60.07/60.25 (~P10(f5(a10,a11),a11)+~P10(a9,f5(a10,a11))),
% 60.07/60.25 inference(scs_inference,[],[221,82])).
% 60.07/60.25 cnf(370,plain,
% 60.07/60.25 (~P6(f5(a10,a11),a9,x3701)+~P10(f5(a10,a11),a11)),
% 60.07/60.25 inference(scs_inference,[],[367,96])).
% 60.07/60.25 cnf(375,plain,
% 60.07/60.25 (~P6(f5(a10,a11),a9,x3751)),
% 60.07/60.25 inference(scs_inference,[],[60,370,91])).
% 60.07/60.25 cnf(376,plain,
% 60.07/60.25 (~P10(a9,f5(a10,a11))),
% 60.07/60.25 inference(scs_inference,[],[375,114,93])).
% 60.07/60.25 cnf(400,plain,
% 60.07/60.25 (~E(a12,f5(a10,a11))),
% 60.07/60.25 inference(scs_inference,[],[376,59,276,86,33])).
% 60.07/60.25 cnf(420,plain,
% 60.07/60.25 (~E(a10,f5(a10,a11))),
% 60.07/60.25 inference(scs_inference,[],[376,57,33])).
% 60.07/60.25 cnf(433,plain,
% 60.07/60.25 (P4(f3(a2,a1),x4331,x4332,x4333)+P2(f7(a1,x4331,x4332,x4333),a1,x4331)),
% 60.07/60.25 inference(scs_inference,[],[191,110,24])).
% 60.07/60.25 cnf(436,plain,
% 60.07/60.25 (P4(x4361,f3(a2,a1),x4362,x4363)+~P2(f7(x4361,a1,x4362,x4363),x4362,x4363)),
% 60.07/60.25 inference(scs_inference,[],[191,113,25])).
% 60.07/60.25 cnf(461,plain,
% 60.07/60.25 (P4(f3(a2,a1),x4611,f3(a2,a1),x4612)+P2(f7(a1,x4611,a1,x4612),a1,x4611)),
% 60.07/60.25 inference(scs_inference,[],[191,433,26])).
% 60.07/60.25 cnf(464,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),a1,a1)+P4(f3(a2,a1),a1,f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[436,461])).
% 60.07/60.25 cnf(468,plain,
% 60.07/60.25 (P4(a1,a1,f3(a2,a1),a1)+P4(a1,f3(a2,a1),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[192,464,24])).
% 60.07/60.25 cnf(469,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),f3(a2,a1),a1)+P4(a1,f3(a2,a1),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[191,468,25])).
% 60.07/60.25 cnf(470,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[192,469,26])).
% 60.07/60.25 cnf(471,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[191,470,24])).
% 60.07/60.25 cnf(472,plain,
% 60.07/60.25 (P4(a1,a1,a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[191,192,470,24,25])).
% 60.07/60.25 cnf(473,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[191,192,470,24,25,26])).
% 60.07/60.25 cnf(474,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[191,192,470,24,25,26,27])).
% 60.07/60.25 cnf(475,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[191,474,26])).
% 60.07/60.25 cnf(476,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[191,474,471,26,27])).
% 60.07/60.25 cnf(477,plain,
% 60.07/60.25 (P4(a1,a1,f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[191,192,473,474,471,26,27,25])).
% 60.07/60.25 cnf(478,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[191,192,473,474,471,26,27,25,24])).
% 60.07/60.25 cnf(480,plain,
% 60.07/60.25 (P4(a1,a1,f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[192,475,25])).
% 60.07/60.25 cnf(482,plain,
% 60.07/60.25 (P4(a1,a1,a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[191,192,475,478,25,27,26])).
% 60.07/60.25 cnf(483,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[191,192,475,478,477,25,27,26,24])).
% 60.07/60.25 cnf(485,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[192,483,26])).
% 60.07/60.25 cnf(486,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[191,192,483,480,26,24])).
% 60.07/60.25 cnf(487,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[191,192,483,480,26,24,27])).
% 60.07/60.25 cnf(491,plain,
% 60.07/60.25 (P4(a1,f3(a1,f3(a2,a1)),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[236,472,25])).
% 60.07/60.25 cnf(492,plain,
% 60.07/60.25 (P4(a1,a1,a1,f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[236,472,25,27])).
% 60.07/60.25 cnf(493,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),f3(a1,f3(a2,a1)),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[236,476,472,25,27,26])).
% 60.07/60.25 cnf(494,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),a1,a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[236,476,472,25,27,26,24])).
% 60.07/60.25 cnf(495,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a1,f3(a2,a1)),f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[236,486,25])).
% 60.07/60.25 cnf(496,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,f3(a1,f3(a2,a1)),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[236,486,487,25,26])).
% 60.07/60.25 cnf(497,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,a1,f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[236,486,487,485,25,26,27])).
% 60.07/60.25 cnf(498,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),a1,a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[236,486,487,482,485,25,26,27,24])).
% 60.07/60.25 cnf(499,plain,
% 60.07/60.25 (P4(a1,f3(a1,f3(a2,a1)),f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[236,477,25])).
% 60.07/60.25 cnf(500,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),f3(a1,f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[236,192,493,477,25,27])).
% 60.07/60.25 cnf(501,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),f3(a1,f3(a2,a1)),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[236,192,493,477,25,27,24])).
% 60.07/60.25 cnf(502,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a1,f3(a2,a1)),a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[236,192,493,495,477,25,27,24,26])).
% 60.07/60.25 cnf(503,plain,
% 60.07/60.25 (P4(a1,a1,f3(a1,f3(a2,a1)),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[192,501,25])).
% 60.07/60.25 cnf(504,plain,
% 60.07/60.25 (P4(a1,f3(a1,f3(a2,a1)),a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[192,502,501,25,24])).
% 60.07/60.25 cnf(505,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,f3(a1,f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[192,496,502,501,25,24,27])).
% 60.07/60.25 cnf(506,plain,
% 60.07/60.25 (P4(a1,a1,f3(a1,f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[236,192,496,502,501,472,25,24,27,26])).
% 60.07/60.25 cnf(508,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a1,f3(a2,a1)),f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[236,483,25])).
% 60.07/60.25 cnf(509,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),f3(a2,a1),f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[236,478,483,25,27])).
% 60.07/60.25 cnf(510,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),f3(a1,f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[236,478,483,470,25,27,26])).
% 60.07/60.25 cnf(511,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),f3(a2,a1),f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[236,475,478,483,470,25,27,26,24])).
% 60.07/60.25 cnf(513,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),f3(a2,a1),a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[192,511,26])).
% 60.07/60.25 cnf(514,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),a1,f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[192,511,26,25])).
% 60.07/60.25 cnf(515,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),f3(a2,a1),f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[192,511,509,26,25,24])).
% 60.07/60.25 cnf(516,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),f3(a2,a1),f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[192,511,509,26,25,24,27])).
% 60.07/60.25 cnf(518,plain,
% 60.07/60.25 (P4(a1,f3(a1,f3(a2,a1)),f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[192,495,24])).
% 60.07/60.25 cnf(519,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),f3(a2,a1),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[192,513,495,24,27])).
% 60.07/60.25 cnf(520,plain,
% 60.07/60.25 (P4(f3(a1,f3(a2,a1)),a1,f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[192,516,513,495,24,27,25])).
% 60.07/60.25 cnf(521,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a1,f3(a2,a1)),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[192,516,508,513,495,24,27,25,26])).
% 60.07/60.25 cnf(523,plain,
% 60.07/60.25 (P4(a1,a1,f3(a2,a1),f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[192,515,25])).
% 60.07/60.25 cnf(524,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),a1,f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[192,515,25,26])).
% 60.07/60.25 cnf(525,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),a1,f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[236,192,515,471,25,26,27])).
% 60.07/60.25 cnf(527,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,f3(a2,a1),f3(a1,f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[236,483,27])).
% 60.07/60.25 cnf(544,plain,
% 60.07/60.25 (P4(f3(f3(a2,a1),f3(a2,a1)),a1,a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[296,498,24])).
% 60.07/60.25 cnf(545,plain,
% 60.07/60.25 (E(f3(a1,x5451),f3(f3(a2,a1),x5451))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(546,plain,
% 60.07/60.25 (P4(a1,f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[296,545,498,499,24,25])).
% 60.07/60.25 cnf(547,plain,
% 60.07/60.25 (E(f3(a1,x5471),f3(f3(a2,a1),x5471))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(548,plain,
% 60.07/60.25 (P4(a1,a1,f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[296,545,547,498,499,503,24,25,26])).
% 60.07/60.25 cnf(549,plain,
% 60.07/60.25 (E(f3(a1,x5491),f3(f3(a2,a1),x5491))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(550,plain,
% 60.07/60.25 (P4(a1,a1,a1,f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[296,545,547,549,498,499,503,492,24,25,26,27])).
% 60.07/60.25 cnf(553,plain,
% 60.07/60.25 (P4(f3(f3(a2,a1),f3(a2,a1)),a1,f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[296,514,24])).
% 60.07/60.25 cnf(554,plain,
% 60.07/60.25 (E(f3(a1,x5541),f3(f3(a2,a1),x5541))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(555,plain,
% 60.07/60.25 (P4(f3(a2,a1),f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[296,554,514,500,24,26])).
% 60.07/60.25 cnf(556,plain,
% 60.07/60.25 (E(f3(a1,x5561),f3(f3(a2,a1),x5561))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(557,plain,
% 60.07/60.25 (P4(a1,f3(f3(a2,a1),f3(a2,a1)),a1,f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[296,554,556,504,514,500,24,26,25])).
% 60.07/60.25 cnf(558,plain,
% 60.07/60.25 (E(f3(a1,x5581),f3(f3(a2,a1),x5581))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(559,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,a1,f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[296,554,556,558,504,514,497,500,24,26,25,27])).
% 60.07/60.25 cnf(562,plain,
% 60.07/60.25 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[296,519,24])).
% 60.07/60.25 cnf(563,plain,
% 60.07/60.25 (E(f3(a1,x5631),f3(f3(a2,a1),x5631))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(564,plain,
% 60.07/60.25 (P4(a1,f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),f3(a2,a1))),
% 60.07/60.25 inference(scs_inference,[],[296,563,518,519,24,25])).
% 60.07/60.25 cnf(565,plain,
% 60.07/60.25 (E(f3(a1,x5651),f3(f3(a2,a1),x5651))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(566,plain,
% 60.07/60.25 (P4(f3(a2,a1),a1,f3(f3(a2,a1),f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[296,563,565,518,519,505,24,25,26])).
% 60.07/60.25 cnf(567,plain,
% 60.07/60.25 (E(f3(a1,x5671),f3(f3(a2,a1),x5671))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(568,plain,
% 60.07/60.25 (P4(a1,a1,f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[296,563,565,567,518,519,505,523,24,25,26,27])).
% 60.07/60.25 cnf(571,plain,
% 60.07/60.25 (P4(a1,f3(f3(a2,a1),f3(a2,a1)),a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[296,491,25])).
% 60.07/60.25 cnf(572,plain,
% 60.07/60.25 (E(f3(a1,x5721),f3(f3(a2,a1),x5721))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(573,plain,
% 60.07/60.25 (P4(a1,a1,f3(f3(a2,a1),f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[296,572,491,506,25,26])).
% 60.07/60.25 cnf(574,plain,
% 60.07/60.25 (E(f3(a1,x5741),f3(f3(a2,a1),x5741))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(575,plain,
% 60.07/60.25 (P4(f3(f3(a2,a1),f3(a2,a1)),a1,f3(a2,a1),a1)),
% 60.07/60.25 inference(scs_inference,[],[296,572,574,520,491,506,25,26,24])).
% 60.07/60.25 cnf(576,plain,
% 60.07/60.25 (E(f3(a1,x5761),f3(f3(a2,a1),x5761))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(577,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),a1,f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.25 inference(scs_inference,[],[296,572,574,576,520,491,506,524,25,26,24,27])).
% 60.07/60.25 cnf(580,plain,
% 60.07/60.25 (P4(a1,f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),a1)),
% 60.07/60.25 inference(scs_inference,[],[296,510,26])).
% 60.07/60.25 cnf(581,plain,
% 60.07/60.25 (E(f3(a1,x5811),f3(f3(a2,a1),x5811))),
% 60.07/60.25 inference(rename_variables,[],[296])).
% 60.07/60.25 cnf(582,plain,
% 60.07/60.25 (P4(f3(f3(a2,a1),f3(a2,a1)),a1,a1,a1)),
% 60.07/60.25 inference(scs_inference,[],[296,581,494,510,26,24])).
% 60.07/60.25 cnf(583,plain,
% 60.07/60.25 (E(f3(a1,x5831),f3(f3(a2,a1),x5831))),
% 60.07/60.26 inference(rename_variables,[],[296])).
% 60.07/60.26 cnf(584,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),a1,a1)),
% 60.07/60.26 inference(scs_inference,[],[296,581,583,494,510,521,26,24,25])).
% 60.07/60.26 cnf(585,plain,
% 60.07/60.26 (E(f3(a1,x5851),f3(f3(a2,a1),x5851))),
% 60.07/60.26 inference(rename_variables,[],[296])).
% 60.07/60.26 cnf(586,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),a1,f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[296,581,583,585,494,510,521,525,26,24,25,27])).
% 60.07/60.26 cnf(588,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[191,568,24])).
% 60.07/60.26 cnf(589,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[191,568,24,25])).
% 60.07/60.26 cnf(591,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,586,568,555,24,25,26,27])).
% 60.07/60.26 cnf(593,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[192,591,25])).
% 60.07/60.26 cnf(594,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[191,192,591,562,25,26])).
% 60.07/60.26 cnf(595,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,192,591,562,25,26,24])).
% 60.07/60.26 cnf(596,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,192,591,562,25,26,24,27])).
% 60.07/60.26 cnf(598,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),f3(a2,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,596,26])).
% 60.07/60.26 cnf(599,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,564,596,26,24])).
% 60.07/60.26 cnf(600,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[296,191,564,596,502,26,24,25])).
% 60.07/60.26 cnf(602,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[296,191,192,564,596,502,26,24,25,27])).
% 60.07/60.26 cnf(629,plain,
% 60.07/60.26 (~P7(a1,a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[125,191,37,38])).
% 60.07/60.26 cnf(630,plain,
% 60.07/60.26 (~P10(a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[114,629,94])).
% 60.07/60.26 cnf(633,plain,
% 60.07/60.26 (~P7(a1,x6331,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[114,629,94,97])).
% 60.07/60.26 cnf(635,plain,
% 60.07/60.26 (~P6(f3(a2,a1),a1,x6351)),
% 60.07/60.26 inference(scs_inference,[],[114,629,94,97,96])).
% 60.07/60.26 cnf(637,plain,
% 60.07/60.26 (~P8(f3(a2,a1),a1,x6371)),
% 60.07/60.26 inference(scs_inference,[],[114,629,94,97,96,98])).
% 60.07/60.26 cnf(639,plain,
% 60.07/60.26 (~P8(a1,x6391,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[114,629,94,97,96,98,99])).
% 60.07/60.26 cnf(676,plain,
% 60.07/60.26 (E(f3(x6761,f3(a2,a1)),f3(x6761,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,2,5])).
% 60.07/60.26 cnf(677,plain,
% 60.07/60.26 (P11(f3(x6771,a1),f3(x6771,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[676,136])).
% 60.07/60.26 cnf(678,plain,
% 60.07/60.26 (E(f3(x6781,a1),f3(x6781,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[676,136,2])).
% 60.07/60.26 cnf(679,plain,
% 60.07/60.26 (P11(a1,f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[192,676,136,2,40])).
% 60.07/60.26 cnf(681,plain,
% 60.07/60.26 (E(f3(x6811,f3(a2,a1)),f3(x6811,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(682,plain,
% 60.07/60.26 (P1(f3(f3(a2,a1),a1))),
% 60.07/60.26 inference(scs_inference,[],[192,676,681,194,301,136,2,40,3,20])).
% 60.07/60.26 cnf(684,plain,
% 60.07/60.26 (E(a1,f3(a2,f3(a2,a1)))+~P11(f3(a2,f3(a2,a1)),a1)),
% 60.07/60.26 inference(scs_inference,[],[192,676,681,194,301,136,2,40,3,20,84])).
% 60.07/60.26 cnf(708,plain,
% 60.07/60.26 (P11(f3(x7081,f3(a2,a1)),f3(x7081,a1))),
% 60.07/60.26 inference(scs_inference,[],[678,136])).
% 60.07/60.26 cnf(709,plain,
% 60.07/60.26 (P11(a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[234,678,136,40])).
% 60.07/60.26 cnf(710,plain,
% 60.07/60.26 (~E(a2,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[234,678,238,136,40,3])).
% 60.07/60.26 cnf(714,plain,
% 60.07/60.26 (P11(f3(a1,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[234,295,678,682,238,677,136,40,3,20,41])).
% 60.07/60.26 cnf(716,plain,
% 60.07/60.26 (E(a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[234,295,678,682,238,677,136,40,3,20,41,84])).
% 60.07/60.26 cnf(720,plain,
% 60.07/60.26 (E(f3(a1,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[234,295,678,682,238,677,679,136,40,3,20,41,84,83,2])).
% 60.07/60.26 cnf(722,plain,
% 60.07/60.26 (P11(f3(f3(a2,a1),a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[296,714,40])).
% 60.07/60.26 cnf(729,plain,
% 60.07/60.26 (E(f3(a2,f3(a2,a1)),a1)),
% 60.07/60.26 inference(scs_inference,[],[192,295,296,710,708,714,40,3,41,684,2])).
% 60.07/60.26 cnf(730,plain,
% 60.07/60.26 (E(f3(f3(a2,a1),a1),a1)+~P11(a1,f3(f3(a2,a1),a1))),
% 60.07/60.26 inference(scs_inference,[],[192,295,296,710,708,714,40,3,41,684,2,84])).
% 60.07/60.26 cnf(754,plain,
% 60.07/60.26 (P11(f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,709,40])).
% 60.07/60.26 cnf(755,plain,
% 60.07/60.26 (P11(a1,f3(f3(a2,a1),a1))),
% 60.07/60.26 inference(scs_inference,[],[191,296,709,40,41])).
% 60.07/60.26 cnf(759,plain,
% 60.07/60.26 (E(f3(a2,a1),f3(a1,a1))+~P11(f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,296,709,40,41,730,2,84])).
% 60.07/60.26 cnf(782,plain,
% 60.07/60.26 (P11(f3(f3(a2,a1),a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[191,755,722,40,41])).
% 60.07/60.26 cnf(783,plain,
% 60.07/60.26 (E(f3(a2,a1),f3(f3(a2,a1),a1))),
% 60.07/60.26 inference(scs_inference,[],[191,755,722,40,41,84])).
% 60.07/60.26 cnf(793,plain,
% 60.07/60.26 (P11(f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[295,782,783,2,40])).
% 60.07/60.26 cnf(795,plain,
% 60.07/60.26 (E(f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[295,782,783,2,40,759])).
% 60.07/60.26 cnf(796,plain,
% 60.07/60.26 (E(f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[295,754,782,783,2,40,759,84])).
% 60.07/60.26 cnf(886,plain,
% 60.07/60.26 (E(f3(x8861,f3(a2,a1)),f3(x8861,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(889,plain,
% 60.07/60.26 (E(f3(x8891,f3(a2,a1)),f3(x8891,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(890,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),a1),a1,f3(a2,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,886,889,553,325,297,40,41,24])).
% 60.07/60.26 cnf(891,plain,
% 60.07/60.26 (E(f3(x8911,f3(a2,a1)),f3(x8911,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(893,plain,
% 60.07/60.26 (E(f3(x8931,f3(a2,a1)),f3(x8931,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(894,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(f3(a2,a1),a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,886,889,891,893,553,557,593,325,297,40,41,24,25,26])).
% 60.07/60.26 cnf(895,plain,
% 60.07/60.26 (E(f3(x8951,f3(a2,a1)),f3(x8951,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(896,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,886,889,891,893,895,553,557,593,527,325,297,40,41,24,25,26,27])).
% 60.07/60.26 cnf(906,plain,
% 60.07/60.26 (E(f3(x9061,f3(a2,a1)),f3(x9061,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(908,plain,
% 60.07/60.26 (E(f3(x9081,f3(a2,a1)),f3(x9081,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(909,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),f3(f3(a2,a1),a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,906,908,575,595,599,24,25,26])).
% 60.07/60.26 cnf(910,plain,
% 60.07/60.26 (E(f3(x9101,f3(a2,a1)),f3(x9101,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(911,plain,
% 60.07/60.26 (P4(a1,a1,a1,f3(f3(a2,a1),a1))),
% 60.07/60.26 inference(scs_inference,[],[676,906,908,910,575,595,599,550,24,25,26,27])).
% 60.07/60.26 cnf(913,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),a1),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,600,25])).
% 60.07/60.26 cnf(914,plain,
% 60.07/60.26 (E(f3(x9141,f3(a2,a1)),f3(x9141,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(915,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),a1),f3(a2,a1),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[676,914,594,600,25,24])).
% 60.07/60.26 cnf(923,plain,
% 60.07/60.26 (E(f3(x9231,f3(a2,a1)),f3(x9231,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(924,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),a1),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[676,923,598,602,24,25])).
% 60.07/60.26 cnf(939,plain,
% 60.07/60.26 (E(f3(x9391,f3(a2,a1)),f3(x9391,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(941,plain,
% 60.07/60.26 (E(f3(x9411,f3(a2,a1)),f3(x9411,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(942,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),a1),a1,a1)),
% 60.07/60.26 inference(scs_inference,[],[676,939,941,584,498,501,26,24,25])).
% 60.07/60.26 cnf(946,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,513,24])).
% 60.07/60.26 cnf(955,plain,
% 60.07/60.26 (E(f3(x9551,f3(a2,a1)),f3(x9551,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(956,plain,
% 60.07/60.26 (P4(a1,a1,f3(f3(a2,a1),a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,955,504,548,25,26])).
% 60.07/60.26 cnf(957,plain,
% 60.07/60.26 (E(f3(x9571,f3(a2,a1)),f3(x9571,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(958,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,f3(a2,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,955,957,504,514,548,25,26,24])).
% 60.07/60.26 cnf(959,plain,
% 60.07/60.26 (E(f3(x9591,f3(a2,a1)),f3(x9591,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(960,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,955,957,959,504,514,548,497,25,26,24,27])).
% 60.07/60.26 cnf(962,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),f3(a1,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[676,500,26])).
% 60.07/60.26 cnf(963,plain,
% 60.07/60.26 (E(f3(x9631,f3(a2,a1)),f3(x9631,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(964,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[676,963,516,500,26,24])).
% 60.07/60.26 cnf(965,plain,
% 60.07/60.26 (E(f3(x9651,f3(a2,a1)),f3(x9651,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(966,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[676,963,965,508,516,500,26,24,25])).
% 60.07/60.26 cnf(967,plain,
% 60.07/60.26 (E(f3(x9671,f3(a2,a1)),f3(x9671,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(968,plain,
% 60.07/60.26 (P4(a1,a1,f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,963,965,967,508,516,500,523,26,24,25,27])).
% 60.07/60.26 cnf(970,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),a1,a1)),
% 60.07/60.26 inference(scs_inference,[],[676,519,24])).
% 60.07/60.26 cnf(971,plain,
% 60.07/60.26 (E(f3(x9711,f3(a2,a1)),f3(x9711,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(973,plain,
% 60.07/60.26 (E(f3(x9731,f3(a2,a1)),f3(x9731,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(975,plain,
% 60.07/60.26 (E(f3(x9751,f3(a2,a1)),f3(x9751,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(976,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,971,973,975,518,519,505,524,24,25,26,27])).
% 60.07/60.26 cnf(979,plain,
% 60.07/60.26 (E(f3(x9791,f3(a2,a1)),f3(x9791,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(981,plain,
% 60.07/60.26 (E(f3(x9811,f3(a2,a1)),f3(x9811,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(982,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[676,979,981,520,546,506,25,26,24])).
% 60.07/60.26 cnf(983,plain,
% 60.07/60.26 (E(f3(x9831,f3(a2,a1)),f3(x9831,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(984,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,979,981,983,520,546,506,525,25,26,24,27])).
% 60.07/60.26 cnf(987,plain,
% 60.07/60.26 (E(f3(x9871,f3(a2,a1)),f3(x9871,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(989,plain,
% 60.07/60.26 (E(f3(x9891,f3(a2,a1)),f3(x9891,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(990,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),a1),a1,a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,987,989,544,564,510,25,26,24])).
% 60.07/60.26 cnf(991,plain,
% 60.07/60.26 (E(f3(x9911,f3(a2,a1)),f3(x9911,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(992,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),a1,f3(f3(a2,a1),a1))),
% 60.07/60.26 inference(scs_inference,[],[676,987,989,991,544,564,510,586,25,26,24,27])).
% 60.07/60.26 cnf(995,plain,
% 60.07/60.26 (E(f3(x9951,f3(a2,a1)),f3(x9951,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(996,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),f3(f3(a2,a1),a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[676,995,491,555,25,26])).
% 60.07/60.26 cnf(997,plain,
% 60.07/60.26 (E(f3(x9971,f3(a2,a1)),f3(x9971,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(999,plain,
% 60.07/60.26 (E(f3(x9991,f3(a2,a1)),f3(x9991,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(1000,plain,
% 60.07/60.26 (P4(a1,a1,a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,995,997,999,596,491,555,492,25,26,24,27])).
% 60.07/60.26 cnf(1002,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),a1,a1)),
% 60.07/60.26 inference(scs_inference,[],[676,521,25])).
% 60.07/60.26 cnf(1003,plain,
% 60.07/60.26 (E(f3(x10031,f3(a2,a1)),f3(x10031,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(1005,plain,
% 60.07/60.26 (E(f3(x10051,f3(a2,a1)),f3(x10051,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(1006,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,a1,a1)),
% 60.07/60.26 inference(scs_inference,[],[676,1003,1005,494,521,493,25,26,24])).
% 60.07/60.26 cnf(1007,plain,
% 60.07/60.26 (E(f3(x10071,f3(a2,a1)),f3(x10071,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(1008,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,1003,1005,1007,494,521,493,515,25,26,24,27])).
% 60.07/60.26 cnf(1011,plain,
% 60.07/60.26 (E(f3(x10111,f3(a2,a1)),f3(x10111,a1))),
% 60.07/60.26 inference(rename_variables,[],[676])).
% 60.07/60.26 cnf(1012,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,1011,495,496,25,26])).
% 60.07/60.26 cnf(1018,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[676,502,25])).
% 60.07/60.26 cnf(1119,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,f3(a2,a1)),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[678,984,25])).
% 60.07/60.26 cnf(1120,plain,
% 60.07/60.26 (E(f3(x11201,a1),f3(x11201,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1122,plain,
% 60.07/60.26 (E(f3(x11221,a1),f3(x11221,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1124,plain,
% 60.07/60.26 (E(f3(x11241,a1),f3(x11241,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1125,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),a1,f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[678,1120,1122,1124,896,984,946,25,26,24,27])).
% 60.07/60.26 cnf(1128,plain,
% 60.07/60.26 (E(f3(x11281,a1),f3(x11281,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1130,plain,
% 60.07/60.26 (E(f3(x11301,a1),f3(x11301,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1131,plain,
% 60.07/60.26 (P4(f3(a2,f3(a2,a1)),a1,a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[678,1128,1130,960,958,964,25,26,24])).
% 60.07/60.26 cnf(1132,plain,
% 60.07/60.26 (E(f3(x11321,a1),f3(x11321,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1133,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,f3(a2,a1),f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[678,1128,1130,1132,960,958,964,25,26,24,27])).
% 60.07/60.26 cnf(1137,plain,
% 60.07/60.26 (E(f3(x11371,a1),f3(x11371,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1139,plain,
% 60.07/60.26 (E(f3(x11391,a1),f3(x11391,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1140,plain,
% 60.07/60.26 (P4(f3(a2,f3(a2,a1)),f3(a2,a1),f3(a1,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[678,1137,1139,1008,962,25,26,24])).
% 60.07/60.26 cnf(1145,plain,
% 60.07/60.26 (E(f3(x11451,a1),f3(x11451,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1147,plain,
% 60.07/60.26 (E(f3(x11471,a1),f3(x11471,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1149,plain,
% 60.07/60.26 (E(f3(x11491,a1),f3(x11491,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1150,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(a1,a1),f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[678,1145,1147,1149,1012,968,976,25,26,24,27])).
% 60.07/60.26 cnf(1153,plain,
% 60.07/60.26 (E(f3(x11531,a1),f3(x11531,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1154,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,f3(a2,f3(a2,a1)),a1)),
% 60.07/60.26 inference(scs_inference,[],[678,1153,970,982,25,26])).
% 60.07/60.26 cnf(1155,plain,
% 60.07/60.26 (E(f3(x11551,a1),f3(x11551,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1156,plain,
% 60.07/60.26 (P4(f3(a2,f3(a2,a1)),f3(a1,a1),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[678,1153,1155,1018,970,982,25,26,24])).
% 60.07/60.26 cnf(1157,plain,
% 60.07/60.26 (E(f3(x11571,a1),f3(x11571,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1158,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),a1,f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[678,1153,1155,1157,1018,970,982,25,26,24,27])).
% 60.07/60.26 cnf(1177,plain,
% 60.07/60.26 (P4(f3(a2,f3(a2,a1)),f3(a1,a1),a1,a1)),
% 60.07/60.26 inference(scs_inference,[],[678,191,1002,1158,1131,25,26,24])).
% 60.07/60.26 cnf(1181,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a2,f3(a2,a1)),a1)),
% 60.07/60.26 inference(scs_inference,[],[191,1154,25])).
% 60.07/60.26 cnf(1185,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,f3(a2,a1)),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[678,946,25])).
% 60.07/60.26 cnf(1186,plain,
% 60.07/60.26 (E(f3(x11861,a1),f3(x11861,f3(a2,a1)))),
% 60.07/60.26 inference(rename_variables,[],[678])).
% 60.07/60.26 cnf(1187,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),f3(a2,f3(a2,a1)),a1)),
% 60.07/60.26 inference(scs_inference,[],[678,1186,946,966,25,26])).
% 60.07/60.26 cnf(1200,plain,
% 60.07/60.26 (P4(a1,f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,553,557,25,26])).
% 60.07/60.26 cnf(1202,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),a1,f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,553,557,575,25,26,24,27])).
% 60.07/60.26 cnf(1213,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),a1,f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,559,25])).
% 60.07/60.26 cnf(1216,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,559,566,571,25,24,26,27])).
% 60.07/60.26 cnf(1219,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),f3(a1,a1),f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,573,577,25,26])).
% 60.07/60.26 cnf(1225,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,580,582,25,24,26,27])).
% 60.07/60.26 cnf(1229,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,584,588,589,25,26,24,27])).
% 60.07/60.26 cnf(1233,plain,
% 60.07/60.26 (P4(f3(a1,f3(a2,a1)),a1,f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,498,499,25,24,26])).
% 60.07/60.26 cnf(1234,plain,
% 60.07/60.26 (P4(a1,f3(a1,f3(a2,a1)),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,498,499,25,24,26,27])).
% 60.07/60.26 cnf(1236,plain,
% 60.07/60.26 (P4(a1,f3(a1,a1),f3(a1,f3(a2,a1)),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,503,25])).
% 60.07/60.26 cnf(1245,plain,
% 60.07/60.26 (P4(f3(a1,f3(a2,a1)),f3(a1,a1),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[716,520,25])).
% 60.07/60.26 cnf(1248,plain,
% 60.07/60.26 (P4(f3(a1,f3(a2,a1)),f3(a2,a1),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,519,520,546,25,24,26,27])).
% 60.07/60.26 cnf(1251,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),a1,f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,544,25,26])).
% 60.07/60.26 cnf(1253,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,544,548,491,25,26,27,24])).
% 60.07/60.26 cnf(1267,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a1,f3(a2,a1)),a1)),
% 60.07/60.26 inference(scs_inference,[],[716,505,510,521,25,26,24])).
% 60.07/60.26 cnf(1273,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,f3(a2,a1),f3(a1,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,523,524,555,25,26,27,24])).
% 60.07/60.26 cnf(1287,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,f3(a2,a1)),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,502,504,548,25,26,24])).
% 60.07/60.26 cnf(1288,plain,
% 60.07/60.26 (P4(a1,f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,502,504,546,548,25,26,24,27])).
% 60.07/60.26 cnf(1292,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,562,492,25,26,27])).
% 60.07/60.26 cnf(1308,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,f3(a2,a1)),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,521,568,491,25,26,24,27])).
% 60.07/60.26 cnf(1310,plain,
% 60.07/60.26 (P4(a1,f3(a1,a1),f3(a1,f3(a2,a1)),a1)),
% 60.07/60.26 inference(scs_inference,[],[716,506,25])).
% 60.07/60.26 cnf(1315,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),a1),f3(a1,a1),f3(a2,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,890,25])).
% 60.07/60.26 cnf(1320,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),f3(f3(a2,a1),a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,894,25])).
% 60.07/60.26 cnf(1321,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,894,913,25,26])).
% 60.07/60.26 cnf(1322,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),a1),f3(a2,a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,894,913,915,25,26,27])).
% 60.07/60.26 cnf(1323,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(f3(a2,a1),a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,894,909,913,915,25,26,27,24])).
% 60.07/60.26 cnf(1326,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),a1),a1,f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,956,990,25,26])).
% 60.07/60.26 cnf(1327,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(f3(a2,a1),a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,924,956,990,25,26,27])).
% 60.07/60.26 cnf(1336,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1000,1006,25,26,27])).
% 60.07/60.26 cnf(1339,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[295,1321,25])).
% 60.07/60.26 cnf(1345,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[295,1327,25])).
% 60.07/60.26 cnf(1346,plain,
% 60.07/60.26 (E(f3(f3(a2,a1),x13461),f3(a1,x13461))),
% 60.07/60.26 inference(rename_variables,[],[295])).
% 60.07/60.26 cnf(1349,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(a2,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[192,295,1346,1315,1327,25,26,27,24])).
% 60.07/60.26 cnf(1352,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,295,1323,911,25,26])).
% 60.07/60.26 cnf(1353,plain,
% 60.07/60.26 (E(f3(f3(a2,a1),x13531),f3(a1,x13531))),
% 60.07/60.26 inference(rename_variables,[],[295])).
% 60.07/60.26 cnf(1355,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,295,1353,1320,1322,1323,911,25,26,27,24])).
% 60.07/60.26 cnf(1360,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),f3(a1,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[192,1339,1345,1352,25,26,27])).
% 60.07/60.26 cnf(1361,plain,
% 60.07/60.26 (P4(a1,f3(a1,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[192,1339,1345,1352,25,26,27,24])).
% 60.07/60.26 cnf(1363,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),a1,f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[192,1349,26])).
% 60.07/60.26 cnf(1365,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(a2,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[192,1349,1355,26,25,27])).
% 60.07/60.26 cnf(1378,plain,
% 60.07/60.26 (P4(f3(a2,f3(a2,a1)),f3(a2,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1140,942,26,27])).
% 60.07/60.26 cnf(1382,plain,
% 60.07/60.26 (P4(f3(a2,f3(a2,a1)),f3(a1,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1156,26])).
% 60.07/60.26 cnf(1387,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,f3(a2,a1)),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1185,26])).
% 60.07/60.26 cnf(1390,plain,
% 60.07/60.26 (P4(a1,f3(a2,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,729,1185,1378,1382,26,27,25,24])).
% 60.07/60.26 cnf(1399,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(a2,a1),f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1387,992,1133,26,27,25])).
% 60.07/60.26 cnf(1402,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),a1,f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[192,1399,26])).
% 60.07/60.26 cnf(1403,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),f3(f3(a2,a1),a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,996,1399,26,27])).
% 60.07/60.26 cnf(1407,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a2,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[295,1403,26])).
% 60.07/60.26 cnf(1410,plain,
% 60.07/60.26 (P4(f3(a2,a1),f3(a1,a1),f3(a1,a1),f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,295,1403,1181,1150,26,27,25])).
% 60.07/60.26 cnf(1416,plain,
% 60.07/60.26 (P4(f3(a2,a1),a1,f3(a1,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1119,1407,1187,1410,26,27,24,25])).
% 60.07/60.26 cnf(1423,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a1,a1),f3(a2,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,1125,26])).
% 60.07/60.26 cnf(1425,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1125,1177,1202,26,27,25])).
% 60.07/60.26 cnf(1428,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1),a1,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[192,1425,26])).
% 60.07/60.26 cnf(1431,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,729,1425,1423,1200,1216,26,27,25,24])).
% 60.07/60.26 cnf(1434,plain,
% 60.07/60.26 (P4(f3(a1,f3(a2,a1)),f3(a1,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1431,1233,1229,26,27,25])).
% 60.07/60.26 cnf(1437,plain,
% 60.07/60.26 (P4(f3(a1,f3(a2,a1)),f3(a2,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1248,26])).
% 60.07/60.26 cnf(1439,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1434,1251,1248,26,27,25])).
% 60.07/60.26 cnf(1442,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,f3(a2,a1)),f3(a1,a1),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1287,26])).
% 60.07/60.26 cnf(1445,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1437,1439,1225,1287,26,25,27,24])).
% 60.07/60.26 cnf(1450,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,f3(a2,a1)),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1442,1445,1234,1308,26,27,25,24])).
% 60.07/60.26 cnf(1453,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1450,1253,26,25])).
% 60.07/60.26 cnf(1454,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a1,f3(a2,a1)),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1450,1253,1267,26,25,27])).
% 60.07/60.26 cnf(1457,plain,
% 60.07/60.26 (P4(f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,1292,26])).
% 60.07/60.26 cnf(1460,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(a1,f3(a2,a1)),f3(a2,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1453,1454,1236,1292,26,27,25,24])).
% 60.07/60.26 cnf(1465,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(f3(a2,a1),f3(a2,a1)),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1457,1460,1288,1213,26,25,27,24])).
% 60.07/60.26 cnf(1468,plain,
% 60.07/60.26 (P4(f3(a1,f3(a2,a1)),f3(a1,a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1465,1245,26,27])).
% 60.07/60.26 cnf(1473,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(a2,a1),f3(a1,f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1468,1273,26,25])).
% 60.07/60.26 cnf(1475,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a2,a1),f3(a1,a1),f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,192,1468,1219,1273,1310,26,25,27,24])).
% 60.07/60.26 cnf(1479,plain,
% 60.07/60.26 (P4(f3(a1,a1),a1,f3(a1,a1),f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[192,1473,1475,1326,26,27,25])).
% 60.07/60.26 cnf(1544,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(f3(a2,a1),f3(a2,a1)))),
% 60.07/60.26 inference(scs_inference,[],[716,296,1428,1479,1336,26,27,25])).
% 60.07/60.26 cnf(1548,plain,
% 60.07/60.26 (P4(f3(a1,a1),f3(a1,a1),f3(a1,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[716,329,1544,1402,26,27])).
% 60.07/60.26 cnf(1716,plain,
% 60.07/60.26 (P10(a11,f5(a11,a12))),
% 60.07/60.26 inference(scs_inference,[],[62,90])).
% 60.07/60.26 cnf(1718,plain,
% 60.07/60.26 (P10(f5(a11,a12),a12)),
% 60.07/60.26 inference(scs_inference,[],[62,90,91])).
% 60.07/60.26 cnf(1722,plain,
% 60.07/60.26 (E(f3(a4,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[52,62,61,90,91,104,119])).
% 60.07/60.26 cnf(1724,plain,
% 60.07/60.26 (E(f3(a1,a2),a1)),
% 60.07/60.26 inference(scs_inference,[],[51,52,62,61,90,91,104,119,120])).
% 60.07/60.26 cnf(1726,plain,
% 60.07/60.26 (P11(f3(a4,a1),a1)),
% 60.07/60.26 inference(scs_inference,[],[51,52,62,61,90,91,104,119,120,74])).
% 60.07/60.26 cnf(1728,plain,
% 60.07/60.26 (P11(a11,a12)),
% 60.07/60.26 inference(scs_inference,[],[51,52,62,61,90,91,104,119,120,74,82])).
% 60.07/60.26 cnf(1730,plain,
% 60.07/60.26 (~E(a4,a1)),
% 60.07/60.26 inference(scs_inference,[],[51,52,64,62,61,90,91,104,119,120,74,82,2])).
% 60.07/60.26 cnf(1731,plain,
% 60.07/60.26 (~P8(f3(a2,a1),f3(a1,a1),x17311)),
% 60.07/60.26 inference(scs_inference,[],[51,127,52,64,795,62,61,90,91,104,119,120,74,82,2,29])).
% 60.07/60.26 cnf(1732,plain,
% 60.07/60.26 (~P8(x17321,x17321,x17322)),
% 60.07/60.26 inference(rename_variables,[],[127])).
% 60.07/60.26 cnf(1733,plain,
% 60.07/60.26 (~P8(f3(a1,a1),f3(a2,a1),x17331)),
% 60.07/60.26 inference(scs_inference,[],[51,127,1732,52,64,795,62,61,90,91,104,119,120,74,82,2,29,30])).
% 60.07/60.26 cnf(1735,plain,
% 60.07/60.26 (~P8(a1,x17351,f3(a1,a1))),
% 60.07/60.26 inference(scs_inference,[],[51,127,1732,52,64,795,639,62,796,61,90,91,104,119,120,74,82,2,29,30,31])).
% 60.07/60.26 cnf(1736,plain,
% 60.07/60.26 (~P6(f3(a1,a1),a1,x17361)),
% 60.07/60.26 inference(scs_inference,[],[51,127,1732,52,64,635,795,639,62,796,61,90,91,104,119,120,74,82,2,29,30,31,34])).
% 60.07/60.26 cnf(1737,plain,
% 60.07/60.26 (~P6(f3(a2,a1),f3(a1,a1),x17371)),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,52,64,635,795,639,62,796,720,61,90,91,104,119,120,74,82,2,29,30,31,34,35])).
% 60.07/60.27 cnf(1738,plain,
% 60.07/60.27 (P2(f3(a2,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,52,64,635,795,639,62,793,796,720,61,754,90,91,104,119,120,74,82,2,29,30,31,34,35,92])).
% 60.07/60.27 cnf(1740,plain,
% 60.07/60.27 (~P10(f3(a2,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,52,64,635,795,639,62,793,796,720,61,754,72,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87])).
% 60.07/60.27 cnf(1741,plain,
% 60.07/60.27 (~P10(x17411,x17411)),
% 60.07/60.27 inference(rename_variables,[],[72])).
% 60.07/60.27 cnf(1743,plain,
% 60.07/60.27 (~P10(a1,f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,52,64,635,795,639,630,62,793,796,720,61,754,72,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88])).
% 60.07/60.27 cnf(1745,plain,
% 60.07/60.27 (P11(f3(a4,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,52,64,635,795,639,630,62,793,796,720,61,709,754,72,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89])).
% 60.07/60.27 cnf(1747,plain,
% 60.07/60.27 (~P7(a1,x17471,f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,52,64,633,635,795,639,630,62,793,796,720,61,709,754,72,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39])).
% 60.07/60.27 cnf(1748,plain,
% 60.07/60.27 (~P7(f3(a1,a1),x17481,f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,52,64,633,635,795,639,630,62,793,796,720,61,709,754,72,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37])).
% 60.07/60.27 cnf(1750,plain,
% 60.07/60.27 (P11(x17501,x17501)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(1753,plain,
% 60.07/60.27 (P11(x17531,x17531)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(1755,plain,
% 60.07/60.27 (~P11(a12,a11)),
% 60.07/60.27 inference(scs_inference,[],[51,127,1732,185,52,64,633,635,795,639,630,62,793,796,720,61,709,754,72,114,1750,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84])).
% 60.07/60.27 cnf(1761,plain,
% 60.07/60.27 (~P11(a11,a9)),
% 60.07/60.27 inference(scs_inference,[],[51,67,127,1732,185,52,64,633,635,200,795,639,630,62,793,796,720,61,709,58,754,159,72,114,1750,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84,86,95,83])).
% 60.07/60.27 cnf(1765,plain,
% 60.07/60.27 (~E(f3(a2,a1),a4)),
% 60.07/60.27 inference(scs_inference,[],[51,67,127,1732,185,52,64,633,635,200,795,639,630,62,793,796,720,61,709,58,754,159,72,1741,114,1750,191,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84,86,95,83,33,3])).
% 60.07/60.27 cnf(1766,plain,
% 60.07/60.27 (E(f3(a2,a4),a4)),
% 60.07/60.27 inference(scs_inference,[],[51,67,127,1732,185,52,64,633,635,200,795,639,630,62,793,796,720,61,709,58,754,159,145,72,1741,114,1750,191,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84,86,95,83,33,3,121])).
% 60.07/60.27 cnf(1768,plain,
% 60.07/60.27 (E(f3(a4,a2),a4)),
% 60.07/60.27 inference(scs_inference,[],[51,67,127,1732,185,52,64,633,635,200,795,639,630,62,793,796,720,61,709,58,754,159,145,72,1741,114,1750,191,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84,86,95,83,33,3,121,122])).
% 60.07/60.27 cnf(1770,plain,
% 60.07/60.27 (P2(f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,67,127,1732,185,52,64,633,635,200,795,639,630,62,793,796,720,61,709,58,754,159,145,72,1741,114,1750,191,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84,86,95,83,33,3,121,122,21])).
% 60.07/60.27 cnf(1773,plain,
% 60.07/60.27 (P11(a1,f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[51,67,127,1732,185,52,64,633,635,1360,200,795,639,630,62,793,796,720,61,709,58,754,159,145,72,1741,114,1750,1753,191,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84,86,95,83,33,3,121,122,21,106,40])).
% 60.07/60.27 cnf(1774,plain,
% 60.07/60.27 (P11(x17741,x17741)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(1775,plain,
% 60.07/60.27 (P11(f3(a1,a2),a1)),
% 60.07/60.27 inference(scs_inference,[],[51,67,127,1732,185,52,64,633,635,1360,200,795,639,630,62,793,796,720,61,709,58,754,159,145,72,1741,114,1750,1753,1774,191,90,91,104,119,120,74,82,2,29,30,31,34,35,92,87,88,89,39,37,94,93,84,86,95,83,33,3,121,122,21,106,40,41])).
% 60.07/60.27 cnf(1783,plain,
% 60.07/60.27 (~P1(x17831)+E(x17831,a1)+E(f3(x17831,a4),a4)),
% 60.07/60.27 inference(scs_inference,[],[1730,121])).
% 60.07/60.27 cnf(1786,plain,
% 60.07/60.27 (P10(a10,f5(a10,a12))),
% 60.07/60.27 inference(scs_inference,[],[61,90])).
% 60.07/60.27 cnf(1788,plain,
% 60.07/60.27 (P11(f3(a2,a4),a4)),
% 60.07/60.27 inference(scs_inference,[],[1766,61,90,74])).
% 60.07/60.27 cnf(1792,plain,
% 60.07/60.27 (P10(f5(a10,a12),a12)),
% 60.07/60.27 inference(scs_inference,[],[1766,61,60,90,74,104,91])).
% 60.07/60.27 cnf(1794,plain,
% 60.07/60.27 (E(f3(a1,a4),a1)),
% 60.07/60.27 inference(scs_inference,[],[1766,52,61,60,90,74,104,91,120])).
% 60.07/60.27 cnf(1796,plain,
% 60.07/60.27 (P11(f5(a11,a12),a12)),
% 60.07/60.27 inference(scs_inference,[],[1718,1766,52,61,60,90,74,104,91,120,82])).
% 60.07/60.27 cnf(1798,plain,
% 60.07/60.27 (~E(a2,a4)),
% 60.07/60.27 inference(scs_inference,[],[65,1718,1766,52,61,60,90,74,104,91,120,82,2])).
% 60.07/60.27 cnf(1799,plain,
% 60.07/60.27 (P3(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1738,1718,1766,52,61,60,90,74,104,91,120,82,2,105])).
% 60.07/60.27 cnf(1801,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1738,1718,1766,52,61,60,90,74,104,91,120,82,2,105,107])).
% 60.07/60.27 cnf(1803,plain,
% 60.07/60.27 (~P5(f3(a2,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1738,1718,1766,52,61,795,60,90,74,104,91,120,82,2,105,107,42])).
% 60.07/60.27 cnf(1804,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a2,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1738,1718,1766,52,61,795,60,90,74,104,91,120,82,2,105,107,42,43])).
% 60.07/60.27 cnf(1805,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a1,a1),f3(a2,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1738,1718,1766,52,61,795,60,90,74,104,91,120,82,2,105,107,42,43,44])).
% 60.07/60.27 cnf(1806,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1738,1718,1766,52,61,795,60,90,74,104,91,120,82,2,105,107,42,43,44,45])).
% 60.07/60.27 cnf(1808,plain,
% 60.07/60.27 (~P8(f3(a2,a1),f3(a4,a1),x18081)),
% 60.07/60.27 inference(scs_inference,[],[65,1738,1718,1722,1766,637,52,61,720,795,60,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30])).
% 60.07/60.27 cnf(1809,plain,
% 60.07/60.27 (P2(a11,a11,a12)),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1738,1718,1722,1766,637,52,61,720,795,114,60,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92])).
% 60.07/60.27 cnf(1810,plain,
% 60.07/60.27 (P11(x18101,x18101)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(1812,plain,
% 60.07/60.27 (~P8(f3(a4,a1),x18121,f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1738,1735,1718,1722,1766,637,52,61,720,795,114,60,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29])).
% 60.07/60.27 cnf(1813,plain,
% 60.07/60.27 (~P6(f3(a4,a1),a1,x18131)),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1738,1735,1718,1722,1766,637,52,61,720,795,123,114,60,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34])).
% 60.07/60.27 cnf(1815,plain,
% 60.07/60.27 (~P6(f3(a1,a1),f3(a4,a1),x18151)),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1738,1735,1736,1718,1722,1766,637,52,61,720,795,123,114,60,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35])).
% 60.07/60.27 cnf(1816,plain,
% 60.07/60.27 (~P10(f3(a4,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1738,1743,1735,1736,1773,1718,1722,1766,637,52,61,720,795,123,114,60,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87])).
% 60.07/60.27 cnf(1818,plain,
% 60.07/60.27 (~P10(f3(a2,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1738,1740,1745,1743,1735,1736,1773,1718,1722,1766,637,52,61,720,795,123,114,60,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88])).
% 60.07/60.27 cnf(1822,plain,
% 60.07/60.27 (~P7(f3(a1,a1),x18221,a1)),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1761,1738,1740,1748,1745,1743,1735,1736,1773,1718,1722,1766,637,52,61,720,795,123,114,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39])).
% 60.07/60.27 cnf(1823,plain,
% 60.07/60.27 (~P7(f3(a4,a1),x18231,f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1761,1738,1740,1748,1745,1743,1735,1736,1747,1773,1718,1722,1766,637,52,61,720,795,123,114,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37])).
% 60.07/60.27 cnf(1829,plain,
% 60.07/60.27 (E(a1,f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1722,1766,637,52,61,720,58,795,123,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84])).
% 60.07/60.27 cnf(1831,plain,
% 60.07/60.27 (~P10(f5(a11,a12),a10)),
% 60.07/60.27 inference(scs_inference,[],[65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1766,637,52,200,61,720,58,795,123,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86])).
% 60.07/60.27 cnf(1837,plain,
% 60.07/60.27 (~P10(a1,f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1766,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33])).
% 60.07/60.27 cnf(1839,plain,
% 60.07/60.27 (E(f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1766,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3])).
% 60.07/60.27 cnf(1840,plain,
% 60.07/60.27 (~P10(f3(a1,a2),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1724,1766,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3,32])).
% 60.07/60.27 cnf(1841,plain,
% 60.07/60.27 (P4(f3(a1,a1),f3(a1,a1),f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1724,1766,1363,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3,32,26])).
% 60.07/60.27 cnf(1842,plain,
% 60.07/60.27 (P4(f3(a1,a1),f3(a1,a1),f3(a2,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1724,1766,1363,1365,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3,32,26,27])).
% 60.07/60.27 cnf(1843,plain,
% 60.07/60.27 (P4(f3(a2,a1),f3(a4,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1724,1766,1363,1365,1416,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3,32,26,27,25])).
% 60.07/60.27 cnf(1844,plain,
% 60.07/60.27 (P4(f3(a4,a1),f3(a1,a1),f3(a1,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1724,1766,1361,1363,1365,1416,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3,32,26,27,25,24])).
% 60.07/60.27 cnf(1845,plain,
% 60.07/60.27 (~P3(f3(a4,a1),x18451,x18452,x18453)+P3(a1,x18451,x18452,x18453)),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1724,1766,1361,1363,1365,1416,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3,32,26,27,25,24,46])).
% 60.07/60.27 cnf(1846,plain,
% 60.07/60.27 (~P3(f3(a4,a1),x18461,f3(a4,a1),x18462)+P3(a1,x18461,a1,x18462)),
% 60.07/60.27 inference(scs_inference,[],[66,65,1728,1761,1738,1740,1748,1745,1743,1726,1735,1736,1747,1773,1718,1716,1722,1724,1766,1361,1363,1365,1416,637,52,200,61,720,58,795,123,131,72,114,1810,60,191,90,74,104,91,120,82,2,105,107,42,43,44,45,47,30,92,29,34,35,87,88,89,39,37,94,93,84,86,95,83,33,3,32,26,27,25,24,46,48])).
% 60.07/60.27 cnf(1861,plain,
% 60.07/60.27 (P10(a9,f5(a9,a12))),
% 60.07/60.27 inference(scs_inference,[],[59,90])).
% 60.07/60.27 cnf(1865,plain,
% 60.07/60.27 (P11(f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[1839,1786,59,90,104,74])).
% 60.07/60.27 cnf(1867,plain,
% 60.07/60.27 (P10(f5(a9,a12),a12)),
% 60.07/60.27 inference(scs_inference,[],[1839,1786,59,90,104,74,91])).
% 60.07/60.27 cnf(1869,plain,
% 60.07/60.27 (P11(f5(a10,a12),a12)),
% 60.07/60.27 inference(scs_inference,[],[1839,1792,1786,59,90,104,74,91,82])).
% 60.07/60.27 cnf(1871,plain,
% 60.07/60.27 (~E(f5(a10,a11),a12)),
% 60.07/60.27 inference(scs_inference,[],[400,1839,1792,1786,59,90,104,74,91,82,2])).
% 60.07/60.27 cnf(1872,plain,
% 60.07/60.27 (~P5(f3(a4,a1),f3(a1,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1803,1839,1792,1786,59,90,104,74,91,82,2,42])).
% 60.07/60.27 cnf(1873,plain,
% 60.07/60.27 (E(f3(a4,a4),a4)),
% 60.07/60.27 inference(scs_inference,[],[400,1803,1839,1792,1786,1730,52,59,90,104,74,91,82,2,42,1783])).
% 60.07/60.27 cnf(1875,plain,
% 60.07/60.27 (P2(f3(a1,a1),f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1770,1803,1841,1839,1792,1786,1730,52,59,90,104,74,91,82,2,42,1783,106])).
% 60.07/60.27 cnf(1877,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a4,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1770,1803,1804,1841,1839,1792,1786,1730,52,59,90,104,74,91,82,2,42,1783,106,43])).
% 60.07/60.27 cnf(1878,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a1,a1),f3(a4,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1770,1803,1804,1805,1841,1839,1792,1786,1730,52,59,90,104,74,91,82,2,42,1783,106,43,44])).
% 60.07/60.27 cnf(1879,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a1,a1),f3(a1,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1770,1803,1804,1805,1806,1841,1839,1792,1786,1730,52,59,90,104,74,91,82,2,42,1783,106,43,44,45])).
% 60.07/60.27 cnf(1880,plain,
% 60.07/60.27 (~P8(f3(a1,a1),f3(a4,a1),x18801)),
% 60.07/60.27 inference(scs_inference,[],[400,1733,1770,1803,1804,1805,1806,1841,1839,1792,1786,1730,52,59,90,104,74,91,82,2,42,1783,106,43,44,45,30])).
% 60.07/60.27 cnf(1881,plain,
% 60.07/60.27 (~P6(f3(a4,a1),f3(a1,a1),x18811)),
% 60.07/60.27 inference(scs_inference,[],[400,1733,1737,1770,1803,1804,1805,1806,1841,1839,1792,1786,1730,52,59,90,104,74,91,82,2,42,1783,106,43,44,45,30,34])).
% 60.07/60.27 cnf(1883,plain,
% 60.07/60.27 (~P8(f3(a4,a1),f3(a1,a1),x18831)),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1841,1839,1813,1792,1786,1794,1730,52,59,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29])).
% 60.07/60.27 cnf(1884,plain,
% 60.07/60.27 (P2(a1,f3(a1,a2),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1841,1839,1775,1813,1792,1786,1794,1730,1773,52,59,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92])).
% 60.07/60.27 cnf(1886,plain,
% 60.07/60.27 (~P10(a4,f3(a2,a4))),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1841,1839,1775,1813,1788,1792,1786,1794,1730,1773,52,59,72,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87])).
% 60.07/60.27 cnf(1887,plain,
% 60.07/60.27 (~P10(x18871,x18871)),
% 60.07/60.27 inference(rename_variables,[],[72])).
% 60.07/60.27 cnf(1889,plain,
% 60.07/60.27 (~P10(a1,f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1841,1839,1775,1813,1788,1792,1786,1794,1730,1773,52,59,72,1887,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88])).
% 60.07/60.27 cnf(1890,plain,
% 60.07/60.27 (~P10(x18901,x18901)),
% 60.07/60.27 inference(rename_variables,[],[72])).
% 60.07/60.27 cnf(1892,plain,
% 60.07/60.27 (P11(f3(a1,a2),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1841,1839,1775,1813,1788,1792,1786,1794,1730,1773,52,59,72,1887,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89])).
% 60.07/60.27 cnf(1894,plain,
% 60.07/60.27 (~P7(f3(a4,a1),x18941,f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1841,1823,1839,1775,1813,1788,1792,1786,1794,1730,1773,52,59,795,72,1887,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89,39])).
% 60.07/60.27 cnf(1895,plain,
% 60.07/60.27 (~P7(f3(a2,a1),x18951,a1)),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1841,1823,1839,1775,1813,1822,1788,1792,1786,1794,1730,1773,52,59,795,72,1887,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89,39,37])).
% 60.07/60.27 cnf(1897,plain,
% 60.07/60.27 (P11(x18971,x18971)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(1907,plain,
% 60.07/60.27 (E(f3(a4,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[400,1731,1733,1737,1770,1803,1804,1805,1806,1816,1841,1823,1839,1775,1813,1822,1788,1792,1786,1794,1745,1730,1773,52,59,795,72,1887,1890,114,1897,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89,39,37,94,93,86,95,83])).
% 60.07/60.27 cnf(1910,plain,
% 60.07/60.27 (~E(a2,f3(a4,a2))),
% 60.07/60.27 inference(scs_inference,[],[1798,400,1731,1733,1737,1770,1803,1804,1805,1806,1816,1841,1823,1839,1775,1813,1822,1788,1792,1786,1794,1768,1745,1730,1773,52,59,795,72,1887,1890,114,1897,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89,39,37,94,93,86,95,83,33,3])).
% 60.07/60.27 cnf(1911,plain,
% 60.07/60.27 (~P10(f3(a1,a4),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1798,400,1731,1733,1737,1770,1803,1804,1805,1806,1816,1841,1823,1839,1775,1813,1822,1788,1837,1792,1786,1794,1768,1745,1730,1773,52,59,795,72,1887,1890,114,1897,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89,39,37,94,93,86,95,83,33,3,32])).
% 60.07/60.27 cnf(1913,plain,
% 60.07/60.27 (E(f3(a2,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1798,400,1731,1733,1737,1770,1803,1804,1805,1806,1816,1841,1823,1818,1839,1775,1813,1822,1788,1837,1792,1786,1794,1768,1745,1730,1773,202,52,59,795,72,1887,1890,114,1897,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89,39,37,94,93,86,95,83,33,3,32,22,75])).
% 60.07/60.27 cnf(1915,plain,
% 60.07/60.27 (P1(f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1798,400,1731,1733,1737,1770,1803,1804,1805,1806,1816,1841,1823,1818,1839,1775,1813,1822,1788,1829,1837,1792,1786,1794,1768,1745,1730,1773,202,52,59,795,50,72,1887,1890,114,1897,90,104,74,91,82,2,42,1783,106,43,44,45,30,34,35,29,92,87,88,89,39,37,94,93,86,95,83,33,3,32,22,75,20])).
% 60.07/60.27 cnf(1919,plain,
% 60.07/60.27 (P10(a9,f5(a9,a11))),
% 60.07/60.27 inference(scs_inference,[],[58,90])).
% 60.07/60.27 cnf(1921,plain,
% 60.07/60.27 (P10(f5(a9,a11),a11)),
% 60.07/60.27 inference(scs_inference,[],[58,90,91])).
% 60.07/60.27 cnf(1923,plain,
% 60.07/60.27 (P11(f3(a2,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1913,58,90,91,74])).
% 60.07/60.27 cnf(1925,plain,
% 60.07/60.27 (P11(f5(a9,a12),a12)),
% 60.07/60.27 inference(scs_inference,[],[1913,1867,58,90,91,74,82])).
% 60.07/60.27 cnf(1928,plain,
% 60.07/60.27 (~P5(f3(a4,a1),f3(a4,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1877,1913,1907,1867,58,90,91,74,82,2,42])).
% 60.07/60.27 cnf(1931,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a4,a1),f3(a4,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1877,1878,1913,1907,1867,1809,204,58,90,91,74,82,2,42,106,43])).
% 60.07/60.27 cnf(1932,plain,
% 60.07/60.27 (P2(f3(a4,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1877,1878,1913,1907,1867,1809,1738,204,58,90,91,74,82,2,42,106,43,21])).
% 60.07/60.27 cnf(1935,plain,
% 60.07/60.27 (~P5(f3(a4,a1),f3(a1,a1),f3(a4,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1892,1867,1809,1738,204,58,90,91,74,82,2,42,106,43,21,92,44])).
% 60.07/60.27 cnf(1936,plain,
% 60.07/60.27 (~P6(f3(a1,a1),f3(a2,a1),x19361)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1867,1809,1738,204,58,90,91,74,82,2,42,106,43,21,92,44,35])).
% 60.07/60.27 cnf(1937,plain,
% 60.07/60.27 (~P5(f3(a4,a1),f3(a1,a1),f3(a1,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1867,1809,1738,204,58,90,91,74,82,2,42,106,43,21,92,44,35,45])).
% 60.07/60.27 cnf(1938,plain,
% 60.07/60.27 (~P8(f3(a4,a1),f3(a2,a1),x19381)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1867,1809,127,1738,204,58,90,91,74,82,2,42,106,43,21,92,44,35,45,30])).
% 60.07/60.27 cnf(1939,plain,
% 60.07/60.27 (~P8(x19391,x19391,x19392)),
% 60.07/60.27 inference(rename_variables,[],[127])).
% 60.07/60.27 cnf(1940,plain,
% 60.07/60.27 (~P6(f3(a4,a4),a4,x19401)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1873,1867,1809,127,1738,204,58,123,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34])).
% 60.07/60.27 cnf(1944,plain,
% 60.07/60.27 (~P10(f3(a1,a1),f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1873,1889,1867,1809,127,1939,1738,204,709,58,123,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87])).
% 60.07/60.27 cnf(1946,plain,
% 60.07/60.27 (~P10(f3(a1,a2),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1840,1873,1889,1867,1809,127,1939,1745,1738,204,709,58,123,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88])).
% 60.07/60.27 cnf(1948,plain,
% 60.07/60.27 (~P11(a12,a10)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1840,1873,1889,1867,1809,127,1939,1745,1738,1728,204,709,58,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89])).
% 60.07/60.27 cnf(1950,plain,
% 60.07/60.27 (~P7(f3(a2,a1),x19501,f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1840,1873,1895,1889,1867,1809,127,1939,1724,1745,1738,1728,204,709,58,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39])).
% 60.07/60.27 cnf(1951,plain,
% 60.07/60.27 (~P7(f3(a4,a4),x19511,a4)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1840,1873,1895,1889,1867,1809,127,1939,1724,1745,1738,1728,204,709,58,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37])).
% 60.07/60.27 cnf(1953,plain,
% 60.07/60.27 (~P10(f3(a2,a1),a1)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1865,1907,1815,1892,1840,1873,1895,1889,1867,1809,127,1939,1724,1745,1738,1728,204,709,58,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37,94])).
% 60.07/60.27 cnf(1956,plain,
% 60.07/60.27 (~P10(f3(a1,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1881,1865,1907,1815,1892,1840,1873,1895,1889,1867,1809,127,1939,1724,1745,1738,1728,204,709,58,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37,94,93])).
% 60.07/60.27 cnf(1963,plain,
% 60.07/60.27 (~P10(f3(a1,a4),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1881,1865,1907,1815,1892,1840,1911,1873,1895,1889,1867,1861,1809,127,1939,1724,1745,1716,1738,1728,204,709,58,159,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37,94,93,86,95,33])).
% 60.07/60.27 cnf(1964,plain,
% 60.07/60.27 (~E(f3(a4,a1),a4)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1881,1865,1907,1815,1892,1840,1911,1873,1895,1765,1889,1867,1861,1809,127,1939,1724,1745,1716,1738,1728,204,709,58,159,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37,94,93,86,95,33,3])).
% 60.07/60.27 cnf(1966,plain,
% 60.07/60.27 (P2(f7(a11,a12,x19661,a10),a11,a12)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1881,1865,1907,1815,1892,1840,1911,1873,1895,1765,1886,1889,1867,1861,1809,127,1939,1724,1745,1716,1738,1728,204,709,58,159,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37,94,93,86,95,33,3,32,110])).
% 60.07/60.27 cnf(1968,plain,
% 60.07/60.27 (~P2(f7(a11,a12,x19681,a10),x19681,a10)),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1881,1865,1907,1815,1892,1840,1911,1873,1895,1765,1886,1889,1867,1861,1809,127,1939,1724,1745,1716,1738,1728,204,709,58,159,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37,94,93,86,95,33,3,32,110,113])).
% 60.07/60.27 cnf(1972,plain,
% 60.07/60.27 (P11(f3(a1,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[420,1872,1877,1878,1913,1881,1865,1907,1815,1892,1840,1911,1873,1895,1765,1886,1889,1867,1861,1809,127,1939,1724,1745,1716,1738,1728,204,709,58,159,125,123,199,90,91,74,82,2,42,106,43,21,92,44,35,45,30,34,29,87,88,89,39,37,94,93,86,95,33,3,32,110,113,101,100])).
% 60.07/60.27 cnf(1978,plain,
% 60.07/60.27 (P10(a9,f5(a9,a10))),
% 60.07/60.27 inference(scs_inference,[],[57,90])).
% 60.07/60.27 cnf(1980,plain,
% 60.07/60.27 (P11(f3(a4,a2),a4)),
% 60.07/60.27 inference(scs_inference,[],[1768,57,90,74])).
% 60.07/60.27 cnf(1982,plain,
% 60.07/60.27 (P10(f5(a9,a10),a10)),
% 60.07/60.27 inference(scs_inference,[],[1768,57,90,74,91])).
% 60.07/60.27 cnf(1984,plain,
% 60.07/60.27 (P11(f5(a9,a11),a11)),
% 60.07/60.27 inference(scs_inference,[],[1921,1768,57,90,74,91,82])).
% 60.07/60.27 cnf(1986,plain,
% 60.07/60.27 (P11(a11,f7(a11,a12,x19861,a10))),
% 60.07/60.27 inference(scs_inference,[],[1921,1966,1768,57,90,74,91,82,100])).
% 60.07/60.27 cnf(1991,plain,
% 60.07/60.27 (P2(f3(a4,a1),f3(a2,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1932,1842,1968,1910,1921,1966,1768,57,90,74,91,82,100,2,22,106])).
% 60.07/60.27 cnf(1993,plain,
% 60.07/60.27 (~P5(a1,f3(a4,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[1928,1932,1842,1968,1910,1921,1966,1829,1768,57,90,74,91,82,100,2,22,106,42])).
% 60.07/60.27 cnf(2000,plain,
% 60.07/60.27 (~P6(f3(a4,a4),f3(a4,a2),x20001)),
% 60.07/60.27 inference(scs_inference,[],[1928,1972,1932,1931,1842,1940,1968,1910,1921,1966,1726,1829,1768,202,57,90,74,91,82,100,2,22,106,42,92,43,21,44,35])).
% 60.07/60.27 cnf(2002,plain,
% 60.07/60.27 (~P6(f3(a4,a1),f3(a2,a1),x20021)),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1879,1931,1842,1940,1968,1910,1921,1966,1726,1829,1768,202,1907,57,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34])).
% 60.07/60.27 cnf(2003,plain,
% 60.07/60.27 (~P10(f3(a4,a1),a1)),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1879,1923,1931,1842,1940,1968,1910,1953,1921,1966,1726,1829,1768,202,1907,57,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87])).
% 60.07/60.27 cnf(2005,plain,
% 60.07/60.27 (~P8(f3(a1,a1),a1,x20051)),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1879,1923,1931,1880,1842,1940,1968,1910,1953,1921,1966,1726,1829,1768,202,1907,57,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30])).
% 60.07/60.27 cnf(2006,plain,
% 60.07/60.27 (~P10(a12,f5(a11,a12))),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1879,1923,1931,1880,1842,1940,1968,1910,1953,1796,1921,1966,1726,1829,1768,202,1907,57,72,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88])).
% 60.07/60.27 cnf(2007,plain,
% 60.07/60.27 (~P10(x20071,x20071)),
% 60.07/60.27 inference(rename_variables,[],[72])).
% 60.07/60.27 cnf(2009,plain,
% 60.07/60.27 (~P8(a1,f3(a2,a1),x20091)),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1880,1842,1940,1968,1910,1953,1796,1921,1966,1726,1829,1768,202,1907,57,72,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29])).
% 60.07/60.27 cnf(2010,plain,
% 60.07/60.27 (P11(f5(a9,a11),a12)),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1880,1842,1940,1968,1910,1953,1796,1921,1966,1726,1829,1768,202,1728,1907,57,72,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89])).
% 60.07/60.27 cnf(2019,plain,
% 60.07/60.27 (E(f3(a1,a2),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1880,1950,1944,1842,1940,1951,1968,1910,1953,1796,1921,1966,1840,1726,1829,1768,202,1728,1907,796,57,72,114,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89,39,37,94,93,75])).
% 60.07/60.27 cnf(2021,plain,
% 60.07/60.27 (E(f3(a1,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1880,1950,1944,1842,1940,1951,1968,1910,1953,1796,1921,1966,1840,1726,1829,1768,1745,202,1728,1907,796,57,72,114,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89,39,37,94,93,75,84])).
% 60.07/60.27 cnf(2023,plain,
% 60.07/60.27 (~P10(a11,f5(a9,a11))),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1880,1950,1944,1842,1940,1951,1968,1910,1953,1796,1921,1966,1840,1726,1829,1768,1745,202,1728,1907,796,57,72,2007,114,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89,39,37,94,93,75,84,86])).
% 60.07/60.27 cnf(2028,plain,
% 60.07/60.27 (~P10(f3(a1,a1),a1)),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1956,1880,1950,1944,1842,1940,1951,1968,1910,1953,1796,1921,1919,1966,1840,1726,1829,1768,1745,202,1728,1907,796,57,72,2007,114,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89,39,37,94,93,75,84,86,95,33])).
% 60.07/60.27 cnf(2029,plain,
% 60.07/60.27 (~E(f3(a1,a1),a4)),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1956,1880,1950,1944,1842,1940,1951,1968,1910,1953,1964,1796,1921,1919,1966,1840,1726,1829,1768,1745,202,1728,1907,796,57,72,2007,114,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89,39,37,94,93,75,84,86,95,33,3])).
% 60.07/60.27 cnf(2030,plain,
% 60.07/60.27 (~P10(f3(a4,a1),f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[1936,1928,1972,1932,1938,1879,1923,1931,1956,1880,1950,1944,1842,1940,1951,1968,1910,1953,1964,1796,1921,1919,1966,1840,1726,1829,1768,1745,202,1728,1907,796,57,72,2007,114,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89,39,37,94,93,75,84,86,95,33,3,32])).
% 60.07/60.27 cnf(2031,plain,
% 60.07/60.27 (~P11(a11,f5(a10,a11))+P10(a11,f5(a10,a11))),
% 60.07/60.27 inference(scs_inference,[],[294,1936,1928,1972,1932,1938,1879,1923,1931,1956,1880,1950,1944,1842,1940,1951,1968,1910,1953,1964,1796,1921,1919,1966,1840,1726,1829,1768,1745,202,1728,1907,796,57,72,2007,114,90,74,91,82,100,2,22,106,42,92,43,21,44,35,45,34,87,30,88,29,89,39,37,94,93,75,84,86,95,33,3,32,83])).
% 60.07/60.27 cnf(2035,plain,
% 60.07/60.27 (P10(a10,f5(a10,a11))),
% 60.07/60.27 inference(scs_inference,[],[60,90])).
% 60.07/60.27 cnf(2037,plain,
% 60.07/60.27 (P10(f5(a10,a11),a11)),
% 60.07/60.27 inference(scs_inference,[],[60,90,91])).
% 60.07/60.27 cnf(2039,plain,
% 60.07/60.27 (P11(f3(a1,a2),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[2019,60,90,91,74])).
% 60.07/60.27 cnf(2041,plain,
% 60.07/60.27 (P11(f5(a9,a10),a10)),
% 60.07/60.27 inference(scs_inference,[],[2019,1982,60,90,91,74,82])).
% 60.07/60.27 cnf(2043,plain,
% 60.07/60.27 (~E(a4,f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[2019,2029,1982,60,90,91,74,82,2])).
% 60.07/60.27 cnf(2044,plain,
% 60.07/60.27 (~P8(f3(a4,a1),x20441,f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[2019,1812,2029,1982,60,90,91,74,82,2,31])).
% 60.07/60.27 cnf(2049,plain,
% 60.07/60.27 (~P10(f7(a11,a12,x20491,a10),f5(a9,a11))),
% 60.07/60.27 inference(scs_inference,[],[1801,2019,1812,1980,2029,2023,1982,1986,60,114,90,91,74,82,2,31,92,42,87])).
% 60.07/60.27 cnf(2052,plain,
% 60.07/60.27 (~P10(f3(a1,a2),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[1801,2019,1946,1812,1980,2029,2023,1982,1986,1923,60,114,90,91,74,82,2,31,92,42,87,43,88])).
% 60.07/60.27 cnf(2056,plain,
% 60.07/60.27 (P2(f3(a4,a1),f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,2029,2023,1982,1986,1875,1923,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21])).
% 60.07/60.27 cnf(2058,plain,
% 60.07/60.27 (~P6(f3(a2,a1),f3(a1,a2),x20581)),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,2029,2023,1982,1986,1875,1737,1923,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35])).
% 60.07/60.27 cnf(2059,plain,
% 60.07/60.27 (~P6(f3(a1,a2),f3(a2,a1),x20591)),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,2029,2023,1982,1986,1875,1737,1936,1923,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34])).
% 60.07/60.27 cnf(2063,plain,
% 60.07/60.27 (~P7(f3(a4,a1),x20631,f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,2005,2029,2023,1982,1986,1875,1737,1936,1923,1823,1761,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39])).
% 60.07/60.27 cnf(2064,plain,
% 60.07/60.27 (~P7(f3(a2,a4),x20641,a4)),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,2005,2029,2023,1982,1986,1875,1737,1936,1923,1823,1761,1766,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37])).
% 60.07/60.27 cnf(2066,plain,
% 60.07/60.27 (P7(a11,f5(a9,a11),f5(a11,a12))),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,2005,2029,1984,2023,1982,1986,1875,1737,1936,1923,1823,1761,1766,1716,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94])).
% 60.07/60.27 cnf(2070,plain,
% 60.07/60.27 (~P10(a12,a11)),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,1869,2005,2029,1984,2006,2023,1982,1986,1875,1737,1936,1923,1823,1761,1766,1786,1716,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94,93,86])).
% 60.07/60.27 cnf(2072,plain,
% 60.07/60.27 (P8(a10,f5(a9,a10),f5(a10,a12))),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,1869,2005,2029,1984,2006,2023,1982,1986,1875,1737,1936,1923,1823,1761,1766,1786,1716,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94,93,86,95])).
% 60.07/60.27 cnf(2074,plain,
% 60.07/60.27 (E(f3(a1,a2),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,1869,2005,2029,1984,2006,2023,1982,1986,1875,1737,1936,1923,1892,1823,1761,1766,1786,1716,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94,93,86,95,83])).
% 60.07/60.27 cnf(2076,plain,
% 60.07/60.27 (~P10(f3(a2,a1),f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,1869,2005,2029,1984,2006,2023,1982,1986,1875,1737,1936,1923,1892,1823,1740,1761,1766,1786,1716,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94,93,86,95,83,33])).
% 60.07/60.27 cnf(2077,plain,
% 60.07/60.27 (E(f3(a1,a4),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,1869,2005,2029,1984,2006,2023,1982,1986,1875,1737,1936,1923,1892,1823,1740,1761,1766,1786,1794,1716,1829,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94,93,86,95,83,33,3])).
% 60.07/60.27 cnf(2078,plain,
% 60.07/60.27 (~E(f5(a9,a11),a12)),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,1869,2005,2029,1984,2006,2023,1982,1986,1875,1755,1737,1936,1923,1892,1823,1740,1761,1766,1786,1794,1716,1829,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94,93,86,95,83,33,3,40])).
% 60.07/60.27 cnf(2079,plain,
% 60.07/60.27 (~P10(f3(a1,a2),a1)),
% 60.07/60.27 inference(scs_inference,[],[1801,2021,2019,1883,1946,1812,1980,1869,2005,2028,2029,1984,2006,2023,1982,1986,1875,1755,1737,1936,1923,1892,1823,1740,1761,1766,1786,1794,1716,1829,125,60,114,90,91,74,82,2,31,92,42,87,43,88,45,30,21,44,35,34,29,89,39,37,94,93,86,95,83,33,3,40,32])).
% 60.07/60.27 cnf(2088,plain,
% 60.07/60.27 (P11(f3(a1,a4),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[2077,74])).
% 60.07/60.27 cnf(2090,plain,
% 60.07/60.27 (P11(f5(a10,a11),a11)),
% 60.07/60.27 inference(scs_inference,[],[2077,2037,74,82])).
% 60.07/60.27 cnf(2094,plain,
% 60.07/60.27 (~P5(f3(a4,a1),f3(a2,a1),f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2077,2037,2078,2021,74,82,2,48,107])).
% 60.07/60.27 cnf(2100,plain,
% 60.07/60.27 (~P2(f7(a11,a12,a1,a10),f3(a1,a2),a10)),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2077,2037,2078,2021,1968,1724,74,82,2,48,107,105,49,46,22])).
% 60.07/60.27 cnf(2107,plain,
% 60.07/60.27 (~P10(x21071,x21071)),
% 60.07/60.27 inference(rename_variables,[],[72])).
% 60.07/60.27 cnf(2110,plain,
% 60.07/60.27 (~P10(x21101,x21101)),
% 60.07/60.27 inference(rename_variables,[],[72])).
% 60.07/60.27 cnf(2114,plain,
% 60.07/60.27 (~P6(f3(a1,a1),f3(a1,a2),x21141)),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2039,1935,1937,2077,1993,2037,1925,2078,2010,2021,1968,714,1724,796,72,2107,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34])).
% 60.07/60.27 cnf(2115,plain,
% 60.07/60.27 (~P8(f3(a1,a2),f3(a2,a1),x21151)),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2039,1935,1937,2077,1993,2037,1925,2009,2078,2010,2021,1968,714,1724,796,72,2107,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29])).
% 60.07/60.27 cnf(2116,plain,
% 60.07/60.27 (~P6(f3(a1,a2),f3(a1,a1),x21161)),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,1935,1937,2077,1993,2037,1925,2009,2078,2010,2021,1968,714,1724,796,72,2107,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35])).
% 60.07/60.27 cnf(2117,plain,
% 60.07/60.27 (P11(f5(a9,a11),f7(a11,a12,x21171,a10))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,1935,1937,2077,1993,2037,1925,2009,2078,2010,2021,1968,714,1984,1724,1986,796,72,2107,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89])).
% 60.07/60.27 cnf(2119,plain,
% 60.07/60.27 (~E(f5(a11,a12),a10)),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,1935,1937,2077,1993,2037,1925,2009,2066,2078,2010,212,2021,1968,714,1984,1724,1986,796,72,2107,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39])).
% 60.07/60.27 cnf(2121,plain,
% 60.07/60.27 (~P7(f3(a1,a2),x21211,f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,1935,1937,2077,1993,2037,1925,2009,2066,2078,2010,1894,212,2021,1968,714,1984,1724,1986,796,72,2107,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37])).
% 60.07/60.27 cnf(2123,plain,
% 60.07/60.27 (P11(x21231,x21231)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(2127,plain,
% 60.07/60.27 (E(f3(a2,a1),f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,2052,2076,1935,1937,2077,1993,2037,1925,2009,2066,2078,2010,1894,212,2021,1968,714,1984,1724,1986,796,72,2107,114,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75])).
% 60.07/60.27 cnf(2131,plain,
% 60.07/60.27 (~P10(a11,f5(a10,a11))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,2052,2076,1935,1937,2077,1993,2037,1925,2009,2066,2078,2010,1894,212,2021,1968,714,1984,1724,1986,796,72,2107,2110,114,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86])).
% 60.07/60.27 cnf(2138,plain,
% 60.07/60.27 (~P10(f3(a1,a4),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,2052,2076,1935,1937,2077,1963,1993,2037,1925,2009,2066,2078,2010,2035,1894,212,2021,1968,714,1984,1724,1986,796,72,2107,2110,114,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86,95,83,33])).
% 60.07/60.27 cnf(2140,plain,
% 60.07/60.27 (P11(f3(a4,a1),f3(a1,a4))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,2052,2076,1935,1937,2077,1963,1993,2037,1925,2009,2066,2043,2078,2010,2035,1894,212,2021,1968,714,1984,1724,1986,796,1907,72,2107,2110,114,2123,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86,95,83,33,3,40])).
% 60.07/60.27 cnf(2141,plain,
% 60.07/60.27 (P11(x21411,x21411)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(2142,plain,
% 60.07/60.27 (~E(f5(a9,a10),f5(a11,a12))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,2052,2076,1935,1937,2077,1963,1993,2037,1831,1925,2009,2066,2043,2078,2010,2035,1894,212,2021,1968,714,1982,1984,1724,1986,796,1907,72,2107,2110,114,2123,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86,95,83,33,3,40,32])).
% 60.07/60.27 cnf(2143,plain,
% 60.07/60.27 (P11(f3(a1,a4),a1)),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2039,2052,2076,1935,1937,2077,1963,1993,2037,1831,1925,2009,2066,2043,2078,2010,2035,1894,212,2021,1968,714,1982,1984,1724,1986,1794,796,1907,72,2107,2110,114,2123,2141,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86,95,83,33,3,40,32,41])).
% 60.07/60.27 cnf(2148,plain,
% 60.07/60.27 (~P8(f3(a4,a1),x21481,f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2044,2039,2052,2076,1935,1937,2077,1963,1993,2037,1831,1925,2009,2066,2043,2078,2010,2035,1894,212,2021,1968,714,1982,1984,1724,1986,1794,796,1907,72,2107,2110,114,2123,2141,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86,95,83,33,3,40,32,41,1845,1846,47,31])).
% 60.07/60.27 cnf(2149,plain,
% 60.07/60.27 (~P8(f3(a2,a1),f3(a1,a2),x21491)),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2044,2039,2052,2076,1935,1937,1808,2077,1963,1993,2037,1831,1925,2009,2066,2043,2078,2010,2035,1894,212,2021,1968,714,1982,1984,1724,1986,1794,796,1907,72,2107,2110,114,2123,2141,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86,95,83,33,3,40,32,41,1845,1846,47,31,30])).
% 60.07/60.27 cnf(2150,plain,
% 60.07/60.27 (~P11(a11,f5(a10,a11))),
% 60.07/60.27 inference(scs_inference,[],[1799,2056,2074,2058,2059,2044,2039,2052,2076,1935,1937,1808,2077,1963,1993,2037,1831,1925,2009,2066,2043,2078,2010,2035,1894,212,2021,1968,714,1982,1984,1724,1986,1794,796,1907,72,2107,2110,114,2123,2141,74,82,2,48,107,105,49,46,22,92,42,43,87,88,44,45,34,29,35,89,39,37,94,93,75,84,86,95,83,33,3,40,32,41,1845,1846,47,31,30,2031])).
% 60.07/60.27 cnf(2153,plain,
% 60.07/60.27 (P11(f3(a2,a1),f3(a1,a2))),
% 60.07/60.27 inference(scs_inference,[],[2127,74])).
% 60.07/60.27 cnf(2155,plain,
% 60.07/60.27 (P11(a9,f5(a9,a10))),
% 60.07/60.27 inference(scs_inference,[],[2127,1978,74,82])).
% 60.07/60.27 cnf(2162,plain,
% 60.07/60.27 (~P2(f7(a11,a12,a1,a10),f3(a2,a1),a10)),
% 60.07/60.27 inference(scs_inference,[],[2127,2142,1978,2100,2072,157,1548,1770,74,82,2,31,106,22])).
% 60.07/60.27 cnf(2167,plain,
% 60.07/60.27 (~P5(f3(a4,a1),f3(a4,a1),f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[2070,2094,2127,2088,2140,2142,1978,2100,2090,2072,157,1548,1770,1839,74,82,2,31,106,22,92,88,43])).
% 60.07/60.27 cnf(2172,plain,
% 60.07/60.27 (~P5(f3(a4,a1),f3(a2,a1),f3(a4,a1),f3(a4,a1))),
% 60.07/60.27 inference(scs_inference,[],[2070,2094,2127,2030,2088,2140,2142,1978,2100,2090,2072,157,1548,1770,2077,1839,74,82,2,31,106,22,92,88,43,42,87,44,45])).
% 60.07/60.27 cnf(2184,plain,
% 60.07/60.27 (P10(f5(a10,a11),a12)),
% 60.07/60.27 inference(scs_inference,[],[2070,2148,2094,2127,2002,2063,2030,2088,2140,1871,2142,1978,2117,2041,2064,2100,2090,2150,2072,157,1548,1770,1815,1919,2035,2077,1873,1986,1839,74,82,2,31,106,22,92,88,43,42,87,44,45,34,35,29,89,39,37,94,93,75])).
% 60.07/60.27 cnf(2186,plain,
% 60.07/60.27 (E(f3(a4,a1),f3(a1,a4))),
% 60.07/60.27 inference(scs_inference,[],[2070,2148,2094,2127,2002,2063,2030,2088,2140,1871,2142,1978,2117,2041,2064,2100,2090,2150,2072,157,1548,1770,1815,1919,2035,2077,1873,1986,1839,74,82,2,31,106,22,92,88,43,42,87,44,45,34,35,29,89,39,37,94,93,75,84])).
% 60.07/60.27 cnf(2192,plain,
% 60.07/60.27 (~P11(f5(a11,a12),a10)),
% 60.07/60.27 inference(scs_inference,[],[2070,2148,2094,2127,2002,2063,2030,2088,2140,1871,2142,1978,2117,2049,2041,2064,2100,2090,2119,2150,2072,157,1548,1770,1815,1919,1831,2035,2077,1982,1873,1986,1839,74,82,2,31,106,22,92,88,43,42,87,44,45,34,35,29,89,39,37,94,93,75,84,86,95,83])).
% 60.07/60.27 cnf(2194,plain,
% 60.07/60.27 (~P10(f3(a1,a1),f3(a1,a4))),
% 60.07/60.27 inference(scs_inference,[],[2070,2148,2094,2127,2002,2063,2030,2088,2140,1871,2142,1978,2117,2049,2041,2064,2100,2090,2119,2150,2072,157,1548,1770,1956,1815,1919,1831,2035,2077,1982,1873,1986,1839,74,82,2,31,106,22,92,88,43,42,87,44,45,34,35,29,89,39,37,94,93,75,84,86,95,83,33])).
% 60.07/60.27 cnf(2195,plain,
% 60.07/60.27 (~E(f3(a1,a2),a4)),
% 60.07/60.27 inference(scs_inference,[],[2070,2148,2094,2127,2002,2063,2030,2088,2140,1871,2142,1978,2117,2049,2041,2064,2100,2090,2119,2150,2072,157,1548,1770,1956,1815,1919,1831,1765,2035,2077,1982,1873,1986,1839,74,82,2,31,106,22,92,88,43,42,87,44,45,34,35,29,89,39,37,94,93,75,84,86,95,83,33,3])).
% 60.07/60.27 cnf(2201,plain,
% 60.07/60.27 (P4(f3(a1,a2),f3(a4,a1),f3(a1,a1),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[2070,2148,2094,2127,2002,2063,2030,1843,1844,2088,2140,1871,2142,1978,2117,2049,2041,2064,2100,2090,2119,2150,2072,1948,157,1390,1548,1770,1956,1815,1919,1831,1765,1886,2035,2077,1982,1873,1986,1768,1839,74,82,2,31,106,22,92,88,43,42,87,44,45,34,35,29,89,39,37,94,93,75,84,86,95,83,33,3,40,32,41,27,25,24])).
% 60.07/60.27 cnf(2208,plain,
% 60.07/60.27 (P11(f3(a4,a4),a4)),
% 60.07/60.27 inference(scs_inference,[],[1873,74])).
% 60.07/60.27 cnf(2212,plain,
% 60.07/60.27 (~E(a10,f5(a11,a12))),
% 60.07/60.27 inference(scs_inference,[],[2184,2192,1873,74,82,136])).
% 60.07/60.27 cnf(2218,plain,
% 60.07/60.27 (~P10(f3(a4,a1),f3(a1,a4))),
% 60.07/60.27 inference(scs_inference,[],[2153,2003,2143,2195,2184,2192,2039,1968,1766,1873,74,82,136,2,92,22,88])).
% 60.07/60.27 cnf(2220,plain,
% 60.07/60.27 (~P10(f5(a9,a10),f5(a10,a11))),
% 60.07/60.27 inference(scs_inference,[],[2153,2003,2143,2195,2184,2192,2155,2039,1968,1766,1873,376,74,82,136,2,92,22,88,87])).
% 60.07/60.27 cnf(2222,plain,
% 60.07/60.27 (~P5(f3(a1,a1),f3(a4,a1),f3(a4,a1),f3(a2,a1))),
% 60.07/60.27 inference(scs_inference,[],[2167,2153,2003,2143,2195,2184,2192,2155,2039,1968,1766,2021,1873,376,74,82,136,2,92,22,88,87,42])).
% 60.07/60.27 cnf(2226,plain,
% 60.07/60.27 (~P8(f3(a1,a2),f3(a1,a1),x22261)),
% 60.07/60.27 inference(scs_inference,[],[2167,2153,2115,2186,2003,2143,2195,2184,2192,2155,1991,2039,1968,1766,2021,1873,796,376,74,82,136,2,92,22,88,87,42,44,21,43,30])).
% 60.07/60.27 cnf(2230,plain,
% 60.07/60.27 (~P8(f3(a1,a1),f3(a1,a2),x22301)),
% 60.07/60.27 inference(scs_inference,[],[2167,2172,2153,2149,2114,2115,2116,2186,2003,2143,2195,2184,2192,2155,1991,2039,1968,1766,2021,1873,1907,796,376,74,82,136,2,92,22,88,87,42,44,21,43,30,34,45,35,29])).
% 60.07/60.27 cnf(2231,plain,
% 60.07/60.27 (P11(a9,a10)),
% 60.07/60.27 inference(scs_inference,[],[2167,2172,2153,2149,2114,2115,2116,2186,2003,2143,2195,2184,2192,2155,1991,2039,2041,1968,1766,2021,1873,1907,796,376,74,82,136,2,92,22,88,87,42,44,21,43,30,34,45,35,29,89])).
% 60.07/60.27 cnf(2233,plain,
% 60.07/60.27 (~P7(f3(a1,a2),x22331,f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[2167,2172,2153,2149,2114,2115,2116,2121,2186,2003,2143,2195,2184,2192,2155,1991,2039,2041,1968,1766,2021,1873,1907,796,376,74,82,136,2,92,22,88,87,42,44,21,43,30,34,45,35,29,89,39])).
% 60.07/60.27 cnf(2236,plain,
% 60.07/60.27 (P11(x22361,x22361)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(2239,plain,
% 60.07/60.27 (P11(x22391,x22391)),
% 60.07/60.27 inference(rename_variables,[],[114])).
% 60.07/60.27 cnf(2241,plain,
% 60.07/60.27 (E(f3(a1,a4),f3(a1,a1))),
% 60.07/60.27 inference(scs_inference,[],[2167,2172,2153,2149,2114,2115,2116,2121,2194,2186,2138,2003,2143,2195,2184,2192,2155,1991,2039,1822,2041,1968,1766,2021,1873,1907,796,376,114,2236,74,82,136,2,92,22,88,87,42,44,21,43,30,34,45,35,29,89,39,37,94,93,75])).
% 60.07/60.27 cnf(2250,plain,
% 60.07/60.27 (~E(f5(a11,a12),f5(a10,a11))),
% 60.07/60.27 inference(scs_inference,[],[2167,2172,2153,2149,2114,2115,2116,2121,2194,2186,2138,2003,2143,2195,2184,2192,2155,2131,1991,400,2039,1915,1861,1822,2041,2035,1968,1766,2021,1716,1873,1907,796,376,114,2236,74,82,136,2,92,22,88,87,42,44,21,43,30,34,45,35,29,89,39,37,94,93,75,84,86,95,20,33])).
% 60.07/60.27 cnf(2252,plain,
% 60.07/60.27 (P11(a4,f3(a4,a4))),
% 60.07/60.27 inference(scs_inference,[],[2167,2172,2153,2149,2114,2115,2116,2121,2194,2186,2138,2003,2143,2195,2184,2192,2155,2131,1991,63,400,2039,1915,1861,1822,2041,2035,1968,1766,2021,1716,1873,1907,796,1829,376,114,2236,2239,74,82,136,2,92,22,88,87,42,44,21,43,30,34,45,35,29,89,39,37,94,93,75,84,86,95,20,33,3,40])).
% 60.07/60.27 cnf(2306,plain,
% 60.07/60.27 ($false),
% 60.07/60.27 inference(scs_inference,[],[2231,2222,2226,2230,2233,2201,2218,2241,2000,2250,2220,2079,2162,2208,2252,2212,1884,2116,2143,1747,1861,1726,1831,1766,1982,2035,1794,1913,1839,123,114,74,82,2,106,92,22,88,87,43,44,42,34,45,35,30,29,39,37,94,93,75,84,86]),
% 60.07/60.27 ['proof']).
% 60.07/60.27 % SZS output end Proof
% 60.07/60.27 % Total time :59.704954s
%------------------------------------------------------------------------------