%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG087+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 14 18:02:17 EDT 2022 % Result : Theorem 0.19s 0.50s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG087+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n022.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 8 03:31:50 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.50 % 0.19/0.50 SPASS V 3.9 % 0.19/0.50 SPASS beiseite: Proof found. % 0.19/0.50 % SZS status Theorem % 0.19/0.50 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.50 SPASS derived 590 clauses, backtracked 603 clauses, performed 12 splits and kept 1061 clauses. % 0.19/0.50 SPASS allocated 85686 KBytes. % 0.19/0.50 SPASS spent 0:00:00.15 on the problem. % 0.19/0.50 0:00:00.04 for the input. % 0.19/0.50 0:00:00.03 for the FLOTTER CNF translation. % 0.19/0.50 0:00:00.00 for inferences. % 0.19/0.50 0:00:00.00 for the backtracking. % 0.19/0.50 0:00:00.05 for the reduction. % 0.19/0.50 % 0.19/0.50 % 0.19/0.50 Here is a proof with depth 4, length 272 : % 0.19/0.50 % SZS output start Refutation % 0.19/0.50 1[0:Inp] || equal(e11,e10)** -> . % 0.19/0.50 2[0:Inp] || equal(e12,e10)** -> . % 0.19/0.50 3[0:Inp] || equal(e13,e10)** -> . % 0.19/0.50 4[0:Inp] || equal(e14,e10)** -> . % 0.19/0.50 11[0:Inp] || equal(e21,e20)** -> . % 0.19/0.50 12[0:Inp] || equal(e22,e20)** -> . % 0.19/0.50 14[0:Inp] || equal(e24,e20)** -> . % 0.19/0.50 15[0:Inp] || equal(e22,e21)** -> . % 0.19/0.50 16[0:Inp] || equal(e23,e21)** -> . % 0.19/0.50 46[0:Inp] || -> equal(h(j(e20)),e20)**. % 0.19/0.50 47[0:Inp] || -> equal(h(j(e21)),e21)**. % 0.19/0.50 48[0:Inp] || -> equal(h(j(e22)),e22)**. % 0.19/0.50 51[0:Inp] || -> equal(j(h(e10)),e10)**. % 0.19/0.50 52[0:Inp] || -> equal(j(h(e11)),e11)**. % 0.19/0.50 53[0:Inp] || -> equal(j(h(e12)),e12)**. % 0.19/0.50 54[0:Inp] || -> equal(j(h(e13)),e13)**. % 0.19/0.50 55[0:Inp] || -> equal(j(h(e14)),e14)**. % 0.19/0.50 56[0:Inp] || -> equal(op1(e10,e10),e10)**. % 0.19/0.50 57[0:Inp] || -> equal(op1(e10,e11),e11)**. % 0.19/0.50 61[0:Inp] || -> equal(op1(e11,e10),e11)**. % 0.19/0.50 62[0:Inp] || -> equal(op1(e11,e11),e10)**. % 0.19/0.50 63[0:Inp] || -> equal(op1(e11,e12),e13)**. % 0.19/0.50 67[0:Inp] || -> equal(op1(e12,e11),e14)**. % 0.19/0.50 68[0:Inp] || -> equal(op1(e12,e12),e10)**. % 0.19/0.50 71[0:Inp] || -> equal(op1(e13,e10),e13)**. % 0.19/0.50 72[0:Inp] || -> equal(op1(e13,e11),e12)**. % 0.19/0.50 76[0:Inp] || -> equal(op1(e14,e10),e14)**. % 0.19/0.50 77[0:Inp] || -> equal(op1(e14,e11),e13)**. % 0.19/0.50 78[0:Inp] || -> equal(op1(e14,e12),e11)**. % 0.19/0.50 79[0:Inp] || -> equal(op1(e14,e13),e12)**. % 0.19/0.50 82[0:Inp] || -> equal(op2(e20,e21),e21)**. % 0.19/0.50 83[0:Inp] || -> equal(op2(e20,e22),e22)**. % 0.19/0.50 84[0:Inp] || -> equal(op2(e20,e23),e23)**. % 0.19/0.50 85[0:Inp] || -> equal(op2(e20,e24),e24)**. % 0.19/0.50 86[0:Inp] || -> equal(op2(e21,e20),e21)**. % 0.19/0.50 87[0:Inp] || -> equal(op2(e21,e21),e20)**. % 0.19/0.50 88[0:Inp] || -> equal(op2(e21,e22),e24)**. % 0.19/0.50 89[0:Inp] || -> equal(op2(e21,e23),e22)**. % 0.19/0.50 90[0:Inp] || -> equal(op2(e21,e24),e23)**. % 0.19/0.50 93[0:Inp] || -> equal(op2(e22,e22),e23)**. % 0.19/0.50 94[0:Inp] || -> equal(op2(e22,e23),e20)**. % 0.19/0.50 95[0:Inp] || -> equal(op2(e22,e24),e21)**. % 0.19/0.50 97[0:Inp] || -> equal(op2(e23,e21),e22)**. % 0.19/0.50 98[0:Inp] || -> equal(op2(e23,e22),e21)**. % 0.19/0.50 99[0:Inp] || -> equal(op2(e23,e23),e24)**. % 0.19/0.50 100[0:Inp] || -> equal(op2(e23,e24),e20)**. % 0.19/0.50 103[0:Inp] || -> equal(op2(e24,e22),e20)**. % 0.19/0.50 104[0:Inp] || -> equal(op2(e24,e23),e21)**. % 0.19/0.50 105[0:Inp] || -> equal(op2(e24,e24),e22)**. % 0.19/0.50 113[0:Inp] || -> equal(op2(h(e11),h(e12)),h(op1(e11,e12)))**. % 0.19/0.50 117[0:Inp] || -> equal(op2(h(e12),h(e11)),h(op1(e12,e11)))**. % 0.19/0.50 118[0:Inp] || -> equal(op2(h(e12),h(e12)),h(op1(e12,e12)))**. % 0.19/0.50 121[0:Inp] || -> equal(op2(h(e13),h(e10)),h(op1(e13,e10)))**. % 0.19/0.50 122[0:Inp] || -> equal(op2(h(e13),h(e11)),h(op1(e13,e11)))**. % 0.19/0.50 126[0:Inp] || -> equal(op2(h(e14),h(e10)),h(op1(e14,e10)))**. % 0.19/0.50 127[0:Inp] || -> equal(op2(h(e14),h(e11)),h(op1(e14,e11)))**. % 0.19/0.50 128[0:Inp] || -> equal(op2(h(e14),h(e12)),h(op1(e14,e12)))**. % 0.19/0.50 129[0:Inp] || -> equal(op2(h(e14),h(e13)),h(op1(e14,e13)))**. % 0.19/0.50 133[0:Inp] || -> equal(op1(j(e20),j(e22)),j(op2(e20,e22)))**. % 0.19/0.50 134[0:Inp] || -> equal(op1(j(e20),j(e23)),j(op2(e20,e23)))**. % 0.19/0.50 135[0:Inp] || -> equal(op1(j(e20),j(e24)),j(op2(e20,e24)))**. % 0.19/0.50 136[0:Inp] || -> equal(op1(j(e21),j(e20)),j(op2(e21,e20)))**. % 0.19/0.50 137[0:Inp] || -> equal(op1(j(e21),j(e21)),j(op2(e21,e21)))**. % 0.19/0.50 138[0:Inp] || -> equal(op1(j(e21),j(e22)),j(op2(e21,e22)))**. % 0.19/0.50 139[0:Inp] || -> equal(op1(j(e21),j(e23)),j(op2(e21,e23)))**. % 0.19/0.50 140[0:Inp] || -> equal(op1(j(e21),j(e24)),j(op2(e21,e24)))**. % 0.19/0.50 143[0:Inp] || -> equal(op1(j(e22),j(e22)),j(op2(e22,e22)))**. % 0.19/0.50 144[0:Inp] || -> equal(op1(j(e22),j(e23)),j(op2(e22,e23)))**. % 0.19/0.50 145[0:Inp] || -> equal(op1(j(e22),j(e24)),j(op2(e22,e24)))**. % 0.19/0.50 148[0:Inp] || -> equal(op1(j(e23),j(e22)),j(op2(e23,e22)))**. % 0.19/0.50 149[0:Inp] || -> equal(op1(j(e23),j(e23)),j(op2(e23,e23)))**. % 0.19/0.50 150[0:Inp] || -> equal(op1(j(e23),j(e24)),j(op2(e23,e24)))**. % 0.19/0.50 153[0:Inp] || -> equal(op1(j(e24),j(e22)),j(op2(e24,e22)))**. % 0.19/0.50 154[0:Inp] || -> equal(op1(j(e24),j(e23)),j(op2(e24,e23)))**. % 0.19/0.50 155[0:Inp] || -> equal(op1(j(e24),j(e24)),j(op2(e24,e24)))**. % 0.19/0.50 163[0:Inp] || -> equal(h(e12),e24)** equal(h(e12),e23) equal(h(e12),e22) equal(h(e12),e21) equal(h(e12),e20). % 0.19/0.50 164[0:Inp] || -> equal(h(e11),e24)** equal(h(e11),e23) equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.19/0.50 165[0:Inp] || -> equal(h(e10),e24)** equal(h(e10),e23) equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.19/0.50 166[0:Rew:105.0,155.0] || -> equal(op1(j(e24),j(e24)),j(e22))**. % 0.19/0.50 167[0:Rew:104.0,154.0] || -> equal(op1(j(e24),j(e23)),j(e21))**. % 0.19/0.50 168[0:Rew:103.0,153.0] || -> equal(op1(j(e24),j(e22)),j(e20))**. % 0.19/0.50 171[0:Rew:100.0,150.0] || -> equal(op1(j(e23),j(e24)),j(e20))**. % 0.19/0.50 172[0:Rew:99.0,149.0] || -> equal(op1(j(e23),j(e23)),j(e24))**. % 0.19/0.50 173[0:Rew:98.0,148.0] || -> equal(op1(j(e23),j(e22)),j(e21))**. % 0.19/0.50 176[0:Rew:95.0,145.0] || -> equal(op1(j(e22),j(e24)),j(e21))**. % 0.19/0.50 177[0:Rew:94.0,144.0] || -> equal(op1(j(e22),j(e23)),j(e20))**. % 0.19/0.50 178[0:Rew:93.0,143.0] || -> equal(op1(j(e22),j(e22)),j(e23))**. % 0.19/0.50 181[0:Rew:90.0,140.0] || -> equal(op1(j(e21),j(e24)),j(e23))**. % 0.19/0.50 182[0:Rew:89.0,139.0] || -> equal(op1(j(e21),j(e23)),j(e22))**. % 0.19/0.50 183[0:Rew:88.0,138.0] || -> equal(op1(j(e21),j(e22)),j(e24))**. % 0.19/0.50 184[0:Rew:87.0,137.0] || -> equal(op1(j(e21),j(e21)),j(e20))**. % 0.19/0.50 185[0:Rew:86.0,136.0] || -> equal(op1(j(e21),j(e20)),j(e21))**. % 0.19/0.50 186[0:Rew:85.0,135.0] || -> equal(op1(j(e20),j(e24)),j(e24))**. % 0.19/0.50 187[0:Rew:84.0,134.0] || -> equal(op1(j(e20),j(e23)),j(e23))**. % 0.19/0.50 188[0:Rew:83.0,133.0] || -> equal(op1(j(e20),j(e22)),j(e22))**. % 0.19/0.50 192[0:Rew:79.0,129.0] || -> equal(op2(h(e14),h(e13)),h(e12))**. % 0.19/0.50 193[0:Rew:78.0,128.0] || -> equal(op2(h(e14),h(e12)),h(e11))**. % 0.19/0.50 194[0:Rew:77.0,127.0] || -> equal(op2(h(e14),h(e11)),h(e13))**. % 0.19/0.50 195[0:Rew:76.0,126.0] || -> equal(op2(h(e14),h(e10)),h(e14))**. % 0.19/0.50 199[0:Rew:72.0,122.0] || -> equal(op2(h(e13),h(e11)),h(e12))**. % 0.19/0.50 200[0:Rew:71.0,121.0] || -> equal(op2(h(e13),h(e10)),h(e13))**. % 0.19/0.50 203[0:Rew:68.0,118.0] || -> equal(op2(h(e12),h(e12)),h(e10))**. % 0.19/0.50 204[0:Rew:67.0,117.0] || -> equal(op2(h(e12),h(e11)),h(e14))**. % 0.19/0.50 208[0:Rew:63.0,113.0] || -> equal(op2(h(e11),h(e12)),h(e13))**. % 0.19/0.50 216[1:Spt:165.0] || -> equal(h(e10),e24)**. % 0.19/0.50 217[1:Rew:216.0,51.0] || -> equal(j(e24),e10)**. % 0.19/0.50 232[1:Rew:217.0,166.0] || -> equal(op1(e10,e10),j(e22))**. % 0.19/0.50 233[1:Rew:217.0,167.0] || -> equal(op1(e10,j(e23)),j(e21))**. % 0.19/0.50 246[1:Rew:56.0,232.0] || -> equal(j(e22),e10)**. % 0.19/0.50 251[1:Rew:246.0,178.0] || -> equal(op1(e10,e10),j(e23))**. % 0.19/0.50 257[1:Rew:56.0,251.0] || -> equal(j(e23),e10)**. % 0.19/0.50 263[1:Rew:56.0,233.0,257.0,233.0] || -> equal(j(e21),e10)**. % 0.19/0.50 265[1:Rew:263.0,184.0] || -> equal(op1(e10,e10),j(e20))**. % 0.19/0.50 270[1:Rew:56.0,265.0] || -> equal(j(e20),e10)**. % 0.19/0.50 271[1:Rew:270.0,46.0] || -> equal(h(e10),e20)**. % 0.19/0.50 275[1:Rew:216.0,271.0] || -> equal(e24,e20)**. % 0.19/0.50 276[1:MRR:275.0,14.0] || -> . % 0.19/0.50 291[1:Spt:276.0,165.0,216.0] || equal(h(e10),e24)** -> . % 0.19/0.50 292[1:Spt:276.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.19/0.50 293[2:Spt:292.0] || -> equal(h(e10),e23)**. % 0.19/0.50 294[2:Rew:293.0,51.0] || -> equal(j(e23),e10)**. % 0.19/0.50 311[2:Rew:294.0,172.0] || -> equal(op1(e10,e10),j(e24))**. % 0.19/0.50 314[2:Rew:294.0,167.0] || -> equal(op1(j(e24),e10),j(e21))**. % 0.19/0.50 324[2:Rew:56.0,311.0] || -> equal(j(e24),e10)**. % 0.19/0.50 353[2:Rew:56.0,314.0,324.0,314.0] || -> equal(j(e21),e10)**. % 0.19/0.50 354[2:Rew:353.0,47.0] || -> equal(h(e10),e21)**. % 0.19/0.50 357[2:Rew:293.0,354.0] || -> equal(e23,e21)**. % 0.19/0.50 358[2:MRR:357.0,16.0] || -> . % 0.19/0.50 371[2:Spt:358.0,292.0,293.0] || equal(h(e10),e23)** -> . % 0.19/0.50 372[2:Spt:358.0,292.1,292.2,292.3] || -> equal(h(e10),e22)** equal(h(e10),e21) equal(h(e10),e20). % 0.19/0.50 373[3:Spt:372.0] || -> equal(h(e10),e22)**. % 0.19/0.50 375[3:Rew:373.0,51.0] || -> equal(j(e22),e10)**. % 0.19/0.50 391[3:Rew:375.0,173.0] || -> equal(op1(j(e23),e10),j(e21))**. % 0.19/0.50 394[3:Rew:375.0,178.0] || -> equal(op1(e10,e10),j(e23))**. % 0.19/0.50 405[3:Rew:56.0,394.0] || -> equal(j(e23),e10)**. % 0.19/0.50 422[3:Rew:56.0,391.0,405.0,391.0] || -> equal(j(e21),e10)**. % 0.19/0.50 424[3:Rew:422.0,184.0] || -> equal(op1(e10,e10),j(e20))**. % 0.19/0.50 429[3:Rew:56.0,424.0] || -> equal(j(e20),e10)**. % 0.19/0.50 430[3:Rew:429.0,46.0] || -> equal(h(e10),e20)**. % 0.19/0.51 434[3:Rew:373.0,430.0] || -> equal(e22,e20)**. % 0.19/0.51 435[3:MRR:434.0,12.0] || -> . % 0.19/0.51 450[3:Spt:435.0,372.0,373.0] || equal(h(e10),e22)** -> . % 0.19/0.51 451[3:Spt:435.0,372.1,372.2] || -> equal(h(e10),e21)** equal(h(e10),e20). % 0.19/0.51 452[4:Spt:451.0] || -> equal(h(e10),e21)**. % 0.19/0.51 454[4:Rew:452.0,51.0] || -> equal(j(e21),e10)**. % 0.19/0.51 471[4:Rew:454.0,183.0] || -> equal(op1(e10,j(e22)),j(e24))**. % 0.19/0.51 474[4:Rew:454.0,182.0] || -> equal(op1(e10,j(e23)),j(e22))**. % 0.19/0.51 482[4:Rew:454.0,184.0] || -> equal(op1(e10,e10),j(e20))**. % 0.19/0.51 485[4:Rew:56.0,482.0] || -> equal(j(e20),e10)**. % 0.19/0.51 487[4:Rew:485.0,188.0] || -> equal(op1(e10,j(e22)),j(e22))**. % 0.19/0.51 489[4:Rew:485.0,168.0] || -> equal(op1(j(e24),j(e22)),e10)**. % 0.19/0.51 501[4:Rew:471.0,487.0] || -> equal(j(e24),j(e22))**. % 0.19/0.51 514[4:Rew:178.0,489.0,501.0,489.0] || -> equal(j(e23),e10)**. % 0.19/0.51 517[4:Rew:514.0,474.0] || -> equal(op1(e10,e10),j(e22))**. % 0.19/0.51 522[4:Rew:56.0,517.0] || -> equal(j(e22),e10)**. % 0.19/0.51 523[4:Rew:522.0,48.0] || -> equal(h(e10),e22)**. % 0.19/0.51 526[4:Rew:452.0,523.0] || -> equal(e22,e21)**. % 0.19/0.51 527[4:MRR:526.0,15.0] || -> . % 0.19/0.51 545[4:Spt:527.0,451.0,452.0] || equal(h(e10),e21)** -> . % 0.19/0.51 546[4:Spt:527.0,451.1] || -> equal(h(e10),e20)**. % 0.19/0.51 549[4:Rew:546.0,51.0] || -> equal(j(e20),e10)**. % 0.19/0.51 554[4:Rew:546.0,195.0] || -> equal(op2(h(e14),e20),h(e14))**. % 0.19/0.51 556[4:Rew:546.0,200.0] || -> equal(op2(h(e13),e20),h(e13))**. % 0.19/0.51 557[4:Rew:546.0,203.0] || -> equal(op2(h(e12),h(e12)),e20)**. % 0.19/0.51 567[4:Rew:549.0,185.0] || -> equal(op1(j(e21),e10),j(e21))**. % 0.19/0.51 571[4:Rew:549.0,186.0] || -> equal(op1(e10,j(e24)),j(e24))**. % 0.19/0.51 573[4:Rew:549.0,187.0] || -> equal(op1(e10,j(e23)),j(e23))**. % 0.19/0.51 574[4:Rew:549.0,171.0] || -> equal(op1(j(e23),j(e24)),e10)**. % 0.19/0.51 575[4:Rew:549.0,177.0] || -> equal(op1(j(e22),j(e23)),e10)**. % 0.19/0.51 576[4:Rew:549.0,168.0] || -> equal(op1(j(e24),j(e22)),e10)**. % 0.19/0.51 578[4:Rew:549.0,188.0] || -> equal(op1(e10,j(e22)),j(e22))**. % 0.19/0.51 580[5:Spt:164.0] || -> equal(h(e11),e24)**. % 0.19/0.51 581[5:Rew:580.0,52.0] || -> equal(j(e24),e11)**. % 0.19/0.51 595[5:Rew:581.0,167.0] || -> equal(op1(e11,j(e23)),j(e21))**. % 0.19/0.51 606[5:Rew:581.0,166.0] || -> equal(op1(e11,e11),j(e22))**. % 0.19/0.51 609[5:Rew:62.0,606.0] || -> equal(j(e22),e10)**. % 0.19/0.51 613[5:Rew:609.0,182.0] || -> equal(op1(j(e21),j(e23)),e10)**. % 0.19/0.51 614[5:Rew:609.0,575.0] || -> equal(op1(e10,j(e23)),e10)**. % 0.19/0.51 623[5:Rew:573.0,614.0] || -> equal(j(e23),e10)**. % 0.19/0.51 633[5:Rew:61.0,595.0,623.0,595.0] || -> equal(j(e21),e11)**. % 0.19/0.51 651[5:Rew:61.0,613.0,633.0,613.0,623.0,613.0] || -> equal(e11,e10)**. % 0.19/0.51 652[5:MRR:651.0,1.0] || -> . % 0.19/0.51 653[5:Spt:652.0,164.0,580.0] || equal(h(e11),e24)** -> . % 0.19/0.51 654[5:Spt:652.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.19/0.51 655[6:Spt:654.0] || -> equal(h(e11),e23)**. % 0.19/0.51 656[6:Rew:655.0,52.0] || -> equal(j(e23),e11)**. % 0.19/0.51 675[6:Rew:656.0,172.0] || -> equal(op1(e11,e11),j(e24))**. % 0.19/0.51 676[6:Rew:656.0,181.0] || -> equal(op1(j(e21),j(e24)),e11)**. % 0.19/0.51 685[6:Rew:62.0,675.0] || -> equal(j(e24),e10)**. % 0.19/0.51 687[6:Rew:685.0,576.0] || -> equal(op1(e10,j(e22)),e10)**. % 0.19/0.51 693[6:Rew:685.0,176.0] || -> equal(op1(j(e22),e10),j(e21))**. % 0.19/0.51 699[6:Rew:578.0,687.0] || -> equal(j(e22),e10)**. % 0.19/0.51 709[6:Rew:567.0,676.0,685.0,676.0] || -> equal(j(e21),e11)**. % 0.19/0.51 727[6:Rew:56.0,693.0,699.0,693.0,709.0,693.0] || -> equal(e11,e10)**. % 0.19/0.51 728[6:MRR:727.0,1.0] || -> . % 0.19/0.51 729[6:Spt:728.0,654.0,655.0] || equal(h(e11),e23)** -> . % 0.19/0.51 730[6:Spt:728.0,654.1,654.2,654.3] || -> equal(h(e11),e22)** equal(h(e11),e21) equal(h(e11),e20). % 0.19/0.51 731[7:Spt:730.0] || -> equal(h(e11),e22)**. % 0.19/0.51 733[7:Rew:731.0,52.0] || -> equal(j(e22),e11)**. % 0.19/0.51 752[7:Rew:733.0,173.0] || -> equal(op1(j(e23),e11),j(e21))**. % 0.19/0.51 755[7:Rew:733.0,178.0] || -> equal(op1(e11,e11),j(e23))**. % 0.19/0.51 762[7:Rew:62.0,755.0] || -> equal(j(e23),e10)**. % 0.19/0.51 766[7:Rew:762.0,574.0] || -> equal(op1(e10,j(e24)),e10)**. % 0.19/0.51 769[7:Rew:762.0,181.0] || -> equal(op1(j(e21),j(e24)),e10)**. % 0.19/0.51 776[7:Rew:571.0,766.0] || -> equal(j(e24),e10)**. % 0.19/0.51 786[7:Rew:57.0,752.0,762.0,752.0] || -> equal(j(e21),e11)**. % 0.19/0.51 804[7:Rew:61.0,769.0,786.0,769.0,776.0,769.0] || -> equal(e11,e10)**. % 0.19/0.51 805[7:MRR:804.0,1.0] || -> . % 0.19/0.51 806[7:Spt:805.0,730.0,731.0] || equal(h(e11),e22)** -> . % 0.19/0.51 807[7:Spt:805.0,730.1,730.2] || -> equal(h(e11),e21)** equal(h(e11),e20). % 0.19/0.51 808[8:Spt:807.0] || -> equal(h(e11),e21)**. % 0.19/0.51 816[8:Rew:808.0,208.0] || -> equal(op2(e21,h(e12)),h(e13))**. % 0.19/0.51 819[8:Rew:808.0,204.0] || -> equal(op2(h(e12),e21),h(e14))**. % 0.19/0.51 823[8:Rew:808.0,194.0] || -> equal(op2(h(e14),e21),h(e13))**. % 0.19/0.51 824[8:Rew:808.0,193.0] || -> equal(op2(h(e14),h(e12)),e21)**. % 0.19/0.51 839[9:Spt:163.0] || -> equal(h(e12),e24)**. % 0.19/0.51 840[9:Rew:839.0,53.0] || -> equal(j(e24),e12)**. % 0.19/0.51 847[9:Rew:839.0,816.0] || -> equal(op2(e21,e24),h(e13))**. % 0.19/0.51 858[9:Rew:840.0,166.0] || -> equal(op1(e12,e12),j(e22))**. % 0.19/0.51 868[9:Rew:90.0,847.0] || -> equal(h(e13),e23)**. % 0.19/0.51 869[9:Rew:868.0,54.0] || -> equal(j(e23),e13)**. % 0.19/0.51 880[9:Rew:869.0,178.0] || -> equal(op1(j(e22),j(e22)),e13)**. % 0.19/0.51 905[9:Rew:68.0,858.0] || -> equal(j(e22),e10)**. % 0.19/0.51 945[9:Rew:56.0,880.0,905.0,880.0] || -> equal(e13,e10)**. % 0.19/0.51 946[9:MRR:945.0,3.0] || -> . % 0.19/0.51 947[9:Spt:946.0,163.0,839.0] || equal(h(e12),e24)** -> . % 0.19/0.51 948[9:Spt:946.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.19/0.51 949[10:Spt:948.0] || -> equal(h(e12),e23)**. % 0.19/0.51 950[10:Rew:949.0,53.0] || -> equal(j(e23),e12)**. % 0.19/0.51 955[10:Rew:949.0,819.0] || -> equal(op2(e23,e21),h(e14))**. % 0.19/0.51 975[10:Rew:950.0,172.0] || -> equal(op1(e12,e12),j(e24))**. % 0.19/0.51 979[10:Rew:97.0,955.0] || -> equal(h(e14),e22)**. % 0.19/0.51 980[10:Rew:979.0,55.0] || -> equal(j(e22),e14)**. % 0.19/0.51 995[10:Rew:980.0,166.0] || -> equal(op1(j(e24),j(e24)),e14)**. % 0.19/0.51 1022[10:Rew:68.0,975.0] || -> equal(j(e24),e10)**. % 0.19/0.51 1061[10:Rew:56.0,995.0,1022.0,995.0] || -> equal(e14,e10)**. % 0.19/0.51 1062[10:MRR:1061.0,4.0] || -> . % 0.19/0.51 1063[10:Spt:1062.0,948.0,949.0] || equal(h(e12),e23)** -> . % 0.19/0.51 1064[10:Spt:1062.0,948.1,948.2,948.3] || -> equal(h(e12),e22)** equal(h(e12),e21) equal(h(e12),e20). % 0.19/0.51 1065[11:Spt:1064.0] || -> equal(h(e12),e22)**. % 0.19/0.51 1067[11:Rew:1065.0,53.0] || -> equal(j(e22),e12)**. % 0.19/0.51 1072[11:Rew:1065.0,816.0] || -> equal(op2(e21,e22),h(e13))**. % 0.19/0.51 1092[11:Rew:1067.0,178.0] || -> equal(op1(e12,e12),j(e23))**. % 0.19/0.51 1096[11:Rew:88.0,1072.0] || -> equal(h(e13),e24)**. % 0.19/0.51 1097[11:Rew:1096.0,54.0] || -> equal(j(e24),e13)**. % 0.19/0.51 1111[11:Rew:1097.0,172.0] || -> equal(op1(j(e23),j(e23)),e13)**. % 0.19/0.51 1137[11:Rew:68.0,1092.0] || -> equal(j(e23),e10)**. % 0.19/0.51 1176[11:Rew:56.0,1111.0,1137.0,1111.0] || -> equal(e13,e10)**. % 0.19/0.51 1177[11:MRR:1176.0,3.0] || -> . % 0.19/0.51 1178[11:Spt:1177.0,1064.0,1065.0] || equal(h(e12),e22)** -> . % 0.19/0.51 1179[11:Spt:1177.0,1064.1,1064.2] || -> equal(h(e12),e21)** equal(h(e12),e20). % 0.19/0.51 1180[12:Spt:1179.0] || -> equal(h(e12),e21)**. % 0.19/0.51 1185[12:Rew:1180.0,824.0] || -> equal(op2(h(e14),e21),e21)**. % 0.19/0.51 1190[12:Rew:1180.0,816.0] || -> equal(op2(e21,e21),h(e13))**. % 0.19/0.51 1199[12:Rew:823.0,1185.0] || -> equal(h(e13),e21)**. % 0.19/0.51 1221[12:Rew:87.0,1190.0,1199.0,1190.0] || -> equal(e21,e20)**. % 0.19/0.51 1222[12:MRR:1221.0,11.0] || -> . % 0.19/0.51 1229[12:Spt:1222.0,1179.0,1180.0] || equal(h(e12),e21)** -> . % 0.19/0.51 1230[12:Spt:1222.0,1179.1] || -> equal(h(e12),e20)**. % 0.19/0.51 1240[12:Rew:86.0,816.0,1230.0,816.0] || -> equal(h(e13),e21)**. % 0.19/0.51 1245[12:Rew:82.0,819.0,1230.0,819.0] || -> equal(h(e14),e21)**. % 0.19/0.51 1257[12:Rew:87.0,823.0,1245.0,823.0,1240.0,823.0] || -> equal(e21,e20)**. % 0.19/0.51 1258[12:MRR:1257.0,11.0] || -> . % 0.19/0.51 1268[8:Spt:1258.0,807.0,808.0] || equal(h(e11),e21)** -> . % 0.19/0.51 1269[8:Spt:1258.0,807.1] || -> equal(h(e11),e20)**. % 0.19/0.51 1280[8:Rew:554.0,194.0,1269.0,194.0] || -> equal(h(e14),h(e13))**. % 0.19/0.51 1285[8:Rew:1280.0,192.0] || -> equal(op2(h(e13),h(e13)),h(e12))**. % 0.19/0.51 1292[8:Rew:556.0,199.0,1269.0,199.0] || -> equal(h(e13),h(e12))**. % 0.19/0.51 1306[8:Rew:557.0,1285.0,1292.0,1285.0] || -> equal(h(e12),e20)**. % 0.19/0.51 1307[8:Rew:1306.0,53.0] || -> equal(j(e20),e12)**. % 0.19/0.51 1313[8:Rew:549.0,1307.0] || -> equal(e12,e10)**. % 0.19/0.51 1314[8:MRR:1313.0,2.0] || -> . % 0.19/0.51 % SZS output end Refutation % 0.19/0.51 Formulae used in the proof : ax1 ax2 co1 ax4 ax5 % 0.19/0.51 %------------------------------------------------------------------------------