%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG184+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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.11s 0.40s % Output : Refutation 0.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.07 % Problem : ALG184+1 : TPTP v8.1.0. Released v2.7.0. % 0.02/0.07 % Command : run_spass %d %s % 0.07/0.26 % Computer : n026.cluster.edu % 0.07/0.26 % Model : x86_64 x86_64 % 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.26 % Memory : 8042.1875MB % 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.26 % CPULimit : 300 % 0.07/0.26 % WCLimit : 600 % 0.07/0.26 % DateTime : Wed Jun 8 11:15:01 EDT 2022 % 0.07/0.26 % CPUTime : % 0.11/0.40 % 0.11/0.40 SPASS V 3.9 % 0.11/0.40 SPASS beiseite: Proof found. % 0.11/0.40 % SZS status Theorem % 0.11/0.40 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.11/0.40 SPASS derived 1434 clauses, backtracked 1460 clauses, performed 24 splits and kept 2618 clauses. % 0.11/0.40 SPASS allocated 86272 KBytes. % 0.11/0.40 SPASS spent 0:00:00.13 on the problem. % 0.11/0.40 0:00:00.02 for the input. % 0.11/0.40 0:00:00.02 for the FLOTTER CNF translation. % 0.11/0.40 0:00:00.00 for inferences. % 0.11/0.40 0:00:00.00 for the backtracking. % 0.11/0.40 0:00:00.08 for the reduction. % 0.11/0.40 % 0.11/0.40 % 0.11/0.40 Here is a proof with depth 4, length 414 : % 0.11/0.40 % SZS output start Refutation % 0.11/0.40 4[0:Inp] || equal(e14,e10)** -> . % 0.11/0.40 8[0:Inp] || equal(e13,e12)** -> . % 0.11/0.40 11[0:Inp] || equal(e21,e20)** -> . % 0.11/0.40 13[0:Inp] || equal(e23,e20)** -> . % 0.11/0.40 14[0:Inp] || equal(e24,e20)** -> . % 0.11/0.40 15[0:Inp] || equal(e22,e21)** -> . % 0.11/0.40 16[0:Inp] || equal(e23,e21)** -> . % 0.11/0.40 17[0:Inp] || equal(e24,e21)** -> . % 0.11/0.40 19[0:Inp] || equal(e24,e22)** -> . % 0.11/0.40 20[0:Inp] || equal(e24,e23)** -> . % 0.11/0.40 46[0:Inp] || -> equal(h(j(e20)),e20)**. % 0.11/0.40 47[0:Inp] || -> equal(h(j(e21)),e21)**. % 0.11/0.40 48[0:Inp] || -> equal(h(j(e22)),e22)**. % 0.11/0.40 49[0:Inp] || -> equal(h(j(e23)),e23)**. % 0.11/0.40 50[0:Inp] || -> equal(h(j(e24)),e24)**. % 0.11/0.40 52[0:Inp] || -> equal(j(h(e11)),e11)**. % 0.11/0.40 53[0:Inp] || -> equal(j(h(e12)),e12)**. % 0.11/0.40 56[0:Inp] || -> equal(op1(e10,e10),e14)**. % 0.11/0.40 57[0:Inp] || -> equal(op1(e10,e11),e12)**. % 0.11/0.40 60[0:Inp] || -> equal(op1(e10,e14),e13)**. % 0.11/0.40 61[0:Inp] || -> equal(op1(e11,e10),e10)**. % 0.11/0.40 62[0:Inp] || -> equal(op1(e11,e11),e11)**. % 0.11/0.40 63[0:Inp] || -> equal(op1(e11,e12),e12)**. % 0.11/0.40 67[0:Inp] || -> equal(op1(e12,e11),e14)**. % 0.11/0.40 68[0:Inp] || -> equal(op1(e12,e12),e13)**. % 0.11/0.40 69[0:Inp] || -> equal(op1(e12,e13),e10)**. % 0.11/0.40 72[0:Inp] || -> equal(op1(e13,e11),e10)**. % 0.11/0.40 74[0:Inp] || -> equal(op1(e13,e13),e12)**. % 0.11/0.40 76[0:Inp] || -> equal(op1(e14,e10),e12)**. % 0.11/0.40 77[0:Inp] || -> equal(op1(e14,e11),e13)**. % 0.11/0.40 80[0:Inp] || -> equal(op1(e14,e14),e10)**. % 0.11/0.40 81[0:Inp] || -> equal(op2(e20,e20),e20)**. % 0.11/0.40 82[0:Inp] || -> equal(op2(e20,e21),e23)**. % 0.11/0.40 83[0:Inp] || -> equal(op2(e20,e22),e24)**. % 0.11/0.40 85[0:Inp] || -> equal(op2(e20,e24),e21)**. % 0.11/0.40 86[0:Inp] || -> equal(op2(e21,e20),e22)**. % 0.11/0.40 87[0:Inp] || -> equal(op2(e21,e21),e21)**. % 0.11/0.40 90[0:Inp] || -> equal(op2(e21,e24),e20)**. % 0.11/0.40 92[0:Inp] || -> equal(op2(e22,e21),e24)**. % 0.11/0.40 93[0:Inp] || -> equal(op2(e22,e22),e22)**. % 0.11/0.40 94[0:Inp] || -> equal(op2(e22,e23),e20)**. % 0.11/0.40 96[0:Inp] || -> equal(op2(e23,e20),e24)**. % 0.11/0.40 97[0:Inp] || -> equal(op2(e23,e21),e20)**. % 0.11/0.40 98[0:Inp] || -> equal(op2(e23,e22),e21)**. % 0.11/0.40 99[0:Inp] || -> equal(op2(e23,e23),e23)**. % 0.11/0.40 101[0:Inp] || -> equal(op2(e24,e20),e23)**. % 0.11/0.40 104[0:Inp] || -> equal(op2(e24,e23),e21)**. % 0.11/0.40 105[0:Inp] || -> equal(op2(e24,e24),e24)**. % 0.11/0.40 106[0:Inp] || -> equal(op2(h(e10),h(e10)),h(op1(e10,e10)))**. % 0.11/0.40 107[0:Inp] || -> equal(op2(h(e10),h(e11)),h(op1(e10,e11)))**. % 0.11/0.40 110[0:Inp] || -> equal(op2(h(e10),h(e14)),h(op1(e10,e14)))**. % 0.11/0.40 118[0:Inp] || -> equal(op2(h(e12),h(e12)),h(op1(e12,e12)))**. % 0.11/0.40 119[0:Inp] || -> equal(op2(h(e12),h(e13)),h(op1(e12,e13)))**. % 0.11/0.40 124[0:Inp] || -> equal(op2(h(e13),h(e13)),h(op1(e13,e13)))**. % 0.11/0.40 126[0:Inp] || -> equal(op2(h(e14),h(e10)),h(op1(e14,e10)))**. % 0.11/0.40 130[0:Inp] || -> equal(op2(h(e14),h(e14)),h(op1(e14,e14)))**. % 0.11/0.40 131[0:Inp] || -> equal(op1(j(e20),j(e20)),j(op2(e20,e20)))**. % 0.11/0.40 132[0:Inp] || -> equal(op1(j(e20),j(e21)),j(op2(e20,e21)))**. % 0.11/0.40 133[0:Inp] || -> equal(op1(j(e20),j(e22)),j(op2(e20,e22)))**. % 0.11/0.40 135[0:Inp] || -> equal(op1(j(e20),j(e24)),j(op2(e20,e24)))**. % 0.11/0.40 136[0:Inp] || -> equal(op1(j(e21),j(e20)),j(op2(e21,e20)))**. % 0.11/0.40 140[0:Inp] || -> equal(op1(j(e21),j(e24)),j(op2(e21,e24)))**. % 0.11/0.40 142[0:Inp] || -> equal(op1(j(e22),j(e21)),j(op2(e22,e21)))**. % 0.11/0.40 144[0:Inp] || -> equal(op1(j(e22),j(e23)),j(op2(e22,e23)))**. % 0.11/0.40 146[0:Inp] || -> equal(op1(j(e23),j(e20)),j(op2(e23,e20)))**. % 0.11/0.40 147[0:Inp] || -> equal(op1(j(e23),j(e21)),j(op2(e23,e21)))**. % 0.11/0.40 148[0:Inp] || -> equal(op1(j(e23),j(e22)),j(op2(e23,e22)))**. % 0.11/0.40 149[0:Inp] || -> equal(op1(j(e23),j(e23)),j(op2(e23,e23)))**. % 0.11/0.40 151[0:Inp] || -> equal(op1(j(e24),j(e20)),j(op2(e24,e20)))**. % 0.11/0.40 154[0:Inp] || -> equal(op1(j(e24),j(e23)),j(op2(e24,e23)))**. % 0.11/0.40 155[0:Inp] || -> equal(op1(j(e24),j(e24)),j(op2(e24,e24)))**. % 0.11/0.40 156[0:Inp] || -> equal(j(e24),e14)** equal(j(e24),e13) equal(j(e24),e12) equal(j(e24),e11) equal(j(e24),e10). % 0.11/0.40 157[0:Inp] || -> equal(j(e23),e14)** equal(j(e23),e13) equal(j(e23),e12) equal(j(e23),e11) equal(j(e23),e10). % 0.11/0.40 158[0:Inp] || -> equal(j(e22),e14)** equal(j(e22),e13) equal(j(e22),e12) equal(j(e22),e11) equal(j(e22),e10). % 0.11/0.40 159[0:Inp] || -> equal(j(e21),e14)** equal(j(e21),e13) equal(j(e21),e12) equal(j(e21),e11) equal(j(e21),e10). % 0.11/0.40 160[0:Inp] || -> equal(j(e20),e14)** equal(j(e20),e13) equal(j(e20),e12) equal(j(e20),e11) equal(j(e20),e10). % 0.11/0.40 164[0:Inp] || -> equal(h(e11),e24)** equal(h(e11),e23) equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.11/0.40 166[0:Rew:105.0,155.0] || -> equal(op1(j(e24),j(e24)),j(e24))**. % 0.11/0.40 167[0:Rew:104.0,154.0] || -> equal(op1(j(e24),j(e23)),j(e21))**. % 0.11/0.40 170[0:Rew:101.0,151.0] || -> equal(op1(j(e24),j(e20)),j(e23))**. % 0.11/0.40 172[0:Rew:99.0,149.0] || -> equal(op1(j(e23),j(e23)),j(e23))**. % 0.11/0.40 173[0:Rew:98.0,148.0] || -> equal(op1(j(e23),j(e22)),j(e21))**. % 0.11/0.40 174[0:Rew:97.0,147.0] || -> equal(op1(j(e23),j(e21)),j(e20))**. % 0.11/0.40 175[0:Rew:96.0,146.0] || -> equal(op1(j(e23),j(e20)),j(e24))**. % 0.11/0.40 177[0:Rew:94.0,144.0] || -> equal(op1(j(e22),j(e23)),j(e20))**. % 0.11/0.40 179[0:Rew:92.0,142.0] || -> equal(op1(j(e22),j(e21)),j(e24))**. % 0.11/0.40 181[0:Rew:90.0,140.0] || -> equal(op1(j(e21),j(e24)),j(e20))**. % 0.11/0.40 185[0:Rew:86.0,136.0] || -> equal(op1(j(e21),j(e20)),j(e22))**. % 0.11/0.40 186[0:Rew:85.0,135.0] || -> equal(op1(j(e20),j(e24)),j(e21))**. % 0.11/0.40 188[0:Rew:83.0,133.0] || -> equal(op1(j(e20),j(e22)),j(e24))**. % 0.11/0.40 189[0:Rew:82.0,132.0] || -> equal(op1(j(e20),j(e21)),j(e23))**. % 0.11/0.40 190[0:Rew:81.0,131.0] || -> equal(op1(j(e20),j(e20)),j(e20))**. % 0.11/0.40 191[0:Rew:80.0,130.0] || -> equal(op2(h(e14),h(e14)),h(e10))**. % 0.11/0.40 195[0:Rew:76.0,126.0] || -> equal(op2(h(e14),h(e10)),h(e12))**. % 0.11/0.40 197[0:Rew:74.0,124.0] || -> equal(op2(h(e13),h(e13)),h(e12))**. % 0.11/0.40 202[0:Rew:69.0,119.0] || -> equal(op2(h(e12),h(e13)),h(e10))**. % 0.11/0.40 203[0:Rew:68.0,118.0] || -> equal(op2(h(e12),h(e12)),h(e13))**. % 0.11/0.40 211[0:Rew:60.0,110.0] || -> equal(op2(h(e10),h(e14)),h(e13))**. % 0.11/0.40 214[0:Rew:57.0,107.0] || -> equal(op2(h(e10),h(e11)),h(e12))**. % 0.11/0.40 215[0:Rew:56.0,106.0] || -> equal(op2(h(e10),h(e10)),h(e14))**. % 0.11/0.40 216[1:Spt:164.0] || -> equal(h(e11),e24)**. % 0.11/0.40 217[1:Rew:216.0,52.0] || -> equal(j(e24),e11)**. % 0.11/0.40 236[1:Rew:217.0,170.0] || -> equal(op1(e11,j(e20)),j(e23))**. % 0.11/0.40 243[1:Rew:217.0,186.0] || -> equal(op1(j(e20),e11),j(e21))**. % 0.11/0.40 246[2:Spt:160.0] || -> equal(j(e20),e14)**. % 0.11/0.40 247[2:Rew:246.0,46.0] || -> equal(h(e14),e20)**. % 0.11/0.40 259[2:Rew:246.0,243.0] || -> equal(op1(e14,e11),j(e21))**. % 0.11/0.40 262[2:Rew:247.0,191.0] || -> equal(op2(e20,e20),h(e10))**. % 0.11/0.40 293[2:Rew:77.0,259.0] || -> equal(j(e21),e13)**. % 0.11/0.40 294[2:Rew:293.0,47.0] || -> equal(h(e13),e21)**. % 0.11/0.40 300[2:Rew:294.0,197.0] || -> equal(op2(e21,e21),h(e12))**. % 0.11/0.40 302[2:Rew:294.0,202.0] || -> equal(op2(h(e12),e21),h(e10))**. % 0.11/0.40 313[2:Rew:81.0,262.0] || -> equal(h(e10),e20)**. % 0.11/0.40 349[2:Rew:87.0,300.0] || -> equal(h(e12),e21)**. % 0.11/0.40 393[2:Rew:87.0,302.0,349.0,302.0,313.0,302.0] || -> equal(e21,e20)**. % 0.11/0.40 394[2:MRR:393.0,11.0] || -> . % 0.11/0.40 396[2:Spt:394.0,160.0,246.0] || equal(j(e20),e14)** -> . % 0.11/0.40 397[2:Spt:394.0,160.1,160.2,160.3,160.4] || -> equal(j(e20),e13)** equal(j(e20),e12) equal(j(e20),e11) equal(j(e20),e10). % 0.11/0.40 398[3:Spt:397.0] || -> equal(j(e20),e13)**. % 0.11/0.40 399[3:Rew:398.0,46.0] || -> equal(h(e13),e20)**. % 0.11/0.40 402[3:Rew:398.0,243.0] || -> equal(op1(e13,e11),j(e21))**. % 0.11/0.40 426[3:Rew:399.0,197.0] || -> equal(op2(e20,e20),h(e12))**. % 0.11/0.40 431[3:Rew:72.0,402.0] || -> equal(j(e21),e10)**. % 0.11/0.40 432[3:Rew:431.0,47.0] || -> equal(h(e10),e21)**. % 0.11/0.40 444[3:Rew:432.0,215.0] || -> equal(op2(e21,e21),h(e14))**. % 0.11/0.40 445[3:Rew:432.0,195.0] || -> equal(op2(h(e14),e21),h(e12))**. % 0.11/0.40 471[3:Rew:81.0,426.0] || -> equal(h(e12),e20)**. % 0.11/0.40 503[3:Rew:87.0,444.0] || -> equal(h(e14),e21)**. % 0.11/0.40 547[3:Rew:87.0,445.0,503.0,445.0,471.0,445.0] || -> equal(e21,e20)**. % 0.11/0.40 548[3:MRR:547.0,11.0] || -> . % 0.11/0.40 550[3:Spt:548.0,397.0,398.0] || equal(j(e20),e13)** -> . % 0.11/0.40 551[3:Spt:548.0,397.1,397.2,397.3] || -> equal(j(e20),e12)** equal(j(e20),e11) equal(j(e20),e10). % 0.11/0.40 552[4:Spt:551.0] || -> equal(j(e20),e12)**. % 0.11/0.40 554[4:Rew:552.0,46.0] || -> equal(h(e12),e20)**. % 0.11/0.40 560[4:Rew:552.0,243.0] || -> equal(op1(e12,e11),j(e21))**. % 0.11/0.40 577[4:Rew:554.0,203.0] || -> equal(op2(e20,e20),h(e13))**. % 0.11/0.40 601[4:Rew:67.0,560.0] || -> equal(j(e21),e14)**. % 0.11/0.40 602[4:Rew:601.0,47.0] || -> equal(h(e14),e21)**. % 0.11/0.40 612[4:Rew:602.0,211.0] || -> equal(op2(h(e10),e21),h(e13))**. % 0.11/0.40 613[4:Rew:602.0,191.0] || -> equal(op2(e21,e21),h(e10))**. % 0.11/0.40 624[4:Rew:81.0,577.0] || -> equal(h(e13),e20)**. % 0.11/0.40 662[4:Rew:87.0,613.0] || -> equal(h(e10),e21)**. % 0.11/0.40 701[4:Rew:87.0,612.0,662.0,612.0,624.0,612.0] || -> equal(e21,e20)**. % 0.11/0.40 702[4:MRR:701.0,11.0] || -> . % 0.11/0.40 704[4:Spt:702.0,551.0,552.0] || equal(j(e20),e12)** -> . % 0.11/0.40 705[4:Spt:702.0,551.1,551.2] || -> equal(j(e20),e11)** equal(j(e20),e10). % 0.11/0.40 706[5:Spt:705.0] || -> equal(j(e20),e11)**. % 0.11/0.40 715[5:Rew:706.0,236.0] || -> equal(op1(e11,e11),j(e23))**. % 0.11/0.40 746[5:Rew:62.0,715.0] || -> equal(j(e23),e11)**. % 0.11/0.40 747[5:Rew:746.0,49.0] || -> equal(h(e11),e23)**. % 0.11/0.40 749[5:Rew:216.0,747.0] || -> equal(e24,e23)**. % 0.11/0.40 750[5:MRR:749.0,20.0] || -> . % 0.11/0.40 766[5:Spt:750.0,705.0,706.0] || equal(j(e20),e11)** -> . % 0.11/0.40 767[5:Spt:750.0,705.1] || -> equal(j(e20),e10)**. % 0.11/0.40 836[5:Rew:61.0,236.0,767.0,236.0] || -> equal(j(e23),e10)**. % 0.11/0.40 896[5:Rew:56.0,172.0,836.0,172.0] || -> equal(e14,e10)**. % 0.11/0.40 897[5:MRR:896.0,4.0] || -> . % 0.11/0.40 898[1:Spt:897.0,164.0,216.0] || equal(h(e11),e24)** -> . % 0.11/0.40 899[1:Spt:897.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.11/0.40 900[2:Spt:899.0] || -> equal(h(e11),e23)**. % 0.11/0.40 901[2:Rew:900.0,52.0] || -> equal(j(e23),e11)**. % 0.11/0.40 903[2:Rew:900.0,214.0] || -> equal(op2(h(e10),e23),h(e12))**. % 0.11/0.40 917[2:Rew:901.0,174.0] || -> equal(op1(e11,j(e21)),j(e20))**. % 0.11/0.40 929[2:Rew:901.0,167.0] || -> equal(op1(j(e24),e11),j(e21))**. % 0.11/0.40 931[3:Spt:156.0] || -> equal(j(e24),e14)**. % 0.11/0.40 932[3:Rew:931.0,50.0] || -> equal(h(e14),e24)**. % 0.11/0.40 945[3:Rew:931.0,929.0] || -> equal(op1(e14,e11),j(e21))**. % 0.11/0.40 948[3:Rew:932.0,191.0] || -> equal(op2(e24,e24),h(e10))**. % 0.11/0.40 979[3:Rew:77.0,945.0] || -> equal(j(e21),e13)**. % 0.11/0.40 980[3:Rew:979.0,47.0] || -> equal(h(e13),e21)**. % 0.11/0.40 987[3:Rew:980.0,202.0] || -> equal(op2(h(e12),e21),h(e10))**. % 0.11/0.40 988[3:Rew:980.0,197.0] || -> equal(op2(e21,e21),h(e12))**. % 0.11/0.40 999[3:Rew:105.0,948.0] || -> equal(h(e10),e24)**. % 0.11/0.40 1037[3:Rew:87.0,988.0] || -> equal(h(e12),e21)**. % 0.11/0.40 1079[3:Rew:87.0,987.0,1037.0,987.0,999.0,987.0] || -> equal(e24,e21)**. % 0.11/0.40 1080[3:MRR:1079.0,17.0] || -> . % 0.11/0.40 1082[3:Spt:1080.0,156.0,931.0] || equal(j(e24),e14)** -> . % 0.11/0.40 1083[3:Spt:1080.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.11/0.40 1084[4:Spt:1083.0] || -> equal(j(e24),e13)**. % 0.11/0.40 1085[4:Rew:1084.0,50.0] || -> equal(h(e13),e24)**. % 0.11/0.40 1087[4:Rew:1084.0,929.0] || -> equal(op1(e13,e11),j(e21))**. % 0.11/0.40 1110[4:Rew:1085.0,197.0] || -> equal(op2(e24,e24),h(e12))**. % 0.11/0.40 1117[4:Rew:72.0,1087.0] || -> equal(j(e21),e10)**. % 0.11/0.40 1118[4:Rew:1117.0,47.0] || -> equal(h(e10),e21)**. % 0.11/0.40 1130[4:Rew:1118.0,195.0] || -> equal(op2(h(e14),e21),h(e12))**. % 0.11/0.40 1131[4:Rew:1118.0,215.0] || -> equal(op2(e21,e21),h(e14))**. % 0.11/0.40 1154[4:Rew:105.0,1110.0] || -> equal(h(e12),e24)**. % 0.11/0.40 1188[4:Rew:87.0,1131.0] || -> equal(h(e14),e21)**. % 0.11/0.40 1232[4:Rew:87.0,1130.0,1188.0,1130.0,1154.0,1130.0] || -> equal(e24,e21)**. % 0.11/0.40 1233[4:MRR:1232.0,17.0] || -> . % 0.11/0.40 1235[4:Spt:1233.0,1083.0,1084.0] || equal(j(e24),e13)** -> . % 0.11/0.40 1236[4:Spt:1233.0,1083.1,1083.2,1083.3] || -> equal(j(e24),e12)** equal(j(e24),e11) equal(j(e24),e10). % 0.11/0.40 1237[5:Spt:1236.0] || -> equal(j(e24),e12)**. % 0.11/0.40 1239[5:Rew:1237.0,50.0] || -> equal(h(e12),e24)**. % 0.11/0.40 1246[5:Rew:1237.0,929.0] || -> equal(op1(e12,e11),j(e21))**. % 0.11/0.40 1262[5:Rew:1239.0,203.0] || -> equal(op2(e24,e24),h(e13))**. % 0.11/0.40 1287[5:Rew:67.0,1246.0] || -> equal(j(e21),e14)**. % 0.11/0.40 1288[5:Rew:1287.0,47.0] || -> equal(h(e14),e21)**. % 0.11/0.40 1297[5:Rew:1288.0,211.0] || -> equal(op2(h(e10),e21),h(e13))**. % 0.11/0.40 1299[5:Rew:1288.0,191.0] || -> equal(op2(e21,e21),h(e10))**. % 0.11/0.40 1310[5:Rew:105.0,1262.0] || -> equal(h(e13),e24)**. % 0.11/0.40 1348[5:Rew:87.0,1299.0] || -> equal(h(e10),e21)**. % 0.11/0.40 1387[5:Rew:87.0,1297.0,1348.0,1297.0,1310.0,1297.0] || -> equal(e24,e21)**. % 0.11/0.40 1388[5:MRR:1387.0,17.0] || -> . % 0.11/0.40 1390[5:Spt:1388.0,1236.0,1237.0] || equal(j(e24),e12)** -> . % 0.11/0.40 1391[5:Spt:1388.0,1236.1,1236.2] || -> equal(j(e24),e11)** equal(j(e24),e10). % 0.11/0.40 1392[6:Spt:1391.0] || -> equal(j(e24),e11)**. % 0.11/0.40 1397[6:Rew:1392.0,929.0] || -> equal(op1(e11,e11),j(e21))**. % 0.11/0.40 1412[6:Rew:62.0,1397.0] || -> equal(j(e21),e11)**. % 0.11/0.40 1417[6:Rew:1412.0,917.0] || -> equal(op1(e11,e11),j(e20))**. % 0.11/0.40 1434[6:Rew:62.0,1417.0] || -> equal(j(e20),e11)**. % 0.11/0.40 1435[6:Rew:1434.0,46.0] || -> equal(h(e11),e20)**. % 0.11/0.40 1439[6:Rew:900.0,1435.0] || -> equal(e23,e20)**. % 0.11/0.40 1440[6:MRR:1439.0,13.0] || -> . % 0.11/0.40 1451[6:Spt:1440.0,1391.0,1392.0] || equal(j(e24),e11)** -> . % 0.11/0.40 1452[6:Spt:1440.0,1391.1] || -> equal(j(e24),e10)**. % 0.11/0.40 1455[6:Rew:1452.0,50.0] || -> equal(h(e10),e24)**. % 0.11/0.40 1458[6:Rew:1455.0,903.0] || -> equal(op2(e24,e23),h(e12))**. % 0.11/0.40 1473[6:Rew:104.0,1458.0] || -> equal(h(e12),e21)**. % 0.11/0.40 1474[6:Rew:1473.0,53.0] || -> equal(j(e21),e12)**. % 0.11/0.40 1534[6:Rew:63.0,917.0,1474.0,917.0] || -> equal(j(e20),e12)**. % 0.11/0.40 1584[6:Rew:68.0,190.0,1534.0,190.0] || -> equal(e13,e12)**. % 0.11/0.40 1585[6:MRR:1584.0,8.0] || -> . % 0.11/0.40 1586[2:Spt:1585.0,899.0,900.0] || equal(h(e11),e23)** -> . % 0.11/0.40 1587[2:Spt:1585.0,899.1,899.2,899.3] || -> equal(h(e11),e22)** equal(h(e11),e21) equal(h(e11),e20). % 0.11/0.40 1588[3:Spt:1587.0] || -> equal(h(e11),e22)**. % 0.11/0.40 1590[3:Rew:1588.0,52.0] || -> equal(j(e22),e11)**. % 0.11/0.40 1606[3:Rew:1590.0,188.0] || -> equal(op1(j(e20),e11),j(e24))**. % 0.11/0.40 1616[3:Rew:1590.0,173.0] || -> equal(op1(j(e23),e11),j(e21))**. % 0.11/0.40 1618[3:Rew:1590.0,177.0] || -> equal(op1(e11,j(e23)),j(e20))**. % 0.11/0.40 1620[4:Spt:157.0] || -> equal(j(e23),e14)**. % 0.11/0.40 1621[4:Rew:1620.0,49.0] || -> equal(h(e14),e23)**. % 0.11/0.40 1632[4:Rew:1620.0,1616.0] || -> equal(op1(e14,e11),j(e21))**. % 0.11/0.40 1637[4:Rew:1621.0,191.0] || -> equal(op2(e23,e23),h(e10))**. % 0.11/0.40 1652[4:Rew:77.0,1632.0] || -> equal(j(e21),e13)**. % 0.11/0.40 1653[4:Rew:1652.0,47.0] || -> equal(h(e13),e21)**. % 0.11/0.40 1664[4:Rew:1653.0,202.0] || -> equal(op2(h(e12),e21),h(e10))**. % 0.11/0.40 1665[4:Rew:1653.0,197.0] || -> equal(op2(e21,e21),h(e12))**. % 0.11/0.40 1688[4:Rew:99.0,1637.0] || -> equal(h(e10),e23)**. % 0.11/0.40 1723[4:Rew:87.0,1665.0] || -> equal(h(e12),e21)**. % 0.11/0.40 1768[4:Rew:87.0,1664.0,1723.0,1664.0,1688.0,1664.0] || -> equal(e23,e21)**. % 0.11/0.40 1769[4:MRR:1768.0,16.0] || -> . % 0.11/0.40 1771[4:Spt:1769.0,157.0,1620.0] || equal(j(e23),e14)** -> . % 0.11/0.40 1772[4:Spt:1769.0,157.1,157.2,157.3,157.4] || -> equal(j(e23),e13)** equal(j(e23),e12) equal(j(e23),e11) equal(j(e23),e10). % 0.11/0.40 1773[5:Spt:1772.0] || -> equal(j(e23),e13)**. % 0.11/0.40 1774[5:Rew:1773.0,49.0] || -> equal(h(e13),e23)**. % 0.11/0.40 1778[5:Rew:1773.0,1616.0] || -> equal(op1(e13,e11),j(e21))**. % 0.11/0.40 1799[5:Rew:1774.0,197.0] || -> equal(op2(e23,e23),h(e12))**. % 0.11/0.40 1821[5:Rew:72.0,1778.0] || -> equal(j(e21),e10)**. % 0.11/0.40 1822[5:Rew:1821.0,47.0] || -> equal(h(e10),e21)**. % 0.11/0.40 1830[5:Rew:1822.0,195.0] || -> equal(op2(h(e14),e21),h(e12))**. % 0.11/0.40 1831[5:Rew:1822.0,215.0] || -> equal(op2(e21,e21),h(e14))**. % 0.11/0.40 1843[5:Rew:99.0,1799.0] || -> equal(h(e12),e23)**. % 0.11/0.40 1880[5:Rew:87.0,1831.0] || -> equal(h(e14),e21)**. % 0.11/0.40 1921[5:Rew:87.0,1830.0,1880.0,1830.0,1843.0,1830.0] || -> equal(e23,e21)**. % 0.11/0.40 1922[5:MRR:1921.0,16.0] || -> . % 0.11/0.40 1924[5:Spt:1922.0,1772.0,1773.0] || equal(j(e23),e13)** -> . % 0.11/0.40 1925[5:Spt:1922.0,1772.1,1772.2,1772.3] || -> equal(j(e23),e12)** equal(j(e23),e11) equal(j(e23),e10). % 0.11/0.40 1926[6:Spt:1925.0] || -> equal(j(e23),e12)**. % 0.11/0.40 1928[6:Rew:1926.0,49.0] || -> equal(h(e12),e23)**. % 0.11/0.40 1933[6:Rew:1926.0,1616.0] || -> equal(op1(e12,e11),j(e21))**. % 0.11/0.40 1951[6:Rew:1928.0,203.0] || -> equal(op2(e23,e23),h(e13))**. % 0.11/0.40 1960[6:Rew:67.0,1933.0] || -> equal(j(e21),e14)**. % 0.11/0.40 1961[6:Rew:1960.0,47.0] || -> equal(h(e14),e21)**. % 0.11/0.40 1974[6:Rew:1961.0,211.0] || -> equal(op2(h(e10),e21),h(e13))**. % 0.11/0.40 1976[6:Rew:1961.0,191.0] || -> equal(op2(e21,e21),h(e10))**. % 0.11/0.40 1999[6:Rew:99.0,1951.0] || -> equal(h(e13),e23)**. % 0.11/0.40 2034[6:Rew:87.0,1976.0] || -> equal(h(e10),e21)**. % 0.11/0.40 2076[6:Rew:87.0,1974.0,2034.0,1974.0,1999.0,1974.0] || -> equal(e23,e21)**. % 0.11/0.40 2077[6:MRR:2076.0,16.0] || -> . % 0.11/0.40 2079[6:Spt:2077.0,1925.0,1926.0] || equal(j(e23),e12)** -> . % 0.11/0.40 2080[6:Spt:2077.0,1925.1,1925.2] || -> equal(j(e23),e11)** equal(j(e23),e10). % 0.11/0.40 2081[7:Spt:2080.0] || -> equal(j(e23),e11)**. % 0.11/0.40 2086[7:Rew:2081.0,1618.0] || -> equal(op1(e11,e11),j(e20))**. % 0.11/0.40 2101[7:Rew:62.0,2086.0] || -> equal(j(e20),e11)**. % 0.11/0.40 2106[7:Rew:2101.0,1606.0] || -> equal(op1(e11,e11),j(e24))**. % 0.11/0.40 2123[7:Rew:62.0,2106.0] || -> equal(j(e24),e11)**. % 0.11/0.40 2124[7:Rew:2123.0,50.0] || -> equal(h(e11),e24)**. % 0.11/0.40 2128[7:Rew:1588.0,2124.0] || -> equal(e24,e22)**. % 0.11/0.40 2129[7:MRR:2128.0,19.0] || -> . % 0.11/0.40 2140[7:Spt:2129.0,2080.0,2081.0] || equal(j(e23),e11)** -> . % 0.11/0.40 2141[7:Spt:2129.0,2080.1] || -> equal(j(e23),e10)**. % 0.11/0.40 2215[7:Rew:61.0,1618.0,2141.0,1618.0] || -> equal(j(e20),e10)**. % 0.11/0.40 2222[7:Rew:57.0,1606.0,2215.0,1606.0] || -> equal(j(e24),e12)**. % 0.11/0.40 2272[7:Rew:68.0,166.0,2222.0,166.0] || -> equal(e13,e12)**. % 0.11/0.40 2273[7:MRR:2272.0,8.0] || -> . % 0.11/0.40 2274[3:Spt:2273.0,1587.0,1588.0] || equal(h(e11),e22)** -> . % 0.11/0.40 2275[3:Spt:2273.0,1587.1,1587.2] || -> equal(h(e11),e21)** equal(h(e11),e20). % 0.11/0.40 2276[4:Spt:2275.0] || -> equal(h(e11),e21)**. % 0.11/0.40 2278[4:Rew:2276.0,52.0] || -> equal(j(e21),e11)**. % 0.11/0.40 2281[4:Rew:2276.0,214.0] || -> equal(op2(h(e10),e21),h(e12))**. % 0.11/0.40 2300[4:Rew:2278.0,181.0] || -> equal(op1(e11,j(e24)),j(e20))**. % 0.11/0.40 2307[4:Rew:2278.0,179.0] || -> equal(op1(j(e22),e11),j(e24))**. % 0.11/0.40 2309[5:Spt:158.0] || -> equal(j(e22),e14)**. % 0.11/0.40 2310[5:Rew:2309.0,48.0] || -> equal(h(e14),e22)**. % 0.11/0.40 2323[5:Rew:2309.0,2307.0] || -> equal(op1(e14,e11),j(e24))**. % 0.11/0.41 2326[5:Rew:2310.0,191.0] || -> equal(op2(e22,e22),h(e10))**. % 0.11/0.41 2357[5:Rew:77.0,2323.0] || -> equal(j(e24),e13)**. % 0.11/0.41 2358[5:Rew:2357.0,50.0] || -> equal(h(e13),e24)**. % 0.11/0.41 2365[5:Rew:2358.0,202.0] || -> equal(op2(h(e12),e24),h(e10))**. % 0.11/0.41 2366[5:Rew:2358.0,197.0] || -> equal(op2(e24,e24),h(e12))**. % 0.11/0.41 2377[5:Rew:93.0,2326.0] || -> equal(h(e10),e22)**. % 0.11/0.41 2416[5:Rew:105.0,2366.0] || -> equal(h(e12),e24)**. % 0.11/0.41 2458[5:Rew:105.0,2365.0,2416.0,2365.0,2377.0,2365.0] || -> equal(e24,e22)**. % 0.11/0.41 2459[5:MRR:2458.0,19.0] || -> . % 0.11/0.41 2461[5:Spt:2459.0,158.0,2309.0] || equal(j(e22),e14)** -> . % 0.11/0.41 2462[5:Spt:2459.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.11/0.41 2463[6:Spt:2462.0] || -> equal(j(e22),e13)**. % 0.11/0.41 2464[6:Rew:2463.0,48.0] || -> equal(h(e13),e22)**. % 0.11/0.41 2466[6:Rew:2463.0,2307.0] || -> equal(op1(e13,e11),j(e24))**. % 0.11/0.41 2489[6:Rew:2464.0,197.0] || -> equal(op2(e22,e22),h(e12))**. % 0.11/0.41 2496[6:Rew:72.0,2466.0] || -> equal(j(e24),e10)**. % 0.11/0.41 2497[6:Rew:2496.0,50.0] || -> equal(h(e10),e24)**. % 0.11/0.41 2509[6:Rew:2497.0,195.0] || -> equal(op2(h(e14),e24),h(e12))**. % 0.11/0.41 2510[6:Rew:2497.0,215.0] || -> equal(op2(e24,e24),h(e14))**. % 0.11/0.41 2533[6:Rew:93.0,2489.0] || -> equal(h(e12),e22)**. % 0.11/0.41 2566[6:Rew:105.0,2510.0] || -> equal(h(e14),e24)**. % 0.11/0.41 2610[6:Rew:105.0,2509.0,2566.0,2509.0,2533.0,2509.0] || -> equal(e24,e22)**. % 0.11/0.41 2611[6:MRR:2610.0,19.0] || -> . % 0.11/0.41 2613[6:Spt:2611.0,2462.0,2463.0] || equal(j(e22),e13)** -> . % 0.11/0.41 2614[6:Spt:2611.0,2462.1,2462.2,2462.3] || -> equal(j(e22),e12)** equal(j(e22),e11) equal(j(e22),e10). % 0.11/0.41 2615[7:Spt:2614.0] || -> equal(j(e22),e12)**. % 0.11/0.41 2617[7:Rew:2615.0,48.0] || -> equal(h(e12),e22)**. % 0.11/0.41 2624[7:Rew:2615.0,2307.0] || -> equal(op1(e12,e11),j(e24))**. % 0.11/0.41 2640[7:Rew:2617.0,203.0] || -> equal(op2(e22,e22),h(e13))**. % 0.11/0.41 2665[7:Rew:67.0,2624.0] || -> equal(j(e24),e14)**. % 0.11/0.41 2666[7:Rew:2665.0,50.0] || -> equal(h(e14),e24)**. % 0.11/0.41 2675[7:Rew:2666.0,211.0] || -> equal(op2(h(e10),e24),h(e13))**. % 0.11/0.41 2677[7:Rew:2666.0,191.0] || -> equal(op2(e24,e24),h(e10))**. % 0.11/0.41 2688[7:Rew:93.0,2640.0] || -> equal(h(e13),e22)**. % 0.11/0.41 2727[7:Rew:105.0,2677.0] || -> equal(h(e10),e24)**. % 0.11/0.41 2766[7:Rew:105.0,2675.0,2727.0,2675.0,2688.0,2675.0] || -> equal(e24,e22)**. % 0.11/0.41 2767[7:MRR:2766.0,19.0] || -> . % 0.11/0.41 2769[7:Spt:2767.0,2614.0,2615.0] || equal(j(e22),e12)** -> . % 0.11/0.41 2770[7:Spt:2767.0,2614.1,2614.2] || -> equal(j(e22),e11)** equal(j(e22),e10). % 0.11/0.41 2771[8:Spt:2770.0] || -> equal(j(e22),e11)**. % 0.11/0.41 2776[8:Rew:2771.0,2307.0] || -> equal(op1(e11,e11),j(e24))**. % 0.11/0.41 2791[8:Rew:62.0,2776.0] || -> equal(j(e24),e11)**. % 0.11/0.41 2795[8:Rew:2791.0,2300.0] || -> equal(op1(e11,e11),j(e20))**. % 0.11/0.41 2813[8:Rew:62.0,2795.0] || -> equal(j(e20),e11)**. % 0.11/0.41 2814[8:Rew:2813.0,46.0] || -> equal(h(e11),e20)**. % 0.11/0.41 2817[8:Rew:2276.0,2814.0] || -> equal(e21,e20)**. % 0.11/0.41 2818[8:MRR:2817.0,11.0] || -> . % 0.11/0.41 2830[8:Spt:2818.0,2770.0,2771.0] || equal(j(e22),e11)** -> . % 0.11/0.41 2831[8:Spt:2818.0,2770.1] || -> equal(j(e22),e10)**. % 0.11/0.41 2834[8:Rew:2831.0,48.0] || -> equal(h(e10),e22)**. % 0.11/0.41 2837[8:Rew:2834.0,2281.0] || -> equal(op2(e22,e21),h(e12))**. % 0.11/0.41 2852[8:Rew:92.0,2837.0] || -> equal(h(e12),e24)**. % 0.11/0.41 2853[8:Rew:2852.0,53.0] || -> equal(j(e24),e12)**. % 0.11/0.41 2914[8:Rew:63.0,2300.0,2853.0,2300.0] || -> equal(j(e20),e12)**. % 0.11/0.41 2965[8:Rew:68.0,190.0,2914.0,190.0] || -> equal(e13,e12)**. % 0.11/0.41 2966[8:MRR:2965.0,8.0] || -> . % 0.11/0.41 2967[4:Spt:2966.0,2275.0,2276.0] || equal(h(e11),e21)** -> . % 0.11/0.41 2968[4:Spt:2966.0,2275.1] || -> equal(h(e11),e20)**. % 0.11/0.41 2971[4:Rew:2968.0,52.0] || -> equal(j(e20),e11)**. % 0.11/0.41 2980[4:Rew:2971.0,175.0] || -> equal(op1(j(e23),e11),j(e24))**. % 0.11/0.41 2996[4:Rew:2971.0,185.0] || -> equal(op1(j(e21),e11),j(e22))**. % 0.11/0.41 3000[4:Rew:2971.0,189.0] || -> equal(op1(e11,j(e21)),j(e23))**. % 0.11/0.41 3002[5:Spt:159.0] || -> equal(j(e21),e14)**. % 0.11/0.41 3003[5:Rew:3002.0,47.0] || -> equal(h(e14),e21)**. % 0.11/0.41 3007[5:Rew:3002.0,2996.0] || -> equal(op1(e14,e11),j(e22))**. % 0.11/0.41 3019[5:Rew:3003.0,191.0] || -> equal(op2(e21,e21),h(e10))**. % 0.11/0.41 3034[5:Rew:77.0,3007.0] || -> equal(j(e22),e13)**. % 0.11/0.41 3035[5:Rew:3034.0,48.0] || -> equal(h(e13),e22)**. % 0.11/0.41 3046[5:Rew:3035.0,202.0] || -> equal(op2(h(e12),e22),h(e10))**. % 0.11/0.41 3047[5:Rew:3035.0,197.0] || -> equal(op2(e22,e22),h(e12))**. % 0.11/0.41 3070[5:Rew:87.0,3019.0] || -> equal(h(e10),e21)**. % 0.11/0.41 3106[5:Rew:93.0,3047.0] || -> equal(h(e12),e22)**. % 0.11/0.41 3151[5:Rew:93.0,3046.0,3106.0,3046.0,3070.0,3046.0] || -> equal(e22,e21)**. % 0.11/0.41 3152[5:MRR:3151.0,15.0] || -> . % 0.11/0.41 3154[5:Spt:3152.0,159.0,3002.0] || equal(j(e21),e14)** -> . % 0.11/0.41 3155[5:Spt:3152.0,159.1,159.2,159.3,159.4] || -> equal(j(e21),e13)** equal(j(e21),e12) equal(j(e21),e11) equal(j(e21),e10). % 0.11/0.41 3156[6:Spt:3155.0] || -> equal(j(e21),e13)**. % 0.11/0.41 3157[6:Rew:3156.0,47.0] || -> equal(h(e13),e21)**. % 0.11/0.41 3163[6:Rew:3156.0,2996.0] || -> equal(op1(e13,e11),j(e22))**. % 0.11/0.41 3182[6:Rew:3157.0,197.0] || -> equal(op2(e21,e21),h(e12))**. % 0.11/0.41 3204[6:Rew:72.0,3163.0] || -> equal(j(e22),e10)**. % 0.11/0.41 3205[6:Rew:3204.0,48.0] || -> equal(h(e10),e22)**. % 0.11/0.41 3213[6:Rew:3205.0,195.0] || -> equal(op2(h(e14),e22),h(e12))**. % 0.11/0.41 3214[6:Rew:3205.0,215.0] || -> equal(op2(e22,e22),h(e14))**. % 0.11/0.41 3226[6:Rew:87.0,3182.0] || -> equal(h(e12),e21)**. % 0.11/0.41 3262[6:Rew:93.0,3214.0] || -> equal(h(e14),e22)**. % 0.11/0.41 3303[6:Rew:93.0,3213.0,3262.0,3213.0,3226.0,3213.0] || -> equal(e22,e21)**. % 0.11/0.41 3304[6:MRR:3303.0,15.0] || -> . % 0.11/0.41 3306[6:Spt:3304.0,3155.0,3156.0] || equal(j(e21),e13)** -> . % 0.11/0.41 3307[6:Spt:3304.0,3155.1,3155.2,3155.3] || -> equal(j(e21),e12)** equal(j(e21),e11) equal(j(e21),e10). % 0.11/0.41 3308[7:Spt:3307.0] || -> equal(j(e21),e12)**. % 0.11/0.41 3310[7:Rew:3308.0,47.0] || -> equal(h(e12),e21)**. % 0.11/0.41 3313[7:Rew:3308.0,2996.0] || -> equal(op1(e12,e11),j(e22))**. % 0.11/0.41 3333[7:Rew:3310.0,203.0] || -> equal(op2(e21,e21),h(e13))**. % 0.11/0.41 3342[7:Rew:67.0,3313.0] || -> equal(j(e22),e14)**. % 0.11/0.41 3343[7:Rew:3342.0,48.0] || -> equal(h(e14),e22)**. % 0.11/0.41 3356[7:Rew:3343.0,211.0] || -> equal(op2(h(e10),e22),h(e13))**. % 0.11/0.41 3358[7:Rew:3343.0,191.0] || -> equal(op2(e22,e22),h(e10))**. % 0.11/0.41 3381[7:Rew:87.0,3333.0] || -> equal(h(e13),e21)**. % 0.11/0.41 3417[7:Rew:93.0,3358.0] || -> equal(h(e10),e22)**. % 0.11/0.41 3459[7:Rew:93.0,3356.0,3417.0,3356.0,3381.0,3356.0] || -> equal(e22,e21)**. % 0.11/0.41 3460[7:MRR:3459.0,15.0] || -> . % 0.11/0.41 3462[7:Spt:3460.0,3307.0,3308.0] || equal(j(e21),e12)** -> . % 0.11/0.41 3463[7:Spt:3460.0,3307.1,3307.2] || -> equal(j(e21),e11)** equal(j(e21),e10). % 0.11/0.41 3464[8:Spt:3463.0] || -> equal(j(e21),e11)**. % 0.11/0.41 3469[8:Rew:3464.0,3000.0] || -> equal(op1(e11,e11),j(e23))**. % 0.11/0.41 3484[8:Rew:62.0,3469.0] || -> equal(j(e23),e11)**. % 0.11/0.41 3488[8:Rew:3484.0,2980.0] || -> equal(op1(e11,e11),j(e24))**. % 0.11/0.41 3506[8:Rew:62.0,3488.0] || -> equal(j(e24),e11)**. % 0.11/0.41 3507[8:Rew:3506.0,50.0] || -> equal(h(e11),e24)**. % 0.11/0.41 3510[8:Rew:2968.0,3507.0] || -> equal(e24,e20)**. % 0.11/0.41 3511[8:MRR:3510.0,14.0] || -> . % 0.11/0.41 3523[8:Spt:3511.0,3463.0,3464.0] || equal(j(e21),e11)** -> . % 0.11/0.41 3524[8:Spt:3511.0,3463.1] || -> equal(j(e21),e10)**. % 0.11/0.41 3598[8:Rew:61.0,3000.0,3524.0,3000.0] || -> equal(j(e23),e10)**. % 0.11/0.41 3606[8:Rew:57.0,2980.0,3598.0,2980.0] || -> equal(j(e24),e12)**. % 0.11/0.41 3657[8:Rew:68.0,166.0,3606.0,166.0] || -> equal(e13,e12)**. % 0.11/0.41 3658[8:MRR:3657.0,8.0] || -> . % 0.11/0.41 % SZS output end Refutation % 0.11/0.41 Formulae used in the proof : ax1 ax2 co1 ax4 ax5 % 0.11/0.41 %------------------------------------------------------------------------------