%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : LAT351+4 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n028.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 : Sun Jul 17 04:30:10 EDT 2022
% Result : Theorem 99.11s 17.05s
% Output : CNFRefutation 99.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 25
% Syntax : Number of clauses : 57 ( 42 unt; 4 nHn; 41 RR)
% Number of literals : 172 ( 8 equ; 119 neg)
% Maximal clause size : 20 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-1 aty)
% Number of variables : 38 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_3772,plain,
( r5_waybel_1(X1,X2)
| k1_card_1(X3) != k1_card_1(X4)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v3_waybel_3(X2)
| ~ v3_waybel_3(X1)
| ~ r1_waybel22(X2,X4)
| ~ r1_waybel22(X1,X3) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3772) ).
cnf(i_0_3690,plain,
r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))),k1_waybel22(X1)),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3690) ).
cnf(i_0_3154,plain,
k1_card_1(k1_waybel22(X1)) = k1_card_1(X1),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3154) ).
cnf(i_0_1942,plain,
v4_orders_2(k2_yellow_1(X1)),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1942) ).
cnf(i_0_1943,plain,
v3_orders_2(k2_yellow_1(X1)),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1943) ).
cnf(i_0_1944,plain,
v2_orders_2(k2_yellow_1(X1)),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1944) ).
cnf(i_0_1150,plain,
l1_orders_2(k2_yellow_1(X1)),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1150) ).
cnf(i_0_3870,negated_conjecture,
r1_waybel22(esk382_0,esk383_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3870) ).
cnf(i_0_3872,negated_conjecture,
v3_waybel_3(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3872) ).
cnf(i_0_3874,negated_conjecture,
v2_lattice3(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3874) ).
cnf(i_0_3875,negated_conjecture,
v1_lattice3(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3875) ).
cnf(i_0_3876,negated_conjecture,
v4_orders_2(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3876) ).
cnf(i_0_3877,negated_conjecture,
v3_orders_2(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3877) ).
cnf(i_0_3873,negated_conjecture,
v3_lattice3(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3873) ).
cnf(i_0_3878,negated_conjecture,
v2_orders_2(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3878) ).
cnf(i_0_3871,negated_conjecture,
l1_orders_2(esk382_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3871) ).
cnf(i_0_3869,negated_conjecture,
k1_card_1(esk381_0) = k1_card_1(esk383_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3869) ).
cnf(i_0_3868,negated_conjecture,
~ r5_waybel_1(esk382_0,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0))))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_3868) ).
cnf(i_0_1605,plain,
( v3_struct_0(X1)
| v3_waybel_3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1605) ).
cnf(i_0_1463,plain,
v2_yellow_0(k2_yellow_1(k1_zfmisc_1(X1))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1463) ).
cnf(i_0_1466,plain,
v2_lattice3(k2_yellow_1(k1_zfmisc_1(X1))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1466) ).
cnf(i_0_1472,plain,
~ v3_struct_0(k2_yellow_1(k1_zfmisc_1(X1))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1472) ).
cnf(i_0_1747,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1747) ).
cnf(i_0_1748,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1748) ).
cnf(i_0_1608,plain,
( v3_struct_0(X1)
| v1_lattice3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-m27ac2d_/input.p',i_0_1608) ).
cnf(c_0_3904,plain,
( r5_waybel_1(X1,X2)
| k1_card_1(X3) != k1_card_1(X4)
| ~ l1_orders_2(X2)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X2)
| ~ v2_orders_2(X1)
| ~ v3_lattice3(X2)
| ~ v3_lattice3(X1)
| ~ v3_orders_2(X2)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X2)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X2)
| ~ v1_lattice3(X1)
| ~ v2_lattice3(X2)
| ~ v2_lattice3(X1)
| ~ v3_waybel_3(X2)
| ~ v3_waybel_3(X1)
| ~ r1_waybel22(X2,X4)
| ~ r1_waybel22(X1,X3) ),
i_0_3772 ).
cnf(c_0_3905,plain,
r1_waybel22(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))),k1_waybel22(X1)),
i_0_3690 ).
cnf(c_0_3906,plain,
k1_card_1(k1_waybel22(X1)) = k1_card_1(X1),
i_0_3154 ).
cnf(c_0_3907,plain,
v4_orders_2(k2_yellow_1(X1)),
i_0_1942 ).
cnf(c_0_3908,plain,
v3_orders_2(k2_yellow_1(X1)),
i_0_1943 ).
cnf(c_0_3909,plain,
v2_orders_2(k2_yellow_1(X1)),
i_0_1944 ).
cnf(c_0_3910,plain,
l1_orders_2(k2_yellow_1(X1)),
i_0_1150 ).
cnf(c_0_3911,plain,
( r5_waybel_1(X1,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))
| k1_card_1(X3) != k1_card_1(X2)
| ~ r1_waybel22(X1,X3)
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))
| ~ v3_waybel_3(X1)
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))
| ~ v2_lattice3(X1)
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X2)))))
| ~ v3_lattice3(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1) ),
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_3904,c_0_3905]),c_0_3906]),c_0_3907]),c_0_3908]),c_0_3909]),c_0_3910])]) ).
cnf(c_0_3912,negated_conjecture,
r1_waybel22(esk382_0,esk383_0),
i_0_3870 ).
cnf(c_0_3913,negated_conjecture,
v3_waybel_3(esk382_0),
i_0_3872 ).
cnf(c_0_3914,negated_conjecture,
v2_lattice3(esk382_0),
i_0_3874 ).
cnf(c_0_3915,negated_conjecture,
v1_lattice3(esk382_0),
i_0_3875 ).
cnf(c_0_3916,negated_conjecture,
v4_orders_2(esk382_0),
i_0_3876 ).
cnf(c_0_3917,negated_conjecture,
v3_orders_2(esk382_0),
i_0_3877 ).
cnf(c_0_3918,negated_conjecture,
v3_lattice3(esk382_0),
i_0_3873 ).
cnf(c_0_3919,negated_conjecture,
v2_orders_2(esk382_0),
i_0_3878 ).
cnf(c_0_3920,negated_conjecture,
l1_orders_2(esk382_0),
i_0_3871 ).
cnf(c_0_3921,negated_conjecture,
( r5_waybel_1(esk382_0,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))))
| k1_card_1(esk383_0) != k1_card_1(X1)
| ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(X1))))) ),
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(spm,[status(thm)],[c_0_3911,c_0_3912]),c_0_3913]),c_0_3914]),c_0_3915]),c_0_3916]),c_0_3917]),c_0_3918]),c_0_3919]),c_0_3920])]) ).
cnf(c_0_3922,negated_conjecture,
k1_card_1(esk381_0) = k1_card_1(esk383_0),
i_0_3869 ).
cnf(c_0_3923,negated_conjecture,
~ r5_waybel_1(esk382_0,k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0))))),
i_0_3868 ).
cnf(c_0_3924,negated_conjecture,
( ~ v3_waybel_3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0)))))
| ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0)))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0))))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3921,c_0_3922]),c_0_3923]) ).
cnf(c_0_3925,plain,
( v3_struct_0(X1)
| v3_waybel_3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
i_0_1605 ).
cnf(c_0_3926,plain,
v2_yellow_0(k2_yellow_1(k1_zfmisc_1(X1))),
i_0_1463 ).
cnf(c_0_3927,plain,
v2_lattice3(k2_yellow_1(k1_zfmisc_1(X1))),
i_0_1466 ).
cnf(c_0_3928,plain,
~ v3_struct_0(k2_yellow_1(k1_zfmisc_1(X1))),
i_0_1472 ).
cnf(c_0_3929,plain,
( ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0)))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0)))))
| ~ v3_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_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(spm,[status(thm)],[c_0_3924,c_0_3925]),c_0_3926]),c_0_3927]),c_0_3907]),c_0_3908]),c_0_3909]),c_0_3910])]),c_0_3928]) ).
cnf(c_0_3930,plain,
( v3_lattice3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
i_0_1747 ).
cnf(c_0_3931,plain,
( ~ v2_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0)))))
| ~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0))))) ),
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_3929,c_0_3930]),c_0_3926]),c_0_3927]),c_0_3907]),c_0_3908]),c_0_3909]),c_0_3910])]) ).
cnf(c_0_3932,plain,
( v2_lattice3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
i_0_1748 ).
cnf(c_0_3933,plain,
~ v1_lattice3(k2_yellow_1(k9_waybel_0(k2_yellow_1(k1_zfmisc_1(esk381_0))))),
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_3931,c_0_3932]),c_0_3926]),c_0_3927]),c_0_3907]),c_0_3908]),c_0_3909]),c_0_3910])]) ).
cnf(c_0_3934,plain,
( v3_struct_0(X1)
| v1_lattice3(k2_yellow_1(k9_waybel_0(X1)))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v2_lattice3(X1)
| ~ v2_yellow_0(X1) ),
i_0_1608 ).
cnf(c_0_3935,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(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3933,c_0_3934]),c_0_3926]),c_0_3927]),c_0_3907]),c_0_3908]),c_0_3909]),c_0_3910])]),c_0_3928]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : LAT351+4 : TPTP v8.1.0. Released v3.4.0.
% 0.06/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Wed Jun 29 21:31:22 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.19/0.44 # ENIGMATIC: Selected SinE mode:
% 1.70/1.94 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.70/1.94 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 1.70/1.94 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 1.70/1.94 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 99.11/17.05 # ENIGMATIC: Solved by Enigma+tptp-cade20-model03-h2e15+lgb-t150-d30-l6400-e0.15+coop-eprover66:
% 99.11/17.05 # ENIGMA: LightGBM model '/export/starexec/sandbox/solver/bin/data/Enigma/tptp-cade20-model03-h2e15/lgb-t150-d30-l6400-e0.15/model.lgb' loaded. (hash_base: 32768; conj_feats: 42; version: 991; iters: 150)
% 99.11/17.05 # Preprocessing time : 5.119 s
% 99.11/17.05 # Presaturation interreduction done
% 99.11/17.05
% 99.11/17.05 # Proof found!
% 99.11/17.05 # SZS status Theorem
% 99.11/17.05 # SZS output start CNFRefutation
% See solution above
% 99.11/17.05 # Training examples: 0 positive, 0 negative
% 99.11/17.05
% 99.11/17.05 # -------------------------------------------------
% 99.11/17.05 # User time : 10.778 s
% 99.11/17.05 # System time : 0.170 s
% 99.11/17.05 # Total time : 10.948 s
% 99.11/17.05 # ...preprocessing : 5.119 s
% 99.11/17.05 # ...main loop : 5.829 s
% 99.11/17.05 # Maximum resident set size: 190688 pages
% 99.11/17.05
%------------------------------------------------------------------------------