%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU344+2 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:36:27 EDT 2022 % Result : Theorem 185.20s 185.41s % Output : Refutation 185.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SEU344+2 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n024.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sun Jun 19 03:41:47 EDT 2022 % 0.13/0.35 % CPUTime : % 185.20/185.41 % 185.20/185.41 SPASS V 3.9 % 185.20/185.41 SPASS beiseite: Proof found. % 185.20/185.41 % SZS status Theorem % 185.20/185.41 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 185.20/185.41 SPASS derived 13499 clauses, backtracked 726 clauses, performed 46 splits and kept 9451 clauses. % 185.20/185.41 SPASS allocated 184793 KBytes. % 185.20/185.41 SPASS spent 0:03:04.68 on the problem. % 185.20/185.41 0:00:00.05 for the input. % 185.20/185.41 0:2:53.89 for the FLOTTER CNF translation. % 185.20/185.41 0:00:00.24 for inferences. % 185.20/185.41 0:00:00.06 for the backtracking. % 185.20/185.41 0:00:09.43 for the reduction. % 185.20/185.41 % 185.20/185.41 % 185.20/185.41 Here is a proof with depth 3, length 35 : % 185.20/185.41 % SZS output start Refutation % 185.20/185.41 91[0:Inp] || -> latt_str(boole_lattice(u))*. % 185.20/185.41 98[0:Inp] || -> strict_latt_str(boole_lattice(u))*. % 185.20/185.41 144[0:Inp] || empty_carrier(boole_lattice(u))* -> . % 185.20/185.41 167[0:Inp] || -> element(skc37,the_carrier(boole_lattice(skc35)))*. % 185.20/185.41 168[0:Inp] || -> element(skc36,the_carrier(boole_lattice(skc35)))*. % 185.20/185.41 202[0:Inp] latt_str(u) || -> join_semilatt_str(u)*. % 185.20/185.41 235[0:Inp] || -> subset(u,set_union2(u,v))*r. % 185.20/185.41 407[0:Inp] || -> subset(skc36,skc37) below(boole_lattice(skc35),skc36,skc37)*. % 185.20/185.41 550[0:Inp] || subset(u,v) -> equal(set_union2(u,v),v)**. % 185.20/185.41 577[0:Inp] || subset(skc36,skc37) below(boole_lattice(skc35),skc36,skc37)* -> . % 185.20/185.41 1153[0:Inp] || element(u,the_carrier(boole_lattice(v))) element(w,the_carrier(boole_lattice(v))) -> equal(join(boole_lattice(v),w,u),set_union2(w,u))**. % 185.20/185.41 1335[0:Inp] join_semilatt_str(u) || element(v,the_carrier(u)) element(w,the_carrier(u)) equal(join(u,w,v),v)** -> empty_carrier(u) below(u,w,v). % 185.20/185.41 1336[0:Inp] join_semilatt_str(u) || element(v,the_carrier(u)) element(w,the_carrier(u)) below(u,w,v) -> empty_carrier(u) equal(join(u,w,v),v)**. % 185.20/185.41 1783[0:Res:168.0,1336.2] join_semilatt_str(boole_lattice(skc35)) || below(boole_lattice(skc35),skc36,u) element(u,the_carrier(boole_lattice(skc35))) -> equal(join(boole_lattice(skc35),skc36,u),u)** empty_carrier(boole_lattice(skc35)). % 185.20/185.41 1784[0:Res:168.0,1335.2] join_semilatt_str(boole_lattice(skc35)) || equal(join(boole_lattice(skc35),skc36,u),u)** element(u,the_carrier(boole_lattice(skc35))) -> below(boole_lattice(skc35),skc36,u) empty_carrier(boole_lattice(skc35)). % 185.20/185.41 1800[0:Res:168.0,1153.0] || element(u,the_carrier(boole_lattice(skc35))) -> equal(join(boole_lattice(skc35),skc36,u),set_union2(skc36,u))**. % 185.20/185.41 1965[0:Rew:1800.1,1784.1] join_semilatt_str(boole_lattice(skc35)) || equal(set_union2(skc36,u),u) element(u,the_carrier(boole_lattice(skc35))) -> below(boole_lattice(skc35),skc36,u)* empty_carrier(boole_lattice(skc35)). % 185.20/185.41 1966[0:MRR:1965.4,144.0] join_semilatt_str(boole_lattice(skc35)) || element(u,the_carrier(boole_lattice(skc35))) equal(set_union2(skc36,u),u) -> below(boole_lattice(skc35),skc36,u)*. % 185.20/185.41 1967[0:Rew:1800.1,1783.3] join_semilatt_str(boole_lattice(skc35)) || below(boole_lattice(skc35),skc36,u)* element(u,the_carrier(boole_lattice(skc35))) -> equal(set_union2(skc36,u),u) empty_carrier(boole_lattice(skc35)). % 185.20/185.41 1968[0:MRR:1967.4,144.0] join_semilatt_str(boole_lattice(skc35)) || element(u,the_carrier(boole_lattice(skc35))) below(boole_lattice(skc35),skc36,u)* -> equal(set_union2(skc36,u),u). % 185.20/185.41 2051[0:Res:167.0,1968.2] join_semilatt_str(boole_lattice(skc35)) || below(boole_lattice(skc35),skc36,skc37)* -> equal(set_union2(skc36,skc37),skc37). % 185.20/185.41 2052[0:Res:167.0,1966.2] join_semilatt_str(boole_lattice(skc35)) || equal(set_union2(skc36,skc37),skc37) -> below(boole_lattice(skc35),skc36,skc37)*. % 185.20/185.41 2202[1:Spt:407.1] || -> below(boole_lattice(skc35),skc36,skc37)*. % 185.20/185.41 2203[1:MRR:577.1,2202.0] || subset(skc36,skc37)*r -> . % 185.20/185.41 2204[1:MRR:2051.1,2202.0] join_semilatt_str(boole_lattice(skc35)) || -> equal(set_union2(skc36,skc37),skc37)**. % 185.20/185.41 2719[1:SSi:2204.0,202.0,98.0,91.1] || -> equal(set_union2(skc36,skc37),skc37)**. % 185.20/185.41 7077[1:SpR:2719.0,235.0] || -> subset(skc36,skc37)*r. % 185.20/185.41 7080[1:MRR:7077.0,2203.0] || -> . % 185.20/185.41 7081[1:Spt:7080.0,407.1,2202.0] || below(boole_lattice(skc35),skc36,skc37)* -> . % 185.20/185.41 7082[1:Spt:7080.0,407.0] || -> subset(skc36,skc37)*r. % 185.20/185.41 7103[0:SSi:2052.0,202.0,98.0,91.1] || equal(set_union2(skc36,skc37),skc37) -> below(boole_lattice(skc35),skc36,skc37)*. % 185.20/185.41 7104[1:MRR:7103.1,7081.0] || equal(set_union2(skc36,skc37),skc37)** -> . % 185.20/185.41 18094[1:SpL:550.1,7104.0] || subset(skc36,skc37)*r equal(skc37,skc37) -> . % 185.20/185.41 18098[1:Obv:18094.1] || subset(skc36,skc37)*r -> . % 185.20/185.41 18099[1:MRR:18098.0,7082.0] || -> . % 185.20/185.41 % SZS output end Refutation % 185.20/185.41 Formulae used in the proof : dt_k1_lattice3 fc1_lattice3 t2_lattice3 dt_l3_lattices t7_xboole_1 t12_xboole_1 t1_lattice3 d3_lattices % 185.20/185.41 %------------------------------------------------------------------------------