%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU381+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:47 EDT 2022 % Result : Theorem 284.66s 284.89s % Output : Refutation 295.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU381+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n006.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun Jun 19 02:13:10 EDT 2022 % 0.13/0.34 % CPUTime : % 284.66/284.89 % 284.66/284.89 SPASS V 3.9 % 284.66/284.89 SPASS beiseite: Proof found. % 284.66/284.89 % SZS status Theorem % 284.66/284.89 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 284.66/284.89 SPASS derived 91835 clauses, backtracked 3197 clauses, performed 18 splits and kept 55010 clauses. % 284.66/284.89 SPASS allocated 207645 KBytes. % 284.66/284.89 SPASS spent 0:4:44.41 on the problem. % 284.66/284.89 0:00:00.04 for the input. % 284.66/284.89 0:00:00.07 for the FLOTTER CNF translation. % 284.66/284.89 0:00:04.17 for inferences. % 284.66/284.89 0:0:11.07 for the backtracking. % 284.66/284.89 0:4:20.04 for the reduction. % 284.66/284.89 % 284.66/284.89 % 284.66/284.89 Here is a proof with depth 5, length 92 : % 284.66/284.89 % SZS output start Refutation % 284.66/284.89 145[0:Inp] || -> subset(skc26,skc25)*. % 284.66/284.89 146[0:Inp] || -> subset(skc25,skc23)*. % 284.66/284.89 148[0:Inp] || -> rel_str(boole_POSet(u))*. % 284.66/284.89 172[0:Inp] || -> heyting_relstr(boole_POSet(u))*. % 284.66/284.89 174[0:Inp] || -> boolean_relstr(boole_POSet(u))*. % 284.66/284.89 192[0:Inp] || -> strict_rel_str(boole_POSet(u))*. % 284.66/284.89 193[0:Inp] || -> reflexive_relstr(boole_POSet(u))*. % 284.66/284.89 194[0:Inp] || -> transitive_relstr(boole_POSet(u))*. % 284.66/284.89 195[0:Inp] || -> antisymmetric_relstr(boole_POSet(u))*. % 284.66/284.89 196[0:Inp] || -> with_suprema_relstr(boole_POSet(u))*. % 284.66/284.89 197[0:Inp] || -> with_infima_relstr(boole_POSet(u))*. % 284.66/284.89 198[0:Inp] || -> complete_relstr(boole_POSet(u))*. % 284.66/284.89 199[0:Inp] || -> lower_bounded_relstr(boole_POSet(u))*. % 284.66/284.89 200[0:Inp] || -> upper_bounded_relstr(boole_POSet(u))*. % 284.66/284.89 201[0:Inp] || -> bounded_relstr(boole_POSet(u))*. % 284.66/284.89 202[0:Inp] || -> up_complete_relstr(boole_POSet(u))*. % 284.66/284.89 203[0:Inp] || -> join_complete_relstr(boole_POSet(u))*. % 284.66/284.89 204[0:Inp] || -> distributive_relstr(boole_POSet(u))*. % 284.66/284.89 205[0:Inp] || -> complemented_relstr(boole_POSet(u))*. % 284.66/284.89 232[0:Inp] || v1_yellow_3(boole_POSet(u))* -> . % 284.66/284.89 261[0:Inp] || -> element(skc24,powerset(the_carrier(boole_POSet(skc23))))*. % 284.66/284.89 262[0:Inp] || -> element(skf16(u,v),the_carrier(v))*. % 284.66/284.89 263[0:Inp] || -> element(skf15(u,v),the_carrier(v))*. % 284.66/284.89 278[0:Inp] || -> equal(the_carrier(boole_POSet(u)),powerset(u))**. % 284.66/284.89 286[0:Inp] || upper_relstr_subset(skc24,boole_POSet(skc23))* -> in(skc26,skc24). % 284.66/284.89 289[0:Inp] empty_carrier(u) rel_str(u) || -> v1_yellow_3(u)*. % 284.66/284.89 293[0:Inp] || element(u,powerset(v))* -> subset(u,v). % 284.66/284.89 294[0:Inp] || subset(u,v) -> element(u,powerset(v))*. % 284.66/284.89 295[0:Inp] || in(skc25,skc24) upper_relstr_subset(skc24,boole_POSet(skc23))* -> . % 284.66/284.89 346[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 284.66/284.89 369[0:Inp] rel_str(u) || element(v,powerset(the_carrier(u)))*+ -> upper_relstr_subset(v,u) in(skf15(v,u),v)*. % 284.66/284.89 371[0:Inp] rel_str(u) || element(v,powerset(the_carrier(u)))*+ in(skf16(v,u),v)* -> upper_relstr_subset(v,u). % 284.66/284.89 372[0:Inp] || subset(u,v)*+ subset(v,skc23)* in(u,skc24) -> in(v,skc24) upper_relstr_subset(skc24,boole_POSet(skc23))*. % 284.66/284.89 374[0:Inp] rel_str(u) || element(v,powerset(the_carrier(u))) -> upper_relstr_subset(v,u) related(u,skf15(v,u),skf16(v,u))*. % 284.66/284.89 375[0:Inp] || subset(u,v) element(u,the_carrier(boole_POSet(w))) element(v,the_carrier(boole_POSet(w))) -> related_reflexive(boole_POSet(w),u,v)*. % 284.66/284.89 376[0:Inp] || related_reflexive(boole_POSet(u),v,w)* element(v,the_carrier(boole_POSet(u))) element(w,the_carrier(boole_POSet(u))) -> subset(v,w). % 284.66/284.89 401[0:Inp] rel_str(u) reflexive_relstr(u) || element(v,the_carrier(u)) element(w,the_carrier(u)) related(u,v,w) -> empty_carrier(u) related_reflexive(u,v,w)*. % 284.66/284.89 402[0:Inp] rel_str(u) reflexive_relstr(u) || element(v,the_carrier(u)) element(w,the_carrier(u)) related_reflexive(u,v,w)* -> empty_carrier(u) related(u,v,w). % 284.66/284.89 409[0:Inp] rel_str(u) || element(v,the_carrier(u)) element(w,the_carrier(u)) related(u,v,w)* in(v,x)* upper_relstr_subset(x,u) element(x,powerset(the_carrier(u)))* -> in(w,x)*. % 284.66/284.89 410[0:Rew:278.0,261.0] || -> element(skc24,powerset(powerset(skc23)))*. % 284.66/284.89 411[0:Rew:278.0,375.2,278.0,375.1] || subset(u,v) element(v,powerset(w)) element(u,powerset(w)) -> related_reflexive(boole_POSet(w),u,v)*. % 284.66/284.89 412[0:Rew:278.0,376.2,278.0,376.1] || element(u,powerset(v)) element(w,powerset(v)) related_reflexive(boole_POSet(v),w,u)* -> subset(w,u). % 284.66/284.89 417[0:MRR:409.1,346.2] rel_str(u) || upper_relstr_subset(v,u) in(w,v)* element(x,the_carrier(u)) element(v,powerset(the_carrier(u)))*+ related(u,w,x)* -> in(x,v)*. % 284.66/284.89 420[0:Res:146.0,294.0] || -> element(skc25,powerset(skc23))*. % 284.66/284.89 422[0:Res:145.0,411.0] || element(skc25,powerset(u)) element(skc26,powerset(u)) -> related_reflexive(boole_POSet(u),skc26,skc25)*. % 284.66/284.89 431[0:Res:410.0,346.1] || in(u,skc24) -> element(u,powerset(skc23))*. % 284.66/284.89 451[1:Spt:372.0,372.1,372.2,372.3] || subset(u,v)*+ subset(v,skc23)* in(u,skc24) -> in(v,skc24). % 284.66/284.89 452[2:Spt:295.1] || upper_relstr_subset(skc24,boole_POSet(skc23))* -> . % 284.66/284.89 458[1:Res:145.0,451.0] || subset(skc25,skc23)* in(skc26,skc24) -> in(skc25,skc24). % 284.66/284.89 475[0:SpR:278.0,263.0] || -> element(skf15(u,boole_POSet(v)),powerset(v))*. % 284.66/284.89 476[0:SpR:278.0,262.0] || -> element(skf16(u,boole_POSet(v)),powerset(v))*. % 284.66/284.89 481[0:Res:289.2,232.0] empty_carrier(boole_POSet(u)) rel_str(boole_POSet(u)) || -> . % 284.66/284.89 484[0:SSi:481.1,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0] empty_carrier(boole_POSet(u)) || -> . % 284.66/284.89 505[0:Res:476.0,293.0] || -> subset(skf16(u,boole_POSet(v)),v)*. % 284.66/284.89 2743[0:SpL:278.0,369.1] rel_str(boole_POSet(u)) || element(v,powerset(powerset(u))) -> upper_relstr_subset(v,boole_POSet(u)) in(skf15(v,boole_POSet(u)),v)*. % 284.66/284.89 2757[0:SSi:2743.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0] || element(u,powerset(powerset(v))) -> upper_relstr_subset(u,boole_POSet(v)) in(skf15(u,boole_POSet(v)),u)*. % 284.66/284.89 2765[0:SpL:278.0,371.1] rel_str(boole_POSet(u)) || element(v,powerset(powerset(u))) in(skf16(v,boole_POSet(u)),v)* -> upper_relstr_subset(v,boole_POSet(u)). % 284.66/284.89 2779[0:SSi:2765.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0] || element(u,powerset(powerset(v))) in(skf16(u,boole_POSet(v)),u)* -> upper_relstr_subset(u,boole_POSet(v)). % 284.66/284.89 4957[0:Res:401.6,412.2] rel_str(boole_POSet(u)) reflexive_relstr(boole_POSet(u)) || element(v,the_carrier(boole_POSet(u))) element(w,the_carrier(boole_POSet(u))) related(boole_POSet(u),v,w)* element(w,powerset(u)) element(v,powerset(u)) -> empty_carrier(boole_POSet(u)) subset(v,w). % 284.66/284.89 4959[0:Rew:278.0,4957.3,278.0,4957.2] rel_str(boole_POSet(u)) reflexive_relstr(boole_POSet(u)) || element(v,powerset(u)) element(w,powerset(u)) related(boole_POSet(u),v,w)* element(w,powerset(u)) element(v,powerset(u)) -> empty_carrier(boole_POSet(u)) subset(v,w). % 284.66/284.89 4960[0:Obv:4959.3] rel_str(boole_POSet(u)) reflexive_relstr(boole_POSet(u)) || related(boole_POSet(u),v,w)* element(w,powerset(u)) element(v,powerset(u)) -> empty_carrier(boole_POSet(u)) subset(v,w). % 284.66/284.89 4961[0:SSi:4960.1,4960.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0] || related(boole_POSet(u),v,w)* element(w,powerset(u)) element(v,powerset(u)) -> empty_carrier(boole_POSet(u)) subset(v,w). % 284.66/284.89 4962[0:MRR:4961.3,484.0] || related(boole_POSet(u),v,w)* element(w,powerset(u)) element(v,powerset(u)) -> subset(v,w). % 284.66/284.89 5045[0:SpL:278.0,417.4] rel_str(boole_POSet(u)) || upper_relstr_subset(v,boole_POSet(u)) in(w,v)* element(x,the_carrier(boole_POSet(u))) element(v,powerset(powerset(u)))* related(boole_POSet(u),w,x)* -> in(x,v)*. % 284.66/284.89 5062[0:Rew:278.0,5045.3] rel_str(boole_POSet(u)) || upper_relstr_subset(v,boole_POSet(u)) in(w,v)* element(x,powerset(u)) element(v,powerset(powerset(u)))* related(boole_POSet(u),w,x)* -> in(x,v)*. % 284.66/284.89 5063[0:SSi:5062.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0] || upper_relstr_subset(u,boole_POSet(v)) in(w,u)* element(x,powerset(v)) element(u,powerset(powerset(v)))*+ related(boole_POSet(v),w,x)* -> in(x,u)*. % 284.66/284.89 8574[0:Res:374.3,4962.0] rel_str(boole_POSet(u)) || element(v,powerset(the_carrier(boole_POSet(u)))) element(skf16(v,boole_POSet(u)),powerset(u)) element(skf15(v,boole_POSet(u)),powerset(u)) -> upper_relstr_subset(v,boole_POSet(u)) subset(skf15(v,boole_POSet(u)),skf16(v,boole_POSet(u)))*. % 284.66/284.89 8582[0:Rew:278.0,8574.1] rel_str(boole_POSet(u)) || element(v,powerset(powerset(u))) element(skf16(v,boole_POSet(u)),powerset(u)) element(skf15(v,boole_POSet(u)),powerset(u)) -> upper_relstr_subset(v,boole_POSet(u)) subset(skf15(v,boole_POSet(u)),skf16(v,boole_POSet(u)))*. % 295.56/295.76 8583[0:SSi:8582.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0] || element(u,powerset(powerset(v))) element(skf16(u,boole_POSet(v)),powerset(v)) element(skf15(u,boole_POSet(v)),powerset(v)) -> upper_relstr_subset(u,boole_POSet(v)) subset(skf15(u,boole_POSet(v)),skf16(u,boole_POSet(v)))*. % 295.56/295.76 8584[0:MRR:8583.1,8583.2,476.0,475.0] || element(u,powerset(powerset(v))) -> upper_relstr_subset(u,boole_POSet(v)) subset(skf15(u,boole_POSet(v)),skf16(u,boole_POSet(v)))*. % 295.56/295.76 9540[0:Res:410.0,5063.3] || upper_relstr_subset(skc24,boole_POSet(skc23)) in(u,skc24) element(v,powerset(skc23)) related(boole_POSet(skc23),u,v)* -> in(v,skc24). % 295.56/295.76 14582[1:Res:8584.2,451.0] || element(u,powerset(powerset(v))) subset(skf16(u,boole_POSet(v)),skc23)* in(skf15(u,boole_POSet(v)),skc24) -> upper_relstr_subset(u,boole_POSet(v)) in(skf16(u,boole_POSet(v)),skc24). % 295.56/295.76 43443[1:Res:505.0,14582.1] || element(u,powerset(powerset(skc23))) in(skf15(u,boole_POSet(skc23)),skc24) -> upper_relstr_subset(u,boole_POSet(skc23)) in(skf16(u,boole_POSet(skc23)),skc24)*. % 295.56/295.76 105829[1:Res:43443.3,2779.1] || element(skc24,powerset(powerset(skc23))) in(skf15(skc24,boole_POSet(skc23)),skc24)* element(skc24,powerset(powerset(skc23))) -> upper_relstr_subset(skc24,boole_POSet(skc23)) upper_relstr_subset(skc24,boole_POSet(skc23)). % 295.56/295.76 105842[1:Obv:105829.3] || in(skf15(skc24,boole_POSet(skc23)),skc24)* element(skc24,powerset(powerset(skc23))) -> upper_relstr_subset(skc24,boole_POSet(skc23)). % 295.56/295.76 105843[2:MRR:105842.0,105842.1,105842.2,2757.2,410.0,452.0] || -> . % 295.56/295.76 105856[2:Spt:105843.0,295.1,452.0] || -> upper_relstr_subset(skc24,boole_POSet(skc23))*. % 295.56/295.76 105857[2:Spt:105843.0,295.0] || in(skc25,skc24)* -> . % 295.56/295.76 105858[2:MRR:286.0,105856.0] || -> in(skc26,skc24)*. % 295.56/295.76 105860[2:MRR:458.0,458.1,458.2,146.0,105858.0,105857.0] || -> . % 295.56/295.76 105893[1:Spt:105860.0,372.4] || -> upper_relstr_subset(skc24,boole_POSet(skc23))*. % 295.56/295.76 105894[1:MRR:286.0,105893.0] || -> in(skc26,skc24)*. % 295.56/295.76 105895[1:MRR:295.1,105893.0] || in(skc25,skc24)* -> . % 295.56/295.76 105897[1:MRR:9540.0,105893.0] || in(u,skc24) element(v,powerset(skc23)) related(boole_POSet(skc23),u,v)* -> in(v,skc24). % 295.56/295.76 106087[0:Res:422.2,402.4] rel_str(boole_POSet(u)) reflexive_relstr(boole_POSet(u)) || element(skc25,powerset(u)) element(skc26,powerset(u)) element(skc26,the_carrier(boole_POSet(u))) element(skc25,the_carrier(boole_POSet(u))) -> empty_carrier(boole_POSet(u)) related(boole_POSet(u),skc26,skc25)*. % 295.56/295.76 106089[0:Rew:278.0,106087.5,278.0,106087.4] rel_str(boole_POSet(u)) reflexive_relstr(boole_POSet(u)) || element(skc25,powerset(u)) element(skc26,powerset(u)) element(skc26,powerset(u)) element(skc25,powerset(u)) -> empty_carrier(boole_POSet(u)) related(boole_POSet(u),skc26,skc25)*. % 295.56/295.76 106090[0:Obv:106089.3] rel_str(boole_POSet(u)) reflexive_relstr(boole_POSet(u)) || element(skc26,powerset(u)) element(skc25,powerset(u)) -> empty_carrier(boole_POSet(u)) related(boole_POSet(u),skc26,skc25)*. % 295.56/295.76 106091[0:SSi:106090.1,106090.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0,205.0,204.0,172.0,203.0,192.0,174.0,201.0,200.0,198.0,202.0,197.0,199.0,196.0,195.0,194.0,193.0,148.0] || element(skc26,powerset(u)) element(skc25,powerset(u)) -> empty_carrier(boole_POSet(u)) related(boole_POSet(u),skc26,skc25)*. % 295.56/295.76 106092[0:MRR:106091.2,484.0] || element(skc26,powerset(u)) element(skc25,powerset(u)) -> related(boole_POSet(u),skc26,skc25)*. % 295.56/295.76 106855[1:Res:106092.2,105897.2] || element(skc26,powerset(skc23))* element(skc25,powerset(skc23)) in(skc26,skc24) element(skc25,powerset(skc23)) -> in(skc25,skc24). % 295.56/295.76 106858[1:Obv:106855.1] || element(skc26,powerset(skc23))* in(skc26,skc24) element(skc25,powerset(skc23)) -> in(skc25,skc24). % 295.56/295.76 106859[1:MRR:106858.0,106858.1,106858.2,106858.3,431.1,105894.0,420.0,105895.0] || -> . % 295.56/295.76 % SZS output end Refutation % 295.56/295.76 Formulae used in the proof : t11_waybel_7 reflexivity_r1_tarski dt_k3_yellow_1 fc1_waybel_7 fc9_waybel_1 d20_waybel_0 existence_m1_subset_1 t4_waybel_7 cc2_yellow_3 t3_subset t4_subset t2_yellow_1 redefinition_r3_orders_2 % 295.56/295.76 %------------------------------------------------------------------------------