%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU337+1 : 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:36:23 EDT 2022 % Result : Theorem 2.89s 3.09s % Output : Refutation 2.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU337+1 : TPTP v8.1.0. Released v3.3.0. % 0.12/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.18/0.34 % DateTime : Mon Jun 20 11:49:59 EDT 2022 % 0.18/0.34 % CPUTime : % 2.89/3.09 % 2.89/3.09 SPASS V 3.9 % 2.89/3.09 SPASS beiseite: Proof found. % 2.89/3.09 % SZS status Theorem % 2.89/3.09 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.89/3.09 SPASS derived 14138 clauses, backtracked 1714 clauses, performed 17 splits and kept 6482 clauses. % 2.89/3.09 SPASS allocated 107703 KBytes. % 2.89/3.09 SPASS spent 0:00:02.74 on the problem. % 2.89/3.09 0:00:00.04 for the input. % 2.89/3.09 0:00:00.03 for the FLOTTER CNF translation. % 2.89/3.09 0:00:00.14 for inferences. % 2.89/3.09 0:00:00.06 for the backtracking. % 2.89/3.09 0:00:02.33 for the reduction. % 2.89/3.09 % 2.89/3.09 % 2.89/3.09 Here is a proof with depth 5, length 107 : % 2.89/3.09 % SZS output start Refutation % 2.89/3.09 1[0:Inp] || -> top_str(skc5)*. % 2.89/3.09 29[0:Inp] top_str(u) || -> one_sorted_str(u)*. % 2.89/3.09 32[0:Inp] || -> element(skc6,powerset(powerset(the_carrier(skc5))))*. % 2.89/3.09 43[0:Inp] || -> open_subsets(skc6,skc5) closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)*. % 2.89/3.09 76[0:Inp] || open_subsets(skc6,skc5) closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* -> . % 2.89/3.09 79[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 2.89/3.09 81[0:Inp] || element(u,powerset(powerset(v))) -> element(complements_of_subsets(v,u),powerset(powerset(v)))*. % 2.89/3.09 82[0:Inp] || element(u,powerset(powerset(v))) -> equal(complements_of_subsets(v,complements_of_subsets(v,u)),u)**. % 2.89/3.09 83[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ -> open_subsets(v,u) in(skf6(v,u),v)*. % 2.89/3.09 84[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ -> closed_subsets(v,u) in(skf7(v,u),v)*. % 2.89/3.09 85[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ open_subset(skf6(v,u),u)* -> open_subsets(v,u). % 2.89/3.09 86[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ closed_subset(skf7(v,u),u)* -> closed_subsets(v,u). % 2.89/3.09 88[0:Inp] top_str(u) || element(v,powerset(the_carrier(u))) open_subset(subset_complement(the_carrier(u),v),u)* -> closed_subset(v,u). % 2.89/3.09 90[0:Inp] top_str(u) || element(v,powerset(the_carrier(u))) closed_subset(subset_complement(the_carrier(u),v),u)* -> open_subset(v,u). % 2.89/3.09 91[0:Inp] top_str(u) || element(v,powerset(the_carrier(u)))* in(v,w)* closed_subsets(w,u) element(w,powerset(powerset(the_carrier(u))))* -> closed_subset(v,u). % 2.89/3.09 92[0:Inp] top_str(u) || element(v,powerset(the_carrier(u)))* in(v,w)* open_subsets(w,u) element(w,powerset(powerset(the_carrier(u))))* -> open_subset(v,u). % 2.89/3.09 93[0:Inp] || element(u,powerset(powerset(v)))+ element(w,powerset(powerset(v))) -> equal(u,complements_of_subsets(v,w)) in(subset_complement(v,skf8(w,u,v)),w)* in(skf8(w,u,v),u)*. % 2.89/3.09 95[0:Inp] || in(u,v)* equal(v,complements_of_subsets(w,x))* element(u,powerset(w)) element(x,powerset(powerset(w)))* element(v,powerset(powerset(w)))* -> in(subset_complement(w,u),x)*. % 2.89/3.09 97[0:MRR:91.1,79.2] top_str(u) || closed_subsets(v,u) in(w,v)* element(v,powerset(powerset(the_carrier(u))))*+ -> closed_subset(w,u)*. % 2.89/3.09 98[0:MRR:92.1,79.2] top_str(u) || open_subsets(v,u) in(w,v)* element(v,powerset(powerset(the_carrier(u))))*+ -> open_subset(w,u)*. % 2.89/3.09 99[0:MRR:95.2,79.2] || in(u,v)* element(v,powerset(powerset(w)))*+ element(x,powerset(powerset(w)))* equal(v,complements_of_subsets(w,x))* -> in(subset_complement(w,u),x)*. % 2.89/3.09 103[0:Res:1.0,86.0] || element(u,powerset(powerset(the_carrier(skc5))))* closed_subset(skf7(u,skc5),skc5) -> closed_subsets(u,skc5). % 2.89/3.09 105[0:Res:1.0,88.0] || element(u,powerset(the_carrier(skc5))) open_subset(subset_complement(the_carrier(skc5),u),skc5)* -> closed_subset(u,skc5). % 2.89/3.09 107[0:Res:1.0,90.0] || element(u,powerset(the_carrier(skc5))) closed_subset(subset_complement(the_carrier(skc5),u),skc5)* -> open_subset(u,skc5). % 2.89/3.09 108[0:Res:1.0,83.0] || element(u,powerset(powerset(the_carrier(skc5))))*+ -> open_subsets(u,skc5) in(skf6(u,skc5),u)*. % 2.89/3.09 110[0:Res:1.0,29.0] || -> one_sorted_str(skc5)*. % 2.89/3.09 143[0:Res:32.0,85.2] top_str(skc5) || open_subset(skf6(skc6,skc5),skc5)* -> open_subsets(skc6,skc5). % 2.89/3.09 144[0:Res:32.0,86.2] top_str(skc5) || closed_subset(skf7(skc6,skc5),skc5)* -> closed_subsets(skc6,skc5). % 2.89/3.09 145[0:Res:32.0,83.1] top_str(skc5) || -> in(skf6(skc6,skc5),skc6)* open_subsets(skc6,skc5). % 2.89/3.09 146[0:Res:32.0,84.1] top_str(skc5) || -> in(skf7(skc6,skc5),skc6)* closed_subsets(skc6,skc5). % 2.89/3.09 147[0:Res:32.0,98.3] top_str(skc5) || in(u,skc6) open_subsets(skc6,skc5) -> open_subset(u,skc5)*. % 2.89/3.09 148[0:Res:32.0,97.3] top_str(skc5) || in(u,skc6) closed_subsets(skc6,skc5) -> closed_subset(u,skc5)*. % 2.89/3.09 152[0:Res:32.0,99.2] || in(u,v)* element(v,powerset(powerset(the_carrier(skc5))))*+ equal(v,complements_of_subsets(the_carrier(skc5),skc6)) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 2.89/3.09 154[0:Res:32.0,99.3] || in(u,skc6) element(v,powerset(powerset(the_carrier(skc5))))*+ equal(complements_of_subsets(the_carrier(skc5),v),skc6) -> in(subset_complement(the_carrier(skc5),u),v)*. % 2.89/3.09 155[0:Res:32.0,79.1] || in(u,skc6) -> element(u,powerset(the_carrier(skc5)))*. % 2.89/3.09 160[0:Res:32.0,93.0] || element(u,powerset(powerset(the_carrier(skc5))))+ -> equal(u,complements_of_subsets(the_carrier(skc5),skc6)) in(subset_complement(the_carrier(skc5),skf8(skc6,u,the_carrier(skc5))),skc6)* in(skf8(skc6,u,the_carrier(skc5)),u)*. % 2.89/3.09 161[0:Res:32.0,81.0] || -> element(complements_of_subsets(the_carrier(skc5),skc6),powerset(powerset(the_carrier(skc5))))*. % 2.89/3.09 162[0:Res:32.0,82.0] || -> equal(complements_of_subsets(the_carrier(skc5),complements_of_subsets(the_carrier(skc5),skc6)),skc6)**. % 2.89/3.09 164[0:MRR:145.0,1.0] || -> open_subsets(skc6,skc5) in(skf6(skc6,skc5),skc6)*. % 2.89/3.09 165[0:MRR:146.0,1.0] || -> closed_subsets(skc6,skc5) in(skf7(skc6,skc5),skc6)*. % 2.89/3.09 167[0:MRR:143.0,1.0] || open_subset(skf6(skc6,skc5),skc5)* -> open_subsets(skc6,skc5). % 2.89/3.09 168[0:MRR:144.0,1.0] || closed_subset(skf7(skc6,skc5),skc5)* -> closed_subsets(skc6,skc5). % 2.89/3.09 169[0:MRR:147.0,1.0] || in(u,skc6) open_subsets(skc6,skc5) -> open_subset(u,skc5)*. % 2.89/3.09 170[0:MRR:148.0,1.0] || in(u,skc6) closed_subsets(skc6,skc5) -> closed_subset(u,skc5)*. % 2.89/3.09 173[0:Res:32.0,152.2] || in(u,skc6) equal(complements_of_subsets(the_carrier(skc5),skc6),skc6) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 2.89/3.09 180[0:Res:32.0,160.0] || -> equal(complements_of_subsets(the_carrier(skc5),skc6),skc6) in(subset_complement(the_carrier(skc5),skf8(skc6,skc6,the_carrier(skc5))),skc6)* in(skf8(skc6,skc6,the_carrier(skc5)),skc6). % 2.89/3.09 185[1:Spt:180.0] || -> equal(complements_of_subsets(the_carrier(skc5),skc6),skc6)**. % 2.89/3.09 186[1:Rew:185.0,76.1] || open_subsets(skc6,skc5) closed_subsets(skc6,skc5)* -> . % 2.89/3.09 187[1:Rew:185.0,43.1] || -> open_subsets(skc6,skc5) closed_subsets(skc6,skc5)*. % 2.89/3.09 193[1:Rew:185.0,173.1] || in(u,skc6) equal(skc6,skc6) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 2.89/3.09 196[1:Obv:193.1] || in(u,skc6) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 2.89/3.09 199[2:Spt:164.0] || -> open_subsets(skc6,skc5)*. % 2.89/3.09 200[2:MRR:169.1,199.0] || in(u,skc6) -> open_subset(u,skc5)*. % 2.89/3.09 201[2:MRR:186.0,199.0] || closed_subsets(skc6,skc5)* -> . % 2.89/3.09 202[2:MRR:165.0,201.0] || -> in(skf7(skc6,skc5),skc6)*. % 2.89/3.09 203[2:MRR:168.1,201.0] || closed_subset(skf7(skc6,skc5),skc5)* -> . % 2.89/3.09 759[0:Res:81.1,79.1] || element(u,powerset(powerset(v)))*+ in(w,complements_of_subsets(v,u))* -> element(w,powerset(v)). % 2.89/3.09 804[0:Res:81.1,84.1] top_str(u) || element(v,powerset(powerset(the_carrier(u)))) -> closed_subsets(complements_of_subsets(the_carrier(u),v),u) in(skf7(complements_of_subsets(the_carrier(u),v),u),complements_of_subsets(the_carrier(u),v))*. % 2.89/3.09 835[2:Res:200.1,88.2] top_str(skc5) || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> closed_subset(u,skc5). % 2.89/3.09 837[2:SSi:835.0,1.0,110.0] || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> closed_subset(u,skc5). % 2.89/3.09 969[0:Res:81.1,97.3] top_str(u) || element(v,powerset(powerset(the_carrier(u))))+ closed_subsets(complements_of_subsets(the_carrier(u),v),u)* in(w,complements_of_subsets(the_carrier(u),v))* -> closed_subset(w,u). % 2.89/3.09 3679[0:Res:32.0,108.0] || -> open_subsets(skc6,skc5) in(skf6(skc6,skc5),skc6)*. % 2.89/3.09 4299[0:Res:32.0,759.0] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> element(u,powerset(the_carrier(skc5))). % 2.89/3.09 8540[0:Res:32.0,969.1] top_str(skc5) || closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> closed_subset(u,skc5). % 2.89/3.09 11454[2:Res:196.1,837.0] || in(u,skc6) element(u,powerset(the_carrier(skc5)))* -> closed_subset(u,skc5). % 2.89/3.09 11456[2:MRR:11454.1,155.1] || in(u,skc6) -> closed_subset(u,skc5)*. % 2.95/3.15 11469[2:Res:11456.1,203.0] || in(skf7(skc6,skc5),skc6)* -> . % 2.95/3.15 11473[2:MRR:11469.0,202.0] || -> . % 2.95/3.15 11478[2:Spt:11473.0,164.0,199.0] || open_subsets(skc6,skc5)* -> . % 2.95/3.15 11479[2:Spt:11473.0,164.1] || -> in(skf6(skc6,skc5),skc6)*. % 2.95/3.15 11480[2:MRR:187.0,11478.0] || -> closed_subsets(skc6,skc5)*. % 2.95/3.15 11481[2:MRR:167.1,11478.0] || open_subset(skf6(skc6,skc5),skc5)* -> . % 2.95/3.15 11483[2:MRR:170.1,11480.0] || in(u,skc6) -> closed_subset(u,skc5)*. % 2.95/3.15 11541[2:Res:11483.1,107.1] || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> open_subset(u,skc5). % 2.95/3.15 11678[2:Res:196.1,11541.0] || in(u,skc6) element(u,powerset(the_carrier(skc5)))* -> open_subset(u,skc5). % 2.95/3.15 11680[2:MRR:11678.1,155.1] || in(u,skc6) -> open_subset(u,skc5)*. % 2.95/3.15 11736[2:Res:11680.1,11481.0] || in(skf6(skc6,skc5),skc6)* -> . % 2.95/3.15 11744[2:MRR:11736.0,11479.0] || -> . % 2.95/3.15 11749[1:Spt:11744.0,180.0,185.0] || equal(complements_of_subsets(the_carrier(skc5),skc6),skc6)** -> . % 2.95/3.15 11750[1:Spt:11744.0,180.1,180.2] || -> in(subset_complement(the_carrier(skc5),skf8(skc6,skc6,the_carrier(skc5))),skc6)* in(skf8(skc6,skc6,the_carrier(skc5)),skc6). % 2.95/3.15 11751[0:SSi:8540.0,1.0,110.0] || closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> closed_subset(u,skc5). % 2.95/3.15 11792[2:Spt:43.0] || -> open_subsets(skc6,skc5)*. % 2.95/3.15 11793[2:MRR:169.1,11792.0] || in(u,skc6) -> open_subset(u,skc5)*. % 2.95/3.15 11794[2:MRR:76.0,11792.0] || closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* -> . % 2.95/3.15 11815[2:Res:11793.1,105.1] || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> closed_subset(u,skc5). % 2.95/3.15 11889[0:Res:161.0,154.1] || in(u,skc6) equal(complements_of_subsets(the_carrier(skc5),complements_of_subsets(the_carrier(skc5),skc6)),skc6) -> in(subset_complement(the_carrier(skc5),u),complements_of_subsets(the_carrier(skc5),skc6))*. % 2.95/3.15 11911[0:Res:161.0,103.0] || closed_subset(skf7(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)* -> closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5). % 2.95/3.15 11917[2:MRR:11911.1,11794.0] || closed_subset(skf7(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)* -> . % 2.95/3.15 11919[0:Rew:162.0,11889.1] || in(u,skc6) equal(skc6,skc6) -> in(subset_complement(the_carrier(skc5),u),complements_of_subsets(the_carrier(skc5),skc6))*. % 2.95/3.15 11920[0:Obv:11919.1] || in(u,skc6) -> in(subset_complement(the_carrier(skc5),u),complements_of_subsets(the_carrier(skc5),skc6))*. % 2.95/3.15 12014[0:Res:161.0,152.1] || in(u,complements_of_subsets(the_carrier(skc5),skc6)) equal(complements_of_subsets(the_carrier(skc5),skc6),complements_of_subsets(the_carrier(skc5),skc6)) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 2.95/3.15 12022[0:Obv:12014.1] || in(u,complements_of_subsets(the_carrier(skc5),skc6)) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 2.95/3.15 14266[2:Res:12022.1,11815.0] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* element(u,powerset(the_carrier(skc5))) -> closed_subset(u,skc5). % 2.95/3.15 14272[2:MRR:14266.1,4299.1] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> closed_subset(u,skc5). % 2.95/3.15 14290[2:Res:804.3,14272.0] top_str(skc5) || element(skc6,powerset(powerset(the_carrier(skc5)))) -> closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5) closed_subset(skf7(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)*. % 2.95/3.15 14304[2:SSi:14290.0,1.0,110.0] || element(skc6,powerset(powerset(the_carrier(skc5)))) -> closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5) closed_subset(skf7(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)*. % 2.95/3.15 14305[2:MRR:14304.0,14304.1,14304.2,32.0,11794.0,11917.0] || -> . % 2.95/3.15 14306[2:Spt:14305.0,43.0,11792.0] || open_subsets(skc6,skc5)* -> . % 2.95/3.15 14307[2:Spt:14305.0,43.1] || -> closed_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)*. % 2.95/3.15 14308[2:MRR:3679.0,14306.0] || -> in(skf6(skc6,skc5),skc6)*. % 2.95/3.15 14309[2:MRR:167.1,14306.0] || open_subset(skf6(skc6,skc5),skc5)* -> . % 2.95/3.15 14310[2:MRR:11751.0,14307.0] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> closed_subset(u,skc5). % 2.95/3.15 14383[2:Res:11920.1,14310.0] || in(u,skc6) -> closed_subset(subset_complement(the_carrier(skc5),u),skc5)*. % 2.95/3.15 15364[2:Res:14383.1,107.1] || in(u,skc6) element(u,powerset(the_carrier(skc5)))* -> open_subset(u,skc5). % 2.95/3.15 15365[2:MRR:15364.1,155.1] || in(u,skc6) -> open_subset(u,skc5)*. % 2.95/3.15 15369[2:Res:15365.1,14309.0] || in(skf6(skc6,skc5),skc6)* -> . % 2.95/3.15 15377[2:MRR:15369.0,14308.0] || -> . % 2.95/3.15 % SZS output end Refutation % 2.95/3.15 Formulae used in the proof : t17_tops_2 dt_l1_pre_topc t4_subset dt_k7_setfam_1 involutiveness_k7_setfam_1 d1_tops_2 existence_m1_subset_1 d2_tops_2 t29_tops_1 t30_tops_1 d8_setfam_1 % 2.95/3.15 %------------------------------------------------------------------------------