%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV464+1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n025.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:24 EDT 2024
% Result : Theorem 0.56s 0.84s
% Output : CNFRefutation 0.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SWV464+1 : TPTP v8.2.0. Released v4.0.0.
% 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n025.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu Jun 20 17:31:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.60 start to proof:theBenchmark
% 0.56/0.83 %-------------------------------------------
% 0.56/0.83 % File :CSE---1.7
% 0.56/0.83 % Problem :theBenchmark
% 0.56/0.83 % Transform :cnf
% 0.56/0.83 % Format :tptp:raw
% 0.56/0.83 % Command :java -jar mcs_scs.jar %d %s
% 0.56/0.83
% 0.56/0.83 % Result :Theorem 0.160000s
% 0.56/0.83 % Output :CNFRefutation 0.160000s
% 0.56/0.83 %-------------------------------------------
% 0.56/0.83 %------------------------------------------------------------------------------
% 0.56/0.83 % File : SWV464+1 : TPTP v8.2.0. Released v4.0.0.
% 0.56/0.83 % Domain : Software Verification
% 0.56/0.83 % Problem : Establishing that there cannot be two leaders, part i52_p46
% 0.56/0.83 % Version : [Sve07] axioms : Especial.
% 0.56/0.83 % English :
% 0.56/0.83
% 0.56/0.83 % Refs : [Sto97] Stoller (1997), Leader Election in Distributed Systems
% 0.56/0.83 % : [Sve07] Svensson (2007), Email to Koen Claessen
% 0.56/0.83 % : [Sve08] Svensson (2008), A Semi-Automatic Correctness Proof Pr
% 0.56/0.83 % Source : [Sve07]
% 0.56/0.83 % Names : stoller_i52_p46 [Sve07]
% 0.56/0.83
% 0.56/0.83 % Status : Theorem
% 0.56/0.83 % Rating : 0.31 v8.2.0, 0.33 v7.5.0, 0.31 v7.4.0, 0.27 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.26 v7.0.0, 0.30 v6.4.0, 0.35 v6.3.0, 0.38 v6.2.0, 0.44 v6.1.0, 0.47 v6.0.0, 0.43 v5.5.0, 0.56 v5.4.0, 0.57 v5.3.0, 0.63 v5.2.0, 0.45 v5.1.0, 0.52 v5.0.0, 0.58 v4.1.0, 0.57 v4.0.0
% 0.56/0.83 % Syntax : Number of formulae : 67 ( 40 unt; 0 def)
% 0.56/0.83 % Number of atoms : 202 ( 102 equ)
% 0.56/0.83 % Maximal formula atoms : 91 ( 3 avg)
% 0.56/0.83 % Number of connectives : 200 ( 65 ~; 10 |; 78 &)
% 0.56/0.83 % ( 13 <=>; 34 =>; 0 <=; 0 <~>)
% 0.56/0.83 % Maximal formula depth : 32 ( 4 avg)
% 0.56/0.83 % Maximal term depth : 4 ( 2 avg)
% 0.56/0.83 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty)
% 0.56/0.83 % Number of functors : 33 ( 33 usr; 16 con; 0-2 aty)
% 0.56/0.83 % Number of variables : 165 ( 164 !; 1 ?)
% 0.56/0.83 % SPC : FOF_THM_RFO_SEQ
% 0.56/0.83
% 0.56/0.83 % Comments :
% 0.56/0.83 %------------------------------------------------------------------------------
% 0.56/0.83 %----Include axioms for verification of Stoller's leader election algorithm
% 0.56/0.83 include('Axioms/SWV011+0.ax').
% 0.56/0.83 %------------------------------------------------------------------------------
% 0.56/0.83 fof(conj,conjecture,
% 0.56/0.83 ! [V,W,X,Y] :
% 0.56/0.83 ( ( ! [Z,Pid0] :
% 0.56/0.83 ( elem(m_Ldr(Pid0),queue(host(Z)))
% 0.56/0.83 => ~ leq(host(Z),host(Pid0)) )
% 0.56/0.83 & ! [Z,Pid0] :
% 0.56/0.83 ( elem(m_Down(Pid0),queue(host(Z)))
% 0.56/0.83 => host(Pid0) != host(Z) )
% 0.56/0.83 & ! [Z,Pid0] :
% 0.56/0.83 ( elem(m_Halt(Pid0),queue(host(Z)))
% 0.56/0.83 => ~ leq(host(Z),host(Pid0)) )
% 0.56/0.83 & ! [Z,Pid20,Pid0] :
% 0.56/0.83 ( elem(m_Ack(Pid0,Z),queue(host(Pid20)))
% 0.56/0.83 => ~ leq(host(Z),host(Pid0)) )
% 0.56/0.83 & ! [Z,Pid0] :
% 0.56/0.83 ( ( Pid0 != Z
% 0.56/0.83 & host(Pid0) = host(Z) )
% 0.56/0.83 => ( ~ setIn(Z,alive)
% 0.56/0.83 | ~ setIn(Pid0,alive) ) )
% 0.56/0.83 & ! [Z,Pid0] :
% 0.56/0.83 ( ( setIn(Pid0,alive)
% 0.56/0.83 & elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
% 0.56/0.83 => leq(host(Z),index(pendack,host(Pid0))) )
% 0.56/0.83 & ! [Z,Pid0] :
% 0.56/0.83 ( ( setIn(Pid0,alive)
% 0.56/0.83 & index(status,host(Pid0)) = elec_1 )
% 0.56/0.83 => ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
% 0.56/0.83 & ! [Z] :
% 0.56/0.83 ( ( ( index(status,host(Z)) = elec_1
% 0.56/0.83 | index(status,host(Z)) = elec_2 )
% 0.56/0.83 & setIn(Z,alive) )
% 0.56/0.83 => index(elid,host(Z)) = Z )
% 0.56/0.83 & ! [Z,Pid20,Pid0] :
% 0.56/0.83 ( ( setIn(Pid0,alive)
% 0.56/0.84 & elem(m_Down(Pid20),queue(host(Pid0)))
% 0.56/0.84 & host(Pid20) = host(Z) )
% 0.56/0.84 => ~ ( setIn(Z,alive)
% 0.56/0.84 & index(ldr,host(Z)) = host(Z)
% 0.56/0.84 & index(status,host(Z)) = norm ) )
% 0.56/0.84 & ! [Z,Pid0] :
% 0.56/0.84 ( ( ~ leq(host(Z),host(Pid0))
% 0.56/0.84 & setIn(Z,alive)
% 0.56/0.84 & setIn(Pid0,alive)
% 0.56/0.84 & index(status,host(Z)) = elec_2
% 0.56/0.84 & index(status,host(Pid0)) = elec_2 )
% 0.56/0.84 => leq(index(pendack,host(Pid0)),host(Z)) )
% 0.56/0.84 & ! [Z,Pid20,Pid0] :
% 0.56/0.84 ( ( setIn(Z,alive)
% 0.56/0.84 & setIn(Pid0,alive)
% 0.56/0.84 & host(Pid0) = host(Pid20)
% 0.56/0.84 & index(status,host(Z)) = elec_2
% 0.56/0.84 & index(status,host(Pid0)) = elec_2 )
% 0.56/0.84 => ~ elem(m_Ack(Z,Pid20),queue(host(Z))) )
% 0.56/0.84 & ! [Z,Pid0] :
% 0.56/0.84 ( ( ~ leq(host(Z),host(Pid0))
% 0.56/0.84 & setIn(Z,alive)
% 0.56/0.84 & setIn(Pid0,alive)
% 0.56/0.84 & index(status,host(Z)) = elec_2
% 0.56/0.84 & index(status,host(Pid0)) = elec_2 )
% 0.56/0.84 => ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) )
% 0.56/0.84 & ! [Z,Pid20,Pid0] :
% 0.56/0.84 ( ( ~ leq(index(pendack,host(Pid0)),host(Z))
% 0.56/0.84 & setIn(Pid0,alive)
% 0.56/0.84 & elem(m_Halt(Pid0),queue(host(Pid20)))
% 0.56/0.84 & index(status,host(Pid0)) = elec_2 )
% 0.56/0.84 => ~ ( setIn(Z,alive)
% 0.56/0.84 & index(ldr,host(Z)) = host(Z)
% 0.56/0.84 & index(status,host(Z)) = norm ) )
% 0.56/0.84 & ! [Z,Pid30,Pid20,Pid0] :
% 0.56/0.84 ( ( ! [V0] :
% 0.56/0.84 ( ( ~ leq(host(Pid0),V0)
% 0.56/0.84 & leq(s(zero),V0) )
% 0.56/0.84 => ( setIn(V0,index(down,host(Pid0)))
% 0.56/0.84 | V0 = host(Pid20) ) )
% 0.56/0.84 & elem(m_Down(Pid20),queue(host(Pid0)))
% 0.56/0.84 & host(Pid0) = nbr_proc
% 0.56/0.84 & host(Pid0) = host(Pid30)
% 0.56/0.84 & index(status,host(Pid0)) = elec_1 )
% 0.56/0.84 => ~ ( setIn(Z,alive)
% 0.56/0.84 & elem(m_Down(Pid30),queue(host(Z))) ) )
% 0.56/0.84 & ! [Z,Pid30,Pid20,Pid0] :
% 0.56/0.84 ( ( setIn(Pid0,alive)
% 0.56/0.84 & elem(m_Down(Pid20),queue(host(Pid0)))
% 0.56/0.84 & elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
% 0.56/0.84 & leq(nbr_proc,s(index(pendack,host(Pid0))))
% 0.56/0.84 & index(status,host(Pid0)) = elec_2
% 0.56/0.84 & host(Pid30) = index(pendack,host(Pid0))
% 0.56/0.84 & host(Pid20) = s(index(pendack,host(Pid0))) )
% 0.56/0.84 => ~ ( setIn(Z,alive)
% 0.56/0.84 & index(ldr,host(Z)) = host(Z)
% 0.56/0.84 & index(status,host(Z)) = norm ) )
% 0.56/0.84 & queue(host(X)) = cons(m_Ack(W,Y),V) )
% 0.56/0.84 => ( setIn(X,alive)
% 0.56/0.84 => ( ( index(elid,host(X)) = W
% 0.56/0.84 & index(status,host(X)) = elec_2
% 0.56/0.84 & host(Y) = index(pendack,host(X)) )
% 0.56/0.84 => ( ~ leq(nbr_proc,index(pendack,host(X)))
% 0.56/0.84 => ! [Z,W0,X0,Y0] :
% 0.56/0.84 ( s(index(pendack,host(X))) = host(Y0)
% 0.56/0.84 => ( host(X) != host(Y0)
% 0.56/0.84 => ( ( setIn(Y0,alive)
% 0.56/0.84 & leq(nbr_proc,s(index(pendack,host(Y0))))
% 0.56/0.84 & elem(m_Down(X0),snoc(queue(host(Y0)),m_Halt(X)))
% 0.56/0.84 & elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Halt(X)))
% 0.56/0.84 & index(status,host(Y0)) = elec_2
% 0.56/0.84 & host(W0) = index(pendack,host(Y0))
% 0.56/0.84 & host(X0) = s(index(pendack,host(Y0))) )
% 0.56/0.84 => ~ ( setIn(Z,alive)
% 0.56/0.84 & index(ldr,host(Z)) = host(Z)
% 0.56/0.84 & index(status,host(Z)) = norm ) ) ) ) ) ) ) ) ).
% 0.56/0.84
% 0.56/0.84 %------------------------------------------------------------------------------
% 0.56/0.84 %-------------------------------------------
% 0.56/0.84 % Proof found
% 0.56/0.84 % SZS status Theorem for theBenchmark
% 0.56/0.84 % SZS output start Proof
% 0.56/0.84 %ClaNum:178(EqnAxiom:50)
% 0.56/0.84 %VarNum:560(SingletonVarNum:295)
% 0.56/0.84 %MaxLitNum:11
% 0.56/0.84 %MaxfuncDepth:3
% 0.56/0.84 %SharedTerms:72
% 0.56/0.84 %goalClause: 54 55 56 58 59 60 61 63 64 65 75 76 77 78 80 81 88 110
% 0.56/0.84 %singleGoalClaCount:18
% 0.56/0.84 [51]P1(a1)
% 0.56/0.84 [54]P5(a4,a5)
% 0.56/0.84 [55]P5(a21,a5)
% 0.56/0.84 [56]P5(a6,a5)
% 0.56/0.84 [81]P4(a4,a22,a15,a14)
% 0.56/0.84 [82]~E(a9,a7)
% 0.56/0.84 [83]~E(a46,a9)
% 0.56/0.84 [84]~E(a46,a7)
% 0.56/0.84 [85]~E(a9,a31)
% 0.56/0.84 [86]~E(a31,a7)
% 0.56/0.84 [87]~E(a46,a31)
% 0.56/0.84 [99]~P5(a36,a5)
% 0.56/0.84 [62]P2(f40(a44),a32)
% 0.56/0.84 [88]~E(f23(a6),f23(a4))
% 0.56/0.84 [58]E(f25(a39,f23(a4)),a7)
% 0.56/0.84 [59]E(f25(a39,f23(a21)),a31)
% 0.56/0.84 [60]E(f25(a39,f23(a6)),a7)
% 0.56/0.84 [61]E(f25(a11,f23(a4)),a14)
% 0.56/0.84 [63]E(f25(a37,f23(a4)),f23(a22))
% 0.56/0.84 [64]E(f25(a37,f23(a6)),f23(a12))
% 0.56/0.84 [65]E(f25(a26,f23(a21)),f23(a21))
% 0.56/0.84 [77]P3(f3(a13),f42(f41(f23(a6)),f2(a4)))
% 0.56/0.84 [80]P3(f29(a6,a12),f42(f41(f23(a6)),f2(a4)))
% 0.56/0.84 [110]~P2(a32,f25(a37,f23(a4)))
% 0.56/0.84 [75]E(f40(f25(a37,f23(a6))),f23(a13))
% 0.56/0.84 [76]E(f40(f25(a37,f23(a4))),f23(a6))
% 0.56/0.84 [78]P2(a32,f40(f25(a37,f23(a6))))
% 0.56/0.84 [57]P2(x571,x571)
% 0.56/0.84 [100]~P3(x1001,a1)
% 0.56/0.84 [101]~P5(x1011,a43)
% 0.56/0.84 [66]P2(f23(x661),a32)
% 0.56/0.84 [67]P2(f40(a44),f23(x671))
% 0.56/0.84 [68]E(f42(a1,x681),f8(x681,a1))
% 0.56/0.84 [69]P1(f8(x691,a1))
% 0.56/0.84 [70]P1(f42(a1,x701))
% 0.56/0.84 [109]~P2(f40(x1091),x1091)
% 0.56/0.84 [52]E(f30(f2(x521)),x521)
% 0.56/0.84 [53]E(f30(f3(x531)),x531)
% 0.56/0.84 [89]~E(f3(x891),f2(x892))
% 0.56/0.84 [90]~E(f33(x901),f3(x902))
% 0.56/0.84 [91]~E(f33(x911),f2(x912))
% 0.56/0.84 [92]~E(f34(x921),f3(x922))
% 0.56/0.84 [93]~E(f34(x931),f2(x932))
% 0.56/0.84 [94]~E(f34(x941),f33(x942))
% 0.56/0.84 [95]~E(f35(x951),f3(x952))
% 0.56/0.84 [96]~E(f35(x961),f34(x962))
% 0.56/0.84 [97]~E(f35(x971),f2(x972))
% 0.56/0.84 [98]~E(f35(x981),f33(x982))
% 0.56/0.84 [102]~E(f8(x1021,x1022),a1)
% 0.56/0.84 [103]~E(f42(x1031,x1032),a1)
% 0.56/0.84 [71]E(f24(f8(x711,x712)),x711)
% 0.56/0.84 [72]E(f45(f8(x721,x722)),x722)
% 0.56/0.84 [73]E(f27(f42(x731,x732)),x732)
% 0.56/0.84 [74]E(f28(f42(x741,x742)),x741)
% 0.56/0.84 [104]~E(f29(x1041,x1042),f2(x1043))
% 0.56/0.84 [105]~E(f29(x1051,x1052),f3(x1053))
% 0.56/0.84 [106]~E(f29(x1061,x1062),f33(x1063))
% 0.56/0.84 [107]~E(f29(x1071,x1072),f34(x1073))
% 0.56/0.84 [108]~E(f29(x1081,x1082),f35(x1083))
% 0.56/0.84 [79]E(f42(f8(x791,x792),x793),f8(x791,f42(x792,x793)))
% 0.56/0.84 [120]E(x1201,a1)+E(f8(f24(x1201),f45(x1201)),x1201)
% 0.56/0.84 [121]E(x1211,a1)+E(f42(f28(x1211),f27(x1211)),x1211)
% 0.56/0.84 [119]~E(x1191,x1192)+P2(x1191,x1192)
% 0.56/0.84 [122]P2(x1222,x1221)+P2(x1221,x1222)
% 0.56/0.84 [111]P6(x1111)+~E(x1111,f2(x1112))
% 0.56/0.84 [112]P6(x1121)+~E(x1121,f3(x1122))
% 0.56/0.84 [113]E(x1131,x1132)+~E(f2(x1131),f2(x1132))
% 0.56/0.84 [114]E(x1141,x1142)+~E(f3(x1141),f3(x1142))
% 0.56/0.84 [115]E(x1151,x1152)+~E(f33(x1151),f33(x1152))
% 0.56/0.84 [116]E(x1161,x1162)+~E(f34(x1161),f34(x1162))
% 0.56/0.84 [117]E(x1171,x1172)+~E(f35(x1171),f35(x1172))
% 0.56/0.84 [128]~P2(x1281,x1282)+P2(x1281,f40(x1282))
% 0.56/0.84 [134]~P2(x1341,x1342)+P2(f40(x1341),f40(x1342))
% 0.56/0.84 [137]P1(x1371)+~P1(f8(x1372,x1371))
% 0.56/0.84 [138]P1(x1381)+~P1(f42(x1381,x1382))
% 0.56/0.84 [139]P2(x1391,x1392)+~P2(f40(x1391),f40(x1392))
% 0.56/0.84 [125]~E(f23(x1251),f23(x1252))+~E(f40(f23(x1251)),f23(x1252))
% 0.56/0.84 [135]~P1(x1351)+P1(f42(x1351,f34(x1352)))
% 0.56/0.84 [150]P5(x1501,a38)+~P3(f29(x1502,x1501),f41(f23(x1502)))
% 0.56/0.84 [151]P5(x1511,a38)+~P3(f29(x1511,x1512),f41(f23(x1511)))
% 0.56/0.84 [129]~E(x1291,x1292)+P3(x1291,f8(x1292,x1293))
% 0.56/0.84 [130]~E(x1301,x1303)+P3(x1301,f42(x1302,x1303))
% 0.56/0.84 [141]~P3(x1411,x1413)+P3(x1411,f8(x1412,x1413))
% 0.56/0.84 [142]~P3(x1421,x1422)+P3(x1421,f42(x1422,x1423))
% 0.56/0.84 [149]~P1(x1491)+P1(f42(x1491,f29(x1492,x1493)))
% 0.56/0.84 [131]E(x1311,x1312)+~E(f29(x1313,x1311),f29(x1314,x1312))
% 0.56/0.84 [132]E(x1321,x1322)+~E(f29(x1321,x1323),f29(x1322,x1324))
% 0.56/0.84 [159]~P4(x1591,x1593,x1594,x1592)+E(f41(f23(x1591)),f8(f29(x1592,x1593),x1594))
% 0.56/0.84 [124]~P6(x1241)+E(f3(f18(x1241)),x1241)+E(f2(f16(x1241)),x1241)
% 0.56/0.84 [133]~P2(x1332,x1331)+~P2(x1331,x1332)+E(x1331,x1332)
% 0.56/0.84 [126]~P1(x1262)+P6(x1261)+P1(f8(x1261,x1262))
% 0.56/0.84 [127]~P1(x1272)+P6(x1271)+P1(f42(x1272,x1271))
% 0.56/0.84 [136]P2(x1361,x1362)+E(x1361,f40(x1362))+~P2(x1361,f40(x1362))
% 0.56/0.84 [143]~P1(x1432)+P1(f8(x1431,x1432))+P6(f19(x1431,x1432))
% 0.56/0.84 [144]~P1(x1442)+P1(f42(x1442,x1441))+P6(f20(x1441,x1442))
% 0.56/0.84 [145]~P1(x1452)+P3(f19(x1451,x1452),x1452)+P1(f8(x1451,x1452))
% 0.56/0.84 [146]~P1(x1461)+P3(f20(x1462,x1461),x1461)+P1(f42(x1461,x1462))
% 0.56/0.84 [157]~P1(x1572)+~P2(f30(x1571),f30(f19(x1571,x1572)))+P1(f8(x1571,x1572))
% 0.56/0.84 [158]~P1(x1581)+~P2(f30(f20(x1582,x1581)),f30(x1582))+P1(f42(x1581,x1582))
% 0.56/0.84 [152]~P1(x1522)+P1(f8(x1521,x1522))+E(f23(f30(f19(x1521,x1522))),f23(f30(x1521)))
% 0.56/0.84 [153]~P1(x1532)+P1(f42(x1532,x1531))+E(f23(f30(f20(x1531,x1532))),f23(f30(x1531)))
% 0.56/0.84 [140]~P2(x1401,x1403)+P2(x1401,x1402)+~P2(x1403,x1402)
% 0.56/0.84 [147]E(x1471,x1472)+P3(x1471,x1473)+~P3(x1471,f42(x1473,x1472))
% 0.56/0.84 [148]E(x1481,x1482)+P3(x1481,x1483)+~P3(x1481,f8(x1482,x1483))
% 0.56/0.84 [163]~P4(x1633,x1634,x1635,x1636)+~E(f23(x1631),f23(x1632))+~P3(f3(x1631),f41(f23(x1632)))
% 0.56/0.84 [164]~P4(x1641,x1642,x1643,x1644)+~P2(f23(x1645),f23(x1646))+~P3(f2(x1646),f41(f23(x1645)))
% 0.56/0.84 [165]~P4(x1651,x1652,x1653,x1654)+~P2(f23(x1655),f23(x1656))+~P3(f34(x1656),f41(f23(x1655)))
% 0.56/0.84 [166]~P4(x1661,x1662,x1663,x1664)+~P2(f23(x1665),f23(x1666))+~P3(f29(x1666,x1665),f41(f23(x1667)))
% 0.56/0.84 [154]P2(x1541,x1542)+~E(f23(x1541),f23(x1542))+~P3(f3(x1542),x1543)+~P1(f8(f2(x1541),x1543))
% 0.56/0.84 [161]~P4(x1612,x1613,x1614,x1615)+~P5(x1611,a5)+E(f25(a11,f23(x1611)),x1611)+~E(f25(a39,f23(x1611)),a9)
% 0.56/0.84 [162]~P4(x1622,x1623,x1624,x1625)+~P5(x1621,a5)+E(f25(a11,f23(x1621)),x1621)+~E(f25(a39,f23(x1621)),a7)
% 0.56/0.84 [167]~P4(x1672,x1673,x1674,x1675)+~P5(x1671,a5)+~P3(f29(x1671,x1676),f41(f23(x1671)))+~E(f25(a39,f23(x1671)),a9)
% 0.56/0.84 [168]~P4(x1683,x1684,x1685,x1686)+~P5(x1682,a5)+~P3(f29(x1682,x1681),f41(f23(x1682)))+P2(f23(x1681),f25(a37,f23(x1682)))
% 0.56/0.84 [160]E(x1601,x1602)+~P4(x1603,x1604,x1605,x1606)+~E(f23(x1601),f23(x1602))+~P5(x1602,a5)+~P5(x1601,a5)
% 0.56/0.84 [155]~P6(x1551)+~P6(x1552)+~P3(x1552,x1553)+P2(f30(x1551),f30(x1552))+~P1(f8(x1551,x1553))+~E(f23(f30(x1552)),f23(f30(x1551)))
% 0.56/0.84 [156]~P6(x1562)+~P6(x1561)+~P3(x1561,x1563)+P2(f30(x1561),f30(x1562))+~P1(f42(x1563,x1562))+~E(f23(f30(x1561)),f23(f30(x1562)))
% 0.56/0.84 [170]~P4(x1703,x1704,x1705,x1706)+~P5(x1702,a5)+~P5(x1701,a5)+P2(f23(x1701),f23(x1702))+P2(f25(a37,f23(x1702)),f23(x1701))+~E(f25(a39,f23(x1701)),a7)+~E(f25(a39,f23(x1702)),a7)
% 0.56/0.84 [173]~P4(x1733,x1734,x1735,x1736)+~P5(x1732,a5)+~P5(x1731,a5)+P2(f23(x1731),f23(x1732))+~P2(f25(a37,f23(x1731)),f25(a37,f23(x1732)))+~E(f25(a39,f23(x1731)),a7)+~E(f25(a39,f23(x1732)),a7)
% 0.56/0.84 [169]~P4(x1694,x1695,x1696,x1697)+~P5(x1692,a5)+~E(f23(x1691),f23(x1692))+~P5(x1693,a5)+~P3(f3(x1691),f41(f23(x1693)))+~E(f25(a26,f23(x1692)),f23(x1692))+~E(f25(a39,f23(x1692)),a31)
% 0.56/0.84 [171]~P4(x1714,x1715,x1716,x1717)+~P5(x1711,a5)+~P5(x1713,a5)+~E(f23(x1711),f23(x1712))+~P3(f29(x1713,x1712),f41(f23(x1713)))+~E(f25(a39,f23(x1711)),a7)+~E(f25(a39,f23(x1713)),a7)
% 0.56/0.84 [172]~P4(x1723,x1724,x1725,x1726)+~P5(x1722,a5)+~P5(x1721,a5)+~P3(f2(x1721),f41(f23(x1727)))+P2(f25(a37,f23(x1721)),f23(x1722))+~E(f25(a26,f23(x1722)),f23(x1722))+~E(f25(a39,f23(x1721)),a7)+~E(f25(a39,f23(x1722)),a31)
% 0.56/0.84 [175]~P4(x1756,x1755,x1754,x1753)+~P5(x1757,a5)+~E(f17(x1753,x1754,x1755,x1756,x1757,x1752,x1758,x1751),f23(x1758))+~E(f23(x1752),f23(x1751))+~P3(f3(x1752),f41(f23(x1757)))+~P3(f3(x1758),f41(f23(x1751)))+~E(f23(x1751),a32)+~E(f25(a39,f23(x1751)),a9)
% 0.56/0.84 [176]~P4(x1764,x1763,x1762,x1761)+~E(f23(x1766),f23(x1768))+~P5(x1765,a5)+P2(f40(a44),f17(x1761,x1762,x1763,x1764,x1765,x1766,x1767,x1768))+~E(f23(x1768),a32)+~P3(f3(x1767),f41(f23(x1768)))+~P3(f3(x1766),f41(f23(x1765)))+~E(f25(a39,f23(x1768)),a9)
% 0.56/0.84 [177]~P4(x1774,x1775,x1776,x1777)+~P2(f23(x1771),f17(x1777,x1776,x1775,x1774,x1773,x1772,x1778,x1771))+~E(f23(x1771),f23(x1772))+~P5(x1773,a5)+~P3(f3(x1772),f41(f23(x1773)))+~E(f23(x1771),a32)+~P3(f3(x1778),f41(f23(x1771)))+~E(f25(a39,f23(x1771)),a9)
% 0.56/0.84 [178]~P4(x1784,x1785,x1786,x1787)+~E(f23(x1782),f23(x1781))+~P5(x1783,a5)+~P3(f3(x1782),f41(f23(x1783)))+~E(f23(x1781),a32)+~P3(f3(x1788),f41(f23(x1781)))+~P5(f17(x1787,x1786,x1785,x1784,x1783,x1782,x1788,x1781),f25(a10,f23(x1781)))+~E(f25(a39,f23(x1781)),a9)
% 0.56/0.84 [174]~P4(x1745,x1746,x1747,x1748)+~P5(x1741,a5)+~P5(x1742,a5)+~P3(f29(x1742,x1743),f41(f23(x1742)))+~P3(f3(x1744),f41(f23(x1742)))+~E(f25(a26,f23(x1741)),f23(x1741))+~E(f23(x1743),f25(a37,f23(x1742)))+~E(f23(x1744),f40(f25(a37,f23(x1742))))+~E(f25(a39,f23(x1741)),a31)+~E(f25(a39,f23(x1742)),a7)+~P2(a32,f40(f25(a37,f23(x1742))))
% 0.56/0.84 %EqnAxiom
% 0.56/0.84 [1]E(x11,x11)
% 0.56/0.84 [2]E(x22,x21)+~E(x21,x22)
% 0.56/0.84 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.56/0.84 [4]~E(x41,x42)+E(f2(x41),f2(x42))
% 0.56/0.84 [5]~E(x51,x52)+E(f30(x51),f30(x52))
% 0.56/0.85 [6]~E(x61,x62)+E(f3(x61),f3(x62))
% 0.56/0.85 [7]~E(x71,x72)+E(f17(x71,x73,x74,x75,x76,x77,x78,x79),f17(x72,x73,x74,x75,x76,x77,x78,x79))
% 0.56/0.85 [8]~E(x81,x82)+E(f17(x83,x81,x84,x85,x86,x87,x88,x89),f17(x83,x82,x84,x85,x86,x87,x88,x89))
% 0.56/0.85 [9]~E(x91,x92)+E(f17(x93,x94,x91,x95,x96,x97,x98,x99),f17(x93,x94,x92,x95,x96,x97,x98,x99))
% 0.56/0.85 [10]~E(x101,x102)+E(f17(x103,x104,x105,x101,x106,x107,x108,x109),f17(x103,x104,x105,x102,x106,x107,x108,x109))
% 0.56/0.85 [11]~E(x111,x112)+E(f17(x113,x114,x115,x116,x111,x117,x118,x119),f17(x113,x114,x115,x116,x112,x117,x118,x119))
% 0.56/0.85 [12]~E(x121,x122)+E(f17(x123,x124,x125,x126,x127,x121,x128,x129),f17(x123,x124,x125,x126,x127,x122,x128,x129))
% 0.56/0.85 [13]~E(x131,x132)+E(f17(x133,x134,x135,x136,x137,x138,x131,x139),f17(x133,x134,x135,x136,x137,x138,x132,x139))
% 0.56/0.85 [14]~E(x141,x142)+E(f17(x143,x144,x145,x146,x147,x148,x149,x141),f17(x143,x144,x145,x146,x147,x148,x149,x142))
% 0.56/0.85 [15]~E(x151,x152)+E(f23(x151),f23(x152))
% 0.56/0.85 [16]~E(x161,x162)+E(f25(x161,x163),f25(x162,x163))
% 0.56/0.85 [17]~E(x171,x172)+E(f25(x173,x171),f25(x173,x172))
% 0.56/0.85 [18]~E(x181,x182)+E(f41(x181),f41(x182))
% 0.56/0.85 [19]~E(x191,x192)+E(f42(x191,x193),f42(x192,x193))
% 0.56/0.85 [20]~E(x201,x202)+E(f42(x203,x201),f42(x203,x202))
% 0.56/0.85 [21]~E(x211,x212)+E(f29(x211,x213),f29(x212,x213))
% 0.56/0.85 [22]~E(x221,x222)+E(f29(x223,x221),f29(x223,x222))
% 0.56/0.85 [23]~E(x231,x232)+E(f8(x231,x233),f8(x232,x233))
% 0.56/0.85 [24]~E(x241,x242)+E(f8(x243,x241),f8(x243,x242))
% 0.56/0.85 [25]~E(x251,x252)+E(f20(x251,x253),f20(x252,x253))
% 0.56/0.85 [26]~E(x261,x262)+E(f20(x263,x261),f20(x263,x262))
% 0.56/0.85 [27]~E(x271,x272)+E(f33(x271),f33(x272))
% 0.56/0.85 [28]~E(x281,x282)+E(f40(x281),f40(x282))
% 0.56/0.85 [29]~E(x291,x292)+E(f34(x291),f34(x292))
% 0.56/0.85 [30]~E(x301,x302)+E(f19(x301,x303),f19(x302,x303))
% 0.56/0.85 [31]~E(x311,x312)+E(f19(x313,x311),f19(x313,x312))
% 0.56/0.85 [32]~E(x321,x322)+E(f27(x321),f27(x322))
% 0.56/0.85 [33]~E(x331,x332)+E(f35(x331),f35(x332))
% 0.56/0.85 [34]~E(x341,x342)+E(f18(x341),f18(x342))
% 0.56/0.85 [35]~E(x351,x352)+E(f24(x351),f24(x352))
% 0.56/0.85 [36]~E(x361,x362)+E(f16(x361),f16(x362))
% 0.56/0.85 [37]~E(x371,x372)+E(f28(x371),f28(x372))
% 0.56/0.85 [38]~E(x381,x382)+E(f45(x381),f45(x382))
% 0.56/0.85 [39]~P1(x391)+P1(x392)+~E(x391,x392)
% 0.56/0.85 [40]P5(x402,x403)+~E(x401,x402)+~P5(x401,x403)
% 0.56/0.85 [41]P5(x413,x412)+~E(x411,x412)+~P5(x413,x411)
% 0.56/0.85 [42]P2(x422,x423)+~E(x421,x422)+~P2(x421,x423)
% 0.56/0.85 [43]P2(x433,x432)+~E(x431,x432)+~P2(x433,x431)
% 0.56/0.85 [44]P3(x442,x443)+~E(x441,x442)+~P3(x441,x443)
% 0.56/0.85 [45]P3(x453,x452)+~E(x451,x452)+~P3(x453,x451)
% 0.56/0.85 [46]P4(x462,x463,x464,x465)+~E(x461,x462)+~P4(x461,x463,x464,x465)
% 0.56/0.85 [47]P4(x473,x472,x474,x475)+~E(x471,x472)+~P4(x473,x471,x474,x475)
% 0.56/0.85 [48]P4(x483,x484,x482,x485)+~E(x481,x482)+~P4(x483,x484,x481,x485)
% 0.56/0.85 [49]P4(x493,x494,x495,x492)+~E(x491,x492)+~P4(x493,x494,x495,x491)
% 0.56/0.85 [50]~P6(x501)+P6(x502)+~E(x501,x502)
% 0.56/0.85
% 0.56/0.85 %-------------------------------------------
% 0.56/0.85 cnf(179,plain,
% 0.56/0.85 (P6(f2(x1791))),
% 0.56/0.85 inference(equality_inference,[],[111])).
% 0.56/0.85 cnf(187,plain,
% 0.56/0.85 (P3(x1871,f8(x1871,x1872))),
% 0.56/0.85 inference(equality_inference,[],[129])).
% 0.56/0.85 cnf(188,plain,
% 0.56/0.85 (P3(x1881,f42(x1882,x1881))),
% 0.56/0.85 inference(equality_inference,[],[130])).
% 0.56/0.85 cnf(195,plain,
% 0.56/0.85 (~P4(x1951,x1952,x1953,x1954)+~P3(f3(x1955),f41(f23(x1955)))),
% 0.56/0.85 inference(equality_inference,[],[163])).
% 0.56/0.85 cnf(196,plain,
% 0.56/0.85 (~P3(f3(x1961),f41(f23(x1961)))),
% 0.56/0.85 inference(scs_inference,[],[81,195])).
% 0.56/0.85 cnf(202,plain,
% 0.56/0.85 (E(f30(f2(x2021)),x2021)),
% 0.56/0.85 inference(rename_variables,[],[52])).
% 0.56/0.85 cnf(207,plain,
% 0.56/0.85 (P2(f25(a37,f23(a4)),a32)),
% 0.56/0.85 inference(scs_inference,[],[88,63,110,52,202,119,2,15,111,112,122])).
% 0.56/0.85 cnf(209,plain,
% 0.56/0.85 (~P2(f40(f40(x2091)),x2091)),
% 0.56/0.85 inference(scs_inference,[],[88,63,110,109,52,202,119,2,15,111,112,122,128])).
% 0.56/0.85 cnf(224,plain,
% 0.56/0.85 (P3(f29(a6,a12),f41(f23(a6)))),
% 0.56/0.85 inference(scs_inference,[],[54,88,80,63,110,58,78,187,57,179,101,109,89,104,82,99,52,202,119,2,15,111,112,122,128,3,40,41,42,43,44,124,147])).
% 0.56/0.85 cnf(227,plain,
% 0.56/0.85 (~P2(f23(a12),f23(a6))),
% 0.56/0.85 inference(scs_inference,[],[54,81,88,80,63,110,58,78,187,57,179,101,109,89,104,82,99,52,202,119,2,15,111,112,122,128,3,40,41,42,43,44,124,147,166])).
% 0.56/0.85 cnf(233,plain,
% 0.56/0.85 (~E(f23(a6),f23(a12))),
% 0.56/0.85 inference(scs_inference,[],[54,56,81,88,80,63,110,58,60,78,187,57,179,100,101,109,89,104,82,99,52,202,119,2,15,111,112,122,128,3,40,41,42,43,44,124,147,166,45,162,171])).
% 0.56/0.85 cnf(235,plain,
% 0.56/0.85 (E(f16(f2(x2351)),x2351)),
% 0.56/0.85 inference(scs_inference,[],[54,56,81,88,80,63,110,58,60,78,187,57,179,100,101,109,89,104,82,99,52,202,119,2,15,111,112,122,128,3,40,41,42,43,44,124,147,166,45,162,171,113])).
% 0.56/0.85 cnf(237,plain,
% 0.56/0.85 (P5(a12,a38)),
% 0.56/0.85 inference(scs_inference,[],[54,56,81,88,80,63,110,58,60,78,187,57,179,100,101,109,89,104,82,99,52,202,119,2,15,111,112,122,128,3,40,41,42,43,44,124,147,166,45,162,171,113,150])).
% 0.56/0.85 cnf(254,plain,
% 0.56/0.85 (~P5(x2541,a5)+E(f25(a11,f23(x2541)),x2541)+~E(f25(a39,f23(x2541)),a7)),
% 0.56/0.85 inference(scs_inference,[],[81,162])).
% 0.56/0.85 cnf(258,plain,
% 0.56/0.85 (~P2(f23(x2581),f23(x2582))+~P3(f29(x2582,x2581),f41(f23(x2583)))),
% 0.56/0.85 inference(scs_inference,[],[81,166])).
% 0.56/0.85 cnf(260,plain,
% 0.56/0.85 (~P5(x2601,a5)+~P3(f29(x2601,x2602),f41(f23(x2601)))+P2(f23(x2602),f25(a37,f23(x2601)))),
% 0.56/0.85 inference(scs_inference,[],[81,168])).
% 0.56/0.85 cnf(261,plain,
% 0.56/0.85 (~E(f23(x2611),f23(x2612))+~P5(x2612,a5)+~P5(x2613,a5)+~P3(f3(x2611),f41(f23(x2613)))+~E(f25(a26,f23(x2612)),f23(x2612))+~E(f25(a39,f23(x2612)),a31)),
% 0.56/0.85 inference(scs_inference,[],[81,169])).
% 0.56/0.85 cnf(266,plain,
% 0.56/0.85 (~P5(x2661,a5)+~P5(x2662,a5)+~P3(f29(x2662,x2663),f41(f23(x2662)))+~P3(f3(x2664),f41(f23(x2662)))+~E(f25(a26,f23(x2661)),f23(x2661))+~E(f23(x2663),f25(a37,f23(x2662)))+~E(f23(x2664),f40(f25(a37,f23(x2662))))+~E(f25(a39,f23(x2661)),a31)+~E(f25(a39,f23(x2662)),a7)+~P2(a32,f40(f25(a37,f23(x2662))))),
% 0.56/0.85 inference(scs_inference,[],[81,174])).
% 0.56/0.85 cnf(267,plain,
% 0.56/0.85 (~P3(f29(x2671,x2671),f41(f23(x2672)))),
% 0.56/0.85 inference(scs_inference,[],[57,258])).
% 0.56/0.85 cnf(270,plain,
% 0.56/0.85 (~E(f40(f40(x2701)),x2701)),
% 0.56/0.85 inference(scs_inference,[],[209,57,258,119])).
% 0.56/0.85 cnf(273,plain,
% 0.56/0.85 (E(f16(f2(x2731)),x2731)),
% 0.56/0.85 inference(rename_variables,[],[235])).
% 0.56/0.85 cnf(275,plain,
% 0.56/0.85 (~P2(f40(f40(f40(x2751))),x2751)),
% 0.56/0.85 inference(scs_inference,[],[209,235,57,258,119,111,128])).
% 0.56/0.85 cnf(276,plain,
% 0.56/0.85 (~P2(f40(f40(x2761)),x2761)),
% 0.56/0.85 inference(rename_variables,[],[209])).
% 0.56/0.85 cnf(278,plain,
% 0.56/0.85 (P2(x2781,f40(f40(x2781)))),
% 0.56/0.85 inference(scs_inference,[],[209,276,235,57,258,119,111,128,122])).
% 0.56/0.85 cnf(287,plain,
% 0.56/0.85 (P2(f23(a12),f25(a37,f23(a6)))),
% 0.56/0.85 inference(scs_inference,[],[60,56,233,209,276,235,273,224,57,258,119,111,128,122,15,112,2,254,260])).
% 0.56/0.85 cnf(288,plain,
% 0.56/0.85 (~P5(x2881,a5)+P2(f23(x2882),f25(a37,f23(x2881)))+~P3(f29(x2881,x2882),f41(f23(x2881)))),
% 0.56/0.85 inference(rename_variables,[],[260])).
% 0.56/0.85 cnf(291,plain,
% 0.56/0.85 (P3(f3(a13),f41(f23(a6)))),
% 0.56/0.85 inference(scs_inference,[],[60,77,56,78,233,209,276,235,273,224,207,57,89,258,119,111,128,122,15,112,2,254,260,140,147])).
% 0.56/0.85 cnf(301,plain,
% 0.56/0.85 (~E(f25(a37,f23(a4)),f40(f40(a32)))),
% 0.56/0.85 inference(scs_inference,[],[60,55,77,56,78,188,233,196,209,276,235,273,224,207,237,57,101,89,99,258,119,111,128,122,15,112,2,254,260,140,147,45,41,44,40,42])).
% 0.56/0.85 cnf(314,plain,
% 0.56/0.85 (~P3(f3(x3141),f41(f23(a4)))+~E(f23(x3141),f23(a21))),
% 0.56/0.85 inference(scs_inference,[],[54,60,55,77,65,59,56,78,188,233,196,209,276,235,273,224,207,67,84,237,57,101,109,89,99,258,119,111,128,122,15,112,2,254,260,140,147,45,41,44,40,42,3,43,288,136,50,133,39,261])).
% 0.56/0.85 cnf(318,plain,
% 0.56/0.85 (~P3(f3(a21),f41(f23(a4)))),
% 0.56/0.85 inference(equality_inference,[],[314])).
% 0.56/0.85 cnf(320,plain,
% 0.56/0.85 (E(f30(f3(x3201)),x3201)),
% 0.56/0.85 inference(rename_variables,[],[53])).
% 0.56/0.85 cnf(322,plain,
% 0.56/0.85 (~E(f40(f40(f40(x3221))),x3221)),
% 0.56/0.85 inference(scs_inference,[],[275,53,111,119])).
% 0.56/0.85 cnf(331,plain,
% 0.56/0.85 (P3(x3311,f8(x3311,x3312))),
% 0.56/0.85 inference(rename_variables,[],[187])).
% 0.56/0.85 cnf(346,plain,
% 0.56/0.85 (P2(f25(a37,f23(a4)),f40(f40(a32)))),
% 0.56/0.85 inference(scs_inference,[],[60,58,55,56,270,287,318,187,331,207,275,227,53,320,99,111,119,112,122,2,45,42,44,40,3,43,260,140,133,136])).
% 0.56/0.85 cnf(357,plain,
% 0.56/0.85 (E(f24(f8(x3571,x3572)),x3571)),
% 0.56/0.85 inference(rename_variables,[],[71])).
% 0.56/0.85 cnf(379,plain,
% 0.56/0.85 (~E(f23(a13),f40(f25(a37,f23(a6))))),
% 0.56/0.85 inference(scs_inference,[],[60,78,55,56,64,65,59,110,301,322,188,318,224,209,109,278,267,291,346,66,71,357,111,119,112,122,2,133,42,45,3,44,43,266])).
% 0.56/0.85 cnf(467,plain,
% 0.56/0.85 ($false),
% 0.56/0.85 inference(scs_inference,[],[75,379,2]),
% 0.56/0.85 ['proof']).
% 0.56/0.85 % SZS output end Proof
% 0.56/0.85 % Total time :0.160000s
%------------------------------------------------------------------------------