%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : SWV461+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 : n024.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 16:47:24 EDT 2024
% Result : Theorem 0.63s 0.91s
% Output : CNFRefutation 0.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV461+1 : TPTP v8.2.0. Released v4.0.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n024.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 20 18:11:09 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.60/0.64 start to proof:theBenchmark
% 0.63/0.90 %-------------------------------------------
% 0.63/0.90 % File :CSE---1.7
% 0.63/0.90 % Problem :theBenchmark
% 0.63/0.90 % Transform :cnf
% 0.63/0.90 % Format :tptp:raw
% 0.63/0.90 % Command :java -jar mcs_scs.jar %d %s
% 0.63/0.90
% 0.63/0.90 % Result :Theorem 0.190000s
% 0.63/0.90 % Output :CNFRefutation 0.190000s
% 0.63/0.90 %-------------------------------------------
% 0.63/0.90 %------------------------------------------------------------------------------
% 0.63/0.90 % File : SWV461+1 : TPTP v8.2.0. Released v4.0.0.
% 0.63/0.90 % Domain : Software Verification
% 0.63/0.90 % Problem : Establishing that there cannot be two leaders, part i52_p18
% 0.63/0.90 % Version : [Sve07] axioms : Especial.
% 0.63/0.90 % English :
% 0.63/0.90
% 0.63/0.90 % Refs : [Sto97] Stoller (1997), Leader Election in Distributed Systems
% 0.63/0.90 % : [Sve07] Svensson (2007), Email to Koen Claessen
% 0.63/0.90 % : [Sve08] Svensson (2008), A Semi-Automatic Correctness Proof Pr
% 0.63/0.90 % Source : [Sve07]
% 0.63/0.90 % Names : stoller_i52_p18 [Sve07]
% 0.63/0.90
% 0.63/0.90 % Status : Theorem
% 0.63/0.90 % Rating : 0.36 v8.2.0, 0.42 v8.1.0, 0.36 v7.5.0, 0.34 v7.4.0, 0.30 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.30 v7.0.0, 0.33 v6.4.0, 0.38 v6.2.0, 0.44 v6.1.0, 0.50 v6.0.0, 0.43 v5.5.0, 0.52 v5.4.0, 0.57 v5.3.0, 0.67 v5.2.0, 0.50 v5.1.0, 0.57 v5.0.0, 0.62 v4.1.0, 0.61 v4.0.1, 0.65 v4.0.0
% 0.63/0.90 % Syntax : Number of formulae : 67 ( 40 unt; 0 def)
% 0.63/0.90 % Number of atoms : 208 ( 106 equ)
% 0.63/0.90 % Maximal formula atoms : 97 ( 3 avg)
% 0.63/0.90 % Number of connectives : 209 ( 68 ~; 12 |; 78 &)
% 0.63/0.90 % ( 13 <=>; 38 =>; 0 <=; 0 <~>)
% 0.63/0.90 % Maximal formula depth : 30 ( 4 avg)
% 0.63/0.90 % Maximal term depth : 4 ( 1 avg)
% 0.63/0.90 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty)
% 0.63/0.90 % Number of functors : 33 ( 33 usr; 16 con; 0-2 aty)
% 0.63/0.90 % Number of variables : 165 ( 164 !; 1 ?)
% 0.63/0.90 % SPC : FOF_THM_RFO_SEQ
% 0.63/0.90
% 0.63/0.90 % Comments :
% 0.63/0.90 %------------------------------------------------------------------------------
% 0.63/0.90 %----Include axioms for verification of Stoller's leader election algorithm
% 0.63/0.90 include('Axioms/SWV011+0.ax').
% 0.63/0.90 %------------------------------------------------------------------------------
% 0.63/0.90 fof(conj,conjecture,
% 0.63/0.90 ! [V,W] :
% 0.63/0.90 ( ( ! [X] :
% 0.63/0.90 ( host(W) = host(X)
% 0.63/0.90 => ~ setIn(X,alive) )
% 0.63/0.90 & ! [X,Y] :
% 0.63/0.90 ( elem(m_Ldr(Y),queue(host(X)))
% 0.63/0.90 => ~ leq(host(X),host(Y)) )
% 0.63/0.90 & ! [X,Y] :
% 0.63/0.90 ( elem(m_Down(Y),queue(host(X)))
% 0.63/0.90 => host(Y) != host(X) )
% 0.63/0.90 & ! [X,Y] :
% 0.63/0.90 ( elem(m_Halt(Y),queue(host(X)))
% 0.63/0.90 => ~ leq(host(X),host(Y)) )
% 0.63/0.90 & ! [X,Y,Z] :
% 0.63/0.90 ( elem(m_Ack(Z,X),queue(host(Y)))
% 0.63/0.90 => ~ leq(host(X),host(Z)) )
% 0.63/0.90 & ! [X,Y] :
% 0.63/0.90 ( ( Y != X
% 0.63/0.91 & host(Y) = host(X) )
% 0.63/0.91 => ( ~ setIn(X,alive)
% 0.63/0.91 | ~ setIn(Y,alive) ) )
% 0.63/0.91 & ! [X,Y] :
% 0.63/0.91 ( ( setIn(Y,alive)
% 0.63/0.91 & elem(m_Ack(Y,X),queue(host(Y))) )
% 0.63/0.91 => leq(host(X),index(pendack,host(Y))) )
% 0.63/0.91 & ! [X,Y] :
% 0.63/0.91 ( ( setIn(Y,alive)
% 0.63/0.91 & index(status,host(Y)) = elec_1 )
% 0.63/0.91 => ~ elem(m_Ack(Y,X),queue(host(Y))) )
% 0.63/0.91 & ! [X] :
% 0.63/0.91 ( ( ( index(status,host(X)) = elec_1
% 0.63/0.91 | index(status,host(X)) = elec_2 )
% 0.63/0.91 & setIn(X,alive) )
% 0.63/0.91 => index(elid,host(X)) = X )
% 0.63/0.91 & ! [X,Y,Z] :
% 0.63/0.91 ( ( setIn(Z,alive)
% 0.63/0.91 & elem(m_Down(Y),queue(host(Z)))
% 0.63/0.91 & host(Y) = host(X) )
% 0.63/0.91 => ~ ( setIn(X,alive)
% 0.63/0.91 & index(ldr,host(X)) = host(X)
% 0.63/0.91 & index(status,host(X)) = norm ) )
% 0.63/0.91 & ! [X,Y,Z] :
% 0.63/0.91 ( ( setIn(X,alive)
% 0.63/0.91 & setIn(Z,alive)
% 0.63/0.91 & host(Z) = host(Y)
% 0.63/0.91 & index(status,host(X)) = elec_2
% 0.63/0.91 & index(status,host(Z)) = elec_2 )
% 0.63/0.91 => ~ elem(m_Ack(X,Y),queue(host(X))) )
% 0.63/0.91 & ! [X,Y] :
% 0.63/0.91 ( ( ~ leq(host(X),host(Y))
% 0.63/0.91 & setIn(X,alive)
% 0.63/0.91 & setIn(Y,alive)
% 0.63/0.91 & index(status,host(X)) = elec_2
% 0.63/0.91 & index(status,host(Y)) = elec_2 )
% 0.63/0.91 => leq(index(pendack,host(Y)),host(X)) )
% 0.63/0.91 & ! [X,Y] :
% 0.63/0.91 ( ( ~ leq(host(X),host(Y))
% 0.63/0.91 & setIn(X,alive)
% 0.63/0.91 & setIn(Y,alive)
% 0.63/0.91 & index(status,host(X)) = elec_2
% 0.63/0.91 & index(status,host(Y)) = elec_2 )
% 0.63/0.91 => ~ leq(index(pendack,host(X)),index(pendack,host(Y))) )
% 0.63/0.91 & ! [X,Y,Z] :
% 0.63/0.91 ( ( ~ leq(index(pendack,host(Z)),host(X))
% 0.63/0.91 & setIn(Z,alive)
% 0.63/0.91 & elem(m_Halt(Z),queue(host(Y)))
% 0.63/0.91 & index(status,host(Z)) = elec_2 )
% 0.63/0.91 => ~ ( setIn(X,alive)
% 0.63/0.91 & index(ldr,host(X)) = host(X)
% 0.63/0.91 & index(status,host(X)) = norm ) )
% 0.63/0.91 & ! [X,Y,Z,Pid0] :
% 0.63/0.91 ( ( ! [V0] :
% 0.63/0.91 ( ( ~ leq(host(Pid0),V0)
% 0.63/0.91 & leq(s(zero),V0) )
% 0.63/0.91 => ( setIn(V0,index(down,host(Pid0)))
% 0.63/0.91 | V0 = host(Z) ) )
% 0.63/0.91 & elem(m_Down(Z),queue(host(Pid0)))
% 0.63/0.91 & host(Pid0) = host(Y)
% 0.63/0.91 & host(Pid0) = nbr_proc
% 0.63/0.91 & index(status,host(Pid0)) = elec_1 )
% 0.63/0.91 => ~ ( setIn(X,alive)
% 0.63/0.91 & elem(m_Down(Y),queue(host(X))) ) )
% 0.63/0.91 & ! [X,Y,Z,Pid0] :
% 0.63/0.91 ( ( setIn(Pid0,alive)
% 0.63/0.91 & elem(m_Down(Z),queue(host(Pid0)))
% 0.63/0.91 & elem(m_Ack(Pid0,Y),queue(host(Pid0)))
% 0.63/0.91 & leq(nbr_proc,s(index(pendack,host(Pid0))))
% 0.63/0.91 & index(status,host(Pid0)) = elec_2
% 0.63/0.91 & host(Y) = index(pendack,host(Pid0))
% 0.63/0.91 & host(Z) = s(index(pendack,host(Pid0))) )
% 0.63/0.91 => ~ ( setIn(X,alive)
% 0.63/0.91 & index(ldr,host(X)) = host(X)
% 0.63/0.91 & index(status,host(X)) = norm ) ) )
% 0.63/0.91 => ( queue(host(W)) = q_nil
% 0.63/0.91 => ( ( ! [X] :
% 0.63/0.91 ( host(W) = host(X)
% 0.63/0.91 => leq(X,V) )
% 0.63/0.91 & ~ setIn(V,pids)
% 0.63/0.91 & host(W) = host(V) )
% 0.63/0.91 => ( host(V) = s(zero)
% 0.63/0.91 => ( ~ leq(nbr_proc,host(V))
% 0.63/0.91 => ! [X] :
% 0.63/0.91 ( host(V) != host(X)
% 0.63/0.91 => ! [Y,Z,Z0] :
% 0.63/0.91 ( s(host(V)) = host(Z0)
% 0.63/0.91 => ( host(V) != host(Z0)
% 0.63/0.91 => ( ( ( setIn(Z0,alive)
% 0.63/0.91 | Z0 = V )
% 0.63/0.91 & leq(nbr_proc,s(index(pendack,host(Z0))))
% 0.63/0.91 & elem(m_Down(Z),snoc(queue(host(Z0)),m_Halt(V)))
% 0.63/0.91 & elem(m_Ack(Z0,Y),snoc(queue(host(Z0)),m_Halt(V)))
% 0.63/0.91 & index(status,host(Z0)) = elec_2
% 0.63/0.91 & host(Y) = index(pendack,host(Z0))
% 0.63/0.91 & host(Z) = s(index(pendack,host(Z0))) )
% 0.63/0.91 => ~ ( ( setIn(X,alive)
% 0.63/0.91 | X = V )
% 0.63/0.91 & index(ldr,host(X)) = host(X)
% 0.63/0.91 & index(status,host(X)) = norm ) ) ) ) ) ) ) ) ) ) ).
% 0.63/0.91
% 0.63/0.91 %------------------------------------------------------------------------------
% 0.63/0.91 %-------------------------------------------
% 0.63/0.91 % Proof found
% 0.63/0.91 % SZS status Theorem for theBenchmark
% 0.63/0.91 % SZS output start Proof
% 0.63/0.91 %ClaNum:174(EqnAxiom:44)
% 0.63/0.91 %VarNum:489(SingletonVarNum:237)
% 0.63/0.91 %MaxLitNum:11
% 0.63/0.91 %MaxfuncDepth:3
% 0.63/0.91 %SharedTerms:71
% 0.63/0.91 %goalClause: 46 47 48 49 50 54 55 57 58 68 69 70 72 79 80 92 97 104 105 115
% 0.63/0.91 %singleGoalClaCount:17
% 0.63/0.91 [45]P1(a1)
% 0.63/0.91 [46]P2(a2)
% 0.63/0.91 [73]~E(a8,a5)
% 0.63/0.91 [74]~E(a44,a8)
% 0.63/0.91 [75]~E(a44,a5)
% 0.63/0.91 [76]~E(a8,a29)
% 0.63/0.91 [77]~E(a5,a29)
% 0.63/0.91 [78]~E(a44,a29)
% 0.63/0.91 [91]~P5(a34,a7)
% 0.63/0.91 [92]~P5(a3,a36)
% 0.63/0.91 [47]E(f16(a3),f16(a2))
% 0.63/0.91 [48]E(f38(a37),f16(a3))
% 0.63/0.91 [56]P4(f38(a37),a30)
% 0.63/0.91 [79]~E(f16(a17),f16(a3))
% 0.63/0.91 [80]~E(f16(a4),f16(a3))
% 0.63/0.91 [97]~P4(a30,f16(a3))
% 0.63/0.91 [49]E(f39(f16(a2)),a1)
% 0.63/0.91 [50]E(f38(f16(a3)),f16(a4))
% 0.63/0.91 [54]E(f23(a40,f16(a17)),a29)
% 0.63/0.91 [55]E(f23(a40,f16(a4)),a5)
% 0.63/0.91 [57]E(f23(a35,f16(a4)),f16(a18))
% 0.63/0.91 [58]E(f23(a24,f16(a17)),f16(a17))
% 0.63/0.91 [69]P3(f22(a20),f41(f39(f16(a4)),f21(a3)))
% 0.63/0.91 [72]P3(f27(a4,a18),f41(f39(f16(a4)),f21(a3)))
% 0.63/0.91 [68]E(f38(f23(a35,f16(a4))),f16(a20))
% 0.63/0.91 [70]P4(a30,f38(f23(a35,f16(a4))))
% 0.63/0.91 [53]P4(x531,x531)
% 0.63/0.91 [93]~P3(x931,a1)
% 0.63/0.91 [94]~P5(x941,a42)
% 0.63/0.91 [59]P4(f16(x591),a30)
% 0.63/0.91 [60]P4(f38(a37),f16(x601))
% 0.63/0.91 [61]E(f41(a1,x611),f6(x611,a1))
% 0.63/0.91 [62]P1(f6(x621,a1))
% 0.63/0.91 [63]P1(f41(a1,x631))
% 0.63/0.91 [103]~P4(f38(x1031),x1031)
% 0.63/0.91 [51]E(f28(f21(x511)),x511)
% 0.63/0.91 [52]E(f28(f22(x521)),x521)
% 0.63/0.91 [81]~E(f22(x811),f21(x812))
% 0.63/0.91 [82]~E(f31(x821),f22(x822))
% 0.63/0.91 [83]~E(f31(x831),f21(x832))
% 0.63/0.91 [84]~E(f32(x841),f22(x842))
% 0.63/0.91 [85]~E(f32(x851),f21(x852))
% 0.63/0.91 [86]~E(f32(x861),f31(x862))
% 0.63/0.91 [87]~E(f33(x871),f22(x872))
% 0.63/0.91 [88]~E(f33(x881),f32(x882))
% 0.63/0.91 [89]~E(f33(x891),f21(x892))
% 0.63/0.91 [90]~E(f33(x901),f31(x902))
% 0.63/0.91 [95]~E(f6(x951,x952),a1)
% 0.63/0.91 [96]~E(f41(x961,x962),a1)
% 0.63/0.91 [64]E(f19(f6(x641,x642)),x641)
% 0.63/0.91 [65]E(f43(f6(x651,x652)),x652)
% 0.63/0.91 [66]E(f25(f41(x661,x662)),x662)
% 0.63/0.91 [67]E(f26(f41(x671,x672)),x671)
% 0.63/0.91 [98]~E(f27(x981,x982),f21(x983))
% 0.63/0.91 [99]~E(f27(x991,x992),f22(x993))
% 0.63/0.91 [100]~E(f27(x1001,x1002),f31(x1003))
% 0.63/0.91 [101]~E(f27(x1011,x1012),f32(x1013))
% 0.63/0.91 [102]~E(f27(x1021,x1022),f33(x1023))
% 0.63/0.91 [71]E(f41(f6(x711,x712),x713),f6(x711,f41(x712,x713)))
% 0.63/0.91 [104]E(a17,a3)+P5(a17,a7)
% 0.63/0.91 [105]E(a4,a3)+P5(a4,a7)
% 0.63/0.91 [115]P4(x1151,a3)+~E(f16(a2),f16(x1151))
% 0.63/0.91 [116]E(x1161,a1)+E(f6(f19(x1161),f43(x1161)),x1161)
% 0.63/0.91 [117]E(x1171,a1)+E(f41(f26(x1171),f25(x1171)),x1171)
% 0.63/0.91 [114]~E(x1141,x1142)+P4(x1141,x1142)
% 0.63/0.91 [118]P4(x1182,x1181)+P4(x1181,x1182)
% 0.63/0.91 [106]P6(x1061)+~E(x1061,f21(x1062))
% 0.63/0.91 [107]P6(x1071)+~E(x1071,f22(x1072))
% 0.63/0.91 [108]E(x1081,x1082)+~E(f21(x1081),f21(x1082))
% 0.63/0.91 [109]E(x1091,x1092)+~E(f22(x1091),f22(x1092))
% 0.63/0.91 [110]E(x1101,x1102)+~E(f31(x1101),f31(x1102))
% 0.63/0.91 [111]E(x1111,x1112)+~E(f32(x1111),f32(x1112))
% 0.63/0.91 [112]E(x1121,x1122)+~E(f33(x1121),f33(x1122))
% 0.63/0.91 [125]~P4(x1251,x1252)+P4(x1251,f38(x1252))
% 0.63/0.91 [131]~P4(x1311,x1312)+P4(f38(x1311),f38(x1312))
% 0.63/0.91 [134]P1(x1341)+~P1(f6(x1342,x1341))
% 0.63/0.91 [135]P1(x1351)+~P1(f41(x1351,x1352))
% 0.63/0.91 [136]P4(x1361,x1362)+~P4(f38(x1361),f38(x1362))
% 0.63/0.91 [121]~E(f16(x1211),f16(x1212))+~E(f38(f16(x1211)),f16(x1212))
% 0.63/0.91 [132]~P1(x1321)+P1(f41(x1321,f32(x1322)))
% 0.63/0.91 [151]P5(x1511,a36)+~P3(f27(x1512,x1511),f39(f16(x1512)))
% 0.63/0.91 [152]P5(x1521,a36)+~P3(f27(x1521,x1522),f39(f16(x1521)))
% 0.63/0.91 [126]~E(x1261,x1262)+P3(x1261,f6(x1262,x1263))
% 0.63/0.91 [127]~E(x1271,x1273)+P3(x1271,f41(x1272,x1273))
% 0.63/0.91 [138]~P3(x1381,x1383)+P3(x1381,f6(x1382,x1383))
% 0.63/0.91 [139]~P3(x1391,x1392)+P3(x1391,f41(x1392,x1393))
% 0.63/0.91 [150]~P1(x1501)+P1(f41(x1501,f27(x1502,x1503)))
% 0.63/0.91 [128]E(x1281,x1282)+~E(f27(x1283,x1281),f27(x1284,x1282))
% 0.63/0.91 [129]E(x1291,x1292)+~E(f27(x1291,x1293),f27(x1292,x1294))
% 0.63/0.91 [120]~P6(x1201)+E(f22(f13(x1201)),x1201)+E(f21(f11(x1201)),x1201)
% 0.63/0.91 [130]~P4(x1302,x1301)+~P4(x1301,x1302)+E(x1301,x1302)
% 0.63/0.91 [122]~P2(x1221)+~P5(x1222,a7)+~E(f16(x1221),f16(x1222))
% 0.63/0.91 [123]~P1(x1232)+P6(x1231)+P1(f6(x1231,x1232))
% 0.63/0.91 [124]~P1(x1242)+P6(x1241)+P1(f41(x1242,x1241))
% 0.63/0.91 [133]P4(x1331,x1332)+E(x1331,f38(x1332))+~P4(x1331,f38(x1332))
% 0.63/0.91 [141]~P1(x1412)+P1(f6(x1411,x1412))+P6(f14(x1411,x1412))
% 0.63/0.91 [142]~P1(x1422)+P1(f41(x1422,x1421))+P6(f15(x1421,x1422))
% 0.63/0.91 [145]~P1(x1452)+P3(f14(x1451,x1452),x1452)+P1(f6(x1451,x1452))
% 0.63/0.91 [146]~P1(x1461)+P3(f15(x1462,x1461),x1461)+P1(f41(x1461,x1462))
% 0.63/0.91 [162]~P1(x1622)+~P4(f28(x1621),f28(f14(x1621,x1622)))+P1(f6(x1621,x1622))
% 0.63/0.91 [163]~P1(x1631)+~P4(f28(f15(x1632,x1631)),f28(x1632))+P1(f41(x1631,x1632))
% 0.63/0.91 [153]~P1(x1532)+P1(f6(x1531,x1532))+E(f16(f28(f14(x1531,x1532))),f16(f28(x1531)))
% 0.63/0.91 [154]~P1(x1542)+P1(f41(x1542,x1541))+E(f16(f28(f15(x1541,x1542))),f16(f28(x1541)))
% 0.63/0.91 [137]~P4(x1371,x1373)+P4(x1371,x1372)+~P4(x1373,x1372)
% 0.63/0.91 [147]E(x1471,x1472)+P3(x1471,x1473)+~P3(x1471,f41(x1473,x1472))
% 0.63/0.91 [148]E(x1481,x1482)+P3(x1481,x1483)+~P3(x1481,f6(x1482,x1483))
% 0.63/0.91 [149]~P2(x1493)+~E(f16(x1491),f16(x1492))+~P3(f22(x1491),f39(f16(x1492)))
% 0.63/0.91 [155]~P2(x1551)+~P4(f16(x1552),f16(x1553))+~P3(f21(x1553),f39(f16(x1552)))
% 0.63/0.91 [156]~P2(x1561)+~P4(f16(x1562),f16(x1563))+~P3(f32(x1563),f39(f16(x1562)))
% 0.63/0.91 [158]~P2(x1581)+~P4(f16(x1582),f16(x1583))+~P3(f27(x1583,x1582),f39(f16(x1584)))
% 0.63/0.91 [143]~P2(x1432)+~P5(x1431,a7)+E(f23(a10,f16(x1431)),x1431)+~E(f23(a40,f16(x1431)),a8)
% 0.63/0.91 [144]~P2(x1442)+~P5(x1441,a7)+E(f23(a10,f16(x1441)),x1441)+~E(f23(a40,f16(x1441)),a5)
% 0.63/0.91 [157]P4(x1571,x1572)+~E(f16(x1571),f16(x1572))+~P3(f22(x1572),x1573)+~P1(f6(f21(x1571),x1573))
% 0.63/0.91 [161]~P2(x1612)+~P5(x1611,a7)+~P3(f27(x1611,x1613),f39(f16(x1611)))+~E(f23(a40,f16(x1611)),a8)
% 0.63/0.91 [164]~P2(x1643)+~P5(x1642,a7)+~P3(f27(x1642,x1641),f39(f16(x1642)))+P4(f16(x1641),f23(a35,f16(x1642)))
% 0.63/0.91 [140]E(x1401,x1402)+~P2(x1403)+~E(f16(x1401),f16(x1402))+~P5(x1402,a7)+~P5(x1401,a7)
% 0.63/0.91 [159]~P6(x1591)+~P6(x1592)+~P3(x1592,x1593)+P4(f28(x1591),f28(x1592))+~P1(f6(x1591,x1593))+~E(f16(f28(x1592)),f16(f28(x1591)))
% 0.63/0.91 [160]~P6(x1602)+~P6(x1601)+~P3(x1601,x1603)+P4(f28(x1601),f28(x1602))+~P1(f41(x1603,x1602))+~E(f16(f28(x1601)),f16(f28(x1602)))
% 0.63/0.91 [166]~P2(x1663)+~P5(x1662,a7)+~P5(x1661,a7)+P4(f16(x1661),f16(x1662))+P4(f23(a35,f16(x1662)),f16(x1661))+~E(f23(a40,f16(x1661)),a5)+~E(f23(a40,f16(x1662)),a5)
% 0.63/0.91 [169]~P2(x1693)+~P5(x1692,a7)+~P5(x1691,a7)+P4(f16(x1691),f16(x1692))+~P4(f23(a35,f16(x1691)),f23(a35,f16(x1692)))+~E(f23(a40,f16(x1691)),a5)+~E(f23(a40,f16(x1692)),a5)
% 0.63/0.91 [165]~P2(x1653)+~P5(x1652,a7)+~E(f16(x1651),f16(x1652))+~P5(x1654,a7)+~P3(f22(x1651),f39(f16(x1654)))+~E(f23(a24,f16(x1652)),f16(x1652))+~E(f23(a40,f16(x1652)),a29)
% 0.63/0.91 [167]~P2(x1674)+~P5(x1671,a7)+~P5(x1673,a7)+~E(f16(x1671),f16(x1672))+~P3(f27(x1673,x1672),f39(f16(x1673)))+~E(f23(a40,f16(x1671)),a5)+~E(f23(a40,f16(x1673)),a5)
% 0.63/0.91 [168]~P2(x1683)+~P5(x1682,a7)+~P5(x1681,a7)+~P3(f21(x1681),f39(f16(x1684)))+P4(f23(a35,f16(x1681)),f16(x1682))+~E(f23(a24,f16(x1682)),f16(x1682))+~E(f23(a40,f16(x1681)),a5)+~E(f23(a40,f16(x1682)),a29)
% 0.63/0.91 [171]~P2(x1713)+~P5(x1714,a7)+~E(f12(x1713,x1714,x1712,x1715,x1711),f16(x1715))+~E(f16(x1712),f16(x1711))+~P3(f22(x1712),f39(f16(x1714)))+~P3(f22(x1715),f39(f16(x1711)))+~E(f16(x1711),a30)+~E(f23(a40,f16(x1711)),a8)
% 0.63/0.91 [172]~P2(x1721)+~E(f16(x1723),f16(x1725))+~P5(x1722,a7)+P4(f38(a37),f12(x1721,x1722,x1723,x1724,x1725))+~E(f16(x1725),a30)+~P3(f22(x1724),f39(f16(x1725)))+~P3(f22(x1723),f39(f16(x1722)))+~E(f23(a40,f16(x1725)),a8)
% 0.63/0.91 [173]~P2(x1733)+~P4(f16(x1731),f12(x1733,x1734,x1732,x1735,x1731))+~E(f16(x1731),f16(x1732))+~P5(x1734,a7)+~P3(f22(x1732),f39(f16(x1734)))+~E(f16(x1731),a30)+~P3(f22(x1735),f39(f16(x1731)))+~E(f23(a40,f16(x1731)),a8)
% 0.63/0.91 [174]~P2(x1743)+~E(f16(x1742),f16(x1741))+~P5(x1744,a7)+~P3(f22(x1742),f39(f16(x1744)))+~E(f16(x1741),a30)+~P3(f22(x1745),f39(f16(x1741)))+~P5(f12(x1743,x1744,x1742,x1745,x1741),f23(a9,f16(x1741)))+~E(f23(a40,f16(x1741)),a8)
% 0.63/0.91 [170]~P2(x1705)+~P5(x1701,a7)+~P5(x1702,a7)+~P3(f27(x1702,x1703),f39(f16(x1702)))+~P3(f22(x1704),f39(f16(x1702)))+~E(f23(a24,f16(x1701)),f16(x1701))+~E(f16(x1703),f23(a35,f16(x1702)))+~E(f16(x1704),f38(f23(a35,f16(x1702))))+~E(f23(a40,f16(x1701)),a29)+~E(f23(a40,f16(x1702)),a5)+~P4(a30,f38(f23(a35,f16(x1702))))
% 0.63/0.91 %EqnAxiom
% 0.63/0.91 [1]E(x11,x11)
% 0.63/0.91 [2]E(x22,x21)+~E(x21,x22)
% 0.63/0.91 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.63/0.91 [4]~E(x41,x42)+E(f16(x41),f16(x42))
% 0.63/0.91 [5]~E(x51,x52)+E(f23(x51,x53),f23(x52,x53))
% 0.63/0.91 [6]~E(x61,x62)+E(f23(x63,x61),f23(x63,x62))
% 0.63/0.91 [7]~E(x71,x72)+E(f38(x71),f38(x72))
% 0.63/0.91 [8]~E(x81,x82)+E(f12(x81,x83,x84,x85,x86),f12(x82,x83,x84,x85,x86))
% 0.63/0.91 [9]~E(x91,x92)+E(f12(x93,x91,x94,x95,x96),f12(x93,x92,x94,x95,x96))
% 0.63/0.91 [10]~E(x101,x102)+E(f12(x103,x104,x101,x105,x106),f12(x103,x104,x102,x105,x106))
% 0.63/0.91 [11]~E(x111,x112)+E(f12(x113,x114,x115,x111,x116),f12(x113,x114,x115,x112,x116))
% 0.63/0.91 [12]~E(x121,x122)+E(f12(x123,x124,x125,x126,x121),f12(x123,x124,x125,x126,x122))
% 0.63/0.91 [13]~E(x131,x132)+E(f39(x131),f39(x132))
% 0.63/0.91 [14]~E(x141,x142)+E(f22(x141),f22(x142))
% 0.63/0.91 [15]~E(x151,x152)+E(f28(x151),f28(x152))
% 0.63/0.91 [16]~E(x161,x162)+E(f27(x161,x163),f27(x162,x163))
% 0.63/0.92 [17]~E(x171,x172)+E(f27(x173,x171),f27(x173,x172))
% 0.63/0.92 [18]~E(x181,x182)+E(f21(x181),f21(x182))
% 0.63/0.92 [19]~E(x191,x192)+E(f31(x191),f31(x192))
% 0.63/0.92 [20]~E(x201,x202)+E(f11(x201),f11(x202))
% 0.63/0.92 [21]~E(x211,x212)+E(f6(x211,x213),f6(x212,x213))
% 0.63/0.92 [22]~E(x221,x222)+E(f6(x223,x221),f6(x223,x222))
% 0.63/0.92 [23]~E(x231,x232)+E(f13(x231),f13(x232))
% 0.63/0.92 [24]~E(x241,x242)+E(f41(x241,x243),f41(x242,x243))
% 0.63/0.92 [25]~E(x251,x252)+E(f41(x253,x251),f41(x253,x252))
% 0.63/0.92 [26]~E(x261,x262)+E(f33(x261),f33(x262))
% 0.63/0.92 [27]~E(x271,x272)+E(f15(x271,x273),f15(x272,x273))
% 0.63/0.92 [28]~E(x281,x282)+E(f15(x283,x281),f15(x283,x282))
% 0.63/0.92 [29]~E(x291,x292)+E(f26(x291),f26(x292))
% 0.63/0.92 [30]~E(x301,x302)+E(f32(x301),f32(x302))
% 0.63/0.92 [31]~E(x311,x312)+E(f43(x311),f43(x312))
% 0.63/0.92 [32]~E(x321,x322)+E(f25(x321),f25(x322))
% 0.63/0.92 [33]~E(x331,x332)+E(f14(x331,x333),f14(x332,x333))
% 0.63/0.92 [34]~E(x341,x342)+E(f14(x343,x341),f14(x343,x342))
% 0.63/0.92 [35]~E(x351,x352)+E(f19(x351),f19(x352))
% 0.63/0.92 [36]~P1(x361)+P1(x362)+~E(x361,x362)
% 0.63/0.92 [37]~P2(x371)+P2(x372)+~E(x371,x372)
% 0.63/0.92 [38]P4(x382,x383)+~E(x381,x382)+~P4(x381,x383)
% 0.63/0.92 [39]P4(x393,x392)+~E(x391,x392)+~P4(x393,x391)
% 0.63/0.92 [40]P5(x402,x403)+~E(x401,x402)+~P5(x401,x403)
% 0.63/0.92 [41]P5(x413,x412)+~E(x411,x412)+~P5(x413,x411)
% 0.63/0.92 [42]P3(x422,x423)+~E(x421,x422)+~P3(x421,x423)
% 0.63/0.92 [43]P3(x433,x432)+~E(x431,x432)+~P3(x433,x431)
% 0.63/0.92 [44]~P6(x441)+P6(x442)+~E(x441,x442)
% 0.63/0.92
% 0.63/0.92 %-------------------------------------------
% 0.63/0.92 cnf(175,plain,
% 0.63/0.92 (P6(f21(x1751))),
% 0.63/0.92 inference(equality_inference,[],[106])).
% 0.63/0.92 cnf(183,plain,
% 0.63/0.92 (P4(a2,a3)),
% 0.63/0.92 inference(equality_inference,[],[115])).
% 0.63/0.92 cnf(184,plain,
% 0.63/0.92 (~P2(x1841)+~P5(x1841,a7)),
% 0.63/0.92 inference(equality_inference,[],[122])).
% 0.63/0.92 cnf(185,plain,
% 0.63/0.92 (P3(x1851,f6(x1851,x1852))),
% 0.63/0.92 inference(equality_inference,[],[126])).
% 0.63/0.92 cnf(186,plain,
% 0.63/0.92 (P3(x1861,f41(x1862,x1861))),
% 0.63/0.92 inference(equality_inference,[],[127])).
% 0.63/0.92 cnf(190,plain,
% 0.63/0.92 (~P2(x1901)+~P3(f22(x1902),f39(f16(x1902)))),
% 0.63/0.92 inference(equality_inference,[],[149])).
% 0.63/0.92 cnf(194,plain,
% 0.63/0.92 (~P3(f22(x1941),f39(f16(x1941)))),
% 0.63/0.92 inference(scs_inference,[],[46,190])).
% 0.63/0.92 cnf(197,plain,
% 0.63/0.92 (~E(f16(a3),f16(a4))),
% 0.63/0.92 inference(scs_inference,[],[97,50,114,121])).
% 0.63/0.92 cnf(199,plain,
% 0.63/0.92 (E(f16(a2),f16(a3))),
% 0.63/0.92 inference(scs_inference,[],[47,97,50,114,121,2])).
% 0.63/0.92 cnf(202,plain,
% 0.63/0.92 (E(f28(f21(x2021)),x2021)),
% 0.63/0.92 inference(rename_variables,[],[51])).
% 0.63/0.92 cnf(205,plain,
% 0.63/0.92 (E(f28(f21(x2051)),x2051)),
% 0.63/0.92 inference(rename_variables,[],[51])).
% 0.63/0.92 cnf(207,plain,
% 0.63/0.92 (P4(x2071,f38(x2071))),
% 0.63/0.92 inference(scs_inference,[],[47,79,97,50,103,51,202,114,121,2,4,106,107,118])).
% 0.63/0.92 cnf(209,plain,
% 0.63/0.92 (~P4(f38(f38(x2091)),x2091)),
% 0.63/0.92 inference(scs_inference,[],[47,79,97,50,103,51,202,114,121,2,4,106,107,118,125])).
% 0.63/0.92 cnf(210,plain,
% 0.63/0.92 (~P4(f38(x2101),x2101)),
% 0.63/0.92 inference(rename_variables,[],[103])).
% 0.63/0.92 cnf(215,plain,
% 0.63/0.92 (~E(a2,f38(a3))),
% 0.63/0.92 inference(scs_inference,[],[46,183,47,48,79,97,50,103,210,51,202,114,121,2,4,106,107,118,125,122,3,38])).
% 0.63/0.92 cnf(223,plain,
% 0.63/0.92 (P3(f27(a4,a18),f39(f16(a4)))),
% 0.63/0.92 inference(scs_inference,[],[46,183,47,48,79,97,72,50,70,185,175,103,210,81,98,51,202,114,121,2,4,106,107,118,125,122,3,38,39,42,120,147])).
% 0.63/0.92 cnf(228,plain,
% 0.63/0.92 (P5(a17,a7)),
% 0.63/0.92 inference(scs_inference,[],[46,183,47,48,79,97,72,50,70,185,175,93,103,210,81,98,51,202,114,121,2,4,106,107,118,125,122,3,38,39,42,120,147,43,104])).
% 0.63/0.92 cnf(231,plain,
% 0.63/0.92 (E(f11(f21(x2311)),x2311)),
% 0.63/0.92 inference(scs_inference,[],[46,183,47,48,79,97,72,50,70,185,175,93,103,210,81,98,51,202,114,121,2,4,106,107,118,125,122,3,38,39,42,120,147,43,104,184,108])).
% 0.63/0.92 cnf(233,plain,
% 0.63/0.92 (P5(a18,a36)),
% 0.63/0.92 inference(scs_inference,[],[46,183,47,48,79,97,72,50,70,185,175,93,103,210,81,98,51,202,114,121,2,4,106,107,118,125,122,3,38,39,42,120,147,43,104,184,108,151])).
% 0.63/0.92 cnf(237,plain,
% 0.63/0.92 (~P4(f16(a18),f16(a4))),
% 0.63/0.92 inference(scs_inference,[],[46,183,47,48,79,97,72,50,70,185,175,93,103,210,81,98,51,202,114,121,2,4,106,107,118,125,122,3,38,39,42,120,147,43,104,184,108,151,152,158])).
% 0.63/0.92 cnf(248,plain,
% 0.63/0.92 (~P5(a4,a7)+E(f23(a10,f16(a4)),a4)),
% 0.63/0.92 inference(scs_inference,[],[46,183,47,48,79,97,72,50,55,70,185,175,93,94,103,210,81,98,91,51,202,205,114,121,2,4,106,107,118,125,122,3,38,39,42,120,147,43,104,184,108,151,152,158,36,37,40,41,130,44,144])).
% 0.63/0.92 cnf(254,plain,
% 0.63/0.92 (~E(f16(x2541),f16(x2542))+~P3(f22(x2541),f39(f16(x2542)))),
% 0.63/0.92 inference(scs_inference,[],[46,149])).
% 0.63/0.92 cnf(257,plain,
% 0.63/0.92 (~P4(f16(x2571),f16(x2572))+~P3(f27(x2572,x2571),f39(f16(x2573)))),
% 0.63/0.92 inference(scs_inference,[],[46,158])).
% 0.63/0.92 cnf(259,plain,
% 0.63/0.92 (~P5(x2591,a7)+~P3(f27(x2591,x2592),f39(f16(x2591)))+P4(f16(x2592),f23(a35,f16(x2591)))),
% 0.63/0.92 inference(scs_inference,[],[46,164])).
% 0.63/0.92 cnf(260,plain,
% 0.63/0.92 (~E(f16(x2601),f16(x2602))+~P5(x2602,a7)+~P5(x2603,a7)+~P3(f22(x2601),f39(f16(x2603)))+~E(f23(a24,f16(x2602)),f16(x2602))+~E(f23(a40,f16(x2602)),a29)),
% 0.63/0.92 inference(scs_inference,[],[46,165])).
% 0.63/0.92 cnf(262,plain,
% 0.63/0.92 (~P5(x2621,a7)+~E(f16(x2621),f16(x2622))+~P5(x2623,a7)+~P3(f27(x2623,x2622),f39(f16(x2623)))+~E(f23(a40,f16(x2621)),a5)+~E(f23(a40,f16(x2623)),a5)),
% 0.63/0.92 inference(scs_inference,[],[46,167])).
% 0.63/0.92 cnf(265,plain,
% 0.63/0.92 (~P5(x2651,a7)+~P5(x2652,a7)+~P3(f27(x2652,x2653),f39(f16(x2652)))+~P3(f22(x2654),f39(f16(x2652)))+~E(f23(a24,f16(x2651)),f16(x2651))+~E(f16(x2653),f23(a35,f16(x2652)))+~E(f16(x2654),f38(f23(a35,f16(x2652))))+~E(f23(a40,f16(x2651)),a29)+~E(f23(a40,f16(x2652)),a5)+~P4(a30,f38(f23(a35,f16(x2652))))),
% 0.63/0.92 inference(scs_inference,[],[46,170])).
% 0.63/0.92 cnf(266,plain,
% 0.63/0.92 (~P3(f22(a3),f39(f16(a2)))),
% 0.63/0.92 inference(scs_inference,[],[47,254])).
% 0.63/0.92 cnf(268,plain,
% 0.63/0.92 (~P3(f27(x2681,x2681),f39(f16(x2682)))),
% 0.63/0.92 inference(scs_inference,[],[47,53,254,257])).
% 0.63/0.92 cnf(269,plain,
% 0.63/0.92 (P4(x2691,x2691)),
% 0.63/0.92 inference(rename_variables,[],[53])).
% 0.63/0.92 cnf(271,plain,
% 0.63/0.92 (~P4(f38(f38(f38(x2711))),x2711)),
% 0.63/0.92 inference(scs_inference,[],[47,209,53,254,257,125])).
% 0.63/0.92 cnf(272,plain,
% 0.63/0.92 (~P4(f38(f38(x2721)),x2721)),
% 0.63/0.92 inference(rename_variables,[],[209])).
% 0.63/0.92 cnf(275,plain,
% 0.63/0.92 (E(f11(f21(x2751)),x2751)),
% 0.63/0.92 inference(rename_variables,[],[231])).
% 0.63/0.92 cnf(280,plain,
% 0.63/0.92 (~E(f38(f38(x2801)),x2801)),
% 0.63/0.92 inference(scs_inference,[],[47,209,272,53,231,275,254,257,125,107,106,114])).
% 0.63/0.92 cnf(283,plain,
% 0.63/0.92 (P4(x2831,f38(f38(x2831)))),
% 0.63/0.92 inference(scs_inference,[],[80,47,209,272,53,231,275,254,257,125,107,106,114,4,118])).
% 0.63/0.92 cnf(286,plain,
% 0.63/0.92 (P3(f22(a20),f39(f16(a4)))),
% 0.63/0.92 inference(scs_inference,[],[80,69,57,47,209,272,53,231,275,81,254,257,125,107,106,114,4,118,2,147])).
% 0.63/0.92 cnf(301,plain,
% 0.63/0.92 (P5(a4,a7)),
% 0.63/0.92 inference(scs_inference,[],[92,80,69,57,97,47,186,194,209,272,53,269,207,231,275,233,94,81,254,257,125,107,106,114,4,118,2,147,39,41,3,40,43,42,38,105])).
% 0.63/0.92 cnf(308,plain,
% 0.63/0.92 (~E(f16(a4),f16(a18))),
% 0.63/0.92 inference(scs_inference,[],[92,228,80,69,57,55,97,47,186,194,209,272,53,269,207,231,275,223,233,94,81,254,257,125,107,106,114,4,118,2,147,39,41,3,40,43,42,38,105,248,184,259,37,262])).
% 0.63/0.92 cnf(310,plain,
% 0.63/0.92 (~E(f16(a20),f38(f23(a35,f16(a4))))),
% 0.63/0.92 inference(scs_inference,[],[92,228,80,69,57,58,54,55,70,97,47,186,194,209,272,53,269,207,231,275,223,233,94,81,254,257,125,107,106,114,4,118,2,147,39,41,3,40,43,42,38,105,248,184,259,37,262,265])).
% 0.63/0.92 cnf(323,plain,
% 0.63/0.92 (E(f28(f22(x3231)),x3231)),
% 0.63/0.92 inference(rename_variables,[],[52])).
% 0.63/0.92 cnf(330,plain,
% 0.63/0.92 (~E(f38(f38(f38(x3301))),x3301)),
% 0.63/0.92 inference(scs_inference,[],[199,271,52,323,107,106,254,114])).
% 0.63/0.92 cnf(336,plain,
% 0.63/0.92 (P4(a2,f38(f38(a3)))),
% 0.63/0.92 inference(scs_inference,[],[55,183,199,271,197,283,52,323,107,106,254,114,118,2,4,137])).
% 0.63/0.92 cnf(339,plain,
% 0.63/0.92 (P4(f16(a18),f23(a35,f16(a4)))),
% 0.63/0.92 inference(scs_inference,[],[55,301,183,199,271,197,223,283,52,323,107,106,254,114,118,2,4,137,259])).
% 0.63/0.92 cnf(344,plain,
% 0.63/0.92 (P3(x3441,f6(x3441,x3442))),
% 0.63/0.92 inference(rename_variables,[],[185])).
% 0.63/0.92 cnf(351,plain,
% 0.63/0.92 (~E(f16(a20),f16(a17))),
% 0.63/0.92 inference(scs_inference,[],[55,301,58,54,183,228,199,280,268,271,197,237,185,344,223,59,283,286,52,323,107,106,254,114,118,2,4,137,259,3,43,42,39,38,260])).
% 0.63/0.92 cnf(362,plain,
% 0.63/0.92 (E(f19(f6(x3621,x3622)),x3621)),
% 0.63/0.92 inference(rename_variables,[],[64])).
% 0.63/0.92 cnf(376,plain,
% 0.63/0.92 (P3(x3761,f41(x3762,x3761))),
% 0.63/0.92 inference(rename_variables,[],[186])).
% 0.63/0.92 cnf(384,plain,
% 0.63/0.92 (P4(a2,f38(a3))),
% 0.63/0.92 inference(scs_inference,[],[55,50,183,209,330,308,266,339,186,376,237,336,64,362,106,118,107,114,2,4,3,42,39,43,38,257,133])).
% 0.63/0.92 cnf(398,plain,
% 0.63/0.92 (E(f43(f6(x3981,x3982)),x3982)),
% 0.63/0.92 inference(rename_variables,[],[65])).
% 0.63/0.92 cnf(405,plain,
% 0.63/0.92 (~P4(f38(a3),a2)),
% 0.63/0.92 inference(scs_inference,[],[54,215,351,103,384,65,398,114,107,106,2,4,130])).
% 0.63/0.92 cnf(455,plain,
% 0.63/0.92 (E(f26(f41(x4551,x4552)),x4551)),
% 0.63/0.92 inference(rename_variables,[],[67])).
% 0.63/0.92 cnf(460,plain,
% 0.63/0.92 ($false),
% 0.63/0.92 inference(scs_inference,[],[68,310,405,67,455,114,106,107,2]),
% 0.63/0.92 ['proof']).
% 0.63/0.92 % SZS output end Proof
% 0.63/0.92 % Total time :0.190000s
%------------------------------------------------------------------------------