%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET810+4 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n026.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:32 EDT 2024
% Result : Theorem 62.10s 62.20s
% Output : CNFRefutation 62.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.11 % Problem : SET810+4 : TPTP v8.2.0. Released v3.2.0.
% 0.09/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n026.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Sun Jun 23 13:39:39 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.17/0.56 start to proof:theBenchmark
% 62.10/62.18 %-------------------------------------------
% 62.10/62.18 % File :CSE---1.7
% 62.10/62.18 % Problem :theBenchmark
% 62.10/62.18 % Transform :cnf
% 62.10/62.18 % Format :tptp:raw
% 62.10/62.18 % Command :java -jar mcs_scs.jar %d %s
% 62.10/62.18
% 62.10/62.18 % Result :Theorem 61.560000s
% 62.10/62.18 % Output :CNFRefutation 61.560000s
% 62.10/62.18 %-------------------------------------------
% 62.10/62.19 %------------------------------------------------------------------------------
% 62.10/62.19 % File : SET810+4 : TPTP v8.2.0. Released v3.2.0.
% 62.10/62.19 % Domain : Set Theory (Order relations)
% 62.10/62.19 % Problem : Ordinal numbers do not contain each other
% 62.10/62.19 % Version : [Pas05] axioms.
% 62.10/62.19 % English : If a and b are ordinal numbers, it is not possible that a belongs
% 62.10/62.20 % to b and b belongs to a
% 62.10/62.20
% 62.10/62.20 % Refs : [Pas05] Pastre (2005), Email to G. Sutcliffe
% 62.10/62.20 % Source : [Pas05]
% 62.10/62.20 % Names :
% 62.10/62.20
% 62.10/62.20 % Status : Theorem
% 62.10/62.20 % Rating : 0.19 v8.2.0, 0.14 v8.1.0, 0.19 v7.4.0, 0.17 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v6.4.0, 0.12 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.15 v5.1.0, 0.14 v5.0.0, 0.21 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.25 v3.7.0, 0.30 v3.5.0, 0.32 v3.4.0, 0.26 v3.3.0, 0.07 v3.2.0
% 62.10/62.20 % Syntax : Number of formulae : 20 ( 1 unt; 0 def)
% 62.10/62.20 % Number of atoms : 69 ( 4 equ)
% 62.10/62.20 % Maximal formula atoms : 11 ( 3 avg)
% 62.10/62.20 % Number of connectives : 53 ( 4 ~; 3 |; 18 &)
% 62.10/62.20 % ( 17 <=>; 11 =>; 0 <=; 0 <~>)
% 62.10/62.20 % Maximal formula depth : 11 ( 6 avg)
% 62.10/62.20 % Maximal term depth : 3 ( 1 avg)
% 62.10/62.20 % Number of predicates : 9 ( 8 usr; 0 prp; 1-3 aty)
% 62.10/62.20 % Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% 62.10/62.20 % Number of variables : 58 ( 55 !; 3 ?)
% 62.10/62.20 % SPC : FOF_THM_RFO_SEQ
% 62.10/62.20
% 62.10/62.20 % Comments :
% 62.10/62.20 %------------------------------------------------------------------------------
% 62.10/62.20 %----Include set theory definitions
% 62.10/62.20 include('Axioms/SET006+0.ax').
% 62.10/62.20 %----Include ordinal numbers axioms
% 62.10/62.20 include('Axioms/SET006+4.ax').
% 62.10/62.20 %------------------------------------------------------------------------------
% 62.10/62.20 fof(thV3,conjecture,
% 62.10/62.20 ! [A,B] :
% 62.10/62.20 ( ( member(A,on)
% 62.10/62.20 & member(B,on) )
% 62.10/62.20 => ~ ( member(A,B)
% 62.10/62.20 & member(B,A) ) ) ).
% 62.10/62.20
% 62.10/62.20 %------------------------------------------------------------------------------
% 62.10/62.20 %-------------------------------------------
% 62.10/62.20 % Proof found
% 62.10/62.20 % SZS status Theorem for theBenchmark
% 62.10/62.20 % SZS output start Proof
% 62.10/62.20 %ClaNum:145(EqnAxiom:63)
% 62.10/62.20 %VarNum:560(SingletonVarNum:186)
% 62.10/62.20 %MaxLitNum:7
% 62.10/62.20 %MaxfuncDepth:2
% 62.10/62.20 %SharedTerms:9
% 62.10/62.20 %goalClause: 64 65 66 67
% 62.10/62.20 %singleGoalClaCount:4
% 62.10/62.20 [64]P1(a1,a8)
% 62.10/62.20 [65]P1(a1,a9)
% 62.10/62.20 [66]P1(a9,a8)
% 62.10/62.20 [67]P1(a9,a1)
% 62.10/62.20 [68]~P1(x681,a2)
% 62.10/62.20 [70]P5(x701)+~P1(x701,a8)
% 62.10/62.20 [71]~P1(x711,a8)+P6(a10,x711)
% 62.10/62.20 [74]~P2(x742,x741)+P8(x741,x742)
% 62.10/62.20 [75]~P2(x751,x752)+P8(x751,x752)
% 62.10/62.20 [76]~P6(x761,x762)+P7(x761,x762)
% 62.10/62.20 [95]~P1(x951,x952)+P3(a10,x951,x952)
% 62.10/62.20 [113]P1(x1131,x1132)+~P3(a10,x1131,x1132)
% 62.10/62.20 [69]~E(x691,x692)+P1(x691,f22(x692))
% 62.10/62.20 [73]E(x731,x732)+~P1(x731,f22(x732))
% 62.10/62.20 [77]~P8(x771,x772)+P1(x771,f23(x772))
% 62.10/62.20 [80]P8(x801,x802)+~P1(x801,f23(x802))
% 62.10/62.20 [81]P8(x811,x812)+P1(f11(x811,x812),x811)
% 62.10/62.20 [85]P1(f12(x851,x852),x852)+P1(x851,f24(x852))
% 62.10/62.21 [92]~P1(x921,f27(x922))+P1(x921,f13(x921,x922))
% 62.10/62.21 [93]~P1(x931,f27(x932))+P1(f13(x931,x932),x932)
% 62.10/62.21 [101]P8(x1011,x1012)+~P1(f11(x1011,x1012),x1012)
% 62.10/62.21 [102]~P1(x1021,f12(x1021,x1022))+P1(x1021,f24(x1022))
% 62.10/62.21 [103]~P1(x1031,f28(x1032))+P1(x1031,f26(x1032,f22(x1032)))
% 62.10/62.21 [115]P1(x1151,f28(x1152))+~P1(x1151,f26(x1152,f22(x1152)))
% 62.10/62.21 [114]P1(x1141,x1142)+~P4(x1141,x1143,x1142)
% 62.10/62.21 [78]~E(x781,x783)+P1(x781,f25(x782,x783))
% 62.10/62.21 [79]~E(x791,x792)+P1(x791,f25(x792,x793))
% 62.10/62.21 [87]~P1(x871,x873)+P1(x871,f26(x872,x873))
% 62.10/62.21 [88]~P1(x881,x882)+P1(x881,f26(x882,x883))
% 62.10/62.21 [98]P1(x981,x982)+~P1(x981,f17(x983,x982))
% 62.10/62.21 [99]P1(x991,x992)+~P1(x991,f17(x992,x993))
% 62.10/62.21 [100]P1(x1001,x1002)+~P1(x1001,f3(x1002,x1003))
% 62.10/62.21 [105]~P1(x1051,x1052)+~P1(x1051,f3(x1053,x1052))
% 62.10/62.21 [131]P1(x1311,x1312)+~P1(x1311,f21(x1313,x1314,x1312))
% 62.10/62.21 [141]P3(x1411,x1412,x1413)+~P1(x1412,f21(x1413,x1411,x1414))
% 62.10/62.21 [72]~P1(x721,x722)+P5(x721)+~P5(x722)
% 62.10/62.21 [82]~P1(x821,x822)+P8(x821,x822)+~P1(x822,a8)
% 62.10/62.21 [84]~P8(x842,x841)+~P8(x841,x842)+P2(x841,x842)
% 62.10/62.21 [97]~P7(x971,x972)+P6(x971,x972)+P8(f15(x971,x972),x972)
% 62.10/62.21 [107]P7(x1071,x1072)+P1(f18(x1071,x1072),x1072)+P1(f4(x1071,x1072),x1072)
% 62.10/62.21 [108]P7(x1081,x1082)+P1(f18(x1081,x1082),x1082)+P1(f6(x1081,x1082),x1082)
% 62.10/62.21 [109]P7(x1091,x1092)+P1(f18(x1091,x1092),x1092)+P1(f7(x1091,x1092),x1092)
% 62.10/62.21 [110]P7(x1101,x1102)+P1(f5(x1101,x1102),x1102)+P1(f4(x1101,x1102),x1102)
% 62.10/62.21 [111]P7(x1111,x1112)+P1(f5(x1111,x1112),x1112)+P1(f6(x1111,x1112),x1112)
% 62.10/62.21 [112]P7(x1121,x1122)+P1(f5(x1121,x1122),x1122)+P1(f7(x1121,x1122),x1122)
% 62.10/62.21 [116]~P7(x1161,x1162)+P6(x1161,x1162)+P1(f19(x1161,x1162),f15(x1161,x1162))
% 62.10/62.21 [117]P7(x1171,x1172)+P3(x1171,f4(x1171,x1172),f6(x1171,x1172))+P1(f18(x1171,x1172),x1172)
% 62.10/62.21 [118]P7(x1181,x1182)+P3(x1181,f6(x1181,x1182),f7(x1181,x1182))+P1(f18(x1181,x1182),x1182)
% 62.10/62.21 [119]P7(x1191,x1192)+P3(x1191,f4(x1191,x1192),f6(x1191,x1192))+P1(f5(x1191,x1192),x1192)
% 62.10/62.21 [120]P7(x1201,x1202)+P3(x1201,f6(x1201,x1202),f7(x1201,x1202))+P1(f5(x1201,x1202),x1202)
% 62.10/62.21 [121]P7(x1211,x1212)+P3(x1211,f18(x1211,x1212),f5(x1211,x1212))+P1(f4(x1211,x1212),x1212)
% 62.10/62.21 [122]P7(x1221,x1222)+P3(x1221,f5(x1221,x1222),f18(x1221,x1222))+P1(f4(x1221,x1222),x1222)
% 62.10/62.21 [123]P7(x1231,x1232)+P3(x1231,f18(x1231,x1232),f5(x1231,x1232))+P1(f6(x1231,x1232),x1232)
% 62.10/62.21 [124]P7(x1241,x1242)+P3(x1241,f5(x1241,x1242),f18(x1241,x1242))+P1(f6(x1241,x1242),x1242)
% 62.10/62.21 [125]P7(x1251,x1252)+P3(x1251,f18(x1251,x1252),f5(x1251,x1252))+P1(f7(x1251,x1252),x1252)
% 62.10/62.21 [126]P7(x1261,x1262)+P3(x1261,f5(x1261,x1262),f18(x1261,x1262))+P1(f7(x1261,x1262),x1262)
% 62.10/62.21 [132]P7(x1321,x1322)+~P3(x1321,f4(x1321,x1322),f7(x1321,x1322))+P1(f18(x1321,x1322),x1322)
% 62.10/62.21 [133]P7(x1331,x1332)+~P3(x1331,f4(x1331,x1332),f7(x1331,x1332))+P1(f5(x1331,x1332),x1332)
% 62.10/62.21 [134]P7(x1341,x1342)+P3(x1341,f18(x1341,x1342),f5(x1341,x1342))+P3(x1341,f4(x1341,x1342),f6(x1341,x1342))
% 62.10/62.21 [135]P7(x1351,x1352)+P3(x1351,f18(x1351,x1352),f5(x1351,x1352))+P3(x1351,f6(x1351,x1352),f7(x1351,x1352))
% 62.10/62.21 [136]P7(x1361,x1362)+P3(x1361,f5(x1361,x1362),f18(x1361,x1362))+P3(x1361,f4(x1361,x1362),f6(x1361,x1362))
% 62.10/62.21 [137]P7(x1371,x1372)+P3(x1371,f5(x1371,x1372),f18(x1371,x1372))+P3(x1371,f6(x1371,x1372),f7(x1371,x1372))
% 62.10/62.21 [142]P7(x1421,x1422)+P3(x1421,f18(x1421,x1422),f5(x1421,x1422))+~P3(x1421,f4(x1421,x1422),f7(x1421,x1422))
% 62.10/62.21 [143]P7(x1431,x1432)+P3(x1431,f5(x1431,x1432),f18(x1431,x1432))+~P3(x1431,f4(x1431,x1432),f7(x1431,x1432))
% 62.10/62.21 [83]~P1(x831,x833)+P1(x831,x832)+~P8(x833,x832)
% 62.10/62.21 [89]~P1(x893,x892)+~P1(x891,x893)+P1(x891,f27(x892))
% 62.10/62.21 [90]E(x901,x902)+E(x901,x903)+~P1(x901,f25(x903,x902))
% 62.10/62.21 [91]P1(x911,x912)+~P1(x912,x913)+~P1(x911,f24(x913))
% 62.10/62.21 [96]~P1(x961,x963)+P1(x961,x962)+P1(x961,f3(x963,x962))
% 62.10/62.21 [104]~P1(x1041,x1043)+~P1(x1041,x1042)+P1(x1041,f17(x1042,x1043))
% 62.10/62.21 [106]P1(x1061,x1062)+P1(x1061,x1063)+~P1(x1061,f26(x1063,x1062))
% 62.10/62.21 [127]~P7(x1271,x1272)+P6(x1271,x1272)+~P4(x1273,x1271,f15(x1271,x1272))
% 62.10/62.21 [128]~P1(x1281,x1283)+P4(x1281,x1282,x1283)+~E(f20(x1282,x1283,x1281),x1281)
% 62.10/62.21 [130]~P1(x1301,x1303)+P4(x1301,x1302,x1303)+P1(f20(x1302,x1303,x1301),x1303)
% 62.10/62.21 [145]~P1(x1451,x1453)+P4(x1451,x1452,x1453)+~P3(x1452,x1451,f20(x1452,x1453,x1451))
% 62.10/62.21 [139]~P1(x1391,x1394)+~P3(x1393,x1391,x1392)+P1(x1391,f21(x1392,x1393,x1394))
% 62.10/62.21 [86]~P5(x861)+P1(f14(x861),x861)+~P6(a10,x861)+P1(x861,a8)
% 62.10/62.21 [94]~P5(x941)+~P6(a10,x941)+~P8(f14(x941),x941)+P1(x941,a8)
% 62.10/62.21 [129]~P4(x1292,x1293,x1294)+E(x1291,x1292)+P3(x1293,x1292,x1291)+~P1(x1291,x1294)
% 62.10/62.21 [138]~P8(x1383,x1382)+~P6(x1381,x1382)+~P1(x1384,x1383)+P4(f16(x1381,x1382,x1383),x1381,x1383)
% 62.10/62.21 [140]~P3(x1404,x1401,x1403)+~P3(x1404,x1403,x1401)+~P1(x1401,x1402)+~P1(x1403,x1402)+~P7(x1404,x1402)
% 62.10/62.21 [144]~P1(x1442,x1444)+~P7(x1441,x1444)+~P3(x1441,x1445,x1443)+~P3(x1441,x1442,x1445)+P3(x1441,x1442,x1443)+~P1(x1443,x1444)+~P1(x1445,x1444)
% 62.10/62.21 %EqnAxiom
% 62.10/62.21 [1]E(x11,x11)
% 62.10/62.21 [2]E(x22,x21)+~E(x21,x22)
% 62.10/62.21 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 62.10/62.21 [4]~E(x41,x42)+E(f22(x41),f22(x42))
% 62.10/62.21 [5]~E(x51,x52)+E(f20(x51,x53,x54),f20(x52,x53,x54))
% 62.10/62.21 [6]~E(x61,x62)+E(f20(x63,x61,x64),f20(x63,x62,x64))
% 62.10/62.21 [7]~E(x71,x72)+E(f20(x73,x74,x71),f20(x73,x74,x72))
% 62.10/62.21 [8]~E(x81,x82)+E(f23(x81),f23(x82))
% 62.10/62.21 [9]~E(x91,x92)+E(f25(x91,x93),f25(x92,x93))
% 62.10/62.21 [10]~E(x101,x102)+E(f25(x103,x101),f25(x103,x102))
% 62.10/62.21 [11]~E(x111,x112)+E(f4(x111,x113),f4(x112,x113))
% 62.10/62.21 [12]~E(x121,x122)+E(f4(x123,x121),f4(x123,x122))
% 62.10/62.21 [13]~E(x131,x132)+E(f7(x131,x133),f7(x132,x133))
% 62.10/62.21 [14]~E(x141,x142)+E(f7(x143,x141),f7(x143,x142))
% 62.10/62.21 [15]~E(x151,x152)+E(f11(x151,x153),f11(x152,x153))
% 62.10/62.21 [16]~E(x161,x162)+E(f11(x163,x161),f11(x163,x162))
% 62.10/62.21 [17]~E(x171,x172)+E(f24(x171),f24(x172))
% 62.10/62.21 [18]~E(x181,x182)+E(f12(x181,x183),f12(x182,x183))
% 62.10/62.21 [19]~E(x191,x192)+E(f12(x193,x191),f12(x193,x192))
% 62.10/62.21 [20]~E(x201,x202)+E(f14(x201),f14(x202))
% 62.10/62.21 [21]~E(x211,x212)+E(f26(x211,x213),f26(x212,x213))
% 62.10/62.21 [22]~E(x221,x222)+E(f26(x223,x221),f26(x223,x222))
% 62.10/62.21 [23]~E(x231,x232)+E(f5(x231,x233),f5(x232,x233))
% 62.10/62.21 [24]~E(x241,x242)+E(f5(x243,x241),f5(x243,x242))
% 62.10/62.21 [25]~E(x251,x252)+E(f27(x251),f27(x252))
% 62.10/62.21 [26]~E(x261,x262)+E(f18(x261,x263),f18(x262,x263))
% 62.10/62.21 [27]~E(x271,x272)+E(f18(x273,x271),f18(x273,x272))
% 62.10/62.21 [28]~E(x281,x282)+E(f6(x281,x283),f6(x282,x283))
% 62.10/62.21 [29]~E(x291,x292)+E(f6(x293,x291),f6(x293,x292))
% 62.10/62.21 [30]~E(x301,x302)+E(f13(x301,x303),f13(x302,x303))
% 62.10/62.21 [31]~E(x311,x312)+E(f13(x313,x311),f13(x313,x312))
% 62.10/62.21 [32]~E(x321,x322)+E(f21(x321,x323,x324),f21(x322,x323,x324))
% 62.10/62.21 [33]~E(x331,x332)+E(f21(x333,x331,x334),f21(x333,x332,x334))
% 62.10/62.21 [34]~E(x341,x342)+E(f21(x343,x344,x341),f21(x343,x344,x342))
% 62.10/62.21 [35]~E(x351,x352)+E(f3(x351,x353),f3(x352,x353))
% 62.10/62.21 [36]~E(x361,x362)+E(f3(x363,x361),f3(x363,x362))
% 62.10/62.21 [37]~E(x371,x372)+E(f28(x371),f28(x372))
% 62.10/62.21 [38]~E(x381,x382)+E(f17(x381,x383),f17(x382,x383))
% 62.10/62.21 [39]~E(x391,x392)+E(f17(x393,x391),f17(x393,x392))
% 62.10/62.21 [40]~E(x401,x402)+E(f15(x401,x403),f15(x402,x403))
% 62.10/62.21 [41]~E(x411,x412)+E(f15(x413,x411),f15(x413,x412))
% 62.10/62.21 [42]~E(x421,x422)+E(f16(x421,x423,x424),f16(x422,x423,x424))
% 62.10/62.21 [43]~E(x431,x432)+E(f16(x433,x431,x434),f16(x433,x432,x434))
% 62.10/62.21 [44]~E(x441,x442)+E(f16(x443,x444,x441),f16(x443,x444,x442))
% 62.10/62.21 [45]~E(x451,x452)+E(f19(x451,x453),f19(x452,x453))
% 62.10/62.21 [46]~E(x461,x462)+E(f19(x463,x461),f19(x463,x462))
% 62.10/62.21 [47]P1(x472,x473)+~E(x471,x472)+~P1(x471,x473)
% 62.10/62.21 [48]P1(x483,x482)+~E(x481,x482)+~P1(x483,x481)
% 62.10/62.21 [49]P3(x492,x493,x494)+~E(x491,x492)+~P3(x491,x493,x494)
% 62.10/62.21 [50]P3(x503,x502,x504)+~E(x501,x502)+~P3(x503,x501,x504)
% 62.10/62.21 [51]P3(x513,x514,x512)+~E(x511,x512)+~P3(x513,x514,x511)
% 62.10/62.21 [52]P4(x522,x523,x524)+~E(x521,x522)+~P4(x521,x523,x524)
% 62.10/62.21 [53]P4(x533,x532,x534)+~E(x531,x532)+~P4(x533,x531,x534)
% 62.10/62.21 [54]P4(x543,x544,x542)+~E(x541,x542)+~P4(x543,x544,x541)
% 62.10/62.21 [55]P7(x552,x553)+~E(x551,x552)+~P7(x551,x553)
% 62.10/62.21 [56]P7(x563,x562)+~E(x561,x562)+~P7(x563,x561)
% 62.10/62.21 [57]P8(x572,x573)+~E(x571,x572)+~P8(x571,x573)
% 62.10/62.21 [58]P8(x583,x582)+~E(x581,x582)+~P8(x583,x581)
% 62.10/62.21 [59]P6(x592,x593)+~E(x591,x592)+~P6(x591,x593)
% 62.10/62.21 [60]P6(x603,x602)+~E(x601,x602)+~P6(x603,x601)
% 62.10/62.21 [61]~P5(x611)+P5(x612)+~E(x611,x612)
% 62.10/62.21 [62]P2(x622,x623)+~E(x621,x622)+~P2(x621,x623)
% 62.10/62.21 [63]P2(x633,x632)+~E(x631,x632)+~P2(x633,x631)
% 62.10/62.21
% 62.10/62.21 %-------------------------------------------
% 62.10/62.22 cnf(146,plain,
% 62.10/62.22 (P1(x1461,f22(x1461))),
% 62.10/62.22 inference(equality_inference,[],[69])).
% 62.10/62.22 cnf(147,plain,
% 62.10/62.22 (P1(x1471,f25(x1472,x1471))),
% 62.10/62.22 inference(equality_inference,[],[78])).
% 62.10/62.22 cnf(148,plain,
% 62.10/62.22 (P1(x1481,f25(x1481,x1482))),
% 62.10/62.22 inference(equality_inference,[],[79])).
% 62.10/62.22 cnf(149,plain,
% 62.10/62.22 (P5(a1)),
% 62.10/62.22 inference(scs_inference,[],[64,70])).
% 62.10/62.22 cnf(151,plain,
% 62.10/62.22 (P8(a2,x1511)),
% 62.10/62.22 inference(scs_inference,[],[64,68,70,81])).
% 62.10/62.22 cnf(152,plain,
% 62.10/62.22 (~P1(x1521,a2)),
% 62.10/62.22 inference(rename_variables,[],[68])).
% 62.10/62.22 cnf(154,plain,
% 62.10/62.22 (~P1(x1541,f27(a2))),
% 62.10/62.22 inference(scs_inference,[],[64,68,152,70,81,93])).
% 62.10/62.22 cnf(155,plain,
% 62.10/62.22 (~P1(x1551,a2)),
% 62.10/62.22 inference(rename_variables,[],[68])).
% 62.10/62.22 cnf(157,plain,
% 62.10/62.22 (~P4(x1571,x1572,a2)),
% 62.10/62.22 inference(scs_inference,[],[64,68,152,155,70,81,93,114])).
% 62.10/62.22 cnf(159,plain,
% 62.10/62.22 (P8(a9,a1)),
% 62.10/62.22 inference(scs_inference,[],[64,67,68,152,155,70,81,93,114,82])).
% 62.10/62.22 cnf(161,plain,
% 62.10/62.22 (P1(a1,a1)),
% 62.10/62.22 inference(scs_inference,[],[64,65,67,68,152,155,70,81,93,114,82,83])).
% 62.10/62.22 cnf(163,plain,
% 62.10/62.22 (P2(a2,a2)),
% 62.10/62.22 inference(scs_inference,[],[64,65,67,68,152,155,70,81,93,114,82,83,84])).
% 62.10/62.22 cnf(166,plain,
% 62.10/62.22 (~P1(x1661,a2)),
% 62.10/62.22 inference(rename_variables,[],[68])).
% 62.10/62.22 cnf(170,plain,
% 62.10/62.22 (~P1(x1701,a2)),
% 62.10/62.22 inference(rename_variables,[],[68])).
% 62.10/62.22 cnf(171,plain,
% 62.10/62.22 (~P1(x1711,a2)),
% 62.10/62.22 inference(rename_variables,[],[68])).
% 62.10/62.22 cnf(172,plain,
% 62.10/62.22 (~P1(x1721,a2)),
% 62.10/62.22 inference(rename_variables,[],[68])).
% 62.10/62.22 cnf(174,plain,
% 62.10/62.22 (P7(x1741,a2)+~E(a1,f11(x1742,a8))+P1(f4(x1741,a2),a2)),
% 62.10/62.22 inference(scs_inference,[],[64,65,67,68,152,155,166,170,171,172,70,81,93,114,82,83,84,48,47,101,110])).
% 62.10/62.22 cnf(176,plain,
% 62.10/62.22 (P5(a9)),
% 62.10/62.22 inference(scs_inference,[],[66,70])).
% 62.10/62.22 cnf(178,plain,
% 62.10/62.22 (~P1(x1781,f27(f27(a2)))),
% 62.10/62.22 inference(scs_inference,[],[66,154,70,93])).
% 62.10/62.22 cnf(179,plain,
% 62.10/62.22 (~P1(x1791,f27(a2))),
% 62.10/62.22 inference(rename_variables,[],[154])).
% 62.10/62.22 cnf(181,plain,
% 62.10/62.22 (P8(f27(a2),x1811)),
% 62.10/62.22 inference(scs_inference,[],[66,154,179,70,93,81])).
% 62.10/62.22 cnf(182,plain,
% 62.10/62.22 (~P1(x1821,f27(a2))),
% 62.10/62.22 inference(rename_variables,[],[154])).
% 62.10/62.22 cnf(186,plain,
% 62.10/62.22 (P2(f27(a2),a2)),
% 62.10/62.22 inference(scs_inference,[],[66,154,179,182,151,70,93,81,114,84])).
% 62.10/62.23 cnf(189,plain,
% 62.10/62.23 (P8(a1,a9)),
% 62.10/62.23 inference(scs_inference,[],[66,65,154,179,182,151,70,93,81,114,84,82])).
% 62.10/62.23 cnf(192,plain,
% 62.10/62.23 (~P1(x1921,f27(a2))),
% 62.10/62.23 inference(rename_variables,[],[154])).
% 62.10/62.23 cnf(195,plain,
% 62.10/62.23 (P1(a9,a9)),
% 62.10/62.23 inference(scs_inference,[],[64,66,65,67,154,179,182,151,68,70,93,81,114,84,82,48,174,83])).
% 62.10/62.23 cnf(197,plain,
% 62.10/62.23 (P7(x1971,f27(a2))+P1(f6(x1971,f27(a2)),f27(a2))),
% 62.10/62.23 inference(scs_inference,[],[64,66,65,67,154,179,182,192,151,68,70,93,81,114,84,82,48,174,83,111])).
% 62.10/62.23 cnf(212,plain,
% 62.10/62.23 (P7(x2121,f27(a2))),
% 62.10/62.23 inference(scs_inference,[],[154,197])).
% 62.10/62.23 cnf(214,plain,
% 62.10/62.23 (P8(f27(f27(a2)),x2141)),
% 62.10/62.23 inference(scs_inference,[],[178,154,197,81])).
% 62.10/62.23 cnf(234,plain,
% 62.10/62.23 (P2(a1,a9)),
% 62.10/62.23 inference(scs_inference,[],[159,189,84])).
% 62.10/62.23 cnf(247,plain,
% 62.10/62.23 (P2(f27(a2),f27(a2))),
% 62.10/62.23 inference(scs_inference,[],[181,84])).
% 62.10/62.23 cnf(253,plain,
% 62.10/62.23 (P7(x2531,x2532)+~E(f27(a2),x2532)),
% 62.10/62.23 inference(scs_inference,[],[67,154,181,212,84,48,56])).
% 62.10/62.23 cnf(256,plain,
% 62.10/62.23 (P2(f27(f27(a2)),a2)),
% 62.10/62.23 inference(scs_inference,[],[151,214,84])).
% 62.10/62.23 cnf(258,plain,
% 62.10/62.23 (P8(a2,x2581)),
% 62.10/62.23 inference(rename_variables,[],[151])).
% 62.10/62.23 cnf(260,plain,
% 62.10/62.23 (~E(a9,f27(a2))),
% 62.10/62.23 inference(scs_inference,[],[65,154,151,214,84,48])).
% 62.10/62.23 cnf(261,plain,
% 62.10/62.23 (~P1(x2611,f27(a2))),
% 62.10/62.23 inference(rename_variables,[],[154])).
% 62.10/62.23 cnf(263,plain,
% 62.10/62.23 (~P1(x2631,a2)),
% 62.10/62.23 inference(rename_variables,[],[68])).
% 62.23/62.23 cnf(265,plain,
% 62.23/62.23 (~P1(x2651,a2)),
% 62.23/62.23 inference(rename_variables,[],[68])).
% 62.23/62.23 cnf(269,plain,
% 62.23/62.23 (P7(x2691,a2)+~E(f6(x2691,a2),x2692)),
% 62.23/62.23 inference(scs_inference,[],[65,154,261,68,263,265,151,258,214,157,84,48,111,130,83,47])).
% 62.23/62.23 cnf(283,plain,
% 62.23/62.23 (P7(x2831,a2)),
% 62.23/62.23 inference(equality_inference,[],[269])).
% 62.23/62.23 cnf(289,plain,
% 62.23/62.23 (P8(a9,x2891)+~E(a1,x2891)),
% 62.23/62.23 inference(scs_inference,[],[67,159,178,48,58])).
% 62.23/62.23 cnf(299,plain,
% 62.23/62.23 (~E(f22(x2991),f27(a2))),
% 62.23/62.23 inference(scs_inference,[],[154,146,48])).
% 62.23/62.23 cnf(310,plain,
% 62.23/62.23 (~E(f25(x3101,x3102),f27(a2))),
% 62.23/62.23 inference(scs_inference,[],[154,147,48])).
% 62.23/62.23 cnf(334,plain,
% 62.23/62.23 (P8(x3341,x3342)+~E(a2,x3341)),
% 62.23/62.23 inference(scs_inference,[],[65,151,256,62,47,57])).
% 62.23/62.23 cnf(345,plain,
% 62.23/62.23 (P8(x3451,x3452)+~E(f27(f27(a2)),x3451)),
% 62.23/62.23 inference(scs_inference,[],[161,214,186,62,47,57])).
% 62.23/62.23 cnf(355,plain,
% 62.23/62.23 (P8(x3551,x3552)+~E(f27(a2),x3551)),
% 62.23/62.23 inference(scs_inference,[],[181,247,62,57])).
% 62.23/62.23 cnf(366,plain,
% 62.23/62.23 (P1(x3661,f25(x3662,x3663))+~E(x3662,x3661)),
% 62.23/62.23 inference(scs_inference,[],[148,163,62,47])).
% 62.23/62.23 cnf(383,plain,
% 62.23/62.23 (P1(x3831,f25(x3832,x3833))+~E(x3833,x3831)),
% 62.23/62.23 inference(scs_inference,[],[147,47])).
% 62.23/62.23 cnf(384,plain,
% 62.23/62.23 (P8(x3841,f25(x3842,x3843))+~E(x3843,f11(x3841,f25(x3842,x3843)))),
% 62.23/62.23 inference(scs_inference,[],[147,47,101])).
% 62.23/62.23 cnf(392,plain,
% 62.23/62.23 (~P1(f27(a2),f22(a9))),
% 62.23/62.23 inference(scs_inference,[],[260,2,73])).
% 62.23/62.23 cnf(393,plain,
% 62.23/62.23 (~E(f27(a2),a9)),
% 62.23/62.23 inference(scs_inference,[],[392,69])).
% 62.23/62.23 cnf(471,plain,
% 62.23/62.23 (~P6(x4711,a9)+P4(f16(x4711,a9,a1),x4711,a1)),
% 62.23/62.23 inference(scs_inference,[],[234,67,75,138])).
% 62.23/62.23 cnf(502,plain,
% 62.23/62.23 (~P6(x5021,x5022)+P7(x5023,x5022)+~E(x5021,x5023)),
% 62.23/62.23 inference(scs_inference,[],[76,55])).
% 62.23/62.23 cnf(565,plain,
% 62.23/62.23 (P3(a10,x5651,f24(f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[154,95,85])).
% 62.23/62.23 cnf(566,plain,
% 62.23/62.23 (P1(x5661,f24(f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[565,113])).
% 62.23/62.23 cnf(569,plain,
% 62.23/62.23 (P8(x5691,f24(f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[565,154,113,48,101])).
% 62.23/62.23 cnf(605,plain,
% 62.23/62.23 (P8(x6051,x6052)+~E(f24(f27(a2)),x6052)),
% 62.23/62.23 inference(scs_inference,[],[569,58])).
% 62.23/62.23 cnf(1019,plain,
% 62.23/62.23 (P1(a9,f26(x10191,f26(a8,x10192)))),
% 62.23/62.23 inference(scs_inference,[],[66,87,88])).
% 62.23/62.23 cnf(1020,plain,
% 62.23/62.23 (P1(a9,f26(a8,x10201))),
% 62.23/62.23 inference(scs_inference,[],[1019,154,106])).
% 62.23/62.23 cnf(1021,plain,
% 62.23/62.23 (P1(a9,f26(x10211,f26(a8,x10212)))),
% 62.23/62.23 inference(rename_variables,[],[1019])).
% 62.23/62.23 cnf(1022,plain,
% 62.23/62.23 (~P1(x10221,f27(a2))),
% 62.23/62.23 inference(rename_variables,[],[154])).
% 62.23/62.23 cnf(1026,plain,
% 62.23/62.23 (P1(a9,f28(a8))),
% 62.23/62.23 inference(scs_inference,[],[1019,1021,154,1022,106,48,115])).
% 62.23/62.23 cnf(1477,plain,
% 62.23/62.23 (~P1(x14771,f27(x14772))+P1(x14771,f26(x14773,f13(x14771,x14772)))),
% 62.23/62.23 inference(scs_inference,[],[92,87])).
% 62.23/62.23 cnf(2758,plain,
% 62.23/62.23 (~P1(x27581,f21(f27(a2),a10,x27582))),
% 62.23/62.23 inference(scs_inference,[],[154,141,113])).
% 62.23/62.23 cnf(2759,plain,
% 62.23/62.23 (P8(f21(f27(a2),a10,x27591),x27592)),
% 62.23/62.23 inference(scs_inference,[],[2758,81])).
% 62.23/62.23 cnf(2760,plain,
% 62.23/62.23 (~P1(x27601,f21(f27(a2),a10,x27602))),
% 62.23/62.23 inference(rename_variables,[],[2758])).
% 62.23/62.23 cnf(2762,plain,
% 62.23/62.23 (~P4(x27621,x27622,f21(f27(a2),a10,x27623))),
% 62.23/62.23 inference(scs_inference,[],[2758,2760,81,114])).
% 62.23/62.23 cnf(2764,plain,
% 62.23/62.23 (~P3(a10,x27641,f27(a2))),
% 62.23/62.23 inference(scs_inference,[],[148,2758,2760,81,114,139])).
% 62.23/62.23 cnf(2788,plain,
% 62.23/62.23 (P8(x27881,x27882)+~E(f21(f27(a2),a10,x27883),x27881)),
% 62.23/62.23 inference(scs_inference,[],[148,2764,214,393,2759,84,129,57])).
% 62.23/62.23 cnf(2923,plain,
% 62.23/62.23 (P1(f16(x29231,a9,a1),a1)+~P6(x29231,a9)),
% 62.23/62.23 inference(scs_inference,[],[471,114])).
% 62.23/62.23 cnf(2969,plain,
% 62.23/62.23 (P1(f16(a10,a9,a1),a1)),
% 62.23/62.23 inference(scs_inference,[],[66,2923,71])).
% 62.23/62.23 cnf(4631,plain,
% 62.23/62.23 (P8(a1,a1)),
% 62.23/62.23 inference(scs_inference,[],[161,64,82])).
% 62.23/62.23 cnf(6025,plain,
% 62.23/62.23 (~E(f26(a8,x60251),f27(f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[178,1020,48])).
% 62.23/62.23 cnf(8114,plain,
% 62.23/62.23 (P8(a9,a9)),
% 62.23/62.23 inference(scs_inference,[],[195,66,82])).
% 62.23/62.23 cnf(8116,plain,
% 62.23/62.23 (P8(a9,x81161)+~E(a9,x81161)),
% 62.23/62.23 inference(scs_inference,[],[195,66,82,58])).
% 62.23/62.23 cnf(10246,plain,
% 62.23/62.23 (~E(a1,f21(f27(a2),a10,x102461))),
% 62.23/62.23 inference(scs_inference,[],[67,2758,48])).
% 62.23/62.23 cnf(10604,plain,
% 62.23/62.23 (~E(f27(a2),f25(x106041,x106042))),
% 62.23/62.23 inference(scs_inference,[],[310,2])).
% 62.23/62.23 cnf(10613,plain,
% 62.23/62.23 (~P4(f25(x106131,x106132),a10,f25(x106133,f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[2764,147,10604,6025,2,129])).
% 62.23/62.23 cnf(10691,plain,
% 62.23/62.23 (~E(f21(f27(a2),a10,x106911),a1)),
% 62.23/62.23 inference(scs_inference,[],[10246,2])).
% 62.23/62.23 cnf(11708,plain,
% 62.23/62.23 (P3(x117081,f27(a2),f22(x117082))+~P4(f27(a2),x117081,f24(f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[566,299,129])).
% 62.23/62.23 cnf(12054,plain,
% 62.23/62.23 (~E(f22(f27(a2)),f22(a9))),
% 62.23/62.23 inference(scs_inference,[],[392,146,48])).
% 62.23/62.23 cnf(14323,plain,
% 62.23/62.23 (P1(a1,f23(a1))),
% 62.23/62.23 inference(scs_inference,[],[4631,77])).
% 62.23/62.23 cnf(14325,plain,
% 62.23/62.23 (P1(a1,f26(x143251,a8))),
% 62.23/62.23 inference(scs_inference,[],[64,4631,77,87])).
% 62.23/62.23 cnf(14327,plain,
% 62.23/62.23 (P1(a1,f26(a8,x143271))),
% 62.23/62.23 inference(scs_inference,[],[64,4631,77,87,88])).
% 62.23/62.23 cnf(14335,plain,
% 62.23/62.23 (~P1(a1,f3(x143351,a8))),
% 62.23/62.23 inference(scs_inference,[],[64,4631,392,77,87,88,98,99,100,105])).
% 62.23/62.23 cnf(14339,plain,
% 62.23/62.23 (P1(x143391,f24(a2))),
% 62.23/62.23 inference(scs_inference,[],[64,4631,392,68,77,87,88,98,99,100,105,131,85])).
% 62.23/62.23 cnf(14340,plain,
% 62.23/62.23 (~P1(x143401,a2)),
% 62.23/62.23 inference(rename_variables,[],[68])).
% 62.23/62.23 cnf(14342,plain,
% 62.23/62.23 (P3(a10,a1,a8)),
% 62.23/62.23 inference(scs_inference,[],[64,4631,392,68,77,87,88,98,99,100,105,131,85,95])).
% 62.23/62.23 cnf(14346,plain,
% 62.23/62.23 (~P3(a10,f27(a2),f22(a9))),
% 62.23/62.23 inference(scs_inference,[],[64,4631,12054,392,68,77,87,88,98,99,100,105,131,85,95,73,113])).
% 62.23/62.23 cnf(14348,plain,
% 62.23/62.23 (P6(a10,a1)),
% 62.23/62.23 inference(scs_inference,[],[64,4631,12054,392,68,77,87,88,98,99,100,105,131,85,95,73,113,71])).
% 62.23/62.23 cnf(14355,plain,
% 62.23/62.23 (P1(x143551,f22(x143551))),
% 62.23/62.23 inference(rename_variables,[],[146])).
% 62.23/62.23 cnf(14357,plain,
% 62.23/62.23 (P1(a1,f17(a8,a8))),
% 62.23/62.23 inference(scs_inference,[],[64,4631,12054,2969,392,149,146,68,77,87,88,98,99,100,105,131,85,95,73,113,71,114,72,96,104])).
% 62.23/62.23 cnf(14360,plain,
% 62.23/62.23 (P1(x143601,f25(x143601,x143602))),
% 62.23/62.23 inference(rename_variables,[],[148])).
% 62.23/62.23 cnf(14361,plain,
% 62.23/62.23 (~P4(f25(x143611,x143612),a10,f25(x143613,f27(a2)))),
% 62.23/62.23 inference(rename_variables,[],[10613])).
% 62.23/62.23 cnf(14368,plain,
% 62.23/62.23 (P1(x143681,f22(x143681))),
% 62.23/62.23 inference(rename_variables,[],[146])).
% 62.23/62.23 cnf(14371,plain,
% 62.23/62.23 (P3(a10,x143711,f24(f27(a2)))),
% 62.23/62.23 inference(rename_variables,[],[565])).
% 62.23/62.23 cnf(14374,plain,
% 62.23/62.23 (P1(x143741,f22(x143741))),
% 62.23/62.23 inference(rename_variables,[],[146])).
% 62.23/62.23 cnf(14379,plain,
% 62.23/62.23 (~P1(x143791,f21(f27(a2),a10,x143792))),
% 62.23/62.23 inference(rename_variables,[],[2758])).
% 62.23/62.23 cnf(14381,plain,
% 62.23/62.23 (~P1(f27(a2),f26(f22(a9),f22(a9)))),
% 62.23/62.23 inference(scs_inference,[],[64,10613,14361,4631,12054,2969,1026,392,2758,149,146,14355,14368,148,14360,565,68,14340,77,87,88,98,99,100,105,131,85,95,73,113,71,114,72,96,104,128,145,91,139,89,90,83,106])).
% 62.23/62.23 cnf(14391,plain,
% 62.23/62.23 (~P7(a10,f24(f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[64,10613,14361,4631,12054,2969,1019,1026,299,569,392,2758,14379,149,146,14355,14368,14374,148,14360,566,565,14371,68,14340,77,87,88,98,99,100,105,131,85,95,73,113,71,114,72,96,104,128,145,91,139,89,90,83,106,48,58,129,140])).
% 62.23/62.23 cnf(14402,plain,
% 62.23/62.23 (P7(a10,a1)),
% 62.23/62.23 inference(scs_inference,[],[64,10613,14361,4631,12054,2969,1019,1026,299,569,392,2758,14379,149,146,14355,14368,14374,148,14360,566,565,14371,68,14340,77,87,88,98,99,100,105,131,85,95,73,113,71,114,72,96,104,128,145,91,139,89,90,83,106,48,58,129,140,92,141,11708,76])).
% 62.23/62.23 cnf(14404,plain,
% 62.23/62.23 (~E(x144041,a10)+~P6(x144041,f24(f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[64,10613,14361,4631,12054,2969,1019,1026,299,569,392,2758,14379,149,146,14355,14368,14374,148,14360,566,565,14371,68,14340,77,87,88,98,99,100,105,131,85,95,73,113,71,114,72,96,104,128,145,91,139,89,90,83,106,48,58,129,140,92,141,11708,76,502])).
% 62.23/62.23 cnf(14406,plain,
% 62.23/62.23 (P8(f16(a10,a9,a1),a1)),
% 62.23/62.23 inference(scs_inference,[],[64,10613,14361,4631,12054,2969,1019,1026,299,569,392,2758,14379,149,146,14355,14368,14374,148,14360,566,565,14371,68,14340,77,87,88,98,99,100,105,131,85,95,73,113,71,114,72,96,104,128,145,91,139,89,90,83,106,48,58,129,140,92,141,11708,76,502,82])).
% 62.23/62.23 cnf(14411,plain,
% 62.23/62.23 (~P6(a10,f24(f27(a2)))),
% 62.23/62.23 inference(equality_inference,[],[14404])).
% 62.23/62.23 cnf(14414,plain,
% 62.23/62.23 (~P1(x144141,f3(x144142,f24(a2)))),
% 62.23/62.23 inference(scs_inference,[],[14339,105])).
% 62.23/62.23 cnf(14420,plain,
% 62.23/62.23 (P1(f16(a10,a9,a1),f23(a1))),
% 62.23/62.23 inference(scs_inference,[],[14339,14335,14406,105,114,99,77])).
% 62.23/62.23 cnf(14426,plain,
% 62.23/62.23 (P1(x144261,f26(x144262,f24(a2)))),
% 62.23/62.23 inference(scs_inference,[],[14339,14335,14406,105,114,99,77,100,131,87])).
% 62.23/62.23 cnf(14430,plain,
% 62.23/62.23 (P1(x144301,f26(f24(a2),x144302))),
% 62.23/62.23 inference(scs_inference,[],[14339,14335,14406,105,114,99,77,100,131,87,98,88])).
% 62.23/62.23 cnf(14432,plain,
% 62.23/62.23 (P3(a10,x144321,f24(a2))),
% 62.23/62.23 inference(scs_inference,[],[14339,14335,14406,105,114,99,77,100,131,87,98,88,95])).
% 62.23/62.23 cnf(14436,plain,
% 62.23/62.23 (~P1(f21(f27(a2),a10,x144361),f22(a1))),
% 62.23/62.23 inference(scs_inference,[],[14339,14335,14406,10691,105,114,99,77,100,131,87,98,88,95,113,73])).
% 62.23/62.23 cnf(14444,plain,
% 62.23/62.23 (P1(x144441,f24(a2))),
% 62.23/62.23 inference(rename_variables,[],[14339])).
% 62.23/62.23 cnf(14447,plain,
% 62.23/62.23 (P1(x144471,f24(a2))),
% 62.23/62.23 inference(rename_variables,[],[14339])).
% 62.23/62.23 cnf(14449,plain,
% 62.23/62.23 (P1(a1,f21(a8,a10,a8))),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14335,14406,14411,10691,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139])).
% 62.23/62.23 cnf(14451,plain,
% 62.23/62.23 (P1(a9,f27(a8))),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14335,14406,14411,10691,67,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89])).
% 62.23/62.23 cnf(14455,plain,
% 62.23/62.23 (~E(f24(a2),f27(a2))),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14335,14406,14411,10691,67,2764,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89,90,51])).
% 62.23/62.23 cnf(14462,plain,
% 62.23/62.23 (P1(x144621,f24(a2))),
% 62.23/62.23 inference(rename_variables,[],[14339])).
% 62.23/62.23 cnf(14472,plain,
% 62.23/62.23 (P7(a10,a9)),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14447,14335,14346,14406,14411,10691,8114,67,299,2764,195,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89,90,51,83,106,129,138,1477,605,80,76])).
% 62.23/62.23 cnf(14474,plain,
% 62.23/62.23 (P1(a9,f13(a9,a8))),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14447,14335,14346,14406,14411,10691,8114,67,299,2764,195,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89,90,51,83,106,129,138,1477,605,80,76,92])).
% 62.23/62.23 cnf(14478,plain,
% 62.23/62.23 (P1(f11(a8,f3(x144781,a8)),a8)),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14447,14335,14346,14406,14411,10691,8114,67,299,2764,195,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89,90,51,83,106,129,138,1477,605,80,76,92,141,81])).
% 62.23/62.23 cnf(14480,plain,
% 62.23/62.23 (~P1(f11(a8,f3(x144801,a8)),f3(x144801,a8))),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14447,14335,14346,14406,14411,10691,8114,67,299,2764,195,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89,90,51,83,106,129,138,1477,605,80,76,92,141,81,101])).
% 62.23/62.23 cnf(14484,plain,
% 62.23/62.23 (~P3(a10,f27(a2),f20(a10,f24(a2),f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14447,14462,14335,14346,14406,14411,10691,8114,283,67,299,2764,195,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89,90,51,83,106,129,138,1477,605,80,76,92,141,81,101,97,145])).
% 62.23/62.23 cnf(14485,plain,
% 62.23/62.23 (P1(x144851,f24(a2))),
% 62.23/62.23 inference(rename_variables,[],[14339])).
% 62.23/62.23 cnf(14487,plain,
% 62.23/62.23 (~E(f20(a10,f24(a2),f27(a2)),f27(a2))),
% 62.23/62.23 inference(scs_inference,[],[64,14342,14348,14339,14444,14447,14462,14485,14335,14346,14406,14411,10691,8114,283,67,299,2764,195,66,105,114,99,77,100,131,87,98,88,95,113,73,71,60,96,104,91,139,89,90,51,83,106,129,138,1477,605,80,76,92,141,81,101,97,145,128])).
% 62.23/62.23 cnf(14498,plain,
% 62.23/62.23 (~P1(a1,f3(x144981,a9))),
% 62.23/62.23 inference(scs_inference,[],[65,105])).
% 62.23/62.23 cnf(14500,plain,
% 62.23/62.23 (P1(a1,f26(x145001,a9))),
% 62.23/62.23 inference(scs_inference,[],[65,105,87])).
% 62.23/62.23 cnf(14504,plain,
% 62.23/62.23 (P1(a1,f26(a9,x145041))),
% 62.23/62.23 inference(scs_inference,[],[65,14480,105,87,114,88])).
% 62.23/62.23 cnf(14506,plain,
% 62.23/62.23 (~P1(x145061,f3(f27(a2),x145062))),
% 62.23/62.23 inference(scs_inference,[],[65,14480,154,105,87,114,88,100])).
% 62.23/62.23 cnf(14508,plain,
% 62.23/62.23 (~P1(x145081,f17(f27(a2),x145082))),
% 62.23/62.23 inference(scs_inference,[],[65,14480,154,105,87,114,88,100,99])).
% 62.23/62.23 cnf(14510,plain,
% 62.23/62.23 (P1(a9,f23(a9))),
% 62.23/62.23 inference(scs_inference,[],[65,14480,8114,154,105,87,114,88,100,99,77])).
% 62.23/62.23 cnf(14512,plain,
% 62.23/62.23 (~P1(x145121,f21(x145122,x145123,f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[65,14480,8114,154,105,87,114,88,100,99,77,131])).
% 62.23/62.23 cnf(14514,plain,
% 62.23/62.23 (~P1(x145141,f17(x145142,f27(a2)))),
% 62.23/62.23 inference(scs_inference,[],[65,14480,8114,154,105,87,114,88,100,99,77,131,98])).
% 62.23/62.23 cnf(14520,plain,
% 62.23/62.23 (P3(a10,a1,a9)),
% 62.23/62.23 inference(scs_inference,[],[65,14455,14480,8114,154,105,87,114,88,100,99,77,131,98,73,113,95])).
% 62.23/62.23 cnf(14524,plain,
% 62.23/62.23 (P1(a1,f17(a9,a9))),
% 62.23/62.23 inference(scs_inference,[],[65,14455,14480,14478,8114,154,105,87,114,88,100,99,77,131,98,73,113,95,71,104])).
% 62.23/62.23 cnf(14532,plain,
% 62.23/62.23 (P3(a10,x145321,f24(a2))),
% 62.23/62.23 inference(rename_variables,[],[14432])).
% 62.23/62.23 cnf(14537,plain,
% 62.23/62.23 (~P1(x145371,f3(x145372,f24(a2)))),
% 62.23/62.23 inference(rename_variables,[],[14414])).
% 62.23/62.23 cnf(14539,plain,
% 62.23/62.23 (~E(f27(a2),f24(a2))),
% 62.23/62.23 inference(scs_inference,[],[65,14472,14451,14432,14455,14480,14414,14478,14391,8114,14335,146,154,105,87,114,88,100,99,77,131,98,73,113,95,71,104,96,89,56,139,90,108,47])).
% 62.23/62.23 cnf(14546,plain,
% 62.23/62.23 (P4(f16(a10,a1,a9),a10,a9)),
% 62.23/62.23 inference(scs_inference,[],[65,14472,14451,14432,14455,14480,14414,14537,14478,14391,14348,8114,14335,159,146,154,105,87,114,88,100,99,77,131,98,73,113,95,71,104,96,89,56,139,90,108,47,83,106,138])).
% 62.23/62.23 cnf(14548,plain,
% 62.23/62.23 (~P7(a10,f26(x145481,f24(a2)))),
% 62.23/62.23 inference(scs_inference,[],[65,14472,14451,14432,14532,14455,14480,14414,14537,14426,14478,14391,14348,8114,14335,159,146,154,105,87,114,88,100,99,77,131,98,73,113,95,71,104,96,89,56,139,90,108,47,83,106,138,140])).
% 62.23/62.23 cnf(14581,plain,
% 62.23/62.23 (P1(a2,f23(x145811))),
% 62.23/62.23 inference(scs_inference,[],[14357,14498,151,105,87,114,88,100,99,131,77])).
% 62.23/62.23 cnf(14587,plain,
% 62.23/62.23 (~P3(a10,a1,f3(x145871,a9))),
% 62.23/62.23 inference(scs_inference,[],[14539,14357,14498,151,105,87,114,88,100,99,131,77,98,73,113])).
% 62.23/62.23 cnf(14589,plain,
% 62.23/62.23 (P3(a10,a1,f17(a8,a8))),
% 62.23/62.23 inference(scs_inference,[],[14539,14357,14498,151,105,87,114,88,100,99,131,77,98,73,113,95])).
% 62.23/62.23 cnf(14599,plain,
% 62.23/62.23 (P1(a1,f21(a9,a10,a9))),
% 62.23/62.23 inference(scs_inference,[],[65,14520,14539,14357,14498,2969,151,105,87,114,88,100,99,131,77,98,73,113,95,141,104,96,89,139])).
% 62.23/62.23 cnf(14608,plain,
% 62.23/62.23 (~P3(a10,a9,a1)),
% 62.23/62.24 inference(scs_inference,[],[65,14520,14539,14357,14498,14402,2969,67,151,161,154,105,87,114,88,100,99,131,77,98,73,113,95,141,104,96,89,139,90,83,106,140])).
% 62.23/62.24 cnf(14610,plain,
% 62.23/62.24 (~E(a9,f3(x146101,a9))),
% 62.23/62.24 inference(scs_inference,[],[65,14520,14539,14357,14498,14402,2969,67,151,161,154,105,87,114,88,100,99,131,77,98,73,113,95,141,104,96,89,139,90,83,106,140,8116])).
% 62.23/62.24 cnf(14611,plain,
% 62.23/62.24 (~E(a1,f3(x146111,a9))),
% 62.23/62.24 inference(scs_inference,[],[65,14520,14539,14357,14498,14402,2969,67,151,161,154,105,87,114,88,100,99,131,77,98,73,113,95,141,104,96,89,139,90,83,106,140,8116,289])).
% 62.23/62.24 cnf(14617,plain,
% 62.23/62.24 (P1(f11(a9,f3(x146171,a9)),a9)),
% 62.23/62.24 inference(scs_inference,[],[65,14520,14539,14357,14498,14402,2969,67,151,161,154,105,87,114,88,100,99,131,77,98,73,113,95,141,104,96,89,139,90,83,106,140,8116,289,605,80,92,81])).
% 62.23/62.24 cnf(14619,plain,
% 62.23/62.24 (~P1(f11(a9,f3(x146191,a9)),f3(x146191,a9))),
% 62.23/62.24 inference(scs_inference,[],[65,14520,14539,14357,14498,14402,2969,67,151,161,154,105,87,114,88,100,99,131,77,98,73,113,95,141,104,96,89,139,90,83,106,140,8116,289,605,80,92,81,101])).
% 62.23/62.24 cnf(14637,plain,
% 62.23/62.24 (~P1(x146371,f17(a2,x146372))),
% 62.23/62.24 inference(scs_inference,[],[14474,14524,14619,68,105,114,87,88,99])).
% 62.23/62.24 cnf(14639,plain,
% 62.23/62.24 (~P1(x146391,f3(a2,x146392))),
% 62.23/62.24 inference(scs_inference,[],[14474,14524,14619,68,105,114,87,88,99,100])).
% 62.23/62.24 cnf(14641,plain,
% 62.23/62.24 (~P1(x146411,f17(x146412,a2))),
% 62.23/62.24 inference(scs_inference,[],[14474,14524,14619,68,105,114,87,88,99,100,98])).
% 62.23/62.24 cnf(14643,plain,
% 62.23/62.24 (P1(f27(a2),f23(x146431))),
% 62.23/62.24 inference(scs_inference,[],[14474,14524,14619,181,68,105,114,87,88,99,100,98,77])).
% 62.23/62.24 cnf(14645,plain,
% 62.23/62.24 (~P1(x146451,f21(x146452,x146453,a2))),
% 62.23/62.24 inference(scs_inference,[],[14474,14524,14619,181,68,105,114,87,88,99,100,98,77,131])).
% 62.23/62.24 cnf(14651,plain,
% 62.23/62.24 (P3(a10,a9,f13(a9,a8))),
% 62.23/62.24 inference(scs_inference,[],[14474,14524,14610,14619,181,68,105,114,87,88,99,100,98,77,131,73,113,95])).
% 62.23/62.24 cnf(14653,plain,
% 62.23/62.24 (~P1(a9,f21(a1,a10,x146531))),
% 62.23/62.24 inference(scs_inference,[],[14608,14474,14524,14610,14619,181,68,105,114,87,88,99,100,98,77,131,73,113,95,141])).
% 62.23/62.24 cnf(14657,plain,
% 62.23/62.24 (~P1(x146571,f24(f23(x146572)))),
% 62.23/62.24 inference(scs_inference,[],[14608,14474,14524,14581,14610,14619,181,68,105,114,87,88,99,100,98,77,131,73,113,95,141,104,91])).
% 62.23/62.24 cnf(14659,plain,
% 62.23/62.24 (P8(f11(a9,f3(x146591,a9)),a9)),
% 62.23/62.24 inference(scs_inference,[],[14608,14474,14524,14581,14610,14619,14617,181,66,68,105,114,87,88,99,100,98,77,131,73,113,95,141,104,91,82])).
% 62.23/62.24 cnf(14678,plain,
% 62.23/62.24 (~E(f3(x146781,a9),a9)),
% 62.23/62.24 inference(scs_inference,[],[65,14608,14474,14524,14581,14610,14589,14619,14512,14514,14617,181,154,66,68,105,114,87,88,99,100,98,77,131,73,113,95,141,104,91,82,96,89,139,90,110,83,106,366])).
% 62.23/62.24 cnf(14688,plain,
% 62.23/62.24 (P1(x146881,f24(f21(x146882,x146883,a2)))),
% 62.23/62.24 inference(scs_inference,[],[14645,85])).
% 62.23/62.24 cnf(14689,plain,
% 62.23/62.24 (~P1(x146891,f21(x146892,x146893,a2))),
% 62.23/62.24 inference(rename_variables,[],[14645])).
% 62.23/62.24 cnf(14693,plain,
% 62.23/62.24 (~P1(x146931,f27(f21(x146932,x146933,a2)))),
% 62.23/62.24 inference(scs_inference,[],[14420,14645,14689,85,105,93])).
% 62.23/62.24 cnf(14694,plain,
% 62.23/62.24 (~P1(x146941,f21(x146942,x146943,a2))),
% 62.23/62.24 inference(rename_variables,[],[14645])).
% 62.23/62.24 cnf(14704,plain,
% 62.23/62.24 (~P1(x147041,f17(f21(x147042,x147043,a2),x147044))),
% 62.23/62.24 inference(scs_inference,[],[14420,14645,14689,14694,85,105,93,87,114,88,100,99])).
% 62.23/62.24 cnf(14708,plain,
% 62.23/62.24 (P1(f11(a9,f3(x147081,a9)),f23(a9))),
% 62.23/62.24 inference(scs_inference,[],[14420,14645,14689,14694,14659,85,105,93,87,114,88,100,99,131,77])).
% 62.23/62.24 cnf(14710,plain,
% 62.23/62.24 (~P1(x147101,f17(x147102,f21(x147103,x147104,a2)))),
% 62.23/62.24 inference(scs_inference,[],[14420,14645,14689,14694,14659,85,105,93,87,114,88,100,99,131,77,98])).
% 62.23/62.24 cnf(14714,plain,
% 62.23/62.24 (P3(a10,f16(a10,a9,a1),f23(a1))),
% 62.23/62.24 inference(scs_inference,[],[14420,14645,14689,14694,14611,14659,85,105,93,87,114,88,100,99,131,77,98,73,95])).
% 62.23/62.24 cnf(14716,plain,
% 62.23/62.24 (~P3(a10,x147161,f21(x147162,x147163,a2))),
% 62.23/62.24 inference(scs_inference,[],[14420,14645,14689,14694,14611,14659,85,105,93,87,114,88,100,99,131,77,98,73,95,113])).
% 62.23/62.24 cnf(14718,plain,
% 62.23/62.24 (~P1(x147181,f21(f21(x147182,x147183,a2),a10,x147184))),
% 62.23/62.24 inference(scs_inference,[],[14420,14645,14689,14694,14611,14659,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141])).
% 62.23/62.24 cnf(14726,plain,
% 62.23/62.24 (~P1(x147261,f21(x147262,x147263,a2))),
% 62.23/62.24 inference(rename_variables,[],[14645])).
% 62.23/62.24 cnf(14728,plain,
% 62.23/62.24 (P1(a9,f27(a9))),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14611,14659,14339,67,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89])).
% 62.23/62.24 cnf(14735,plain,
% 62.23/62.24 (~P1(x147351,f21(x147352,x147353,a2))),
% 62.23/62.24 inference(rename_variables,[],[14645])).
% 62.23/62.24 cnf(14738,plain,
% 62.23/62.24 (P7(x147381,f17(a2,a2))),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14726,14637,14641,14510,14611,14651,14659,14339,67,2758,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89,139,90,107,109])).
% 62.23/62.24 cnf(14747,plain,
% 62.23/62.24 (~P1(x147471,f21(x147472,x147473,a2))),
% 62.23/62.24 inference(rename_variables,[],[14645])).
% 62.23/62.24 cnf(14749,plain,
% 62.23/62.24 (~P1(x147491,f26(f21(x147492,x147493,a2),f21(x147492,x147493,a2)))),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14726,14735,14747,14637,14639,14641,14510,14611,14651,14659,14414,14339,67,2758,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89,139,90,107,109,111,83,106])).
% 62.23/62.24 cnf(14751,plain,
% 62.23/62.24 (~E(f3(x147511,a9),a1)),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14726,14735,14747,14637,14639,14641,14510,14611,14651,14659,14414,14339,67,2758,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89,139,90,107,109,111,83,106,383])).
% 62.23/62.24 cnf(14754,plain,
% 62.23/62.24 (~E(a9,f21(x147541,x147542,a2))),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14726,14735,14747,14637,14639,14641,14510,14611,14651,14659,14414,14339,67,2758,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89,139,90,107,109,111,83,106,383,1477,8116])).
% 62.23/62.24 cnf(14755,plain,
% 62.23/62.24 (~E(a1,f21(x147551,x147552,a2))),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14726,14735,14747,14637,14639,14641,14510,14611,14651,14659,14414,14339,67,2758,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89,139,90,107,109,111,83,106,383,1477,8116,289])).
% 62.23/62.24 cnf(14759,plain,
% 62.23/62.24 (P1(a9,f13(a9,a9))),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14726,14735,14747,14637,14639,14641,14510,14611,14651,14659,14414,14339,67,2758,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89,139,90,107,109,111,83,106,383,1477,8116,289,605,80,92])).
% 62.23/62.24 cnf(14761,plain,
% 62.23/62.24 (P1(f11(a9,f21(x147611,x147612,a2)),a9)),
% 62.23/62.24 inference(scs_inference,[],[65,14420,14645,14689,14694,14726,14735,14747,14637,14639,14641,14510,14611,14651,14659,14414,14339,67,2758,85,105,93,87,114,88,100,99,131,77,98,73,95,113,141,104,91,96,89,139,90,107,109,111,83,106,383,1477,8116,289,605,80,92,81])).
% 62.23/62.24 cnf(14768,plain,
% 62.23/62.24 (P1(x147681,f24(f17(a2,x147682)))),
% 62.23/62.24 inference(scs_inference,[],[14637,85])).
% 62.23/62.24 cnf(14769,plain,
% 62.23/62.24 (~P1(x147691,f17(a2,x147692))),
% 62.23/62.24 inference(rename_variables,[],[14637])).
% 62.23/62.24 cnf(14771,plain,
% 62.23/62.24 (~P1(x147711,f27(f17(a2,x147712)))),
% 62.23/62.24 inference(scs_inference,[],[14637,14769,85,93])).
% 62.23/62.24 cnf(14788,plain,
% 62.23/62.24 (P1(f27(f27(a2)),f23(x147881))),
% 62.23/62.24 inference(scs_inference,[],[14323,14653,14637,14769,214,85,93,105,87,114,88,99,100,131,77])).
% 62.23/62.24 cnf(14794,plain,
% 62.23/62.24 (P3(a10,a1,f23(a1))),
% 62.23/62.24 inference(scs_inference,[],[14323,14754,14653,14637,14769,214,85,93,105,87,114,88,99,100,131,77,73,98,95])).
% 62.23/62.24 cnf(14801,plain,
% 62.23/62.24 (~P1(x148011,f24(f23(x148012)))),
% 62.23/62.24 inference(rename_variables,[],[14657])).
% 62.23/62.24 cnf(14808,plain,
% 62.23/62.24 (P1(a1,f21(a8,a10,a9))),
% 62.23/62.24 inference(scs_inference,[],[65,14323,14728,14754,14653,14657,14342,14637,14769,214,85,93,105,87,114,88,99,100,131,77,73,98,95,113,141,48,104,96,89,139])).
% 62.23/62.24 cnf(14813,plain,
% 62.23/62.24 (~P1(x148131,f21(x148132,x148133,a2))),
% 62.23/62.24 inference(rename_variables,[],[14645])).
% 62.23/62.24 cnf(14822,plain,
% 62.23/62.24 (~P7(a10,f24(f21(x148221,x148222,a2)))),
% 62.23/62.24 inference(scs_inference,[],[65,14323,14728,14754,14653,14657,14801,14688,14718,14342,14645,14813,14637,14769,14432,214,85,93,105,87,114,88,99,100,131,77,73,98,95,113,141,48,104,96,89,139,90,112,83,106,140])).
% 62.23/62.24 cnf(14827,plain,
% 62.23/62.24 (~E(f27(a2),f24(f21(x148271,x148272,a2)))),
% 62.23/62.24 inference(scs_inference,[],[65,14323,14728,14754,14653,14657,14801,14688,14718,14342,14645,14813,14637,14769,14432,214,85,93,105,87,114,88,99,100,131,77,73,98,95,113,141,48,104,96,89,139,90,112,83,106,140,253])).
% 62.23/62.24 cnf(14828,plain,
% 62.23/62.24 (~E(f21(x148281,x148282,a2),a9)),
% 62.23/62.24 inference(scs_inference,[],[65,14323,14728,14754,14653,14657,14801,14688,14718,14342,14645,14813,14637,14769,14432,214,85,93,105,87,114,88,99,100,131,77,73,98,95,113,141,48,104,96,89,139,90,112,83,106,140,253,366])).
% 62.23/62.24 cnf(14838,plain,
% 62.23/62.24 (P1(x148381,f24(f3(a2,x148382)))),
% 62.23/62.24 inference(scs_inference,[],[14639,85])).
% 62.23/62.24 cnf(14839,plain,
% 62.23/62.24 (~P1(x148391,f3(a2,x148392))),
% 62.23/62.24 inference(rename_variables,[],[14639])).
% 62.23/62.24 cnf(14844,plain,
% 62.23/62.24 (~P1(x148441,f3(a2,x148442))),
% 62.23/62.24 inference(rename_variables,[],[14639])).
% 62.23/62.24 cnf(14846,plain,
% 62.23/62.24 (P1(f27(a2),f26(x148461,f23(x148462)))),
% 62.23/62.24 inference(scs_inference,[],[14759,14643,14639,14839,85,105,93,87])).
% 62.23/62.24 cnf(14852,plain,
% 62.23/62.24 (~P1(x148521,f3(f3(a2,x148522),x148523))),
% 62.23/62.24 inference(scs_inference,[],[14759,14643,14436,14639,14839,14844,85,105,93,87,114,88,100])).
% 62.23/62.24 cnf(14858,plain,
% 62.23/62.24 (P1(f21(f27(a2),a10,x148581),f23(x148582))),
% 62.23/62.24 inference(scs_inference,[],[14759,14643,14436,14639,14839,14844,2759,85,105,93,87,114,88,100,99,131,77])).
% 62.23/62.24 cnf(14860,plain,
% 62.23/62.24 (~P1(x148601,f17(x148602,f3(a2,x148603)))),
% 62.23/62.24 inference(scs_inference,[],[14759,14643,14436,14639,14839,14844,2759,85,105,93,87,114,88,100,99,131,77,98])).
% 62.23/62.24 cnf(14864,plain,
% 62.23/62.24 (P3(a10,a9,f13(a9,a9))),
% 62.23/62.24 inference(scs_inference,[],[14759,14643,14755,14436,14639,14839,14844,2759,85,105,93,87,114,88,100,99,131,77,98,73,95])).
% 62.23/62.24 cnf(14878,plain,
% 62.23/62.24 (~E(f23(a1),f21(x148781,x148782,a2))),
% 62.23/62.24 inference(scs_inference,[],[65,14759,14643,14714,14755,14794,14436,14761,14716,14639,14839,14844,176,2759,85,105,93,87,114,88,100,99,131,77,98,73,95,113,104,72,89,139,90,51])).
% 62.23/62.24 cnf(14880,plain,
% 62.23/62.24 (~P8(f26(f24(a2),x148801),f22(a1))),
% 62.23/62.24 inference(scs_inference,[],[65,14759,14643,14714,14755,14794,14436,14430,14761,14716,14639,14839,14844,176,2759,85,105,93,87,114,88,100,99,131,77,98,73,95,113,104,72,89,139,90,51,83])).
% 62.23/62.24 cnf(14888,plain,
% 62.23/62.24 (~E(f21(x148881,x148882,a2),a1)),
% 62.23/62.24 inference(scs_inference,[],[65,14759,14643,14714,14755,14794,14436,14430,14827,14761,14716,14639,14839,14844,14472,176,2759,2764,85,105,93,87,114,88,100,99,131,77,98,73,95,113,104,72,89,139,90,51,83,129,140,383])).
% 62.23/62.24 cnf(14891,plain,
% 62.23/62.24 (~P1(a1,f21(a1,a10,x148911))),
% 62.23/62.24 inference(scs_inference,[],[65,14759,14643,14714,14755,14794,14436,14430,14827,14761,14716,14639,14839,14844,14472,176,2759,2764,85,105,93,87,114,88,100,99,131,77,98,73,95,113,104,72,89,139,90,51,83,129,140,383,92,141])).
% 62.23/62.24 cnf(14901,plain,
% 62.23/62.24 (P1(x149011,f24(f17(x149012,a2)))),
% 62.23/62.24 inference(scs_inference,[],[14880,14641,334,355,85])).
% 62.23/62.24 cnf(14902,plain,
% 62.23/62.24 (~P1(x149021,f17(x149022,a2))),
% 62.23/62.24 inference(rename_variables,[],[14641])).
% 62.23/62.24 cnf(14905,plain,
% 62.23/62.24 (~P1(x149051,f17(x149052,a2))),
% 62.23/62.24 inference(rename_variables,[],[14641])).
% 62.23/62.24 cnf(14920,plain,
% 62.23/62.24 (P1(a9,f23(a1))),
% 62.23/62.24 inference(scs_inference,[],[14808,14891,14880,14641,14902,159,334,355,85,93,605,105,87,114,88,99,131,77])).
% 62.23/62.24 cnf(14928,plain,
% 62.23/62.24 (P3(a10,a1,f21(a8,a10,a9))),
% 62.23/62.24 inference(scs_inference,[],[14878,14808,14891,14880,14641,14902,159,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95])).
% 62.23/62.24 cnf(14930,plain,
% 62.23/62.24 (~P3(a10,a1,f21(a1,a10,x149301))),
% 62.23/62.24 inference(scs_inference,[],[14878,14808,14891,14880,14641,14902,159,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113])).
% 62.23/62.24 cnf(14938,plain,
% 62.23/62.24 (P1(a1,f27(a1))),
% 62.23/62.24 inference(scs_inference,[],[65,14878,14808,14891,14880,14641,14902,159,161,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113,141,104,96,89])).
% 62.23/62.24 cnf(14947,plain,
% 62.23/62.24 (~P1(x149471,f17(x149472,a2))),
% 62.23/62.24 inference(rename_variables,[],[14641])).
% 62.23/62.24 cnf(14950,plain,
% 62.23/62.24 (~E(f21(x149501,x149502,a2),f23(a1))),
% 62.23/62.24 inference(scs_inference,[],[65,14878,14808,14891,14880,14704,14822,14641,14902,14905,14738,14589,159,146,161,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113,141,104,96,89,56,139,90,108,47])).
% 62.23/62.24 cnf(14952,plain,
% 62.23/62.24 (~P8(a9,f21(a1,a10,x149521))),
% 62.23/62.24 inference(scs_inference,[],[65,14878,14808,14891,14880,14704,14822,14641,14902,14905,14738,14589,159,146,161,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113,141,104,96,89,56,139,90,108,47,83])).
% 62.23/62.24 cnf(14964,plain,
% 62.23/62.24 (~E(a1,f21(a1,a10,x149641))),
% 62.23/62.24 inference(scs_inference,[],[65,14878,14808,14751,14891,14587,14880,14704,14768,14822,14641,14902,14905,14947,14738,14589,159,146,161,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113,141,104,96,89,56,139,90,108,47,83,106,129,1477,8116,289])).
% 62.23/62.24 cnf(14967,plain,
% 62.23/62.24 (P1(a1,f13(a1,a1))),
% 62.23/62.24 inference(scs_inference,[],[65,14878,14808,14751,14891,14587,14880,14704,14768,14822,14641,14902,14905,14947,14738,14589,159,146,161,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113,141,104,96,89,56,139,90,108,47,83,106,129,1477,8116,289,80,92])).
% 62.23/62.24 cnf(14969,plain,
% 62.23/62.24 (P1(f11(a9,f21(a1,a10,x149691)),a9)),
% 62.23/62.24 inference(scs_inference,[],[65,14878,14808,14751,14891,14587,14880,14704,14768,14822,14641,14902,14905,14947,14738,14589,159,146,161,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113,141,104,96,89,56,139,90,108,47,83,106,129,1477,8116,289,80,92,81])).
% 62.23/62.24 cnf(14971,plain,
% 62.23/62.24 (~P1(f11(a9,f21(a1,a10,x149711)),f21(a1,a10,x149711))),
% 62.23/62.24 inference(scs_inference,[],[65,14878,14808,14751,14891,14587,14880,14704,14768,14822,14641,14902,14905,14947,14738,14589,159,146,161,334,355,85,93,605,105,87,114,88,99,131,77,100,73,98,95,113,141,104,96,89,56,139,90,108,47,83,106,129,1477,8116,289,80,92,81,101])).
% 62.23/62.24 cnf(14988,plain,
% 62.23/62.24 (~P1(x149881,f17(f17(a2,x149882),x149883))),
% 62.23/62.24 inference(scs_inference,[],[14325,14952,14971,14637,105,605,87,114,88,99])).
% 62.23/62.24 cnf(14996,plain,
% 62.23/62.24 (~P1(x149961,f17(x149962,f17(a2,x149963)))),
% 62.23/62.24 inference(scs_inference,[],[14950,14325,14952,14971,14637,105,605,87,114,88,99,100,131,73,98])).
% 62.23/62.24 cnf(14998,plain,
% 62.23/62.24 (P3(a10,a1,f26(x149981,a8))),
% 62.23/62.24 inference(scs_inference,[],[14950,14325,14952,14971,14637,105,605,87,114,88,99,100,131,73,98,95])).
% 62.23/62.24 cnf(15014,plain,
% 62.23/62.24 (~P8(f24(f3(a2,x150141)),f21(a1,a10,x150142))),
% 62.23/62.24 inference(scs_inference,[],[14546,14950,14325,14952,14864,14920,14971,14838,14969,2762,14637,2969,66,105,605,87,114,88,99,100,131,73,98,95,113,54,104,82,89,139,90,83])).
% 62.23/62.24 cnf(15035,plain,
% 62.23/62.24 (~P1(x150351,f17(f17(x150352,a2),x150353))),
% 62.23/62.24 inference(scs_inference,[],[14967,14327,15014,14381,14641,334,355,105,87,114,88,99])).
% 62.23/62.24 cnf(15037,plain,
% 62.23/62.24 (~P1(f21(x150371,x150372,a2),f22(a9))),
% 62.23/62.24 inference(scs_inference,[],[14967,14828,14327,15014,14381,14641,334,355,105,87,114,88,99,73])).
% 62.23/62.24 cnf(15041,plain,
% 62.23/62.24 (~P1(x150411,f3(f17(x150412,a2),x150413))),
% 62.23/62.24 inference(scs_inference,[],[14967,14828,14327,15014,14381,14641,334,355,105,87,114,88,99,73,131,100])).
% 62.23/62.24 cnf(15045,plain,
% 62.23/62.24 (P3(a10,a1,f13(a1,a1))),
% 62.23/62.24 inference(scs_inference,[],[14967,14828,14327,15014,14381,14641,334,355,105,87,114,88,99,73,131,100,98,95])).
% 62.23/62.24 cnf(15053,plain,
% 62.23/62.24 (~P1(f21(x150531,x150532,a2),f25(a9,a9))),
% 62.23/62.24 inference(scs_inference,[],[65,14967,14828,14327,14928,15014,14381,14641,334,355,105,87,114,88,99,73,131,100,98,95,113,104,139,90])).
% 62.23/62.24 cnf(15084,plain,
% 62.23/62.24 (~P1(f21(x150841,x150842,a2),f22(a1))),
% 62.23/62.24 inference(scs_inference,[],[15053,14888,14500,105,87,88,114,131,73])).
% 62.23/62.24 cnf(15092,plain,
% 62.23/62.24 (P3(a10,a1,f26(x150921,a9))),
% 62.23/62.24 inference(scs_inference,[],[15053,14888,14500,105,87,88,114,131,73,99,100,98,95])).
% 62.23/62.24 cnf(15105,plain,
% 62.23/62.24 (~P1(f21(x151051,x151052,a2),f25(a1,a1))),
% 62.23/62.24 inference(scs_inference,[],[65,15053,14888,14500,15045,14339,105,87,88,114,131,73,99,100,98,95,113,141,104,96,139,90])).
% 62.23/62.24 cnf(15116,plain,
% 62.23/62.24 (~P1(f21(x151161,x151162,a2),f25(a9,a9))),
% 62.23/62.24 inference(rename_variables,[],[15053])).
% 62.23/62.24 cnf(15124,plain,
% 62.23/62.24 (~E(a2,f23(x151241))),
% 62.23/62.24 inference(scs_inference,[],[65,15053,15116,14888,14500,15045,14858,14710,14988,14637,14339,14641,105,87,88,114,131,73,99,100,98,95,113,141,104,96,139,90,111,109,83,106,384,345,334])).
% 62.23/62.24 cnf(15126,plain,
% 62.23/62.24 (~E(f27(a2),f23(x151261))),
% 62.23/62.24 inference(scs_inference,[],[65,15053,15116,14888,14500,15045,14858,14710,14988,14637,14339,14641,105,87,88,114,131,73,99,100,98,95,113,141,104,96,139,90,111,109,83,106,384,345,334,2788,355])).
% 62.23/62.24 cnf(15127,plain,
% 62.23/62.24 (~P1(f23(x151271),f23(f25(a9,a9)))),
% 62.23/62.24 inference(scs_inference,[],[65,15053,15116,14888,14500,15045,14858,14710,14988,14637,14339,14641,105,87,88,114,131,73,99,100,98,95,113,141,104,96,139,90,111,109,83,106,384,345,334,2788,355,80])).
% 62.23/62.24 cnf(15130,plain,
% 62.23/62.24 (P1(f11(f23(x151301),f25(a9,a9)),f23(x151301))),
% 62.23/62.24 inference(scs_inference,[],[65,15053,15116,14888,14500,15045,14858,14710,14988,14637,14339,14641,105,87,88,114,131,73,99,100,98,95,113,141,104,96,139,90,111,109,83,106,384,345,334,2788,355,80,605,81])).
% 62.23/62.24 cnf(15158,plain,
% 62.23/62.24 (P3(a10,a1,f26(a9,x151581))),
% 62.23/62.24 inference(scs_inference,[],[15105,15126,14504,105,87,114,88,73,99,131,100,98,95])).
% 62.23/62.24 cnf(15186,plain,
% 62.23/62.24 (~E(f23(x151861),f27(a2))),
% 62.23/62.24 inference(scs_inference,[],[65,15105,15126,14504,14998,14749,14860,15035,14639,14637,14641,105,87,114,88,73,99,131,100,98,95,113,141,83,104,106,96,139,90,107,112,366])).
% 62.23/62.24 cnf(15195,plain,
% 62.23/62.24 (~P1(a9,f3(x151951,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,105])).
% 62.23/62.24 cnf(15197,plain,
% 62.23/62.24 (P1(a9,f26(x151971,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,105,87])).
% 62.23/62.24 cnf(15213,plain,
% 62.23/62.24 (P3(a10,a9,a8)),
% 62.23/62.24 inference(scs_inference,[],[66,15186,15037,14449,105,87,88,114,99,131,73,100,98,95])).
% 62.23/62.24 cnf(15219,plain,
% 62.23/62.24 (~E(f26(x152191,a9),f21(a1,a10,x152192))),
% 62.23/62.24 inference(scs_inference,[],[66,15186,15037,14449,15092,14930,105,87,88,114,99,131,73,100,98,95,113,141,51])).
% 62.23/62.24 cnf(15223,plain,
% 62.23/62.24 (P1(a9,f17(a8,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,15186,15037,14449,15092,14901,14930,105,87,88,114,99,131,73,100,98,95,113,141,51,83,104])).
% 62.23/62.24 cnf(15265,plain,
% 62.23/62.24 (P3(a10,a9,f17(a8,a8))),
% 62.23/62.24 inference(scs_inference,[],[15219,15223,15195,105,87,114,88,131,73,99,100,98,95])).
% 62.23/62.24 cnf(15284,plain,
% 62.23/62.24 (P1(a9,f21(a8,a10,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,15213,15219,15223,15195,14548,14617,14402,146,105,87,114,88,131,73,99,100,98,95,113,141,47,83,104,106,96,89,56,139])).
% 62.23/62.24 cnf(15296,plain,
% 62.23/62.24 (~E(a2,f17(a8,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,15213,15219,15223,15195,14487,14484,14996,14548,14430,14617,14402,14637,146,105,87,114,88,131,73,99,100,98,95,113,141,47,83,104,106,96,89,56,139,90,108,129,345,334])).
% 62.23/62.24 cnf(15298,plain,
% 62.23/62.24 (~E(f27(a2),f17(a8,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,15213,15219,15223,15195,14487,14484,14996,14548,14430,14617,14402,14637,146,105,87,114,88,131,73,99,100,98,95,113,141,47,83,104,106,96,89,56,139,90,108,129,345,334,2788,355])).
% 62.23/62.24 cnf(15303,plain,
% 62.23/62.24 (~P1(f11(f17(a8,a8),f3(x153031,a8)),f3(x153031,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,15213,15219,15223,15195,14487,14484,14996,14548,14430,14617,14402,14637,146,105,87,114,88,131,73,99,100,98,95,113,141,47,83,104,106,96,89,56,139,90,108,129,345,334,2788,355,80,81,101])).
% 62.23/62.24 cnf(15346,plain,
% 62.23/62.24 (~E(f17(a8,a8),f27(a2))),
% 62.23/62.24 inference(scs_inference,[],[66,15298,15284,15265,15303,14852,14846,15084,14761,2764,105,87,88,114,73,99,131,100,98,95,113,83,104,89,139,90,129,366])).
% 62.23/62.24 cnf(15362,plain,
% 62.23/62.24 (P3(a10,a9,f26(x153621,a8))),
% 62.23/62.24 inference(scs_inference,[],[15346,15197,15127,105,114,87,88,73,95])).
% 62.23/62.24 cnf(15414,plain,
% 62.23/62.24 (P1(a1,f27(a8))),
% 62.23/62.24 inference(scs_inference,[],[66,15296,15130,15041,14938,65,105,114,88,87,73,113,95,83,104,89])).
% 62.23/62.24 cnf(15424,plain,
% 62.23/62.24 (~E(f17(a8,a8),a2)),
% 62.23/62.24 inference(scs_inference,[],[66,15296,15362,15130,15041,14508,14938,14641,65,105,114,88,87,73,113,95,83,104,89,139,90,111,383])).
% 62.23/62.24 cnf(15427,plain,
% 62.23/62.24 (P1(a1,f13(a1,a8))),
% 62.23/62.24 inference(scs_inference,[],[66,15296,15362,15130,15041,14508,14938,14641,65,105,114,88,87,73,113,95,83,104,89,139,90,111,383,1477,92])).
% 62.23/62.24 cnf(15446,plain,
% 62.23/62.24 (~P1(f17(a8,a8),f22(a2))),
% 62.23/62.24 inference(scs_inference,[],[15424,15427,15414,14693,105,87,114,88,73])).
% 62.23/62.24 cnf(15450,plain,
% 62.23/62.24 (P3(a10,a1,f13(a1,a8))),
% 62.23/62.24 inference(scs_inference,[],[15424,15427,15414,14693,105,87,114,88,73,98,95])).
% 62.23/62.24 cnf(15468,plain,
% 62.23/62.24 (~P1(f17(a8,a8),f25(a2,a2))),
% 62.23/62.24 inference(scs_inference,[],[66,15424,15427,15158,15414,14693,14645,67,105,87,114,88,73,98,95,113,83,104,106,96,89,139,90])).
% 62.23/62.24 cnf(15494,plain,
% 62.23/62.24 (~P1(f17(a8,a8),f21(x154941,x154942,f25(a2,a2)))),
% 62.23/62.24 inference(scs_inference,[],[15468,14510,105,87,88,114,99,131])).
% 62.23/62.24 cnf(15553,plain,
% 62.23/62.24 (~P1(x155531,f3(a2,x155532))),
% 62.23/62.24 inference(rename_variables,[],[14639])).
% 62.23/62.24 cnf(15568,plain,
% 62.23/62.24 (~E(f23(x155681),a2)),
% 62.23/62.24 inference(scs_inference,[],[66,15446,15124,15450,14788,14506,14524,14920,14838,14548,14432,14472,14639,15553,105,87,114,88,73,113,95,83,104,106,96,56,139,90,140,366])).
% 62.23/62.24 cnf(15596,plain,
% 62.23/62.24 (~P1(f23(x155961),f26(f22(a2),f22(a2)))),
% 62.23/62.24 inference(scs_inference,[],[66,15568,14708,15494,14771,14581,105,87,88,114,73,113,95,83,104,106])).
% 62.23/62.24 cnf(15600,plain,
% 62.23/62.24 (~P1(f23(x156001),f25(a2,a2))),
% 62.23/62.24 inference(scs_inference,[],[66,15568,14708,15494,14771,14581,14864,105,87,88,114,73,113,95,83,104,106,139,90])).
% 62.23/62.24 cnf(15638,plain,
% 62.23/62.24 (~P1(f3(x156381,a9),f22(a9))),
% 62.23/62.24 inference(scs_inference,[],[15600,14678,14327,14599,105,99,87,131,114,88,100,73])).
% 62.23/62.24 cnf(15742,plain,
% 62.23/62.24 ($false),
% 62.23/62.24 inference(scs_inference,[],[67,14964,15596,15638,14608,105,99,87,131,114,88,98,100,73,113,95]),
% 62.23/62.24 ['proof']).
% 62.23/62.24 % SZS output end Proof
% 62.23/62.24 % Total time :61.560000s
%------------------------------------------------------------------------------