%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET809+4 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:22:31 EDT 2024
% Result : Theorem 102.16s 102.49s
% Output : CNFRefutation 102.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.09 % Problem : SET809+4 : TPTP v8.2.0. Released v3.2.0.
% 0.05/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.28 % Computer : n021.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Sun Jun 23 16:09:23 EDT 2024
% 0.08/0.29 % CPUTime :
% 0.14/0.50 start to proof:theBenchmark
% 102.11/102.47 %-------------------------------------------
% 102.11/102.47 % File :CSE---1.7
% 102.11/102.47 % Problem :theBenchmark
% 102.11/102.47 % Transform :cnf
% 102.11/102.47 % Format :tptp:raw
% 102.11/102.47 % Command :java -jar mcs_scs.jar %d %s
% 102.11/102.47
% 102.11/102.47 % Result :Theorem 101.620000s
% 102.11/102.47 % Output :CNFRefutation 101.620000s
% 102.11/102.47 %-------------------------------------------
% 102.16/102.49 %------------------------------------------------------------------------------
% 102.16/102.49 % File : SET809+4 : TPTP v8.2.0. Released v3.2.0.
% 102.16/102.49 % Domain : Set Theory (Order relations)
% 102.16/102.49 % Problem : An ordinal number is not a member of itself
% 102.16/102.49 % Version : [Pas05] axioms.
% 102.16/102.49 % English :
% 102.16/102.49
% 102.16/102.49 % Refs : [Pas05] Pastre (2005), Email to G. Sutcliffe
% 102.16/102.49 % Source : [Pas05]
% 102.16/102.49 % Names :
% 102.16/102.49
% 102.16/102.49 % Status : Theorem
% 102.16/102.49 % Rating : 0.14 v8.2.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.13 v7.3.0, 0.07 v7.2.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.10 v6.4.0, 0.08 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.23 v6.0.0, 0.26 v5.4.0, 0.29 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.17 v4.1.0, 0.13 v4.0.0, 0.21 v3.7.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.21 v3.3.0, 0.14 v3.2.0
% 102.16/102.49 % Syntax : Number of formulae : 20 ( 1 unt; 0 def)
% 102.16/102.49 % Number of atoms : 67 ( 4 equ)
% 102.16/102.49 % Maximal formula atoms : 11 ( 3 avg)
% 102.16/102.49 % Number of connectives : 51 ( 4 ~; 3 |; 16 &)
% 102.16/102.49 % ( 17 <=>; 11 =>; 0 <=; 0 <~>)
% 102.16/102.49 % Maximal formula depth : 11 ( 6 avg)
% 102.16/102.49 % Maximal term depth : 3 ( 1 avg)
% 102.16/102.49 % Number of predicates : 9 ( 8 usr; 0 prp; 1-3 aty)
% 102.16/102.49 % Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% 102.16/102.49 % Number of variables : 57 ( 54 !; 3 ?)
% 102.16/102.49 % SPC : FOF_THM_RFO_SEQ
% 102.16/102.49
% 102.16/102.49 % Comments :
% 102.16/102.49 %------------------------------------------------------------------------------
% 102.16/102.49 %----Include set theory definitions
% 102.16/102.49 include('Axioms/SET006+0.ax').
% 102.16/102.49 %----Include ordinal numbers axioms
% 102.16/102.49 include('Axioms/SET006+4.ax').
% 102.16/102.49 %------------------------------------------------------------------------------
% 102.16/102.49 fof(thV2,conjecture,
% 102.16/102.49 ! [A] :
% 102.16/102.49 ( member(A,on)
% 102.16/102.49 => ~ member(A,A) ) ).
% 102.16/102.49
% 102.16/102.49 %------------------------------------------------------------------------------
% 102.16/102.49 %-------------------------------------------
% 102.16/102.49 % Proof found
% 102.16/102.49 % SZS status Theorem for theBenchmark
% 102.16/102.49 % SZS output start Proof
% 102.16/102.50 %ClaNum:143(EqnAxiom:63)
% 102.16/102.50 %VarNum:560(SingletonVarNum:186)
% 102.16/102.50 %MaxLitNum:7
% 102.16/102.50 %MaxfuncDepth:2
% 102.16/102.50 %SharedTerms:6
% 102.16/102.50 %goalClause: 64 65
% 102.16/102.50 %singleGoalClaCount:2
% 102.16/102.50 [64]P1(a1,a8)
% 102.16/102.50 [65]P1(a1,a1)
% 102.16/102.50 [66]~P1(x661,a2)
% 102.16/102.50 [68]P5(x681)+~P1(x681,a8)
% 102.16/102.50 [69]~P1(x691,a8)+P6(a9,x691)
% 102.16/102.50 [72]~P2(x722,x721)+P8(x721,x722)
% 102.16/102.50 [73]~P2(x731,x732)+P8(x731,x732)
% 102.16/102.50 [74]~P6(x741,x742)+P7(x741,x742)
% 102.16/102.50 [93]~P1(x931,x932)+P3(a9,x931,x932)
% 102.16/102.50 [111]P1(x1111,x1112)+~P3(a9,x1111,x1112)
% 102.16/102.50 [67]~E(x671,x672)+P1(x671,f21(x672))
% 102.16/102.50 [71]E(x711,x712)+~P1(x711,f21(x712))
% 102.16/102.50 [75]~P8(x751,x752)+P1(x751,f22(x752))
% 102.16/102.50 [78]P8(x781,x782)+~P1(x781,f22(x782))
% 102.16/102.50 [79]P8(x791,x792)+P1(f10(x791,x792),x791)
% 102.16/102.50 [83]P1(f11(x831,x832),x832)+P1(x831,f23(x832))
% 102.16/102.50 [90]~P1(x901,f26(x902))+P1(x901,f12(x901,x902))
% 102.16/102.50 [91]~P1(x911,f26(x912))+P1(f12(x911,x912),x912)
% 102.16/102.50 [99]P8(x991,x992)+~P1(f10(x991,x992),x992)
% 102.16/102.50 [100]~P1(x1001,f11(x1001,x1002))+P1(x1001,f23(x1002))
% 102.16/102.50 [101]~P1(x1011,f27(x1012))+P1(x1011,f25(x1012,f21(x1012)))
% 102.16/102.50 [113]P1(x1131,f27(x1132))+~P1(x1131,f25(x1132,f21(x1132)))
% 102.16/102.50 [112]P1(x1121,x1122)+~P4(x1121,x1123,x1122)
% 102.16/102.50 [76]~E(x761,x763)+P1(x761,f24(x762,x763))
% 102.16/102.50 [77]~E(x771,x772)+P1(x771,f24(x772,x773))
% 102.16/102.50 [85]~P1(x851,x853)+P1(x851,f25(x852,x853))
% 102.16/102.50 [86]~P1(x861,x862)+P1(x861,f25(x862,x863))
% 102.16/102.50 [96]P1(x961,x962)+~P1(x961,f16(x963,x962))
% 102.16/102.50 [97]P1(x971,x972)+~P1(x971,f16(x972,x973))
% 102.16/102.50 [98]P1(x981,x982)+~P1(x981,f3(x982,x983))
% 102.16/102.50 [103]~P1(x1031,x1032)+~P1(x1031,f3(x1033,x1032))
% 102.16/102.50 [129]P1(x1291,x1292)+~P1(x1291,f20(x1293,x1294,x1292))
% 102.16/102.50 [139]P3(x1391,x1392,x1393)+~P1(x1392,f20(x1393,x1391,x1394))
% 102.16/102.50 [70]~P1(x701,x702)+P5(x701)+~P5(x702)
% 102.16/102.50 [80]~P1(x801,x802)+P8(x801,x802)+~P1(x802,a8)
% 102.16/102.50 [82]~P8(x822,x821)+~P8(x821,x822)+P2(x821,x822)
% 102.16/102.50 [95]~P7(x951,x952)+P6(x951,x952)+P8(f14(x951,x952),x952)
% 102.16/102.51 [105]P7(x1051,x1052)+P1(f17(x1051,x1052),x1052)+P1(f4(x1051,x1052),x1052)
% 102.16/102.51 [106]P7(x1061,x1062)+P1(f17(x1061,x1062),x1062)+P1(f6(x1061,x1062),x1062)
% 102.16/102.51 [107]P7(x1071,x1072)+P1(f17(x1071,x1072),x1072)+P1(f7(x1071,x1072),x1072)
% 102.16/102.51 [108]P7(x1081,x1082)+P1(f5(x1081,x1082),x1082)+P1(f4(x1081,x1082),x1082)
% 102.16/102.51 [109]P7(x1091,x1092)+P1(f5(x1091,x1092),x1092)+P1(f6(x1091,x1092),x1092)
% 102.16/102.51 [110]P7(x1101,x1102)+P1(f5(x1101,x1102),x1102)+P1(f7(x1101,x1102),x1102)
% 102.16/102.51 [114]~P7(x1141,x1142)+P6(x1141,x1142)+P1(f18(x1141,x1142),f14(x1141,x1142))
% 102.16/102.51 [115]P7(x1151,x1152)+P3(x1151,f4(x1151,x1152),f6(x1151,x1152))+P1(f17(x1151,x1152),x1152)
% 102.16/102.51 [116]P7(x1161,x1162)+P3(x1161,f6(x1161,x1162),f7(x1161,x1162))+P1(f17(x1161,x1162),x1162)
% 102.16/102.51 [117]P7(x1171,x1172)+P3(x1171,f4(x1171,x1172),f6(x1171,x1172))+P1(f5(x1171,x1172),x1172)
% 102.16/102.51 [118]P7(x1181,x1182)+P3(x1181,f6(x1181,x1182),f7(x1181,x1182))+P1(f5(x1181,x1182),x1182)
% 102.16/102.51 [119]P7(x1191,x1192)+P3(x1191,f17(x1191,x1192),f5(x1191,x1192))+P1(f4(x1191,x1192),x1192)
% 102.16/102.51 [120]P7(x1201,x1202)+P3(x1201,f5(x1201,x1202),f17(x1201,x1202))+P1(f4(x1201,x1202),x1202)
% 102.16/102.51 [121]P7(x1211,x1212)+P3(x1211,f17(x1211,x1212),f5(x1211,x1212))+P1(f6(x1211,x1212),x1212)
% 102.16/102.51 [122]P7(x1221,x1222)+P3(x1221,f5(x1221,x1222),f17(x1221,x1222))+P1(f6(x1221,x1222),x1222)
% 102.16/102.51 [123]P7(x1231,x1232)+P3(x1231,f17(x1231,x1232),f5(x1231,x1232))+P1(f7(x1231,x1232),x1232)
% 102.16/102.51 [124]P7(x1241,x1242)+P3(x1241,f5(x1241,x1242),f17(x1241,x1242))+P1(f7(x1241,x1242),x1242)
% 102.16/102.51 [130]P7(x1301,x1302)+~P3(x1301,f4(x1301,x1302),f7(x1301,x1302))+P1(f17(x1301,x1302),x1302)
% 102.16/102.51 [131]P7(x1311,x1312)+~P3(x1311,f4(x1311,x1312),f7(x1311,x1312))+P1(f5(x1311,x1312),x1312)
% 102.16/102.51 [132]P7(x1321,x1322)+P3(x1321,f17(x1321,x1322),f5(x1321,x1322))+P3(x1321,f4(x1321,x1322),f6(x1321,x1322))
% 102.16/102.51 [133]P7(x1331,x1332)+P3(x1331,f17(x1331,x1332),f5(x1331,x1332))+P3(x1331,f6(x1331,x1332),f7(x1331,x1332))
% 102.16/102.51 [134]P7(x1341,x1342)+P3(x1341,f5(x1341,x1342),f17(x1341,x1342))+P3(x1341,f4(x1341,x1342),f6(x1341,x1342))
% 102.16/102.51 [135]P7(x1351,x1352)+P3(x1351,f5(x1351,x1352),f17(x1351,x1352))+P3(x1351,f6(x1351,x1352),f7(x1351,x1352))
% 102.16/102.51 [140]P7(x1401,x1402)+P3(x1401,f17(x1401,x1402),f5(x1401,x1402))+~P3(x1401,f4(x1401,x1402),f7(x1401,x1402))
% 102.16/102.51 [141]P7(x1411,x1412)+P3(x1411,f5(x1411,x1412),f17(x1411,x1412))+~P3(x1411,f4(x1411,x1412),f7(x1411,x1412))
% 102.16/102.51 [81]~P1(x811,x813)+P1(x811,x812)+~P8(x813,x812)
% 102.16/102.51 [87]~P1(x873,x872)+~P1(x871,x873)+P1(x871,f26(x872))
% 102.16/102.51 [88]E(x881,x882)+E(x881,x883)+~P1(x881,f24(x883,x882))
% 102.16/102.51 [89]P1(x891,x892)+~P1(x892,x893)+~P1(x891,f23(x893))
% 102.16/102.51 [94]~P1(x941,x943)+P1(x941,x942)+P1(x941,f3(x943,x942))
% 102.16/102.51 [102]~P1(x1021,x1023)+~P1(x1021,x1022)+P1(x1021,f16(x1022,x1023))
% 102.16/102.51 [104]P1(x1041,x1042)+P1(x1041,x1043)+~P1(x1041,f25(x1043,x1042))
% 102.16/102.51 [125]~P7(x1251,x1252)+P6(x1251,x1252)+~P4(x1253,x1251,f14(x1251,x1252))
% 102.16/102.51 [126]~P1(x1261,x1263)+P4(x1261,x1262,x1263)+~E(f19(x1262,x1263,x1261),x1261)
% 102.16/102.51 [128]~P1(x1281,x1283)+P4(x1281,x1282,x1283)+P1(f19(x1282,x1283,x1281),x1283)
% 102.16/102.51 [143]~P1(x1431,x1433)+P4(x1431,x1432,x1433)+~P3(x1432,x1431,f19(x1432,x1433,x1431))
% 102.16/102.51 [137]~P1(x1371,x1374)+~P3(x1373,x1371,x1372)+P1(x1371,f20(x1372,x1373,x1374))
% 102.16/102.51 [84]~P5(x841)+P1(f13(x841),x841)+~P6(a9,x841)+P1(x841,a8)
% 102.16/102.51 [92]~P5(x921)+~P6(a9,x921)+~P8(f13(x921),x921)+P1(x921,a8)
% 102.16/102.51 [127]~P4(x1272,x1273,x1274)+E(x1271,x1272)+P3(x1273,x1272,x1271)+~P1(x1271,x1274)
% 102.16/102.51 [136]~P8(x1363,x1362)+~P6(x1361,x1362)+~P1(x1364,x1363)+P4(f15(x1361,x1362,x1363),x1361,x1363)
% 102.16/102.51 [138]~P3(x1384,x1381,x1383)+~P3(x1384,x1383,x1381)+~P1(x1381,x1382)+~P1(x1383,x1382)+~P7(x1384,x1382)
% 102.16/102.51 [142]~P1(x1422,x1424)+~P7(x1421,x1424)+~P3(x1421,x1425,x1423)+~P3(x1421,x1422,x1425)+P3(x1421,x1422,x1423)+~P1(x1423,x1424)+~P1(x1425,x1424)
% 102.16/102.51 %EqnAxiom
% 102.16/102.51 [1]E(x11,x11)
% 102.16/102.51 [2]E(x22,x21)+~E(x21,x22)
% 102.16/102.51 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 102.16/102.51 [4]~E(x41,x42)+E(f21(x41),f21(x42))
% 102.16/102.51 [5]~E(x51,x52)+E(f19(x51,x53,x54),f19(x52,x53,x54))
% 102.16/102.51 [6]~E(x61,x62)+E(f19(x63,x61,x64),f19(x63,x62,x64))
% 102.16/102.51 [7]~E(x71,x72)+E(f19(x73,x74,x71),f19(x73,x74,x72))
% 102.16/102.51 [8]~E(x81,x82)+E(f22(x81),f22(x82))
% 102.16/102.51 [9]~E(x91,x92)+E(f24(x91,x93),f24(x92,x93))
% 102.16/102.51 [10]~E(x101,x102)+E(f24(x103,x101),f24(x103,x102))
% 102.16/102.51 [11]~E(x111,x112)+E(f4(x111,x113),f4(x112,x113))
% 102.16/102.51 [12]~E(x121,x122)+E(f4(x123,x121),f4(x123,x122))
% 102.16/102.51 [13]~E(x131,x132)+E(f7(x131,x133),f7(x132,x133))
% 102.16/102.51 [14]~E(x141,x142)+E(f7(x143,x141),f7(x143,x142))
% 102.16/102.51 [15]~E(x151,x152)+E(f10(x151,x153),f10(x152,x153))
% 102.16/102.51 [16]~E(x161,x162)+E(f10(x163,x161),f10(x163,x162))
% 102.16/102.51 [17]~E(x171,x172)+E(f23(x171),f23(x172))
% 102.16/102.51 [18]~E(x181,x182)+E(f11(x181,x183),f11(x182,x183))
% 102.16/102.51 [19]~E(x191,x192)+E(f11(x193,x191),f11(x193,x192))
% 102.16/102.51 [20]~E(x201,x202)+E(f13(x201),f13(x202))
% 102.16/102.51 [21]~E(x211,x212)+E(f25(x211,x213),f25(x212,x213))
% 102.16/102.51 [22]~E(x221,x222)+E(f25(x223,x221),f25(x223,x222))
% 102.16/102.51 [23]~E(x231,x232)+E(f5(x231,x233),f5(x232,x233))
% 102.16/102.51 [24]~E(x241,x242)+E(f5(x243,x241),f5(x243,x242))
% 102.16/102.51 [25]~E(x251,x252)+E(f26(x251),f26(x252))
% 102.16/102.51 [26]~E(x261,x262)+E(f17(x261,x263),f17(x262,x263))
% 102.16/102.51 [27]~E(x271,x272)+E(f17(x273,x271),f17(x273,x272))
% 102.16/102.51 [28]~E(x281,x282)+E(f6(x281,x283),f6(x282,x283))
% 102.16/102.51 [29]~E(x291,x292)+E(f6(x293,x291),f6(x293,x292))
% 102.16/102.51 [30]~E(x301,x302)+E(f12(x301,x303),f12(x302,x303))
% 102.16/102.51 [31]~E(x311,x312)+E(f12(x313,x311),f12(x313,x312))
% 102.16/102.51 [32]~E(x321,x322)+E(f20(x321,x323,x324),f20(x322,x323,x324))
% 102.16/102.51 [33]~E(x331,x332)+E(f20(x333,x331,x334),f20(x333,x332,x334))
% 102.16/102.51 [34]~E(x341,x342)+E(f20(x343,x344,x341),f20(x343,x344,x342))
% 102.16/102.51 [35]~E(x351,x352)+E(f3(x351,x353),f3(x352,x353))
% 102.16/102.51 [36]~E(x361,x362)+E(f3(x363,x361),f3(x363,x362))
% 102.16/102.51 [37]~E(x371,x372)+E(f27(x371),f27(x372))
% 102.16/102.51 [38]~E(x381,x382)+E(f16(x381,x383),f16(x382,x383))
% 102.16/102.51 [39]~E(x391,x392)+E(f16(x393,x391),f16(x393,x392))
% 102.16/102.51 [40]~E(x401,x402)+E(f14(x401,x403),f14(x402,x403))
% 102.16/102.51 [41]~E(x411,x412)+E(f14(x413,x411),f14(x413,x412))
% 102.16/102.51 [42]~E(x421,x422)+E(f15(x421,x423,x424),f15(x422,x423,x424))
% 102.16/102.51 [43]~E(x431,x432)+E(f15(x433,x431,x434),f15(x433,x432,x434))
% 102.16/102.51 [44]~E(x441,x442)+E(f15(x443,x444,x441),f15(x443,x444,x442))
% 102.16/102.51 [45]~E(x451,x452)+E(f18(x451,x453),f18(x452,x453))
% 102.16/102.51 [46]~E(x461,x462)+E(f18(x463,x461),f18(x463,x462))
% 102.16/102.51 [47]P1(x472,x473)+~E(x471,x472)+~P1(x471,x473)
% 102.16/102.51 [48]P1(x483,x482)+~E(x481,x482)+~P1(x483,x481)
% 102.16/102.51 [49]P3(x492,x493,x494)+~E(x491,x492)+~P3(x491,x493,x494)
% 102.16/102.51 [50]P3(x503,x502,x504)+~E(x501,x502)+~P3(x503,x501,x504)
% 102.16/102.51 [51]P3(x513,x514,x512)+~E(x511,x512)+~P3(x513,x514,x511)
% 102.16/102.51 [52]P4(x522,x523,x524)+~E(x521,x522)+~P4(x521,x523,x524)
% 102.16/102.51 [53]P4(x533,x532,x534)+~E(x531,x532)+~P4(x533,x531,x534)
% 102.16/102.51 [54]P4(x543,x544,x542)+~E(x541,x542)+~P4(x543,x544,x541)
% 102.16/102.51 [55]P7(x552,x553)+~E(x551,x552)+~P7(x551,x553)
% 102.16/102.51 [56]P7(x563,x562)+~E(x561,x562)+~P7(x563,x561)
% 102.16/102.51 [57]~P5(x571)+P5(x572)+~E(x571,x572)
% 102.16/102.51 [58]P6(x582,x583)+~E(x581,x582)+~P6(x581,x583)
% 102.16/102.51 [59]P6(x593,x592)+~E(x591,x592)+~P6(x593,x591)
% 102.16/102.51 [60]P8(x602,x603)+~E(x601,x602)+~P8(x601,x603)
% 102.16/102.51 [61]P8(x613,x612)+~E(x611,x612)+~P8(x613,x611)
% 102.16/102.51 [62]P2(x622,x623)+~E(x621,x622)+~P2(x621,x623)
% 102.16/102.51 [63]P2(x633,x632)+~E(x631,x632)+~P2(x633,x631)
% 102.16/102.51
% 102.16/102.51 %-------------------------------------------
% 102.16/102.53 cnf(144,plain,
% 102.16/102.53 (P1(x1441,f21(x1441))),
% 102.16/102.53 inference(equality_inference,[],[67])).
% 102.16/102.53 cnf(145,plain,
% 102.16/102.53 (P1(x1451,f24(x1452,x1451))),
% 102.16/102.53 inference(equality_inference,[],[76])).
% 102.16/102.53 cnf(146,plain,
% 102.16/102.53 (P1(x1461,f24(x1461,x1462))),
% 102.16/102.53 inference(equality_inference,[],[77])).
% 102.16/102.53 cnf(147,plain,
% 102.16/102.53 (P5(a1)),
% 102.16/102.53 inference(scs_inference,[],[64,68])).
% 102.16/102.53 cnf(149,plain,
% 102.16/102.53 (P8(a2,x1491)),
% 102.16/102.53 inference(scs_inference,[],[64,66,68,79])).
% 102.16/102.53 cnf(150,plain,
% 102.16/102.53 (~P1(x1501,a2)),
% 102.16/102.53 inference(rename_variables,[],[66])).
% 102.16/102.53 cnf(152,plain,
% 102.16/102.53 (~P1(x1521,f26(a2))),
% 102.16/102.53 inference(scs_inference,[],[64,66,150,68,79,91])).
% 102.16/102.53 cnf(153,plain,
% 102.16/102.53 (~P1(x1531,a2)),
% 102.16/102.53 inference(rename_variables,[],[66])).
% 102.16/102.54 cnf(155,plain,
% 102.16/102.54 (~P4(x1551,x1552,a2)),
% 102.16/102.54 inference(scs_inference,[],[64,66,150,153,68,79,91,112])).
% 102.16/102.54 cnf(157,plain,
% 102.16/102.54 (P8(a1,a1)),
% 102.16/102.54 inference(scs_inference,[],[64,65,66,150,153,68,79,91,112,80])).
% 102.16/102.54 cnf(161,plain,
% 102.16/102.54 (~E(a8,a2)),
% 102.16/102.54 inference(scs_inference,[],[64,65,66,150,153,68,79,91,112,80,82,48])).
% 102.16/102.54 cnf(162,plain,
% 102.16/102.54 (~P1(x1621,a2)),
% 102.16/102.54 inference(rename_variables,[],[66])).
% 102.16/102.54 cnf(166,plain,
% 102.16/102.54 (~P1(x1661,a2)),
% 102.16/102.54 inference(rename_variables,[],[66])).
% 102.16/102.54 cnf(167,plain,
% 102.16/102.54 (~P1(x1671,a2)),
% 102.16/102.54 inference(rename_variables,[],[66])).
% 102.16/102.54 cnf(168,plain,
% 102.16/102.54 (~P1(x1681,a2)),
% 102.16/102.54 inference(rename_variables,[],[66])).
% 102.16/102.54 cnf(170,plain,
% 102.16/102.54 (P7(x1701,a2)+~E(a1,f10(x1702,a8))+P1(f4(x1701,a2),a2)),
% 102.16/102.54 inference(scs_inference,[],[64,65,66,150,153,162,166,167,168,68,79,91,112,80,82,48,47,99,108])).
% 102.16/102.54 cnf(172,plain,
% 102.16/102.54 (~P1(x1721,f26(f26(a2)))),
% 102.16/102.54 inference(scs_inference,[],[152,91])).
% 102.16/102.54 cnf(173,plain,
% 102.16/102.54 (~P1(x1731,f26(a2))),
% 102.16/102.54 inference(rename_variables,[],[152])).
% 102.16/102.54 cnf(175,plain,
% 102.16/102.54 (P8(f26(a2),x1751)),
% 102.16/102.54 inference(scs_inference,[],[152,173,91,79])).
% 102.16/102.54 cnf(176,plain,
% 102.16/102.54 (~P1(x1761,f26(a2))),
% 102.16/102.54 inference(rename_variables,[],[152])).
% 102.16/102.54 cnf(178,plain,
% 102.16/102.54 (~P4(x1781,x1782,f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[152,173,176,91,79,112])).
% 102.16/102.54 cnf(180,plain,
% 102.16/102.54 (P2(a1,a1)),
% 102.16/102.54 inference(scs_inference,[],[157,152,173,176,91,79,112,82])).
% 102.16/102.54 cnf(182,plain,
% 102.16/102.54 (~E(a8,f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[64,157,152,173,176,91,79,112,82,48])).
% 102.16/102.54 cnf(183,plain,
% 102.16/102.54 (~P1(x1831,f26(a2))),
% 102.16/102.54 inference(rename_variables,[],[152])).
% 102.16/102.54 cnf(186,plain,
% 102.16/102.54 (P7(x1861,f26(a2))+P1(f6(x1861,f26(a2)),f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[64,157,152,173,176,183,66,91,79,112,82,48,170,109])).
% 102.16/102.54 cnf(201,plain,
% 102.16/102.54 (P7(x2011,f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[152,186])).
% 102.16/102.54 cnf(205,plain,
% 102.16/102.54 (P8(f26(f26(a2)),x2051)),
% 102.16/102.54 inference(scs_inference,[],[172,152,186,112,79])).
% 102.16/102.54 cnf(208,plain,
% 102.16/102.54 (P2(f26(a2),a2)),
% 102.16/102.54 inference(scs_inference,[],[149,172,175,152,186,112,79,82])).
% 102.16/102.54 cnf(225,plain,
% 102.16/102.54 (P2(f26(f26(a2)),a2)),
% 102.16/102.54 inference(scs_inference,[],[149,205,82])).
% 102.16/102.54 cnf(244,plain,
% 102.16/102.54 (~E(a1,f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[65,152,175,82,48])).
% 102.16/102.54 cnf(246,plain,
% 102.16/102.54 (P7(x2461,x2462)+~E(f26(a2),x2462)),
% 102.16/102.54 inference(scs_inference,[],[65,152,175,201,82,48,56])).
% 102.16/102.54 cnf(249,plain,
% 102.16/102.54 (~E(f21(x2491),f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[152,144,48])).
% 102.16/102.54 cnf(267,plain,
% 102.16/102.54 (~P1(x2671,a2)),
% 102.16/102.54 inference(rename_variables,[],[66])).
% 102.16/102.54 cnf(269,plain,
% 102.16/102.54 (~P1(x2691,a2)),
% 102.16/102.54 inference(rename_variables,[],[66])).
% 102.16/102.54 cnf(271,plain,
% 102.16/102.54 (P7(x2711,a2)+~E(f7(x2711,a2),x2712)),
% 102.16/102.54 inference(scs_inference,[],[152,66,267,269,145,155,48,110,128,47])).
% 102.16/102.54 cnf(284,plain,
% 102.16/102.54 (P7(x2841,a2)),
% 102.16/102.54 inference(equality_inference,[],[271])).
% 102.16/102.54 cnf(313,plain,
% 102.16/102.54 (P2(f26(a2),f26(f26(a2)))),
% 102.16/102.54 inference(scs_inference,[],[205,175,82])).
% 102.16/102.54 cnf(315,plain,
% 102.16/102.54 (P8(f26(f26(a2)),x3151)),
% 102.16/102.54 inference(rename_variables,[],[205])).
% 102.16/102.54 cnf(318,plain,
% 102.16/102.54 (P8(x3181,x3182)+~E(f26(f26(a2)),x3181)),
% 102.16/102.54 inference(scs_inference,[],[205,315,175,225,82,63,60])).
% 102.16/102.54 cnf(320,plain,
% 102.16/102.54 (P7(x3201,x3202)+~E(a2,x3202)),
% 102.16/102.54 inference(scs_inference,[],[205,315,175,284,225,82,63,60,62,56])).
% 102.16/102.54 cnf(326,plain,
% 102.16/102.54 (P8(x3261,x3262)+~E(a2,x3261)),
% 102.16/102.54 inference(scs_inference,[],[149,60])).
% 102.16/102.54 cnf(337,plain,
% 102.16/102.54 (P8(x3371,x3372)+~E(f26(a2),x3371)),
% 102.16/102.54 inference(scs_inference,[],[175,208,63,60])).
% 102.16/102.54 cnf(367,plain,
% 102.16/102.54 (P1(x3671,f24(x3672,x3673))+~E(x3673,x3671)),
% 102.16/102.54 inference(scs_inference,[],[145,313,63,62,47])).
% 102.16/102.54 cnf(381,plain,
% 102.16/102.54 (~P1(f26(a2),f21(a1))),
% 102.16/102.54 inference(scs_inference,[],[244,2,71])).
% 102.16/102.54 cnf(382,plain,
% 102.16/102.54 (~E(f26(a2),a1)),
% 102.16/102.54 inference(scs_inference,[],[381,67])).
% 102.16/102.54 cnf(421,plain,
% 102.16/102.54 (P1(a1,f22(a1))),
% 102.16/102.54 inference(scs_inference,[],[180,72,75])).
% 102.16/102.54 cnf(422,plain,
% 102.16/102.54 (~E(f22(a1),f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[152,421,48])).
% 102.16/102.54 cnf(462,plain,
% 102.16/102.54 (P1(f26(f26(a2)),f22(a2))),
% 102.16/102.54 inference(scs_inference,[],[225,73,75])).
% 102.16/102.54 cnf(463,plain,
% 102.16/102.54 (~E(f22(a2),f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[152,462,48])).
% 102.16/102.54 cnf(476,plain,
% 102.16/102.54 (~E(a1,a2)),
% 102.16/102.54 inference(scs_inference,[],[65,66,48])).
% 102.16/102.54 cnf(507,plain,
% 102.16/102.54 (~P6(x5071,x5072)+P7(x5073,x5072)+~E(x5071,x5073)),
% 102.16/102.54 inference(scs_inference,[],[74,55])).
% 102.16/102.54 cnf(539,plain,
% 102.16/102.54 (~P6(x5391,a1)+P4(f15(x5391,a1,a1),x5391,a1)),
% 102.16/102.54 inference(scs_inference,[],[421,65,78,136])).
% 102.16/102.54 cnf(851,plain,
% 102.16/102.54 (~E(f24(x8511,x8512),a2)),
% 102.16/102.54 inference(scs_inference,[],[66,146,48])).
% 102.16/102.54 cnf(856,plain,
% 102.16/102.54 (~E(f22(a1),a2)),
% 102.16/102.54 inference(scs_inference,[],[66,421,48])).
% 102.16/102.54 cnf(861,plain,
% 102.16/102.54 (~P1(x8611,f16(f3(a2,x8612),x8613))),
% 102.16/102.54 inference(scs_inference,[],[66,97,98])).
% 102.16/102.54 cnf(862,plain,
% 102.16/102.54 (P8(f16(f3(a2,x8621),x8622),x8623)),
% 102.16/102.54 inference(scs_inference,[],[861,79])).
% 102.16/102.54 cnf(863,plain,
% 102.16/102.54 (~P1(x8631,f16(f3(a2,x8632),x8633))),
% 102.16/102.54 inference(rename_variables,[],[861])).
% 102.16/102.54 cnf(867,plain,
% 102.16/102.54 (~P1(a1,f3(a2,x8671))),
% 102.16/102.54 inference(scs_inference,[],[64,861,863,79,112,102])).
% 102.16/102.54 cnf(873,plain,
% 102.16/102.54 (~E(f22(a2),a2)),
% 102.16/102.54 inference(scs_inference,[],[66,64,149,462,861,863,79,112,102,82,48])).
% 102.16/102.54 cnf(893,plain,
% 102.16/102.54 (~E(f21(x8931),a2)),
% 102.16/102.54 inference(scs_inference,[],[66,867,205,149,144,112,82,48])).
% 102.16/102.54 cnf(896,plain,
% 102.16/102.54 (P8(x8961,x8962)+~E(f16(f3(a2,x8963),x8964),x8961)),
% 102.16/102.54 inference(scs_inference,[],[66,867,205,149,144,862,112,82,48,63,60])).
% 102.16/102.54 cnf(948,plain,
% 102.16/102.54 (~P1(a1,f3(x9481,f25(x9482,a8)))),
% 102.16/102.54 inference(scs_inference,[],[64,103,85])).
% 102.16/102.54 cnf(951,plain,
% 102.16/102.54 (P1(a1,f25(x9511,a8))),
% 102.16/102.54 inference(scs_inference,[],[64,948,112,94])).
% 102.16/102.54 cnf(954,plain,
% 102.16/102.54 (~E(f25(x9541,a8),a2)),
% 102.16/102.54 inference(scs_inference,[],[66,64,948,112,94,48])).
% 102.16/102.54 cnf(1025,plain,
% 102.16/102.54 (P3(a9,x10251,f12(x10251,x10252))+~P1(x10251,f26(x10252))),
% 102.16/102.54 inference(scs_inference,[],[90,93])).
% 102.16/102.54 cnf(1056,plain,
% 102.16/102.54 (~P1(x10561,f11(x10561,f24(x10562,a2)))),
% 102.16/102.54 inference(scs_inference,[],[66,145,100,89])).
% 102.16/102.54 cnf(1057,plain,
% 102.16/102.54 (~P4(x10571,x10572,f11(x10571,f24(x10573,a2)))),
% 102.16/102.54 inference(scs_inference,[],[1056,112])).
% 102.16/102.54 cnf(1089,plain,
% 102.16/102.54 (~P1(a8,f20(x10891,x10892,f21(a2)))),
% 102.16/102.54 inference(scs_inference,[],[161,129,71])).
% 102.16/102.54 cnf(1092,plain,
% 102.16/102.54 (~P1(a8,f21(a2))+~P3(x10921,a8,x10922)),
% 102.16/102.54 inference(scs_inference,[],[1089,112,137])).
% 102.16/102.54 cnf(1124,plain,
% 102.16/102.54 (~P3(x11241,a8,x11242)+P1(a8,f3(f24(x11243,a8),f21(a2)))),
% 102.16/102.54 inference(scs_inference,[],[145,1092,94])).
% 102.16/102.54 cnf(1166,plain,
% 102.16/102.54 (~P1(x11661,f3(a2,x11662))),
% 102.16/102.54 inference(scs_inference,[],[144,861,102])).
% 102.16/102.54 cnf(1182,plain,
% 102.16/102.54 (~P1(x11821,f26(f3(a2,x11822)))),
% 102.16/102.54 inference(scs_inference,[],[1166,91])).
% 102.16/102.54 cnf(1183,plain,
% 102.16/102.54 (~P1(x11831,f3(a2,x11832))),
% 102.16/102.54 inference(rename_variables,[],[1166])).
% 102.16/102.54 cnf(1185,plain,
% 102.16/102.54 (~P4(x11851,x11852,f3(a2,x11853))),
% 102.16/102.54 inference(scs_inference,[],[1166,1183,91,112])).
% 102.16/102.54 cnf(1187,plain,
% 102.16/102.54 (P8(f3(a2,x11871),x11872)),
% 102.16/102.54 inference(scs_inference,[],[1166,1183,91,112,79])).
% 102.16/102.54 cnf(1205,plain,
% 102.16/102.54 (P8(f26(f3(a2,x12051)),x12052)),
% 102.16/102.54 inference(scs_inference,[],[1182,112,79])).
% 102.16/102.54 cnf(1214,plain,
% 102.16/102.54 (~P1(x12141,f3(a2,x12142))),
% 102.16/102.54 inference(rename_variables,[],[1166])).
% 102.16/102.54 cnf(1216,plain,
% 102.16/102.54 (P8(f3(a2,x12161),x12162)),
% 102.16/102.54 inference(rename_variables,[],[1187])).
% 102.16/102.54 cnf(1218,plain,
% 102.16/102.54 (P7(x12181,f3(a2,x12182))+~P6(x12183,x12184)),
% 102.16/102.54 inference(scs_inference,[],[64,948,1166,1214,862,205,1182,1185,1187,1216,112,79,82,48,108,81,136])).
% 102.16/102.54 cnf(1323,plain,
% 102.16/102.54 (~P1(x13231,f3(a2,x13232))),
% 102.16/102.54 inference(rename_variables,[],[1166])).
% 102.16/102.54 cnf(1327,plain,
% 102.16/102.54 (P8(x13271,x13272)+~E(f26(f3(a2,x13273)),x13271)),
% 102.16/102.54 inference(scs_inference,[],[1166,1323,462,1205,48,130,60])).
% 102.16/102.54 cnf(1332,plain,
% 102.16/102.54 (P8(x13321,x13322)+~E(f3(a2,x13323),x13321)),
% 102.16/102.54 inference(scs_inference,[],[1187,60])).
% 102.16/102.54 cnf(1345,plain,
% 102.16/102.54 (P7(x13451,f3(a2,x13452))),
% 102.16/102.54 inference(scs_inference,[],[64,1218,69])).
% 102.16/102.54 cnf(1346,plain,
% 102.16/102.54 (~E(f21(x13461),f3(a2,x13462))),
% 102.16/102.54 inference(scs_inference,[],[144,1166,48])).
% 102.16/102.54 cnf(1348,plain,
% 102.16/102.54 (P7(x13481,x13482)+~E(f3(a2,x13483),x13482)),
% 102.16/102.54 inference(scs_inference,[],[144,1166,1345,48,56])).
% 102.16/102.54 cnf(1375,plain,
% 102.16/102.54 (~E(f25(x13751,a8),f3(a2,x13752))),
% 102.16/102.54 inference(scs_inference,[],[951,1166,48])).
% 102.16/102.54 cnf(1384,plain,
% 102.16/102.54 (~E(f24(x13841,x13842),f3(a2,x13843))),
% 102.16/102.54 inference(scs_inference,[],[1166,145,48])).
% 102.16/102.54 cnf(1994,plain,
% 102.16/102.54 (P8(f27(x19941),x19942)+P1(f10(f27(x19941),x19942),f25(x19941,f21(x19941)))),
% 102.16/102.54 inference(scs_inference,[],[101,79])).
% 102.16/102.54 cnf(2025,plain,
% 102.16/102.54 (P8(x20251,f27(x20252))+~P1(f10(x20251,f27(x20252)),f25(x20252,f21(x20252)))),
% 102.16/102.54 inference(scs_inference,[],[113,99])).
% 102.16/102.54 cnf(2056,plain,
% 102.16/102.54 (~P1(x20561,f20(f3(a2,x20562),a9,x20563))),
% 102.16/102.54 inference(scs_inference,[],[1166,139,111])).
% 102.16/102.54 cnf(2057,plain,
% 102.16/102.54 (P8(f20(f3(a2,x20571),a9,x20572),x20573)),
% 102.16/102.54 inference(scs_inference,[],[2056,79])).
% 102.16/102.54 cnf(2058,plain,
% 102.16/102.54 (~P1(x20581,f20(f3(a2,x20582),a9,x20583))),
% 102.16/102.54 inference(rename_variables,[],[2056])).
% 102.16/102.54 cnf(2060,plain,
% 102.16/102.54 (~P4(x20601,x20602,f20(f3(a2,x20603),a9,x20604))),
% 102.16/102.54 inference(scs_inference,[],[2056,2058,79,112])).
% 102.16/102.54 cnf(2065,plain,
% 102.16/102.54 (~P3(a9,x20651,f3(a2,x20652))),
% 102.16/102.54 inference(scs_inference,[],[146,1205,2056,2058,79,112,82,137])).
% 102.16/102.54 cnf(2075,plain,
% 102.16/102.54 (P2(f26(f26(a2)),f3(a2,x20751))),
% 102.16/102.54 inference(scs_inference,[],[1187,205,82])).
% 102.16/102.54 cnf(2079,plain,
% 102.16/102.54 (P8(x20791,x20792)+~E(f20(f3(a2,x20793),a9,x20794),x20791)),
% 102.16/102.54 inference(scs_inference,[],[1187,205,2057,82,60])).
% 102.16/102.54 cnf(2093,plain,
% 102.16/102.54 (~P4(x20931,a9,f24(f3(a2,x20932),x20933))+E(f3(a2,x20932),x20931)),
% 102.16/102.54 inference(scs_inference,[],[146,2065,1187,2057,2075,82,62,63,127])).
% 102.16/102.54 cnf(2161,plain,
% 102.16/102.54 (P1(f15(x21611,a1,a1),a1)+~P6(x21611,a1)),
% 102.16/102.54 inference(scs_inference,[],[539,112])).
% 102.16/102.54 cnf(2192,plain,
% 102.16/102.54 (P1(f15(a9,a1,a1),a1)),
% 102.16/102.54 inference(scs_inference,[],[64,2161,69])).
% 102.16/102.54 cnf(2194,plain,
% 102.16/102.54 (P8(x21941,a1)+~E(f15(a9,a1,a1),f10(x21941,a1))),
% 102.16/102.54 inference(scs_inference,[],[2192,47,99])).
% 102.16/102.54 cnf(2221,plain,
% 102.16/102.54 (~P4(x22211,a9,f24(x22212,f3(a2,x22213)))+E(f3(a2,x22213),x22211)),
% 102.16/102.54 inference(scs_inference,[],[2065,145,127])).
% 102.16/102.54 cnf(2233,plain,
% 102.16/102.54 (P3(a9,a1,f12(a1,a8))),
% 102.16/102.54 inference(scs_inference,[],[64,65,1025,87])).
% 102.16/102.54 cnf(2234,plain,
% 102.16/102.54 (P1(a1,f12(a1,a8))),
% 102.16/102.54 inference(scs_inference,[],[2233,111])).
% 102.16/102.54 cnf(2236,plain,
% 102.16/102.54 (~E(f12(a1,a8),f3(a2,x22361))),
% 102.16/102.54 inference(scs_inference,[],[1166,2233,111,48])).
% 102.16/102.54 cnf(2397,plain,
% 102.16/102.54 (~E(f10(x23971,a1),f15(a9,a1,a1))+P8(x23971,a1)),
% 102.16/102.54 inference(scs_inference,[],[2194,2])).
% 102.16/102.54 cnf(2473,plain,
% 102.16/102.54 (P8(x24731,a1)+~P1(f10(x24731,a1),f21(f15(a9,a1,a1)))),
% 102.16/102.54 inference(scs_inference,[],[2397,71])).
% 102.16/102.54 cnf(2799,plain,
% 102.16/102.54 (~P4(x27991,a9,f21(f3(a2,x27992)))+E(f3(a2,x27992),x27991)),
% 102.16/102.54 inference(scs_inference,[],[149,2065,1205,144,82,62,63,127])).
% 102.16/102.54 cnf(2846,plain,
% 102.16/102.54 (P1(a8,f3(f24(x28461,a8),f21(a2)))),
% 102.16/102.54 inference(scs_inference,[],[144,1124,93])).
% 102.16/102.54 cnf(2847,plain,
% 102.16/102.54 (~P1(a8,f21(a2))),
% 102.16/102.54 inference(scs_inference,[],[2846,103])).
% 102.16/102.54 cnf(2858,plain,
% 102.16/102.54 (~E(a2,a8)),
% 102.16/102.54 inference(scs_inference,[],[2847,144,47])).
% 102.16/102.54 cnf(2904,plain,
% 102.16/102.54 (P8(f21(f15(a9,a1,a1)),a1)),
% 102.16/102.54 inference(scs_inference,[],[2473,79])).
% 102.16/102.54 cnf(3212,plain,
% 102.16/102.54 (P8(f27(x32121),f27(x32121))),
% 102.16/102.54 inference(scs_inference,[],[1994,2025])).
% 102.16/102.54 cnf(3353,plain,
% 102.16/102.54 (~E(f25(x33531,a8),f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[152,951,48])).
% 102.16/102.54 cnf(3369,plain,
% 102.16/102.54 (~E(f12(a1,a8),f26(a2))),
% 102.16/102.54 inference(scs_inference,[],[152,2234,48])).
% 102.16/102.54 cnf(6347,plain,
% 102.16/102.54 (~P1(a2,f16(x63471,f24(a8,a8)))),
% 102.16/102.54 inference(scs_inference,[],[2858,88,96])).
% 102.16/102.54 cnf(6350,plain,
% 102.16/102.54 (~P1(a2,f24(a8,a8))),
% 102.16/102.54 inference(scs_inference,[],[145,6347,112,102])).
% 102.16/102.54 cnf(6431,plain,
% 102.16/102.54 (~P1(a2,f25(f26(f26(a2)),f21(a8)))),
% 102.16/102.54 inference(scs_inference,[],[172,2858,104,71])).
% 102.16/102.54 cnf(6432,plain,
% 102.16/102.54 (~P1(a2,f21(a8))),
% 102.16/102.54 inference(scs_inference,[],[6431,85])).
% 102.16/102.54 cnf(8865,plain,
% 102.16/102.54 (~E(a2,a1)),
% 102.16/102.54 inference(scs_inference,[],[476,2])).
% 102.16/102.54 cnf(8866,plain,
% 102.16/102.54 (~P1(a1,f21(a2))),
% 102.16/102.54 inference(scs_inference,[],[476,2,71])).
% 102.16/102.54 cnf(8870,plain,
% 102.16/102.54 (P1(a1,f25(a8,x88701))),
% 102.16/102.54 inference(scs_inference,[],[64,476,2904,2,71,75,86])).
% 102.16/102.54 cnf(8878,plain,
% 102.16/102.54 (P1(x88781,f23(a2))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2904,66,2,71,75,86,96,97,129,83])).
% 102.16/102.54 cnf(8881,plain,
% 102.16/102.54 (P3(a9,a1,a8)),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2904,66,2,71,75,86,96,97,129,83,93])).
% 102.16/102.54 cnf(8883,plain,
% 102.16/102.54 (P1(f15(a9,a1,a1),f25(x88831,a1))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2192,2904,66,2,71,75,86,96,97,129,83,93,85])).
% 102.16/102.54 cnf(8885,plain,
% 102.16/102.54 (P6(a9,a1)),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2192,2904,66,2,71,75,86,96,97,129,83,93,85,69])).
% 102.16/102.54 cnf(8887,plain,
% 102.16/102.54 (~P3(a9,a2,f21(a8))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2192,2904,66,2,71,75,86,96,97,129,83,93,85,69,111])).
% 102.16/102.54 cnf(8891,plain,
% 102.16/102.54 (~P1(a1,f3(x88911,a8))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2192,2904,66,2,71,75,86,96,97,129,83,93,85,69,111,98,103])).
% 102.16/102.54 cnf(8895,plain,
% 102.16/102.54 (~P1(x88951,f23(f22(a2)))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2192,147,2904,462,172,66,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89])).
% 102.16/102.54 cnf(8897,plain,
% 102.16/102.54 (~P1(a1,f24(a2,a2))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2192,147,2904,462,172,66,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88])).
% 102.16/102.54 cnf(8903,plain,
% 102.16/102.54 (P1(a1,f16(a8,a8))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,172,66,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102])).
% 102.16/102.54 cnf(8905,plain,
% 102.16/102.54 (P1(f15(a9,a1,a1),f26(a8))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,172,66,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87])).
% 102.16/102.54 cnf(8908,plain,
% 102.16/102.54 (P1(x89081,f21(x89081))),
% 102.16/102.54 inference(rename_variables,[],[144])).
% 102.16/102.54 cnf(8914,plain,
% 102.16/102.54 (P7(a9,a1)),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74])).
% 102.16/102.54 cnf(8916,plain,
% 102.16/102.54 (~E(a2,f21(a2))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326])).
% 102.16/102.54 cnf(8918,plain,
% 102.16/102.54 (~E(f3(a2,x89181),f21(a2))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326,337,1332])).
% 102.16/102.54 cnf(8919,plain,
% 102.16/102.54 (P1(f15(a9,a1,a1),f12(f15(a9,a1,a1),a8))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326,337,1332,90])).
% 102.16/102.54 cnf(8934,plain,
% 102.16/102.54 (~P1(f21(a2),f22(f21(a8)))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326,337,1332,90,139,1327,896,1025,2079,2799,2093,2221,78])).
% 102.16/102.54 cnf(8936,plain,
% 102.16/102.54 (P1(f12(f15(a9,a1,a1),a8),a8)),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326,337,1332,90,139,1327,896,1025,2079,2799,2093,2221,78,91])).
% 102.16/102.54 cnf(8940,plain,
% 102.16/102.54 (P1(f10(f21(a2),f21(a8)),f21(a2))),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326,337,1332,90,139,1327,896,1025,2079,2799,2093,2221,78,91,99,79])).
% 102.16/102.54 cnf(8946,plain,
% 102.16/102.54 (P8(f15(a9,a1,a1),a1)),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,205,144,172,66,145,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326,337,1332,90,139,1327,896,1025,2079,2799,2093,2221,78,91,99,79,57,143,80])).
% 102.16/102.54 cnf(8950,plain,
% 102.16/102.54 (P4(f15(a9,a1,a1),a9,a1)),
% 102.16/102.54 inference(scs_inference,[],[64,476,6432,2847,2192,147,2904,462,2846,157,205,144,8908,172,66,145,2233,2,71,75,86,96,97,129,83,93,85,69,111,98,103,70,89,88,104,94,102,87,81,60,137,74,326,337,1332,90,139,1327,896,1025,2079,2799,2093,2221,78,91,99,79,57,143,80,47,136])).
% 102.16/102.54 cnf(8961,plain,
% 102.16/102.54 (P1(f15(a9,a1,a1),f22(a1))),
% 102.16/102.54 inference(scs_inference,[],[8946,8891,97,75])).
% 102.16/102.54 cnf(8965,plain,
% 102.16/102.54 (P1(x89651,f23(f26(a2)))),
% 102.16/102.54 inference(scs_inference,[],[8946,8891,152,97,75,129,83])).
% 102.16/102.54 cnf(8968,plain,
% 102.16/102.54 (~P1(a2,f21(a1))),
% 102.16/102.54 inference(scs_inference,[],[8865,8946,8891,152,97,75,129,83,71])).
% 102.16/102.54 cnf(8970,plain,
% 102.16/102.54 (P1(x89701,f25(f23(a2),x89702))),
% 102.16/102.54 inference(scs_inference,[],[8865,8878,8946,8891,152,97,75,129,83,71,86])).
% 102.16/102.54 cnf(8974,plain,
% 102.16/102.54 (P1(x89741,f25(x89742,f23(a2)))),
% 102.16/102.54 inference(scs_inference,[],[8865,8878,8946,8891,152,97,75,129,83,71,86,96,85])).
% 102.16/102.54 cnf(8978,plain,
% 102.16/102.54 (P3(a9,x89781,f23(a2))),
% 102.16/102.54 inference(scs_inference,[],[8865,8878,8946,8891,8936,152,97,75,129,83,71,86,96,85,69,93])).
% 102.16/102.54 cnf(8980,plain,
% 102.16/102.54 (~E(f26(a2),a8)),
% 102.16/102.54 inference(scs_inference,[],[8865,182,8878,8946,8891,8936,152,97,75,129,83,71,86,96,85,69,93,2])).
% 102.16/102.54 cnf(8981,plain,
% 102.16/102.54 (~P3(a9,a1,f3(x89811,a8))),
% 102.16/102.54 inference(scs_inference,[],[8865,182,8878,8946,8891,8936,152,97,75,129,83,71,86,96,85,69,93,2,111])).
% 102.16/102.54 cnf(8990,plain,
% 102.16/102.54 (P1(x89901,f23(a2))),
% 102.16/102.54 inference(rename_variables,[],[8878])).
% 102.16/102.54 cnf(8996,plain,
% 102.16/102.54 (~P1(a2,f24(a1,a1))),
% 102.16/102.54 inference(scs_inference,[],[64,8865,182,8878,8946,8891,8950,1057,8936,152,97,75,129,83,71,86,96,85,69,93,2,111,103,98,54,89,104,94,88])).
% 102.16/102.54 cnf(8999,plain,
% 102.16/102.54 (P1(x89991,f23(a2))),
% 102.16/102.54 inference(rename_variables,[],[8878])).
% 102.16/102.54 cnf(9006,plain,
% 102.16/102.54 (~P8(a8,f3(x90061,a8))),
% 102.16/102.54 inference(scs_inference,[],[64,8865,8881,182,8878,8990,8999,8946,8891,8950,8866,1057,8936,152,97,75,129,83,71,86,96,85,69,93,2,111,103,98,54,89,104,94,88,102,87,51,48,81])).
% 102.16/102.54 cnf(9008,plain,
% 102.16/102.54 (P1(a1,f20(a8,a9,a8))),
% 102.16/102.54 inference(scs_inference,[],[64,8865,8881,182,8878,8990,8999,8946,8891,8950,8866,1057,8936,152,97,75,129,83,71,86,96,85,69,93,2,111,103,98,54,89,104,94,88,102,87,51,48,81,137])).
% 102.16/102.54 cnf(9027,plain,
% 102.16/102.54 (P1(f10(a8,f3(a2,a8)),a8)),
% 102.16/102.54 inference(scs_inference,[],[64,8865,8881,182,8878,8990,8999,8918,8946,8891,8950,8866,1057,8936,2065,152,97,75,129,83,71,86,96,85,69,93,2,111,103,98,54,89,104,94,88,102,87,51,48,81,137,127,318,74,78,90,1327,2079,1332,896,1025,79])).
% 102.16/102.54 cnf(9031,plain,
% 102.16/102.54 (~P3(a9,f15(a9,a1,a1),f15(a9,a1,a1))),
% 102.16/102.54 inference(scs_inference,[],[64,8865,8881,182,8878,8990,8999,8918,8946,8891,8950,8866,1057,8919,8936,284,2065,152,97,75,129,83,71,86,96,85,69,93,2,111,103,98,54,89,104,94,88,102,87,51,48,81,137,127,318,74,78,90,1327,2079,1332,896,1025,79,95,138])).
% 102.16/102.54 cnf(9037,plain,
% 102.16/102.54 (~P1(f15(a9,a1,a1),f20(f15(a9,a1,a1),a9,x90371))),
% 102.16/102.54 inference(scs_inference,[],[64,8865,8881,182,8878,8990,8999,8918,8946,8891,8950,8866,1057,8919,8936,284,2065,152,97,75,129,83,71,86,96,85,69,93,2,111,103,98,54,89,104,94,88,102,87,51,48,81,137,127,318,74,78,90,1327,2079,1332,896,1025,79,95,138,2221,2093,139])).
% 102.16/102.55 cnf(9044,plain,
% 102.16/102.55 (P1(f27(x90441),f22(f27(x90441)))),
% 102.16/102.55 inference(scs_inference,[],[8968,3212,129,75])).
% 102.16/102.55 cnf(9050,plain,
% 102.16/102.55 (P1(x90501,f23(f3(a2,x90502)))),
% 102.16/102.55 inference(scs_inference,[],[8903,9006,8968,3212,1166,129,75,86,78,83])).
% 102.16/102.55 cnf(9067,plain,
% 102.16/102.55 (~P1(f10(a8,f3(x90671,a8)),f3(x90671,a8))),
% 102.16/102.55 inference(scs_inference,[],[422,8903,9006,8968,8981,9027,3212,1166,129,75,86,78,83,85,96,97,71,139,93,69,99])).
% 102.16/102.55 cnf(9070,plain,
% 102.16/102.55 (~P3(a9,a2,f21(a1))),
% 102.16/102.55 inference(scs_inference,[],[422,8903,9006,8968,8981,9027,3212,1166,129,75,86,78,83,85,96,97,71,139,93,69,99,2,111])).
% 102.16/102.55 cnf(9074,plain,
% 102.16/102.55 (~P1(a1,f3(x90741,f16(a8,a8)))),
% 102.16/102.55 inference(scs_inference,[],[422,8903,9006,8968,8981,9027,3212,1166,129,75,86,78,83,85,96,97,71,139,93,69,99,2,111,98,103])).
% 102.16/102.55 cnf(9076,plain,
% 102.16/102.55 (P1(f10(a8,f3(x90761,a8)),a8)),
% 102.16/102.55 inference(scs_inference,[],[422,8903,9006,8968,8981,9027,3212,1166,129,75,86,78,83,85,96,97,71,139,93,69,99,2,111,98,103,79])).
% 102.16/102.55 cnf(9083,plain,
% 102.16/102.55 (~P1(f26(a2),f24(a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[382,422,8903,9006,8968,8981,9027,8878,3212,1166,129,75,86,78,83,85,96,97,71,139,93,69,99,2,111,98,103,79,94,104,88])).
% 102.16/102.55 cnf(9117,plain,
% 102.16/102.55 (P1(f20(f3(a2,x91171),a9,x91172),f22(x91173))),
% 102.16/102.55 inference(scs_inference,[],[8961,2057,86,75])).
% 102.16/102.55 cnf(9125,plain,
% 102.16/102.55 (~P1(f26(a2),f20(x91251,x91252,f24(a1,a1)))),
% 102.16/102.55 inference(scs_inference,[],[8961,9083,2057,86,75,85,97,96,129])).
% 102.16/102.55 cnf(9133,plain,
% 102.16/102.55 (~P3(a9,f26(a2),f24(a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[463,8961,9083,9070,2057,86,75,85,97,96,129,139,93,71,111])).
% 102.16/102.55 cnf(9137,plain,
% 102.16/102.55 (~E(f26(a2),f22(a2))),
% 102.16/102.55 inference(scs_inference,[],[463,8961,9083,9070,9076,2057,86,75,85,97,96,129,139,93,71,111,69,2])).
% 102.16/102.55 cnf(9175,plain,
% 102.16/102.55 (P1(f26(f26(a2)),f22(x91751))),
% 102.16/102.55 inference(scs_inference,[],[8883,205,85,75])).
% 102.16/102.55 cnf(9187,plain,
% 102.16/102.55 (P3(a9,f15(a9,a1,a1),f25(x91871,a1))),
% 102.16/102.55 inference(scs_inference,[],[8883,9133,8996,205,85,75,129,97,139,86,96,93])).
% 102.16/102.55 cnf(9189,plain,
% 102.16/102.55 (~P1(f22(a1),f21(a2))),
% 102.16/102.55 inference(scs_inference,[],[856,8883,9133,8996,205,85,75,129,97,139,86,96,93,71])).
% 102.16/102.55 cnf(9195,plain,
% 102.16/102.55 (~P1(f15(a9,a1,a1),f3(x91951,f25(x91952,a1)))),
% 102.16/102.55 inference(scs_inference,[],[856,8883,9133,9067,8996,205,85,75,129,97,139,86,96,93,71,111,98,103])).
% 102.16/102.55 cnf(9197,plain,
% 102.16/102.55 (~E(a2,f22(a1))),
% 102.16/102.55 inference(scs_inference,[],[856,8883,9133,9067,8996,205,85,75,129,97,139,86,96,93,71,111,98,103,2])).
% 102.16/102.55 cnf(9204,plain,
% 102.16/102.55 (~P1(f22(a1),f24(a2,a2))),
% 102.16/102.55 inference(scs_inference,[],[856,8883,9133,9117,9067,9125,8996,205,85,75,129,97,139,86,96,93,71,111,98,103,2,89,104,88])).
% 102.16/102.55 cnf(9210,plain,
% 102.16/102.55 (~P8(f25(x92101,f23(a2)),f3(x92102,a8))),
% 102.16/102.55 inference(scs_inference,[],[856,8883,9133,8870,9117,9067,8974,9125,8996,2192,205,85,75,129,97,139,86,96,93,71,111,98,103,2,89,104,88,102,87,81])).
% 102.16/102.55 cnf(9248,plain,
% 102.16/102.55 (~P1(f22(a2),f21(a2))),
% 102.16/102.55 inference(scs_inference,[],[873,9204,8940,9210,8905,862,337,75,129,86,85,93,96,97,326,1332,111,71])).
% 102.16/102.55 cnf(9254,plain,
% 102.16/102.55 (~E(a2,f22(a2))),
% 102.16/102.55 inference(scs_inference,[],[873,9204,8940,9210,8905,862,337,75,129,86,85,93,96,97,326,1332,111,71,98,103,2])).
% 102.16/102.55 cnf(9255,plain,
% 102.16/102.55 (~P1(x92551,f23(f22(x92552)))),
% 102.16/102.55 inference(scs_inference,[],[873,9204,8940,9175,9210,8905,862,172,337,75,129,86,85,93,96,97,326,1332,111,71,98,103,2,89])).
% 102.16/102.55 cnf(9261,plain,
% 102.16/102.55 (~P1(f22(a2),f24(a2,a2))),
% 102.16/102.55 inference(scs_inference,[],[64,873,9204,8940,9175,9210,8905,8866,862,172,337,75,129,86,85,93,96,97,326,1332,111,71,98,103,2,89,94,104,88])).
% 102.16/102.55 cnf(9266,plain,
% 102.16/102.55 (~P1(x92661,f23(f22(a2)))),
% 102.16/102.55 inference(rename_variables,[],[8895])).
% 102.16/102.55 cnf(9268,plain,
% 102.16/102.55 (P1(a1,f26(a1))),
% 102.16/102.55 inference(scs_inference,[],[64,873,9204,8940,9175,9210,8895,8905,8866,862,172,65,337,75,129,86,85,93,96,97,326,1332,111,71,98,103,2,89,94,104,88,102,107,87])).
% 102.16/102.55 cnf(9273,plain,
% 102.16/102.55 (P1(f12(a1,a1),a1)),
% 102.16/102.55 inference(scs_inference,[],[64,873,9204,8940,9175,9210,8895,9266,8905,8866,862,172,65,337,75,129,86,85,93,96,97,326,1332,111,71,98,103,2,89,94,104,88,102,107,87,81,91])).
% 102.16/102.55 cnf(9277,plain,
% 102.16/102.55 (P1(a1,f12(a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[64,873,9204,8940,9175,9210,8895,9266,8905,8866,862,172,65,337,75,129,86,85,93,96,97,326,1332,111,71,98,103,2,89,94,104,88,102,107,87,81,91,139,90])).
% 102.16/102.55 cnf(9279,plain,
% 102.16/102.55 (P3(a9,a1,f12(a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[64,873,9204,8940,9175,9210,8895,9266,8905,8866,862,172,65,337,75,129,86,85,93,96,97,326,1332,111,71,98,103,2,89,94,104,88,102,107,87,81,91,139,90,1025])).
% 102.16/102.55 cnf(9309,plain,
% 102.16/102.55 (~E(f26(a2),f12(a1,a8))),
% 102.16/102.55 inference(scs_inference,[],[3369,9261,9277,9268,1205,75,129,93,86,97,96,85,111,98,71,103,2])).
% 102.16/102.55 cnf(9310,plain,
% 102.16/102.55 (P8(f12(a1,a1),a1)),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9277,9268,9273,1205,75,129,93,86,97,96,85,111,98,71,103,2,80])).
% 102.16/102.55 cnf(9311,plain,
% 102.16/102.55 (~P1(x93111,x93112)+P8(x93111,x93112)+~P1(x93112,a8)),
% 102.16/102.55 inference(rename_variables,[],[80])).
% 102.16/102.55 cnf(9312,plain,
% 102.16/102.55 (P5(f12(a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9277,9268,9273,147,1205,75,129,93,86,97,96,85,111,98,71,103,2,80,70])).
% 102.16/102.55 cnf(9323,plain,
% 102.16/102.55 (P1(f12(a1,a1),f26(a8))),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9277,9268,9273,147,8878,1205,75,129,93,86,97,96,85,111,98,71,103,2,80,70,94,104,88,102,87])).
% 102.16/102.55 cnf(9331,plain,
% 102.16/102.55 (P4(f15(a9,a1,f12(a1,a1)),a9,f12(a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9248,9277,9279,9268,9273,9050,8885,8940,147,8878,1205,75,129,93,86,97,96,85,111,98,71,103,2,80,70,94,104,88,102,87,47,81,137,136])).
% 102.16/102.55 cnf(9333,plain,
% 102.16/102.55 (P1(f15(a9,a1,f12(a1,a1)),f12(a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9248,9277,9279,9268,9273,9050,8885,8940,147,8878,1205,75,129,93,86,97,96,85,111,98,71,103,2,80,70,94,104,88,102,87,47,81,137,136,112])).
% 102.16/102.55 cnf(9338,plain,
% 102.16/102.55 (P1(f12(f12(a1,a1),a8),a8)),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9248,9277,9279,9268,9273,9050,8885,8940,147,8878,1205,75,129,93,86,97,96,85,111,98,71,103,2,80,70,94,104,88,102,87,47,81,137,136,112,139,337,91])).
% 102.16/102.55 cnf(9340,plain,
% 102.16/102.55 (P1(f12(a1,a1),f12(f12(a1,a1),a8))),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9248,9277,9279,9268,9273,9050,8885,8940,147,8878,1205,75,129,93,86,97,96,85,111,98,71,103,2,80,70,94,104,88,102,87,47,81,137,136,112,139,337,91,90])).
% 102.16/102.55 cnf(9348,plain,
% 102.16/102.55 (P6(a9,f12(f12(a1,a1),a8))),
% 102.16/102.55 inference(scs_inference,[],[64,3369,9261,9248,9277,9279,9268,9273,9050,8885,8940,147,8878,1205,75,129,93,86,97,96,85,111,98,71,103,2,80,70,94,104,88,102,87,47,81,137,136,112,139,337,91,90,326,1025,1332,9311,69])).
% 102.16/102.55 cnf(9356,plain,
% 102.16/102.55 (P3(a9,f12(a1,a1),f26(a8))),
% 102.16/102.55 inference(scs_inference,[],[9323,9348,9189,74,129,93])).
% 102.16/102.55 cnf(9360,plain,
% 102.16/102.55 (P1(f12(a1,a1),f22(a1))),
% 102.16/102.55 inference(scs_inference,[],[9323,9310,9348,9189,74,129,93,96,75])).
% 102.16/102.55 cnf(9372,plain,
% 102.16/102.55 (~P1(f12(a1,a1),f3(x93721,f26(a8)))),
% 102.16/102.55 inference(scs_inference,[],[9137,9323,9310,9255,9348,9189,74,129,93,96,75,86,85,97,111,71,103])).
% 102.16/102.55 cnf(9376,plain,
% 102.16/102.55 (~E(f3(a2,x93761),f21(x93762))),
% 102.16/102.55 inference(scs_inference,[],[9137,1346,9323,9310,9255,9348,9189,74,129,93,96,75,86,85,97,111,71,103,98,2])).
% 102.16/102.55 cnf(9379,plain,
% 102.16/102.55 (P1(a1,f3(a8,a2))),
% 102.16/102.55 inference(scs_inference,[],[64,9137,9312,1346,9323,9310,9333,9255,9348,9189,66,74,129,93,96,75,86,85,97,111,71,103,98,2,70,94])).
% 102.16/102.55 cnf(9392,plain,
% 102.16/102.55 (~E(f25(x93921,a1),f15(a9,a1,a1))),
% 102.16/102.55 inference(scs_inference,[],[64,9137,9031,9312,1346,9323,9187,9310,9333,9255,9348,9189,9277,66,74,129,93,96,75,86,85,97,111,71,103,98,2,70,94,104,88,48,102,87,51])).
% 102.16/102.55 cnf(9416,plain,
% 102.16/102.55 (P3(a9,f12(a1,a1),f22(a1))),
% 102.16/102.55 inference(scs_inference,[],[9360,9248,129,93])).
% 102.16/102.55 cnf(9426,plain,
% 102.16/102.55 (P1(a2,f22(x94261))),
% 102.16/102.55 inference(scs_inference,[],[9360,9248,149,129,93,86,96,97,85,75])).
% 102.16/102.55 cnf(9441,plain,
% 102.16/102.55 (P1(f12(a1,a1),f16(f22(a1),f22(a1)))),
% 102.16/102.55 inference(scs_inference,[],[9197,1384,9360,8934,9248,149,129,93,86,96,97,85,75,111,71,103,98,2,104,88,102])).
% 102.16/102.55 cnf(9459,plain,
% 102.16/102.55 (P1(f12(f12(a1,a1),f3(a8,a2)),f3(a8,a2))),
% 102.16/102.55 inference(scs_inference,[],[9197,1384,9360,9356,9379,8934,9372,9248,9273,149,129,93,86,96,97,85,75,111,71,103,98,2,104,88,102,87,81,137,318,2093,2221,1327,896,2079,2799,91])).
% 102.16/102.55 cnf(9463,plain,
% 102.16/102.55 (~E(f3(a2,x94631),f22(a1))),
% 102.16/102.55 inference(scs_inference,[],[9197,1384,9360,9356,9379,8934,9372,9248,9273,149,129,93,86,96,97,85,75,111,71,103,98,2,104,88,102,87,81,137,318,2093,2221,1327,896,2079,2799,91,90,1332])).
% 102.16/102.55 cnf(9476,plain,
% 102.16/102.55 (P3(a9,a2,f22(x94761))),
% 102.16/102.55 inference(scs_inference,[],[9463,9426,2221,2093,2799,93])).
% 102.16/102.55 cnf(9482,plain,
% 102.16/102.55 (~P1(a1,f20(x94821,x94822,f24(a2,a2)))),
% 102.16/102.55 inference(scs_inference,[],[9463,9426,8897,2221,2093,2799,93,86,85,129])).
% 102.16/102.55 cnf(9486,plain,
% 102.16/102.55 (P1(f26(a2),f22(x94861))),
% 102.16/102.55 inference(scs_inference,[],[9463,9426,8897,175,2221,2093,2799,93,86,85,129,96,75])).
% 102.16/102.55 cnf(9488,plain,
% 102.16/102.55 (~P1(a1,f16(f24(a2,a2),x94881))),
% 102.16/102.55 inference(scs_inference,[],[9463,9426,8897,175,2221,2093,2799,93,86,85,129,96,75,97])).
% 102.16/102.55 cnf(9494,plain,
% 102.16/102.55 (~P1(f26(a2),f21(a8))),
% 102.16/102.55 inference(scs_inference,[],[8980,9463,9426,9195,8897,175,2221,2093,2799,93,86,85,129,96,75,97,111,103,71])).
% 102.16/102.55 cnf(9498,plain,
% 102.16/102.55 (~E(f15(a9,a1,a1),f25(x94981,a1))),
% 102.16/102.55 inference(scs_inference,[],[8980,9392,9463,9426,9195,8897,175,2221,2093,2799,93,86,85,129,96,75,97,111,103,71,98,2])).
% 102.16/102.55 cnf(9503,plain,
% 102.16/102.55 (~P1(f26(a2),f24(a8,a8))),
% 102.16/102.55 inference(scs_inference,[],[8980,9392,9463,9426,9340,9195,9338,8897,175,2221,2093,2799,93,86,85,129,96,75,97,111,103,71,98,2,80,104,88])).
% 102.16/102.55 cnf(9522,plain,
% 102.16/102.55 (P1(f3(a2,x95221),f22(x95222))),
% 102.16/102.55 inference(scs_inference,[],[9486,9503,1187,93,85,129,75])).
% 102.16/102.55 cnf(9538,plain,
% 102.16/102.55 (~E(f26(a2),f21(x95381))),
% 102.16/102.55 inference(scs_inference,[],[9254,249,9486,9503,1187,93,85,129,75,86,96,97,111,98,103,71,2])).
% 102.16/102.55 cnf(9556,plain,
% 102.16/102.55 (~P1(f22(x95561),f22(f24(a8,a8)))),
% 102.16/102.55 inference(scs_inference,[],[9254,9376,249,9486,9503,8978,1187,2065,93,85,129,75,86,96,97,111,98,103,71,2,94,104,88,102,81,137,127,78])).
% 102.16/102.55 cnf(9560,plain,
% 102.16/102.55 (~P1(f10(f22(x95601),f24(a8,a8)),f24(a8,a8))),
% 102.16/102.55 inference(scs_inference,[],[9254,9376,249,9486,9503,8978,1187,2065,93,85,129,75,86,96,97,111,98,103,71,2,94,104,88,102,81,137,127,78,318,896,99])).
% 102.16/102.55 cnf(9566,plain,
% 102.16/102.55 (P1(f10(f22(x95661),f24(a8,a8)),f22(x95661))),
% 102.16/102.55 inference(scs_inference,[],[9254,9376,249,9486,9503,8978,1187,2065,93,85,129,75,86,96,97,111,98,103,71,2,94,104,88,102,81,137,127,78,318,896,99,1327,2079,139,79])).
% 102.16/102.55 cnf(9568,plain,
% 102.16/102.55 (~E(f26(a2),f22(x95681))),
% 102.16/102.55 inference(scs_inference,[],[9254,9376,249,9486,9503,8978,1187,2065,93,85,129,75,86,96,97,111,98,103,71,2,94,104,88,102,81,137,127,78,318,896,99,1327,2079,139,79,337])).
% 102.16/102.55 cnf(9569,plain,
% 102.16/102.55 (~E(a2,f22(x95691))),
% 102.16/102.55 inference(scs_inference,[],[9254,9376,249,9486,9503,8978,1187,2065,93,85,129,75,86,96,97,111,98,103,71,2,94,104,88,102,81,137,127,78,318,896,99,1327,2079,139,79,337,326])).
% 102.16/102.55 cnf(9570,plain,
% 102.16/102.55 (~E(f3(a2,x95701),f22(x95702))),
% 102.16/102.55 inference(scs_inference,[],[9254,9376,249,9486,9503,8978,1187,2065,93,85,129,75,86,96,97,111,98,103,71,2,94,104,88,102,81,137,127,78,318,896,99,1327,2079,139,79,337,326,1332])).
% 102.16/102.55 cnf(9596,plain,
% 102.16/102.55 (P3(a9,f3(a2,x95961),f22(x95962))),
% 102.16/102.55 inference(scs_inference,[],[9522,9570,9560,367,2221,2093,2799,93])).
% 102.16/102.55 cnf(9608,plain,
% 102.16/102.55 (~P3(a9,f10(f22(x96081),f24(a8,a8)),f24(a8,a8))),
% 102.16/102.55 inference(scs_inference,[],[9522,9570,9560,9494,367,2221,2093,2799,93,129,85,96,86,97,111])).
% 102.16/102.55 cnf(9616,plain,
% 102.16/102.55 (~E(f22(x96161),f3(a2,x96162))),
% 102.16/102.55 inference(scs_inference,[],[9309,9522,9570,9560,9494,367,2221,2093,2799,93,129,85,96,86,97,111,98,71,103,2])).
% 102.16/102.55 cnf(9620,plain,
% 102.16/102.55 (~P1(f26(a2),f25(f21(a8),f21(a8)))),
% 102.16/102.55 inference(scs_inference,[],[64,9309,9522,9570,9560,9494,152,367,2221,2093,2799,93,129,85,96,86,97,111,98,71,103,2,94,104])).
% 102.16/102.55 cnf(9626,plain,
% 102.16/102.55 (P1(f3(a2,x96261),f16(f22(x96262),f22(x96262)))),
% 102.16/102.55 inference(scs_inference,[],[64,9309,9522,9570,9560,9008,9494,9273,152,367,2221,2093,2799,93,129,85,96,86,97,111,98,71,103,2,94,104,88,87,102])).
% 102.16/102.55 cnf(9632,plain,
% 102.16/102.55 (P1(f12(f12(a1,a1),f20(a8,a9,a8)),f20(a8,a9,a8))),
% 102.16/102.55 inference(scs_inference,[],[64,9309,9522,9570,9560,9074,9008,9494,9273,152,367,2221,2093,2799,93,129,85,96,86,97,111,98,71,103,2,94,104,88,87,102,81,137,91])).
% 102.16/102.55 cnf(9661,plain,
% 102.16/102.55 (~E(f3(a2,x96611),f25(x96612,a8))),
% 102.16/102.55 inference(scs_inference,[],[8916,1375,9459,9556,9379,6350,8866,129,93,85,96,86,97,111,98,103,71,2])).
% 102.16/102.55 cnf(9664,plain,
% 102.16/102.55 (~P1(a2,f25(f24(a8,a8),f24(a8,a8)))),
% 102.16/102.55 inference(scs_inference,[],[8916,1375,9459,9556,9331,2060,9379,6350,8866,129,93,85,96,86,97,111,98,103,71,2,54,104])).
% 102.16/102.55 cnf(9677,plain,
% 102.28/102.55 (P1(x96771,f23(f26(a2)))),
% 102.28/102.55 inference(rename_variables,[],[8965])).
% 102.28/102.55 cnf(9687,plain,
% 102.28/102.55 (~P7(a9,f23(f26(a2)))),
% 102.28/102.55 inference(scs_inference,[],[64,8916,1375,893,9416,9459,9556,8965,9677,9482,8887,9331,2060,9379,6350,8940,8978,8866,9273,129,93,85,96,86,97,111,98,103,71,2,54,104,88,47,102,81,137,127,2221,2093,2799,70,138])).
% 102.28/102.55 cnf(9717,plain,
% 102.28/102.55 (~P1(a1,f3(x97171,f20(a8,a9,a8)))),
% 102.28/102.55 inference(scs_inference,[],[9632,9037,9687,9008,2847,381,246,320,1348,129,85,96,93,86,97,111,103])).
% 102.28/102.55 cnf(9723,plain,
% 102.28/102.55 (~E(f22(x97231),f26(a2))),
% 102.28/102.55 inference(scs_inference,[],[9498,9568,9632,9037,9687,9008,2847,381,246,320,1348,129,85,96,93,86,97,111,103,98,71,2])).
% 102.28/102.55 cnf(9729,plain,
% 102.28/102.55 (~E(f23(a2),f24(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[64,9498,9568,9632,9608,9037,9488,9687,9008,2847,381,8978,246,320,1348,129,85,96,93,86,97,111,103,98,71,2,104,48,88,51])).
% 102.28/102.55 cnf(9737,plain,
% 102.28/102.55 (~P1(f12(a1,a1),f20(a1,a9,x97371))),
% 102.28/102.55 inference(scs_inference,[],[64,9498,9568,9632,9608,9037,9488,9687,9279,9008,8914,2847,381,8978,9273,65,246,320,1348,129,85,96,93,86,97,111,103,98,71,2,104,48,88,51,102,81,138,139])).
% 102.28/102.55 cnf(9745,plain,
% 102.28/102.55 (~P1(f12(a1,a1),f20(x97451,x97452,f20(a1,a9,x97453)))),
% 102.28/102.55 inference(scs_inference,[],[9737,129])).
% 102.28/102.55 cnf(9774,plain,
% 102.28/102.55 (~P8(f16(f22(a1),f22(a1)),f20(a1,a9,x97741))),
% 102.28/102.55 inference(scs_inference,[],[9616,9737,2236,9566,9441,8870,9323,129,96,85,93,97,86,111,103,98,71,2,94,104,88,102,81])).
% 102.28/102.55 cnf(9798,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),a8),f25(x97981,a8))),
% 102.28/102.55 inference(scs_inference,[],[9044,9338,381,8866,129,96,93,85])).
% 102.28/102.55 cnf(9800,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),a8),f25(a8,x98001))),
% 102.28/102.55 inference(scs_inference,[],[9044,9338,381,8866,129,96,93,85,86])).
% 102.28/102.55 cnf(9806,plain,
% 102.28/102.55 (~P1(f12(f12(a1,a1),a8),f3(x98061,a8))),
% 102.28/102.55 inference(scs_inference,[],[9044,9745,9338,381,8866,129,96,93,85,86,97,111,103])).
% 102.28/102.55 cnf(9812,plain,
% 102.28/102.55 (~E(f26(a2),f25(x98121,a8))),
% 102.28/102.55 inference(scs_inference,[],[9538,3353,9044,9745,9338,381,8866,129,96,93,85,86,97,111,103,71,98,2])).
% 102.28/102.55 cnf(9820,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),a8),f16(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[64,9538,3353,9044,9745,9338,381,8866,1166,129,96,93,85,86,97,111,103,71,98,2,94,104,88,102])).
% 102.28/102.55 cnf(9828,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),f26(a1)),f26(a1))),
% 102.28/102.55 inference(scs_inference,[],[64,9538,3353,9044,9745,9717,9338,9268,9687,381,8866,9273,1166,129,96,93,85,86,97,111,103,71,98,2,94,104,88,102,81,507,87,91])).
% 102.28/102.55 cnf(9836,plain,
% 102.28/102.55 (~P1(x98361,f20(x98362,x98363,a2))),
% 102.28/102.55 inference(scs_inference,[],[66,129])).
% 102.28/102.55 cnf(9838,plain,
% 102.28/102.55 (~P1(x98381,f16(x98382,a2))),
% 102.28/102.55 inference(scs_inference,[],[66,129,96])).
% 102.28/102.55 cnf(9856,plain,
% 102.28/102.55 (~E(f24(a8,a8),f23(a2))),
% 102.28/102.55 inference(scs_inference,[],[9723,9729,9820,9806,9076,8866,66,129,96,85,93,97,86,103,111,98,71,2])).
% 102.28/102.55 cnf(9874,plain,
% 102.28/102.55 (~P1(f10(f16(a8,a8),f3(x98741,a8)),f3(x98741,a8))),
% 102.28/102.55 inference(scs_inference,[],[9723,9729,9820,9806,9340,9076,2056,8866,66,129,96,85,93,97,86,103,111,98,71,2,107,104,88,87,102,81,78,318,896,99])).
% 102.28/102.55 cnf(9878,plain,
% 102.28/102.55 (P1(f10(f16(a8,a8),f3(x98781,a8)),f16(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[9723,9729,9820,9806,9340,9076,2056,8866,66,129,96,85,93,97,86,103,111,98,71,2,107,104,88,87,102,81,78,318,896,99,1327,2079,79])).
% 102.28/102.55 cnf(9880,plain,
% 102.28/102.55 (~E(f26(a2),f16(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[9723,9729,9820,9806,9340,9076,2056,8866,66,129,96,85,93,97,86,103,111,98,71,2,107,104,88,87,102,81,78,318,896,99,1327,2079,79,337])).
% 102.28/102.55 cnf(9881,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),f16(a8,a8)),f16(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[9723,9729,9820,9806,9340,9076,2056,8866,66,129,96,85,93,97,86,103,111,98,71,2,107,104,88,87,102,81,78,318,896,99,1327,2079,79,337,91])).
% 102.28/102.55 cnf(9887,plain,
% 102.28/102.55 (~E(a2,f16(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[9723,9729,9820,9806,9340,9076,2056,8866,66,129,96,85,93,97,86,103,111,98,71,2,107,104,88,87,102,81,78,318,896,99,1327,2079,79,337,91,1025,90,326])).
% 102.28/102.55 cnf(9888,plain,
% 102.28/102.55 (~E(f3(a2,x98881),f16(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[9723,9729,9820,9806,9340,9076,2056,8866,66,129,96,85,93,97,86,103,111,98,71,2,107,104,88,87,102,81,78,318,896,99,1327,2079,79,337,91,1025,90,326,1332])).
% 102.28/102.55 cnf(9901,plain,
% 102.28/102.55 (~P1(x99011,f20(x99012,x99013,a2))),
% 102.28/102.55 inference(rename_variables,[],[9836])).
% 102.28/102.55 cnf(9909,plain,
% 102.28/102.55 (~P1(x99091,f20(x99092,x99093,f20(x99094,x99095,a2)))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,83,2221,2093,2799,129])).
% 102.28/102.55 cnf(9911,plain,
% 102.28/102.55 (~P1(x99111,f16(x99112,f20(x99113,x99114,a2)))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,83,2221,2093,2799,129,96])).
% 102.28/102.55 cnf(9915,plain,
% 102.28/102.55 (P1(f12(f15(a9,a1,a1),a8),f25(x99151,a8))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,9881,8936,83,2221,2093,2799,129,96,93,85])).
% 102.28/102.55 cnf(9919,plain,
% 102.28/102.55 (~P1(x99191,f16(f20(x99192,x99193,a2),x99194))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,9881,8936,83,2221,2093,2799,129,96,93,85,86,97])).
% 102.28/102.55 cnf(9921,plain,
% 102.28/102.55 (~P3(a9,x99211,f20(x99212,x99213,a2))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,9881,8936,83,2221,2093,2799,129,96,93,85,86,97,111])).
% 102.28/102.55 cnf(9923,plain,
% 102.28/102.55 (~P1(f12(f15(a9,a1,a1),a8),f3(x99231,a8))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,9881,8936,83,2221,2093,2799,129,96,93,85,86,97,111,103])).
% 102.28/102.55 cnf(9927,plain,
% 102.28/102.55 (~P1(x99271,f3(f20(x99272,x99273,a2),x99274))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,9881,8936,83,2221,2093,2799,129,96,93,85,86,97,111,103,71,98])).
% 102.28/102.55 cnf(9929,plain,
% 102.28/102.55 (~E(f16(a8,a8),f3(a2,x99291))),
% 102.28/102.55 inference(scs_inference,[],[9836,9901,9888,9881,8936,83,2221,2093,2799,129,96,93,85,86,97,111,103,71,98,2])).
% 102.28/102.55 cnf(9934,plain,
% 102.28/102.55 (~P1(x99341,f16(x99342,a2))),
% 102.28/102.55 inference(rename_variables,[],[9838])).
% 102.28/102.55 cnf(9940,plain,
% 102.28/102.55 (P1(f12(f15(a9,a1,a1),a8),f16(a8,a8))),
% 102.28/102.55 inference(scs_inference,[],[64,9836,9901,9838,9888,9881,9798,9340,8936,2056,83,2221,2093,2799,129,96,93,85,86,97,111,103,71,98,2,105,94,88,87,102])).
% 102.28/102.55 cnf(9952,plain,
% 102.28/102.55 (P1(f10(a8,f16(x99521,a2)),a8)),
% 102.28/102.55 inference(scs_inference,[],[64,9836,9901,9838,9934,9888,9881,9798,9626,9340,8936,2056,2065,83,2221,2093,2799,129,96,93,85,86,97,111,103,71,98,2,105,94,88,87,102,81,127,78,79])).
% 102.28/102.55 cnf(9954,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),f25(x99541,a8)),f25(x99541,a8))),
% 102.28/102.55 inference(scs_inference,[],[64,9836,9901,9838,9934,9888,9881,9798,9626,9340,8936,2056,2065,83,2221,2093,2799,129,96,93,85,86,97,111,103,71,98,2,105,94,88,87,102,81,127,78,79,91])).
% 102.28/102.55 cnf(9964,plain,
% 102.28/102.55 (P6(a9,f10(a8,f16(x99641,a2)))),
% 102.28/102.55 inference(scs_inference,[],[64,9836,9901,9838,9934,9888,9476,9881,9798,9626,9340,8936,9268,2056,9426,2065,83,2221,2093,2799,129,96,93,85,86,97,111,103,71,98,2,105,94,88,87,102,81,127,78,79,91,1025,90,143,137,69])).
% 102.28/102.55 cnf(9968,plain,
% 102.28/102.55 (P1(x99681,f23(f16(x99682,a2)))),
% 102.28/102.55 inference(scs_inference,[],[9838,83])).
% 102.28/102.55 cnf(9969,plain,
% 102.28/102.55 (~P1(x99691,f16(x99692,a2))),
% 102.28/102.55 inference(rename_variables,[],[9838])).
% 102.28/102.55 cnf(9973,plain,
% 102.28/102.55 (~P1(x99731,f20(f20(x99732,x99733,a2),a9,x99734))),
% 102.28/102.55 inference(scs_inference,[],[9921,9964,9838,83,74,139])).
% 102.28/102.55 cnf(9977,plain,
% 102.28/102.55 (~P1(x99771,f16(x99772,f16(x99773,a2)))),
% 102.28/102.55 inference(scs_inference,[],[9921,9964,9838,9969,83,74,139,129,96])).
% 102.28/102.55 cnf(9983,plain,
% 102.28/102.55 (~P1(x99831,f16(f16(x99832,a2),x99833))),
% 102.28/102.55 inference(scs_inference,[],[9921,9940,9952,9964,9838,9969,83,74,139,129,96,85,93,97])).
% 102.28/102.55 cnf(9987,plain,
% 102.28/102.55 (~P3(a9,f10(f16(a8,a8),f3(x99871,a8)),f3(x99871,a8))),
% 102.28/102.55 inference(scs_inference,[],[9921,9940,9874,9952,9964,9838,9969,83,74,139,129,96,85,93,97,86,111])).
% 102.28/102.55 cnf(9989,plain,
% 102.28/102.55 (~P1(f10(a8,f16(x99891,a2)),f3(x99892,a8))),
% 102.28/102.55 inference(scs_inference,[],[9921,9940,9874,9952,9964,9838,9969,83,74,139,129,96,85,93,97,86,111,103])).
% 102.28/102.55 cnf(9991,plain,
% 102.28/102.55 (~P1(x99911,f3(f16(x99912,a2),x99913))),
% 102.28/102.55 inference(scs_inference,[],[9921,9940,9874,9952,9964,9838,9969,83,74,139,129,96,85,93,97,86,111,103,98])).
% 102.28/102.55 cnf(9995,plain,
% 102.28/102.55 (~E(f16(a8,a8),f26(a2))),
% 102.28/102.55 inference(scs_inference,[],[9880,9921,9940,9874,9952,9964,9838,9969,83,74,139,129,96,85,93,97,86,111,103,98,71,2])).
% 102.28/102.55 cnf(10003,plain,
% 102.28/102.55 (~P1(x100031,f20(x100032,x100033,f20(x100034,x100035,a2)))),
% 102.28/102.55 inference(rename_variables,[],[9909])).
% 102.28/102.55 cnf(10015,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),f25(a8,x100151)),f25(a8,x100151))),
% 102.28/102.55 inference(scs_inference,[],[64,9880,9921,9940,9874,9800,9909,10003,9919,9952,9964,9838,9969,8950,2060,8940,9340,9189,83,74,139,129,96,85,93,97,86,111,103,98,71,2,54,108,110,88,47,87,102,81,91])).
% 102.28/102.55 cnf(10040,plain,
% 102.28/102.55 (~P1(x100401,f16(a2,x100402))),
% 102.28/102.55 inference(scs_inference,[],[9268,66,152,129,85,96,97])).
% 102.28/102.55 cnf(10054,plain,
% 102.28/102.55 (~E(f16(a8,a8),a2)),
% 102.28/102.55 inference(scs_inference,[],[9995,9887,9828,9923,9268,66,152,129,85,96,97,93,86,111,103,71,98,2])).
% 102.28/102.55 cnf(10060,plain,
% 102.28/102.55 (P3(a9,x100601,f23(a2))),
% 102.28/102.55 inference(rename_variables,[],[8978])).
% 102.28/102.55 cnf(10061,plain,
% 102.28/102.55 (~E(f25(x100611,a8),f3(x100612,a8))),
% 102.28/102.55 inference(scs_inference,[],[9995,9887,9828,9915,9923,9987,9973,9836,9268,8978,66,152,129,85,96,97,93,86,111,103,71,98,2,109,51,48])).
% 102.28/102.55 cnf(10077,plain,
% 102.28/102.55 (P1(x100771,f23(f16(a2,x100772)))),
% 102.28/102.55 inference(scs_inference,[],[64,9995,9887,9828,9915,9923,9987,9911,9968,9973,9836,8919,9268,8978,10060,66,152,129,85,96,97,93,86,111,103,71,98,2,109,51,48,88,87,102,81,138,246,83])).
% 102.28/102.55 cnf(10081,plain,
% 102.28/102.55 (P1(f12(f15(a9,a1,a1),f25(x100811,a8)),f25(x100811,a8))),
% 102.28/102.55 inference(scs_inference,[],[64,9995,9887,9828,9915,9923,9987,9911,9968,9973,9836,8919,9268,8978,10060,66,152,129,85,96,97,93,86,111,103,71,98,2,109,51,48,88,87,102,81,138,246,83,1348,320,91])).
% 102.28/102.55 cnf(10093,plain,
% 102.28/102.55 (~P1(f11(x100931,f16(a2,x100932)),f25(a2,a2))),
% 102.28/102.55 inference(scs_inference,[],[64,9995,9887,9828,9915,9923,9987,9911,9983,9968,9973,9836,9838,8919,9268,8978,10060,66,152,129,85,96,97,93,86,111,103,71,98,2,109,51,48,88,87,102,81,138,246,83,1348,320,91,90,1025,89,106,104])).
% 102.28/102.55 cnf(10107,plain,
% 102.28/102.55 (~P1(x101071,f16(f16(a2,x101072),x101073))),
% 102.28/102.55 inference(scs_inference,[],[10040,2234,129,85,97])).
% 102.28/102.55 cnf(10109,plain,
% 102.28/102.55 (~P1(x101091,f16(x101092,f16(a2,x101093)))),
% 102.28/102.55 inference(scs_inference,[],[10040,2234,129,85,97,96])).
% 102.28/102.55 cnf(10117,plain,
% 102.28/102.55 (~P3(a9,x101171,f16(a2,x101172))),
% 102.28/102.55 inference(scs_inference,[],[10040,9878,2234,129,85,97,96,93,86,103,111])).
% 102.28/102.55 cnf(10125,plain,
% 102.28/102.55 (~P1(x101251,f16(a2,x101252))),
% 102.28/102.55 inference(rename_variables,[],[10040])).
% 102.28/102.55 cnf(10140,plain,
% 102.28/102.55 (P1(f10(a8,f16(a2,x101401)),a8)),
% 102.28/102.55 inference(scs_inference,[],[64,9929,10040,10125,10061,9878,2234,129,85,97,96,93,86,103,111,98,71,2,94,104,88,102,81,78,139,79])).
% 102.28/102.55 cnf(10144,plain,
% 102.28/102.55 (P6(a9,f10(a8,f16(a2,x101441)))),
% 102.28/102.55 inference(scs_inference,[],[64,9929,10040,10125,10061,9878,9774,2234,129,85,97,96,93,86,103,111,98,71,2,94,104,88,102,81,78,139,79,80,69])).
% 102.28/102.55 cnf(10150,plain,
% 102.28/102.55 (~P1(x101501,f20(f16(a2,x101502),a9,x101503))),
% 102.28/102.55 inference(scs_inference,[],[10117,10144,74,139])).
% 102.28/102.55 cnf(10154,plain,
% 102.28/102.55 (~P1(x101541,f16(f26(a2),x101542))),
% 102.28/102.55 inference(scs_inference,[],[10117,10144,152,1166,74,139,129,97])).
% 102.28/102.55 cnf(10158,plain,
% 102.28/102.55 (~P1(x101581,f16(x101582,f3(a2,x101583)))),
% 102.28/102.55 inference(scs_inference,[],[10117,10140,10144,152,1166,74,139,129,97,85,96])).
% 102.28/102.55 cnf(10164,plain,
% 102.28/102.55 (~P1(f10(a8,f16(a2,x101641)),f3(x101642,a8))),
% 102.28/102.55 inference(scs_inference,[],[10117,9954,10140,10144,152,1166,74,139,129,97,85,96,86,93,103])).
% 102.28/102.55 cnf(10198,plain,
% 102.28/102.55 (~P1(a1,f3(x101981,f22(a1)))),
% 102.28/102.55 inference(scs_inference,[],[10015,951,421,85,86,93,103])).
% 102.28/102.55 cnf(10213,plain,
% 102.28/102.55 (~P8(f23(f16(a2,x102131)),f25(a2,a2))),
% 102.28/102.55 inference(scs_inference,[],[9812,851,10015,9989,10093,10077,10150,9836,951,421,85,86,93,103,111,71,2,107,88,102,81])).
% 102.28/102.55 cnf(10223,plain,
% 102.28/102.55 (P1(f12(a1,a1),f25(x102231,a1))),
% 102.28/102.55 inference(scs_inference,[],[10213,9273,337,326,1332,85])).
% 102.28/102.55 cnf(10227,plain,
% 102.28/102.55 (P1(f12(a1,a1),f25(a1,x102271))),
% 102.28/102.55 inference(scs_inference,[],[10081,10213,9273,337,326,1332,85,93,86])).
% 102.28/102.55 cnf(10229,plain,
% 102.28/102.55 (~P1(f12(a1,a1),f3(x102291,a1))),
% 102.28/102.55 inference(scs_inference,[],[10081,10213,9273,337,326,1332,85,93,86,103])).
% 102.28/102.55 cnf(10249,plain,
% 102.28/102.55 (P1(f12(a1,a1),f16(a1,a1))),
% 102.28/102.55 inference(scs_inference,[],[9856,9596,9569,10081,10164,10213,10107,9838,9522,9273,337,326,1332,85,93,86,103,111,98,71,2,105,104,88,137,102])).
% 102.28/102.55 cnf(10269,plain,
% 102.28/102.55 (P3(a9,f12(a1,a1),f25(x102691,a1))),
% 102.28/102.55 inference(scs_inference,[],[10223,86,93])).
% 102.28/102.55 cnf(10275,plain,
% 102.28/102.55 (~P3(a9,f12(a1,a1),f3(x102751,a1))),
% 102.28/102.55 inference(scs_inference,[],[10223,10229,86,93,85,103,111])).
% 102.28/102.55 cnf(10277,plain,
% 102.28/102.55 (~P1(f16(a8,a8),f21(a2))),
% 102.28/102.55 inference(scs_inference,[],[10223,10229,10054,86,93,85,103,111,71])).
% 102.28/102.55 cnf(10280,plain,
% 102.28/102.55 (~E(f12(a1,a1),f26(a2))),
% 102.28/102.55 inference(scs_inference,[],[10223,10229,10054,954,178,9331,86,93,85,103,111,71,2,54])).
% 102.28/102.55 cnf(10298,plain,
% 102.28/102.55 (~P1(f16(a8,a8),f24(a2,a2))),
% 102.28/102.55 inference(scs_inference,[],[10223,10229,10054,954,10154,9977,178,9331,8940,9836,9838,10040,2847,9277,86,93,85,103,111,71,2,54,110,108,94,47,104,87,88])).
% 102.28/102.55 cnf(10307,plain,
% 102.28/102.55 (~P1(f10(f25(x103071,a1),f3(x103072,a1)),f3(x103072,a1))),
% 102.28/102.55 inference(scs_inference,[],[10223,10229,10054,954,10154,9977,178,9416,9331,8940,9836,9838,10040,2847,9277,86,93,85,103,111,71,2,54,110,108,94,47,104,87,88,137,102,81,318,99])).
% 102.28/102.55 cnf(10314,plain,
% 102.28/102.55 (P1(f10(f25(x103141,a1),f3(x103142,a1)),f25(x103141,a1))),
% 102.28/102.55 inference(scs_inference,[],[10223,10229,10054,954,10154,9977,178,9416,9331,8940,9836,9838,10040,2847,9277,86,93,85,103,111,71,2,54,110,108,94,47,104,87,88,137,102,81,318,99,896,1327,78,2079,79])).
% 102.28/102.55 cnf(10353,plain,
% 102.28/102.55 (P3(a9,f12(a1,a1),f25(a1,x103531))),
% 102.28/102.55 inference(scs_inference,[],[10298,10227,129,96,97,86,93])).
% 102.28/102.55 cnf(10365,plain,
% 102.28/102.55 (~E(f26(a2),f12(a1,a1))),
% 102.28/102.55 inference(scs_inference,[],[10298,10227,10280,129,96,97,86,93,85,103,111,98,71,2])).
% 102.28/102.55 cnf(10375,plain,
% 102.28/102.55 (~E(f25(x103751,a1),f3(x103752,a1))),
% 102.28/102.55 inference(scs_inference,[],[10298,10227,10280,10269,10275,10109,10229,10040,8878,129,96,97,86,93,85,103,111,98,71,2,89,106,94,51])).
% 102.28/102.55 cnf(10382,plain,
% 102.28/102.55 (~P1(f12(a1,a1),f24(f26(a2),f26(a2)))),
% 102.28/102.55 inference(scs_inference,[],[10298,10227,10280,10269,10275,10109,8970,10229,9379,10040,8878,2192,129,96,97,86,93,85,103,111,98,71,2,89,106,94,51,48,87,104,88])).
% 102.28/102.55 cnf(10393,plain,
% 102.28/102.55 (P1(f12(f15(a9,a1,a1),f3(a8,a2)),f3(a8,a2))),
% 102.28/102.55 inference(scs_inference,[],[64,10298,10227,10280,10269,10275,9927,10109,8970,10229,9379,10040,8878,2192,129,96,97,86,93,85,103,111,98,71,2,89,106,94,51,48,87,104,88,137,102,81,139,91])).
% 102.28/102.55 cnf(10416,plain,
% 102.28/102.55 (P3(a9,f12(a1,a1),f16(a1,a1))),
% 102.28/102.55 inference(scs_inference,[],[10249,86,93])).
% 102.28/102.55 cnf(10426,plain,
% 102.28/102.55 (~E(f3(x104261,a1),f25(x104262,a1))),
% 102.28/102.55 inference(scs_inference,[],[10365,10249,10375,10307,86,93,85,103,111,71,2])).
% 102.28/102.55 cnf(10433,plain,
% 102.28/102.55 (~P1(f16(a8,a8),f25(f21(a2),f21(a2)))),
% 102.28/102.55 inference(scs_inference,[],[10365,10249,10375,10307,10277,10158,9277,10040,86,93,85,103,111,71,2,109,87,104])).
% 102.28/102.55 cnf(10445,plain,
% 102.28/102.55 (~E(f26(f3(a2,x104451)),f16(a1,a1))),
% 102.28/102.55 inference(scs_inference,[],[10365,10249,10375,10353,10307,10382,10277,10158,9277,10040,86,93,85,103,111,71,2,109,87,104,88,137,102,81,318,896,1327])).
% 102.28/102.55 cnf(10447,plain,
% 102.28/102.55 (~E(f26(a2),f16(a1,a1))),
% 102.28/102.55 inference(scs_inference,[],[10365,10249,10375,10353,10307,10382,10277,10158,9277,10040,86,93,85,103,111,71,2,109,87,104,88,137,102,81,318,896,1327,2079,337])).
% 102.28/102.55 cnf(10454,plain,
% 102.28/102.55 (~E(a2,f16(a1,a1))),
% 102.28/102.55 inference(scs_inference,[],[10365,10249,10375,10353,10307,10382,10277,10158,9277,10040,86,93,85,103,111,71,2,109,87,104,88,137,102,81,318,896,1327,2079,337,90,91,1025,326])).
% 102.28/102.55 cnf(10455,plain,
% 102.28/102.55 (~E(f3(a2,x104551),f16(a1,a1))),
% 102.28/102.55 inference(scs_inference,[],[10365,10249,10375,10353,10307,10382,10277,10158,9277,10040,86,93,85,103,111,71,2,109,87,104,88,137,102,81,318,896,1327,2079,337,90,91,1025,326,1332])).
% 102.28/102.55 cnf(10487,plain,
% 102.28/102.55 (~P1(f15(a9,a1,a1),f3(x104871,a1))),
% 102.28/102.55 inference(scs_inference,[],[10455,10393,421,2192,2093,2799,2221,86,93,85,103])).
% 102.28/102.55 cnf(10515,plain,
% 102.28/102.55 (P1(f12(f15(a9,a1,a1),f20(a8,a9,a8)),f20(a8,a9,a8))),
% 102.28/102.55 inference(scs_inference,[],[64,10426,10455,10416,10393,10433,9991,9008,10227,421,2192,2093,2799,2221,86,93,85,103,111,98,71,2,87,88,104,137,102,81,1025,90,129,91])).
% 102.28/102.55 cnf(10527,plain,
% 102.28/102.55 (P1(f15(a9,a1,a1),f25(a1,x105271))),
% 102.28/102.55 inference(scs_inference,[],[10515,2192,93,86])).
% 102.28/102.55 cnf(10531,plain,
% 102.28/102.55 (~P1(x105311,f3(x105312,f21(x105311)))),
% 102.28/102.55 inference(scs_inference,[],[10515,2192,144,93,86,85,103])).
% 102.28/102.55 cnf(10537,plain,
% 102.28/102.55 (~E(f16(a1,a1),f26(a2))),
% 102.28/102.55 inference(scs_inference,[],[10447,10487,10515,2192,144,93,86,85,103,111,71,2])).
% 102.28/102.55 cnf(10593,plain,
% 102.28/102.55 (P1(f12(f12(a1,a1),f12(a1,a8)),f12(a1,a8))),
% 102.28/102.55 inference(scs_inference,[],[64,10537,10454,10527,10531,9187,10487,2234,9273,93,86,85,111,103,71,2,94,87,88,137,102,81,90,1025,91])).
% 102.28/102.55 cnf(10689,plain,
% 102.28/102.55 (~P1(x106891,f3(x106892,f24(x106891,x106893)))),
% 102.28/102.55 inference(scs_inference,[],[10593,9620,145,146,93,86,111,103])).
% 102.28/102.55 cnf(10725,plain,
% 102.28/102.55 (~P1(a1,f3(x107251,a1))),
% 102.28/102.55 inference(scs_inference,[],[10314,10689,146,65,86,93,111,103])).
% 102.28/102.55 cnf(11382,plain,
% 102.28/102.55 ($false),
% 102.28/102.55 inference(scs_inference,[],[65,10445,9664,10198,9661,10725,8914,8878,2057,9273,2,93,111,71,102,81,94,87,60,88,138]),
% 102.28/102.55 ['proof']).
% 102.28/102.55 % SZS output end Proof
% 102.28/102.55 % Total time :101.620000s
%------------------------------------------------------------------------------