%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SET813+4 : TPTP v8.2.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 14:22:32 EDT 2024
% Result : Theorem 59.25s 59.29s
% Output : CNFRefutation 59.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SET813+4 : TPTP v8.2.0. Released v3.2.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n018.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 : Sun Jun 23 15:10:39 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.22/0.58 start to proof:theBenchmark
% 59.22/59.28 %-------------------------------------------
% 59.22/59.28 % File :CSE---1.7
% 59.22/59.28 % Problem :theBenchmark
% 59.22/59.28 % Transform :cnf
% 59.22/59.28 % Format :tptp:raw
% 59.22/59.28 % Command :java -jar mcs_scs.jar %d %s
% 59.22/59.28
% 59.22/59.28 % Result :Theorem 58.630000s
% 59.22/59.28 % Output :CNFRefutation 58.630000s
% 59.22/59.28 %-------------------------------------------
% 59.25/59.29 %------------------------------------------------------------------------------
% 59.25/59.29 % File : SET813+4 : TPTP v8.2.0. Released v3.2.0.
% 59.25/59.29 % Domain : Set Theory (Order relations)
% 59.25/59.29 % Problem : An ordinal number is a member of its successor
% 59.25/59.29 % Version : [Pas05] axioms.
% 59.25/59.29 % English :
% 59.25/59.29
% 59.25/59.29 % Refs : [Pas05] Pastre (2005), Email to G. Sutcliffe
% 59.25/59.29 % Source : [Pas05]
% 59.25/59.29 % Names :
% 59.25/59.29
% 59.25/59.29 % Status : Theorem
% 59.25/59.29 % Rating : 0.14 v8.2.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.07 v7.3.0, 0.10 v7.1.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.17 v6.2.0, 0.16 v6.1.0, 0.17 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.10 v5.0.0, 0.21 v4.1.0, 0.22 v4.0.0, 0.25 v3.5.0, 0.26 v3.4.0, 0.21 v3.3.0, 0.14 v3.2.0
% 59.25/59.29 % Syntax : Number of formulae : 20 ( 1 unt; 0 def)
% 59.25/59.29 % Number of atoms : 67 ( 4 equ)
% 59.25/59.29 % Maximal formula atoms : 11 ( 3 avg)
% 59.25/59.29 % Number of connectives : 50 ( 3 ~; 3 |; 16 &)
% 59.25/59.29 % ( 17 <=>; 11 =>; 0 <=; 0 <~>)
% 59.25/59.29 % Maximal formula depth : 11 ( 6 avg)
% 59.25/59.29 % Maximal term depth : 3 ( 1 avg)
% 59.25/59.29 % Number of predicates : 9 ( 8 usr; 0 prp; 1-3 aty)
% 59.25/59.29 % Number of functors : 13 ( 13 usr; 3 con; 0-3 aty)
% 59.25/59.29 % Number of variables : 57 ( 54 !; 3 ?)
% 59.25/59.29 % SPC : FOF_THM_RFO_SEQ
% 59.25/59.29
% 59.25/59.29 % Comments :
% 59.25/59.29 %------------------------------------------------------------------------------
% 59.25/59.29 %----Include set theory definitions
% 59.25/59.29 include('Axioms/SET006+0.ax').
% 59.25/59.29 %----Include ordinal numbers axioms
% 59.25/59.29 include('Axioms/SET006+4.ax').
% 59.25/59.29 %------------------------------------------------------------------------------
% 59.25/59.29 fof(thV12,conjecture,
% 59.25/59.29 ! [A] :
% 59.25/59.29 ( member(A,on)
% 59.25/59.29 => member(A,suc(A)) ) ).
% 59.25/59.29
% 59.25/59.29 %------------------------------------------------------------------------------
% 59.25/59.29 %-------------------------------------------
% 59.25/59.29 % Proof found
% 59.25/59.29 % SZS status Theorem for theBenchmark
% 59.25/59.29 % SZS output start Proof
% 59.25/59.30 %ClaNum:143(EqnAxiom:63)
% 59.25/59.30 %VarNum:560(SingletonVarNum:186)
% 59.25/59.30 %MaxLitNum:7
% 59.25/59.30 %MaxfuncDepth:2
% 59.25/59.30 %SharedTerms:7
% 59.25/59.30 %goalClause: 64 66
% 59.25/59.30 %singleGoalClaCount:2
% 59.25/59.30 [64]P1(a1,a8)
% 59.25/59.30 [66]~P1(a1,f21(a1))
% 59.25/59.30 [65]~P1(x651,a2)
% 59.25/59.30 [68]P5(x681)+~P1(x681,a8)
% 59.25/59.30 [69]~P1(x691,a8)+P6(a9,x691)
% 59.25/59.30 [72]~P2(x722,x721)+P8(x721,x722)
% 59.25/59.30 [73]~P2(x731,x732)+P8(x731,x732)
% 59.25/59.30 [74]~P6(x741,x742)+P7(x741,x742)
% 59.25/59.30 [93]~P1(x931,x932)+P3(a9,x931,x932)
% 59.25/59.30 [111]P1(x1111,x1112)+~P3(a9,x1111,x1112)
% 59.25/59.30 [67]~E(x671,x672)+P1(x671,f22(x672))
% 59.25/59.30 [71]E(x711,x712)+~P1(x711,f22(x712))
% 59.25/59.30 [75]~P8(x751,x752)+P1(x751,f23(x752))
% 59.25/59.30 [78]P8(x781,x782)+~P1(x781,f23(x782))
% 59.25/59.30 [79]P8(x791,x792)+P1(f10(x791,x792),x791)
% 59.25/59.30 [83]P1(f11(x831,x832),x832)+P1(x831,f24(x832))
% 59.25/59.30 [90]~P1(x901,f27(x902))+P1(x901,f12(x901,x902))
% 59.25/59.30 [91]~P1(x911,f27(x912))+P1(f12(x911,x912),x912)
% 59.25/59.30 [99]P8(x991,x992)+~P1(f10(x991,x992),x992)
% 59.25/59.30 [100]~P1(x1001,f11(x1001,x1002))+P1(x1001,f24(x1002))
% 59.25/59.30 [101]~P1(x1011,f21(x1012))+P1(x1011,f26(x1012,f22(x1012)))
% 59.25/59.30 [113]P1(x1131,f21(x1132))+~P1(x1131,f26(x1132,f22(x1132)))
% 59.25/59.30 [112]P1(x1121,x1122)+~P4(x1121,x1123,x1122)
% 59.25/59.30 [76]~E(x761,x763)+P1(x761,f25(x762,x763))
% 59.25/59.30 [77]~E(x771,x772)+P1(x771,f25(x772,x773))
% 59.25/59.30 [85]~P1(x851,x853)+P1(x851,f26(x852,x853))
% 59.25/59.30 [86]~P1(x861,x862)+P1(x861,f26(x862,x863))
% 59.25/59.30 [96]P1(x961,x962)+~P1(x961,f16(x963,x962))
% 59.25/59.30 [97]P1(x971,x972)+~P1(x971,f16(x972,x973))
% 59.25/59.30 [98]P1(x981,x982)+~P1(x981,f3(x982,x983))
% 59.25/59.30 [103]~P1(x1031,x1032)+~P1(x1031,f3(x1033,x1032))
% 59.25/59.30 [129]P1(x1291,x1292)+~P1(x1291,f20(x1293,x1294,x1292))
% 59.25/59.30 [139]P3(x1391,x1392,x1393)+~P1(x1392,f20(x1393,x1391,x1394))
% 59.25/59.30 [70]~P1(x701,x702)+P5(x701)+~P5(x702)
% 59.25/59.30 [80]~P1(x801,x802)+P8(x801,x802)+~P1(x802,a8)
% 59.25/59.30 [82]~P8(x822,x821)+~P8(x821,x822)+P2(x821,x822)
% 59.25/59.30 [95]~P7(x951,x952)+P6(x951,x952)+P8(f14(x951,x952),x952)
% 59.25/59.30 [105]P7(x1051,x1052)+P1(f17(x1051,x1052),x1052)+P1(f4(x1051,x1052),x1052)
% 59.25/59.30 [106]P7(x1061,x1062)+P1(f17(x1061,x1062),x1062)+P1(f6(x1061,x1062),x1062)
% 59.25/59.30 [107]P7(x1071,x1072)+P1(f17(x1071,x1072),x1072)+P1(f7(x1071,x1072),x1072)
% 59.25/59.30 [108]P7(x1081,x1082)+P1(f5(x1081,x1082),x1082)+P1(f4(x1081,x1082),x1082)
% 59.25/59.30 [109]P7(x1091,x1092)+P1(f5(x1091,x1092),x1092)+P1(f6(x1091,x1092),x1092)
% 59.25/59.30 [110]P7(x1101,x1102)+P1(f5(x1101,x1102),x1102)+P1(f7(x1101,x1102),x1102)
% 59.25/59.30 [114]~P7(x1141,x1142)+P6(x1141,x1142)+P1(f18(x1141,x1142),f14(x1141,x1142))
% 59.25/59.30 [115]P7(x1151,x1152)+P3(x1151,f4(x1151,x1152),f6(x1151,x1152))+P1(f17(x1151,x1152),x1152)
% 59.25/59.31 [116]P7(x1161,x1162)+P3(x1161,f6(x1161,x1162),f7(x1161,x1162))+P1(f17(x1161,x1162),x1162)
% 59.25/59.31 [117]P7(x1171,x1172)+P3(x1171,f4(x1171,x1172),f6(x1171,x1172))+P1(f5(x1171,x1172),x1172)
% 59.25/59.31 [118]P7(x1181,x1182)+P3(x1181,f6(x1181,x1182),f7(x1181,x1182))+P1(f5(x1181,x1182),x1182)
% 59.25/59.31 [119]P7(x1191,x1192)+P3(x1191,f17(x1191,x1192),f5(x1191,x1192))+P1(f4(x1191,x1192),x1192)
% 59.25/59.31 [120]P7(x1201,x1202)+P3(x1201,f5(x1201,x1202),f17(x1201,x1202))+P1(f4(x1201,x1202),x1202)
% 59.25/59.31 [121]P7(x1211,x1212)+P3(x1211,f17(x1211,x1212),f5(x1211,x1212))+P1(f6(x1211,x1212),x1212)
% 59.25/59.31 [122]P7(x1221,x1222)+P3(x1221,f5(x1221,x1222),f17(x1221,x1222))+P1(f6(x1221,x1222),x1222)
% 59.25/59.31 [123]P7(x1231,x1232)+P3(x1231,f17(x1231,x1232),f5(x1231,x1232))+P1(f7(x1231,x1232),x1232)
% 59.25/59.31 [124]P7(x1241,x1242)+P3(x1241,f5(x1241,x1242),f17(x1241,x1242))+P1(f7(x1241,x1242),x1242)
% 59.25/59.31 [130]P7(x1301,x1302)+~P3(x1301,f4(x1301,x1302),f7(x1301,x1302))+P1(f17(x1301,x1302),x1302)
% 59.25/59.31 [131]P7(x1311,x1312)+~P3(x1311,f4(x1311,x1312),f7(x1311,x1312))+P1(f5(x1311,x1312),x1312)
% 59.25/59.31 [132]P7(x1321,x1322)+P3(x1321,f17(x1321,x1322),f5(x1321,x1322))+P3(x1321,f4(x1321,x1322),f6(x1321,x1322))
% 59.25/59.31 [133]P7(x1331,x1332)+P3(x1331,f17(x1331,x1332),f5(x1331,x1332))+P3(x1331,f6(x1331,x1332),f7(x1331,x1332))
% 59.25/59.31 [134]P7(x1341,x1342)+P3(x1341,f5(x1341,x1342),f17(x1341,x1342))+P3(x1341,f4(x1341,x1342),f6(x1341,x1342))
% 59.25/59.31 [135]P7(x1351,x1352)+P3(x1351,f5(x1351,x1352),f17(x1351,x1352))+P3(x1351,f6(x1351,x1352),f7(x1351,x1352))
% 59.25/59.31 [140]P7(x1401,x1402)+P3(x1401,f17(x1401,x1402),f5(x1401,x1402))+~P3(x1401,f4(x1401,x1402),f7(x1401,x1402))
% 59.25/59.31 [141]P7(x1411,x1412)+P3(x1411,f5(x1411,x1412),f17(x1411,x1412))+~P3(x1411,f4(x1411,x1412),f7(x1411,x1412))
% 59.25/59.31 [81]~P1(x811,x813)+P1(x811,x812)+~P8(x813,x812)
% 59.25/59.31 [87]~P1(x873,x872)+~P1(x871,x873)+P1(x871,f27(x872))
% 59.25/59.31 [88]E(x881,x882)+E(x881,x883)+~P1(x881,f25(x883,x882))
% 59.25/59.31 [89]P1(x891,x892)+~P1(x892,x893)+~P1(x891,f24(x893))
% 59.25/59.31 [94]~P1(x941,x943)+P1(x941,x942)+P1(x941,f3(x943,x942))
% 59.25/59.31 [102]~P1(x1021,x1023)+~P1(x1021,x1022)+P1(x1021,f16(x1022,x1023))
% 59.25/59.31 [104]P1(x1041,x1042)+P1(x1041,x1043)+~P1(x1041,f26(x1043,x1042))
% 59.25/59.31 [125]~P7(x1251,x1252)+P6(x1251,x1252)+~P4(x1253,x1251,f14(x1251,x1252))
% 59.25/59.31 [126]~P1(x1261,x1263)+P4(x1261,x1262,x1263)+~E(f19(x1262,x1263,x1261),x1261)
% 59.25/59.31 [128]~P1(x1281,x1283)+P4(x1281,x1282,x1283)+P1(f19(x1282,x1283,x1281),x1283)
% 59.25/59.31 [143]~P1(x1431,x1433)+P4(x1431,x1432,x1433)+~P3(x1432,x1431,f19(x1432,x1433,x1431))
% 59.25/59.31 [137]~P1(x1371,x1374)+~P3(x1373,x1371,x1372)+P1(x1371,f20(x1372,x1373,x1374))
% 59.25/59.31 [84]~P5(x841)+P1(f13(x841),x841)+~P6(a9,x841)+P1(x841,a8)
% 59.25/59.31 [92]~P5(x921)+~P6(a9,x921)+~P8(f13(x921),x921)+P1(x921,a8)
% 59.25/59.31 [127]~P4(x1272,x1273,x1274)+E(x1271,x1272)+P3(x1273,x1272,x1271)+~P1(x1271,x1274)
% 59.25/59.31 [136]~P8(x1363,x1362)+~P6(x1361,x1362)+~P1(x1364,x1363)+P4(f15(x1361,x1362,x1363),x1361,x1363)
% 59.25/59.31 [138]~P3(x1384,x1381,x1383)+~P3(x1384,x1383,x1381)+~P1(x1381,x1382)+~P1(x1383,x1382)+~P7(x1384,x1382)
% 59.25/59.31 [142]~P1(x1422,x1424)+~P7(x1421,x1424)+~P3(x1421,x1425,x1423)+~P3(x1421,x1422,x1425)+P3(x1421,x1422,x1423)+~P1(x1423,x1424)+~P1(x1425,x1424)
% 59.25/59.31 %EqnAxiom
% 59.25/59.31 [1]E(x11,x11)
% 59.25/59.31 [2]E(x22,x21)+~E(x21,x22)
% 59.25/59.31 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.25/59.31 [4]~E(x41,x42)+E(f21(x41),f21(x42))
% 59.25/59.31 [5]~E(x51,x52)+E(f22(x51),f22(x52))
% 59.25/59.31 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 59.25/59.31 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 59.25/59.31 [8]~E(x81,x82)+E(f23(x81),f23(x82))
% 59.25/59.31 [9]~E(x91,x92)+E(f25(x91,x93),f25(x92,x93))
% 59.25/59.31 [10]~E(x101,x102)+E(f25(x103,x101),f25(x103,x102))
% 59.25/59.31 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113))
% 59.25/59.31 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122))
% 59.25/59.31 [13]~E(x131,x132)+E(f6(x131,x133),f6(x132,x133))
% 59.25/59.31 [14]~E(x141,x142)+E(f6(x143,x141),f6(x143,x142))
% 59.25/59.31 [15]~E(x151,x152)+E(f10(x151,x153),f10(x152,x153))
% 59.25/59.31 [16]~E(x161,x162)+E(f10(x163,x161),f10(x163,x162))
% 59.25/59.31 [17]~E(x171,x172)+E(f24(x171),f24(x172))
% 59.25/59.31 [18]~E(x181,x182)+E(f11(x181,x183),f11(x182,x183))
% 59.25/59.31 [19]~E(x191,x192)+E(f11(x193,x191),f11(x193,x192))
% 59.25/59.31 [20]~E(x201,x202)+E(f13(x201),f13(x202))
% 59.25/59.31 [21]~E(x211,x212)+E(f26(x211,x213),f26(x212,x213))
% 59.25/59.31 [22]~E(x221,x222)+E(f26(x223,x221),f26(x223,x222))
% 59.25/59.31 [23]~E(x231,x232)+E(f15(x231,x233,x234),f15(x232,x233,x234))
% 59.25/59.31 [24]~E(x241,x242)+E(f15(x243,x241,x244),f15(x243,x242,x244))
% 59.25/59.31 [25]~E(x251,x252)+E(f15(x253,x254,x251),f15(x253,x254,x252))
% 59.25/59.31 [26]~E(x261,x262)+E(f27(x261),f27(x262))
% 59.25/59.31 [27]~E(x271,x272)+E(f17(x271,x273),f17(x272,x273))
% 59.25/59.31 [28]~E(x281,x282)+E(f17(x283,x281),f17(x283,x282))
% 59.25/59.31 [29]~E(x291,x292)+E(f7(x291,x293),f7(x292,x293))
% 59.25/59.31 [30]~E(x301,x302)+E(f7(x303,x301),f7(x303,x302))
% 59.25/59.31 [31]~E(x311,x312)+E(f12(x311,x313),f12(x312,x313))
% 59.25/59.31 [32]~E(x321,x322)+E(f12(x323,x321),f12(x323,x322))
% 59.25/59.31 [33]~E(x331,x332)+E(f19(x331,x333,x334),f19(x332,x333,x334))
% 59.25/59.31 [34]~E(x341,x342)+E(f19(x343,x341,x344),f19(x343,x342,x344))
% 59.25/59.31 [35]~E(x351,x352)+E(f19(x353,x354,x351),f19(x353,x354,x352))
% 59.25/59.31 [36]~E(x361,x362)+E(f3(x361,x363),f3(x362,x363))
% 59.25/59.31 [37]~E(x371,x372)+E(f3(x373,x371),f3(x373,x372))
% 59.25/59.31 [38]~E(x381,x382)+E(f14(x381,x383),f14(x382,x383))
% 59.25/59.31 [39]~E(x391,x392)+E(f14(x393,x391),f14(x393,x392))
% 59.25/59.31 [40]~E(x401,x402)+E(f16(x401,x403),f16(x402,x403))
% 59.25/59.31 [41]~E(x411,x412)+E(f16(x413,x411),f16(x413,x412))
% 59.25/59.31 [42]~E(x421,x422)+E(f18(x421,x423),f18(x422,x423))
% 59.25/59.31 [43]~E(x431,x432)+E(f18(x433,x431),f18(x433,x432))
% 59.25/59.31 [44]~E(x441,x442)+E(f20(x441,x443,x444),f20(x442,x443,x444))
% 59.25/59.31 [45]~E(x451,x452)+E(f20(x453,x451,x454),f20(x453,x452,x454))
% 59.25/59.31 [46]~E(x461,x462)+E(f20(x463,x464,x461),f20(x463,x464,x462))
% 59.25/59.31 [47]P1(x472,x473)+~E(x471,x472)+~P1(x471,x473)
% 59.25/59.31 [48]P1(x483,x482)+~E(x481,x482)+~P1(x483,x481)
% 59.25/59.31 [49]P3(x492,x493,x494)+~E(x491,x492)+~P3(x491,x493,x494)
% 59.25/59.31 [50]P3(x503,x502,x504)+~E(x501,x502)+~P3(x503,x501,x504)
% 59.25/59.31 [51]P3(x513,x514,x512)+~E(x511,x512)+~P3(x513,x514,x511)
% 59.25/59.31 [52]P4(x522,x523,x524)+~E(x521,x522)+~P4(x521,x523,x524)
% 59.25/59.31 [53]P4(x533,x532,x534)+~E(x531,x532)+~P4(x533,x531,x534)
% 59.25/59.31 [54]P4(x543,x544,x542)+~E(x541,x542)+~P4(x543,x544,x541)
% 59.25/59.31 [55]P7(x552,x553)+~E(x551,x552)+~P7(x551,x553)
% 59.25/59.31 [56]P7(x563,x562)+~E(x561,x562)+~P7(x563,x561)
% 59.25/59.31 [57]~P5(x571)+P5(x572)+~E(x571,x572)
% 59.25/59.31 [58]P6(x582,x583)+~E(x581,x582)+~P6(x581,x583)
% 59.25/59.31 [59]P6(x593,x592)+~E(x591,x592)+~P6(x593,x591)
% 59.25/59.31 [60]P8(x602,x603)+~E(x601,x602)+~P8(x601,x603)
% 59.25/59.31 [61]P8(x613,x612)+~E(x611,x612)+~P8(x613,x611)
% 59.25/59.31 [62]P2(x622,x623)+~E(x621,x622)+~P2(x621,x623)
% 59.25/59.31 [63]P2(x633,x632)+~E(x631,x632)+~P2(x633,x631)
% 59.25/59.31
% 59.25/59.31 %-------------------------------------------
% 59.25/59.32 cnf(144,plain,
% 59.25/59.32 (P1(x1441,f22(x1441))),
% 59.25/59.32 inference(equality_inference,[],[67])).
% 59.25/59.32 cnf(146,plain,
% 59.25/59.32 (P1(x1461,f25(x1461,x1462))),
% 59.25/59.32 inference(equality_inference,[],[77])).
% 59.25/59.32 cnf(150,plain,
% 59.25/59.32 (~P1(x1501,a2)),
% 59.25/59.32 inference(rename_variables,[],[65])).
% 59.25/59.32 cnf(152,plain,
% 59.25/59.32 (~P1(x1521,f27(a2))),
% 59.25/59.32 inference(scs_inference,[],[64,65,150,68,79,91])).
% 59.25/59.32 cnf(157,plain,
% 59.25/59.32 (P2(a2,a2)),
% 59.25/59.32 inference(scs_inference,[],[64,66,65,150,68,79,91,112,82])).
% 59.25/59.32 cnf(159,plain,
% 59.25/59.32 (~E(a8,f21(a1))),
% 59.25/59.32 inference(scs_inference,[],[64,66,65,150,68,79,91,112,82,48])).
% 59.25/59.32 cnf(317,plain,
% 59.25/59.32 (P1(x3171,f22(x3172))+~E(x3172,x3171)),
% 59.25/59.32 inference(scs_inference,[],[144,47])).
% 59.25/59.32 cnf(341,plain,
% 59.25/59.32 (~E(f25(x3411,x3412),f21(a1))+~E(x3411,a1)),
% 59.25/59.32 inference(scs_inference,[],[66,146,157,63,62,47,48])).
% 59.25/59.32 cnf(363,plain,
% 59.25/59.32 (~P1(f21(a1),f22(a8))),
% 59.25/59.32 inference(scs_inference,[],[159,2,71])).
% 59.25/59.32 cnf(829,plain,
% 59.25/59.32 (~E(a8,a2)),
% 59.25/59.32 inference(scs_inference,[],[65,64,48])).
% 59.25/59.32 cnf(939,plain,
% 59.25/59.32 (P1(x9391,f26(x9392,f24(a2)))),
% 59.25/59.32 inference(scs_inference,[],[65,85,83])).
% 59.25/59.32 cnf(941,plain,
% 59.25/59.32 (P1(x9411,f26(x9412,f24(a2)))),
% 59.25/59.32 inference(rename_variables,[],[939])).
% 59.25/59.32 cnf(943,plain,
% 59.25/59.32 (P1(x9431,f24(a2))),
% 59.25/59.32 inference(scs_inference,[],[65,939,941,99,104])).
% 59.25/59.32 cnf(957,plain,
% 59.25/59.32 (P8(x9571,f24(a2))),
% 59.25/59.32 inference(scs_inference,[],[943,99])).
% 59.25/59.32 cnf(1626,plain,
% 59.25/59.32 (~E(x16261,a1)+~P1(f25(x16261,x16262),f22(f21(a1)))),
% 59.25/59.32 inference(scs_inference,[],[341,71])).
% 59.25/59.32 cnf(1627,plain,
% 59.25/59.32 (~P1(f25(a1,x16271),f22(f21(a1)))),
% 59.25/59.32 inference(equality_inference,[],[1626])).
% 59.25/59.32 cnf(6459,plain,
% 59.25/59.32 (~P1(a1,f26(a1,f22(a1)))),
% 59.25/59.32 inference(scs_inference,[],[64,829,1627,363,957,66,152,2,75,85,86,96,97,129,83,111,71,69,103,93,113])).
% 59.25/59.32 cnf(6464,plain,
% 59.25/59.32 (~P1(a8,f25(a2,a2))),
% 59.25/59.32 inference(scs_inference,[],[64,829,1627,363,957,66,152,2,75,85,86,96,97,129,83,111,71,69,103,93,113,98,317,88])).
% 59.25/59.32 cnf(7023,plain,
% 59.25/59.32 ($false),
% 59.25/59.32 inference(scs_inference,[],[6464,6459,144,86,97,85]),
% 59.25/59.32 ['proof']).
% 59.25/59.33 % SZS output end Proof
% 59.25/59.33 % Total time :58.630000s
%------------------------------------------------------------------------------