%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : ALG214+3 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n024.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 : Thu Jul 14 15:33:01 EDT 2022
% Result : Theorem 10.75s 4.30s
% Output : CNFRefutation 10.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 27
% Syntax : Number of clauses : 64 ( 49 unt; 15 nHn; 64 RR)
% Number of literals : 331 ( 13 equ; 242 neg)
% Maximal clause size : 22 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-4 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 45 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_2610,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| m2_rmod_4(X3,X2,X1,X4)
| ~ v4_group_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v7_vectsp_1(X2)
| ~ l3_vectsp_1(X2)
| ~ r1_tarski(X5,X4)
| ~ v5_vectsp_2(X1,X2)
| ~ l1_vectsp_2(X1,X2)
| ~ m2_rmod_4(X3,X2,X1,X5)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2610) ).
cnf(i_0_2859,negated_conjecture,
m1_subset_1(esk413_0,k1_zfmisc_1(u1_struct_0(esk412_0))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2859) ).
cnf(i_0_2862,negated_conjecture,
v6_rlvect_1(esk412_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2862) ).
cnf(i_0_2863,negated_conjecture,
v5_rlvect_1(esk412_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2863) ).
cnf(i_0_2864,negated_conjecture,
v4_rlvect_1(esk412_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2864) ).
cnf(i_0_2865,negated_conjecture,
v3_rlvect_1(esk412_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2865) ).
cnf(i_0_2866,negated_conjecture,
~ v3_struct_0(esk412_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2866) ).
cnf(i_0_301,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| v1_rmod_5(X3,X2,X1)
| m2_rmod_4(esk47_3(X2,X1,X3),X2,X1,X3)
| ~ v4_group_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v7_vectsp_1(X2)
| ~ l3_vectsp_1(X2)
| ~ v5_vectsp_2(X1,X2)
| ~ l1_vectsp_2(X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_301) ).
cnf(i_0_2858,negated_conjecture,
m1_subset_1(esk414_0,k1_zfmisc_1(u1_struct_0(esk412_0))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2858) ).
cnf(i_0_2857,negated_conjecture,
r1_tarski(esk413_0,esk414_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2857) ).
cnf(i_0_2860,negated_conjecture,
l1_vectsp_2(esk412_0,esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2860) ).
cnf(i_0_2867,negated_conjecture,
l3_vectsp_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2867) ).
cnf(i_0_2869,negated_conjecture,
v7_vectsp_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2869) ).
cnf(i_0_2872,negated_conjecture,
v6_rlvect_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2872) ).
cnf(i_0_2873,negated_conjecture,
v5_rlvect_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2873) ).
cnf(i_0_2874,negated_conjecture,
v4_rlvect_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2874) ).
cnf(i_0_2875,negated_conjecture,
v3_rlvect_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2875) ).
cnf(i_0_2870,negated_conjecture,
v6_vectsp_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2870) ).
cnf(i_0_2868,negated_conjecture,
v8_vectsp_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2868) ).
cnf(i_0_2871,negated_conjecture,
v4_group_1(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2871) ).
cnf(i_0_2861,negated_conjecture,
v5_vectsp_2(esk412_0,esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2861) ).
cnf(i_0_2876,negated_conjecture,
~ v3_struct_0(esk411_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2876) ).
cnf(i_0_2855,negated_conjecture,
~ v1_rmod_5(esk413_0,esk411_0,esk412_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2855) ).
cnf(i_0_300,plain,
( k5_rmod_4(X1,X2,esk47_3(X1,X2,X3)) = k1_rlvect_1(X2)
| v3_struct_0(X2)
| v3_struct_0(X1)
| v1_rmod_5(X3,X1,X2)
| ~ v4_group_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v7_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_300) ).
cnf(i_0_302,plain,
( k2_rmod_4(X1,X2,X3) = k1_xboole_0
| v3_struct_0(X2)
| v3_struct_0(X1)
| k5_rmod_4(X1,X2,X3) != k1_rlvect_1(X2)
| ~ v4_group_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v7_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,X1)
| ~ v1_rmod_5(X4,X1,X2)
| ~ m2_rmod_4(X3,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_302) ).
cnf(i_0_2856,negated_conjecture,
v1_rmod_5(esk414_0,esk411_0,esk412_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_2856) ).
cnf(i_0_299,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| v1_rmod_5(X3,X2,X1)
| k2_rmod_4(X2,X1,esk47_3(X2,X1,X3)) != k1_xboole_0
| ~ v4_group_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v7_vectsp_1(X2)
| ~ l3_vectsp_1(X2)
| ~ v5_vectsp_2(X1,X2)
| ~ l1_vectsp_2(X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-cuj0w1iw/lgb.p',i_0_299) ).
cnf(c_0_2904,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| m2_rmod_4(X3,X2,X1,X4)
| ~ v4_group_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v7_vectsp_1(X2)
| ~ l3_vectsp_1(X2)
| ~ r1_tarski(X5,X4)
| ~ v5_vectsp_2(X1,X2)
| ~ l1_vectsp_2(X1,X2)
| ~ m2_rmod_4(X3,X2,X1,X5)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m1_subset_1(X5,k1_zfmisc_1(u1_struct_0(X1))) ),
i_0_2610 ).
cnf(c_0_2905,negated_conjecture,
m1_subset_1(esk413_0,k1_zfmisc_1(u1_struct_0(esk412_0))),
i_0_2859 ).
cnf(c_0_2906,negated_conjecture,
v6_rlvect_1(esk412_0),
i_0_2862 ).
cnf(c_0_2907,negated_conjecture,
v5_rlvect_1(esk412_0),
i_0_2863 ).
cnf(c_0_2908,negated_conjecture,
v4_rlvect_1(esk412_0),
i_0_2864 ).
cnf(c_0_2909,negated_conjecture,
v3_rlvect_1(esk412_0),
i_0_2865 ).
cnf(c_0_2910,negated_conjecture,
~ v3_struct_0(esk412_0),
i_0_2866 ).
cnf(c_0_2911,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| v1_rmod_5(X3,X2,X1)
| m2_rmod_4(esk47_3(X2,X1,X3),X2,X1,X3)
| ~ v4_group_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v7_vectsp_1(X2)
| ~ l3_vectsp_1(X2)
| ~ v5_vectsp_2(X1,X2)
| ~ l1_vectsp_2(X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) ),
i_0_301 ).
cnf(c_0_2912,negated_conjecture,
( m2_rmod_4(X1,X2,esk412_0,X3)
| v3_struct_0(X2)
| ~ m2_rmod_4(X1,X2,esk412_0,esk413_0)
| ~ l3_vectsp_1(X2)
| ~ v7_vectsp_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v3_rlvect_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v4_group_1(X2)
| ~ r1_tarski(esk413_0,X3)
| ~ l1_vectsp_2(esk412_0,X2)
| ~ v5_vectsp_2(esk412_0,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(esk412_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_2904,c_0_2905]),c_0_2906]),c_0_2907]),c_0_2908]),c_0_2909])]),c_0_2910]) ).
cnf(c_0_2913,negated_conjecture,
m1_subset_1(esk414_0,k1_zfmisc_1(u1_struct_0(esk412_0))),
i_0_2858 ).
cnf(c_0_2914,negated_conjecture,
r1_tarski(esk413_0,esk414_0),
i_0_2857 ).
cnf(c_0_2915,negated_conjecture,
( m2_rmod_4(esk47_3(X1,esk412_0,esk413_0),X1,esk412_0,esk413_0)
| v3_struct_0(X1)
| v1_rmod_5(esk413_0,X1,esk412_0)
| ~ l3_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v4_group_1(X1)
| ~ l1_vectsp_2(esk412_0,X1)
| ~ v5_vectsp_2(esk412_0,X1) ),
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_2911,c_0_2905]),c_0_2906]),c_0_2907]),c_0_2908]),c_0_2909])]),c_0_2910]) ).
cnf(c_0_2916,negated_conjecture,
l1_vectsp_2(esk412_0,esk411_0),
i_0_2860 ).
cnf(c_0_2917,negated_conjecture,
l3_vectsp_1(esk411_0),
i_0_2867 ).
cnf(c_0_2918,negated_conjecture,
v7_vectsp_1(esk411_0),
i_0_2869 ).
cnf(c_0_2919,negated_conjecture,
v6_rlvect_1(esk411_0),
i_0_2872 ).
cnf(c_0_2920,negated_conjecture,
v5_rlvect_1(esk411_0),
i_0_2873 ).
cnf(c_0_2921,negated_conjecture,
v4_rlvect_1(esk411_0),
i_0_2874 ).
cnf(c_0_2922,negated_conjecture,
v3_rlvect_1(esk411_0),
i_0_2875 ).
cnf(c_0_2923,negated_conjecture,
v6_vectsp_1(esk411_0),
i_0_2870 ).
cnf(c_0_2924,negated_conjecture,
v8_vectsp_1(esk411_0),
i_0_2868 ).
cnf(c_0_2925,negated_conjecture,
v4_group_1(esk411_0),
i_0_2871 ).
cnf(c_0_2926,negated_conjecture,
v5_vectsp_2(esk412_0,esk411_0),
i_0_2861 ).
cnf(c_0_2927,negated_conjecture,
~ v3_struct_0(esk411_0),
i_0_2876 ).
cnf(c_0_2928,negated_conjecture,
~ v1_rmod_5(esk413_0,esk411_0,esk412_0),
i_0_2855 ).
cnf(c_0_2929,plain,
( k5_rmod_4(X1,X2,esk47_3(X1,X2,X3)) = k1_rlvect_1(X2)
| v3_struct_0(X2)
| v3_struct_0(X1)
| v1_rmod_5(X3,X1,X2)
| ~ v4_group_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v7_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,X1)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X2))) ),
i_0_300 ).
cnf(c_0_2930,plain,
( k2_rmod_4(X1,X2,X3) = k1_xboole_0
| v3_struct_0(X2)
| v3_struct_0(X1)
| k5_rmod_4(X1,X2,X3) != k1_rlvect_1(X2)
| ~ v4_group_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v7_vectsp_1(X1)
| ~ l3_vectsp_1(X1)
| ~ v5_vectsp_2(X2,X1)
| ~ l1_vectsp_2(X2,X1)
| ~ v1_rmod_5(X4,X1,X2)
| ~ m2_rmod_4(X3,X1,X2,X4)
| ~ m1_subset_1(X4,k1_zfmisc_1(u1_struct_0(X2))) ),
i_0_302 ).
cnf(c_0_2931,negated_conjecture,
( m2_rmod_4(X1,X2,esk412_0,esk414_0)
| v3_struct_0(X2)
| ~ m2_rmod_4(X1,X2,esk412_0,esk413_0)
| ~ l3_vectsp_1(X2)
| ~ v7_vectsp_1(X2)
| ~ v6_rlvect_1(X2)
| ~ v5_rlvect_1(X2)
| ~ v4_rlvect_1(X2)
| ~ v3_rlvect_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v4_group_1(X2)
| ~ l1_vectsp_2(esk412_0,X2)
| ~ v5_vectsp_2(esk412_0,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2912,c_0_2913]),c_0_2914])]) ).
cnf(c_0_2932,negated_conjecture,
m2_rmod_4(esk47_3(esk411_0,esk412_0,esk413_0),esk411_0,esk412_0,esk413_0),
inference(sr,[status(thm)],[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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2915,c_0_2916]),c_0_2917]),c_0_2918]),c_0_2919]),c_0_2920]),c_0_2921]),c_0_2922]),c_0_2923]),c_0_2924]),c_0_2925]),c_0_2926])]),c_0_2927]),c_0_2928]) ).
cnf(c_0_2933,negated_conjecture,
( k5_rmod_4(X1,esk412_0,esk47_3(X1,esk412_0,esk413_0)) = k1_rlvect_1(esk412_0)
| v3_struct_0(X1)
| v1_rmod_5(esk413_0,X1,esk412_0)
| ~ l3_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v4_group_1(X1)
| ~ l1_vectsp_2(esk412_0,X1)
| ~ v5_vectsp_2(esk412_0,X1) ),
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_2929,c_0_2905]),c_0_2906]),c_0_2907]),c_0_2908]),c_0_2909])]),c_0_2910]) ).
cnf(c_0_2934,negated_conjecture,
( k2_rmod_4(X1,esk412_0,X2) = k1_xboole_0
| v3_struct_0(X1)
| k5_rmod_4(X1,esk412_0,X2) != k1_rlvect_1(esk412_0)
| ~ m2_rmod_4(X2,X1,esk412_0,esk414_0)
| ~ l3_vectsp_1(X1)
| ~ v7_vectsp_1(X1)
| ~ v6_rlvect_1(X1)
| ~ v5_rlvect_1(X1)
| ~ v4_rlvect_1(X1)
| ~ v3_rlvect_1(X1)
| ~ v6_vectsp_1(X1)
| ~ v8_vectsp_1(X1)
| ~ v4_group_1(X1)
| ~ v1_rmod_5(esk414_0,X1,esk412_0)
| ~ l1_vectsp_2(esk412_0,X1)
| ~ v5_vectsp_2(esk412_0,X1) ),
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_2930,c_0_2913]),c_0_2906]),c_0_2907]),c_0_2908]),c_0_2909])]),c_0_2910]) ).
cnf(c_0_2935,negated_conjecture,
m2_rmod_4(esk47_3(esk411_0,esk412_0,esk413_0),esk411_0,esk412_0,esk414_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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2931,c_0_2932]),c_0_2917]),c_0_2918]),c_0_2919]),c_0_2920]),c_0_2921]),c_0_2922]),c_0_2923]),c_0_2924]),c_0_2925]),c_0_2916]),c_0_2926])]),c_0_2927]) ).
cnf(c_0_2936,negated_conjecture,
k5_rmod_4(esk411_0,esk412_0,esk47_3(esk411_0,esk412_0,esk413_0)) = k1_rlvect_1(esk412_0),
inference(sr,[status(thm)],[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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2933,c_0_2916]),c_0_2917]),c_0_2918]),c_0_2919]),c_0_2920]),c_0_2921]),c_0_2922]),c_0_2923]),c_0_2924]),c_0_2925]),c_0_2926])]),c_0_2927]),c_0_2928]) ).
cnf(c_0_2937,negated_conjecture,
v1_rmod_5(esk414_0,esk411_0,esk412_0),
i_0_2856 ).
cnf(c_0_2938,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| v1_rmod_5(X3,X2,X1)
| k2_rmod_4(X2,X1,esk47_3(X2,X1,X3)) != k1_xboole_0
| ~ v4_group_1(X2)
| ~ v8_vectsp_1(X2)
| ~ v6_vectsp_1(X2)
| ~ v3_rlvect_1(X1)
| ~ v3_rlvect_1(X2)
| ~ v4_rlvect_1(X1)
| ~ v4_rlvect_1(X2)
| ~ v5_rlvect_1(X1)
| ~ v5_rlvect_1(X2)
| ~ v6_rlvect_1(X1)
| ~ v6_rlvect_1(X2)
| ~ v7_vectsp_1(X2)
| ~ l3_vectsp_1(X2)
| ~ v5_vectsp_2(X1,X2)
| ~ l1_vectsp_2(X1,X2)
| ~ m1_subset_1(X3,k1_zfmisc_1(u1_struct_0(X1))) ),
i_0_299 ).
cnf(c_0_2939,negated_conjecture,
k2_rmod_4(esk411_0,esk412_0,esk47_3(esk411_0,esk412_0,esk413_0)) = k1_xboole_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(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_2934,c_0_2935]),c_0_2936]),c_0_2917]),c_0_2918]),c_0_2919]),c_0_2920]),c_0_2921]),c_0_2922]),c_0_2923]),c_0_2924]),c_0_2925]),c_0_2937]),c_0_2916]),c_0_2926])]),c_0_2927]) ).
cnf(c_0_2940,plain,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[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(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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_2938,c_0_2939]),c_0_2917]),c_0_2918]),c_0_2919]),c_0_2906]),c_0_2920]),c_0_2907]),c_0_2921]),c_0_2908]),c_0_2922]),c_0_2909]),c_0_2923]),c_0_2924]),c_0_2925]),c_0_2916]),c_0_2926]),c_0_2905])]),c_0_2927]),c_0_2910]),c_0_2928]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : ALG214+3 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.13/0.33 % Computer : n024.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Wed Jun 8 13:48:22 EDT 2022
% 0.13/0.33 % CPUTime :
% 0.19/0.44 # ENIGMATIC: Selected SinE mode:
% 0.54/0.76 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.54/0.76 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.54/0.76 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.54/0.76 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 10.75/4.30 # ENIGMATIC: Solved by autoschedule-lgb:
% 10.75/4.30 # No SInE strategy applied
% 10.75/4.30 # Trying AutoSched0 for 149 seconds
% 10.75/4.30 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
% 10.75/4.30 # and selection function SelectComplexExceptUniqMaxHorn.
% 10.75/4.30 #
% 10.75/4.30 # Preprocessing time : 0.027 s
% 10.75/4.30 # Presaturation interreduction done
% 10.75/4.30
% 10.75/4.30 # Proof found!
% 10.75/4.30 # SZS status Theorem
% 10.75/4.30 # SZS output start CNFRefutation
% See solution above
% 10.75/4.30 # Training examples: 0 positive, 0 negative
% 10.75/4.30
% 10.75/4.30 # -------------------------------------------------
% 10.75/4.30 # User time : 0.055 s
% 10.75/4.30 # System time : 0.003 s
% 10.75/4.30 # Total time : 0.058 s
% 10.75/4.30 # Maximum resident set size: 7128 pages
% 10.75/4.30
%------------------------------------------------------------------------------