%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SET890+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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 05:29:36 EDT 2022 % Result : Theorem 0.19s 0.55s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SET890+1 : TPTP v8.1.0. Released v3.2.0. % 0.13/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n028.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 : Mon Jul 11 09:40:13 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.55 % 0.19/0.55 SPASS V 3.9 % 0.19/0.55 SPASS beiseite: Proof found. % 0.19/0.55 % SZS status Theorem % 0.19/0.55 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.55 SPASS derived 550 clauses, backtracked 12 clauses, performed 2 splits and kept 382 clauses. % 0.19/0.55 SPASS allocated 85805 KBytes. % 0.19/0.55 SPASS spent 0:00:00.20 on the problem. % 0.19/0.55 0:00:00.04 for the input. % 0.19/0.55 0:00:00.04 for the FLOTTER CNF translation. % 0.19/0.55 0:00:00.01 for inferences. % 0.19/0.55 0:00:00.00 for the backtracking. % 0.19/0.55 0:00:00.08 for the reduction. % 0.19/0.55 % 0.19/0.55 % 0.19/0.55 Here is a proof with depth 4, length 25 : % 0.19/0.55 % SZS output start Refutation % 0.19/0.55 5[0:Inp] || equal(union(singleton(skc3)),skc3)** -> . % 0.19/0.55 8[0:Inp] || -> in(skf9(u,v),skf10(v,u))*. % 0.19/0.55 15[0:Inp] || in(u,v)* equal(v,singleton(w))*+ -> equal(u,w)*. % 0.19/0.55 16[0:Inp] || equal(u,v)* equal(w,singleton(v))*+ -> in(u,w)*. % 0.19/0.55 19[0:Inp] || -> equal(u,union(v)) in(skf10(u,v),v)* in(skf9(v,u),u)*. % 0.19/0.55 22[0:Inp] || in(u,v) in(skf9(v,w),u)*+ in(skf9(v,w),w)* -> equal(w,union(v)). % 0.19/0.55 27[0:Res:22.3,5.0] || in(u,singleton(skc3)) in(skf9(singleton(skc3),skc3),u)* in(skf9(singleton(skc3),skc3),skc3)* -> . % 0.19/0.55 28[0:Res:19.2,5.0] || -> in(skf10(skc3,singleton(skc3)),singleton(skc3))* in(skf9(singleton(skc3),skc3),skc3). % 0.19/0.55 44[0:EqR:16.1] || equal(u,v) -> in(u,singleton(v))*. % 0.19/0.55 53[0:EqR:15.1] || in(u,singleton(v))* -> equal(u,v). % 0.19/0.55 311[0:Res:28.0,53.0] || -> in(skf9(singleton(skc3),skc3),skc3)* equal(skf10(skc3,singleton(skc3)),skc3). % 0.19/0.55 312[0:Rew:311.1,28.0] || -> in(skc3,singleton(skc3)) in(skf9(singleton(skc3),skc3),skc3)*. % 0.19/0.55 316[1:Spt:312.0] || -> in(skc3,singleton(skc3))*. % 0.19/0.55 551[2:Spt:311.0] || -> in(skf9(singleton(skc3),skc3),skc3)*. % 0.19/0.55 552[2:MRR:27.2,551.0] || in(u,singleton(skc3)) in(skf9(singleton(skc3),skc3),u)* -> . % 0.19/0.55 578[2:Res:551.0,552.1] || in(skc3,singleton(skc3))* -> . % 0.19/0.55 579[2:MRR:578.0,316.0] || -> . % 0.19/0.55 581[2:Spt:579.0,311.0,551.0] || in(skf9(singleton(skc3),skc3),skc3)* -> . % 0.19/0.55 582[2:Spt:579.0,311.1] || -> equal(skf10(skc3,singleton(skc3)),skc3)**. % 0.19/0.55 584[2:SpR:582.0,8.0] || -> in(skf9(singleton(skc3),skc3),skc3)*. % 0.19/0.55 594[2:MRR:584.0,581.0] || -> . % 0.19/0.55 596[1:Spt:594.0,312.0,316.0] || in(skc3,singleton(skc3))* -> . % 0.19/0.55 597[1:Spt:594.0,312.1] || -> in(skf9(singleton(skc3),skc3),skc3)*. % 0.19/0.55 607[1:Res:44.1,596.0] || equal(skc3,skc3)* -> . % 0.19/0.55 608[1:Obv:607.0] || -> . % 0.19/0.55 % SZS output end Refutation % 0.19/0.55 Formulae used in the proof : t31_zfmisc_1 d4_tarski reflexivity_r1_tarski d10_xboole_0 d1_tarski % 0.19/0.55 %------------------------------------------------------------------------------