%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : GEO354+1 : TPTP v8.1.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n029.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 : Sat Jul 16 03:45:27 EDT 2022
% Result : Satisfiable 5.45s 2.06s
% Output : Saturation 5.45s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(cld5,axiom,
! [X2,X3,X6] :
( ~ unequally_directed_lines(X2,reverse_line(X3))
& ( ~ unequally_directed_lines(X2,reverse_line(X6))
=> ~ unequally_directed_lines(X3,X6) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+1.ax',cld5) ).
fof(oag8,axiom,
! [X2,X3] :
( ( line(X2)
& line(X3) )
=> ( unequally_directed_lines(X2,X3)
| unequally_directed_lines(X2,reverse_line(X3)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag8) ).
fof(oagco3,axiom,
! [X2,X1] :
( ( point(X1)
& line(X2) )
=> line(parallel_through_point(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oagco3) ).
fof(oagco1,axiom,
! [X1,X4] :
( ( point(X1)
& point(X4)
& distinct_points(X1,X4) )
=> line(line_connecting(X1,X4)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oagco1) ).
fof(bf_def,axiom,
! [X2,X1,X4] :
( before_on_line(X2,X1,X4)
<=> ( distinct_points(X1,X4)
& ~ ( left_apart_point(X1,X2)
| left_apart_point(X1,reverse_line(X2)) )
& ~ ( left_apart_point(X4,X2)
| left_apart_point(X4,reverse_line(X2)) )
& ~ unequally_directed_lines(X2,line_connecting(X1,X4)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',bf_def) ).
fof(oag10,axiom,
! [X1,X2] :
~ ( left_apart_point(X1,X2)
| left_apart_point(X1,reverse_line(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag10) ).
fof(oaguc1,axiom,
! [X1,X4,X2,X3] :
( ( distinct_points(X1,X4)
& distinct_lines(X2,X3) )
=> ( left_apart_point(X1,X2)
| left_apart_point(X4,X2)
| left_apart_point(X1,X3)
| left_apart_point(X4,X3)
| left_apart_point(X1,reverse_line(X2))
| left_apart_point(X4,reverse_line(X2))
| left_apart_point(X1,reverse_line(X3))
| left_apart_point(X4,reverse_line(X3)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oaguc1) ).
fof(div_def,axiom,
! [X1,X4,X2] :
( divides_points(X2,X1,X4)
<=> ( ( left_apart_point(X1,X2)
& left_apart_point(X4,reverse_line(X2)) )
| ( left_apart_point(X1,reverse_line(X2))
& left_apart_point(X4,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',div_def) ).
fof(apt_def,axiom,
! [X1,X2] :
( apart_point_and_line(X1,X2)
<=> ( left_apart_point(X1,X2)
| left_apart_point(X1,reverse_line(X2)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',apt_def) ).
fof(con_def,axiom,
! [X2,X3] :
( convergent_lines(X2,X3)
<=> ( unequally_directed_lines(X2,X3)
& unequally_directed_lines(X2,reverse_line(X3)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',con_def) ).
fof(bet_def,axiom,
! [X2,X1,X4,X5] :
( between_on_line(X2,X1,X4,X5)
<=> ( ( before_on_line(X2,X1,X4)
& before_on_line(X2,X4,X5) )
| ( before_on_line(X2,X5,X4)
& before_on_line(X2,X4,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',bet_def) ).
fof(oag4,axiom,
! [X2,X3,X6] :
( distinct_lines(X2,X3)
=> ( distinct_lines(X2,X6)
| distinct_lines(X3,X6) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag4) ).
fof(oag2,axiom,
! [X1,X4,X5] :
( distinct_points(X1,X4)
=> ( distinct_points(X1,X5)
| distinct_points(X4,X5) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag2) ).
fof(oagco4,axiom,
! [X2] :
( line(X2)
=> line(reverse_line(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oagco4) ).
fof(oagco8,axiom,
! [X2] : ~ distinct_lines(X2,reverse_line(X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oagco8) ).
fof(oag11,axiom,
! [X2,X3] :
~ ( left_convergent_lines(X2,X3)
| left_convergent_lines(X2,reverse_line(X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag11) ).
fof(oag3,axiom,
! [X2] : ~ distinct_lines(X2,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag3) ).
fof(oag1,axiom,
! [X1] : ~ distinct_points(X1,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag1) ).
fof(oag5,axiom,
! [X2] : ~ unequally_directed_lines(X2,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO007+0.ax',oag5) ).
fof(c_0_19,plain,
! [X89,X90,X91] :
( ~ unequally_directed_lines(X89,reverse_line(X90))
& ( unequally_directed_lines(X89,reverse_line(X91))
| ~ unequally_directed_lines(X90,X91) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[cld5])])]) ).
fof(c_0_20,plain,
! [X36,X37] :
( ~ line(X36)
| ~ line(X37)
| unequally_directed_lines(X36,X37)
| unequally_directed_lines(X36,reverse_line(X37)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag8])]) ).
cnf(c_0_21,plain,
( unequally_directed_lines(X1,reverse_line(X2))
| ~ unequally_directed_lines(X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_22,plain,
~ unequally_directed_lines(X1,reverse_line(X2)),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_23,plain,
! [X48,X49] :
( ~ point(X49)
| ~ line(X48)
| line(parallel_through_point(X48,X49)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagco3])]) ).
cnf(c_0_24,plain,
( unequally_directed_lines(X1,X2)
| unequally_directed_lines(X1,reverse_line(X2))
| ~ line(X1)
| ~ line(X2) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_25,plain,
~ unequally_directed_lines(X1,X2),
inference(sr,[status(thm)],[c_0_21,c_0_22]),
[final] ).
fof(c_0_26,plain,
! [X44,X45] :
( ~ point(X44)
| ~ point(X45)
| ~ distinct_points(X44,X45)
| line(line_connecting(X44,X45)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagco1])]) ).
cnf(c_0_27,plain,
( line(parallel_through_point(X2,X1))
| ~ point(X1)
| ~ line(X2) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_28,plain,
( ~ line(X1)
| ~ line(X2) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_24,c_0_25]),c_0_22]),
[final] ).
fof(c_0_29,plain,
! [X14,X15,X16] :
( ( distinct_points(X15,X16)
| ~ before_on_line(X14,X15,X16) )
& ( ~ left_apart_point(X15,X14)
| ~ before_on_line(X14,X15,X16) )
& ( ~ left_apart_point(X15,reverse_line(X14))
| ~ before_on_line(X14,X15,X16) )
& ( ~ left_apart_point(X16,X14)
| ~ before_on_line(X14,X15,X16) )
& ( ~ left_apart_point(X16,reverse_line(X14))
| ~ before_on_line(X14,X15,X16) )
& ( ~ unequally_directed_lines(X14,line_connecting(X15,X16))
| ~ before_on_line(X14,X15,X16) )
& ( ~ distinct_points(X15,X16)
| left_apart_point(X15,X14)
| left_apart_point(X15,reverse_line(X14))
| left_apart_point(X16,X14)
| left_apart_point(X16,reverse_line(X14))
| unequally_directed_lines(X14,line_connecting(X15,X16))
| before_on_line(X14,X15,X16) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[bf_def])])])]) ).
fof(c_0_30,plain,
! [X40,X41] :
( ~ left_apart_point(X40,X41)
& ~ left_apart_point(X40,reverse_line(X41)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag10])]) ).
fof(c_0_31,plain,
! [X62,X63,X64,X65] :
( ~ distinct_points(X62,X63)
| ~ distinct_lines(X64,X65)
| left_apart_point(X62,X64)
| left_apart_point(X63,X64)
| left_apart_point(X62,X65)
| left_apart_point(X63,X65)
| left_apart_point(X62,reverse_line(X64))
| left_apart_point(X63,reverse_line(X64))
| left_apart_point(X62,reverse_line(X65))
| left_apart_point(X63,reverse_line(X65)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oaguc1])]) ).
fof(c_0_32,plain,
! [X11,X12,X13] :
( ( left_apart_point(X11,reverse_line(X13))
| left_apart_point(X11,X13)
| ~ divides_points(X13,X11,X12) )
& ( left_apart_point(X12,X13)
| left_apart_point(X11,X13)
| ~ divides_points(X13,X11,X12) )
& ( left_apart_point(X11,reverse_line(X13))
| left_apart_point(X12,reverse_line(X13))
| ~ divides_points(X13,X11,X12) )
& ( left_apart_point(X12,X13)
| left_apart_point(X12,reverse_line(X13))
| ~ divides_points(X13,X11,X12) )
& ( ~ left_apart_point(X11,X13)
| ~ left_apart_point(X12,reverse_line(X13))
| divides_points(X13,X11,X12) )
& ( ~ left_apart_point(X11,reverse_line(X13))
| ~ left_apart_point(X12,X13)
| divides_points(X13,X11,X12) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[div_def])])]) ).
fof(c_0_33,plain,
! [X7,X8] :
( ( ~ apart_point_and_line(X7,X8)
| left_apart_point(X7,X8)
| left_apart_point(X7,reverse_line(X8)) )
& ( ~ left_apart_point(X7,X8)
| apart_point_and_line(X7,X8) )
& ( ~ left_apart_point(X7,reverse_line(X8))
| apart_point_and_line(X7,X8) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[apt_def])])]) ).
fof(c_0_34,plain,
! [X9,X10] :
( ( unequally_directed_lines(X9,X10)
| ~ convergent_lines(X9,X10) )
& ( unequally_directed_lines(X9,reverse_line(X10))
| ~ convergent_lines(X9,X10) )
& ( ~ unequally_directed_lines(X9,X10)
| ~ unequally_directed_lines(X9,reverse_line(X10))
| convergent_lines(X9,X10) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[con_def])])]) ).
fof(c_0_35,plain,
! [X17,X18,X19,X20] :
( ( before_on_line(X17,X20,X19)
| before_on_line(X17,X18,X19)
| ~ between_on_line(X17,X18,X19,X20) )
& ( before_on_line(X17,X19,X18)
| before_on_line(X17,X18,X19)
| ~ between_on_line(X17,X18,X19,X20) )
& ( before_on_line(X17,X20,X19)
| before_on_line(X17,X19,X20)
| ~ between_on_line(X17,X18,X19,X20) )
& ( before_on_line(X17,X19,X18)
| before_on_line(X17,X19,X20)
| ~ between_on_line(X17,X18,X19,X20) )
& ( ~ before_on_line(X17,X18,X19)
| ~ before_on_line(X17,X19,X20)
| between_on_line(X17,X18,X19,X20) )
& ( ~ before_on_line(X17,X20,X19)
| ~ before_on_line(X17,X19,X18)
| between_on_line(X17,X18,X19,X20) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[bet_def])])]) ).
fof(c_0_36,plain,
! [X26,X27,X28] :
( ~ distinct_lines(X26,X27)
| distinct_lines(X26,X28)
| distinct_lines(X27,X28) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag4])]) ).
fof(c_0_37,plain,
! [X22,X23,X24] :
( ~ distinct_points(X22,X23)
| distinct_points(X22,X24)
| distinct_points(X23,X24) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag2])]) ).
cnf(c_0_38,plain,
( line(line_connecting(X1,X2))
| ~ point(X1)
| ~ point(X2)
| ~ distinct_points(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_39,plain,
( ~ point(X1)
| ~ line(X2) ),
inference(csr,[status(thm)],[c_0_27,c_0_28]),
[final] ).
cnf(c_0_40,plain,
( left_apart_point(X1,X3)
| left_apart_point(X1,reverse_line(X3))
| left_apart_point(X2,X3)
| left_apart_point(X2,reverse_line(X3))
| unequally_directed_lines(X3,line_connecting(X1,X2))
| before_on_line(X3,X1,X2)
| ~ distinct_points(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_41,plain,
~ left_apart_point(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_30]),
[final] ).
cnf(c_0_42,plain,
( left_apart_point(X1,X3)
| left_apart_point(X2,X3)
| left_apart_point(X1,X4)
| left_apart_point(X2,X4)
| left_apart_point(X1,reverse_line(X3))
| left_apart_point(X2,reverse_line(X3))
| left_apart_point(X1,reverse_line(X4))
| left_apart_point(X2,reverse_line(X4))
| ~ distinct_points(X1,X2)
| ~ distinct_lines(X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
fof(c_0_43,plain,
! [X50] :
( ~ line(X50)
| line(reverse_line(X50)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oagco4])]) ).
cnf(c_0_44,plain,
( left_apart_point(X1,X2)
| left_apart_point(X3,X2)
| ~ divides_points(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
fof(c_0_45,plain,
! [X57] : ~ distinct_lines(X57,reverse_line(X57)),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[oagco8])]) ).
cnf(c_0_46,plain,
( left_apart_point(X1,X2)
| left_apart_point(X1,reverse_line(X2))
| ~ apart_point_and_line(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_33]) ).
cnf(c_0_47,plain,
( unequally_directed_lines(X1,reverse_line(X2))
| ~ convergent_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
fof(c_0_48,plain,
! [X42,X43] :
( ~ left_convergent_lines(X42,X43)
& ~ left_convergent_lines(X42,reverse_line(X43)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[oag11])]) ).
fof(c_0_49,plain,
! [X25] : ~ distinct_lines(X25,X25),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[oag3])]) ).
fof(c_0_50,plain,
! [X21] : ~ distinct_points(X21,X21),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[oag1])]) ).
fof(c_0_51,plain,
! [X29] : ~ unequally_directed_lines(X29,X29),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[oag5])]) ).
cnf(c_0_52,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X2,X4)
| ~ between_on_line(X1,X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_35]),
[final] ).
cnf(c_0_53,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X3,X2)
| ~ between_on_line(X1,X3,X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_35]),
[final] ).
cnf(c_0_54,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X3,X2)
| ~ between_on_line(X1,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_35]),
[final] ).
cnf(c_0_55,plain,
( before_on_line(X1,X2,X3)
| before_on_line(X1,X4,X3)
| ~ between_on_line(X1,X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[c_0_35]),
[final] ).
cnf(c_0_56,plain,
( between_on_line(X1,X2,X3,X4)
| ~ before_on_line(X1,X2,X3)
| ~ before_on_line(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_35]),
[final] ).
cnf(c_0_57,plain,
( between_on_line(X1,X4,X3,X2)
| ~ before_on_line(X1,X2,X3)
| ~ before_on_line(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_35]),
[final] ).
cnf(c_0_58,plain,
( distinct_lines(X1,X3)
| distinct_lines(X2,X3)
| ~ distinct_lines(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_36]),
[final] ).
cnf(c_0_59,plain,
( distinct_points(X1,X3)
| distinct_points(X2,X3)
| ~ distinct_points(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_37]),
[final] ).
cnf(c_0_60,plain,
( ~ point(X1)
| ~ point(X2)
| ~ distinct_points(X2,X1) ),
inference(csr,[status(thm)],[c_0_38,c_0_39]),
[final] ).
cnf(c_0_61,plain,
( before_on_line(X1,X2,X3)
| ~ distinct_points(X2,X3) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_40,c_0_41]),c_0_41]),c_0_41]),c_0_41]),c_0_25]),
[final] ).
cnf(c_0_62,plain,
( ~ distinct_lines(X1,X2)
| ~ distinct_points(X3,X4) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_42,c_0_41]),c_0_41]),c_0_41]),c_0_41]),c_0_41]),c_0_41]),c_0_41]),c_0_41]),
[final] ).
cnf(c_0_63,plain,
( distinct_points(X1,X2)
| ~ before_on_line(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_29]),
[final] ).
cnf(c_0_64,plain,
( line(reverse_line(X1))
| ~ line(X1) ),
inference(split_conjunct,[status(thm)],[c_0_43]),
[final] ).
cnf(c_0_65,plain,
~ divides_points(X1,X2,X3),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_44,c_0_41]),c_0_41]),
[final] ).
cnf(c_0_66,plain,
~ distinct_lines(X1,reverse_line(X1)),
inference(split_conjunct,[status(thm)],[c_0_45]),
[final] ).
cnf(c_0_67,plain,
~ apart_point_and_line(X1,X2),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_46,c_0_41]),c_0_41]),
[final] ).
cnf(c_0_68,plain,
~ convergent_lines(X1,X2),
inference(sr,[status(thm)],[c_0_47,c_0_22]),
[final] ).
cnf(c_0_69,plain,
~ left_convergent_lines(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_48]),
[final] ).
cnf(c_0_70,plain,
~ distinct_lines(X1,X1),
inference(split_conjunct,[status(thm)],[c_0_49]),
[final] ).
cnf(c_0_71,plain,
~ distinct_points(X1,X1),
inference(split_conjunct,[status(thm)],[c_0_50]),
[final] ).
cnf(c_0_72,plain,
~ unequally_directed_lines(X1,X1),
inference(split_conjunct,[status(thm)],[c_0_51]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GEO354+1 : TPTP v8.1.0. Released v6.4.0.
% 0.08/0.14 % Command : enigmatic-eprover.py %s %d 1
% 0.14/0.36 % Computer : n029.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Sat Jun 18 16:51:46 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.22/0.47 # ENIGMATIC: Selected SinE mode:
% 0.22/0.48 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.48 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.22/0.48 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.22/0.48 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 4.19/1.68 [LightGBM] [Fatal] Data file /export/starexec/sandbox2/tmp/enigma-theBenchmark.p-_pych7qz/test couldn't be read
% 4.19/1.68 [11657] Failed to execute script predict4sine1
% 4.19/1.68 Traceback (most recent call last):
% 4.19/1.68 File "predict4sine1.py", line 24, in <module>
% 4.19/1.68 File "site-packages/lightgbm/basic.py", line 1037, in construct
% 4.19/1.68 File "site-packages/lightgbm/basic.py", line 833, in _lazy_init
% 4.19/1.68 File "site-packages/lightgbm/basic.py", line 47, in _safe_call
% 4.19/1.68 lightgbm.basic.LightGBMError: Data file /export/starexec/sandbox2/tmp/enigma-theBenchmark.p-_pych7qz/test couldn't be read
% 5.45/2.06 # ENIGMATIC: Solved by autoschedule:
% 5.45/2.06 # No SInE strategy applied
% 5.45/2.06 # Trying AutoSched0 for 150 seconds
% 5.45/2.06 # AutoSched0-Mode selected heuristic G_E___207_C18_F1_SE_CS_SP_PI_PS_S2SA
% 5.45/2.06 # and selection function SelectNewComplexAHP.
% 5.45/2.06 #
% 5.45/2.06 # Preprocessing time : 0.027 s
% 5.45/2.06 # Presaturation interreduction done
% 5.45/2.06
% 5.45/2.06 # No proof found!
% 5.45/2.06 # SZS status Satisfiable
% 5.45/2.06 # SZS output start Saturation
% See solution above
% 5.45/2.06
% 5.45/2.06 # -------------------------------------------------
% 5.45/2.06 # User time : 0.032 s
% 5.45/2.06 # System time : 0.006 s
% 5.45/2.06 # Total time : 0.037 s
% 5.45/2.06 # Maximum resident set size: 7112 pages
% 5.45/2.06
%------------------------------------------------------------------------------