%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG206+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n032.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:56 EDT 2022 % Result : Theorem 0.38s 0.55s % Output : Refutation 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : ALG206+1 : TPTP v8.1.0. Released v2.7.0. % 0.05/0.10 % Command : run_spass %d %s % 0.09/0.30 % Computer : n032.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 600 % 0.09/0.30 % DateTime : Wed Jun 8 15:44:51 EDT 2022 % 0.09/0.30 % CPUTime : % 0.38/0.55 % 0.38/0.55 SPASS V 3.9 % 0.38/0.55 SPASS beiseite: Proof found. % 0.38/0.55 % SZS status Theorem % 0.38/0.55 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.38/0.55 SPASS derived 1326 clauses, backtracked 1248 clauses, performed 12 splits and kept 2264 clauses. % 0.38/0.55 SPASS allocated 86426 KBytes. % 0.38/0.55 SPASS spent 0:00:00.25 on the problem. % 0.38/0.55 0:00:00.03 for the input. % 0.38/0.55 0:00:00.04 for the FLOTTER CNF translation. % 0.38/0.55 0:00:00.00 for inferences. % 0.38/0.55 0:00:00.00 for the backtracking. % 0.38/0.55 0:00:00.14 for the reduction. % 0.38/0.55 % 0.38/0.55 % 0.38/0.55 Here is a proof with depth 6, length 338 : % 0.38/0.55 % SZS output start Refutation % 0.38/0.55 5[0:Inp] || equal(e15,e10)** -> . % 0.38/0.55 19[0:Inp] || equal(e15,e14)** -> . % 0.38/0.55 21[0:Inp] || equal(e16,e15)** -> . % 0.38/0.55 25[0:Inp] || equal(e24,e20)** -> . % 0.38/0.55 30[0:Inp] || equal(e24,e21)** -> . % 0.38/0.55 34[0:Inp] || equal(e24,e22)** -> . % 0.38/0.55 37[0:Inp] || equal(e24,e23)** -> . % 0.38/0.55 40[0:Inp] || equal(e25,e24)** -> . % 0.38/0.55 41[0:Inp] || equal(e26,e24)** -> . % 0.38/0.55 42[0:Inp] || equal(e26,e25)** -> . % 0.38/0.55 96[0:Inp] || -> equal(h(j(e24)),e24)**. % 0.38/0.55 99[0:Inp] || -> equal(j(h(e10)),e10)**. % 0.38/0.55 103[0:Inp] || -> equal(j(h(e14)),e14)**. % 0.38/0.55 104[0:Inp] || -> equal(j(h(e15)),e15)**. % 0.38/0.55 105[0:Inp] || -> equal(j(h(e16)),e16)**. % 0.38/0.55 106[0:Inp] || -> equal(op1(e10,e10),e10)**. % 0.38/0.55 107[0:Inp] || -> equal(op1(e10,e11),e13)**. % 0.38/0.55 109[0:Inp] || -> equal(op1(e10,e13),e12)**. % 0.38/0.55 112[0:Inp] || -> equal(op1(e10,e16),e15)**. % 0.38/0.55 113[0:Inp] || -> equal(op1(e11,e10),e13)**. % 0.38/0.55 115[0:Inp] || -> equal(op1(e11,e12),e16)**. % 0.38/0.55 128[0:Inp] || -> equal(op1(e13,e11),e15)**. % 0.38/0.55 134[0:Inp] || -> equal(op1(e14,e10),e16)**. % 0.38/0.55 138[0:Inp] || -> equal(op1(e14,e14),e14)**. % 0.38/0.55 141[0:Inp] || -> equal(op1(e15,e10),e14)**. % 0.38/0.55 142[0:Inp] || -> equal(op1(e15,e11),e10)**. % 0.38/0.55 146[0:Inp] || -> equal(op1(e15,e15),e15)**. % 0.38/0.55 148[0:Inp] || -> equal(op1(e16,e10),e15)**. % 0.38/0.55 154[0:Inp] || -> equal(op1(e16,e16),e16)**. % 0.38/0.55 155[0:Inp] || -> equal(op2(e20,e20),e22)**. % 0.38/0.55 157[0:Inp] || -> equal(op2(e20,e22),e21)**. % 0.38/0.55 159[0:Inp] || -> equal(op2(e20,e24),e23)**. % 0.38/0.55 160[0:Inp] || -> equal(op2(e20,e25),e24)**. % 0.38/0.55 162[0:Inp] || -> equal(op2(e21,e20),e20)**. % 0.38/0.55 163[0:Inp] || -> equal(op2(e21,e21),e26)**. % 0.38/0.55 164[0:Inp] || -> equal(op2(e21,e22),e24)**. % 0.38/0.55 165[0:Inp] || -> equal(op2(e21,e23),e21)**. % 0.38/0.55 166[0:Inp] || -> equal(op2(e21,e24),e25)**. % 0.38/0.55 167[0:Inp] || -> equal(op2(e21,e25),e22)**. % 0.38/0.55 168[0:Inp] || -> equal(op2(e21,e26),e23)**. % 0.38/0.55 170[0:Inp] || -> equal(op2(e22,e21),e24)**. % 0.38/0.55 171[0:Inp] || -> equal(op2(e22,e22),e23)**. % 0.38/0.55 173[0:Inp] || -> equal(op2(e22,e24),e20)**. % 0.38/0.55 176[0:Inp] || -> equal(op2(e23,e20),e25)**. % 0.38/0.55 178[0:Inp] || -> equal(op2(e23,e22),e26)**. % 0.38/0.55 179[0:Inp] || -> equal(op2(e23,e23),e20)**. % 0.38/0.55 180[0:Inp] || -> equal(op2(e23,e24),e22)**. % 0.38/0.55 182[0:Inp] || -> equal(op2(e23,e26),e24)**. % 0.38/0.55 184[0:Inp] || -> equal(op2(e24,e21),e25)**. % 0.38/0.55 185[0:Inp] || -> equal(op2(e24,e22),e20)**. % 0.38/0.55 186[0:Inp] || -> equal(op2(e24,e23),e22)**. % 0.38/0.55 187[0:Inp] || -> equal(op2(e24,e24),e24)**. % 0.38/0.55 188[0:Inp] || -> equal(op2(e24,e25),e26)**. % 0.38/0.55 189[0:Inp] || -> equal(op2(e24,e26),e21)**. % 0.38/0.55 190[0:Inp] || -> equal(op2(e25,e20),e24)**. % 0.38/0.55 191[0:Inp] || -> equal(op2(e25,e21),e22)**. % 0.38/0.55 194[0:Inp] || -> equal(op2(e25,e24),e26)**. % 0.38/0.55 195[0:Inp] || -> equal(op2(e25,e25),e21)**. % 0.38/0.55 196[0:Inp] || -> equal(op2(e25,e26),e20)**. % 0.38/0.55 197[0:Inp] || -> equal(op2(e26,e20),e26)**. % 0.38/0.55 199[0:Inp] || -> equal(op2(e26,e22),e22)**. % 0.38/0.55 200[0:Inp] || -> equal(op2(e26,e23),e24)**. % 0.38/0.55 201[0:Inp] || -> equal(op2(e26,e24),e21)**. % 0.38/0.55 202[0:Inp] || -> equal(op2(e26,e25),e20)**. % 0.38/0.55 203[0:Inp] || -> equal(op2(e26,e26),e25)**. % 0.38/0.55 205[0:Inp] || -> equal(op2(h(e10),h(e11)),h(op1(e10,e11)))**. % 0.38/0.55 207[0:Inp] || -> equal(op2(h(e10),h(e13)),h(op1(e10,e13)))**. % 0.38/0.55 210[0:Inp] || -> equal(op2(h(e10),h(e16)),h(op1(e10,e16)))**. % 0.38/0.55 211[0:Inp] || -> equal(op2(h(e11),h(e10)),h(op1(e11,e10)))**. % 0.38/0.55 213[0:Inp] || -> equal(op2(h(e11),h(e12)),h(op1(e11,e12)))**. % 0.38/0.55 226[0:Inp] || -> equal(op2(h(e13),h(e11)),h(op1(e13,e11)))**. % 0.38/0.55 232[0:Inp] || -> equal(op2(h(e14),h(e10)),h(op1(e14,e10)))**. % 0.38/0.55 236[0:Inp] || -> equal(op2(h(e14),h(e14)),h(op1(e14,e14)))**. % 0.38/0.55 239[0:Inp] || -> equal(op2(h(e15),h(e10)),h(op1(e15,e10)))**. % 0.38/0.55 240[0:Inp] || -> equal(op2(h(e15),h(e11)),h(op1(e15,e11)))**. % 0.38/0.55 246[0:Inp] || -> equal(op2(h(e16),h(e10)),h(op1(e16,e10)))**. % 0.38/0.55 253[0:Inp] || -> equal(op1(j(e20),j(e20)),j(op2(e20,e20)))**. % 0.38/0.55 258[0:Inp] || -> equal(op1(j(e20),j(e25)),j(op2(e20,e25)))**. % 0.38/0.55 260[0:Inp] || -> equal(op1(j(e21),j(e20)),j(op2(e21,e20)))**. % 0.38/0.55 261[0:Inp] || -> equal(op1(j(e21),j(e21)),j(op2(e21,e21)))**. % 0.38/0.55 262[0:Inp] || -> equal(op1(j(e21),j(e22)),j(op2(e21,e22)))**. % 0.38/0.55 263[0:Inp] || -> equal(op1(j(e21),j(e23)),j(op2(e21,e23)))**. % 0.38/0.55 265[0:Inp] || -> equal(op1(j(e21),j(e25)),j(op2(e21,e25)))**. % 0.38/0.55 268[0:Inp] || -> equal(op1(j(e22),j(e21)),j(op2(e22,e21)))**. % 0.38/0.55 269[0:Inp] || -> equal(op1(j(e22),j(e22)),j(op2(e22,e22)))**. % 0.38/0.55 276[0:Inp] || -> equal(op1(j(e23),j(e22)),j(op2(e23,e22)))**. % 0.38/0.55 277[0:Inp] || -> equal(op1(j(e23),j(e23)),j(op2(e23,e23)))**. % 0.38/0.55 280[0:Inp] || -> equal(op1(j(e23),j(e26)),j(op2(e23,e26)))**. % 0.38/0.55 288[0:Inp] || -> equal(op1(j(e25),j(e20)),j(op2(e25,e20)))**. % 0.38/0.55 293[0:Inp] || -> equal(op1(j(e25),j(e25)),j(op2(e25,e25)))**. % 0.38/0.55 294[0:Inp] || -> equal(op1(j(e25),j(e26)),j(op2(e25,e26)))**. % 0.38/0.55 295[0:Inp] || -> equal(op1(j(e26),j(e20)),j(op2(e26,e20)))**. % 0.38/0.55 297[0:Inp] || -> equal(op1(j(e26),j(e22)),j(op2(e26,e22)))**. % 0.38/0.55 298[0:Inp] || -> equal(op1(j(e26),j(e23)),j(op2(e26,e23)))**. % 0.38/0.55 300[0:Inp] || -> equal(op1(j(e26),j(e25)),j(op2(e26,e25)))**. % 0.38/0.55 301[0:Inp] || -> equal(op1(j(e26),j(e26)),j(op2(e26,e26)))**. % 0.38/0.55 314[0:Inp] || -> equal(h(e11),e26)** equal(h(e11),e25) equal(h(e11),e24) equal(h(e11),e23) equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.38/0.55 315[0:Inp] || -> equal(h(e10),e26)** equal(h(e10),e25) equal(h(e10),e24) equal(h(e10),e23) equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.38/0.55 316[0:Rew:203.0,301.0] || -> equal(op1(j(e26),j(e26)),j(e25))**. % 0.38/0.55 317[0:Rew:202.0,300.0] || -> equal(op1(j(e26),j(e25)),j(e20))**. % 0.38/0.55 319[0:Rew:200.0,298.0] || -> equal(op1(j(e26),j(e23)),j(e24))**. % 0.38/0.55 320[0:Rew:199.0,297.0] || -> equal(op1(j(e26),j(e22)),j(e22))**. % 0.38/0.55 322[0:Rew:197.0,295.0] || -> equal(op1(j(e26),j(e20)),j(e26))**. % 0.38/0.55 323[0:Rew:196.0,294.0] || -> equal(op1(j(e25),j(e26)),j(e20))**. % 0.38/0.55 324[0:Rew:195.0,293.0] || -> equal(op1(j(e25),j(e25)),j(e21))**. % 0.38/0.55 329[0:Rew:190.0,288.0] || -> equal(op1(j(e25),j(e20)),j(e24))**. % 0.38/0.55 337[0:Rew:182.0,280.0] || -> equal(op1(j(e23),j(e26)),j(e24))**. % 0.38/0.55 340[0:Rew:179.0,277.0] || -> equal(op1(j(e23),j(e23)),j(e20))**. % 0.38/0.55 341[0:Rew:178.0,276.0] || -> equal(op1(j(e23),j(e22)),j(e26))**. % 0.38/0.55 348[0:Rew:171.0,269.0] || -> equal(op1(j(e22),j(e22)),j(e23))**. % 0.38/0.55 349[0:Rew:170.0,268.0] || -> equal(op1(j(e22),j(e21)),j(e24))**. % 0.38/0.55 352[0:Rew:167.0,265.0] || -> equal(op1(j(e21),j(e25)),j(e22))**. % 0.38/0.55 354[0:Rew:165.0,263.0] || -> equal(op1(j(e21),j(e23)),j(e21))**. % 0.38/0.55 355[0:Rew:164.0,262.0] || -> equal(op1(j(e21),j(e22)),j(e24))**. % 0.38/0.55 356[0:Rew:163.0,261.0] || -> equal(op1(j(e21),j(e21)),j(e26))**. % 0.38/0.55 357[0:Rew:162.0,260.0] || -> equal(op1(j(e21),j(e20)),j(e20))**. % 0.38/0.55 359[0:Rew:160.0,258.0] || -> equal(op1(j(e20),j(e25)),j(e24))**. % 0.38/0.55 364[0:Rew:155.0,253.0] || -> equal(op1(j(e20),j(e20)),j(e22))**. % 0.38/0.55 371[0:Rew:148.0,246.0] || -> equal(op2(h(e16),h(e10)),h(e15))**. % 0.38/0.55 377[0:Rew:142.0,240.0] || -> equal(op2(h(e15),h(e11)),h(e10))**. % 0.38/0.55 378[0:Rew:141.0,239.0] || -> equal(op2(h(e15),h(e10)),h(e14))**. % 0.38/0.55 381[0:Rew:138.0,236.0] || -> equal(op2(h(e14),h(e14)),h(e14))**. % 0.38/0.55 385[0:Rew:134.0,232.0] || -> equal(op2(h(e14),h(e10)),h(e16))**. % 0.38/0.55 391[0:Rew:128.0,226.0] || -> equal(op2(h(e13),h(e11)),h(e15))**. % 0.38/0.55 404[0:Rew:115.0,213.0] || -> equal(op2(h(e11),h(e12)),h(e16))**. % 0.38/0.55 406[0:Rew:113.0,211.0] || -> equal(op2(h(e11),h(e10)),h(e13))**. % 0.38/0.55 407[0:Rew:112.0,210.0] || -> equal(op2(h(e10),h(e16)),h(e15))**. % 0.38/0.55 410[0:Rew:109.0,207.0] || -> equal(op2(h(e10),h(e13)),h(e12))**. % 0.38/0.55 412[0:Rew:107.0,205.0] || -> equal(op2(h(e10),h(e11)),h(e13))**. % 0.38/0.55 414[1:Spt:315.0] || -> equal(h(e10),e26)**. % 0.38/0.55 415[1:Rew:414.0,99.0] || -> equal(j(e26),e10)**. % 0.38/0.55 436[1:Rew:415.0,316.0] || -> equal(op1(e10,e10),j(e25))**. % 0.38/0.55 437[1:Rew:415.0,317.0] || -> equal(op1(e10,j(e25)),j(e20))**. % 0.38/0.55 439[1:Rew:415.0,319.0] || -> equal(op1(e10,j(e23)),j(e24))**. % 0.38/0.55 456[1:Rew:106.0,436.0] || -> equal(j(e25),e10)**. % 0.38/0.55 485[1:Rew:106.0,437.0,456.0,437.0] || -> equal(j(e20),e10)**. % 0.38/0.55 492[1:Rew:485.0,364.0] || -> equal(op1(e10,e10),j(e22))**. % 0.38/0.55 497[1:Rew:106.0,492.0] || -> equal(j(e22),e10)**. % 0.38/0.55 501[1:Rew:497.0,348.0] || -> equal(op1(e10,e10),j(e23))**. % 0.38/0.55 506[1:Rew:106.0,501.0] || -> equal(j(e23),e10)**. % 0.38/0.55 513[1:Rew:106.0,439.0,506.0,439.0] || -> equal(j(e24),e10)**. % 0.38/0.55 514[1:Rew:513.0,96.0] || -> equal(h(e10),e24)**. % 0.38/0.55 517[1:Rew:414.0,514.0] || -> equal(e26,e24)**. % 0.38/0.55 518[1:MRR:517.0,41.0] || -> . % 0.38/0.55 554[1:Spt:518.0,315.0,414.0] || equal(h(e10),e26)** -> . % 0.38/0.55 555[1:Spt:518.0,315.1,315.2,315.3,315.4,315.5,315.6] || -> equal(h(e10),e25)** equal(h(e10),e24) equal(h(e10),e23) equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.38/0.55 556[2:Spt:555.0] || -> equal(h(e10),e25)**. % 0.38/0.55 557[2:Rew:556.0,99.0] || -> equal(j(e25),e10)**. % 0.38/0.55 581[2:Rew:557.0,323.0] || -> equal(op1(e10,j(e26)),j(e20))**. % 0.38/0.55 585[2:Rew:557.0,359.0] || -> equal(op1(j(e20),e10),j(e24))**. % 0.38/0.55 596[2:Rew:557.0,324.0] || -> equal(op1(e10,e10),j(e21))**. % 0.38/0.55 599[2:Rew:106.0,596.0] || -> equal(j(e21),e10)**. % 0.38/0.55 601[2:Rew:599.0,356.0] || -> equal(op1(e10,e10),j(e26))**. % 0.38/0.55 616[2:Rew:106.0,601.0] || -> equal(j(e26),e10)**. % 0.38/0.55 630[2:Rew:106.0,581.0,616.0,581.0] || -> equal(j(e20),e10)**. % 0.38/0.55 660[2:Rew:106.0,585.0,630.0,585.0] || -> equal(j(e24),e10)**. % 0.38/0.55 661[2:Rew:660.0,96.0] || -> equal(h(e10),e24)**. % 0.38/0.55 665[2:Rew:556.0,661.0] || -> equal(e25,e24)**. % 0.38/0.55 666[2:MRR:665.0,40.0] || -> . % 0.38/0.55 698[2:Spt:666.0,555.0,556.0] || equal(h(e10),e25)** -> . % 0.38/0.55 699[2:Spt:666.0,555.1,555.2,555.3,555.4,555.5] || -> equal(h(e10),e24)** equal(h(e10),e23) equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.38/0.55 700[3:Spt:699.0] || -> equal(h(e10),e24)**. % 0.38/0.55 702[3:Rew:700.0,99.0] || -> equal(j(e24),e10)**. % 0.38/0.55 705[3:Rew:700.0,371.0] || -> equal(op2(h(e16),e24),h(e15))**. % 0.38/0.55 706[3:Rew:700.0,377.0] || -> equal(op2(h(e15),h(e11)),e24)**. % 0.38/0.55 707[3:Rew:700.0,378.0] || -> equal(op2(h(e15),e24),h(e14))**. % 0.38/0.55 709[3:Rew:700.0,385.0] || -> equal(op2(h(e14),e24),h(e16))**. % 0.38/0.55 715[3:Rew:700.0,406.0] || -> equal(op2(h(e11),e24),h(e13))**. % 0.38/0.55 716[3:Rew:700.0,407.0] || -> equal(op2(e24,h(e16)),h(e15))**. % 0.38/0.55 719[3:Rew:700.0,410.0] || -> equal(op2(e24,h(e13)),h(e12))**. % 0.38/0.55 721[3:Rew:700.0,412.0] || -> equal(op2(e24,h(e11)),h(e13))**. % 0.38/0.55 744[4:Spt:314.0] || -> equal(h(e11),e26)**. % 0.38/0.55 752[4:Rew:744.0,391.0] || -> equal(op2(h(e13),e26),h(e15))**. % 0.38/0.55 762[4:Rew:744.0,715.0] || -> equal(op2(e26,e24),h(e13))**. % 0.38/0.55 786[4:Rew:201.0,762.0] || -> equal(h(e13),e21)**. % 0.38/0.55 863[4:Rew:168.0,752.0,786.0,752.0] || -> equal(h(e15),e23)**. % 0.38/0.55 864[4:Rew:863.0,104.0] || -> equal(j(e23),e15)**. % 0.38/0.55 867[4:Rew:863.0,707.0] || -> equal(op2(e23,e24),h(e14))**. % 0.38/0.55 875[4:Rew:864.0,340.0] || -> equal(op1(e15,e15),j(e20))**. % 0.38/0.55 891[4:Rew:180.0,867.0] || -> equal(h(e14),e22)**. % 0.38/0.55 892[4:Rew:891.0,103.0] || -> equal(j(e22),e14)**. % 0.38/0.55 901[4:Rew:892.0,364.0] || -> equal(op1(j(e20),j(e20)),e14)**. % 0.38/0.55 919[4:Rew:146.0,875.0] || -> equal(j(e20),e15)**. % 0.38/0.55 1022[4:Rew:146.0,901.0,919.0,901.0] || -> equal(e15,e14)**. % 0.38/0.55 1023[4:MRR:1022.0,19.0] || -> . % 0.38/0.55 1024[4:Spt:1023.0,314.0,744.0] || equal(h(e11),e26)** -> . % 0.38/0.55 1025[4:Spt:1023.0,314.1,314.2,314.3,314.4,314.5,314.6] || -> equal(h(e11),e25)** equal(h(e11),e24) equal(h(e11),e23) equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.38/0.55 1026[5:Spt:1025.0] || -> equal(h(e11),e25)**. % 0.38/0.55 1029[5:Rew:1026.0,721.0] || -> equal(op2(e24,e25),h(e13))**. % 0.38/0.55 1036[5:Rew:1026.0,404.0] || -> equal(op2(e25,h(e12)),h(e16))**. % 0.38/0.55 1069[5:Rew:188.0,1029.0] || -> equal(h(e13),e26)**. % 0.38/0.55 1071[5:Rew:1069.0,719.0] || -> equal(op2(e24,e26),h(e12))**. % 0.38/0.55 1121[5:Rew:189.0,1071.0] || -> equal(h(e12),e21)**. % 0.38/0.55 1145[5:Rew:191.0,1036.0,1121.0,1036.0] || -> equal(h(e16),e22)**. % 0.38/0.55 1146[5:Rew:1145.0,105.0] || -> equal(j(e22),e16)**. % 0.38/0.55 1147[5:Rew:1145.0,716.0] || -> equal(op2(e24,e22),h(e15))**. % 0.38/0.55 1159[5:Rew:1146.0,348.0] || -> equal(op1(e16,e16),j(e23))**. % 0.38/0.55 1169[5:Rew:185.0,1147.0] || -> equal(h(e15),e20)**. % 0.38/0.55 1170[5:Rew:1169.0,104.0] || -> equal(j(e20),e15)**. % 0.38/0.55 1179[5:Rew:1170.0,340.0] || -> equal(op1(j(e23),j(e23)),e15)**. % 0.38/0.55 1193[5:Rew:154.0,1159.0] || -> equal(j(e23),e16)**. % 0.38/0.55 1306[5:Rew:154.0,1179.0,1193.0,1179.0] || -> equal(e16,e15)**. % 0.38/0.55 1307[5:MRR:1306.0,21.0] || -> . % 0.38/0.55 1308[5:Spt:1307.0,1025.0,1026.0] || equal(h(e11),e25)** -> . % 0.38/0.55 1309[5:Spt:1307.0,1025.1,1025.2,1025.3,1025.4,1025.5] || -> equal(h(e11),e24)** equal(h(e11),e23) equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.38/0.55 1310[6:Spt:1309.0] || -> equal(h(e11),e24)**. % 0.38/0.55 1314[6:Rew:1310.0,706.0] || -> equal(op2(h(e15),e24),e24)**. % 0.38/0.55 1335[6:Rew:707.0,1314.0] || -> equal(h(e14),e24)**. % 0.38/0.55 1339[6:Rew:1335.0,709.0] || -> equal(op2(e24,e24),h(e16))**. % 0.38/0.55 1366[6:Rew:187.0,1339.0] || -> equal(h(e16),e24)**. % 0.38/0.55 1370[6:Rew:1366.0,705.0] || -> equal(op2(e24,e24),h(e15))**. % 0.38/0.55 1388[6:Rew:187.0,1370.0] || -> equal(h(e15),e24)**. % 0.38/0.55 1389[6:Rew:1388.0,104.0] || -> equal(j(e24),e15)**. % 0.38/0.55 1393[6:Rew:702.0,1389.0] || -> equal(e15,e10)**. % 0.38/0.55 1394[6:MRR:1393.0,5.0] || -> . % 0.38/0.55 1420[6:Spt:1394.0,1309.0,1310.0] || equal(h(e11),e24)** -> . % 0.38/0.55 1421[6:Spt:1394.0,1309.1,1309.2,1309.3,1309.4] || -> equal(h(e11),e23)** equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.38/0.55 1422[7:Spt:1421.0] || -> equal(h(e11),e23)**. % 0.38/0.55 1427[7:Rew:1422.0,721.0] || -> equal(op2(e24,e23),h(e13))**. % 0.38/0.55 1434[7:Rew:1422.0,404.0] || -> equal(op2(e23,h(e12)),h(e16))**. % 0.38/0.55 1467[7:Rew:186.0,1427.0] || -> equal(h(e13),e22)**. % 0.38/0.55 1471[7:Rew:1467.0,719.0] || -> equal(op2(e24,e22),h(e12))**. % 0.38/0.55 1519[7:Rew:185.0,1471.0] || -> equal(h(e12),e20)**. % 0.38/0.55 1543[7:Rew:176.0,1434.0,1519.0,1434.0] || -> equal(h(e16),e25)**. % 0.38/0.55 1544[7:Rew:1543.0,105.0] || -> equal(j(e25),e16)**. % 0.38/0.55 1547[7:Rew:1543.0,716.0] || -> equal(op2(e24,e25),h(e15))**. % 0.38/0.55 1557[7:Rew:1544.0,324.0] || -> equal(op1(e16,e16),j(e21))**. % 0.38/0.55 1567[7:Rew:188.0,1547.0] || -> equal(h(e15),e26)**. % 0.38/0.55 1568[7:Rew:1567.0,104.0] || -> equal(j(e26),e15)**. % 0.38/0.55 1577[7:Rew:1568.0,356.0] || -> equal(op1(j(e21),j(e21)),e15)**. % 0.38/0.55 1591[7:Rew:154.0,1557.0] || -> equal(j(e21),e16)**. % 0.38/0.55 1704[7:Rew:154.0,1577.0,1591.0,1577.0] || -> equal(e16,e15)**. % 0.38/0.55 1705[7:MRR:1704.0,21.0] || -> . % 0.38/0.55 1706[7:Spt:1705.0,1421.0,1422.0] || equal(h(e11),e23)** -> . % 0.38/0.55 1707[7:Spt:1705.0,1421.1,1421.2,1421.3] || -> equal(h(e11),e22)** equal(h(e11),e21) equal(h(e11),e20). % 0.38/0.55 1708[8:Spt:1707.0] || -> equal(h(e11),e22)**. % 0.38/0.55 1717[8:Rew:1708.0,715.0] || -> equal(op2(e22,e24),h(e13))**. % 0.38/0.55 1726[8:Rew:1708.0,391.0] || -> equal(op2(h(e13),e22),h(e15))**. % 0.38/0.55 1754[8:Rew:173.0,1717.0] || -> equal(h(e13),e20)**. % 0.38/0.55 1833[8:Rew:157.0,1726.0,1754.0,1726.0] || -> equal(h(e15),e21)**. % 0.38/0.55 1834[8:Rew:1833.0,104.0] || -> equal(j(e21),e15)**. % 0.38/0.55 1837[8:Rew:1833.0,707.0] || -> equal(op2(e21,e24),h(e14))**. % 0.38/0.55 1850[8:Rew:1834.0,356.0] || -> equal(op1(e15,e15),j(e26))**. % 0.38/0.55 1861[8:Rew:166.0,1837.0] || -> equal(h(e14),e25)**. % 0.38/0.55 1862[8:Rew:1861.0,103.0] || -> equal(j(e25),e14)**. % 0.38/0.55 1873[8:Rew:1862.0,316.0] || -> equal(op1(j(e26),j(e26)),e14)**. % 0.38/0.55 1891[8:Rew:146.0,1850.0] || -> equal(j(e26),e15)**. % 0.38/0.55 1994[8:Rew:146.0,1873.0,1891.0,1873.0] || -> equal(e15,e14)**. % 0.38/0.55 1995[8:MRR:1994.0,19.0] || -> . % 0.38/0.55 1996[8:Spt:1995.0,1707.0,1708.0] || equal(h(e11),e22)** -> . % 0.38/0.55 1997[8:Spt:1995.0,1707.1,1707.2] || -> equal(h(e11),e21)** equal(h(e11),e20). % 0.38/0.55 1998[9:Spt:1997.0] || -> equal(h(e11),e21)**. % 0.38/0.55 2005[9:Rew:1998.0,721.0] || -> equal(op2(e24,e21),h(e13))**. % 0.38/0.55 2012[9:Rew:1998.0,404.0] || -> equal(op2(e21,h(e12)),h(e16))**. % 0.38/0.55 2045[9:Rew:184.0,2005.0] || -> equal(h(e13),e25)**. % 0.38/0.55 2049[9:Rew:2045.0,719.0] || -> equal(op2(e24,e25),h(e12))**. % 0.38/0.55 2097[9:Rew:188.0,2049.0] || -> equal(h(e12),e26)**. % 0.38/0.55 2121[9:Rew:168.0,2012.0,2097.0,2012.0] || -> equal(h(e16),e23)**. % 0.38/0.55 2122[9:Rew:2121.0,105.0] || -> equal(j(e23),e16)**. % 0.38/0.55 2123[9:Rew:2121.0,716.0] || -> equal(op2(e24,e23),h(e15))**. % 0.38/0.55 2136[9:Rew:2122.0,340.0] || -> equal(op1(e16,e16),j(e20))**. % 0.38/0.55 2145[9:Rew:186.0,2123.0] || -> equal(h(e15),e22)**. % 0.38/0.55 2146[9:Rew:2145.0,104.0] || -> equal(j(e22),e15)**. % 0.38/0.55 2155[9:Rew:2146.0,364.0] || -> equal(op1(j(e20),j(e20)),e15)**. % 0.38/0.55 2169[9:Rew:154.0,2136.0] || -> equal(j(e20),e16)**. % 0.38/0.55 2282[9:Rew:154.0,2155.0,2169.0,2155.0] || -> equal(e16,e15)**. % 0.38/0.55 2283[9:MRR:2282.0,21.0] || -> . % 0.38/0.55 2284[9:Spt:2283.0,1997.0,1998.0] || equal(h(e11),e21)** -> . % 0.38/0.55 2285[9:Spt:2283.0,1997.1] || -> equal(h(e11),e20)**. % 0.38/0.55 2297[9:Rew:159.0,715.0,2285.0,715.0] || -> equal(h(e13),e23)**. % 0.38/0.55 2330[9:Rew:176.0,391.0,2297.0,391.0,2285.0,391.0] || -> equal(h(e15),e25)**. % 0.38/0.55 2336[9:Rew:2330.0,707.0] || -> equal(op2(e25,e24),h(e14))**. % 0.38/0.55 2347[9:Rew:194.0,2336.0] || -> equal(h(e14),e26)**. % 0.38/0.55 2472[9:Rew:203.0,381.0,2347.0,381.0] || -> equal(e26,e25)**. % 0.38/0.55 2473[9:MRR:2472.0,42.0] || -> . % 0.38/0.57 2474[3:Spt:2473.0,699.0,700.0] || equal(h(e10),e24)** -> . % 0.38/0.57 2475[3:Spt:2473.0,699.1,699.2,699.3,699.4] || -> equal(h(e10),e23)** equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.38/0.57 2476[4:Spt:2475.0] || -> equal(h(e10),e23)**. % 0.38/0.57 2478[4:Rew:2476.0,99.0] || -> equal(j(e23),e10)**. % 0.38/0.57 2501[4:Rew:2478.0,354.0] || -> equal(op1(j(e21),e10),j(e21))**. % 0.38/0.57 2511[4:Rew:2478.0,340.0] || -> equal(op1(e10,e10),j(e20))**. % 0.38/0.57 2517[4:Rew:2478.0,337.0] || -> equal(op1(e10,j(e26)),j(e24))**. % 0.38/0.57 2521[4:Rew:106.0,2511.0] || -> equal(j(e20),e10)**. % 0.38/0.57 2524[4:Rew:2521.0,357.0] || -> equal(op1(j(e21),e10),e10)**. % 0.38/0.57 2550[4:Rew:2524.0,2501.0] || -> equal(j(e21),e10)**. % 0.38/0.57 2553[4:Rew:2550.0,356.0] || -> equal(op1(e10,e10),j(e26))**. % 0.38/0.57 2562[4:Rew:106.0,2553.0] || -> equal(j(e26),e10)**. % 0.38/0.57 2589[4:Rew:106.0,2517.0,2562.0,2517.0] || -> equal(j(e24),e10)**. % 0.38/0.57 2590[4:Rew:2589.0,96.0] || -> equal(h(e10),e24)**. % 0.38/0.57 2594[4:Rew:2476.0,2590.0] || -> equal(e24,e23)**. % 0.38/0.57 2595[4:MRR:2594.0,37.0] || -> . % 0.38/0.57 2620[4:Spt:2595.0,2475.0,2476.0] || equal(h(e10),e23)** -> . % 0.38/0.57 2621[4:Spt:2595.0,2475.1,2475.2,2475.3] || -> equal(h(e10),e22)** equal(h(e10),e21) equal(h(e10),e20). % 0.38/0.57 2622[5:Spt:2621.0] || -> equal(h(e10),e22)**. % 0.38/0.57 2625[5:Rew:2622.0,99.0] || -> equal(j(e22),e10)**. % 0.38/0.57 2650[5:Rew:2625.0,348.0] || -> equal(op1(e10,e10),j(e23))**. % 0.38/0.57 2651[5:Rew:2625.0,341.0] || -> equal(op1(j(e23),e10),j(e26))**. % 0.38/0.57 2658[5:Rew:2625.0,349.0] || -> equal(op1(e10,j(e21)),j(e24))**. % 0.38/0.57 2668[5:Rew:106.0,2650.0] || -> equal(j(e23),e10)**. % 0.38/0.57 2699[5:Rew:106.0,2651.0,2668.0,2651.0] || -> equal(j(e26),e10)**. % 0.38/0.57 2706[5:Rew:2699.0,316.0] || -> equal(op1(e10,e10),j(e25))**. % 0.38/0.57 2711[5:Rew:106.0,2706.0] || -> equal(j(e25),e10)**. % 0.38/0.57 2715[5:Rew:2711.0,324.0] || -> equal(op1(e10,e10),j(e21))**. % 0.38/0.57 2720[5:Rew:106.0,2715.0] || -> equal(j(e21),e10)**. % 0.38/0.57 2732[5:Rew:106.0,2658.0,2720.0,2658.0] || -> equal(j(e24),e10)**. % 0.38/0.57 2733[5:Rew:2732.0,96.0] || -> equal(h(e10),e24)**. % 0.38/0.57 2737[5:Rew:2622.0,2733.0] || -> equal(e24,e22)**. % 0.38/0.57 2738[5:MRR:2737.0,34.0] || -> . % 0.38/0.57 2767[5:Spt:2738.0,2621.0,2622.0] || equal(h(e10),e22)** -> . % 0.38/0.57 2768[5:Spt:2738.0,2621.1,2621.2] || -> equal(h(e10),e21)** equal(h(e10),e20). % 0.38/0.57 2769[6:Spt:2768.0] || -> equal(h(e10),e21)**. % 0.38/0.57 2772[6:Rew:2769.0,99.0] || -> equal(j(e21),e10)**. % 0.38/0.57 2796[6:Rew:2772.0,352.0] || -> equal(op1(e10,j(e25)),j(e22))**. % 0.38/0.57 2798[6:Rew:2772.0,355.0] || -> equal(op1(e10,j(e22)),j(e24))**. % 0.38/0.57 2808[6:Rew:2772.0,356.0] || -> equal(op1(e10,e10),j(e26))**. % 0.38/0.57 2816[6:Rew:106.0,2808.0] || -> equal(j(e26),e10)**. % 0.38/0.57 2828[6:Rew:2816.0,316.0] || -> equal(op1(e10,e10),j(e25))**. % 0.38/0.57 2833[6:Rew:106.0,2828.0] || -> equal(j(e25),e10)**. % 0.38/0.57 2845[6:Rew:106.0,2796.0,2833.0,2796.0] || -> equal(j(e22),e10)**. % 0.38/0.57 2873[6:Rew:106.0,2798.0,2845.0,2798.0] || -> equal(j(e24),e10)**. % 0.38/0.57 2874[6:Rew:2873.0,96.0] || -> equal(h(e10),e24)**. % 0.38/0.57 2876[6:Rew:2769.0,2874.0] || -> equal(e24,e21)**. % 0.38/0.57 2877[6:MRR:2876.0,30.0] || -> . % 0.38/0.57 2913[6:Spt:2877.0,2768.0,2769.0] || equal(h(e10),e21)** -> . % 0.38/0.57 2914[6:Spt:2877.0,2768.1] || -> equal(h(e10),e20)**. % 0.38/0.57 2918[6:Rew:2914.0,99.0] || -> equal(j(e20),e10)**. % 0.38/0.57 2947[6:Rew:2918.0,322.0] || -> equal(op1(j(e26),e10),j(e26))**. % 0.38/0.57 2951[6:Rew:2918.0,329.0] || -> equal(op1(j(e25),e10),j(e24))**. % 0.38/0.57 2957[6:Rew:106.0,364.0,2918.0,364.0] || -> equal(j(e22),e10)**. % 0.38/0.57 2967[6:Rew:2957.0,320.0] || -> equal(op1(j(e26),e10),e10)**. % 0.38/0.57 2995[6:Rew:2947.0,2967.0] || -> equal(j(e26),e10)**. % 0.38/0.57 2999[6:Rew:2995.0,316.0] || -> equal(op1(e10,e10),j(e25))**. % 0.38/0.57 3020[6:Rew:106.0,2999.0] || -> equal(j(e25),e10)**. % 0.38/0.57 3022[6:Rew:3020.0,2951.0] || -> equal(op1(e10,e10),j(e24))**. % 0.38/0.57 3032[6:Rew:106.0,3022.0] || -> equal(j(e24),e10)**. % 0.38/0.57 3033[6:Rew:3032.0,96.0] || -> equal(h(e10),e24)**. % 0.38/0.57 3036[6:Rew:2914.0,3033.0] || -> equal(e24,e20)**. % 0.38/0.57 3037[6:MRR:3036.0,25.0] || -> . % 0.38/0.57 % SZS output end Refutation % 0.38/0.57 Formulae used in the proof : ax1 ax2 co1 ax4 ax5 % 0.38/0.57 %------------------------------------------------------------------------------