%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU238+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n004.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 : Tue Jul 19 14:35:24 EDT 2022 % Result : Theorem 0.71s 0.90s % Output : Refutation 0.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU238+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n004.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 : Sat Jun 18 20:59:38 EDT 2022 % 0.13/0.34 % CPUTime : % 0.71/0.90 % 0.71/0.90 SPASS V 3.9 % 0.71/0.90 SPASS beiseite: Proof found. % 0.71/0.90 % SZS status Theorem % 0.71/0.90 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.71/0.90 SPASS derived 3542 clauses, backtracked 475 clauses, performed 24 splits and kept 1525 clauses. % 0.71/0.90 SPASS allocated 119563 KBytes. % 0.71/0.90 SPASS spent 0:00:00.49 on the problem. % 0.71/0.90 0:00:00.04 for the input. % 0.71/0.90 0:00:00.03 for the FLOTTER CNF translation. % 0.71/0.90 0:00:00.06 for inferences. % 0.71/0.90 0:00:00.01 for the backtracking. % 0.71/0.90 0:00:00.31 for the reduction. % 0.71/0.90 % 0.71/0.90 % 0.71/0.90 Here is a proof with depth 12, length 161 : % 0.71/0.90 % SZS output start Refutation % 0.71/0.90 1[0:Inp] || -> ordinal(skc15)*. % 0.71/0.90 2[0:Inp] || -> ordinal(skc14)*. % 0.71/0.90 51[0:Inp] || -> ordinal(skf3(u))*. % 0.71/0.90 52[0:Inp] || -> SkP0(skc14) being_limit_ordinal(skc14)*. % 0.71/0.90 56[0:Inp] || -> in(u,succ(u))*. % 0.71/0.90 58[0:Inp] ordinal(u) || -> epsilon_transitive(u)*. % 0.71/0.90 59[0:Inp] ordinal(u) || -> epsilon_connected(u)*. % 0.71/0.90 66[0:Inp] || -> SkP0(skc14) equal(succ(skc15),skc14)**. % 0.71/0.90 67[0:Inp] SkP0(u) being_limit_ordinal(u) || -> . % 0.71/0.90 68[0:Inp] ordinal(u) || -> epsilon_transitive(succ(u))*. % 0.71/0.90 69[0:Inp] ordinal(u) || -> epsilon_connected(succ(u))*. % 0.71/0.90 70[0:Inp] ordinal(u) || -> ordinal(succ(u))*. % 0.71/0.90 71[0:Inp] ordinal(u) || -> ordinal_subset(u,u)*. % 0.71/0.90 75[0:Inp] || proper_subset(u,v) -> subset(u,v)*. % 0.71/0.90 80[0:Inp] empty(u) || in(v,u)* -> . % 0.71/0.90 81[0:Inp] || in(u,v)*+ in(v,u)* -> . % 0.71/0.90 82[0:Inp] || proper_subset(u,v)*+ proper_subset(v,u)* -> . % 0.71/0.90 86[0:Inp] || subset(u,v) -> element(u,powerset(v))*. % 0.71/0.90 87[0:Inp] || element(u,v)* -> empty(v) in(u,v). % 0.71/0.90 88[0:Inp] ordinal(u) || -> being_limit_ordinal(u) in(skf3(u),u)*. % 0.71/0.90 90[0:Inp] || subset(u,v)* -> proper_subset(u,v) equal(u,v). % 0.71/0.90 92[0:Inp] SkP0(u) ordinal(v) || equal(u,succ(v))* -> . % 0.71/0.90 94[0:Inp] ordinal(u) || in(succ(skf3(u)),u)* -> being_limit_ordinal(u). % 0.71/0.90 95[0:Inp] ordinal(u) ordinal(v) || -> ordinal_subset(u,v)* ordinal_subset(v,u)*. % 0.71/0.90 96[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 0.71/0.90 98[0:Inp] ordinal(u) ordinal(v) || ordinal_subset(v,u) -> subset(v,u)*. % 0.71/0.90 100[0:Inp] ordinal(u) epsilon_transitive(v) || proper_subset(v,u)* -> in(v,u). % 0.71/0.90 101[0:Inp] ordinal(u) ordinal(v) || in(v,u) -> ordinal_subset(succ(v),u)*. % 0.71/0.90 102[0:Inp] ordinal(u) ordinal(v) || ordinal_subset(succ(v),u)* -> in(v,u). % 0.71/0.90 103[0:Inp] ordinal(u) ordinal(v) being_limit_ordinal(u) || in(v,u) -> in(succ(v),u)*. % 0.71/0.90 105[0:Res:2.0,103.2] ordinal(u) being_limit_ordinal(skc14) || in(u,skc14) -> in(succ(u),skc14)*. % 0.71/0.90 107[0:Res:2.0,102.0] ordinal(u) || ordinal_subset(succ(skc14),u)* -> in(skc14,u). % 0.71/0.90 108[0:Res:2.0,98.0] ordinal(u) || ordinal_subset(skc14,u) -> subset(skc14,u)*. % 0.71/0.90 110[0:Res:2.0,95.0] ordinal(u) || -> ordinal_subset(u,skc14)* ordinal_subset(skc14,u)*. % 0.71/0.90 112[0:Res:2.0,94.0] || in(succ(skf3(skc14)),skc14)* -> being_limit_ordinal(skc14). % 0.71/0.90 113[0:Res:2.0,88.0] || -> being_limit_ordinal(skc14) in(skf3(skc14),skc14)*. % 0.71/0.90 114[0:Res:2.0,68.0] || -> epsilon_transitive(succ(skc14))*. % 0.71/0.90 115[0:Res:2.0,69.0] || -> epsilon_connected(succ(skc14))*. % 0.71/0.90 116[0:Res:2.0,70.0] || -> ordinal(succ(skc14))*. % 0.71/0.90 117[0:Res:2.0,71.0] || -> ordinal_subset(skc14,skc14)*. % 0.71/0.90 118[0:Res:2.0,58.0] || -> epsilon_transitive(skc14)*. % 0.71/0.90 119[0:Res:2.0,59.0] || -> epsilon_connected(skc14)*. % 0.71/0.90 120[0:Res:2.0,103.1] ordinal(u) being_limit_ordinal(u) || in(skc14,u) -> in(succ(skc14),u)*. % 0.71/0.90 122[0:Res:2.0,102.1] ordinal(u) || ordinal_subset(succ(u),skc14)* -> in(u,skc14). % 0.71/0.90 123[0:Res:2.0,98.1] ordinal(u) || ordinal_subset(u,skc14) -> subset(u,skc14)*. % 0.71/0.90 125[0:Res:2.0,100.1] epsilon_transitive(u) || proper_subset(u,skc14)* -> in(u,skc14). % 0.71/0.90 133[0:Res:1.0,92.0] SkP0(u) || equal(u,succ(skc15))* -> . % 0.71/0.90 162[0:Res:1.0,105.1] being_limit_ordinal(skc14) || in(skc15,skc14) -> in(succ(skc15),skc14)*. % 0.71/0.90 167[0:Res:1.0,122.0] || ordinal_subset(succ(skc15),skc14)* -> in(skc15,skc14). % 0.71/0.90 185[0:Res:2.0,120.1] being_limit_ordinal(skc14) || in(skc14,skc14) -> in(succ(skc14),skc14)*. % 0.71/0.90 191[0:Res:2.0,122.0] || ordinal_subset(succ(skc14),skc14)* -> in(skc14,skc14). % 0.71/0.90 209[1:Spt:66.1] || -> equal(succ(skc15),skc14)**. % 0.71/0.90 215[1:Rew:209.0,167.0] || ordinal_subset(skc14,skc14)* -> in(skc15,skc14). % 0.71/0.90 219[1:Rew:209.0,133.1] SkP0(u) || equal(u,skc14)* -> . % 0.71/0.90 221[1:Rew:209.0,162.2] being_limit_ordinal(skc14) || in(skc15,skc14)* -> in(skc14,skc14). % 0.71/0.90 223[1:MRR:215.0,117.0] || -> in(skc15,skc14)*. % 0.71/0.90 224[1:MRR:221.1,223.0] being_limit_ordinal(skc14) || -> in(skc14,skc14)*. % 0.71/0.90 225[1:MRR:185.1,224.1] being_limit_ordinal(skc14) || -> in(succ(skc14),skc14)*. % 0.71/0.90 227[2:Spt:52.1] || -> being_limit_ordinal(skc14)*. % 0.71/0.90 230[2:MRR:225.0,227.0] || -> in(succ(skc14),skc14)*. % 0.71/0.90 281[0:Res:56.0,80.1] empty(succ(u)) || -> . % 0.71/0.90 333[0:Res:56.0,81.0] || in(succ(u),u)* -> . % 0.71/0.90 340[2:UnC:333.0,230.0] || -> . % 0.71/0.90 341[2:Spt:340.0,52.1,227.0] || being_limit_ordinal(skc14)* -> . % 0.71/0.90 342[2:Spt:340.0,52.0] || -> SkP0(skc14)*. % 0.71/0.90 348[2:EmS:219.0,342.0] || equal(skc14,skc14)* -> . % 0.71/0.90 349[2:Obv:348.0] || -> . % 0.71/0.90 350[1:Spt:349.0,66.1,209.0] || equal(succ(skc15),skc14)** -> . % 0.71/0.90 351[1:Spt:349.0,66.0] || -> SkP0(skc14)*. % 0.71/0.90 354[2:Spt:113.0] || -> being_limit_ordinal(skc14)*. % 0.71/0.90 359[2:EmS:67.0,67.1,351.0,354.0] || -> . % 0.71/0.90 360[2:Spt:359.0,113.0,354.0] || being_limit_ordinal(skc14)* -> . % 0.71/0.90 361[2:Spt:359.0,113.1] || -> in(skf3(skc14),skc14)*. % 0.71/0.90 362[2:MRR:112.1,360.0] || in(succ(skf3(skc14)),skc14)* -> . % 0.71/0.90 364[2:Res:361.0,80.1] empty(skc14) || -> . % 0.71/0.90 484[0:Res:95.2,191.0] ordinal(succ(skc14)) ordinal(skc14) || -> ordinal_subset(skc14,succ(skc14))* in(skc14,skc14). % 0.71/0.90 494[1:SSi:484.1,484.0,2.0,119.0,118.0,351.0,115.0,114.0,116.0] || -> ordinal_subset(skc14,succ(skc14))* in(skc14,skc14). % 0.71/0.90 505[0:Res:86.1,96.1] || subset(u,v)*+ in(w,u)* -> element(w,v)*. % 0.71/0.90 508[3:Spt:494.1] || -> in(skc14,skc14)*. % 0.71/0.90 511[3:Res:508.0,81.0] || in(skc14,skc14)* -> . % 0.71/0.90 513[3:MRR:511.0,508.0] || -> . % 0.71/0.90 514[3:Spt:513.0,494.1,508.0] || in(skc14,skc14)* -> . % 0.71/0.90 515[3:Spt:513.0,494.0] || -> ordinal_subset(skc14,succ(skc14))*. % 0.71/0.90 517[0:Res:98.3,90.0] ordinal(u) ordinal(v) || ordinal_subset(v,u)* -> proper_subset(v,u) equal(v,u). % 0.71/0.90 573[0:Res:108.2,90.0] ordinal(u) || ordinal_subset(skc14,u)* -> proper_subset(skc14,u) equal(skc14,u). % 0.71/0.90 615[0:Res:103.4,333.0] ordinal(u) ordinal(u) being_limit_ordinal(u) || in(u,u)* -> . % 0.71/0.90 618[0:Obv:615.0] ordinal(u) being_limit_ordinal(u) || in(u,u)* -> . % 0.71/0.90 686[0:Res:95.2,107.1] ordinal(succ(skc14)) ordinal(u) ordinal(u) || -> ordinal_subset(u,succ(skc14))* in(skc14,u). % 0.71/0.90 695[0:Obv:686.1] ordinal(succ(skc14)) ordinal(u) || -> ordinal_subset(u,succ(skc14))* in(skc14,u). % 0.71/0.90 696[0:SSi:695.0,115.0,114.0,116.0] ordinal(u) || -> ordinal_subset(u,succ(skc14))* in(skc14,u). % 0.71/0.90 698[0:Res:696.1,102.2] ordinal(succ(u)) ordinal(succ(skc14)) ordinal(u) || -> in(skc14,succ(u))* in(u,succ(skc14))*. % 0.71/0.90 701[0:SSi:698.1,698.0,115.1,114.1,116.1,69.0,68.0,70.0] ordinal(u) || -> in(skc14,succ(u))* in(u,succ(skc14))*. % 0.71/0.90 845[0:Res:75.1,505.0] || proper_subset(u,v)*+ in(w,u)* -> element(w,v)*. % 0.71/0.90 846[0:Res:123.2,505.0] ordinal(u) || ordinal_subset(u,skc14)*+ in(v,u)* -> element(v,skc14)*. % 0.71/0.90 916[0:Res:701.2,333.0] ordinal(succ(succ(skc14))) || -> in(skc14,succ(succ(succ(skc14))))*. % 0.71/0.90 919[0:SSi:916.0,69.0,115.0,114.0,116.1,68.0,115.0,114.0,116.1,70.0,115.0,114.0,116.1] || -> in(skc14,succ(succ(succ(skc14))))*. % 0.71/0.90 960[0:Res:120.3,618.2] ordinal(succ(skc14)) being_limit_ordinal(succ(skc14)) ordinal(succ(skc14)) being_limit_ordinal(succ(skc14)) || in(skc14,succ(skc14))* -> . % 0.71/0.90 965[0:Obv:960.1] ordinal(succ(skc14)) being_limit_ordinal(succ(skc14)) || in(skc14,succ(skc14))* -> . % 0.71/0.90 966[0:SSi:965.0,115.0,114.0,116.0] being_limit_ordinal(succ(skc14)) || in(skc14,succ(skc14))* -> . % 0.71/0.90 967[0:MRR:966.1,56.0] being_limit_ordinal(succ(skc14)) || -> . % 0.71/0.90 1023[0:Res:110.2,517.2] ordinal(u) ordinal(u) ordinal(skc14) || -> ordinal_subset(u,skc14)* proper_subset(skc14,u) equal(skc14,u). % 0.71/0.90 1026[0:Res:101.3,517.2] ordinal(u) ordinal(v) ordinal(u) ordinal(succ(v)) || in(v,u) -> proper_subset(succ(v),u)* equal(succ(v),u). % 0.71/0.90 1034[3:Res:515.0,517.2] ordinal(succ(skc14)) ordinal(skc14) || -> proper_subset(skc14,succ(skc14))* equal(succ(skc14),skc14). % 0.71/0.90 1046[3:SSi:1034.1,1034.0,2.0,119.0,118.0,351.0,115.0,114.0,116.0] || -> proper_subset(skc14,succ(skc14))* equal(succ(skc14),skc14). % 0.71/0.90 1051[0:Obv:1023.0] ordinal(u) ordinal(skc14) || -> ordinal_subset(u,skc14)* proper_subset(skc14,u) equal(skc14,u). % 0.71/0.90 1052[1:SSi:1051.1,2.0,119.0,118.0,351.0] ordinal(u) || -> ordinal_subset(u,skc14)* proper_subset(skc14,u) equal(skc14,u). % 0.71/0.90 1079[0:Obv:1026.0] ordinal(u) ordinal(v) ordinal(succ(u)) || in(u,v) -> proper_subset(succ(u),v)* equal(succ(u),v). % 0.71/0.93 1080[0:SSi:1079.2,69.1,68.1,70.1] ordinal(u) ordinal(v) || in(u,v) -> proper_subset(succ(u),v)* equal(succ(u),v). % 0.71/0.93 1379[4:Spt:1046.1] || -> equal(succ(skc14),skc14)**. % 0.71/0.93 1394[4:Rew:1379.0,919.0] || -> in(skc14,succ(succ(skc14)))*. % 0.71/0.93 1418[4:Rew:1379.0,1394.0,1379.0,1394.0] || -> in(skc14,skc14)*. % 0.71/0.93 1419[4:MRR:1418.0,514.0] || -> . % 0.71/0.93 1423[4:Spt:1419.0,1046.1,1379.0] || equal(succ(skc14),skc14)** -> . % 0.71/0.93 1424[4:Spt:1419.0,1046.0] || -> proper_subset(skc14,succ(skc14))*. % 0.71/0.93 2730[4:Res:1424.0,845.0] || in(u,skc14) -> element(u,succ(skc14))*. % 0.71/0.93 2736[4:Res:2730.1,87.0] || in(u,skc14) -> empty(succ(skc14)) in(u,succ(skc14))*. % 0.71/0.93 2737[4:MRR:2736.1,281.0] || in(u,skc14) -> in(u,succ(skc14))*. % 0.71/0.93 2760[1:Res:1052.1,517.2] ordinal(u) ordinal(skc14) ordinal(u) || -> proper_subset(skc14,u)* equal(skc14,u) proper_subset(u,skc14)* equal(u,skc14). % 0.71/0.93 2767[1:Obv:2760.4] ordinal(skc14) ordinal(u) || -> proper_subset(skc14,u)* proper_subset(u,skc14)* equal(u,skc14). % 0.71/0.93 2768[1:SSi:2767.0,351.0,118.0,119.0,2.0] ordinal(u) || -> proper_subset(skc14,u)* proper_subset(u,skc14)* equal(u,skc14). % 0.71/0.93 2773[4:Res:2737.1,94.1] ordinal(succ(skc14)) || in(succ(skf3(succ(skc14))),skc14)* -> being_limit_ordinal(succ(skc14)). % 0.71/0.93 2775[4:SSi:2773.0,69.0,351.0,118.0,119.0,2.1,68.0,351.0,118.0,119.0,2.1,70.0,351.0,118.0,119.0,2.1] || in(succ(skf3(succ(skc14))),skc14)* -> being_limit_ordinal(succ(skc14)). % 0.71/0.93 2776[4:MRR:2775.1,967.0] || in(succ(skf3(succ(skc14))),skc14)* -> . % 0.71/0.93 3010[1:Res:2768.2,125.1] ordinal(u) epsilon_transitive(u) || -> proper_subset(skc14,u)* equal(u,skc14) in(u,skc14). % 0.71/0.93 3020[1:SSi:3010.1,58.1] ordinal(u) || -> proper_subset(skc14,u)* equal(u,skc14) in(u,skc14). % 0.71/0.93 3156[1:Res:3020.1,100.2] ordinal(u) ordinal(u) epsilon_transitive(skc14) || -> equal(u,skc14) in(u,skc14)* in(skc14,u)*. % 0.71/0.93 3162[1:Obv:3156.0] ordinal(u) epsilon_transitive(skc14) || -> equal(u,skc14) in(u,skc14)* in(skc14,u)*. % 0.71/0.93 3163[1:SSi:3162.1,351.0,118.0,119.0,2.0] ordinal(u) || -> equal(u,skc14) in(u,skc14)* in(skc14,u)*. % 0.71/0.93 3199[2:Res:3163.2,362.0] ordinal(succ(skf3(skc14))) || -> equal(succ(skf3(skc14)),skc14) in(skc14,succ(skf3(skc14)))*. % 0.71/0.93 3200[4:Res:3163.2,2776.0] ordinal(succ(skf3(succ(skc14)))) || -> equal(succ(skf3(succ(skc14))),skc14) in(skc14,succ(skf3(succ(skc14))))*. % 0.71/0.93 3208[2:SSi:3199.0,69.0,51.0,351.0,118.0,119.0,2.1,68.0,51.0,351.0,118.0,119.0,2.1,70.0,51.0,351.0,118.0,119.0,2.1] || -> equal(succ(skf3(skc14)),skc14) in(skc14,succ(skf3(skc14)))*. % 0.71/0.93 3209[4:SSi:3200.0,69.0,51.0,69.0,351.0,118.1,119.0,2.0,68.0,351.0,118.1,119.0,2.0,70.0,351.0,118.1,119.0,2.1,68.0,51.0,69.0,351.0,118.1,119.0,2.0,68.0,351.0,118.1,119.0,2.0,70.0,351.0,118.1,119.0,2.1,70.0,51.0,69.0,351.0,118.1,119.0,2.0,68.0,351.0,118.1,119.0,2.0,70.0,351.0,118.1,119.0,2.1] || -> equal(succ(skf3(succ(skc14))),skc14) in(skc14,succ(skf3(succ(skc14))))*. % 0.71/0.93 3211[5:Spt:3208.0] || -> equal(succ(skf3(skc14)),skc14)**. % 0.71/0.93 3238[5:SpL:3211.0,92.2] SkP0(u) ordinal(skf3(skc14)) || equal(u,skc14)* -> . % 0.71/0.93 3241[5:SSi:3238.1,51.0,351.0,118.0,119.0,2.0] SkP0(u) || equal(u,skc14)* -> . % 0.71/0.93 3249[5:EmS:3241.0,351.0] || equal(skc14,skc14)* -> . % 0.71/0.93 3250[5:Obv:3249.0] || -> . % 0.71/0.93 3251[5:Spt:3250.0,3208.0,3211.0] || equal(succ(skf3(skc14)),skc14)** -> . % 0.71/0.93 3252[5:Spt:3250.0,3208.1] || -> in(skc14,succ(skf3(skc14)))*. % 0.71/0.93 3279[0:Res:110.1,846.1] ordinal(u) ordinal(u) || in(v,u)* -> ordinal_subset(skc14,u)* element(v,skc14)*. % 0.71/0.93 3284[0:Obv:3279.0] ordinal(u) || in(v,u)*+ -> ordinal_subset(skc14,u)* element(v,skc14)*. % 0.71/0.93 3292[6:Spt:3209.0] || -> equal(succ(skf3(succ(skc14))),skc14)**. % 0.71/0.93 3322[6:SpL:3292.0,94.1] ordinal(succ(skc14)) || in(skc14,succ(skc14))* -> being_limit_ordinal(succ(skc14)). % 0.71/0.93 3326[6:SSi:3322.0,69.0,351.0,118.0,119.0,2.1,68.0,351.0,118.0,119.0,2.1,70.0,351.0,118.0,119.0,2.1] || in(skc14,succ(skc14))* -> being_limit_ordinal(succ(skc14)). % 0.71/0.93 3327[6:MRR:3326.0,3326.1,56.0,967.0] || -> . % 0.71/0.93 3334[6:Spt:3327.0,3209.0,3292.0] || equal(succ(skf3(succ(skc14))),skc14)** -> . % 0.71/0.93 3335[6:Spt:3327.0,3209.1] || -> in(skc14,succ(skf3(succ(skc14))))*. % 0.71/0.93 4502[5:Res:3252.0,3284.1] ordinal(succ(skf3(skc14))) || -> ordinal_subset(skc14,succ(skf3(skc14)))* element(skc14,skc14). % 0.71/0.93 4506[5:SSi:4502.0,69.0,51.0,351.0,118.0,119.0,2.1,68.0,51.0,351.0,118.0,119.0,2.1,70.0,51.0,351.0,118.0,119.0,2.1] || -> ordinal_subset(skc14,succ(skf3(skc14)))* element(skc14,skc14). % 0.71/0.93 4541[7:Spt:4506.0] || -> ordinal_subset(skc14,succ(skf3(skc14)))*. % 0.71/0.93 4545[7:Res:4541.0,573.1] ordinal(succ(skf3(skc14))) || -> proper_subset(skc14,succ(skf3(skc14)))* equal(succ(skf3(skc14)),skc14). % 0.71/0.93 4547[7:SSi:4545.0,69.0,51.0,351.0,118.0,119.0,2.1,68.0,51.0,351.0,118.0,119.0,2.1,70.0,51.0,351.0,118.0,119.0,2.1] || -> proper_subset(skc14,succ(skf3(skc14)))* equal(succ(skf3(skc14)),skc14). % 0.71/0.93 4548[7:MRR:4547.1,3251.0] || -> proper_subset(skc14,succ(skf3(skc14)))*. % 0.71/0.93 4554[7:Res:4548.0,82.0] || proper_subset(succ(skf3(skc14)),skc14)* -> . % 0.71/0.93 4564[7:Res:1080.3,4554.0] ordinal(skf3(skc14)) ordinal(skc14) || in(skf3(skc14),skc14)* -> equal(succ(skf3(skc14)),skc14). % 0.71/0.93 4567[7:SSi:4564.1,4564.0,351.0,118.0,119.0,2.0,51.0,351.0,118.0,119.0,2.0] || in(skf3(skc14),skc14)* -> equal(succ(skf3(skc14)),skc14). % 0.71/0.93 4568[7:MRR:4567.0,4567.1,361.0,3251.0] || -> . % 0.71/0.93 4569[7:Spt:4568.0,4506.0,4541.0] || ordinal_subset(skc14,succ(skf3(skc14)))* -> . % 0.71/0.93 4570[7:Spt:4568.0,4506.1] || -> element(skc14,skc14)*. % 0.71/0.93 4571[7:Res:4570.0,87.0] || -> empty(skc14) in(skc14,skc14)*. % 0.71/0.93 4572[7:MRR:4571.0,4571.1,364.0,514.0] || -> . % 0.71/0.93 % SZS output end Refutation % 0.71/0.93 Formulae used in the proof : t42_ordinal1 rc3_ordinal1 t41_ordinal1 t10_ordinal1 cc1_ordinal1 fc3_ordinal1 reflexivity_r1_ordinal1 d8_xboole_0 t7_boole antisymmetry_r2_hidden antisymmetry_r2_xboole_0 t3_subset t2_subset connectedness_r1_ordinal1 t4_subset redefinition_r1_ordinal1 t21_ordinal1 t33_ordinal1 % 0.71/0.93 %------------------------------------------------------------------------------