%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU094+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:33:56 EDT 2022 % Result : Theorem 0.21s 0.49s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU094+1 : TPTP v8.1.0. Released v3.2.0. % 0.06/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n011.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sun Jun 19 22:44:39 EDT 2022 % 0.14/0.34 % CPUTime : % 0.21/0.49 % 0.21/0.49 SPASS V 3.9 % 0.21/0.49 SPASS beiseite: Proof found. % 0.21/0.49 % SZS status Theorem % 0.21/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.49 SPASS derived 511 clauses, backtracked 21 clauses, performed 3 splits and kept 436 clauses. % 0.21/0.49 SPASS allocated 98119 KBytes. % 0.21/0.49 SPASS spent 0:00:00.14 on the problem. % 0.21/0.49 0:00:00.03 for the input. % 0.21/0.49 0:00:00.04 for the FLOTTER CNF translation. % 0.21/0.49 0:00:00.01 for inferences. % 0.21/0.49 0:00:00.00 for the backtracking. % 0.21/0.49 0:00:00.03 for the reduction. % 0.21/0.49 % 0.21/0.49 % 0.21/0.49 Here is a proof with depth 5, length 42 : % 0.21/0.49 % SZS output start Refutation % 0.21/0.49 97[0:Inp] || -> finite(skc23) finite(union(skc23))*. % 0.21/0.49 111[0:Inp] || -> subset(u,powerset(union(u)))*. % 0.21/0.49 117[0:Inp] finite(u) || -> finite(powerset(u))*. % 0.21/0.49 129[0:Inp] || in(u,v) -> subset(u,union(v))*. % 0.21/0.49 130[0:Inp] || in(u,skc23)*+ -> finite(u) finite(union(skc23))*. % 0.21/0.49 137[0:Inp] finite(u) || subset(v,u)* -> finite(v). % 0.21/0.49 140[0:Inp] || finite(skc23) finite(union(skc23))* -> in(skc24,skc23). % 0.21/0.49 141[0:Inp] || finite(skc23) finite(skc24) finite(union(skc23))* -> . % 0.21/0.49 143[0:Inp] finite(u) || -> finite(union(u)) in(skf7(u),u)*. % 0.21/0.49 144[0:Inp] finite(u) || finite(skf7(v))*+ -> finite(union(u))*. % 0.21/0.49 150[1:Spt:130.0,130.1] || in(u,skc23)* -> finite(u). % 0.21/0.49 151[2:Spt:97.0] || -> finite(skc23)*. % 0.21/0.49 152[2:MRR:141.0,151.0] || finite(skc24) finite(union(skc23))* -> . % 0.21/0.49 153[2:MRR:140.0,151.0] || finite(union(skc23))* -> in(skc24,skc23). % 0.21/0.49 254[0:Res:111.0,137.1] finite(powerset(union(u))) || -> finite(u)*. % 0.21/0.49 255[0:Res:129.1,137.1] finite(union(u)) || in(v,u)* -> finite(v). % 0.21/0.49 284[1:Res:143.2,150.0] finite(skc23) || -> finite(union(skc23)) finite(skf7(skc23))*. % 0.21/0.49 289[2:SSi:284.0,151.0] || -> finite(union(skc23)) finite(skf7(skc23))*. % 0.21/0.49 297[3:Spt:289.0] || -> finite(union(skc23))*. % 0.21/0.49 298[3:MRR:152.1,297.0] || finite(skc24)* -> . % 0.21/0.49 299[3:MRR:153.0,297.0] || -> in(skc24,skc23)*. % 0.21/0.49 301[3:Res:299.0,150.0] || -> finite(skc24)*. % 0.21/0.49 304[3:MRR:301.0,298.0] || -> . % 0.21/0.49 305[3:Spt:304.0,289.0,297.0] || finite(union(skc23))* -> . % 0.21/0.49 306[3:Spt:304.0,289.1] || -> finite(skf7(skc23))*. % 0.21/0.49 307[3:Res:306.0,144.1] finite(u) || -> finite(union(u))*. % 0.21/0.49 316[3:Res:307.1,305.0] finite(skc23) || -> . % 0.21/0.49 317[3:SSi:316.0,151.0] || -> . % 0.21/0.49 318[2:Spt:317.0,97.0,151.0] || finite(skc23)* -> . % 0.21/0.49 319[2:Spt:317.0,97.1] || -> finite(union(skc23))*. % 0.21/0.49 337[0:SoR:254.0,117.1] finite(union(u)) || -> finite(u)*. % 0.21/0.49 339[2:SoR:337.0,319.0] || -> finite(skc23)*. % 0.21/0.49 343[2:MRR:339.0,318.0] || -> . % 0.21/0.49 344[1:Spt:343.0,130.2] || -> finite(union(skc23))*. % 0.21/0.49 345[1:MRR:140.1,344.0] || finite(skc23) -> in(skc24,skc23)*. % 0.21/0.49 346[1:MRR:141.2,344.0] || finite(skc23) finite(skc24)* -> . % 0.21/0.49 347[1:SoR:337.0,344.0] || -> finite(skc23)*. % 0.21/0.49 348[1:MRR:345.0,347.0] || -> in(skc24,skc23)*. % 0.21/0.49 349[1:MRR:346.0,347.0] || finite(skc24)* -> . % 0.21/0.49 716[1:SoR:255.0,344.0] || in(u,skc23)* -> finite(u). % 0.21/0.49 728[1:Res:348.0,716.0] || -> finite(skc24)*. % 0.21/0.49 729[1:MRR:728.0,349.0] || -> . % 0.21/0.49 % SZS output end Refutation % 0.21/0.49 Formulae used in the proof : t25_finset_1 t100_zfmisc_1 t24_finset_1 t92_zfmisc_1 t13_finset_1 l22_finset_1 % 0.21/0.49 %------------------------------------------------------------------------------