%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU336+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:22 EDT 2022 % Result : Theorem 3.00s 3.25s % Output : Refutation 3.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SEU336+1 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n026.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 03:28:10 EDT 2022 % 0.12/0.33 % CPUTime : % 3.00/3.25 % 3.00/3.25 SPASS V 3.9 % 3.00/3.25 SPASS beiseite: Proof found. % 3.00/3.25 % SZS status Theorem % 3.00/3.25 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 3.00/3.25 SPASS derived 14138 clauses, backtracked 1714 clauses, performed 17 splits and kept 6482 clauses. % 3.00/3.25 SPASS allocated 107702 KBytes. % 3.00/3.25 SPASS spent 0:00:02.91 on the problem. % 3.00/3.25 0:00:00.03 for the input. % 3.00/3.25 0:00:00.03 for the FLOTTER CNF translation. % 3.00/3.25 0:00:00.16 for inferences. % 3.00/3.25 0:00:00.06 for the backtracking. % 3.00/3.25 0:00:02.48 for the reduction. % 3.00/3.25 % 3.00/3.25 % 3.00/3.25 Here is a proof with depth 5, length 107 : % 3.00/3.25 % SZS output start Refutation % 3.00/3.25 1[0:Inp] || -> top_str(skc5)*. % 3.00/3.25 29[0:Inp] top_str(u) || -> one_sorted_str(u)*. % 3.00/3.25 32[0:Inp] || -> element(skc6,powerset(powerset(the_carrier(skc5))))*. % 3.00/3.25 43[0:Inp] || -> closed_subsets(skc6,skc5) open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)*. % 3.00/3.25 76[0:Inp] || closed_subsets(skc6,skc5) open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* -> . % 3.00/3.25 79[0:Inp] || in(u,v)* element(v,powerset(w))*+ -> element(u,w)*. % 3.00/3.25 81[0:Inp] || element(u,powerset(powerset(v))) -> element(complements_of_subsets(v,u),powerset(powerset(v)))*. % 3.00/3.25 82[0:Inp] || element(u,powerset(powerset(v))) -> equal(complements_of_subsets(v,complements_of_subsets(v,u)),u)**. % 3.00/3.25 83[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ -> open_subsets(v,u) in(skf6(v,u),v)*. % 3.00/3.25 84[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ -> closed_subsets(v,u) in(skf7(v,u),v)*. % 3.00/3.25 85[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ open_subset(skf6(v,u),u)* -> open_subsets(v,u). % 3.00/3.25 86[0:Inp] top_str(u) || element(v,powerset(powerset(the_carrier(u))))*+ closed_subset(skf7(v,u),u)* -> closed_subsets(v,u). % 3.00/3.25 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). % 3.00/3.25 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). % 3.00/3.25 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). % 3.00/3.25 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). % 3.00/3.25 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)*. % 3.00/3.25 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)*. % 3.00/3.25 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)*. % 3.00/3.25 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)*. % 3.00/3.25 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)*. % 3.00/3.25 102[0:Res:1.0,85.0] || element(u,powerset(powerset(the_carrier(skc5))))* open_subset(skf6(u,skc5),skc5) -> open_subsets(u,skc5). % 3.00/3.25 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). % 3.00/3.25 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). % 3.00/3.25 109[0:Res:1.0,84.0] || element(u,powerset(powerset(the_carrier(skc5))))*+ -> closed_subsets(u,skc5) in(skf7(u,skc5),u)*. % 3.00/3.25 110[0:Res:1.0,29.0] || -> one_sorted_str(skc5)*. % 3.00/3.25 143[0:Res:32.0,85.2] top_str(skc5) || open_subset(skf6(skc6,skc5),skc5)* -> open_subsets(skc6,skc5). % 3.00/3.25 144[0:Res:32.0,86.2] top_str(skc5) || closed_subset(skf7(skc6,skc5),skc5)* -> closed_subsets(skc6,skc5). % 3.00/3.25 145[0:Res:32.0,83.1] top_str(skc5) || -> in(skf6(skc6,skc5),skc6)* open_subsets(skc6,skc5). % 3.00/3.25 146[0:Res:32.0,84.1] top_str(skc5) || -> in(skf7(skc6,skc5),skc6)* closed_subsets(skc6,skc5). % 3.00/3.25 147[0:Res:32.0,98.3] top_str(skc5) || in(u,skc6) open_subsets(skc6,skc5) -> open_subset(u,skc5)*. % 3.00/3.25 148[0:Res:32.0,97.3] top_str(skc5) || in(u,skc6) closed_subsets(skc6,skc5) -> closed_subset(u,skc5)*. % 3.00/3.25 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)*. % 3.00/3.25 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)*. % 3.00/3.25 155[0:Res:32.0,79.1] || in(u,skc6) -> element(u,powerset(the_carrier(skc5)))*. % 3.00/3.25 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)*. % 3.00/3.25 161[0:Res:32.0,81.0] || -> element(complements_of_subsets(the_carrier(skc5),skc6),powerset(powerset(the_carrier(skc5))))*. % 3.00/3.25 162[0:Res:32.0,82.0] || -> equal(complements_of_subsets(the_carrier(skc5),complements_of_subsets(the_carrier(skc5),skc6)),skc6)**. % 3.00/3.25 164[0:MRR:145.0,1.0] || -> open_subsets(skc6,skc5) in(skf6(skc6,skc5),skc6)*. % 3.00/3.25 165[0:MRR:146.0,1.0] || -> closed_subsets(skc6,skc5) in(skf7(skc6,skc5),skc6)*. % 3.00/3.25 167[0:MRR:143.0,1.0] || open_subset(skf6(skc6,skc5),skc5)* -> open_subsets(skc6,skc5). % 3.00/3.25 168[0:MRR:144.0,1.0] || closed_subset(skf7(skc6,skc5),skc5)* -> closed_subsets(skc6,skc5). % 3.00/3.25 169[0:MRR:147.0,1.0] || in(u,skc6) open_subsets(skc6,skc5) -> open_subset(u,skc5)*. % 3.00/3.25 170[0:MRR:148.0,1.0] || in(u,skc6) closed_subsets(skc6,skc5) -> closed_subset(u,skc5)*. % 3.00/3.25 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)*. % 3.00/3.25 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). % 3.00/3.25 185[1:Spt:180.0] || -> equal(complements_of_subsets(the_carrier(skc5),skc6),skc6)**. % 3.00/3.25 186[1:Rew:185.0,76.1] || closed_subsets(skc6,skc5)* open_subsets(skc6,skc5) -> . % 3.00/3.25 187[1:Rew:185.0,43.1] || -> closed_subsets(skc6,skc5)* open_subsets(skc6,skc5). % 3.00/3.25 193[1:Rew:185.0,173.1] || in(u,skc6) equal(skc6,skc6) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 3.00/3.25 196[1:Obv:193.1] || in(u,skc6) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 3.00/3.25 199[2:Spt:165.0] || -> closed_subsets(skc6,skc5)*. % 3.00/3.25 200[2:MRR:170.1,199.0] || in(u,skc6) -> closed_subset(u,skc5)*. % 3.00/3.25 201[2:MRR:186.0,199.0] || open_subsets(skc6,skc5)* -> . % 3.00/3.25 202[2:MRR:164.0,201.0] || -> in(skf6(skc6,skc5),skc6)*. % 3.00/3.25 203[2:MRR:167.1,201.0] || open_subset(skf6(skc6,skc5),skc5)* -> . % 3.00/3.25 759[0:Res:81.1,79.1] || element(u,powerset(powerset(v)))*+ in(w,complements_of_subsets(v,u))* -> element(w,powerset(v)). % 3.00/3.25 821[0:Res:81.1,83.1] top_str(u) || element(v,powerset(powerset(the_carrier(u)))) -> open_subsets(complements_of_subsets(the_carrier(u),v),u) in(skf6(complements_of_subsets(the_carrier(u),v),u),complements_of_subsets(the_carrier(u),v))*. % 3.00/3.25 833[2:Res:200.1,90.2] top_str(skc5) || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> open_subset(u,skc5). % 3.00/3.25 835[2:SSi:833.0,1.0,110.0] || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> open_subset(u,skc5). % 3.00/3.25 953[0:Res:81.1,98.3] top_str(u) || element(v,powerset(powerset(the_carrier(u))))+ open_subsets(complements_of_subsets(the_carrier(u),v),u)* in(w,complements_of_subsets(the_carrier(u),v))* -> open_subset(w,u). % 3.00/3.25 3662[0:Res:32.0,109.0] || -> closed_subsets(skc6,skc5) in(skf7(skc6,skc5),skc6)*. % 3.00/3.25 4299[0:Res:32.0,759.0] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> element(u,powerset(the_carrier(skc5))). % 3.00/3.25 8541[0:Res:32.0,953.1] top_str(skc5) || open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> open_subset(u,skc5). % 3.00/3.25 11454[2:Res:196.1,835.0] || in(u,skc6) element(u,powerset(the_carrier(skc5)))* -> open_subset(u,skc5). % 3.00/3.25 11456[2:MRR:11454.1,155.1] || in(u,skc6) -> open_subset(u,skc5)*. % 3.13/3.32 11469[2:Res:11456.1,203.0] || in(skf6(skc6,skc5),skc6)* -> . % 3.13/3.32 11473[2:MRR:11469.0,202.0] || -> . % 3.13/3.32 11478[2:Spt:11473.0,165.0,199.0] || closed_subsets(skc6,skc5)* -> . % 3.13/3.32 11479[2:Spt:11473.0,165.1] || -> in(skf7(skc6,skc5),skc6)*. % 3.13/3.32 11480[2:MRR:187.0,11478.0] || -> open_subsets(skc6,skc5)*. % 3.13/3.32 11481[2:MRR:168.1,11478.0] || closed_subset(skf7(skc6,skc5),skc5)* -> . % 3.13/3.32 11483[2:MRR:169.1,11480.0] || in(u,skc6) -> open_subset(u,skc5)*. % 3.13/3.32 11541[2:Res:11483.1,105.1] || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> closed_subset(u,skc5). % 3.13/3.32 11678[2:Res:196.1,11541.0] || in(u,skc6) element(u,powerset(the_carrier(skc5)))* -> closed_subset(u,skc5). % 3.13/3.32 11680[2:MRR:11678.1,155.1] || in(u,skc6) -> closed_subset(u,skc5)*. % 3.13/3.32 11736[2:Res:11680.1,11481.0] || in(skf7(skc6,skc5),skc6)* -> . % 3.13/3.32 11744[2:MRR:11736.0,11479.0] || -> . % 3.13/3.32 11749[1:Spt:11744.0,180.0,185.0] || equal(complements_of_subsets(the_carrier(skc5),skc6),skc6)** -> . % 3.13/3.32 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). % 3.13/3.32 11752[0:SSi:8541.0,1.0,110.0] || open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> open_subset(u,skc5). % 3.13/3.32 11792[2:Spt:43.0] || -> closed_subsets(skc6,skc5)*. % 3.13/3.32 11793[2:MRR:170.1,11792.0] || in(u,skc6) -> closed_subset(u,skc5)*. % 3.13/3.32 11794[2:MRR:76.0,11792.0] || open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)* -> . % 3.13/3.32 11815[2:Res:11793.1,107.1] || in(subset_complement(the_carrier(skc5),u),skc6)* element(u,powerset(the_carrier(skc5))) -> open_subset(u,skc5). % 3.13/3.32 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))*. % 3.13/3.32 11910[0:Res:161.0,102.0] || open_subset(skf6(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)* -> open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5). % 3.13/3.32 11917[2:MRR:11910.1,11794.0] || open_subset(skf6(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)* -> . % 3.13/3.32 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))*. % 3.13/3.32 11920[0:Obv:11919.1] || in(u,skc6) -> in(subset_complement(the_carrier(skc5),u),complements_of_subsets(the_carrier(skc5),skc6))*. % 3.13/3.32 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)*. % 3.13/3.32 12022[0:Obv:12014.1] || in(u,complements_of_subsets(the_carrier(skc5),skc6)) -> in(subset_complement(the_carrier(skc5),u),skc6)*. % 3.13/3.32 14266[2:Res:12022.1,11815.0] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* element(u,powerset(the_carrier(skc5))) -> open_subset(u,skc5). % 3.13/3.32 14272[2:MRR:14266.1,4299.1] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> open_subset(u,skc5). % 3.13/3.32 14291[2:Res:821.3,14272.0] top_str(skc5) || element(skc6,powerset(powerset(the_carrier(skc5)))) -> open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5) open_subset(skf6(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)*. % 3.13/3.32 14302[2:SSi:14291.0,1.0,110.0] || element(skc6,powerset(powerset(the_carrier(skc5)))) -> open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5) open_subset(skf6(complements_of_subsets(the_carrier(skc5),skc6),skc5),skc5)*. % 3.13/3.32 14303[2:MRR:14302.0,14302.1,14302.2,32.0,11794.0,11917.0] || -> . % 3.13/3.32 14306[2:Spt:14303.0,43.0,11792.0] || closed_subsets(skc6,skc5)* -> . % 3.13/3.32 14307[2:Spt:14303.0,43.1] || -> open_subsets(complements_of_subsets(the_carrier(skc5),skc6),skc5)*. % 3.13/3.32 14308[2:MRR:3662.0,14306.0] || -> in(skf7(skc6,skc5),skc6)*. % 3.13/3.32 14309[2:MRR:168.1,14306.0] || closed_subset(skf7(skc6,skc5),skc5)* -> . % 3.13/3.32 14310[2:MRR:11752.0,14307.0] || in(u,complements_of_subsets(the_carrier(skc5),skc6))* -> open_subset(u,skc5). % 3.13/3.32 14383[2:Res:11920.1,14310.0] || in(u,skc6) -> open_subset(subset_complement(the_carrier(skc5),u),skc5)*. % 3.13/3.32 15364[2:Res:14383.1,105.1] || in(u,skc6) element(u,powerset(the_carrier(skc5)))* -> closed_subset(u,skc5). % 3.13/3.32 15365[2:MRR:15364.1,155.1] || in(u,skc6) -> closed_subset(u,skc5)*. % 3.13/3.32 15369[2:Res:15365.1,14309.0] || in(skf7(skc6,skc5),skc6)* -> . % 3.13/3.32 15377[2:MRR:15369.0,14308.0] || -> . % 3.13/3.32 % SZS output end Refutation % 3.13/3.32 Formulae used in the proof : t16_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 % 3.13/3.32 %------------------------------------------------------------------------------