%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.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 : Sat Jul 16 11:48:41 EDT 2022
% Result : Theorem 1.07s 1.24s
% Output : Refutation 1.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 26
% Syntax : Number of clauses : 42 ( 18 unt; 17 nHn; 42 RR)
% Number of literals : 240 ( 0 equ; 168 neg)
% Maximal clause size : 22 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
v1_funct_1(skc14),
file('GRP653+1.p',unknown),
[] ).
cnf(2,axiom,
v3_group_1(skc12),
file('GRP653+1.p',unknown),
[] ).
cnf(3,axiom,
v4_group_1(skc12),
file('GRP653+1.p',unknown),
[] ).
cnf(4,axiom,
l1_group_1(skc12),
file('GRP653+1.p',unknown),
[] ).
cnf(5,axiom,
v3_group_1(skc13),
file('GRP653+1.p',unknown),
[] ).
cnf(6,axiom,
v4_group_1(skc13),
file('GRP653+1.p',unknown),
[] ).
cnf(7,axiom,
l1_group_1(skc13),
file('GRP653+1.p',unknown),
[] ).
cnf(8,axiom,
v2_funct_1(skc14),
file('GRP653+1.p',unknown),
[] ).
cnf(21,axiom,
~ v3_struct_0(skc13),
file('GRP653+1.p',unknown),
[] ).
cnf(22,axiom,
~ v3_struct_0(skc12),
file('GRP653+1.p',unknown),
[] ).
cnf(27,axiom,
v1_group_6(skc14,skc12,skc13),
file('GRP653+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ l1_group_1(u)
| l1_struct_0(u) ),
file('GRP653+1.p',unknown),
[] ).
cnf(41,axiom,
v1_funct_2(skc14,u1_struct_0(skc12),u1_struct_0(skc13)),
file('GRP653+1.p',unknown),
[] ).
cnf(42,axiom,
m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13)),
file('GRP653+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w)))
| v1_relat_1(u) ),
file('GRP653+1.p',unknown),
[] ).
cnf(66,axiom,
~ m1_lattice4(k3_latsubgr(skc12,skc13,skc14),k11_group_4(skc12),k11_group_4(skc13)),
file('GRP653+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ m2_relset_1(u,v,w)
| m1_subset_1(u,k1_zfmisc_1(k2_zfmisc_1(v,w))) ),
file('GRP653+1.p',unknown),
[] ).
cnf(76,axiom,
( ~ l1_group_1(u)
| ~ v4_group_1(u)
| ~ v3_group_1(u)
| v3_struct_0(u)
| l3_lattices(k11_group_4(u)) ),
file('GRP653+1.p',unknown),
[] ).
cnf(84,axiom,
( ~ l1_group_1(u)
| ~ v4_group_1(u)
| ~ v3_group_1(u)
| v3_struct_0(u)
| v10_lattices(k11_group_4(u)) ),
file('GRP653+1.p',unknown),
[] ).
cnf(90,axiom,
( ~ l1_group_1(u)
| ~ v4_group_1(u)
| ~ v3_group_1(u)
| ~ v3_struct_0(k11_group_4(u))
| v3_struct_0(u) ),
file('GRP653+1.p',unknown),
[] ).
cnf(99,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ l3_lattices(v)
| ~ v10_lattices(v)
| ~ m3_vectsp_8(w,v,u)
| v3_struct_0(u)
| v3_struct_0(v)
| v1_funct_1(w) ),
file('GRP653+1.p',unknown),
[] ).
cnf(103,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ l3_lattices(v)
| ~ v10_lattices(v)
| ~ m3_vectsp_8(w,v,u)
| v3_struct_0(u)
| v3_struct_0(v)
| m2_relset_1(w,u1_struct_0(v),u1_struct_0(u)) ),
file('GRP653+1.p',unknown),
[] ).
cnf(104,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ l3_lattices(v)
| ~ v10_lattices(v)
| ~ m3_vectsp_8(w,v,u)
| v3_struct_0(u)
| v3_struct_0(v)
| v1_funct_2(w,u1_struct_0(v),u1_struct_0(u)) ),
file('GRP653+1.p',unknown),
[] ).
cnf(112,axiom,
( ~ v10_lattices(u)
| ~ l3_lattices(u)
| ~ v10_lattices(v)
| ~ l3_lattices(v)
| ~ v1_funct_1(w)
| ~ m3_vectsp_8(w,u,v)
| ~ m4_vectsp_8(w,u,v)
| ~ v1_funct_2(w,u1_struct_0(u),u1_struct_0(v))
| ~ m2_relset_1(w,u1_struct_0(u),u1_struct_0(v))
| m1_lattice4(w,u,v)
| v3_struct_0(u)
| v3_struct_0(v) ),
file('GRP653+1.p',unknown),
[] ).
cnf(118,axiom,
( ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ l1_group_1(w)
| ~ v4_group_1(w)
| ~ v3_group_1(w)
| ~ v1_group_6(u,w,v)
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| v3_struct_0(v)
| v3_struct_0(w)
| m4_vectsp_8(k3_latsubgr(w,v,u),k11_group_4(w),k11_group_4(v)) ),
file('GRP653+1.p',unknown),
[] ).
cnf(119,axiom,
( ~ v2_funct_1(u)
| ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ l1_group_1(w)
| ~ v4_group_1(w)
| ~ v3_group_1(w)
| ~ v1_group_6(u,w,v)
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| v3_struct_0(v)
| v3_struct_0(w)
| m3_vectsp_8(k3_latsubgr(w,v,u),k11_group_4(w),k11_group_4(v)) ),
file('GRP653+1.p',unknown),
[] ).
cnf(122,plain,
( ~ l3_lattices(u)
| ~ v10_lattices(u)
| ~ l3_lattices(v)
| ~ v10_lattices(v)
| ~ m4_vectsp_8(w,v,u)
| ~ m3_vectsp_8(w,v,u)
| v3_struct_0(u)
| v3_struct_0(v)
| m1_lattice4(w,v,u) ),
inference(mrr,[status(thm)],[112,99,104,103]),
[iquote('0:MRR:112.4,112.7,112.8,99.5,104.5,103.5')] ).
cnf(142,plain,
l1_struct_0(skc13),
inference(res,[status(thm),theory(equality)],[7,34]),
[iquote('0:Res:7.0,34.0')] ).
cnf(189,plain,
( ~ v3_group_1(u)
| ~ v4_group_1(u)
| ~ l1_group_1(u)
| ~ v4_group_1(skc13)
| ~ l1_group_1(skc13)
| ~ v1_funct_1(v)
| ~ v2_funct_1(v)
| ~ v1_group_6(v,u,skc13)
| ~ m2_relset_1(v,u1_struct_0(u),u1_struct_0(skc13))
| ~ v1_funct_2(v,u1_struct_0(u),u1_struct_0(skc13))
| v3_struct_0(u)
| v3_struct_0(skc13)
| m3_vectsp_8(k3_latsubgr(u,skc13,v),k11_group_4(u),k11_group_4(skc13)) ),
inference(res,[status(thm),theory(equality)],[5,119]),
[iquote('0:Res:5.0,119.3')] ).
cnf(212,plain,
l1_struct_0(skc12),
inference(res,[status(thm),theory(equality)],[4,34]),
[iquote('0:Res:4.0,34.0')] ).
cnf(285,plain,
( ~ v2_funct_1(u)
| ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ v1_group_6(u,v,skc13)
| ~ v1_funct_2(u,u1_struct_0(v),u1_struct_0(skc13))
| ~ m2_relset_1(u,u1_struct_0(v),u1_struct_0(skc13))
| v3_struct_0(v)
| m3_vectsp_8(k3_latsubgr(v,skc13,u),k11_group_4(v),k11_group_4(skc13)) ),
inference(mrr,[status(thm)],[189,6,7,21]),
[iquote('0:MRR:189.3,189.4,189.11,6.0,7.0,21.0')] ).
cnf(352,plain,
( ~ m2_relset_1(u,v,w)
| v1_relat_1(u) ),
inference(res,[status(thm),theory(equality)],[67,58]),
[iquote('0:Res:67.1,58.0')] ).
cnf(355,plain,
v1_relat_1(skc14),
inference(res,[status(thm),theory(equality)],[42,352]),
[iquote('0:Res:42.0,352.0')] ).
cnf(1217,plain,
( ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ l1_group_1(w)
| ~ v4_group_1(w)
| ~ v3_group_1(w)
| ~ l3_lattices(k11_group_4(v))
| ~ v10_lattices(k11_group_4(v))
| ~ l3_lattices(k11_group_4(w))
| ~ v10_lattices(k11_group_4(w))
| ~ v1_group_6(u,w,v)
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| ~ m3_vectsp_8(k3_latsubgr(w,v,u),k11_group_4(w),k11_group_4(v))
| v3_struct_0(v)
| v3_struct_0(w)
| v3_struct_0(k11_group_4(v))
| v3_struct_0(k11_group_4(w))
| m1_lattice4(k3_latsubgr(w,v,u),k11_group_4(w),k11_group_4(v)) ),
inference(res,[status(thm),theory(equality)],[118,122]),
[iquote('0:Res:118.12,122.4')] ).
cnf(1219,plain,
( ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ l1_group_1(w)
| ~ v4_group_1(w)
| ~ v3_group_1(w)
| ~ v1_group_6(u,w,v)
| ~ m2_relset_1(u,u1_struct_0(w),u1_struct_0(v))
| ~ v1_funct_2(u,u1_struct_0(w),u1_struct_0(v))
| ~ m3_vectsp_8(k3_latsubgr(w,v,u),k11_group_4(w),k11_group_4(v))
| v3_struct_0(v)
| v3_struct_0(w)
| m1_lattice4(k3_latsubgr(w,v,u),k11_group_4(w),k11_group_4(v)) ),
inference(mrr,[status(thm)],[1217,76,84,90]),
[iquote('0:MRR:1217.7,1217.8,1217.9,1217.10,1217.17,1217.18,76.4,84.4,76.4,84.4,90.3,90.3')] ).
cnf(2219,plain,
( ~ v2_funct_1(u)
| ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ v1_funct_1(u)
| ~ l1_group_1(skc13)
| ~ v4_group_1(skc13)
| ~ v3_group_1(skc13)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ v1_group_6(u,v,skc13)
| ~ v1_funct_2(u,u1_struct_0(v),u1_struct_0(skc13))
| ~ m2_relset_1(u,u1_struct_0(v),u1_struct_0(skc13))
| ~ v1_group_6(u,v,skc13)
| ~ m2_relset_1(u,u1_struct_0(v),u1_struct_0(skc13))
| ~ v1_funct_2(u,u1_struct_0(v),u1_struct_0(skc13))
| v3_struct_0(v)
| v3_struct_0(skc13)
| v3_struct_0(v)
| m1_lattice4(k3_latsubgr(v,skc13,u),k11_group_4(v),k11_group_4(skc13)) ),
inference(res,[status(thm),theory(equality)],[285,1219]),
[iquote('0:Res:285.9,1219.10')] ).
cnf(2225,plain,
( ~ v2_funct_1(u)
| ~ v1_funct_1(u)
| ~ l1_group_1(skc13)
| ~ v4_group_1(skc13)
| ~ v3_group_1(skc13)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ v1_group_6(u,v,skc13)
| ~ m2_relset_1(u,u1_struct_0(v),u1_struct_0(skc13))
| ~ v1_funct_2(u,u1_struct_0(v),u1_struct_0(skc13))
| v3_struct_0(skc13)
| v3_struct_0(v)
| m1_lattice4(k3_latsubgr(v,skc13,u),k11_group_4(v),k11_group_4(skc13)) ),
inference(obv,[status(thm),theory(equality)],[2219]),
[iquote('0:Obv:2219.18')] ).
cnf(2226,plain,
( ~ v2_funct_1(u)
| ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ v1_group_6(u,v,skc13)
| ~ m2_relset_1(u,u1_struct_0(v),u1_struct_0(skc13))
| ~ v1_funct_2(u,u1_struct_0(v),u1_struct_0(skc13))
| v3_struct_0(skc13)
| v3_struct_0(v)
| m1_lattice4(k3_latsubgr(v,skc13,u),k11_group_4(v),k11_group_4(skc13)) ),
inference(ssi,[status(thm)],[2225,6,5,7,142]),
[iquote('0:SSi:2225.4,2225.3,2225.2,6.0,5.0,7.0,142.0,6.0,5.0,7.0,142.0,6.0,5.0,7.0,142.0')] ).
cnf(2227,plain,
( ~ v2_funct_1(u)
| ~ v1_funct_1(u)
| ~ l1_group_1(v)
| ~ v4_group_1(v)
| ~ v3_group_1(v)
| ~ v1_group_6(u,v,skc13)
| ~ m2_relset_1(u,u1_struct_0(v),u1_struct_0(skc13))
| ~ v1_funct_2(u,u1_struct_0(v),u1_struct_0(skc13))
| v3_struct_0(v)
| m1_lattice4(k3_latsubgr(v,skc13,u),k11_group_4(v),k11_group_4(skc13)) ),
inference(mrr,[status(thm)],[2226,21]),
[iquote('0:MRR:2226.8,21.0')] ).
cnf(3547,plain,
( ~ v2_funct_1(skc14)
| ~ v1_funct_1(skc14)
| ~ l1_group_1(skc12)
| ~ v4_group_1(skc12)
| ~ v3_group_1(skc12)
| ~ v1_group_6(skc14,skc12,skc13)
| ~ m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| ~ v1_funct_2(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| v3_struct_0(skc12) ),
inference(res,[status(thm),theory(equality)],[2227,66]),
[iquote('0:Res:2227.9,66.0')] ).
cnf(3552,plain,
( ~ v1_group_6(skc14,skc12,skc13)
| ~ m2_relset_1(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| ~ v1_funct_2(skc14,u1_struct_0(skc12),u1_struct_0(skc13))
| v3_struct_0(skc12) ),
inference(ssi,[status(thm)],[3547,3,2,4,212,8,1,355]),
[iquote('0:SSi:3547.4,3547.3,3547.2,3547.1,3547.0,3.0,2.0,4.0,212.0,3.0,2.0,4.0,212.0,3.0,2.0,4.0,212.0,8.0,1.0,355.0,8.0,1.0,355.0')] ).
cnf(3553,plain,
$false,
inference(mrr,[status(thm)],[3552,27,42,41,22]),
[iquote('0:MRR:3552.0,3552.1,3552.2,3552.3,27.0,42.0,41.0,22.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0.
% 0.04/0.14 % Command : run_spass %d %s
% 0.14/0.36 % Computer : n027.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Tue Jun 14 12:20:03 EDT 2022
% 0.14/0.36 % CPUTime :
% 1.07/1.24
% 1.07/1.24 SPASS V 3.9
% 1.07/1.24 SPASS beiseite: Proof found.
% 1.07/1.24 % SZS status Theorem
% 1.07/1.24 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.07/1.24 SPASS derived 2923 clauses, backtracked 0 clauses, performed 0 splits and kept 1836 clauses.
% 1.07/1.24 SPASS allocated 101565 KBytes.
% 1.07/1.24 SPASS spent 0:00:00.85 on the problem.
% 1.07/1.24 0:00:00.04 for the input.
% 1.07/1.24 0:00:00.05 for the FLOTTER CNF translation.
% 1.07/1.24 0:00:00.07 for inferences.
% 1.07/1.24 0:00:00.00 for the backtracking.
% 1.07/1.24 0:00:00.60 for the reduction.
% 1.07/1.24
% 1.07/1.24
% 1.07/1.24 Here is a proof with depth 3, length 42 :
% 1.07/1.24 % SZS output start Refutation
% See solution above
% 1.07/1.24 Formulae used in the proof : t38_latsubgr dt_l1_group_1 cc1_relset_1 dt_m2_relset_1 dt_k11_group_4 fc1_group_4 dt_m3_vectsp_8 t11_vectsp_8 t37_latsubgr t36_latsubgr
% 1.07/1.24
%------------------------------------------------------------------------------