%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : GRP634+3 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n009.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:42 EDT 2022
% Result : Theorem 36.91s 8.57s
% Output : CNFRefutation 36.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 43
% Syntax : Number of clauses : 131 ( 42 unt; 67 nHn; 131 RR)
% Number of literals : 514 ( 33 equ; 318 neg)
% Maximal clause size : 13 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-2 aty)
% Number of variables : 110 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_6554,plain,
( v3_struct_0(X1)
| v1_group_3(k10_group_5(X1),X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_6554) ).
cnf(i_0_4259,negated_conjecture,
v3_group_1(esk608_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4259) ).
cnf(i_0_4258,negated_conjecture,
v4_group_1(esk608_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4258) ).
cnf(i_0_4257,negated_conjecture,
l1_group_1(esk608_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4257) ).
cnf(i_0_4261,negated_conjecture,
~ v3_struct_0(esk608_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4261) ).
cnf(i_0_6605,plain,
( k10_group_5(X1) = X1
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_6605) ).
cnf(i_0_4253,negated_conjecture,
v7_group_1(esk608_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4253) ).
cnf(i_0_4260,negated_conjecture,
v1_group_1(esk608_0),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4260) ).
cnf(i_0_902,plain,
( k4_autgroup(X1) = u1_struct_0(X2)
| v3_struct_0(X1)
| X2 != k5_autgroup(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v1_group_1(X2)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,k3_autgroup(X1))
| ~ v1_group_3(X2,k3_autgroup(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_902) ).
cnf(i_0_1246,plain,
( v3_struct_0(X1)
| v1_group_1(k5_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1246) ).
cnf(i_0_1244,plain,
( v3_struct_0(X1)
| m1_group_2(k5_autgroup(X1),k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1244) ).
cnf(i_0_1245,plain,
( v3_struct_0(X1)
| v1_group_3(k5_autgroup(X1),k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1245) ).
cnf(i_0_1238,plain,
( v3_struct_0(X1)
| m1_fraenkel(k4_autgroup(X1),u1_struct_0(X1),u1_struct_0(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1238) ).
cnf(i_0_5671,plain,
( v3_struct_0(X1)
| m1_group_2(X1,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_5671) ).
cnf(i_0_572,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_572) ).
cnf(i_0_1320,plain,
( l1_struct_0(X1)
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1320) ).
cnf(i_0_1329,plain,
( ~ v1_xboole_0(X1)
| ~ m1_fraenkel(X1,X2,X3) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1329) ).
cnf(i_0_4132,plain,
( v3_struct_0(X1)
| r2_group_6(k5_autgroup(X1),k6_group_6(X1,k10_group_5(X1)))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4132) ).
cnf(i_0_1704,plain,
( v3_struct_0(X1)
| v3_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1704) ).
cnf(i_0_1703,plain,
( v3_struct_0(X1)
| v4_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1703) ).
cnf(i_0_1706,plain,
( v3_struct_0(X1)
| v1_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1706) ).
cnf(i_0_1272,plain,
( v3_struct_0(X1)
| l1_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1272) ).
cnf(i_0_1224,plain,
( v3_struct_0(X1)
| v3_group_1(k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1224) ).
cnf(i_0_1222,plain,
( v3_struct_0(X1)
| l1_group_1(k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1222) ).
cnf(i_0_1223,plain,
( v3_struct_0(X1)
| v4_group_1(k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1223) ).
cnf(i_0_1101,plain,
( g1_group_1(u1_struct_0(X1),u1_group_1(X1)) = k6_group_2(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1101) ).
cnf(i_0_1071,plain,
( X1 = X2
| ~ v3_realset2(X3)
| ~ l1_struct_0(X3)
| ~ m1_subset_1(X2,u1_struct_0(X3))
| ~ m1_subset_1(X1,u1_struct_0(X3)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1071) ).
cnf(i_0_4251,negated_conjecture,
m1_subset_1(esk609_0,u1_struct_0(k5_autgroup(esk608_0))),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4251) ).
cnf(i_0_2330,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| r2_group_6(X1,X2)
| ~ l1_group_1(X1)
| ~ l1_group_1(X2)
| ~ v1_group_1(X1)
| ~ v1_group_1(X2)
| ~ v4_group_1(X1)
| ~ v4_group_1(X2)
| ~ v3_group_1(X1)
| ~ v3_group_1(X2)
| ~ r2_group_6(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_2330) ).
cnf(i_0_1331,plain,
( v3_struct_0(X1)
| v3_group_1(X2)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1331) ).
cnf(i_0_1330,plain,
( l1_group_1(X1)
| v3_struct_0(X2)
| ~ l1_group_1(X2)
| ~ v3_group_1(X2)
| ~ m1_group_2(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1330) ).
cnf(i_0_81,plain,
( v3_struct_0(X1)
| v4_group_1(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_81) ).
cnf(i_0_6389,plain,
( v3_struct_0(X1)
| v3_realset2(k6_group_6(X1,k6_group_2(X1)))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_6389) ).
cnf(i_0_2,plain,
( g1_group_1(u1_struct_0(X1),u1_group_1(X1)) = X1
| ~ l1_group_1(X1)
| ~ v1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_2) ).
cnf(i_0_1332,plain,
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v3_struct_0(X2)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1332) ).
cnf(i_0_1213,plain,
( v3_struct_0(X1)
| m1_subset_1(k2_group_1(X1),u1_struct_0(X1))
| ~ l1_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1213) ).
cnf(i_0_5227,plain,
( k2_group_1(X1) = k2_group_1(X2)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_5227) ).
cnf(i_0_3435,plain,
( u1_vectsp_1(k19_monoid_0(u1_struct_0(X1))) = k2_group_1(k5_autgroup(X1))
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_3435) ).
cnf(i_0_6451,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| v3_realset2(X1)
| ~ l1_group_1(X1)
| ~ l1_group_1(X2)
| ~ v1_group_1(X1)
| ~ v1_group_1(X2)
| ~ v4_group_1(X1)
| ~ v4_group_1(X2)
| ~ v3_realset2(X2)
| ~ v3_group_1(X1)
| ~ v3_group_1(X2)
| ~ r2_group_6(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_6451) ).
cnf(i_0_2392,plain,
( u1_vectsp_1(k19_monoid_0(u1_struct_0(X1))) = k2_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_2392) ).
cnf(i_0_4250,negated_conjecture,
k2_group_1(k5_autgroup(esk608_0)) != esk609_0,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_4250) ).
cnf(i_0_1226,plain,
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ v3_struct_0(k3_autgroup(X1)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1226) ).
cnf(i_0_1707,plain,
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1)
| ~ v3_struct_0(k6_group_6(X1,X2)) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-q5cu3czw/lgb.p',i_0_1707) ).
cnf(c_0_6649,plain,
( v3_struct_0(X1)
| v1_group_3(k10_group_5(X1),X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_6554 ).
cnf(c_0_6650,negated_conjecture,
v3_group_1(esk608_0),
i_0_4259 ).
cnf(c_0_6651,negated_conjecture,
v4_group_1(esk608_0),
i_0_4258 ).
cnf(c_0_6652,negated_conjecture,
l1_group_1(esk608_0),
i_0_4257 ).
cnf(c_0_6653,negated_conjecture,
~ v3_struct_0(esk608_0),
i_0_4261 ).
cnf(c_0_6654,plain,
( k10_group_5(X1) = X1
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v7_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_6605 ).
cnf(c_0_6655,negated_conjecture,
v7_group_1(esk608_0),
i_0_4253 ).
cnf(c_0_6656,negated_conjecture,
v1_group_1(esk608_0),
i_0_4260 ).
cnf(c_0_6657,plain,
( k4_autgroup(X1) = u1_struct_0(X2)
| v3_struct_0(X1)
| X2 != k5_autgroup(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v1_group_1(X2)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,k3_autgroup(X1))
| ~ v1_group_3(X2,k3_autgroup(X1)) ),
i_0_902 ).
cnf(c_0_6658,plain,
( v3_struct_0(X1)
| v1_group_1(k5_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1246 ).
cnf(c_0_6659,plain,
( v3_struct_0(X1)
| m1_group_2(k5_autgroup(X1),k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1244 ).
cnf(c_0_6660,plain,
( v3_struct_0(X1)
| v1_group_3(k5_autgroup(X1),k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1245 ).
cnf(c_0_6661,plain,
( v3_struct_0(X1)
| m1_fraenkel(k4_autgroup(X1),u1_struct_0(X1),u1_struct_0(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1238 ).
cnf(c_0_6662,negated_conjecture,
v1_group_3(k10_group_5(esk608_0),esk608_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6649,c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6663,negated_conjecture,
k10_group_5(esk608_0) = esk608_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_6654,c_0_6655]),c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6664,plain,
( v3_struct_0(X1)
| m1_group_2(X1,X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_5671 ).
cnf(c_0_6665,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
i_0_572 ).
cnf(c_0_6666,plain,
( l1_struct_0(X1)
| ~ l1_group_1(X1) ),
i_0_1320 ).
cnf(c_0_6667,plain,
( u1_struct_0(k5_autgroup(X1)) = k4_autgroup(X1)
| v3_struct_0(X1)
| ~ v3_group_1(X1)
| ~ v4_group_1(X1)
| ~ v1_group_1(X1)
| ~ l1_group_1(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(er,[status(thm)],[c_0_6657]),c_0_6658]),c_0_6659]),c_0_6660]) ).
cnf(c_0_6668,plain,
( ~ v1_xboole_0(X1)
| ~ m1_fraenkel(X1,X2,X3) ),
i_0_1329 ).
cnf(c_0_6669,negated_conjecture,
m1_fraenkel(k4_autgroup(esk608_0),u1_struct_0(esk608_0),u1_struct_0(esk608_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_6661,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6670,plain,
( v3_struct_0(X1)
| r2_group_6(k5_autgroup(X1),k6_group_6(X1,k10_group_5(X1)))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_4132 ).
cnf(c_0_6671,plain,
( v3_struct_0(X1)
| v3_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
i_0_1704 ).
cnf(c_0_6672,negated_conjecture,
v1_group_3(esk608_0,esk608_0),
inference(rw,[status(thm)],[c_0_6662,c_0_6663]) ).
cnf(c_0_6673,negated_conjecture,
m1_group_2(esk608_0,esk608_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6664,c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6674,plain,
( v3_struct_0(X1)
| v4_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
i_0_1703 ).
cnf(c_0_6675,plain,
( v3_struct_0(X1)
| v1_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
i_0_1706 ).
cnf(c_0_6676,plain,
( v3_struct_0(X1)
| l1_group_1(k6_group_6(X1,X2))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1) ),
i_0_1272 ).
cnf(c_0_6677,plain,
( v1_xboole_0(u1_struct_0(X1))
| ~ l1_group_1(X1)
| ~ v3_struct_0(X1) ),
inference(spm,[status(thm)],[c_0_6665,c_0_6666]) ).
cnf(c_0_6678,negated_conjecture,
u1_struct_0(k5_autgroup(esk608_0)) = k4_autgroup(esk608_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_6667,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6679,plain,
~ v1_xboole_0(k4_autgroup(esk608_0)),
inference(spm,[status(thm)],[c_0_6668,c_0_6669]) ).
cnf(c_0_6680,plain,
( v3_struct_0(X1)
| v3_group_1(k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1224 ).
cnf(c_0_6681,plain,
( v3_struct_0(X1)
| l1_group_1(k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1222 ).
cnf(c_0_6682,plain,
( v3_struct_0(X1)
| v4_group_1(k3_autgroup(X1))
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1223 ).
cnf(c_0_6683,plain,
( g1_group_1(u1_struct_0(X1),u1_group_1(X1)) = k6_group_2(X1)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_1101 ).
cnf(c_0_6684,plain,
( X1 = X2
| ~ v3_realset2(X3)
| ~ l1_struct_0(X3)
| ~ m1_subset_1(X2,u1_struct_0(X3))
| ~ m1_subset_1(X1,u1_struct_0(X3)) ),
i_0_1071 ).
cnf(c_0_6685,negated_conjecture,
m1_subset_1(esk609_0,u1_struct_0(k5_autgroup(esk608_0))),
i_0_4251 ).
cnf(c_0_6686,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| r2_group_6(X1,X2)
| ~ l1_group_1(X1)
| ~ l1_group_1(X2)
| ~ v1_group_1(X1)
| ~ v1_group_1(X2)
| ~ v4_group_1(X1)
| ~ v4_group_1(X2)
| ~ v3_group_1(X1)
| ~ v3_group_1(X2)
| ~ r2_group_6(X2,X1) ),
i_0_2330 ).
cnf(c_0_6687,negated_conjecture,
r2_group_6(k5_autgroup(esk608_0),k6_group_6(esk608_0,esk608_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_6670,c_0_6650]),c_0_6663]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6688,negated_conjecture,
v3_group_1(k6_group_6(esk608_0,esk608_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_6671,c_0_6672]),c_0_6673]),c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6689,negated_conjecture,
v4_group_1(k6_group_6(esk608_0,esk608_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_6674,c_0_6672]),c_0_6673]),c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6690,negated_conjecture,
v1_group_1(k5_autgroup(esk608_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_6658,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6691,negated_conjecture,
v1_group_1(k6_group_6(esk608_0,esk608_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_6675,c_0_6672]),c_0_6673]),c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6692,negated_conjecture,
l1_group_1(k6_group_6(esk608_0,esk608_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_6676,c_0_6672]),c_0_6673]),c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6693,plain,
( ~ l1_group_1(k5_autgroup(esk608_0))
| ~ v3_struct_0(k5_autgroup(esk608_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_6677,c_0_6678]),c_0_6679]) ).
cnf(c_0_6694,plain,
( v3_struct_0(X1)
| v3_group_1(X2)
| ~ l1_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
i_0_1331 ).
cnf(c_0_6695,negated_conjecture,
m1_group_2(k5_autgroup(esk608_0),k3_autgroup(esk608_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_6659,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6696,negated_conjecture,
v3_group_1(k3_autgroup(esk608_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_6680,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6697,negated_conjecture,
l1_group_1(k3_autgroup(esk608_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_6681,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6698,plain,
( l1_group_1(X1)
| v3_struct_0(X2)
| ~ l1_group_1(X2)
| ~ v3_group_1(X2)
| ~ m1_group_2(X1,X2) ),
i_0_1330 ).
cnf(c_0_6699,plain,
( v3_struct_0(X1)
| v4_group_1(X2)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
i_0_81 ).
cnf(c_0_6700,negated_conjecture,
v4_group_1(k3_autgroup(esk608_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_6682,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6701,plain,
( v3_struct_0(X1)
| v3_realset2(k6_group_6(X1,k6_group_2(X1)))
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_6389 ).
cnf(c_0_6702,plain,
( g1_group_1(u1_struct_0(X1),u1_group_1(X1)) = X1
| ~ l1_group_1(X1)
| ~ v1_group_1(X1) ),
i_0_2 ).
cnf(c_0_6703,negated_conjecture,
g1_group_1(u1_struct_0(esk608_0),u1_group_1(esk608_0)) = k6_group_2(esk608_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6683,c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6704,plain,
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v3_struct_0(X2)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
i_0_1332 ).
cnf(c_0_6705,negated_conjecture,
( X1 = esk609_0
| ~ l1_struct_0(k5_autgroup(esk608_0))
| ~ v3_realset2(k5_autgroup(esk608_0))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(esk608_0))) ),
inference(spm,[status(thm)],[c_0_6684,c_0_6685]) ).
cnf(c_0_6706,negated_conjecture,
( r2_group_6(k6_group_6(esk608_0,esk608_0),k5_autgroup(esk608_0))
| v3_struct_0(k6_group_6(esk608_0,esk608_0))
| ~ v3_group_1(k5_autgroup(esk608_0))
| ~ v4_group_1(k5_autgroup(esk608_0))
| ~ l1_group_1(k5_autgroup(esk608_0)) ),
inference(csr,[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_6686,c_0_6687]),c_0_6688]),c_0_6689]),c_0_6690]),c_0_6691]),c_0_6692])]),c_0_6693]) ).
cnf(c_0_6707,plain,
( v3_group_1(k5_autgroup(esk608_0))
| v3_struct_0(k3_autgroup(esk608_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6694,c_0_6695]),c_0_6696]),c_0_6697])]) ).
cnf(c_0_6708,plain,
( l1_group_1(k5_autgroup(esk608_0))
| v3_struct_0(k3_autgroup(esk608_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6698,c_0_6695]),c_0_6696]),c_0_6697])]) ).
cnf(c_0_6709,plain,
( v4_group_1(k5_autgroup(esk608_0))
| v3_struct_0(k3_autgroup(esk608_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6699,c_0_6695]),c_0_6696]),c_0_6700]),c_0_6697])]) ).
cnf(c_0_6710,negated_conjecture,
v3_realset2(k6_group_6(esk608_0,k6_group_2(esk608_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6701,c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6711,plain,
k6_group_2(esk608_0) = esk608_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6702,c_0_6703]),c_0_6656]),c_0_6652])]) ).
cnf(c_0_6712,plain,
( v3_struct_0(X1)
| m1_subset_1(k2_group_1(X1),u1_struct_0(X1))
| ~ l1_group_1(X1) ),
i_0_1213 ).
cnf(c_0_6713,plain,
( v3_struct_0(k3_autgroup(esk608_0))
| ~ v3_struct_0(k5_autgroup(esk608_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6704,c_0_6695]),c_0_6696]),c_0_6697])]) ).
cnf(c_0_6714,plain,
( k2_group_1(X1) = k2_group_1(X2)
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1) ),
i_0_5227 ).
cnf(c_0_6715,plain,
( u1_vectsp_1(k19_monoid_0(u1_struct_0(X1))) = k2_group_1(k5_autgroup(X1))
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_3435 ).
cnf(c_0_6716,plain,
( X1 = esk609_0
| ~ v3_realset2(k5_autgroup(esk608_0))
| ~ l1_group_1(k5_autgroup(esk608_0))
| ~ m1_subset_1(X1,u1_struct_0(k5_autgroup(esk608_0))) ),
inference(spm,[status(thm)],[c_0_6705,c_0_6666]) ).
cnf(c_0_6717,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| v3_realset2(X1)
| ~ l1_group_1(X1)
| ~ l1_group_1(X2)
| ~ v1_group_1(X1)
| ~ v1_group_1(X2)
| ~ v4_group_1(X1)
| ~ v4_group_1(X2)
| ~ v3_realset2(X2)
| ~ v3_group_1(X1)
| ~ v3_group_1(X2)
| ~ r2_group_6(X2,X1) ),
i_0_6451 ).
cnf(c_0_6718,plain,
( r2_group_6(k6_group_6(esk608_0,esk608_0),k5_autgroup(esk608_0))
| v3_struct_0(k6_group_6(esk608_0,esk608_0))
| v3_struct_0(k3_autgroup(esk608_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_6706,c_0_6707]),c_0_6708]),c_0_6709]) ).
cnf(c_0_6719,negated_conjecture,
v3_realset2(k6_group_6(esk608_0,esk608_0)),
inference(rw,[status(thm)],[c_0_6710,c_0_6711]) ).
cnf(c_0_6720,plain,
( v3_struct_0(k3_autgroup(esk608_0))
| m1_subset_1(k2_group_1(k5_autgroup(esk608_0)),u1_struct_0(k5_autgroup(esk608_0))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_6712,c_0_6708]),c_0_6713]) ).
cnf(c_0_6721,plain,
( k2_group_1(k5_autgroup(esk608_0)) = k2_group_1(k3_autgroup(esk608_0))
| v3_struct_0(k3_autgroup(esk608_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6714,c_0_6695]),c_0_6696]),c_0_6700]),c_0_6697])]) ).
cnf(c_0_6722,plain,
( u1_vectsp_1(k19_monoid_0(u1_struct_0(X1))) = k2_group_1(k3_autgroup(X1))
| v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1) ),
i_0_2392 ).
cnf(c_0_6723,negated_conjecture,
u1_vectsp_1(k19_monoid_0(u1_struct_0(esk608_0))) = k2_group_1(k5_autgroup(esk608_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_6715,c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6724,plain,
( X1 = esk609_0
| ~ v3_realset2(k5_autgroup(esk608_0))
| ~ l1_group_1(k5_autgroup(esk608_0))
| ~ m1_subset_1(X1,k4_autgroup(esk608_0)) ),
inference(rw,[status(thm)],[c_0_6716,c_0_6678]) ).
cnf(c_0_6725,plain,
( v3_realset2(k5_autgroup(esk608_0))
| v3_struct_0(k6_group_6(esk608_0,esk608_0))
| v3_struct_0(k3_autgroup(esk608_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[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(spm,[status(thm)],[c_0_6717,c_0_6718]),c_0_6719]),c_0_6688]),c_0_6689]),c_0_6691]),c_0_6690]),c_0_6692])]),c_0_6708]),c_0_6709]),c_0_6707]),c_0_6713]) ).
cnf(c_0_6726,plain,
( v3_struct_0(k3_autgroup(esk608_0))
| m1_subset_1(k2_group_1(k3_autgroup(esk608_0)),u1_struct_0(k5_autgroup(esk608_0))) ),
inference(spm,[status(thm)],[c_0_6720,c_0_6721]) ).
cnf(c_0_6727,negated_conjecture,
k2_group_1(k5_autgroup(esk608_0)) != esk609_0,
i_0_4250 ).
cnf(c_0_6728,negated_conjecture,
k2_group_1(k5_autgroup(esk608_0)) = k2_group_1(k3_autgroup(esk608_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_6722,c_0_6650]),c_0_6723]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6729,plain,
( X1 = esk609_0
| v3_struct_0(k6_group_6(esk608_0,esk608_0))
| v3_struct_0(k3_autgroup(esk608_0))
| ~ m1_subset_1(X1,k4_autgroup(esk608_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_6724,c_0_6725]),c_0_6708]) ).
cnf(c_0_6730,plain,
( v3_struct_0(k3_autgroup(esk608_0))
| m1_subset_1(k2_group_1(k3_autgroup(esk608_0)),k4_autgroup(esk608_0)) ),
inference(rw,[status(thm)],[c_0_6726,c_0_6678]) ).
cnf(c_0_6731,negated_conjecture,
k2_group_1(k3_autgroup(esk608_0)) != esk609_0,
inference(rw,[status(thm)],[c_0_6727,c_0_6728]) ).
cnf(c_0_6732,plain,
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ v3_struct_0(k3_autgroup(X1)) ),
i_0_1226 ).
cnf(c_0_6733,plain,
( v3_struct_0(k6_group_6(esk608_0,esk608_0))
| v3_struct_0(k3_autgroup(esk608_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_6729,c_0_6730]),c_0_6731]) ).
cnf(c_0_6734,plain,
( v3_struct_0(X1)
| ~ l1_group_1(X1)
| ~ v4_group_1(X1)
| ~ v3_group_1(X1)
| ~ m1_group_2(X2,X1)
| ~ v1_group_3(X2,X1)
| ~ v3_struct_0(k6_group_6(X1,X2)) ),
i_0_1707 ).
cnf(c_0_6735,plain,
v3_struct_0(k6_group_6(esk608_0,esk608_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_6732,c_0_6733]),c_0_6650]),c_0_6651]),c_0_6656]),c_0_6652])]),c_0_6653]) ).
cnf(c_0_6736,plain,
$false,
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_6734,c_0_6735]),c_0_6672]),c_0_6673]),c_0_6650]),c_0_6651]),c_0_6652])]),c_0_6653]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GRP634+3 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.11/0.33 % Computer : n009.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 10:21:11 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected SinE mode:
% 0.71/0.88 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.71/0.88 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.71/0.88 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.71/0.88 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 36.91/8.57 # ENIGMATIC: Solved by autoschedule-lgb:
% 36.91/8.57 # No SInE strategy applied
% 36.91/8.57 # Trying AutoSched0 for 149 seconds
% 36.91/8.57 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
% 36.91/8.57 # and selection function SelectComplexExceptUniqMaxHorn.
% 36.91/8.57 #
% 36.91/8.57 # Preprocessing time : 0.028 s
% 36.91/8.57 # Presaturation interreduction done
% 36.91/8.57
% 36.91/8.57 # Proof found!
% 36.91/8.57 # SZS status Theorem
% 36.91/8.57 # SZS output start CNFRefutation
% See solution above
% 36.91/8.57 # Training examples: 0 positive, 0 negative
% 36.91/8.57
% 36.91/8.57 # -------------------------------------------------
% 36.91/8.57 # User time : 2.996 s
% 36.91/8.57 # System time : 0.062 s
% 36.91/8.57 # Total time : 3.058 s
% 36.91/8.57 # Maximum resident set size: 7124 pages
% 36.91/8.57
%------------------------------------------------------------------------------