%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU173+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n003.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:34:42 EDT 2022 % Result : Theorem 9.55s 9.76s % Output : Refutation 9.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU173+2 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n003.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 23:05:29 EDT 2022 % 0.13/0.34 % CPUTime : % 9.55/9.76 % 9.55/9.76 SPASS V 3.9 % 9.55/9.76 SPASS beiseite: Proof found. % 9.55/9.76 % SZS status Theorem % 9.55/9.76 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 9.55/9.76 SPASS derived 17964 clauses, backtracked 118 clauses, performed 3 splits and kept 7874 clauses. % 9.55/9.76 SPASS allocated 112261 KBytes. % 9.55/9.76 SPASS spent 0:00:09.27 on the problem. % 9.55/9.76 0:00:00.04 for the input. % 9.55/9.76 0:00:00.25 for the FLOTTER CNF translation. % 9.55/9.76 0:00:00.21 for inferences. % 9.55/9.76 0:00:00.13 for the backtracking. % 9.55/9.76 0:00:08.47 for the reduction. % 9.55/9.76 % 9.55/9.76 % 9.55/9.76 Here is a proof with depth 4, length 15 : % 9.55/9.76 % SZS output start Refutation % 9.55/9.76 12[0:Inp] || element(skc4,powerset(skc5))* -> . % 9.55/9.76 32[0:Inp] || in(u,skc4) -> in(u,skc5)*. % 9.55/9.76 46[0:Inp] empty(u) || in(v,u)* -> . % 9.55/9.76 50[0:Inp] || -> subset(u,v) in(skf31(v,u),u)*. % 9.55/9.76 64[0:Inp] || in(u,v) -> element(u,v)* empty(v). % 9.55/9.76 67[0:Inp] || in(skf31(u,v),u)*+ -> subset(w,u)*. % 9.55/9.76 121[0:Inp] || subset(u,v)*+ equal(w,powerset(v))* -> in(u,w)*. % 9.55/9.76 185[0:MRR:64.2,46.0] || in(u,v) -> element(u,v)*. % 9.55/9.76 189[0:Res:185.1,12.0] || in(skc4,powerset(skc5))* -> . % 9.55/9.76 2964[0:Res:32.1,67.0] || in(skf31(skc5,u),skc4)*+ -> subset(v,skc5)*. % 9.55/9.76 18715[0:Res:50.1,2964.0] || -> subset(skc4,skc5)*r subset(u,skc5)*. % 9.55/9.76 18716[0:Con:18715.1] || -> subset(skc4,skc5)*r. % 9.55/9.76 18724[0:Res:18716.0,121.0] || equal(u,powerset(skc5)) -> in(skc4,u)*. % 9.55/9.76 20425[0:Res:18724.1,189.0] || equal(powerset(skc5),powerset(skc5))* -> . % 9.55/9.76 20442[0:Obv:20425.0] || -> . % 9.55/9.76 % SZS output end Refutation % 9.55/9.76 Formulae used in the proof : l71_subset_1 t7_boole d3_tarski d2_subset_1 d1_zfmisc_1 % 9.55/9.76 %------------------------------------------------------------------------------