%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG042+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:05 EDT 2022 % Result : Theorem 0.18s 0.46s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : ALG042+1 : TPTP v8.1.0. Released v2.7.0. % 0.10/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 8 14:48:36 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.46 % 0.18/0.46 SPASS V 3.9 % 0.18/0.46 SPASS beiseite: Proof found. % 0.18/0.46 % SZS status Theorem % 0.18/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.46 SPASS derived 442 clauses, backtracked 468 clauses, performed 15 splits and kept 754 clauses. % 0.18/0.46 SPASS allocated 85497 KBytes. % 0.18/0.46 SPASS spent 0:00:00.13 on the problem. % 0.18/0.46 0:00:00.03 for the input. % 0.18/0.46 0:00:00.03 for the FLOTTER CNF translation. % 0.18/0.46 0:00:00.00 for inferences. % 0.18/0.46 0:00:00.00 for the backtracking. % 0.18/0.46 0:00:00.04 for the reduction. % 0.18/0.46 % 0.18/0.46 % 0.18/0.46 Here is a proof with depth 3, length 245 : % 0.18/0.46 % SZS output start Refutation % 0.18/0.46 1[0:Inp] || equal(e11,e10)** -> . % 0.18/0.46 2[0:Inp] || equal(e12,e10)** -> . % 0.18/0.46 3[0:Inp] || equal(e13,e10)** -> . % 0.18/0.46 4[0:Inp] || equal(e12,e11)** -> . % 0.18/0.46 5[0:Inp] || equal(e13,e11)** -> . % 0.18/0.46 6[0:Inp] || equal(e13,e12)** -> . % 0.18/0.46 9[0:Inp] || equal(e23,e20)** -> . % 0.18/0.46 10[0:Inp] || equal(e22,e21)** -> . % 0.18/0.46 29[0:Inp] || -> equal(h(j(e20)),e20)**. % 0.18/0.46 30[0:Inp] || -> equal(h(j(e21)),e21)**. % 0.18/0.46 31[0:Inp] || -> equal(h(j(e22)),e22)**. % 0.18/0.46 32[0:Inp] || -> equal(h(j(e23)),e23)**. % 0.18/0.46 34[0:Inp] || -> equal(j(h(e11)),e11)**. % 0.18/0.46 35[0:Inp] || -> equal(j(h(e12)),e12)**. % 0.18/0.46 36[0:Inp] || -> equal(j(h(e13)),e13)**. % 0.18/0.46 38[0:Inp] || -> equal(op1(e10,e11),e11)**. % 0.18/0.46 40[0:Inp] || -> equal(op1(e10,e13),e13)**. % 0.18/0.46 41[0:Inp] || -> equal(op1(e11,e10),e11)**. % 0.18/0.46 42[0:Inp] || -> equal(op1(e11,e11),e10)**. % 0.18/0.46 43[0:Inp] || -> equal(op1(e11,e12),e13)**. % 0.18/0.46 44[0:Inp] || -> equal(op1(e11,e13),e12)**. % 0.18/0.46 45[0:Inp] || -> equal(op1(e12,e10),e12)**. % 0.18/0.46 46[0:Inp] || -> equal(op1(e12,e11),e13)**. % 0.18/0.46 47[0:Inp] || -> equal(op1(e12,e12),e10)**. % 0.18/0.46 48[0:Inp] || -> equal(op1(e12,e13),e11)**. % 0.18/0.46 49[0:Inp] || -> equal(op1(e13,e10),e13)**. % 0.18/0.46 50[0:Inp] || -> equal(op1(e13,e11),e12)**. % 0.18/0.46 51[0:Inp] || -> equal(op1(e13,e12),e11)**. % 0.18/0.46 52[0:Inp] || -> equal(op1(e13,e13),e10)**. % 0.18/0.46 53[0:Inp] || -> equal(op2(e20,e20),e20)**. % 0.18/0.46 56[0:Inp] || -> equal(op2(e20,e23),e23)**. % 0.18/0.46 57[0:Inp] || -> equal(op2(e21,e20),e21)**. % 0.18/0.46 58[0:Inp] || -> equal(op2(e21,e21),e23)**. % 0.18/0.46 59[0:Inp] || -> equal(op2(e21,e22),e20)**. % 0.18/0.46 60[0:Inp] || -> equal(op2(e21,e23),e22)**. % 0.18/0.46 62[0:Inp] || -> equal(op2(e22,e21),e20)**. % 0.18/0.46 63[0:Inp] || -> equal(op2(e22,e22),e23)**. % 0.18/0.46 64[0:Inp] || -> equal(op2(e22,e23),e21)**. % 0.18/0.46 66[0:Inp] || -> equal(op2(e23,e21),e22)**. % 0.18/0.46 67[0:Inp] || -> equal(op2(e23,e22),e21)**. % 0.18/0.46 68[0:Inp] || -> equal(op2(e23,e23),e20)**. % 0.18/0.46 72[0:Inp] || -> equal(op2(h(e10),h(e13)),h(op1(e10,e13)))**. % 0.18/0.46 74[0:Inp] || -> equal(op2(h(e11),h(e11)),h(op1(e11,e11)))**. % 0.18/0.46 75[0:Inp] || -> equal(op2(h(e11),h(e12)),h(op1(e11,e12)))**. % 0.18/0.46 77[0:Inp] || -> equal(op2(h(e12),h(e10)),h(op1(e12,e10)))**. % 0.18/0.46 78[0:Inp] || -> equal(op2(h(e12),h(e11)),h(op1(e12,e11)))**. % 0.18/0.46 79[0:Inp] || -> equal(op2(h(e12),h(e12)),h(op1(e12,e12)))**. % 0.18/0.46 80[0:Inp] || -> equal(op2(h(e12),h(e13)),h(op1(e12,e13)))**. % 0.18/0.46 83[0:Inp] || -> equal(op2(h(e13),h(e12)),h(op1(e13,e12)))**. % 0.18/0.46 84[0:Inp] || -> equal(op2(h(e13),h(e13)),h(op1(e13,e13)))**. % 0.18/0.46 89[0:Inp] || -> equal(op1(j(e21),j(e20)),j(op2(e21,e20)))**. % 0.18/0.46 90[0:Inp] || -> equal(op1(j(e21),j(e21)),j(op2(e21,e21)))**. % 0.18/0.46 91[0:Inp] || -> equal(op1(j(e21),j(e22)),j(op2(e21,e22)))**. % 0.18/0.46 92[0:Inp] || -> equal(op1(j(e21),j(e23)),j(op2(e21,e23)))**. % 0.18/0.46 94[0:Inp] || -> equal(op1(j(e22),j(e21)),j(op2(e22,e21)))**. % 0.18/0.46 95[0:Inp] || -> equal(op1(j(e22),j(e22)),j(op2(e22,e22)))**. % 0.18/0.46 96[0:Inp] || -> equal(op1(j(e22),j(e23)),j(op2(e22,e23)))**. % 0.18/0.46 98[0:Inp] || -> equal(op1(j(e23),j(e21)),j(op2(e23,e21)))**. % 0.18/0.46 99[0:Inp] || -> equal(op1(j(e23),j(e22)),j(op2(e23,e22)))**. % 0.18/0.46 102[0:Inp] || -> equal(h(e11),e23)** equal(h(e11),e22) equal(h(e11),e21) equal(h(e11),e20). % 0.18/0.46 105[0:Inp] || -> equal(j(e20),e13)** equal(j(e20),e12) equal(j(e20),e11) equal(j(e20),e10). % 0.18/0.46 106[0:Inp] || -> equal(j(e21),e13)** equal(j(e21),e12) equal(j(e21),e11) equal(j(e21),e10). % 0.18/0.46 107[0:Inp] || -> equal(j(e22),e13)** equal(j(e22),e12) equal(j(e22),e11) equal(j(e22),e10). % 0.18/0.46 108[0:Inp] || -> equal(j(e23),e13)** equal(j(e23),e12) equal(j(e23),e11) equal(j(e23),e10). % 0.18/0.46 110[0:Rew:67.0,99.0] || -> equal(op1(j(e23),j(e22)),j(e21))**. % 0.18/0.46 111[0:Rew:66.0,98.0] || -> equal(op1(j(e23),j(e21)),j(e22))**. % 0.18/0.46 113[0:Rew:64.0,96.0] || -> equal(op1(j(e22),j(e23)),j(e21))**. % 0.18/0.46 114[0:Rew:63.0,95.0] || -> equal(op1(j(e22),j(e22)),j(e23))**. % 0.18/0.46 115[0:Rew:62.0,94.0] || -> equal(op1(j(e22),j(e21)),j(e20))**. % 0.18/0.46 117[0:Rew:60.0,92.0] || -> equal(op1(j(e21),j(e23)),j(e22))**. % 0.18/0.46 118[0:Rew:59.0,91.0] || -> equal(op1(j(e21),j(e22)),j(e20))**. % 0.18/0.46 119[0:Rew:58.0,90.0] || -> equal(op1(j(e21),j(e21)),j(e23))**. % 0.18/0.46 120[0:Rew:57.0,89.0] || -> equal(op1(j(e21),j(e20)),j(e21))**. % 0.18/0.46 125[0:Rew:52.0,84.0] || -> equal(op2(h(e13),h(e13)),h(e10))**. % 0.18/0.46 126[0:Rew:51.0,83.0] || -> equal(op2(h(e13),h(e12)),h(e11))**. % 0.18/0.46 129[0:Rew:48.0,80.0] || -> equal(op2(h(e12),h(e13)),h(e11))**. % 0.18/0.46 130[0:Rew:47.0,79.0] || -> equal(op2(h(e12),h(e12)),h(e10))**. % 0.18/0.46 131[0:Rew:46.0,78.0] || -> equal(op2(h(e12),h(e11)),h(e13))**. % 0.18/0.46 132[0:Rew:45.0,77.0] || -> equal(op2(h(e12),h(e10)),h(e12))**. % 0.18/0.46 134[0:Rew:43.0,75.0] || -> equal(op2(h(e11),h(e12)),h(e13))**. % 0.18/0.46 135[0:Rew:42.0,74.0] || -> equal(op2(h(e11),h(e11)),h(e10))**. % 0.18/0.46 137[0:Rew:40.0,72.0] || -> equal(op2(h(e10),h(e13)),h(e13))**. % 0.18/0.46 141[1:Spt:105.0] || -> equal(j(e20),e13)**. % 0.18/0.46 142[1:Rew:141.0,29.0] || -> equal(h(e13),e20)**. % 0.18/0.46 154[1:Rew:142.0,125.0] || -> equal(op2(e20,e20),h(e10))**. % 0.18/0.46 158[1:Rew:142.0,129.0] || -> equal(op2(h(e12),e20),h(e11))**. % 0.18/0.46 165[1:Rew:53.0,154.0] || -> equal(h(e10),e20)**. % 0.18/0.46 168[1:Rew:165.0,132.0] || -> equal(op2(h(e12),e20),h(e12))**. % 0.18/0.46 178[1:Rew:158.0,168.0] || -> equal(h(e12),h(e11))**. % 0.18/0.46 179[1:Rew:178.0,35.0] || -> equal(j(h(e11)),e12)**. % 0.18/0.46 188[1:Rew:34.0,179.0] || -> equal(e12,e11)**. % 0.18/0.46 189[1:MRR:188.0,4.0] || -> . % 0.18/0.46 192[1:Spt:189.0,105.0,141.0] || equal(j(e20),e13)** -> . % 0.18/0.46 193[1:Spt:189.0,105.1,105.2,105.3] || -> equal(j(e20),e12)** equal(j(e20),e11) equal(j(e20),e10). % 0.18/0.46 194[2:Spt:193.0] || -> equal(j(e20),e12)**. % 0.18/0.46 195[2:Rew:194.0,29.0] || -> equal(h(e12),e20)**. % 0.18/0.46 211[2:Rew:195.0,129.0] || -> equal(op2(e20,h(e13)),h(e11))**. % 0.18/0.46 216[2:Rew:195.0,130.0] || -> equal(op2(e20,e20),h(e10))**. % 0.18/0.46 219[2:Rew:53.0,216.0] || -> equal(h(e10),e20)**. % 0.18/0.46 221[2:Rew:219.0,137.0] || -> equal(op2(e20,h(e13)),h(e13))**. % 0.18/0.46 232[2:Rew:211.0,221.0] || -> equal(h(e13),h(e11))**. % 0.18/0.46 233[2:Rew:232.0,36.0] || -> equal(j(h(e11)),e13)**. % 0.18/0.46 241[2:Rew:34.0,233.0] || -> equal(e13,e11)**. % 0.18/0.46 242[2:MRR:241.0,5.0] || -> . % 0.18/0.46 246[2:Spt:242.0,193.0,194.0] || equal(j(e20),e12)** -> . % 0.18/0.46 247[2:Spt:242.0,193.1,193.2] || -> equal(j(e20),e11)** equal(j(e20),e10). % 0.18/0.46 248[3:Spt:247.0] || -> equal(j(e20),e11)**. % 0.18/0.46 250[3:Rew:248.0,29.0] || -> equal(h(e11),e20)**. % 0.18/0.46 266[3:Rew:250.0,131.0] || -> equal(op2(h(e12),e20),h(e13))**. % 0.18/0.46 269[3:Rew:250.0,135.0] || -> equal(op2(e20,e20),h(e10))**. % 0.18/0.46 274[3:Rew:53.0,269.0] || -> equal(h(e10),e20)**. % 0.18/0.46 277[3:Rew:274.0,132.0] || -> equal(op2(h(e12),e20),h(e12))**. % 0.18/0.46 287[3:Rew:266.0,277.0] || -> equal(h(e13),h(e12))**. % 0.18/0.46 288[3:Rew:287.0,36.0] || -> equal(j(h(e12)),e13)**. % 0.18/0.46 296[3:Rew:35.0,288.0] || -> equal(e13,e12)**. % 0.18/0.46 297[3:MRR:296.0,6.0] || -> . % 0.18/0.46 302[3:Spt:297.0,247.0,248.0] || equal(j(e20),e11)** -> . % 0.18/0.46 303[3:Spt:297.0,247.1] || -> equal(j(e20),e10)**. % 0.18/0.46 313[3:Rew:303.0,120.0] || -> equal(op1(j(e21),e10),j(e21))**. % 0.18/0.46 314[3:Rew:303.0,118.0] || -> equal(op1(j(e21),j(e22)),e10)**. % 0.18/0.46 316[3:Rew:303.0,115.0] || -> equal(op1(j(e22),j(e21)),e10)**. % 0.18/0.46 330[4:Spt:108.0] || -> equal(j(e23),e13)**. % 0.18/0.46 331[4:Rew:330.0,32.0] || -> equal(h(e13),e23)**. % 0.18/0.46 332[4:Rew:330.0,110.0] || -> equal(op1(e13,j(e22)),j(e21))**. % 0.18/0.46 334[4:Rew:330.0,113.0] || -> equal(op1(j(e22),e13),j(e21))**. % 0.18/0.46 337[4:Rew:330.0,119.0] || -> equal(op1(j(e21),j(e21)),e13)**. % 0.18/0.46 342[4:Rew:331.0,134.0] || -> equal(op2(h(e11),h(e12)),e23)**. % 0.18/0.46 344[4:Rew:331.0,131.0] || -> equal(op2(h(e12),h(e11)),e23)**. % 0.18/0.46 352[5:Spt:107.0] || -> equal(j(e22),e13)**. % 0.18/0.46 357[5:Rew:352.0,316.0] || -> equal(op1(e13,j(e21)),e10)**. % 0.18/0.46 358[5:Rew:352.0,332.0] || -> equal(op1(e13,e13),j(e21))**. % 0.18/0.46 367[5:Rew:52.0,358.0] || -> equal(j(e21),e10)**. % 0.18/0.46 373[5:Rew:367.0,357.0] || -> equal(op1(e13,e10),e10)**. % 0.18/0.46 380[5:Rew:49.0,373.0] || -> equal(e13,e10)**. % 0.18/0.46 381[5:MRR:380.0,3.0] || -> . % 0.18/0.46 385[5:Spt:381.0,107.0,352.0] || equal(j(e22),e13)** -> . % 0.18/0.46 386[5:Spt:381.0,107.1,107.2,107.3] || -> equal(j(e22),e12)** equal(j(e22),e11) equal(j(e22),e10). % 0.18/0.46 387[6:Spt:386.0] || -> equal(j(e22),e12)**. % 0.18/0.46 388[6:Rew:387.0,31.0] || -> equal(h(e12),e22)**. % 0.18/0.46 392[6:Rew:387.0,334.0] || -> equal(op1(e12,e13),j(e21))**. % 0.18/0.46 405[6:Rew:388.0,344.0] || -> equal(op2(e22,h(e11)),e23)**. % 0.18/0.47 413[6:Rew:48.0,392.0] || -> equal(j(e21),e11)**. % 0.18/0.47 414[6:Rew:413.0,30.0] || -> equal(h(e11),e21)**. % 0.18/0.47 436[6:Rew:62.0,405.0,414.0,405.0] || -> equal(e23,e20)**. % 0.18/0.47 437[6:MRR:436.0,9.0] || -> . % 0.18/0.47 441[6:Spt:437.0,386.0,387.0] || equal(j(e22),e12)** -> . % 0.18/0.47 442[6:Spt:437.0,386.1,386.2] || -> equal(j(e22),e11)** equal(j(e22),e10). % 0.18/0.47 443[7:Spt:442.0] || -> equal(j(e22),e11)**. % 0.18/0.47 445[7:Rew:443.0,31.0] || -> equal(h(e11),e22)**. % 0.18/0.47 451[7:Rew:443.0,332.0] || -> equal(op1(e13,e11),j(e21))**. % 0.18/0.47 462[7:Rew:445.0,342.0] || -> equal(op2(e22,h(e12)),e23)**. % 0.18/0.47 470[7:Rew:50.0,451.0] || -> equal(j(e21),e12)**. % 0.18/0.47 471[7:Rew:470.0,30.0] || -> equal(h(e12),e21)**. % 0.18/0.47 498[7:Rew:62.0,462.0,471.0,462.0] || -> equal(e23,e20)**. % 0.18/0.47 499[7:MRR:498.0,9.0] || -> . % 0.18/0.47 500[7:Spt:499.0,442.0,443.0] || equal(j(e22),e11)** -> . % 0.18/0.47 501[7:Spt:499.0,442.1] || -> equal(j(e22),e10)**. % 0.18/0.47 510[7:Rew:40.0,334.0,501.0,334.0] || -> equal(j(e21),e13)**. % 0.18/0.47 523[7:Rew:52.0,337.0,510.0,337.0] || -> equal(e13,e10)**. % 0.18/0.47 524[7:MRR:523.0,3.0] || -> . % 0.18/0.47 527[4:Spt:524.0,108.0,330.0] || equal(j(e23),e13)** -> . % 0.18/0.47 528[4:Spt:524.0,108.1,108.2,108.3] || -> equal(j(e23),e12)** equal(j(e23),e11) equal(j(e23),e10). % 0.18/0.47 529[5:Spt:528.0] || -> equal(j(e23),e12)**. % 0.18/0.47 530[5:Rew:529.0,32.0] || -> equal(h(e12),e23)**. % 0.18/0.47 548[5:Rew:530.0,131.0] || -> equal(op2(e23,h(e11)),h(e13))**. % 0.18/0.47 550[5:Rew:530.0,134.0] || -> equal(op2(h(e11),e23),h(e13))**. % 0.18/0.47 552[6:Spt:102.0] || -> equal(h(e11),e23)**. % 0.18/0.47 560[6:Rew:552.0,548.0] || -> equal(op2(e23,e23),h(e13))**. % 0.18/0.47 565[6:Rew:68.0,560.0] || -> equal(h(e13),e20)**. % 0.18/0.47 566[6:Rew:565.0,36.0] || -> equal(j(e20),e13)**. % 0.18/0.47 572[6:Rew:303.0,566.0] || -> equal(e13,e10)**. % 0.18/0.47 573[6:MRR:572.0,3.0] || -> . % 0.18/0.47 576[6:Spt:573.0,102.0,552.0] || equal(h(e11),e23)** -> . % 0.18/0.47 577[6:Spt:573.0,102.1,102.2,102.3] || -> equal(h(e11),e22)** equal(h(e11),e21) equal(h(e11),e20). % 0.18/0.47 578[7:Spt:577.0] || -> equal(h(e11),e22)**. % 0.18/0.47 579[7:Rew:578.0,34.0] || -> equal(j(e22),e11)**. % 0.18/0.47 581[7:Rew:578.0,550.0] || -> equal(op2(e22,e23),h(e13))**. % 0.18/0.47 593[7:Rew:579.0,314.0] || -> equal(op1(j(e21),e11),e10)**. % 0.18/0.47 604[7:Rew:64.0,581.0] || -> equal(h(e13),e21)**. % 0.18/0.47 605[7:Rew:604.0,36.0] || -> equal(j(e21),e13)**. % 0.18/0.47 626[7:Rew:50.0,593.0,605.0,593.0] || -> equal(e12,e10)**. % 0.18/0.47 627[7:MRR:626.0,2.0] || -> . % 0.18/0.47 632[7:Spt:627.0,577.0,578.0] || equal(h(e11),e22)** -> . % 0.18/0.47 633[7:Spt:627.0,577.1,577.2] || -> equal(h(e11),e21)** equal(h(e11),e20). % 0.18/0.47 634[8:Spt:633.0] || -> equal(h(e11),e21)**. % 0.18/0.47 636[8:Rew:634.0,34.0] || -> equal(j(e21),e11)**. % 0.18/0.47 644[8:Rew:634.0,548.0] || -> equal(op2(e23,e21),h(e13))**. % 0.18/0.47 653[8:Rew:636.0,316.0] || -> equal(op1(j(e22),e11),e10)**. % 0.18/0.47 661[8:Rew:66.0,644.0] || -> equal(h(e13),e22)**. % 0.18/0.47 662[8:Rew:661.0,36.0] || -> equal(j(e22),e13)**. % 0.18/0.47 688[8:Rew:50.0,653.0,662.0,653.0] || -> equal(e12,e10)**. % 0.18/0.47 689[8:MRR:688.0,2.0] || -> . % 0.18/0.47 690[8:Spt:689.0,633.0,634.0] || equal(h(e11),e21)** -> . % 0.18/0.47 691[8:Spt:689.0,633.1] || -> equal(h(e11),e20)**. % 0.18/0.47 698[8:Rew:56.0,550.0,691.0,550.0] || -> equal(h(e13),e23)**. % 0.18/0.47 699[8:Rew:698.0,36.0] || -> equal(j(e23),e13)**. % 0.18/0.47 700[8:Rew:529.0,699.0] || -> equal(e13,e12)**. % 0.18/0.47 701[8:MRR:700.0,6.0] || -> . % 0.18/0.47 713[5:Spt:701.0,528.0,529.0] || equal(j(e23),e12)** -> . % 0.18/0.47 714[5:Spt:701.0,528.1,528.2] || -> equal(j(e23),e11)** equal(j(e23),e10). % 0.18/0.47 715[6:Spt:714.0] || -> equal(j(e23),e11)**. % 0.18/0.47 717[6:Rew:715.0,32.0] || -> equal(h(e11),e23)**. % 0.18/0.47 723[6:Rew:715.0,111.0] || -> equal(op1(e11,j(e21)),j(e22))**. % 0.18/0.47 725[6:Rew:715.0,114.0] || -> equal(op1(j(e22),j(e22)),e11)**. % 0.18/0.47 726[6:Rew:715.0,117.0] || -> equal(op1(j(e21),e11),j(e22))**. % 0.18/0.47 735[6:Rew:717.0,129.0] || -> equal(op2(h(e12),h(e13)),e23)**. % 0.18/0.47 737[6:Rew:717.0,126.0] || -> equal(op2(h(e13),h(e12)),e23)**. % 0.18/0.47 739[7:Spt:106.0] || -> equal(j(e21),e13)**. % 0.18/0.47 740[7:Rew:739.0,30.0] || -> equal(h(e13),e21)**. % 0.18/0.47 746[7:Rew:739.0,723.0] || -> equal(op1(e11,e13),j(e22))**. % 0.18/0.47 759[7:Rew:740.0,737.0] || -> equal(op2(e21,h(e12)),e23)**. % 0.18/0.47 764[7:Rew:44.0,746.0] || -> equal(j(e22),e12)**. % 0.18/0.47 765[7:Rew:764.0,31.0] || -> equal(h(e12),e22)**. % 0.18/0.47 792[7:Rew:59.0,759.0,765.0,759.0] || -> equal(e23,e20)**. % 0.18/0.47 793[7:MRR:792.0,9.0] || -> . % 0.18/0.47 794[7:Spt:793.0,106.0,739.0] || equal(j(e21),e13)** -> . % 0.18/0.47 795[7:Spt:793.0,106.1,106.2,106.3] || -> equal(j(e21),e12)** equal(j(e21),e11) equal(j(e21),e10). % 0.18/0.47 796[8:Spt:795.0] || -> equal(j(e21),e12)**. % 0.18/0.47 797[8:Rew:796.0,30.0] || -> equal(h(e12),e21)**. % 0.18/0.47 800[8:Rew:796.0,726.0] || -> equal(op1(e12,e11),j(e22))**. % 0.18/0.47 811[8:Rew:797.0,735.0] || -> equal(op2(e21,h(e13)),e23)**. % 0.18/0.47 822[8:Rew:46.0,800.0] || -> equal(j(e22),e13)**. % 0.18/0.47 823[8:Rew:822.0,31.0] || -> equal(h(e13),e22)**. % 0.18/0.47 845[8:Rew:59.0,811.0,823.0,811.0] || -> equal(e23,e20)**. % 0.18/0.47 846[8:MRR:845.0,9.0] || -> . % 0.18/0.47 850[8:Spt:846.0,795.0,796.0] || equal(j(e21),e12)** -> . % 0.18/0.47 851[8:Spt:846.0,795.1,795.2] || -> equal(j(e21),e11)** equal(j(e21),e10). % 0.18/0.47 852[9:Spt:851.0] || -> equal(j(e21),e11)**. % 0.18/0.47 859[9:Rew:852.0,314.0] || -> equal(op1(e11,j(e22)),e10)**. % 0.18/0.47 861[9:Rew:852.0,723.0] || -> equal(op1(e11,e11),j(e22))**. % 0.18/0.47 871[9:Rew:42.0,861.0] || -> equal(j(e22),e10)**. % 0.18/0.47 877[9:Rew:871.0,859.0] || -> equal(op1(e11,e10),e10)**. % 0.18/0.47 884[9:Rew:41.0,877.0] || -> equal(e11,e10)**. % 0.18/0.47 885[9:MRR:884.0,1.0] || -> . % 0.18/0.47 888[9:Spt:885.0,851.0,852.0] || equal(j(e21),e11)** -> . % 0.18/0.47 889[9:Spt:885.0,851.1] || -> equal(j(e21),e10)**. % 0.18/0.47 897[9:Rew:38.0,726.0,889.0,726.0] || -> equal(j(e22),e11)**. % 0.18/0.47 910[9:Rew:42.0,725.0,897.0,725.0] || -> equal(e11,e10)**. % 0.18/0.47 911[9:MRR:910.0,1.0] || -> . % 0.18/0.47 914[6:Spt:911.0,714.0,715.0] || equal(j(e23),e11)** -> . % 0.18/0.47 915[6:Spt:911.0,714.1] || -> equal(j(e23),e10)**. % 0.18/0.47 925[6:Rew:313.0,117.0,915.0,117.0] || -> equal(j(e22),j(e21))**. % 0.18/0.47 926[6:Rew:925.0,31.0] || -> equal(h(j(e21)),e22)**. % 0.18/0.47 931[6:Rew:30.0,926.0] || -> equal(e22,e21)**. % 0.18/0.47 932[6:MRR:931.0,10.0] || -> . % 0.18/0.47 % SZS output end Refutation % 0.18/0.47 Formulae used in the proof : ax1 ax2 co1 ax4 ax5 % 0.18/0.47 %------------------------------------------------------------------------------