%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV463+1 : TPTP v8.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n022.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 1.04s 1.12s
% Output : CNFRefutation 1.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWV463+1 : TPTP v8.2.0. Released v4.0.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n022.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Thu Jun 20 20:33:09 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.45/0.59 start to proof:theBenchmark
% 1.04/1.11 %-------------------------------------------
% 1.04/1.11 % File :CSE---1.7
% 1.04/1.11 % Problem :theBenchmark
% 1.04/1.11 % Transform :cnf
% 1.04/1.11 % Format :tptp:raw
% 1.04/1.11 % Command :java -jar mcs_scs.jar %d %s
% 1.04/1.11
% 1.04/1.11 % Result :Theorem 0.450000s
% 1.04/1.11 % Output :CNFRefutation 0.450000s
% 1.04/1.11 %-------------------------------------------
% 1.04/1.11 %------------------------------------------------------------------------------
% 1.04/1.11 % File : SWV463+1 : TPTP v8.2.0. Released v4.0.0.
% 1.04/1.11 % Domain : Software Verification
% 1.04/1.11 % Problem : Establishing that there cannot be two leaders, part i52_p38
% 1.04/1.11 % Version : [Sve07] axioms : Especial.
% 1.04/1.11 % English :
% 1.04/1.11
% 1.04/1.11 % Refs : [Sto97] Stoller (1997), Leader Election in Distributed Systems
% 1.04/1.11 % : [Sve07] Svensson (2007), Email to Koen Claessen
% 1.04/1.11 % : [Sve08] Svensson (2008), A Semi-Automatic Correctness Proof Pr
% 1.04/1.11 % Source : [Sve07]
% 1.04/1.11 % Names : stoller_i52_p38 [Sve07]
% 1.04/1.11
% 1.04/1.11 % Status : Theorem
% 1.04/1.11 % Rating : 0.28 v8.2.0, 0.31 v8.1.0, 0.28 v7.4.0, 0.23 v7.3.0, 0.24 v7.2.0, 0.21 v7.1.0, 0.22 v7.0.0, 0.23 v6.4.0, 0.31 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.40 v6.0.0, 0.35 v5.5.0, 0.41 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.35 v5.1.0, 0.48 v5.0.0, 0.46 v4.1.0, 0.48 v4.0.0
% 1.04/1.11 % Syntax : Number of formulae : 67 ( 40 unt; 0 def)
% 1.04/1.11 % Number of atoms : 205 ( 104 equ)
% 1.04/1.11 % Maximal formula atoms : 94 ( 3 avg)
% 1.04/1.11 % Number of connectives : 203 ( 65 ~; 11 |; 78 &)
% 1.04/1.11 % ( 13 <=>; 36 =>; 0 <=; 0 <~>)
% 1.04/1.11 % Maximal formula depth : 32 ( 4 avg)
% 1.04/1.11 % Maximal term depth : 4 ( 1 avg)
% 1.04/1.11 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty)
% 1.04/1.11 % Number of functors : 34 ( 34 usr; 17 con; 0-2 aty)
% 1.04/1.11 % Number of variables : 166 ( 165 !; 1 ?)
% 1.04/1.11 % SPC : FOF_THM_RFO_SEQ
% 1.04/1.11
% 1.04/1.11 % Comments :
% 1.04/1.11 %------------------------------------------------------------------------------
% 1.04/1.11 %----Include axioms for verification of Stoller's leader election algorithm
% 1.04/1.11 include('Axioms/SWV011+0.ax').
% 1.04/1.11 %------------------------------------------------------------------------------
% 1.04/1.11 fof(conj,conjecture,
% 1.04/1.12 ! [V,W,X,Y] :
% 1.04/1.12 ( ( ! [Z,Pid0] :
% 1.04/1.12 ( elem(m_Ldr(Pid0),queue(host(Z)))
% 1.04/1.12 => ~ leq(host(Z),host(Pid0)) )
% 1.04/1.12 & ! [Z,Pid0] :
% 1.04/1.12 ( elem(m_Down(Pid0),queue(host(Z)))
% 1.04/1.12 => host(Pid0) != host(Z) )
% 1.04/1.12 & ! [Z,Pid0] :
% 1.04/1.12 ( elem(m_Halt(Pid0),queue(host(Z)))
% 1.04/1.12 => ~ leq(host(Z),host(Pid0)) )
% 1.04/1.12 & ! [Z,Pid20,Pid0] :
% 1.04/1.12 ( elem(m_Ack(Pid0,Z),queue(host(Pid20)))
% 1.04/1.12 => ~ leq(host(Z),host(Pid0)) )
% 1.04/1.12 & ! [Z,Pid0] :
% 1.04/1.12 ( ( Pid0 != Z
% 1.04/1.12 & host(Pid0) = host(Z) )
% 1.04/1.12 => ( ~ setIn(Z,alive)
% 1.04/1.12 | ~ setIn(Pid0,alive) ) )
% 1.04/1.12 & ! [Z,Pid0] :
% 1.04/1.12 ( ( setIn(Pid0,alive)
% 1.04/1.12 & elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
% 1.04/1.12 => leq(host(Z),index(pendack,host(Pid0))) )
% 1.04/1.12 & ! [Z,Pid0] :
% 1.04/1.12 ( ( setIn(Pid0,alive)
% 1.04/1.12 & index(status,host(Pid0)) = elec_1 )
% 1.04/1.12 => ~ elem(m_Ack(Pid0,Z),queue(host(Pid0))) )
% 1.04/1.12 & ! [Z] :
% 1.04/1.12 ( ( ( index(status,host(Z)) = elec_1
% 1.04/1.12 | index(status,host(Z)) = elec_2 )
% 1.04/1.12 & setIn(Z,alive) )
% 1.04/1.12 => index(elid,host(Z)) = Z )
% 1.04/1.12 & ! [Z,Pid20,Pid0] :
% 1.04/1.12 ( ( setIn(Pid0,alive)
% 1.04/1.12 & elem(m_Down(Pid20),queue(host(Pid0)))
% 1.04/1.12 & host(Pid20) = host(Z) )
% 1.04/1.12 => ~ ( setIn(Z,alive)
% 1.04/1.12 & index(ldr,host(Z)) = host(Z)
% 1.04/1.12 & index(status,host(Z)) = norm ) )
% 1.04/1.12 & ! [Z,Pid0] :
% 1.04/1.12 ( ( ~ leq(host(Z),host(Pid0))
% 1.04/1.12 & setIn(Z,alive)
% 1.04/1.12 & setIn(Pid0,alive)
% 1.04/1.12 & index(status,host(Z)) = elec_2
% 1.04/1.12 & index(status,host(Pid0)) = elec_2 )
% 1.04/1.12 => leq(index(pendack,host(Pid0)),host(Z)) )
% 1.04/1.12 & ! [Z,Pid20,Pid0] :
% 1.04/1.12 ( ( setIn(Z,alive)
% 1.04/1.12 & setIn(Pid0,alive)
% 1.04/1.12 & host(Pid0) = host(Pid20)
% 1.04/1.12 & index(status,host(Z)) = elec_2
% 1.04/1.12 & index(status,host(Pid0)) = elec_2 )
% 1.04/1.12 => ~ elem(m_Ack(Z,Pid20),queue(host(Z))) )
% 1.04/1.12 & ! [Z,Pid0] :
% 1.04/1.12 ( ( ~ leq(host(Z),host(Pid0))
% 1.04/1.12 & setIn(Z,alive)
% 1.04/1.12 & setIn(Pid0,alive)
% 1.04/1.12 & index(status,host(Z)) = elec_2
% 1.04/1.12 & index(status,host(Pid0)) = elec_2 )
% 1.04/1.12 => ~ leq(index(pendack,host(Z)),index(pendack,host(Pid0))) )
% 1.04/1.12 & ! [Z,Pid20,Pid0] :
% 1.04/1.12 ( ( ~ leq(index(pendack,host(Pid0)),host(Z))
% 1.04/1.12 & setIn(Pid0,alive)
% 1.04/1.12 & elem(m_Halt(Pid0),queue(host(Pid20)))
% 1.04/1.12 & index(status,host(Pid0)) = elec_2 )
% 1.04/1.12 => ~ ( setIn(Z,alive)
% 1.04/1.12 & index(ldr,host(Z)) = host(Z)
% 1.04/1.12 & index(status,host(Z)) = norm ) )
% 1.04/1.12 & ! [Z,Pid30,Pid20,Pid0] :
% 1.04/1.12 ( ( ! [V0] :
% 1.04/1.12 ( ( ~ leq(host(Pid0),V0)
% 1.04/1.12 & leq(s(zero),V0) )
% 1.04/1.12 => ( setIn(V0,index(down,host(Pid0)))
% 1.04/1.12 | V0 = host(Pid20) ) )
% 1.04/1.12 & elem(m_Down(Pid20),queue(host(Pid0)))
% 1.04/1.12 & host(Pid0) = nbr_proc
% 1.04/1.12 & host(Pid0) = host(Pid30)
% 1.04/1.12 & index(status,host(Pid0)) = elec_1 )
% 1.04/1.12 => ~ ( setIn(Z,alive)
% 1.04/1.12 & elem(m_Down(Pid30),queue(host(Z))) ) )
% 1.04/1.12 & ! [Z,Pid30,Pid20,Pid0] :
% 1.04/1.12 ( ( setIn(Pid0,alive)
% 1.04/1.12 & elem(m_Down(Pid20),queue(host(Pid0)))
% 1.04/1.12 & elem(m_Ack(Pid0,Pid30),queue(host(Pid0)))
% 1.04/1.12 & leq(nbr_proc,s(index(pendack,host(Pid0))))
% 1.04/1.12 & index(status,host(Pid0)) = elec_2
% 1.04/1.12 & host(Pid30) = index(pendack,host(Pid0))
% 1.04/1.12 & host(Pid20) = s(index(pendack,host(Pid0))) )
% 1.04/1.12 => ~ ( setIn(Z,alive)
% 1.04/1.12 & index(ldr,host(Z)) = host(Z)
% 1.04/1.12 & index(status,host(Z)) = norm ) )
% 1.04/1.12 & queue(host(X)) = cons(m_Ack(W,Y),V) )
% 1.04/1.12 => ( setIn(X,alive)
% 1.04/1.12 => ( ( index(elid,host(X)) = W
% 1.04/1.12 & index(status,host(X)) = elec_2
% 1.04/1.12 & host(Y) = index(pendack,host(X)) )
% 1.04/1.12 => ( leq(nbr_proc,index(pendack,host(X)))
% 1.04/1.12 => ! [Z] :
% 1.04/1.12 ( ( setIn(host(Z),index(acks,host(X)))
% 1.04/1.12 | host(Z) = host(Y) )
% 1.04/1.12 => ! [V0] :
% 1.04/1.12 ( host(X) != host(V0)
% 1.04/1.12 => ! [W0,X0,Y0] :
% 1.04/1.12 ( host(Z) = host(Y0)
% 1.04/1.12 => ( host(X) != host(Y0)
% 1.04/1.12 => ( ( setIn(Y0,alive)
% 1.04/1.12 & leq(nbr_proc,s(index(pendack,host(Y0))))
% 1.04/1.12 & elem(m_Down(X0),snoc(queue(host(Y0)),m_Ldr(X)))
% 1.04/1.12 & elem(m_Ack(Y0,W0),snoc(queue(host(Y0)),m_Ldr(X)))
% 1.04/1.12 & index(status,host(Y0)) = elec_2
% 1.04/1.12 & host(W0) = index(pendack,host(Y0))
% 1.04/1.12 & host(X0) = s(index(pendack,host(Y0))) )
% 1.04/1.12 => ~ ( setIn(V0,alive)
% 1.04/1.12 & index(ldr,host(V0)) = host(V0)
% 1.04/1.12 & index(status,host(V0)) = norm ) ) ) ) ) ) ) ) ) ) ).
% 1.04/1.12
% 1.04/1.12 %------------------------------------------------------------------------------
% 1.04/1.12 %-------------------------------------------
% 1.04/1.12 % Proof found
% 1.04/1.12 % SZS status Theorem for theBenchmark
% 1.04/1.12 % SZS output start Proof
% 1.04/1.12 %ClaNum:180(EqnAxiom:50)
% 1.04/1.12 %VarNum:560(SingletonVarNum:295)
% 1.04/1.12 %MaxLitNum:11
% 1.04/1.12 %MaxfuncDepth:3
% 1.04/1.12 %SharedTerms:78
% 1.04/1.12 %goalClause: 52 55 56 57 59 60 61 62 64 65 66 76 77 78 79 81 82 89 90 137
% 1.04/1.12 %singleGoalClaCount:19
% 1.04/1.12 [51]P1(a1)
% 1.04/1.12 [55]P5(a14,a4)
% 1.04/1.12 [56]P5(a6,a4)
% 1.04/1.12 [57]P5(a3,a4)
% 1.04/1.12 [82]P4(a14,a22,a16,a15)
% 1.04/1.12 [83]~E(a9,a7)
% 1.04/1.12 [84]~E(a48,a9)
% 1.04/1.12 [85]~E(a48,a7)
% 1.04/1.12 [86]~E(a9,a33)
% 1.04/1.12 [87]~E(a33,a7)
% 1.04/1.12 [88]~E(a48,a33)
% 1.04/1.12 [101]~P5(a38,a4)
% 1.04/1.12 [52]E(f23(a2),f23(a3))
% 1.04/1.12 [63]P2(f42(a46),a34)
% 1.04/1.12 [89]~E(f23(a6),f23(a14))
% 1.04/1.12 [90]~E(f23(a14),f23(a3))
% 1.04/1.12 [59]E(f27(a41,f23(a14)),a7)
% 1.04/1.12 [60]E(f27(a41,f23(a6)),a33)
% 1.04/1.12 [61]E(f27(a41,f23(a3)),a7)
% 1.04/1.12 [62]E(f27(a11,f23(a14)),a15)
% 1.04/1.12 [64]E(f27(a39,f23(a14)),f23(a22))
% 1.04/1.12 [65]E(f27(a39,f23(a3)),f23(a12))
% 1.04/1.12 [66]E(f27(a28,f23(a6)),f23(a6))
% 1.04/1.12 [77]P2(a34,f27(a39,f23(a14)))
% 1.04/1.12 [78]P3(f26(a13),f44(f43(f23(a3)),f35(a14)))
% 1.04/1.12 [81]P3(f31(a3,a12),f44(f43(f23(a3)),f35(a14)))
% 1.04/1.12 [76]E(f42(f27(a39,f23(a3))),f23(a13))
% 1.04/1.12 [79]P2(a34,f42(f27(a39,f23(a3))))
% 1.04/1.12 [58]P2(x581,x581)
% 1.04/1.12 [102]~P3(x1021,a1)
% 1.04/1.12 [103]~P5(x1031,a45)
% 1.04/1.12 [67]P2(f23(x671),a34)
% 1.04/1.12 [68]P2(f42(a46),f23(x681))
% 1.04/1.12 [69]E(f44(a1,x691),f8(x691,a1))
% 1.04/1.12 [70]P1(f8(x701,a1))
% 1.04/1.12 [71]P1(f44(a1,x711))
% 1.04/1.12 [111]~P2(f42(x1111),x1111)
% 1.04/1.12 [53]E(f32(f25(x531)),x531)
% 1.04/1.12 [54]E(f32(f26(x541)),x541)
% 1.04/1.12 [91]~E(f26(x911),f25(x912))
% 1.04/1.12 [92]~E(f36(x921),f26(x922))
% 1.04/1.12 [93]~E(f36(x931),f25(x932))
% 1.04/1.12 [94]~E(f35(x941),f26(x942))
% 1.04/1.12 [95]~E(f35(x951),f25(x952))
% 1.04/1.12 [96]~E(f35(x961),f36(x962))
% 1.04/1.12 [97]~E(f37(x971),f26(x972))
% 1.04/1.12 [98]~E(f37(x981),f35(x982))
% 1.04/1.12 [99]~E(f37(x991),f25(x992))
% 1.04/1.12 [100]~E(f37(x1001),f36(x1002))
% 1.04/1.12 [104]~E(f8(x1041,x1042),a1)
% 1.04/1.12 [105]~E(f44(x1051,x1052),a1)
% 1.04/1.12 [72]E(f24(f8(x721,x722)),x721)
% 1.04/1.12 [73]E(f47(f8(x731,x732)),x732)
% 1.04/1.12 [74]E(f29(f44(x741,x742)),x742)
% 1.04/1.12 [75]E(f30(f44(x751,x752)),x751)
% 1.04/1.12 [106]~E(f31(x1061,x1062),f25(x1063))
% 1.04/1.12 [107]~E(f31(x1071,x1072),f26(x1073))
% 1.04/1.12 [108]~E(f31(x1081,x1082),f36(x1083))
% 1.04/1.12 [109]~E(f31(x1091,x1092),f35(x1093))
% 1.04/1.12 [110]~E(f31(x1101,x1102),f37(x1103))
% 1.04/1.12 [80]E(f44(f8(x801,x802),x803),f8(x801,f44(x802,x803)))
% 1.04/1.12 [137]E(f23(a22),f23(a2))+P5(f23(a2),f27(a5,f23(a14)))
% 1.04/1.12 [121]E(x1211,a1)+E(f8(f24(x1211),f47(x1211)),x1211)
% 1.04/1.12 [122]E(x1221,a1)+E(f44(f30(x1221),f29(x1221)),x1221)
% 1.04/1.12 [120]~E(x1201,x1202)+P2(x1201,x1202)
% 1.04/1.12 [123]P2(x1232,x1231)+P2(x1231,x1232)
% 1.04/1.12 [112]P6(x1121)+~E(x1121,f25(x1122))
% 1.04/1.12 [113]P6(x1131)+~E(x1131,f26(x1132))
% 1.04/1.12 [114]E(x1141,x1142)+~E(f25(x1141),f25(x1142))
% 1.04/1.12 [115]E(x1151,x1152)+~E(f26(x1151),f26(x1152))
% 1.04/1.12 [116]E(x1161,x1162)+~E(f36(x1161),f36(x1162))
% 1.04/1.12 [117]E(x1171,x1172)+~E(f35(x1171),f35(x1172))
% 1.04/1.12 [118]E(x1181,x1182)+~E(f37(x1181),f37(x1182))
% 1.04/1.12 [129]~P2(x1291,x1292)+P2(x1291,f42(x1292))
% 1.04/1.12 [135]~P2(x1351,x1352)+P2(f42(x1351),f42(x1352))
% 1.04/1.12 [139]P1(x1391)+~P1(f8(x1392,x1391))
% 1.04/1.12 [140]P1(x1401)+~P1(f44(x1401,x1402))
% 1.04/1.12 [141]P2(x1411,x1412)+~P2(f42(x1411),f42(x1412))
% 1.04/1.12 [126]~E(f23(x1261),f23(x1262))+~E(f42(f23(x1261)),f23(x1262))
% 1.04/1.12 [136]~P1(x1361)+P1(f44(x1361,f35(x1362)))
% 1.04/1.12 [152]P5(x1521,a40)+~P3(f31(x1522,x1521),f43(f23(x1522)))
% 1.04/1.12 [153]P5(x1531,a40)+~P3(f31(x1531,x1532),f43(f23(x1531)))
% 1.04/1.12 [130]~E(x1301,x1302)+P3(x1301,f8(x1302,x1303))
% 1.04/1.12 [131]~E(x1311,x1313)+P3(x1311,f44(x1312,x1313))
% 1.04/1.12 [143]~P3(x1431,x1433)+P3(x1431,f8(x1432,x1433))
% 1.04/1.12 [144]~P3(x1441,x1442)+P3(x1441,f44(x1442,x1443))
% 1.04/1.12 [151]~P1(x1511)+P1(f44(x1511,f31(x1512,x1513)))
% 1.13/1.13 [132]E(x1321,x1322)+~E(f31(x1323,x1321),f31(x1324,x1322))
% 1.13/1.13 [133]E(x1331,x1332)+~E(f31(x1331,x1333),f31(x1332,x1334))
% 1.13/1.13 [161]~P4(x1611,x1613,x1614,x1612)+E(f43(f23(x1611)),f8(f31(x1612,x1613),x1614))
% 1.13/1.13 [125]~P6(x1251)+E(f26(f19(x1251)),x1251)+E(f25(f17(x1251)),x1251)
% 1.13/1.13 [134]~P2(x1342,x1341)+~P2(x1341,x1342)+E(x1341,x1342)
% 1.13/1.13 [127]~P1(x1272)+P6(x1271)+P1(f8(x1271,x1272))
% 1.13/1.13 [128]~P1(x1282)+P6(x1281)+P1(f44(x1282,x1281))
% 1.13/1.13 [138]P2(x1381,x1382)+E(x1381,f42(x1382))+~P2(x1381,f42(x1382))
% 1.13/1.13 [145]~P1(x1452)+P1(f8(x1451,x1452))+P6(f20(x1451,x1452))
% 1.13/1.13 [146]~P1(x1462)+P1(f44(x1462,x1461))+P6(f21(x1461,x1462))
% 1.13/1.13 [147]~P1(x1472)+P3(f20(x1471,x1472),x1472)+P1(f8(x1471,x1472))
% 1.13/1.13 [148]~P1(x1481)+P3(f21(x1482,x1481),x1481)+P1(f44(x1481,x1482))
% 1.13/1.13 [159]~P1(x1592)+~P2(f32(x1591),f32(f20(x1591,x1592)))+P1(f8(x1591,x1592))
% 1.13/1.13 [160]~P1(x1601)+~P2(f32(f21(x1602,x1601)),f32(x1602))+P1(f44(x1601,x1602))
% 1.13/1.13 [154]~P1(x1542)+P1(f8(x1541,x1542))+E(f23(f32(f20(x1541,x1542))),f23(f32(x1541)))
% 1.13/1.13 [155]~P1(x1552)+P1(f44(x1552,x1551))+E(f23(f32(f21(x1551,x1552))),f23(f32(x1551)))
% 1.13/1.13 [142]~P2(x1421,x1423)+P2(x1421,x1422)+~P2(x1423,x1422)
% 1.13/1.13 [149]E(x1491,x1492)+P3(x1491,x1493)+~P3(x1491,f44(x1493,x1492))
% 1.13/1.13 [150]E(x1501,x1502)+P3(x1501,x1503)+~P3(x1501,f8(x1502,x1503))
% 1.13/1.13 [165]~P4(x1653,x1654,x1655,x1656)+~E(f23(x1651),f23(x1652))+~P3(f26(x1651),f43(f23(x1652)))
% 1.13/1.13 [166]~P4(x1661,x1662,x1663,x1664)+~P2(f23(x1665),f23(x1666))+~P3(f25(x1666),f43(f23(x1665)))
% 1.13/1.13 [167]~P4(x1671,x1672,x1673,x1674)+~P2(f23(x1675),f23(x1676))+~P3(f35(x1676),f43(f23(x1675)))
% 1.13/1.13 [168]~P4(x1681,x1682,x1683,x1684)+~P2(f23(x1685),f23(x1686))+~P3(f31(x1686,x1685),f43(f23(x1687)))
% 1.13/1.13 [156]P2(x1561,x1562)+~E(f23(x1561),f23(x1562))+~P3(f26(x1562),x1563)+~P1(f8(f25(x1561),x1563))
% 1.13/1.13 [163]~P4(x1632,x1633,x1634,x1635)+~P5(x1631,a4)+E(f27(a11,f23(x1631)),x1631)+~E(f27(a41,f23(x1631)),a9)
% 1.13/1.13 [164]~P4(x1642,x1643,x1644,x1645)+~P5(x1641,a4)+E(f27(a11,f23(x1641)),x1641)+~E(f27(a41,f23(x1641)),a7)
% 1.13/1.13 [169]~P4(x1692,x1693,x1694,x1695)+~P5(x1691,a4)+~P3(f31(x1691,x1696),f43(f23(x1691)))+~E(f27(a41,f23(x1691)),a9)
% 1.13/1.13 [170]~P4(x1703,x1704,x1705,x1706)+~P5(x1702,a4)+~P3(f31(x1702,x1701),f43(f23(x1702)))+P2(f23(x1701),f27(a39,f23(x1702)))
% 1.13/1.13 [162]E(x1621,x1622)+~P4(x1623,x1624,x1625,x1626)+~E(f23(x1621),f23(x1622))+~P5(x1622,a4)+~P5(x1621,a4)
% 1.13/1.13 [157]~P6(x1571)+~P6(x1572)+~P3(x1572,x1573)+P2(f32(x1571),f32(x1572))+~P1(f8(x1571,x1573))+~E(f23(f32(x1572)),f23(f32(x1571)))
% 1.13/1.13 [158]~P6(x1582)+~P6(x1581)+~P3(x1581,x1583)+P2(f32(x1581),f32(x1582))+~P1(f44(x1583,x1582))+~E(f23(f32(x1581)),f23(f32(x1582)))
% 1.13/1.13 [172]~P4(x1723,x1724,x1725,x1726)+~P5(x1722,a4)+~P5(x1721,a4)+P2(f23(x1721),f23(x1722))+P2(f27(a39,f23(x1722)),f23(x1721))+~E(f27(a41,f23(x1721)),a7)+~E(f27(a41,f23(x1722)),a7)
% 1.13/1.13 [175]~P4(x1753,x1754,x1755,x1756)+~P5(x1752,a4)+~P5(x1751,a4)+P2(f23(x1751),f23(x1752))+~P2(f27(a39,f23(x1751)),f27(a39,f23(x1752)))+~E(f27(a41,f23(x1751)),a7)+~E(f27(a41,f23(x1752)),a7)
% 1.13/1.13 [171]~P4(x1714,x1715,x1716,x1717)+~P5(x1712,a4)+~E(f23(x1711),f23(x1712))+~P5(x1713,a4)+~P3(f26(x1711),f43(f23(x1713)))+~E(f27(a28,f23(x1712)),f23(x1712))+~E(f27(a41,f23(x1712)),a33)
% 1.13/1.13 [173]~P4(x1734,x1735,x1736,x1737)+~P5(x1731,a4)+~P5(x1733,a4)+~E(f23(x1731),f23(x1732))+~P3(f31(x1733,x1732),f43(f23(x1733)))+~E(f27(a41,f23(x1731)),a7)+~E(f27(a41,f23(x1733)),a7)
% 1.13/1.13 [174]~P4(x1743,x1744,x1745,x1746)+~P5(x1742,a4)+~P5(x1741,a4)+~P3(f25(x1741),f43(f23(x1747)))+P2(f27(a39,f23(x1741)),f23(x1742))+~E(f27(a28,f23(x1742)),f23(x1742))+~E(f27(a41,f23(x1741)),a7)+~E(f27(a41,f23(x1742)),a33)
% 1.13/1.13 [177]~P4(x1776,x1775,x1774,x1773)+~P5(x1777,a4)+~E(f18(x1773,x1774,x1775,x1776,x1777,x1772,x1778,x1771),f23(x1778))+~E(f23(x1772),f23(x1771))+~P3(f26(x1772),f43(f23(x1777)))+~P3(f26(x1778),f43(f23(x1771)))+~E(f23(x1771),a34)+~E(f27(a41,f23(x1771)),a9)
% 1.13/1.13 [178]~P4(x1784,x1783,x1782,x1781)+~E(f23(x1786),f23(x1788))+~P5(x1785,a4)+P2(f42(a46),f18(x1781,x1782,x1783,x1784,x1785,x1786,x1787,x1788))+~E(f23(x1788),a34)+~P3(f26(x1787),f43(f23(x1788)))+~P3(f26(x1786),f43(f23(x1785)))+~E(f27(a41,f23(x1788)),a9)
% 1.13/1.13 [179]~P4(x1794,x1795,x1796,x1797)+~P2(f23(x1791),f18(x1797,x1796,x1795,x1794,x1793,x1792,x1798,x1791))+~E(f23(x1791),f23(x1792))+~P5(x1793,a4)+~P3(f26(x1792),f43(f23(x1793)))+~E(f23(x1791),a34)+~P3(f26(x1798),f43(f23(x1791)))+~E(f27(a41,f23(x1791)),a9)
% 1.13/1.13 [180]~P4(x1804,x1805,x1806,x1807)+~E(f23(x1802),f23(x1801))+~P5(x1803,a4)+~P3(f26(x1802),f43(f23(x1803)))+~E(f23(x1801),a34)+~P3(f26(x1808),f43(f23(x1801)))+~P5(f18(x1807,x1806,x1805,x1804,x1803,x1802,x1808,x1801),f27(a10,f23(x1801)))+~E(f27(a41,f23(x1801)),a9)
% 1.13/1.13 [176]~P4(x1765,x1766,x1767,x1768)+~P5(x1761,a4)+~P5(x1762,a4)+~P3(f31(x1762,x1763),f43(f23(x1762)))+~P3(f26(x1764),f43(f23(x1762)))+~E(f27(a28,f23(x1761)),f23(x1761))+~E(f23(x1763),f27(a39,f23(x1762)))+~E(f23(x1764),f42(f27(a39,f23(x1762))))+~E(f27(a41,f23(x1761)),a33)+~E(f27(a41,f23(x1762)),a7)+~P2(a34,f42(f27(a39,f23(x1762))))
% 1.13/1.13 %EqnAxiom
% 1.13/1.13 [1]E(x11,x11)
% 1.13/1.13 [2]E(x22,x21)+~E(x21,x22)
% 1.13/1.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.13/1.13 [4]~E(x41,x42)+E(f23(x41),f23(x42))
% 1.13/1.13 [5]~E(x51,x52)+E(f27(x51,x53),f27(x52,x53))
% 1.13/1.13 [6]~E(x61,x62)+E(f27(x63,x61),f27(x63,x62))
% 1.13/1.13 [7]~E(x71,x72)+E(f25(x71),f25(x72))
% 1.13/1.13 [8]~E(x81,x82)+E(f32(x81),f32(x82))
% 1.13/1.13 [9]~E(x91,x92)+E(f26(x91),f26(x92))
% 1.13/1.13 [10]~E(x101,x102)+E(f21(x101,x103),f21(x102,x103))
% 1.13/1.13 [11]~E(x111,x112)+E(f21(x113,x111),f21(x113,x112))
% 1.13/1.13 [12]~E(x121,x122)+E(f18(x121,x123,x124,x125,x126,x127,x128,x129),f18(x122,x123,x124,x125,x126,x127,x128,x129))
% 1.13/1.13 [13]~E(x131,x132)+E(f18(x133,x131,x134,x135,x136,x137,x138,x139),f18(x133,x132,x134,x135,x136,x137,x138,x139))
% 1.13/1.13 [14]~E(x141,x142)+E(f18(x143,x144,x141,x145,x146,x147,x148,x149),f18(x143,x144,x142,x145,x146,x147,x148,x149))
% 1.13/1.13 [15]~E(x151,x152)+E(f18(x153,x154,x155,x151,x156,x157,x158,x159),f18(x153,x154,x155,x152,x156,x157,x158,x159))
% 1.13/1.13 [16]~E(x161,x162)+E(f18(x163,x164,x165,x166,x161,x167,x168,x169),f18(x163,x164,x165,x166,x162,x167,x168,x169))
% 1.13/1.13 [17]~E(x171,x172)+E(f18(x173,x174,x175,x176,x177,x171,x178,x179),f18(x173,x174,x175,x176,x177,x172,x178,x179))
% 1.13/1.13 [18]~E(x181,x182)+E(f18(x183,x184,x185,x186,x187,x188,x181,x189),f18(x183,x184,x185,x186,x187,x188,x182,x189))
% 1.13/1.13 [19]~E(x191,x192)+E(f18(x193,x194,x195,x196,x197,x198,x199,x191),f18(x193,x194,x195,x196,x197,x198,x199,x192))
% 1.13/1.13 [20]~E(x201,x202)+E(f31(x201,x203),f31(x202,x203))
% 1.13/1.13 [21]~E(x211,x212)+E(f31(x213,x211),f31(x213,x212))
% 1.13/1.13 [22]~E(x221,x222)+E(f43(x221),f43(x222))
% 1.13/1.13 [23]~E(x231,x232)+E(f42(x231),f42(x232))
% 1.13/1.13 [24]~E(x241,x242)+E(f8(x241,x243),f8(x242,x243))
% 1.13/1.13 [25]~E(x251,x252)+E(f8(x253,x251),f8(x253,x252))
% 1.13/1.13 [26]~E(x261,x262)+E(f44(x261,x263),f44(x262,x263))
% 1.13/1.13 [27]~E(x271,x272)+E(f44(x273,x271),f44(x273,x272))
% 1.13/1.13 [28]~E(x281,x282)+E(f35(x281),f35(x282))
% 1.13/1.13 [29]~E(x291,x292)+E(f20(x291,x293),f20(x292,x293))
% 1.13/1.13 [30]~E(x301,x302)+E(f20(x303,x301),f20(x303,x302))
% 1.13/1.13 [31]~E(x311,x312)+E(f36(x311),f36(x312))
% 1.13/1.13 [32]~E(x321,x322)+E(f19(x321),f19(x322))
% 1.13/1.13 [33]~E(x331,x332)+E(f29(x331),f29(x332))
% 1.13/1.13 [34]~E(x341,x342)+E(f17(x341),f17(x342))
% 1.13/1.13 [35]~E(x351,x352)+E(f30(x351),f30(x352))
% 1.13/1.13 [36]~E(x361,x362)+E(f47(x361),f47(x362))
% 1.13/1.13 [37]~E(x371,x372)+E(f37(x371),f37(x372))
% 1.13/1.13 [38]~E(x381,x382)+E(f24(x381),f24(x382))
% 1.13/1.13 [39]~P1(x391)+P1(x392)+~E(x391,x392)
% 1.13/1.13 [40]P5(x402,x403)+~E(x401,x402)+~P5(x401,x403)
% 1.13/1.13 [41]P5(x413,x412)+~E(x411,x412)+~P5(x413,x411)
% 1.13/1.13 [42]P2(x422,x423)+~E(x421,x422)+~P2(x421,x423)
% 1.13/1.13 [43]P2(x433,x432)+~E(x431,x432)+~P2(x433,x431)
% 1.13/1.13 [44]P3(x442,x443)+~E(x441,x442)+~P3(x441,x443)
% 1.13/1.13 [45]P3(x453,x452)+~E(x451,x452)+~P3(x453,x451)
% 1.13/1.13 [46]P4(x462,x463,x464,x465)+~E(x461,x462)+~P4(x461,x463,x464,x465)
% 1.13/1.13 [47]P4(x473,x472,x474,x475)+~E(x471,x472)+~P4(x473,x471,x474,x475)
% 1.13/1.13 [48]P4(x483,x484,x482,x485)+~E(x481,x482)+~P4(x483,x484,x481,x485)
% 1.13/1.13 [49]P4(x493,x494,x495,x492)+~E(x491,x492)+~P4(x493,x494,x495,x491)
% 1.13/1.13 [50]~P6(x501)+P6(x502)+~E(x501,x502)
% 1.13/1.13
% 1.13/1.13 %-------------------------------------------
% 1.13/1.13 cnf(181,plain,
% 1.13/1.13 (P6(f25(x1811))),
% 1.13/1.13 inference(equality_inference,[],[112])).
% 1.13/1.13 cnf(189,plain,
% 1.13/1.13 (P3(x1891,f8(x1891,x1892))),
% 1.13/1.13 inference(equality_inference,[],[130])).
% 1.13/1.13 cnf(204,plain,
% 1.13/1.13 (E(f32(f25(x2041)),x2041)),
% 1.13/1.13 inference(rename_variables,[],[53])).
% 1.13/1.13 cnf(211,plain,
% 1.13/1.13 (~P2(f42(f42(x2111)),x2111)),
% 1.13/1.13 inference(scs_inference,[],[52,89,111,53,204,120,2,4,112,113,123,129])).
% 1.13/1.13 cnf(212,plain,
% 1.13/1.13 (~P2(f42(x2121),x2121)),
% 1.13/1.13 inference(rename_variables,[],[111])).
% 1.13/1.13 cnf(229,plain,
% 1.13/1.13 (P3(f31(a3,a12),f43(f23(a3)))),
% 1.13/1.13 inference(scs_inference,[],[52,55,89,90,81,64,77,189,181,103,111,212,91,109,101,67,53,204,120,2,4,112,113,123,129,3,40,41,42,43,44,125,134,149])).
% 1.13/1.13 cnf(232,plain,
% 1.13/1.13 (~P2(f23(a12),f23(a3))),
% 1.13/1.13 inference(scs_inference,[],[52,55,82,89,90,81,64,77,189,181,103,111,212,91,109,101,67,53,204,120,2,4,112,113,123,129,3,40,41,42,43,44,125,134,149,168])).
% 1.13/1.13 cnf(240,plain,
% 1.13/1.13 (E(f17(f25(x2401)),x2401)),
% 1.13/1.13 inference(scs_inference,[],[52,55,57,82,89,90,81,64,77,59,61,189,181,102,103,111,212,91,109,101,67,53,204,120,2,4,112,113,123,129,3,40,41,42,43,44,125,134,149,168,45,164,173,114])).
% 1.13/1.13 cnf(259,plain,
% 1.13/1.13 (~E(f23(x2591),f23(x2592))+~P3(f26(x2591),f43(f23(x2592)))),
% 1.13/1.13 inference(scs_inference,[],[82,165])).
% 1.13/1.13 cnf(262,plain,
% 1.13/1.13 (~P2(f23(x2621),f23(x2622))+~P3(f31(x2622,x2621),f43(f23(x2623)))),
% 1.13/1.13 inference(scs_inference,[],[82,168])).
% 1.13/1.13 cnf(270,plain,
% 1.13/1.13 (~P5(x2701,a4)+~P5(x2702,a4)+~P3(f31(x2702,x2703),f43(f23(x2702)))+~P3(f26(x2704),f43(f23(x2702)))+~E(f27(a28,f23(x2701)),f23(x2701))+~E(f23(x2703),f27(a39,f23(x2702)))+~E(f23(x2704),f42(f27(a39,f23(x2702))))+~E(f27(a41,f23(x2701)),a33)+~E(f27(a41,f23(x2702)),a7)+~P2(a34,f42(f27(a39,f23(x2702))))),
% 1.13/1.13 inference(scs_inference,[],[82,176])).
% 1.13/1.13 cnf(279,plain,
% 1.13/1.13 (E(f17(f25(x2791)),x2791)),
% 1.13/1.13 inference(rename_variables,[],[240])).
% 1.13/1.13 cnf(282,plain,
% 1.13/1.13 (~P2(f42(f42(x2821)),x2821)),
% 1.13/1.13 inference(rename_variables,[],[211])).
% 1.13/1.13 cnf(288,plain,
% 1.13/1.13 (~E(f42(f42(x2881)),x2881)),
% 1.13/1.13 inference(scs_inference,[],[52,90,58,211,282,240,279,259,262,123,113,129,4,112,120])).
% 1.13/1.13 cnf(359,plain,
% 1.13/1.13 (~E(f23(a12),f23(a3))),
% 1.13/1.13 inference(scs_inference,[],[232,123,120])).
% 1.13/1.13 cnf(393,plain,
% 1.13/1.13 (E(f47(f8(x3931,x3932)),x3932)),
% 1.13/1.13 inference(rename_variables,[],[73])).
% 1.13/1.13 cnf(399,plain,
% 1.13/1.13 (E(f23(a12),f27(a39,f23(a3)))),
% 1.13/1.13 inference(scs_inference,[],[359,65,73,393,112,113,4,2])).
% 1.13/1.13 cnf(486,plain,
% 1.13/1.13 (E(f26(a13),f35(a14))),
% 1.13/1.13 inference(scs_inference,[],[61,56,57,78,60,288,79,76,66,399,229,211,67,2,3,42,270,149])).
% 1.13/1.13 cnf(740,plain,
% 1.13/1.13 ($false),
% 1.13/1.13 inference(scs_inference,[],[486,94,2]),
% 1.13/1.13 ['proof']).
% 1.13/1.13 % SZS output end Proof
% 1.13/1.13 % Total time :0.450000s
%------------------------------------------------------------------------------