%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM538+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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:16 EDT 2022 % Result : Theorem 0.80s 1.25s % Output : Refutation 0.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.37 % Problem : NUM538+2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.38 % Command : run_spass %d %s % 0.16/0.59 % Computer : n023.cluster.edu % 0.16/0.59 % Model : x86_64 x86_64 % 0.16/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.59 % Memory : 8042.1875MB % 0.16/0.59 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.59 % CPULimit : 300 % 0.16/0.59 % WCLimit : 600 % 0.16/0.59 % DateTime : Thu Jul 7 02:04:57 EDT 2022 % 0.16/0.59 % CPUTime : % 0.80/1.25 % 0.80/1.25 SPASS V 3.9 % 0.80/1.25 SPASS beiseite: Proof found. % 0.80/1.25 % SZS status Theorem % 0.80/1.25 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.80/1.25 SPASS derived 3802 clauses, backtracked 275 clauses, performed 12 splits and kept 1434 clauses. % 0.80/1.25 SPASS allocated 101515 KBytes. % 0.80/1.25 SPASS spent 0:00:00.65 on the problem. % 0.80/1.25 0:00:00.04 for the input. % 0.80/1.25 0:00:00.05 for the FLOTTER CNF translation. % 0.80/1.25 0:00:00.07 for inferences. % 0.80/1.25 0:00:00.01 for the backtracking. % 0.80/1.25 0:00:00.45 for the reduction. % 0.80/1.25 % 0.80/1.25 % 0.80/1.25 Here is a proof with depth 7, length 173 : % 0.80/1.25 % SZS output start Refutation % 0.80/1.25 1[0:Inp] || -> isFinite0(slcrc0)*. % 0.80/1.25 2[0:Inp] || -> aSet0(szNzAzT0)*. % 0.80/1.25 3[0:Inp] || -> isCountable0(szNzAzT0)*. % 0.80/1.25 4[0:Inp] || -> aSet0(xS)*. % 0.80/1.25 5[0:Inp] || -> isFinite0(xS)*. % 0.80/1.25 6[0:Inp] || -> aElementOf0(sz00,szNzAzT0)*. % 0.80/1.25 7[0:Inp] || -> aElementOf0(xx,xS)*. % 0.80/1.25 8[0:Inp] || -> aSet0(sdtmndt0(xS,xx))*. % 0.80/1.25 10[0:Inp] || equal(u,slcrc0) -> aSet0(u)*. % 0.80/1.25 12[0:Inp] aSet0(u) || -> aSubsetOf0(u,u)*. % 0.80/1.25 19[0:Inp] || aElementOf0(u,v)* equal(v,slcrc0) -> . % 0.80/1.25 24[0:Inp] || aElementOf0(u,sdtmndt0(xS,xx))* -> aElementOf0(u,xS). % 0.80/1.25 25[0:Inp] || equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))),sbrdtbr0(xS))** -> . % 0.80/1.25 26[0:Inp] aSet0(u) || aElementOf0(v,u)* -> aElement0(v). % 0.80/1.25 28[0:Inp] aSet0(u) || aSubsetOf0(v,u)* -> aSet0(v). % 0.80/1.25 33[0:Inp] || equal(u,xx) aElementOf0(u,sdtmndt0(xS,xx))* -> . % 0.80/1.25 34[0:Inp] aSet0(u) || -> equal(u,slcrc0) aElementOf0(skf5(u),u)*. % 0.80/1.25 42[0:Inp] isFinite0(u) aSet0(u) || aSubsetOf0(v,u)* -> isFinite0(v). % 0.80/1.25 47[0:Inp] isFinite0(u) aSet0(u) aElement0(v) || -> isFinite0(sdtmndt0(u,v))*. % 0.80/1.25 48[0:Inp] aSet0(u) || aElementOf0(v,w)*+ aSubsetOf0(w,u)* -> aElementOf0(v,u)*. % 0.80/1.25 49[0:Inp] aSet0(u) aSet0(v) || -> aSubsetOf0(v,u)* aElementOf0(skf6(v,w),v)*. % 0.80/1.25 51[0:Inp] aElement0(u) aSet0(v) || equal(w,sdtmndt0(v,u))*+ -> aSet0(w)*. % 0.80/1.25 53[0:Inp] aSet0(u) || aElementOf0(v,u) -> equal(sdtpldt0(sdtmndt0(u,v),v),u)**. % 0.80/1.25 54[0:Inp] aElement0(u) || aElementOf0(u,xS) -> equal(u,xx) aElementOf0(u,sdtmndt0(xS,xx))*. % 0.80/1.25 55[0:Inp] aSet0(u) aSet0(v) || aElementOf0(skf6(v,u),u)* -> aSubsetOf0(v,u). % 0.80/1.25 58[0:Inp] aSet0(u) aSet0(v) || aSubsetOf0(v,u)* aSubsetOf0(u,v)* -> equal(u,v). % 0.80/1.25 63[0:Inp] aElement0(u) isFinite0(v) aSet0(v) || -> aElementOf0(u,v) equal(sbrdtbr0(sdtpldt0(v,u)),szszuzczcdt0(sbrdtbr0(v)))**. % 0.80/1.25 66[0:Inp] aElement0(u) aSet0(v) || equal(w,sdtpldt0(v,u))*+ SkP0(u,v,x)* -> aElementOf0(x,w)*. % 0.80/1.25 67[0:Inp] aElement0(u) aSet0(v) || aElementOf0(w,x)* equal(x,sdtpldt0(v,u))*+ -> SkP0(u,v,w)*. % 0.80/1.25 68[0:Inp] aSet0(u) aSet0(v) aSet0(w) || aSubsetOf0(u,v)* aSubsetOf0(v,w)* -> aSubsetOf0(u,w)*. % 0.80/1.25 75[0:MRR:58.0,28.2] aSet0(u) || aSubsetOf0(v,u)*+ aSubsetOf0(u,v)* -> equal(v,u). % 0.80/1.25 76[0:MRR:68.0,68.1,28.2,28.2] aSet0(u) || aSubsetOf0(v,u)*+ aSubsetOf0(w,v)* -> aSubsetOf0(w,u)*. % 0.80/1.25 89[0:Res:8.0,48.0] || aElementOf0(u,v)* aSubsetOf0(v,sdtmndt0(xS,xx))*+ -> aElementOf0(u,sdtmndt0(xS,xx))*. % 0.80/1.25 94[0:Res:8.0,42.0] isFinite0(sdtmndt0(xS,xx)) || aSubsetOf0(u,sdtmndt0(xS,xx))* -> isFinite0(u). % 0.80/1.25 101[0:Res:8.0,28.0] || aSubsetOf0(u,sdtmndt0(xS,xx))* -> aSet0(u). % 0.80/1.25 102[0:Res:8.0,12.0] || -> aSubsetOf0(sdtmndt0(xS,xx),sdtmndt0(xS,xx))*. % 0.80/1.25 110[0:Res:8.0,49.1] aSet0(u) || -> aSubsetOf0(u,sdtmndt0(xS,xx))* aElementOf0(skf6(u,v),u)*. % 0.80/1.25 144[0:Res:7.0,26.1] aSet0(xS) || -> aElement0(xx)*. % 0.80/1.25 148[0:SSi:144.0,5.0,4.0] || -> aElement0(xx)*. % 0.80/1.25 172[0:Res:34.2,24.0] aSet0(sdtmndt0(xS,xx)) || -> equal(sdtmndt0(xS,xx),slcrc0) aElementOf0(skf5(sdtmndt0(xS,xx)),xS)*. % 0.80/1.25 183[0:SSi:172.0,8.0] || -> equal(sdtmndt0(xS,xx),slcrc0) aElementOf0(skf5(sdtmndt0(xS,xx)),xS)*. % 0.80/1.25 187[1:Spt:183.0] || -> equal(sdtmndt0(xS,xx),slcrc0)**. % 0.80/1.25 188[1:Rew:187.0,8.0] || -> aSet0(slcrc0)*. % 0.80/1.25 190[1:Rew:187.0,33.1] || equal(u,xx) aElementOf0(u,slcrc0)* -> . % 0.80/1.25 194[1:Rew:187.0,25.0] || equal(szszuzczcdt0(sbrdtbr0(slcrc0)),sbrdtbr0(xS))** -> . % 0.80/1.25 195[1:Rew:187.0,54.3] aElement0(u) || aElementOf0(u,xS)* -> equal(u,xx) aElementOf0(u,slcrc0). % 0.80/1.25 196[1:Rew:187.0,89.2] || aElementOf0(u,v)* aSubsetOf0(v,sdtmndt0(xS,xx))* -> aElementOf0(u,slcrc0)*. % 0.80/1.25 207[1:Rew:187.0,110.1] aSet0(u) || -> aSubsetOf0(u,slcrc0) aElementOf0(skf6(u,v),u)*. % 0.80/1.25 211[1:Rew:187.0,196.1] || aElementOf0(u,v)*+ aSubsetOf0(v,slcrc0)* -> aElementOf0(u,slcrc0)*. % 0.80/1.25 323[1:Res:207.2,195.1] aSet0(xS) aElement0(skf6(xS,u)) || -> aSubsetOf0(xS,slcrc0) equal(skf6(xS,u),xx) aElementOf0(skf6(xS,u),slcrc0)*. % 0.80/1.25 326[1:SSi:323.0,5.0,4.0] aElement0(skf6(xS,u)) || -> aSubsetOf0(xS,slcrc0) equal(skf6(xS,u),xx) aElementOf0(skf6(xS,u),slcrc0)*. % 0.80/1.25 414[0:EqR:51.2] aElement0(u) aSet0(v) || -> aSet0(sdtmndt0(v,u))*. % 0.80/1.25 450[1:SpR:187.0,53.2] aSet0(xS) || aElementOf0(xx,xS) -> equal(sdtpldt0(slcrc0,xx),xS)**. % 0.80/1.25 452[1:SSi:450.0,5.0,4.0] || aElementOf0(xx,xS) -> equal(sdtpldt0(slcrc0,xx),xS)**. % 0.80/1.25 453[1:MRR:452.0,7.0] || -> equal(sdtpldt0(slcrc0,xx),xS)**. % 0.80/1.25 533[0:Res:49.3,19.0] aSet0(u) aSet0(v) || equal(v,slcrc0) -> aSubsetOf0(v,u)*. % 0.80/1.25 538[0:Res:49.3,26.1] aSet0(u) aSet0(v) aSet0(v) || -> aSubsetOf0(v,u)* aElement0(skf6(v,w))*. % 0.80/1.25 539[0:MRR:533.1,10.1] aSet0(u) || equal(v,slcrc0) -> aSubsetOf0(v,u)*. % 0.80/1.25 542[0:Obv:538.1] aSet0(u) aSet0(v) || -> aSubsetOf0(v,u)* aElement0(skf6(v,w))*. % 0.80/1.25 582[0:Res:539.2,76.1] aSet0(u) aSet0(u) || equal(v,slcrc0) aSubsetOf0(w,v)* -> aSubsetOf0(w,u)*. % 0.80/1.25 589[0:Obv:582.0] aSet0(u) || equal(v,slcrc0)+ aSubsetOf0(w,v)* -> aSubsetOf0(w,u)*. % 0.80/1.25 613[0:Res:7.0,48.1] aSet0(u) || aSubsetOf0(xS,u)* -> aElementOf0(xx,u). % 0.80/1.25 614[0:Res:6.0,48.1] aSet0(u) || aSubsetOf0(szNzAzT0,u)* -> aElementOf0(sz00,u). % 0.80/1.25 620[0:Res:34.2,48.1] aSet0(u) aSet0(v) || aSubsetOf0(u,v) -> equal(u,slcrc0) aElementOf0(skf5(u),v)*. % 0.80/1.25 623[0:MRR:620.0,28.2] aSet0(u) || aSubsetOf0(v,u) -> equal(v,slcrc0) aElementOf0(skf5(v),u)*. % 0.80/1.25 627[0:Res:542.2,613.1] aSet0(u) aSet0(xS) aSet0(u) || -> aElement0(skf6(xS,v))* aElementOf0(xx,u)*. % 0.80/1.25 629[0:Res:49.2,613.1] aSet0(u) aSet0(xS) aSet0(u) || -> aElementOf0(skf6(xS,v),xS)* aElementOf0(xx,u)*. % 0.80/1.25 633[0:Obv:627.0] aSet0(xS) aSet0(u) || -> aElement0(skf6(xS,v))* aElementOf0(xx,u)*. % 0.80/1.25 634[0:SSi:633.0,5.0,4.0] aSet0(u) || -> aElement0(skf6(xS,v))* aElementOf0(xx,u)*. % 0.80/1.25 635[0:Obv:629.0] aSet0(xS) aSet0(u) || -> aElementOf0(skf6(xS,v),xS)* aElementOf0(xx,u)*. % 0.80/1.25 636[0:SSi:635.0,5.0,4.0] aSet0(u) || -> aElementOf0(skf6(xS,v),xS)* aElementOf0(xx,u)*. % 0.80/1.25 638[0:Res:542.2,614.1] aSet0(u) aSet0(szNzAzT0) aSet0(u) || -> aElement0(skf6(szNzAzT0,v))* aElementOf0(sz00,u)*. % 0.80/1.25 644[0:Obv:638.0] aSet0(szNzAzT0) aSet0(u) || -> aElement0(skf6(szNzAzT0,v))* aElementOf0(sz00,u)*. % 0.80/1.25 645[0:SSi:644.0,3.0,2.0] aSet0(u) || -> aElement0(skf6(szNzAzT0,v))* aElementOf0(sz00,u)*. % 0.80/1.25 648[2:Spt:634.0,634.2] aSet0(u) || -> aElementOf0(xx,u)*. % 0.80/1.25 656[2:Res:648.1,190.1] aSet0(slcrc0) || equal(xx,xx)* -> . % 0.80/1.25 665[2:Obv:656.1] aSet0(slcrc0) || -> . % 0.80/1.25 666[2:SSi:665.0,1.0,188.0] || -> . % 0.80/1.25 673[2:Spt:666.0,634.1] || -> aElement0(skf6(xS,u))*. % 0.80/1.25 674[2:MRR:326.0,673.0] || -> aSubsetOf0(xS,slcrc0) equal(skf6(xS,u),xx) aElementOf0(skf6(xS,u),slcrc0)*. % 0.80/1.25 681[3:Spt:645.0,645.2] aSet0(u) || -> aElementOf0(sz00,u)*. % 0.80/1.25 688[3:Res:681.1,19.0] aSet0(u) || equal(u,slcrc0)* -> . % 0.80/1.25 694[3:MRR:688.0,10.1] || equal(u,slcrc0)* -> . % 0.80/1.25 695[3:UnC:694.0,187.0] || -> . % 0.80/1.25 701[3:Spt:695.0,645.1] || -> aElement0(skf6(szNzAzT0,u))*. % 0.80/1.25 720[4:Spt:636.0,636.2] aSet0(u) || -> aElementOf0(xx,u)*. % 0.80/1.25 728[4:Res:720.1,190.1] aSet0(slcrc0) || equal(xx,xx)* -> . % 0.80/1.25 736[4:Obv:728.1] aSet0(slcrc0) || -> . % 0.80/1.25 737[4:SSi:736.0,1.0,188.0] || -> . % 0.80/1.25 743[4:Spt:737.0,636.1] || -> aElementOf0(skf6(xS,u),xS)*. % 0.80/1.25 744[4:Res:743.0,211.0] || aSubsetOf0(xS,slcrc0) -> aElementOf0(skf6(xS,u),slcrc0)*. % 0.80/1.25 749[4:MRR:674.0,744.0] || -> equal(skf6(xS,u),xx) aElementOf0(skf6(xS,u),slcrc0)*. % 0.80/1.25 758[4:Res:744.1,19.0] || aSubsetOf0(xS,slcrc0)* equal(slcrc0,slcrc0) -> . % 0.80/1.25 763[4:Obv:758.1] || aSubsetOf0(xS,slcrc0)* -> . % 0.80/1.25 767[4:Res:749.1,19.0] || equal(slcrc0,slcrc0) -> equal(skf6(xS,u),xx)**. % 0.80/1.25 772[4:Obv:767.0] || -> equal(skf6(xS,u),xx)**. % 0.80/1.25 788[4:SpL:772.0,55.2] aSet0(u) aSet0(xS) || aElementOf0(xx,u) -> aSubsetOf0(xS,u)*. % 0.80/1.25 789[4:SSi:788.1,5.0,4.0] aSet0(u) || aElementOf0(xx,u) -> aSubsetOf0(xS,u)*. % 0.80/1.25 811[4:Res:789.2,763.0] aSet0(slcrc0) || aElementOf0(xx,slcrc0)* -> . % 0.80/1.25 814[4:SSi:811.0,1.0,188.0] || aElementOf0(xx,slcrc0)* -> . % 0.80/1.25 1055[0:SpR:53.2,63.4] aSet0(u) aElement0(v) isFinite0(sdtmndt0(u,v)) aSet0(sdtmndt0(u,v)) || aElementOf0(v,u) -> aElementOf0(v,sdtmndt0(u,v))* equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u))**. % 0.80/1.25 1056[1:SpR:453.0,63.4] aElement0(xx) isFinite0(slcrc0) aSet0(slcrc0) || -> aElementOf0(xx,slcrc0) equal(szszuzczcdt0(sbrdtbr0(slcrc0)),sbrdtbr0(xS))**. % 0.80/1.29 1061[1:SSi:1056.2,1056.1,1056.0,1.0,188.0,1.0,188.0,148.0] || -> aElementOf0(xx,slcrc0) equal(szszuzczcdt0(sbrdtbr0(slcrc0)),sbrdtbr0(xS))**. % 0.80/1.29 1062[4:MRR:1061.0,1061.1,814.0,194.0] || -> . % 0.80/1.29 1068[0:SSi:1055.3,414.2] aSet0(u) aElement0(v) isFinite0(sdtmndt0(u,v)) || aElementOf0(v,u) -> aElementOf0(v,sdtmndt0(u,v))* equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u))**. % 0.80/1.29 1069[0:MRR:1068.1,26.2] aSet0(u) isFinite0(sdtmndt0(u,v)) || aElementOf0(v,u) -> aElementOf0(v,sdtmndt0(u,v))* equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u))**. % 0.80/1.29 1070[1:Spt:1062.0,183.0,187.0] || equal(sdtmndt0(xS,xx),slcrc0)** -> . % 0.80/1.29 1071[1:Spt:1062.0,183.1] || -> aElementOf0(skf5(sdtmndt0(xS,xx)),xS)*. % 0.80/1.29 1073[0:SSi:94.0,414.0,5.0,4.0,148.3,47.0,5.0,4.0,148.2] || aSubsetOf0(u,sdtmndt0(xS,xx))* -> isFinite0(u). % 0.80/1.29 1110[0:Res:102.0,1073.0] || -> isFinite0(sdtmndt0(xS,xx))*. % 0.80/1.29 1126[0:Res:49.3,24.0] aSet0(u) aSet0(sdtmndt0(xS,xx)) || -> aSubsetOf0(sdtmndt0(xS,xx),u)* aElementOf0(skf6(sdtmndt0(xS,xx),v),xS)*. % 0.80/1.29 1130[0:SSi:1126.1,414.0,5.0,4.0,148.3,47.0,5.0,4.0,148.2] aSet0(u) || -> aSubsetOf0(sdtmndt0(xS,xx),u)* aElementOf0(skf6(sdtmndt0(xS,xx),v),xS)*. % 0.80/1.29 1161[0:Res:54.3,55.2] aElement0(skf6(u,sdtmndt0(xS,xx))) aSet0(sdtmndt0(xS,xx)) aSet0(u) || aElementOf0(skf6(u,sdtmndt0(xS,xx)),xS)* -> equal(skf6(u,sdtmndt0(xS,xx)),xx) aSubsetOf0(u,sdtmndt0(xS,xx)). % 0.80/1.29 1163[0:SSi:1161.1,414.0,5.0,4.0,148.3,47.0,5.0,4.0,148.2] aElement0(skf6(u,sdtmndt0(xS,xx))) aSet0(u) || aElementOf0(skf6(u,sdtmndt0(xS,xx)),xS)* -> equal(skf6(u,sdtmndt0(xS,xx)),xx) aSubsetOf0(u,sdtmndt0(xS,xx)). % 0.80/1.29 1167[2:Spt:634.0,634.2] aSet0(u) || -> aElementOf0(xx,u)*. % 0.80/1.29 1174[2:Res:1167.1,33.1] aSet0(sdtmndt0(xS,xx)) || equal(xx,xx)* -> . % 0.80/1.29 1188[2:Obv:1174.1] aSet0(sdtmndt0(xS,xx)) || -> . % 0.80/1.29 1189[2:SSi:1188.0,414.0,5.0,4.0,148.3,47.0,5.0,4.0,148.2] || -> . % 0.80/1.29 1191[2:Spt:1189.0,634.1] || -> aElement0(skf6(xS,u))*. % 0.80/1.29 1297[3:Spt:636.0,636.2] aSet0(u) || -> aElementOf0(xx,u)*. % 0.80/1.29 1304[3:Res:1297.1,33.1] aSet0(sdtmndt0(xS,xx)) || equal(xx,xx)* -> . % 0.80/1.29 1318[3:Obv:1304.1] aSet0(sdtmndt0(xS,xx)) || -> . % 0.80/1.29 1319[3:SSi:1318.0,414.0,5.0,4.0,148.3,47.0,5.0,4.0,148.2] || -> . % 0.80/1.29 1321[3:Spt:1319.0,636.1] || -> aElementOf0(skf6(xS,u),xS)*. % 0.80/1.29 1439[0:SpL:53.2,67.3] aSet0(u) aElement0(v) aSet0(sdtmndt0(u,v)) || aElementOf0(v,u) aElementOf0(w,x)* equal(x,u)* -> SkP0(v,sdtmndt0(u,v),w)*. % 0.80/1.29 1440[0:SSi:1439.2,414.2] aSet0(u) aElement0(v) || aElementOf0(v,u) aElementOf0(w,x)* equal(x,u)* -> SkP0(v,sdtmndt0(u,v),w)*. % 0.80/1.29 1441[0:MRR:1440.1,26.2] aSet0(u) || aElementOf0(v,u)+ aElementOf0(w,x)* equal(x,u)* -> SkP0(v,sdtmndt0(u,v),w)*. % 0.80/1.29 1494[0:SpL:53.2,66.2] aSet0(u) aElement0(v) aSet0(sdtmndt0(u,v)) || aElementOf0(v,u) equal(w,u)* SkP0(v,sdtmndt0(u,v),x)* -> aElementOf0(x,w)*. % 0.80/1.29 1495[0:SSi:1494.2,414.2] aSet0(u) aElement0(v) || aElementOf0(v,u) equal(w,u)* SkP0(v,sdtmndt0(u,v),x)* -> aElementOf0(x,w)*. % 0.80/1.29 1496[0:MRR:1495.1,26.2] aSet0(u) || aElementOf0(v,u) equal(w,u)* SkP0(v,sdtmndt0(u,v),x)*+ -> aElementOf0(x,w)*. % 0.80/1.29 1521[0:Res:110.2,26.1] aSet0(u) aSet0(u) || -> aSubsetOf0(u,sdtmndt0(xS,xx))* aElement0(skf6(u,v))*. % 0.80/1.29 1525[0:Obv:1521.0] aSet0(u) || -> aSubsetOf0(u,sdtmndt0(xS,xx))* aElement0(skf6(u,v))*. % 0.80/1.29 1526[0:MRR:1163.0,1525.2] aSet0(u) || aElementOf0(skf6(u,sdtmndt0(xS,xx)),xS)* -> equal(skf6(u,sdtmndt0(xS,xx)),xx) aSubsetOf0(u,sdtmndt0(xS,xx)). % 0.80/1.29 1605[0:EqR:589.1] aSet0(u) || aSubsetOf0(v,slcrc0)*+ -> aSubsetOf0(v,u)*. % 0.80/1.29 1606[0:Res:12.1,1605.1] aSet0(slcrc0) aSet0(u) || -> aSubsetOf0(slcrc0,u)*. % 0.80/1.29 1626[0:SoR:1606.0,10.1] aSet0(u) || equal(slcrc0,slcrc0) -> aSubsetOf0(slcrc0,u)*. % 0.80/1.29 1627[0:Obv:1626.1] aSet0(u) || -> aSubsetOf0(slcrc0,u)*. % 0.80/1.29 1629[0:Res:1627.1,75.1] aSet0(u) aSet0(u) || aSubsetOf0(u,slcrc0)* -> equal(slcrc0,u). % 0.80/1.29 1634[0:Res:1627.1,101.0] aSet0(sdtmndt0(xS,xx)) || -> aSet0(slcrc0)*. % 0.80/1.29 1636[0:SSi:1634.0,414.0,5.0,4.0,148.3,47.0,5.0,4.0,148.2] || -> aSet0(slcrc0)*. % 0.80/1.29 1641[0:Obv:1629.0] aSet0(u) || aSubsetOf0(u,slcrc0)* -> equal(slcrc0,u). % 0.80/1.29 1674[0:Res:623.3,19.0] aSet0(u) || aSubsetOf0(v,u)* equal(u,slcrc0) -> equal(v,slcrc0). % 0.80/1.29 1681[0:MRR:1674.0,10.1] || aSubsetOf0(u,v)* equal(v,slcrc0) -> equal(u,slcrc0). % 0.80/1.29 1734[4:Spt:1130.0,1130.1] aSet0(u) || -> aSubsetOf0(sdtmndt0(xS,xx),u)*. % 0.80/1.29 1741[4:Res:1734.1,1681.0] aSet0(u) || equal(u,slcrc0)* -> equal(sdtmndt0(xS,xx),slcrc0)**. % 0.80/1.29 1748[4:Res:1734.1,1641.1] aSet0(slcrc0) aSet0(sdtmndt0(xS,xx)) || -> equal(sdtmndt0(xS,xx),slcrc0)**. % 0.80/1.29 1750[4:MRR:1741.0,1741.2,10.1,1070.0] || equal(u,slcrc0)* -> . % 0.80/1.29 1766[4:SSi:1748.1,1748.0,414.0,5.0,4.0,148.0,47.0,5.3,4.0,148.0,1.0,1636.2] || -> equal(sdtmndt0(xS,xx),slcrc0)**. % 0.80/1.29 1767[4:MRR:1766.0,1750.0] || -> . % 0.80/1.29 1772[4:Spt:1767.0,1130.2] || -> aElementOf0(skf6(sdtmndt0(xS,xx),u),xS)*. % 0.80/1.29 1775[4:Res:1772.0,55.2] aSet0(xS) aSet0(sdtmndt0(xS,xx)) || -> aSubsetOf0(sdtmndt0(xS,xx),xS)*. % 0.80/1.29 1778[4:SSi:1775.1,1775.0,414.0,5.0,4.0,148.0,47.0,5.3,4.0,148.0,5.0,4.2] || -> aSubsetOf0(sdtmndt0(xS,xx),xS)*. % 0.80/1.29 1780[4:Res:1778.0,75.1] aSet0(xS) || aSubsetOf0(xS,sdtmndt0(xS,xx))* -> equal(sdtmndt0(xS,xx),xS). % 0.80/1.29 1784[4:SSi:1780.0,5.0,4.0] || aSubsetOf0(xS,sdtmndt0(xS,xx))* -> equal(sdtmndt0(xS,xx),xS). % 0.80/1.29 4321[0:Res:7.0,1441.1] aSet0(xS) || aElementOf0(u,v)* equal(v,xS) -> SkP0(xx,sdtmndt0(xS,xx),u)*. % 0.80/1.29 4374[0:SSi:4321.0,5.0,4.0] || aElementOf0(u,v)*+ equal(v,xS) -> SkP0(xx,sdtmndt0(xS,xx),u)*. % 0.80/1.29 4438[0:Res:7.0,4374.0] || equal(xS,xS) -> SkP0(xx,sdtmndt0(xS,xx),xx)*. % 0.80/1.29 4491[0:Obv:4438.0] || -> SkP0(xx,sdtmndt0(xS,xx),xx)*. % 0.80/1.29 4513[0:Res:4491.0,1496.3] aSet0(xS) || aElementOf0(xx,xS)* equal(u,xS) -> aElementOf0(xx,u)*. % 0.80/1.29 4514[0:SSi:4513.0,5.0,4.0] || aElementOf0(xx,xS)* equal(u,xS) -> aElementOf0(xx,u)*. % 0.80/1.29 4515[0:MRR:4514.0,7.0] || equal(u,xS) -> aElementOf0(xx,u)*. % 0.80/1.29 4528[0:Res:4515.1,33.1] || equal(sdtmndt0(xS,xx),xS)** equal(xx,xx) -> . % 0.80/1.29 4540[0:Obv:4528.1] || equal(sdtmndt0(xS,xx),xS)** -> . % 0.80/1.29 4541[4:MRR:1784.1,4540.0] || aSubsetOf0(xS,sdtmndt0(xS,xx))* -> . % 0.80/1.29 4755[3:Res:1321.0,1526.1] aSet0(xS) || -> equal(skf6(xS,sdtmndt0(xS,xx)),xx)** aSubsetOf0(xS,sdtmndt0(xS,xx)). % 0.80/1.29 4772[3:SSi:4755.0,5.0,4.0] || -> equal(skf6(xS,sdtmndt0(xS,xx)),xx)** aSubsetOf0(xS,sdtmndt0(xS,xx)). % 0.80/1.29 4773[4:MRR:4772.1,4541.0] || -> equal(skf6(xS,sdtmndt0(xS,xx)),xx)**. % 0.80/1.29 4813[4:SpL:4773.0,55.2] aSet0(sdtmndt0(xS,xx)) aSet0(xS) || aElementOf0(xx,sdtmndt0(xS,xx)) -> aSubsetOf0(xS,sdtmndt0(xS,xx))*. % 0.80/1.29 4822[4:SSi:4813.1,4813.0,5.0,4.0,1110.0,414.2,5.0,4.0,148.0] || aElementOf0(xx,sdtmndt0(xS,xx)) -> aSubsetOf0(xS,sdtmndt0(xS,xx))*. % 0.80/1.29 4823[4:MRR:4822.1,4541.0] || aElementOf0(xx,sdtmndt0(xS,xx))* -> . % 0.80/1.29 5228[0:SoR:1069.1,1110.0] aSet0(xS) || aElementOf0(xx,xS) -> aElementOf0(xx,sdtmndt0(xS,xx)) equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))),sbrdtbr0(xS))**. % 0.80/1.29 5230[0:SSi:5228.0,5.0,4.0] || aElementOf0(xx,xS) -> aElementOf0(xx,sdtmndt0(xS,xx)) equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))),sbrdtbr0(xS))**. % 0.80/1.29 5231[4:MRR:5230.0,5230.1,5230.2,7.0,4823.0,25.0] || -> . % 0.80/1.29 % SZS output end Refutation % 0.80/1.29 Formulae used in the proof : mEmpFin mNATSet m__1522 m__1522_02 mZeroNum m__ mDefEmp mSubRefl mEOfElem mDefSub mSubFSet mFDiffSet mDefDiff mConsDiff mSubASymm mCardCons mDefCons mSubTrans % 0.80/1.29 %------------------------------------------------------------------------------