%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU119+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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:04 EDT 2022 % Result : Theorem 0.53s 0.71s % Output : Refutation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU119+2 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 20 12:27:29 EDT 2022 % 0.12/0.34 % CPUTime : % 0.53/0.71 % 0.53/0.71 SPASS V 3.9 % 0.53/0.71 SPASS beiseite: Proof found. % 0.53/0.71 % SZS status Theorem % 0.53/0.71 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.53/0.71 SPASS derived 1472 clauses, backtracked 84 clauses, performed 3 splits and kept 619 clauses. % 0.53/0.71 SPASS allocated 86270 KBytes. % 0.53/0.71 SPASS spent 0:00:00.35 on the problem. % 0.53/0.71 0:00:00.03 for the input. % 0.53/0.71 0:00:00.05 for the FLOTTER CNF translation. % 0.53/0.71 0:00:00.02 for inferences. % 0.53/0.71 0:00:00.00 for the backtracking. % 0.53/0.71 0:00:00.22 for the reduction. % 0.53/0.71 % 0.53/0.71 % 0.53/0.71 Here is a proof with depth 8, length 52 : % 0.53/0.71 % SZS output start Refutation % 0.53/0.71 3[0:Inp] || -> disjoint(skc10,skc9)*. % 0.53/0.71 5[0:Inp] || -> equal(set_intersection2(u,u),u)**. % 0.53/0.71 6[0:Inp] || -> SkP0(skc7,skc8) in(skc11,skc10)*. % 0.53/0.71 7[0:Inp] || -> SkP0(skc7,skc8) in(skc11,skc9)*. % 0.53/0.71 8[0:Inp] || -> equal(set_intersection2(u,v),set_intersection2(v,u))*. % 0.53/0.71 9[0:Inp] || -> equal(u,empty_set) in(skf2(u),u)*. % 0.53/0.71 11[0:Inp] || SkP0(u,v) disjoint(v,u)* -> . % 0.53/0.71 13[0:Inp] || in(u,v)* equal(v,empty_set) -> . % 0.53/0.71 14[0:Inp] || disjoint(u,v) -> equal(set_intersection2(u,v),empty_set)**. % 0.53/0.71 15[0:Inp] || equal(set_intersection2(u,v),empty_set)** -> disjoint(u,v). % 0.53/0.71 16[0:Inp] || SkP0(u,v)*+ in(w,u)* in(w,v)* -> . % 0.53/0.71 18[0:Inp] || in(u,v)* equal(v,set_intersection2(w,x))*+ -> in(u,x)*. % 0.53/0.71 19[0:Inp] || in(u,v)* in(u,w)* equal(x,set_intersection2(w,v))*+ -> in(u,x)*. % 0.53/0.71 23[0:Res:3.0,14.0] || -> equal(set_intersection2(skc10,skc9),empty_set)**. % 0.53/0.71 27[0:Rew:8.0,23.0] || -> equal(set_intersection2(skc9,skc10),empty_set)**. % 0.53/0.71 55[0:SpL:8.0,15.0] || equal(set_intersection2(u,v),empty_set)** -> disjoint(v,u). % 0.53/0.71 84[0:EqR:18.1] || in(u,set_intersection2(v,w))* -> in(u,w). % 0.53/0.71 85[0:SpL:5.0,18.1] || in(u,v)*+ equal(v,w)* -> in(u,w)*. % 0.53/0.71 97[0:Res:9.1,84.0] || -> equal(set_intersection2(u,v),empty_set) in(skf2(set_intersection2(u,v)),v)*. % 0.53/0.71 120[0:EqR:19.2] || in(u,v) in(u,w) -> in(u,set_intersection2(w,v))*. % 0.53/0.71 138[0:SpR:8.0,97.1] || -> equal(set_intersection2(u,v),empty_set) in(skf2(set_intersection2(v,u)),v)*. % 0.53/0.71 330[0:Res:7.1,85.0] || equal(skc9,u) -> SkP0(skc7,skc8) in(skc11,u)*. % 0.53/0.71 331[0:Res:6.1,85.0] || equal(skc10,u) -> SkP0(skc7,skc8) in(skc11,u)*. % 0.53/0.71 414[1:Spt:330.0,330.2] || equal(skc9,u) -> in(skc11,u)*. % 0.53/0.71 488[2:Spt:331.0,331.2] || equal(skc10,u) -> in(skc11,u)*. % 0.53/0.71 507[0:SpR:27.0,120.2] || in(u,skc10)* in(u,skc9) -> in(u,empty_set). % 0.53/0.71 697[2:Res:488.1,507.0] || equal(skc10,skc10) in(skc11,skc9)* -> in(skc11,empty_set). % 0.53/0.71 711[2:Obv:697.0] || in(skc11,skc9)* -> in(skc11,empty_set). % 0.53/0.71 730[2:Res:414.1,711.0] || equal(skc9,skc9) -> in(skc11,empty_set)*. % 0.53/0.71 731[2:Obv:730.0] || -> in(skc11,empty_set)*. % 0.53/0.71 734[2:Res:731.0,13.0] || equal(empty_set,empty_set)* -> . % 0.53/0.71 738[2:Obv:734.0] || -> . % 0.53/0.71 739[2:Spt:738.0,331.1] || -> SkP0(skc7,skc8)*. % 0.53/0.71 742[2:Res:739.0,16.0] || in(u,skc7) in(u,skc8)* -> . % 0.53/0.71 803[2:Res:97.1,742.1] || in(skf2(set_intersection2(u,skc8)),skc7)* -> equal(set_intersection2(u,skc8),empty_set). % 0.53/0.71 1142[2:Res:138.1,803.0] || -> equal(set_intersection2(skc8,skc7),empty_set)** equal(set_intersection2(skc7,skc8),empty_set). % 0.53/0.71 1145[2:Rew:8.0,1142.0] || -> equal(set_intersection2(skc7,skc8),empty_set)** equal(set_intersection2(skc7,skc8),empty_set)**. % 0.53/0.71 1146[2:Obv:1145.0] || -> equal(set_intersection2(skc7,skc8),empty_set)**. % 0.53/0.71 1159[2:SpL:1146.0,55.0] || equal(empty_set,empty_set) -> disjoint(skc8,skc7)*. % 0.53/0.71 1170[2:Obv:1159.0] || -> disjoint(skc8,skc7)*. % 0.53/0.71 1177[2:Res:1170.0,11.1] || SkP0(skc7,skc8)* -> . % 0.53/0.71 1178[2:MRR:1177.0,739.0] || -> . % 0.53/0.71 1179[1:Spt:1178.0,330.1] || -> SkP0(skc7,skc8)*. % 0.53/0.71 1183[1:Res:1179.0,16.0] || in(u,skc7) in(u,skc8)* -> . % 0.53/0.71 1204[1:Res:97.1,1183.1] || in(skf2(set_intersection2(u,skc8)),skc7)* -> equal(set_intersection2(u,skc8),empty_set). % 0.53/0.71 1710[1:Res:138.1,1204.0] || -> equal(set_intersection2(skc8,skc7),empty_set)** equal(set_intersection2(skc7,skc8),empty_set). % 0.53/0.71 1714[1:Rew:8.0,1710.0] || -> equal(set_intersection2(skc7,skc8),empty_set)** equal(set_intersection2(skc7,skc8),empty_set)**. % 0.53/0.71 1715[1:Obv:1714.0] || -> equal(set_intersection2(skc7,skc8),empty_set)**. % 0.53/0.71 1778[1:SpL:1715.0,55.0] || equal(empty_set,empty_set) -> disjoint(skc8,skc7)*. % 0.53/0.71 1788[1:Obv:1778.0] || -> disjoint(skc8,skc7)*. % 0.53/0.71 1797[1:Res:1788.0,11.1] || SkP0(skc7,skc8)* -> . % 0.53/0.71 1798[1:MRR:1797.0,1179.0] || -> . % 0.53/0.71 % SZS output end Refutation % 0.53/0.71 Formulae used in the proof : t3_xboole_0 d1_xboole_0 idempotence_k3_xboole_0 d3_xboole_0 d7_xboole_0 commutativity_k3_xboole_0 % 0.53/0.71 %------------------------------------------------------------------------------