%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG185+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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 : 600s % DateTime : Thu Jul 14 18:02:50 EDT 2022 % Result : Theorem 0.17s 0.53s % Output : Refutation 0.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.11 % Problem : ALG185+1 : TPTP v8.1.0. Released v2.7.0. % 0.02/0.11 % Command : run_spass %d %s % 0.12/0.32 % Computer : n028.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 600 % 0.12/0.32 % DateTime : Thu Jun 9 04:08:47 EDT 2022 % 0.12/0.32 % CPUTime : % 0.17/0.53 % 0.17/0.53 SPASS V 3.9 % 0.17/0.53 SPASS beiseite: Proof found. % 0.17/0.53 % SZS status Theorem % 0.17/0.53 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.53 SPASS derived 1383 clauses, backtracked 1516 clauses, performed 24 splits and kept 2355 clauses. % 0.17/0.53 SPASS allocated 86230 KBytes. % 0.17/0.53 SPASS spent 0:00:00.21 on the problem. % 0.17/0.53 0:00:00.04 for the input. % 0.17/0.53 0:00:00.04 for the FLOTTER CNF translation. % 0.17/0.53 0:00:00.00 for inferences. % 0.17/0.53 0:00:00.00 for the backtracking. % 0.17/0.53 0:00:00.10 for the reduction. % 0.17/0.53 % 0.17/0.53 % 0.17/0.53 Here is a proof with depth 4, length 475 : % 0.17/0.53 % SZS output start Refutation % 0.17/0.53 1[0:Inp] || equal(e11,e10)** -> . % 0.17/0.53 3[0:Inp] || equal(e13,e10)** -> . % 0.17/0.53 4[0:Inp] || equal(e14,e10)** -> . % 0.17/0.53 6[0:Inp] || equal(e13,e11)** -> . % 0.17/0.53 7[0:Inp] || equal(e14,e11)** -> . % 0.17/0.53 9[0:Inp] || equal(e14,e12)** -> . % 0.17/0.53 11[0:Inp] || equal(e21,e20)** -> . % 0.17/0.53 13[0:Inp] || equal(e23,e20)** -> . % 0.17/0.53 16[0:Inp] || equal(e23,e21)** -> . % 0.17/0.53 17[0:Inp] || equal(e24,e21)** -> . % 0.17/0.53 18[0:Inp] || equal(e23,e22)** -> . % 0.17/0.53 19[0:Inp] || equal(e24,e22)** -> . % 0.17/0.53 46[0:Inp] || -> equal(h(j(e20)),e20)**. % 0.17/0.53 47[0:Inp] || -> equal(h(j(e21)),e21)**. % 0.17/0.53 48[0:Inp] || -> equal(h(j(e22)),e22)**. % 0.17/0.53 49[0:Inp] || -> equal(h(j(e23)),e23)**. % 0.17/0.53 50[0:Inp] || -> equal(h(j(e24)),e24)**. % 0.17/0.53 51[0:Inp] || -> equal(j(h(e10)),e10)**. % 0.17/0.53 52[0:Inp] || -> equal(j(h(e11)),e11)**. % 0.17/0.53 53[0:Inp] || -> equal(j(h(e12)),e12)**. % 0.17/0.53 54[0:Inp] || -> equal(j(h(e13)),e13)**. % 0.17/0.53 55[0:Inp] || -> equal(j(h(e14)),e14)**. % 0.17/0.53 56[0:Inp] || -> equal(op1(e10,e10),e10)**. % 0.17/0.53 57[0:Inp] || -> equal(op1(e10,e11),e13)**. % 0.17/0.53 58[0:Inp] || -> equal(op1(e10,e12),e14)**. % 0.17/0.53 59[0:Inp] || -> equal(op1(e10,e13),e11)**. % 0.17/0.53 60[0:Inp] || -> equal(op1(e10,e14),e12)**. % 0.17/0.53 61[0:Inp] || -> equal(op1(e11,e10),e14)**. % 0.17/0.53 63[0:Inp] || -> equal(op1(e11,e12),e13)**. % 0.17/0.53 64[0:Inp] || -> equal(op1(e11,e13),e12)**. % 0.17/0.53 66[0:Inp] || -> equal(op1(e12,e10),e11)**. % 0.17/0.53 69[0:Inp] || -> equal(op1(e12,e13),e14)**. % 0.17/0.53 70[0:Inp] || -> equal(op1(e12,e14),e13)**. % 0.17/0.53 71[0:Inp] || -> equal(op1(e13,e10),e12)**. % 0.17/0.53 72[0:Inp] || -> equal(op1(e13,e11),e14)**. % 0.17/0.53 73[0:Inp] || -> equal(op1(e13,e12),e10)**. % 0.17/0.53 76[0:Inp] || -> equal(op1(e14,e10),e13)**. % 0.17/0.53 78[0:Inp] || -> equal(op1(e14,e12),e11)**. % 0.17/0.53 79[0:Inp] || -> equal(op1(e14,e13),e10)**. % 0.17/0.53 81[0:Inp] || -> equal(op2(e20,e20),e20)**. % 0.17/0.53 82[0:Inp] || -> equal(op2(e20,e21),e23)**. % 0.17/0.53 83[0:Inp] || -> equal(op2(e20,e22),e24)**. % 0.17/0.53 84[0:Inp] || -> equal(op2(e20,e23),e22)**. % 0.17/0.53 85[0:Inp] || -> equal(op2(e20,e24),e21)**. % 0.17/0.53 86[0:Inp] || -> equal(op2(e21,e20),e22)**. % 0.17/0.53 88[0:Inp] || -> equal(op2(e21,e22),e23)**. % 0.17/0.53 89[0:Inp] || -> equal(op2(e21,e23),e24)**. % 0.17/0.53 90[0:Inp] || -> equal(op2(e21,e24),e20)**. % 0.17/0.53 91[0:Inp] || -> equal(op2(e22,e20),e21)**. % 0.17/0.53 92[0:Inp] || -> equal(op2(e22,e21),e24)**. % 0.17/0.53 93[0:Inp] || -> equal(op2(e22,e22),e22)**. % 0.17/0.53 94[0:Inp] || -> equal(op2(e22,e23),e20)**. % 0.17/0.53 95[0:Inp] || -> equal(op2(e22,e24),e23)**. % 0.17/0.53 96[0:Inp] || -> equal(op2(e23,e20),e24)**. % 0.17/0.53 97[0:Inp] || -> equal(op2(e23,e21),e20)**. % 0.17/0.53 98[0:Inp] || -> equal(op2(e23,e22),e21)**. % 0.17/0.53 100[0:Inp] || -> equal(op2(e23,e24),e22)**. % 0.17/0.53 101[0:Inp] || -> equal(op2(e24,e20),e23)**. % 0.17/0.53 102[0:Inp] || -> equal(op2(e24,e21),e22)**. % 0.17/0.53 103[0:Inp] || -> equal(op2(e24,e22),e20)**. % 0.17/0.53 104[0:Inp] || -> equal(op2(e24,e23),e21)**. % 0.17/0.53 105[0:Inp] || -> equal(op2(e24,e24),e24)**. % 0.17/0.53 107[0:Inp] || -> equal(op2(h(e10),h(e11)),h(op1(e10,e11)))**. % 0.17/0.53 108[0:Inp] || -> equal(op2(h(e10),h(e12)),h(op1(e10,e12)))**. % 0.17/0.53 110[0:Inp] || -> equal(op2(h(e10),h(e14)),h(op1(e10,e14)))**. % 0.17/0.53 111[0:Inp] || -> equal(op2(h(e11),h(e10)),h(op1(e11,e10)))**. % 0.17/0.53 113[0:Inp] || -> equal(op2(h(e11),h(e12)),h(op1(e11,e12)))**. % 0.17/0.53 116[0:Inp] || -> equal(op2(h(e12),h(e10)),h(op1(e12,e10)))**. % 0.17/0.53 120[0:Inp] || -> equal(op2(h(e12),h(e14)),h(op1(e12,e14)))**. % 0.17/0.53 121[0:Inp] || -> equal(op2(h(e13),h(e10)),h(op1(e13,e10)))**. % 0.17/0.53 122[0:Inp] || -> equal(op2(h(e13),h(e11)),h(op1(e13,e11)))**. % 0.17/0.53 126[0:Inp] || -> equal(op2(h(e14),h(e10)),h(op1(e14,e10)))**. % 0.17/0.53 128[0:Inp] || -> equal(op2(h(e14),h(e12)),h(op1(e14,e12)))**. % 0.17/0.53 132[0:Inp] || -> equal(op1(j(e20),j(e21)),j(op2(e20,e21)))**. % 0.17/0.53 134[0:Inp] || -> equal(op1(j(e20),j(e23)),j(op2(e20,e23)))**. % 0.17/0.53 135[0:Inp] || -> equal(op1(j(e20),j(e24)),j(op2(e20,e24)))**. % 0.17/0.53 136[0:Inp] || -> equal(op1(j(e21),j(e20)),j(op2(e21,e20)))**. % 0.17/0.53 138[0:Inp] || -> equal(op1(j(e21),j(e22)),j(op2(e21,e22)))**. % 0.17/0.53 139[0:Inp] || -> equal(op1(j(e21),j(e23)),j(op2(e21,e23)))**. % 0.17/0.53 140[0:Inp] || -> equal(op1(j(e21),j(e24)),j(op2(e21,e24)))**. % 0.17/0.53 142[0:Inp] || -> equal(op1(j(e22),j(e21)),j(op2(e22,e21)))**. % 0.17/0.53 144[0:Inp] || -> equal(op1(j(e22),j(e23)),j(op2(e22,e23)))**. % 0.17/0.53 145[0:Inp] || -> equal(op1(j(e22),j(e24)),j(op2(e22,e24)))**. % 0.17/0.53 146[0:Inp] || -> equal(op1(j(e23),j(e20)),j(op2(e23,e20)))**. % 0.17/0.53 147[0:Inp] || -> equal(op1(j(e23),j(e21)),j(op2(e23,e21)))**. % 0.17/0.53 150[0:Inp] || -> equal(op1(j(e23),j(e24)),j(op2(e23,e24)))**. % 0.17/0.53 152[0:Inp] || -> equal(op1(j(e24),j(e21)),j(op2(e24,e21)))**. % 0.17/0.53 154[0:Inp] || -> equal(op1(j(e24),j(e23)),j(op2(e24,e23)))**. % 0.17/0.53 156[0:Inp] || -> equal(j(e24),e14)** equal(j(e24),e13) equal(j(e24),e12) equal(j(e24),e11) equal(j(e24),e10). % 0.17/0.53 158[0:Inp] || -> equal(j(e22),e14)** equal(j(e22),e13) equal(j(e22),e12) equal(j(e22),e11) equal(j(e22),e10). % 0.17/0.53 163[0:Inp] || -> equal(h(e12),e24)** equal(h(e12),e23) equal(h(e12),e22) equal(h(e12),e21) equal(h(e12),e20). % 0.17/0.53 164[0:Inp] || -> equal(h(e11),e24)** equal(h(e11),e23) equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.17/0.53 165[0:Inp] || -> equal(h(e10),e24)** equal(h(e10),e23) equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.17/0.53 167[0:Rew:104.0,154.0] || -> equal(op1(j(e24),j(e23)),j(e21))**. % 0.17/0.53 169[0:Rew:102.0,152.0] || -> equal(op1(j(e24),j(e21)),j(e22))**. % 0.17/0.53 171[0:Rew:100.0,150.0] || -> equal(op1(j(e23),j(e24)),j(e22))**. % 0.17/0.53 174[0:Rew:97.0,147.0] || -> equal(op1(j(e23),j(e21)),j(e20))**. % 0.17/0.53 175[0:Rew:96.0,146.0] || -> equal(op1(j(e23),j(e20)),j(e24))**. % 0.17/0.53 176[0:Rew:95.0,145.0] || -> equal(op1(j(e22),j(e24)),j(e23))**. % 0.17/0.53 177[0:Rew:94.0,144.0] || -> equal(op1(j(e22),j(e23)),j(e20))**. % 0.17/0.53 179[0:Rew:92.0,142.0] || -> equal(op1(j(e22),j(e21)),j(e24))**. % 0.17/0.53 181[0:Rew:90.0,140.0] || -> equal(op1(j(e21),j(e24)),j(e20))**. % 0.17/0.53 182[0:Rew:89.0,139.0] || -> equal(op1(j(e21),j(e23)),j(e24))**. % 0.17/0.53 183[0:Rew:88.0,138.0] || -> equal(op1(j(e21),j(e22)),j(e23))**. % 0.17/0.53 185[0:Rew:86.0,136.0] || -> equal(op1(j(e21),j(e20)),j(e22))**. % 0.17/0.53 186[0:Rew:85.0,135.0] || -> equal(op1(j(e20),j(e24)),j(e21))**. % 0.17/0.53 187[0:Rew:84.0,134.0] || -> equal(op1(j(e20),j(e23)),j(e22))**. % 0.17/0.53 189[0:Rew:82.0,132.0] || -> equal(op1(j(e20),j(e21)),j(e23))**. % 0.17/0.53 193[0:Rew:78.0,128.0] || -> equal(op2(h(e14),h(e12)),h(e11))**. % 0.17/0.53 195[0:Rew:76.0,126.0] || -> equal(op2(h(e14),h(e10)),h(e13))**. % 0.17/0.53 199[0:Rew:72.0,122.0] || -> equal(op2(h(e13),h(e11)),h(e14))**. % 0.17/0.53 200[0:Rew:71.0,121.0] || -> equal(op2(h(e13),h(e10)),h(e12))**. % 0.17/0.53 201[0:Rew:70.0,120.0] || -> equal(op2(h(e12),h(e14)),h(e13))**. % 0.17/0.53 205[0:Rew:66.0,116.0] || -> equal(op2(h(e12),h(e10)),h(e11))**. % 0.17/0.53 208[0:Rew:63.0,113.0] || -> equal(op2(h(e11),h(e12)),h(e13))**. % 0.17/0.53 210[0:Rew:61.0,111.0] || -> equal(op2(h(e11),h(e10)),h(e14))**. % 0.17/0.53 211[0:Rew:60.0,110.0] || -> equal(op2(h(e10),h(e14)),h(e12))**. % 0.17/0.53 213[0:Rew:58.0,108.0] || -> equal(op2(h(e10),h(e12)),h(e14))**. % 0.17/0.53 214[0:Rew:57.0,107.0] || -> equal(op2(h(e10),h(e11)),h(e13))**. % 0.17/0.53 216[1:Spt:165.0] || -> equal(h(e10),e24)**. % 0.17/0.53 217[1:Rew:216.0,51.0] || -> equal(j(e24),e10)**. % 0.17/0.53 221[1:Rew:216.0,200.0] || -> equal(op2(h(e13),e24),h(e12))**. % 0.17/0.53 225[1:Rew:216.0,210.0] || -> equal(op2(h(e11),e24),h(e14))**. % 0.17/0.53 226[1:Rew:216.0,211.0] || -> equal(op2(e24,h(e14)),h(e12))**. % 0.17/0.53 229[1:Rew:216.0,214.0] || -> equal(op2(e24,h(e11)),h(e13))**. % 0.17/0.53 235[1:Rew:217.0,169.0] || -> equal(op1(e10,j(e21)),j(e22))**. % 0.17/0.53 246[2:Spt:164.0] || -> equal(h(e11),e24)**. % 0.17/0.53 260[2:Rew:246.0,229.0] || -> equal(op2(e24,e24),h(e13))**. % 0.17/0.53 282[2:Rew:105.0,260.0] || -> equal(h(e13),e24)**. % 0.17/0.53 283[2:Rew:282.0,54.0] || -> equal(j(e24),e13)**. % 0.17/0.53 286[2:Rew:217.0,283.0] || -> equal(e13,e10)**. % 0.17/0.53 287[2:MRR:286.0,3.0] || -> . % 0.17/0.53 302[2:Spt:287.0,164.0,246.0] || equal(h(e11),e24)** -> . % 0.17/0.53 303[2:Spt:287.0,164.1,164.2,164.3,164.4] || -> equal(h(e11),e23)** equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.17/0.53 304[3:Spt:303.0] || -> equal(h(e11),e23)**. % 0.17/0.53 307[3:Rew:304.0,229.0] || -> equal(op2(e24,e23),h(e13))**. % 0.17/0.53 309[3:Rew:304.0,225.0] || -> equal(op2(e23,e24),h(e14))**. % 0.17/0.53 334[3:Rew:104.0,307.0] || -> equal(h(e13),e21)**. % 0.17/0.53 335[3:Rew:334.0,54.0] || -> equal(j(e21),e13)**. % 0.17/0.53 336[3:Rew:334.0,221.0] || -> equal(op2(e21,e24),h(e12))**. % 0.17/0.53 346[3:Rew:335.0,185.0] || -> equal(op1(e13,j(e20)),j(e22))**. % 0.17/0.53 353[3:Rew:100.0,309.0] || -> equal(h(e14),e22)**. % 0.17/0.53 354[3:Rew:353.0,55.0] || -> equal(j(e22),e14)**. % 0.17/0.53 370[3:Rew:90.0,336.0] || -> equal(h(e12),e20)**. % 0.17/0.53 371[3:Rew:370.0,53.0] || -> equal(j(e20),e12)**. % 0.17/0.53 428[3:Rew:73.0,346.0,371.0,346.0,354.0,346.0] || -> equal(e14,e10)**. % 0.17/0.53 429[3:MRR:428.0,4.0] || -> . % 0.17/0.53 430[3:Spt:429.0,303.0,304.0] || equal(h(e11),e23)** -> . % 0.17/0.53 431[3:Spt:429.0,303.1,303.2,303.3] || -> equal(h(e11),e22)** equal(h(e11),e21) equal(h(e11),e20). % 0.17/0.53 432[4:Spt:431.0] || -> equal(h(e11),e22)**. % 0.17/0.53 439[4:Rew:432.0,225.0] || -> equal(op2(e22,e24),h(e14))**. % 0.17/0.53 441[4:Rew:432.0,229.0] || -> equal(op2(e24,e22),h(e13))**. % 0.17/0.53 463[4:Rew:95.0,439.0] || -> equal(h(e14),e23)**. % 0.17/0.53 464[4:Rew:463.0,55.0] || -> equal(j(e23),e14)**. % 0.17/0.53 467[4:Rew:463.0,226.0] || -> equal(op2(e24,e23),h(e12))**. % 0.17/0.53 479[4:Rew:464.0,174.0] || -> equal(op1(e14,j(e21)),j(e20))**. % 0.17/0.53 483[4:Rew:103.0,441.0] || -> equal(h(e13),e20)**. % 0.17/0.53 484[4:Rew:483.0,54.0] || -> equal(j(e20),e13)**. % 0.17/0.54 504[4:Rew:104.0,467.0] || -> equal(h(e12),e21)**. % 0.17/0.54 505[4:Rew:504.0,53.0] || -> equal(j(e21),e12)**. % 0.17/0.54 559[4:Rew:78.0,479.0,505.0,479.0,484.0,479.0] || -> equal(e13,e11)**. % 0.17/0.54 560[4:MRR:559.0,6.0] || -> . % 0.17/0.54 561[4:Spt:560.0,431.0,432.0] || equal(h(e11),e22)** -> . % 0.17/0.54 562[4:Spt:560.0,431.1,431.2] || -> equal(h(e11),e21)** equal(h(e11),e20). % 0.17/0.54 563[5:Spt:562.0] || -> equal(h(e11),e21)**. % 0.17/0.54 568[5:Rew:563.0,229.0] || -> equal(op2(e24,e21),h(e13))**. % 0.17/0.54 570[5:Rew:563.0,225.0] || -> equal(op2(e21,e24),h(e14))**. % 0.17/0.54 595[5:Rew:102.0,568.0] || -> equal(h(e13),e22)**. % 0.17/0.54 596[5:Rew:595.0,54.0] || -> equal(j(e22),e13)**. % 0.17/0.54 599[5:Rew:595.0,221.0] || -> equal(op2(e22,e24),h(e12))**. % 0.17/0.54 611[5:Rew:596.0,187.0] || -> equal(op1(j(e20),j(e23)),e13)**. % 0.17/0.54 614[5:Rew:90.0,570.0] || -> equal(h(e14),e20)**. % 0.17/0.54 615[5:Rew:614.0,55.0] || -> equal(j(e20),e14)**. % 0.17/0.54 634[5:Rew:95.0,599.0] || -> equal(h(e12),e23)**. % 0.17/0.54 635[5:Rew:634.0,53.0] || -> equal(j(e23),e12)**. % 0.17/0.54 689[5:Rew:78.0,611.0,615.0,611.0,635.0,611.0] || -> equal(e13,e11)**. % 0.17/0.54 690[5:MRR:689.0,6.0] || -> . % 0.17/0.54 691[5:Spt:690.0,562.0,563.0] || equal(h(e11),e21)** -> . % 0.17/0.54 692[5:Spt:690.0,562.1] || -> equal(h(e11),e20)**. % 0.17/0.54 695[5:Rew:692.0,52.0] || -> equal(j(e20),e11)**. % 0.17/0.54 702[5:Rew:85.0,225.0,692.0,225.0] || -> equal(h(e14),e21)**. % 0.17/0.54 703[5:Rew:702.0,55.0] || -> equal(j(e21),e14)**. % 0.17/0.54 709[5:Rew:101.0,229.0,692.0,229.0] || -> equal(h(e13),e23)**. % 0.17/0.54 710[5:Rew:709.0,54.0] || -> equal(j(e23),e13)**. % 0.17/0.54 722[5:Rew:60.0,235.0,703.0,235.0] || -> equal(j(e22),e12)**. % 0.17/0.54 780[5:Rew:69.0,177.0,722.0,177.0,710.0,177.0,695.0,177.0] || -> equal(e14,e11)**. % 0.17/0.54 781[5:MRR:780.0,7.0] || -> . % 0.17/0.54 787[1:Spt:781.0,165.0,216.0] || equal(h(e10),e24)** -> . % 0.17/0.54 788[1:Spt:781.0,165.1,165.2,165.3,165.4] || -> equal(h(e10),e23)** equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.17/0.54 789[2:Spt:788.0] || -> equal(h(e10),e23)**. % 0.17/0.54 790[2:Rew:789.0,51.0] || -> equal(j(e23),e10)**. % 0.17/0.54 807[2:Rew:790.0,174.0] || -> equal(op1(e10,j(e21)),j(e20))**. % 0.17/0.54 811[2:Rew:790.0,177.0] || -> equal(op1(j(e22),e10),j(e20))**. % 0.17/0.54 816[2:Rew:790.0,171.0] || -> equal(op1(e10,j(e24)),j(e22))**. % 0.17/0.54 818[2:Rew:790.0,167.0] || -> equal(op1(j(e24),e10),j(e21))**. % 0.17/0.54 820[3:Spt:156.0] || -> equal(j(e24),e14)**. % 0.17/0.54 832[3:Rew:820.0,816.0] || -> equal(op1(e10,e14),j(e22))**. % 0.17/0.54 834[3:Rew:820.0,818.0] || -> equal(op1(e14,e10),j(e21))**. % 0.17/0.54 849[3:Rew:60.0,832.0] || -> equal(j(e22),e12)**. % 0.17/0.54 850[3:Rew:849.0,48.0] || -> equal(h(e12),e22)**. % 0.17/0.54 857[3:Rew:849.0,811.0] || -> equal(op1(e12,e10),j(e20))**. % 0.17/0.54 861[3:Rew:850.0,208.0] || -> equal(op2(h(e11),e22),h(e13))**. % 0.17/0.54 869[3:Rew:76.0,834.0] || -> equal(j(e21),e13)**. % 0.17/0.54 870[3:Rew:869.0,47.0] || -> equal(h(e13),e21)**. % 0.17/0.54 890[3:Rew:66.0,857.0] || -> equal(j(e20),e11)**. % 0.17/0.54 891[3:Rew:890.0,46.0] || -> equal(h(e11),e20)**. % 0.17/0.54 946[3:Rew:83.0,861.0,891.0,861.0,870.0,861.0] || -> equal(e24,e21)**. % 0.17/0.54 947[3:MRR:946.0,17.0] || -> . % 0.17/0.54 948[3:Spt:947.0,156.0,820.0] || equal(j(e24),e14)** -> . % 0.17/0.54 949[3:Spt:947.0,156.1,156.2,156.3,156.4] || -> equal(j(e24),e13)** equal(j(e24),e12) equal(j(e24),e11) equal(j(e24),e10). % 0.17/0.54 950[4:Spt:949.0] || -> equal(j(e24),e13)**. % 0.17/0.54 953[4:Rew:950.0,818.0] || -> equal(op1(e13,e10),j(e21))**. % 0.17/0.54 955[4:Rew:950.0,816.0] || -> equal(op1(e10,e13),j(e22))**. % 0.17/0.54 980[4:Rew:71.0,953.0] || -> equal(j(e21),e12)**. % 0.17/0.54 981[4:Rew:980.0,47.0] || -> equal(h(e12),e21)**. % 0.17/0.54 984[4:Rew:980.0,807.0] || -> equal(op1(e10,e12),j(e20))**. % 0.17/0.54 995[4:Rew:981.0,193.0] || -> equal(op2(h(e14),e21),h(e11))**. % 0.17/0.54 997[4:Rew:59.0,955.0] || -> equal(j(e22),e11)**. % 0.17/0.54 998[4:Rew:997.0,48.0] || -> equal(h(e11),e22)**. % 0.17/0.54 1019[4:Rew:58.0,984.0] || -> equal(j(e20),e14)**. % 0.17/0.54 1020[4:Rew:1019.0,46.0] || -> equal(h(e14),e20)**. % 0.17/0.54 1074[4:Rew:82.0,995.0,1020.0,995.0,998.0,995.0] || -> equal(e23,e22)**. % 0.17/0.54 1075[4:MRR:1074.0,18.0] || -> . % 0.17/0.54 1076[4:Spt:1075.0,949.0,950.0] || equal(j(e24),e13)** -> . % 0.17/0.54 1077[4:Spt:1075.0,949.1,949.2,949.3] || -> equal(j(e24),e12)** equal(j(e24),e11) equal(j(e24),e10). % 0.17/0.54 1078[5:Spt:1077.0] || -> equal(j(e24),e12)**. % 0.17/0.54 1085[5:Rew:1078.0,816.0] || -> equal(op1(e10,e12),j(e22))**. % 0.17/0.54 1087[5:Rew:1078.0,818.0] || -> equal(op1(e12,e10),j(e21))**. % 0.17/0.54 1109[5:Rew:58.0,1085.0] || -> equal(j(e22),e14)**. % 0.17/0.54 1110[5:Rew:1109.0,48.0] || -> equal(h(e14),e22)**. % 0.17/0.54 1114[5:Rew:1109.0,811.0] || -> equal(op1(e14,e10),j(e20))**. % 0.17/0.54 1125[5:Rew:1110.0,199.0] || -> equal(op2(h(e13),h(e11)),e22)**. % 0.17/0.54 1129[5:Rew:66.0,1087.0] || -> equal(j(e21),e11)**. % 0.17/0.54 1130[5:Rew:1129.0,47.0] || -> equal(h(e11),e21)**. % 0.17/0.54 1150[5:Rew:76.0,1114.0] || -> equal(j(e20),e13)**. % 0.17/0.54 1151[5:Rew:1150.0,46.0] || -> equal(h(e13),e20)**. % 0.17/0.54 1206[5:Rew:82.0,1125.0,1151.0,1125.0,1130.0,1125.0] || -> equal(e23,e22)**. % 0.17/0.54 1207[5:MRR:1206.0,18.0] || -> . % 0.17/0.54 1208[5:Spt:1207.0,1077.0,1078.0] || equal(j(e24),e12)** -> . % 0.17/0.54 1209[5:Spt:1207.0,1077.1,1077.2] || -> equal(j(e24),e11)** equal(j(e24),e10). % 0.17/0.54 1210[6:Spt:1209.0] || -> equal(j(e24),e11)**. % 0.17/0.54 1215[6:Rew:1210.0,818.0] || -> equal(op1(e11,e10),j(e21))**. % 0.17/0.54 1217[6:Rew:1210.0,816.0] || -> equal(op1(e10,e11),j(e22))**. % 0.17/0.54 1242[6:Rew:61.0,1215.0] || -> equal(j(e21),e14)**. % 0.17/0.54 1243[6:Rew:1242.0,47.0] || -> equal(h(e14),e21)**. % 0.17/0.54 1246[6:Rew:1242.0,807.0] || -> equal(op1(e10,e14),j(e20))**. % 0.17/0.54 1257[6:Rew:1243.0,201.0] || -> equal(op2(h(e12),e21),h(e13))**. % 0.17/0.54 1259[6:Rew:57.0,1217.0] || -> equal(j(e22),e13)**. % 0.17/0.54 1260[6:Rew:1259.0,48.0] || -> equal(h(e13),e22)**. % 0.17/0.54 1281[6:Rew:60.0,1246.0] || -> equal(j(e20),e12)**. % 0.17/0.54 1282[6:Rew:1281.0,46.0] || -> equal(h(e12),e20)**. % 0.17/0.54 1336[6:Rew:82.0,1257.0,1282.0,1257.0,1260.0,1257.0] || -> equal(e23,e22)**. % 0.17/0.54 1337[6:MRR:1336.0,18.0] || -> . % 0.17/0.54 1338[6:Spt:1337.0,1209.0,1210.0] || equal(j(e24),e11)** -> . % 0.17/0.54 1339[6:Spt:1337.0,1209.1] || -> equal(j(e24),e10)**. % 0.17/0.54 1356[6:Rew:56.0,818.0,1339.0,818.0] || -> equal(j(e21),e10)**. % 0.17/0.54 1362[6:Rew:56.0,807.0,1356.0,807.0] || -> equal(j(e20),e10)**. % 0.17/0.54 1363[6:Rew:1362.0,46.0] || -> equal(h(e10),e20)**. % 0.17/0.54 1366[6:Rew:789.0,1363.0] || -> equal(e23,e20)**. % 0.17/0.54 1367[6:MRR:1366.0,13.0] || -> . % 0.17/0.54 1384[2:Spt:1367.0,788.0,789.0] || equal(h(e10),e23)** -> . % 0.17/0.54 1385[2:Spt:1367.0,788.1,788.2,788.3] || -> equal(h(e10),e22)** equal(h(e10),e21) equal(h(e10),e20). % 0.17/0.54 1386[3:Spt:1385.0] || -> equal(h(e10),e22)**. % 0.17/0.54 1388[3:Rew:1386.0,51.0] || -> equal(j(e22),e10)**. % 0.17/0.54 1391[3:Rew:1386.0,195.0] || -> equal(op2(h(e14),e22),h(e13))**. % 0.17/0.54 1395[3:Rew:1386.0,205.0] || -> equal(op2(h(e12),e22),h(e11))**. % 0.17/0.54 1400[3:Rew:1386.0,213.0] || -> equal(op2(e22,h(e12)),h(e14))**. % 0.17/0.54 1401[3:Rew:1386.0,214.0] || -> equal(op2(e22,h(e11)),h(e13))**. % 0.17/0.54 1416[3:Rew:1388.0,183.0] || -> equal(op1(j(e21),e10),j(e23))**. % 0.17/0.54 1418[4:Spt:163.0] || -> equal(h(e12),e24)**. % 0.17/0.54 1430[4:Rew:1418.0,1395.0] || -> equal(op2(e24,e22),h(e11))**. % 0.17/0.54 1432[4:Rew:1418.0,1400.0] || -> equal(op2(e22,e24),h(e14))**. % 0.17/0.54 1447[4:Rew:103.0,1430.0] || -> equal(h(e11),e20)**. % 0.17/0.54 1448[4:Rew:1447.0,52.0] || -> equal(j(e20),e11)**. % 0.17/0.54 1455[4:Rew:1447.0,1401.0] || -> equal(op2(e22,e20),h(e13))**. % 0.17/0.54 1460[4:Rew:1448.0,189.0] || -> equal(op1(e11,j(e21)),j(e23))**. % 0.17/0.54 1467[4:Rew:95.0,1432.0] || -> equal(h(e14),e23)**. % 0.17/0.54 1468[4:Rew:1467.0,55.0] || -> equal(j(e23),e14)**. % 0.17/0.54 1488[4:Rew:91.0,1455.0] || -> equal(h(e13),e21)**. % 0.17/0.54 1489[4:Rew:1488.0,54.0] || -> equal(j(e21),e13)**. % 0.17/0.54 1544[4:Rew:64.0,1460.0,1489.0,1460.0,1468.0,1460.0] || -> equal(e14,e12)**. % 0.17/0.54 1545[4:MRR:1544.0,9.0] || -> . % 0.17/0.54 1546[4:Spt:1545.0,163.0,1418.0] || equal(h(e12),e24)** -> . % 0.17/0.54 1547[4:Spt:1545.0,163.1,163.2,163.3,163.4] || -> equal(h(e12),e23)** equal(h(e12),e22) equal(h(e12),e21) equal(h(e12),e20). % 0.17/0.54 1548[5:Spt:1547.0] || -> equal(h(e12),e23)**. % 0.17/0.54 1551[5:Rew:1548.0,1400.0] || -> equal(op2(e22,e23),h(e14))**. % 0.17/0.54 1553[5:Rew:1548.0,1395.0] || -> equal(op2(e23,e22),h(e11))**. % 0.17/0.54 1578[5:Rew:94.0,1551.0] || -> equal(h(e14),e20)**. % 0.17/0.54 1579[5:Rew:1578.0,55.0] || -> equal(j(e20),e14)**. % 0.17/0.54 1582[5:Rew:1578.0,1391.0] || -> equal(op2(e20,e22),h(e13))**. % 0.17/0.54 1593[5:Rew:1579.0,186.0] || -> equal(op1(e14,j(e24)),j(e21))**. % 0.17/0.54 1597[5:Rew:98.0,1553.0] || -> equal(h(e11),e21)**. % 0.17/0.54 1598[5:Rew:1597.0,52.0] || -> equal(j(e21),e11)**. % 0.17/0.54 1617[5:Rew:83.0,1582.0] || -> equal(h(e13),e24)**. % 0.17/0.54 1618[5:Rew:1617.0,54.0] || -> equal(j(e24),e13)**. % 0.17/0.54 1672[5:Rew:79.0,1593.0,1618.0,1593.0,1598.0,1593.0] || -> equal(e11,e10)**. % 0.17/0.54 1673[5:MRR:1672.0,1.0] || -> . % 0.17/0.54 1674[5:Spt:1673.0,1547.0,1548.0] || equal(h(e12),e23)** -> . % 0.17/0.54 1675[5:Spt:1673.0,1547.1,1547.2,1547.3] || -> equal(h(e12),e22)** equal(h(e12),e21) equal(h(e12),e20). % 0.17/0.54 1676[6:Spt:1675.0] || -> equal(h(e12),e22)**. % 0.17/0.54 1685[6:Rew:1676.0,1400.0] || -> equal(op2(e22,e22),h(e14))**. % 0.17/0.54 1714[6:Rew:93.0,1685.0] || -> equal(h(e14),e22)**. % 0.17/0.54 1715[6:Rew:1714.0,55.0] || -> equal(j(e22),e14)**. % 0.17/0.54 1718[6:Rew:1388.0,1715.0] || -> equal(e14,e10)**. % 0.17/0.54 1719[6:MRR:1718.0,4.0] || -> . % 0.17/0.54 1734[6:Spt:1719.0,1675.0,1676.0] || equal(h(e12),e22)** -> . % 0.17/0.54 1735[6:Spt:1719.0,1675.1,1675.2] || -> equal(h(e12),e21)** equal(h(e12),e20). % 0.17/0.54 1736[7:Spt:1735.0] || -> equal(h(e12),e21)**. % 0.17/0.54 1741[7:Rew:1736.0,1400.0] || -> equal(op2(e22,e21),h(e14))**. % 0.17/0.54 1743[7:Rew:1736.0,1395.0] || -> equal(op2(e21,e22),h(e11))**. % 0.17/0.54 1768[7:Rew:92.0,1741.0] || -> equal(h(e14),e24)**. % 0.17/0.54 1769[7:Rew:1768.0,55.0] || -> equal(j(e24),e14)**. % 0.17/0.54 1770[7:Rew:1768.0,1391.0] || -> equal(op2(e24,e22),h(e13))**. % 0.17/0.54 1783[7:Rew:1769.0,175.0] || -> equal(op1(j(e23),j(e20)),e14)**. % 0.17/0.54 1787[7:Rew:88.0,1743.0] || -> equal(h(e11),e23)**. % 0.17/0.54 1788[7:Rew:1787.0,52.0] || -> equal(j(e23),e11)**. % 0.17/0.54 1804[7:Rew:103.0,1770.0] || -> equal(h(e13),e20)**. % 0.17/0.54 1805[7:Rew:1804.0,54.0] || -> equal(j(e20),e13)**. % 0.17/0.54 1862[7:Rew:64.0,1783.0,1788.0,1783.0,1805.0,1783.0] || -> equal(e14,e12)**. % 0.17/0.54 1863[7:MRR:1862.0,9.0] || -> . % 0.17/0.54 1864[7:Spt:1863.0,1735.0,1736.0] || equal(h(e12),e21)** -> . % 0.17/0.54 1865[7:Spt:1863.0,1735.1] || -> equal(h(e12),e20)**. % 0.17/0.54 1868[7:Rew:1865.0,53.0] || -> equal(j(e20),e12)**. % 0.17/0.54 1875[7:Rew:83.0,1395.0,1865.0,1395.0] || -> equal(h(e11),e24)**. % 0.17/0.54 1876[7:Rew:1875.0,52.0] || -> equal(j(e24),e11)**. % 0.17/0.54 1882[7:Rew:91.0,1400.0,1865.0,1400.0] || -> equal(h(e14),e21)**. % 0.17/0.54 1883[7:Rew:1882.0,55.0] || -> equal(j(e21),e14)**. % 0.17/0.54 1894[7:Rew:76.0,1416.0,1883.0,1416.0] || -> equal(j(e23),e13)**. % 0.17/0.54 1951[7:Rew:73.0,175.0,1894.0,175.0,1868.0,175.0,1876.0,175.0] || -> equal(e11,e10)**. % 0.17/0.54 1952[7:MRR:1951.0,1.0] || -> . % 0.17/0.54 1958[3:Spt:1952.0,1385.0,1386.0] || equal(h(e10),e22)** -> . % 0.17/0.54 1959[3:Spt:1952.0,1385.1,1385.2] || -> equal(h(e10),e21)** equal(h(e10),e20). % 0.17/0.54 1960[4:Spt:1959.0] || -> equal(h(e10),e21)**. % 0.17/0.54 1962[4:Rew:1960.0,51.0] || -> equal(j(e21),e10)**. % 0.17/0.54 1980[4:Rew:1962.0,181.0] || -> equal(op1(e10,j(e24)),j(e20))**. % 0.17/0.54 1985[4:Rew:1962.0,174.0] || -> equal(op1(j(e23),e10),j(e20))**. % 0.17/0.54 1986[4:Rew:1962.0,183.0] || -> equal(op1(e10,j(e22)),j(e23))**. % 0.17/0.54 1991[4:Rew:1962.0,179.0] || -> equal(op1(j(e22),e10),j(e24))**. % 0.17/0.54 1993[5:Spt:158.0] || -> equal(j(e22),e14)**. % 0.17/0.54 2002[5:Rew:1993.0,1986.0] || -> equal(op1(e10,e14),j(e23))**. % 0.17/0.54 2007[5:Rew:1993.0,1991.0] || -> equal(op1(e14,e10),j(e24))**. % 0.17/0.54 2022[5:Rew:60.0,2002.0] || -> equal(j(e23),e12)**. % 0.17/0.54 2023[5:Rew:2022.0,49.0] || -> equal(h(e12),e23)**. % 0.17/0.54 2030[5:Rew:2022.0,1985.0] || -> equal(op1(e12,e10),j(e20))**. % 0.17/0.54 2033[5:Rew:2023.0,208.0] || -> equal(op2(h(e11),e23),h(e13))**. % 0.17/0.54 2041[5:Rew:76.0,2007.0] || -> equal(j(e24),e13)**. % 0.17/0.54 2042[5:Rew:2041.0,50.0] || -> equal(h(e13),e24)**. % 0.17/0.54 2062[5:Rew:66.0,2030.0] || -> equal(j(e20),e11)**. % 0.17/0.54 2063[5:Rew:2062.0,46.0] || -> equal(h(e11),e20)**. % 0.17/0.54 2118[5:Rew:84.0,2033.0,2063.0,2033.0,2042.0,2033.0] || -> equal(e24,e22)**. % 0.17/0.54 2119[5:MRR:2118.0,19.0] || -> . % 0.17/0.54 2120[5:Spt:2119.0,158.0,1993.0] || equal(j(e22),e14)** -> . % 0.17/0.54 2121[5:Spt:2119.0,158.1,158.2,158.3,158.4] || -> equal(j(e22),e13)** equal(j(e22),e12) equal(j(e22),e11) equal(j(e22),e10). % 0.17/0.54 2122[6:Spt:2121.0] || -> equal(j(e22),e13)**. % 0.17/0.54 2125[6:Rew:2122.0,1991.0] || -> equal(op1(e13,e10),j(e24))**. % 0.17/0.54 2130[6:Rew:2122.0,1986.0] || -> equal(op1(e10,e13),j(e23))**. % 0.17/0.54 2152[6:Rew:71.0,2125.0] || -> equal(j(e24),e12)**. % 0.17/0.54 2153[6:Rew:2152.0,50.0] || -> equal(h(e12),e24)**. % 0.17/0.54 2157[6:Rew:2152.0,1980.0] || -> equal(op1(e10,e12),j(e20))**. % 0.17/0.54 2167[6:Rew:2153.0,193.0] || -> equal(op2(h(e14),e24),h(e11))**. % 0.17/0.54 2171[6:Rew:59.0,2130.0] || -> equal(j(e23),e11)**. % 0.17/0.54 2172[6:Rew:2171.0,49.0] || -> equal(h(e11),e23)**. % 0.17/0.54 2192[6:Rew:58.0,2157.0] || -> equal(j(e20),e14)**. % 0.17/0.54 2193[6:Rew:2192.0,46.0] || -> equal(h(e14),e20)**. % 0.17/0.54 2248[6:Rew:85.0,2167.0,2193.0,2167.0,2172.0,2167.0] || -> equal(e23,e21)**. % 0.17/0.54 2249[6:MRR:2248.0,16.0] || -> . % 0.17/0.54 2250[6:Spt:2249.0,2121.0,2122.0] || equal(j(e22),e13)** -> . % 0.17/0.54 2251[6:Spt:2249.0,2121.1,2121.2,2121.3] || -> equal(j(e22),e12)** equal(j(e22),e11) equal(j(e22),e10). % 0.17/0.54 2252[7:Spt:2251.0] || -> equal(j(e22),e12)**. % 0.17/0.54 2256[7:Rew:2252.0,1986.0] || -> equal(op1(e10,e12),j(e23))**. % 0.17/0.54 2261[7:Rew:2252.0,1991.0] || -> equal(op1(e12,e10),j(e24))**. % 0.17/0.54 2283[7:Rew:58.0,2256.0] || -> equal(j(e23),e14)**. % 0.17/0.54 2284[7:Rew:2283.0,49.0] || -> equal(h(e14),e23)**. % 0.17/0.54 2288[7:Rew:2283.0,1985.0] || -> equal(op1(e14,e10),j(e20))**. % 0.17/0.54 2298[7:Rew:2284.0,199.0] || -> equal(op2(h(e13),h(e11)),e23)**. % 0.17/0.54 2302[7:Rew:66.0,2261.0] || -> equal(j(e24),e11)**. % 0.17/0.54 2303[7:Rew:2302.0,50.0] || -> equal(h(e11),e24)**. % 0.17/0.54 2323[7:Rew:76.0,2288.0] || -> equal(j(e20),e13)**. % 0.17/0.54 2324[7:Rew:2323.0,46.0] || -> equal(h(e13),e20)**. % 0.17/0.54 2379[7:Rew:85.0,2298.0,2324.0,2298.0,2303.0,2298.0] || -> equal(e23,e21)**. % 0.17/0.54 2380[7:MRR:2379.0,16.0] || -> . % 0.17/0.54 2381[7:Spt:2380.0,2251.0,2252.0] || equal(j(e22),e12)** -> . % 0.17/0.54 2382[7:Spt:2380.0,2251.1,2251.2] || -> equal(j(e22),e11)** equal(j(e22),e10). % 0.17/0.54 2383[8:Spt:2382.0] || -> equal(j(e22),e11)**. % 0.17/0.54 2388[8:Rew:2383.0,1991.0] || -> equal(op1(e11,e10),j(e24))**. % 0.17/0.54 2393[8:Rew:2383.0,1986.0] || -> equal(op1(e10,e11),j(e23))**. % 0.17/0.54 2415[8:Rew:61.0,2388.0] || -> equal(j(e24),e14)**. % 0.17/0.54 2416[8:Rew:2415.0,50.0] || -> equal(h(e14),e24)**. % 0.17/0.54 2420[8:Rew:2415.0,1980.0] || -> equal(op1(e10,e14),j(e20))**. % 0.17/0.54 2430[8:Rew:2416.0,201.0] || -> equal(op2(h(e12),e24),h(e13))**. % 0.17/0.54 2434[8:Rew:57.0,2393.0] || -> equal(j(e23),e13)**. % 0.17/0.54 2435[8:Rew:2434.0,49.0] || -> equal(h(e13),e23)**. % 0.17/0.54 2455[8:Rew:60.0,2420.0] || -> equal(j(e20),e12)**. % 0.17/0.54 2456[8:Rew:2455.0,46.0] || -> equal(h(e12),e20)**. % 0.17/0.54 2511[8:Rew:85.0,2430.0,2456.0,2430.0,2435.0,2430.0] || -> equal(e23,e21)**. % 0.17/0.54 2512[8:MRR:2511.0,16.0] || -> . % 0.17/0.54 2513[8:Spt:2512.0,2382.0,2383.0] || equal(j(e22),e11)** -> . % 0.17/0.54 2514[8:Spt:2512.0,2382.1] || -> equal(j(e22),e10)**. % 0.17/0.54 2530[8:Rew:56.0,1991.0,2514.0,1991.0] || -> equal(j(e24),e10)**. % 0.17/0.54 2535[8:Rew:56.0,1980.0,2530.0,1980.0] || -> equal(j(e20),e10)**. % 0.17/0.54 2536[8:Rew:2535.0,46.0] || -> equal(h(e10),e20)**. % 0.17/0.54 2538[8:Rew:1960.0,2536.0] || -> equal(e21,e20)**. % 0.17/0.54 2539[8:MRR:2538.0,11.0] || -> . % 0.17/0.54 2557[4:Spt:2539.0,1959.0,1960.0] || equal(h(e10),e21)** -> . % 0.17/0.54 2558[4:Spt:2539.0,1959.1] || -> equal(h(e10),e20)**. % 0.17/0.54 2561[4:Rew:2558.0,51.0] || -> equal(j(e20),e10)**. % 0.17/0.54 2573[4:Rew:2558.0,195.0] || -> equal(op2(h(e14),e20),h(e13))**. % 0.17/0.54 2577[4:Rew:2558.0,205.0] || -> equal(op2(h(e12),e20),h(e11))**. % 0.17/0.54 2582[4:Rew:2558.0,213.0] || -> equal(op2(e20,h(e12)),h(e14))**. % 0.17/0.54 2583[4:Rew:2558.0,214.0] || -> equal(op2(e20,h(e11)),h(e13))**. % 0.17/0.54 2592[5:Spt:163.0] || -> equal(h(e12),e24)**. % 0.17/0.54 2604[5:Rew:2592.0,2577.0] || -> equal(op2(e24,e20),h(e11))**. % 0.17/0.54 2606[5:Rew:2592.0,2582.0] || -> equal(op2(e20,e24),h(e14))**. % 0.17/0.54 2621[5:Rew:101.0,2604.0] || -> equal(h(e11),e23)**. % 0.17/0.54 2622[5:Rew:2621.0,52.0] || -> equal(j(e23),e11)**. % 0.17/0.54 2629[5:Rew:2621.0,2583.0] || -> equal(op2(e20,e23),h(e13))**. % 0.17/0.54 2636[5:Rew:2622.0,183.0] || -> equal(op1(j(e21),j(e22)),e11)**. % 0.17/0.54 2641[5:Rew:85.0,2606.0] || -> equal(h(e14),e21)**. % 0.17/0.54 2642[5:Rew:2641.0,55.0] || -> equal(j(e21),e14)**. % 0.17/0.54 2662[5:Rew:84.0,2629.0] || -> equal(h(e13),e22)**. % 0.17/0.54 2663[5:Rew:2662.0,54.0] || -> equal(j(e22),e13)**. % 0.17/0.54 2718[5:Rew:79.0,2636.0,2642.0,2636.0,2663.0,2636.0] || -> equal(e11,e10)**. % 0.17/0.54 2719[5:MRR:2718.0,1.0] || -> . % 0.17/0.54 2720[5:Spt:2719.0,163.0,2592.0] || equal(h(e12),e24)** -> . % 0.17/0.54 2721[5:Spt:2719.0,163.1,163.2,163.3,163.4] || -> equal(h(e12),e23)** equal(h(e12),e22) equal(h(e12),e21) equal(h(e12),e20). % 0.17/0.54 2722[6:Spt:2721.0] || -> equal(h(e12),e23)**. % 0.17/0.54 2725[6:Rew:2722.0,2582.0] || -> equal(op2(e20,e23),h(e14))**. % 0.17/0.54 2727[6:Rew:2722.0,2577.0] || -> equal(op2(e23,e20),h(e11))**. % 0.17/0.54 2752[6:Rew:84.0,2725.0] || -> equal(h(e14),e22)**. % 0.17/0.54 2753[6:Rew:2752.0,55.0] || -> equal(j(e22),e14)**. % 0.17/0.54 2756[6:Rew:2752.0,2573.0] || -> equal(op2(e22,e20),h(e13))**. % 0.17/0.54 2767[6:Rew:2753.0,179.0] || -> equal(op1(e14,j(e21)),j(e24))**. % 0.17/0.54 2771[6:Rew:96.0,2727.0] || -> equal(h(e11),e24)**. % 0.17/0.54 2772[6:Rew:2771.0,52.0] || -> equal(j(e24),e11)**. % 0.17/0.54 2791[6:Rew:91.0,2756.0] || -> equal(h(e13),e21)**. % 0.17/0.54 2792[6:Rew:2791.0,54.0] || -> equal(j(e21),e13)**. % 0.17/0.54 2846[6:Rew:79.0,2767.0,2792.0,2767.0,2772.0,2767.0] || -> equal(e11,e10)**. % 0.17/0.54 2847[6:MRR:2846.0,1.0] || -> . % 0.17/0.54 2848[6:Spt:2847.0,2721.0,2722.0] || equal(h(e12),e23)** -> . % 0.17/0.54 2849[6:Spt:2847.0,2721.1,2721.2,2721.3] || -> equal(h(e12),e22)** equal(h(e12),e21) equal(h(e12),e20). % 0.17/0.54 2850[7:Spt:2849.0] || -> equal(h(e12),e22)**. % 0.17/0.54 2857[7:Rew:2850.0,2577.0] || -> equal(op2(e22,e20),h(e11))**. % 0.17/0.54 2859[7:Rew:2850.0,2582.0] || -> equal(op2(e20,e22),h(e14))**. % 0.17/0.54 2881[7:Rew:91.0,2857.0] || -> equal(h(e11),e21)**. % 0.17/0.54 2882[7:Rew:2881.0,52.0] || -> equal(j(e21),e11)**. % 0.17/0.54 2886[7:Rew:2881.0,2583.0] || -> equal(op2(e20,e21),h(e13))**. % 0.17/0.54 2897[7:Rew:2882.0,182.0] || -> equal(op1(e11,j(e23)),j(e24))**. % 0.17/0.54 2901[7:Rew:83.0,2859.0] || -> equal(h(e14),e24)**. % 0.17/0.54 2902[7:Rew:2901.0,55.0] || -> equal(j(e24),e14)**. % 0.17/0.54 2922[7:Rew:82.0,2886.0] || -> equal(h(e13),e23)**. % 0.17/0.54 2923[7:Rew:2922.0,54.0] || -> equal(j(e23),e13)**. % 0.17/0.54 2978[7:Rew:64.0,2897.0,2923.0,2897.0,2902.0,2897.0] || -> equal(e14,e12)**. % 0.17/0.54 2979[7:MRR:2978.0,9.0] || -> . % 0.17/0.54 2980[7:Spt:2979.0,2849.0,2850.0] || equal(h(e12),e22)** -> . % 0.17/0.54 2981[7:Spt:2979.0,2849.1,2849.2] || -> equal(h(e12),e21)** equal(h(e12),e20). % 0.17/0.54 2982[8:Spt:2981.0] || -> equal(h(e12),e21)**. % 0.17/0.54 2987[8:Rew:2982.0,2582.0] || -> equal(op2(e20,e21),h(e14))**. % 0.17/0.54 2989[8:Rew:2982.0,2577.0] || -> equal(op2(e21,e20),h(e11))**. % 0.17/0.54 3014[8:Rew:82.0,2987.0] || -> equal(h(e14),e23)**. % 0.17/0.54 3015[8:Rew:3014.0,55.0] || -> equal(j(e23),e14)**. % 0.17/0.54 3018[8:Rew:3014.0,2573.0] || -> equal(op2(e23,e20),h(e13))**. % 0.17/0.54 3029[8:Rew:3015.0,176.0] || -> equal(op1(j(e22),j(e24)),e14)**. % 0.17/0.54 3033[8:Rew:86.0,2989.0] || -> equal(h(e11),e22)**. % 0.17/0.54 3034[8:Rew:3033.0,52.0] || -> equal(j(e22),e11)**. % 0.17/0.54 3053[8:Rew:96.0,3018.0] || -> equal(h(e13),e24)**. % 0.17/0.54 3054[8:Rew:3053.0,54.0] || -> equal(j(e24),e13)**. % 0.17/0.54 3108[8:Rew:64.0,3029.0,3034.0,3029.0,3054.0,3029.0] || -> equal(e14,e12)**. % 0.17/0.54 3109[8:MRR:3108.0,9.0] || -> . % 0.17/0.54 3110[8:Spt:3109.0,2981.0,2982.0] || equal(h(e12),e21)** -> . % 0.17/0.54 3111[8:Spt:3109.0,2981.1] || -> equal(h(e12),e20)**. % 0.17/0.54 3127[8:Rew:81.0,2582.0,3111.0,2582.0] || -> equal(h(e14),e20)**. % 0.17/0.54 3133[8:Rew:81.0,2573.0,3127.0,2573.0] || -> equal(h(e13),e20)**. % 0.17/0.54 3134[8:Rew:3133.0,54.0] || -> equal(j(e20),e13)**. % 0.17/0.54 3137[8:Rew:2561.0,3134.0] || -> equal(e13,e10)**. % 0.17/0.54 3138[8:MRR:3137.0,3.0] || -> . % 0.17/0.54 % SZS output end Refutation % 0.17/0.54 Formulae used in the proof : ax1 ax2 co1 ax4 ax5 % 0.17/0.54 %------------------------------------------------------------------------------