%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : CSR084+5 : TPTP v8.1.0. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n015.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:38 EDT 2022
% Result : Theorem 20.10s 5.26s
% Output : CNFRefutation 20.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 21
% Syntax : Number of clauses : 83 ( 46 unt; 3 nHn; 83 RR)
% Number of literals : 169 ( 0 equ; 87 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 12 con; 0-1 aty)
% Number of variables : 60 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_1138,plain,
( s__subclass(X1,X2)
| ~ s__subclass(X1,X3)
| ~ s__subclass(X3,X2)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_1138) ).
cnf(i_0_1759,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_1759) ).
cnf(i_0_1758,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X2,X1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_1758) ).
cnf(i_0_3005,plain,
s__subclass(s__Animal,s__Organism),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3005) ).
cnf(i_0_2996,plain,
s__subclass(s__Organism,s__Agent),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_2996) ).
cnf(i_0_3013,plain,
s__subclass(s__Vertebrate,s__Animal),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3013) ).
cnf(i_0_3015,plain,
s__subclass(s__Invertebrate,s__Animal),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3015) ).
cnf(i_0_3323,plain,
s__subclass(s__Agent,s__Object),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3323) ).
cnf(i_0_2762,plain,
s__subclass(s__Object,s__Physical),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_2762) ).
cnf(i_0_1811,plain,
( s__instance(X1,X2)
| ~ s__instance(X1,X3)
| ~ s__subclass(X3,X2)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_1811) ).
cnf(i_0_2736,plain,
s__subclass(s__Physical,s__Entity),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_2736) ).
cnf(i_0_2731,plain,
( s__instance(X1,s__Class)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,s__Entity) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_2731) ).
cnf(i_0_3484,plain,
s__instance(s__BananaSlug10_1,s__Animal),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3484) ).
cnf(i_0_3482,plain,
( s__partition_3(X1,X2,X3)
| ~ s__instance(X2,s__Class)
| ~ s__instance(X3,s__Class)
| ~ s__instance(X1,s__Class)
| ~ s__partition_3(X1,X3,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3482) ).
cnf(i_0_3481,plain,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3481) ).
cnf(i_0_3483,plain,
( s__instance(X1,X2)
| s__instance(X1,X3)
| ~ s__instance(X1,X4)
| ~ s__instance(X2,s__Class)
| ~ s__instance(X3,s__Class)
| ~ s__instance(X4,s__Class)
| ~ s__partition_3(X4,X3,X2) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3483) ).
cnf(i_0_3477,plain,
( s__part(esk444_1(X1),X1)
| ~ s__instance(X1,s__Animal)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__Vertebrate) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3477) ).
cnf(i_0_3487,negated_conjecture,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3487) ).
cnf(i_0_3479,plain,
( s__instance(esk444_1(X1),s__Object)
| ~ s__instance(X1,s__Animal)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__Vertebrate) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3479) ).
cnf(i_0_3478,plain,
( s__instance(esk444_1(X1),s__SpinalColumn)
| ~ s__instance(X1,s__Animal)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__Vertebrate) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3478) ).
cnf(i_0_3480,plain,
( ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__SpinalColumn)
| ~ s__part(X1,s__BananaSlug10_1) ),
file('/export/starexec/sandbox2/tmp/enigma-theBenchmark.p-z9lc4bzn/lgb.p',i_0_3480) ).
cnf(c_0_3509,plain,
( s__subclass(X1,X2)
| ~ s__subclass(X1,X3)
| ~ s__subclass(X3,X2)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
i_0_1138 ).
cnf(c_0_3510,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,X2) ),
i_0_1759 ).
cnf(c_0_3511,plain,
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X2,X1) ),
i_0_1758 ).
cnf(c_0_3512,plain,
( s__subclass(X1,X2)
| ~ s__subclass(X3,X2)
| ~ s__subclass(X1,X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_3509,c_0_3510]),c_0_3511]),c_0_3510]) ).
cnf(c_0_3513,plain,
s__subclass(s__Animal,s__Organism),
i_0_3005 ).
cnf(c_0_3514,plain,
s__subclass(s__Organism,s__Agent),
i_0_2996 ).
cnf(c_0_3515,plain,
( s__subclass(X1,s__Organism)
| ~ s__subclass(X1,s__Animal) ),
inference(spm,[status(thm)],[c_0_3512,c_0_3513]) ).
cnf(c_0_3516,plain,
s__subclass(s__Vertebrate,s__Animal),
i_0_3013 ).
cnf(c_0_3517,plain,
s__subclass(s__Invertebrate,s__Animal),
i_0_3015 ).
cnf(c_0_3518,plain,
s__subclass(s__Agent,s__Object),
i_0_3323 ).
cnf(c_0_3519,plain,
( s__subclass(X1,s__Agent)
| ~ s__subclass(X1,s__Organism) ),
inference(spm,[status(thm)],[c_0_3512,c_0_3514]) ).
cnf(c_0_3520,plain,
s__subclass(s__Vertebrate,s__Organism),
inference(spm,[status(thm)],[c_0_3515,c_0_3516]) ).
cnf(c_0_3521,plain,
s__subclass(s__Invertebrate,s__Organism),
inference(spm,[status(thm)],[c_0_3515,c_0_3517]) ).
cnf(c_0_3522,plain,
s__subclass(s__Object,s__Physical),
i_0_2762 ).
cnf(c_0_3523,plain,
( s__subclass(X1,s__Object)
| ~ s__subclass(X1,s__Agent) ),
inference(spm,[status(thm)],[c_0_3512,c_0_3518]) ).
cnf(c_0_3524,plain,
s__subclass(s__Vertebrate,s__Agent),
inference(spm,[status(thm)],[c_0_3519,c_0_3520]) ).
cnf(c_0_3525,plain,
s__subclass(s__Invertebrate,s__Agent),
inference(spm,[status(thm)],[c_0_3519,c_0_3521]) ).
cnf(c_0_3526,plain,
s__subclass(s__Animal,s__Agent),
inference(spm,[status(thm)],[c_0_3519,c_0_3513]) ).
cnf(c_0_3527,plain,
( s__instance(X1,X2)
| ~ s__instance(X1,X3)
| ~ s__subclass(X3,X2)
| ~ s__instance(X3,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass) ),
i_0_1811 ).
cnf(c_0_3528,plain,
s__subclass(s__Physical,s__Entity),
i_0_2736 ).
cnf(c_0_3529,plain,
( s__subclass(X1,s__Physical)
| ~ s__subclass(X1,s__Object) ),
inference(spm,[status(thm)],[c_0_3512,c_0_3522]) ).
cnf(c_0_3530,plain,
s__subclass(s__Vertebrate,s__Object),
inference(spm,[status(thm)],[c_0_3523,c_0_3524]) ).
cnf(c_0_3531,plain,
s__subclass(s__Invertebrate,s__Object),
inference(spm,[status(thm)],[c_0_3523,c_0_3525]) ).
cnf(c_0_3532,plain,
s__subclass(s__Animal,s__Object),
inference(spm,[status(thm)],[c_0_3523,c_0_3526]) ).
cnf(c_0_3533,plain,
( s__instance(X1,X2)
| ~ s__subclass(X3,X2)
| ~ s__instance(X1,X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_3527,c_0_3511]),c_0_3510]) ).
cnf(c_0_3534,plain,
( s__instance(X1,s__Class)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__subclass(X1,s__Entity) ),
i_0_2731 ).
cnf(c_0_3535,plain,
( s__subclass(X1,s__Entity)
| ~ s__subclass(X1,s__Physical) ),
inference(spm,[status(thm)],[c_0_3512,c_0_3528]) ).
cnf(c_0_3536,plain,
s__subclass(s__Vertebrate,s__Physical),
inference(spm,[status(thm)],[c_0_3529,c_0_3530]) ).
cnf(c_0_3537,plain,
s__subclass(s__Invertebrate,s__Physical),
inference(spm,[status(thm)],[c_0_3529,c_0_3531]) ).
cnf(c_0_3538,plain,
s__subclass(s__Animal,s__Physical),
inference(spm,[status(thm)],[c_0_3529,c_0_3532]) ).
cnf(c_0_3539,plain,
( s__instance(X1,s__Organism)
| ~ s__instance(X1,s__Animal) ),
inference(spm,[status(thm)],[c_0_3533,c_0_3513]) ).
cnf(c_0_3540,plain,
s__instance(s__BananaSlug10_1,s__Animal),
i_0_3484 ).
cnf(c_0_3541,plain,
( s__instance(X1,s__Class)
| ~ s__subclass(X1,s__Entity) ),
inference(csr,[status(thm)],[c_0_3534,c_0_3510]) ).
cnf(c_0_3542,plain,
s__subclass(s__Vertebrate,s__Entity),
inference(spm,[status(thm)],[c_0_3535,c_0_3536]) ).
cnf(c_0_3543,plain,
s__subclass(s__Invertebrate,s__Entity),
inference(spm,[status(thm)],[c_0_3535,c_0_3537]) ).
cnf(c_0_3544,plain,
s__subclass(s__Animal,s__Entity),
inference(spm,[status(thm)],[c_0_3535,c_0_3538]) ).
cnf(c_0_3545,plain,
( s__instance(X1,s__Agent)
| ~ s__instance(X1,s__Organism) ),
inference(spm,[status(thm)],[c_0_3533,c_0_3514]) ).
cnf(c_0_3546,plain,
s__instance(s__BananaSlug10_1,s__Organism),
inference(spm,[status(thm)],[c_0_3539,c_0_3540]) ).
cnf(c_0_3547,plain,
( s__partition_3(X1,X2,X3)
| ~ s__instance(X2,s__Class)
| ~ s__instance(X3,s__Class)
| ~ s__instance(X1,s__Class)
| ~ s__partition_3(X1,X3,X2) ),
i_0_3482 ).
cnf(c_0_3548,plain,
s__partition_3(s__Animal,s__Vertebrate,s__Invertebrate),
i_0_3481 ).
cnf(c_0_3549,plain,
s__instance(s__Vertebrate,s__Class),
inference(spm,[status(thm)],[c_0_3541,c_0_3542]) ).
cnf(c_0_3550,plain,
s__instance(s__Invertebrate,s__Class),
inference(spm,[status(thm)],[c_0_3541,c_0_3543]) ).
cnf(c_0_3551,plain,
s__instance(s__Animal,s__Class),
inference(spm,[status(thm)],[c_0_3541,c_0_3544]) ).
cnf(c_0_3552,plain,
( s__instance(X1,s__Object)
| ~ s__instance(X1,s__Agent) ),
inference(spm,[status(thm)],[c_0_3533,c_0_3518]) ).
cnf(c_0_3553,plain,
s__instance(s__BananaSlug10_1,s__Agent),
inference(spm,[status(thm)],[c_0_3545,c_0_3546]) ).
cnf(c_0_3554,plain,
( s__instance(X1,X2)
| s__instance(X1,X3)
| ~ s__instance(X1,X4)
| ~ s__instance(X2,s__Class)
| ~ s__instance(X3,s__Class)
| ~ s__instance(X4,s__Class)
| ~ s__partition_3(X4,X3,X2) ),
i_0_3483 ).
cnf(c_0_3555,plain,
s__partition_3(s__Animal,s__Invertebrate,s__Vertebrate),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3547,c_0_3548]),c_0_3549]),c_0_3550]),c_0_3551])]) ).
cnf(c_0_3556,plain,
( s__part(esk444_1(X1),X1)
| ~ s__instance(X1,s__Animal)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__Vertebrate) ),
i_0_3477 ).
cnf(c_0_3557,plain,
s__instance(s__BananaSlug10_1,s__Object),
inference(spm,[status(thm)],[c_0_3552,c_0_3553]) ).
cnf(c_0_3558,plain,
( s__instance(X1,s__Vertebrate)
| s__instance(X1,s__Invertebrate)
| ~ s__instance(X1,s__Animal) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3554,c_0_3555]),c_0_3551]),c_0_3550]),c_0_3549])]) ).
cnf(c_0_3559,negated_conjecture,
~ s__instance(s__BananaSlug10_1,s__Invertebrate),
i_0_3487 ).
cnf(c_0_3560,plain,
( s__instance(esk444_1(X1),s__Object)
| ~ s__instance(X1,s__Animal)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__Vertebrate) ),
i_0_3479 ).
cnf(c_0_3561,plain,
( s__instance(esk444_1(X1),s__SpinalColumn)
| ~ s__instance(X1,s__Animal)
| ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__Vertebrate) ),
i_0_3478 ).
cnf(c_0_3562,plain,
( s__part(esk444_1(s__BananaSlug10_1),s__BananaSlug10_1)
| ~ s__instance(s__BananaSlug10_1,s__Vertebrate) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3556,c_0_3557]),c_0_3540])]) ).
cnf(c_0_3563,plain,
s__instance(s__BananaSlug10_1,s__Vertebrate),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_3558,c_0_3540]),c_0_3559]) ).
cnf(c_0_3564,plain,
( s__instance(esk444_1(s__BananaSlug10_1),s__Object)
| ~ s__instance(s__BananaSlug10_1,s__Vertebrate) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3560,c_0_3557]),c_0_3540])]) ).
cnf(c_0_3565,plain,
( s__instance(esk444_1(s__BananaSlug10_1),s__SpinalColumn)
| ~ s__instance(s__BananaSlug10_1,s__Vertebrate) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3561,c_0_3557]),c_0_3540])]) ).
cnf(c_0_3566,plain,
( ~ s__instance(X1,s__Object)
| ~ s__instance(X1,s__SpinalColumn)
| ~ s__part(X1,s__BananaSlug10_1) ),
i_0_3480 ).
cnf(c_0_3567,plain,
s__part(esk444_1(s__BananaSlug10_1),s__BananaSlug10_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3562,c_0_3563])]) ).
cnf(c_0_3568,plain,
s__instance(esk444_1(s__BananaSlug10_1),s__Object),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3564,c_0_3563])]) ).
cnf(c_0_3569,plain,
s__instance(esk444_1(s__BananaSlug10_1),s__SpinalColumn),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_3565,c_0_3563])]) ).
cnf(c_0_3570,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_3566,c_0_3567]),c_0_3568]),c_0_3569])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR084+5 : TPTP v8.1.0. Bugfixed v7.3.0.
% 0.11/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.13/0.33 % Computer : n015.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 : Sat Jun 11 01:47:21 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.45 # ENIGMATIC: Selected SinE mode:
% 0.60/0.80 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.60/0.80 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.60/0.80 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.60/0.80 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 20.10/5.26 # ENIGMATIC: Solved by autoschedule-lgb:
% 20.10/5.26 # SinE strategy is gf600_h_gu_R05_F100_L20000
% 20.10/5.26 # Trying AutoSched0 for 150 seconds
% 20.10/5.26 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S5PRR_S4d
% 20.10/5.26 # and selection function SelectCQIPrecWNTNp.
% 20.10/5.26 #
% 20.10/5.26 # Preprocessing time : 0.039 s
% 20.10/5.26 # Presaturation interreduction done
% 20.10/5.26
% 20.10/5.26 # Proof found!
% 20.10/5.26 # SZS status Theorem
% 20.10/5.26 # SZS output start CNFRefutation
% See solution above
% 20.10/5.26 # Training examples: 0 positive, 0 negative
% 20.10/5.26
% 20.10/5.26 # -------------------------------------------------
% 20.10/5.26 # User time : 1.413 s
% 20.10/5.26 # System time : 0.035 s
% 20.10/5.26 # Total time : 1.448 s
% 20.10/5.26 # Maximum resident set size: 7124 pages
% 20.10/5.26
%------------------------------------------------------------------------------