%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV365+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 : n024.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:00 EDT 2024
% Result : Theorem 0.54s 0.88s
% Output : CNFRefutation 0.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWV365+1 : TPTP v8.2.0. Released v3.3.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 20 18:06:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.58 start to proof:theBenchmark
% 0.54/0.87 %-------------------------------------------
% 0.54/0.87 % File :CSE---1.7
% 0.54/0.87 % Problem :theBenchmark
% 0.54/0.87 % Transform :cnf
% 0.54/0.87 % Format :tptp:raw
% 0.54/0.87 % Command :java -jar mcs_scs.jar %d %s
% 0.54/0.87
% 0.54/0.87 % Result :Theorem 0.240000s
% 0.54/0.87 % Output :CNFRefutation 0.240000s
% 0.54/0.87 %-------------------------------------------
% 0.54/0.88 %------------------------------------------------------------------------------
% 0.54/0.88 % File : SWV365+1 : TPTP v8.2.0. Released v3.3.0.
% 0.54/0.88 % Domain : Software Verification
% 0.54/0.88 % Problem : Priority queue checker: lemma_I_s base
% 0.54/0.88 % Version : [dNP05] axioms.
% 0.54/0.88 % English :
% 0.54/0.88
% 0.54/0.88 % Refs : [Pis06] Piskac (2006), Email to Geoff Sutcliffe
% 0.54/0.88 % : [dNP05] de Nivelle & Piskac (2005), Verification of an Off-Lin
% 0.54/0.88 % Source : [Pis06]
% 0.54/0.88 % Names : cpq_l001 [Pis06]
% 0.54/0.88
% 0.54/0.88 % Status : Theorem
% 0.54/0.88 % Rating : 0.11 v8.1.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.3.0, 0.14 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.28 v6.1.0, 0.23 v6.0.0, 0.13 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.26 v5.2.0, 0.10 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.25 v3.7.0, 0.20 v3.5.0, 0.21 v3.4.0, 0.26 v3.3.0
% 0.54/0.88 % Syntax : Number of formulae : 63 ( 24 unt; 0 def)
% 0.54/0.88 % Number of atoms : 129 ( 41 equ)
% 0.54/0.88 % Maximal formula atoms : 4 ( 2 avg)
% 0.54/0.88 % Number of connectives : 82 ( 16 ~; 4 |; 21 &)
% 0.54/0.88 % ( 16 <=>; 25 =>; 0 <=; 0 <~>)
% 0.54/0.88 % Maximal formula depth : 9 ( 5 avg)
% 0.54/0.88 % Maximal term depth : 5 ( 1 avg)
% 0.54/0.88 % Number of predicates : 21 ( 19 usr; 1 prp; 0-3 aty)
% 0.54/0.88 % Number of functors : 26 ( 26 usr; 4 con; 0-3 aty)
% 0.54/0.88 % Number of variables : 167 ( 164 !; 3 ?)
% 0.54/0.88 % SPC : FOF_THM_RFO_SEQ
% 0.54/0.88
% 0.54/0.88 % Comments :
% 0.54/0.88 %------------------------------------------------------------------------------
% 0.54/0.88 %----Include the axioms about priority queues and checked priority queues
% 0.54/0.88 include('Axioms/SWV007+0.ax').
% 0.54/0.88 include('Axioms/SWV007+1.ax').
% 0.54/0.88 include('Axioms/SWV007+2.ax').
% 0.54/0.88 include('Axioms/SWV007+3.ax').
% 0.54/0.88 include('Axioms/SWV007+4.ax').
% 0.54/0.88 %------------------------------------------------------------------------------
% 0.54/0.88 %----goal: fof(lemma_I_s, conjecture,
% 0.54/0.88 %---- (! [U,V,W,X,Y] : (i(triple(U,W,X)) = i(triple(V,W,Y))))).
% 0.54/0.88
% 0.54/0.88 %----base:
% 0.54/0.88 fof(l1_co,conjecture,
% 0.54/0.88 ! [U,V,X,Y] : i(triple(U,create_slb,X)) = i(triple(V,create_slb,Y)) ).
% 0.54/0.88
% 0.54/0.88 %------------------------------------------------------------------------------
% 0.54/0.88 %-------------------------------------------
% 0.54/0.88 % Proof found
% 0.54/0.88 % SZS status Theorem for theBenchmark
% 0.54/0.88 % SZS output start Proof
% 0.54/0.88 %ClaNum:162(EqnAxiom:77)
% 0.54/0.88 %VarNum:463(SingletonVarNum:220)
% 0.54/0.88 %MaxLitNum:4
% 0.54/0.88 %MaxfuncDepth:4
% 0.54/0.88 %SharedTerms:15
% 0.54/0.88 %goalClause: 100
% 0.54/0.88 %singleGoalClaCount:1
% 0.54/0.88 [94]~P2(a4)
% 0.54/0.88 [95]~P7(a1)
% 0.54/0.88 [100]~E(f17(f30(a9,a1,a14)),f17(f30(a15,a1,a16)))
% 0.54/0.88 [79]P1(a2,x791)
% 0.54/0.88 [80]P1(x801,x801)
% 0.54/0.88 [81]P9(x811,x811)
% 0.54/0.88 [96]~P4(a4,x961)
% 0.54/0.88 [97]~P6(a1,x971)
% 0.54/0.88 [78]E(f5(a1,x781),a1)
% 0.54/0.88 [98]~P10(a1,x981,x982)
% 0.54/0.88 [82]P2(f6(x821,x822))
% 0.54/0.88 [90]P3(f30(x901,a1,x902))
% 0.54/0.88 [99]~P11(f30(x991,x992,a3))
% 0.54/0.88 [83]E(f22(f6(x831,x832),x832),x831)
% 0.54/0.88 [88]E(f7(f30(x881,a1,x882)),a2)
% 0.54/0.88 [89]E(f17(f30(x891,a1,x892)),a4)
% 0.54/0.88 [91]E(f8(f30(x911,a1,x912)),f30(x911,a1,a3))
% 0.54/0.88 [84]E(f6(f6(x841,x842),x843),f6(f6(x841,x843),x842))
% 0.54/0.88 [85]P7(f24(x851,f23(x852,x853)))
% 0.54/0.88 [86]E(f28(f24(x861,f23(x862,x863)),x862),x861)
% 0.54/0.88 [87]E(f26(f24(x871,f23(x872,x873)),x872),x873)
% 0.54/0.88 [92]E(f30(f25(x921,x922),f24(x923,f23(x922,a2)),x924),f21(f30(x921,x923,x924),x922))
% 0.54/0.88 [93]E(f17(f30(x931,f24(x932,f23(x933,x934)),x935)),f6(f17(f30(x931,x932,x935)),x933))
% 0.54/0.88 [101]~P12(x1011)+P3(f10(x1011))
% 0.54/0.88 [102]~P12(x1021)+P11(f10(x1021))
% 0.54/0.88 [103]~P12(x1031)+P9(x1031,f10(x1031))
% 0.54/0.88 [105]~P14(x1051)+P13(f17(x1051),f11(x1051))
% 0.54/0.88 [106]~P15(x1061)+P13(f17(x1061),f13(x1061))
% 0.54/0.88 [104]P1(x1042,x1041)+P1(x1041,x1042)
% 0.54/0.88 [109]~P17(x1091,x1092)+P1(x1091,x1092)
% 0.54/0.88 [110]~P18(x1101,x1102)+P4(x1101,x1102)
% 0.54/0.88 [111]~P13(x1111,x1112)+P4(x1111,x1112)
% 0.54/0.88 [112]~P19(x1121,x1122)+P4(x1121,x1122)
% 0.54/0.88 [113]~P13(x1131,x1132)+P8(x1131,x1132)
% 0.54/0.88 [114]~P19(x1141,x1142)+P8(x1141,x1142)
% 0.54/0.88 [115]~P4(x1151,x1152)+P18(x1151,x1152)
% 0.54/0.88 [120]~P17(x1202,x1201)+~P1(x1201,x1202)
% 0.54/0.88 [107]P14(x1071)+~P13(f17(x1071),x1072)
% 0.54/0.88 [108]P15(x1081)+~P13(f17(x1081),x1082)
% 0.54/0.88 [117]~P9(x1171,x1172)+P9(x1171,f8(x1172))
% 0.54/0.88 [118]~P16(x1181,x1182)+P18(f17(x1181),x1182)
% 0.54/0.88 [121]P16(x1211,x1212)+~P18(f17(x1211),x1212)
% 0.54/0.88 [123]P8(x1231,x1232)+P4(x1231,f12(x1231,x1232))
% 0.54/0.88 [135]P8(x1351,x1352)+~P1(x1352,f12(x1351,x1352))
% 0.54/0.88 [137]~P9(x1371,x1372)+P9(x1371,f27(f8(x1372),f7(x1372)))
% 0.54/0.88 [119]~E(x1192,x1193)+P4(f6(x1191,x1192),x1193)
% 0.54/0.88 [131]~P9(x1311,x1312)+P9(x1311,f21(x1312,x1313))
% 0.54/0.88 [132]~P9(x1321,x1322)+P9(x1321,f27(x1322,x1323))
% 0.54/0.88 [133]~P4(x1331,x1333)+P4(f6(x1331,x1332),x1333)
% 0.54/0.88 [140]E(x1401,a3)+P11(f30(x1402,x1403,x1401))
% 0.54/0.88 [142]E(x1421,a1)+E(f7(f30(x1422,x1421,x1423)),f20(x1422))
% 0.54/0.88 [145]~P6(x1452,x1454)+P5(f30(x1451,x1452,x1453),x1454)
% 0.54/0.88 [151]P6(x1511,x1512)+~P5(f30(x1513,x1511,x1514),x1512)
% 0.54/0.88 [138]~E(x1382,x1384)+P6(f24(x1381,f23(x1382,x1383)),x1384)
% 0.54/0.88 [141]~P6(x1411,x1414)+P6(f24(x1411,f23(x1412,x1413)),x1414)
% 0.54/0.88 [150]P6(x1502,x1504)+E(f27(f30(x1501,x1502,x1503),x1504),f30(x1501,x1502,a3))
% 0.54/0.88 [147]~P1(x1472,x1474)+E(f24(f5(x1471,x1472),f23(x1473,x1474)),f5(f24(x1471,f23(x1473,x1474)),x1472))
% 0.54/0.88 [148]~P17(x1483,x1484)+E(f5(f24(x1481,f23(x1482,x1483)),x1484),f24(f5(x1481,x1484),f23(x1482,x1484)))
% 0.54/0.88 [152]~P10(x1521,x1524,x1525)+P10(f24(x1521,f23(x1522,x1523)),x1524,x1525)
% 0.54/0.88 [160]~P17(x1601,x1602)+~P3(f30(x1603,f24(x1604,f23(x1601,x1602)),x1605))
% 0.54/0.88 [122]P17(x1222,x1221)+~P1(x1222,x1221)+P1(x1221,x1222)
% 0.54/0.88 [126]~P4(x1261,x1262)+~P8(x1261,x1262)+P13(x1261,x1262)
% 0.54/0.88 [127]~P4(x1271,x1272)+~P8(x1271,x1272)+P19(x1271,x1272)
% 0.54/0.88 [128]~P4(x1281,x1282)+~P8(x1281,x1282)+E(f18(x1281,x1282),x1281)
% 0.54/0.88 [129]~P4(x1291,x1292)+~P8(x1291,x1292)+E(f19(x1291,x1292),x1292)
% 0.54/0.88 [130]~P4(x1301,x1302)+~P8(x1301,x1302)+E(f31(x1301,x1302),x1302)
% 0.54/0.88 [134]~P4(x1341,x1342)+~P8(x1341,x1342)+E(f32(x1341,x1342),f22(x1341,x1342))
% 0.54/0.88 [124]~P8(x1243,x1241)+P1(x1241,x1242)+~P4(x1243,x1242)
% 0.54/0.88 [125]~P1(x1251,x1253)+P1(x1251,x1252)+~P1(x1253,x1252)
% 0.54/0.88 [136]E(x1361,x1362)+P4(x1363,x1362)+~P4(f6(x1363,x1361),x1362)
% 0.54/0.88 [139]~P4(x1393,x1391)+E(x1391,x1392)+E(f22(f6(x1393,x1392),x1391),f6(f22(x1393,x1391),x1392))
% 0.54/0.88 [153]P6(x1531,f20(x1532))+E(x1531,a1)+E(f8(f30(x1532,x1531,x1533)),f30(x1532,f5(x1531,f20(x1532)),a3))
% 0.54/0.88 [146]E(x1461,x1462)+P6(x1463,x1462)+~P6(f24(x1463,f23(x1461,x1464)),x1462)
% 0.54/0.88 [156]~P6(x1562,x1564)+~P17(x1564,f26(x1562,x1564))+E(f27(f30(x1561,x1562,x1563),x1564),f30(f29(x1561,x1564),f28(x1562,x1564),a3))
% 0.54/0.88 [157]~P6(x1573,x1572)+~P1(f26(x1573,x1572),x1572)+E(f30(f29(x1571,x1572),f28(x1573,x1572),x1574),f27(f30(x1571,x1573,x1574),x1572))
% 0.54/0.88 [143]~P6(x1433,x1432)+E(x1431,x1432)+E(f26(f24(x1433,f23(x1431,x1434)),x1432),f26(x1433,x1432))
% 0.54/0.88 [149]~P6(x1493,x1492)+E(x1491,x1492)+E(f28(f24(x1493,f23(x1491,x1494)),x1492),f24(f28(x1493,x1492),f23(x1491,x1494)))
% 0.54/0.88 [144]~E(x1443,x1445)+~E(x1442,x1444)+P10(f24(x1441,f23(x1442,x1443)),x1444,x1445)
% 0.54/0.88 [154]E(x1541,x1542)+P10(x1543,x1544,x1542)+~P10(f24(x1543,f23(x1545,x1541)),x1544,x1542)
% 0.54/0.88 [155]E(x1551,x1552)+P10(x1553,x1552,x1554)+~P10(f24(x1553,f23(x1551,x1555)),x1552,x1554)
% 0.54/0.88 [161]~P1(x1614,x1613)+~P3(f30(x1611,x1612,x1615))+P3(f30(x1611,f24(x1612,f23(x1613,x1614)),x1615))
% 0.54/0.88 [162]~P1(x1624,x1625)+P3(f30(x1621,x1622,x1623))+~P3(f30(x1621,f24(x1622,f23(x1625,x1624)),x1623))
% 0.54/0.88 [116]~P11(x1162)+~P9(x1161,x1162)+P12(x1161)+~P3(x1162)
% 0.54/0.88 [158]~P6(x1581,f20(x1582))+E(x1581,a1)+~P17(f20(x1582),f26(x1581,f20(x1582)))+E(f8(f30(x1582,x1581,x1583)),f30(x1582,f5(x1581,f20(x1582)),a3))
% 0.54/0.88 [159]~P6(x1591,f20(x1592))+E(x1591,a1)+~P1(f26(x1591,f20(x1592)),f20(x1592))+E(f30(x1592,f5(x1591,f20(x1592)),x1593),f8(f30(x1592,x1591,x1593)))
% 0.54/0.88 %EqnAxiom
% 0.54/0.88 [1]E(x11,x11)
% 0.54/0.88 [2]E(x22,x21)+~E(x21,x22)
% 0.54/0.88 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.54/0.88 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43))
% 0.54/0.88 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52))
% 0.54/0.88 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 0.54/0.88 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 0.54/0.88 [8]~E(x81,x82)+E(f23(x81,x83),f23(x82,x83))
% 0.54/0.88 [9]~E(x91,x92)+E(f23(x93,x91),f23(x93,x92))
% 0.54/0.88 [10]~E(x101,x102)+E(f22(x101,x103),f22(x102,x103))
% 0.54/0.88 [11]~E(x111,x112)+E(f22(x113,x111),f22(x113,x112))
% 0.54/0.88 [12]~E(x121,x122)+E(f30(x121,x123,x124),f30(x122,x123,x124))
% 0.54/0.88 [13]~E(x131,x132)+E(f30(x133,x131,x134),f30(x133,x132,x134))
% 0.54/0.88 [14]~E(x141,x142)+E(f30(x143,x144,x141),f30(x143,x144,x142))
% 0.54/0.88 [15]~E(x151,x152)+E(f24(x151,x153),f24(x152,x153))
% 0.54/0.88 [16]~E(x161,x162)+E(f24(x163,x161),f24(x163,x162))
% 0.54/0.88 [17]~E(x171,x172)+E(f26(x171,x173),f26(x172,x173))
% 0.54/0.88 [18]~E(x181,x182)+E(f26(x183,x181),f26(x183,x182))
% 0.54/0.88 [19]~E(x191,x192)+E(f20(x191),f20(x192))
% 0.54/0.88 [20]~E(x201,x202)+E(f27(x201,x203),f27(x202,x203))
% 0.54/0.88 [21]~E(x211,x212)+E(f27(x213,x211),f27(x213,x212))
% 0.54/0.88 [22]~E(x221,x222)+E(f17(x221),f17(x222))
% 0.54/0.88 [23]~E(x231,x232)+E(f29(x231,x233),f29(x232,x233))
% 0.54/0.88 [24]~E(x241,x242)+E(f29(x243,x241),f29(x243,x242))
% 0.54/0.88 [25]~E(x251,x252)+E(f8(x251),f8(x252))
% 0.54/0.88 [26]~E(x261,x262)+E(f28(x261,x263),f28(x262,x263))
% 0.54/0.88 [27]~E(x271,x272)+E(f28(x273,x271),f28(x273,x272))
% 0.54/0.88 [28]~E(x281,x282)+E(f32(x281,x283),f32(x282,x283))
% 0.54/0.88 [29]~E(x291,x292)+E(f32(x293,x291),f32(x293,x292))
% 0.54/0.88 [30]~E(x301,x302)+E(f13(x301),f13(x302))
% 0.54/0.88 [31]~E(x311,x312)+E(f7(x311),f7(x312))
% 0.54/0.88 [32]~E(x321,x322)+E(f10(x321),f10(x322))
% 0.54/0.88 [33]~E(x331,x332)+E(f21(x331,x333),f21(x332,x333))
% 0.54/0.88 [34]~E(x341,x342)+E(f21(x343,x341),f21(x343,x342))
% 0.54/0.89 [35]~E(x351,x352)+E(f12(x351,x353),f12(x352,x353))
% 0.54/0.89 [36]~E(x361,x362)+E(f12(x363,x361),f12(x363,x362))
% 0.54/0.89 [37]~E(x371,x372)+E(f11(x371),f11(x372))
% 0.54/0.89 [38]~E(x381,x382)+E(f18(x381,x383),f18(x382,x383))
% 0.54/0.89 [39]~E(x391,x392)+E(f18(x393,x391),f18(x393,x392))
% 0.54/0.89 [40]~E(x401,x402)+E(f25(x401,x403),f25(x402,x403))
% 0.54/0.89 [41]~E(x411,x412)+E(f25(x413,x411),f25(x413,x412))
% 0.54/0.89 [42]~E(x421,x422)+E(f19(x421,x423),f19(x422,x423))
% 0.54/0.89 [43]~E(x431,x432)+E(f19(x433,x431),f19(x433,x432))
% 0.54/0.89 [44]~E(x441,x442)+E(f31(x441,x443),f31(x442,x443))
% 0.54/0.89 [45]~E(x451,x452)+E(f31(x453,x451),f31(x453,x452))
% 0.54/0.89 [46]P1(x462,x463)+~E(x461,x462)+~P1(x461,x463)
% 0.54/0.89 [47]P1(x473,x472)+~E(x471,x472)+~P1(x473,x471)
% 0.54/0.89 [48]~P3(x481)+P3(x482)+~E(x481,x482)
% 0.54/0.89 [49]P9(x492,x493)+~E(x491,x492)+~P9(x491,x493)
% 0.54/0.89 [50]P9(x503,x502)+~E(x501,x502)+~P9(x503,x501)
% 0.54/0.89 [51]~P2(x511)+P2(x512)+~E(x511,x512)
% 0.54/0.89 [52]~P7(x521)+P7(x522)+~E(x521,x522)
% 0.54/0.89 [53]P10(x532,x533,x534)+~E(x531,x532)+~P10(x531,x533,x534)
% 0.54/0.89 [54]P10(x543,x542,x544)+~E(x541,x542)+~P10(x543,x541,x544)
% 0.54/0.89 [55]P10(x553,x554,x552)+~E(x551,x552)+~P10(x553,x554,x551)
% 0.54/0.89 [56]P6(x562,x563)+~E(x561,x562)+~P6(x561,x563)
% 0.54/0.89 [57]P6(x573,x572)+~E(x571,x572)+~P6(x573,x571)
% 0.54/0.89 [58]P4(x582,x583)+~E(x581,x582)+~P4(x581,x583)
% 0.54/0.89 [59]P4(x593,x592)+~E(x591,x592)+~P4(x593,x591)
% 0.54/0.89 [60]P8(x602,x603)+~E(x601,x602)+~P8(x601,x603)
% 0.54/0.89 [61]P8(x613,x612)+~E(x611,x612)+~P8(x613,x611)
% 0.54/0.89 [62]P17(x622,x623)+~E(x621,x622)+~P17(x621,x623)
% 0.54/0.89 [63]P17(x633,x632)+~E(x631,x632)+~P17(x633,x631)
% 0.54/0.89 [64]P18(x642,x643)+~E(x641,x642)+~P18(x641,x643)
% 0.54/0.89 [65]P18(x653,x652)+~E(x651,x652)+~P18(x653,x651)
% 0.54/0.89 [66]~P11(x661)+P11(x662)+~E(x661,x662)
% 0.54/0.89 [67]P16(x672,x673)+~E(x671,x672)+~P16(x671,x673)
% 0.54/0.89 [68]P16(x683,x682)+~E(x681,x682)+~P16(x683,x681)
% 0.86/0.89 [69]~P12(x691)+P12(x692)+~E(x691,x692)
% 0.86/0.89 [70]P19(x702,x703)+~E(x701,x702)+~P19(x701,x703)
% 0.86/0.89 [71]P19(x713,x712)+~E(x711,x712)+~P19(x713,x711)
% 0.86/0.89 [72]P5(x722,x723)+~E(x721,x722)+~P5(x721,x723)
% 0.86/0.89 [73]P5(x733,x732)+~E(x731,x732)+~P5(x733,x731)
% 0.86/0.89 [74]P13(x742,x743)+~E(x741,x742)+~P13(x741,x743)
% 0.86/0.89 [75]P13(x753,x752)+~E(x751,x752)+~P13(x753,x751)
% 0.86/0.89 [76]~P15(x761)+P15(x762)+~E(x761,x762)
% 0.86/0.89 [77]~P14(x771)+P14(x772)+~E(x771,x772)
% 0.86/0.89
% 0.86/0.89 %-------------------------------------------
% 0.86/0.89 cnf(163,plain,
% 0.86/0.89 (P4(f6(x1632,x1631),x1631)),
% 0.86/0.89 inference(equality_inference,[],[119])).
% 0.86/0.89 cnf(164,plain,
% 0.86/0.89 (P6(f24(x1642,f23(x1641,x1643)),x1641)),
% 0.86/0.89 inference(equality_inference,[],[138])).
% 0.86/0.89 cnf(165,plain,
% 0.86/0.89 (E(x1651,f22(f6(x1651,x1652),x1652))),
% 0.86/0.89 inference(scs_inference,[],[83,2])).
% 0.86/0.89 cnf(175,plain,
% 0.86/0.89 (P8(a4,x1751)),
% 0.86/0.89 inference(scs_inference,[],[100,80,96,83,2,22,110,111,112,120,123])).
% 0.86/0.89 cnf(176,plain,
% 0.86/0.89 (~P4(a4,x1761)),
% 0.86/0.89 inference(rename_variables,[],[96])).
% 0.86/0.89 cnf(178,plain,
% 0.86/0.89 (P8(x1781,a2)),
% 0.86/0.89 inference(scs_inference,[],[100,80,79,96,83,2,22,110,111,112,120,123,135])).
% 0.86/0.89 cnf(182,plain,
% 0.86/0.89 (E(f22(f6(x1821,x1822),x1822),x1821)),
% 0.86/0.89 inference(rename_variables,[],[83])).
% 0.86/0.89 cnf(183,plain,
% 0.86/0.89 (P1(x1831,f22(f6(x1831,x1832),x1832))),
% 0.86/0.89 inference(scs_inference,[],[100,80,79,96,83,182,2,22,110,111,112,120,123,135,3,46])).
% 0.86/0.89 cnf(184,plain,
% 0.86/0.89 (P1(x1841,x1841)),
% 0.86/0.89 inference(rename_variables,[],[80])).
% 0.86/0.89 cnf(185,plain,
% 0.86/0.89 (P1(f22(f6(x1851,x1852),x1852),x1851)),
% 0.86/0.89 inference(scs_inference,[],[100,80,184,79,96,83,182,2,22,110,111,112,120,123,135,3,46,47])).
% 0.86/0.89 cnf(187,plain,
% 0.86/0.89 (P9(x1871,f22(f6(x1871,x1872),x1872))),
% 0.86/0.89 inference(scs_inference,[],[100,80,184,81,79,96,83,182,2,22,110,111,112,120,123,135,3,46,47,49])).
% 0.86/0.89 cnf(188,plain,
% 0.86/0.89 (P9(x1881,x1881)),
% 0.86/0.89 inference(rename_variables,[],[81])).
% 0.86/0.89 cnf(189,plain,
% 0.86/0.89 (P9(f22(f6(x1891,x1892),x1892),x1891)),
% 0.86/0.89 inference(scs_inference,[],[100,80,184,81,188,79,96,83,182,2,22,110,111,112,120,123,135,3,46,47,49,50])).
% 0.86/0.89 cnf(191,plain,
% 0.86/0.89 (~P2(f22(f6(a4,x1911),x1911))),
% 0.86/0.89 inference(scs_inference,[],[100,80,184,81,188,79,96,94,83,182,2,22,110,111,112,120,123,135,3,46,47,49,50,51])).
% 0.86/0.89 cnf(192,plain,
% 0.86/0.89 (E(f22(f6(x1921,x1922),x1922),x1921)),
% 0.86/0.89 inference(rename_variables,[],[83])).
% 0.86/0.89 cnf(193,plain,
% 0.86/0.89 (~P7(f22(f6(a1,x1931),x1931))),
% 0.86/0.89 inference(scs_inference,[],[100,80,184,81,188,79,96,94,95,83,182,192,2,22,110,111,112,120,123,135,3,46,47,49,50,51,52])).
% 0.86/0.89 cnf(194,plain,
% 0.86/0.89 (E(f22(f6(x1941,x1942),x1942),x1941)),
% 0.86/0.89 inference(rename_variables,[],[83])).
% 0.86/0.89 cnf(195,plain,
% 0.86/0.89 (~E(f24(x1951,f23(x1952,x1953)),a1)),
% 0.86/0.89 inference(scs_inference,[],[100,164,80,184,81,188,79,96,97,94,95,83,182,192,2,22,110,111,112,120,123,135,3,46,47,49,50,51,52,56])).
% 0.86/0.89 cnf(196,plain,
% 0.86/0.89 (P6(f24(x1961,f23(x1962,x1963)),x1962)),
% 0.86/0.89 inference(rename_variables,[],[164])).
% 0.86/0.89 cnf(197,plain,
% 0.86/0.89 (P6(f24(x1971,f23(f22(f6(x1972,x1973),x1973),x1974)),x1972)),
% 0.86/0.89 inference(scs_inference,[],[100,164,196,80,184,81,188,79,96,97,94,95,83,182,192,194,2,22,110,111,112,120,123,135,3,46,47,49,50,51,52,56,57])).
% 0.86/0.89 cnf(200,plain,
% 0.86/0.89 (P4(f6(x2001,x2002),x2002)),
% 0.86/0.89 inference(rename_variables,[],[163])).
% 0.86/0.89 cnf(201,plain,
% 0.86/0.89 (P4(f6(x2011,f22(f6(x2012,x2013),x2013)),x2012)),
% 0.86/0.89 inference(scs_inference,[],[100,163,200,164,196,80,184,81,188,79,96,176,97,94,95,83,182,192,194,2,22,110,111,112,120,123,135,3,46,47,49,50,51,52,56,57,58,59])).
% 0.86/0.89 cnf(203,plain,
% 0.86/0.89 (~P11(f22(f6(f30(x2031,x2032,a3),x2033),x2033))),
% 0.86/0.89 inference(scs_inference,[],[100,163,200,164,196,80,184,81,188,79,96,176,97,94,95,83,182,192,194,99,2,22,110,111,112,120,123,135,3,46,47,49,50,51,52,56,57,58,59,66])).
% 0.86/0.89 cnf(225,plain,
% 0.86/0.89 (P1(x2251,f22(f6(x2251,x2252),x2252))),
% 0.86/0.89 inference(rename_variables,[],[183])).
% 0.86/0.89 cnf(227,plain,
% 0.86/0.89 (P2(f22(f6(f6(x2271,x2272),x2273),x2273))),
% 0.86/0.89 inference(scs_inference,[],[165,183,185,82,78,120,2,125,51])).
% 0.86/0.89 cnf(228,plain,
% 0.86/0.89 (E(x2281,f22(f6(x2281,x2282),x2282))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(230,plain,
% 0.86/0.89 (P9(x2301,f22(f6(x2301,x2302),x2302))),
% 0.86/0.89 inference(rename_variables,[],[187])).
% 0.86/0.89 cnf(233,plain,
% 0.86/0.89 (E(x2331,f22(f6(x2331,x2332),x2332))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(234,plain,
% 0.86/0.89 (P6(f24(x2341,f23(f22(f6(x2342,x2343),x2343),x2344)),f22(f6(x2342,x2345),x2345))),
% 0.86/0.89 inference(scs_inference,[],[165,228,233,183,185,187,197,195,82,78,85,120,2,125,51,49,3,52,57])).
% 0.86/0.89 cnf(236,plain,
% 0.86/0.89 (P1(x2361,f22(f6(f22(f6(x2361,x2362),x2362),x2363),x2363))),
% 0.86/0.89 inference(scs_inference,[],[165,228,233,183,225,185,187,197,195,82,78,85,120,2,125,51,49,3,52,57,47])).
% 0.86/0.89 cnf(237,plain,
% 0.86/0.89 (E(x2371,f22(f6(x2371,x2372),x2372))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(243,plain,
% 0.86/0.89 (P3(f22(f6(f30(x2431,a1,x2432),x2433),x2433))),
% 0.86/0.89 inference(scs_inference,[],[165,228,233,237,183,225,185,187,201,197,195,82,78,90,91,85,99,120,2,125,51,49,3,52,57,47,66,59,48])).
% 0.86/0.89 cnf(244,plain,
% 0.86/0.89 (E(x2441,f22(f6(x2441,x2442),x2442))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(246,plain,
% 0.86/0.89 (E(x2461,f22(f6(x2461,x2462),x2462))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(247,plain,
% 0.86/0.89 (P8(f22(f6(a4,x2471),x2471),x2472)),
% 0.86/0.89 inference(scs_inference,[],[165,228,233,237,244,246,183,225,185,187,230,201,197,195,175,82,78,90,91,85,99,120,2,125,51,49,3,52,57,47,66,59,48,50,60])).
% 0.86/0.89 cnf(248,plain,
% 0.86/0.89 (E(x2481,f22(f6(x2481,x2482),x2482))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(249,plain,
% 0.86/0.89 (P1(f22(f6(f22(f6(x2491,x2492),x2492),x2493),x2493),x2491)),
% 0.86/0.89 inference(scs_inference,[],[165,228,233,237,244,246,248,183,225,185,187,230,201,197,195,175,82,78,90,91,85,99,120,2,125,51,49,3,52,57,47,66,59,48,50,60,46])).
% 0.86/0.89 cnf(250,plain,
% 0.86/0.89 (E(x2501,f22(f6(x2501,x2502),x2502))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(251,plain,
% 0.86/0.89 (P8(x2511,f22(f6(a2,x2512),x2512))),
% 0.86/0.89 inference(scs_inference,[],[165,228,233,237,244,246,248,250,183,225,185,187,230,201,197,195,175,178,82,78,90,91,85,99,120,2,125,51,49,3,52,57,47,66,59,48,50,60,46,61])).
% 0.86/0.89 cnf(272,plain,
% 0.86/0.89 (E(x2721,f28(f24(x2721,f23(x2722,x2723)),x2722))),
% 0.86/0.89 inference(scs_inference,[],[185,86,120,2])).
% 0.86/0.89 cnf(273,plain,
% 0.86/0.89 (E(f22(f6(x2731,x2732),x2732),f22(f6(x2731,x2733),x2733))),
% 0.86/0.89 inference(scs_inference,[],[185,234,86,97,120,2,146])).
% 0.86/0.89 cnf(284,plain,
% 0.86/0.89 (E(x2841,f22(f6(x2841,x2842),x2842))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(286,plain,
% 0.86/0.89 (E(f28(f24(x2861,f23(x2862,x2863)),x2862),x2861)),
% 0.86/0.89 inference(rename_variables,[],[86])).
% 0.86/0.89 cnf(288,plain,
% 0.86/0.89 (E(x2881,f22(f6(x2881,x2882),x2882))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(290,plain,
% 0.86/0.89 (E(x2901,f22(f6(x2901,x2902),x2902))),
% 0.86/0.89 inference(rename_variables,[],[165])).
% 0.86/0.89 cnf(292,plain,
% 0.86/0.89 (E(f28(f24(x2921,f23(x2922,x2923)),x2922),x2921)),
% 0.86/0.89 inference(rename_variables,[],[86])).
% 0.86/0.89 cnf(295,plain,
% 0.86/0.89 (~P11(f28(f24(f22(f6(f30(x2951,x2952,a3),x2953),x2953),f23(x2954,x2955)),x2954))),
% 0.86/0.89 inference(scs_inference,[],[100,165,284,288,290,163,185,234,227,236,203,243,247,251,193,86,286,292,97,120,2,146,124,125,51,3,48,60,52,46,66])).
% 0.86/0.89 cnf(319,plain,
% 0.86/0.89 (E(f26(f24(x3191,f23(x3192,x3193)),x3192),x3193)),
% 0.86/0.89 inference(rename_variables,[],[87])).
% 0.86/0.89 cnf(324,plain,
% 0.86/0.89 (P8(f28(f24(a4,f23(x3241,x3242)),x3241),x3243)),
% 0.86/0.89 inference(scs_inference,[],[273,272,189,187,185,249,191,175,87,120,2,47,51,49,50,60])).
% 0.86/0.89 cnf(325,plain,
% 0.86/0.89 (E(x3251,f28(f24(x3251,f23(x3252,x3253)),x3252))),
% 0.86/0.89 inference(rename_variables,[],[272])).
% 0.86/0.89 cnf(330,plain,
% 0.86/0.89 (P8(x3301,f28(f24(a2,f23(x3302,x3303)),x3302))),
% 0.86/0.89 inference(scs_inference,[],[273,272,325,189,187,185,249,295,191,175,87,319,88,178,86,120,2,47,51,49,50,60,3,66,61])).
% 0.86/0.89 cnf(331,plain,
% 0.86/0.89 (E(x3311,f28(f24(x3311,f23(x3312,x3313)),x3312))),
% 0.86/0.89 inference(rename_variables,[],[272])).
% 0.86/0.89 cnf(332,plain,
% 0.86/0.89 (P1(f28(f24(a2,f23(x3321,x3322)),x3321),x3323)),
% 0.86/0.89 inference(scs_inference,[],[273,272,325,331,189,187,185,249,295,191,175,79,87,319,88,178,86,120,2,47,51,49,50,60,3,66,61,46])).
% 0.86/0.89 cnf(389,plain,
% 0.86/0.89 (E(x3891,f28(f24(x3891,f23(x3892,x3893)),x3892))),
% 0.86/0.89 inference(rename_variables,[],[272])).
% 0.86/0.89 cnf(391,plain,
% 0.86/0.89 (E(x3911,f28(f24(x3911,f23(x3912,x3913)),x3912))),
% 0.86/0.89 inference(rename_variables,[],[272])).
% 0.86/0.89 cnf(392,plain,
% 0.86/0.89 (P1(f28(f24(f28(f24(a2,f23(x3921,x3922)),x3921),f23(x3923,x3924)),x3923),x3925)),
% 0.86/0.89 inference(scs_inference,[],[272,389,391,330,332,324,83,91,90,99,120,2,48,3,66,60,61,46])).
% 0.86/0.89 cnf(469,plain,
% 0.86/0.89 (~E(f17(f30(a9,a1,a14)),a4)),
% 0.86/0.89 inference(scs_inference,[],[100,272,392,89,120,2,46,3])).
% 0.86/0.89 cnf(485,plain,
% 0.86/0.89 ($false),
% 0.86/0.89 inference(scs_inference,[],[469,89]),
% 0.86/0.89 ['proof']).
% 0.86/0.89 % SZS output end Proof
% 0.86/0.89 % Total time :0.240000s
%------------------------------------------------------------------------------