%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU141+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n012.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:17 EDT 2022 % Result : Theorem 8.00s 8.21s % Output : Refutation 8.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU141+2 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n012.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 01:56:08 EDT 2022 % 0.14/0.34 % CPUTime : % 8.00/8.21 % 8.00/8.21 SPASS V 3.9 % 8.00/8.21 SPASS beiseite: Proof found. % 8.00/8.21 % SZS status Theorem % 8.00/8.21 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.00/8.21 SPASS derived 28114 clauses, backtracked 5898 clauses, performed 1 splits and kept 5036 clauses. % 8.00/8.21 SPASS allocated 117734 KBytes. % 8.00/8.21 SPASS spent 0:00:07.47 on the problem. % 8.00/8.21 0:00:00.03 for the input. % 8.00/8.21 0:00:00.07 for the FLOTTER CNF translation. % 8.00/8.21 0:00:00.20 for inferences. % 8.00/8.21 0:00:00.13 for the backtracking. % 8.00/8.21 0:00:06.94 for the reduction. % 8.00/8.21 % 8.00/8.21 % 8.00/8.21 Here is a proof with depth 5, length 66 : % 8.00/8.21 % SZS output start Refutation % 8.00/8.21 2[0:Inp] || -> empty(skc26)*. % 8.00/8.21 4[0:Inp] || -> subset(u,u)*. % 8.00/8.21 10[0:Inp] || -> equal(set_union2(u,empty_set),u)**. % 8.00/8.21 12[0:Inp] || -> subset(set_difference(u,v),u)*l. % 8.00/8.21 13[0:Inp] || -> equal(set_difference(u,empty_set),u)**. % 8.00/8.21 14[0:Inp] || -> equal(set_difference(empty_set,u),empty_set)**. % 8.00/8.21 15[0:Inp] || -> subset(u,set_union2(u,v))*r. % 8.00/8.21 17[0:Inp] empty(u) || -> equal(u,empty_set)*. % 8.00/8.21 18[0:Inp] || -> equal(set_union2(u,v),set_union2(v,u))*. % 8.00/8.21 19[0:Inp] || -> equal(set_intersection2(u,v),set_intersection2(v,u))*. % 8.00/8.21 26[0:Inp] || disjoint(u,v)*+ -> disjoint(v,u)*. % 8.00/8.21 29[0:Inp] || -> disjoint(skc4,skc5) equal(set_difference(skc4,skc5),skc4)**. % 8.00/8.21 38[0:Inp] || disjoint(u,v) -> equal(set_intersection2(u,v),empty_set)**. % 8.00/8.21 39[0:Inp] || equal(set_intersection2(u,v),empty_set)** -> disjoint(u,v). % 8.00/8.21 46[0:Inp] || -> equal(set_union2(u,set_difference(v,u)),set_union2(u,v))**. % 8.00/8.21 47[0:Inp] || -> equal(set_difference(set_union2(u,v),v),set_difference(u,v))**. % 8.00/8.21 48[0:Inp] || -> equal(set_difference(u,set_difference(u,v)),set_intersection2(u,v))**. % 8.00/8.21 50[0:Inp] || disjoint(skc4,skc5) equal(set_difference(skc4,skc5),skc4)** -> . % 8.00/8.21 54[0:Inp] || subset(u,v)*+ subset(v,u)* -> equal(v,u). % 8.00/8.21 69[0:Inp] || subset(u,v)*+ subset(w,v)* -> subset(set_union2(w,u),v)*. % 8.00/8.21 96[0:EmS:17.0,2.0] || -> equal(empty_set,skc26)**. % 8.00/8.21 98[0:Rew:96.0,14.0] || -> equal(set_difference(skc26,u),skc26)**. % 8.00/8.21 100[0:Rew:96.0,13.0] || -> equal(set_difference(u,skc26),u)**. % 8.00/8.21 101[0:Rew:96.0,10.0] || -> equal(set_union2(u,skc26),u)**. % 8.00/8.21 105[0:Rew:96.0,38.1] || disjoint(u,v) -> equal(set_intersection2(u,v),skc26)**. % 8.00/8.21 106[0:Rew:96.0,39.0] || equal(set_intersection2(u,v),skc26)** -> disjoint(u,v). % 8.00/8.21 141[0:SpR:18.0,101.0] || -> equal(set_union2(skc26,u),u)**. % 8.00/8.21 159[1:Spt:29.0] || -> disjoint(skc4,skc5)*. % 8.00/8.21 160[1:MRR:50.0,159.0] || equal(set_difference(skc4,skc5),skc4)** -> . % 8.00/8.21 161[1:Res:159.0,26.0] || -> disjoint(skc5,skc4)*. % 8.00/8.21 191[0:SpR:105.1,19.0] || disjoint(u,v) -> equal(set_intersection2(v,u),skc26)**. % 8.00/8.21 205[0:SpL:19.0,106.0] || equal(set_intersection2(u,v),skc26)** -> disjoint(v,u). % 8.00/8.21 223[0:SpR:18.0,47.0] || -> equal(set_difference(set_union2(u,v),u),set_difference(v,u))**. % 8.00/8.21 225[0:SpR:141.0,47.0] || -> equal(set_difference(u,u),set_difference(skc26,u))*. % 8.00/8.21 227[0:Rew:98.0,225.0] || -> equal(set_difference(u,u),skc26)**. % 8.00/8.21 252[0:SpR:46.0,47.0] || -> equal(set_difference(set_union2(u,v),set_difference(v,u)),set_difference(u,set_difference(v,u)))**. % 8.00/8.21 258[0:SpR:48.0,46.0] || -> equal(set_union2(set_difference(u,v),set_intersection2(u,v)),set_union2(set_difference(u,v),u))**. % 8.00/8.21 265[0:Rew:18.0,258.0,18.0,258.0] || -> equal(set_union2(set_intersection2(u,v),set_difference(u,v)),set_union2(u,set_difference(u,v)))**. % 8.00/8.21 293[0:SpR:223.0,46.0] || -> equal(set_union2(u,set_difference(v,u)),set_union2(u,set_union2(u,v)))**. % 8.00/8.21 296[0:SpR:223.0,48.0] || -> equal(set_difference(set_union2(u,v),set_difference(v,u)),set_intersection2(set_union2(u,v),u))**. % 8.00/8.21 307[0:Rew:46.0,293.0] || -> equal(set_union2(u,set_union2(u,v)),set_union2(u,v))**. % 8.00/8.21 309[0:Rew:19.0,296.0] || -> equal(set_difference(set_union2(u,v),set_difference(v,u)),set_intersection2(u,set_union2(u,v)))**. % 8.00/8.21 310[0:Rew:252.0,309.0] || -> equal(set_difference(u,set_difference(v,u)),set_intersection2(u,set_union2(u,v)))**. % 8.00/8.21 347[0:SpR:307.0,47.0] || -> equal(set_difference(set_union2(u,v),set_union2(u,v)),set_difference(u,set_union2(u,v)))**. % 8.00/8.21 365[0:Rew:227.0,347.0] || -> equal(set_difference(u,set_union2(u,v)),skc26)**. % 8.00/8.21 377[0:SpR:365.0,48.0] || -> equal(set_intersection2(u,set_union2(u,v)),set_difference(u,skc26))**. % 8.00/8.21 389[0:Rew:100.0,377.0] || -> equal(set_intersection2(u,set_union2(u,v)),u)**. % 8.00/8.21 390[0:Rew:389.0,310.0] || -> equal(set_difference(u,set_difference(v,u)),u)**. % 8.00/8.21 428[0:SpR:390.0,48.0] || -> equal(set_intersection2(u,set_difference(v,u)),set_difference(u,u))**. % 8.00/8.21 440[0:Rew:227.0,428.0] || -> equal(set_intersection2(u,set_difference(v,u)),skc26)**. % 8.00/8.21 467[0:SpL:440.0,205.0] || equal(skc26,skc26) -> disjoint(set_difference(u,v),v)*. % 8.00/8.21 471[0:Obv:467.0] || -> disjoint(set_difference(u,v),v)*. % 8.00/8.21 3430[0:Res:15.0,54.0] || subset(set_union2(u,v),u)*l -> equal(set_union2(u,v),u). % 8.00/8.21 4302[0:Res:12.0,69.0] || subset(u,v) -> subset(set_union2(u,set_difference(v,w)),v)*l. % 8.00/8.21 8482[0:SpR:191.1,265.0] || disjoint(u,v) -> equal(set_union2(skc26,set_difference(v,u)),set_union2(v,set_difference(v,u)))*. % 8.00/8.21 8605[0:Rew:141.0,8482.1] || disjoint(u,v) -> equal(set_union2(v,set_difference(v,u)),set_difference(v,u))**. % 8.00/8.21 30961[0:Res:4302.1,3430.0] || subset(u,u) -> equal(set_union2(u,set_difference(u,v)),u)**. % 8.00/8.21 31049[0:MRR:30961.0,4.0] || -> equal(set_union2(u,set_difference(u,v)),u)**. % 8.00/8.21 31056[0:Rew:31049.0,8605.1] || disjoint(u,v) -> equal(set_difference(v,u),v)**. % 8.00/8.21 35244[1:SpL:31056.1,160.0] || disjoint(skc5,skc4)* equal(skc4,skc4) -> . % 8.00/8.21 35256[1:Obv:35244.1] || disjoint(skc5,skc4)* -> . % 8.00/8.21 35257[1:MRR:35256.0,161.0] || -> . % 8.00/8.21 35272[1:Spt:35257.0,29.0,159.0] || disjoint(skc4,skc5)* -> . % 8.00/8.21 35273[1:Spt:35257.0,29.1] || -> equal(set_difference(skc4,skc5),skc4)**. % 8.00/8.21 35420[1:SpR:35273.0,471.0] || -> disjoint(skc4,skc5)*. % 8.00/8.21 35499[1:MRR:35420.0,35272.0] || -> . % 8.00/8.21 % SZS output end Refutation % 8.00/8.21 Formulae used in the proof : rc1_xboole_0 reflexivity_r1_tarski t1_boole t36_xboole_1 t3_boole t4_boole t7_xboole_1 t6_boole commutativity_k2_xboole_0 commutativity_k3_xboole_0 symmetry_r1_xboole_0 t83_xboole_1 d7_xboole_0 t39_xboole_1 t40_xboole_1 t48_xboole_1 d10_xboole_0 t8_xboole_1 % 8.00/8.21 %------------------------------------------------------------------------------