%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : GRP648+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n012.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 08:39:54 EDT 2022
% Result : Theorem 15.30s 3.54s
% Output : CNFRefutation 15.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 47
% Syntax : Number of clauses : 158 ( 57 unt; 61 nHn; 158 RR)
% Number of literals : 569 ( 59 equ; 356 neg)
% Maximal clause size : 15 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 5 con; 0-6 aty)
% Number of variables : 193 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_45,plain,
( v3_struct_0(X1)
| l3_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_45) ).
cnf(i_0_9,negated_conjecture,
l1_group_1(esk1_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_9) ).
cnf(i_0_10,negated_conjecture,
v4_group_1(esk1_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_10) ).
cnf(i_0_11,negated_conjecture,
v3_group_1(esk1_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_11) ).
cnf(i_0_12,negated_conjecture,
~ v3_struct_0(esk1_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_12) ).
cnf(i_0_69,plain,
( l1_lattices(X1)
| ~ l3_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_69) ).
cnf(i_0_80,plain,
( m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_80) ).
cnf(i_0_68,plain,
( l2_lattices(X1)
| ~ l3_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_68) ).
cnf(i_0_160,plain,
( v3_struct_0(X1)
| r1_tarski(u1_struct_0(X2),u1_struct_0(X3))
| X4 != X3
| X5 != X2
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1)
| ~ r3_lattices(k11_group_4(X1),X5,X4)
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X1)))
| ~ m1_subset_1(X5,u1_struct_0(k11_group_4(X1))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_160) ).
cnf(i_0_8,negated_conjecture,
m1_group_2(esk2_0,esk1_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_8) ).
cnf(i_0_4,negated_conjecture,
esk4_0 = esk2_0,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_4) ).
cnf(i_0_1,negated_conjecture,
( m1_group_6(esk2_0,esk1_0,esk3_0)
| r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_1) ).
cnf(i_0_3,negated_conjecture,
esk3_0 = esk5_0,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_3) ).
cnf(i_0_7,negated_conjecture,
m1_group_2(esk3_0,esk1_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_7) ).
cnf(i_0_81,plain,
( v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_81) ).
cnf(i_0_82,plain,
( v1_funct_1(u1_lattices(X1))
| ~ l1_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_82) ).
cnf(i_0_142,plain,
( m1_relset_1(X1,X2,X3)
| ~ m2_relset_1(X1,X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_142) ).
cnf(i_0_47,plain,
( v3_struct_0(X1)
| v3_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_47) ).
cnf(i_0_84,plain,
( m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_84) ).
cnf(i_0_6,negated_conjecture,
m1_subset_1(esk4_0,u1_struct_0(k11_group_4(esk1_0))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_6) ).
cnf(i_0_140,plain,
( v3_struct_0(X1)
| m1_group_2(X2,X3)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_6(X2,X1,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_140) ).
cnf(i_0_118,plain,
( X1 = X2
| g3_lattices(X1,X3,X4) != g3_lattices(X2,X5,X6)
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_118) ).
cnf(i_0_85,plain,
( v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_85) ).
cnf(i_0_14,plain,
( g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) = X1
| ~ l3_lattices(X1)
| ~ v3_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_14) ).
cnf(i_0_86,plain,
( v1_funct_1(u2_lattices(X1))
| ~ l2_lattices(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_86) ).
cnf(i_0_5,negated_conjecture,
m1_subset_1(esk5_0,u1_struct_0(k11_group_4(esk1_0))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_5) ).
cnf(i_0_36,plain,
( g3_lattices(k1_group_3(X1),k9_group_4(X1),k10_group_4(X1)) = k11_group_4(X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_36) ).
cnf(i_0_165,plain,
( v3_struct_0(X1)
| m1_group_2(X2,X3)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1)
| ~ r1_tarski(u1_struct_0(X2),u1_struct_0(X3)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_165) ).
cnf(i_0_157,plain,
( v3_struct_0(X1)
| v1_group_1(X2)
| X2 != X3
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X1))) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_157) ).
cnf(i_0_35,plain,
( k2_binop_1(k1_group_3(X1),k1_group_3(X1),k1_group_3(X1),X2,X3,X4) = k9_group_2(X1,X5,X6)
| v3_struct_0(X1)
| X4 != X6
| X3 != X5
| X2 != k10_group_4(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| ~ m1_group_2(X6,X1)
| ~ m1_group_2(X5,X1)
| ~ m1_subset_1(X4,k1_group_3(X1))
| ~ m1_subset_1(X3,k1_group_3(X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ m2_relset_1(X2,k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_35) ).
cnf(i_0_42,plain,
( v3_struct_0(X1)
| m2_relset_1(k10_group_4(X1),k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_42) ).
cnf(i_0_43,plain,
( v3_struct_0(X1)
| v1_funct_2(k10_group_4(X1),k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_43) ).
cnf(i_0_44,plain,
( v3_struct_0(X1)
| v1_funct_1(k10_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_44) ).
cnf(i_0_152,plain,
( v3_struct_0(X1)
| r1_group_2(X1,k9_group_2(X1,X2,X3),X2)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_152) ).
cnf(i_0_60,plain,
( v3_struct_0(X1)
| v1_group_1(k9_group_2(X1,X2,X3))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_60) ).
cnf(i_0_59,plain,
( v3_struct_0(X1)
| m1_group_2(k9_group_2(X1,X2,X3),X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_59) ).
cnf(i_0_116,plain,
( X1 = X2
| g3_lattices(X3,X4,X1) != g3_lattices(X5,X6,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X4,k2_zfmisc_1(X3,X3),X3)
| ~ m1_relset_1(X1,k2_zfmisc_1(X3,X3),X3)
| ~ v1_funct_2(X4,k2_zfmisc_1(X3,X3),X3)
| ~ v1_funct_2(X1,k2_zfmisc_1(X3,X3),X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_116) ).
cnf(i_0_102,plain,
( v3_struct_0(X1)
| v9_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_102) ).
cnf(i_0_103,plain,
( v3_struct_0(X1)
| v8_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_103) ).
cnf(i_0_37,plain,
( k2_binop_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1),u1_lattices(X1),X2,X3) = k2_lattices(X1,X2,X3)
| v3_struct_0(X1)
| ~ l1_lattices(X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_37) ).
cnf(i_0_144,plain,
( X1 = X2
| v3_struct_0(X3)
| ~ v3_group_1(X3)
| ~ v4_group_1(X3)
| ~ l1_group_1(X3)
| ~ v1_group_1(X2)
| ~ v1_group_1(X1)
| ~ m1_group_2(X2,X3)
| ~ m1_group_2(X1,X3)
| ~ r1_group_2(X3,X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_144) ).
cnf(i_0_105,plain,
( v3_struct_0(X1)
| v6_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_105) ).
cnf(i_0_154,plain,
( v3_struct_0(X1)
| r1_lattices(X1,X2,X3)
| k2_lattices(X1,X2,X3) != X2
| ~ l3_lattices(X1)
| ~ v8_lattices(X1)
| ~ v9_lattices(X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_154) ).
cnf(i_0_139,plain,
( v3_struct_0(X1)
| m1_group_6(X2,X1,X3)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_139) ).
cnf(i_0_145,plain,
( v3_struct_0(X1)
| r3_lattices(X1,X2,X3)
| ~ l3_lattices(X1)
| ~ v6_lattices(X1)
| ~ v8_lattices(X1)
| ~ v9_lattices(X1)
| ~ r1_lattices(X1,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_145) ).
cnf(i_0_2,negated_conjecture,
( ~ m1_group_6(esk2_0,esk1_0,esk3_0)
| ~ r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_2) ).
cnf(i_0_48,plain,
( v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v3_struct_0(k11_group_4(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-lx1mcsp0/input.p',i_0_48) ).
cnf(c_0_213,plain,
( v3_struct_0(X1)
| l3_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_45 ).
cnf(c_0_214,negated_conjecture,
l1_group_1(esk1_0),
i_0_9 ).
cnf(c_0_215,negated_conjecture,
v4_group_1(esk1_0),
i_0_10 ).
cnf(c_0_216,negated_conjecture,
v3_group_1(esk1_0),
i_0_11 ).
cnf(c_0_217,negated_conjecture,
~ v3_struct_0(esk1_0),
i_0_12 ).
cnf(c_0_218,plain,
( l1_lattices(X1)
| ~ l3_lattices(X1) ),
i_0_69 ).
cnf(c_0_219,negated_conjecture,
l3_lattices(k11_group_4(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_213,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_220,plain,
( m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
i_0_80 ).
cnf(c_0_221,plain,
l1_lattices(k11_group_4(esk1_0)),
inference(spm,[status(thm)],[c_0_218,c_0_219]) ).
cnf(c_0_222,plain,
( l2_lattices(X1)
| ~ l3_lattices(X1) ),
i_0_68 ).
cnf(c_0_223,plain,
( v3_struct_0(X1)
| r1_tarski(u1_struct_0(X2),u1_struct_0(X3))
| X4 != X3
| X5 != X2
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1)
| ~ r3_lattices(k11_group_4(X1),X5,X4)
| ~ m1_subset_1(X4,u1_struct_0(k11_group_4(X1)))
| ~ m1_subset_1(X5,u1_struct_0(k11_group_4(X1))) ),
i_0_160 ).
cnf(c_0_224,negated_conjecture,
m1_group_2(esk2_0,esk1_0),
i_0_8 ).
cnf(c_0_225,negated_conjecture,
esk4_0 = esk2_0,
i_0_4 ).
cnf(c_0_226,negated_conjecture,
( m1_group_6(esk2_0,esk1_0,esk3_0)
| r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0) ),
i_0_1 ).
cnf(c_0_227,negated_conjecture,
esk3_0 = esk5_0,
i_0_3 ).
cnf(c_0_228,negated_conjecture,
m1_group_2(esk3_0,esk1_0),
i_0_7 ).
cnf(c_0_229,plain,
( v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
i_0_81 ).
cnf(c_0_230,plain,
( v1_funct_1(u1_lattices(X1))
| ~ l1_lattices(X1) ),
i_0_82 ).
cnf(c_0_231,plain,
( m1_relset_1(X1,X2,X3)
| ~ m2_relset_1(X1,X2,X3) ),
i_0_142 ).
cnf(c_0_232,plain,
m2_relset_1(u1_lattices(k11_group_4(esk1_0)),k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_220,c_0_221]) ).
cnf(c_0_233,plain,
( v3_struct_0(X1)
| v3_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_47 ).
cnf(c_0_234,plain,
( m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
i_0_84 ).
cnf(c_0_235,plain,
l2_lattices(k11_group_4(esk1_0)),
inference(spm,[status(thm)],[c_0_222,c_0_219]) ).
cnf(c_0_236,plain,
( v3_struct_0(X1)
| r1_tarski(u1_struct_0(X2),u1_struct_0(X3))
| ~ r3_lattices(k11_group_4(X1),X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(k11_group_4(X1)))
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X1)))
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_223])]) ).
cnf(c_0_237,negated_conjecture,
m1_subset_1(esk4_0,u1_struct_0(k11_group_4(esk1_0))),
i_0_6 ).
cnf(c_0_238,negated_conjecture,
m1_group_2(esk4_0,esk1_0),
inference(rw,[status(thm)],[c_0_224,c_0_225]) ).
cnf(c_0_239,plain,
( v3_struct_0(X1)
| m1_group_2(X2,X3)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_6(X2,X1,X3) ),
i_0_140 ).
cnf(c_0_240,negated_conjecture,
( r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0)
| m1_group_6(esk4_0,esk1_0,esk5_0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_226,c_0_225]),c_0_227]) ).
cnf(c_0_241,negated_conjecture,
m1_group_2(esk5_0,esk1_0),
inference(rw,[status(thm)],[c_0_228,c_0_227]) ).
cnf(c_0_242,plain,
( X1 = X2
| g3_lattices(X1,X3,X4) != g3_lattices(X2,X5,X6)
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X3)
| ~ m1_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1) ),
i_0_118 ).
cnf(c_0_243,plain,
v1_funct_2(u1_lattices(k11_group_4(esk1_0)),k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_229,c_0_221]) ).
cnf(c_0_244,plain,
v1_funct_1(u1_lattices(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_230,c_0_221]) ).
cnf(c_0_245,plain,
m1_relset_1(u1_lattices(k11_group_4(esk1_0)),k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_231,c_0_232]) ).
cnf(c_0_246,plain,
( v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
i_0_85 ).
cnf(c_0_247,plain,
( g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) = X1
| ~ l3_lattices(X1)
| ~ v3_lattices(X1) ),
i_0_14 ).
cnf(c_0_248,negated_conjecture,
v3_lattices(k11_group_4(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_233,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_249,plain,
m2_relset_1(u2_lattices(k11_group_4(esk1_0)),k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_234,c_0_235]) ).
cnf(c_0_250,plain,
( v1_funct_1(u2_lattices(X1))
| ~ l2_lattices(X1) ),
i_0_86 ).
cnf(c_0_251,negated_conjecture,
( r1_tarski(u1_struct_0(esk4_0),u1_struct_0(X1))
| ~ r3_lattices(k11_group_4(esk1_0),esk4_0,X1)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(esk1_0)))
| ~ m1_group_2(X1,esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_236,c_0_237]),c_0_238]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_252,negated_conjecture,
( r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0)
| m1_group_2(esk4_0,esk5_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_239,c_0_240]),c_0_241]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_253,negated_conjecture,
m1_subset_1(esk5_0,u1_struct_0(k11_group_4(esk1_0))),
i_0_5 ).
cnf(c_0_254,plain,
( u1_struct_0(k11_group_4(esk1_0)) = X1
| g3_lattices(u1_struct_0(k11_group_4(esk1_0)),X2,u1_lattices(k11_group_4(esk1_0))) != g3_lattices(X1,X3,X4)
| ~ v1_funct_2(X2,k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0)))
| ~ m1_relset_1(X2,k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0)))
| ~ v1_funct_1(X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_242,c_0_243]),c_0_244])]),c_0_245])]) ).
cnf(c_0_255,plain,
v1_funct_2(u2_lattices(k11_group_4(esk1_0)),k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_246,c_0_235]) ).
cnf(c_0_256,negated_conjecture,
g3_lattices(u1_struct_0(k11_group_4(esk1_0)),u2_lattices(k11_group_4(esk1_0)),u1_lattices(k11_group_4(esk1_0))) = k11_group_4(esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_247,c_0_248]),c_0_219])]) ).
cnf(c_0_257,plain,
m1_relset_1(u2_lattices(k11_group_4(esk1_0)),k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_231,c_0_249]) ).
cnf(c_0_258,plain,
v1_funct_1(u2_lattices(k11_group_4(esk1_0))),
inference(spm,[status(thm)],[c_0_250,c_0_235]) ).
cnf(c_0_259,plain,
( g3_lattices(k1_group_3(X1),k9_group_4(X1),k10_group_4(X1)) = k11_group_4(X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_36 ).
cnf(c_0_260,plain,
( v3_struct_0(X1)
| m1_group_2(X2,X3)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1)
| ~ r1_tarski(u1_struct_0(X2),u1_struct_0(X3)) ),
i_0_165 ).
cnf(c_0_261,negated_conjecture,
( r1_tarski(u1_struct_0(esk4_0),u1_struct_0(esk5_0))
| m1_group_2(esk4_0,esk5_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_251,c_0_252]),c_0_253]),c_0_241])]) ).
cnf(c_0_262,plain,
( v3_struct_0(X1)
| v1_group_1(X2)
| X2 != X3
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ m1_subset_1(X3,u1_struct_0(k11_group_4(X1))) ),
i_0_157 ).
cnf(c_0_263,plain,
( k2_binop_1(k1_group_3(X1),k1_group_3(X1),k1_group_3(X1),X2,X3,X4) = k9_group_2(X1,X5,X6)
| v3_struct_0(X1)
| X4 != X6
| X3 != X5
| X2 != k10_group_4(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_funct_1(X2)
| ~ m1_group_2(X6,X1)
| ~ m1_group_2(X5,X1)
| ~ m1_subset_1(X4,k1_group_3(X1))
| ~ m1_subset_1(X3,k1_group_3(X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ m2_relset_1(X2,k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1)) ),
i_0_35 ).
cnf(c_0_264,plain,
( v3_struct_0(X1)
| m2_relset_1(k10_group_4(X1),k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_42 ).
cnf(c_0_265,plain,
( v3_struct_0(X1)
| v1_funct_2(k10_group_4(X1),k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_43 ).
cnf(c_0_266,plain,
( v3_struct_0(X1)
| v1_funct_1(k10_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_44 ).
cnf(c_0_267,plain,
( u1_struct_0(k11_group_4(esk1_0)) = X1
| g3_lattices(X1,X2,X3) != k11_group_4(esk1_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_254,c_0_255]),c_0_256]),c_0_257]),c_0_258])]) ).
cnf(c_0_268,negated_conjecture,
g3_lattices(k1_group_3(esk1_0),k9_group_4(esk1_0),k10_group_4(esk1_0)) = k11_group_4(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_259,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_269,plain,
( v3_struct_0(X1)
| r1_group_2(X1,k9_group_2(X1,X2,X3),X2)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X2)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1)
| ~ m1_group_2(X2,X3) ),
i_0_152 ).
cnf(c_0_270,negated_conjecture,
( v3_struct_0(X1)
| m1_group_2(esk4_0,esk5_0)
| ~ m1_group_2(esk5_0,X1)
| ~ m1_group_2(esk4_0,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
inference(spm,[status(thm)],[c_0_260,c_0_261]) ).
cnf(c_0_271,plain,
( v1_group_1(X1)
| v3_struct_0(X2)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(X2)))
| ~ m1_group_2(X1,X2)
| ~ l1_group_1(X2)
| ~ v4_group_1(X2)
| ~ v3_group_1(X2) ),
inference(er,[status(thm)],[c_0_262]) ).
cnf(c_0_272,plain,
( v3_struct_0(X1)
| v1_group_1(k9_group_2(X1,X2,X3))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1) ),
i_0_60 ).
cnf(c_0_273,plain,
( v3_struct_0(X1)
| m1_group_2(k9_group_2(X1,X2,X3),X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X1) ),
i_0_59 ).
cnf(c_0_274,plain,
( X1 = X2
| g3_lattices(X3,X4,X1) != g3_lattices(X5,X6,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_1(X1)
| ~ m1_relset_1(X4,k2_zfmisc_1(X3,X3),X3)
| ~ m1_relset_1(X1,k2_zfmisc_1(X3,X3),X3)
| ~ v1_funct_2(X4,k2_zfmisc_1(X3,X3),X3)
| ~ v1_funct_2(X1,k2_zfmisc_1(X3,X3),X3) ),
i_0_116 ).
cnf(c_0_275,plain,
( k2_binop_1(k1_group_3(X1),k1_group_3(X1),k1_group_3(X1),X2,X3,X4) = k9_group_2(X1,X3,X4)
| v3_struct_0(X1)
| X2 != k10_group_4(X1)
| ~ m2_relset_1(X2,k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ v1_funct_2(X2,k2_zfmisc_1(k1_group_3(X1),k1_group_3(X1)),k1_group_3(X1))
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X4,k1_group_3(X1))
| ~ m1_subset_1(X3,k1_group_3(X1))
| ~ m1_group_2(X4,X1)
| ~ m1_group_2(X3,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_263])]) ).
cnf(c_0_276,negated_conjecture,
m2_relset_1(k10_group_4(esk1_0),k2_zfmisc_1(k1_group_3(esk1_0),k1_group_3(esk1_0)),k1_group_3(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_264,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_277,negated_conjecture,
v1_funct_2(k10_group_4(esk1_0),k2_zfmisc_1(k1_group_3(esk1_0),k1_group_3(esk1_0)),k1_group_3(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_265,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_278,negated_conjecture,
v1_funct_1(k10_group_4(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_266,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_279,negated_conjecture,
u1_struct_0(k11_group_4(esk1_0)) = k1_group_3(esk1_0),
inference(spm,[status(thm)],[c_0_267,c_0_268]) ).
cnf(c_0_280,negated_conjecture,
( r1_group_2(esk1_0,k9_group_2(esk1_0,X1,esk5_0),X1)
| ~ v1_group_1(X1)
| ~ m1_group_2(X1,esk5_0)
| ~ m1_group_2(X1,esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_269,c_0_241]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_281,negated_conjecture,
m1_group_2(esk4_0,esk5_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_270,c_0_241]),c_0_238]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_282,negated_conjecture,
v1_group_1(esk4_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_271,c_0_237]),c_0_238]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_283,negated_conjecture,
( v1_group_1(k9_group_2(esk1_0,X1,esk5_0))
| ~ m1_group_2(X1,esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_272,c_0_241]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_284,negated_conjecture,
( m1_group_2(k9_group_2(esk1_0,X1,esk5_0),esk1_0)
| ~ m1_group_2(X1,esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_241]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_285,plain,
( v3_struct_0(X1)
| v9_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_102 ).
cnf(c_0_286,plain,
( v3_struct_0(X1)
| v8_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_103 ).
cnf(c_0_287,plain,
( k2_binop_1(u1_struct_0(X1),u1_struct_0(X1),u1_struct_0(X1),u1_lattices(X1),X2,X3) = k2_lattices(X1,X2,X3)
| v3_struct_0(X1)
| ~ l1_lattices(X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
i_0_37 ).
cnf(c_0_288,plain,
( X1 = X2
| g3_lattices(u1_struct_0(k11_group_4(esk1_0)),u2_lattices(k11_group_4(esk1_0)),X1) != g3_lattices(X3,X4,X2)
| ~ v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0)))
| ~ m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0))),u1_struct_0(k11_group_4(esk1_0)))
| ~ v1_funct_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_274,c_0_255]),c_0_258])]),c_0_257])]) ).
cnf(c_0_289,negated_conjecture,
( k2_binop_1(k1_group_3(esk1_0),k1_group_3(esk1_0),k1_group_3(esk1_0),k10_group_4(esk1_0),X1,X2) = k9_group_2(esk1_0,X1,X2)
| ~ m1_subset_1(X2,k1_group_3(esk1_0))
| ~ m1_subset_1(X1,k1_group_3(esk1_0))
| ~ m1_group_2(X2,esk1_0)
| ~ m1_group_2(X1,esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_275,c_0_276]),c_0_277]),c_0_278]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_290,negated_conjecture,
m1_subset_1(esk5_0,k1_group_3(esk1_0)),
inference(rw,[status(thm)],[c_0_253,c_0_279]) ).
cnf(c_0_291,plain,
( X1 = X2
| v3_struct_0(X3)
| ~ v3_group_1(X3)
| ~ v4_group_1(X3)
| ~ l1_group_1(X3)
| ~ v1_group_1(X2)
| ~ v1_group_1(X1)
| ~ m1_group_2(X2,X3)
| ~ m1_group_2(X1,X3)
| ~ r1_group_2(X3,X1,X2) ),
i_0_144 ).
cnf(c_0_292,negated_conjecture,
r1_group_2(esk1_0,k9_group_2(esk1_0,esk4_0,esk5_0),esk4_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_280,c_0_281]),c_0_282]),c_0_238])]) ).
cnf(c_0_293,negated_conjecture,
v1_group_1(k9_group_2(esk1_0,esk4_0,esk5_0)),
inference(spm,[status(thm)],[c_0_283,c_0_238]) ).
cnf(c_0_294,negated_conjecture,
m1_group_2(k9_group_2(esk1_0,esk4_0,esk5_0),esk1_0),
inference(spm,[status(thm)],[c_0_284,c_0_238]) ).
cnf(c_0_295,plain,
( v3_struct_0(X1)
| v6_lattices(k11_group_4(X1))
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1) ),
i_0_105 ).
cnf(c_0_296,plain,
( v3_struct_0(X1)
| r1_lattices(X1,X2,X3)
| k2_lattices(X1,X2,X3) != X2
| ~ l3_lattices(X1)
| ~ v8_lattices(X1)
| ~ v9_lattices(X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
i_0_154 ).
cnf(c_0_297,negated_conjecture,
v9_lattices(k11_group_4(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_285,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_298,negated_conjecture,
v8_lattices(k11_group_4(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_286,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_299,negated_conjecture,
( k2_binop_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0)),u1_lattices(k11_group_4(esk1_0)),X1,esk5_0) = k2_lattices(k11_group_4(esk1_0),X1,esk5_0)
| v3_struct_0(k11_group_4(esk1_0))
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(esk1_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_287,c_0_253]),c_0_221])]) ).
cnf(c_0_300,plain,
( u1_lattices(k11_group_4(esk1_0)) = X1
| g3_lattices(X2,X3,X1) != k11_group_4(esk1_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_288,c_0_243]),c_0_256]),c_0_245]),c_0_244])]) ).
cnf(c_0_301,negated_conjecture,
( k2_binop_1(k1_group_3(esk1_0),k1_group_3(esk1_0),k1_group_3(esk1_0),k10_group_4(esk1_0),X1,esk5_0) = k9_group_2(esk1_0,X1,esk5_0)
| ~ m1_subset_1(X1,k1_group_3(esk1_0))
| ~ m1_group_2(X1,esk1_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_289,c_0_290]),c_0_241])]) ).
cnf(c_0_302,negated_conjecture,
m1_subset_1(esk4_0,k1_group_3(esk1_0)),
inference(rw,[status(thm)],[c_0_237,c_0_279]) ).
cnf(c_0_303,plain,
k9_group_2(esk1_0,esk4_0,esk5_0) = esk4_0,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_292]),c_0_282]),c_0_293]),c_0_238]),c_0_294]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_304,plain,
( v3_struct_0(X1)
| m1_group_6(X2,X1,X3)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ m1_group_2(X3,X1)
| ~ m1_group_2(X2,X3) ),
i_0_139 ).
cnf(c_0_305,plain,
( v3_struct_0(X1)
| r3_lattices(X1,X2,X3)
| ~ l3_lattices(X1)
| ~ v6_lattices(X1)
| ~ v8_lattices(X1)
| ~ v9_lattices(X1)
| ~ r1_lattices(X1,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
i_0_145 ).
cnf(c_0_306,negated_conjecture,
v6_lattices(k11_group_4(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_295,c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_307,negated_conjecture,
( r1_lattices(k11_group_4(esk1_0),X1,esk5_0)
| v3_struct_0(k11_group_4(esk1_0))
| k2_lattices(k11_group_4(esk1_0),X1,esk5_0) != X1
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(esk1_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_296,c_0_253]),c_0_297]),c_0_298]),c_0_219])]) ).
cnf(c_0_308,negated_conjecture,
( k2_binop_1(u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0)),u1_struct_0(k11_group_4(esk1_0)),u1_lattices(k11_group_4(esk1_0)),esk4_0,esk5_0) = k2_lattices(k11_group_4(esk1_0),esk4_0,esk5_0)
| v3_struct_0(k11_group_4(esk1_0)) ),
inference(spm,[status(thm)],[c_0_299,c_0_237]) ).
cnf(c_0_309,negated_conjecture,
u1_lattices(k11_group_4(esk1_0)) = k10_group_4(esk1_0),
inference(spm,[status(thm)],[c_0_300,c_0_268]) ).
cnf(c_0_310,negated_conjecture,
k2_binop_1(k1_group_3(esk1_0),k1_group_3(esk1_0),k1_group_3(esk1_0),k10_group_4(esk1_0),esk4_0,esk5_0) = esk4_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_301,c_0_302]),c_0_303]),c_0_238])]) ).
cnf(c_0_311,negated_conjecture,
( ~ m1_group_6(esk2_0,esk1_0,esk3_0)
| ~ r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0) ),
i_0_2 ).
cnf(c_0_312,negated_conjecture,
( m1_group_6(X1,esk1_0,esk5_0)
| ~ m1_group_2(X1,esk5_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_304,c_0_241]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]) ).
cnf(c_0_313,negated_conjecture,
( r3_lattices(k11_group_4(esk1_0),X1,esk5_0)
| v3_struct_0(k11_group_4(esk1_0))
| ~ r1_lattices(k11_group_4(esk1_0),X1,esk5_0)
| ~ m1_subset_1(X1,u1_struct_0(k11_group_4(esk1_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_305,c_0_253]),c_0_297]),c_0_298]),c_0_306]),c_0_219])]) ).
cnf(c_0_314,negated_conjecture,
( r1_lattices(k11_group_4(esk1_0),X1,esk5_0)
| v3_struct_0(k11_group_4(esk1_0))
| k2_lattices(k11_group_4(esk1_0),X1,esk5_0) != X1
| ~ m1_subset_1(X1,k1_group_3(esk1_0)) ),
inference(rw,[status(thm)],[c_0_307,c_0_279]) ).
cnf(c_0_315,negated_conjecture,
( k2_lattices(k11_group_4(esk1_0),esk4_0,esk5_0) = esk4_0
| v3_struct_0(k11_group_4(esk1_0)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_308,c_0_279]),c_0_279]),c_0_279]),c_0_309]),c_0_310]) ).
cnf(c_0_316,negated_conjecture,
( ~ r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0)
| ~ m1_group_6(esk4_0,esk1_0,esk5_0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_311,c_0_225]),c_0_227]) ).
cnf(c_0_317,negated_conjecture,
m1_group_6(esk4_0,esk1_0,esk5_0),
inference(spm,[status(thm)],[c_0_312,c_0_281]) ).
cnf(c_0_318,negated_conjecture,
( r3_lattices(k11_group_4(esk1_0),X1,esk5_0)
| v3_struct_0(k11_group_4(esk1_0))
| ~ r1_lattices(k11_group_4(esk1_0),X1,esk5_0)
| ~ m1_subset_1(X1,k1_group_3(esk1_0)) ),
inference(rw,[status(thm)],[c_0_313,c_0_279]) ).
cnf(c_0_319,negated_conjecture,
( r1_lattices(k11_group_4(esk1_0),esk4_0,esk5_0)
| v3_struct_0(k11_group_4(esk1_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_314,c_0_315]),c_0_302])]) ).
cnf(c_0_320,negated_conjecture,
~ r3_lattices(k11_group_4(esk1_0),esk4_0,esk5_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_316,c_0_317])]) ).
cnf(c_0_321,plain,
( v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ l1_group_1(X1)
| ~ v3_struct_0(k11_group_4(X1)) ),
i_0_48 ).
cnf(c_0_322,negated_conjecture,
v3_struct_0(k11_group_4(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_318,c_0_319]),c_0_302])]),c_0_320]) ).
cnf(c_0_323,plain,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_321,c_0_322]),c_0_214]),c_0_215]),c_0_216])]),c_0_217]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP648+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Tue Jun 14 05:00:57 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.20/0.47 # ENIGMATIC: Selected complete mode:
% 15.30/3.54 # ENIGMATIC: Solved by Enigma+tptp-cade20-model02-h2e15+lgb-t150-d30-l4800-e0.15+coop-paramils157:
% 15.30/3.54 # SinE strategy is GSinE(CountFormulas,hypos,5.0,,3,500,1.0)
% 15.30/3.54 # ENIGMA: LightGBM model '/export/starexec/sandbox2/solver/bin/data/Enigma/tptp-cade20-model02-h2e15/lgb-t150-d30-l4800-e0.15/model.lgb' loaded. (hash_base: 32768; conj_feats: 51; version: 991; iters: 150)
% 15.30/3.54 # Preprocessing time : 0.721 s
% 15.30/3.54
% 15.30/3.54 # Proof found!
% 15.30/3.54 # SZS status Theorem
% 15.30/3.54 # SZS output start CNFRefutation
% See solution above
% 15.30/3.54 # Training examples: 0 positive, 0 negative
% 15.30/3.54
% 15.30/3.54 # -------------------------------------------------
% 15.30/3.54 # User time : 0.879 s
% 15.30/3.54 # System time : 0.118 s
% 15.30/3.54 # Total time : 0.997 s
% 15.30/3.54 # ...preprocessing : 0.721 s
% 15.30/3.54 # ...main loop : 0.275 s
% 15.30/3.54 # Maximum resident set size: 151592 pages
% 15.30/3.54
%------------------------------------------------------------------------------