%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : CSR110+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:16:58 PM UTC 2026
% Result : Unsatisfiable 115.88s 26.26s
% Output : CNFRefutation 115.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 9
% Syntax : Number of formulae : 54 ( 16 unt; 0 def)
% Number of atoms : 237 ( 37 equ)
% Maximal formula atoms : 45 ( 4 avg)
% Number of connectives : 281 ( 98 ~; 108 |; 59 &)
% ( 6 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 12 con; 0-3 aty)
% Number of variables : 117 ( 31 sgn 47 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(kb_SUMO_10668,axiom,
~ s__overlapsTemporally(s__CommonEra,s__BeforeCommonEra),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_10668) ).
fof(kb_SUMO_4682,axiom,
! [X171,X172,X173] :
( X172 = s__UnionFn(X173,X171)
<=> ! [X174,X175,X176] :
( ( s__instance(X171,s__SetOrClass)
& s__instance(X172,s__SetOrClass)
& s__instance(X173,s__SetOrClass) )
=> ( ( s__instance(X176,X172)
& s__instance(X175,X171)
& s__instance(X174,X173) )
=> ( ( s__instance(X176,X171)
| s__instance(X176,X173) )
& s__instance(X175,X172)
& s__instance(X174,X172) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_4682) ).
fof(kb_SUMO_1099,axiom,
! [X48] :
( s__instance(X48,s__TimeInterval)
=> s__overlapsTemporally(X48,X48) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_1099) ).
fof(kb_SUMO_4719,axiom,
! [X168] :
( s__instance(X168,s__SetOrClass)
=> ( s__instance(X168,s__NullSet)
=> ~ ? [X48] : s__instance(X48,X168) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_4719) ).
fof(kb_SUMO_10665,axiom,
s__instance(s__BeforeCommonEra,s__TimeInterval),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_10665) ).
fof(kb_SUMO_374,axiom,
! [X9,X10] :
( s__disjoint(X9,X10)
<=> ! [X48] :
( ( s__instance(X9,s__SetOrClass)
& s__instance(X10,s__SetOrClass) )
=> ~ ( s__instance(X48,X10)
& s__instance(X48,X9) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_374) ).
fof(kb_SUMO_4675,axiom,
! [X169,X170] :
( ! [X49] :
( ( s__instance(X169,s__Set)
& s__instance(X170,s__Set) )
=> ( s__element(X49,X170)
<=> s__element(X49,X169) ) )
=> X170 = X169 ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_4675) ).
fof(kb_SUMO_10189,axiom,
! [X749] :
( s__instance(X749,s__ConjugatedSubstance)
<=> ? [X173,X171,X121] :
( s__result(X121,X749)
& s__resource(X121,X171)
& s__resource(X121,X173)
& s__instance(X121,s__ChemicalSynthesis)
& X173 != X171
& s__instance(X171,s__CompoundSubstance)
& s__instance(X173,s__CompoundSubstance)
& s__instance(X173,s__Object)
& s__instance(X171,s__Object)
& s__instance(X121,s__Process) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_10189) ).
fof(kb_SUMO_5845,axiom,
! [X51] :
( s__instance(X51,s__SelfConnectedObject)
<=> ! [X159,X160] :
( ( s__instance(X159,s__Object)
& s__instance(X160,s__Object) )
=> ( X51 = s__MereologicalSumFn(X159,X160)
=> s__connected(X159,X160) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR003+1.ax',kb_SUMO_5845) ).
fof(c_0_9,plain,
~ s__overlapsTemporally(s__CommonEra,s__BeforeCommonEra),
inference(fof_simplification,[status(thm)],[kb_SUMO_10668]) ).
fof(c_0_10,plain,
~ s__overlapsTemporally(s__CommonEra,s__BeforeCommonEra),
inference(fof_nnf,[status(thm)],[c_0_9]) ).
fof(c_0_11,plain,
! [X9512,X9513,X9514,X9515,X9516,X9517,X9518,X9519,X9520] :
( ( X9519 = s__UnionFn(X9520,X9518)
| ~ s__instance(esk189_3(X9518,X9519,X9520),X9519)
| ~ s__instance(esk188_3(X9518,X9519,X9520),X9519)
| ~ s__instance(esk190_3(X9518,X9519,X9520),X9518) )
& ( X9519 = s__UnionFn(X9520,X9518)
| ~ s__instance(esk189_3(X9518,X9519,X9520),X9519)
| ~ s__instance(esk188_3(X9518,X9519,X9520),X9519)
| ~ s__instance(esk190_3(X9518,X9519,X9520),X9520) )
& ( X9519 = s__UnionFn(X9520,X9518)
| s__instance(esk190_3(X9518,X9519,X9520),X9519) )
& ( X9519 = s__UnionFn(X9520,X9518)
| s__instance(esk189_3(X9518,X9519,X9520),X9518) )
& ( X9519 = s__UnionFn(X9520,X9518)
| s__instance(esk188_3(X9518,X9519,X9520),X9520) )
& ( X9519 = s__UnionFn(X9520,X9518)
| s__instance(X9518,s__SetOrClass) )
& ( X9519 = s__UnionFn(X9520,X9518)
| s__instance(X9519,s__SetOrClass) )
& ( X9519 = s__UnionFn(X9520,X9518)
| s__instance(X9520,s__SetOrClass) )
& ( X9513 != s__UnionFn(X9514,X9512)
| ~ s__instance(X9512,s__SetOrClass)
| ~ s__instance(X9513,s__SetOrClass)
| ~ s__instance(X9514,s__SetOrClass)
| ~ s__instance(X9517,X9513)
| ~ s__instance(X9516,X9512)
| ~ s__instance(X9515,X9514)
| s__instance(X9517,X9512)
| s__instance(X9517,X9514) )
& ( X9513 != s__UnionFn(X9514,X9512)
| ~ s__instance(X9512,s__SetOrClass)
| ~ s__instance(X9513,s__SetOrClass)
| ~ s__instance(X9514,s__SetOrClass)
| ~ s__instance(X9517,X9513)
| ~ s__instance(X9516,X9512)
| ~ s__instance(X9515,X9514)
| s__instance(X9516,X9513) )
& ( X9513 != s__UnionFn(X9514,X9512)
| ~ s__instance(X9512,s__SetOrClass)
| ~ s__instance(X9513,s__SetOrClass)
| ~ s__instance(X9514,s__SetOrClass)
| ~ s__instance(X9517,X9513)
| ~ s__instance(X9516,X9512)
| ~ s__instance(X9515,X9514)
| s__instance(X9515,X9513) ) ),
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)],[kb_SUMO_4682])])])])])])]) ).
cnf(c_0_12,plain,
~ s__overlapsTemporally(s__CommonEra,s__BeforeCommonEra),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_13,plain,
( X2 = s__UnionFn(X3,X1)
| s__instance(X1,s__SetOrClass) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_14,plain,
( ~ s__overlapsTemporally(s__UnionFn(X2,X1),s__BeforeCommonEra)
| s__instance(X1,s__SetOrClass) ),
inference(spm,[status(thm)],[c_0_12,c_0_13]) ).
fof(c_0_15,plain,
! [X3461] :
( s__overlapsTemporally(X3461,X3461)
| ~ s__instance(X3461,s__TimeInterval) ),
inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_1099])])]) ).
fof(c_0_16,plain,
! [X9524,X9525] :
( ~ s__instance(X9525,X9524)
| ~ s__instance(X9524,s__NullSet)
| ~ s__instance(X9524,s__SetOrClass) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_4719])])])]) ).
cnf(c_0_17,plain,
( ~ s__overlapsTemporally(X2,s__BeforeCommonEra)
| s__instance(X1,s__SetOrClass) ),
inference(spm,[status(thm)],[c_0_14,c_0_13]) ).
cnf(c_0_18,plain,
( ~ s__instance(X1,s__TimeInterval)
| s__overlapsTemporally(X1,X1) ),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_19,plain,
s__instance(s__BeforeCommonEra,s__TimeInterval),
inference(split_conjunct,[status(thm)],[kb_SUMO_10665]) ).
cnf(c_0_20,plain,
( ~ s__instance(X2,X1)
| ~ s__instance(X1,s__NullSet)
| ~ s__instance(X1,s__SetOrClass) ),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_21,plain,
s__instance(X1,s__SetOrClass),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17,c_0_18]),c_0_19])]) ).
fof(c_0_22,plain,
! [X2341,X2342,X2343,X2344,X2345] :
( ( s__disjoint(X2344,X2345)
| s__instance(esk1_2(X2344,X2345),X2345) )
& ( s__disjoint(X2344,X2345)
| s__instance(esk1_2(X2344,X2345),X2344) )
& ( s__disjoint(X2344,X2345)
| s__instance(X2344,s__SetOrClass) )
& ( s__disjoint(X2344,X2345)
| s__instance(X2345,s__SetOrClass) )
& ( ~ s__instance(X2343,X2342)
| ~ s__instance(X2343,X2341)
| ~ s__instance(X2341,s__SetOrClass)
| ~ s__instance(X2342,s__SetOrClass)
| ~ s__disjoint(X2341,X2342) ) ),
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)],[kb_SUMO_374])])])])])])]) ).
cnf(c_0_23,plain,
( ~ s__instance(X2,X1)
| ~ s__instance(X1,s__NullSet) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20,c_0_21])]) ).
cnf(c_0_24,plain,
( s__disjoint(X1,X2)
| s__instance(esk1_2(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_25,plain,
( ~ s__instance(X2,esk1_2(s__NullSet,X1))
| s__disjoint(s__NullSet,X1) ),
inference(spm,[status(thm)],[c_0_23,c_0_24]) ).
cnf(c_0_26,plain,
( X2 = s__UnionFn(X3,X1)
| s__instance(esk188_3(X1,X2,X3),X3) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_27,plain,
( s__disjoint(s__NullSet,X2)
| X1 = s__UnionFn(esk1_2(s__NullSet,X2),X3) ),
inference(spm,[status(thm)],[c_0_25,c_0_26]) ).
cnf(c_0_28,plain,
( s__disjoint(s__NullSet,X3)
| X1 = X2 ),
inference(spm,[status(thm)],[c_0_27,c_0_27]) ).
fof(c_0_29,plain,
! [X9509,X9510] :
( ( X9510 = X9509
| s__element(esk187_2(X9509,X9510),X9509)
| s__element(esk187_2(X9509,X9510),X9510) )
& ( X9510 = X9509
| ~ s__element(esk187_2(X9509,X9510),X9509)
| ~ s__element(esk187_2(X9509,X9510),X9510) )
& ( X9510 = X9509
| s__instance(X9509,s__Set) )
& ( X9510 = X9509
| s__instance(X9510,s__Set) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_4675])])])])])]) ).
cnf(c_0_30,plain,
( ~ s__instance(X3,X2)
| ~ s__instance(X3,X1)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,s__SetOrClass)
| ~ s__disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_22]) ).
cnf(c_0_31,plain,
( ~ s__overlapsTemporally(X2,s__BeforeCommonEra)
| s__disjoint(s__NullSet,X1) ),
inference(spm,[status(thm)],[c_0_12,c_0_28]) ).
cnf(c_0_32,plain,
( X2 = X1
| s__instance(X1,s__Set) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_33,plain,
( ~ s__instance(X3,X1)
| ~ s__instance(X3,X2)
| ~ s__disjoint(X1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30,c_0_21]),c_0_21])]) ).
cnf(c_0_34,plain,
s__disjoint(s__NullSet,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_18]),c_0_19])]) ).
cnf(c_0_35,plain,
( ~ s__overlapsTemporally(X1,s__BeforeCommonEra)
| s__instance(X1,s__Set) ),
inference(spm,[status(thm)],[c_0_12,c_0_32]) ).
cnf(c_0_36,plain,
( ~ s__instance(X1,X2)
| ~ s__instance(X1,s__NullSet) ),
inference(spm,[status(thm)],[c_0_33,c_0_34]) ).
cnf(c_0_37,plain,
( X2 = s__UnionFn(X3,X1)
| s__instance(esk190_3(X1,X2,X3),X2) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_38,plain,
s__instance(s__BeforeCommonEra,s__Set),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_18]),c_0_19])]) ).
cnf(c_0_39,plain,
( ~ s__instance(esk190_3(X2,s__NullSet,X1),X3)
| s__NullSet = s__UnionFn(X1,X2) ),
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
cnf(c_0_40,plain,
s__instance(X1,s__Set),
inference(spm,[status(thm)],[c_0_38,c_0_32]) ).
fof(c_0_41,plain,
! [X749] :
( s__instance(X749,s__ConjugatedSubstance)
<=> ? [X173,X171,X121] :
( s__result(X121,X749)
& s__resource(X121,X171)
& s__resource(X121,X173)
& s__instance(X121,s__ChemicalSynthesis)
& X173 != X171
& s__instance(X171,s__CompoundSubstance)
& s__instance(X173,s__CompoundSubstance)
& s__instance(X173,s__Object)
& s__instance(X171,s__Object)
& s__instance(X121,s__Process) ) ),
inference(fof_simplification,[status(thm)],[kb_SUMO_10189]) ).
cnf(c_0_42,plain,
( X2 = s__UnionFn(X3,X1)
| s__instance(esk189_3(X1,X2,X3),X1) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_43,plain,
s__NullSet = s__UnionFn(X1,X2),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
fof(c_0_44,plain,
! [X11975,X11979,X11980,X11981,X11982] :
( ( s__instance(X11979,s__ConjugatedSubstance)
| ~ s__result(X11982,X11979)
| ~ s__resource(X11982,X11981)
| ~ s__resource(X11982,X11980)
| ~ s__instance(X11982,s__ChemicalSynthesis)
| X11980 = X11981
| ~ s__instance(X11981,s__CompoundSubstance)
| ~ s__instance(X11980,s__CompoundSubstance)
| ~ s__instance(X11980,s__Object)
| ~ s__instance(X11981,s__Object)
| ~ s__instance(X11982,s__Process) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__result(esk748_1(X11975),X11975) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__resource(esk748_1(X11975),esk747_1(X11975)) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__resource(esk748_1(X11975),esk746_1(X11975)) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__instance(esk748_1(X11975),s__ChemicalSynthesis) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| esk746_1(X11975) != esk747_1(X11975) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__instance(esk747_1(X11975),s__CompoundSubstance) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__instance(esk746_1(X11975),s__CompoundSubstance) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__instance(esk746_1(X11975),s__Object) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__instance(esk747_1(X11975),s__Object) )
& ( ~ s__instance(X11975,s__ConjugatedSubstance)
| s__instance(esk748_1(X11975),s__Process) ) ),
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)],[c_0_41])])])])])])]) ).
cnf(c_0_45,plain,
( ~ s__instance(esk189_3(s__NullSet,X1,X2),X3)
| X1 = s__NullSet ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_42]),c_0_43]) ).
cnf(c_0_46,plain,
( ~ s__instance(X1,s__ConjugatedSubstance)
| esk746_1(X1) != esk747_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_47,plain,
X1 = s__NullSet,
inference(spm,[status(thm)],[c_0_45,c_0_40]) ).
fof(c_0_48,plain,
! [X10109,X10110,X10111,X10112] :
( ( s__instance(X10112,s__SelfConnectedObject)
| ~ s__connected(esk244_1(X10112),esk245_1(X10112)) )
& ( s__instance(X10112,s__SelfConnectedObject)
| X10112 = s__MereologicalSumFn(esk244_1(X10112),esk245_1(X10112)) )
& ( s__instance(X10112,s__SelfConnectedObject)
| s__instance(esk244_1(X10112),s__Object) )
& ( s__instance(X10112,s__SelfConnectedObject)
| s__instance(esk245_1(X10112),s__Object) )
& ( s__connected(X10110,X10111)
| X10109 != s__MereologicalSumFn(X10110,X10111)
| ~ s__instance(X10110,s__Object)
| ~ s__instance(X10111,s__Object)
| ~ s__instance(X10109,s__SelfConnectedObject) ) ),
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)],[kb_SUMO_5845])])])])])])]) ).
cnf(c_0_49,plain,
~ s__instance(X1,s__ConjugatedSubstance),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_47]),c_0_47]) ).
cnf(c_0_50,plain,
X1 = X2,
inference(spm,[status(thm)],[c_0_47,c_0_47]) ).
cnf(c_0_51,plain,
( s__instance(X1,s__SelfConnectedObject)
| s__instance(esk244_1(X1),s__Object) ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
cnf(c_0_52,plain,
~ s__instance(X1,X2),
inference(spm,[status(thm)],[c_0_49,c_0_50]) ).
cnf(c_0_53,plain,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_51,c_0_52]),c_0_52]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR110+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 15:02:19 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p
% 115.88/26.26 % Version: 3.5.1
% 115.88/26.26 % Preprocessing class: FMLLSMSLSSSNFFN.
% 115.88/26.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 115.88/26.26 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 115.88/26.26 % Starting new_bool_3 with 300s (1) cores
% 115.88/26.26 % Starting new_bool_1 with 300s (1) cores
% 115.88/26.26 % Starting sh5l with 300s (1) cores
% 115.88/26.26 % new_bool_1 with pid 2851502 completed with status 9
% 115.88/26.26 % sh5l with pid 2851503 completed with status 9
% 115.88/26.26 % new_bool_3 with pid 2851501 completed with status 9
% 115.88/26.26 % G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with pid 2851500 completed with status 0
% 115.88/26.26 % Result found by G-E--_208_B07_F1_AE_CS_SP_PS_S0Y
% 115.88/26.26 % Preprocessing class: FMLLSMSLSSSNFFN.
% 115.88/26.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 115.88/26.26 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 115.88/26.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 115.88/26.26 % No SInE strategy applied
% 115.88/26.26 % Search class: FGHSM-SMLM31-MFFFFFNN
% 115.88/26.26 % Scheduled 7 strats onto 5 cores with 1497 seconds (1497 total)
% 115.88/26.26 % Starting SubtermCWHack with 135s (1) cores
% 115.88/26.26 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 150s (1) cores
% 115.88/26.26 % Starting G-E--_208_B07_F1_S5PRR_SE_CS_SP_PS_S0Y with 135s (1) cores
% 115.88/26.26 % Starting new_bool_3 with 135s (1) cores
% 115.88/26.26 % Starting new_bool_1 with 135s (1) cores
% 115.88/26.26 % G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with pid 2851575 completed with status 0
% 115.88/26.26 % Result found by G-E--_208_B07_F1_AE_CS_SP_PS_S0Y
% 115.88/26.26 % Preprocessing class: FMLLSMSLSSSNFFN.
% 115.88/26.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 115.88/26.26 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 1500s (5) cores
% 115.88/26.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 115.88/26.26 % No SInE strategy applied
% 115.88/26.26 % Search class: FGHSM-SMLM31-MFFFFFNN
% 115.88/26.26 % Scheduled 7 strats onto 5 cores with 1497 seconds (1497 total)
% 115.88/26.26 % Starting SubtermCWHack with 135s (1) cores
% 115.88/26.26 % Starting G-E--_208_B07_F1_AE_CS_SP_PS_S0Y with 150s (1) cores
% 115.88/26.26 % Preprocessing time : 0.419 s
% 115.88/26.26 % Presaturation interreduction done
% 115.88/26.26
% 115.88/26.26 % Proof found!
% 115.88/26.26 % SZS status Unsatisfiable
% 115.88/26.26 % SZS output start CNFRefutation
% See solution above
% 115.88/26.26 % Parsed axioms : 16748
% 115.88/26.26 % Removed by relevancy pruning/SinE : 0
% 115.88/26.26 % Initial clauses : 20270
% 115.88/26.26 % Removed in clause preprocessing : 63
% 115.88/26.26 % Initial clauses in saturation : 20207
% 115.88/26.26 % Processed clauses : 42174
% 115.88/26.26 % ...of these trivial : 2349
% 115.88/26.26 % ...subsumed : 511
% 115.88/26.26 % ...remaining for further processing : 39314
% 115.88/26.26 % Other redundant clauses eliminated : 71
% 115.88/26.26 % Clauses deleted for lack of memory : 0
% 115.88/26.26 % Backward-subsumed : 4981
% 115.88/26.26 % Backward-rewritten : 8254
% 115.88/26.26 % Generated clauses : 254462
% 115.88/26.26 % ...of the previous two non-redundant : 235177
% 115.88/26.26 % ...aggressively subsumed : 0
% 115.88/26.26 % Contextual simplify-reflections : 1058
% 115.88/26.26 % Paramodulations : 252984
% 115.88/26.26 % Factorizations : 1
% 115.88/26.26 % NegExts : 0
% 115.88/26.26 % Equation resolutions : 86
% 115.88/26.26 % Disequality decompositions : 0
% 115.88/26.26 % Total rewrite steps : 33554
% 115.88/26.26 % ...of those cached : 18093
% 115.88/26.26 % Propositional unsat checks : 0
% 115.88/26.26 % Propositional check models : 0
% 115.88/26.26 % Propositional check unsatisfiable : 0
% 115.88/26.26 % Propositional clauses : 0
% 115.88/26.26 % Propositional clauses after purity: 0
% 115.88/26.26 % Propositional unsat core size : 0
% 115.88/26.26 % Propositional preprocessing time : 0.000
% 115.88/26.26 % Propositional encoding time : 0.000
% 115.88/26.26 % Propositional solver time : 0.000
% 115.88/26.26 % Success case prop preproc time : 0.000
% 115.88/26.26 % Success case prop encoding time : 0.000
% 115.88/26.26 % Success case prop solver time : 0.000
% 115.88/26.26 % Current number of processed clauses : 4757
% 115.88/26.26 % Positive orientable unit clauses : 4683
% 115.88/26.26 % Positive unorientable unit clauses: 1
% 115.88/26.26 % Negative unit clauses : 31
% 115.88/26.26 % Non-unit-clauses : 42
% 115.88/26.26 % Current number of unprocessed clauses: 103828
% 115.88/26.26 % ...number of literals in the above : 205176
% 115.88/26.26 % Current number of archived formulas : 0
% 115.88/26.26 % Current number of archived clauses : 34547
% 115.88/26.26 % Clause-clause subsumption calls (NU) : 24523771
% 115.88/26.26 % Rec. Clause-clause subsumption calls : 6265915
% 115.88/26.26 % Non-unit clause-clause subsumptions : 1535
% 115.88/26.26 % Unit Clause-clause subsumption calls : 240553
% 115.88/26.26 % Rewrite failures with RHS unbound : 10022
% 115.88/26.26 % BW rewrite match attempts : 65141
% 115.88/26.26 % BW rewrite match successes : 21934
% 115.88/26.26 % Condensation attempts : 0
% 115.88/26.26 % Condensation successes : 0
% 115.88/26.26 % Termbank termtop insertions : 2655366
% 115.88/26.26 % Search garbage collected termcells : 181009
% 115.88/26.26
% 115.88/26.26 % -------------------------------------------------
% 115.88/26.26 % User time : 24.394 s
% 115.88/26.26 % System time : 0.719 s
% 115.88/26.26 % Total time : 25.112 s
% 115.88/26.26 % Maximum resident set size: 62616 pages
% 115.88/26.26
% 115.88/26.26 % -------------------------------------------------
% 115.88/26.26 % User time : 112.544 s
% 115.88/26.26 % System time : 3.175 s
% 115.88/26.26 % Total time : 115.719 s
% 115.88/26.26 % Maximum resident set size: 22272 pages
% 115.88/26.26 % E exiting
%------------------------------------------------------------------------------