%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : KRS217+1 : TPTP v5.3.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : nashville.cs.miami.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Core(TM)2 CPU 6600 @ 2.40GHz @ 2400MHz
% Memory : 1003MB
% OS : Linux 2.6.32.26-175.fc12.x86_64
% CPULimit : 300s
% DateTime : Fri Jun 15 10:49:41 EDT 2012
% Result : Theorem 81.38s
% Output : Solution 82.19s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP19145/KRS217+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 59.42s, total lost is 59.42s
% not found
% Adding ~C to TBU ... ~nota_noc_thm:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ... not found
% Looking for CSA axiom ... nota:
% CSA axiom nota found
% Looking for CSA axiom ... thm:
% CSA axiom thm found
% Looking for CSA axiom ... completeness:
% CSA axiom completeness found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ... yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... not:
% tautology: CSA axiom tautology found
% Looking for CSA axiom ... satisfiable:
% CSA axiom satisfiable found
% Looking for CSA axiom ... contradiction:
% CSA axiom contradiction found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ... not found
% Looking for CSA axiom ... not:
% sat_non_taut_pair:
% mixed_pair:
% CSA axiom mixed_pair found
% Looking for CSA axiom ... non_thm_spt:
% noc:
% CSA axiom noc found
% Looking for CSA axiom ... csa:
% CSA axiom csa found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ... yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :csa:noc:mixed_pair:contradiction:satisfiable:tautology:completeness:thm:nota (9)
% Unselected axioms are ... :not:sat_non_taut_pair:non_thm_spt:uns:unp:sap:esa:sat:eqv:tac:wec:eth:tau:wtc:wth:cax:sca:tca:wca:mighta:isa:nevera:xora (23)
% SZS status THM for /tmp/SystemOnTPTP19145/KRS217+1.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP19145/KRS217+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.5/eproof_ram --print-statistics -xAuto -tAuto --cpu-limit=600 --memory-limit=Auto --tstp-format /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 21393
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Auto-Ordering is analysing problem.
% # Problem is type GHNFNFFSS21MS
% # Auto-mode selected ordering type KBO6
% # Auto-mode selected ordering precedence scheme <invfreq>
% # Auto-mode selected weight ordering scheme <invfreqrank>
% #
% # Auto-Heuristic is analysing problem.
% # Problem is type GHNFNFFSS21MS
% # Auto-Mode selected heuristic G_E___024_C18_F1_PI_AE_Q4_CS_SP_S0Y
% # and selection function SelectMaxLComplexAvoidPosPred.
% #
% # No equality, disabling AC handling.
% #
% # Initializing proof state
% # Proof found!
% # SZS status Theorem
% # Parsed axioms : 10
% # Removed by relevancy pruning : 0
% # Initial clauses : 26
% # Removed in clause preprocessing : 0
% # Initial clauses in saturation : 26
% # Processed clauses : 3367
% # ...of these trivial : 137
% # ...subsumed : 2334
% # ...remaining for further processing: 896
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 28
% # Backward-rewritten : 40
% # Generated clauses : 30295
% # ...of the previous two non-trivial : 17516
% # Contextual simplify-reflections : 148
% # Paramodulations : 30275
% # Factorizations : 20
% # Equation resolutions : 0
% # Current number of processed clauses: 828
% # Positive orientable unit clauses: 204
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 58
% # Non-unit-clauses : 566
% # Current number of unprocessed clauses: 13129
% # ...number of literals in the above : 41198
% # Clause-clause subsumption calls (NU) : 82902
% # Rec. Clause-clause subsumption calls : 59798
% # Non-unit clause-clause subsumptions: 1824
% # Unit Clause-clause subsumption calls : 5002
% # Rewrite failures with RHS unbound : 0
% # BW rewrite match attempts : 2071
% # BW rewrite match successes : 16
% # Backwards rewriting index : 1228 nodes, 285 leaves, 2.83+/-5.071 terms/leaf
% # Paramod-from index : 545 nodes, 138 leaves, 3.02+/-5.702 terms/leaf
% # Paramod-into index : 982 nodes, 222 leaves, 2.55+/-4.990 terms/leaf
% # Paramod-neg-atom index : 354 nodes, 81 leaves, 2.10+/-1.909 terms/leaf
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:(?[X3]:(model(X3,X1)&model(X3,not(X2)))<=>status(X1,X2,csa)),file('/tmp/SRASS.s.p', csa)).
% fof(2, axiom,![X1]:![X2]:((?[X3]:(model(X3,X1)&model(X3,X2))&?[X4]:(model(X4,X1)&model(X4,not(X2))))<=>status(X1,X2,noc)),file('/tmp/SRASS.s.p', noc)).
% fof(3, axiom,?[X1]:?[X2]:(((?[X3]:model(X3,X1)&![X4]:(model(X4,X1)=>model(X4,X2)))&?[X5]:(~(model(X5,X1))&model(X5,X2)))&?[X6]:~(model(X6,X2))),file('/tmp/SRASS.s.p', mixed_pair)).
% fof(7, axiom,![X8]:![X7]:(model(X8,X7)<~>model(X8,not(X7))),file('/tmp/SRASS.s.p', completeness)).
% fof(8, axiom,![X1]:![X2]:(![X3]:(model(X3,X1)=>model(X3,X2))<=>status(X1,X2,thm)),file('/tmp/SRASS.s.p', thm)).
% fof(9, axiom,![X9]:![X10]:(?[X1]:?[X2]:(status(X1,X2,X9)&~(status(X1,X2,X10)))<=>nota(X9,X10)),file('/tmp/SRASS.s.p', nota)).
% fof(10, conjecture,nota(noc,thm),file('/tmp/SRASS.s.p', nota_noc_thm)).
% fof(11, negated_conjecture,~(nota(noc,thm)),inference(assume_negation,[status(cth)],[10])).
% fof(12, plain,?[X1]:?[X2]:(((?[X3]:model(X3,X1)&![X4]:(model(X4,X1)=>model(X4,X2)))&?[X5]:(~(model(X5,X1))&model(X5,X2)))&?[X6]:~(model(X6,X2))),inference(fof_simplification,[status(thm)],[3,theory(equality)])).
% fof(15, plain,![X8]:![X7]:~((model(X8,X7)<=>model(X8,not(X7)))),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% fof(16, plain,![X9]:![X10]:(?[X1]:?[X2]:(status(X1,X2,X9)&~(status(X1,X2,X10)))<=>nota(X9,X10)),inference(fof_simplification,[status(thm)],[9,theory(equality)])).
% fof(17, negated_conjecture,~(nota(noc,thm)),inference(fof_simplification,[status(thm)],[11,theory(equality)])).
% fof(18, plain,![X1]:![X2]:((![X3]:(~(model(X3,X1))|~(model(X3,not(X2))))|status(X1,X2,csa))&(~(status(X1,X2,csa))|?[X3]:(model(X3,X1)&model(X3,not(X2))))),inference(fof_nnf,[status(thm)],[1])).
% fof(19, plain,(![X1]:![X2]:(![X3]:(~(model(X3,X1))|~(model(X3,not(X2))))|status(X1,X2,csa))&![X1]:![X2]:(~(status(X1,X2,csa))|?[X3]:(model(X3,X1)&model(X3,not(X2))))),inference(shift_quantors,[status(thm)],[18])).
% fof(20, plain,(![X4]:![X5]:(![X6]:(~(model(X6,X4))|~(model(X6,not(X5))))|status(X4,X5,csa))&![X7]:![X8]:(~(status(X7,X8,csa))|?[X9]:(model(X9,X7)&model(X9,not(X8))))),inference(variable_rename,[status(thm)],[19])).
% fof(21, plain,(![X4]:![X5]:(![X6]:(~(model(X6,X4))|~(model(X6,not(X5))))|status(X4,X5,csa))&![X7]:![X8]:(~(status(X7,X8,csa))|(model(esk1_2(X7,X8),X7)&model(esk1_2(X7,X8),not(X8))))),inference(skolemize,[status(esa)],[20])).
% fof(22, plain,![X4]:![X5]:![X6]:![X7]:![X8]:(((~(model(X6,X4))|~(model(X6,not(X5))))|status(X4,X5,csa))&(~(status(X7,X8,csa))|(model(esk1_2(X7,X8),X7)&model(esk1_2(X7,X8),not(X8))))),inference(shift_quantors,[status(thm)],[21])).
% fof(23, plain,![X4]:![X5]:![X6]:![X7]:![X8]:(((~(model(X6,X4))|~(model(X6,not(X5))))|status(X4,X5,csa))&((model(esk1_2(X7,X8),X7)|~(status(X7,X8,csa)))&(model(esk1_2(X7,X8),not(X8))|~(status(X7,X8,csa))))),inference(distribute,[status(thm)],[22])).
% cnf(24,plain,(model(esk1_2(X1,X2),not(X2))|~status(X1,X2,csa)),inference(split_conjunct,[status(thm)],[23])).
% cnf(25,plain,(model(esk1_2(X1,X2),X1)|~status(X1,X2,csa)),inference(split_conjunct,[status(thm)],[23])).
% cnf(26,plain,(status(X1,X2,csa)|~model(X3,not(X2))|~model(X3,X1)),inference(split_conjunct,[status(thm)],[23])).
% fof(27, plain,![X1]:![X2]:(((![X3]:(~(model(X3,X1))|~(model(X3,X2)))|![X4]:(~(model(X4,X1))|~(model(X4,not(X2)))))|status(X1,X2,noc))&(~(status(X1,X2,noc))|(?[X3]:(model(X3,X1)&model(X3,X2))&?[X4]:(model(X4,X1)&model(X4,not(X2)))))),inference(fof_nnf,[status(thm)],[2])).
% fof(28, plain,(![X1]:![X2]:((![X3]:(~(model(X3,X1))|~(model(X3,X2)))|![X4]:(~(model(X4,X1))|~(model(X4,not(X2)))))|status(X1,X2,noc))&![X1]:![X2]:(~(status(X1,X2,noc))|(?[X3]:(model(X3,X1)&model(X3,X2))&?[X4]:(model(X4,X1)&model(X4,not(X2)))))),inference(shift_quantors,[status(thm)],[27])).
% fof(29, plain,(![X5]:![X6]:((![X7]:(~(model(X7,X5))|~(model(X7,X6)))|![X8]:(~(model(X8,X5))|~(model(X8,not(X6)))))|status(X5,X6,noc))&![X9]:![X10]:(~(status(X9,X10,noc))|(?[X11]:(model(X11,X9)&model(X11,X10))&?[X12]:(model(X12,X9)&model(X12,not(X10)))))),inference(variable_rename,[status(thm)],[28])).
% fof(30, plain,(![X5]:![X6]:((![X7]:(~(model(X7,X5))|~(model(X7,X6)))|![X8]:(~(model(X8,X5))|~(model(X8,not(X6)))))|status(X5,X6,noc))&![X9]:![X10]:(~(status(X9,X10,noc))|((model(esk2_2(X9,X10),X9)&model(esk2_2(X9,X10),X10))&(model(esk3_2(X9,X10),X9)&model(esk3_2(X9,X10),not(X10)))))),inference(skolemize,[status(esa)],[29])).
% fof(31, plain,![X5]:![X6]:![X7]:![X8]:![X9]:![X10]:((((~(model(X7,X5))|~(model(X7,X6)))|(~(model(X8,X5))|~(model(X8,not(X6)))))|status(X5,X6,noc))&(~(status(X9,X10,noc))|((model(esk2_2(X9,X10),X9)&model(esk2_2(X9,X10),X10))&(model(esk3_2(X9,X10),X9)&model(esk3_2(X9,X10),not(X10)))))),inference(shift_quantors,[status(thm)],[30])).
% fof(32, plain,![X5]:![X6]:![X7]:![X8]:![X9]:![X10]:((((~(model(X7,X5))|~(model(X7,X6)))|(~(model(X8,X5))|~(model(X8,not(X6)))))|status(X5,X6,noc))&(((model(esk2_2(X9,X10),X9)|~(status(X9,X10,noc)))&(model(esk2_2(X9,X10),X10)|~(status(X9,X10,noc))))&((model(esk3_2(X9,X10),X9)|~(status(X9,X10,noc)))&(model(esk3_2(X9,X10),not(X10))|~(status(X9,X10,noc)))))),inference(distribute,[status(thm)],[31])).
% cnf(37,plain,(status(X1,X2,noc)|~model(X3,not(X2))|~model(X3,X1)|~model(X4,X2)|~model(X4,X1)),inference(split_conjunct,[status(thm)],[32])).
% fof(38, plain,?[X1]:?[X2]:(((?[X3]:model(X3,X1)&![X4]:(~(model(X4,X1))|model(X4,X2)))&?[X5]:(~(model(X5,X1))&model(X5,X2)))&?[X6]:~(model(X6,X2))),inference(fof_nnf,[status(thm)],[12])).
% fof(39, plain,?[X7]:?[X8]:(((?[X9]:model(X9,X7)&![X10]:(~(model(X10,X7))|model(X10,X8)))&?[X11]:(~(model(X11,X7))&model(X11,X8)))&?[X12]:~(model(X12,X8))),inference(variable_rename,[status(thm)],[38])).
% fof(40, plain,(((model(esk6_0,esk4_0)&![X10]:(~(model(X10,esk4_0))|model(X10,esk5_0)))&(~(model(esk7_0,esk4_0))&model(esk7_0,esk5_0)))&~(model(esk8_0,esk5_0))),inference(skolemize,[status(esa)],[39])).
% fof(41, plain,![X10]:(((model(esk6_0,esk4_0)&(~(model(X10,esk4_0))|model(X10,esk5_0)))&(~(model(esk7_0,esk4_0))&model(esk7_0,esk5_0)))&~(model(esk8_0,esk5_0))),inference(shift_quantors,[status(thm)],[40])).
% cnf(43,plain,(model(esk7_0,esk5_0)),inference(split_conjunct,[status(thm)],[41])).
% cnf(44,plain,(~model(esk7_0,esk4_0)),inference(split_conjunct,[status(thm)],[41])).
% cnf(45,plain,(model(X1,esk5_0)|~model(X1,esk4_0)),inference(split_conjunct,[status(thm)],[41])).
% cnf(46,plain,(model(esk6_0,esk4_0)),inference(split_conjunct,[status(thm)],[41])).
% fof(57, plain,![X8]:![X7]:((~(model(X8,X7))|~(model(X8,not(X7))))&(model(X8,X7)|model(X8,not(X7)))),inference(fof_nnf,[status(thm)],[15])).
% fof(58, plain,(![X8]:![X7]:(~(model(X8,X7))|~(model(X8,not(X7))))&![X8]:![X7]:(model(X8,X7)|model(X8,not(X7)))),inference(shift_quantors,[status(thm)],[57])).
% fof(59, plain,(![X9]:![X10]:(~(model(X9,X10))|~(model(X9,not(X10))))&![X11]:![X12]:(model(X11,X12)|model(X11,not(X12)))),inference(variable_rename,[status(thm)],[58])).
% fof(60, plain,![X9]:![X10]:![X11]:![X12]:((~(model(X9,X10))|~(model(X9,not(X10))))&(model(X11,X12)|model(X11,not(X12)))),inference(shift_quantors,[status(thm)],[59])).
% cnf(61,plain,(model(X1,not(X2))|model(X1,X2)),inference(split_conjunct,[status(thm)],[60])).
% cnf(62,plain,(~model(X1,not(X2))|~model(X1,X2)),inference(split_conjunct,[status(thm)],[60])).
% fof(63, plain,![X1]:![X2]:((?[X3]:(model(X3,X1)&~(model(X3,X2)))|status(X1,X2,thm))&(~(status(X1,X2,thm))|![X3]:(~(model(X3,X1))|model(X3,X2)))),inference(fof_nnf,[status(thm)],[8])).
% fof(64, plain,(![X1]:![X2]:(?[X3]:(model(X3,X1)&~(model(X3,X2)))|status(X1,X2,thm))&![X1]:![X2]:(~(status(X1,X2,thm))|![X3]:(~(model(X3,X1))|model(X3,X2)))),inference(shift_quantors,[status(thm)],[63])).
% fof(65, plain,(![X4]:![X5]:(?[X6]:(model(X6,X4)&~(model(X6,X5)))|status(X4,X5,thm))&![X7]:![X8]:(~(status(X7,X8,thm))|![X9]:(~(model(X9,X7))|model(X9,X8)))),inference(variable_rename,[status(thm)],[64])).
% fof(66, plain,(![X4]:![X5]:((model(esk14_2(X4,X5),X4)&~(model(esk14_2(X4,X5),X5)))|status(X4,X5,thm))&![X7]:![X8]:(~(status(X7,X8,thm))|![X9]:(~(model(X9,X7))|model(X9,X8)))),inference(skolemize,[status(esa)],[65])).
% fof(67, plain,![X4]:![X5]:![X7]:![X8]:![X9]:(((model(esk14_2(X4,X5),X4)&~(model(esk14_2(X4,X5),X5)))|status(X4,X5,thm))&(~(status(X7,X8,thm))|(~(model(X9,X7))|model(X9,X8)))),inference(shift_quantors,[status(thm)],[66])).
% fof(68, plain,![X4]:![X5]:![X7]:![X8]:![X9]:(((model(esk14_2(X4,X5),X4)|status(X4,X5,thm))&(~(model(esk14_2(X4,X5),X5))|status(X4,X5,thm)))&(~(status(X7,X8,thm))|(~(model(X9,X7))|model(X9,X8)))),inference(distribute,[status(thm)],[67])).
% cnf(69,plain,(model(X1,X2)|~model(X1,X3)|~status(X3,X2,thm)),inference(split_conjunct,[status(thm)],[68])).
% cnf(70,plain,(status(X1,X2,thm)|~model(esk14_2(X1,X2),X2)),inference(split_conjunct,[status(thm)],[68])).
% cnf(71,plain,(status(X1,X2,thm)|model(esk14_2(X1,X2),X1)),inference(split_conjunct,[status(thm)],[68])).
% fof(72, plain,![X9]:![X10]:((![X1]:![X2]:(~(status(X1,X2,X9))|status(X1,X2,X10))|nota(X9,X10))&(~(nota(X9,X10))|?[X1]:?[X2]:(status(X1,X2,X9)&~(status(X1,X2,X10))))),inference(fof_nnf,[status(thm)],[16])).
% fof(73, plain,(![X9]:![X10]:(![X1]:![X2]:(~(status(X1,X2,X9))|status(X1,X2,X10))|nota(X9,X10))&![X9]:![X10]:(~(nota(X9,X10))|?[X1]:?[X2]:(status(X1,X2,X9)&~(status(X1,X2,X10))))),inference(shift_quantors,[status(thm)],[72])).
% fof(74, plain,(![X11]:![X12]:(![X13]:![X14]:(~(status(X13,X14,X11))|status(X13,X14,X12))|nota(X11,X12))&![X15]:![X16]:(~(nota(X15,X16))|?[X17]:?[X18]:(status(X17,X18,X15)&~(status(X17,X18,X16))))),inference(variable_rename,[status(thm)],[73])).
% fof(75, plain,(![X11]:![X12]:(![X13]:![X14]:(~(status(X13,X14,X11))|status(X13,X14,X12))|nota(X11,X12))&![X15]:![X16]:(~(nota(X15,X16))|(status(esk15_2(X15,X16),esk16_2(X15,X16),X15)&~(status(esk15_2(X15,X16),esk16_2(X15,X16),X16))))),inference(skolemize,[status(esa)],[74])).
% fof(76, plain,![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:(((~(status(X13,X14,X11))|status(X13,X14,X12))|nota(X11,X12))&(~(nota(X15,X16))|(status(esk15_2(X15,X16),esk16_2(X15,X16),X15)&~(status(esk15_2(X15,X16),esk16_2(X15,X16),X16))))),inference(shift_quantors,[status(thm)],[75])).
% fof(77, plain,![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:(((~(status(X13,X14,X11))|status(X13,X14,X12))|nota(X11,X12))&((status(esk15_2(X15,X16),esk16_2(X15,X16),X15)|~(nota(X15,X16)))&(~(status(esk15_2(X15,X16),esk16_2(X15,X16),X16))|~(nota(X15,X16))))),inference(distribute,[status(thm)],[76])).
% cnf(80,plain,(nota(X1,X2)|status(X3,X4,X2)|~status(X3,X4,X1)),inference(split_conjunct,[status(thm)],[77])).
% cnf(81,negated_conjecture,(~nota(noc,thm)),inference(split_conjunct,[status(thm)],[17])).
% cnf(85,plain,(status(not(X1),X2,thm)|~model(esk14_2(not(X1),X2),X1)),inference(spm,[status(thm)],[62,71,theory(equality)])).
% cnf(88,plain,(status(X1,not(X2),thm)|model(esk14_2(X1,not(X2)),X2)),inference(spm,[status(thm)],[70,61,theory(equality)])).
% cnf(106,plain,(~model(esk1_2(X1,X2),X2)|~status(X1,X2,csa)),inference(spm,[status(thm)],[62,24,theory(equality)])).
% cnf(117,plain,(status(X1,X2,noc)|model(X3,X2)|~model(X4,X2)|~model(X4,X1)|~model(X3,X1)),inference(spm,[status(thm)],[37,61,theory(equality)])).
% cnf(127,plain,(status(not(esk5_0),X1,thm)|~model(esk14_2(not(esk5_0),X1),esk4_0)),inference(spm,[status(thm)],[85,45,theory(equality)])).
% cnf(403,plain,(~status(X1,X1,csa)),inference(spm,[status(thm)],[106,25,theory(equality)])).
% cnf(1802,plain,(status(X1,esk4_0,noc)|model(X2,esk4_0)|~model(esk6_0,X1)|~model(X2,X1)),inference(spm,[status(thm)],[117,46,theory(equality)])).
% cnf(1976,plain,(status(not(esk5_0),not(esk4_0),thm)),inference(spm,[status(thm)],[127,88,theory(equality)])).
% cnf(1977,plain,(model(X1,not(esk4_0))|~model(X1,not(esk5_0))),inference(spm,[status(thm)],[69,1976,theory(equality)])).
% cnf(1991,plain,(model(X1,not(esk4_0))|model(X1,esk5_0)),inference(spm,[status(thm)],[1977,61,theory(equality)])).
% cnf(2024,plain,(status(X1,esk4_0,csa)|model(X2,esk5_0)|~model(X2,X1)),inference(spm,[status(thm)],[26,1991,theory(equality)])).
% cnf(2437,plain,(status(esk4_0,esk4_0,csa)|model(esk6_0,esk5_0)),inference(spm,[status(thm)],[2024,46,theory(equality)])).
% cnf(2455,plain,(model(esk6_0,esk5_0)),inference(sr,[status(thm)],[2437,403,theory(equality)])).
% cnf(47153,plain,(status(esk5_0,esk4_0,noc)|model(esk7_0,esk4_0)|~model(esk6_0,esk5_0)),inference(spm,[status(thm)],[1802,43,theory(equality)])).
% cnf(47222,plain,(status(esk5_0,esk4_0,noc)|model(esk7_0,esk4_0)|$false),inference(rw,[status(thm)],[47153,2455,theory(equality)])).
% cnf(47223,plain,(status(esk5_0,esk4_0,noc)|model(esk7_0,esk4_0)),inference(cn,[status(thm)],[47222,theory(equality)])).
% cnf(47224,plain,(status(esk5_0,esk4_0,noc)),inference(sr,[status(thm)],[47223,44,theory(equality)])).
% cnf(47277,plain,(nota(noc,X1)|status(esk5_0,esk4_0,X1)),inference(spm,[status(thm)],[80,47224,theory(equality)])).
% cnf(50501,negated_conjecture,(status(esk5_0,esk4_0,thm)),inference(spm,[status(thm)],[81,47277,theory(equality)])).
% cnf(50505,negated_conjecture,(model(X1,esk4_0)|~model(X1,esk5_0)),inference(spm,[status(thm)],[69,50501,theory(equality)])).
% cnf(50866,negated_conjecture,(model(esk7_0,esk4_0)),inference(spm,[status(thm)],[50505,43,theory(equality)])).
% cnf(50909,negated_conjecture,($false),inference(sr,[status(thm)],[50866,44,theory(equality)])).
% cnf(50910,negated_conjecture,($false),50909,['proof']).
% # SZS output end CNFRefutation
% PrfWatch: 0.68 CPU 0.44 WC
% FINAL PrfWatch: 0.68 CPU 0.44 WC
% SZS output end Solution for /tmp/SystemOnTPTP19145/KRS217+1.tptp
%
%------------------------------------------------------------------------------