%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU146+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:20 EDT 2022 % Result : Theorem 0.38s 0.60s % Output : Refutation 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SEU146+2 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : run_spass %d %s % 0.11/0.32 % Computer : n019.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Sun Jun 19 01:08:09 EDT 2022 % 0.11/0.33 % CPUTime : % 0.38/0.60 % 0.38/0.60 SPASS V 3.9 % 0.38/0.60 SPASS beiseite: Proof found. % 0.38/0.60 % SZS status Theorem % 0.38/0.60 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.38/0.60 SPASS derived 2525 clauses, backtracked 24 clauses, performed 1 splits and kept 672 clauses. % 0.38/0.60 SPASS allocated 99499 KBytes. % 0.38/0.60 SPASS spent 0:00:00.26 on the problem. % 0.38/0.60 0:00:00.04 for the input. % 0.38/0.60 0:00:00.07 for the FLOTTER CNF translation. % 0.38/0.60 0:00:00.01 for inferences. % 0.38/0.60 0:00:00.00 for the backtracking. % 0.38/0.60 0:00:00.12 for the reduction. % 0.38/0.60 % 0.38/0.60 % 0.38/0.60 Here is a proof with depth 11, length 63 : % 0.38/0.60 % SZS output start Refutation % 0.38/0.60 2[0:Inp] || -> empty(skc36)*. % 0.38/0.60 5[0:Inp] || -> subset(empty_set,u)*. % 0.38/0.60 8[0:Inp] || -> equal(set_intersection2(u,u),u)**. % 0.38/0.60 9[0:Inp] || equal(singleton(u),empty_set)** -> . % 0.38/0.60 11[0:Inp] || -> equal(set_union2(u,empty_set),u)**. % 0.38/0.60 15[0:Inp] || -> equal(set_difference(empty_set,u),empty_set)**. % 0.38/0.60 18[0:Inp] empty(u) || -> equal(u,empty_set)*. % 0.38/0.60 20[0:Inp] || -> equal(set_union2(u,v),set_union2(v,u))*. % 0.38/0.60 23[0:Inp] || equal(u,v)* -> subset(v,u). % 0.38/0.60 28[0:Inp] || disjoint(u,v)*+ -> disjoint(v,u)*. % 0.38/0.60 37[0:Inp] || in(u,v)* -> subset(singleton(u),v). % 0.38/0.60 38[0:Inp] || -> disjoint(u,v) in(skf18(v,u),u)*. % 0.38/0.60 39[0:Inp] || -> disjoint(u,v)* in(skf18(v,w),v)*. % 0.38/0.60 41[0:Inp] || equal(empty_set,skc4) subset(skc4,singleton(skc5))*r -> . % 0.38/0.60 43[0:Inp] || disjoint(u,v) -> equal(set_intersection2(u,v),empty_set)**. % 0.38/0.60 51[0:Inp] || -> equal(set_union2(u,set_difference(v,u)),set_union2(u,v))**. % 0.38/0.60 52[0:Inp] || -> equal(set_difference(set_union2(u,v),v),set_difference(u,v))**. % 0.38/0.60 54[0:Inp] || disjoint(u,v) -> equal(set_difference(u,v),u)**. % 0.38/0.60 57[0:Inp] || equal(singleton(skc5),skc4) subset(skc4,singleton(skc5))*r -> . % 0.38/0.60 61[0:Inp] || -> subset(skc4,singleton(skc5))*r equal(empty_set,skc4) equal(singleton(skc5),skc4). % 0.38/0.60 62[0:Inp] || subset(u,v)* subset(v,u)* -> equal(v,u). % 0.38/0.60 68[0:Inp] || disjoint(u,v)* subset(w,u)*+ -> disjoint(w,v)*. % 0.38/0.60 69[0:Inp] || in(u,v)* equal(v,singleton(w))*+ -> equal(u,w)*. % 0.38/0.60 104[0:MRR:57.1,23.1] || equal(singleton(skc5),skc4)** -> . % 0.38/0.60 106[0:MRR:61.2,104.0] || -> equal(empty_set,skc4) subset(skc4,singleton(skc5))*r. % 0.38/0.60 117[0:Res:62.2,104.0] || subset(skc4,singleton(skc5)) subset(singleton(skc5),skc4)*l -> . % 0.38/0.60 125[1:Spt:106.0] || -> equal(empty_set,skc4)**. % 0.38/0.60 133[1:Rew:125.0,41.0] || equal(skc4,skc4) subset(skc4,singleton(skc5))*r -> . % 0.38/0.60 141[1:Rew:125.0,5.0] || -> subset(skc4,u)*. % 0.38/0.60 147[1:Obv:133.0] || subset(skc4,singleton(skc5))*r -> . % 0.38/0.60 148[1:MRR:147.0,141.0] || -> . % 0.38/0.60 149[1:Spt:148.0,106.0,125.0] || equal(empty_set,skc4)** -> . % 0.38/0.60 150[1:Spt:148.0,106.1] || -> subset(skc4,singleton(skc5))*r. % 0.38/0.60 152[1:MRR:117.0,150.0] || subset(singleton(skc5),skc4)*l -> . % 0.38/0.60 163[0:EmS:18.0,2.0] || -> equal(empty_set,skc36)**. % 0.38/0.60 165[1:Rew:163.0,149.0] || equal(skc36,skc4)** -> . % 0.38/0.60 166[0:Rew:163.0,9.0] || equal(singleton(u),skc36)** -> . % 0.38/0.60 168[0:Rew:163.0,15.0] || -> equal(set_difference(skc36,u),skc36)**. % 0.38/0.60 169[0:Rew:163.0,11.0] || -> equal(set_union2(u,skc36),u)**. % 0.38/0.60 177[0:Rew:163.0,43.1] || disjoint(u,v) -> equal(set_intersection2(u,v),skc36)**. % 0.38/0.60 211[0:SpR:20.0,169.0] || -> equal(set_union2(skc36,u),u)**. % 0.38/0.60 249[0:Res:39.0,28.0] || -> in(skf18(u,v),u)* disjoint(u,w)*. % 0.38/0.60 264[0:SpR:177.1,8.0] || disjoint(u,u)* -> equal(skc36,u). % 0.38/0.60 308[0:SpR:20.0,52.0] || -> equal(set_difference(set_union2(u,v),u),set_difference(v,u))**. % 0.38/0.60 310[0:SpR:211.0,52.0] || -> equal(set_difference(u,u),set_difference(skc36,u))*. % 0.38/0.60 312[0:Rew:168.0,310.0] || -> equal(set_difference(u,u),skc36)**. % 0.38/0.60 378[0:SpR:308.0,51.0] || -> equal(set_union2(u,set_difference(v,u)),set_union2(u,set_union2(u,v)))**. % 0.38/0.60 394[0:Rew:51.0,378.0] || -> equal(set_union2(u,set_union2(u,v)),set_union2(u,v))**. % 0.38/0.60 442[0:SpR:394.0,52.0] || -> equal(set_difference(set_union2(u,v),set_union2(u,v)),set_difference(u,set_union2(u,v)))**. % 0.38/0.60 460[0:Rew:312.0,442.0] || -> equal(set_difference(u,set_union2(u,v)),skc36)**. % 0.38/0.60 465[0:SpR:460.0,54.1] || disjoint(u,set_union2(u,v))* -> equal(skc36,u). % 0.38/0.60 841[0:Res:249.1,465.0] || -> in(skf18(u,v),u)* equal(skc36,u). % 0.38/0.60 898[0:EqR:69.1] || in(u,singleton(v))* -> equal(u,v). % 0.38/0.60 901[0:Res:841.0,898.0] || -> equal(singleton(u),skc36) equal(skf18(singleton(u),v),u)**. % 0.38/0.60 907[0:MRR:901.0,166.0] || -> equal(skf18(singleton(u),v),u)**. % 0.38/0.60 940[0:SpR:907.0,38.1] || -> disjoint(u,singleton(v))* in(v,u). % 0.38/0.60 949[0:Res:940.0,28.0] || -> in(u,v) disjoint(singleton(u),v)*. % 0.38/0.60 3118[1:Res:150.0,68.1] || disjoint(singleton(skc5),u)* -> disjoint(skc4,u). % 0.38/0.60 3147[1:Res:949.1,3118.0] || -> in(skc5,u) disjoint(skc4,u)*. % 0.38/0.60 3179[1:Res:3147.1,264.0] || -> in(skc5,skc4)* equal(skc36,skc4). % 0.38/0.60 3180[1:MRR:3179.1,165.0] || -> in(skc5,skc4)*. % 0.38/0.60 3204[1:Res:3180.0,37.0] || -> subset(singleton(skc5),skc4)*l. % 0.38/0.60 3207[1:MRR:3204.0,152.0] || -> . % 0.38/0.60 % SZS output end Refutation % 0.38/0.60 Formulae used in the proof : rc1_xboole_0 t2_xboole_1 idempotence_k3_xboole_0 l1_zfmisc_1 t1_boole t4_boole t6_boole commutativity_k2_xboole_0 d10_xboole_0 symmetry_r1_xboole_0 l2_zfmisc_1 t3_xboole_0 l4_zfmisc_1 d7_xboole_0 t39_xboole_1 t40_xboole_1 t83_xboole_1 t63_xboole_1 d1_tarski % 0.38/0.60 %------------------------------------------------------------------------------