%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU265+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:35:40 EDT 2022 % Result : Theorem 0.68s 0.92s % Output : Refutation 0.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SEU265+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n016.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Mon Jun 20 03:02:09 EDT 2022 % 0.14/0.35 % CPUTime : % 0.68/0.92 % 0.68/0.92 SPASS V 3.9 % 0.68/0.92 SPASS beiseite: Proof found. % 0.68/0.92 % SZS status Theorem % 0.68/0.92 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.68/0.92 SPASS derived 2377 clauses, backtracked 220 clauses, performed 10 splits and kept 1254 clauses. % 0.68/0.92 SPASS allocated 100190 KBytes. % 0.68/0.92 SPASS spent 0:00:00.54 on the problem. % 0.68/0.92 0:00:00.03 for the input. % 0.68/0.92 0:00:00.04 for the FLOTTER CNF translation. % 0.68/0.92 0:00:00.04 for inferences. % 0.68/0.92 0:00:00.01 for the backtracking. % 0.68/0.92 0:00:00.38 for the reduction. % 0.68/0.92 % 0.68/0.92 % 0.68/0.92 Here is a proof with depth 8, length 87 : % 0.68/0.92 % SZS output start Refutation % 0.68/0.92 1[0:Inp] || -> empty(empty_set)*. % 0.68/0.92 5[0:Inp] || -> relation_of2_as_subset(skc8,skc7,skc6)*. % 0.68/0.92 6[0:Inp] || -> element(skf15(u),u)*. % 0.68/0.92 10[0:Inp] empty(u) || -> equal(u,empty_set)*. % 0.68/0.92 13[0:Inp] empty(u) || in(v,u)* -> . % 0.68/0.92 17[0:Inp] || element(u,powerset(cartesian_product2(v,w)))* -> relation(u). % 0.68/0.92 18[0:Inp] || relation_of2_as_subset(u,v,w)* -> relation_of2(u,v,w). % 0.68/0.92 20[0:Inp] || element(u,v)* -> empty(v) in(u,v). % 0.68/0.92 22[0:Inp] || equal(relation_dom_as_subset(skc7,skc6,skc8),skc7)** -> in(skc9,skc7). % 0.68/0.92 24[0:Inp] || relation_of2_as_subset(u,v,w) -> element(u,powerset(cartesian_product2(v,w)))*. % 0.68/0.92 25[0:Inp] || relation_of2(u,v,w) -> element(relation_dom_as_subset(v,w,u),powerset(v))*. % 0.68/0.92 26[0:Inp] || relation_of2(u,v,w) -> equal(relation_dom_as_subset(v,w,u),relation_dom(u))**. % 0.68/0.92 28[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 0.68/0.92 29[0:Inp] empty(u) || in(v,w)* element(w,powerset(u))*+ -> . % 0.68/0.92 30[0:Inp] || in(ordered_pair(skc9,u),skc8)* equal(relation_dom_as_subset(skc7,skc6,skc8),skc7) -> . % 0.68/0.92 31[0:Inp] relation(u) || in(ordered_pair(v,w),u)* -> in(v,relation_dom(u)). % 0.68/0.92 33[0:Inp] || -> equal(u,v) in(skf17(v,u),v)* in(skf17(v,u),u)*. % 0.68/0.92 34[0:Inp] || in(skf12(u,v),v)* in(ordered_pair(skf12(u,v),w),u)*+ -> . % 0.68/0.92 35[0:Inp] || in(u,skc7) -> in(ordered_pair(u,skf8(u)),skc8)* equal(relation_dom_as_subset(skc7,skc6,skc8),skc7). % 0.68/0.92 37[0:Inp] relation(u) || in(v,w)* equal(w,relation_dom(u))*+ -> in(ordered_pair(v,skf10(u,v)),u)*. % 0.68/0.92 38[0:Inp] relation(u) || -> equal(v,relation_dom(u)) in(skf12(u,v),v) in(ordered_pair(skf12(u,v),skf13(v,u)),u)*. % 0.68/0.92 40[0:Rew:26.1,25.1] || relation_of2(u,v,w)*+ -> element(relation_dom(u),powerset(v))*. % 0.68/0.92 41[0:Res:5.0,24.0] || -> element(skc8,powerset(cartesian_product2(skc7,skc6)))*. % 0.68/0.92 42[0:Res:5.0,18.0] || -> relation_of2(skc8,skc7,skc6)*. % 0.68/0.92 57[0:Res:41.0,17.0] || -> relation(skc8)*. % 0.68/0.92 60[0:Res:6.0,20.0] || -> empty(u) in(skf15(u),u)*. % 0.68/0.92 74[1:Spt:22.0] || equal(relation_dom_as_subset(skc7,skc6,skc8),skc7)** -> . % 0.68/0.92 75[1:MRR:35.2,74.0] || in(u,skc7) -> in(ordered_pair(u,skf8(u)),skc8)*. % 0.68/0.92 82[0:Res:42.0,40.0] || -> element(relation_dom(skc8),powerset(skc7))*. % 0.68/0.92 98[0:Res:6.0,29.2] empty(u) || in(v,skf15(powerset(u)))* -> . % 0.68/0.92 102[0:Res:82.0,29.2] empty(skc7) || in(u,relation_dom(skc8))* -> . % 0.68/0.92 119[0:Res:82.0,28.1] || in(u,relation_dom(skc8))* -> element(u,skc7). % 0.68/0.92 123[0:Res:60.1,119.0] || -> empty(relation_dom(skc8)) element(skf15(relation_dom(skc8)),skc7)*. % 0.68/0.92 124[0:Res:123.1,20.0] || -> empty(relation_dom(skc8)) empty(skc7) in(skf15(relation_dom(skc8)),skc7)*. % 0.68/0.92 131[1:SpL:26.1,74.0] || relation_of2(skc8,skc7,skc6)* equal(relation_dom(skc8),skc7) -> . % 0.68/0.92 132[1:MRR:131.0,42.0] || equal(relation_dom(skc8),skc7)** -> . % 0.68/0.92 133[0:Res:60.1,98.1] empty(u) || -> empty(skf15(powerset(u)))*. % 0.68/0.92 135[0:EmS:10.0,133.1] empty(u) || -> equal(skf15(powerset(u)),empty_set)**. % 0.68/0.92 137[0:Rew:135.1,98.1] empty(u) || in(v,empty_set)* -> . % 0.68/0.92 143[0:EmS:137.0,1.0] || in(u,empty_set)* -> . % 0.68/0.92 163[1:Res:75.1,31.1] relation(skc8) || in(u,skc7) -> in(u,relation_dom(skc8))*. % 0.68/0.92 164[1:SSi:163.0,57.0] || in(u,skc7) -> in(u,relation_dom(skc8))*. % 0.68/0.92 166[1:Res:164.1,13.1] empty(relation_dom(skc8)) || in(u,skc7)* -> . % 0.68/0.92 180[0:Res:33.1,143.0] || -> equal(u,empty_set) in(skf17(empty_set,u),u)*. % 0.68/0.92 192[0:Res:180.1,119.0] || -> equal(relation_dom(skc8),empty_set) element(skf17(empty_set,relation_dom(skc8)),skc7)*. % 0.68/0.92 205[1:Res:75.1,34.1] || in(skf12(skc8,u),skc7)*+ in(skf12(skc8,u),u)* -> . % 0.68/0.92 221[2:Spt:124.0] || -> empty(relation_dom(skc8))*. % 0.68/0.92 222[2:MRR:166.0,221.0] || in(u,skc7)* -> . % 0.68/0.92 224[2:EmS:10.0,221.0] || -> equal(relation_dom(skc8),empty_set)**. % 0.68/0.92 232[2:Rew:224.0,132.0] || equal(skc7,empty_set)** -> . % 0.68/0.92 241[0:EqR:37.2] relation(u) || in(v,relation_dom(u)) -> in(ordered_pair(v,skf10(u,v)),u)*. % 0.68/0.92 251[2:Res:180.1,222.0] || -> equal(skc7,empty_set)**. % 0.68/0.92 254[2:MRR:251.0,232.0] || -> . % 0.68/0.92 255[2:Spt:254.0,124.0,221.0] || empty(relation_dom(skc8))* -> . % 0.68/0.92 256[2:Spt:254.0,124.1,124.2] || -> empty(skc7) in(skf15(relation_dom(skc8)),skc7)*. % 0.68/0.92 292[0:Res:38.3,31.1] relation(u) relation(u) || -> equal(v,relation_dom(u)) in(skf12(u,v),v)* in(skf12(u,v),relation_dom(u))*. % 0.68/0.92 302[0:Obv:292.0] relation(u) || -> equal(v,relation_dom(u)) in(skf12(u,v),v)* in(skf12(u,v),relation_dom(u))*. % 0.68/0.92 354[3:Spt:192.0] || -> equal(relation_dom(skc8),empty_set)**. % 0.68/0.92 359[3:Rew:354.0,255.0] || empty(empty_set)* -> . % 0.68/0.92 377[3:MRR:359.0,1.0] || -> . % 0.68/0.92 396[3:Spt:377.0,192.0,354.0] || equal(relation_dom(skc8),empty_set)** -> . % 0.68/0.92 397[3:Spt:377.0,192.1] || -> element(skf17(empty_set,relation_dom(skc8)),skc7)*. % 0.68/0.92 411[4:Spt:256.0] || -> empty(skc7)*. % 0.68/0.92 414[4:MRR:102.0,411.0] || in(u,relation_dom(skc8))* -> . % 0.68/0.92 502[4:Res:180.1,414.0] || -> equal(relation_dom(skc8),empty_set)**. % 0.68/0.92 507[4:MRR:502.0,396.0] || -> . % 0.68/0.92 508[4:Spt:507.0,256.0,411.0] || empty(skc7)* -> . % 0.68/0.92 509[4:Spt:507.0,256.1] || -> in(skf15(relation_dom(skc8)),skc7)*. % 0.68/0.92 514[4:Res:509.0,13.1] empty(skc7) || -> . % 0.68/0.92 1289[0:Res:302.3,119.0] relation(skc8) || -> equal(u,relation_dom(skc8)) in(skf12(skc8,u),u)* element(skf12(skc8,u),skc7)*. % 0.68/0.92 1292[0:SSi:1289.0,57.0] || -> equal(u,relation_dom(skc8)) in(skf12(skc8,u),u)* element(skf12(skc8,u),skc7)*. % 0.68/0.92 2735[0:Res:1292.2,20.0] || -> equal(u,relation_dom(skc8)) in(skf12(skc8,u),u)* empty(skc7) in(skf12(skc8,u),skc7)*. % 0.68/0.92 2736[4:MRR:2735.2,514.0] || -> equal(u,relation_dom(skc8)) in(skf12(skc8,u),u)* in(skf12(skc8,u),skc7)*. % 0.68/0.92 2826[4:Fac:2736.1,2736.2] || -> equal(relation_dom(skc8),skc7) in(skf12(skc8,skc7),skc7)*. % 0.68/0.92 2851[4:MRR:2826.0,132.0] || -> in(skf12(skc8,skc7),skc7)*. % 0.68/0.92 2860[4:Res:2851.0,205.0] || in(skf12(skc8,skc7),skc7)* -> . % 0.68/0.92 2861[4:MRR:2860.0,2851.0] || -> . % 0.68/0.92 2864[1:Spt:2861.0,22.0,74.0] || -> equal(relation_dom_as_subset(skc7,skc6,skc8),skc7)**. % 0.68/0.92 2865[1:Spt:2861.0,22.1] || -> in(skc9,skc7)*. % 0.68/0.92 2871[1:Rew:2864.0,30.1] || in(ordered_pair(skc9,u),skc8)* equal(skc7,skc7) -> . % 0.68/0.92 2872[1:Obv:2871.1] || in(ordered_pair(skc9,u),skc8)* -> . % 0.68/0.92 2884[1:SpR:2864.0,26.1] || relation_of2(skc8,skc7,skc6)* -> equal(relation_dom(skc8),skc7). % 0.68/0.92 2886[1:MRR:2884.0,42.0] || -> equal(relation_dom(skc8),skc7)**. % 0.68/0.92 2991[1:Res:241.2,2872.0] relation(skc8) || in(skc9,relation_dom(skc8))* -> . % 0.68/0.92 2992[1:Rew:2886.0,2991.1] relation(skc8) || in(skc9,skc7)* -> . % 0.68/0.92 2993[1:SSi:2992.0,57.0] || in(skc9,skc7)* -> . % 0.68/0.92 2994[1:MRR:2993.0,2865.0] || -> . % 0.68/0.92 % SZS output end Refutation % 0.68/0.92 Formulae used in the proof : fc1_xboole_0 t22_relset_1 existence_m1_subset_1 t6_boole t7_boole cc1_relset_1 redefinition_m2_relset_1 t2_subset dt_m2_relset_1 dt_k4_relset_1 redefinition_k4_relset_1 t4_subset t5_subset t20_relat_1 t2_tarski antisymmetry_r2_hidden d4_relat_1 % 0.68/0.92 %------------------------------------------------------------------------------