%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ALG180+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:49 EDT 2022 % Result : Theorem 0.18s 0.48s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ALG180+1 : TPTP v8.1.0. Released v2.7.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n019.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 : Tue Jun 7 22:13:40 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.48 % 0.18/0.48 SPASS V 3.9 % 0.18/0.48 SPASS beiseite: Proof found. % 0.18/0.48 % SZS status Theorem % 0.18/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.48 SPASS derived 457 clauses, backtracked 464 clauses, performed 8 splits and kept 909 clauses. % 0.18/0.48 SPASS allocated 85634 KBytes. % 0.18/0.48 SPASS spent 0:00:00.14 on the problem. % 0.18/0.48 0:00:00.04 for the input. % 0.18/0.48 0:00:00.03 for the FLOTTER CNF translation. % 0.18/0.48 0:00:00.00 for inferences. % 0.18/0.48 0:00:00.00 for the backtracking. % 0.18/0.48 0:00:00.04 for the reduction. % 0.18/0.48 % 0.18/0.48 % 0.18/0.48 Here is a proof with depth 4, length 189 : % 0.18/0.48 % SZS output start Refutation % 0.18/0.48 1[0:Inp] || equal(e11,e10)** -> . % 0.18/0.48 8[0:Inp] || equal(e13,e12)** -> . % 0.18/0.48 11[0:Inp] || equal(e21,e20)** -> . % 0.18/0.48 12[0:Inp] || equal(e22,e20)** -> . % 0.18/0.48 15[0:Inp] || equal(e22,e21)** -> . % 0.18/0.48 16[0:Inp] || equal(e23,e21)** -> . % 0.18/0.48 19[0:Inp] || equal(e24,e22)** -> . % 0.18/0.48 47[0:Inp] || -> equal(h(j(e21)),e21)**. % 0.18/0.48 48[0:Inp] || -> equal(h(j(e22)),e22)**. % 0.18/0.48 50[0:Inp] || -> equal(h(j(e24)),e24)**. % 0.18/0.48 51[0:Inp] || -> equal(j(h(e10)),e10)**. % 0.18/0.48 53[0:Inp] || -> equal(j(h(e12)),e12)**. % 0.18/0.48 54[0:Inp] || -> equal(j(h(e13)),e13)**. % 0.18/0.48 56[0:Inp] || -> equal(op1(e10,e10),e13)**. % 0.18/0.48 58[0:Inp] || -> equal(op1(e10,e12),e10)**. % 0.18/0.48 59[0:Inp] || -> equal(op1(e10,e13),e11)**. % 0.18/0.48 66[0:Inp] || -> equal(op1(e12,e10),e11)**. % 0.18/0.48 68[0:Inp] || -> equal(op1(e12,e12),e12)**. % 0.18/0.48 72[0:Inp] || -> equal(op1(e13,e11),e11)**. % 0.18/0.48 81[0:Inp] || -> equal(op2(e20,e20),e24)**. % 0.18/0.48 83[0:Inp] || -> equal(op2(e20,e22),e20)**. % 0.18/0.48 84[0:Inp] || -> equal(op2(e20,e23),e21)**. % 0.18/0.48 85[0:Inp] || -> equal(op2(e20,e24),e23)**. % 0.18/0.48 86[0:Inp] || -> equal(op2(e21,e20),e20)**. % 0.18/0.48 87[0:Inp] || -> equal(op2(e21,e21),e21)**. % 0.18/0.48 91[0:Inp] || -> equal(op2(e22,e20),e21)**. % 0.18/0.48 92[0:Inp] || -> equal(op2(e22,e21),e24)**. % 0.18/0.48 93[0:Inp] || -> equal(op2(e22,e22),e23)**. % 0.18/0.48 94[0:Inp] || -> equal(op2(e22,e23),e20)**. % 0.18/0.48 96[0:Inp] || -> equal(op2(e23,e20),e23)**. % 0.18/0.48 97[0:Inp] || -> equal(op2(e23,e21),e20)**. % 0.18/0.48 98[0:Inp] || -> equal(op2(e23,e22),e24)**. % 0.18/0.48 99[0:Inp] || -> equal(op2(e23,e23),e22)**. % 0.18/0.48 100[0:Inp] || -> equal(op2(e23,e24),e21)**. % 0.18/0.48 101[0:Inp] || -> equal(op2(e24,e20),e22)**. % 0.18/0.48 102[0:Inp] || -> equal(op2(e24,e21),e23)**. % 0.18/0.48 103[0:Inp] || -> equal(op2(e24,e22),e21)**. % 0.18/0.48 104[0:Inp] || -> equal(op2(e24,e23),e24)**. % 0.18/0.48 105[0:Inp] || -> equal(op2(e24,e24),e20)**. % 0.18/0.48 106[0:Inp] || -> equal(op2(h(e10),h(e10)),h(op1(e10,e10)))**. % 0.18/0.48 116[0:Inp] || -> equal(op2(h(e12),h(e10)),h(op1(e12,e10)))**. % 0.18/0.48 122[0:Inp] || -> equal(op2(h(e13),h(e11)),h(op1(e13,e11)))**. % 0.18/0.48 131[0:Inp] || -> equal(op1(j(e20),j(e20)),j(op2(e20,e20)))**. % 0.18/0.48 133[0:Inp] || -> equal(op1(j(e20),j(e22)),j(op2(e20,e22)))**. % 0.18/0.48 134[0:Inp] || -> equal(op1(j(e20),j(e23)),j(op2(e20,e23)))**. % 0.18/0.48 135[0:Inp] || -> equal(op1(j(e20),j(e24)),j(op2(e20,e24)))**. % 0.18/0.48 141[0:Inp] || -> equal(op1(j(e22),j(e20)),j(op2(e22,e20)))**. % 0.18/0.48 142[0:Inp] || -> equal(op1(j(e22),j(e21)),j(op2(e22,e21)))**. % 0.18/0.48 143[0:Inp] || -> equal(op1(j(e22),j(e22)),j(op2(e22,e22)))**. % 0.18/0.48 144[0:Inp] || -> equal(op1(j(e22),j(e23)),j(op2(e22,e23)))**. % 0.18/0.48 146[0:Inp] || -> equal(op1(j(e23),j(e20)),j(op2(e23,e20)))**. % 0.18/0.48 147[0:Inp] || -> equal(op1(j(e23),j(e21)),j(op2(e23,e21)))**. % 0.18/0.48 148[0:Inp] || -> equal(op1(j(e23),j(e22)),j(op2(e23,e22)))**. % 0.18/0.48 149[0:Inp] || -> equal(op1(j(e23),j(e23)),j(op2(e23,e23)))**. % 0.18/0.48 150[0:Inp] || -> equal(op1(j(e23),j(e24)),j(op2(e23,e24)))**. % 0.18/0.48 152[0:Inp] || -> equal(op1(j(e24),j(e21)),j(op2(e24,e21)))**. % 0.18/0.48 153[0:Inp] || -> equal(op1(j(e24),j(e22)),j(op2(e24,e22)))**. % 0.18/0.48 154[0:Inp] || -> equal(op1(j(e24),j(e23)),j(op2(e24,e23)))**. % 0.18/0.48 155[0:Inp] || -> equal(op1(j(e24),j(e24)),j(op2(e24,e24)))**. % 0.18/0.48 163[0:Inp] || -> equal(h(e12),e24)** equal(h(e12),e23) equal(h(e12),e22) equal(h(e12),e21) equal(h(e12),e20). % 0.18/0.48 165[0:Inp] || -> equal(h(e10),e24)** equal(h(e10),e23) equal(h(e10),e22) equal(h(e10),e21) equal(h(e10),e20). % 0.18/0.48 166[0:Rew:105.0,155.0] || -> equal(op1(j(e24),j(e24)),j(e20))**. % 0.18/0.48 167[0:Rew:104.0,154.0] || -> equal(op1(j(e24),j(e23)),j(e24))**. % 0.18/0.48 168[0:Rew:103.0,153.0] || -> equal(op1(j(e24),j(e22)),j(e21))**. % 0.18/0.48 169[0:Rew:102.0,152.0] || -> equal(op1(j(e24),j(e21)),j(e23))**. % 0.18/0.48 171[0:Rew:100.0,150.0] || -> equal(op1(j(e23),j(e24)),j(e21))**. % 0.18/0.48 172[0:Rew:99.0,149.0] || -> equal(op1(j(e23),j(e23)),j(e22))**. % 0.18/0.48 173[0:Rew:98.0,148.0] || -> equal(op1(j(e23),j(e22)),j(e24))**. % 0.18/0.48 174[0:Rew:97.0,147.0] || -> equal(op1(j(e23),j(e21)),j(e20))**. % 0.18/0.48 175[0:Rew:96.0,146.0] || -> equal(op1(j(e23),j(e20)),j(e23))**. % 0.18/0.48 177[0:Rew:94.0,144.0] || -> equal(op1(j(e22),j(e23)),j(e20))**. % 0.18/0.48 178[0:Rew:93.0,143.0] || -> equal(op1(j(e22),j(e22)),j(e23))**. % 0.18/0.48 179[0:Rew:92.0,142.0] || -> equal(op1(j(e22),j(e21)),j(e24))**. % 0.18/0.48 180[0:Rew:91.0,141.0] || -> equal(op1(j(e22),j(e20)),j(e21))**. % 0.18/0.48 186[0:Rew:85.0,135.0] || -> equal(op1(j(e20),j(e24)),j(e23))**. % 0.18/0.48 187[0:Rew:84.0,134.0] || -> equal(op1(j(e20),j(e23)),j(e21))**. % 0.18/0.48 188[0:Rew:83.0,133.0] || -> equal(op1(j(e20),j(e22)),j(e20))**. % 0.18/0.48 190[0:Rew:81.0,131.0] || -> equal(op1(j(e20),j(e20)),j(e24))**. % 0.18/0.48 199[0:Rew:72.0,122.0] || -> equal(op2(h(e13),h(e11)),h(e11))**. % 0.18/0.48 205[0:Rew:66.0,116.0] || -> equal(op2(h(e12),h(e10)),h(e11))**. % 0.18/0.48 215[0:Rew:56.0,106.0] || -> equal(op2(h(e10),h(e10)),h(e13))**. % 0.18/0.48 216[1:Spt:163.0] || -> equal(h(e12),e24)**. % 0.18/0.48 217[1:Rew:216.0,53.0] || -> equal(j(e24),e12)**. % 0.18/0.48 232[1:Rew:217.0,166.0] || -> equal(op1(e12,e12),j(e20))**. % 0.18/0.48 234[1:Rew:217.0,168.0] || -> equal(op1(e12,j(e22)),j(e21))**. % 0.18/0.48 235[1:Rew:217.0,169.0] || -> equal(op1(e12,j(e21)),j(e23))**. % 0.18/0.48 246[1:Rew:68.0,232.0] || -> equal(j(e20),e12)**. % 0.18/0.48 254[1:Rew:246.0,188.0] || -> equal(op1(e12,j(e22)),e12)**. % 0.18/0.48 258[1:Rew:254.0,234.0] || -> equal(j(e21),e12)**. % 0.18/0.48 266[1:Rew:68.0,235.0,258.0,235.0] || -> equal(j(e23),e12)**. % 0.18/0.48 268[1:Rew:266.0,172.0] || -> equal(op1(e12,e12),j(e22))**. % 0.18/0.48 273[1:Rew:68.0,268.0] || -> equal(j(e22),e12)**. % 0.18/0.48 274[1:Rew:273.0,48.0] || -> equal(h(e12),e22)**. % 0.18/0.48 276[1:Rew:216.0,274.0] || -> equal(e24,e22)**. % 0.18/0.48 277[1:MRR:276.0,19.0] || -> . % 0.18/0.48 294[1:Spt:277.0,163.0,216.0] || equal(h(e12),e24)** -> . % 0.18/0.48 295[1:Spt:277.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.18/0.48 296[2:Spt:295.0] || -> equal(h(e12),e23)**. % 0.18/0.48 297[2:Rew:296.0,53.0] || -> equal(j(e23),e12)**. % 0.18/0.48 314[2:Rew:297.0,173.0] || -> equal(op1(e12,j(e22)),j(e24))**. % 0.18/0.48 315[2:Rew:297.0,171.0] || -> equal(op1(e12,j(e24)),j(e21))**. % 0.18/0.48 324[2:Rew:297.0,172.0] || -> equal(op1(e12,e12),j(e22))**. % 0.18/0.48 327[2:Rew:68.0,324.0] || -> equal(j(e22),e12)**. % 0.18/0.48 339[2:Rew:68.0,314.0,327.0,314.0] || -> equal(j(e24),e12)**. % 0.18/0.48 355[2:Rew:68.0,315.0,339.0,315.0] || -> equal(j(e21),e12)**. % 0.18/0.48 356[2:Rew:355.0,47.0] || -> equal(h(e12),e21)**. % 0.18/0.48 359[2:Rew:296.0,356.0] || -> equal(e23,e21)**. % 0.18/0.48 360[2:MRR:359.0,16.0] || -> . % 0.18/0.48 374[2:Spt:360.0,295.0,296.0] || equal(h(e12),e23)** -> . % 0.18/0.48 375[2:Spt:360.0,295.1,295.2,295.3] || -> equal(h(e12),e22)** equal(h(e12),e21) equal(h(e12),e20). % 0.18/0.48 376[3:Spt:375.0] || -> equal(h(e12),e22)**. % 0.18/0.48 378[3:Rew:376.0,53.0] || -> equal(j(e22),e12)**. % 0.18/0.48 395[3:Rew:378.0,178.0] || -> equal(op1(e12,e12),j(e23))**. % 0.18/0.48 396[3:Rew:378.0,177.0] || -> equal(op1(e12,j(e23)),j(e20))**. % 0.18/0.48 399[3:Rew:378.0,180.0] || -> equal(op1(e12,j(e20)),j(e21))**. % 0.18/0.48 408[3:Rew:68.0,395.0] || -> equal(j(e23),e12)**. % 0.18/0.48 421[3:Rew:68.0,396.0,408.0,396.0] || -> equal(j(e20),e12)**. % 0.18/0.48 436[3:Rew:68.0,399.0,421.0,399.0] || -> equal(j(e21),e12)**. % 0.18/0.48 437[3:Rew:436.0,47.0] || -> equal(h(e12),e21)**. % 0.18/0.48 440[3:Rew:376.0,437.0] || -> equal(e22,e21)**. % 0.18/0.48 441[3:MRR:440.0,15.0] || -> . % 0.18/0.48 454[3:Spt:441.0,375.0,376.0] || equal(h(e12),e22)** -> . % 0.18/0.48 455[3:Spt:441.0,375.1,375.2] || -> equal(h(e12),e21)** equal(h(e12),e20). % 0.18/0.48 456[4:Spt:455.0] || -> equal(h(e12),e21)**. % 0.18/0.48 458[4:Rew:456.0,53.0] || -> equal(j(e21),e12)**. % 0.18/0.48 465[4:Rew:456.0,205.0] || -> equal(op2(e21,h(e10)),h(e11))**. % 0.18/0.48 475[4:Rew:458.0,179.0] || -> equal(op1(j(e22),e12),j(e24))**. % 0.18/0.48 481[4:Rew:458.0,169.0] || -> equal(op1(j(e24),e12),j(e23))**. % 0.18/0.48 483[4:Rew:458.0,174.0] || -> equal(op1(j(e23),e12),j(e20))**. % 0.18/0.48 489[5:Spt:165.0] || -> equal(h(e10),e24)**. % 0.18/0.48 490[5:Rew:489.0,51.0] || -> equal(j(e24),e10)**. % 0.18/0.48 497[5:Rew:489.0,215.0] || -> equal(op2(e24,e24),h(e13))**. % 0.18/0.48 514[5:Rew:490.0,481.0] || -> equal(op1(e10,e12),j(e23))**. % 0.18/0.48 520[5:Rew:105.0,497.0] || -> equal(h(e13),e20)**. % 0.18/0.48 521[5:Rew:520.0,54.0] || -> equal(j(e20),e13)**. % 0.18/0.48 533[5:Rew:521.0,175.0] || -> equal(op1(j(e23),e13),j(e23))**. % 0.18/0.48 559[5:Rew:58.0,514.0] || -> equal(j(e23),e10)**. % 0.18/0.48 644[5:Rew:59.0,533.0,559.0,533.0] || -> equal(e11,e10)**. % 0.18/0.48 645[5:MRR:644.0,1.0] || -> . % 0.18/0.49 648[5:Spt:645.0,165.0,489.0] || equal(h(e10),e24)** -> . % 0.18/0.49 649[5:Spt:645.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.18/0.49 650[6:Spt:649.0] || -> equal(h(e10),e23)**. % 0.18/0.49 651[6:Rew:650.0,51.0] || -> equal(j(e23),e10)**. % 0.18/0.49 658[6:Rew:650.0,215.0] || -> equal(op2(e23,e23),h(e13))**. % 0.18/0.49 668[6:Rew:651.0,483.0] || -> equal(op1(e10,e12),j(e20))**. % 0.18/0.49 697[6:Rew:99.0,658.0] || -> equal(h(e13),e22)**. % 0.18/0.49 698[6:Rew:697.0,54.0] || -> equal(j(e22),e13)**. % 0.18/0.49 711[6:Rew:698.0,188.0] || -> equal(op1(j(e20),e13),j(e20))**. % 0.18/0.49 718[6:Rew:58.0,668.0] || -> equal(j(e20),e10)**. % 0.18/0.49 802[6:Rew:59.0,711.0,718.0,711.0] || -> equal(e11,e10)**. % 0.18/0.49 803[6:MRR:802.0,1.0] || -> . % 0.18/0.49 805[6:Spt:803.0,649.0,650.0] || equal(h(e10),e23)** -> . % 0.18/0.49 806[6:Spt:803.0,649.1,649.2,649.3] || -> equal(h(e10),e22)** equal(h(e10),e21) equal(h(e10),e20). % 0.18/0.49 807[7:Spt:806.0] || -> equal(h(e10),e22)**. % 0.18/0.49 809[7:Rew:807.0,51.0] || -> equal(j(e22),e10)**. % 0.18/0.49 822[7:Rew:807.0,215.0] || -> equal(op2(e22,e22),h(e13))**. % 0.18/0.49 827[7:Rew:809.0,475.0] || -> equal(op1(e10,e12),j(e24))**. % 0.18/0.49 858[7:Rew:93.0,822.0] || -> equal(h(e13),e23)**. % 0.18/0.49 859[7:Rew:858.0,54.0] || -> equal(j(e23),e13)**. % 0.18/0.49 872[7:Rew:859.0,167.0] || -> equal(op1(j(e24),e13),j(e24))**. % 0.18/0.49 877[7:Rew:58.0,827.0] || -> equal(j(e24),e10)**. % 0.18/0.49 961[7:Rew:59.0,872.0,877.0,872.0] || -> equal(e11,e10)**. % 0.18/0.49 962[7:MRR:961.0,1.0] || -> . % 0.18/0.49 964[7:Spt:962.0,806.0,807.0] || equal(h(e10),e22)** -> . % 0.18/0.49 965[7:Spt:962.0,806.1,806.2] || -> equal(h(e10),e21)** equal(h(e10),e20). % 0.18/0.49 966[8:Spt:965.0] || -> equal(h(e10),e21)**. % 0.18/0.49 976[8:Rew:966.0,215.0] || -> equal(op2(e21,e21),h(e13))**. % 0.18/0.49 1006[8:Rew:87.0,976.0] || -> equal(h(e13),e21)**. % 0.18/0.49 1007[8:Rew:1006.0,54.0] || -> equal(j(e21),e13)**. % 0.18/0.49 1009[8:Rew:458.0,1007.0] || -> equal(e13,e12)**. % 0.18/0.49 1010[8:MRR:1009.0,8.0] || -> . % 0.18/0.49 1026[8:Spt:1010.0,965.0,966.0] || equal(h(e10),e21)** -> . % 0.18/0.49 1027[8:Spt:1010.0,965.1] || -> equal(h(e10),e20)**. % 0.18/0.49 1030[8:Rew:1027.0,51.0] || -> equal(j(e20),e10)**. % 0.18/0.49 1043[8:Rew:1030.0,190.0] || -> equal(op1(e10,e10),j(e24))**. % 0.18/0.49 1066[8:Rew:56.0,1043.0] || -> equal(j(e24),e13)**. % 0.18/0.49 1067[8:Rew:1066.0,50.0] || -> equal(h(e13),e24)**. % 0.18/0.49 1102[8:Rew:86.0,465.0,1027.0,465.0] || -> equal(h(e11),e20)**. % 0.18/0.49 1164[8:Rew:101.0,199.0,1067.0,199.0,1102.0,199.0] || -> equal(e22,e20)**. % 0.18/0.49 1165[8:MRR:1164.0,12.0] || -> . % 0.18/0.49 1166[4:Spt:1165.0,455.0,456.0] || equal(h(e12),e21)** -> . % 0.18/0.49 1167[4:Spt:1165.0,455.1] || -> equal(h(e12),e20)**. % 0.18/0.49 1170[4:Rew:1167.0,53.0] || -> equal(j(e20),e12)**. % 0.18/0.49 1174[4:Rew:68.0,190.0,1170.0,190.0] || -> equal(j(e24),e12)**. % 0.18/0.49 1180[4:Rew:68.0,186.0,1170.0,186.0,1174.0,186.0] || -> equal(j(e23),e12)**. % 0.18/0.49 1216[4:Rew:68.0,187.0,1170.0,187.0,1180.0,187.0] || -> equal(j(e21),e12)**. % 0.18/0.49 1217[4:Rew:1216.0,47.0] || -> equal(h(e12),e21)**. % 0.18/0.49 1221[4:Rew:1167.0,1217.0] || -> equal(e21,e20)**. % 0.18/0.49 1222[4:MRR:1221.0,11.0] || -> . % 0.18/0.49 % SZS output end Refutation % 0.18/0.49 Formulae used in the proof : ax1 ax2 co1 ax4 ax5 % 0.18/0.49 %------------------------------------------------------------------------------