%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU238+3 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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.69s 0.91s % Output : Refutation 0.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU238+3 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n005.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 : Sun Jun 19 09:34:23 EDT 2022 % 0.13/0.34 % CPUTime : % 0.69/0.91 % 0.69/0.91 SPASS V 3.9 % 0.69/0.91 SPASS beiseite: Proof found. % 0.69/0.91 % SZS status Theorem % 0.69/0.91 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.69/0.91 SPASS derived 3537 clauses, backtracked 474 clauses, performed 24 splits and kept 1527 clauses. % 0.69/0.91 SPASS allocated 119565 KBytes. % 0.69/0.91 SPASS spent 0:00:00.50 on the problem. % 0.69/0.91 0:00:00.04 for the input. % 0.69/0.91 0:00:00.03 for the FLOTTER CNF translation. % 0.69/0.91 0:00:00.06 for inferences. % 0.69/0.91 0:00:00.01 for the backtracking. % 0.69/0.91 0:00:00.31 for the reduction. % 0.69/0.91 % 0.69/0.91 % 0.69/0.91 Here is a proof with depth 12, length 161 : % 0.69/0.91 % SZS output start Refutation % 0.69/0.91 1[0:Inp] || -> ordinal(skc16)*. % 0.69/0.91 2[0:Inp] || -> ordinal(skc15)*. % 0.69/0.91 54[0:Inp] || -> ordinal(skf3(u))*. % 0.69/0.91 55[0:Inp] || -> SkP0(skc15) being_limit_ordinal(skc15)*. % 0.69/0.91 59[0:Inp] || -> in(u,succ(u))*. % 0.69/0.91 61[0:Inp] ordinal(u) || -> epsilon_transitive(u)*. % 0.69/0.91 62[0:Inp] ordinal(u) || -> epsilon_connected(u)*. % 0.69/0.91 69[0:Inp] || -> SkP0(skc15) equal(succ(skc16),skc15)**. % 0.69/0.91 70[0:Inp] SkP0(u) being_limit_ordinal(u) || -> . % 0.69/0.91 71[0:Inp] ordinal(u) || -> epsilon_transitive(succ(u))*. % 0.69/0.91 72[0:Inp] ordinal(u) || -> epsilon_connected(succ(u))*. % 0.69/0.91 73[0:Inp] ordinal(u) || -> ordinal(succ(u))*. % 0.69/0.91 74[0:Inp] ordinal(u) || -> ordinal_subset(u,u)*. % 0.69/0.91 78[0:Inp] || proper_subset(u,v) -> subset(u,v)*. % 0.69/0.91 83[0:Inp] empty(u) || in(v,u)* -> . % 0.69/0.91 84[0:Inp] || in(u,v)*+ in(v,u)* -> . % 0.69/0.91 85[0:Inp] || proper_subset(u,v)*+ proper_subset(v,u)* -> . % 0.69/0.91 89[0:Inp] || subset(u,v) -> element(u,powerset(v))*. % 0.69/0.91 90[0:Inp] || element(u,v)* -> empty(v) in(u,v). % 0.69/0.91 91[0:Inp] ordinal(u) || -> being_limit_ordinal(u) in(skf3(u),u)*. % 0.69/0.91 93[0:Inp] || subset(u,v)* -> proper_subset(u,v) equal(u,v). % 0.69/0.91 95[0:Inp] SkP0(u) ordinal(v) || equal(u,succ(v))* -> . % 0.69/0.91 97[0:Inp] ordinal(u) || in(succ(skf3(u)),u)* -> being_limit_ordinal(u). % 0.69/0.91 98[0:Inp] ordinal(u) ordinal(v) || -> ordinal_subset(u,v)* ordinal_subset(v,u)*. % 0.69/0.91 99[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 0.69/0.91 101[0:Inp] ordinal(u) ordinal(v) || ordinal_subset(v,u) -> subset(v,u)*. % 0.69/0.91 103[0:Inp] ordinal(u) epsilon_transitive(v) || proper_subset(v,u)* -> in(v,u). % 0.69/0.91 104[0:Inp] ordinal(u) ordinal(v) || in(v,u) -> ordinal_subset(succ(v),u)*. % 0.69/0.91 105[0:Inp] ordinal(u) ordinal(v) || ordinal_subset(succ(v),u)* -> in(v,u). % 0.69/0.91 106[0:Inp] ordinal(u) ordinal(v) being_limit_ordinal(u) || in(v,u) -> in(succ(v),u)*. % 0.69/0.91 108[0:Res:2.0,106.2] ordinal(u) being_limit_ordinal(skc15) || in(u,skc15) -> in(succ(u),skc15)*. % 0.69/0.91 110[0:Res:2.0,105.0] ordinal(u) || ordinal_subset(succ(skc15),u)* -> in(skc15,u). % 0.69/0.91 111[0:Res:2.0,101.0] ordinal(u) || ordinal_subset(skc15,u) -> subset(skc15,u)*. % 0.69/0.91 113[0:Res:2.0,98.0] ordinal(u) || -> ordinal_subset(u,skc15)* ordinal_subset(skc15,u)*. % 0.69/0.91 115[0:Res:2.0,97.0] || in(succ(skf3(skc15)),skc15)* -> being_limit_ordinal(skc15). % 0.69/0.91 116[0:Res:2.0,91.0] || -> being_limit_ordinal(skc15) in(skf3(skc15),skc15)*. % 0.69/0.91 117[0:Res:2.0,71.0] || -> epsilon_transitive(succ(skc15))*. % 0.69/0.91 118[0:Res:2.0,72.0] || -> epsilon_connected(succ(skc15))*. % 0.69/0.91 119[0:Res:2.0,73.0] || -> ordinal(succ(skc15))*. % 0.69/0.91 120[0:Res:2.0,74.0] || -> ordinal_subset(skc15,skc15)*. % 0.69/0.91 121[0:Res:2.0,61.0] || -> epsilon_transitive(skc15)*. % 0.69/0.91 122[0:Res:2.0,62.0] || -> epsilon_connected(skc15)*. % 0.69/0.91 123[0:Res:2.0,106.1] ordinal(u) being_limit_ordinal(u) || in(skc15,u) -> in(succ(skc15),u)*. % 0.69/0.91 125[0:Res:2.0,105.1] ordinal(u) || ordinal_subset(succ(u),skc15)* -> in(u,skc15). % 0.69/0.91 126[0:Res:2.0,101.1] ordinal(u) || ordinal_subset(u,skc15) -> subset(u,skc15)*. % 0.69/0.91 128[0:Res:2.0,103.1] epsilon_transitive(u) || proper_subset(u,skc15)* -> in(u,skc15). % 0.69/0.91 136[0:Res:1.0,95.0] SkP0(u) || equal(u,succ(skc16))* -> . % 0.69/0.91 165[0:Res:1.0,108.1] being_limit_ordinal(skc15) || in(skc16,skc15) -> in(succ(skc16),skc15)*. % 0.69/0.91 170[0:Res:1.0,125.0] || ordinal_subset(succ(skc16),skc15)* -> in(skc16,skc15). % 0.69/0.91 188[0:Res:2.0,123.1] being_limit_ordinal(skc15) || in(skc15,skc15) -> in(succ(skc15),skc15)*. % 0.69/0.91 194[0:Res:2.0,125.0] || ordinal_subset(succ(skc15),skc15)* -> in(skc15,skc15). % 0.69/0.91 212[1:Spt:69.1] || -> equal(succ(skc16),skc15)**. % 0.69/0.91 218[1:Rew:212.0,170.0] || ordinal_subset(skc15,skc15)* -> in(skc16,skc15). % 0.69/0.91 222[1:Rew:212.0,136.1] SkP0(u) || equal(u,skc15)* -> . % 0.69/0.91 224[1:Rew:212.0,165.2] being_limit_ordinal(skc15) || in(skc16,skc15)* -> in(skc15,skc15). % 0.69/0.91 226[1:MRR:218.0,120.0] || -> in(skc16,skc15)*. % 0.69/0.91 227[1:MRR:224.1,226.0] being_limit_ordinal(skc15) || -> in(skc15,skc15)*. % 0.69/0.91 228[1:MRR:188.1,227.1] being_limit_ordinal(skc15) || -> in(succ(skc15),skc15)*. % 0.69/0.91 230[2:Spt:55.1] || -> being_limit_ordinal(skc15)*. % 0.69/0.91 233[2:MRR:228.0,230.0] || -> in(succ(skc15),skc15)*. % 0.69/0.91 284[0:Res:59.0,83.1] empty(succ(u)) || -> . % 0.69/0.91 336[0:Res:59.0,84.0] || in(succ(u),u)* -> . % 0.69/0.91 343[2:UnC:336.0,233.0] || -> . % 0.69/0.91 344[2:Spt:343.0,55.1,230.0] || being_limit_ordinal(skc15)* -> . % 0.69/0.91 345[2:Spt:343.0,55.0] || -> SkP0(skc15)*. % 0.69/0.91 351[2:EmS:222.0,345.0] || equal(skc15,skc15)* -> . % 0.69/0.91 352[2:Obv:351.0] || -> . % 0.69/0.91 353[1:Spt:352.0,69.1,212.0] || equal(succ(skc16),skc15)** -> . % 0.69/0.91 354[1:Spt:352.0,69.0] || -> SkP0(skc15)*. % 0.69/0.91 357[2:Spt:116.0] || -> being_limit_ordinal(skc15)*. % 0.69/0.91 362[2:EmS:70.0,70.1,354.0,357.0] || -> . % 0.69/0.91 363[2:Spt:362.0,116.0,357.0] || being_limit_ordinal(skc15)* -> . % 0.69/0.91 364[2:Spt:362.0,116.1] || -> in(skf3(skc15),skc15)*. % 0.69/0.91 365[2:MRR:115.1,363.0] || in(succ(skf3(skc15)),skc15)* -> . % 0.69/0.91 367[2:Res:364.0,83.1] empty(skc15) || -> . % 0.69/0.91 482[0:Res:98.2,194.0] ordinal(succ(skc15)) ordinal(skc15) || -> ordinal_subset(skc15,succ(skc15))* in(skc15,skc15). % 0.69/0.91 492[1:SSi:482.1,482.0,2.0,122.0,121.0,354.0,118.0,117.0,119.0] || -> ordinal_subset(skc15,succ(skc15))* in(skc15,skc15). % 0.69/0.91 503[0:Res:89.1,99.1] || subset(u,v)*+ in(w,u)* -> element(w,v)*. % 0.69/0.91 506[3:Spt:492.1] || -> in(skc15,skc15)*. % 0.69/0.91 509[3:Res:506.0,84.0] || in(skc15,skc15)* -> . % 0.69/0.91 511[3:MRR:509.0,506.0] || -> . % 0.69/0.91 512[3:Spt:511.0,492.1,506.0] || in(skc15,skc15)* -> . % 0.69/0.91 513[3:Spt:511.0,492.0] || -> ordinal_subset(skc15,succ(skc15))*. % 0.69/0.91 515[0:Res:101.3,93.0] ordinal(u) ordinal(v) || ordinal_subset(v,u)* -> proper_subset(v,u) equal(v,u). % 0.69/0.91 571[0:Res:111.2,93.0] ordinal(u) || ordinal_subset(skc15,u)* -> proper_subset(skc15,u) equal(skc15,u). % 0.69/0.91 613[0:Res:106.4,336.0] ordinal(u) ordinal(u) being_limit_ordinal(u) || in(u,u)* -> . % 0.69/0.91 616[0:Obv:613.0] ordinal(u) being_limit_ordinal(u) || in(u,u)* -> . % 0.69/0.91 684[0:Res:98.2,110.1] ordinal(succ(skc15)) ordinal(u) ordinal(u) || -> ordinal_subset(u,succ(skc15))* in(skc15,u). % 0.69/0.91 693[0:Obv:684.1] ordinal(succ(skc15)) ordinal(u) || -> ordinal_subset(u,succ(skc15))* in(skc15,u). % 0.69/0.91 694[0:SSi:693.0,118.0,117.0,119.0] ordinal(u) || -> ordinal_subset(u,succ(skc15))* in(skc15,u). % 0.69/0.91 696[0:Res:694.1,105.2] ordinal(succ(u)) ordinal(succ(skc15)) ordinal(u) || -> in(skc15,succ(u))* in(u,succ(skc15))*. % 0.69/0.91 699[0:SSi:696.1,696.0,118.1,117.1,119.1,72.0,71.0,73.0] ordinal(u) || -> in(skc15,succ(u))* in(u,succ(skc15))*. % 0.69/0.91 843[0:Res:78.1,503.0] || proper_subset(u,v)*+ in(w,u)* -> element(w,v)*. % 0.69/0.91 844[0:Res:126.2,503.0] ordinal(u) || ordinal_subset(u,skc15)*+ in(v,u)* -> element(v,skc15)*. % 0.69/0.91 914[0:Res:699.2,336.0] ordinal(succ(succ(skc15))) || -> in(skc15,succ(succ(succ(skc15))))*. % 0.69/0.91 917[0:SSi:914.0,72.0,118.0,117.0,119.1,71.0,118.0,117.0,119.1,73.0,118.0,117.0,119.1] || -> in(skc15,succ(succ(succ(skc15))))*. % 0.69/0.91 958[0:Res:123.3,616.2] ordinal(succ(skc15)) being_limit_ordinal(succ(skc15)) ordinal(succ(skc15)) being_limit_ordinal(succ(skc15)) || in(skc15,succ(skc15))* -> . % 0.69/0.91 963[0:Obv:958.1] ordinal(succ(skc15)) being_limit_ordinal(succ(skc15)) || in(skc15,succ(skc15))* -> . % 0.69/0.91 964[0:SSi:963.0,118.0,117.0,119.0] being_limit_ordinal(succ(skc15)) || in(skc15,succ(skc15))* -> . % 0.69/0.91 965[0:MRR:964.1,59.0] being_limit_ordinal(succ(skc15)) || -> . % 0.69/0.91 1021[0:Res:113.2,515.2] ordinal(u) ordinal(u) ordinal(skc15) || -> ordinal_subset(u,skc15)* proper_subset(skc15,u) equal(skc15,u). % 0.69/0.91 1024[0:Res:104.3,515.2] ordinal(u) ordinal(v) ordinal(u) ordinal(succ(v)) || in(v,u) -> proper_subset(succ(v),u)* equal(succ(v),u). % 0.69/0.91 1032[3:Res:513.0,515.2] ordinal(succ(skc15)) ordinal(skc15) || -> proper_subset(skc15,succ(skc15))* equal(succ(skc15),skc15). % 0.69/0.91 1044[3:SSi:1032.1,1032.0,2.0,122.0,121.0,354.0,118.0,117.0,119.0] || -> proper_subset(skc15,succ(skc15))* equal(succ(skc15),skc15). % 0.69/0.91 1049[0:Obv:1021.0] ordinal(u) ordinal(skc15) || -> ordinal_subset(u,skc15)* proper_subset(skc15,u) equal(skc15,u). % 0.69/0.91 1050[1:SSi:1049.1,2.0,122.0,121.0,354.0] ordinal(u) || -> ordinal_subset(u,skc15)* proper_subset(skc15,u) equal(skc15,u). % 0.69/0.91 1077[0:Obv:1024.0] ordinal(u) ordinal(v) ordinal(succ(u)) || in(u,v) -> proper_subset(succ(u),v)* equal(succ(u),v). % 0.77/0.94 1078[0:SSi:1077.2,72.1,71.1,73.1] ordinal(u) ordinal(v) || in(u,v) -> proper_subset(succ(u),v)* equal(succ(u),v). % 0.77/0.94 1377[4:Spt:1044.1] || -> equal(succ(skc15),skc15)**. % 0.77/0.94 1392[4:Rew:1377.0,917.0] || -> in(skc15,succ(succ(skc15)))*. % 0.77/0.94 1416[4:Rew:1377.0,1392.0,1377.0,1392.0] || -> in(skc15,skc15)*. % 0.77/0.94 1417[4:MRR:1416.0,512.0] || -> . % 0.77/0.94 1421[4:Spt:1417.0,1044.1,1377.0] || equal(succ(skc15),skc15)** -> . % 0.77/0.94 1422[4:Spt:1417.0,1044.0] || -> proper_subset(skc15,succ(skc15))*. % 0.77/0.94 2728[4:Res:1422.0,843.0] || in(u,skc15) -> element(u,succ(skc15))*. % 0.77/0.94 2734[4:Res:2728.1,90.0] || in(u,skc15) -> empty(succ(skc15)) in(u,succ(skc15))*. % 0.77/0.94 2735[4:MRR:2734.1,284.0] || in(u,skc15) -> in(u,succ(skc15))*. % 0.77/0.94 2758[1:Res:1050.1,515.2] ordinal(u) ordinal(skc15) ordinal(u) || -> proper_subset(skc15,u)* equal(skc15,u) proper_subset(u,skc15)* equal(u,skc15). % 0.77/0.94 2765[1:Obv:2758.4] ordinal(skc15) ordinal(u) || -> proper_subset(skc15,u)* proper_subset(u,skc15)* equal(u,skc15). % 0.77/0.94 2766[1:SSi:2765.0,354.0,121.0,122.0,2.0] ordinal(u) || -> proper_subset(skc15,u)* proper_subset(u,skc15)* equal(u,skc15). % 0.77/0.94 2771[4:Res:2735.1,97.1] ordinal(succ(skc15)) || in(succ(skf3(succ(skc15))),skc15)* -> being_limit_ordinal(succ(skc15)). % 0.77/0.94 2773[4:SSi:2771.0,72.0,354.0,121.0,122.0,2.1,71.0,354.0,121.0,122.0,2.1,73.0,354.0,121.0,122.0,2.1] || in(succ(skf3(succ(skc15))),skc15)* -> being_limit_ordinal(succ(skc15)). % 0.77/0.94 2774[4:MRR:2773.1,965.0] || in(succ(skf3(succ(skc15))),skc15)* -> . % 0.77/0.94 3008[1:Res:2766.2,128.1] ordinal(u) epsilon_transitive(u) || -> proper_subset(skc15,u)* equal(u,skc15) in(u,skc15). % 0.77/0.94 3018[1:SSi:3008.1,61.1] ordinal(u) || -> proper_subset(skc15,u)* equal(u,skc15) in(u,skc15). % 0.77/0.94 3154[1:Res:3018.1,103.2] ordinal(u) ordinal(u) epsilon_transitive(skc15) || -> equal(u,skc15) in(u,skc15)* in(skc15,u)*. % 0.77/0.94 3160[1:Obv:3154.0] ordinal(u) epsilon_transitive(skc15) || -> equal(u,skc15) in(u,skc15)* in(skc15,u)*. % 0.77/0.94 3161[1:SSi:3160.1,354.0,121.0,122.0,2.0] ordinal(u) || -> equal(u,skc15) in(u,skc15)* in(skc15,u)*. % 0.77/0.94 3197[2:Res:3161.2,365.0] ordinal(succ(skf3(skc15))) || -> equal(succ(skf3(skc15)),skc15) in(skc15,succ(skf3(skc15)))*. % 0.77/0.94 3198[4:Res:3161.2,2774.0] ordinal(succ(skf3(succ(skc15)))) || -> equal(succ(skf3(succ(skc15))),skc15) in(skc15,succ(skf3(succ(skc15))))*. % 0.77/0.94 3206[2:SSi:3197.0,72.0,54.0,354.0,121.0,122.0,2.1,71.0,54.0,354.0,121.0,122.0,2.1,73.0,54.0,354.0,121.0,122.0,2.1] || -> equal(succ(skf3(skc15)),skc15) in(skc15,succ(skf3(skc15)))*. % 0.77/0.94 3207[4:SSi:3198.0,72.0,54.0,72.0,354.0,121.1,122.0,2.0,71.0,354.0,121.1,122.0,2.0,73.0,354.0,121.1,122.0,2.1,71.0,54.0,72.0,354.0,121.1,122.0,2.0,71.0,354.0,121.1,122.0,2.0,73.0,354.0,121.1,122.0,2.1,73.0,54.0,72.0,354.0,121.1,122.0,2.0,71.0,354.0,121.1,122.0,2.0,73.0,354.0,121.1,122.0,2.1] || -> equal(succ(skf3(succ(skc15))),skc15) in(skc15,succ(skf3(succ(skc15))))*. % 0.77/0.94 3209[5:Spt:3206.0] || -> equal(succ(skf3(skc15)),skc15)**. % 0.77/0.94 3236[5:SpL:3209.0,95.2] SkP0(u) ordinal(skf3(skc15)) || equal(u,skc15)* -> . % 0.77/0.94 3239[5:SSi:3236.1,54.0,354.0,121.0,122.0,2.0] SkP0(u) || equal(u,skc15)* -> . % 0.77/0.94 3247[5:EmS:3239.0,354.0] || equal(skc15,skc15)* -> . % 0.77/0.94 3248[5:Obv:3247.0] || -> . % 0.77/0.94 3249[5:Spt:3248.0,3206.0,3209.0] || equal(succ(skf3(skc15)),skc15)** -> . % 0.77/0.94 3250[5:Spt:3248.0,3206.1] || -> in(skc15,succ(skf3(skc15)))*. % 0.77/0.94 3277[0:Res:113.1,844.1] ordinal(u) ordinal(u) || in(v,u)* -> ordinal_subset(skc15,u)* element(v,skc15)*. % 0.77/0.94 3282[0:Obv:3277.0] ordinal(u) || in(v,u)*+ -> ordinal_subset(skc15,u)* element(v,skc15)*. % 0.77/0.94 3290[6:Spt:3207.0] || -> equal(succ(skf3(succ(skc15))),skc15)**. % 0.77/0.94 3320[6:SpL:3290.0,97.1] ordinal(succ(skc15)) || in(skc15,succ(skc15))* -> being_limit_ordinal(succ(skc15)). % 0.77/0.94 3324[6:SSi:3320.0,72.0,354.0,121.0,122.0,2.1,71.0,354.0,121.0,122.0,2.1,73.0,354.0,121.0,122.0,2.1] || in(skc15,succ(skc15))* -> being_limit_ordinal(succ(skc15)). % 0.77/0.94 3325[6:MRR:3324.0,3324.1,59.0,965.0] || -> . % 0.77/0.94 3332[6:Spt:3325.0,3207.0,3290.0] || equal(succ(skf3(succ(skc15))),skc15)** -> . % 0.77/0.94 3333[6:Spt:3325.0,3207.1] || -> in(skc15,succ(skf3(succ(skc15))))*. % 0.77/0.94 4500[5:Res:3250.0,3282.1] ordinal(succ(skf3(skc15))) || -> ordinal_subset(skc15,succ(skf3(skc15)))* element(skc15,skc15). % 0.77/0.94 4504[5:SSi:4500.0,72.0,54.0,354.0,121.0,122.0,2.1,71.0,54.0,354.0,121.0,122.0,2.1,73.0,54.0,354.0,121.0,122.0,2.1] || -> ordinal_subset(skc15,succ(skf3(skc15)))* element(skc15,skc15). % 0.77/0.94 4539[7:Spt:4504.0] || -> ordinal_subset(skc15,succ(skf3(skc15)))*. % 0.77/0.94 4543[7:Res:4539.0,571.1] ordinal(succ(skf3(skc15))) || -> proper_subset(skc15,succ(skf3(skc15)))* equal(succ(skf3(skc15)),skc15). % 0.77/0.94 4545[7:SSi:4543.0,72.0,54.0,354.0,121.0,122.0,2.1,71.0,54.0,354.0,121.0,122.0,2.1,73.0,54.0,354.0,121.0,122.0,2.1] || -> proper_subset(skc15,succ(skf3(skc15)))* equal(succ(skf3(skc15)),skc15). % 0.77/0.94 4546[7:MRR:4545.1,3249.0] || -> proper_subset(skc15,succ(skf3(skc15)))*. % 0.77/0.94 4552[7:Res:4546.0,85.0] || proper_subset(succ(skf3(skc15)),skc15)* -> . % 0.77/0.94 4562[7:Res:1078.3,4552.0] ordinal(skf3(skc15)) ordinal(skc15) || in(skf3(skc15),skc15)* -> equal(succ(skf3(skc15)),skc15). % 0.77/0.94 4565[7:SSi:4562.1,4562.0,354.0,121.0,122.0,2.0,54.0,354.0,121.0,122.0,2.0] || in(skf3(skc15),skc15)* -> equal(succ(skf3(skc15)),skc15). % 0.77/0.94 4566[7:MRR:4565.0,4565.1,364.0,3249.0] || -> . % 0.77/0.94 4567[7:Spt:4566.0,4504.0,4539.0] || ordinal_subset(skc15,succ(skf3(skc15)))* -> . % 0.77/0.94 4568[7:Spt:4566.0,4504.1] || -> element(skc15,skc15)*. % 0.77/0.94 4569[7:Res:4568.0,90.0] || -> empty(skc15) in(skc15,skc15)*. % 0.77/0.94 4570[7:MRR:4569.0,4569.1,367.0,512.0] || -> . % 0.77/0.94 % SZS output end Refutation % 0.77/0.94 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.77/0.94 %------------------------------------------------------------------------------