tptp/reports/report[ap1].html

<!DOCTYPE html
	PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
	 "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en-US" xml:lang="en-US">
<head>
<title>System Results</title>
<meta name="ROBOTS" content="INDEX,NOFOLLOW" />
<script type="text/javascript">//<![CDATA[

  var tstp_dump;
  function openSoTSTP (dump) {   
    var tstp_url = 'http://www.tptp.org/cgi-bin/SystemOnTSTP';
    var tstp_browser = window.open(tstp_url, '_blank');
    tstp_dump = dump;
  }
  function getTSTPDump () {
    return tstp_dump;
  }

//]]></script>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1" />
</head>
<body>

% SZS start RequiredInformation<BR>
% Congratulations - you have become a registered power user of SystemOnTPTP, at IP address 191.6.38.118.<BR>
% Please consider donating to the TPTP project - see www.tptp.org for details.<BR>
% When you donate this message will disappear.<BR>
% If you do not donate a random delay might be added to your processing time.<BR>
% SZS end RequiredInformation<BR>
<PRE>
Getting system recommendations for generic problem /tmp/qZi2mWPEWe/SOT_MiFT3j
This is a FOF_THM_RFO_SEQ report.
Vampire---THF-4.5    recommended  0.95
Vampire---TF1-4.5    recommended  0.95
Vampire---4.5        recommended  0.95
Vampire---SAT-4.5    recommended  0.95
ET---2.0             recommended  0.80
E---2.5              recommended  0.78
E---FNT-2.5          recommended  0.78
CSE_E---1.0          recommended  0.76
E---FNT-2.5          recommended  0.74
Isabelle---2TH0      recommended  0.69
Isabelle---2TF0      recommended  0.69
Isabelle---2FOF      recommended  0.69
Isabelle---2016      recommended  0.69
Isabelle-HOT---2016  recommended  0.68
CVC4---1.7           recommended  0.68
CVC4---SAT-1.7       recommended  0.68
Leo-III---1.4        recommended  0.61
Vampire---THF-4.5    recommended  0.59
Vampire---TF1-4.5    recommended  0.59
Vampire---SAT-4.5    recommended  0.59
iProver---3.0        recommended  0.58
iProver---SAT-3.0    recommended  0.58
Fampire---1.3        recommended  0.57
SInE---0.4           recommended  0.53
iProver---SAT-3.0    recommended  0.52
ePrincess---1.0      recommended  0.50
Princess---170717    recommended  0.48
SPASS---3.9          recommended  0.48
Z3---4.4.1           recommended  0.46
Zipperpin---1.5      recommended  0.40
CVC4---SAT-1.7       recommended  0.40
Prover9---1109a      recommended  0.39
Equinox---6.0.1a     recommended  0.37
LEO-II---1.7.0       recommended  0.35
nanoCoP---1.1        recommended  0.34
Muscadet---4.5       recommended  0.25
Twee---2.2           recommended  0.23
Metis---2.4          recommended  0.23
Geo-III---2018C      recommended  0.18
iProverMo---2.5-0.1  recommended  0.14
Beagle---0.9.47      subsumed     0.41
leanCoP---2.2        subsumed     0.36
E-Darwin---1.5       subsumed     0.31
CSE---1.0            subsumed     0.28
Darwin---1.4.5       subsumed     0.28
Bliksem---1.12       subsumed     0.21
Zenon---0.7.1        subsumed     0.16
ZenonModulo---0.4.2  subsumed     0.15
SOS---2.0            subsumed     0.11
Otter---3.3          subsumed     0.04
This is a FOF_CSA_RFO_SEQ report.
Vampire---THF-4.5    recommended  0.98
Vampire---TF1-4.5    recommended  0.98
Vampire---SAT-4.5    recommended  0.98
Paradox---4.0        recommended  0.60
Nitpick---2016       subsumed     0.55
DarwinFM---1.4.5     subsumed     0.43
CVC4---SAT-1.7       subsumed     0.40
Vampire---THF-4.5    subsumed     0.34
Vampire---TF1-4.5    subsumed     0.34
Vampire---4.5        subsumed     0.34
Vampire---SAT-4.5    subsumed     0.34
E---2.5              subsumed     0.34
E---FNT-2.5          subsumed     0.34
E---FNT-2.5          subsumed     0.34
iProver---SAT-3.0    subsumed     0.32
Metis---2.4          subsumed     0.32
SPASS---3.9          subsumed     0.28
Beagle---0.9.47      subsumed     0.26
Geo-III---2018C      subsumed     0.25
Z3---4.4.1           subsumed     0.25
Princess---170717    subsumed     0.25
Equinox---6.0.1a     subsumed     0.19
iProver---3.0        subsumed     0.11
iProver---SAT-3.0    subsumed     0.11
Darwin---1.4.5       subsumed     0.06
E-Darwin---1.5       subsumed     0.04
Check if we can use Vampire,THF-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,TF1-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,SAT-4.5
Vampire---SAT-4.5 can be used
Check if we can use ET,2.0
Check if we can use E,2.5
E---FNT-2.5 can be used
Check if we can use E,FNT-2.5
E---FNT-2.5 can be used
Check if we can use CSE_E,1.0
CSE_E---1.0 can be used
Check if we can use E,FNT-2.5
E---FNT-2.5 can be used
Check if we can use Isabelle,2TH0
Isabelle---2016 can be used
Check if we can use Isabelle,2TF0
Isabelle---2016 can be used
Check if we can use Isabelle,2FOF
Isabelle---2016 can be used
Check if we can use Isabelle,2016
Isabelle---2016 can be used
Check if we can use Isabelle-HOT,2016
Isabelle-HOT---2016 can be used
Check if we can use CVC4,1.7
CVC4---SAT-1.7 can be used
Check if we can use CVC4,SAT-1.7
CVC4---SAT-1.7 can be used
Check if we can use Leo-III,1.4
Leo-III---1.4 can be used
Check if we can use Vampire,THF-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,TF1-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,SAT-4.5
Vampire---SAT-4.5 can be used
Check if we can use iProver,3.0
iProver---SAT-3.0 can be used
Check if we can use iProver,SAT-3.0
iProver---SAT-3.0 can be used
Check if we can use Fampire,1.3
Check if we can use SInE,0.4
Check if we can use iProver,SAT-3.0
iProver---SAT-3.0 can be used
Check if we can use ePrincess,1.0
Check if we can use Princess,170717
Princess---170717 can be used
Check if we can use SPASS,3.9
SPASS---3.9 can be used
Check if we can use Z3,4.4.1
Z3---4.4.1 can be used
Check if we can use Zipperpin,1.5
Check if we can use CVC4,SAT-1.7
CVC4---SAT-1.7 can be used
Check if we can use Prover9,1109a
Prover9---1109a can be used
Check if we can use Equinox,6.0.1a
Equinox---6.0.1a can be used
Check if we can use LEO-II,1.7.0
LEO-II---1.7.0 can be used
Check if we can use nanoCoP,1.1
nanoCoP---1.1 can be used
Check if we can use Muscadet,4.5
Muscadet---4.5 can be used
Check if we can use Twee,2.2
Twee---2.2 can be used
Check if we can use Metis,2.4
Metis---2.4 can be used
Check if we can use Geo-III,2018C
Geo-III---2018C can be used
Check if we can use iProverMo,2.5-0.1
iProverMo---2.5-0.1 can be used
Check if we can use Beagle,0.9.47
Check if we can use leanCoP,2.2
leanCoP---2.2 can be used
Check if we can use E-Darwin,1.5
E-Darwin---1.5 can be used
Check if we can use CSE,1.0
CSE---1.0 can be used
Check if we can use Darwin,1.4.5
Darwin---1.4.5 can be used
Check if we can use Bliksem,1.12
Bliksem---1.12 can be used
Check if we can use Zenon,0.7.1
Zenon---0.7.1 can be used
Check if we can use ZenonModulo,0.4.2
Check if we can use SOS,2.0
SOS---2.0 can be used
Check if we can use Otter,3.3
Otter---3.3 can be used
Check if we can use Vampire,THF-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,TF1-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,SAT-4.5
Vampire---SAT-4.5 can be used
Check if we can use Paradox,4.0
Paradox---4.0 can be used
Check if we can use Nitpick,2016
Nitpick---2016 can be used
Check if we can use DarwinFM,1.4.5
DarwinFM---1.4.5 can be used
Check if we can use CVC4,SAT-1.7
CVC4---SAT-1.7 can be used
Check if we can use Vampire,THF-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,TF1-4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,4.5
Vampire---SAT-4.5 can be used
Check if we can use Vampire,SAT-4.5
Vampire---SAT-4.5 can be used
Check if we can use E,2.5
E---FNT-2.5 can be used
Check if we can use E,FNT-2.5
E---FNT-2.5 can be used
Check if we can use E,FNT-2.5
E---FNT-2.5 can be used
Check if we can use iProver,SAT-3.0
iProver---SAT-3.0 can be used
Check if we can use Metis,2.4
Metis---2.4 can be used
Check if we can use SPASS,3.9
SPASS---3.9 can be used
Check if we can use Beagle,0.9.47
Check if we can use Geo-III,2018C
Geo-III---2018C can be used
Check if we can use Z3,4.4.1
Z3---4.4.1 can be used
Check if we can use Princess,170717
Princess---170717 can be used
Check if we can use Equinox,6.0.1a
Equinox---6.0.1a can be used
Check if we can use iProver,3.0
iProver---SAT-3.0 can be used
Check if we can use iProver,SAT-3.0
iProver---SAT-3.0 can be used
Check if we can use Darwin,1.4.5
Darwin---1.4.5 can be used
Check if we can use E-Darwin,1.5
E-Darwin---1.5 can be used
Vampire---SAT-4.5 will be used
Vampire---SAT-4.5 will be used
Vampire---SAT-4.5 will be used
Vampire---SAT-4.5 will be used
E---FNT-2.5 will be used
E---FNT-2.5 will be used
CSE_E---1.0 will be used
E---FNT-2.5 will be used
Isabelle---2016 will be used
Isabelle---2016 will be used
Vampire---SAT-4.5 is given 30 seconds in -cS mode
Vampire---SAT-4.5 is given 30 seconds in -cS mode
Vampire---SAT-4.5 is given 30 seconds in -cS mode
Vampire---SAT-4.5 is given 30 seconds in -cS mode
E---FNT-2.5 is given 30 seconds in -cS mode
E---FNT-2.5 is given 30 seconds in -cS mode
CSE_E---1.0 is given 30 seconds in -cS mode
E---FNT-2.5 is given 30 seconds in -cS mode
Isabelle---2016 is given 30 seconds in -cS mode
Isabelle---2016 is given 30 seconds in -cS mode
Vampire---SAT-4.5 has started (PID 107033)
Vampire---SAT-4.5 has started (PID 107034)
Vampire---SAT-4.5 has started (PID 107035)
Vampire---SAT-4.5 has started (PID 107036)
E---FNT-2.5 has started (PID 107037)
E---FNT-2.5 has started (PID 107038)
CSE_E---1.0 has started (PID 107039)
E---FNT-2.5 has started (PID 107040)
Isabelle---2016 has started (PID 107041)
Isabelle---2016 has started (PID 107042)
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 Vampire---SAT-4.5  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 Vampire---SAT-4.5  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 Vampire---SAT-4.5  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 Vampire---SAT-4.5  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 E---FNT-2.5  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 E---FNT-2.5  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 CSE_E---1.0  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 E---FNT-2.5  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 Isabelle---2016  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
Running /home/tptp/SystemExecution/SystemOnTPTP -q01 Isabelle---2016  30  /tmp/qZi2mWPEWe/SOT_MiFT3j
% START OF SYSTEM OUTPUT
% START OF SYSTEM OUTPUT
% ott+11_3_aac=none:afr=on:afp=4000:afq=1.4:amm=off:anc=all:bs=unit_only:bsr=on:bce=on:fde=unused:irw=on:nm=64:newcnf=on:nwc=1:nicw=on:sac=on:sp=reverse_arity:uhcvi=on_31 on SOT_MiFT
% Refutation found. Thanks to Tanya!
% START OF SYSTEM OUTPUT
% SZS status Theorem for SOT_MiFT
% SZS output start Proof for SOT_MiFT
fof(f211,plain,(
% START OF SYSTEM OUTPUT
  $false),
  inference(avatar_sat_refutation,[],[f125,f129,f153,f210])).
fof(f210,plain,(
  ~spl16_1 | ~spl16_2 | ~spl16_8),
  inference(avatar_contradiction_clause,[],[f209])).
# Version: 2.4dev006
fof(f209,plain,(
  $false | (~spl16_1 | ~spl16_2 | ~spl16_8)),
  inference(subsumption_resolution,[],[f128,f208])).
fof(f208,plain,(
# Trying AutoSched0 for 14 seconds
  ( ! [X0] : (~iof(X0,sK0)) ) | (~spl16_1 | ~spl16_8)),
  inference(resolution,[],[f152,f124])).
fof(f124,plain,(
  individual(sK0) | ~spl16_1),
# AutoSched0-Mode selected heuristic G_E___208_C02CMA_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
  inference(avatar_component_clause,[],[f123])).
fof(f123,plain,(
# and selection function SelectComplexExceptUniqMaxHorn.
  spl16_1 <=> individual(sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl16_1])])).
fof(f152,plain,(
#
  ( ! [X0,X1] : (~individual(X0) | ~iof(X1,X0)) ) | ~spl16_8),
  inference(avatar_component_clause,[],[f151])).
fof(f151,plain,(
  spl16_8 <=> ! [X1,X0] : (~iof(X1,X0) | ~individual(X0))),
# Preprocessing time       : 0.018 s
  introduced(avatar_definition,[new_symbols(naming,[spl16_8])])).
fof(f128,plain,(
  iof(sK1,sK0) | ~spl16_2),
# Presaturation interreduction done
  inference(avatar_component_clause,[],[f127])).
fof(f127,plain,(
  spl16_2 <=> iof(sK1,sK0)),

  introduced(avatar_definition,[new_symbols(naming,[spl16_2])])).
fof(f153,plain,(
# Proof found!
  spl16_8),
  inference(avatar_split_clause,[],[f80,f151])).
fof(f80,plain,(
  ( ! [X0,X1] : (~iof(X1,X0) | ~individual(X0)) )),
# SZS status Theorem
  inference(cnf_transformation,[],[f49])).
fof(f49,plain,(
# SZS output start CNFRefutation
  ! [X0] : (individual(X0) <=> ! [X1] : ~iof(X1,X0))),
fof(t7_ap1, conjecture, ~(?[X7, X8]:(individual(X7)&iof(X8,X7))), file('/tmp/qZi2mWPEWe/SOT_MiFT3j', t7_ap1)).
  inference(ennf_transformation,[],[f2])).
fof(a2, axiom, ![X1]:(individual(X1)<=>~(?[X2]:iof(X2,X1))), file('/tmp/qZi2mWPEWe/SOT_MiFT3j', a2)).
fof(f2,axiom,(
fof(c_0_2, negated_conjecture, ~(~(?[X7, X8]:(individual(X7)&iof(X8,X7)))), inference(assume_negation,[status(cth)],[t7_ap1])).
  ! [X0] : (individual(X0) <=> ~? [X1] : iof(X1,X0))),
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',a2)).
fof(c_0_3, plain, ![X13, X14, X15]:((~individual(X13)|~iof(X14,X13))&(iof(esk1_1(X15),X15)|individual(X15))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[a2])])])])])).
fof(f129,plain,(
fof(c_0_4, negated_conjecture, (individual(esk25_0)&iof(esk26_0,esk25_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])).
  spl16_2),
cnf(c_0_5, plain, (~individual(X1)|~iof(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
cnf(c_0_6, negated_conjecture, (iof(esk26_0,esk25_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
  inference(avatar_split_clause,[],[f58,f127])).
fof(f58,plain,(
cnf(c_0_7, negated_conjecture, (individual(esk25_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_8, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5, c_0_6]), c_0_7])]), ['proof']).
  iof(sK1,sK0)),
  inference(cnf_transformation,[],[f27])).
# SZS output end CNFRefutation
fof(f27,plain,(
# Proof object total steps             : 9
  ? [X0,X1] : (iof(X1,X0) & individual(X0))),
# Proof object clause steps            : 4
  inference(flattening,[],[f26])).
# Proof object formula steps           : 5
# Proof object conjectures             : 6
fof(f26,plain,(
  ~~? [X0,X1] : (iof(X1,X0) & individual(X0))),
# Proof object clause conjectures      : 3
  inference(rectify,[],[f25])).
# Proof object formula conjectures     : 3
fof(f25,negated_conjecture,(
# Proof object initial clauses used    : 3
  ~~? [X6,X7] : (iof(X7,X6) & individual(X6))),
# Proof object initial formulas used   : 2
  inference(negated_conjecture,[],[f24])).
# Proof object generating inferences   : 1
fof(f24,conjecture,(
# Proof object simplifying inferences  : 2
  ~? [X6,X7] : (iof(X7,X6) & individual(X6))),
# Training examples: 0 positive, 0 negative
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',t7_ap1)).
# Parsed axioms                        : 24
# Removed by relevancy pruning/SinE    : 0
fof(f125,plain,(
# Initial clauses                      : 88
  spl16_1),
# Removed in clause preprocessing      : 5
  inference(avatar_split_clause,[],[f57,f123])).
fof(f57,plain,(
# Initial clauses in saturation        : 83
  individual(sK0)),
# Processed clauses                    : 93
  inference(cnf_transformation,[],[f27])).
# ...of these trivial                  : 0
% SZS output end Proof for SOT_MiFT
# ...subsumed                          : 0
# ...remaining for further processing  : 93
% ------------------------------
% Version: Vampire 4.4.0 (commit 4fef31f on 2020-05-01 13:38:24 +0200)
# Other redundant clauses eliminated   : 7
% Termination reason: Refutation
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0

% Memory used [KB]: 5373
# Backward-rewritten                   : 0
# Generated clauses                    : 8
% Time elapsed: 0.007 s
# ...of the previous two non-trivial   : 7
% ------------------------------
% ------------------------------
# Contextual simplify-reflections      : 13
# Paramodulations                      : 1
% Success in time 0.051 s
# Factorizations                       : 0
# Equation resolutions                 : 7
# Propositional unsat checks           : 0
#    Propositional check models        : 0
#    Propositional check unsatisfiable : 0
#    Propositional clauses             : 0
#    Propositional clauses after purity: 0
#    Propositional unsat core size     : 0
#    Propositional preprocessing time  : 0.000
#    Propositional encoding time       : 0.000
#    Propositional solver time         : 0.000
#    Success case prop preproc time    : 0.000
#    Success case prop encoding time   : 0.000
#    Success case prop solver time     : 0.000
# Current number of processed clauses  : 3
#    Positive orientable unit clauses  : 2
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 0
#    Non-unit-clauses                  : 1
# Current number of unprocessed clauses: 80
# ...number of literals in the above   : 227
# Current number of archived formulas  : 0
# Current number of archived clauses   : 84
# Clause-clause subsumption calls (NU) : 2560
# Rec. Clause-clause subsumption calls : 1796
# Non-unit clause-clause subsumptions  : 13
# Unit Clause-clause subsumption calls : 5
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 0
# BW rewrite match successes           : 0
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 5838

# -------------------------------------------------
# User time                : 0.019 s
# System time              : 0.006 s
# Total time               : 0.025 s
# Maximum resident set size: 1608 pages
% START OF SYSTEM OUTPUT
# Version: 2.4dev006
# Trying AutoSched0 for 14 seconds
# AutoSched0-Mode selected heuristic G_E___208_C02CMA_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
# and selection function SelectComplexExceptUniqMaxHorn.
#
# Preprocessing time       : 0.016 s
# Presaturation interreduction done

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(t7_ap1, conjecture, ~(?[X7, X8]:(individual(X7)&iof(X8,X7))), file('/tmp/qZi2mWPEWe/SOT_MiFT3j', t7_ap1)).
fof(a2, axiom, ![X1]:(individual(X1)<=>~(?[X2]:iof(X2,X1))), file('/tmp/qZi2mWPEWe/SOT_MiFT3j', a2)).
fof(c_0_2, negated_conjecture, ~(~(?[X7, X8]:(individual(X7)&iof(X8,X7)))), inference(assume_negation,[status(cth)],[t7_ap1])).
fof(c_0_3, plain, ![X13, X14, X15]:((~individual(X13)|~iof(X14,X13))&(iof(esk1_1(X15),X15)|individual(X15))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[a2])])])])])).
fof(c_0_4, negated_conjecture, (individual(esk25_0)&iof(esk26_0,esk25_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])).
cnf(c_0_5, plain, (~individual(X1)|~iof(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
cnf(c_0_6, negated_conjecture, (iof(esk26_0,esk25_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_7, negated_conjecture, (individual(esk25_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_8, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5, c_0_6]), c_0_7])]), ['proof']).
# SZS output end CNFRefutation
# Proof object total steps             : 9
# Proof object clause steps            : 4
# Proof object formula steps           : 5
# Proof object conjectures             : 6
# Proof object clause conjectures      : 3
# Proof object formula conjectures     : 3
# Proof object initial clauses used    : 3
# Proof object initial formulas used   : 2
# Proof object generating inferences   : 1
# Proof object simplifying inferences  : 2
# Training examples: 0 positive, 0 negative
# Parsed axioms                        : 24
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 88
# Removed in clause preprocessing      : 5
# Initial clauses in saturation        : 83
# Processed clauses                    : 93
# ...of these trivial                  : 0
# ...subsumed                          : 0
# ...remaining for further processing  : 93
# Other redundant clauses eliminated   : 7
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0
# Backward-rewritten                   : 0
# Generated clauses                    : 8
# ...of the previous two non-trivial   : 7
# Contextual simplify-reflections      : 13
# Paramodulations                      : 1
# Factorizations                       : 0
# Equation resolutions                 : 7
# Propositional unsat checks           : 0
#    Propositional check models        : 0
#    Propositional check unsatisfiable : 0
#    Propositional clauses             : 0
#    Propositional clauses after purity: 0
#    Propositional unsat core size     : 0
#    Propositional preprocessing time  : 0.000
#    Propositional encoding time       : 0.000
#    Propositional solver time         : 0.000
#    Success case prop preproc time    : 0.000
#    Success case prop encoding time   : 0.000
#    Success case prop solver time     : 0.000
# Current number of processed clauses  : 3
#    Positive orientable unit clauses  : 2
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 0
#    Non-unit-clauses                  : 1
# Current number of unprocessed clauses: 80
# ...number of literals in the above   : 227
# Current number of archived formulas  : 0
# Current number of archived clauses   : 84
# Clause-clause subsumption calls (NU) : 2560
# Rec. Clause-clause subsumption calls : 1796
# Non-unit clause-clause subsumptions  : 13
# Unit Clause-clause subsumption calls : 5
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 0
# BW rewrite match successes           : 0
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 5838

# -------------------------------------------------
# User time                : 0.019 s
# System time              : 0.006 s
# Total time               : 0.025 s
# Maximum resident set size: 1612 pages
% START OF SYSTEM OUTPUT
% START OF SYSTEM OUTPUT
% START OF SYSTEM OUTPUT
% START OF SYSTEM OUTPUT
% START OF SYSTEM OUTPUT
# Version: 2.4dev006
# Trying AutoSched0 for 14 seconds
% ott+11_3_aac=none:afr=on:afp=4000:afq=1.4:amm=off:anc=all:bs=unit_only:bsr=on:bce=on:fde=unused:irw=on:nm=64:newcnf=on:nwc=1:nicw=on:sac=on:sp=reverse_arity:uhcvi=on_31 on SOT_MiFT
% Refutation found. Thanks to Tanya!
% SZS status Theorem for SOT_MiFT
% SZS output start Proof for SOT_MiFT
fof(f211,plain,(
  $false),
  inference(avatar_sat_refutation,[],[f125,f129,f153,f210])).
fof(f210,plain,(
  ~spl16_1 | ~spl16_2 | ~spl16_8),
  inference(avatar_contradiction_clause,[],[f209])).
fof(f209,plain,(
  $false | (~spl16_1 | ~spl16_2 | ~spl16_8)),
  inference(subsumption_resolution,[],[f128,f208])).
fof(f208,plain,(
  ( ! [X0] : (~iof(X0,sK0)) ) | (~spl16_1 | ~spl16_8)),
  inference(resolution,[],[f152,f124])).
fof(f124,plain,(
  individual(sK0) | ~spl16_1),
  inference(avatar_component_clause,[],[f123])).
fof(f123,plain,(
  spl16_1 <=> individual(sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl16_1])])).
fof(f152,plain,(
  ( ! [X0,X1] : (~individual(X0) | ~iof(X1,X0)) ) | ~spl16_8),
  inference(avatar_component_clause,[],[f151])).
fof(f151,plain,(
  spl16_8 <=> ! [X1,X0] : (~iof(X1,X0) | ~individual(X0))),
  introduced(avatar_definition,[new_symbols(naming,[spl16_8])])).
fof(f128,plain,(
  iof(sK1,sK0) | ~spl16_2),
  inference(avatar_component_clause,[],[f127])).
fof(f127,plain,(
  spl16_2 <=> iof(sK1,sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl16_2])])).
fof(f153,plain,(
  spl16_8),
  inference(avatar_split_clause,[],[f80,f151])).
fof(f80,plain,(
  ( ! [X0,X1] : (~iof(X1,X0) | ~individual(X0)) )),
  inference(cnf_transformation,[],[f49])).
fof(f49,plain,(
  ! [X0] : (individual(X0) <=> ! [X1] : ~iof(X1,X0))),
  inference(ennf_transformation,[],[f2])).
fof(f2,axiom,(
  ! [X0] : (individual(X0) <=> ~? [X1] : iof(X1,X0))),
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',a2)).
fof(f129,plain,(
  spl16_2),
  inference(avatar_split_clause,[],[f58,f127])).
fof(f58,plain,(
  iof(sK1,sK0)),
  inference(cnf_transformation,[],[f27])).
fof(f27,plain,(
  ? [X0,X1] : (iof(X1,X0) & individual(X0))),
  inference(flattening,[],[f26])).
fof(f26,plain,(
  ~~? [X0,X1] : (iof(X1,X0) & individual(X0))),
  inference(rectify,[],[f25])).
fof(f25,negated_conjecture,(
  ~~? [X6,X7] : (iof(X7,X6) & individual(X6))),
  inference(negated_conjecture,[],[f24])).
fof(f24,conjecture,(
  ~? [X6,X7] : (iof(X7,X6) & individual(X6))),
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',t7_ap1)).
fof(f125,plain,(
  spl16_1),
  inference(avatar_split_clause,[],[f57,f123])).
fof(f57,plain,(
  individual(sK0)),
  inference(cnf_transformation,[],[f27])).
% SZS output end Proof for SOT_MiFT
% ------------------------------
% Version: Vampire 4.4.0 (commit 4fef31f on 2020-05-01 13:38:24 +0200)
% Termination reason: Refutation

% Memory used [KB]: 5373
% Time elapsed: 0.008 s
% ------------------------------
% ------------------------------
% Success in time 0.053 s
# AutoSched0-Mode selected heuristic G_E___208_C02CMA_F1_SE_CS_SP_PS_S5PRR_RG_S04AN
# and selection function SelectComplexExceptUniqMaxHorn.
#
# Preprocessing time       : 0.017 s
# Presaturation interreduction done

# Proof found!
# SZS status Theorem
# SZS output start CNFRefutation
fof(t7_ap1, conjecture, ~(?[X7, X8]:(individual(X7)&iof(X8,X7))), file('/tmp/qZi2mWPEWe/SOT_MiFT3j', t7_ap1)).
fof(a2, axiom, ![X1]:(individual(X1)<=>~(?[X2]:iof(X2,X1))), file('/tmp/qZi2mWPEWe/SOT_MiFT3j', a2)).
fof(c_0_2, negated_conjecture, ~(~(?[X7, X8]:(individual(X7)&iof(X8,X7)))), inference(assume_negation,[status(cth)],[t7_ap1])).
fof(c_0_3, plain, ![X13, X14, X15]:((~individual(X13)|~iof(X14,X13))&(iof(esk1_1(X15),X15)|individual(X15))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[a2])])])])])).
fof(c_0_4, negated_conjecture, (individual(esk25_0)&iof(esk26_0,esk25_0)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])).
cnf(c_0_5, plain, (~individual(X1)|~iof(X2,X1)), inference(split_conjunct,[status(thm)],[c_0_3])).
cnf(c_0_6, negated_conjecture, (iof(esk26_0,esk25_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_7, negated_conjecture, (individual(esk25_0)), inference(split_conjunct,[status(thm)],[c_0_4])).
cnf(c_0_8, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5, c_0_6]), c_0_7])]), ['proof']).
# SZS output end CNFRefutation
# Proof object total steps             : 9
# Proof object clause steps            : 4
# Proof object formula steps           : 5
# Proof object conjectures             : 6
# Proof object clause conjectures      : 3
# Proof object formula conjectures     : 3
# Proof object initial clauses used    : 3
# Proof object initial formulas used   : 2
# Proof object generating inferences   : 1
# Proof object simplifying inferences  : 2
# Training examples: 0 positive, 0 negative
# Parsed axioms                        : 24
# Removed by relevancy pruning/SinE    : 0
# Initial clauses                      : 88
# Removed in clause preprocessing      : 5
# Initial clauses in saturation        : 83
# Processed clauses                    : 93
# ...of these trivial                  : 0
# ...subsumed                          : 0
# ...remaining for further processing  : 93
# Other redundant clauses eliminated   : 7
# Clauses deleted for lack of memory   : 0
# Backward-subsumed                    : 0
# Backward-rewritten                   : 0
# Generated clauses                    : 8
# ...of the previous two non-trivial   : 7
# Contextual simplify-reflections      : 13
# Paramodulations                      : 1
# Factorizations                       : 0
# Equation resolutions                 : 7
# Propositional unsat checks           : 0
#    Propositional check models        : 0
#    Propositional check unsatisfiable : 0
#    Propositional clauses             : 0
#    Propositional clauses after purity: 0
#    Propositional unsat core size     : 0
#    Propositional preprocessing time  : 0.000
#    Propositional encoding time       : 0.000
#    Propositional solver time         : 0.000
#    Success case prop preproc time    : 0.000
#    Success case prop encoding time   : 0.000
#    Success case prop solver time     : 0.000
# Current number of processed clauses  : 3
#    Positive orientable unit clauses  : 2
#    Positive unorientable unit clauses: 0
#    Negative unit clauses             : 0
#    Non-unit-clauses                  : 1
# Current number of unprocessed clauses: 80
# ...number of literals in the above   : 227
# Current number of archived formulas  : 0
# Current number of archived clauses   : 84
# Clause-clause subsumption calls (NU) : 2560
# Rec. Clause-clause subsumption calls : 1796
# Non-unit clause-clause subsumptions  : 13
# Unit Clause-clause subsumption calls : 5
# Rewrite failures with RHS unbound    : 0
# BW rewrite match attempts            : 0
# BW rewrite match successes           : 0
# Condensation attempts                : 0
# Condensation successes               : 0
# Termbank termtop insertions          : 5838

# -------------------------------------------------
# User time                : 0.020 s
# System time              : 0.004 s
# Total time               : 0.024 s
# Maximum resident set size: 1608 pages
% ott+11_3_aac=none:afr=on:afp=4000:afq=1.4:amm=off:anc=all:bs=unit_only:bsr=on:bce=on:fde=unused:irw=on:nm=64:newcnf=on:nwc=1:nicw=on:sac=on:sp=reverse_arity:uhcvi=on_31 on SOT_MiFT
% Refutation found. Thanks to Tanya!
% SZS status Theorem for SOT_MiFT
% SZS output start Proof for SOT_MiFT
fof(f211,plain,(
  $false),
  inference(avatar_sat_refutation,[],[f125,f129,f153,f210])).
fof(f210,plain,(
  ~spl16_1 | ~spl16_2 | ~spl16_8),
  inference(avatar_contradiction_clause,[],[f209])).
fof(f209,plain,(
  $false | (~spl16_1 | ~spl16_2 | ~spl16_8)),
  inference(subsumption_resolution,[],[f128,f208])).
fof(f208,plain,(
  ( ! [X0] : (~iof(X0,sK0)) ) | (~spl16_1 | ~spl16_8)),
  inference(resolution,[],[f152,f124])).
fof(f124,plain,(
  individual(sK0) | ~spl16_1),
  inference(avatar_component_clause,[],[f123])).
fof(f123,plain,(
  spl16_1 <=> individual(sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl16_1])])).
fof(f152,plain,(
  ( ! [X0,X1] : (~individual(X0) | ~iof(X1,X0)) ) | ~spl16_8),
  inference(avatar_component_clause,[],[f151])).
fof(f151,plain,(
  spl16_8 <=> ! [X1,X0] : (~iof(X1,X0) | ~individual(X0))),
  introduced(avatar_definition,[new_symbols(naming,[spl16_8])])).
fof(f128,plain,(
  iof(sK1,sK0) | ~spl16_2),
  inference(avatar_component_clause,[],[f127])).
fof(f127,plain,(
  spl16_2 <=> iof(sK1,sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl16_2])])).
fof(f153,plain,(
  spl16_8),
  inference(avatar_split_clause,[],[f80,f151])).
fof(f80,plain,(
  ( ! [X0,X1] : (~iof(X1,X0) | ~individual(X0)) )),
  inference(cnf_transformation,[],[f49])).
fof(f49,plain,(
  ! [X0] : (individual(X0) <=> ! [X1] : ~iof(X1,X0))),
  inference(ennf_transformation,[],[f2])).
fof(f2,axiom,(
  ! [X0] : (individual(X0) <=> ~? [X1] : iof(X1,X0))),
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',a2)).
fof(f129,plain,(
  spl16_2),
  inference(avatar_split_clause,[],[f58,f127])).
fof(f58,plain,(
  iof(sK1,sK0)),
  inference(cnf_transformation,[],[f27])).
fof(f27,plain,(
  ? [X0,X1] : (iof(X1,X0) & individual(X0))),
  inference(flattening,[],[f26])).
fof(f26,plain,(
  ~~? [X0,X1] : (iof(X1,X0) & individual(X0))),
  inference(rectify,[],[f25])).
fof(f25,negated_conjecture,(
  ~~? [X6,X7] : (iof(X7,X6) & individual(X6))),
  inference(negated_conjecture,[],[f24])).
fof(f24,conjecture,(
  ~? [X6,X7] : (iof(X7,X6) & individual(X6))),
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',t7_ap1)).
fof(f125,plain,(
  spl16_1),
  inference(avatar_split_clause,[],[f57,f123])).
fof(f57,plain,(
  individual(sK0)),
  inference(cnf_transformation,[],[f27])).
% SZS output end Proof for SOT_MiFT
% ------------------------------
% Version: Vampire 4.4.0 (commit 4fef31f on 2020-05-01 13:38:24 +0200)
% Termination reason: Refutation

% Memory used [KB]: 5373
% Time elapsed: 0.005 s
% ------------------------------
% ------------------------------
% Success in time 0.05 s
Moving to /home/tptp/Systems/CSE_E---1.0
java -jar /home/tptp/Systems/CSE_E---1.0/mcs_epr.jar 30 /tmp/qZi2mWPEWe/SOT_MiFT3j
% ott+11_3_aac=none:afr=on:afp=4000:afq=1.4:amm=off:anc=all:bs=unit_only:bsr=on:bce=on:fde=unused:irw=on:nm=64:newcnf=on:nwc=1:nicw=on:sac=on:sp=reverse_arity:uhcvi=on_31 on SOT_MiFT
% Refutation found. Thanks to Tanya!
% SZS status Theorem for SOT_MiFT
% SZS output start Proof for SOT_MiFT
fof(f211,plain,(
  $false),
  inference(avatar_sat_refutation,[],[f125,f129,f153,f210])).
fof(f210,plain,(
  ~spl16_1 | ~spl16_2 | ~spl16_8),
  inference(avatar_contradiction_clause,[],[f209])).
fof(f209,plain,(
  $false | (~spl16_1 | ~spl16_2 | ~spl16_8)),
  inference(subsumption_resolution,[],[f128,f208])).
fof(f208,plain,(
  ( ! [X0] : (~iof(X0,sK0)) ) | (~spl16_1 | ~spl16_8)),
  inference(resolution,[],[f152,f124])).
fof(f124,plain,(
  individual(sK0) | ~spl16_1),
  inference(avatar_component_clause,[],[f123])).
fof(f123,plain,(
  spl16_1 <=> individual(sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl16_1])])).
fof(f152,plain,(
  ( ! [X0,X1] : (~individual(X0) | ~iof(X1,X0)) ) | ~spl16_8),
  inference(avatar_component_clause,[],[f151])).
fof(f151,plain,(
  spl16_8 <=> ! [X1,X0] : (~iof(X1,X0) | ~individual(X0))),
  introduced(avatar_definition,[new_symbols(naming,[spl16_8])])).
fof(f128,plain,(
  iof(sK1,sK0) | ~spl16_2),
  inference(avatar_component_clause,[],[f127])).
fof(f127,plain,(
  spl16_2 <=> iof(sK1,sK0)),
  introduced(avatar_definition,[new_symbols(naming,[spl16_2])])).
fof(f153,plain,(
  spl16_8),
  inference(avatar_split_clause,[],[f80,f151])).
fof(f80,plain,(
  ( ! [X0,X1] : (~iof(X1,X0) | ~individual(X0)) )),
  inference(cnf_transformation,[],[f49])).
fof(f49,plain,(
  ! [X0] : (individual(X0) <=> ! [X1] : ~iof(X1,X0))),
  inference(ennf_transformation,[],[f2])).
fof(f2,axiom,(
  ! [X0] : (individual(X0) <=> ~? [X1] : iof(X1,X0))),
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',a2)).
fof(f129,plain,(
  spl16_2),
  inference(avatar_split_clause,[],[f58,f127])).
fof(f58,plain,(
  iof(sK1,sK0)),
  inference(cnf_transformation,[],[f27])).
fof(f27,plain,(
  ? [X0,X1] : (iof(X1,X0) & individual(X0))),
  inference(flattening,[],[f26])).
fof(f26,plain,(
  ~~? [X0,X1] : (iof(X1,X0) & individual(X0))),
  inference(rectify,[],[f25])).
fof(f25,negated_conjecture,(
  ~~? [X6,X7] : (iof(X7,X6) & individual(X6))),
  inference(negated_conjecture,[],[f24])).
fof(f24,conjecture,(
  ~? [X6,X7] : (iof(X7,X6) & individual(X6))),
  file('/tmp/qZi2mWPEWe/SOT_MiFT3j',t7_ap1)).
fof(f125,plain,(
  spl16_1),
  inference(avatar_split_clause,[],[f57,f123])).
fof(f57,plain,(
  individual(sK0)),
  inference(cnf_transformation,[],[f27])).
% SZS output end Proof for SOT_MiFT
% ------------------------------
% Version: Vampire 4.4.0 (commit 4fef31f on 2020-05-01 13:38:24 +0200)
% Termination reason: Refutation

% Memory used [KB]: 5373
% Time elapsed: 0.007 s
% ------------------------------
% ------------------------------
% Success in time 0.054 s
start to proof:SOT_MiFT3j

% END OF SYSTEM OUTPUT

% END OF SYSTEM OUTPUT

% END OF SYSTEM OUTPUT
% RESULT: SOT_MiFT3j - Vampire---SAT-4.5 says Theorem - CPU = 0.00 WC = 0.05 
% OUTPUT: SOT_MiFT3j - Vampire---SAT-4.5 says Refutation - CPU = 0.00 WC = 0.05 
% RESULT: SOT_MiFT3j - Vampire---SAT-4.5 says Theorem - CPU = 0.00 WC = 0.15 
% OUTPUT: SOT_MiFT3j - Vampire---SAT-4.5 says Refutation - CPU = 0.00 WC = 0.15 
% RESULT: SOT_MiFT3j - E---FNT-2.5 says Theorem - CPU = 0.00 WC = 0.02 
% OUTPUT: SOT_MiFT3j - E---FNT-2.5 says CNFRefutation - CPU = 0.00 WC = 0.02 

% END OF SYSTEM OUTPUT

% END OF SYSTEM OUTPUT

% END OF SYSTEM OUTPUT

% END OF SYSTEM OUTPUT
% RESULT: SOT_MiFT3j - E---FNT-2.5 says Theorem - CPU = 0.00 WC = 0.02 
% OUTPUT: SOT_MiFT3j - E---FNT-2.5 says CNFRefutation - CPU = 0.00 WC = 0.02 
% RESULT: SOT_MiFT3j - E---FNT-2.5 says Theorem - CPU = 0.00 WC = 0.02 
% OUTPUT: SOT_MiFT3j - E---FNT-2.5 says CNFRefutation - CPU = 0.00 WC = 0.02 
% RESULT: SOT_MiFT3j - Vampire---SAT-4.5 says Theorem - CPU = 0.00 WC = 0.05 
% OUTPUT: SOT_MiFT3j - Vampire---SAT-4.5 says Refutation - CPU = 0.00 WC = 0.05 
% RESULT: SOT_MiFT3j - Vampire---SAT-4.5 says Theorem - CPU = 0.00 WC = 0.05 
% OUTPUT: SOT_MiFT3j - Vampire---SAT-4.5 says Refutation - CPU = 0.00 WC = 0.05 

% END OF SYSTEM OUTPUT
% RESULT: SOT_MiFT3j - CSE_E---1.0 says Unknown - CPU = 0 WC = 0 
% OUTPUT: SOT_MiFT3j - CSE_E---1.0 says None - CPU = 0 WC = 0 
% 10 wall clock seconds gone, waiting for system output
% 20 wall clock seconds gone, waiting for system output
% 30 wall clock seconds gone, waiting for system output

% END OF SYSTEM OUTPUT
% RESULT: SOT_MiFT3j - Isabelle---2016 says Unknown - CPU = 0 WC = 0 
% OUTPUT: SOT_MiFT3j - Isabelle---2016 says None - CPU = 0 WC = 0 

% END OF SYSTEM OUTPUT
% RESULT: SOT_MiFT3j - Isabelle---2016 says Unknown - CPU = 0 WC = 0 
% OUTPUT: SOT_MiFT3j - Isabelle---2016 says None - CPU = 0 WC = 0 
Vampire---SAT-4.5 has ended (PID 107033)
Vampire---SAT-4.5 has ended (PID 107034)
Vampire---SAT-4.5 has ended (PID 107035)
Vampire---SAT-4.5 has ended (PID 107036)
E---FNT-2.5 has ended (PID 107037)
E---FNT-2.5 has ended (PID 107038)
CSE_E---1.0 has ended (PID 107039)
E---FNT-2.5 has ended (PID 107040)
Isabelle---2016 has ended (PID 107041)
Isabelle---2016 has ended (PID 107042)
RESULT: SOT_MiFT3j - SSCPA---0.0 says Theorem - CPU = 193.0 WC = 33.8  SolvingSystem = Vampire---SAT-4.5
</PRE>

</body>
</html>