%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU340+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:24 EDT 2022 % Result : Theorem 1.36s 1.55s % Output : Refutation 1.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU340+1 : TPTP v8.1.0. Released v3.3.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n005.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 : Mon Jun 20 01:02:08 EDT 2022 % 0.12/0.33 % CPUTime : % 1.36/1.55 % 1.36/1.55 SPASS V 3.9 % 1.36/1.55 SPASS beiseite: Proof found. % 1.36/1.55 % SZS status Theorem % 1.36/1.55 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.36/1.55 SPASS derived 3888 clauses, backtracked 29 clauses, performed 2 splits and kept 2241 clauses. % 1.36/1.55 SPASS allocated 102699 KBytes. % 1.36/1.55 SPASS spent 0:00:01.18 on the problem. % 1.36/1.55 0:00:00.04 for the input. % 1.36/1.55 0:00:00.04 for the FLOTTER CNF translation. % 1.36/1.55 0:00:00.08 for inferences. % 1.36/1.55 0:00:00.00 for the backtracking. % 1.36/1.55 0:00:00.96 for the reduction. % 1.36/1.55 % 1.36/1.55 % 1.36/1.55 Here is a proof with depth 8, length 74 : % 1.36/1.55 % SZS output start Refutation % 1.36/1.55 1[0:Inp] || -> transitive_relstr(skc8)*. % 1.36/1.55 2[0:Inp] || -> rel_str(skc8)*. % 1.36/1.55 5[0:Inp] || -> empty(empty_set)*. % 1.36/1.55 7[0:Inp] || -> empty(skf15(u))*. % 1.36/1.55 10[0:Inp] || -> element(skc11,the_carrier(skc8))*. % 1.36/1.55 11[0:Inp] || -> element(skc10,the_carrier(skc8))*. % 1.36/1.55 12[0:Inp] || -> element(skc9,the_carrier(skc8))*. % 1.36/1.55 13[0:Inp] || -> related(skc8,skc10,skc11)*. % 1.36/1.55 14[0:Inp] || -> related(skc8,skc9,skc10)*. % 1.36/1.55 18[0:Inp] || related(skc8,skc9,skc11)* -> . % 1.36/1.55 19[0:Inp] rel_str(u) || -> one_sorted_str(u)*. % 1.36/1.55 22[0:Inp] || -> element(skf15(u),powerset(u))*. % 1.36/1.55 26[0:Inp] empty(u) || -> equal(u,empty_set)*. % 1.36/1.55 31[0:Inp] || element(u,powerset(v))* -> subset(u,v). % 1.36/1.55 32[0:Inp] || subset(u,v) -> element(u,powerset(v))*. % 1.36/1.55 33[0:Inp] || element(u,powerset(cartesian_product2(v,w)))* -> relation(u). % 1.36/1.55 37[0:Inp] || element(u,v)* -> empty(v) in(u,v). % 1.36/1.55 40[0:Inp] rel_str(u) || -> relation_of2_as_subset(the_InternalRel(u),the_carrier(u),the_carrier(u))*. % 1.36/1.55 41[0:Inp] rel_str(u) transitive_relstr(u) || -> is_transitive_in(the_InternalRel(u),the_carrier(u))*. % 1.36/1.55 46[0:Inp] || relation_of2_as_subset(u,v,w) -> element(u,powerset(cartesian_product2(v,w)))*. % 1.36/1.55 48[0:Inp] || in(ordered_pair(u,v),cartesian_product2(w,x))* -> in(v,x). % 1.36/1.55 49[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 1.36/1.55 50[0:Inp] empty(u) || in(v,w)* element(w,powerset(u))*+ -> . % 1.36/1.55 55[0:Inp] rel_str(u) || element(v,the_carrier(u)) element(w,the_carrier(u)) in(ordered_pair(w,v),the_InternalRel(u))* -> related(u,w,v). % 1.36/1.55 56[0:Inp] rel_str(u) || element(v,the_carrier(u)) element(w,the_carrier(u)) related(u,w,v) -> in(ordered_pair(w,v),the_InternalRel(u))*. % 1.36/1.55 57[0:Inp] relation(u) || is_transitive_in(u,v)* in(w,v)* in(x,v)* in(y,v)* in(ordered_pair(x,w),u)*+ in(ordered_pair(y,x),u)* -> in(ordered_pair(y,w),u)*. % 1.36/1.55 63[0:Res:2.0,40.0] || -> relation_of2_as_subset(the_InternalRel(skc8),the_carrier(skc8),the_carrier(skc8))*. % 1.36/1.55 64[0:Res:2.0,19.0] || -> one_sorted_str(skc8)*. % 1.36/1.55 66[0:Res:14.0,56.1] rel_str(skc8) || element(skc9,the_carrier(skc8)) element(skc10,the_carrier(skc8)) -> in(ordered_pair(skc9,skc10),the_InternalRel(skc8))*. % 1.36/1.55 67[0:Res:13.0,56.1] rel_str(skc8) || element(skc10,the_carrier(skc8)) element(skc11,the_carrier(skc8)) -> in(ordered_pair(skc10,skc11),the_InternalRel(skc8))*. % 1.36/1.55 72[0:Res:12.0,37.0] || -> empty(the_carrier(skc8)) in(skc9,the_carrier(skc8))*. % 1.36/1.55 77[0:Res:11.0,37.0] || -> empty(the_carrier(skc8)) in(skc10,the_carrier(skc8))*. % 1.36/1.55 82[0:Res:10.0,37.0] || -> empty(the_carrier(skc8)) in(skc11,the_carrier(skc8))*. % 1.36/1.55 83[0:Res:55.4,18.0] rel_str(skc8) || in(ordered_pair(skc9,skc11),the_InternalRel(skc8))* element(skc9,the_carrier(skc8)) element(skc11,the_carrier(skc8)) -> . % 1.36/1.55 85[0:MRR:66.0,66.1,66.2,2.0,12.0,11.0] || -> in(ordered_pair(skc9,skc10),the_InternalRel(skc8))*. % 1.36/1.55 86[0:MRR:67.0,67.1,67.2,2.0,11.0,10.0] || -> in(ordered_pair(skc10,skc11),the_InternalRel(skc8))*. % 1.36/1.55 99[0:MRR:83.0,83.2,83.3,2.0,12.0,10.0] || in(ordered_pair(skc9,skc11),the_InternalRel(skc8))* -> . % 1.36/1.55 132[0:EmS:26.0,7.0] || -> equal(skf15(u),empty_set)**. % 1.36/1.55 137[0:Rew:132.0,22.0] || -> element(empty_set,powerset(u))*. % 1.36/1.55 142[1:Spt:82.0] || -> empty(the_carrier(skc8))*. % 1.36/1.55 143[1:EmS:26.0,142.0] || -> equal(the_carrier(skc8),empty_set)**. % 1.36/1.55 148[1:Rew:143.0,63.0] || -> relation_of2_as_subset(the_InternalRel(skc8),empty_set,empty_set)*. % 1.36/1.55 183[0:Res:137.0,33.0] || -> relation(empty_set)*. % 1.36/1.55 271[0:Res:46.1,31.0] || relation_of2_as_subset(u,v,w) -> subset(u,cartesian_product2(v,w))*. % 1.36/1.55 272[0:Res:46.1,33.0] || relation_of2_as_subset(u,v,w)* -> relation(u). % 1.36/1.55 277[0:Res:40.1,272.0] rel_str(u) || -> relation(the_InternalRel(u))*. % 1.36/1.55 289[0:Res:137.0,50.2] empty(u) || in(v,empty_set)* -> . % 1.36/1.55 291[0:Res:32.1,50.2] empty(u) || subset(v,u)*+ in(w,v)* -> . % 1.36/1.55 293[0:EmS:289.0,5.0] || in(u,empty_set)* -> . % 1.36/1.55 307[0:Res:46.1,49.1] || relation_of2_as_subset(u,v,w)*+ in(x,u)* -> element(x,cartesian_product2(v,w))*. % 1.36/1.55 494[0:Res:86.0,57.5] relation(the_InternalRel(skc8)) || is_transitive_in(the_InternalRel(skc8),u)* in(skc11,u) in(skc10,u) in(v,u)* in(ordered_pair(v,skc10),the_InternalRel(skc8)) -> in(ordered_pair(v,skc11),the_InternalRel(skc8))*. % 1.36/1.55 800[1:Res:148.0,307.0] || in(u,the_InternalRel(skc8)) -> element(u,cartesian_product2(empty_set,empty_set))*. % 1.36/1.55 802[1:Res:800.1,37.0] || in(u,the_InternalRel(skc8)) -> empty(cartesian_product2(empty_set,empty_set)) in(u,cartesian_product2(empty_set,empty_set))*. % 1.36/1.55 1266[2:Spt:802.0,802.2] || in(u,the_InternalRel(skc8)) -> in(u,cartesian_product2(empty_set,empty_set))*. % 1.36/1.55 1268[2:Res:1266.1,48.0] || in(ordered_pair(u,v),the_InternalRel(skc8))* -> in(v,empty_set). % 1.36/1.55 1277[2:MRR:1268.1,293.0] || in(ordered_pair(u,v),the_InternalRel(skc8))* -> . % 1.36/1.55 1278[2:UnC:1277.0,85.0] || -> . % 1.36/1.55 1281[2:Spt:1278.0,802.1] || -> empty(cartesian_product2(empty_set,empty_set))*. % 1.36/1.55 1283[2:EmS:26.0,1281.0] || -> equal(cartesian_product2(empty_set,empty_set),empty_set)**. % 1.36/1.55 1308[2:SpR:1283.0,271.1] || relation_of2_as_subset(u,empty_set,empty_set)* -> subset(u,empty_set). % 1.36/1.55 1446[2:Res:148.0,1308.0] || -> subset(the_InternalRel(skc8),empty_set)*. % 1.36/1.55 1449[2:Res:1446.0,291.1] empty(empty_set) || in(u,the_InternalRel(skc8))* -> . % 1.36/1.55 1450[2:SSi:1449.0,5.0,183.0] || in(u,the_InternalRel(skc8))* -> . % 1.36/1.55 1451[2:UnC:1450.0,85.0] || -> . % 1.36/1.55 1452[1:Spt:1451.0,82.0,142.0] || empty(the_carrier(skc8))* -> . % 1.36/1.55 1453[1:Spt:1451.0,82.1] || -> in(skc11,the_carrier(skc8))*. % 1.36/1.55 1454[1:MRR:77.0,1452.0] || -> in(skc10,the_carrier(skc8))*. % 1.36/1.55 1455[1:MRR:72.0,1452.0] || -> in(skc9,the_carrier(skc8))*. % 1.36/1.55 1456[0:SSi:494.0,277.0,1.0,2.0,64.1] || is_transitive_in(the_InternalRel(skc8),u)* in(skc11,u) in(skc10,u) in(v,u)* in(ordered_pair(v,skc10),the_InternalRel(skc8))+ -> in(ordered_pair(v,skc11),the_InternalRel(skc8))*. % 1.36/1.55 3204[0:Res:85.0,1456.4] || is_transitive_in(the_InternalRel(skc8),u)* in(skc11,u) in(skc10,u) in(skc9,u) -> in(ordered_pair(skc9,skc11),the_InternalRel(skc8))*. % 1.36/1.55 3211[0:MRR:3204.4,99.0] || is_transitive_in(the_InternalRel(skc8),u)* in(skc11,u) in(skc10,u) in(skc9,u) -> . % 1.36/1.55 4415[0:Res:41.2,3211.0] rel_str(skc8) transitive_relstr(skc8) || in(skc11,the_carrier(skc8))* in(skc10,the_carrier(skc8)) in(skc9,the_carrier(skc8)) -> . % 1.36/1.55 4426[0:SSi:4415.1,4415.0,1.0,2.0,64.0,1.0,2.0,64.0] || in(skc11,the_carrier(skc8))* in(skc10,the_carrier(skc8)) in(skc9,the_carrier(skc8)) -> . % 1.36/1.55 4427[1:MRR:4426.0,4426.1,4426.2,1453.0,1454.0,1455.0] || -> . % 1.36/1.55 % SZS output end Refutation % 1.36/1.55 Formulae used in the proof : t26_orders_2 fc1_xboole_0 rc2_subset_1 dt_l1_orders_2 t6_boole t3_subset cc1_relset_1 t2_subset dt_u1_orders_2 d5_orders_2 dt_m2_relset_1 t106_zfmisc_1 t4_subset t5_subset d9_orders_2 d8_relat_2 % 1.36/1.55 %------------------------------------------------------------------------------