%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU359+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:36 EDT 2022 % Result : Theorem 0.21s 0.48s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : SEU359+1 : TPTP v8.1.0. Released v3.3.0. % 0.13/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n006.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 : Sun Jun 19 09:35:55 EDT 2022 % 0.14/0.36 % CPUTime : % 0.21/0.48 % 0.21/0.48 SPASS V 3.9 % 0.21/0.48 SPASS beiseite: Proof found. % 0.21/0.48 % SZS status Theorem % 0.21/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.48 SPASS derived 117 clauses, backtracked 10 clauses, performed 2 splits and kept 106 clauses. % 0.21/0.48 SPASS allocated 97818 KBytes. % 0.21/0.48 SPASS spent 0:00:00.12 on the problem. % 0.21/0.48 0:00:00.04 for the input. % 0.21/0.48 0:00:00.04 for the FLOTTER CNF translation. % 0.21/0.48 0:00:00.00 for inferences. % 0.21/0.48 0:00:00.00 for the backtracking. % 0.21/0.48 0:00:00.02 for the reduction. % 0.21/0.48 % 0.21/0.48 % 0.21/0.48 Here is a proof with depth 6, length 80 : % 0.21/0.48 % SZS output start Refutation % 0.21/0.48 1[0:Inp] || -> antisymmetric_relstr(skc6)*. % 0.21/0.48 2[0:Inp] || -> rel_str(skc6)*. % 0.21/0.48 5[0:Inp] || -> element(skc7,the_carrier(skc6))*. % 0.21/0.48 7[0:Inp] rel_str(u) || -> one_sorted_str(u)*. % 0.21/0.48 9[0:Inp] || -> element(skf6(u,v,w),the_carrier(w))*. % 0.21/0.48 10[0:Inp] || -> ex_sup_of_relstr_set(u,v) SkP0(v,u,w)*. % 0.21/0.48 11[0:Inp] || -> element(skf7(u,v,w),the_carrier(w))*. % 0.21/0.48 12[0:Inp] || -> element(skf10(u,v,w),the_carrier(w))*. % 0.21/0.48 13[0:Inp] || SkP0(skc8,skc6,skc7)* -> relstr_set_smaller(skc6,skc9,skc7). % 0.21/0.48 14[0:Inp] || -> equal(u,join_on_relstr(v,w)) SkP0(w,v,u)*. % 0.21/0.49 16[0:Inp] || ex_sup_of_relstr_set(skc6,skc9) equal(join_on_relstr(skc6,skc9),skc7) SkP0(skc8,skc6,skc7)* -> . % 0.21/0.49 17[0:Inp] || relstr_set_smaller(u,v,w) -> SkP0(v,u,w) relstr_set_smaller(u,v,skf6(w,v,u))*. % 0.21/0.49 19[0:Inp] || relstr_set_smaller(u,v,w) related(u,w,skf6(w,v,u))* -> SkP0(v,u,w). % 0.21/0.49 20[0:Inp] || element(u,the_carrier(skc6))+ relstr_set_smaller(skc6,skc9,u) SkP0(skc8,skc6,skc7)* -> related(skc6,skc7,u)*. % 0.21/0.49 21[0:Inp] rel_str(u) || ex_sup_of_relstr_set(u,v) element(w,the_carrier(u)) equal(w,join_on_relstr(u,v)) -> relstr_set_smaller(u,v,w)*. % 0.21/0.49 22[0:Inp] rel_str(u) antisymmetric_relstr(u) || element(v,the_carrier(u)) relstr_set_smaller(u,w,v) -> ex_sup_of_relstr_set(u,w) relstr_set_smaller(u,w,skf10(v,w,u))*. % 0.21/0.49 24[0:Inp] rel_str(u) antisymmetric_relstr(u) || element(v,the_carrier(u)) relstr_set_smaller(u,w,v) related(u,v,skf10(v,w,u))* -> ex_sup_of_relstr_set(u,w). % 0.21/0.49 25[0:Inp] rel_str(u) || ex_sup_of_relstr_set(u,v) element(w,the_carrier(u)) relstr_set_smaller(u,v,w) -> equal(w,join_on_relstr(u,v)) relstr_set_smaller(u,v,skf7(w,v,u))*. % 0.21/0.49 26[0:Inp] rel_str(u) || ex_sup_of_relstr_set(u,v) element(w,the_carrier(u)) relstr_set_smaller(u,v,w) related(u,w,skf7(w,v,u))* -> equal(w,join_on_relstr(u,v)). % 0.21/0.49 27[0:Inp] rel_str(u) || ex_sup_of_relstr_set(u,v) element(w,the_carrier(u)) element(x,the_carrier(u)) equal(w,join_on_relstr(u,v))*+ relstr_set_smaller(u,v,x)* -> related(u,w,x)*. % 0.21/0.49 37[0:Res:2.0,7.0] || -> one_sorted_str(skc6)*. % 0.21/0.49 43[0:Res:5.0,22.2] antisymmetric_relstr(skc6) rel_str(skc6) || relstr_set_smaller(skc6,u,skc7) -> relstr_set_smaller(skc6,u,skf10(skc7,u,skc6))* ex_sup_of_relstr_set(skc6,u). % 0.21/0.49 46[0:Res:5.0,26.4] rel_str(skc6) || relstr_set_smaller(skc6,u,skc7) related(skc6,skc7,skf7(skc7,u,skc6))* ex_sup_of_relstr_set(skc6,u) -> equal(join_on_relstr(skc6,u),skc7). % 0.21/0.49 47[0:Res:5.0,25.3] rel_str(skc6) || relstr_set_smaller(skc6,u,skc7) ex_sup_of_relstr_set(skc6,u) -> relstr_set_smaller(skc6,u,skf7(skc7,u,skc6))* equal(join_on_relstr(skc6,u),skc7). % 0.21/0.49 48[0:Res:5.0,24.4] antisymmetric_relstr(skc6) rel_str(skc6) || relstr_set_smaller(skc6,u,skc7) related(skc6,skc7,skf10(skc7,u,skc6))* -> ex_sup_of_relstr_set(skc6,u). % 0.21/0.49 50[0:Res:5.0,27.5] rel_str(skc6) || relstr_set_smaller(skc6,u,v)* equal(join_on_relstr(skc6,u),skc7) element(v,the_carrier(skc6)) ex_sup_of_relstr_set(skc6,u) -> related(skc6,skc7,v)*. % 0.21/0.49 64[0:MRR:43.0,43.1,1.0,2.0] || relstr_set_smaller(skc6,u,skc7) -> ex_sup_of_relstr_set(skc6,u) relstr_set_smaller(skc6,u,skf10(skc7,u,skc6))*. % 0.21/0.49 65[0:MRR:48.0,48.1,1.0,2.0] || relstr_set_smaller(skc6,u,skc7) related(skc6,skc7,skf10(skc7,u,skc6))* -> ex_sup_of_relstr_set(skc6,u). % 0.21/0.49 68[0:MRR:47.0,2.0] || ex_sup_of_relstr_set(skc6,u) relstr_set_smaller(skc6,u,skc7) -> equal(join_on_relstr(skc6,u),skc7) relstr_set_smaller(skc6,u,skf7(skc7,u,skc6))*. % 0.21/0.49 70[0:MRR:46.0,2.0] || ex_sup_of_relstr_set(skc6,u) relstr_set_smaller(skc6,u,skc7) related(skc6,skc7,skf7(skc7,u,skc6))* -> equal(join_on_relstr(skc6,u),skc7). % 0.21/0.49 71[0:MRR:50.0,2.0] || element(u,the_carrier(skc6)) ex_sup_of_relstr_set(skc6,v) equal(join_on_relstr(skc6,v),skc7)+ relstr_set_smaller(skc6,v,u)* -> related(skc6,skc7,u)*. % 0.21/0.49 73[1:Spt:20.0,20.1,20.3] || element(u,the_carrier(skc6)) relstr_set_smaller(skc6,skc9,u) -> related(skc6,skc7,u)*. % 0.21/0.49 74[2:Spt:13.0] || SkP0(skc8,skc6,skc7)* -> . % 0.21/0.49 75[2:Res:10.1,74.0] || -> ex_sup_of_relstr_set(skc6,skc8)*. % 0.21/0.49 76[2:Res:14.1,74.0] || -> equal(join_on_relstr(skc6,skc8),skc7)**. % 0.21/0.49 80[1:Res:73.2,65.1] || element(skf10(skc7,u,skc6),the_carrier(skc6)) relstr_set_smaller(skc6,skc9,skf10(skc7,u,skc6))* relstr_set_smaller(skc6,u,skc7) -> ex_sup_of_relstr_set(skc6,u). % 0.21/0.49 81[1:MRR:80.0,12.0] || relstr_set_smaller(skc6,skc9,skf10(skc7,u,skc6))* relstr_set_smaller(skc6,u,skc7) -> ex_sup_of_relstr_set(skc6,u). % 0.21/0.49 82[1:Res:64.2,81.0] || relstr_set_smaller(skc6,skc9,skc7)* relstr_set_smaller(skc6,skc9,skc7)* -> ex_sup_of_relstr_set(skc6,skc9) ex_sup_of_relstr_set(skc6,skc9). % 0.21/0.49 83[1:Obv:82.2] || relstr_set_smaller(skc6,skc9,skc7)* -> ex_sup_of_relstr_set(skc6,skc9). % 0.21/0.49 111[1:Res:73.2,70.2] || element(skf7(skc7,u,skc6),the_carrier(skc6)) relstr_set_smaller(skc6,skc9,skf7(skc7,u,skc6))* ex_sup_of_relstr_set(skc6,u) relstr_set_smaller(skc6,u,skc7) -> equal(join_on_relstr(skc6,u),skc7). % 0.21/0.49 112[1:MRR:111.0,11.0] || relstr_set_smaller(skc6,skc9,skf7(skc7,u,skc6))* ex_sup_of_relstr_set(skc6,u) relstr_set_smaller(skc6,u,skc7) -> equal(join_on_relstr(skc6,u),skc7). % 0.21/0.49 113[1:Res:68.3,112.0] || ex_sup_of_relstr_set(skc6,skc9) relstr_set_smaller(skc6,skc9,skc7)* ex_sup_of_relstr_set(skc6,skc9) relstr_set_smaller(skc6,skc9,skc7)* -> equal(join_on_relstr(skc6,skc9),skc7) equal(join_on_relstr(skc6,skc9),skc7). % 0.21/0.49 116[1:Obv:113.4] || ex_sup_of_relstr_set(skc6,skc9) relstr_set_smaller(skc6,skc9,skc7)* -> equal(join_on_relstr(skc6,skc9),skc7). % 0.21/0.49 117[1:MRR:116.0,83.1] || relstr_set_smaller(skc6,skc9,skc7)* -> equal(join_on_relstr(skc6,skc9),skc7). % 0.21/0.49 128[2:SpL:76.0,71.2] || element(u,the_carrier(skc6)) ex_sup_of_relstr_set(skc6,skc8) equal(skc7,skc7) relstr_set_smaller(skc6,skc8,u) -> related(skc6,skc7,u)*. % 0.21/0.49 129[2:Obv:128.2] || element(u,the_carrier(skc6)) ex_sup_of_relstr_set(skc6,skc8) relstr_set_smaller(skc6,skc8,u) -> related(skc6,skc7,u)*. % 0.21/0.49 130[2:MRR:129.1,75.0] || element(u,the_carrier(skc6)) relstr_set_smaller(skc6,skc8,u) -> related(skc6,skc7,u)*. % 0.21/0.49 134[2:Res:130.2,19.1] || element(skf6(skc7,u,skc6),the_carrier(skc6)) relstr_set_smaller(skc6,skc8,skf6(skc7,u,skc6))* relstr_set_smaller(skc6,u,skc7) -> SkP0(u,skc6,skc7). % 0.21/0.49 137[2:MRR:134.0,9.0] || relstr_set_smaller(skc6,skc8,skf6(skc7,u,skc6))* relstr_set_smaller(skc6,u,skc7) -> SkP0(u,skc6,skc7). % 0.21/0.49 154[2:Res:17.2,137.0] || relstr_set_smaller(skc6,skc8,skc7) relstr_set_smaller(skc6,skc8,skc7) -> SkP0(skc8,skc6,skc7)* SkP0(skc8,skc6,skc7)*. % 0.21/0.49 156[2:Obv:154.2] || relstr_set_smaller(skc6,skc8,skc7) -> SkP0(skc8,skc6,skc7)*. % 0.21/0.49 157[2:MRR:156.1,74.0] || relstr_set_smaller(skc6,skc8,skc7)* -> . % 0.21/0.49 165[2:Res:21.4,157.0] rel_str(skc6) || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* equal(join_on_relstr(skc6,skc8),skc7) -> . % 0.21/0.49 172[2:Rew:76.0,165.3] rel_str(skc6) || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* equal(skc7,skc7) -> . % 0.21/0.49 173[2:Obv:172.3] rel_str(skc6) || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* -> . % 0.21/0.49 174[2:SSi:173.0,1.0,2.0,37.0] || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* -> . % 0.21/0.49 175[2:MRR:174.0,174.1,75.0,5.0] || -> . % 0.21/0.49 176[2:Spt:175.0,13.0,74.0] || -> SkP0(skc8,skc6,skc7)*. % 0.21/0.49 177[2:Spt:175.0,13.1] || -> relstr_set_smaller(skc6,skc9,skc7)*. % 0.21/0.49 178[2:MRR:83.0,177.0] || -> ex_sup_of_relstr_set(skc6,skc9)*. % 0.21/0.49 180[2:MRR:117.0,177.0] || -> equal(join_on_relstr(skc6,skc9),skc7)**. % 0.21/0.49 185[2:Rew:180.0,16.1] || ex_sup_of_relstr_set(skc6,skc9) equal(skc7,skc7) SkP0(skc8,skc6,skc7)* -> . % 0.21/0.49 186[2:Obv:185.1] || ex_sup_of_relstr_set(skc6,skc9) SkP0(skc8,skc6,skc7)* -> . % 0.21/0.49 187[2:MRR:186.0,186.1,178.0,176.0] || -> . % 0.21/0.49 192[1:Spt:187.0,20.2] || SkP0(skc8,skc6,skc7)* -> . % 0.21/0.49 193[1:Res:10.1,192.0] || -> ex_sup_of_relstr_set(skc6,skc8)*. % 0.21/0.49 194[1:Res:14.1,192.0] || -> equal(join_on_relstr(skc6,skc8),skc7)**. % 0.21/0.49 198[1:SpL:194.0,71.2] || element(u,the_carrier(skc6)) ex_sup_of_relstr_set(skc6,skc8) equal(skc7,skc7) relstr_set_smaller(skc6,skc8,u) -> related(skc6,skc7,u)*. % 0.21/0.49 199[1:Obv:198.2] || element(u,the_carrier(skc6)) ex_sup_of_relstr_set(skc6,skc8) relstr_set_smaller(skc6,skc8,u) -> related(skc6,skc7,u)*. % 0.21/0.49 200[1:MRR:199.1,193.0] || element(u,the_carrier(skc6)) relstr_set_smaller(skc6,skc8,u) -> related(skc6,skc7,u)*. % 0.21/0.49 210[1:Res:200.2,19.1] || element(skf6(skc7,u,skc6),the_carrier(skc6)) relstr_set_smaller(skc6,skc8,skf6(skc7,u,skc6))* relstr_set_smaller(skc6,u,skc7) -> SkP0(u,skc6,skc7). % 0.21/0.49 214[1:MRR:210.0,9.0] || relstr_set_smaller(skc6,skc8,skf6(skc7,u,skc6))* relstr_set_smaller(skc6,u,skc7) -> SkP0(u,skc6,skc7). % 0.21/0.49 229[1:Res:17.2,214.0] || relstr_set_smaller(skc6,skc8,skc7) relstr_set_smaller(skc6,skc8,skc7) -> SkP0(skc8,skc6,skc7)* SkP0(skc8,skc6,skc7)*. % 0.21/0.49 231[1:Obv:229.2] || relstr_set_smaller(skc6,skc8,skc7) -> SkP0(skc8,skc6,skc7)*. % 0.21/0.49 232[1:MRR:231.1,192.0] || relstr_set_smaller(skc6,skc8,skc7)* -> . % 0.21/0.49 245[1:Res:21.4,232.0] rel_str(skc6) || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* equal(join_on_relstr(skc6,skc8),skc7) -> . % 0.21/0.49 252[1:Rew:194.0,245.3] rel_str(skc6) || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* equal(skc7,skc7) -> . % 0.21/0.49 253[1:Obv:252.3] rel_str(skc6) || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* -> . % 0.21/0.49 254[1:SSi:253.0,1.0,2.0,37.0] || ex_sup_of_relstr_set(skc6,skc8) element(skc7,the_carrier(skc6))* -> . % 0.21/0.49 255[1:MRR:254.0,254.1,193.0,5.0] || -> . % 0.21/0.49 % SZS output end Refutation % 0.21/0.49 Formulae used in the proof : t30_yellow_0 existence_m1_subset_1 dt_l1_orders_2 d9_yellow_0 t15_yellow_0 % 0.21/0.49 %------------------------------------------------------------------------------