%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : GEO463+1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:28:19 PM UTC 2026
% Result : Theorem 214.19s 31.94s
% Output : CNFRefutation 214.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 5
% Syntax : Number of formulae : 19 ( 15 unt; 0 def)
% Number of atoms : 59 ( 6 equ)
% Maximal formula atoms : 33 ( 3 avg)
% Number of connectives : 63 ( 23 ~; 26 |; 11 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 13 con; 0-2 aty)
% Number of variables : 38 ( 1 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(aSPANu_CLAUSESu_conjunct1,conjecture,
! [X1385] : p(s(bool,i(s(fun(fun(cart(real,X1385),bool),bool),i(s(fun(cart(real,X1385),fun(fun(cart(real,X1385),bool),bool)),in),s(cart(real,X1385),i(s(fun(num,cart(real,X1385)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X1385),bool),i(s(fun(fun(cart(real,X1385),bool),fun(cart(real,X1385),bool)),span),s(fun(cart(real,X1385),bool),s0)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSPANu_CLAUSESu_conjunct1) ).
fof(aNUMERAL,axiom,
! [X84] : s(num,i(s(fun(num,num),numeral),s(num,X84))) = s(num,X84),
file('/export/starexec/sandbox/benchmark/Axioms/GEO010+0.ax',aNUMERAL) ).
fof(aIN,axiom,
! [X4,X7,X1] : s(bool,i(s(fun(fun(X4,bool),bool),i(s(fun(X4,fun(fun(X4,bool),bool)),in),s(X4,X1))),s(fun(X4,bool),X7))) = s(bool,i(s(fun(X4,bool),X7),s(X4,X1))),
file('/export/starexec/sandbox/benchmark/Axioms/GEO010+0.ax',aIN) ).
fof(asubspace,axiom,
! [X1361,X97] :
( p(s(bool,i(s(fun(fun(cart(real,X1361),bool),bool),subspace),s(fun(cart(real,X1361),bool),X97))))
<=> ( ! [X95,X1] :
( p(s(bool,i(s(fun(fun(cart(real,X1361),bool),bool),i(s(fun(cart(real,X1361),fun(fun(cart(real,X1361),bool),bool)),in),s(cart(real,X1361),X1))),s(fun(cart(real,X1361),bool),X97))))
=> p(s(bool,i(s(fun(fun(cart(real,X1361),bool),bool),i(s(fun(cart(real,X1361),fun(fun(cart(real,X1361),bool),bool)),in),s(cart(real,X1361),i(s(fun(cart(real,X1361),cart(real,X1361)),i(s(fun(real,fun(cart(real,X1361),cart(real,X1361))),r_),s(real,X95))),s(cart(real,X1361),X1))))),s(fun(cart(real,X1361),bool),X97)))) )
& ! [X1,X8] :
( ( p(s(bool,i(s(fun(fun(cart(real,X1361),bool),bool),i(s(fun(cart(real,X1361),fun(fun(cart(real,X1361),bool),bool)),in),s(cart(real,X1361),X8))),s(fun(cart(real,X1361),bool),X97))))
& p(s(bool,i(s(fun(fun(cart(real,X1361),bool),bool),i(s(fun(cart(real,X1361),fun(fun(cart(real,X1361),bool),bool)),in),s(cart(real,X1361),X1))),s(fun(cart(real,X1361),bool),X97)))) )
=> p(s(bool,i(s(fun(fun(cart(real,X1361),bool),bool),i(s(fun(cart(real,X1361),fun(fun(cart(real,X1361),bool),bool)),in),s(cart(real,X1361),i(s(fun(cart(real,X1361),cart(real,X1361)),i(s(fun(cart(real,X1361),fun(cart(real,X1361),cart(real,X1361))),vectoru_add),s(cart(real,X1361),X1))),s(cart(real,X1361),X8))))),s(fun(cart(real,X1361),bool),X97)))) )
& p(s(bool,i(s(fun(fun(cart(real,X1361),bool),bool),i(s(fun(cart(real,X1361),fun(fun(cart(real,X1361),bool),bool)),in),s(cart(real,X1361),i(s(fun(num,cart(real,X1361)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X1361),bool),X97)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',asubspace) ).
fof(aSUBSPACEu_SPAN,axiom,
! [X1383,X97] : p(s(bool,i(s(fun(fun(cart(real,X1383),bool),bool),subspace),s(fun(cart(real,X1383),bool),i(s(fun(fun(cart(real,X1383),bool),fun(cart(real,X1383),bool)),span),s(fun(cart(real,X1383),bool),X97)))))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',aSUBSPACEu_SPAN) ).
fof(c_0_5,negated_conjecture,
~ ! [X1385] : p(s(bool,i(s(fun(fun(cart(real,X1385),bool),bool),i(s(fun(cart(real,X1385),fun(fun(cart(real,X1385),bool),bool)),in),s(cart(real,X1385),i(s(fun(num,cart(real,X1385)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X1385),bool),i(s(fun(fun(cart(real,X1385),bool),fun(cart(real,X1385),bool)),span),s(fun(cart(real,X1385),bool),s0)))))),
inference(assume_negation,[status(cth)],[aSPANu_CLAUSESu_conjunct1]) ).
fof(c_0_6,negated_conjecture,
~ p(s(bool,i(s(fun(fun(cart(real,esk1_0),bool),bool),i(s(fun(cart(real,esk1_0),fun(fun(cart(real,esk1_0),bool),bool)),in),s(cart(real,esk1_0),i(s(fun(num,cart(real,esk1_0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,esk1_0),bool),i(s(fun(fun(cart(real,esk1_0),bool),fun(cart(real,esk1_0),bool)),span),s(fun(cart(real,esk1_0),bool),s0)))))),
inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_5])])])]) ).
fof(c_0_7,plain,
! [X2209] : s(num,i(s(fun(num,num),numeral),s(num,X2209))) = s(num,X2209),
inference(variable_rename,[status(thm)],[aNUMERAL]) ).
fof(c_0_8,plain,
! [X2339,X2340,X2341] : s(bool,i(s(fun(fun(X2339,bool),bool),i(s(fun(X2339,fun(fun(X2339,bool),bool)),in),s(X2339,X2341))),s(fun(X2339,bool),X2340))) = s(bool,i(s(fun(X2339,bool),X2340),s(X2339,X2341))),
inference(variable_rename,[status(thm)],[aIN]) ).
fof(c_0_9,plain,
! [X5063,X5064,X5065,X5066,X5067,X5068,X5069,X5070] :
( ( p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),subspace),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(num,cart(real,X5069)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(cart(real,X5069),cart(real,X5069)),i(s(fun(cart(real,X5069),fun(cart(real,X5069),cart(real,X5069))),vectoru_add),s(cart(real,X5069),esk1047_2(X5069,X5070)))),s(cart(real,X5069),esk1048_2(X5069,X5070)))))),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(cart(real,X5069),cart(real,X5069)),i(s(fun(real,fun(cart(real,X5069),cart(real,X5069))),r_),s(real,esk1049_2(X5069,X5070)))),s(cart(real,X5069),esk1050_2(X5069,X5070)))))),s(fun(cart(real,X5069),bool),X5070)))) )
& ( p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),subspace),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(num,cart(real,X5069)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(cart(real,X5069),cart(real,X5069)),i(s(fun(cart(real,X5069),fun(cart(real,X5069),cart(real,X5069))),vectoru_add),s(cart(real,X5069),esk1047_2(X5069,X5070)))),s(cart(real,X5069),esk1048_2(X5069,X5070)))))),s(fun(cart(real,X5069),bool),X5070))))
| p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),esk1050_2(X5069,X5070)))),s(fun(cart(real,X5069),bool),X5070)))) )
& ( p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),subspace),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(num,cart(real,X5069)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X5069),bool),X5070))))
| p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),esk1048_2(X5069,X5070)))),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(cart(real,X5069),cart(real,X5069)),i(s(fun(real,fun(cart(real,X5069),cart(real,X5069))),r_),s(real,esk1049_2(X5069,X5070)))),s(cart(real,X5069),esk1050_2(X5069,X5070)))))),s(fun(cart(real,X5069),bool),X5070)))) )
& ( p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),subspace),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(num,cart(real,X5069)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X5069),bool),X5070))))
| p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),esk1048_2(X5069,X5070)))),s(fun(cart(real,X5069),bool),X5070))))
| p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),esk1050_2(X5069,X5070)))),s(fun(cart(real,X5069),bool),X5070)))) )
& ( p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),subspace),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(num,cart(real,X5069)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X5069),bool),X5070))))
| p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),esk1047_2(X5069,X5070)))),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(cart(real,X5069),cart(real,X5069)),i(s(fun(real,fun(cart(real,X5069),cart(real,X5069))),r_),s(real,esk1049_2(X5069,X5070)))),s(cart(real,X5069),esk1050_2(X5069,X5070)))))),s(fun(cart(real,X5069),bool),X5070)))) )
& ( p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),subspace),s(fun(cart(real,X5069),bool),X5070))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),i(s(fun(num,cart(real,X5069)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X5069),bool),X5070))))
| p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),esk1047_2(X5069,X5070)))),s(fun(cart(real,X5069),bool),X5070))))
| p(s(bool,i(s(fun(fun(cart(real,X5069),bool),bool),i(s(fun(cart(real,X5069),fun(fun(cart(real,X5069),bool),bool)),in),s(cart(real,X5069),esk1050_2(X5069,X5070)))),s(fun(cart(real,X5069),bool),X5070)))) )
& ( ~ p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),subspace),s(fun(cart(real,X5063),bool),X5064))))
| p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),i(s(fun(cart(real,X5063),fun(fun(cart(real,X5063),bool),bool)),in),s(cart(real,X5063),i(s(fun(cart(real,X5063),cart(real,X5063)),i(s(fun(real,fun(cart(real,X5063),cart(real,X5063))),r_),s(real,X5067))),s(cart(real,X5063),X5068))))),s(fun(cart(real,X5063),bool),X5064))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),i(s(fun(cart(real,X5063),fun(fun(cart(real,X5063),bool),bool)),in),s(cart(real,X5063),X5068))),s(fun(cart(real,X5063),bool),X5064)))) )
& ( ~ p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),subspace),s(fun(cart(real,X5063),bool),X5064))))
| p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),i(s(fun(cart(real,X5063),fun(fun(cart(real,X5063),bool),bool)),in),s(cart(real,X5063),i(s(fun(cart(real,X5063),cart(real,X5063)),i(s(fun(cart(real,X5063),fun(cart(real,X5063),cart(real,X5063))),vectoru_add),s(cart(real,X5063),X5065))),s(cart(real,X5063),X5066))))),s(fun(cart(real,X5063),bool),X5064))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),i(s(fun(cart(real,X5063),fun(fun(cart(real,X5063),bool),bool)),in),s(cart(real,X5063),X5066))),s(fun(cart(real,X5063),bool),X5064))))
| ~ p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),i(s(fun(cart(real,X5063),fun(fun(cart(real,X5063),bool),bool)),in),s(cart(real,X5063),X5065))),s(fun(cart(real,X5063),bool),X5064)))) )
& ( ~ p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),subspace),s(fun(cart(real,X5063),bool),X5064))))
| p(s(bool,i(s(fun(fun(cart(real,X5063),bool),bool),i(s(fun(cart(real,X5063),fun(fun(cart(real,X5063),bool),bool)),in),s(cart(real,X5063),i(s(fun(num,cart(real,X5063)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X5063),bool),X5064)))) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[asubspace])])])])])])]) ).
cnf(c_0_10,negated_conjecture,
~ p(s(bool,i(s(fun(fun(cart(real,esk1_0),bool),bool),i(s(fun(cart(real,esk1_0),fun(fun(cart(real,esk1_0),bool),bool)),in),s(cart(real,esk1_0),i(s(fun(num,cart(real,esk1_0)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,esk1_0),bool),i(s(fun(fun(cart(real,esk1_0),bool),fun(cart(real,esk1_0),bool)),span),s(fun(cart(real,esk1_0),bool),s0)))))),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_11,plain,
s(num,i(s(fun(num,num),numeral),s(num,X1))) = s(num,X1),
inference(split_conjunct,[status(thm)],[c_0_7]) ).
cnf(c_0_12,plain,
s(bool,i(s(fun(fun(X1,bool),bool),i(s(fun(X1,fun(fun(X1,bool),bool)),in),s(X1,X2))),s(fun(X1,bool),X3))) = s(bool,i(s(fun(X1,bool),X3),s(X1,X2))),
inference(split_conjunct,[status(thm)],[c_0_8]) ).
cnf(c_0_13,plain,
( ~ p(s(bool,i(s(fun(fun(cart(real,X1),bool),bool),subspace),s(fun(cart(real,X1),bool),X2))))
| p(s(bool,i(s(fun(fun(cart(real,X1),bool),bool),i(s(fun(cart(real,X1),fun(fun(cart(real,X1),bool),bool)),in),s(cart(real,X1),i(s(fun(num,cart(real,X1)),vec),s(num,i(s(fun(num,num),numeral),s(num,u_0))))))),s(fun(cart(real,X1),bool),X2)))) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
fof(c_0_14,plain,
! [X2204,X2205] : p(s(bool,i(s(fun(fun(cart(real,X2204),bool),bool),subspace),s(fun(cart(real,X2204),bool),i(s(fun(fun(cart(real,X2204),bool),fun(cart(real,X2204),bool)),span),s(fun(cart(real,X2204),bool),X2205)))))),
inference(variable_rename,[status(thm)],[aSUBSPACEu_SPAN]) ).
cnf(c_0_15,negated_conjecture,
~ p(s(bool,i(s(fun(cart(real,esk1_0),bool),i(s(fun(fun(cart(real,esk1_0),bool),fun(cart(real,esk1_0),bool)),span),s(fun(cart(real,esk1_0),bool),s0))),s(cart(real,esk1_0),i(s(fun(num,cart(real,esk1_0)),vec),s(num,u_0)))))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_10,c_0_11]),c_0_12]) ).
cnf(c_0_16,plain,
( ~ p(s(bool,i(s(fun(fun(cart(real,X1),bool),bool),subspace),s(fun(cart(real,X1),bool),X2))))
| p(s(bool,i(s(fun(cart(real,X1),bool),X2),s(cart(real,X1),i(s(fun(num,cart(real,X1)),vec),s(num,u_0)))))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_13,c_0_11]),c_0_12]) ).
cnf(c_0_17,plain,
p(s(bool,i(s(fun(fun(cart(real,X1),bool),bool),subspace),s(fun(cart(real,X1),bool),i(s(fun(fun(cart(real,X1),bool),fun(cart(real,X1),bool)),span),s(fun(cart(real,X1),bool),X2)))))),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_18,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15,c_0_16]),c_0_17])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEO463+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.02 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 20 16:27:07 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.33 Running first-order theorem proving
% 0.07/0.33 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 214.19/31.94 % Version: 3.5.1
% 214.19/31.94 % Preprocessing class: FMLMSMSLSSSNFFN.
% 214.19/31.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 214.19/31.94 % Starting G-E--_208_C18C--_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 900s (3) cores
% 214.19/31.94 % Starting new_bool_3 with 600s (2) cores
% 214.19/31.94 % Starting new_bool_1 with 600s (2) cores
% 214.19/31.94 % Starting sh5l with 300s (1) cores
% 214.19/31.94 % new_bool_3 with pid 478380 completed with status 0
% 214.19/31.94 % Result found by new_bool_3
% 214.19/31.94 % Preprocessing class: FMLMSMSLSSSNFFN.
% 214.19/31.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 214.19/31.94 % Starting G-E--_208_C18C--_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 900s (3) cores
% 214.19/31.94 % Starting new_bool_3 with 600s (2) cores
% 214.19/31.94 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 214.19/31.94 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 214.19/31.94 % Search class: FGHSM-SMLM33-DFFFFFNN
% 214.19/31.94 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 214.19/31.94 % Starting SubtermCWHack with 55s (1) cores
% 214.19/31.94 % Starting new_bool_3 with 61s (1) cores
% 214.19/31.94 % SubtermCWHack with pid 478383 completed with status 0
% 214.19/31.94 % Result found by SubtermCWHack
% 214.19/31.94 % Preprocessing class: FMLMSMSLSSSNFFN.
% 214.19/31.94 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 214.19/31.94 % Starting G-E--_208_C18C--_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 900s (3) cores
% 214.19/31.94 % Starting new_bool_3 with 600s (2) cores
% 214.19/31.94 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 214.19/31.94 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 214.19/31.94 % Search class: FGHSM-SMLM33-DFFFFFNN
% 214.19/31.94 % Scheduled 7 strats onto 2 cores with 600 seconds (600 total)
% 214.19/31.94 % Starting SubtermCWHack with 55s (1) cores
% 214.19/31.94 % Preprocessing time : 0.221 s
% 214.19/31.94
% 214.19/31.94 % Proof found!
% 214.19/31.94 % SZS status Theorem
% 214.19/31.94 % SZS output start CNFRefutation
% See solution above
% 214.19/31.94 % Parsed axioms : 3317
% 214.19/31.94 % Removed by relevancy pruning/SinE : 1657
% 214.19/31.94 % Initial clauses : 5083
% 214.19/31.94 % Removed in clause preprocessing : 191
% 214.19/31.94 % Initial clauses in saturation : 4892
% 214.19/31.94 % Processed clauses : 22319
% 214.19/31.94 % ...of these trivial : 169
% 214.19/31.94 % ...subsumed : 18368
% 214.19/31.94 % ...remaining for further processing : 3782
% 214.19/31.94 % Other redundant clauses eliminated : 0
% 214.19/31.94 % Clauses deleted for lack of memory : 0
% 214.19/31.94 % Backward-subsumed : 63
% 214.19/31.94 % Backward-rewritten : 38
% 214.19/31.94 % Generated clauses : 1496212
% 214.19/31.94 % ...of the previous two non-redundant : 1224634
% 214.19/31.94 % ...aggressively subsumed : 0
% 214.19/31.94 % Contextual simplify-reflections : 19
% 214.19/31.94 % Paramodulations : 1496098
% 214.19/31.94 % Factorizations : 20
% 214.19/31.94 % NegExts : 0
% 214.19/31.94 % Equation resolutions : 93
% 214.19/31.94 % Disequality decompositions : 0
% 214.19/31.94 % Total rewrite steps : 497077
% 214.19/31.94 % ...of those cached : 445610
% 214.19/31.94 % Propositional unsat checks : 0
% 214.19/31.94 % Propositional check models : 0
% 214.19/31.94 % Propositional check unsatisfiable : 0
% 214.19/31.94 % Propositional clauses : 0
% 214.19/31.94 % Propositional clauses after purity: 0
% 214.19/31.94 % Propositional unsat core size : 0
% 214.19/31.94 % Propositional preprocessing time : 0.000
% 214.19/31.94 % Propositional encoding time : 0.000
% 214.19/31.94 % Propositional solver time : 0.000
% 214.19/31.94 % Success case prop preproc time : 0.000
% 214.19/31.94 % Success case prop encoding time : 0.000
% 214.19/31.94 % Success case prop solver time : 0.000
% 214.19/31.94 % Current number of processed clauses : 3680
% 214.19/31.94 % Positive orientable unit clauses : 1287
% 214.19/31.94 % Positive unorientable unit clauses: 58
% 214.19/31.94 % Negative unit clauses : 327
% 214.19/31.94 % Non-unit-clauses : 2008
% 214.19/31.94 % Current number of unprocessed clauses: 1206207
% 214.19/31.94 % ...number of literals in the above : 4563617
% 214.19/31.94 % Current number of archived formulas : 0
% 214.19/31.94 % Current number of archived clauses : 102
% 214.19/31.94 % Clause-clause subsumption calls (NU) : 751518
% 214.19/31.94 % Rec. Clause-clause subsumption calls : 305014
% 214.19/31.94 % Non-unit clause-clause subsumptions : 8256
% 214.19/31.94 % Unit Clause-clause subsumption calls : 19338
% 214.19/31.94 % Rewrite failures with RHS unbound : 1132
% 214.19/31.94 % BW rewrite match attempts : 210631
% 214.19/31.94 % BW rewrite match successes : 140
% 214.19/31.94 % Condensation attempts : 0
% 214.19/31.94 % Condensation successes : 0
% 214.19/31.94 % Termbank termtop insertions : 121004545
% 214.19/31.94 % Search garbage collected termcells : 132852
% 214.19/31.94
% 214.19/31.94 % -------------------------------------------------
% 214.19/31.94 % User time : 30.310 s
% 214.19/31.94 % System time : 0.717 s
% 214.19/31.94 % Total time : 31.027 s
% 214.19/31.94 % Maximum resident set size: 37620 pages
% 214.19/31.94
% 214.19/31.94 % -------------------------------------------------
% 214.19/31.94 % User time : 60.221 s
% 214.19/31.94 % System time : 1.556 s
% 214.19/31.94 % Total time : 61.777 s
% 214.19/31.94 % Maximum resident set size: 15104 pages
% 214.19/31.94 % E exiting
%------------------------------------------------------------------------------