%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SEU241+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:26 EDT 2022 % Result : Theorem 0.21s 0.47s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SEU241+1 : TPTP v8.1.0. Released v3.3.0. % 0.04/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n013.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 23:03:59 EDT 2022 % 0.13/0.34 % CPUTime : % 0.21/0.47 % 0.21/0.47 SPASS V 3.9 % 0.21/0.47 SPASS beiseite: Proof found. % 0.21/0.47 % SZS status Theorem % 0.21/0.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.47 SPASS derived 180 clauses, backtracked 33 clauses, performed 2 splits and kept 146 clauses. % 0.21/0.47 SPASS allocated 97877 KBytes. % 0.21/0.47 SPASS spent 0:00:00.11 on the problem. % 0.21/0.47 0:00:00.04 for the input. % 0.21/0.47 0:00:00.04 for the FLOTTER CNF translation. % 0.21/0.47 0:00:00.00 for inferences. % 0.21/0.47 0:00:00.00 for the backtracking. % 0.21/0.47 0:00:00.01 for the reduction. % 0.21/0.47 % 0.21/0.47 % 0.21/0.47 Here is a proof with depth 3, length 43 : % 0.21/0.47 % SZS output start Refutation % 0.21/0.47 1[0:Inp] || -> relation(skc8)*. % 0.21/0.47 13[0:Inp] || equal(skc10,skc9)** -> . % 0.21/0.47 26[0:Inp] || antisymmetric(skc8) -> in(ordered_pair(skc9,skc10),skc8)*. % 0.21/0.47 27[0:Inp] || antisymmetric(skc8) -> in(ordered_pair(skc10,skc9),skc8)*. % 0.21/0.47 31[0:Inp] relation(u) antisymmetric(u) || -> is_antisymmetric_in(u,relation_field(u))*. % 0.21/0.47 32[0:Inp] relation(u) || is_antisymmetric_in(u,relation_field(u))* -> antisymmetric(u). % 0.21/0.47 38[0:Inp] relation(u) || in(ordered_pair(v,w),u)* -> in(v,relation_field(u)). % 0.21/0.47 39[0:Inp] relation(u) || in(ordered_pair(v,w),u)* -> in(w,relation_field(u)). % 0.21/0.47 40[0:Inp] relation(u) || equal(skf4(v,u),skf3(v,u))** -> is_antisymmetric_in(u,v). % 0.21/0.47 41[0:Inp] relation(u) || -> is_antisymmetric_in(u,v) in(ordered_pair(skf4(v,u),skf3(v,u)),u)*. % 0.21/0.47 42[0:Inp] relation(u) || -> is_antisymmetric_in(u,v) in(ordered_pair(skf3(v,u),skf4(v,u)),u)*. % 0.21/0.47 43[0:Inp] || in(ordered_pair(u,v),skc8)*+ in(ordered_pair(v,u),skc8)* -> antisymmetric(skc8) equal(v,u). % 0.21/0.47 44[0:Inp] relation(u) || is_antisymmetric_in(u,v)* in(w,v)* in(x,v)* in(ordered_pair(w,x),u)* in(ordered_pair(x,w),u)* -> equal(x,w). % 0.21/0.47 47[0:Res:1.0,44.0] || in(u,v)* in(w,v)* is_antisymmetric_in(skc8,v)* in(ordered_pair(u,w),skc8)* in(ordered_pair(w,u),skc8)* -> equal(w,u). % 0.21/0.47 48[0:Res:1.0,41.0] || -> is_antisymmetric_in(skc8,u) in(ordered_pair(skf4(u,skc8),skf3(u,skc8)),skc8)*. % 0.21/0.47 49[0:Res:1.0,42.0] || -> is_antisymmetric_in(skc8,u) in(ordered_pair(skf3(u,skc8),skf4(u,skc8)),skc8)*. % 0.21/0.47 50[0:Res:1.0,40.0] || equal(skf4(u,skc8),skf3(u,skc8))** -> is_antisymmetric_in(skc8,u). % 0.21/0.47 51[0:Res:1.0,38.0] || in(ordered_pair(u,v),skc8)* -> in(u,relation_field(skc8)). % 0.21/0.47 52[0:Res:1.0,39.0] || in(ordered_pair(u,v),skc8)* -> in(v,relation_field(skc8)). % 0.21/0.47 58[0:Res:1.0,32.0] || is_antisymmetric_in(skc8,relation_field(skc8))* -> antisymmetric(skc8). % 0.21/0.47 71[0:Res:47.5,13.0] || is_antisymmetric_in(skc8,u)* in(skc10,u) in(skc9,u) in(ordered_pair(skc10,skc9),skc8)* in(ordered_pair(skc9,skc10),skc8) -> . % 0.21/0.47 74[1:Spt:43.0,43.1,43.3] || in(ordered_pair(u,v),skc8)*+ in(ordered_pair(v,u),skc8)* -> equal(v,u). % 0.21/0.47 75[2:Spt:27.0] || antisymmetric(skc8)* -> . % 0.21/0.47 76[2:MRR:58.1,75.0] || is_antisymmetric_in(skc8,relation_field(skc8))* -> . % 0.21/0.47 177[1:Res:49.1,74.0] || in(ordered_pair(skf4(u,skc8),skf3(u,skc8)),skc8)* -> is_antisymmetric_in(skc8,u) equal(skf4(u,skc8),skf3(u,skc8)). % 0.21/0.47 180[1:MRR:177.2,50.0] || in(ordered_pair(skf4(u,skc8),skf3(u,skc8)),skc8)* -> is_antisymmetric_in(skc8,u). % 0.21/0.47 181[1:MRR:180.0,48.1] || -> is_antisymmetric_in(skc8,u)*. % 0.21/0.47 182[2:UnC:181.0,76.0] || -> . % 0.21/0.47 183[2:Spt:182.0,27.0,75.0] || -> antisymmetric(skc8)*. % 0.21/0.47 184[2:Spt:182.0,27.1] || -> in(ordered_pair(skc10,skc9),skc8)*. % 0.21/0.47 185[2:MRR:26.0,183.0] || -> in(ordered_pair(skc9,skc10),skc8)*. % 0.21/0.47 189[2:Res:184.0,74.0] || in(ordered_pair(skc9,skc10),skc8)* -> equal(skc10,skc9). % 0.21/0.47 192[2:MRR:189.1,13.0] || in(ordered_pair(skc9,skc10),skc8)* -> . % 0.21/0.47 193[2:MRR:192.0,185.0] || -> . % 0.21/0.47 194[1:Spt:193.0,43.2] || -> antisymmetric(skc8)*. % 0.21/0.47 196[1:MRR:26.0,194.0] || -> in(ordered_pair(skc9,skc10),skc8)*. % 0.21/0.47 197[1:MRR:27.0,194.0] || -> in(ordered_pair(skc10,skc9),skc8)*. % 0.21/0.47 198[1:MRR:71.3,71.4,197.0,196.0] || is_antisymmetric_in(skc8,u)* in(skc10,u) in(skc9,u) -> . % 0.21/0.47 199[1:Res:196.0,51.0] || -> in(skc9,relation_field(skc8))*. % 0.21/0.47 200[1:Res:196.0,52.0] || -> in(skc10,relation_field(skc8))*. % 0.21/0.47 247[1:Res:31.2,198.0] relation(skc8) antisymmetric(skc8) || in(skc10,relation_field(skc8))* in(skc9,relation_field(skc8)) -> . % 0.21/0.47 253[1:SSi:247.1,247.0,1.0,194.0,1.0,194.0] || in(skc10,relation_field(skc8))* in(skc9,relation_field(skc8)) -> . % 0.21/0.47 254[1:MRR:253.0,253.1,200.0,199.0] || -> . % 0.21/0.47 % SZS output end Refutation % 0.21/0.47 Formulae used in the proof : l3_wellord1 d4_relat_2 d12_relat_2 t30_relat_1 % 0.21/0.47 %------------------------------------------------------------------------------