%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG105+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:28 EDT 2022 % Result : Theorem 0.53s 0.75s % Output : Refutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ALG105+1 : TPTP v8.1.0. Released v2.7.0. % 0.11/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 : Thu Jun 9 06:38:04 EDT 2022 % 0.13/0.34 % CPUTime : % 0.53/0.75 % 0.53/0.75 SPASS V 3.9 % 0.53/0.75 SPASS beiseite: Proof found. % 0.53/0.75 % SZS status Theorem % 0.53/0.75 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.53/0.75 SPASS derived 423 clauses, backtracked 340 clauses, performed 4 splits and kept 777 clauses. % 0.53/0.75 SPASS allocated 87708 KBytes. % 0.53/0.75 SPASS spent 0:00:00.40 on the problem. % 0.53/0.75 0:00:00.04 for the input. % 0.53/0.75 0:00:00.14 for the FLOTTER CNF translation. % 0.53/0.75 0:00:00.00 for inferences. % 0.53/0.75 0:00:00.00 for the backtracking. % 0.53/0.75 0:00:00.17 for the reduction. % 0.53/0.75 % 0.53/0.75 % 0.53/0.75 Here is a proof with depth 2, length 286 : % 0.53/0.75 % SZS output start Refutation % 0.53/0.75 1[0:Inp] || equal(e11,e10)** -> . % 0.53/0.75 2[0:Inp] || equal(e12,e10)** -> . % 0.53/0.75 3[0:Inp] || equal(e13,e10)** -> . % 0.53/0.75 4[0:Inp] || equal(e12,e11)** -> . % 0.53/0.75 5[0:Inp] || equal(e13,e11)** -> . % 0.53/0.75 6[0:Inp] || equal(e13,e12)** -> . % 0.53/0.75 7[0:Inp] || equal(e21,e20)** -> . % 0.53/0.75 8[0:Inp] || equal(e22,e20)** -> . % 0.53/0.75 9[0:Inp] || equal(e23,e20)** -> . % 0.53/0.75 10[0:Inp] || equal(e22,e21)** -> . % 0.53/0.75 11[0:Inp] || equal(e23,e21)** -> . % 0.53/0.75 12[0:Inp] || equal(e22,e23)** -> . % 0.53/0.75 45[0:Inp] || -> equal(h9(e11),e22)**. % 0.53/0.75 46[0:Inp] || -> equal(h9(e12),e23)**. % 0.53/0.75 53[0:Inp] || -> equal(op1(e12,e11),e13)**. % 0.53/0.75 54[0:Inp] || -> equal(op2(e22,e21),e23)**. % 0.53/0.75 151[0:Inp] || equal(h9(e10),e20)** -> SkC30. % 0.53/0.75 158[0:Inp] || equal(h9(e13),e21)** -> SkC31. % 0.53/0.75 160[0:Inp] || equal(h9(e11),e22)** -> SkC32. % 0.53/0.75 199[0:Inp] || -> equal(op2(e21,e20),h1(e13))**. % 0.53/0.75 200[0:Inp] || -> equal(op2(e22,e20),h2(e13))**. % 0.53/0.75 201[0:Inp] || -> equal(op2(e23,e20),h3(e13))**. % 0.53/0.75 202[0:Inp] || -> equal(op2(e20,e21),h4(e13))**. % 0.53/0.75 204[0:Inp] || -> equal(op2(e23,e21),h6(e13))**. % 0.53/0.75 205[0:Inp] || -> equal(op2(e20,e22),h7(e13))**. % 0.53/0.75 206[0:Inp] || -> equal(op2(e21,e22),h8(e13))**. % 0.53/0.75 207[0:Inp] || -> equal(op2(e23,e22),h9(e13))**. % 0.53/0.75 208[0:Inp] || -> equal(op2(e20,e23),h10(e13))**. % 0.53/0.75 209[0:Inp] || -> equal(op2(e21,e23),h11(e13))**. % 0.53/0.75 210[0:Inp] || -> equal(op2(e22,e23),h12(e13))**. % 0.53/0.75 211[0:Inp] || -> equal(op1(op1(e10,e10),e10),e10)**. % 0.53/0.75 212[0:Inp] || -> equal(op1(op1(e10,e11),e10),e11)**. % 0.53/0.75 213[0:Inp] || -> equal(op1(op1(e10,e12),e10),e12)**. % 0.53/0.75 214[0:Inp] || -> equal(op1(op1(e10,e13),e10),e13)**. % 0.53/0.75 220[0:Inp] || -> equal(op1(op1(e12,e11),e12),e11)**. % 0.53/0.75 222[0:Inp] || -> equal(op1(op1(e12,e13),e12),e13)**. % 0.53/0.75 224[0:Inp] || -> equal(op1(op1(e13,e11),e13),e11)**. % 0.53/0.75 225[0:Inp] || -> equal(op1(op1(e13,e12),e13),e12)**. % 0.53/0.75 226[0:Inp] || -> equal(op1(op1(e13,e13),e13),e13)**. % 0.53/0.75 228[0:Inp] || -> equal(op2(op2(e20,e21),e20),e21)**. % 0.53/0.75 229[0:Inp] || -> equal(op2(op2(e20,e22),e20),e22)**. % 0.53/0.75 230[0:Inp] || -> equal(op2(op2(e20,e23),e20),e23)**. % 0.53/0.75 232[0:Inp] || -> equal(op2(op2(e21,e21),e21),e21)**. % 0.53/0.75 235[0:Inp] || -> equal(op2(op2(e22,e20),e22),e20)**. % 0.53/0.75 236[0:Inp] || -> equal(op2(op2(e22,e21),e22),e21)**. % 0.53/0.75 237[0:Inp] || -> equal(op2(op2(e22,e22),e22),e22)**. % 0.53/0.75 238[0:Inp] || -> equal(op2(op2(e22,e23),e22),e23)**. % 0.53/0.75 240[0:Inp] || -> equal(op2(op2(e23,e21),e23),e21)**. % 0.53/0.75 241[0:Inp] || -> equal(op2(op2(e23,e22),e23),e22)**. % 0.53/0.75 242[0:Inp] || -> equal(op2(op2(e23,e23),e23),e23)**. % 0.53/0.75 250[0:Inp] || equal(op1(e12,e11),op1(e10,e11))** -> . % 0.53/0.75 251[0:Inp] || equal(op1(e13,e11),op1(e10,e11))** -> . % 0.53/0.75 257[0:Inp] || equal(op1(e13,e12),op1(e10,e12))** -> . % 0.53/0.75 260[0:Inp] || equal(op1(e13,e12),op1(e12,e12))** -> . % 0.53/0.75 267[0:Inp] || equal(op1(e10,e11),op1(e10,e10))** -> . % 0.53/0.75 268[0:Inp] || equal(op1(e10,e12),op1(e10,e10))** -> . % 0.53/0.75 269[0:Inp] || equal(op1(e10,e13),op1(e10,e10))** -> . % 0.53/0.75 272[0:Inp] || equal(op1(e10,e13),op1(e10,e12))** -> . % 0.53/0.75 280[0:Inp] || equal(op1(e12,e12),op1(e12,e10))** -> . % 0.53/0.75 282[0:Inp] || equal(op1(e12,e12),op1(e12,e11))** -> . % 0.53/0.75 297[0:Inp] || equal(op2(e21,e21),op2(e20,e21))** -> . % 0.53/0.75 298[0:Inp] || equal(op2(e22,e21),op2(e20,e21))** -> . % 0.53/0.75 299[0:Inp] || equal(op2(e23,e21),op2(e20,e21))** -> . % 0.53/0.75 300[0:Inp] || equal(op2(e22,e21),op2(e21,e21))** -> . % 0.53/0.75 305[0:Inp] || equal(op2(e23,e22),op2(e20,e22))** -> . % 0.53/0.75 308[0:Inp] || equal(op2(e22,e22),op2(e23,e22))** -> . % 0.53/0.75 323[0:Inp] || equal(op2(e21,e23),op2(e21,e20))** -> . % 0.53/0.75 325[0:Inp] || equal(op2(e21,e23),op2(e21,e21))** -> . % 0.53/0.75 327[0:Inp] || equal(op2(e22,e21),op2(e22,e20))** -> . % 0.53/0.75 328[0:Inp] || equal(op2(e22,e22),op2(e22,e20))** -> . % 0.53/0.75 329[0:Inp] || equal(op2(e22,e23),op2(e22,e20))** -> . % 0.53/0.75 330[0:Inp] || equal(op2(e22,e22),op2(e22,e21))** -> . % 0.53/0.75 339[0:Inp] || -> equal(op1(op1(e12,e11),op1(e12,e11)),e10)**. % 0.53/0.75 340[0:Inp] || -> equal(op2(op2(e22,e21),op2(e22,e21)),e20)**. % 0.53/0.75 346[0:Inp] || -> equal(op2(op2(e23,e21),op2(e23,e21)),h6(e10))**. % 0.53/0.75 349[0:Inp] || -> equal(op2(op2(e23,e22),op2(e23,e22)),h9(e10))**. % 0.53/0.75 351[0:Inp] || -> equal(op2(op2(e21,e23),op2(e21,e23)),h11(e10))**. % 0.53/0.75 353[0:Inp] || SkC0 -> equal(op1(e10,op1(e10,e10)),op1(e10,e10))**. % 0.53/0.75 354[0:Inp] || SkC0 -> equal(op1(e10,op1(e11,e10)),op1(e11,e10))**. % 0.53/0.75 359[0:Inp] || SkC1 -> equal(op1(e11,op1(e12,e11)),op1(e12,e11))**. % 0.53/0.75 364[0:Inp] || SkC2 -> equal(op1(e12,op1(e13,e12)),op1(e13,e12))**. % 0.53/0.75 365[0:Inp] || SkC3 -> equal(op2(e20,op2(e20,e20)),op2(e20,e20))**. % 0.53/0.75 371[0:Inp] || SkC4 -> equal(op2(e21,op2(e22,e21)),op2(e22,e21))**. % 0.53/0.75 376[0:Inp] || SkC5 -> equal(op2(e22,op2(e23,e22)),op2(e23,e22))**. % 0.53/0.75 380[0:Inp] || -> equal(op1(e13,op1(e13,e13)),op1(e13,e13))** SkC0 SkC1 SkC2. % 0.53/0.75 384[0:Inp] || -> equal(op2(e23,op2(e23,e23)),op2(e23,e23))** SkC3 SkC4 SkC5. % 0.53/0.75 388[0:Inp] || -> equal(op2(e23,e20),e22) equal(op2(e23,e21),e22) equal(op2(e23,e22),e22)** equal(op2(e23,e23),e22). % 0.53/0.75 411[0:Inp] || -> equal(op2(e20,e20),e22) equal(op2(e21,e20),e22) equal(op2(e22,e20),e22)** equal(op2(e23,e20),e22). % 0.53/0.75 414[0:Inp] || -> equal(op2(e20,e20),e21) equal(op2(e20,e21),e21) equal(op2(e20,e22),e21)** equal(op2(e20,e23),e21). % 0.53/0.75 416[0:Inp] || -> equal(op2(e20,e20),e20) equal(op2(e20,e21),e20) equal(op2(e20,e22),e20)** equal(op2(e20,e23),e20). % 0.53/0.75 422[0:Inp] || -> equal(op2(e22,e22),e20) equal(op2(e22,e22),e21) equal(op2(e22,e22),e22)** equal(op2(e22,e22),e23). % 0.53/0.75 424[0:Inp] || -> equal(op2(e22,e20),e20) equal(op2(e22,e20),e21) equal(op2(e22,e20),e22)** equal(op2(e22,e20),e23). % 0.53/0.75 427[0:Inp] || -> equal(op2(e21,e21),e20) equal(op2(e21,e21),e21) equal(op2(e21,e21),e22)** equal(op2(e21,e21),e23). % 0.53/0.75 431[0:Inp] || -> equal(op2(e20,e21),e20) equal(op2(e20,e21),e21) equal(op2(e20,e21),e22)** equal(op2(e20,e21),e23). % 0.53/0.75 436[0:Inp] || -> equal(op1(e13,e10),e12) equal(op1(e13,e11),e12) equal(op1(e13,e12),e12) equal(op1(e13,e13),e12)**. % 0.53/0.75 447[0:Inp] || -> equal(op1(e10,e12),e10) equal(op1(e11,e12),e10) equal(op1(e12,e12),e10) equal(op1(e13,e12),e10)**. % 0.53/0.75 455[0:Inp] || -> equal(op1(e10,e11),e10) equal(op1(e11,e11),e10) equal(op1(e12,e11),e10) equal(op1(e13,e11),e10)**. % 0.53/0.75 470[0:Inp] || -> equal(op1(e12,e12),e10) equal(op1(e12,e12),e11) equal(op1(e12,e12),e12) equal(op1(e12,e12),e13)**. % 0.53/0.75 478[0:Inp] || -> equal(op1(e10,e12),e10) equal(op1(e10,e12),e11) equal(op1(e10,e12),e12) equal(op1(e10,e12),e13)**. % 0.53/0.75 479[0:Inp] || -> equal(op1(e10,e11),e10) equal(op1(e10,e11),e11) equal(op1(e10,e11),e12) equal(op1(e10,e11),e13)**. % 0.53/0.75 480[0:Inp] || -> equal(op1(e10,e10),e10) equal(op1(e10,e10),e11) equal(op1(e10,e10),e12) equal(op1(e10,e10),e13)**. % 0.53/0.75 494[0:Inp] || equal(h9(e12),e23) equal(op2(h9(e10),h9(e10)),h9(op1(e10,e10))) equal(op2(h9(e10),h9(e11)),h9(op1(e10,e11))) equal(op2(h9(e10),h9(e12)),h9(op1(e10,e12))) equal(op2(h9(e10),h9(e13)),h9(op1(e10,e13))) equal(op2(h9(e11),h9(e10)),h9(op1(e11,e10))) equal(op2(h9(e11),h9(e11)),h9(op1(e11,e11))) equal(op2(h9(e11),h9(e12)),h9(op1(e11,e12))) equal(op2(h9(e11),h9(e13)),h9(op1(e11,e13))) equal(op2(h9(e12),h9(e10)),h9(op1(e12,e10))) equal(op2(h9(e12),h9(e11)),h9(op1(e12,e11))) equal(op2(h9(e12),h9(e12)),h9(op1(e12,e12))) equal(op2(h9(e12),h9(e13)),h9(op1(e12,e13))) equal(op2(h9(e13),h9(e10)),h9(op1(e13,e10))) equal(op2(h9(e13),h9(e11)),h9(op1(e13,e11))) equal(op2(h9(e13),h9(e12)),h9(op1(e13,e12))) equal(op2(h9(e13),h9(e13)),h9(op1(e13,e13)))** SkC30 SkC31 SkC32 -> . % 0.53/0.75 549[0:Rew:45.0,160.0] || equal(e22,e22) -> SkC32*. % 0.53/0.75 550[0:Obv:549.0] || -> SkC32*. % 0.53/0.75 614[0:Rew:207.0,241.0] || -> equal(op2(h9(e13),e23),e22)**. % 0.53/0.75 615[0:Rew:204.0,240.0] || -> equal(op2(h6(e13),e23),e21)**. % 0.53/0.75 617[0:Rew:210.0,238.0] || -> equal(op2(h12(e13),e22),e23)**. % 0.53/0.75 618[0:Rew:207.0,236.0,54.0,236.0] || -> equal(h9(e13),e21)**. % 0.53/0.75 619[0:Rew:618.0,207.0] || -> equal(op2(e23,e22),e21)**. % 0.53/0.75 620[0:Rew:618.0,158.0] || equal(e21,e21) -> SkC31*. % 0.53/0.75 622[0:Rew:618.0,614.0] || -> equal(op2(e21,e23),e22)**. % 0.53/0.75 623[0:Obv:620.0] || -> SkC31*. % 0.53/0.75 624[0:Rew:209.0,622.0] || -> equal(h11(e13),e22)**. % 0.53/0.75 625[0:Rew:624.0,209.0] || -> equal(op2(e21,e23),e22)**. % 0.53/0.75 629[0:Rew:200.0,235.0] || -> equal(op2(h2(e13),e22),e20)**. % 0.53/0.75 633[0:Rew:208.0,230.0] || -> equal(op2(h10(e13),e20),e23)**. % 0.53/0.75 634[0:Rew:205.0,229.0] || -> equal(op2(h7(e13),e20),e22)**. % 0.53/0.75 635[0:Rew:202.0,228.0] || -> equal(op2(h4(e13),e20),e21)**. % 0.53/0.75 636[0:Rew:53.0,220.0] || -> equal(op1(e13,e12),e11)**. % 0.53/0.75 637[0:Rew:636.0,225.0] || -> equal(op1(e11,e13),e12)**. % 0.53/0.75 647[0:Rew:54.0,330.0] || equal(op2(e22,e22),e23)** -> . % 0.53/0.75 648[0:Rew:210.0,329.0,200.0,329.0] || equal(h12(e13),h2(e13))** -> . % 0.53/0.75 649[0:Rew:200.0,328.0] || equal(op2(e22,e22),h2(e13))** -> . % 0.53/0.75 650[0:Rew:54.0,327.0,200.0,327.0] || equal(h2(e13),e23)** -> . % 0.53/0.75 652[0:Rew:625.0,325.0] || equal(op2(e21,e21),e22)** -> . % 0.53/0.75 654[0:Rew:625.0,323.0,199.0,323.0] || equal(h1(e13),e22)** -> . % 0.53/0.75 669[0:Rew:619.0,308.0] || equal(op2(e22,e22),e21)** -> . % 0.53/0.75 672[0:Rew:619.0,305.0,205.0,305.0] || equal(h7(e13),e21)** -> . % 0.53/0.75 677[0:Rew:54.0,300.0] || equal(op2(e21,e21),e23)** -> . % 0.53/0.75 678[0:Rew:204.0,299.0,202.0,299.0] || equal(h6(e13),h4(e13))** -> . % 0.53/0.75 679[0:Rew:54.0,298.0,202.0,298.0] || equal(h4(e13),e23)** -> . % 0.53/0.75 680[0:Rew:202.0,297.0] || equal(op2(e21,e21),h4(e13))** -> . % 0.53/0.75 691[0:Rew:53.0,282.0] || equal(op1(e12,e12),e13)** -> . % 0.53/0.75 699[0:Rew:636.0,260.0] || equal(op1(e12,e12),e11)** -> . % 0.53/0.75 701[0:Rew:636.0,257.0] || equal(op1(e10,e12),e11)** -> . % 0.53/0.75 704[0:Rew:53.0,250.0] || equal(op1(e10,e11),e13)** -> . % 0.53/0.75 705[0:Rew:54.0,340.0] || -> equal(op2(e23,e23),e20)**. % 0.53/0.75 706[0:Rew:705.0,242.0] || -> equal(op2(e20,e23),e23)**. % 0.53/0.75 713[0:Rew:208.0,706.0] || -> equal(h10(e13),e23)**. % 0.53/0.75 714[0:Rew:713.0,208.0] || -> equal(op2(e20,e23),e23)**. % 0.53/0.75 716[0:Rew:713.0,633.0] || -> equal(op2(e23,e20),e23)**. % 0.53/0.75 723[0:Rew:201.0,716.0] || -> equal(h3(e13),e23)**. % 0.53/0.75 724[0:Rew:723.0,201.0] || -> equal(op2(e23,e20),e23)**. % 0.53/0.75 733[0:Rew:53.0,339.0] || -> equal(op1(e13,e13),e10)**. % 0.53/0.75 734[0:Rew:733.0,226.0] || -> equal(op1(e10,e13),e13)**. % 0.53/0.75 741[0:Rew:734.0,214.0] || -> equal(op1(e13,e10),e13)**. % 0.53/0.75 742[0:Rew:734.0,272.0] || equal(op1(e10,e12),e13)** -> . % 0.53/0.75 744[0:Rew:734.0,269.0] || equal(op1(e10,e10),e13)** -> . % 0.53/0.75 756[0:Rew:625.0,351.0] || -> equal(op2(e22,e22),h11(e10))**. % 0.53/0.75 757[0:Rew:756.0,237.0] || -> equal(op2(h11(e10),e22),e22)**. % 0.53/0.75 759[0:Rew:756.0,647.0] || equal(h11(e10),e23)** -> . % 0.53/0.75 760[0:Rew:756.0,649.0] || equal(h11(e10),h2(e13))** -> . % 0.53/0.75 761[0:Rew:756.0,669.0] || equal(h11(e10),e21)** -> . % 0.53/0.75 767[0:Rew:619.0,349.0] || -> equal(op2(e21,e21),h9(e10))**. % 0.53/0.75 768[0:Rew:767.0,232.0] || -> equal(op2(h9(e10),e21),e21)**. % 0.53/0.75 769[0:Rew:767.0,652.0] || equal(h9(e10),e22)** -> . % 0.53/0.75 773[0:Rew:767.0,677.0] || equal(h9(e10),e23)** -> . % 0.53/0.75 774[0:Rew:767.0,680.0] || equal(h9(e10),h4(e13))** -> . % 0.53/0.75 777[0:Rew:204.0,346.0] || -> equal(op2(h6(e13),h6(e13)),h6(e10))**. % 0.53/0.75 787[0:Rew:54.0,376.1,619.0,376.1] || SkC5* -> equal(e23,e21). % 0.53/0.75 788[0:MRR:787.1,11.0] || SkC5* -> . % 0.53/0.75 790[0:Rew:625.0,371.1,54.0,371.1] || SkC4* -> equal(e22,e23). % 0.53/0.75 791[0:MRR:790.1,12.0] || SkC4* -> . % 0.53/0.75 795[0:Rew:53.0,364.1,636.0,364.1] || SkC2* -> equal(e13,e11). % 0.53/0.75 796[0:MRR:795.1,5.0] || SkC2* -> . % 0.53/0.75 797[0:Rew:637.0,359.1,53.0,359.1] || SkC1* -> equal(e13,e12). % 0.53/0.75 798[0:MRR:797.1,6.0] || SkC1* -> . % 0.53/0.75 800[0:Rew:724.0,384.0,705.0,384.0] || -> equal(e23,e20) SkC3* SkC4 SkC5. % 0.53/0.75 801[0:MRR:800.0,800.2,800.3,9.0,791.0,788.0] || -> SkC3*. % 0.53/0.75 804[0:MRR:365.0,801.0] || -> equal(op2(e20,op2(e20,e20)),op2(e20,e20))**. % 0.53/0.75 805[0:Rew:741.0,380.0,733.0,380.0] || -> equal(e13,e10) SkC0* SkC1 SkC2. % 0.53/0.75 806[0:MRR:805.0,805.2,805.3,3.0,798.0,796.0] || -> SkC0*. % 0.53/0.75 808[0:MRR:354.0,806.0] || -> equal(op1(e10,op1(e11,e10)),op1(e11,e10))**. % 0.53/0.75 809[0:MRR:353.0,806.0] || -> equal(op1(e10,op1(e10,e10)),op1(e10,e10))**. % 0.53/0.75 810[0:Rew:705.0,388.3,619.0,388.2,204.0,388.1,724.0,388.0] || -> equal(e22,e23) equal(h6(e13),e22)** equal(e22,e21) equal(e22,e20). % 0.53/0.75 811[0:MRR:810.0,810.2,810.3,12.0,10.0,8.0] || -> equal(h6(e13),e22)**. % 0.53/0.75 812[0:Rew:811.0,204.0] || -> equal(op2(e23,e21),e22)**. % 0.53/0.75 814[0:Rew:811.0,615.0] || -> equal(op2(e22,e23),e21)**. % 0.53/0.75 817[0:Rew:811.0,678.0] || equal(h4(e13),e22)** -> . % 0.53/0.75 820[0:Rew:811.0,777.0] || -> equal(op2(e22,e22),h6(e10))**. % 0.53/0.75 822[0:Rew:210.0,814.0] || -> equal(h12(e13),e21)**. % 0.53/0.75 823[0:Rew:822.0,210.0] || -> equal(op2(e22,e23),e21)**. % 0.53/0.75 825[0:Rew:822.0,617.0] || -> equal(op2(e21,e22),e23)**. % 0.53/0.76 827[0:Rew:822.0,648.0] || equal(h2(e13),e21)** -> . % 0.53/0.76 833[0:Rew:206.0,825.0] || -> equal(h8(e13),e23)**. % 0.53/0.76 834[0:Rew:833.0,206.0] || -> equal(op2(e21,e22),e23)**. % 0.53/0.76 844[0:Rew:756.0,820.0] || -> equal(h11(e10),h6(e10))**. % 0.53/0.76 846[0:Rew:844.0,756.0] || -> equal(op2(e22,e22),h6(e10))**. % 0.53/0.76 847[0:Rew:844.0,759.0] || equal(h6(e10),e23)** -> . % 0.53/0.76 848[0:Rew:844.0,761.0] || equal(h6(e10),e21)** -> . % 0.53/0.76 849[0:Rew:844.0,757.0] || -> equal(op2(h6(e10),e22),e22)**. % 0.53/0.76 850[0:Rew:844.0,760.0] || equal(h6(e10),h2(e13))** -> . % 0.53/0.76 873[0:Rew:724.0,411.3,200.0,411.2,199.0,411.1] || -> equal(op2(e20,e20),e22)** equal(h1(e13),e22) equal(h2(e13),e22) equal(e22,e23). % 0.53/0.76 874[0:MRR:873.1,873.3,654.0,12.0] || -> equal(h2(e13),e22) equal(op2(e20,e20),e22)**. % 0.53/0.76 879[0:Rew:714.0,414.3,205.0,414.2,202.0,414.1] || -> equal(op2(e20,e20),e21)** equal(h4(e13),e21) equal(h7(e13),e21) equal(e23,e21). % 0.53/0.76 880[0:MRR:879.2,879.3,672.0,11.0] || -> equal(h4(e13),e21) equal(op2(e20,e20),e21)**. % 0.53/0.76 883[0:Rew:714.0,416.3,205.0,416.2,202.0,416.1] || -> equal(op2(e20,e20),e20)** equal(h4(e13),e20) equal(h7(e13),e20) equal(e23,e20). % 0.53/0.76 884[0:MRR:883.3,9.0] || -> equal(h7(e13),e20) equal(h4(e13),e20) equal(op2(e20,e20),e20)**. % 0.53/0.76 885[0:Rew:846.0,422.3,846.0,422.2,846.0,422.1,846.0,422.0] || -> equal(h6(e10),e20) equal(h6(e10),e21) equal(h6(e10),e22)** equal(h6(e10),e23). % 0.53/0.76 886[0:MRR:885.1,885.3,848.0,847.0] || -> equal(h6(e10),e22)** equal(h6(e10),e20). % 0.53/0.76 887[0:Rew:200.0,424.3,200.0,424.2,200.0,424.1,200.0,424.0] || -> equal(h2(e13),e20) equal(h2(e13),e21) equal(h2(e13),e22)** equal(h2(e13),e23). % 0.53/0.76 888[0:MRR:887.1,887.3,827.0,650.0] || -> equal(h2(e13),e22)** equal(h2(e13),e20). % 0.53/0.76 889[0:Rew:767.0,427.3,767.0,427.2,767.0,427.1,767.0,427.0] || -> equal(h9(e10),e20) equal(h9(e10),e21) equal(h9(e10),e22)** equal(h9(e10),e23). % 0.53/0.76 890[0:MRR:889.2,889.3,769.0,773.0] || -> equal(h9(e10),e21)** equal(h9(e10),e20). % 0.53/0.76 895[0:Rew:202.0,431.3,202.0,431.2,202.0,431.1,202.0,431.0] || -> equal(h4(e13),e20) equal(h4(e13),e21) equal(h4(e13),e22)** equal(h4(e13),e23). % 0.53/0.76 896[0:MRR:895.2,895.3,817.0,679.0] || -> equal(h4(e13),e21)** equal(h4(e13),e20). % 0.53/0.76 898[0:Rew:733.0,436.3,636.0,436.2,741.0,436.0] || -> equal(e13,e12) equal(op1(e13,e11),e12)** equal(e12,e11) equal(e12,e10). % 0.53/0.76 899[0:MRR:898.0,898.2,898.3,6.0,4.0,2.0] || -> equal(op1(e13,e11),e12)**. % 0.53/0.76 900[0:Rew:899.0,224.0] || -> equal(op1(e12,e13),e11)**. % 0.53/0.76 904[0:Rew:899.0,251.0] || equal(op1(e10,e11),e12)** -> . % 0.53/0.76 906[0:Rew:900.0,222.0] || -> equal(op1(e11,e12),e13)**. % 0.53/0.76 923[0:Rew:636.0,447.3,906.0,447.1] || -> equal(op1(e10,e12),e10) equal(e13,e10) equal(op1(e12,e12),e10)** equal(e11,e10). % 0.53/0.76 924[0:MRR:923.1,923.3,3.0,1.0] || -> equal(op1(e12,e12),e10)** equal(op1(e10,e12),e10). % 0.53/0.76 931[0:Rew:899.0,455.3,53.0,455.2] || -> equal(op1(e10,e11),e10) equal(op1(e11,e11),e10)** equal(e13,e10) equal(e12,e10). % 0.53/0.76 932[0:MRR:931.2,931.3,3.0,2.0] || -> equal(op1(e11,e11),e10)** equal(op1(e10,e11),e10). % 0.53/0.76 947[0:MRR:470.1,470.3,699.0,691.0] || -> equal(op1(e12,e12),e12)** equal(op1(e12,e12),e10). % 0.53/0.76 951[0:MRR:478.1,478.3,701.0,742.0] || -> equal(op1(e10,e12),e12)** equal(op1(e10,e12),e10). % 0.53/0.76 952[0:MRR:479.2,479.3,904.0,704.0] || -> equal(op1(e10,e11),e11)** equal(op1(e10,e11),e10). % 0.53/0.76 953[0:MRR:480.3,744.0] || -> equal(op1(e10,e10),e10) equal(op1(e10,e10),e12)** equal(op1(e10,e10),e11). % 0.53/0.76 983[0:Rew:767.0,494.16,618.0,494.16,733.0,494.16,625.0,494.15,618.0,494.15,46.0,494.15,45.0,494.15,636.0,494.15,834.0,494.14,618.0,494.14,45.0,494.14,46.0,494.14,899.0,494.14,618.0,494.13,741.0,494.13,812.0,494.12,46.0,494.12,618.0,494.12,45.0,494.12,900.0,494.12,705.0,494.11,46.0,494.11,619.0,494.10,46.0,494.10,45.0,494.10,618.0,494.10,53.0,494.10,46.0,494.9,54.0,494.8,45.0,494.8,618.0,494.8,46.0,494.8,637.0,494.8,823.0,494.7,45.0,494.7,46.0,494.7,618.0,494.7,906.0,494.7,846.0,494.6,45.0,494.6,45.0,494.5,768.0,494.4,618.0,494.4,734.0,494.4,46.0,494.3,45.0,494.2,46.0,494.0] || equal(e23,e23) equal(op2(h9(e10),h9(e10)),h9(op1(e10,e10)))** equal(op2(h9(e10),e22),h9(op1(e10,e11))) equal(op2(h9(e10),e23),h9(op1(e10,e12))) equal(e21,e21) equal(op2(e22,h9(e10)),h9(op1(e11,e10))) equal(h9(op1(e11,e11)),h6(e10)) equal(e21,e21) equal(e23,e23) equal(op2(e23,h9(e10)),h9(op1(e12,e10))) equal(e21,e21) equal(h9(op1(e12,e12)),e20) equal(e22,e22) equal(op2(e21,h9(e10)),e21) equal(e23,e23) equal(e22,e22) equal(h9(e10),h9(e10)) SkC30 SkC31 SkC32 -> . % 0.53/0.77 984[0:Obv:983.16] || equal(op2(h9(e10),h9(e10)),h9(op1(e10,e10)))** equal(op2(h9(e10),e22),h9(op1(e10,e11))) equal(op2(h9(e10),e23),h9(op1(e10,e12))) equal(op2(e22,h9(e10)),h9(op1(e11,e10))) equal(h9(op1(e11,e11)),h6(e10)) equal(op2(e23,h9(e10)),h9(op1(e12,e10))) equal(h9(op1(e12,e12)),e20) equal(op2(e21,h9(e10)),e21) SkC30 SkC31 SkC32 -> . % 0.53/0.77 985[0:MRR:984.9,984.10,623.0,550.0] || SkC30 equal(h9(op1(e12,e12)),e20) equal(h9(op1(e11,e11)),h6(e10)) equal(op2(e21,h9(e10)),e21) equal(op2(e23,h9(e10)),h9(op1(e12,e10))) equal(op2(e22,h9(e10)),h9(op1(e11,e10))) equal(op2(h9(e10),e23),h9(op1(e10,e12))) equal(op2(h9(e10),e22),h9(op1(e10,e11))) equal(op2(h9(e10),h9(e10)),h9(op1(e10,e10)))** -> . % 0.53/0.77 1050[1:Spt:953.0] || -> equal(op1(e10,e10),e10)**. % 0.53/0.77 1057[1:Rew:1050.0,268.0] || equal(op1(e10,e12),e10)** -> . % 0.53/0.77 1058[1:Rew:1050.0,267.0] || equal(op1(e10,e11),e10)** -> . % 0.53/0.77 1067[1:Rew:1050.0,985.8] || SkC30 equal(h9(op1(e12,e12)),e20) equal(h9(op1(e11,e11)),h6(e10)) equal(op2(e21,h9(e10)),e21) equal(op2(e23,h9(e10)),h9(op1(e12,e10))) equal(op2(e22,h9(e10)),h9(op1(e11,e10))) equal(op2(h9(e10),e23),h9(op1(e10,e12))) equal(op2(h9(e10),e22),h9(op1(e10,e11))) equal(op2(h9(e10),h9(e10)),h9(e10))** -> . % 0.53/0.77 1074[1:MRR:924.1,1057.0] || -> equal(op1(e12,e12),e10)**. % 0.53/0.77 1075[1:MRR:951.1,1057.0] || -> equal(op1(e10,e12),e12)**. % 0.53/0.77 1085[1:Rew:1075.0,213.0] || -> equal(op1(e12,e10),e12)**. % 0.53/0.77 1093[1:MRR:932.1,1058.0] || -> equal(op1(e11,e11),e10)**. % 0.53/0.77 1094[1:MRR:952.1,1058.0] || -> equal(op1(e10,e11),e11)**. % 0.53/0.77 1104[1:Rew:1094.0,212.0] || -> equal(op1(e11,e10),e11)**. % 0.53/0.77 1126[1:Rew:45.0,1067.7,1094.0,1067.7,46.0,1067.6,1075.0,1067.6,45.0,1067.5,1104.0,1067.5,46.0,1067.4,1085.0,1067.4,1093.0,1067.2,1074.0,1067.1] || SkC30 equal(h9(e10),e20) equal(h9(e10),h6(e10)) equal(op2(e21,h9(e10)),e21) equal(op2(e23,h9(e10)),e23) equal(op2(e22,h9(e10)),e22) equal(op2(h9(e10),e23),e23) equal(op2(h9(e10),e22),e22) equal(op2(h9(e10),h9(e10)),h9(e10))** -> . % 0.53/0.77 1127[1:MRR:1126.0,151.1] || equal(h9(e10),e20) equal(h9(e10),h6(e10)) equal(op2(e21,h9(e10)),e21) equal(op2(e23,h9(e10)),e23) equal(op2(e22,h9(e10)),e22) equal(op2(h9(e10),e23),e23) equal(op2(h9(e10),e22),e22) equal(op2(h9(e10),h9(e10)),h9(e10))** -> . % 0.53/0.77 1135[2:Spt:886.0] || -> equal(h6(e10),e22)**. % 0.53/0.77 1147[2:Rew:1135.0,850.0] || equal(h2(e13),e22)** -> . % 0.53/0.77 1152[2:MRR:888.0,1147.0] || -> equal(h2(e13),e20)**. % 0.53/0.77 1153[2:MRR:874.0,1147.0] || -> equal(op2(e20,e20),e22)**. % 0.53/0.77 1157[2:Rew:1152.0,629.0] || -> equal(op2(e20,e22),e20)**. % 0.53/0.77 1181[2:Rew:1153.0,804.0] || -> equal(op2(e20,e22),e22)**. % 0.53/0.77 1215[2:Rew:1157.0,1181.0] || -> equal(e22,e20)**. % 0.53/0.77 1216[2:MRR:1215.0,8.0] || -> . % 0.53/0.77 1241[2:Spt:1216.0,886.0,1135.0] || equal(h6(e10),e22)** -> . % 0.53/0.77 1242[2:Spt:1216.0,886.1] || -> equal(h6(e10),e20)**. % 0.53/0.77 1249[2:Rew:1242.0,849.0] || -> equal(op2(e20,e22),e22)**. % 0.53/0.77 1255[2:Rew:1249.0,205.0] || -> equal(h7(e13),e22)**. % 0.53/0.77 1260[2:Rew:1255.0,634.0] || -> equal(op2(e22,e20),e22)**. % 0.53/0.77 1261[2:Rew:200.0,1260.0] || -> equal(h2(e13),e22)**. % 0.53/0.77 1267[2:Rew:1261.0,200.0] || -> equal(op2(e22,e20),e22)**. % 0.53/0.77 1277[2:Rew:1255.0,884.0] || -> equal(e22,e20) equal(h4(e13),e20) equal(op2(e20,e20),e20)**. % 0.53/0.77 1278[2:MRR:1277.0,8.0] || -> equal(h4(e13),e20) equal(op2(e20,e20),e20)**. % 0.53/0.77 1284[2:Rew:1242.0,1127.1] || equal(h9(e10),e20) equal(h9(e10),e20) equal(op2(e21,h9(e10)),e21) equal(op2(e23,h9(e10)),e23) equal(op2(e22,h9(e10)),e22) equal(op2(h9(e10),e23),e23) equal(op2(h9(e10),e22),e22) equal(op2(h9(e10),h9(e10)),h9(e10))** -> . % 0.53/0.77 1285[2:Obv:1284.0] || equal(h9(e10),e20) equal(op2(e21,h9(e10)),e21) equal(op2(e23,h9(e10)),e23) equal(op2(e22,h9(e10)),e22) equal(op2(h9(e10),e23),e23) equal(op2(h9(e10),e22),e22) equal(op2(h9(e10),h9(e10)),h9(e10))** -> . % 0.53/0.77 1291[3:Spt:890.0] || -> equal(h9(e10),e21)**. % 0.53/0.77 1295[3:Rew:1291.0,774.0] || equal(h4(e13),e21)** -> . % 0.53/0.77 1307[3:MRR:896.0,1295.0] || -> equal(h4(e13),e20)**. % 0.53/0.77 1308[3:MRR:880.0,1295.0] || -> equal(op2(e20,e20),e21)**. % 0.53/0.77 1312[3:Rew:1307.0,202.0] || -> equal(op2(e20,e21),e20)**. % 0.53/0.77 1329[3:Rew:1308.0,804.0] || -> equal(op2(e20,e21),e21)**. % 0.53/0.77 1334[3:Rew:1312.0,1329.0] || -> equal(e21,e20)**. % 0.53/0.77 1335[3:MRR:1334.0,7.0] || -> . % 0.53/0.77 1346[3:Spt:1335.0,890.0,1291.0] || equal(h9(e10),e21)** -> . % 0.53/0.77 1347[3:Spt:1335.0,890.1] || -> equal(h9(e10),e20)**. % 0.53/0.77 1357[3:Rew:1347.0,768.0] || -> equal(op2(e20,e21),e21)**. % 0.53/0.77 1360[3:Rew:1357.0,202.0] || -> equal(h4(e13),e21)**. % 0.53/0.77 1364[3:Rew:1360.0,635.0] || -> equal(op2(e21,e20),e21)**. % 0.53/0.77 1377[3:Rew:1360.0,1278.0] || -> equal(e21,e20) equal(op2(e20,e20),e20)**. % 0.53/0.77 1378[3:MRR:1377.0,7.0] || -> equal(op2(e20,e20),e20)**. % 0.53/0.77 1390[3:Rew:1378.0,1285.6,1347.0,1285.6,1249.0,1285.5,1347.0,1285.5,714.0,1285.4,1347.0,1285.4,1267.0,1285.3,1347.0,1285.3,724.0,1285.2,1347.0,1285.2,1364.0,1285.1,1347.0,1285.1,1347.0,1285.0] || equal(e20,e20) equal(e21,e21) equal(e23,e23) equal(e22,e22)* equal(e23,e23) equal(e22,e22)* equal(e20,e20) -> . % 0.53/0.77 1391[3:Obv:1390.6] || -> . % 0.53/0.77 1396[1:Spt:1391.0,953.0,1050.0] || equal(op1(e10,e10),e10)** -> . % 0.53/0.77 1397[1:Spt:1391.0,953.1,953.2] || -> equal(op1(e10,e10),e12)** equal(op1(e10,e10),e11). % 0.53/0.77 1400[2:Spt:1397.0] || -> equal(op1(e10,e10),e12)**. % 0.53/0.77 1403[2:Rew:1400.0,211.0] || -> equal(op1(e12,e10),e10)**. % 0.53/0.77 1408[2:Rew:1400.0,809.0] || -> equal(op1(e10,e12),e12)**. % 0.53/0.77 1426[2:Rew:1403.0,280.0] || equal(op1(e12,e12),e10)** -> . % 0.53/0.77 1436[2:Rew:1408.0,924.1] || -> equal(op1(e12,e12),e10)** equal(e12,e10). % 0.53/0.77 1446[2:MRR:947.1,1426.0] || -> equal(op1(e12,e12),e12)**. % 0.53/0.77 1475[2:Rew:1446.0,1436.0] || -> equal(e12,e10)** equal(e12,e10)**. % 0.53/0.77 1476[2:Obv:1475.0] || -> equal(e12,e10)**. % 0.53/0.77 1477[2:MRR:1476.0,2.0] || -> . % 0.53/0.77 1494[2:Spt:1477.0,1397.0,1400.0] || equal(op1(e10,e10),e12)** -> . % 0.53/0.77 1495[2:Spt:1477.0,1397.1] || -> equal(op1(e10,e10),e11)**. % 0.53/0.77 1499[2:Rew:1495.0,211.0] || -> equal(op1(e11,e10),e10)**. % 0.53/0.77 1516[2:Rew:1495.0,808.0,1499.0,808.0] || -> equal(e11,e10)**. % 0.53/0.77 1517[2:MRR:1516.0,1.0] || -> . % 0.53/0.77 % SZS output end Refutation % 0.53/0.77 Formulae used in the proof : ax7 ax8 ax22 ax12 ax13 co1 ax14 ax15 ax16 ax17 ax19 ax20 ax21 ax23 ax24 ax25 ax10 ax11 ax5 ax6 ax4 ax3 ax2 ax1 % 0.53/0.77 %------------------------------------------------------------------------------