%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM542+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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 : Mon Jul 18 14:27:19 EDT 2022 % Result : Theorem 0.66s 0.84s % Output : Refutation 0.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM542+2 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n015.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Thu Jul 7 13:23:34 EDT 2022 % 0.12/0.34 % CPUTime : % 0.66/0.84 % 0.66/0.84 SPASS V 3.9 % 0.66/0.84 SPASS beiseite: Proof found. % 0.66/0.84 % SZS status Theorem % 0.66/0.84 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.66/0.84 SPASS derived 1841 clauses, backtracked 345 clauses, performed 18 splits and kept 1202 clauses. % 0.66/0.84 SPASS allocated 99526 KBytes. % 0.66/0.84 SPASS spent 0:00:00.49 on the problem. % 0.66/0.84 0:00:00.03 for the input. % 0.66/0.84 0:00:00.12 for the FLOTTER CNF translation. % 0.66/0.84 0:00:00.03 for inferences. % 0.66/0.84 0:00:00.01 for the backtracking. % 0.66/0.84 0:00:00.27 for the reduction. % 0.66/0.84 % 0.66/0.84 % 0.66/0.84 Here is a proof with depth 7, length 111 : % 0.66/0.84 % SZS output start Refutation % 0.66/0.84 2[0:Inp] || -> aSet0(szNzAzT0)*. % 0.66/0.84 3[0:Inp] || -> isCountable0(szNzAzT0)*. % 0.66/0.84 5[0:Inp] || -> aElementOf0(xm,szNzAzT0)*. % 0.66/0.84 6[0:Inp] || -> aElementOf0(xn,szNzAzT0)*. % 0.66/0.84 7[0:Inp] || -> SkC0 sdtlseqdt0(xm,xn)*. % 0.66/0.84 8[0:Inp] || -> aSet0(slbdtrb0(xm))* SkC0. % 0.66/0.84 9[0:Inp] || -> aSet0(slbdtrb0(xn))* SkC0. % 0.66/0.84 12[0:Inp] || SkC0 -> aSet0(slbdtrb0(xm))*. % 0.66/0.84 13[0:Inp] || SkC0 -> aSet0(slbdtrb0(xn))*. % 0.66/0.84 14[0:Inp] || -> SkC0 aElementOf0(skc1,slbdtrb0(xm))*. % 0.66/0.84 15[0:Inp] || SkC0 sdtlseqdt0(xm,xn)* -> . % 0.66/0.84 16[0:Inp] || aElementOf0(skc1,slbdtrb0(xn))* -> SkC0. % 0.66/0.84 19[0:Inp] aSet0(u) || -> aSubsetOf0(u,u)*. % 0.66/0.84 27[0:Inp] || aElementOf0(u,szNzAzT0) -> isFinite0(slbdtrb0(u))*. % 0.66/0.84 28[0:Inp] || aElementOf0(u,v)* equal(v,slcrc0) -> . % 0.66/0.84 30[0:Inp] || aElementOf0(u,szNzAzT0) -> aElementOf0(szszuzczcdt0(u),szNzAzT0)*. % 0.66/0.84 31[0:Inp] || aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,szszuzczcdt0(u))*. % 0.66/0.84 33[0:Inp] || aElementOf0(u,slbdtrb0(xm))* -> aElementOf0(u,szNzAzT0) SkC0. % 0.66/0.84 35[0:Inp] aSet0(u) || aElementOf0(v,u)* -> aElement0(v). % 0.66/0.84 40[0:Inp] || aElementOf0(u,szNzAzT0)* equal(szszuzczcdt0(u),u) -> . % 0.66/0.84 42[0:Inp] || aElementOf0(u,slbdtrb0(xm))* SkC0 -> aElementOf0(u,szNzAzT0). % 0.66/0.84 44[0:Inp] || aElementOf0(u,slbdtrb0(xm)) -> sdtlseqdt0(szszuzczcdt0(u),xm)* SkC0. % 0.66/0.84 45[0:Inp] || aElementOf0(u,slbdtrb0(xn)) -> sdtlseqdt0(szszuzczcdt0(u),xn)* SkC0. % 0.66/0.84 46[0:Inp] aSet0(u) || -> equal(u,slcrc0) aElementOf0(skf9(u),u)*. % 0.66/0.84 49[0:Inp] || aElementOf0(u,slbdtrb0(xm)) SkC0 -> sdtlseqdt0(szszuzczcdt0(u),xm)*. % 0.66/0.84 50[0:Inp] || aElementOf0(u,slbdtrb0(xn)) SkC0 -> sdtlseqdt0(szszuzczcdt0(u),xn)*. % 0.66/0.84 51[0:Inp] || SkC0 aElementOf0(u,slbdtrb0(xm)) -> aElementOf0(u,slbdtrb0(xn))*. % 0.66/0.84 58[0:Inp] isFinite0(u) aSet0(u) || aSubsetOf0(v,u)* -> isFinite0(v). % 0.66/0.84 64[0:Inp] || aElementOf0(u,szNzAzT0) sdtlseqdt0(szszuzczcdt0(u),xm)* -> aElementOf0(u,slbdtrb0(xm)) SkC0. % 0.66/0.84 65[0:Inp] || aElementOf0(u,szNzAzT0) sdtlseqdt0(szszuzczcdt0(u),xn)* -> aElementOf0(u,slbdtrb0(xn)) SkC0. % 0.66/0.84 66[0:Inp] aSet0(u) || aElementOf0(v,w)*+ aSubsetOf0(w,u)* -> aElementOf0(v,u)*. % 0.66/0.84 67[0:Inp] aSet0(u) aSet0(v) || -> aSubsetOf0(v,u)* aElementOf0(skf10(v,w),v)*. % 0.66/0.84 72[0:Inp] || aElementOf0(u,szNzAzT0) sdtlseqdt0(szszuzczcdt0(u),xm)* SkC0 -> aElementOf0(u,slbdtrb0(xm)). % 0.66/0.84 73[0:Inp] || aElementOf0(u,szNzAzT0) sdtlseqdt0(szszuzczcdt0(u),xn)* SkC0 -> aElementOf0(u,slbdtrb0(xn)). % 0.66/0.84 75[0:Inp] || aElementOf0(u,szNzAzT0) aElementOf0(v,szNzAzT0) -> sdtlseqdt0(v,u) sdtlseqdt0(szszuzczcdt0(u),v)*. % 0.66/0.84 89[0:Inp] || sdtlseqdt0(u,v)*+ sdtlseqdt0(v,u)* aElementOf0(u,szNzAzT0) aElementOf0(v,szNzAzT0) -> equal(v,u). % 0.66/0.84 107[0:Inp] || sdtlseqdt0(u,v)*+ sdtlseqdt0(w,u)* aElementOf0(v,szNzAzT0) aElementOf0(u,szNzAzT0) aElementOf0(w,szNzAzT0) -> sdtlseqdt0(w,v)*. % 0.66/0.84 115[0:MRR:13.0,9.1] || -> aSet0(slbdtrb0(xn))*. % 0.66/0.84 116[0:MRR:12.0,8.1] || -> aSet0(slbdtrb0(xm))*. % 0.66/0.84 118[0:MRR:42.1,33.2] || aElementOf0(u,slbdtrb0(xm))* -> aElementOf0(u,szNzAzT0). % 0.66/0.84 120[0:MRR:50.1,45.2] || aElementOf0(u,slbdtrb0(xn)) -> sdtlseqdt0(szszuzczcdt0(u),xn)*. % 0.66/0.84 121[0:MRR:49.1,44.2] || aElementOf0(u,slbdtrb0(xm)) -> sdtlseqdt0(szszuzczcdt0(u),xm)*. % 0.66/0.84 122[0:MRR:73.2,65.3] || aElementOf0(u,szNzAzT0) sdtlseqdt0(szszuzczcdt0(u),xn)* -> aElementOf0(u,slbdtrb0(xn)). % 0.66/0.84 123[0:MRR:72.2,64.3] || aElementOf0(u,szNzAzT0) sdtlseqdt0(szszuzczcdt0(u),xm)* -> aElementOf0(u,slbdtrb0(xm)). % 0.66/0.84 157[0:Res:115.0,58.0] isFinite0(slbdtrb0(xn)) || aSubsetOf0(u,slbdtrb0(xn))* -> isFinite0(u). % 0.66/0.84 165[0:Res:115.0,19.0] || -> aSubsetOf0(slbdtrb0(xn),slbdtrb0(xn))*. % 0.66/0.84 173[0:Res:115.0,67.1] aSet0(u) || -> aSubsetOf0(u,slbdtrb0(xn)) aElementOf0(skf10(u,v),u)*. % 0.66/0.84 207[0:Res:116.0,35.0] || aElementOf0(u,slbdtrb0(xm))* -> aElement0(u). % 0.66/0.84 227[0:Res:6.0,123.0] || sdtlseqdt0(szszuzczcdt0(xn),xm)* -> aElementOf0(xn,slbdtrb0(xm)). % 0.66/0.84 231[1:Spt:51.1,51.2] || aElementOf0(u,slbdtrb0(xm)) -> aElementOf0(u,slbdtrb0(xn))*. % 0.66/0.84 232[2:Spt:7.0] || -> SkC0*. % 0.66/0.84 233[2:MRR:15.0,232.0] || sdtlseqdt0(xm,xn)* -> . % 0.66/0.84 304[0:Res:46.2,207.0] aSet0(slbdtrb0(xm)) || -> equal(slbdtrb0(xm),slcrc0) aElement0(skf9(slbdtrb0(xm)))*. % 0.66/0.84 314[0:SSi:304.0,116.0] || -> equal(slbdtrb0(xm),slcrc0) aElement0(skf9(slbdtrb0(xm)))*. % 0.66/0.84 326[3:Spt:314.0] || -> equal(slbdtrb0(xm),slcrc0)**. % 0.66/0.84 336[3:Rew:326.0,227.1] || sdtlseqdt0(szszuzczcdt0(xn),xm)* -> aElementOf0(xn,slcrc0). % 0.66/0.84 633[0:SoR:157.0,27.1] || aSubsetOf0(u,slbdtrb0(xn))* aElementOf0(xn,szNzAzT0) -> isFinite0(u). % 0.66/0.84 634[0:MRR:633.1,6.0] || aSubsetOf0(u,slbdtrb0(xn))* -> isFinite0(u). % 0.66/0.84 637[0:Res:165.0,634.0] || -> isFinite0(slbdtrb0(xn))*. % 0.66/0.84 764[0:Res:173.2,35.1] aSet0(u) aSet0(u) || -> aSubsetOf0(u,slbdtrb0(xn))* aElement0(skf10(u,v))*. % 0.66/0.84 766[0:Obv:764.0] aSet0(u) || -> aSubsetOf0(u,slbdtrb0(xn))* aElement0(skf10(u,v))*. % 0.66/0.84 875[0:Res:6.0,66.1] aSet0(u) || aSubsetOf0(szNzAzT0,u)* -> aElementOf0(xn,u). % 0.66/0.84 897[0:Res:766.1,875.1] aSet0(szNzAzT0) aSet0(slbdtrb0(xn)) || -> aElement0(skf10(szNzAzT0,u))* aElementOf0(xn,slbdtrb0(xn))*. % 0.66/0.84 901[0:SSi:897.1,897.0,115.0,637.0,3.0,2.0] || -> aElement0(skf10(szNzAzT0,u))* aElementOf0(xn,slbdtrb0(xn))*. % 0.66/0.84 1051[0:Res:75.3,122.1] || aElementOf0(u,szNzAzT0) aElementOf0(xn,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(xn,u) aElementOf0(u,slbdtrb0(xn))*. % 0.66/0.84 1053[3:Res:75.3,336.0] || aElementOf0(xn,szNzAzT0) aElementOf0(xm,szNzAzT0) -> sdtlseqdt0(xm,xn)* aElementOf0(xn,slcrc0). % 0.66/0.84 1058[3:MRR:1053.0,1053.1,1053.2,6.0,5.0,233.0] || -> aElementOf0(xn,slcrc0)*. % 0.66/0.84 1064[0:Obv:1051.0] || aElementOf0(xn,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(xn,u) aElementOf0(u,slbdtrb0(xn))*. % 0.66/0.84 1065[0:MRR:1064.0,6.0] || aElementOf0(u,szNzAzT0) -> sdtlseqdt0(xn,u) aElementOf0(u,slbdtrb0(xn))*. % 0.66/0.84 1068[3:Res:1058.0,28.0] || equal(slcrc0,slcrc0)* -> . % 0.66/0.84 1077[3:Obv:1068.0] || -> . % 0.66/0.84 1079[3:Spt:1077.0,314.0,326.0] || equal(slbdtrb0(xm),slcrc0)** -> . % 0.66/0.84 1080[3:Spt:1077.0,314.1] || -> aElement0(skf9(slbdtrb0(xm)))*. % 0.66/0.84 1146[0:Res:75.3,123.1] || aElementOf0(u,szNzAzT0) aElementOf0(xm,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(xm,u) aElementOf0(u,slbdtrb0(xm))*. % 0.66/0.84 1148[0:Obv:1146.0] || aElementOf0(xm,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(xm,u) aElementOf0(u,slbdtrb0(xm))*. % 0.66/0.84 1149[0:MRR:1148.0,5.0] || aElementOf0(u,szNzAzT0) -> sdtlseqdt0(xm,u) aElementOf0(u,slbdtrb0(xm))*. % 0.66/0.84 1151[4:Spt:901.1] || -> aElementOf0(xn,slbdtrb0(xn))*. % 0.66/0.84 1557[0:Res:31.1,89.0] || aElementOf0(u,szNzAzT0) sdtlseqdt0(szszuzczcdt0(u),u)* aElementOf0(u,szNzAzT0) aElementOf0(szszuzczcdt0(u),szNzAzT0) -> equal(szszuzczcdt0(u),u). % 0.66/0.84 1569[0:Obv:1557.0] || sdtlseqdt0(szszuzczcdt0(u),u)* aElementOf0(u,szNzAzT0) aElementOf0(szszuzczcdt0(u),szNzAzT0) -> equal(szszuzczcdt0(u),u). % 0.66/0.84 1570[0:MRR:1569.2,1569.3,30.1,40.1] || sdtlseqdt0(szszuzczcdt0(u),u)* aElementOf0(u,szNzAzT0) -> . % 0.66/0.84 1583[0:Res:120.1,1570.0] || aElementOf0(xn,slbdtrb0(xn))* aElementOf0(xn,szNzAzT0) -> . % 0.66/0.84 1587[4:MRR:1583.0,1583.1,1151.0,6.0] || -> . % 0.66/0.84 1592[4:Spt:1587.0,901.1,1151.0] || aElementOf0(xn,slbdtrb0(xn))* -> . % 0.66/0.84 1593[4:Spt:1587.0,901.0] || -> aElement0(skf10(szNzAzT0,u))*. % 0.66/0.84 1605[4:Res:231.1,1592.0] || aElementOf0(xn,slbdtrb0(xm))* -> . % 0.66/0.84 1614[4:Res:1149.2,1605.0] || aElementOf0(xn,szNzAzT0) -> sdtlseqdt0(xm,xn)*. % 0.66/0.84 1615[4:MRR:1614.0,1614.1,6.0,233.0] || -> . % 0.66/0.84 1616[2:Spt:1615.0,7.0,232.0] || SkC0* -> . % 0.66/0.84 1617[2:Spt:1615.0,7.1] || -> sdtlseqdt0(xm,xn)*. % 0.66/0.84 1618[2:MRR:14.0,1616.0] || -> aElementOf0(skc1,slbdtrb0(xm))*. % 0.66/0.84 1619[2:MRR:16.1,1616.0] || aElementOf0(skc1,slbdtrb0(xn))* -> . % 0.66/0.84 1655[2:Res:231.1,1619.0] || aElementOf0(skc1,slbdtrb0(xm))* -> . % 0.66/0.84 1656[2:MRR:1655.0,1618.0] || -> . % 0.66/0.84 1658[1:Spt:1656.0,51.0] || SkC0* -> . % 0.66/0.84 1659[1:MRR:7.0,1658.0] || -> sdtlseqdt0(xm,xn)*. % 0.66/0.84 1660[1:MRR:14.0,1658.0] || -> aElementOf0(skc1,slbdtrb0(xm))*. % 0.66/0.84 1661[1:MRR:16.1,1658.0] || aElementOf0(skc1,slbdtrb0(xn))* -> . % 0.66/0.84 1669[1:Res:1660.0,118.0] || -> aElementOf0(skc1,szNzAzT0)*. % 0.66/0.84 1677[1:Res:1065.2,1661.0] || aElementOf0(skc1,szNzAzT0) -> sdtlseqdt0(xn,skc1)*. % 0.66/0.84 1678[1:MRR:1677.0,1669.0] || -> sdtlseqdt0(xn,skc1)*. % 0.66/0.84 2486[1:Res:1678.0,107.0] || sdtlseqdt0(u,xn) aElementOf0(skc1,szNzAzT0) aElementOf0(xn,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,skc1)*. % 0.66/0.85 2488[1:Res:1659.0,107.0] || sdtlseqdt0(u,xm) aElementOf0(xn,szNzAzT0) aElementOf0(xm,szNzAzT0) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,xn)*. % 0.66/0.85 2490[1:MRR:2486.1,2486.2,1669.0,6.0] || sdtlseqdt0(u,xn) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,skc1)*. % 0.66/0.85 2491[1:MRR:2488.1,2488.2,6.0,5.0] || sdtlseqdt0(u,xm) aElementOf0(u,szNzAzT0) -> sdtlseqdt0(u,xn)*. % 0.66/0.85 2615[1:Res:2490.2,1570.0] || sdtlseqdt0(szszuzczcdt0(skc1),xn)* aElementOf0(szszuzczcdt0(skc1),szNzAzT0) aElementOf0(skc1,szNzAzT0) -> . % 0.66/0.85 2617[1:MRR:2615.1,2615.2,30.1,1669.0] || sdtlseqdt0(szszuzczcdt0(skc1),xn)* -> . % 0.66/0.85 2635[1:Res:2491.2,2617.0] || sdtlseqdt0(szszuzczcdt0(skc1),xm)* aElementOf0(szszuzczcdt0(skc1),szNzAzT0) -> . % 0.66/0.85 2646[1:Res:121.1,2635.0] || aElementOf0(skc1,slbdtrb0(xm)) aElementOf0(szszuzczcdt0(skc1),szNzAzT0)* -> . % 0.66/0.85 2647[1:MRR:2646.0,1660.0] || aElementOf0(szszuzczcdt0(skc1),szNzAzT0)* -> . % 0.66/0.85 2662[1:Res:30.1,2647.0] || aElementOf0(skc1,szNzAzT0)* -> . % 0.66/0.86 2663[1:MRR:2662.0,1669.0] || -> . % 0.66/0.86 % SZS output end Refutation % 0.66/0.86 Formulae used in the proof : mNATSet m__1964 m__ mSubRefl mSegFin mDefEmp mSuccNum mLessSucc mEOfElem mNatNSucc mSubFSet mDefSub mLessTotal mLessASymm mLessTrans % 0.66/0.86 %------------------------------------------------------------------------------