%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG089+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:18 EDT 2022 % Result : Theorem 0.20s 0.49s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ALG089+1 : TPTP v8.1.0. Released v2.7.0. % 0.11/0.12 % Command : run_spass %d %s % 0.13/0.34 % Computer : n019.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 10:34:40 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.49 % 0.20/0.49 SPASS V 3.9 % 0.20/0.49 SPASS beiseite: Proof found. % 0.20/0.49 % SZS status Theorem % 0.20/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.49 SPASS derived 599 clauses, backtracked 603 clauses, performed 12 splits and kept 1071 clauses. % 0.20/0.49 SPASS allocated 85691 KBytes. % 0.20/0.49 SPASS spent 0:00:00.15 on the problem. % 0.20/0.49 0:00:00.04 for the input. % 0.20/0.49 0:00:00.03 for the FLOTTER CNF translation. % 0.20/0.49 0:00:00.00 for inferences. % 0.20/0.49 0:00:00.00 for the backtracking. % 0.20/0.49 0:00:00.05 for the reduction. % 0.20/0.49 % 0.20/0.49 % 0.20/0.49 Here is a proof with depth 4, length 282 : % 0.20/0.49 % SZS output start Refutation % 0.20/0.49 1[0:Inp] || equal(e11,e10)** -> . % 0.20/0.49 2[0:Inp] || equal(e12,e10)** -> . % 0.20/0.49 3[0:Inp] || equal(e13,e10)** -> . % 0.20/0.49 4[0:Inp] || equal(e14,e10)** -> . % 0.20/0.49 11[0:Inp] || equal(e21,e20)** -> . % 0.20/0.49 13[0:Inp] || equal(e23,e20)** -> . % 0.20/0.49 14[0:Inp] || equal(e24,e20)** -> . % 0.20/0.49 17[0:Inp] || equal(e24,e21)** -> . % 0.20/0.49 19[0:Inp] || equal(e24,e22)** -> . % 0.20/0.49 46[0:Inp] || -> equal(h(j(e20)),e20)**. % 0.20/0.49 47[0:Inp] || -> equal(h(j(e21)),e21)**. % 0.20/0.49 50[0:Inp] || -> equal(h(j(e24)),e24)**. % 0.20/0.49 51[0:Inp] || -> equal(j(h(e10)),e10)**. % 0.20/0.49 52[0:Inp] || -> equal(j(h(e11)),e11)**. % 0.20/0.49 53[0:Inp] || -> equal(j(h(e12)),e12)**. % 0.20/0.49 54[0:Inp] || -> equal(j(h(e13)),e13)**. % 0.20/0.49 55[0:Inp] || -> equal(j(h(e14)),e14)**. % 0.20/0.49 56[0:Inp] || -> equal(op1(e10,e10),e10)**. % 0.20/0.49 57[0:Inp] || -> equal(op1(e10,e11),e11)**. % 0.20/0.49 61[0:Inp] || -> equal(op1(e11,e10),e11)**. % 0.20/0.49 62[0:Inp] || -> equal(op1(e11,e11),e10)**. % 0.20/0.49 63[0:Inp] || -> equal(op1(e11,e12),e13)**. % 0.20/0.49 64[0:Inp] || -> equal(op1(e11,e13),e14)**. % 0.20/0.49 67[0:Inp] || -> equal(op1(e12,e11),e14)**. % 0.20/0.49 68[0:Inp] || -> equal(op1(e12,e12),e10)**. % 0.20/0.49 71[0:Inp] || -> equal(op1(e13,e10),e13)**. % 0.20/0.49 72[0:Inp] || -> equal(op1(e13,e11),e12)**. % 0.20/0.49 76[0:Inp] || -> equal(op1(e14,e10),e14)**. % 0.20/0.49 77[0:Inp] || -> equal(op1(e14,e11),e13)**. % 0.20/0.49 78[0:Inp] || -> equal(op1(e14,e12),e11)**. % 0.20/0.49 79[0:Inp] || -> equal(op1(e14,e13),e12)**. % 0.20/0.49 85[0:Inp] || -> equal(op2(e20,e24),e24)**. % 0.20/0.49 86[0:Inp] || -> equal(op2(e21,e20),e21)**. % 0.20/0.49 87[0:Inp] || -> equal(op2(e21,e21),e22)**. % 0.20/0.49 88[0:Inp] || -> equal(op2(e21,e22),e24)**. % 0.20/0.49 89[0:Inp] || -> equal(op2(e21,e23),e20)**. % 0.20/0.49 90[0:Inp] || -> equal(op2(e21,e24),e23)**. % 0.20/0.49 91[0:Inp] || -> equal(op2(e22,e20),e22)**. % 0.20/0.49 92[0:Inp] || -> equal(op2(e22,e21),e20)**. % 0.20/0.49 93[0:Inp] || -> equal(op2(e22,e22),e23)**. % 0.20/0.49 94[0:Inp] || -> equal(op2(e22,e23),e24)**. % 0.20/0.49 95[0:Inp] || -> equal(op2(e22,e24),e21)**. % 0.20/0.49 96[0:Inp] || -> equal(op2(e23,e20),e23)**. % 0.20/0.49 98[0:Inp] || -> equal(op2(e23,e22),e20)**. % 0.20/0.49 99[0:Inp] || -> equal(op2(e23,e23),e21)**. % 0.20/0.49 100[0:Inp] || -> equal(op2(e23,e24),e22)**. % 0.20/0.49 101[0:Inp] || -> equal(op2(e24,e20),e24)**. % 0.20/0.49 102[0:Inp] || -> equal(op2(e24,e21),e23)**. % 0.20/0.49 103[0:Inp] || -> equal(op2(e24,e22),e21)**. % 0.20/0.49 104[0:Inp] || -> equal(op2(e24,e23),e22)**. % 0.20/0.49 105[0:Inp] || -> equal(op2(e24,e24),e20)**. % 0.20/0.49 113[0:Inp] || -> equal(op2(h(e11),h(e12)),h(op1(e11,e12)))**. % 0.20/0.49 114[0:Inp] || -> equal(op2(h(e11),h(e13)),h(op1(e11,e13)))**. % 0.20/0.49 117[0:Inp] || -> equal(op2(h(e12),h(e11)),h(op1(e12,e11)))**. % 0.20/0.49 118[0:Inp] || -> equal(op2(h(e12),h(e12)),h(op1(e12,e12)))**. % 0.20/0.49 121[0:Inp] || -> equal(op2(h(e13),h(e10)),h(op1(e13,e10)))**. % 0.20/0.49 122[0:Inp] || -> equal(op2(h(e13),h(e11)),h(op1(e13,e11)))**. % 0.20/0.49 126[0:Inp] || -> equal(op2(h(e14),h(e10)),h(op1(e14,e10)))**. % 0.20/0.49 127[0:Inp] || -> equal(op2(h(e14),h(e11)),h(op1(e14,e11)))**. % 0.20/0.49 128[0:Inp] || -> equal(op2(h(e14),h(e12)),h(op1(e14,e12)))**. % 0.20/0.49 129[0:Inp] || -> equal(op2(h(e14),h(e13)),h(op1(e14,e13)))**. % 0.20/0.49 136[0:Inp] || -> equal(op1(j(e21),j(e20)),j(op2(e21,e20)))**. % 0.20/0.49 137[0:Inp] || -> equal(op1(j(e21),j(e21)),j(op2(e21,e21)))**. % 0.20/0.49 138[0:Inp] || -> equal(op1(j(e21),j(e22)),j(op2(e21,e22)))**. % 0.20/0.49 139[0:Inp] || -> equal(op1(j(e21),j(e23)),j(op2(e21,e23)))**. % 0.20/0.49 140[0:Inp] || -> equal(op1(j(e21),j(e24)),j(op2(e21,e24)))**. % 0.20/0.49 141[0:Inp] || -> equal(op1(j(e22),j(e20)),j(op2(e22,e20)))**. % 0.20/0.49 142[0:Inp] || -> equal(op1(j(e22),j(e21)),j(op2(e22,e21)))**. % 0.20/0.49 143[0:Inp] || -> equal(op1(j(e22),j(e22)),j(op2(e22,e22)))**. % 0.20/0.49 144[0:Inp] || -> equal(op1(j(e22),j(e23)),j(op2(e22,e23)))**. % 0.20/0.49 145[0:Inp] || -> equal(op1(j(e22),j(e24)),j(op2(e22,e24)))**. % 0.20/0.49 146[0:Inp] || -> equal(op1(j(e23),j(e20)),j(op2(e23,e20)))**. % 0.20/0.49 148[0:Inp] || -> equal(op1(j(e23),j(e22)),j(op2(e23,e22)))**. % 0.20/0.49 149[0:Inp] || -> equal(op1(j(e23),j(e23)),j(op2(e23,e23)))**. % 0.20/0.49 150[0:Inp] || -> equal(op1(j(e23),j(e24)),j(op2(e23,e24)))**. % 0.20/0.49 151[0:Inp] || -> equal(op1(j(e24),j(e20)),j(op2(e24,e20)))**. % 0.20/0.49 153[0:Inp] || -> equal(op1(j(e24),j(e22)),j(op2(e24,e22)))**. % 0.20/0.49 154[0:Inp] || -> equal(op1(j(e24),j(e23)),j(op2(e24,e23)))**. % 0.20/0.49 155[0:Inp] || -> equal(op1(j(e24),j(e24)),j(op2(e24,e24)))**. % 0.20/0.49 163[0:Inp] || -> equal(h(e12),e24)** equal(h(e12),e23) equal(h(e12),e22) equal(h(e12),e21) equal(h(e12),e20). % 0.20/0.49 164[0:Inp] || -> equal(h(e11),e24)** equal(h(e11),e23) equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.20/0.49 165[0:Inp] || -> equal(h(e10),e24)** equal(h(e10),e23) equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.20/0.49 166[0:Rew:105.0,155.0] || -> equal(op1(j(e24),j(e24)),j(e20))**. % 0.20/0.49 167[0:Rew:104.0,154.0] || -> equal(op1(j(e24),j(e23)),j(e22))**. % 0.20/0.49 168[0:Rew:103.0,153.0] || -> equal(op1(j(e24),j(e22)),j(e21))**. % 0.20/0.49 170[0:Rew:101.0,151.0] || -> equal(op1(j(e24),j(e20)),j(e24))**. % 0.20/0.49 171[0:Rew:100.0,150.0] || -> equal(op1(j(e23),j(e24)),j(e22))**. % 0.20/0.49 172[0:Rew:99.0,149.0] || -> equal(op1(j(e23),j(e23)),j(e21))**. % 0.20/0.49 173[0:Rew:98.0,148.0] || -> equal(op1(j(e23),j(e22)),j(e20))**. % 0.20/0.49 175[0:Rew:96.0,146.0] || -> equal(op1(j(e23),j(e20)),j(e23))**. % 0.20/0.49 176[0:Rew:95.0,145.0] || -> equal(op1(j(e22),j(e24)),j(e21))**. % 0.20/0.49 177[0:Rew:94.0,144.0] || -> equal(op1(j(e22),j(e23)),j(e24))**. % 0.20/0.49 178[0:Rew:93.0,143.0] || -> equal(op1(j(e22),j(e22)),j(e23))**. % 0.20/0.49 179[0:Rew:92.0,142.0] || -> equal(op1(j(e22),j(e21)),j(e20))**. % 0.20/0.49 180[0:Rew:91.0,141.0] || -> equal(op1(j(e22),j(e20)),j(e22))**. % 0.20/0.49 181[0:Rew:90.0,140.0] || -> equal(op1(j(e21),j(e24)),j(e23))**. % 0.20/0.49 182[0:Rew:89.0,139.0] || -> equal(op1(j(e21),j(e23)),j(e20))**. % 0.20/0.49 183[0:Rew:88.0,138.0] || -> equal(op1(j(e21),j(e22)),j(e24))**. % 0.20/0.49 184[0:Rew:87.0,137.0] || -> equal(op1(j(e21),j(e21)),j(e22))**. % 0.20/0.49 185[0:Rew:86.0,136.0] || -> equal(op1(j(e21),j(e20)),j(e21))**. % 0.20/0.49 192[0:Rew:79.0,129.0] || -> equal(op2(h(e14),h(e13)),h(e12))**. % 0.20/0.49 193[0:Rew:78.0,128.0] || -> equal(op2(h(e14),h(e12)),h(e11))**. % 0.20/0.49 194[0:Rew:77.0,127.0] || -> equal(op2(h(e14),h(e11)),h(e13))**. % 0.20/0.49 195[0:Rew:76.0,126.0] || -> equal(op2(h(e14),h(e10)),h(e14))**. % 0.20/0.49 199[0:Rew:72.0,122.0] || -> equal(op2(h(e13),h(e11)),h(e12))**. % 0.20/0.49 200[0:Rew:71.0,121.0] || -> equal(op2(h(e13),h(e10)),h(e13))**. % 0.20/0.49 203[0:Rew:68.0,118.0] || -> equal(op2(h(e12),h(e12)),h(e10))**. % 0.20/0.49 204[0:Rew:67.0,117.0] || -> equal(op2(h(e12),h(e11)),h(e14))**. % 0.20/0.49 207[0:Rew:64.0,114.0] || -> equal(op2(h(e11),h(e13)),h(e14))**. % 0.20/0.49 208[0:Rew:63.0,113.0] || -> equal(op2(h(e11),h(e12)),h(e13))**. % 0.20/0.49 216[1:Spt:165.0] || -> equal(h(e10),e24)**. % 0.20/0.49 217[1:Rew:216.0,51.0] || -> equal(j(e24),e10)**. % 0.20/0.49 232[1:Rew:217.0,166.0] || -> equal(op1(e10,e10),j(e20))**. % 0.20/0.49 237[1:Rew:217.0,171.0] || -> equal(op1(j(e23),e10),j(e22))**. % 0.20/0.49 239[1:Rew:217.0,176.0] || -> equal(op1(j(e22),e10),j(e21))**. % 0.20/0.49 246[1:Rew:56.0,232.0] || -> equal(j(e20),e10)**. % 0.20/0.49 249[1:Rew:246.0,175.0] || -> equal(op1(j(e23),e10),j(e23))**. % 0.20/0.49 251[1:Rew:246.0,180.0] || -> equal(op1(j(e22),e10),j(e22))**. % 0.20/0.49 252[1:Rew:246.0,182.0] || -> equal(op1(j(e21),j(e23)),e10)**. % 0.20/0.49 262[1:Rew:237.0,249.0] || -> equal(j(e23),j(e22))**. % 0.20/0.49 264[1:Rew:262.0,172.0] || -> equal(op1(j(e22),j(e22)),j(e21))**. % 0.20/0.49 276[1:Rew:239.0,251.0] || -> equal(j(e22),j(e21))**. % 0.20/0.49 283[1:Rew:276.0,262.0] || -> equal(j(e23),j(e21))**. % 0.20/0.49 287[1:Rew:283.0,252.0] || -> equal(op1(j(e21),j(e21)),e10)**. % 0.20/0.49 297[1:Rew:287.0,264.0,276.0,264.0] || -> equal(j(e21),e10)**. % 0.20/0.49 298[1:Rew:297.0,47.0] || -> equal(h(e10),e21)**. % 0.20/0.49 304[1:Rew:216.0,298.0] || -> equal(e24,e21)**. % 0.20/0.49 305[1:MRR:304.0,17.0] || -> . % 0.20/0.49 308[1:Spt:305.0,165.0,216.0] || equal(h(e10),e24)** -> . % 0.20/0.49 309[1:Spt:305.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.20/0.49 310[2:Spt:309.0] || -> equal(h(e10),e23)**. % 0.20/0.49 311[2:Rew:310.0,51.0] || -> equal(j(e23),e10)**. % 0.20/0.49 328[2:Rew:311.0,177.0] || -> equal(op1(j(e22),e10),j(e24))**. % 0.20/0.49 338[2:Rew:311.0,172.0] || -> equal(op1(e10,e10),j(e21))**. % 0.20/0.49 341[2:Rew:56.0,338.0] || -> equal(j(e21),e10)**. % 0.20/0.49 349[2:Rew:341.0,184.0] || -> equal(op1(e10,e10),j(e22))**. % 0.20/0.49 352[2:Rew:56.0,349.0] || -> equal(j(e22),e10)**. % 0.20/0.49 359[2:Rew:56.0,328.0,352.0,328.0] || -> equal(j(e24),e10)**. % 0.20/0.49 363[2:Rew:359.0,166.0] || -> equal(op1(e10,e10),j(e20))**. % 0.20/0.49 367[2:Rew:56.0,363.0] || -> equal(j(e20),e10)**. % 0.20/0.49 368[2:Rew:367.0,46.0] || -> equal(h(e10),e20)**. % 0.20/0.49 372[2:Rew:310.0,368.0] || -> equal(e23,e20)**. % 0.20/0.49 373[2:MRR:372.0,13.0] || -> . % 0.20/0.49 385[2:Spt:373.0,309.0,310.0] || equal(h(e10),e23)** -> . % 0.20/0.49 386[2:Spt:373.0,309.1,309.2,309.3] || -> equal(h(e10),e22)** equal(h(e10),e21) equal(h(e10),e20). % 0.20/0.49 387[3:Spt:386.0] || -> equal(h(e10),e22)**. % 0.20/0.49 389[3:Rew:387.0,51.0] || -> equal(j(e22),e10)**. % 0.20/0.49 405[3:Rew:389.0,178.0] || -> equal(op1(e10,e10),j(e23))**. % 0.20/0.49 409[3:Rew:389.0,177.0] || -> equal(op1(e10,j(e23)),j(e24))**. % 0.20/0.49 419[3:Rew:56.0,405.0] || -> equal(j(e23),e10)**. % 0.20/0.49 448[3:Rew:56.0,409.0,419.0,409.0] || -> equal(j(e24),e10)**. % 0.20/0.49 449[3:Rew:448.0,50.0] || -> equal(h(e10),e24)**. % 0.20/0.49 452[3:Rew:387.0,449.0] || -> equal(e24,e22)**. % 0.20/0.49 453[3:MRR:452.0,19.0] || -> . % 0.20/0.49 466[3:Spt:453.0,386.0,387.0] || equal(h(e10),e22)** -> . % 0.20/0.49 467[3:Spt:453.0,386.1,386.2] || -> equal(h(e10),e21)** equal(h(e10),e20). % 0.20/0.49 468[4:Spt:467.0] || -> equal(h(e10),e21)**. % 0.20/0.49 470[4:Rew:468.0,51.0] || -> equal(j(e21),e10)**. % 0.20/0.49 487[4:Rew:470.0,183.0] || -> equal(op1(e10,j(e22)),j(e24))**. % 0.20/0.49 491[4:Rew:470.0,184.0] || -> equal(op1(e10,e10),j(e22))**. % 0.20/0.49 501[4:Rew:56.0,491.0] || -> equal(j(e22),e10)**. % 0.20/0.49 518[4:Rew:56.0,487.0,501.0,487.0] || -> equal(j(e24),e10)**. % 0.20/0.49 522[4:Rew:518.0,166.0] || -> equal(op1(e10,e10),j(e20))**. % 0.20/0.49 525[4:Rew:56.0,522.0] || -> equal(j(e20),e10)**. % 0.20/0.49 526[4:Rew:525.0,46.0] || -> equal(h(e10),e20)**. % 0.20/0.49 530[4:Rew:468.0,526.0] || -> equal(e21,e20)**. % 0.20/0.49 531[4:MRR:530.0,11.0] || -> . % 0.20/0.49 544[4:Spt:531.0,467.0,468.0] || equal(h(e10),e21)** -> . % 0.20/0.49 545[4:Spt:531.0,467.1] || -> equal(h(e10),e20)**. % 0.20/0.49 548[4:Rew:545.0,51.0] || -> equal(j(e20),e10)**. % 0.20/0.49 553[4:Rew:545.0,195.0] || -> equal(op2(h(e14),e20),h(e14))**. % 0.20/0.49 555[4:Rew:545.0,200.0] || -> equal(op2(h(e13),e20),h(e13))**. % 0.20/0.49 556[4:Rew:545.0,203.0] || -> equal(op2(h(e12),h(e12)),e20)**. % 0.20/0.49 565[4:Rew:548.0,185.0] || -> equal(op1(j(e21),e10),j(e21))**. % 0.20/0.49 567[4:Rew:548.0,182.0] || -> equal(op1(j(e21),j(e23)),e10)**. % 0.20/0.49 568[4:Rew:548.0,179.0] || -> equal(op1(j(e22),j(e21)),e10)**. % 0.20/0.49 569[4:Rew:548.0,173.0] || -> equal(op1(j(e23),j(e22)),e10)**. % 0.20/0.49 570[4:Rew:548.0,180.0] || -> equal(op1(j(e22),e10),j(e22))**. % 0.20/0.49 572[4:Rew:548.0,175.0] || -> equal(op1(j(e23),e10),j(e23))**. % 0.20/0.49 575[4:Rew:548.0,170.0] || -> equal(op1(j(e24),e10),j(e24))**. % 0.20/0.49 579[5:Spt:164.0] || -> equal(h(e11),e24)**. % 0.20/0.49 581[5:Rew:579.0,193.0] || -> equal(op2(h(e14),h(e12)),e24)**. % 0.20/0.49 582[5:Rew:579.0,194.0] || -> equal(op2(h(e14),e24),h(e13))**. % 0.20/0.49 586[5:Rew:579.0,204.0] || -> equal(op2(h(e12),e24),h(e14))**. % 0.20/0.49 588[5:Rew:579.0,207.0] || -> equal(op2(e24,h(e13)),h(e14))**. % 0.20/0.49 589[5:Rew:579.0,208.0] || -> equal(op2(e24,h(e12)),h(e13))**. % 0.20/0.49 607[6:Spt:163.0] || -> equal(h(e12),e24)**. % 0.20/0.49 615[6:Rew:607.0,581.0] || -> equal(op2(h(e14),e24),e24)**. % 0.20/0.49 620[6:Rew:607.0,589.0] || -> equal(op2(e24,e24),h(e13))**. % 0.20/0.49 623[6:Rew:582.0,615.0] || -> equal(h(e13),e24)**. % 0.20/0.49 645[6:Rew:105.0,620.0,623.0,620.0] || -> equal(e24,e20)**. % 0.20/0.49 646[6:MRR:645.0,14.0] || -> . % 0.20/0.49 653[6:Spt:646.0,163.0,607.0] || equal(h(e12),e24)** -> . % 0.20/0.49 654[6:Spt:646.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.20/0.49 655[7:Spt:654.0] || -> equal(h(e12),e23)**. % 0.20/0.49 656[7:Rew:655.0,53.0] || -> equal(j(e23),e12)**. % 0.20/0.49 658[7:Rew:655.0,589.0] || -> equal(op2(e24,e23),h(e13))**. % 0.20/0.49 671[7:Rew:656.0,172.0] || -> equal(op1(e12,e12),j(e21))**. % 0.20/0.49 685[7:Rew:104.0,658.0] || -> equal(h(e13),e22)**. % 0.20/0.49 686[7:Rew:685.0,54.0] || -> equal(j(e22),e13)**. % 0.20/0.49 694[7:Rew:686.0,184.0] || -> equal(op1(j(e21),j(e21)),e13)**. % 0.20/0.49 720[7:Rew:68.0,671.0] || -> equal(j(e21),e10)**. % 0.20/0.49 762[7:Rew:56.0,694.0,720.0,694.0] || -> equal(e13,e10)**. % 0.20/0.49 763[7:MRR:762.0,3.0] || -> . % 0.20/0.49 764[7:Spt:763.0,654.0,655.0] || equal(h(e12),e23)** -> . % 0.20/0.49 765[7:Spt:763.0,654.1,654.2,654.3] || -> equal(h(e12),e22)** equal(h(e12),e21) equal(h(e12),e20). % 0.20/0.49 766[8:Spt:765.0] || -> equal(h(e12),e22)**. % 0.20/0.49 768[8:Rew:766.0,53.0] || -> equal(j(e22),e12)**. % 0.20/0.49 776[8:Rew:766.0,586.0] || -> equal(op2(e22,e24),h(e14))**. % 0.20/0.49 793[8:Rew:768.0,178.0] || -> equal(op1(e12,e12),j(e23))**. % 0.20/0.49 797[8:Rew:95.0,776.0] || -> equal(h(e14),e21)**. % 0.20/0.49 798[8:Rew:797.0,55.0] || -> equal(j(e21),e14)**. % 0.20/0.49 813[8:Rew:798.0,172.0] || -> equal(op1(j(e23),j(e23)),e14)**. % 0.20/0.49 839[8:Rew:68.0,793.0] || -> equal(j(e23),e10)**. % 0.20/0.49 878[8:Rew:56.0,813.0,839.0,813.0] || -> equal(e14,e10)**. % 0.20/0.49 879[8:MRR:878.0,4.0] || -> . % 0.20/0.49 880[8:Spt:879.0,765.0,766.0] || equal(h(e12),e22)** -> . % 0.20/0.49 881[8:Spt:879.0,765.1,765.2] || -> equal(h(e12),e21)** equal(h(e12),e20). % 0.20/0.49 882[9:Spt:881.0] || -> equal(h(e12),e21)**. % 0.20/0.49 884[9:Rew:882.0,53.0] || -> equal(j(e21),e12)**. % 0.20/0.49 887[9:Rew:882.0,589.0] || -> equal(op2(e24,e21),h(e13))**. % 0.20/0.49 910[9:Rew:884.0,184.0] || -> equal(op1(e12,e12),j(e22))**. % 0.20/0.49 914[9:Rew:102.0,887.0] || -> equal(h(e13),e23)**. % 0.20/0.49 915[9:Rew:914.0,54.0] || -> equal(j(e23),e13)**. % 0.20/0.49 929[9:Rew:915.0,178.0] || -> equal(op1(j(e22),j(e22)),e13)**. % 0.20/0.49 956[9:Rew:68.0,910.0] || -> equal(j(e22),e10)**. % 0.20/0.49 995[9:Rew:56.0,929.0,956.0,929.0] || -> equal(e13,e10)**. % 0.20/0.49 996[9:MRR:995.0,3.0] || -> . % 0.20/0.49 997[9:Spt:996.0,881.0,882.0] || equal(h(e12),e21)** -> . % 0.20/0.49 998[9:Spt:996.0,881.1] || -> equal(h(e12),e20)**. % 0.20/0.49 1011[9:Rew:85.0,586.0,998.0,586.0] || -> equal(h(e14),e24)**. % 0.20/0.49 1017[9:Rew:101.0,589.0,998.0,589.0] || -> equal(h(e13),e24)**. % 0.20/0.49 1030[9:Rew:105.0,588.0,1017.0,588.0,1011.0,588.0] || -> equal(e24,e20)**. % 0.20/0.49 1031[9:MRR:1030.0,14.0] || -> . % 0.20/0.49 1038[5:Spt:1031.0,164.0,579.0] || equal(h(e11),e24)** -> . % 0.20/0.49 1039[5:Spt:1031.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.20/0.49 1040[6:Spt:1039.0] || -> equal(h(e11),e23)**. % 0.20/0.49 1041[6:Rew:1040.0,52.0] || -> equal(j(e23),e11)**. % 0.20/0.49 1060[6:Rew:1041.0,172.0] || -> equal(op1(e11,e11),j(e21))**. % 0.20/0.49 1062[6:Rew:1041.0,177.0] || -> equal(op1(j(e22),e11),j(e24))**. % 0.20/0.49 1070[6:Rew:62.0,1060.0] || -> equal(j(e21),e10)**. % 0.20/0.49 1074[6:Rew:1070.0,568.0] || -> equal(op1(j(e22),e10),e10)**. % 0.20/0.49 1078[6:Rew:1070.0,168.0] || -> equal(op1(j(e24),j(e22)),e10)**. % 0.20/0.49 1084[6:Rew:570.0,1074.0] || -> equal(j(e22),e10)**. % 0.20/0.49 1096[6:Rew:57.0,1062.0,1084.0,1062.0] || -> equal(j(e24),e11)**. % 0.20/0.49 1112[6:Rew:61.0,1078.0,1096.0,1078.0,1084.0,1078.0] || -> equal(e11,e10)**. % 0.20/0.49 1113[6:MRR:1112.0,1.0] || -> . % 0.20/0.49 1114[6:Spt:1113.0,1039.0,1040.0] || equal(h(e11),e23)** -> . % 0.20/0.49 1115[6:Spt:1113.0,1039.1,1039.2,1039.3] || -> equal(h(e11),e22)** equal(h(e11),e21) equal(h(e11),e20). % 0.20/0.49 1116[7:Spt:1115.0] || -> equal(h(e11),e22)**. % 0.20/0.49 1118[7:Rew:1116.0,52.0] || -> equal(j(e22),e11)**. % 0.20/0.49 1137[7:Rew:1118.0,167.0] || -> equal(op1(j(e24),j(e23)),e11)**. % 0.20/0.49 1140[7:Rew:1118.0,178.0] || -> equal(op1(e11,e11),j(e23))**. % 0.20/0.49 1147[7:Rew:62.0,1140.0] || -> equal(j(e23),e10)**. % 0.20/0.49 1151[7:Rew:1147.0,567.0] || -> equal(op1(j(e21),e10),e10)**. % 0.20/0.49 1154[7:Rew:1147.0,181.0] || -> equal(op1(j(e21),j(e24)),e10)**. % 0.20/0.49 1161[7:Rew:565.0,1151.0] || -> equal(j(e21),e10)**. % 0.20/0.49 1171[7:Rew:575.0,1137.0,1147.0,1137.0] || -> equal(j(e24),e11)**. % 0.20/0.49 1189[7:Rew:57.0,1154.0,1161.0,1154.0,1171.0,1154.0] || -> equal(e11,e10)**. % 0.20/0.49 1190[7:MRR:1189.0,1.0] || -> . % 0.20/0.49 1191[7:Spt:1190.0,1115.0,1116.0] || equal(h(e11),e22)** -> . % 0.20/0.49 1192[7:Spt:1190.0,1115.1,1115.2] || -> equal(h(e11),e21)** equal(h(e11),e20). % 0.20/0.49 1193[8:Spt:1192.0] || -> equal(h(e11),e21)**. % 0.20/0.49 1195[8:Rew:1193.0,52.0] || -> equal(j(e21),e11)**. % 0.20/0.49 1215[8:Rew:1195.0,184.0] || -> equal(op1(e11,e11),j(e22))**. % 0.20/0.49 1216[8:Rew:1195.0,183.0] || -> equal(op1(e11,j(e22)),j(e24))**. % 0.20/0.49 1225[8:Rew:62.0,1215.0] || -> equal(j(e22),e10)**. % 0.20/0.49 1229[8:Rew:1225.0,569.0] || -> equal(op1(j(e23),e10),e10)**. % 0.20/0.49 1233[8:Rew:1225.0,167.0] || -> equal(op1(j(e24),j(e23)),e10)**. % 0.20/0.49 1239[8:Rew:572.0,1229.0] || -> equal(j(e23),e10)**. % 0.20/0.49 1249[8:Rew:61.0,1216.0,1225.0,1216.0] || -> equal(j(e24),e11)**. % 0.20/0.49 1267[8:Rew:61.0,1233.0,1249.0,1233.0,1239.0,1233.0] || -> equal(e11,e10)**. % 0.20/0.49 1268[8:MRR:1267.0,1.0] || -> . % 0.20/0.49 1269[8:Spt:1268.0,1192.0,1193.0] || equal(h(e11),e21)** -> . % 0.20/0.49 1270[8:Spt:1268.0,1192.1] || -> equal(h(e11),e20)**. % 0.20/0.49 1281[8:Rew:553.0,194.0,1270.0,194.0] || -> equal(h(e14),h(e13))**. % 0.20/0.49 1286[8:Rew:1281.0,192.0] || -> equal(op2(h(e13),h(e13)),h(e12))**. % 0.20/0.49 1294[8:Rew:555.0,199.0,1270.0,199.0] || -> equal(h(e13),h(e12))**. % 0.20/0.49 1309[8:Rew:556.0,1286.0,1294.0,1286.0] || -> equal(h(e12),e20)**. % 0.20/0.49 1310[8:Rew:1309.0,53.0] || -> equal(j(e20),e12)**. % 0.20/0.50 1316[8:Rew:548.0,1310.0] || -> equal(e12,e10)**. % 0.20/0.50 1317[8:MRR:1316.0,2.0] || -> . % 0.20/0.50 % SZS output end Refutation % 0.20/0.50 Formulae used in the proof : ax1 ax2 co1 ax4 ax5 % 0.20/0.50 %------------------------------------------------------------------------------