%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : CSR061+5 : TPTP v8.1.0. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n020.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:14 EDT 2022
% Result : Theorem 17.15s 11.71s
% Output : CNFRefutation 17.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 20
% Syntax : Number of clauses : 76 ( 56 unt; 0 nHn; 76 RR)
% Number of literals : 98 ( 0 equ; 24 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 18 con; 0-0 aty)
% Number of variables : 26 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(i_0_2548,plain,
( disjointwith(X1,X2)
| ~ genls(X1,X3)
| ~ disjointwith(X3,X2) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_2548) ).
cnf(i_0_365,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_365) ).
cnf(i_0_2546,plain,
( disjointwith(X1,X2)
| ~ disjointwith(X2,X1) ),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_2546) ).
cnf(i_0_451,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_451) ).
cnf(i_0_1713,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_1713) ).
cnf(i_0_1757,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_1757) ).
cnf(i_0_976,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_976) ).
cnf(i_0_712,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_712) ).
cnf(i_0_978,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_978) ).
cnf(i_0_1246,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_1246) ).
cnf(i_0_335,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_335) ).
cnf(i_0_909,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_909) ).
cnf(i_0_2610,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_2610) ).
cnf(i_0_2667,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_2667) ).
cnf(i_0_60,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_60) ).
cnf(i_0_314,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_314) ).
cnf(i_0_2613,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_2613) ).
cnf(i_0_1721,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_1721) ).
cnf(i_0_786,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_786) ).
cnf(i_0_2955,negated_conjecture,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
file('/export/starexec/sandbox/tmp/enigma-theBenchmark.p-sp8bb_gf/lgb.p',i_0_2955) ).
cnf(c_0_2976,plain,
( disjointwith(X1,X2)
| ~ genls(X1,X3)
| ~ disjointwith(X3,X2) ),
i_0_2548 ).
cnf(c_0_2977,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
i_0_365 ).
cnf(c_0_2978,plain,
( disjointwith(X1,X2)
| ~ disjointwith(X2,X1) ),
i_0_2546 ).
cnf(c_0_2979,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
i_0_451 ).
cnf(c_0_2980,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
i_0_1713 ).
cnf(c_0_2981,plain,
( disjointwith(c_tptpcol_4_114689,X1)
| ~ disjointwith(c_tptpcol_3_114688,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_2977]) ).
cnf(c_0_2982,plain,
disjointwith(c_tptpcol_3_114688,c_tptpcol_3_98305),
inference(spm,[status(thm)],[c_0_2978,c_0_2979]) ).
cnf(c_0_2983,plain,
( disjointwith(c_tptpcol_5_114690,X1)
| ~ disjointwith(c_tptpcol_4_114689,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_2980]) ).
cnf(c_0_2984,plain,
disjointwith(c_tptpcol_4_114689,c_tptpcol_3_98305),
inference(spm,[status(thm)],[c_0_2981,c_0_2982]) ).
cnf(c_0_2985,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
i_0_1757 ).
cnf(c_0_2986,plain,
disjointwith(c_tptpcol_5_114690,c_tptpcol_3_98305),
inference(spm,[status(thm)],[c_0_2983,c_0_2984]) ).
cnf(c_0_2987,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
i_0_976 ).
cnf(c_0_2988,plain,
( disjointwith(c_tptpcol_4_106497,X1)
| ~ disjointwith(c_tptpcol_3_98305,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_2985]) ).
cnf(c_0_2989,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_5_114690),
inference(spm,[status(thm)],[c_0_2978,c_0_2986]) ).
cnf(c_0_2990,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
i_0_712 ).
cnf(c_0_2991,plain,
( disjointwith(c_tptpcol_5_110593,X1)
| ~ disjointwith(c_tptpcol_4_106497,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_2987]) ).
cnf(c_0_2992,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_5_114690),
inference(spm,[status(thm)],[c_0_2988,c_0_2989]) ).
cnf(c_0_2993,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
i_0_978 ).
cnf(c_0_2994,plain,
( disjointwith(c_tptpcol_6_112641,X1)
| ~ disjointwith(c_tptpcol_5_110593,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_2990]) ).
cnf(c_0_2995,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_5_114690),
inference(spm,[status(thm)],[c_0_2991,c_0_2992]) ).
cnf(c_0_2996,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
i_0_1246 ).
cnf(c_0_2997,plain,
( disjointwith(c_tptpcol_7_113665,X1)
| ~ disjointwith(c_tptpcol_6_112641,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_2993]) ).
cnf(c_0_2998,plain,
disjointwith(c_tptpcol_6_112641,c_tptpcol_5_114690),
inference(spm,[status(thm)],[c_0_2994,c_0_2995]) ).
cnf(c_0_2999,plain,
( disjointwith(c_tptpcol_8_114177,X1)
| ~ disjointwith(c_tptpcol_7_113665,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_2996]) ).
cnf(c_0_3000,plain,
disjointwith(c_tptpcol_7_113665,c_tptpcol_5_114690),
inference(spm,[status(thm)],[c_0_2997,c_0_2998]) ).
cnf(c_0_3001,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
i_0_335 ).
cnf(c_0_3002,plain,
disjointwith(c_tptpcol_8_114177,c_tptpcol_5_114690),
inference(spm,[status(thm)],[c_0_2999,c_0_3000]) ).
cnf(c_0_3003,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
i_0_909 ).
cnf(c_0_3004,plain,
( disjointwith(c_tptpcol_6_116738,X1)
| ~ disjointwith(c_tptpcol_5_114690,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3001]) ).
cnf(c_0_3005,plain,
disjointwith(c_tptpcol_5_114690,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_2978,c_0_3002]) ).
cnf(c_0_3006,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
i_0_2610 ).
cnf(c_0_3007,plain,
( disjointwith(c_tptpcol_7_117762,X1)
| ~ disjointwith(c_tptpcol_6_116738,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3003]) ).
cnf(c_0_3008,plain,
disjointwith(c_tptpcol_6_116738,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3004,c_0_3005]) ).
cnf(c_0_3009,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
i_0_2667 ).
cnf(c_0_3010,plain,
( disjointwith(c_tptpcol_8_117763,X1)
| ~ disjointwith(c_tptpcol_7_117762,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3006]) ).
cnf(c_0_3011,plain,
disjointwith(c_tptpcol_7_117762,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3007,c_0_3008]) ).
cnf(c_0_3012,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
i_0_60 ).
cnf(c_0_3013,plain,
( disjointwith(c_tptpcol_9_118019,X1)
| ~ disjointwith(c_tptpcol_8_117763,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3009]) ).
cnf(c_0_3014,plain,
disjointwith(c_tptpcol_8_117763,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3010,c_0_3011]) ).
cnf(c_0_3015,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
i_0_314 ).
cnf(c_0_3016,plain,
( disjointwith(c_tptpcol_10_118020,X1)
| ~ disjointwith(c_tptpcol_9_118019,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3012]) ).
cnf(c_0_3017,plain,
disjointwith(c_tptpcol_9_118019,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3013,c_0_3014]) ).
cnf(c_0_3018,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
i_0_2613 ).
cnf(c_0_3019,plain,
( disjointwith(c_tptpcol_11_118084,X1)
| ~ disjointwith(c_tptpcol_10_118020,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3015]) ).
cnf(c_0_3020,plain,
disjointwith(c_tptpcol_10_118020,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3016,c_0_3017]) ).
cnf(c_0_3021,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
i_0_1721 ).
cnf(c_0_3022,plain,
( disjointwith(c_tptpcol_12_118116,X1)
| ~ disjointwith(c_tptpcol_11_118084,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3018]) ).
cnf(c_0_3023,plain,
disjointwith(c_tptpcol_11_118084,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3019,c_0_3020]) ).
cnf(c_0_3024,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
i_0_786 ).
cnf(c_0_3025,plain,
( disjointwith(c_tptpcol_13_118117,X1)
| ~ disjointwith(c_tptpcol_12_118116,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3021]) ).
cnf(c_0_3026,plain,
disjointwith(c_tptpcol_12_118116,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3022,c_0_3023]) ).
cnf(c_0_3027,plain,
( disjointwith(c_tptpcol_14_118118,X1)
| ~ disjointwith(c_tptpcol_13_118117,X1) ),
inference(spm,[status(thm)],[c_0_2976,c_0_3024]) ).
cnf(c_0_3028,plain,
disjointwith(c_tptpcol_13_118117,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3025,c_0_3026]) ).
cnf(c_0_3029,plain,
disjointwith(c_tptpcol_14_118118,c_tptpcol_8_114177),
inference(spm,[status(thm)],[c_0_3027,c_0_3028]) ).
cnf(c_0_3030,negated_conjecture,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
i_0_2955 ).
cnf(c_0_3031,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_2978,c_0_3029]),c_0_3030]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR061+5 : TPTP v8.1.0. Bugfixed v3.5.0.
% 0.03/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.11/0.33 % Computer : n020.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Fri Jun 10 13:15:07 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.19/0.44 # ENIGMATIC: Selected SinE mode:
% 8.56/8.78 # Parsing /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.56/8.78 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 8.56/8.78 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 8.56/8.78 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 17.15/11.71 # ENIGMATIC: Solved by autoschedule-lgb:
% 17.15/11.71 # No SInE strategy applied
% 17.15/11.71 # Trying AutoSched0 for 146 seconds
% 17.15/11.71 # AutoSched0-Mode selected heuristic G_E___208_C18_F1_SE_CS_SP_PS_S064N
% 17.15/11.71 # and selection function SelectComplexG.
% 17.15/11.71 #
% 17.15/11.71 # Preprocessing time : 0.029 s
% 17.15/11.71 # Presaturation interreduction done
% 17.15/11.71
% 17.15/11.71 # Proof found!
% 17.15/11.71 # SZS status Theorem
% 17.15/11.71 # SZS output start CNFRefutation
% See solution above
% 17.15/11.71 # Training examples: 0 positive, 0 negative
% 17.15/11.71
% 17.15/11.71 # -------------------------------------------------
% 17.15/11.71 # User time : 0.064 s
% 17.15/11.71 # System time : 0.012 s
% 17.15/11.71 # Total time : 0.076 s
% 17.15/11.71 # Maximum resident set size: 7132 pages
% 17.15/11.71
%------------------------------------------------------------------------------