%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : CSR079+5 : TPTP v8.1.0. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n007.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 : Fri Jul 15 02:47:33 EDT 2022
% Result : Theorem 14.14s 4.72s
% Output : CNFRefutation 14.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 19
% Syntax : Number of clauses : 58 ( 46 unt; 0 nHn; 58 RR)
% Number of literals : 77 ( 26 equ; 21 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 17 con; 0-0 aty)
% Number of variables : 22 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_3872,plain,
s__Class5_9 = s__Class5_8,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3872) ).
cnf(i_0_3873,plain,
s__Class5_10 = s__Class5_9,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3873) ).
cnf(i_0_3870,plain,
s__Class5_8 = s__Class5_7,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3870) ).
cnf(i_0_3869,plain,
s__Class5_7 = s__Class5_6,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3869) ).
cnf(i_0_3868,plain,
s__Class5_5 = s__Class5_6,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3868) ).
cnf(i_0_3867,plain,
s__Class5_5 = s__Class5_4,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3867) ).
cnf(i_0_3866,plain,
s__Class5_3 = s__Class5_4,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3866) ).
cnf(i_0_3865,plain,
s__Class5_3 = s__Class5_2,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3865) ).
cnf(i_0_3864,plain,
s__Class5_1 = s__Class5_2,
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3864) ).
cnf(i_0_1849,plain,
( s__instance(X1,X2)
| ~ s__subclass(X3,X2)
| ~ s__instance(X1,X3)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_1849) ).
cnf(i_0_1795,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_1795) ).
cnf(i_0_1796,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_1796) ).
cnf(i_0_3874,plain,
s__subclass(s__Lizard5_1,s__Class5_1),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3874) ).
cnf(i_0_3875,plain,
s__subclass(s__Class5_10,s__Reptile),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3875) ).
cnf(i_0_3871,plain,
s__instance(s__Organism5_1,s__Lizard5_1),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3871) ).
cnf(i_0_3203,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3203) ).
cnf(i_0_3178,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3178) ).
cnf(i_0_3162,plain,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3162) ).
cnf(i_0_3883,negated_conjecture,
~ s__instance(s__Organism5_1,s__Animal),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-gtqh_9s1/lgb.p',i_0_3883) ).
cnf(c_0_3903,plain,
s__Class5_9 = s__Class5_8,
i_0_3872 ).
cnf(c_0_3904,plain,
s__Class5_10 = s__Class5_9,
i_0_3873 ).
cnf(c_0_3905,plain,
s__Class5_8 = s__Class5_7,
i_0_3870 ).
cnf(c_0_3906,plain,
s__Class5_8 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3903,c_0_3904]) ).
cnf(c_0_3907,plain,
s__Class5_7 = s__Class5_6,
i_0_3869 ).
cnf(c_0_3908,plain,
s__Class5_7 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3905,c_0_3906]) ).
cnf(c_0_3909,plain,
s__Class5_5 = s__Class5_6,
i_0_3868 ).
cnf(c_0_3910,plain,
s__Class5_6 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3907,c_0_3908]) ).
cnf(c_0_3911,plain,
s__Class5_5 = s__Class5_4,
i_0_3867 ).
cnf(c_0_3912,plain,
s__Class5_5 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3909,c_0_3910]) ).
cnf(c_0_3913,plain,
s__Class5_3 = s__Class5_4,
i_0_3866 ).
cnf(c_0_3914,plain,
s__Class5_4 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3911,c_0_3912]) ).
cnf(c_0_3915,plain,
s__Class5_3 = s__Class5_2,
i_0_3865 ).
cnf(c_0_3916,plain,
s__Class5_3 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3913,c_0_3914]) ).
cnf(c_0_3917,plain,
s__Class5_1 = s__Class5_2,
i_0_3864 ).
cnf(c_0_3918,plain,
s__Class5_2 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3915,c_0_3916]) ).
cnf(c_0_3919,plain,
( s__instance(X1,X2)
| ~ s__subclass(X3,X2)
| ~ s__instance(X1,X3)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
i_0_1849 ).
cnf(c_0_3920,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X2,X1) ),
i_0_1795 ).
cnf(c_0_3921,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X2) ),
i_0_1796 ).
cnf(c_0_3922,plain,
s__subclass(s__Lizard5_1,s__Class5_1),
i_0_3874 ).
cnf(c_0_3923,plain,
s__Class5_1 = s__Class5_10,
inference(rw,[status(thm)],[c_0_3917,c_0_3918]) ).
cnf(c_0_3924,plain,
( s__instance(X1,X2)
| ~ s__subclass(X3,X2)
| ~ s__instance(X1,X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_3919,c_0_3920]),c_0_3921]) ).
cnf(c_0_3925,plain,
s__subclass(s__Lizard5_1,s__Class5_10),
inference(rw,[status(thm)],[c_0_3922,c_0_3923]) ).
cnf(c_0_3926,plain,
s__subclass(s__Class5_10,s__Reptile),
i_0_3875 ).
cnf(c_0_3927,plain,
( s__instance(X1,s__Class5_10)
| ~ s__instance(X1,s__Lizard5_1) ),
inference(spm,[status(thm)],[c_0_3924,c_0_3925]) ).
cnf(c_0_3928,plain,
s__instance(s__Organism5_1,s__Lizard5_1),
i_0_3871 ).
cnf(c_0_3929,plain,
s__subclass(s__Reptile,s__ColdBloodedVertebrate),
i_0_3203 ).
cnf(c_0_3930,plain,
( s__instance(X1,s__Reptile)
| ~ s__instance(X1,s__Class5_10) ),
inference(spm,[status(thm)],[c_0_3924,c_0_3926]) ).
cnf(c_0_3931,plain,
s__instance(s__Organism5_1,s__Class5_10),
inference(spm,[status(thm)],[c_0_3927,c_0_3928]) ).
cnf(c_0_3932,plain,
s__subclass(s__ColdBloodedVertebrate,s__Vertebrate),
i_0_3178 ).
cnf(c_0_3933,plain,
( s__instance(X1,s__ColdBloodedVertebrate)
| ~ s__instance(X1,s__Reptile) ),
inference(spm,[status(thm)],[c_0_3924,c_0_3929]) ).
cnf(c_0_3934,plain,
s__instance(s__Organism5_1,s__Reptile),
inference(spm,[status(thm)],[c_0_3930,c_0_3931]) ).
cnf(c_0_3935,plain,
s__subclass(s__Vertebrate,s__Animal),
i_0_3162 ).
cnf(c_0_3936,plain,
( s__instance(X1,s__Vertebrate)
| ~ s__instance(X1,s__ColdBloodedVertebrate) ),
inference(spm,[status(thm)],[c_0_3924,c_0_3932]) ).
cnf(c_0_3937,plain,
s__instance(s__Organism5_1,s__ColdBloodedVertebrate),
inference(spm,[status(thm)],[c_0_3933,c_0_3934]) ).
cnf(c_0_3938,plain,
( s__instance(X1,s__Animal)
| ~ s__instance(X1,s__Vertebrate) ),
inference(spm,[status(thm)],[c_0_3924,c_0_3935]) ).
cnf(c_0_3939,plain,
s__instance(s__Organism5_1,s__Vertebrate),
inference(spm,[status(thm)],[c_0_3936,c_0_3937]) ).
cnf(c_0_3940,negated_conjecture,
~ s__instance(s__Organism5_1,s__Animal),
i_0_3883 ).
cnf(c_0_3941,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3938,c_0_3939]),c_0_3940]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR079+5 : TPTP v8.1.0. Bugfixed v7.3.0.
% 0.07/0.13 % Command : enigmatic-eprover.py %s %d 1
% 0.12/0.34 % Computer : n007.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Sat Jun 11 12:11:24 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected SinE mode:
% 0.58/0.77 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.58/0.77 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.58/0.77 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.58/0.77 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 14.14/4.72 # ENIGMATIC: Solved by autoschedule-lgb:
% 14.14/4.72 # SinE strategy is gf600_h_gu_R05_F100_L20000
% 14.14/4.72 # Trying AutoSched0 for 149 seconds
% 14.14/4.72 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_S4d
% 14.14/4.72 # and selection function SelectCQIPrecWNTNp.
% 14.14/4.72 #
% 14.14/4.72 # Preprocessing time : 0.029 s
% 14.14/4.72 # Presaturation interreduction done
% 14.14/4.72
% 14.14/4.72 # Proof found!
% 14.14/4.72 # SZS status Theorem
% 14.14/4.72 # SZS output start CNFRefutation
% See solution above
% 14.14/4.72 # Training examples: 0 positive, 0 negative
% 14.14/4.72
% 14.14/4.72 # -------------------------------------------------
% 14.14/4.72 # User time : 0.363 s
% 14.14/4.72 # System time : 0.028 s
% 14.14/4.72 # Total time : 0.391 s
% 14.14/4.72 # Maximum resident set size: 7120 pages
% 14.14/4.72
%------------------------------------------------------------------------------