%------------------------------------------------------------------------------
% File : ET---2.0
% Problem : CSR080+1 : TPTP v8.1.0. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_ET %s %d
% Computer : n023.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 03:02:19 EDT 2022
% Result : Theorem 2.39s 106.58s
% Output : CNFRefutation 2.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 49 ( 24 unt; 0 def)
% Number of atoms : 136 ( 25 equ)
% Maximal formula atoms : 45 ( 2 avg)
% Number of connectives : 144 ( 57 ~; 59 |; 17 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 5 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-3 aty)
% Number of variables : 74 ( 31 sgn 29 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove_from_SUMO,conjecture,
s__part(s__Object6_1,s__Object6_3),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',prove_from_SUMO) ).
fof(kb_SUMO_100,axiom,
! [X15,X16] :
( ( s__instance(X16,s__Substance)
& s__instance(X15,s__Substance) )
=> ( s__piece(X15,X16)
=> s__part(X15,X16) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_100) ).
fof(local_4,axiom,
s__piece(s__Object6_1,s__Object6_2),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',local_4) ).
fof(kb_SUMO_3496,axiom,
! [X171,X172,X173] :
( X172 = s__UnionFn(X173,X171)
<=> ! [X174,X175,X176] :
( ( s__instance(X173,s__SetOrClass)
& s__instance(X172,s__SetOrClass)
& s__instance(X171,s__SetOrClass) )
=> ( ( s__instance(X174,X173)
& s__instance(X175,X171)
& s__instance(X176,X172) )
=> ( s__instance(X174,X172)
& s__instance(X175,X172)
& ( s__instance(X176,X173)
| s__instance(X176,X171) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_3496) ).
fof(local_1,axiom,
s__instance(s__Object6_1,s__Substance),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',local_1) ).
fof(local_3,axiom,
s__instance(s__Object6_3,s__Substance),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',local_3) ).
fof(kb_SUMO_3533,axiom,
! [X168] :
( s__instance(X168,s__SetOrClass)
=> ( s__instance(X168,s__NullSet)
=> ~ ? [X48] : s__instance(X48,X168) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+0.ax',kb_SUMO_3533) ).
fof(local_2,axiom,
s__instance(s__Object6_2,s__Substance),
file('/export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in',local_2) ).
fof(c_0_8,plain,
( ~ epred24_0
<=> ! [X4,X1] : X1 = X4 ),
introduced(definition) ).
fof(c_0_9,negated_conjecture,
~ s__part(s__Object6_1,s__Object6_3),
inference(assume_negation,[status(cth)],[prove_from_SUMO]) ).
fof(c_0_10,plain,
! [X17,X18] :
( ~ s__instance(X18,s__Substance)
| ~ s__instance(X17,s__Substance)
| ~ s__piece(X17,X18)
| s__part(X17,X18) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_100])]) ).
cnf(c_0_11,plain,
s__piece(s__Object6_1,s__Object6_2),
inference(split_conjunct,[status(thm)],[local_4]) ).
cnf(c_0_12,plain,
( X1 = X2
| epred24_0 ),
inference(split_equiv,[status(thm)],[c_0_8]) ).
fof(c_0_13,plain,
! [X177,X178,X179,X180,X181,X182,X177,X178,X179] :
( ( s__instance(X180,X178)
| ~ s__instance(X180,X179)
| ~ s__instance(X181,X177)
| ~ s__instance(X182,X178)
| ~ s__instance(X179,s__SetOrClass)
| ~ s__instance(X178,s__SetOrClass)
| ~ s__instance(X177,s__SetOrClass)
| X178 != s__UnionFn(X179,X177) )
& ( s__instance(X181,X178)
| ~ s__instance(X180,X179)
| ~ s__instance(X181,X177)
| ~ s__instance(X182,X178)
| ~ s__instance(X179,s__SetOrClass)
| ~ s__instance(X178,s__SetOrClass)
| ~ s__instance(X177,s__SetOrClass)
| X178 != s__UnionFn(X179,X177) )
& ( s__instance(X182,X179)
| s__instance(X182,X177)
| ~ s__instance(X180,X179)
| ~ s__instance(X181,X177)
| ~ s__instance(X182,X178)
| ~ s__instance(X179,s__SetOrClass)
| ~ s__instance(X178,s__SetOrClass)
| ~ s__instance(X177,s__SetOrClass)
| X178 != s__UnionFn(X179,X177) )
& ( s__instance(X179,s__SetOrClass)
| X178 = s__UnionFn(X179,X177) )
& ( s__instance(X178,s__SetOrClass)
| X178 = s__UnionFn(X179,X177) )
& ( s__instance(X177,s__SetOrClass)
| X178 = s__UnionFn(X179,X177) )
& ( s__instance(esk158_3(X177,X178,X179),X179)
| X178 = s__UnionFn(X179,X177) )
& ( s__instance(esk159_3(X177,X178,X179),X177)
| X178 = s__UnionFn(X179,X177) )
& ( s__instance(esk160_3(X177,X178,X179),X178)
| X178 = s__UnionFn(X179,X177) )
& ( ~ s__instance(esk160_3(X177,X178,X179),X179)
| ~ s__instance(esk158_3(X177,X178,X179),X178)
| ~ s__instance(esk159_3(X177,X178,X179),X178)
| X178 = s__UnionFn(X179,X177) )
& ( ~ s__instance(esk160_3(X177,X178,X179),X177)
| ~ s__instance(esk158_3(X177,X178,X179),X178)
| ~ s__instance(esk159_3(X177,X178,X179),X178)
| X178 = s__UnionFn(X179,X177) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_3496])])])])])])]) ).
fof(c_0_14,negated_conjecture,
~ s__part(s__Object6_1,s__Object6_3),
inference(fof_simplification,[status(thm)],[c_0_9]) ).
cnf(c_0_15,plain,
( s__part(X1,X2)
| ~ s__piece(X1,X2)
| ~ s__instance(X1,s__Substance)
| ~ s__instance(X2,s__Substance) ),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
cnf(c_0_16,plain,
( epred24_0
| s__piece(s__Object6_1,X1) ),
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
cnf(c_0_17,plain,
s__instance(s__Object6_1,s__Substance),
inference(split_conjunct,[status(thm)],[local_1]) ).
fof(c_0_18,plain,
( ~ epred25_0
<=> ! [X3] : s__instance(X3,s__SetOrClass) ),
introduced(definition) ).
cnf(c_0_19,plain,
( X1 = s__UnionFn(X2,X3)
| s__instance(X3,s__SetOrClass) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_20,negated_conjecture,
~ s__part(s__Object6_1,s__Object6_3),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_21,plain,
( epred24_0
| s__part(s__Object6_1,X1)
| ~ s__instance(X1,s__Substance) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15,c_0_16]),c_0_17])]) ).
cnf(c_0_22,plain,
s__instance(s__Object6_3,s__Substance),
inference(split_conjunct,[status(thm)],[local_3]) ).
cnf(c_0_23,plain,
( ~ epred25_0
| ~ epred24_0 ),
inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(spm,[status(thm)],[c_0_19,c_0_19]),c_0_8]),c_0_18]) ).
cnf(c_0_24,negated_conjecture,
epred24_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_20,c_0_21]),c_0_22])]) ).
fof(c_0_25,plain,
! [X169,X170] :
( ~ s__instance(X169,s__SetOrClass)
| ~ s__instance(X169,s__NullSet)
| ~ s__instance(X170,X169) ),
inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[kb_SUMO_3533])])])])]) ).
cnf(c_0_26,plain,
~ epred25_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23,c_0_24])]) ).
fof(c_0_27,plain,
( ~ epred40_0
<=> ! [X2,X1] : X1 = s__UnionFn(X2,s__NullSet) ),
introduced(definition) ).
cnf(c_0_28,plain,
( ~ s__instance(X1,X2)
| ~ s__instance(X2,s__NullSet)
| ~ s__instance(X2,s__SetOrClass) ),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_29,plain,
s__instance(X1,s__SetOrClass),
inference(sr,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_18]),c_0_26]) ).
cnf(c_0_30,plain,
( X1 = s__UnionFn(X2,s__NullSet)
| epred40_0 ),
inference(split_equiv,[status(thm)],[c_0_27]) ).
cnf(c_0_31,plain,
( ~ s__instance(X1,s__NullSet)
| ~ s__instance(X2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28,c_0_29])]) ).
cnf(c_0_32,plain,
( X1 = s__UnionFn(X2,X3)
| s__instance(esk159_3(X3,X1,X2),X3) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_33,plain,
( X1 = X2
| epred40_0 ),
inference(spm,[status(thm)],[c_0_30,c_0_30]) ).
cnf(c_0_34,plain,
s__instance(s__Object6_2,s__Substance),
inference(split_conjunct,[status(thm)],[local_2]) ).
cnf(c_0_35,plain,
( X1 = s__UnionFn(X2,s__NullSet)
| ~ s__instance(X3,esk159_3(s__NullSet,X1,X2)) ),
inference(spm,[status(thm)],[c_0_31,c_0_32]) ).
cnf(c_0_36,plain,
( X1 = s__UnionFn(X2,X3)
| s__instance(esk160_3(X3,X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_37,negated_conjecture,
( epred40_0
| ~ s__part(s__Object6_1,X1) ),
inference(spm,[status(thm)],[c_0_20,c_0_33]) ).
cnf(c_0_38,plain,
s__part(s__Object6_1,s__Object6_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_15,c_0_11]),c_0_17])]),c_0_34])]) ).
fof(c_0_39,plain,
( ~ epred41_0
<=> ! [X4,X3] : s__instance(s__UnionFn(X3,X4),s__NullSet) ),
introduced(definition) ).
cnf(c_0_40,plain,
( esk159_3(s__NullSet,X1,X2) = s__UnionFn(X3,X4)
| X1 = s__UnionFn(X2,s__NullSet) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_41,negated_conjecture,
epred40_0,
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_42,plain,
~ epred41_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_40]),c_0_27]),c_0_39]),c_0_41])]) ).
cnf(c_0_43,plain,
s__instance(s__UnionFn(X1,X2),s__NullSet),
inference(sr,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_39]),c_0_42]) ).
cnf(c_0_44,plain,
~ s__instance(X1,s__UnionFn(X2,X3)),
inference(spm,[status(thm)],[c_0_31,c_0_43]) ).
cnf(c_0_45,plain,
X1 = s__UnionFn(X2,s__UnionFn(X3,X4)),
inference(spm,[status(thm)],[c_0_44,c_0_32]) ).
cnf(c_0_46,plain,
X1 = X2,
inference(spm,[status(thm)],[c_0_45,c_0_45]) ).
cnf(c_0_47,plain,
s__part(s__Object6_1,X1),
inference(spm,[status(thm)],[c_0_38,c_0_46]) ).
cnf(c_0_48,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20,c_0_47])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR080+1 : TPTP v8.1.0. Bugfixed v7.3.0.
% 0.07/0.14 % Command : run_ET %s %d
% 0.13/0.35 % Computer : n023.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jun 11 09:45:52 EDT 2022
% 0.13/0.35 % CPUTime :
% 1.91/24.95 eprover: CPU time limit exceeded, terminating
% 1.91/24.95 eprover: CPU time limit exceeded, terminating
% 1.91/25.32 eprover: CPU time limit exceeded, terminating
% 1.91/25.67 eprover: CPU time limit exceeded, terminating
% 2.04/48.00 eprover: CPU time limit exceeded, terminating
% 2.05/48.37 eprover: CPU time limit exceeded, terminating
% 2.05/48.75 eprover: CPU time limit exceeded, terminating
% 2.05/49.14 eprover: CPU time limit exceeded, terminating
% 2.18/71.01 eprover: CPU time limit exceeded, terminating
% 2.19/71.80 eprover: CPU time limit exceeded, terminating
% 2.19/72.16 eprover: CPU time limit exceeded, terminating
% 2.22/78.12 eprover: CPU time limit exceeded, terminating
% 2.33/94.03 eprover: CPU time limit exceeded, terminating
% 2.33/94.83 eprover: CPU time limit exceeded, terminating
% 2.33/95.38 eprover: CPU time limit exceeded, terminating
% 2.36/101.15 eprover: CPU time limit exceeded, terminating
% 2.39/106.58 # Running protocol protocol_eprover_4a02c828a8cc55752123edbcc1ad40e453c11447 for 23 seconds:
% 2.39/106.58 # SinE strategy is GSinE(CountFormulas,hypos,1.4,,04,100,1.0)
% 2.39/106.58 # Preprocessing time : 0.235 s
% 2.39/106.58
% 2.39/106.58 # Failure: Out of unprocessed clauses!
% 2.39/106.58 # OLD status GaveUp
% 2.39/106.58 # Parsed axioms : 14793
% 2.39/106.58 # Removed by relevancy pruning/SinE : 14692
% 2.39/106.58 # Initial clauses : 110
% 2.39/106.58 # Removed in clause preprocessing : 4
% 2.39/106.58 # Initial clauses in saturation : 106
% 2.39/106.58 # Processed clauses : 3073
% 2.39/106.58 # ...of these trivial : 81
% 2.39/106.58 # ...subsumed : 2135
% 2.39/106.58 # ...remaining for further processing : 857
% 2.39/106.58 # Other redundant clauses eliminated : 1
% 2.39/106.58 # Clauses deleted for lack of memory : 0
% 2.39/106.58 # Backward-subsumed : 54
% 2.39/106.58 # Backward-rewritten : 0
% 2.39/106.58 # Generated clauses : 3557
% 2.39/106.58 # ...of the previous two non-trivial : 2999
% 2.39/106.58 # Contextual simplify-reflections : 1671
% 2.39/106.58 # Paramodulations : 3556
% 2.39/106.58 # Factorizations : 0
% 2.39/106.58 # Equation resolutions : 1
% 2.39/106.58 # Current number of processed clauses : 802
% 2.39/106.58 # Positive orientable unit clauses : 138
% 2.39/106.58 # Positive unorientable unit clauses: 0
% 2.39/106.58 # Negative unit clauses : 27
% 2.39/106.58 # Non-unit-clauses : 637
% 2.39/106.58 # Current number of unprocessed clauses: 0
% 2.39/106.58 # ...number of literals in the above : 0
% 2.39/106.58 # Current number of archived formulas : 0
% 2.39/106.58 # Current number of archived clauses : 54
% 2.39/106.58 # Clause-clause subsumption calls (NU) : 295477
% 2.39/106.58 # Rec. Clause-clause subsumption calls : 142460
% 2.39/106.58 # Non-unit clause-clause subsumptions : 3790
% 2.39/106.58 # Unit Clause-clause subsumption calls : 1675
% 2.39/106.58 # Rewrite failures with RHS unbound : 0
% 2.39/106.58 # BW rewrite match attempts : 10
% 2.39/106.58 # BW rewrite match successes : 0
% 2.39/106.58 # Condensation attempts : 0
% 2.39/106.58 # Condensation successes : 0
% 2.39/106.58 # Termbank termtop insertions : 157494
% 2.39/106.58
% 2.39/106.58 # -------------------------------------------------
% 2.39/106.58 # User time : 0.353 s
% 2.39/106.58 # System time : 0.012 s
% 2.39/106.58 # Total time : 0.365 s
% 2.39/106.58 # Maximum resident set size: 23556 pages
% 2.39/106.58 # Running protocol protocol_eprover_f171197f65f27d1ba69648a20c844832c84a5dd7 for 23 seconds:
% 2.39/106.58
% 2.39/106.58 # Failure: Resource limit exceeded (time)
% 2.39/106.58 # OLD status Res
% 2.39/106.58 # Preprocessing time : 0.605 s
% 2.39/106.58 # Running protocol protocol_eprover_eb48853eb71ccd2a6fdade56c25b63f5692e1a0c for 23 seconds:
% 2.39/106.58
% 2.39/106.58 # Failure: Resource limit exceeded (time)
% 2.39/106.58 # OLD status Res
% 2.39/106.58 # Preprocessing time : 0.481 s
% 2.39/106.58 # Running protocol protocol_eprover_761a0d093d9701c0eed884aebb46468e8d439c31 for 23 seconds:
% 2.39/106.58 # SinE strategy is GSinE(CountFormulas,hypos,1.2,,,100,1.0)
% 2.39/106.58 # Preprocessing time : 0.217 s
% 2.39/106.58
% 2.39/106.58 # Failure: Out of unprocessed clauses!
% 2.39/106.58 # OLD status GaveUp
% 2.39/106.58 # Parsed axioms : 14793
% 2.39/106.58 # Removed by relevancy pruning/SinE : 14692
% 2.39/106.58 # Initial clauses : 104
% 2.39/106.58 # Removed in clause preprocessing : 4
% 2.39/106.58 # Initial clauses in saturation : 100
% 2.39/106.58 # Processed clauses : 731
% 2.39/106.58 # ...of these trivial : 39
% 2.39/106.58 # ...subsumed : 255
% 2.39/106.58 # ...remaining for further processing : 437
% 2.39/106.58 # Other redundant clauses eliminated : 1
% 2.39/106.58 # Clauses deleted for lack of memory : 0
% 2.39/106.58 # Backward-subsumed : 39
% 2.39/106.58 # Backward-rewritten : 4
% 2.39/106.58 # Generated clauses : 905
% 2.39/106.58 # ...of the previous two non-trivial : 641
% 2.39/106.58 # Contextual simplify-reflections : 171
% 2.39/106.58 # Paramodulations : 904
% 2.39/106.58 # Factorizations : 0
% 2.39/106.58 # Equation resolutions : 1
% 2.39/106.58 # Current number of processed clauses : 393
% 2.39/106.58 # Positive orientable unit clauses : 100
% 2.39/106.58 # Positive unorientable unit clauses: 0
% 2.39/106.58 # Negative unit clauses : 2
% 2.39/106.58 # Non-unit-clauses : 291
% 2.39/106.58 # Current number of unprocessed clauses: 0
% 2.39/106.58 # ...number of literals in the above : 0
% 2.39/106.58 # Current number of archived formulas : 0
% 2.39/106.58 # Current number of archived clauses : 43
% 2.39/106.58 # Clause-clause subsumption calls (NU) : 29173
% 2.39/106.58 # Rec. Clause-clause subsumption calls : 6909
% 2.39/106.58 # Non-unit clause-clause subsumptions : 465
% 2.39/106.58 # Unit Clause-clause subsumption calls : 752
% 2.39/106.58 # Rewrite failures with RHS unbound : 0
% 2.39/106.58 # BW rewrite match attempts : 17
% 2.39/106.58 # BW rewrite match successes : 4
% 2.39/106.58 # Condensation attempts : 0
% 2.39/106.58 # Condensation successes : 0
% 2.39/106.58 # Termbank termtop insertions : 127337
% 2.39/106.58
% 2.39/106.58 # -------------------------------------------------
% 2.39/106.58 # User time : 0.235 s
% 2.39/106.58 # System time : 0.014 s
% 2.39/106.58 # Total time : 0.249 s
% 2.39/106.58 # Maximum resident set size: 23012 pages
% 2.39/106.58 # Running protocol protocol_eprover_bb5e3cecdbc7660bd3a6f864cadb7769d8aea26a for 23 seconds:
% 2.39/106.58 # SinE strategy is GSinE(CountFormulas,hypos,1.1,,,500,1.0)
% 2.39/106.58 # Preprocessing time : 0.181 s
% 2.39/106.58
% 2.39/106.58 # Failure: Out of unprocessed clauses!
% 2.39/106.58 # OLD status GaveUp
% 2.39/106.58 # Parsed axioms : 14793
% 2.39/106.58 # Removed by relevancy pruning/SinE : 14671
% 2.39/106.58 # Initial clauses : 125
% 2.39/106.58 # Removed in clause preprocessing : 4
% 2.39/106.58 # Initial clauses in saturation : 121
% 2.39/106.58 # Processed clauses : 13497
% 2.39/106.58 # ...of these trivial : 1126
% 2.39/106.58 # ...subsumed : 6
% 2.39/106.58 # ...remaining for further processing : 12365
% 2.39/106.58 # Other redundant clauses eliminated : 1
% 2.39/106.58 # Clauses deleted for lack of memory : 2326
% 2.39/106.58 # Backward-subsumed : 0
% 2.39/106.58 # Backward-rewritten : 4
% 2.39/106.58 # Generated clauses : 18556
% 2.39/106.58 # ...of the previous two non-trivial : 15702
% 2.39/106.58 # Contextual simplify-reflections : 0
% 2.39/106.58 # Paramodulations : 18555
% 2.39/106.58 # Factorizations : 0
% 2.39/106.58 # Equation resolutions : 1
% 2.39/106.58 # Current number of processed clauses : 12360
% 2.39/106.58 # Positive orientable unit clauses : 3865
% 2.39/106.58 # Positive unorientable unit clauses: 0
% 2.39/106.58 # Negative unit clauses : 1
% 2.39/106.58 # Non-unit-clauses : 8494
% 2.39/106.58 # Current number of unprocessed clauses: 0
% 2.39/106.58 # ...number of literals in the above : 0
% 2.39/106.58 # Current number of archived formulas : 0
% 2.39/106.58 # Current number of archived clauses : 4
% 2.39/106.58 # Clause-clause subsumption calls (NU) : 4140336
% 2.39/106.58 # Rec. Clause-clause subsumption calls : 3448963
% 2.39/106.58 # Non-unit clause-clause subsumptions : 6
% 2.39/106.58 # Unit Clause-clause subsumption calls : 56327
% 2.39/106.58 # Rewrite failures with RHS unbound : 0
% 2.39/106.58 # BW rewrite match attempts : 948174
% 2.39/106.58 # BW rewrite match successes : 4
% 2.39/106.58 # Condensation attempts : 0
% 2.39/106.58 # Condensation successes : 0
% 2.39/106.58 # Termbank termtop insertions : 9917715
% 2.39/106.58
% 2.39/106.58 # -------------------------------------------------
% 2.39/106.58 # User time : 6.271 s
% 2.39/106.58 # System time : 0.161 s
% 2.39/106.58 # Total time : 6.432 s
% 2.39/106.58 # Maximum resident set size: 279004 pages
% 2.39/106.58 # Running protocol protocol_eprover_e252f7803940d118fa0ef69fc2319cb55aee23b9 for 23 seconds:
% 2.39/106.58
% 2.39/106.58 # Failure: Resource limit exceeded (time)
% 2.39/106.58 # OLD status Res
% 2.39/106.58 # SinE strategy is GSinE(CountFormulas,,1.4,,03,100,1.0)
% 2.39/106.58 # Preprocessing time : 0.174 s
% 2.39/106.58 # Running protocol protocol_eprover_b1d72019af42f5b571a6c0b233a5b6d1de064075 for 23 seconds:
% 2.39/106.58
% 2.39/106.58 # Failure: Resource limit exceeded (time)
% 2.39/106.58 # OLD status Res
% 2.39/106.58 # SinE strategy is GSinE(CountFormulas,hypos,1.5,,02,500,1.0)
% 2.39/106.58 # Preprocessing time : 0.228 s
% 2.39/106.58 # Running protocol protocol_eprover_e96ef4641ae500918cdd95fcfce21e29f2ac5eec for 23 seconds:
% 2.39/106.58 # SinE strategy is GSinE(CountFormulas,,6.0,,03,100,1.0)
% 2.39/106.58 # Preprocessing time : 0.226 s
% 2.39/106.58
% 2.39/106.58 # Failure: Out of unprocessed clauses!
% 2.39/106.58 # OLD status GaveUp
% 2.39/106.58 # Parsed axioms : 14793
% 2.39/106.58 # Removed by relevancy pruning/SinE : 14692
% 2.39/106.58 # Initial clauses : 153
% 2.39/106.58 # Removed in clause preprocessing : 4
% 2.39/106.58 # Initial clauses in saturation : 149
% 2.39/106.58 # Processed clauses : 1272
% 2.39/106.58 # ...of these trivial : 29
% 2.39/106.58 # ...subsumed : 63
% 2.39/106.58 # ...remaining for further processing : 1180
% 2.39/106.58 # Other redundant clauses eliminated : 0
% 2.39/106.58 # Clauses deleted for lack of memory : 0
% 2.39/106.58 # Backward-subsumed : 4
% 2.39/106.58 # Backward-rewritten : 20
% 2.39/106.58 # Generated clauses : 1468
% 2.39/106.58 # ...of the previous two non-trivial : 1123
% 2.39/106.58 # Contextual simplify-reflections : 78
% 2.39/106.58 # Paramodulations : 1468
% 2.39/106.58 # Factorizations : 0
% 2.39/106.58 # Equation resolutions : 0
% 2.39/106.58 # Current number of processed clauses : 1156
% 2.39/106.58 # Positive orientable unit clauses : 165
% 2.39/106.58 # Positive unorientable unit clauses: 0
% 2.39/106.58 # Negative unit clauses : 10
% 2.39/106.58 # Non-unit-clauses : 981
% 2.39/106.58 # Current number of unprocessed clauses: 0
% 2.39/106.58 # ...number of literals in the above : 0
% 2.39/106.58 # Current number of archived formulas : 0
% 2.39/106.58 # Current number of archived clauses : 24
% 2.39/106.58 # Clause-clause subsumption calls (NU) : 113097
% 2.39/106.58 # Rec. Clause-clause subsumption calls : 35373
% 2.39/106.58 # Non-unit clause-clause subsumptions : 109
% 2.39/106.58 # Unit Clause-clause subsumption calls : 5755
% 2.39/106.58 # Rewrite failures with RHS unbound : 0
% 2.39/106.58 # BW rewrite match attempts : 10
% 2.39/106.58 # BW rewrite match successes : 8
% 2.39/106.58 # Condensation attempts : 0
% 2.39/106.58 # Condensation successes : 0
% 2.39/106.58 # Termbank termtop insertions : 133195
% 2.39/106.58
% 2.39/106.58 # -------------------------------------------------
% 2.39/106.58 # User time : 0.304 s
% 2.39/106.58 # System time : 0.014 s
% 2.39/106.58 # Total time : 0.318 s
% 2.39/106.58 # Maximum resident set size: 24140 pages
% 2.39/106.58 # Running protocol protocol_eprover_1f734394cb6ce69b36c9826f6782d3567d6ecd6c for 23 seconds:
% 2.39/106.58 # SinE strategy is GSinE(CountFormulas,hypos,1.1,,02,20000,1.0)
% 2.39/106.58 # Preprocessing time : 0.156 s
% 2.39/106.58
% 2.39/106.58 # Failure: Out of unprocessed clauses!
% 2.39/106.58 # OLD status GaveUp
% 2.39/106.58 # Parsed axioms : 14793
% 2.39/106.58 # Removed by relevancy pruning/SinE : 14760
% 2.39/106.58 # Initial clauses : 36
% 2.39/106.58 # Removed in clause preprocessing : 4
% 2.39/106.58 # Initial clauses in saturation : 32
% 2.39/106.58 # Processed clauses : 179
% 2.39/106.58 # ...of these trivial : 7
% 2.39/106.58 # ...subsumed : 47
% 2.39/106.58 # ...remaining for further processing : 125
% 2.39/106.58 # Other redundant clauses eliminated : 0
% 2.39/106.58 # Clauses deleted for lack of memory : 0
% 2.39/106.58 # Backward-subsumed : 0
% 2.39/106.58 # Backward-rewritten : 14
% 2.39/106.58 # Generated clauses : 153
% 2.39/106.58 # ...of the previous two non-trivial : 147
% 2.39/106.58 # Contextual simplify-reflections : 0
% 2.39/106.58 # Paramodulations : 153
% 2.39/106.58 # Factorizations : 0
% 2.39/106.58 # Equation resolutions : 0
% 2.39/106.58 # Current number of processed clauses : 111
% 2.39/106.58 # Positive orientable unit clauses : 19
% 2.39/106.58 # Positive unorientable unit clauses: 0
% 2.39/106.58 # Negative unit clauses : 2
% 2.39/106.58 # Non-unit-clauses : 90
% 2.39/106.58 # Current number of unprocessed clauses: 0
% 2.39/106.58 # ...number of literals in the above : 0
% 2.39/106.58 # Current number of archived formulas : 0
% 2.39/106.58 # Current number of archived clauses : 14
% 2.39/106.58 # Clause-clause subsumption calls (NU) : 417
% 2.39/106.58 # Rec. Clause-clause subsumption calls : 235
% 2.39/106.58 # Non-unit clause-clause subsumptions : 47
% 2.39/106.58 # Unit Clause-clause subsumption calls : 9
% 2.39/106.58 # Rewrite failures with RHS unbound : 0
% 2.39/106.58 # BW rewrite match attempts : 7
% 2.39/106.58 # BW rewrite match successes : 7
% 2.39/106.58 # Condensation attempts : 0
% 2.39/106.58 # Condensation successes : 0
% 2.39/106.58 # Termbank termtop insertions : 112451
% 2.39/106.58
% 2.39/106.58 # -------------------------------------------------
% 2.39/106.58 # User time : 0.153 s
% 2.39/106.58 # System time : 0.007 s
% 2.39/106.58 # Total time : 0.160 s
% 2.39/106.58 # Maximum resident set size: 22568 pages
% 2.39/106.58 # Running protocol protocol_eprover_e9eb28a402764e1f99b41605245cd0a359f475fb for 23 seconds:
% 2.39/106.58 # Preprocessing time : 0.361 s
% 2.39/106.58
% 2.39/106.58 # Proof found!
% 2.39/106.58 # SZS status Theorem
% 2.39/106.58 # SZS output start CNFRefutation
% See solution above
% 2.39/106.58 # Proof object total steps : 49
% 2.39/106.58 # Proof object clause steps : 32
% 2.39/106.58 # Proof object formula steps : 17
% 2.39/106.58 # Proof object conjectures : 8
% 2.39/106.58 # Proof object clause conjectures : 5
% 2.39/106.58 # Proof object formula conjectures : 3
% 2.39/106.58 # Proof object initial clauses used : 12
% 2.39/106.58 # Proof object initial formulas used : 8
% 2.39/106.58 # Proof object generating inferences : 15
% 2.39/106.58 # Proof object simplifying inferences : 22
% 2.39/106.58 # Training examples: 0 positive, 0 negative
% 2.39/106.58 # Parsed axioms : 14793
% 2.39/106.58 # Removed by relevancy pruning/SinE : 0
% 2.39/106.58 # Initial clauses : 15984
% 2.39/106.58 # Removed in clause preprocessing : 63
% 2.39/106.58 # Initial clauses in saturation : 15921
% 2.39/106.58 # Processed clauses : 20391
% 2.39/106.58 # ...of these trivial : 4003
% 2.39/106.58 # ...subsumed : 624
% 2.39/106.58 # ...remaining for further processing : 15764
% 2.39/106.58 # Other redundant clauses eliminated : 3181
% 2.39/106.58 # Clauses deleted for lack of memory : 98091
% 2.39/106.58 # Backward-subsumed : 644
% 2.39/106.58 # Backward-rewritten : 2662
% 2.39/106.58 # Generated clauses : 732452
% 2.39/106.58 # ...of the previous two non-trivial : 727568
% 2.39/106.58 # Contextual simplify-reflections : 0
% 2.39/106.58 # Paramodulations : 728906
% 2.39/106.58 # Factorizations : 11
% 2.39/106.58 # Equation resolutions : 3296
% 2.39/106.58 # Current number of processed clauses : 12249
% 2.39/106.58 # Positive orientable unit clauses : 10018
% 2.39/106.58 # Positive unorientable unit clauses: 1
% 2.39/106.58 # Negative unit clauses : 22
% 2.39/106.58 # Non-unit-clauses : 2208
% 2.39/106.58 # Current number of unprocessed clauses: 59024
% 2.39/106.58 # ...number of literals in the above : 80799
% 2.39/106.58 # Current number of archived formulas : 0
% 2.39/106.58 # Current number of archived clauses : 3489
% 2.39/106.58 # Clause-clause subsumption calls (NU) : 722184
% 2.39/106.58 # Rec. Clause-clause subsumption calls : 161037
% 2.39/106.58 # Non-unit clause-clause subsumptions : 481
% 2.39/106.58 # Unit Clause-clause subsumption calls : 1143471
% 2.39/106.58 # Rewrite failures with RHS unbound : 12839
% 2.39/106.58 # BW rewrite match attempts : 38554
% 2.39/106.58 # BW rewrite match successes : 13477
% 2.39/106.58 # Condensation attempts : 0
% 2.39/106.58 # Condensation successes : 0
% 2.39/106.58 # Termbank termtop insertions : 4818608
% 2.39/106.58
% 2.39/106.58 # -------------------------------------------------
% 2.39/106.58 # User time : 4.718 s
% 2.39/106.58 # System time : 0.146 s
% 2.39/106.58 # Total time : 4.864 s
% 2.39/106.58 # Maximum resident set size: 219584 pages
% 2.39/117.08 eprover: CPU time limit exceeded, terminating
% 2.39/117.08 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/117.08 eprover: No such file or directory
% 2.39/117.08 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/117.08 eprover: No such file or directory
% 2.39/117.09 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/117.09 eprover: No such file or directory
% 2.39/117.09 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/117.09 eprover: No such file or directory
% 2.39/117.09 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/117.09 eprover: No such file or directory
% 2.39/117.10 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/117.10 eprover: No such file or directory
% 2.39/117.10 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/117.10 eprover: No such file or directory
% 2.39/118.05 eprover: CPU time limit exceeded, terminating
% 2.39/118.06 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 2.39/118.06 eprover: No such file or directory
% 2.39/118.06 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 2.39/118.06 eprover: No such file or directory
% 2.39/118.07 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 2.39/118.07 eprover: No such file or directory
% 2.39/118.07 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 2.39/118.07 eprover: No such file or directory
% 2.39/118.08 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p.mepo_128.in
% 2.39/118.08 eprover: No such file or directory
% 2.39/118.40 eprover: CPU time limit exceeded, terminating
% 2.39/118.42 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/118.42 eprover: No such file or directory
% 2.39/118.43 eprover: Cannot stat file /export/starexec/sandbox/solver/bin/../tmp/theBenchmark.p
% 2.39/118.43 eprover: No such file or directory
%------------------------------------------------------------------------------