%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV415+1 : TPTP v8.2.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n028.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 16:47:09 EDT 2024
% Result : Theorem 1.02s 1.13s
% Output : CNFRefutation 1.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SWV415+1 : TPTP v8.2.0. Released v3.3.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu Jun 20 19:49:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 1.02/1.12 %-------------------------------------------
% 1.02/1.12 % File :CSE---1.7
% 1.02/1.12 % Problem :theBenchmark
% 1.02/1.12 % Transform :cnf
% 1.02/1.12 % Format :tptp:raw
% 1.02/1.12 % Command :java -jar mcs_scs.jar %d %s
% 1.02/1.12
% 1.02/1.12 % Result :Theorem 0.510000s
% 1.02/1.12 % Output :CNFRefutation 0.510000s
% 1.02/1.12 %-------------------------------------------
% 1.02/1.13 %--------------------------------------------------------------------------
% 1.02/1.13 % File : SWV415+1 : TPTP v8.2.0. Released v3.3.0.
% 1.02/1.13 % Domain : Software Verification
% 1.02/1.13 % Problem : Priority queue checker: Formula (7)
% 1.02/1.13 % Version : [dNP05] axioms.
% 1.02/1.13 % English :
% 1.02/1.13
% 1.02/1.13 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 1.02/1.13 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 1.02/1.13 % Source : [Pis06]
% 1.02/1.13 % Names : cpq002 [Pis06]
% 1.02/1.13
% 1.02/1.13 % Status : Theorem
% 1.02/1.13 % Rating : 0.22 v7.5.0, 0.25 v7.4.0, 0.13 v7.3.0, 0.21 v7.1.0, 0.13 v7.0.0, 0.20 v6.4.0, 0.23 v6.3.0, 0.21 v6.2.0, 0.32 v6.1.0, 0.37 v6.0.0, 0.30 v5.5.0, 0.41 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.38 v5.0.0, 0.42 v4.1.0, 0.39 v4.0.1, 0.43 v4.0.0, 0.46 v3.7.0, 0.40 v3.5.0, 0.42 v3.4.0, 0.47 v3.3.0
% 1.02/1.13 % Syntax : Number of formulae : 64 ( 25 unt; 0 def)
% 1.02/1.13 % Number of atoms : 130 ( 42 equ)
% 1.02/1.13 % Maximal formula atoms : 4 ( 2 avg)
% 1.02/1.13 % Number of connectives : 82 ( 16 ~; 4 |; 21 &)
% 1.02/1.13 % ( 16 <=>; 25 =>; 0 <=; 0 <~>)
% 1.02/1.13 % Maximal formula depth : 9 ( 5 avg)
% 1.02/1.13 % Maximal term depth : 5 ( 1 avg)
% 1.02/1.13 % Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% 1.02/1.13 % Number of functors : 26 ( 26 usr; 4 con; 0-3 aty)
% 1.02/1.13 % Number of variables : 172 ( 169 !; 3 ?)
% 1.02/1.13 % SPC : FOF_THM_RFO_SEQ
% 1.02/1.13
% 1.02/1.13 % Comments :
% 1.02/1.13 %--------------------------------------------------------------------------
% 1.02/1.13 %----Include the axioms about priority queues and checked priority queues
% 1.02/1.13 include('Axioms/SWV007+0.ax').
% 1.02/1.13 include('Axioms/SWV007+1.ax').
% 1.02/1.13 include('Axioms/SWV007+2.ax').
% 1.02/1.13 include('Axioms/SWV007+3.ax').
% 1.02/1.13 include('Axioms/SWV007+4.ax').
% 1.02/1.13 %--------------------------------------------------------------------------
% 1.02/1.13 fof(main2_l12,lemma,
% 1.02/1.13 ! [U,V,W,X,Y] : i(triple(U,W,X)) = i(triple(V,W,Y)) ).
% 1.02/1.13
% 1.02/1.13 fof(co2,conjecture,
% 1.02/1.13 ! [U,V,W,X] : i(insert_cpq(triple(U,V,W),X)) = insert_pq(i(triple(U,V,W)),X) ).
% 1.02/1.13
% 1.02/1.13 %--------------------------------------------------------------------------
% 1.02/1.13 %-------------------------------------------
% 1.02/1.13 % Proof found
% 1.02/1.13 % SZS status Theorem for theBenchmark
% 1.02/1.13 % SZS output start Proof
% 1.02/1.13 %ClaNum:163(EqnAxiom:77)
% 1.02/1.13 %VarNum:469(SingletonVarNum:225)
% 1.02/1.13 %MaxLitNum:4
% 1.02/1.13 %MaxfuncDepth:4
% 1.02/1.13 %SharedTerms:16
% 1.02/1.13 %goalClause: 101
% 1.02/1.13 %singleGoalClaCount:1
% 1.02/1.13 [95]~P2(a4)
% 1.02/1.13 [96]~P7(a1)
% 1.02/1.13 [101]~E(f17(f21(f30(a9,a14,a15),a16)),f6(f17(f30(a9,a14,a15)),a16))
% 1.02/1.13 [79]P1(a2,x791)
% 1.02/1.13 [80]P1(x801,x801)
% 1.02/1.13 [81]P9(x811,x811)
% 1.02/1.13 [97]~P4(a4,x971)
% 1.02/1.13 [98]~P6(a1,x981)
% 1.02/1.13 [78]E(f5(a1,x781),a1)
% 1.02/1.13 [99]~P10(a1,x991,x992)
% 1.02/1.13 [82]P2(f6(x821,x822))
% 1.02/1.13 [90]P3(f30(x901,a1,x902))
% 1.02/1.13 [100]~P11(f30(x1001,x1002,a3))
% 1.02/1.13 [83]E(f22(f6(x831,x832),x832),x831)
% 1.02/1.13 [88]E(f7(f30(x881,a1,x882)),a2)
% 1.02/1.13 [89]E(f17(f30(x891,a1,x892)),a4)
% 1.02/1.13 [91]E(f8(f30(x911,a1,x912)),f30(x911,a1,a3))
% 1.02/1.13 [84]E(f6(f6(x841,x842),x843),f6(f6(x841,x843),x842))
% 1.02/1.13 [85]P7(f24(x851,f23(x852,x853)))
% 1.02/1.13 [86]E(f28(f24(x861,f23(x862,x863)),x862),x861)
% 1.02/1.13 [87]E(f26(f24(x871,f23(x872,x873)),x872),x873)
% 1.02/1.13 [93]E(f30(f25(x931,x932),f24(x933,f23(x932,a2)),x934),f21(f30(x931,x933,x934),x932))
% 1.02/1.13 [92]E(f17(f30(x921,x922,x923)),f17(f30(x924,x922,x925)))
% 1.02/1.13 [94]E(f17(f30(x941,f24(x942,f23(x943,x944)),x945)),f6(f17(f30(x941,x942,x945)),x943))
% 1.02/1.13 [102]~P12(x1021)+P3(f10(x1021))
% 1.02/1.13 [103]~P12(x1031)+P11(f10(x1031))
% 1.02/1.13 [104]~P12(x1041)+P9(x1041,f10(x1041))
% 1.02/1.13 [106]~P14(x1061)+P13(f17(x1061),f11(x1061))
% 1.02/1.13 [107]~P15(x1071)+P13(f17(x1071),f13(x1071))
% 1.02/1.13 [105]P1(x1052,x1051)+P1(x1051,x1052)
% 1.02/1.13 [110]~P17(x1101,x1102)+P1(x1101,x1102)
% 1.02/1.13 [111]~P18(x1111,x1112)+P4(x1111,x1112)
% 1.02/1.13 [112]~P13(x1121,x1122)+P4(x1121,x1122)
% 1.02/1.13 [113]~P19(x1131,x1132)+P4(x1131,x1132)
% 1.02/1.13 [114]~P13(x1141,x1142)+P8(x1141,x1142)
% 1.02/1.13 [115]~P19(x1151,x1152)+P8(x1151,x1152)
% 1.02/1.13 [116]~P4(x1161,x1162)+P18(x1161,x1162)
% 1.02/1.13 [121]~P17(x1212,x1211)+~P1(x1211,x1212)
% 1.02/1.13 [108]P14(x1081)+~P13(f17(x1081),x1082)
% 1.02/1.13 [109]P15(x1091)+~P13(f17(x1091),x1092)
% 1.02/1.13 [118]~P9(x1181,x1182)+P9(x1181,f8(x1182))
% 1.02/1.13 [119]~P16(x1191,x1192)+P18(f17(x1191),x1192)
% 1.02/1.13 [122]P16(x1221,x1222)+~P18(f17(x1221),x1222)
% 1.02/1.13 [124]P8(x1241,x1242)+P4(x1241,f12(x1241,x1242))
% 1.02/1.13 [136]P8(x1361,x1362)+~P1(x1362,f12(x1361,x1362))
% 1.02/1.13 [138]~P9(x1381,x1382)+P9(x1381,f27(f8(x1382),f7(x1382)))
% 1.02/1.13 [120]~E(x1202,x1203)+P4(f6(x1201,x1202),x1203)
% 1.02/1.13 [132]~P9(x1321,x1322)+P9(x1321,f21(x1322,x1323))
% 1.02/1.13 [133]~P9(x1331,x1332)+P9(x1331,f27(x1332,x1333))
% 1.02/1.13 [134]~P4(x1341,x1343)+P4(f6(x1341,x1342),x1343)
% 1.02/1.13 [141]E(x1411,a3)+P11(f30(x1412,x1413,x1411))
% 1.02/1.13 [143]E(x1431,a1)+E(f7(f30(x1432,x1431,x1433)),f20(x1432))
% 1.02/1.13 [146]~P6(x1462,x1464)+P5(f30(x1461,x1462,x1463),x1464)
% 1.02/1.13 [152]P6(x1521,x1522)+~P5(f30(x1523,x1521,x1524),x1522)
% 1.02/1.13 [139]~E(x1392,x1394)+P6(f24(x1391,f23(x1392,x1393)),x1394)
% 1.02/1.13 [142]~P6(x1421,x1424)+P6(f24(x1421,f23(x1422,x1423)),x1424)
% 1.02/1.13 [151]P6(x1512,x1514)+E(f27(f30(x1511,x1512,x1513),x1514),f30(x1511,x1512,a3))
% 1.02/1.13 [148]~P1(x1482,x1484)+E(f24(f5(x1481,x1482),f23(x1483,x1484)),f5(f24(x1481,f23(x1483,x1484)),x1482))
% 1.02/1.13 [149]~P17(x1493,x1494)+E(f5(f24(x1491,f23(x1492,x1493)),x1494),f24(f5(x1491,x1494),f23(x1492,x1494)))
% 1.02/1.13 [153]~P10(x1531,x1534,x1535)+P10(f24(x1531,f23(x1532,x1533)),x1534,x1535)
% 1.02/1.13 [161]~P17(x1611,x1612)+~P3(f30(x1613,f24(x1614,f23(x1611,x1612)),x1615))
% 1.02/1.13 [123]P17(x1232,x1231)+~P1(x1232,x1231)+P1(x1231,x1232)
% 1.02/1.13 [127]~P4(x1271,x1272)+~P8(x1271,x1272)+P13(x1271,x1272)
% 1.02/1.13 [128]~P4(x1281,x1282)+~P8(x1281,x1282)+P19(x1281,x1282)
% 1.02/1.13 [129]~P4(x1291,x1292)+~P8(x1291,x1292)+E(f18(x1291,x1292),x1291)
% 1.02/1.13 [130]~P4(x1301,x1302)+~P8(x1301,x1302)+E(f19(x1301,x1302),x1302)
% 1.02/1.13 [131]~P4(x1311,x1312)+~P8(x1311,x1312)+E(f31(x1311,x1312),x1312)
% 1.02/1.13 [135]~P4(x1351,x1352)+~P8(x1351,x1352)+E(f32(x1351,x1352),f22(x1351,x1352))
% 1.02/1.13 [125]~P8(x1253,x1251)+P1(x1251,x1252)+~P4(x1253,x1252)
% 1.02/1.13 [126]~P1(x1261,x1263)+P1(x1261,x1262)+~P1(x1263,x1262)
% 1.02/1.13 [137]E(x1371,x1372)+P4(x1373,x1372)+~P4(f6(x1373,x1371),x1372)
% 1.02/1.13 [140]~P4(x1403,x1401)+E(x1401,x1402)+E(f22(f6(x1403,x1402),x1401),f6(f22(x1403,x1401),x1402))
% 1.02/1.13 [154]P6(x1541,f20(x1542))+E(x1541,a1)+E(f8(f30(x1542,x1541,x1543)),f30(x1542,f5(x1541,f20(x1542)),a3))
% 1.02/1.13 [147]E(x1471,x1472)+P6(x1473,x1472)+~P6(f24(x1473,f23(x1471,x1474)),x1472)
% 1.02/1.13 [157]~P6(x1572,x1574)+~P17(x1574,f26(x1572,x1574))+E(f27(f30(x1571,x1572,x1573),x1574),f30(f29(x1571,x1574),f28(x1572,x1574),a3))
% 1.02/1.13 [158]~P6(x1583,x1582)+~P1(f26(x1583,x1582),x1582)+E(f30(f29(x1581,x1582),f28(x1583,x1582),x1584),f27(f30(x1581,x1583,x1584),x1582))
% 1.02/1.13 [144]~P6(x1443,x1442)+E(x1441,x1442)+E(f26(f24(x1443,f23(x1441,x1444)),x1442),f26(x1443,x1442))
% 1.02/1.13 [150]~P6(x1503,x1502)+E(x1501,x1502)+E(f28(f24(x1503,f23(x1501,x1504)),x1502),f24(f28(x1503,x1502),f23(x1501,x1504)))
% 1.02/1.13 [145]~E(x1453,x1455)+~E(x1452,x1454)+P10(f24(x1451,f23(x1452,x1453)),x1454,x1455)
% 1.02/1.13 [155]E(x1551,x1552)+P10(x1553,x1554,x1552)+~P10(f24(x1553,f23(x1555,x1551)),x1554,x1552)
% 1.02/1.13 [156]E(x1561,x1562)+P10(x1563,x1562,x1564)+~P10(f24(x1563,f23(x1561,x1565)),x1562,x1564)
% 1.02/1.13 [162]~P1(x1624,x1623)+~P3(f30(x1621,x1622,x1625))+P3(f30(x1621,f24(x1622,f23(x1623,x1624)),x1625))
% 1.02/1.13 [163]~P1(x1634,x1635)+P3(f30(x1631,x1632,x1633))+~P3(f30(x1631,f24(x1632,f23(x1635,x1634)),x1633))
% 1.02/1.13 [117]~P11(x1172)+~P9(x1171,x1172)+P12(x1171)+~P3(x1172)
% 1.02/1.13 [159]~P6(x1591,f20(x1592))+E(x1591,a1)+~P17(f20(x1592),f26(x1591,f20(x1592)))+E(f8(f30(x1592,x1591,x1593)),f30(x1592,f5(x1591,f20(x1592)),a3))
% 1.02/1.13 [160]~P6(x1601,f20(x1602))+E(x1601,a1)+~P1(f26(x1601,f20(x1602)),f20(x1602))+E(f30(x1602,f5(x1601,f20(x1602)),x1603),f8(f30(x1602,x1601,x1603)))
% 1.02/1.13 %EqnAxiom
% 1.02/1.13 [1]E(x11,x11)
% 1.02/1.13 [2]E(x22,x21)+~E(x21,x22)
% 1.02/1.14 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.02/1.14 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 1.02/1.14 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 1.02/1.14 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 1.02/1.14 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 1.02/1.14 [8]~E(x81,x82)+E(f23(x81,x83),f23(x82,x83))
% 1.02/1.14 [9]~E(x91,x92)+E(f23(x93,x91),f23(x93,x92))
% 1.02/1.14 [10]~E(x101,x102)+E(f22(x101,x103),f22(x102,x103))
% 1.02/1.14 [11]~E(x111,x112)+E(f22(x113,x111),f22(x113,x112))
% 1.02/1.14 [12]~E(x121,x122)+E(f30(x121,x123,x124),f30(x122,x123,x124))
% 1.02/1.14 [13]~E(x131,x132)+E(f30(x133,x131,x134),f30(x133,x132,x134))
% 1.02/1.14 [14]~E(x141,x142)+E(f30(x143,x144,x141),f30(x143,x144,x142))
% 1.02/1.14 [15]~E(x151,x152)+E(f24(x151,x153),f24(x152,x153))
% 1.02/1.14 [16]~E(x161,x162)+E(f24(x163,x161),f24(x163,x162))
% 1.02/1.14 [17]~E(x171,x172)+E(f20(x171),f20(x172))
% 1.02/1.14 [18]~E(x181,x182)+E(f8(x181),f8(x182))
% 1.02/1.14 [19]~E(x191,x192)+E(f26(x191,x193),f26(x192,x193))
% 1.02/1.14 [20]~E(x201,x202)+E(f26(x203,x201),f26(x203,x202))
% 1.02/1.14 [21]~E(x211,x212)+E(f17(x211),f17(x212))
% 1.02/1.14 [22]~E(x221,x222)+E(f7(x221),f7(x222))
% 1.02/1.14 [23]~E(x231,x232)+E(f10(x231),f10(x232))
% 1.02/1.14 [24]~E(x241,x242)+E(f28(x241,x243),f28(x242,x243))
% 1.02/1.14 [25]~E(x251,x252)+E(f28(x253,x251),f28(x253,x252))
% 1.02/1.14 [26]~E(x261,x262)+E(f12(x261,x263),f12(x262,x263))
% 1.02/1.14 [27]~E(x271,x272)+E(f12(x273,x271),f12(x273,x272))
% 1.02/1.14 [28]~E(x281,x282)+E(f27(x281,x283),f27(x282,x283))
% 1.02/1.14 [29]~E(x291,x292)+E(f27(x293,x291),f27(x293,x292))
% 1.02/1.14 [30]~E(x301,x302)+E(f13(x301),f13(x302))
% 1.02/1.14 [31]~E(x311,x312)+E(f18(x311,x313),f18(x312,x313))
% 1.02/1.14 [32]~E(x321,x322)+E(f18(x323,x321),f18(x323,x322))
% 1.02/1.14 [33]~E(x331,x332)+E(f11(x331),f11(x332))
% 1.02/1.14 [34]~E(x341,x342)+E(f29(x341,x343),f29(x342,x343))
% 1.02/1.14 [35]~E(x351,x352)+E(f29(x353,x351),f29(x353,x352))
% 1.02/1.14 [36]~E(x361,x362)+E(f21(x361,x363),f21(x362,x363))
% 1.02/1.14 [37]~E(x371,x372)+E(f21(x373,x371),f21(x373,x372))
% 1.02/1.14 [38]~E(x381,x382)+E(f19(x381,x383),f19(x382,x383))
% 1.02/1.14 [39]~E(x391,x392)+E(f19(x393,x391),f19(x393,x392))
% 1.02/1.14 [40]~E(x401,x402)+E(f32(x401,x403),f32(x402,x403))
% 1.02/1.14 [41]~E(x411,x412)+E(f32(x413,x411),f32(x413,x412))
% 1.02/1.14 [42]~E(x421,x422)+E(f25(x421,x423),f25(x422,x423))
% 1.02/1.14 [43]~E(x431,x432)+E(f25(x433,x431),f25(x433,x432))
% 1.02/1.14 [44]~E(x441,x442)+E(f31(x441,x443),f31(x442,x443))
% 1.02/1.14 [45]~E(x451,x452)+E(f31(x453,x451),f31(x453,x452))
% 1.02/1.14 [46]P1(x462,x463)+~E(x461,x462)+~P1(x461,x463)
% 1.02/1.14 [47]P1(x473,x472)+~E(x471,x472)+~P1(x473,x471)
% 1.02/1.14 [48]~P3(x481)+P3(x482)+~E(x481,x482)
% 1.02/1.14 [49]P9(x492,x493)+~E(x491,x492)+~P9(x491,x493)
% 1.02/1.14 [50]P9(x503,x502)+~E(x501,x502)+~P9(x503,x501)
% 1.02/1.14 [51]~P2(x511)+P2(x512)+~E(x511,x512)
% 1.02/1.14 [52]~P7(x521)+P7(x522)+~E(x521,x522)
% 1.02/1.14 [53]P10(x532,x533,x534)+~E(x531,x532)+~P10(x531,x533,x534)
% 1.02/1.14 [54]P10(x543,x542,x544)+~E(x541,x542)+~P10(x543,x541,x544)
% 1.02/1.14 [55]P10(x553,x554,x552)+~E(x551,x552)+~P10(x553,x554,x551)
% 1.02/1.14 [56]P6(x562,x563)+~E(x561,x562)+~P6(x561,x563)
% 1.02/1.14 [57]P6(x573,x572)+~E(x571,x572)+~P6(x573,x571)
% 1.02/1.14 [58]P4(x582,x583)+~E(x581,x582)+~P4(x581,x583)
% 1.02/1.14 [59]P4(x593,x592)+~E(x591,x592)+~P4(x593,x591)
% 1.02/1.14 [60]P8(x602,x603)+~E(x601,x602)+~P8(x601,x603)
% 1.02/1.14 [61]P8(x613,x612)+~E(x611,x612)+~P8(x613,x611)
% 1.02/1.14 [62]P17(x622,x623)+~E(x621,x622)+~P17(x621,x623)
% 1.02/1.14 [63]P17(x633,x632)+~E(x631,x632)+~P17(x633,x631)
% 1.02/1.14 [64]P18(x642,x643)+~E(x641,x642)+~P18(x641,x643)
% 1.02/1.14 [65]P18(x653,x652)+~E(x651,x652)+~P18(x653,x651)
% 1.02/1.14 [66]~P11(x661)+P11(x662)+~E(x661,x662)
% 1.02/1.14 [67]P16(x672,x673)+~E(x671,x672)+~P16(x671,x673)
% 1.02/1.14 [68]P16(x683,x682)+~E(x681,x682)+~P16(x683,x681)
% 1.02/1.14 [69]~P12(x691)+P12(x692)+~E(x691,x692)
% 1.02/1.14 [70]P19(x702,x703)+~E(x701,x702)+~P19(x701,x703)
% 1.02/1.14 [71]P19(x713,x712)+~E(x711,x712)+~P19(x713,x711)
% 1.02/1.14 [72]P5(x722,x723)+~E(x721,x722)+~P5(x721,x723)
% 1.02/1.14 [73]P5(x733,x732)+~E(x731,x732)+~P5(x733,x731)
% 1.02/1.14 [74]P13(x742,x743)+~E(x741,x742)+~P13(x741,x743)
% 1.02/1.14 [75]P13(x753,x752)+~E(x751,x752)+~P13(x753,x751)
% 1.02/1.14 [76]~P15(x761)+P15(x762)+~E(x761,x762)
% 1.02/1.14 [77]~P14(x771)+P14(x772)+~E(x771,x772)
% 1.02/1.14
% 1.02/1.14 %-------------------------------------------
% 1.02/1.14 cnf(164,plain,
% 1.02/1.14 (P4(f6(x1642,x1641),x1641)),
% 1.02/1.14 inference(equality_inference,[],[120])).
% 1.02/1.14 cnf(165,plain,
% 1.02/1.14 (P6(f24(x1652,f23(x1651,x1653)),x1651)),
% 1.02/1.14 inference(equality_inference,[],[139])).
% 1.02/1.14 cnf(166,plain,
% 1.02/1.14 (E(x1661,f22(f6(x1661,x1662),x1662))),
% 1.02/1.14 inference(scs_inference,[],[83,2])).
% 1.02/1.14 cnf(175,plain,
% 1.02/1.14 (P8(a4,x1751)),
% 1.02/1.14 inference(scs_inference,[],[80,97,83,2,111,112,113,121,124])).
% 1.02/1.14 cnf(176,plain,
% 1.02/1.14 (~P4(a4,x1761)),
% 1.02/1.14 inference(rename_variables,[],[97])).
% 1.02/1.14 cnf(178,plain,
% 1.02/1.14 (P8(x1781,a2)),
% 1.02/1.14 inference(scs_inference,[],[80,79,97,83,2,111,112,113,121,124,136])).
% 1.02/1.14 cnf(181,plain,
% 1.02/1.14 (E(f22(f6(f5(a1,x1811),x1812),x1812),a1)),
% 1.02/1.14 inference(scs_inference,[],[80,79,97,83,78,2,111,112,113,121,124,136,3])).
% 1.02/1.14 cnf(182,plain,
% 1.02/1.14 (E(f22(f6(x1821,x1822),x1822),x1821)),
% 1.02/1.14 inference(rename_variables,[],[83])).
% 1.02/1.14 cnf(183,plain,
% 1.02/1.14 (P1(x1831,f22(f6(x1831,x1832),x1832))),
% 1.02/1.14 inference(scs_inference,[],[80,79,97,83,182,78,2,111,112,113,121,124,136,3,46])).
% 1.02/1.14 cnf(184,plain,
% 1.02/1.14 (P1(x1841,x1841)),
% 1.02/1.14 inference(rename_variables,[],[80])).
% 1.02/1.14 cnf(185,plain,
% 1.02/1.14 (P1(f22(f6(x1851,x1852),x1852),x1851)),
% 1.02/1.14 inference(scs_inference,[],[80,184,79,97,83,182,78,2,111,112,113,121,124,136,3,46,47])).
% 1.02/1.14 cnf(187,plain,
% 1.02/1.14 (P9(x1871,f22(f6(x1871,x1872),x1872))),
% 1.02/1.14 inference(scs_inference,[],[80,184,81,79,97,83,182,78,2,111,112,113,121,124,136,3,46,47,49])).
% 1.02/1.14 cnf(188,plain,
% 1.02/1.14 (P9(x1881,x1881)),
% 1.02/1.14 inference(rename_variables,[],[81])).
% 1.02/1.14 cnf(189,plain,
% 1.02/1.14 (P9(f22(f6(x1891,x1892),x1892),x1891)),
% 1.02/1.14 inference(scs_inference,[],[80,184,81,188,79,97,83,182,78,2,111,112,113,121,124,136,3,46,47,49,50])).
% 1.02/1.14 cnf(191,plain,
% 1.02/1.14 (~P2(f22(f6(a4,x1911),x1911))),
% 1.02/1.14 inference(scs_inference,[],[80,184,81,188,79,97,95,83,182,78,2,111,112,113,121,124,136,3,46,47,49,50,51])).
% 1.02/1.14 cnf(192,plain,
% 1.02/1.14 (E(f22(f6(x1921,x1922),x1922),x1921)),
% 1.02/1.14 inference(rename_variables,[],[83])).
% 1.02/1.14 cnf(193,plain,
% 1.02/1.14 (~P7(f22(f6(a1,x1931),x1931))),
% 1.02/1.14 inference(scs_inference,[],[80,184,81,188,79,97,95,96,83,182,192,78,2,111,112,113,121,124,136,3,46,47,49,50,51,52])).
% 1.02/1.14 cnf(194,plain,
% 1.02/1.14 (E(f22(f6(x1941,x1942),x1942),x1941)),
% 1.02/1.14 inference(rename_variables,[],[83])).
% 1.02/1.14 cnf(195,plain,
% 1.02/1.14 (~E(f24(x1951,f23(x1952,x1953)),a1)),
% 1.02/1.14 inference(scs_inference,[],[165,80,184,81,188,79,97,98,95,96,83,182,192,78,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56])).
% 1.02/1.14 cnf(196,plain,
% 1.02/1.14 (P6(f24(x1961,f23(x1962,x1963)),x1962)),
% 1.02/1.14 inference(rename_variables,[],[165])).
% 1.02/1.14 cnf(197,plain,
% 1.02/1.14 (P6(f24(x1971,f23(f22(f6(x1972,x1973),x1973),x1974)),x1972)),
% 1.02/1.14 inference(scs_inference,[],[165,196,80,184,81,188,79,97,98,95,96,83,182,192,194,78,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56,57])).
% 1.02/1.14 cnf(200,plain,
% 1.02/1.14 (P4(f6(x2001,x2002),x2002)),
% 1.02/1.14 inference(rename_variables,[],[164])).
% 1.02/1.14 cnf(201,plain,
% 1.02/1.14 (P4(f6(x2011,f22(f6(x2012,x2013),x2013)),x2012)),
% 1.02/1.14 inference(scs_inference,[],[164,200,165,196,80,184,81,188,79,97,176,98,95,96,83,182,192,194,78,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56,57,58,59])).
% 1.02/1.14 cnf(202,plain,
% 1.02/1.14 (P4(f6(x2021,x2022),x2022)),
% 1.02/1.14 inference(rename_variables,[],[164])).
% 1.02/1.14 cnf(203,plain,
% 1.02/1.14 (~P11(f22(f6(f30(x2031,x2032,a3),x2033),x2033))),
% 1.02/1.14 inference(scs_inference,[],[164,200,165,196,80,184,81,188,79,97,176,98,95,96,83,182,192,194,78,100,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56,57,58,59,66])).
% 1.02/1.14 cnf(204,plain,
% 1.02/1.14 (E(f22(f6(x2041,x2042),x2042),x2041)),
% 1.02/1.14 inference(rename_variables,[],[83])).
% 1.02/1.14 cnf(205,plain,
% 1.02/1.14 (P13(f6(x2051,a2),a2)),
% 1.02/1.14 inference(scs_inference,[],[164,200,202,165,196,80,184,81,188,79,97,176,98,95,96,83,182,192,194,78,100,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56,57,58,59,66,127])).
% 1.02/1.14 cnf(206,plain,
% 1.02/1.14 (P4(f6(x2061,x2062),x2062)),
% 1.02/1.14 inference(rename_variables,[],[164])).
% 1.02/1.14 cnf(208,plain,
% 1.02/1.14 (P19(f6(x2081,a2),a2)),
% 1.02/1.14 inference(scs_inference,[],[164,200,202,206,165,196,80,184,81,188,79,97,176,98,95,96,83,182,192,194,78,100,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56,57,58,59,66,127,128])).
% 1.02/1.14 cnf(212,plain,
% 1.02/1.14 (P19(f6(f6(x2121,a2),x2122),a2)),
% 1.02/1.14 inference(scs_inference,[],[164,200,202,206,165,196,80,184,81,188,79,97,176,98,95,96,83,182,192,194,204,84,78,100,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56,57,58,59,66,127,128,48,70])).
% 1.02/1.14 cnf(213,plain,
% 1.02/1.14 (E(f6(f6(x2131,x2132),x2133),f6(f6(x2131,x2133),x2132))),
% 1.02/1.14 inference(rename_variables,[],[84])).
% 1.02/1.14 cnf(214,plain,
% 1.02/1.14 (P13(f6(f6(x2141,a2),x2142),a2)),
% 1.02/1.14 inference(scs_inference,[],[164,200,202,206,165,196,80,184,81,188,79,97,176,98,95,96,83,182,192,194,204,84,213,78,100,2,111,112,113,121,124,136,3,46,47,49,50,51,52,56,57,58,59,66,127,128,48,70,74])).
% 1.02/1.14 cnf(223,plain,
% 1.02/1.14 (E(a1,f22(f6(f5(a1,x2231),x2232),x2232))),
% 1.02/1.14 inference(scs_inference,[],[181,183,121,2])).
% 1.02/1.14 cnf(225,plain,
% 1.02/1.14 (P1(x2251,f22(f6(x2251,x2252),x2252))),
% 1.02/1.14 inference(rename_variables,[],[183])).
% 1.02/1.14 cnf(228,plain,
% 1.02/1.14 (E(x2281,f22(f6(x2281,x2282),x2282))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(229,plain,
% 1.02/1.14 (P4(f6(x2291,f22(f6(x2292,x2293),x2293)),f22(f6(x2292,x2294),x2294))),
% 1.02/1.14 inference(scs_inference,[],[166,228,181,183,185,201,214,121,2,126,75,59])).
% 1.02/1.14 cnf(231,plain,
% 1.02/1.14 (P1(f22(f6(f22(f6(x2311,x2312),x2312),x2313),x2313),x2311)),
% 1.02/1.14 inference(scs_inference,[],[166,228,181,183,185,201,214,121,2,126,75,59,46])).
% 1.02/1.14 cnf(232,plain,
% 1.02/1.14 (E(x2321,f22(f6(x2321,x2322),x2322))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(233,plain,
% 1.02/1.14 (P1(x2331,f22(f6(f22(f6(x2331,x2332),x2332),x2333),x2333))),
% 1.02/1.14 inference(scs_inference,[],[166,228,232,181,183,225,185,201,214,121,2,126,75,59,46,47])).
% 1.02/1.14 cnf(234,plain,
% 1.02/1.14 (E(x2341,f22(f6(x2341,x2342),x2342))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(235,plain,
% 1.02/1.14 (P7(f22(f6(f24(x2351,f23(x2352,x2353)),x2354),x2354))),
% 1.02/1.14 inference(scs_inference,[],[166,228,232,234,181,183,225,185,201,214,85,121,2,126,75,59,46,47,52])).
% 1.02/1.14 cnf(236,plain,
% 1.02/1.14 (E(x2361,f22(f6(x2361,x2362),x2362))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(237,plain,
% 1.02/1.14 (E(f22(f6(f5(a1,x2371),x2372),x2372),f22(f6(a1,x2373),x2373))),
% 1.02/1.14 inference(scs_inference,[],[166,228,232,234,236,181,183,225,185,201,214,85,121,2,126,75,59,46,47,52,3])).
% 1.02/1.14 cnf(238,plain,
% 1.02/1.14 (E(x2381,f22(f6(x2381,x2382),x2382))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(243,plain,
% 1.02/1.14 (E(x2431,f22(f6(x2431,x2432),x2432))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(245,plain,
% 1.02/1.14 (E(x2451,f22(f6(x2451,x2452),x2452))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(249,plain,
% 1.02/1.14 (E(x2491,f22(f6(x2491,x2492),x2492))),
% 1.02/1.14 inference(rename_variables,[],[166])).
% 1.02/1.14 cnf(250,plain,
% 1.02/1.14 (P8(x2501,f22(f6(a2,x2502),x2502))),
% 1.02/1.14 inference(scs_inference,[],[166,228,232,234,236,238,243,245,249,181,183,225,185,187,201,197,212,214,178,90,91,85,100,121,2,126,75,59,46,47,52,3,66,48,50,57,71,61])).
% 1.02/1.14 cnf(272,plain,
% 1.02/1.14 (E(f22(f6(a1,x2721),x2721),f22(f6(f5(a1,x2722),x2723),x2723))),
% 1.02/1.14 inference(scs_inference,[],[237,185,121,2])).
% 1.02/1.14 cnf(273,plain,
% 1.02/1.14 (E(f22(f6(x2731,x2732),x2732),f22(f6(x2731,x2733),x2733))),
% 1.02/1.14 inference(scs_inference,[],[237,185,229,97,121,2,137])).
% 1.02/1.14 cnf(288,plain,
% 1.02/1.14 (~P11(f28(f24(f22(f6(f30(x2881,x2882,a3),x2883),x2883),f23(x2884,x2885)),x2884))),
% 1.02/1.14 inference(scs_inference,[],[237,223,166,181,164,185,229,233,203,250,97,205,86,121,2,137,125,126,59,75,3,66])).
% 1.02/1.14 cnf(290,plain,
% 1.02/1.14 (~P7(f22(f6(f5(a1,x2901),x2902),x2902))),
% 1.02/1.14 inference(scs_inference,[],[237,223,166,181,164,185,229,233,203,250,193,97,205,86,121,2,137,125,126,59,75,3,66,52])).
% 1.02/1.14 cnf(291,plain,
% 1.02/1.14 (E(f22(f6(f5(a1,x2911),x2912),x2912),f22(f6(a1,x2913),x2913))),
% 1.02/1.14 inference(rename_variables,[],[237])).
% 1.02/1.14 cnf(292,plain,
% 1.02/1.14 (P1(f5(a1,x2921),f22(f6(a1,x2922),x2922))),
% 1.02/1.14 inference(scs_inference,[],[237,291,223,166,181,164,185,229,233,203,250,193,183,97,205,86,121,2,137,125,126,59,75,3,66,52,47])).
% 1.02/1.14 cnf(296,plain,
% 1.02/1.14 (P1(f22(f6(a1,x2961),x2961),f5(a1,x2962))),
% 1.02/1.14 inference(scs_inference,[],[237,291,223,166,181,164,185,189,229,233,203,250,193,183,97,205,86,121,2,137,125,126,59,75,3,66,52,47,49,46])).
% 1.02/1.14 cnf(320,plain,
% 1.02/1.14 (E(x3201,f26(f24(x3202,f23(x3203,x3201)),x3203))),
% 1.02/1.14 inference(scs_inference,[],[231,87,121,2])).
% 1.02/1.14 cnf(321,plain,
% 1.02/1.14 (P1(f22(f6(f22(f6(a1,x3211),x3211),x3212),x3212),f5(a1,x3213))),
% 1.02/1.14 inference(scs_inference,[],[185,231,296,87,121,2,126])).
% 1.02/1.14 cnf(322,plain,
% 1.02/1.14 (P1(f22(f6(x3221,x3222),x3222),x3221)),
% 1.02/1.14 inference(rename_variables,[],[185])).
% 1.02/1.14 cnf(327,plain,
% 1.02/1.14 (E(f22(f6(x3271,x3272),x3272),f22(f6(f22(f6(x3271,x3273),x3273),x3274),x3274))),
% 1.02/1.14 inference(scs_inference,[],[273,166,185,231,288,296,87,96,78,86,121,2,126,66,52,3])).
% 1.02/1.14 cnf(333,plain,
% 1.02/1.14 (P1(f22(f6(f22(f6(x3331,x3332),x3332),x3333),x3333),f22(f6(x3331,x3334),x3334))),
% 1.02/1.14 inference(scs_inference,[],[273,166,185,322,231,288,191,296,187,87,96,78,86,121,2,126,66,52,3,51,49,47])).
% 1.02/1.14 cnf(347,plain,
% 1.02/1.14 (E(f22(f6(f22(f6(x3471,x3472),x3472),x3473),x3473),f22(f6(x3471,x3474),x3474))),
% 1.02/1.14 inference(scs_inference,[],[327,296,121,2])).
% 1.02/1.14 cnf(351,plain,
% 1.02/1.14 (P8(x3511,f26(f24(x3512,f23(x3513,a2)),x3513))),
% 1.02/1.14 inference(scs_inference,[],[320,327,231,296,79,178,121,2,126,61])).
% 1.02/1.14 cnf(352,plain,
% 1.02/1.14 (E(x3521,f26(f24(x3522,f23(x3523,x3521)),x3523))),
% 1.02/1.14 inference(rename_variables,[],[320])).
% 1.02/1.14 cnf(354,plain,
% 1.02/1.14 (E(x3541,f26(f24(x3542,f23(x3543,x3541)),x3543))),
% 1.02/1.14 inference(rename_variables,[],[320])).
% 1.02/1.14 cnf(356,plain,
% 1.02/1.14 (E(x3561,f26(f24(x3562,f23(x3563,x3561)),x3563))),
% 1.02/1.15 inference(rename_variables,[],[320])).
% 1.02/1.15 cnf(357,plain,
% 1.02/1.15 (P8(f26(f24(x3571,f23(x3572,a4)),x3572),x3573)),
% 1.02/1.15 inference(scs_inference,[],[320,352,354,356,327,212,214,231,296,175,79,178,121,2,126,61,75,71,60])).
% 1.02/1.15 cnf(358,plain,
% 1.02/1.15 (E(x3581,f26(f24(x3582,f23(x3583,x3581)),x3583))),
% 1.02/1.15 inference(rename_variables,[],[320])).
% 1.02/1.15 cnf(359,plain,
% 1.02/1.15 (~P7(f28(f24(f22(f6(f5(a1,x3591),x3592),x3592),f23(x3593,x3594)),x3593))),
% 1.02/1.15 inference(scs_inference,[],[320,352,354,356,327,212,214,231,296,290,175,79,178,86,121,2,126,61,75,71,60,52])).
% 1.02/1.15 cnf(362,plain,
% 1.02/1.15 (P1(f22(f6(a1,x3621),x3621),f26(f24(x3622,f23(x3623,f5(a1,x3624))),x3623))),
% 1.02/1.15 inference(scs_inference,[],[320,352,354,356,358,327,212,214,231,296,290,203,175,79,178,86,121,2,126,61,75,71,60,52,66,47])).
% 1.02/1.15 cnf(363,plain,
% 1.02/1.15 (E(x3631,f26(f24(x3632,f23(x3633,x3631)),x3633))),
% 1.02/1.15 inference(rename_variables,[],[320])).
% 1.02/1.15 cnf(365,plain,
% 1.02/1.15 (~E(f24(x3651,f23(x3652,x3653)),f22(f6(f5(a1,x3654),x3655),x3655))),
% 1.02/1.15 inference(scs_inference,[],[320,352,354,356,358,327,181,212,214,231,296,290,195,203,175,79,178,89,95,86,121,2,126,61,75,71,60,52,66,47,51,3])).
% 1.02/1.15 cnf(366,plain,
% 1.02/1.15 (P1(f26(f24(x3661,f23(x3662,f5(a1,x3663))),x3662),f22(f6(a1,x3664),x3664))),
% 1.02/1.15 inference(scs_inference,[],[320,352,354,356,358,363,327,181,212,214,231,296,292,290,195,203,175,79,178,89,95,86,121,2,126,61,75,71,60,52,66,47,51,3,46])).
% 1.02/1.15 cnf(382,plain,
% 1.02/1.15 (E(f21(f30(x3821,x3822,x3823),x3824),f30(f25(x3821,x3824),f24(x3822,f23(x3824,a2)),x3823))),
% 1.02/1.15 inference(scs_inference,[],[292,93,121,2])).
% 1.02/1.15 cnf(386,plain,
% 1.02/1.15 (P13(f6(x3861,a2),f26(f24(x3862,f23(x3863,a2)),x3863))),
% 1.02/1.15 inference(scs_inference,[],[320,185,292,205,93,121,2,126,75])).
% 1.02/1.15 cnf(387,plain,
% 1.02/1.15 (E(x3871,f26(f24(x3872,f23(x3873,x3871)),x3873))),
% 1.02/1.15 inference(rename_variables,[],[320])).
% 1.02/1.15 cnf(388,plain,
% 1.02/1.15 (P19(f6(x3881,a2),f26(f24(x3882,f23(x3883,a2)),x3883))),
% 1.02/1.15 inference(scs_inference,[],[320,387,185,292,205,208,93,121,2,126,75,71])).
% 1.02/1.15 cnf(389,plain,
% 1.02/1.15 (E(x3891,f26(f24(x3892,f23(x3893,x3891)),x3893))),
% 1.02/1.15 inference(rename_variables,[],[320])).
% 1.02/1.15 cnf(394,plain,
% 1.02/1.15 (P1(f5(a1,x3941),f26(f24(x3942,f23(x3943,a1)),x3943))),
% 1.02/1.15 inference(scs_inference,[],[347,320,387,389,185,292,290,205,208,93,100,121,2,126,75,71,52,66,47])).
% 1.02/1.15 cnf(395,plain,
% 1.02/1.15 (E(x3951,f26(f24(x3952,f23(x3953,x3951)),x3953))),
% 1.02/1.15 inference(rename_variables,[],[320])).
% 1.02/1.15 cnf(398,plain,
% 1.02/1.15 (P1(f26(f24(x3981,f23(x3982,a2)),x3982),x3983)),
% 1.02/1.15 inference(scs_inference,[],[347,365,272,320,387,389,395,185,292,290,205,208,79,93,100,121,2,126,75,71,52,66,47,3,46])).
% 1.02/1.15 cnf(411,plain,
% 1.02/1.15 (E(a4,f17(f30(x4111,a1,x4112)))),
% 1.02/1.15 inference(scs_inference,[],[333,89,121,2])).
% 1.02/1.15 cnf(416,plain,
% 1.02/1.15 (E(x4161,f22(f6(x4161,x4162),x4162))),
% 1.02/1.15 inference(rename_variables,[],[166])).
% 1.02/1.15 cnf(418,plain,
% 1.02/1.15 (E(x4181,f22(f6(x4181,x4182),x4182))),
% 1.02/1.15 inference(rename_variables,[],[166])).
% 1.02/1.15 cnf(420,plain,
% 1.02/1.15 (E(x4201,f22(f6(x4201,x4202),x4202))),
% 1.02/1.15 inference(rename_variables,[],[166])).
% 1.02/1.15 cnf(422,plain,
% 1.02/1.15 (E(x4221,f22(f6(x4221,x4222),x4222))),
% 1.02/1.15 inference(rename_variables,[],[166])).
% 1.02/1.15 cnf(427,plain,
% 1.02/1.15 (E(f22(f6(f21(f30(x4271,x4272,x4273),x4274),x4275),x4275),f30(f25(x4271,x4274),f24(x4272,f23(x4274,a2)),x4273))),
% 1.02/1.15 inference(scs_inference,[],[166,416,418,420,422,382,351,357,185,333,296,359,398,386,388,83,89,86,121,2,126,61,60,75,71,47,52,3])).
% 1.02/1.15 cnf(442,plain,
% 1.02/1.15 (P1(f5(a1,x4421),f5(a1,x4422))),
% 1.02/1.15 inference(scs_inference,[],[427,292,296,233,121,2,126])).
% 1.02/1.15 cnf(464,plain,
% 1.02/1.15 (E(f30(x4641,a1,a3),f8(f30(x4641,a1,x4642)))),
% 1.02/1.15 inference(scs_inference,[],[398,91,121,2])).
% 1.02/1.15 cnf(470,plain,
% 1.02/1.15 (E(f22(f6(a4,x4701),x4701),f17(f30(x4702,a1,x4703)))),
% 1.02/1.15 inference(scs_inference,[],[411,292,398,362,83,91,90,121,2,126,48,3])).
% 1.02/1.15 cnf(485,plain,
% 1.02/1.15 (E(x4851,f22(f6(x4851,x4852),x4852))),
% 1.02/1.15 inference(rename_variables,[],[166])).
% 1.02/1.15 cnf(488,plain,
% 1.02/1.15 (P1(f22(f6(f5(a1,x4881),x4882),x4882),f5(a1,x4883))),
% 1.02/1.15 inference(scs_inference,[],[166,485,470,464,366,83,321,442,121,2,47,3,46])).
% 1.02/1.15 cnf(606,plain,
% 1.02/1.15 (~E(f17(f21(f30(a9,a14,a15),a16)),f17(f30(a9,f24(a14,f23(a16,x6061)),a15)))),
% 1.02/1.15 inference(scs_inference,[],[101,488,94,82,121,2,51,3])).
% 1.02/1.15 cnf(629,plain,
% 1.02/1.15 ($false),
% 1.02/1.15 inference(scs_inference,[],[382,606,394,235,92,86,121,2,52,3,21]),
% 1.02/1.15 ['proof']).
% 1.02/1.15 % SZS output end Proof
% 1.02/1.15 % Total time :0.510000s
%------------------------------------------------------------------------------