%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU234+3 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:22 EDT 2022 % Result : Theorem 0.22s 0.52s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SEU234+3 : TPTP v8.1.0. Released v3.2.0. % 0.08/0.15 % Command : run_spass %d %s % 0.15/0.37 % Computer : n013.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 600 % 0.15/0.37 % DateTime : Sun Jun 19 12:43:59 EDT 2022 % 0.15/0.37 % CPUTime : % 0.22/0.52 % 0.22/0.52 SPASS V 3.9 % 0.22/0.52 SPASS beiseite: Proof found. % 0.22/0.52 % SZS status Theorem % 0.22/0.52 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.22/0.52 SPASS derived 394 clauses, backtracked 64 clauses, performed 9 splits and kept 303 clauses. % 0.22/0.52 SPASS allocated 98053 KBytes. % 0.22/0.52 SPASS spent 0:00:00.13 on the problem. % 0.22/0.52 0:00:00.04 for the input. % 0.22/0.52 0:00:00.04 for the FLOTTER CNF translation. % 0.22/0.52 0:00:00.01 for inferences. % 0.22/0.52 0:00:00.00 for the backtracking. % 0.22/0.52 0:00:00.03 for the reduction. % 0.22/0.52 % 0.22/0.52 % 0.22/0.52 Here is a proof with depth 8, length 92 : % 0.22/0.52 % SZS output start Refutation % 0.22/0.52 6[0:Inp] || -> relation_empty_yielding(empty_set)*. % 0.22/0.52 7[0:Inp] || -> function(empty_set)*. % 0.22/0.52 8[0:Inp] || -> one_to_one(empty_set)*. % 0.22/0.52 10[0:Inp] || -> epsilon_transitive(empty_set)*. % 0.22/0.52 11[0:Inp] || -> epsilon_connected(empty_set)*. % 0.22/0.52 12[0:Inp] || -> ordinal(empty_set)*. % 0.22/0.52 13[0:Inp] || -> empty(empty_set)*. % 0.22/0.52 14[0:Inp] || -> relation(empty_set)*. % 0.22/0.52 48[0:Inp] || ordinal(skc14)* -> . % 0.22/0.52 53[0:Inp] || -> element(skf7(u),u)*. % 0.22/0.52 60[0:Inp] empty(u) || -> ordinal(u)*. % 0.22/0.52 62[0:Inp] ordinal(u) || -> epsilon_connected(u)*. % 0.22/0.52 63[0:Inp] || in(u,skc14)* -> ordinal(u). % 0.22/0.52 64[0:Inp] || -> epsilon_transitive(u) in(skf4(u),u)*. % 0.22/0.52 65[0:Inp] || in(skf6(u),skf5(u))* -> . % 0.22/0.52 66[0:Inp] || -> epsilon_connected(u) in(skf6(u),u)*. % 0.22/0.52 67[0:Inp] || -> epsilon_connected(u) in(skf5(u),u)*. % 0.22/0.52 68[0:Inp] empty(u) || -> equal(u,empty_set)*. % 0.22/0.52 69[0:Inp] || in(u,skc14) -> subset(u,skc14)*. % 0.22/0.52 70[0:Inp] || subset(skf4(u),u)* -> epsilon_transitive(u). % 0.22/0.52 75[0:Inp] || equal(skf6(u),skf5(u))** -> epsilon_connected(u). % 0.22/0.52 76[0:Inp] || in(skf5(u),skf6(u))* -> epsilon_connected(u). % 0.22/0.52 77[0:Inp] epsilon_connected(u) epsilon_transitive(u) || -> ordinal(u)*. % 0.22/0.52 79[0:Inp] || subset(u,v) -> element(u,powerset(v))*. % 0.22/0.52 80[0:Inp] || element(u,v)* -> empty(v) in(u,v). % 0.22/0.52 84[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 0.22/0.52 85[0:Inp] empty(u) || in(v,w)* element(w,powerset(u))*+ -> . % 0.22/0.52 86[0:Inp] ordinal(u) ordinal(v) || -> in(u,v)* equal(v,u) in(v,u)*. % 0.22/0.52 89[0:Res:77.2,48.0] epsilon_connected(skc14) epsilon_transitive(skc14) || -> . % 0.22/0.52 91[0:Res:60.1,48.0] empty(skc14) || -> . % 0.22/0.52 126[0:Res:67.1,63.0] || -> epsilon_connected(skc14) ordinal(skf5(skc14))*. % 0.22/0.52 127[0:Res:66.1,63.0] || -> epsilon_connected(skc14) ordinal(skf6(skc14))*. % 0.22/0.52 128[1:Spt:126.0] || -> epsilon_connected(skc14)*. % 0.22/0.52 129[1:MRR:89.0,128.0] epsilon_transitive(skc14) || -> . % 0.22/0.52 133[0:Res:69.1,70.0] || in(skf4(skc14),skc14)* -> epsilon_transitive(skc14). % 0.22/0.52 134[1:MRR:133.0,133.1,64.1,129.0] || -> . % 0.22/0.52 135[1:Spt:134.0,126.0,128.0] || epsilon_connected(skc14)* -> . % 0.22/0.52 136[1:Spt:134.0,126.1] || -> ordinal(skf5(skc14))*. % 0.22/0.52 137[1:MRR:127.0,135.0] || -> ordinal(skf6(skc14))*. % 0.22/0.52 138[0:MRR:133.0,64.1] || -> epsilon_transitive(skc14)*. % 0.22/0.52 139[0:MRR:89.1,138.0] epsilon_connected(skc14) || -> . % 0.22/0.52 159[0:Res:53.0,80.0] || -> empty(u) in(skf7(u),u)*. % 0.22/0.52 171[0:Res:53.0,85.2] empty(u) || in(v,skf7(powerset(u)))* -> . % 0.22/0.52 177[0:Res:159.1,171.1] empty(u) || -> empty(skf7(powerset(u)))*. % 0.22/0.52 180[0:Res:79.1,84.1] || subset(u,v)*+ in(w,u)* -> element(w,v)*. % 0.22/0.52 182[0:EmS:68.0,177.1] empty(u) || -> equal(skf7(powerset(u)),empty_set)**. % 0.22/0.52 184[0:Rew:182.1,171.1] empty(u) || in(v,empty_set)* -> . % 0.22/0.52 192[0:EmS:184.0,13.0] || in(u,empty_set)* -> . % 0.22/0.52 195[0:Res:86.2,65.0] ordinal(skf6(u)) ordinal(skf5(u)) || -> equal(skf6(u),skf5(u)) in(skf5(u),skf6(u))*. % 0.22/0.52 208[0:Res:86.4,192.0] ordinal(empty_set) ordinal(u) || -> in(empty_set,u)* equal(u,empty_set). % 0.22/0.52 211[0:SSi:208.0,6.0,8.0,7.0,14.0,10.0,12.0,11.0,13.0] ordinal(u) || -> in(empty_set,u)* equal(u,empty_set). % 0.22/0.52 295[0:Res:69.1,180.0] || in(u,skc14)*+ in(v,u)* -> element(v,skc14)*. % 0.22/0.52 303[0:Res:67.1,295.0] || in(u,skf5(skc14))* -> epsilon_connected(skc14) element(u,skc14). % 0.22/0.52 309[0:MRR:303.1,139.0] || in(u,skf5(skc14))* -> element(u,skc14). % 0.22/0.52 314[0:Res:66.1,309.0] || -> epsilon_connected(skf5(skc14)) element(skf6(skf5(skc14)),skc14)*. % 0.22/0.52 316[0:Res:159.1,309.0] || -> empty(skf5(skc14)) element(skf7(skf5(skc14)),skc14)*. % 0.22/0.52 317[0:Res:211.1,309.0] ordinal(skf5(skc14)) || -> equal(skf5(skc14),empty_set) element(empty_set,skc14)*. % 0.22/0.52 319[1:SSi:317.0,136.0] || -> equal(skf5(skc14),empty_set) element(empty_set,skc14)*. % 0.22/0.52 321[2:Spt:319.0] || -> equal(skf5(skc14),empty_set)**. % 0.22/0.52 333[2:SpL:321.0,76.0] || in(empty_set,skf6(skc14))* -> epsilon_connected(skc14). % 0.22/0.52 336[2:MRR:333.1,139.0] || in(empty_set,skf6(skc14))* -> . % 0.22/0.52 353[2:Res:211.1,336.0] ordinal(skf6(skc14)) || -> equal(skf6(skc14),empty_set)**. % 0.22/0.52 354[2:SSi:353.0,137.0] || -> equal(skf6(skc14),empty_set)**. % 0.22/0.52 361[2:SpL:354.0,75.0] || equal(skf5(skc14),empty_set)** -> epsilon_connected(skc14). % 0.22/0.52 365[2:Rew:321.0,361.0] || equal(empty_set,empty_set) -> epsilon_connected(skc14)*. % 0.22/0.52 366[2:Obv:365.0] || -> epsilon_connected(skc14)*. % 0.22/0.52 367[2:MRR:366.0,139.0] || -> . % 0.22/0.52 368[2:Spt:367.0,319.0,321.0] || equal(skf5(skc14),empty_set)** -> . % 0.22/0.52 369[2:Spt:367.0,319.1] || -> element(empty_set,skc14)*. % 0.22/0.52 377[0:Res:316.1,80.0] || -> empty(skf5(skc14)) empty(skc14) in(skf7(skf5(skc14)),skc14)*. % 0.22/0.52 378[0:MRR:377.1,91.0] || -> empty(skf5(skc14)) in(skf7(skf5(skc14)),skc14)*. % 0.22/0.52 381[3:Spt:314.0] || -> epsilon_connected(skf5(skc14))*. % 0.22/0.52 394[0:Res:378.1,63.0] || -> empty(skf5(skc14)) ordinal(skf7(skf5(skc14)))*. % 0.22/0.52 398[4:Spt:394.0] || -> empty(skf5(skc14))*. % 0.22/0.52 400[4:EmS:68.0,398.0] || -> equal(skf5(skc14),empty_set)**. % 0.22/0.52 402[4:MRR:400.0,368.0] || -> . % 0.22/0.52 403[4:Spt:402.0,394.0,398.0] || empty(skf5(skc14))* -> . % 0.22/0.52 404[4:Spt:402.0,394.1] || -> ordinal(skf7(skf5(skc14)))*. % 0.22/0.52 441[1:SoR:195.0,137.0] ordinal(skf5(skc14)) || -> equal(skf6(skc14),skf5(skc14)) in(skf5(skc14),skf6(skc14))*. % 0.22/0.52 444[3:SSi:441.0,136.0,381.0] || -> equal(skf6(skc14),skf5(skc14)) in(skf5(skc14),skf6(skc14))*. % 0.22/0.52 538[5:Spt:444.0] || -> equal(skf6(skc14),skf5(skc14))**. % 0.22/0.52 544[5:SpL:538.0,75.0] || equal(skf5(skc14),skf5(skc14))* -> epsilon_connected(skc14). % 0.22/0.52 547[5:Obv:544.0] || -> epsilon_connected(skc14)*. % 0.22/0.52 548[5:MRR:547.0,139.0] || -> . % 0.22/0.52 549[5:Spt:548.0,444.0,538.0] || equal(skf6(skc14),skf5(skc14))** -> . % 0.22/0.52 550[5:Spt:548.0,444.1] || -> in(skf5(skc14),skf6(skc14))*. % 0.22/0.52 555[5:Res:550.0,76.0] || -> epsilon_connected(skc14)*. % 0.22/0.52 557[5:MRR:555.0,139.0] || -> . % 0.22/0.52 559[3:Spt:557.0,314.0,381.0] || epsilon_connected(skf5(skc14))* -> . % 0.22/0.52 560[3:Spt:557.0,314.1] || -> element(skf6(skf5(skc14)),skc14)*. % 0.22/0.52 569[3:Res:62.1,559.0] ordinal(skf5(skc14)) || -> . % 0.22/0.52 575[3:SSi:569.0,136.0] || -> . % 0.22/0.52 % SZS output end Refutation % 0.22/0.52 Formulae used in the proof : fc2_ordinal1 fc4_relat_1 t31_ordinal1 existence_m1_subset_1 cc3_ordinal1 d4_ordinal1 d2_ordinal1 d3_ordinal1 antisymmetry_r2_hidden t6_boole t3_subset t2_subset t4_subset t5_subset t24_ordinal1 % 0.22/0.52 %------------------------------------------------------------------------------