%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET776+4 : TPTP v8.2.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n023.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:26 EDT 2024
% Result : Theorem 58.91s 59.44s
% Output : CNFRefutation 58.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET776+4 : TPTP v8.2.0. Released v2.2.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n023.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 : Sun Jun 23 17:49:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.57/0.58 start to proof:theBenchmark
% 58.91/59.43 %-------------------------------------------
% 58.91/59.43 % File :CSE---1.7
% 58.91/59.43 % Problem :theBenchmark
% 58.91/59.43 % Transform :cnf
% 58.91/59.43 % Format :tptp:raw
% 58.91/59.43 % Command :java -jar mcs_scs.jar %d %s
% 58.91/59.43
% 58.91/59.43 % Result :Theorem 58.290000s
% 58.91/59.43 % Output :CNFRefutation 58.290000s
% 58.91/59.43 %-------------------------------------------
% 58.91/59.43 %--------------------------------------------------------------------------
% 58.91/59.43 % File : SET776+4 : TPTP v8.2.0. Released v2.2.0.
% 58.91/59.43 % Domain : Set Theory (Equivalence relations)
% 58.91/59.43 % Problem : Property of pre-order
% 58.91/59.43 % Version : [Pas99] axioms.
% 58.91/59.43 % English : If P is a pre-order relation,and R defined by R(A,B) iff P(A,B)
% 58.91/59.43 % and P(B,A), then R(X1,Y1) and R(X2,Y2) and P(X1,X2) implies
% 58.91/59.43 % P(Y1,Y2).
% 58.91/59.43
% 58.91/59.43 % Refs : [Pas99] Pastre (1999), Email to G. Sutcliffe
% 58.91/59.43 % Source : [Pas99]
% 58.91/59.43 % Names :
% 58.91/59.43
% 58.91/59.43 % Status : Theorem
% 58.91/59.43 % Rating : 0.22 v8.2.0, 0.17 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.17 v7.0.0, 0.20 v6.4.0, 0.19 v6.3.0, 0.25 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.22 v5.5.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.37 v5.2.0, 0.20 v5.1.0, 0.19 v5.0.0, 0.25 v4.1.0, 0.26 v4.0.0, 0.29 v3.7.0, 0.35 v3.5.0, 0.37 v3.4.0, 0.32 v3.3.0, 0.14 v3.2.0, 0.09 v3.1.0, 0.22 v2.7.0, 0.17 v2.6.0, 0.43 v2.5.0, 0.62 v2.4.0, 0.25 v2.3.0, 0.33 v2.2.1
% 58.91/59.43 % Syntax : Number of formulae : 17 ( 1 unt; 0 def)
% 58.91/59.43 % Number of atoms : 82 ( 4 equ)
% 58.91/59.43 % Maximal formula atoms : 14 ( 4 avg)
% 58.91/59.43 % Number of connectives : 68 ( 3 ~; 2 |; 29 &)
% 58.91/59.43 % ( 16 <=>; 18 =>; 0 <=; 0 <~>)
% 58.91/59.43 % Maximal formula depth : 13 ( 7 avg)
% 58.91/59.43 % Maximal term depth : 2 ( 1 avg)
% 58.91/59.44 % Number of predicates : 9 ( 8 usr; 0 prp; 2-3 aty)
% 58.91/59.44 % Number of functors : 10 ( 10 usr; 1 con; 0-3 aty)
% 58.91/59.44 % Number of variables : 66 ( 62 !; 4 ?)
% 58.91/59.44 % SPC : FOF_THM_RFO_SEQ
% 58.91/59.44
% 58.91/59.44 % Comments :
% 58.91/59.44 %--------------------------------------------------------------------------
% 58.91/59.44 %----Include set theory definitions
% 58.91/59.44 include('Axioms/SET006+0.ax').
% 58.91/59.44 %----Include equivalence relation axioms
% 58.91/59.44 include('Axioms/SET006+2.ax').
% 58.91/59.44 %--------------------------------------------------------------------------
% 58.91/59.44 fof(thIII12,conjecture,
% 58.91/59.44 ! [E,P,R] :
% 58.91/59.44 ( ( pre_order(P,E)
% 58.91/59.44 & ! [A,B] :
% 58.91/59.44 ( ( member(A,E)
% 58.91/59.44 & member(B,E) )
% 58.91/59.44 => ( apply(R,A,B)
% 58.91/59.44 <=> ( apply(P,A,B)
% 58.91/59.44 & apply(P,B,A) ) ) ) )
% 58.91/59.44 => ! [X1,X2,Y1,Y2] :
% 58.91/59.44 ( ( member(X1,E)
% 58.91/59.44 & member(X2,E)
% 58.91/59.44 & member(Y1,E)
% 58.91/59.44 & member(Y2,E) )
% 58.91/59.44 => ( ( apply(R,X1,Y1)
% 58.91/59.44 & apply(R,X2,Y2)
% 58.91/59.44 & apply(P,X1,X2) )
% 58.91/59.44 => apply(P,Y1,Y2) ) ) ) ).
% 58.91/59.44
% 58.91/59.44 %--------------------------------------------------------------------------
% 58.91/59.44 %-------------------------------------------
% 58.91/59.44 % Proof found
% 58.91/59.44 % SZS status Theorem for theBenchmark
% 58.91/59.44 % SZS output start Proof
% 58.91/59.44 %ClaNum:216(EqnAxiom:78)
% 58.91/59.44 %VarNum:1351(SingletonVarNum:305)
% 58.91/59.44 %MaxLitNum:7
% 58.91/59.44 %MaxfuncDepth:1
% 58.91/59.44 %SharedTerms:17
% 58.91/59.44 %goalClause: 79 80 81 82 83 84 85 86 88 147 148 176
% 58.91/59.44 %singleGoalClaCount:9
% 58.91/59.44 [79]P1(a1,a2)
% 58.91/59.44 [80]P1(a13,a2)
% 58.91/59.44 [81]P1(a14,a2)
% 58.91/59.44 [82]P1(a16,a2)
% 58.91/59.44 [83]P7(a11,a2)
% 58.91/59.44 [84]P2(a11,a1,a13)
% 58.91/59.44 [85]P2(a12,a1,a14)
% 58.91/59.44 [86]P2(a12,a13,a16)
% 58.91/59.44 [88]~P2(a11,a14,a16)
% 58.91/59.44 [87]~P1(x871,a3)
% 58.91/59.44 [91]~P3(x912,x911)+P9(x911,x912)
% 58.91/59.44 [92]~P3(x921,x922)+P9(x921,x922)
% 58.91/59.44 [93]~P4(x931,x932)+P6(x931,x932)
% 58.91/59.44 [94]~P6(x941,x942)+P4(x941,x942)
% 58.91/59.44 [89]~E(x891,x892)+P1(x891,f17(x892))
% 58.91/59.44 [90]E(x901,x902)+~P1(x901,f17(x902))
% 58.91/59.44 [95]~P9(x951,x952)+P1(x951,f18(x952))
% 58.91/59.44 [98]P9(x981,x982)+~P1(x981,f18(x982))
% 58.91/59.44 [99]P9(x991,x992)+P1(f15(x991,x992),x991)
% 58.91/59.44 [100]P5(x1001,x1002)+P1(f19(x1001,x1002),x1002)
% 58.91/59.44 [101]P5(x1011,x1012)+P1(f19(x1011,x1012),x1011)
% 58.91/59.44 [105]P1(f20(x1051,x1052),x1052)+P1(x1051,f34(x1052))
% 58.91/59.44 [112]~P1(x1121,f37(x1122))+P1(x1121,f21(x1121,x1122))
% 58.91/59.44 [113]~P1(x1131,f37(x1132))+P1(f21(x1131,x1132),x1132)
% 58.91/59.44 [118]P9(x1181,x1182)+~P1(f15(x1181,x1182),x1182)
% 58.91/59.44 [119]~P1(x1191,f20(x1191,x1192))+P1(x1191,f34(x1192))
% 58.91/59.44 [96]~E(x961,x963)+P1(x961,f35(x962,x963))
% 58.91/59.44 [97]~E(x971,x972)+P1(x971,f35(x972,x973))
% 58.91/59.44 [106]~P1(x1061,x1063)+P1(x1061,f36(x1062,x1063))
% 58.91/59.44 [107]~P1(x1071,x1072)+P1(x1071,f36(x1072,x1073))
% 58.91/59.44 [115]P1(x1151,x1152)+~P1(x1151,f28(x1153,x1152))
% 58.91/59.44 [116]P1(x1161,x1162)+~P1(x1161,f28(x1162,x1163))
% 58.91/59.44 [117]P1(x1171,x1172)+~P1(x1171,f4(x1172,x1173))
% 58.91/59.44 [121]~P1(x1211,x1212)+~P1(x1211,f4(x1213,x1212))
% 58.91/59.44 [163]P1(x1631,x1632)+~P1(x1631,f7(x1633,x1632,x1634))
% 58.91/59.44 [175]P2(x1751,x1752,x1753)+~P1(x1753,f7(x1752,x1754,x1751))
% 58.91/59.44 [104]~P9(x1042,x1041)+~P9(x1041,x1042)+P3(x1041,x1042)
% 58.91/59.44 [123]P7(x1231,x1232)+P1(f5(x1231,x1232),x1232)+P1(f8(x1231,x1232),x1232)
% 58.91/59.44 [124]P7(x1241,x1242)+P1(f5(x1241,x1242),x1242)+P1(f9(x1241,x1242),x1242)
% 58.91/59.44 [125]P7(x1251,x1252)+P1(f5(x1251,x1252),x1252)+P1(f10(x1251,x1252),x1252)
% 58.91/59.44 [140]P7(x1401,x1402)+P2(x1401,f8(x1401,x1402),f9(x1401,x1402))+P1(f5(x1401,x1402),x1402)
% 58.91/59.44 [141]P7(x1411,x1412)+P2(x1411,f9(x1411,x1412),f10(x1411,x1412))+P1(f5(x1411,x1412),x1412)
% 58.91/59.44 [168]P7(x1681,x1682)+~P2(x1681,f8(x1681,x1682),f10(x1681,x1682))+P1(f5(x1681,x1682),x1682)
% 58.91/59.44 [169]P7(x1691,x1692)+~P2(x1691,f5(x1691,x1692),f5(x1691,x1692))+P1(f8(x1691,x1692),x1692)
% 58.91/59.44 [170]P7(x1701,x1702)+~P2(x1701,f5(x1701,x1702),f5(x1701,x1702))+P1(f9(x1701,x1702),x1702)
% 58.91/59.44 [171]P7(x1711,x1712)+~P2(x1711,f5(x1711,x1712),f5(x1711,x1712))+P1(f10(x1711,x1712),x1712)
% 58.91/59.44 [190]P7(x1901,x1902)+P2(x1901,f8(x1901,x1902),f9(x1901,x1902))+~P2(x1901,f5(x1901,x1902),f5(x1901,x1902))
% 58.91/59.44 [191]P7(x1911,x1912)+P2(x1911,f9(x1911,x1912),f10(x1911,x1912))+~P2(x1911,f5(x1911,x1912),f5(x1911,x1912))
% 58.91/59.44 [204]P7(x2041,x2042)+~P2(x2041,f5(x2041,x2042),f5(x2041,x2042))+~P2(x2041,f8(x2041,x2042),f10(x2041,x2042))
% 58.91/59.44 [102]~P8(x1023,x1022)+P9(x1021,x1022)+~P1(x1021,x1023)
% 58.91/59.44 [103]~P1(x1031,x1033)+P1(x1031,x1032)+~P9(x1033,x1032)
% 58.91/59.44 [110]~P5(x1103,x1102)+~P1(x1101,x1102)+~P1(x1101,x1103)
% 58.91/59.44 [126]~P7(x1261,x1263)+P2(x1261,x1262,x1262)+~P1(x1262,x1263)
% 58.91/59.44 [127]~P4(x1271,x1273)+P2(x1271,x1272,x1272)+~P1(x1272,x1273)
% 58.91/59.44 [108]~P1(x1083,x1082)+~P1(x1081,x1083)+P1(x1081,f37(x1082))
% 58.91/59.44 [109]E(x1091,x1092)+E(x1091,x1093)+~P1(x1091,f35(x1093,x1092))
% 58.91/59.44 [111]P1(x1111,x1112)+~P1(x1112,x1113)+~P1(x1111,f34(x1113))
% 58.91/59.44 [114]~P1(x1141,x1143)+P1(x1141,x1142)+P1(x1141,f4(x1143,x1142))
% 58.91/59.44 [120]~P1(x1201,x1203)+~P1(x1201,x1202)+P1(x1201,f28(x1202,x1203))
% 58.91/59.44 [122]P1(x1221,x1222)+P1(x1221,x1223)+~P1(x1221,f36(x1223,x1222))
% 58.91/59.44 [145]~P1(x1451,x1453)+~P8(x1452,x1453)+P1(x1451,f30(x1452,x1453,x1451))
% 58.91/59.44 [146]~P1(x1463,x1462)+~P8(x1461,x1462)+P1(f30(x1461,x1462,x1463),x1461)
% 58.91/59.44 [172]~P1(x1721,x1723)+~P2(x1724,x1722,x1721)+P1(x1721,f7(x1722,x1723,x1724))
% 58.91/59.44 [147]~P2(a12,x1472,x1471)+P2(a11,x1471,x1472)+~P1(x1472,a2)+~P1(x1471,a2)
% 58.91/59.44 [148]~P2(a12,x1481,x1482)+P2(a11,x1481,x1482)+~P1(x1482,a2)+~P1(x1481,a2)
% 58.91/59.44 [129]P8(x1291,x1292)+P1(f29(x1291,x1292),x1291)+P1(f31(x1291,x1292),x1292)+P1(f32(x1291,x1292),x1291)
% 58.91/59.44 [130]P8(x1301,x1302)+P1(f29(x1301,x1302),x1301)+P1(f31(x1301,x1302),x1302)+P1(f33(x1301,x1302),x1301)
% 58.91/59.44 [131]P4(x1311,x1312)+P1(f22(x1312,x1311),x1312)+P1(f23(x1312,x1311),x1312)+P1(f24(x1312,x1311),x1312)
% 58.91/59.44 [132]P4(x1321,x1322)+P1(f22(x1322,x1321),x1322)+P1(f23(x1322,x1321),x1322)+P1(f26(x1322,x1321),x1322)
% 58.91/59.44 [133]P4(x1331,x1332)+P1(f22(x1332,x1331),x1332)+P1(f23(x1332,x1331),x1332)+P1(f27(x1332,x1331),x1332)
% 58.91/59.44 [134]P4(x1341,x1342)+P1(f22(x1342,x1341),x1342)+P1(f25(x1342,x1341),x1342)+P1(f24(x1342,x1341),x1342)
% 58.91/59.44 [135]P4(x1351,x1352)+P1(f22(x1352,x1351),x1352)+P1(f25(x1352,x1351),x1352)+P1(f26(x1352,x1351),x1352)
% 58.91/59.44 [136]P4(x1361,x1362)+P1(f22(x1362,x1361),x1362)+P1(f25(x1362,x1361),x1362)+P1(f27(x1362,x1361),x1362)
% 58.91/59.44 [137]P8(x1371,x1372)+P1(f29(x1371,x1372),x1371)+P1(f31(x1371,x1372),x1372)+~E(f33(x1371,x1372),f32(x1371,x1372))
% 58.91/59.44 [138]P8(x1381,x1382)+P1(f31(x1381,x1382),x1382)+P1(f32(x1381,x1382),x1381)+~P9(f29(x1381,x1382),x1382)
% 58.91/59.44 [139]P8(x1391,x1392)+P1(f31(x1391,x1392),x1392)+P1(f33(x1391,x1392),x1391)+~P9(f29(x1391,x1392),x1392)
% 58.91/59.44 [142]P8(x1421,x1422)+P1(f29(x1421,x1422),x1421)+P1(f31(x1421,x1422),x1422)+P1(f6(x1421,x1422),f32(x1421,x1422))
% 58.91/59.44 [143]P8(x1431,x1432)+P1(f29(x1431,x1432),x1431)+P1(f31(x1431,x1432),x1432)+P1(f6(x1431,x1432),f33(x1431,x1432))
% 58.91/59.44 [144]P8(x1441,x1442)+P1(f31(x1441,x1442),x1442)+~E(f33(x1441,x1442),f32(x1441,x1442))+~P9(f29(x1441,x1442),x1442)
% 58.91/59.44 [151]P8(x1511,x1512)+P1(f31(x1511,x1512),x1512)+P1(f6(x1511,x1512),f32(x1511,x1512))+~P9(f29(x1511,x1512),x1512)
% 58.91/59.44 [152]P8(x1521,x1522)+P1(f31(x1521,x1522),x1522)+P1(f6(x1521,x1522),f33(x1521,x1522))+~P9(f29(x1521,x1522),x1522)
% 58.91/59.44 [154]P4(x1541,x1542)+P2(x1541,f23(x1542,x1541),f25(x1542,x1541))+P1(f22(x1542,x1541),x1542)+P1(f24(x1542,x1541),x1542)
% 58.91/59.44 [155]P4(x1551,x1552)+P2(x1551,f23(x1552,x1551),f25(x1552,x1551))+P1(f22(x1552,x1551),x1552)+P1(f26(x1552,x1551),x1552)
% 58.91/59.44 [156]P4(x1561,x1562)+P2(x1561,f23(x1562,x1561),f25(x1562,x1561))+P1(f22(x1562,x1561),x1562)+P1(f27(x1562,x1561),x1562)
% 58.91/59.44 [157]P4(x1571,x1572)+P2(x1571,f24(x1572,x1571),f26(x1572,x1571))+P1(f22(x1572,x1571),x1572)+P1(f23(x1572,x1571),x1572)
% 58.91/59.44 [158]P4(x1581,x1582)+P2(x1581,f26(x1582,x1581),f27(x1582,x1581))+P1(f22(x1582,x1581),x1582)+P1(f23(x1582,x1581),x1582)
% 58.91/59.44 [159]P4(x1591,x1592)+P2(x1591,f24(x1592,x1591),f26(x1592,x1591))+P1(f22(x1592,x1591),x1592)+P1(f25(x1592,x1591),x1592)
% 58.91/59.44 [160]P4(x1601,x1602)+P2(x1601,f26(x1602,x1601),f27(x1602,x1601))+P1(f22(x1602,x1601),x1602)+P1(f25(x1602,x1601),x1602)
% 58.91/59.44 [177]P4(x1771,x1772)+~P2(x1771,f25(x1772,x1771),f23(x1772,x1771))+P1(f22(x1772,x1771),x1772)+P1(f24(x1772,x1771),x1772)
% 58.91/59.44 [178]P4(x1781,x1782)+~P2(x1781,f25(x1782,x1781),f23(x1782,x1781))+P1(f22(x1782,x1781),x1782)+P1(f26(x1782,x1781),x1782)
% 58.91/59.44 [179]P4(x1791,x1792)+~P2(x1791,f25(x1792,x1791),f23(x1792,x1791))+P1(f22(x1792,x1791),x1792)+P1(f27(x1792,x1791),x1792)
% 58.91/59.44 [180]P4(x1801,x1802)+~P2(x1801,f22(x1802,x1801),f22(x1802,x1801))+P1(f23(x1802,x1801),x1802)+P1(f24(x1802,x1801),x1802)
% 58.91/59.44 [181]P4(x1811,x1812)+~P2(x1811,f22(x1812,x1811),f22(x1812,x1811))+P1(f23(x1812,x1811),x1812)+P1(f26(x1812,x1811),x1812)
% 58.91/59.44 [182]P4(x1821,x1822)+~P2(x1821,f22(x1822,x1821),f22(x1822,x1821))+P1(f23(x1822,x1821),x1822)+P1(f27(x1822,x1821),x1822)
% 58.91/59.44 [183]P4(x1831,x1832)+~P2(x1831,f22(x1832,x1831),f22(x1832,x1831))+P1(f25(x1832,x1831),x1832)+P1(f24(x1832,x1831),x1832)
% 58.91/59.44 [184]P4(x1841,x1842)+~P2(x1841,f22(x1842,x1841),f22(x1842,x1841))+P1(f25(x1842,x1841),x1842)+P1(f26(x1842,x1841),x1842)
% 58.91/59.44 [185]P4(x1851,x1852)+~P2(x1851,f22(x1852,x1851),f22(x1852,x1851))+P1(f25(x1852,x1851),x1852)+P1(f27(x1852,x1851),x1852)
% 58.91/59.44 [186]P4(x1861,x1862)+~P2(x1861,f24(x1862,x1861),f27(x1862,x1861))+P1(f22(x1862,x1861),x1862)+P1(f23(x1862,x1861),x1862)
% 58.91/59.44 [187]P4(x1871,x1872)+~P2(x1871,f24(x1872,x1871),f27(x1872,x1871))+P1(f22(x1872,x1871),x1872)+P1(f25(x1872,x1871),x1872)
% 58.91/59.44 [188]P4(x1881,x1882)+P2(x1881,f23(x1882,x1881),f25(x1882,x1881))+P2(x1881,f24(x1882,x1881),f26(x1882,x1881))+P1(f22(x1882,x1881),x1882)
% 58.91/59.44 [189]P4(x1891,x1892)+P2(x1891,f23(x1892,x1891),f25(x1892,x1891))+P2(x1891,f26(x1892,x1891),f27(x1892,x1891))+P1(f22(x1892,x1891),x1892)
% 58.91/59.44 [194]P4(x1941,x1942)+P2(x1941,f23(x1942,x1941),f25(x1942,x1941))+~P2(x1941,f22(x1942,x1941),f22(x1942,x1941))+P1(f24(x1942,x1941),x1942)
% 58.91/59.45 [195]P4(x1951,x1952)+P2(x1951,f23(x1952,x1951),f25(x1952,x1951))+~P2(x1951,f22(x1952,x1951),f22(x1952,x1951))+P1(f26(x1952,x1951),x1952)
% 58.91/59.45 [196]P4(x1961,x1962)+P2(x1961,f23(x1962,x1961),f25(x1962,x1961))+~P2(x1961,f22(x1962,x1961),f22(x1962,x1961))+P1(f27(x1962,x1961),x1962)
% 58.91/59.45 [197]P4(x1971,x1972)+P2(x1971,f23(x1972,x1971),f25(x1972,x1971))+~P2(x1971,f24(x1972,x1971),f27(x1972,x1971))+P1(f22(x1972,x1971),x1972)
% 58.91/59.45 [198]P4(x1981,x1982)+P2(x1981,f24(x1982,x1981),f26(x1982,x1981))+~P2(x1981,f25(x1982,x1981),f23(x1982,x1981))+P1(f22(x1982,x1981),x1982)
% 58.91/59.45 [199]P4(x1991,x1992)+P2(x1991,f26(x1992,x1991),f27(x1992,x1991))+~P2(x1991,f25(x1992,x1991),f23(x1992,x1991))+P1(f22(x1992,x1991),x1992)
% 58.91/59.45 [200]P4(x2001,x2002)+P2(x2001,f24(x2002,x2001),f26(x2002,x2001))+~P2(x2001,f22(x2002,x2001),f22(x2002,x2001))+P1(f23(x2002,x2001),x2002)
% 58.91/59.45 [201]P4(x2011,x2012)+P2(x2011,f26(x2012,x2011),f27(x2012,x2011))+~P2(x2011,f22(x2012,x2011),f22(x2012,x2011))+P1(f23(x2012,x2011),x2012)
% 58.91/59.45 [202]P4(x2021,x2022)+P2(x2021,f24(x2022,x2021),f26(x2022,x2021))+~P2(x2021,f22(x2022,x2021),f22(x2022,x2021))+P1(f25(x2022,x2021),x2022)
% 58.91/59.45 [203]P4(x2031,x2032)+P2(x2031,f26(x2032,x2031),f27(x2032,x2031))+~P2(x2031,f22(x2032,x2031),f22(x2032,x2031))+P1(f25(x2032,x2031),x2032)
% 58.91/59.45 [205]P4(x2051,x2052)+~P2(x2051,f22(x2052,x2051),f22(x2052,x2051))+~P2(x2051,f25(x2052,x2051),f23(x2052,x2051))+P1(f24(x2052,x2051),x2052)
% 58.91/59.45 [206]P4(x2061,x2062)+~P2(x2061,f22(x2062,x2061),f22(x2062,x2061))+~P2(x2061,f25(x2062,x2061),f23(x2062,x2061))+P1(f26(x2062,x2061),x2062)
% 58.91/59.45 [207]P4(x2071,x2072)+~P2(x2071,f22(x2072,x2071),f22(x2072,x2071))+~P2(x2071,f25(x2072,x2071),f23(x2072,x2071))+P1(f27(x2072,x2071),x2072)
% 58.91/59.45 [208]P4(x2081,x2082)+~P2(x2081,f25(x2082,x2081),f23(x2082,x2081))+~P2(x2081,f24(x2082,x2081),f27(x2082,x2081))+P1(f22(x2082,x2081),x2082)
% 58.91/59.45 [209]P4(x2091,x2092)+~P2(x2091,f22(x2092,x2091),f22(x2092,x2091))+~P2(x2091,f24(x2092,x2091),f27(x2092,x2091))+P1(f23(x2092,x2091),x2092)
% 58.91/59.45 [210]P4(x2101,x2102)+~P2(x2101,f22(x2102,x2101),f22(x2102,x2101))+~P2(x2101,f24(x2102,x2101),f27(x2102,x2101))+P1(f25(x2102,x2101),x2102)
% 58.91/59.45 [211]P4(x2111,x2112)+P2(x2111,f23(x2112,x2111),f25(x2112,x2111))+P2(x2111,f24(x2112,x2111),f26(x2112,x2111))+~P2(x2111,f22(x2112,x2111),f22(x2112,x2111))
% 58.91/59.45 [212]P4(x2121,x2122)+P2(x2121,f23(x2122,x2121),f25(x2122,x2121))+P2(x2121,f26(x2122,x2121),f27(x2122,x2121))+~P2(x2121,f22(x2122,x2121),f22(x2122,x2121))
% 58.91/59.45 [213]P4(x2131,x2132)+P2(x2131,f23(x2132,x2131),f25(x2132,x2131))+~P2(x2131,f22(x2132,x2131),f22(x2132,x2131))+~P2(x2131,f24(x2132,x2131),f27(x2132,x2131))
% 58.91/59.45 [214]P4(x2141,x2142)+P2(x2141,f24(x2142,x2141),f26(x2142,x2141))+~P2(x2141,f22(x2142,x2141),f22(x2142,x2141))+~P2(x2141,f25(x2142,x2141),f23(x2142,x2141))
% 58.91/59.45 [215]P4(x2151,x2152)+P2(x2151,f26(x2152,x2151),f27(x2152,x2151))+~P2(x2151,f22(x2152,x2151),f22(x2152,x2151))+~P2(x2151,f25(x2152,x2151),f23(x2152,x2151))
% 58.91/59.45 [216]P4(x2161,x2162)+~P2(x2161,f22(x2162,x2161),f22(x2162,x2161))+~P2(x2161,f25(x2162,x2161),f23(x2162,x2161))+~P2(x2161,f24(x2162,x2161),f27(x2162,x2161))
% 58.91/59.45 [176]~P2(a11,x1762,x1761)+~P2(a11,x1761,x1762)+P2(a12,x1761,x1762)+~P1(x1762,a2)+~P1(x1761,a2)
% 58.91/59.45 [149]P8(x1491,x1492)+~P1(x1493,x1491)+P1(f29(x1491,x1492),x1491)+P1(f32(x1491,x1492),x1491)+~P1(f31(x1491,x1492),x1493)
% 58.91/59.45 [150]P8(x1501,x1502)+~P1(x1503,x1501)+P1(f29(x1501,x1502),x1501)+P1(f33(x1501,x1502),x1501)+~P1(f31(x1501,x1502),x1503)
% 58.91/59.45 [153]P8(x1531,x1532)+~P1(x1533,x1531)+P1(f29(x1531,x1532),x1531)+~E(f33(x1531,x1532),f32(x1531,x1532))+~P1(f31(x1531,x1532),x1533)
% 58.91/59.45 [161]P8(x1611,x1612)+~P1(x1613,x1611)+P1(f32(x1611,x1612),x1611)+~P9(f29(x1611,x1612),x1612)+~P1(f31(x1611,x1612),x1613)
% 58.91/59.45 [162]P8(x1621,x1622)+~P1(x1623,x1621)+P1(f33(x1621,x1622),x1621)+~P9(f29(x1621,x1622),x1622)+~P1(f31(x1621,x1622),x1623)
% 58.91/59.45 [164]P8(x1641,x1642)+~P1(x1643,x1641)+P1(f29(x1641,x1642),x1641)+P1(f6(x1641,x1642),f32(x1641,x1642))+~P1(f31(x1641,x1642),x1643)
% 58.91/59.45 [165]P8(x1651,x1652)+~P1(x1653,x1651)+P1(f29(x1651,x1652),x1651)+P1(f6(x1651,x1652),f33(x1651,x1652))+~P1(f31(x1651,x1652),x1653)
% 58.91/59.45 [166]P8(x1661,x1662)+~P1(x1663,x1661)+~E(f33(x1661,x1662),f32(x1661,x1662))+~P9(f29(x1661,x1662),x1662)+~P1(f31(x1661,x1662),x1663)
% 58.91/59.45 [173]P8(x1731,x1732)+~P1(x1733,x1731)+P1(f6(x1731,x1732),f32(x1731,x1732))+~P9(f29(x1731,x1732),x1732)+~P1(f31(x1731,x1732),x1733)
% 58.91/59.45 [174]P8(x1741,x1742)+~P1(x1743,x1741)+P1(f6(x1741,x1742),f33(x1741,x1742))+~P9(f29(x1741,x1742),x1742)+~P1(f31(x1741,x1742),x1743)
% 58.91/59.45 [167]~P1(x1673,x1674)+~P4(x1671,x1674)+~P2(x1671,x1673,x1672)+P2(x1671,x1672,x1673)+~P1(x1672,x1674)
% 58.91/59.45 [128]~P1(x1283,x1281)+~P1(x1281,x1284)+E(x1281,x1282)+~P1(x1283,x1282)+~P1(x1282,x1284)+~P8(x1284,x1285)
% 58.91/59.45 [192]~P1(x1922,x1924)+~P7(x1921,x1924)+~P2(x1921,x1925,x1923)+~P2(x1921,x1922,x1925)+P2(x1921,x1922,x1923)+~P1(x1923,x1924)+~P1(x1925,x1924)
% 58.91/59.45 [193]~P1(x1932,x1934)+~P4(x1931,x1934)+~P2(x1931,x1935,x1933)+~P2(x1931,x1932,x1935)+P2(x1931,x1932,x1933)+~P1(x1933,x1934)+~P1(x1935,x1934)
% 58.91/59.45 %EqnAxiom
% 58.91/59.45 [1]E(x11,x11)
% 58.91/59.45 [2]E(x22,x21)+~E(x21,x22)
% 58.91/59.45 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.91/59.45 [4]~E(x41,x42)+E(f17(x41),f17(x42))
% 58.91/59.45 [5]~E(x51,x52)+E(f27(x51,x53),f27(x52,x53))
% 58.91/59.45 [6]~E(x61,x62)+E(f27(x63,x61),f27(x63,x62))
% 58.91/59.45 [7]~E(x71,x72)+E(f18(x71),f18(x72))
% 58.91/59.45 [8]~E(x81,x82)+E(f35(x81,x83),f35(x82,x83))
% 58.91/59.45 [9]~E(x91,x92)+E(f35(x93,x91),f35(x93,x92))
% 58.91/59.45 [10]~E(x101,x102)+E(f22(x101,x103),f22(x102,x103))
% 58.91/59.45 [11]~E(x111,x112)+E(f22(x113,x111),f22(x113,x112))
% 58.91/59.45 [12]~E(x121,x122)+E(f26(x121,x123),f26(x122,x123))
% 58.91/59.45 [13]~E(x131,x132)+E(f26(x133,x131),f26(x133,x132))
% 58.91/59.45 [14]~E(x141,x142)+E(f15(x141,x143),f15(x142,x143))
% 58.91/59.45 [15]~E(x151,x152)+E(f15(x153,x151),f15(x153,x152))
% 58.91/59.45 [16]~E(x161,x162)+E(f19(x161,x163),f19(x162,x163))
% 58.91/59.45 [17]~E(x171,x172)+E(f19(x173,x171),f19(x173,x172))
% 58.91/59.45 [18]~E(x181,x182)+E(f10(x181,x183),f10(x182,x183))
% 58.91/59.45 [19]~E(x191,x192)+E(f10(x193,x191),f10(x193,x192))
% 58.91/59.45 [20]~E(x201,x202)+E(f34(x201),f34(x202))
% 58.91/59.45 [21]~E(x211,x212)+E(f20(x211,x213),f20(x212,x213))
% 58.91/59.45 [22]~E(x221,x222)+E(f20(x223,x221),f20(x223,x222))
% 58.91/59.45 [23]~E(x231,x232)+E(f36(x231,x233),f36(x232,x233))
% 58.91/59.45 [24]~E(x241,x242)+E(f36(x243,x241),f36(x243,x242))
% 58.91/59.45 [25]~E(x251,x252)+E(f23(x251,x253),f23(x252,x253))
% 58.91/59.45 [26]~E(x261,x262)+E(f23(x263,x261),f23(x263,x262))
% 58.91/59.45 [27]~E(x271,x272)+E(f37(x271),f37(x272))
% 58.91/59.45 [28]~E(x281,x282)+E(f24(x281,x283),f24(x282,x283))
% 58.91/59.45 [29]~E(x291,x292)+E(f24(x293,x291),f24(x293,x292))
% 58.91/59.45 [30]~E(x301,x302)+E(f25(x301,x303),f25(x302,x303))
% 58.91/59.45 [31]~E(x311,x312)+E(f25(x313,x311),f25(x313,x312))
% 58.91/59.45 [32]~E(x321,x322)+E(f21(x321,x323),f21(x322,x323))
% 58.91/59.45 [33]~E(x331,x332)+E(f21(x333,x331),f21(x333,x332))
% 58.91/59.45 [34]~E(x341,x342)+E(f5(x341,x343),f5(x342,x343))
% 58.91/59.45 [35]~E(x351,x352)+E(f5(x353,x351),f5(x353,x352))
% 58.91/59.45 [36]~E(x361,x362)+E(f7(x361,x363,x364),f7(x362,x363,x364))
% 58.91/59.45 [37]~E(x371,x372)+E(f7(x373,x371,x374),f7(x373,x372,x374))
% 58.91/59.45 [38]~E(x381,x382)+E(f7(x383,x384,x381),f7(x383,x384,x382))
% 58.91/59.45 [39]~E(x391,x392)+E(f9(x391,x393),f9(x392,x393))
% 58.91/59.45 [40]~E(x401,x402)+E(f9(x403,x401),f9(x403,x402))
% 58.91/59.45 [41]~E(x411,x412)+E(f4(x411,x413),f4(x412,x413))
% 58.91/59.45 [42]~E(x421,x422)+E(f4(x423,x421),f4(x423,x422))
% 58.91/59.45 [43]~E(x431,x432)+E(f28(x431,x433),f28(x432,x433))
% 58.91/59.45 [44]~E(x441,x442)+E(f28(x443,x441),f28(x443,x442))
% 58.91/59.45 [45]~E(x451,x452)+E(f29(x451,x453),f29(x452,x453))
% 58.91/59.45 [46]~E(x461,x462)+E(f29(x463,x461),f29(x463,x462))
% 58.91/59.45 [47]~E(x471,x472)+E(f33(x471,x473),f33(x472,x473))
% 58.91/59.45 [48]~E(x481,x482)+E(f33(x483,x481),f33(x483,x482))
% 58.91/59.45 [49]~E(x491,x492)+E(f8(x491,x493),f8(x492,x493))
% 58.91/59.45 [50]~E(x501,x502)+E(f8(x503,x501),f8(x503,x502))
% 58.91/59.45 [51]~E(x511,x512)+E(f6(x511,x513),f6(x512,x513))
% 58.91/59.45 [52]~E(x521,x522)+E(f6(x523,x521),f6(x523,x522))
% 58.91/59.45 [53]~E(x531,x532)+E(f32(x531,x533),f32(x532,x533))
% 58.91/59.45 [54]~E(x541,x542)+E(f32(x543,x541),f32(x543,x542))
% 58.91/59.45 [55]~E(x551,x552)+E(f30(x551,x553,x554),f30(x552,x553,x554))
% 58.91/59.45 [56]~E(x561,x562)+E(f30(x563,x561,x564),f30(x563,x562,x564))
% 58.91/59.45 [57]~E(x571,x572)+E(f30(x573,x574,x571),f30(x573,x574,x572))
% 58.91/59.45 [58]~E(x581,x582)+E(f31(x581,x583),f31(x582,x583))
% 58.91/59.45 [59]~E(x591,x592)+E(f31(x593,x591),f31(x593,x592))
% 58.91/59.45 [60]P1(x602,x603)+~E(x601,x602)+~P1(x601,x603)
% 58.91/59.45 [61]P1(x613,x612)+~E(x611,x612)+~P1(x613,x611)
% 58.91/59.45 [62]P2(x622,x623,x624)+~E(x621,x622)+~P2(x621,x623,x624)
% 58.91/59.45 [63]P2(x633,x632,x634)+~E(x631,x632)+~P2(x633,x631,x634)
% 58.91/59.45 [64]P2(x643,x644,x642)+~E(x641,x642)+~P2(x643,x644,x641)
% 58.91/59.45 [65]P9(x652,x653)+~E(x651,x652)+~P9(x651,x653)
% 58.91/59.45 [66]P9(x663,x662)+~E(x661,x662)+~P9(x663,x661)
% 58.91/59.45 [67]P8(x672,x673)+~E(x671,x672)+~P8(x671,x673)
% 58.91/59.45 [68]P8(x683,x682)+~E(x681,x682)+~P8(x683,x681)
% 58.91/59.45 [69]P7(x692,x693)+~E(x691,x692)+~P7(x691,x693)
% 58.91/59.45 [70]P7(x703,x702)+~E(x701,x702)+~P7(x703,x701)
% 58.91/59.45 [71]P4(x712,x713)+~E(x711,x712)+~P4(x711,x713)
% 58.91/59.45 [72]P4(x723,x722)+~E(x721,x722)+~P4(x723,x721)
% 58.91/59.45 [73]P5(x732,x733)+~E(x731,x732)+~P5(x731,x733)
% 58.91/59.45 [74]P5(x743,x742)+~E(x741,x742)+~P5(x743,x741)
% 58.91/59.45 [75]P3(x752,x753)+~E(x751,x752)+~P3(x751,x753)
% 58.91/59.45 [76]P3(x763,x762)+~E(x761,x762)+~P3(x763,x761)
% 58.91/59.45 [77]P6(x772,x773)+~E(x771,x772)+~P6(x771,x773)
% 58.91/59.45 [78]P6(x783,x782)+~E(x781,x782)+~P6(x783,x781)
% 58.91/59.45
% 58.91/59.45 %-------------------------------------------
% 58.91/59.45 cnf(217,plain,
% 58.91/59.45 (P1(x2171,f17(x2171))),
% 58.91/59.45 inference(equality_inference,[],[89])).
% 58.91/59.45 cnf(218,plain,
% 58.91/59.45 (P1(x2181,f35(x2182,x2181))),
% 58.91/59.45 inference(equality_inference,[],[96])).
% 58.91/59.45 cnf(219,plain,
% 58.91/59.45 (P1(x2191,f35(x2191,x2192))),
% 58.91/59.45 inference(equality_inference,[],[97])).
% 58.91/59.45 cnf(220,plain,
% 58.91/59.45 (P9(a3,x2201)),
% 58.91/59.45 inference(scs_inference,[],[87,99])).
% 58.91/59.45 cnf(221,plain,
% 58.91/59.45 (~P1(x2211,a3)),
% 58.91/59.45 inference(rename_variables,[],[87])).
% 58.91/59.45 cnf(223,plain,
% 58.91/59.45 (P5(x2231,a3)),
% 58.91/59.45 inference(scs_inference,[],[87,221,99,100])).
% 58.91/59.45 cnf(224,plain,
% 58.91/59.45 (~P1(x2241,a3)),
% 58.91/59.45 inference(rename_variables,[],[87])).
% 58.91/59.45 cnf(227,plain,
% 58.91/59.45 (~P1(x2271,a3)),
% 58.91/59.45 inference(rename_variables,[],[87])).
% 58.91/59.45 cnf(229,plain,
% 58.91/59.45 (~P1(x2291,f37(a3))),
% 58.91/59.45 inference(scs_inference,[],[87,221,224,227,99,100,101,113])).
% 58.91/59.45 cnf(230,plain,
% 58.91/59.45 (~P1(x2301,a3)),
% 58.91/59.45 inference(rename_variables,[],[87])).
% 58.91/59.45 cnf(232,plain,
% 58.91/59.45 (P2(a11,a1,a1)),
% 58.91/59.45 inference(scs_inference,[],[79,83,87,221,224,227,99,100,101,113,126])).
% 58.91/59.45 cnf(234,plain,
% 58.91/59.45 (~P8(a3,a2)),
% 58.91/59.45 inference(scs_inference,[],[79,83,87,221,224,227,230,99,100,101,113,126,146])).
% 58.91/59.45 cnf(235,plain,
% 58.91/59.45 (~P1(x2351,a3)),
% 58.91/59.45 inference(rename_variables,[],[87])).
% 58.91/59.45 cnf(237,plain,
% 58.91/59.45 (~E(a2,a3)),
% 58.91/59.45 inference(scs_inference,[],[79,83,87,221,224,227,230,235,99,100,101,113,126,146,61])).
% 58.91/59.45 cnf(239,plain,
% 58.91/59.45 (P3(a3,a3)),
% 58.91/59.45 inference(scs_inference,[],[79,83,87,221,224,227,230,235,99,100,101,113,126,146,61,104])).
% 58.91/59.45 cnf(241,plain,
% 58.91/59.45 (P2(a12,a1,a1)),
% 58.91/59.45 inference(scs_inference,[],[79,83,87,221,224,227,230,235,99,100,101,113,126,146,61,104,176])).
% 58.91/59.45 cnf(257,plain,
% 58.91/59.45 (P5(f37(a3),x2571)),
% 58.91/59.45 inference(scs_inference,[],[229,101])).
% 58.91/59.45 cnf(258,plain,
% 58.91/59.45 (~P1(x2581,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(260,plain,
% 58.91/59.45 (~P1(x2601,f37(f37(a3)))),
% 58.91/59.45 inference(scs_inference,[],[229,258,101,113])).
% 58.91/59.45 cnf(261,plain,
% 58.91/59.45 (~P1(x2611,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(263,plain,
% 58.91/59.45 (P5(x2631,f37(a3))),
% 58.91/59.45 inference(scs_inference,[],[229,258,261,101,113,100])).
% 58.91/59.45 cnf(264,plain,
% 58.91/59.45 (~P1(x2641,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(266,plain,
% 58.91/59.45 (P9(f37(a3),x2661)),
% 58.91/59.45 inference(scs_inference,[],[229,258,261,264,101,113,100,99])).
% 58.91/59.45 cnf(267,plain,
% 58.91/59.45 (~P1(x2671,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(270,plain,
% 58.91/59.45 (~P1(x2701,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(272,plain,
% 58.91/59.45 (P2(a11,a13,a13)),
% 58.91/59.45 inference(scs_inference,[],[79,80,83,229,258,261,264,267,101,113,100,99,146,126])).
% 58.91/59.45 cnf(274,plain,
% 58.91/59.45 (P3(f37(a3),a3)),
% 58.91/59.45 inference(scs_inference,[],[79,80,83,229,258,261,264,267,220,101,113,100,99,146,126,104])).
% 58.91/59.45 cnf(278,plain,
% 58.91/59.45 (~P1(x2781,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(284,plain,
% 58.91/59.45 (~P1(x2841,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(286,plain,
% 58.91/59.45 (P7(x2861,f37(a3))+~E(a1,a14)+P1(f9(x2861,f37(a3)),f37(a3))),
% 58.91/59.45 inference(scs_inference,[],[79,80,81,85,83,229,258,261,264,267,270,278,284,220,101,113,100,99,146,126,104,61,176,63,147,124])).
% 58.91/59.45 cnf(288,plain,
% 58.91/59.45 (P2(a11,a14,a14)),
% 58.91/59.45 inference(scs_inference,[],[81,83,126])).
% 58.91/59.45 cnf(292,plain,
% 58.91/59.45 (P9(f37(a3),x2921)),
% 58.91/59.45 inference(rename_variables,[],[266])).
% 58.91/59.45 cnf(294,plain,
% 58.91/59.45 (~E(a14,a16)),
% 58.91/59.45 inference(scs_inference,[],[81,88,83,266,126,104,64])).
% 58.91/59.45 cnf(300,plain,
% 58.91/59.45 (~P1(x3001,f37(a3))),
% 58.91/59.45 inference(rename_variables,[],[229])).
% 58.91/59.45 cnf(301,plain,
% 58.91/59.45 (P7(x3011,f37(a3))+P1(f10(x3011,f37(a3)),f37(a3))),
% 58.91/59.45 inference(scs_inference,[],[79,81,88,83,260,266,229,300,126,104,64,61,176,286,125])).
% 58.91/59.45 cnf(305,plain,
% 58.91/59.45 (~P1(x3051,a3)),
% 58.91/59.45 inference(rename_variables,[],[87])).
% 58.91/59.45 cnf(310,plain,
% 58.91/59.45 (P9(x3101,x3102)+~E(f37(a3),x3101)),
% 58.91/59.45 inference(scs_inference,[],[79,81,88,83,260,266,292,229,300,87,305,126,104,64,61,176,286,125,168,169,65])).
% 58.91/59.45 cnf(315,plain,
% 58.91/59.45 (P2(a11,a16,a16)),
% 58.91/59.45 inference(scs_inference,[],[82,83,229,301,126])).
% 58.91/59.45 cnf(317,plain,
% 58.91/59.45 (~E(f17(x3171),a3)),
% 58.91/59.45 inference(scs_inference,[],[82,83,87,217,229,301,126,61])).
% 58.91/59.45 cnf(322,plain,
% 58.91/59.45 (~E(a16,a14)),
% 58.91/59.45 inference(scs_inference,[],[82,88,83,87,217,257,229,301,126,61,176,73,63])).
% 58.91/59.45 cnf(328,plain,
% 58.91/59.45 (P7(x3281,a3)+P1(f8(x3281,a3),a3)),
% 58.91/59.45 inference(scs_inference,[],[80,82,88,83,87,217,257,263,239,229,301,126,61,176,73,63,74,75,76,102,123])).
% 58.91/59.45 cnf(336,plain,
% 58.91/59.45 (~P1(x3361,a3)),
% 58.91/59.45 inference(rename_variables,[],[87])).
% 58.91/59.45 cnf(337,plain,
% 58.91/59.45 (~E(f35(x3371,x3372),a3)),
% 58.91/59.46 inference(scs_inference,[],[87,336,218,328,61])).
% 58.91/59.46 cnf(341,plain,
% 58.91/59.46 (P9(x3411,x3412)+~E(a3,x3411)),
% 58.91/59.46 inference(scs_inference,[],[81,87,336,218,220,328,61,102,65])).
% 58.91/59.46 cnf(367,plain,
% 58.91/59.46 (~P8(f35(x3671,x3672),x3673)+P9(x3671,x3673)),
% 58.91/59.46 inference(scs_inference,[],[81,84,85,219,127,63,62,102])).
% 58.91/59.46 cnf(377,plain,
% 58.91/59.46 (P2(a11,a1,a14)),
% 58.91/59.46 inference(scs_inference,[],[79,81,85,83,60,126,148])).
% 58.91/59.46 cnf(400,plain,
% 58.91/59.46 (~P8(f35(x4001,x4002),x4003)+P9(x4002,x4003)),
% 58.91/59.46 inference(scs_inference,[],[86,218,274,76,64,102])).
% 58.91/59.46 cnf(455,plain,
% 58.91/59.46 (~P1(a3,f17(a2))),
% 58.91/59.46 inference(scs_inference,[],[237,2,90])).
% 58.91/59.46 cnf(462,plain,
% 58.91/59.46 (P1(x4621,f35(x4622,x4623))+~E(x4622,x4621)),
% 58.91/59.46 inference(scs_inference,[],[85,288,219,217,455,89,64,63,127,60])).
% 58.91/59.46 cnf(472,plain,
% 58.91/59.46 (~P2(a11,a1,a16)+~E(a1,a14)),
% 58.91/59.46 inference(scs_inference,[],[79,81,82,83,88,232,63,64,192])).
% 58.91/59.46 cnf(487,plain,
% 58.91/59.46 (P1(x4871,f35(x4872,x4873))+~E(x4873,x4871)),
% 58.91/59.46 inference(scs_inference,[],[315,218,62,60])).
% 58.91/59.46 cnf(561,plain,
% 58.91/59.46 (~P2(a11,a13,a16)+~E(a13,a14)),
% 58.91/59.46 inference(scs_inference,[],[80,81,82,83,88,272,63,64,192])).
% 58.91/59.46 cnf(626,plain,
% 58.91/59.46 (P1(a3,f18(a3))),
% 58.91/59.46 inference(scs_inference,[],[239,91,95])).
% 58.91/59.46 cnf(781,plain,
% 58.91/59.46 (~P1(x7811,a3)),
% 58.91/59.46 inference(rename_variables,[],[87])).
% 58.91/59.46 cnf(782,plain,
% 58.91/59.46 (~P1(x7821,a3)),
% 58.91/59.46 inference(rename_variables,[],[87])).
% 58.91/59.46 cnf(784,plain,
% 58.91/59.46 (P4(x7841,a3)+P1(f23(a3,x7841),a3)+P1(f26(a3,x7841),a3)),
% 58.91/59.46 inference(scs_inference,[],[87,781,782,132])).
% 58.91/59.46 cnf(786,plain,
% 58.91/59.46 (~P1(x7861,a3)),
% 58.91/59.46 inference(rename_variables,[],[87])).
% 58.91/59.46 cnf(794,plain,
% 58.91/59.46 (~P1(x7941,a3)),
% 58.91/59.46 inference(rename_variables,[],[87])).
% 58.91/59.46 cnf(795,plain,
% 58.91/59.46 (P4(x7951,a3)),
% 58.91/59.46 inference(scs_inference,[],[79,87,786,794,229,219,220,223,784,108,110,146,103,61])).
% 58.91/59.46 cnf(1974,plain,
% 58.91/59.46 (P2(a11,a1,a16)+~P2(a11,a13,a16)),
% 58.91/59.46 inference(scs_inference,[],[82,83,84,79,80,229,217,61,192])).
% 58.91/59.46 cnf(1976,plain,
% 58.91/59.46 (~P2(a11,a13,a16)+~E(a1,a14)),
% 58.91/59.46 inference(scs_inference,[],[82,83,84,79,80,229,217,61,192,472])).
% 58.91/59.46 cnf(2013,plain,
% 58.91/59.46 (~E(a14,a13)+~P2(a11,a13,a16)),
% 58.91/59.46 inference(scs_inference,[],[561,2])).
% 58.91/59.46 cnf(2456,plain,
% 58.91/59.46 (~P1(x24561,f37(a3))),
% 58.91/59.46 inference(rename_variables,[],[229])).
% 58.91/59.46 cnf(2457,plain,
% 58.91/59.46 (~P1(x24571,f37(a3))),
% 58.91/59.46 inference(rename_variables,[],[229])).
% 58.91/59.46 cnf(2459,plain,
% 58.91/59.46 (P4(x24591,f37(a3))+P1(f25(f37(a3),x24591),f37(a3))+P1(f26(f37(a3),x24591),f37(a3))),
% 58.91/59.46 inference(scs_inference,[],[229,2456,2457,135])).
% 58.91/59.46 cnf(2461,plain,
% 58.91/59.46 (~P1(x24611,f37(a3))),
% 58.91/59.46 inference(rename_variables,[],[229])).
% 58.91/59.46 cnf(2465,plain,
% 58.91/59.46 (P4(x24651,f37(a3))),
% 58.91/59.46 inference(scs_inference,[],[229,2461,257,260,2459,108,110,61])).
% 58.91/59.46 cnf(2894,plain,
% 58.91/59.46 (~E(a1,a14)),
% 58.91/59.46 inference(scs_inference,[],[82,80,86,1976,148])).
% 58.91/59.46 cnf(2955,plain,
% 58.91/59.46 (~E(a14,a13)),
% 58.91/59.46 inference(scs_inference,[],[82,80,86,2013,148])).
% 58.91/59.46 cnf(3447,plain,
% 58.91/59.46 (P1(f37(a3),f36(x34471,f18(x34472)))),
% 58.91/59.46 inference(scs_inference,[],[266,106,95])).
% 58.91/59.46 cnf(3448,plain,
% 58.91/59.46 (P1(f37(a3),f18(x34481))),
% 58.91/59.46 inference(scs_inference,[],[3447,87,122])).
% 58.91/59.46 cnf(3458,plain,
% 58.91/59.46 (~E(f18(x34581),a3)),
% 58.91/59.46 inference(scs_inference,[],[87,3448,61])).
% 58.91/59.46 cnf(3532,plain,
% 58.91/59.46 (P1(x35321,f36(f34(a3),x35322))),
% 58.91/59.46 inference(scs_inference,[],[87,107,105])).
% 58.91/59.46 cnf(3533,plain,
% 58.91/59.46 (P1(x35331,f34(a3))),
% 58.91/59.46 inference(scs_inference,[],[3532,87,122])).
% 58.91/59.46 cnf(3534,plain,
% 58.91/59.46 (P1(x35341,f36(f34(a3),x35342))),
% 58.91/59.46 inference(rename_variables,[],[3532])).
% 58.91/59.46 cnf(3538,plain,
% 58.91/59.46 (P9(x35381,f34(a3))),
% 58.91/59.46 inference(scs_inference,[],[3532,3534,87,122,61,118])).
% 58.91/59.46 cnf(3551,plain,
% 58.91/59.46 (~E(f34(a3),a3)),
% 58.91/59.46 inference(scs_inference,[],[87,3533,61])).
% 58.91/59.46 cnf(3553,plain,
% 58.91/59.46 (P9(x35531,x35532)+~E(f34(a3),x35532)),
% 58.91/59.46 inference(scs_inference,[],[87,3533,3538,61,66])).
% 58.91/59.46 cnf(3560,plain,
% 58.91/59.46 (~P8(f34(a3),x35601)+P9(x35602,x35601)),
% 58.91/59.46 inference(scs_inference,[],[3533,102])).
% 58.91/59.46 cnf(3746,plain,
% 58.91/59.46 (~P1(a1,f4(f4(x37461,a2),x37462))),
% 58.91/59.46 inference(scs_inference,[],[79,117,121])).
% 58.91/59.46 cnf(3747,plain,
% 58.91/59.46 (~P1(a1,f4(x37471,a2))),
% 58.91/59.46 inference(scs_inference,[],[87,3746,114])).
% 58.91/59.46 cnf(3768,plain,
% 58.91/59.46 (~E(f35(x37681,a1),f4(x37682,a2))),
% 58.91/59.46 inference(scs_inference,[],[3747,218,61])).
% 58.91/59.46 cnf(3775,plain,
% 58.91/59.46 (~E(f35(a1,x37751),f4(x37752,a2))),
% 58.91/59.46 inference(scs_inference,[],[3747,219,61])).
% 58.91/59.46 cnf(3828,plain,
% 58.91/59.46 (~P8(f35(a2,x38281),f4(x38282,a2))),
% 58.91/59.46 inference(scs_inference,[],[79,3747,367,103])).
% 58.91/59.46 cnf(3957,plain,
% 58.91/59.46 (~P8(f35(x39571,a2),f4(x39572,a2))),
% 58.91/59.46 inference(scs_inference,[],[79,3747,400,103])).
% 58.91/59.46 cnf(4624,plain,
% 58.91/59.46 (~P2(a11,a13,a16)+P1(a16,f7(a1,a2,a11))),
% 58.91/59.46 inference(scs_inference,[],[82,1974,172])).
% 58.91/59.46 cnf(10563,plain,
% 58.91/59.46 (~P1(x105631,f28(x105632,a3))),
% 58.91/59.46 inference(scs_inference,[],[79,294,2465,220,87,93,90,95,106,107,115])).
% 58.91/59.46 cnf(10565,plain,
% 58.91/59.46 (~P1(x105651,f28(a3,x105652))),
% 58.91/59.46 inference(scs_inference,[],[79,294,2465,220,87,93,90,95,106,107,115,116])).
% 58.91/59.46 cnf(10567,plain,
% 58.91/59.46 (~P1(x105671,f4(a3,x105672))),
% 58.91/59.46 inference(scs_inference,[],[79,294,2465,220,87,93,90,95,106,107,115,116,117])).
% 58.91/59.46 cnf(10571,plain,
% 58.91/59.46 (~P1(x105711,f7(x105712,a3,x105713))),
% 58.91/59.46 inference(scs_inference,[],[79,294,2465,220,81,87,93,90,95,106,107,115,116,117,121,163])).
% 58.91/59.46 cnf(10575,plain,
% 58.91/59.46 (~E(a14,a1)),
% 58.91/59.46 inference(scs_inference,[],[79,294,2894,2465,88,220,81,87,93,90,95,106,107,115,116,117,121,163,175,2])).
% 58.91/59.46 cnf(10588,plain,
% 58.91/59.46 (~P2(a12,a16,a14)),
% 58.91/59.46 inference(scs_inference,[],[79,294,2894,455,2465,241,3448,626,3747,88,220,81,82,229,87,93,90,95,106,107,115,116,117,121,163,175,2,109,172,120,61,146,103,147])).
% 58.91/59.46 cnf(10609,plain,
% 58.91/59.46 (P1(a13,f36(a2,x106091))),
% 58.91/59.46 inference(scs_inference,[],[322,80,90,107])).
% 58.91/59.46 cnf(10619,plain,
% 58.91/59.46 (~E(a13,a14)),
% 58.91/59.46 inference(scs_inference,[],[322,2955,10588,795,80,90,107,93,121,106,175,2])).
% 58.91/59.46 cnf(10620,plain,
% 58.91/59.46 (P1(a13,f28(a2,a2))),
% 58.91/59.46 inference(scs_inference,[],[322,2955,10588,795,80,90,107,93,121,106,175,2,120])).
% 58.91/59.46 cnf(10622,plain,
% 58.91/59.46 (P1(a1,f7(a1,a2,a11))),
% 58.91/59.46 inference(scs_inference,[],[79,322,2955,10588,232,795,80,90,107,93,121,106,175,2,120,172])).
% 58.91/59.46 cnf(10627,plain,
% 58.91/59.46 (~P1(x106271,f28(x106272,a3))),
% 58.91/59.46 inference(rename_variables,[],[10563])).
% 58.91/59.46 cnf(10628,plain,
% 58.91/59.46 (~P1(x106281,f28(a3,x106282))),
% 58.91/59.46 inference(rename_variables,[],[10565])).
% 58.91/59.46 cnf(10631,plain,
% 58.91/59.46 (~P1(x106311,f7(x106312,a3,x106313))),
% 58.91/59.46 inference(rename_variables,[],[10571])).
% 58.91/59.46 cnf(10633,plain,
% 58.91/59.46 (~P2(a12,a14,a16)),
% 58.91/59.46 inference(scs_inference,[],[79,322,2955,10588,10571,10563,10565,232,795,88,80,81,82,90,107,93,121,106,175,2,120,172,109,124,103,148])).
% 58.91/59.46 cnf(10638,plain,
% 58.91/59.46 (~P8(x106381,f4(x106382,a2))+~E(x106381,f35(a2,x106383))),
% 58.91/59.46 inference(scs_inference,[],[79,322,2955,10588,10571,10563,10565,3828,232,795,88,80,81,82,90,107,93,121,106,175,2,120,172,109,124,103,148,3553,3560,67])).
% 58.91/59.46 cnf(10644,plain,
% 58.91/59.46 (P2(a11,a16,a13)),
% 58.91/59.46 inference(scs_inference,[],[79,322,2955,10588,10571,10631,10563,10627,10565,10628,3828,232,86,795,88,80,81,82,90,107,93,121,106,175,2,120,172,109,124,103,148,3553,3560,67,129,147])).
% 58.91/59.46 cnf(10652,plain,
% 58.91/59.46 (~P1(a16,f4(x106521,a2))),
% 58.91/59.46 inference(scs_inference,[],[82,121])).
% 58.91/59.46 cnf(10654,plain,
% 58.91/59.46 (~P1(a13,f17(a14))),
% 58.91/59.46 inference(scs_inference,[],[10619,82,121,90])).
% 58.91/59.46 cnf(10656,plain,
% 58.91/59.46 (P1(a14,f36(x106561,a2))),
% 58.91/59.46 inference(scs_inference,[],[10619,81,82,121,90,106])).
% 58.91/59.46 cnf(10663,plain,
% 58.91/59.46 (P1(a14,f28(a2,a2))),
% 58.91/59.46 inference(scs_inference,[],[10619,10633,3768,81,82,121,90,106,107,175,2,120])).
% 58.91/59.46 cnf(10688,plain,
% 58.91/59.46 (P1(a16,f36(a2,x106881))),
% 58.91/59.46 inference(scs_inference,[],[82,107])).
% 58.91/59.46 cnf(10690,plain,
% 58.91/59.46 (~P1(a14,f17(a1))),
% 58.91/59.46 inference(scs_inference,[],[10575,82,107,90])).
% 58.91/59.46 cnf(10701,plain,
% 58.91/59.46 (~E(a3,f28(a2,a2))),
% 58.91/59.46 inference(scs_inference,[],[10575,10654,3775,10620,82,107,90,106,2,120,109,103,341])).
% 58.91/59.46 cnf(10702,plain,
% 58.91/59.46 (~E(f37(a3),f28(a2,a2))),
% 58.91/59.46 inference(scs_inference,[],[10575,10654,3775,10620,82,107,90,106,2,120,109,103,341,310])).
% 58.91/59.46 cnf(10703,plain,
% 58.91/59.46 (~E(f34(a3),f17(a14))),
% 58.91/59.46 inference(scs_inference,[],[10575,10654,3775,10620,82,107,90,106,2,120,109,103,341,310,3553])).
% 58.91/59.46 cnf(10717,plain,
% 58.91/59.46 (~E(f37(a3),f7(a1,a2,a11))),
% 58.91/59.46 inference(scs_inference,[],[3551,10622,10702,10571,90,2,109,103,310])).
% 58.91/59.46 cnf(10719,plain,
% 58.91/59.46 (P1(f31(a3,a2),a2)+P1(f29(a3,a2),a3)),
% 58.91/59.46 inference(scs_inference,[],[3551,10622,10702,234,10571,87,90,2,109,103,310,341,129])).
% 58.91/59.46 cnf(10722,plain,
% 58.91/59.46 (P1(f29(a3,a2),a3)+~P1(f31(a3,a2),f4(x107221,a2))),
% 58.91/59.46 inference(scs_inference,[],[3551,10622,10702,234,10571,87,90,2,109,103,310,341,129,121])).
% 58.91/59.46 cnf(10724,plain,
% 58.91/59.46 (P1(f29(a3,a2),a3)+P1(f31(a3,a2),f36(a2,x107241))),
% 58.91/59.46 inference(scs_inference,[],[3551,10622,10702,234,10571,87,90,2,109,103,310,341,129,121,107])).
% 58.91/59.46 cnf(10726,plain,
% 58.91/59.46 (P1(f29(a3,a2),a3)+P1(f31(a3,a2),f36(x107261,a2))),
% 58.91/59.46 inference(scs_inference,[],[3551,10622,10702,234,10571,87,90,2,109,103,310,341,129,121,107,106])).
% 58.91/59.46 cnf(10732,plain,
% 58.91/59.46 (~P1(f17(x107321),f35(a3,a3))),
% 58.91/59.46 inference(scs_inference,[],[10703,317,90,2,109])).
% 58.91/59.46 cnf(10738,plain,
% 58.91/59.46 (~P1(x107381,f28(x107382,a3))),
% 58.91/59.46 inference(rename_variables,[],[10563])).
% 58.91/59.46 cnf(10739,plain,
% 58.91/59.46 (~P1(x107391,f28(a3,x107392))),
% 58.91/59.46 inference(rename_variables,[],[10565])).
% 58.91/59.46 cnf(10741,plain,
% 58.91/59.46 (P8(f28(a3,a3),f4(a3,x107411))),
% 58.91/59.46 inference(scs_inference,[],[10703,10663,10690,317,10563,10738,10565,10739,10567,229,90,2,109,103,130,129])).
% 58.91/59.46 cnf(10748,plain,
% 58.91/59.46 (~P1(x107481,a3)),
% 58.91/59.46 inference(rename_variables,[],[87])).
% 58.91/59.46 cnf(10749,plain,
% 58.91/59.46 (~P1(f31(a3,a2),f4(x107491,a2))),
% 58.91/59.46 inference(scs_inference,[],[10703,10663,10690,317,10563,10738,10565,10739,10567,229,87,10748,90,2,109,103,130,129,10638,10719,10722])).
% 58.91/59.46 cnf(10750,plain,
% 58.91/59.46 (~P1(x107501,a3)),
% 58.91/59.46 inference(rename_variables,[],[87])).
% 58.91/59.46 cnf(10752,plain,
% 58.91/59.46 (~P1(x107521,a3)),
% 58.91/59.46 inference(rename_variables,[],[87])).
% 58.91/59.46 cnf(10755,plain,
% 58.91/59.46 (~E(f34(a3),f17(a1))),
% 58.91/59.46 inference(scs_inference,[],[10703,10663,10690,317,10563,10738,10565,10739,10567,229,87,10748,10750,10752,90,2,109,103,130,129,10638,10719,10722,10724,10726,3553])).
% 58.91/59.46 cnf(10758,plain,
% 58.91/59.46 (P1(f31(a3,a2),f28(a2,a2))),
% 58.91/59.46 inference(scs_inference,[],[10703,10663,10690,317,10563,10738,10565,10739,10567,229,87,10748,10750,10752,90,2,109,103,130,129,10638,10719,10722,10724,10726,3553,3560,120])).
% 58.91/59.46 cnf(10768,plain,
% 58.91/59.46 (~E(f28(a2,a2),a3)),
% 58.91/59.46 inference(scs_inference,[],[10701,337,90,2])).
% 58.91/59.46 cnf(10771,plain,
% 58.91/59.46 (~P1(f35(x107711,x107712),f35(a3,a3))),
% 58.91/59.46 inference(scs_inference,[],[10732,10701,337,3533,90,2,61,109])).
% 58.91/59.46 cnf(10783,plain,
% 58.91/59.46 (P2(a11,a13,a16)),
% 58.91/59.46 inference(scs_inference,[],[79,10758,10732,10701,10741,10749,3957,337,10571,3533,86,80,82,90,2,61,109,146,103,487,67,60,148])).
% 58.91/59.46 cnf(10785,plain,
% 58.91/59.46 (P2(a11,a1,a16)),
% 58.91/59.46 inference(scs_inference,[],[79,10758,10732,10701,10741,10749,3957,337,10571,3533,86,80,82,90,2,61,109,146,103,487,67,60,148,1974])).
% 58.91/59.46 cnf(10786,plain,
% 58.91/59.46 (P1(a16,f7(a1,a2,a11))),
% 58.91/59.46 inference(scs_inference,[],[79,10758,10732,10701,10741,10749,3957,337,10571,3533,86,80,82,90,2,61,109,146,103,487,67,60,148,1974,4624])).
% 58.91/59.46 cnf(10804,plain,
% 58.91/59.46 (P2(a11,a14,a1)),
% 58.91/59.46 inference(scs_inference,[],[79,10783,10771,10717,3458,10644,3533,85,81,80,82,90,2,109,103,176,462,3560,147])).
% 58.91/59.46 cnf(10811,plain,
% 58.91/59.46 (~P2(a11,a14,a13)),
% 58.91/59.46 inference(scs_inference,[],[79,10783,10771,10717,3458,10609,10656,10688,10644,3533,88,85,81,80,83,82,90,2,109,103,176,462,3560,147,193,192])).
% 58.91/59.46 cnf(10832,plain,
% 58.91/59.46 ($false),
% 58.91/59.46 inference(scs_inference,[],[79,10785,10811,10804,10755,10768,10652,10786,377,88,81,80,83,82,90,2,64,172,109,103,148,147,176,192]),
% 58.91/59.46 ['proof']).
% 58.91/59.46 % SZS output end Proof
% 58.91/59.46 % Total time :58.290000s
%------------------------------------------------------------------------------