%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : LAT347+3 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n019.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:05 EDT 2022
% Result : Theorem 12.67s 5.13s
% Output : CNFRefutation 12.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 22
% Syntax : Number of clauses : 54 ( 26 unt; 6 nHn; 52 RR)
% Number of literals : 143 ( 10 equ; 94 neg)
% Maximal clause size : 11 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-2 aty)
% Number of variables : 30 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_6745,plain,
( k1_yellow_0(k2_yellow_1(k8_waybel_0(X1)),X2) = k3_tarski(X2)
| v1_xboole_0(X2)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v1_yellow_0(X1)
| ~ v1_waybel_0(X2,k2_yellow_1(k8_waybel_0(X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X1))))) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_6745) ).
cnf(i_0_4158,plain,
u1_struct_0(k2_yellow_1(X1)) = X1,
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4158) ).
cnf(i_0_6556,plain,
( k8_waybel_0(k7_lattice3(X1)) = k9_waybel_0(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_6556) ).
cnf(i_0_1296,plain,
( l1_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_1296) ).
cnf(i_0_5771,plain,
( v2_orders_2(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(k7_lattice3(X1)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_5771) ).
cnf(i_0_6380,plain,
( v3_orders_2(X1)
| ~ l1_orders_2(X1)
| ~ v3_orders_2(k7_lattice3(X1)) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_6380) ).
cnf(i_0_4124,negated_conjecture,
m1_subset_1(esk480_0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(esk479_0))))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4124) ).
cnf(i_0_163,plain,
( ~ l1_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ v2_lattice3(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_163) ).
cnf(i_0_4128,negated_conjecture,
v2_lattice3(esk479_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4128) ).
cnf(i_0_4127,negated_conjecture,
l1_orders_2(esk479_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4127) ).
cnf(i_0_4125,negated_conjecture,
v1_waybel_0(esk480_0,k2_yellow_1(k9_waybel_0(esk479_0))),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4125) ).
cnf(i_0_4123,negated_conjecture,
k1_yellow_0(k2_yellow_1(k9_waybel_0(esk479_0)),esk480_0) != k3_tarski(esk480_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4123) ).
cnf(i_0_4126,negated_conjecture,
~ v1_xboole_0(esk480_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4126) ).
cnf(i_0_3819,plain,
( v1_lattice3(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_3819) ).
cnf(i_0_4955,plain,
( v1_yellow_0(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v2_yellow_0(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4955) ).
cnf(i_0_4129,negated_conjecture,
v2_yellow_0(esk479_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4129) ).
cnf(i_0_5772,plain,
( v2_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_5772) ).
cnf(i_0_4132,negated_conjecture,
v2_orders_2(esk479_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4132) ).
cnf(i_0_6381,plain,
( v3_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v3_orders_2(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_6381) ).
cnf(i_0_4131,negated_conjecture,
v3_orders_2(esk479_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4131) ).
cnf(i_0_6158,plain,
( v4_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_6158) ).
cnf(i_0_4130,negated_conjecture,
v4_orders_2(esk479_0),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-uejqu42t/lgb.p',i_0_4130) ).
cnf(c_0_6768,plain,
( k1_yellow_0(k2_yellow_1(k8_waybel_0(X1)),X2) = k3_tarski(X2)
| v1_xboole_0(X2)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v4_orders_2(X1)
| ~ v1_lattice3(X1)
| ~ v1_yellow_0(X1)
| ~ v1_waybel_0(X2,k2_yellow_1(k8_waybel_0(X1)))
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k8_waybel_0(X1))))) ),
i_0_6745 ).
cnf(c_0_6769,plain,
u1_struct_0(k2_yellow_1(X1)) = X1,
i_0_4158 ).
cnf(c_0_6770,plain,
( k1_yellow_0(k2_yellow_1(k8_waybel_0(X1)),X2) = k3_tarski(X2)
| v1_xboole_0(X2)
| ~ v1_yellow_0(X1)
| ~ v1_lattice3(X1)
| ~ v4_orders_2(X1)
| ~ v3_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ l1_orders_2(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(k8_waybel_0(X1)))
| ~ v1_waybel_0(X2,k2_yellow_1(k8_waybel_0(X1))) ),
inference(rw,[status(thm)],[c_0_6768,c_0_6769]) ).
cnf(c_0_6771,plain,
( k8_waybel_0(k7_lattice3(X1)) = k9_waybel_0(X1)
| v3_struct_0(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1)
| ~ v3_orders_2(X1) ),
i_0_6556 ).
cnf(c_0_6772,plain,
( l1_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1) ),
i_0_1296 ).
cnf(c_0_6773,plain,
( v2_orders_2(X1)
| ~ l1_orders_2(X1)
| ~ v2_orders_2(k7_lattice3(X1)) ),
i_0_5771 ).
cnf(c_0_6774,plain,
( v3_orders_2(X1)
| ~ l1_orders_2(X1)
| ~ v3_orders_2(k7_lattice3(X1)) ),
i_0_6380 ).
cnf(c_0_6775,negated_conjecture,
m1_subset_1(esk480_0,k1_zfmisc_1(u1_struct_0(k2_yellow_1(k9_waybel_0(esk479_0))))),
i_0_4124 ).
cnf(c_0_6776,plain,
( ~ l1_orders_2(X1)
| ~ v3_struct_0(X1)
| ~ v2_lattice3(X1) ),
i_0_163 ).
cnf(c_0_6777,negated_conjecture,
v2_lattice3(esk479_0),
i_0_4128 ).
cnf(c_0_6778,negated_conjecture,
l1_orders_2(esk479_0),
i_0_4127 ).
cnf(c_0_6779,plain,
( k1_yellow_0(k2_yellow_1(k9_waybel_0(X1)),X2) = k3_tarski(X2)
| v3_struct_0(X1)
| v1_xboole_0(X2)
| ~ v1_yellow_0(k7_lattice3(X1))
| ~ v1_lattice3(k7_lattice3(X1))
| ~ v4_orders_2(k7_lattice3(X1))
| ~ v3_orders_2(k7_lattice3(X1))
| ~ v2_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(k9_waybel_0(X1)))
| ~ v1_waybel_0(X2,k2_yellow_1(k9_waybel_0(X1))) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_6770,c_0_6771]),c_0_6772]),c_0_6773]),c_0_6774]) ).
cnf(c_0_6780,negated_conjecture,
m1_subset_1(esk480_0,k1_zfmisc_1(k9_waybel_0(esk479_0))),
inference(rw,[status(thm)],[c_0_6775,c_0_6769]) ).
cnf(c_0_6781,negated_conjecture,
v1_waybel_0(esk480_0,k2_yellow_1(k9_waybel_0(esk479_0))),
i_0_4125 ).
cnf(c_0_6782,negated_conjecture,
k1_yellow_0(k2_yellow_1(k9_waybel_0(esk479_0)),esk480_0) != k3_tarski(esk480_0),
i_0_4123 ).
cnf(c_0_6783,negated_conjecture,
~ v3_struct_0(esk479_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6776,c_0_6777]),c_0_6778])]) ).
cnf(c_0_6784,negated_conjecture,
~ v1_xboole_0(esk480_0),
i_0_4126 ).
cnf(c_0_6785,negated_conjecture,
( ~ v1_yellow_0(k7_lattice3(esk479_0))
| ~ v1_lattice3(k7_lattice3(esk479_0))
| ~ v4_orders_2(k7_lattice3(esk479_0))
| ~ v3_orders_2(k7_lattice3(esk479_0))
| ~ v2_orders_2(k7_lattice3(esk479_0)) ),
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(spm,[status(thm)],[c_0_6779,c_0_6780]),c_0_6778]),c_0_6781])]),c_0_6782]),c_0_6783]),c_0_6784]) ).
cnf(c_0_6786,plain,
( v1_lattice3(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v2_lattice3(X1) ),
i_0_3819 ).
cnf(c_0_6787,plain,
( ~ v1_yellow_0(k7_lattice3(esk479_0))
| ~ v4_orders_2(k7_lattice3(esk479_0))
| ~ v3_orders_2(k7_lattice3(esk479_0))
| ~ v2_orders_2(k7_lattice3(esk479_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6785,c_0_6786]),c_0_6777]),c_0_6778])]) ).
cnf(c_0_6788,plain,
( v1_yellow_0(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v2_yellow_0(X1) ),
i_0_4955 ).
cnf(c_0_6789,negated_conjecture,
v2_yellow_0(esk479_0),
i_0_4129 ).
cnf(c_0_6790,plain,
( ~ v4_orders_2(k7_lattice3(esk479_0))
| ~ v3_orders_2(k7_lattice3(esk479_0))
| ~ v2_orders_2(k7_lattice3(esk479_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6787,c_0_6788]),c_0_6789]),c_0_6778])]) ).
cnf(c_0_6791,plain,
( v2_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v2_orders_2(X1) ),
i_0_5772 ).
cnf(c_0_6792,negated_conjecture,
v2_orders_2(esk479_0),
i_0_4132 ).
cnf(c_0_6793,plain,
( ~ v4_orders_2(k7_lattice3(esk479_0))
| ~ v3_orders_2(k7_lattice3(esk479_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6790,c_0_6791]),c_0_6792]),c_0_6778])]) ).
cnf(c_0_6794,plain,
( v3_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v3_orders_2(X1) ),
i_0_6381 ).
cnf(c_0_6795,negated_conjecture,
v3_orders_2(esk479_0),
i_0_4131 ).
cnf(c_0_6796,plain,
~ v4_orders_2(k7_lattice3(esk479_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6793,c_0_6794]),c_0_6795]),c_0_6778])]) ).
cnf(c_0_6797,plain,
( v4_orders_2(k7_lattice3(X1))
| ~ l1_orders_2(X1)
| ~ v4_orders_2(X1) ),
i_0_6158 ).
cnf(c_0_6798,negated_conjecture,
v4_orders_2(esk479_0),
i_0_4130 ).
cnf(c_0_6799,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_6796,c_0_6797]),c_0_6798]),c_0_6778])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : LAT347+3 : TPTP v8.1.0. Released v3.4.0.
% 0.03/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.13/0.33 % Computer : n019.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.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Thu Jun 30 09:44:58 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.18/0.45 # ENIGMATIC: Selected SinE mode:
% 0.89/1.08 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.89/1.08 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.89/1.08 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.89/1.08 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 12.67/5.13 # ENIGMATIC: Solved by autoschedule-lgb:
% 12.67/5.13 # No SInE strategy applied
% 12.67/5.13 # Trying AutoSched0 for 149 seconds
% 12.67/5.13 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S2s
% 12.67/5.13 # and selection function SelectCQArNT.
% 12.67/5.13 #
% 12.67/5.13 # Preprocessing time : 0.031 s
% 12.67/5.13 # Presaturation interreduction done
% 12.67/5.13
% 12.67/5.13 # Proof found!
% 12.67/5.13 # SZS status Theorem
% 12.67/5.13 # SZS output start CNFRefutation
% See solution above
% 12.67/5.13 # Training examples: 0 positive, 0 negative
% 12.67/5.13
% 12.67/5.13 # -------------------------------------------------
% 12.67/5.13 # User time : 0.137 s
% 12.67/5.13 # System time : 0.008 s
% 12.67/5.13 # Total time : 0.145 s
% 12.67/5.13 # Maximum resident set size: 7128 pages
% 12.67/5.13
%------------------------------------------------------------------------------