%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n008.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 10:14:32 EDT 2022
% Result : Theorem 1.00s 1.39s
% Output : Proof 1.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n008.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Tue Jun 14 12:08:52 EDT 2022
% 0.11/0.33 % CPUTime :
% 1.00/1.39 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.00/1.39 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.00/1.40
% 1.00/1.40 %-----------------------------------------------------
% 1.00/1.40 fof(t38_latsubgr, conjecture, ! [_157061] : (~ v3_struct_0(_157061) & v3_group_1(_157061) & v4_group_1(_157061) & l1_group_1(_157061) => ! [_157099] : (~ v3_struct_0(_157099) & v3_group_1(_157099) & v4_group_1(_157099) & l1_group_1(_157099) => ! [_157137] : (v1_funct_1(_157137) & v1_funct_2(_157137, u1_struct_0(_157061), u1_struct_0(_157099)) & v1_group_6(_157137, _157061, _157099) & m2_relset_1(_157137, u1_struct_0(_157061), u1_struct_0(_157099)) => v2_funct_1(_157137) => m1_lattice4(k3_latsubgr(_157061, _157099, _157137), k11_group_4(_157061), k11_group_4(_157099))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t38_latsubgr)).
% 1.00/1.40 fof(dt_k11_group_4, axiom, ! [_157838] : (~ v3_struct_0(_157838) & v3_group_1(_157838) & v4_group_1(_157838) & l1_group_1(_157838) => ~ v3_struct_0(k11_group_4(_157838)) & v3_lattices(k11_group_4(_157838)) & v10_lattices(k11_group_4(_157838)) & l3_lattices(k11_group_4(_157838))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_k11_group_4)).
% 1.00/1.40 fof(dt_m3_vectsp_8, axiom, ! [_158172, _158175] : (~ v3_struct_0(_158172) & v10_lattices(_158172) & l3_lattices(_158172) & ~ v3_struct_0(_158175) & v10_lattices(_158175) & l3_lattices(_158175) => ! [_158229] : (m3_vectsp_8(_158229, _158172, _158175) => v1_funct_1(_158229) & v1_funct_2(_158229, u1_struct_0(_158172), u1_struct_0(_158175)) & m2_relset_1(_158229, u1_struct_0(_158172), u1_struct_0(_158175)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', dt_m3_vectsp_8)).
% 1.00/1.40 fof(t11_vectsp_8, axiom, ! [_158683] : (~ v3_struct_0(_158683) & v10_lattices(_158683) & l3_lattices(_158683) => ! [_158714] : (~ v3_struct_0(_158714) & v10_lattices(_158714) & l3_lattices(_158714) => ! [_158745] : (v1_funct_1(_158745) & v1_funct_2(_158745, u1_struct_0(_158683), u1_struct_0(_158714)) & m2_relset_1(_158745, u1_struct_0(_158683), u1_struct_0(_158714)) => (m1_lattice4(_158745, _158683, _158714) <=> m4_vectsp_8(_158745, _158683, _158714) & m3_vectsp_8(_158745, _158683, _158714))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t11_vectsp_8)).
% 1.00/1.40 fof(t36_latsubgr, axiom, ! [_159196] : (~ v3_struct_0(_159196) & v3_group_1(_159196) & v4_group_1(_159196) & l1_group_1(_159196) => ! [_159234] : (~ v3_struct_0(_159234) & v3_group_1(_159234) & v4_group_1(_159234) & l1_group_1(_159234) => ! [_159272] : (v1_funct_1(_159272) & v1_funct_2(_159272, u1_struct_0(_159196), u1_struct_0(_159234)) & v1_group_6(_159272, _159196, _159234) & m2_relset_1(_159272, u1_struct_0(_159196), u1_struct_0(_159234)) => v2_funct_1(_159272) => m3_vectsp_8(k3_latsubgr(_159196, _159234, _159272), k11_group_4(_159196), k11_group_4(_159234))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t36_latsubgr)).
% 1.00/1.40 fof(t37_latsubgr, axiom, ! [_159776] : (~ v3_struct_0(_159776) & v3_group_1(_159776) & v4_group_1(_159776) & l1_group_1(_159776) => ! [_159814] : (~ v3_struct_0(_159814) & v3_group_1(_159814) & v4_group_1(_159814) & l1_group_1(_159814) => ! [_159852] : (v1_funct_1(_159852) & v1_funct_2(_159852, u1_struct_0(_159776), u1_struct_0(_159814)) & v1_group_6(_159852, _159776, _159814) & m2_relset_1(_159852, u1_struct_0(_159776), u1_struct_0(_159814)) => m4_vectsp_8(k3_latsubgr(_159776, _159814, _159852), k11_group_4(_159776), k11_group_4(_159814))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t37_latsubgr)).
% 1.00/1.40
% 1.00/1.40 cnf(1, plain, [v3_struct_0(21 ^ [])], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(2, plain, [-(v3_group_1(21 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(3, plain, [-(v4_group_1(21 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(4, plain, [-(l1_group_1(21 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(5, plain, [v3_struct_0(22 ^ [])], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(6, plain, [-(v3_group_1(22 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(7, plain, [-(v4_group_1(22 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(8, plain, [-(l1_group_1(22 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(9, plain, [-(v1_funct_1(23 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(10, plain, [-(v1_funct_2(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(11, plain, [-(v1_group_6(23 ^ [], 21 ^ [], 22 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(12, plain, [-(m2_relset_1(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(13, plain, [-(v2_funct_1(23 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(14, plain, [m1_lattice4(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ []))], clausify(t38_latsubgr)).
% 1.00/1.40 cnf(15, plain, [v3_struct_0(k11_group_4(_71313)), -(v3_struct_0(_71313)), v3_group_1(_71313), v4_group_1(_71313), l1_group_1(_71313)], clausify(dt_k11_group_4)).
% 1.00/1.40 cnf(16, plain, [-(v10_lattices(k11_group_4(_71313))), -(v3_struct_0(_71313)), v3_group_1(_71313), v4_group_1(_71313), l1_group_1(_71313)], clausify(dt_k11_group_4)).
% 1.00/1.40 cnf(17, plain, [-(l3_lattices(k11_group_4(_71313))), -(v3_struct_0(_71313)), v3_group_1(_71313), v4_group_1(_71313), l1_group_1(_71313)], clausify(dt_k11_group_4)).
% 1.00/1.40 cnf(18, plain, [-(v1_funct_1(_77863)), m3_vectsp_8(_77863, _77317, _77423), -(v3_struct_0(_77317)), v10_lattices(_77317), l3_lattices(_77317), -(v3_struct_0(_77423)), v10_lattices(_77423), l3_lattices(_77423)], clausify(dt_m3_vectsp_8)).
% 1.00/1.40 cnf(19, plain, [-(v1_funct_2(_77863, u1_struct_0(_77317), u1_struct_0(_77423))), m3_vectsp_8(_77863, _77317, _77423), -(v3_struct_0(_77317)), v10_lattices(_77317), l3_lattices(_77317), -(v3_struct_0(_77423)), v10_lattices(_77423), l3_lattices(_77423)], clausify(dt_m3_vectsp_8)).
% 1.00/1.40 cnf(20, plain, [-(m2_relset_1(_77863, u1_struct_0(_77317), u1_struct_0(_77423))), m3_vectsp_8(_77863, _77317, _77423), -(v3_struct_0(_77317)), v10_lattices(_77317), l3_lattices(_77317), -(v3_struct_0(_77423)), v10_lattices(_77423), l3_lattices(_77423)], clausify(dt_m3_vectsp_8)).
% 1.00/1.40 cnf(21, plain, [l3_lattices(_93109), v10_lattices(_93109), -(v3_struct_0(_93109)), l3_lattices(_93389), v10_lattices(_93389), -(v3_struct_0(_93389)), m2_relset_1(_93651, u1_struct_0(_93109), u1_struct_0(_93389)), v1_funct_2(_93651, u1_struct_0(_93109), u1_struct_0(_93389)), v1_funct_1(_93651), -(m1_lattice4(_93651, _93109, _93389)), m4_vectsp_8(_93651, _93109, _93389), m3_vectsp_8(_93651, _93109, _93389)], clausify(t11_vectsp_8)).
% 1.00/1.40 cnf(22, plain, [l1_group_1(_95215), v4_group_1(_95215), v3_group_1(_95215), -(v3_struct_0(_95215)), l1_group_1(_95564), v4_group_1(_95564), v3_group_1(_95564), -(v3_struct_0(_95564)), -(m3_vectsp_8(k3_latsubgr(_95215, _95564, _95890), k11_group_4(_95215), k11_group_4(_95564))), v2_funct_1(_95890), v1_funct_1(_95890), v1_funct_2(_95890, u1_struct_0(_95215), u1_struct_0(_95564)), v1_group_6(_95890, _95215, _95564), m2_relset_1(_95890, u1_struct_0(_95215), u1_struct_0(_95564))], clausify(t36_latsubgr)).
% 1.00/1.40 cnf(23, plain, [l1_group_1(_96825), v4_group_1(_96825), v3_group_1(_96825), -(v3_struct_0(_96825)), l1_group_1(_97169), v4_group_1(_97169), v3_group_1(_97169), -(v3_struct_0(_97169)), -(m4_vectsp_8(k3_latsubgr(_96825, _97169, _97490), k11_group_4(_96825), k11_group_4(_97169))), v1_funct_1(_97490), v1_funct_2(_97490, u1_struct_0(_96825), u1_struct_0(_97169)), v1_group_6(_97490, _96825, _97169), m2_relset_1(_97490, u1_struct_0(_96825), u1_struct_0(_97169))], clausify(t37_latsubgr)).
% 1.00/1.40
% 1.00/1.40 cnf('1',plain,[v3_struct_0(22 ^ [])],start(5)).
% 1.00/1.40 cnf('1.1',plain,[-(v3_struct_0(22 ^ [])), l1_group_1(21 ^ []), v4_group_1(21 ^ []), v3_group_1(21 ^ []), -(v3_struct_0(21 ^ [])), l1_group_1(22 ^ []), v4_group_1(22 ^ []), v3_group_1(22 ^ []), -(m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ []))), v2_funct_1(23 ^ []), v1_funct_1(23 ^ []), v1_funct_2(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])), v1_group_6(23 ^ [], 21 ^ [], 22 ^ []), m2_relset_1(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ []))],extension(22,bind([[_95890, _95215, _95564], [23 ^ [], 21 ^ [], 22 ^ []]]))).
% 1.00/1.40 cnf('1.1.1',plain,[-(l1_group_1(21 ^ []))],extension(4)).
% 1.00/1.40 cnf('1.1.2',plain,[-(v4_group_1(21 ^ []))],extension(3)).
% 1.00/1.40 cnf('1.1.3',plain,[-(v3_group_1(21 ^ []))],extension(2)).
% 1.00/1.40 cnf('1.1.4',plain,[v3_struct_0(21 ^ [])],extension(1)).
% 1.00/1.40 cnf('1.1.5',plain,[-(l1_group_1(22 ^ []))],extension(8)).
% 1.00/1.40 cnf('1.1.6',plain,[-(v4_group_1(22 ^ []))],extension(7)).
% 1.00/1.40 cnf('1.1.7',plain,[-(v3_group_1(22 ^ []))],extension(6)).
% 1.00/1.40 cnf('1.1.8',plain,[m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])), l3_lattices(k11_group_4(21 ^ [])), v10_lattices(k11_group_4(21 ^ [])), -(v3_struct_0(k11_group_4(21 ^ []))), l3_lattices(k11_group_4(22 ^ [])), v10_lattices(k11_group_4(22 ^ [])), -(v3_struct_0(k11_group_4(22 ^ []))), m2_relset_1(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), u1_struct_0(k11_group_4(21 ^ [])), u1_struct_0(k11_group_4(22 ^ []))), v1_funct_2(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), u1_struct_0(k11_group_4(21 ^ [])), u1_struct_0(k11_group_4(22 ^ []))), v1_funct_1(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ [])), -(m1_lattice4(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ []))), m4_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ []))],extension(21,bind([[_93651, _93109, _93389], [k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])]]))).
% 1.00/1.40 cnf('1.1.8.1',plain,[-(l3_lattices(k11_group_4(21 ^ []))), -(v3_struct_0(21 ^ [])), v3_group_1(21 ^ []), v4_group_1(21 ^ []), l1_group_1(21 ^ [])],extension(17,bind([[_71313], [21 ^ []]]))).
% 1.00/1.40 cnf('1.1.8.1.1',plain,[v3_struct_0(21 ^ [])],extension(1)).
% 1.00/1.40 cnf('1.1.8.1.2',plain,[-(v3_group_1(21 ^ []))],extension(2)).
% 1.00/1.40 cnf('1.1.8.1.3',plain,[-(v4_group_1(21 ^ []))],extension(3)).
% 1.00/1.40 cnf('1.1.8.1.4',plain,[-(l1_group_1(21 ^ []))],extension(4)).
% 1.00/1.40 cnf('1.1.8.2',plain,[-(v10_lattices(k11_group_4(21 ^ []))), -(v3_struct_0(21 ^ [])), v3_group_1(21 ^ []), v4_group_1(21 ^ []), l1_group_1(21 ^ [])],extension(16,bind([[_71313], [21 ^ []]]))).
% 1.00/1.40 cnf('1.1.8.2.1',plain,[v3_struct_0(21 ^ [])],extension(1)).
% 1.00/1.40 cnf('1.1.8.2.2',plain,[-(v3_group_1(21 ^ []))],extension(2)).
% 1.00/1.40 cnf('1.1.8.2.3',plain,[-(v4_group_1(21 ^ []))],extension(3)).
% 1.00/1.40 cnf('1.1.8.2.4',plain,[-(l1_group_1(21 ^ []))],extension(4)).
% 1.00/1.40 cnf('1.1.8.3',plain,[v3_struct_0(k11_group_4(21 ^ [])), -(v3_struct_0(21 ^ [])), v3_group_1(21 ^ []), v4_group_1(21 ^ []), l1_group_1(21 ^ [])],extension(15,bind([[_71313], [21 ^ []]]))).
% 1.00/1.40 cnf('1.1.8.3.1',plain,[v3_struct_0(21 ^ [])],extension(1)).
% 1.00/1.40 cnf('1.1.8.3.2',plain,[-(v3_group_1(21 ^ []))],extension(2)).
% 1.00/1.40 cnf('1.1.8.3.3',plain,[-(v4_group_1(21 ^ []))],extension(3)).
% 1.00/1.40 cnf('1.1.8.3.4',plain,[-(l1_group_1(21 ^ []))],extension(4)).
% 1.00/1.40 cnf('1.1.8.4',plain,[-(l3_lattices(k11_group_4(22 ^ []))), -(v3_struct_0(22 ^ [])), v3_group_1(22 ^ []), v4_group_1(22 ^ []), l1_group_1(22 ^ [])],extension(17,bind([[_71313], [22 ^ []]]))).
% 1.00/1.40 cnf('1.1.8.4.1',plain,[v3_struct_0(22 ^ [])],extension(5)).
% 1.00/1.40 cnf('1.1.8.4.2',plain,[-(v3_group_1(22 ^ []))],extension(6)).
% 1.00/1.40 cnf('1.1.8.4.3',plain,[-(v4_group_1(22 ^ []))],extension(7)).
% 1.00/1.40 cnf('1.1.8.4.4',plain,[-(l1_group_1(22 ^ []))],extension(8)).
% 1.00/1.40 cnf('1.1.8.5',plain,[-(v10_lattices(k11_group_4(22 ^ []))), -(v3_struct_0(22 ^ [])), v3_group_1(22 ^ []), v4_group_1(22 ^ []), l1_group_1(22 ^ [])],extension(16,bind([[_71313], [22 ^ []]]))).
% 1.00/1.40 cnf('1.1.8.5.1',plain,[v3_struct_0(22 ^ [])],extension(5)).
% 1.00/1.40 cnf('1.1.8.5.2',plain,[-(v3_group_1(22 ^ []))],extension(6)).
% 1.00/1.40 cnf('1.1.8.5.3',plain,[-(v4_group_1(22 ^ []))],extension(7)).
% 1.00/1.40 cnf('1.1.8.5.4',plain,[-(l1_group_1(22 ^ []))],extension(8)).
% 1.00/1.40 cnf('1.1.8.6',plain,[v3_struct_0(k11_group_4(22 ^ [])), -(v3_struct_0(22 ^ [])), v3_group_1(22 ^ []), v4_group_1(22 ^ []), l1_group_1(22 ^ [])],extension(15,bind([[_71313], [22 ^ []]]))).
% 1.00/1.40 cnf('1.1.8.6.1',plain,[v3_struct_0(22 ^ [])],extension(5)).
% 1.00/1.40 cnf('1.1.8.6.2',plain,[-(v3_group_1(22 ^ []))],extension(6)).
% 1.00/1.40 cnf('1.1.8.6.3',plain,[-(v4_group_1(22 ^ []))],extension(7)).
% 1.00/1.40 cnf('1.1.8.6.4',plain,[-(l1_group_1(22 ^ []))],extension(8)).
% 1.00/1.40 cnf('1.1.8.7',plain,[-(m2_relset_1(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), u1_struct_0(k11_group_4(21 ^ [])), u1_struct_0(k11_group_4(22 ^ [])))), m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])), -(v3_struct_0(k11_group_4(21 ^ []))), v10_lattices(k11_group_4(21 ^ [])), l3_lattices(k11_group_4(21 ^ [])), -(v3_struct_0(k11_group_4(22 ^ []))), v10_lattices(k11_group_4(22 ^ [])), l3_lattices(k11_group_4(22 ^ []))],extension(20,bind([[_77863, _77317, _77423], [k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])]]))).
% 1.00/1.40 cnf('1.1.8.7.1',plain,[-(m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])))],reduction('1.1')).
% 1.00/1.40 cnf('1.1.8.7.2',plain,[v3_struct_0(k11_group_4(21 ^ []))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.7.3',plain,[-(v10_lattices(k11_group_4(21 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.7.4',plain,[-(l3_lattices(k11_group_4(21 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.7.5',plain,[v3_struct_0(k11_group_4(22 ^ []))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.7.6',plain,[-(v10_lattices(k11_group_4(22 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.7.7',plain,[-(l3_lattices(k11_group_4(22 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.8',plain,[-(v1_funct_2(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), u1_struct_0(k11_group_4(21 ^ [])), u1_struct_0(k11_group_4(22 ^ [])))), m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])), -(v3_struct_0(k11_group_4(21 ^ []))), v10_lattices(k11_group_4(21 ^ [])), l3_lattices(k11_group_4(21 ^ [])), -(v3_struct_0(k11_group_4(22 ^ []))), v10_lattices(k11_group_4(22 ^ [])), l3_lattices(k11_group_4(22 ^ []))],extension(19,bind([[_77863, _77317, _77423], [k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])]]))).
% 1.00/1.40 cnf('1.1.8.8.1',plain,[-(m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])))],reduction('1.1')).
% 1.00/1.40 cnf('1.1.8.8.2',plain,[v3_struct_0(k11_group_4(21 ^ []))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.8.3',plain,[-(v10_lattices(k11_group_4(21 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.8.4',plain,[-(l3_lattices(k11_group_4(21 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.8.5',plain,[v3_struct_0(k11_group_4(22 ^ []))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.8.6',plain,[-(v10_lattices(k11_group_4(22 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.8.7',plain,[-(l3_lattices(k11_group_4(22 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.9',plain,[-(v1_funct_1(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []))), m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])), -(v3_struct_0(k11_group_4(21 ^ []))), v10_lattices(k11_group_4(21 ^ [])), l3_lattices(k11_group_4(21 ^ [])), -(v3_struct_0(k11_group_4(22 ^ []))), v10_lattices(k11_group_4(22 ^ [])), l3_lattices(k11_group_4(22 ^ []))],extension(18,bind([[_77863, _77317, _77423], [k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])]]))).
% 1.00/1.40 cnf('1.1.8.9.1',plain,[-(m3_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ [])))],reduction('1.1')).
% 1.00/1.40 cnf('1.1.8.9.2',plain,[v3_struct_0(k11_group_4(21 ^ []))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.9.3',plain,[-(v10_lattices(k11_group_4(21 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.9.4',plain,[-(l3_lattices(k11_group_4(21 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.9.5',plain,[v3_struct_0(k11_group_4(22 ^ []))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.9.6',plain,[-(v10_lattices(k11_group_4(22 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.9.7',plain,[-(l3_lattices(k11_group_4(22 ^ [])))],lemmata('1.1.8')).
% 1.00/1.40 cnf('1.1.8.10',plain,[m1_lattice4(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ []))],extension(14)).
% 1.00/1.40 cnf('1.1.8.11',plain,[-(m4_vectsp_8(k3_latsubgr(21 ^ [], 22 ^ [], 23 ^ []), k11_group_4(21 ^ []), k11_group_4(22 ^ []))), l1_group_1(21 ^ []), v4_group_1(21 ^ []), v3_group_1(21 ^ []), -(v3_struct_0(21 ^ [])), l1_group_1(22 ^ []), v4_group_1(22 ^ []), v3_group_1(22 ^ []), -(v3_struct_0(22 ^ [])), v1_funct_1(23 ^ []), v1_funct_2(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])), v1_group_6(23 ^ [], 21 ^ [], 22 ^ []), m2_relset_1(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ []))],extension(23,bind([[_97490, _96825, _97169], [23 ^ [], 21 ^ [], 22 ^ []]]))).
% 1.00/1.40 cnf('1.1.8.11.1',plain,[-(l1_group_1(21 ^ []))],extension(4)).
% 1.00/1.40 cnf('1.1.8.11.2',plain,[-(v4_group_1(21 ^ []))],extension(3)).
% 1.00/1.40 cnf('1.1.8.11.3',plain,[-(v3_group_1(21 ^ []))],extension(2)).
% 1.00/1.40 cnf('1.1.8.11.4',plain,[v3_struct_0(21 ^ [])],extension(1)).
% 1.00/1.40 cnf('1.1.8.11.5',plain,[-(l1_group_1(22 ^ []))],extension(8)).
% 1.00/1.40 cnf('1.1.8.11.6',plain,[-(v4_group_1(22 ^ []))],extension(7)).
% 1.00/1.40 cnf('1.1.8.11.7',plain,[-(v3_group_1(22 ^ []))],extension(6)).
% 1.00/1.40 cnf('1.1.8.11.8',plain,[v3_struct_0(22 ^ [])],extension(5)).
% 1.00/1.40 cnf('1.1.8.11.9',plain,[-(v1_funct_1(23 ^ []))],extension(9)).
% 1.00/1.40 cnf('1.1.8.11.10',plain,[-(v1_funct_2(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])))],extension(10)).
% 1.00/1.40 cnf('1.1.8.11.11',plain,[-(v1_group_6(23 ^ [], 21 ^ [], 22 ^ []))],extension(11)).
% 1.00/1.40 cnf('1.1.8.11.12',plain,[-(m2_relset_1(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])))],extension(12)).
% 1.00/1.40 cnf('1.1.9',plain,[-(v2_funct_1(23 ^ []))],extension(13)).
% 1.00/1.40 cnf('1.1.10',plain,[-(v1_funct_1(23 ^ []))],extension(9)).
% 1.00/1.40 cnf('1.1.11',plain,[-(v1_funct_2(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])))],extension(10)).
% 1.00/1.40 cnf('1.1.12',plain,[-(v1_group_6(23 ^ [], 21 ^ [], 22 ^ []))],extension(11)).
% 1.00/1.40 cnf('1.1.13',plain,[-(m2_relset_1(23 ^ [], u1_struct_0(21 ^ []), u1_struct_0(22 ^ [])))],extension(12)).
% 1.00/1.40 %-----------------------------------------------------
% 1.00/1.40
% 1.00/1.41 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------