%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU145+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.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:19 EDT 2022 % Result : Theorem 1.03s 1.25s % Output : Refutation 1.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SEU145+2 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n008.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sun Jun 19 19:09:52 EDT 2022 % 0.12/0.33 % CPUTime : % 1.03/1.25 % 1.03/1.25 SPASS V 3.9 % 1.03/1.25 SPASS beiseite: Proof found. % 1.03/1.25 % SZS status Theorem % 1.03/1.25 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.03/1.25 SPASS derived 6463 clauses, backtracked 20 clauses, performed 2 splits and kept 1860 clauses. % 1.03/1.25 SPASS allocated 102212 KBytes. % 1.03/1.25 SPASS spent 0:00:00.89 on the problem. % 1.03/1.25 0:00:00.04 for the input. % 1.03/1.25 0:00:00.11 for the FLOTTER CNF translation. % 1.03/1.25 0:00:00.06 for inferences. % 1.03/1.25 0:00:00.00 for the backtracking. % 1.03/1.25 0:00:00.64 for the reduction. % 1.03/1.25 % 1.03/1.25 % 1.03/1.25 Here is a proof with depth 9, length 56 : % 1.03/1.25 % SZS output start Refutation % 1.03/1.25 2[0:Inp] || -> empty(skc38)*. % 1.03/1.25 3[0:Inp] || -> subset(skc5,skc7)*r. % 1.03/1.25 7[0:Inp] || in(skc6,skc5)* -> . % 1.03/1.25 11[0:Inp] || equal(singleton(u),empty_set)** -> . % 1.03/1.25 13[0:Inp] || -> equal(set_union2(u,empty_set),u)**. % 1.03/1.25 16[0:Inp] || -> equal(set_difference(u,empty_set),u)**. % 1.03/1.25 17[0:Inp] || -> equal(set_difference(empty_set,u),empty_set)**. % 1.03/1.25 20[0:Inp] empty(u) || -> equal(u,empty_set)*. % 1.03/1.25 21[0:Inp] || subset(skc5,set_difference(skc7,singleton(skc6)))*r -> . % 1.03/1.25 23[0:Inp] || -> equal(set_union2(u,v),set_union2(v,u))*. % 1.03/1.25 24[0:Inp] || -> equal(set_intersection2(u,v),set_intersection2(v,u))*. % 1.03/1.25 31[0:Inp] || disjoint(u,v)*+ -> disjoint(v,u)*. % 1.03/1.25 41[0:Inp] || -> disjoint(u,v) in(skf18(v,u),u)*. % 1.03/1.25 42[0:Inp] || -> disjoint(u,v)* in(skf18(v,w),v)*. % 1.03/1.25 53[0:Inp] || -> equal(set_union2(u,set_difference(v,u)),set_union2(u,v))**. % 1.03/1.25 54[0:Inp] || -> equal(set_difference(set_union2(u,v),v),set_difference(u,v))**. % 1.03/1.25 55[0:Inp] || -> equal(set_difference(u,set_difference(u,v)),set_intersection2(u,v))**. % 1.03/1.25 56[0:Inp] || disjoint(u,v) -> equal(set_difference(u,v),u)**. % 1.03/1.25 64[0:Inp] || subset(u,v)* subset(v,w)* -> subset(u,w)*. % 1.03/1.25 66[0:Inp] || subset(u,v) -> subset(set_difference(u,w),set_difference(v,w))*. % 1.03/1.25 69[0:Inp] || in(u,v)* equal(v,singleton(w))*+ -> equal(u,w)*. % 1.03/1.25 122[0:Res:3.0,66.0] || -> subset(set_difference(skc5,u),set_difference(skc7,u))*r. % 1.03/1.25 185[0:EmS:20.0,2.0] || -> equal(empty_set,skc38)**. % 1.03/1.25 188[0:Rew:185.0,17.0] || -> equal(set_difference(skc38,u),skc38)**. % 1.03/1.25 190[0:Rew:185.0,11.0] || equal(singleton(u),skc38)** -> . % 1.03/1.25 191[0:Rew:185.0,16.0] || -> equal(set_difference(u,skc38),u)**. % 1.03/1.25 192[0:Rew:185.0,13.0] || -> equal(set_union2(u,skc38),u)**. % 1.03/1.25 234[0:SpR:23.0,192.0] || -> equal(set_union2(skc38,u),u)**. % 1.03/1.25 270[0:Res:42.0,31.0] || -> in(skf18(u,v),u)* disjoint(u,w)*. % 1.03/1.25 329[0:SpR:23.0,54.0] || -> equal(set_difference(set_union2(u,v),u),set_difference(v,u))**. % 1.03/1.25 331[0:SpR:234.0,54.0] || -> equal(set_difference(u,u),set_difference(skc38,u))*. % 1.03/1.25 333[0:Rew:188.0,331.0] || -> equal(set_difference(u,u),skc38)**. % 1.03/1.25 348[0:SpR:53.0,54.0] || -> equal(set_difference(set_union2(u,v),set_difference(v,u)),set_difference(u,set_difference(v,u)))**. % 1.03/1.25 406[0:SpR:329.0,53.0] || -> equal(set_union2(u,set_difference(v,u)),set_union2(u,set_union2(u,v)))**. % 1.03/1.25 409[0:SpR:329.0,55.0] || -> equal(set_difference(set_union2(u,v),set_difference(v,u)),set_intersection2(set_union2(u,v),u))**. % 1.03/1.25 422[0:Rew:53.0,406.0] || -> equal(set_union2(u,set_union2(u,v)),set_union2(u,v))**. % 1.03/1.25 424[0:Rew:24.0,409.0] || -> equal(set_difference(set_union2(u,v),set_difference(v,u)),set_intersection2(u,set_union2(u,v)))**. % 1.03/1.25 425[0:Rew:348.0,424.0] || -> equal(set_difference(u,set_difference(v,u)),set_intersection2(u,set_union2(u,v)))**. % 1.03/1.25 470[0:SpR:422.0,54.0] || -> equal(set_difference(set_union2(u,v),set_union2(u,v)),set_difference(u,set_union2(u,v)))**. % 1.03/1.25 488[0:Rew:333.0,470.0] || -> equal(set_difference(u,set_union2(u,v)),skc38)**. % 1.03/1.25 492[0:SpR:488.0,55.0] || -> equal(set_intersection2(u,set_union2(u,v)),set_difference(u,skc38))**. % 1.03/1.25 493[0:SpR:488.0,56.1] || disjoint(u,set_union2(u,v))* -> equal(skc38,u). % 1.03/1.25 506[0:Rew:191.0,492.0] || -> equal(set_intersection2(u,set_union2(u,v)),u)**. % 1.03/1.25 507[0:Rew:506.0,425.0] || -> equal(set_difference(u,set_difference(v,u)),u)**. % 1.03/1.25 563[0:SpR:56.1,507.0] || disjoint(u,v) -> equal(set_difference(v,u),v)**. % 1.03/1.25 875[0:Res:270.1,493.0] || -> in(skf18(u,v),u)* equal(skc38,u). % 1.03/1.25 994[0:EqR:69.1] || in(u,singleton(v))* -> equal(u,v). % 1.03/1.25 997[0:Res:875.0,994.0] || -> equal(singleton(u),skc38) equal(skf18(singleton(u),v),u)**. % 1.03/1.25 1003[0:MRR:997.0,190.0] || -> equal(skf18(singleton(u),v),u)**. % 1.03/1.25 1037[0:SpR:1003.0,41.1] || -> disjoint(u,singleton(v))* in(v,u). % 1.03/1.25 1046[0:Res:1037.0,31.0] || -> in(u,v) disjoint(singleton(u),v)*. % 1.03/1.25 7541[0:NCh:64.2,64.1,122.0,21.0] || equal(set_difference(skc5,singleton(skc6)),skc5)** -> . % 1.03/1.25 7546[0:SpL:563.1,7541.0] || disjoint(singleton(skc6),skc5)* equal(skc5,skc5) -> . % 1.03/1.25 7552[0:Obv:7546.1] || disjoint(singleton(skc6),skc5)* -> . % 1.03/1.25 7565[0:Res:1046.1,7552.0] || -> in(skc6,skc5)*. % 1.03/1.25 7567[0:MRR:7565.0,7.0] || -> . % 1.03/1.25 % SZS output end Refutation % 1.03/1.25 Formulae used in the proof : rc1_xboole_0 l3_zfmisc_1 l1_zfmisc_1 t1_boole t3_boole t4_boole t6_boole commutativity_k2_xboole_0 commutativity_k3_xboole_0 symmetry_r1_xboole_0 t3_xboole_0 t39_xboole_1 t40_xboole_1 t48_xboole_1 t83_xboole_1 t1_xboole_1 t33_xboole_1 d1_tarski % 1.03/1.25 %------------------------------------------------------------------------------