%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU191+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art01.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Dec 30 01:37:00 EST 2010
% Result : Theorem 1.34s
% Output : Solution 1.34s
% 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/SystemOnTPTP26685/SEU191+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP26685/SEU191+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP26685/SEU191+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 26784
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.015 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,![X1]:![X2]:((relation(X1)&relation(X2))=>relation(relation_composition(X1,X2))),file('/tmp/SRASS.s.p', dt_k5_relat_1)).
% fof(3, axiom,![X1]:relation(identity_relation(X1)),file('/tmp/SRASS.s.p', dt_k6_relat_1)).
% fof(4, axiom,![X1]:![X2]:(relation(X2)=>(X2=identity_relation(X1)<=>![X3]:![X4]:(in(ordered_pair(X3,X4),X2)<=>(in(X3,X1)&X3=X4)))),file('/tmp/SRASS.s.p', d10_relat_1)).
% fof(5, axiom,![X1]:(relation(X1)=>![X2]:(relation(X2)=>![X3]:(relation(X3)=>(X3=relation_composition(X1,X2)<=>![X4]:![X5]:(in(ordered_pair(X4,X5),X3)<=>?[X6]:(in(ordered_pair(X4,X6),X1)&in(ordered_pair(X6,X5),X2))))))),file('/tmp/SRASS.s.p', d8_relat_1)).
% fof(21, axiom,![X1]:![X2]:unordered_pair(X1,X2)=unordered_pair(X2,X1),file('/tmp/SRASS.s.p', commutativity_k2_tarski)).
% fof(22, axiom,![X1]:![X2]:ordered_pair(X1,X2)=unordered_pair(unordered_pair(X1,X2),singleton(X1)),file('/tmp/SRASS.s.p', d5_tarski)).
% fof(31, conjecture,![X1]:![X2]:![X3]:![X4]:(relation(X4)=>(in(ordered_pair(X1,X2),relation_composition(identity_relation(X3),X4))<=>(in(X1,X3)&in(ordered_pair(X1,X2),X4)))),file('/tmp/SRASS.s.p', t74_relat_1)).
% fof(32, negated_conjecture,~(![X1]:![X2]:![X3]:![X4]:(relation(X4)=>(in(ordered_pair(X1,X2),relation_composition(identity_relation(X3),X4))<=>(in(X1,X3)&in(ordered_pair(X1,X2),X4))))),inference(assume_negation,[status(cth)],[31])).
% fof(42, plain,![X1]:![X2]:((~(relation(X1))|~(relation(X2)))|relation(relation_composition(X1,X2))),inference(fof_nnf,[status(thm)],[2])).
% fof(43, plain,![X3]:![X4]:((~(relation(X3))|~(relation(X4)))|relation(relation_composition(X3,X4))),inference(variable_rename,[status(thm)],[42])).
% cnf(44,plain,(relation(relation_composition(X1,X2))|~relation(X2)|~relation(X1)),inference(split_conjunct,[status(thm)],[43])).
% fof(45, plain,![X2]:relation(identity_relation(X2)),inference(variable_rename,[status(thm)],[3])).
% cnf(46,plain,(relation(identity_relation(X1))),inference(split_conjunct,[status(thm)],[45])).
% fof(47, plain,![X1]:![X2]:(~(relation(X2))|((~(X2=identity_relation(X1))|![X3]:![X4]:((~(in(ordered_pair(X3,X4),X2))|(in(X3,X1)&X3=X4))&((~(in(X3,X1))|~(X3=X4))|in(ordered_pair(X3,X4),X2))))&(?[X3]:?[X4]:((~(in(ordered_pair(X3,X4),X2))|(~(in(X3,X1))|~(X3=X4)))&(in(ordered_pair(X3,X4),X2)|(in(X3,X1)&X3=X4)))|X2=identity_relation(X1)))),inference(fof_nnf,[status(thm)],[4])).
% fof(48, plain,![X5]:![X6]:(~(relation(X6))|((~(X6=identity_relation(X5))|![X7]:![X8]:((~(in(ordered_pair(X7,X8),X6))|(in(X7,X5)&X7=X8))&((~(in(X7,X5))|~(X7=X8))|in(ordered_pair(X7,X8),X6))))&(?[X9]:?[X10]:((~(in(ordered_pair(X9,X10),X6))|(~(in(X9,X5))|~(X9=X10)))&(in(ordered_pair(X9,X10),X6)|(in(X9,X5)&X9=X10)))|X6=identity_relation(X5)))),inference(variable_rename,[status(thm)],[47])).
% fof(49, plain,![X5]:![X6]:(~(relation(X6))|((~(X6=identity_relation(X5))|![X7]:![X8]:((~(in(ordered_pair(X7,X8),X6))|(in(X7,X5)&X7=X8))&((~(in(X7,X5))|~(X7=X8))|in(ordered_pair(X7,X8),X6))))&(((~(in(ordered_pair(esk1_2(X5,X6),esk2_2(X5,X6)),X6))|(~(in(esk1_2(X5,X6),X5))|~(esk1_2(X5,X6)=esk2_2(X5,X6))))&(in(ordered_pair(esk1_2(X5,X6),esk2_2(X5,X6)),X6)|(in(esk1_2(X5,X6),X5)&esk1_2(X5,X6)=esk2_2(X5,X6))))|X6=identity_relation(X5)))),inference(skolemize,[status(esa)],[48])).
% fof(50, plain,![X5]:![X6]:![X7]:![X8]:(((((~(in(ordered_pair(X7,X8),X6))|(in(X7,X5)&X7=X8))&((~(in(X7,X5))|~(X7=X8))|in(ordered_pair(X7,X8),X6)))|~(X6=identity_relation(X5)))&(((~(in(ordered_pair(esk1_2(X5,X6),esk2_2(X5,X6)),X6))|(~(in(esk1_2(X5,X6),X5))|~(esk1_2(X5,X6)=esk2_2(X5,X6))))&(in(ordered_pair(esk1_2(X5,X6),esk2_2(X5,X6)),X6)|(in(esk1_2(X5,X6),X5)&esk1_2(X5,X6)=esk2_2(X5,X6))))|X6=identity_relation(X5)))|~(relation(X6))),inference(shift_quantors,[status(thm)],[49])).
% fof(51, plain,![X5]:![X6]:![X7]:![X8]:((((((in(X7,X5)|~(in(ordered_pair(X7,X8),X6)))|~(X6=identity_relation(X5)))|~(relation(X6)))&(((X7=X8|~(in(ordered_pair(X7,X8),X6)))|~(X6=identity_relation(X5)))|~(relation(X6))))&((((~(in(X7,X5))|~(X7=X8))|in(ordered_pair(X7,X8),X6))|~(X6=identity_relation(X5)))|~(relation(X6))))&((((~(in(ordered_pair(esk1_2(X5,X6),esk2_2(X5,X6)),X6))|(~(in(esk1_2(X5,X6),X5))|~(esk1_2(X5,X6)=esk2_2(X5,X6))))|X6=identity_relation(X5))|~(relation(X6)))&((((in(esk1_2(X5,X6),X5)|in(ordered_pair(esk1_2(X5,X6),esk2_2(X5,X6)),X6))|X6=identity_relation(X5))|~(relation(X6)))&(((esk1_2(X5,X6)=esk2_2(X5,X6)|in(ordered_pair(esk1_2(X5,X6),esk2_2(X5,X6)),X6))|X6=identity_relation(X5))|~(relation(X6)))))),inference(distribute,[status(thm)],[50])).
% cnf(55,plain,(in(ordered_pair(X3,X4),X1)|~relation(X1)|X1!=identity_relation(X2)|X3!=X4|~in(X3,X2)),inference(split_conjunct,[status(thm)],[51])).
% cnf(56,plain,(X3=X4|~relation(X1)|X1!=identity_relation(X2)|~in(ordered_pair(X3,X4),X1)),inference(split_conjunct,[status(thm)],[51])).
% cnf(57,plain,(in(X3,X2)|~relation(X1)|X1!=identity_relation(X2)|~in(ordered_pair(X3,X4),X1)),inference(split_conjunct,[status(thm)],[51])).
% fof(58, plain,![X1]:(~(relation(X1))|![X2]:(~(relation(X2))|![X3]:(~(relation(X3))|((~(X3=relation_composition(X1,X2))|![X4]:![X5]:((~(in(ordered_pair(X4,X5),X3))|?[X6]:(in(ordered_pair(X4,X6),X1)&in(ordered_pair(X6,X5),X2)))&(![X6]:(~(in(ordered_pair(X4,X6),X1))|~(in(ordered_pair(X6,X5),X2)))|in(ordered_pair(X4,X5),X3))))&(?[X4]:?[X5]:((~(in(ordered_pair(X4,X5),X3))|![X6]:(~(in(ordered_pair(X4,X6),X1))|~(in(ordered_pair(X6,X5),X2))))&(in(ordered_pair(X4,X5),X3)|?[X6]:(in(ordered_pair(X4,X6),X1)&in(ordered_pair(X6,X5),X2))))|X3=relation_composition(X1,X2)))))),inference(fof_nnf,[status(thm)],[5])).
% fof(59, plain,![X7]:(~(relation(X7))|![X8]:(~(relation(X8))|![X9]:(~(relation(X9))|((~(X9=relation_composition(X7,X8))|![X10]:![X11]:((~(in(ordered_pair(X10,X11),X9))|?[X12]:(in(ordered_pair(X10,X12),X7)&in(ordered_pair(X12,X11),X8)))&(![X13]:(~(in(ordered_pair(X10,X13),X7))|~(in(ordered_pair(X13,X11),X8)))|in(ordered_pair(X10,X11),X9))))&(?[X14]:?[X15]:((~(in(ordered_pair(X14,X15),X9))|![X16]:(~(in(ordered_pair(X14,X16),X7))|~(in(ordered_pair(X16,X15),X8))))&(in(ordered_pair(X14,X15),X9)|?[X17]:(in(ordered_pair(X14,X17),X7)&in(ordered_pair(X17,X15),X8))))|X9=relation_composition(X7,X8)))))),inference(variable_rename,[status(thm)],[58])).
% fof(60, plain,![X7]:(~(relation(X7))|![X8]:(~(relation(X8))|![X9]:(~(relation(X9))|((~(X9=relation_composition(X7,X8))|![X10]:![X11]:((~(in(ordered_pair(X10,X11),X9))|(in(ordered_pair(X10,esk3_5(X7,X8,X9,X10,X11)),X7)&in(ordered_pair(esk3_5(X7,X8,X9,X10,X11),X11),X8)))&(![X13]:(~(in(ordered_pair(X10,X13),X7))|~(in(ordered_pair(X13,X11),X8)))|in(ordered_pair(X10,X11),X9))))&(((~(in(ordered_pair(esk4_3(X7,X8,X9),esk5_3(X7,X8,X9)),X9))|![X16]:(~(in(ordered_pair(esk4_3(X7,X8,X9),X16),X7))|~(in(ordered_pair(X16,esk5_3(X7,X8,X9)),X8))))&(in(ordered_pair(esk4_3(X7,X8,X9),esk5_3(X7,X8,X9)),X9)|(in(ordered_pair(esk4_3(X7,X8,X9),esk6_3(X7,X8,X9)),X7)&in(ordered_pair(esk6_3(X7,X8,X9),esk5_3(X7,X8,X9)),X8))))|X9=relation_composition(X7,X8)))))),inference(skolemize,[status(esa)],[59])).
% fof(61, plain,![X7]:![X8]:![X9]:![X10]:![X11]:![X13]:![X16]:((((((((~(in(ordered_pair(esk4_3(X7,X8,X9),X16),X7))|~(in(ordered_pair(X16,esk5_3(X7,X8,X9)),X8)))|~(in(ordered_pair(esk4_3(X7,X8,X9),esk5_3(X7,X8,X9)),X9)))&(in(ordered_pair(esk4_3(X7,X8,X9),esk5_3(X7,X8,X9)),X9)|(in(ordered_pair(esk4_3(X7,X8,X9),esk6_3(X7,X8,X9)),X7)&in(ordered_pair(esk6_3(X7,X8,X9),esk5_3(X7,X8,X9)),X8))))|X9=relation_composition(X7,X8))&((((~(in(ordered_pair(X10,X13),X7))|~(in(ordered_pair(X13,X11),X8)))|in(ordered_pair(X10,X11),X9))&(~(in(ordered_pair(X10,X11),X9))|(in(ordered_pair(X10,esk3_5(X7,X8,X9,X10,X11)),X7)&in(ordered_pair(esk3_5(X7,X8,X9,X10,X11),X11),X8))))|~(X9=relation_composition(X7,X8))))|~(relation(X9)))|~(relation(X8)))|~(relation(X7))),inference(shift_quantors,[status(thm)],[60])).
% fof(62, plain,![X7]:![X8]:![X9]:![X10]:![X11]:![X13]:![X16]:((((((((~(in(ordered_pair(esk4_3(X7,X8,X9),X16),X7))|~(in(ordered_pair(X16,esk5_3(X7,X8,X9)),X8)))|~(in(ordered_pair(esk4_3(X7,X8,X9),esk5_3(X7,X8,X9)),X9)))|X9=relation_composition(X7,X8))|~(relation(X9)))|~(relation(X8)))|~(relation(X7)))&((((((in(ordered_pair(esk4_3(X7,X8,X9),esk6_3(X7,X8,X9)),X7)|in(ordered_pair(esk4_3(X7,X8,X9),esk5_3(X7,X8,X9)),X9))|X9=relation_composition(X7,X8))|~(relation(X9)))|~(relation(X8)))|~(relation(X7)))&(((((in(ordered_pair(esk6_3(X7,X8,X9),esk5_3(X7,X8,X9)),X8)|in(ordered_pair(esk4_3(X7,X8,X9),esk5_3(X7,X8,X9)),X9))|X9=relation_composition(X7,X8))|~(relation(X9)))|~(relation(X8)))|~(relation(X7)))))&(((((((~(in(ordered_pair(X10,X13),X7))|~(in(ordered_pair(X13,X11),X8)))|in(ordered_pair(X10,X11),X9))|~(X9=relation_composition(X7,X8)))|~(relation(X9)))|~(relation(X8)))|~(relation(X7)))&((((((in(ordered_pair(X10,esk3_5(X7,X8,X9,X10,X11)),X7)|~(in(ordered_pair(X10,X11),X9)))|~(X9=relation_composition(X7,X8)))|~(relation(X9)))|~(relation(X8)))|~(relation(X7)))&(((((in(ordered_pair(esk3_5(X7,X8,X9,X10,X11),X11),X8)|~(in(ordered_pair(X10,X11),X9)))|~(X9=relation_composition(X7,X8)))|~(relation(X9)))|~(relation(X8)))|~(relation(X7)))))),inference(distribute,[status(thm)],[61])).
% cnf(63,plain,(in(ordered_pair(esk3_5(X1,X2,X3,X4,X5),X5),X2)|~relation(X1)|~relation(X2)|~relation(X3)|X3!=relation_composition(X1,X2)|~in(ordered_pair(X4,X5),X3)),inference(split_conjunct,[status(thm)],[62])).
% cnf(64,plain,(in(ordered_pair(X4,esk3_5(X1,X2,X3,X4,X5)),X1)|~relation(X1)|~relation(X2)|~relation(X3)|X3!=relation_composition(X1,X2)|~in(ordered_pair(X4,X5),X3)),inference(split_conjunct,[status(thm)],[62])).
% cnf(65,plain,(in(ordered_pair(X4,X5),X3)|~relation(X1)|~relation(X2)|~relation(X3)|X3!=relation_composition(X1,X2)|~in(ordered_pair(X6,X5),X2)|~in(ordered_pair(X4,X6),X1)),inference(split_conjunct,[status(thm)],[62])).
% fof(116, plain,![X3]:![X4]:unordered_pair(X3,X4)=unordered_pair(X4,X3),inference(variable_rename,[status(thm)],[21])).
% cnf(117,plain,(unordered_pair(X1,X2)=unordered_pair(X2,X1)),inference(split_conjunct,[status(thm)],[116])).
% fof(118, plain,![X3]:![X4]:ordered_pair(X3,X4)=unordered_pair(unordered_pair(X3,X4),singleton(X3)),inference(variable_rename,[status(thm)],[22])).
% cnf(119,plain,(ordered_pair(X1,X2)=unordered_pair(unordered_pair(X1,X2),singleton(X1))),inference(split_conjunct,[status(thm)],[118])).
% fof(132, negated_conjecture,?[X1]:?[X2]:?[X3]:?[X4]:(relation(X4)&((~(in(ordered_pair(X1,X2),relation_composition(identity_relation(X3),X4)))|(~(in(X1,X3))|~(in(ordered_pair(X1,X2),X4))))&(in(ordered_pair(X1,X2),relation_composition(identity_relation(X3),X4))|(in(X1,X3)&in(ordered_pair(X1,X2),X4))))),inference(fof_nnf,[status(thm)],[32])).
% fof(133, negated_conjecture,?[X5]:?[X6]:?[X7]:?[X8]:(relation(X8)&((~(in(ordered_pair(X5,X6),relation_composition(identity_relation(X7),X8)))|(~(in(X5,X7))|~(in(ordered_pair(X5,X6),X8))))&(in(ordered_pair(X5,X6),relation_composition(identity_relation(X7),X8))|(in(X5,X7)&in(ordered_pair(X5,X6),X8))))),inference(variable_rename,[status(thm)],[132])).
% fof(134, negated_conjecture,(relation(esk15_0)&((~(in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0)))|(~(in(esk12_0,esk14_0))|~(in(ordered_pair(esk12_0,esk13_0),esk15_0))))&(in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0))|(in(esk12_0,esk14_0)&in(ordered_pair(esk12_0,esk13_0),esk15_0))))),inference(skolemize,[status(esa)],[133])).
% fof(135, negated_conjecture,(relation(esk15_0)&((~(in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0)))|(~(in(esk12_0,esk14_0))|~(in(ordered_pair(esk12_0,esk13_0),esk15_0))))&((in(esk12_0,esk14_0)|in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0)))&(in(ordered_pair(esk12_0,esk13_0),esk15_0)|in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0)))))),inference(distribute,[status(thm)],[134])).
% cnf(136,negated_conjecture,(in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0))|in(ordered_pair(esk12_0,esk13_0),esk15_0)),inference(split_conjunct,[status(thm)],[135])).
% cnf(137,negated_conjecture,(in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0))|in(esk12_0,esk14_0)),inference(split_conjunct,[status(thm)],[135])).
% cnf(138,negated_conjecture,(~in(ordered_pair(esk12_0,esk13_0),esk15_0)|~in(esk12_0,esk14_0)|~in(ordered_pair(esk12_0,esk13_0),relation_composition(identity_relation(esk14_0),esk15_0))),inference(split_conjunct,[status(thm)],[135])).
% cnf(139,negated_conjecture,(relation(esk15_0)),inference(split_conjunct,[status(thm)],[135])).
% cnf(140,negated_conjecture,(in(esk12_0,esk14_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))),inference(rw,[status(thm)],[137,119,theory(equality)]),['unfolding']).
% cnf(141,negated_conjecture,(in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[136,119,theory(equality)]),119,theory(equality)]),['unfolding']).
% cnf(144,plain,(X3=X4|identity_relation(X2)!=X1|~relation(X1)|~in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),X1)),inference(rw,[status(thm)],[56,119,theory(equality)]),['unfolding']).
% cnf(145,plain,(in(X3,X2)|identity_relation(X2)!=X1|~relation(X1)|~in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),X1)),inference(rw,[status(thm)],[57,119,theory(equality)]),['unfolding']).
% cnf(148,plain,(in(unordered_pair(unordered_pair(X3,X4),singleton(X3)),X1)|X3!=X4|identity_relation(X2)!=X1|~relation(X1)|~in(X3,X2)),inference(rw,[status(thm)],[55,119,theory(equality)]),['unfolding']).
% cnf(150,plain,(in(unordered_pair(unordered_pair(X4,esk3_5(X1,X2,X3,X4,X5)),singleton(X4)),X1)|relation_composition(X1,X2)!=X3|~relation(X3)|~relation(X2)|~relation(X1)|~in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),X3)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[64,119,theory(equality)]),119,theory(equality)]),['unfolding']).
% cnf(151,plain,(in(unordered_pair(unordered_pair(esk3_5(X1,X2,X3,X4,X5),X5),singleton(esk3_5(X1,X2,X3,X4,X5))),X2)|relation_composition(X1,X2)!=X3|~relation(X3)|~relation(X2)|~relation(X1)|~in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),X3)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[63,119,theory(equality)]),119,theory(equality)]),['unfolding']).
% cnf(152,plain,(in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),X3)|relation_composition(X1,X2)!=X3|~relation(X3)|~relation(X2)|~relation(X1)|~in(unordered_pair(unordered_pair(X6,X5),singleton(X6)),X2)|~in(unordered_pair(unordered_pair(X4,X6),singleton(X4)),X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[65,119,theory(equality)]),119,theory(equality)]),119,theory(equality)]),['unfolding']).
% cnf(155,negated_conjecture,(~in(esk12_0,esk14_0)|~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[138,119,theory(equality)]),119,theory(equality)]),['unfolding']).
% cnf(217,plain,(X1=X2|~relation(identity_relation(X3))|~in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),identity_relation(X3))),inference(er,[status(thm)],[144,theory(equality)])).
% cnf(220,plain,(X1=X2|$false|~in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),identity_relation(X3))),inference(rw,[status(thm)],[217,46,theory(equality)])).
% cnf(221,plain,(X1=X2|~in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),identity_relation(X3))),inference(cn,[status(thm)],[220,theory(equality)])).
% cnf(224,plain,(in(unordered_pair(unordered_pair(X1,X1),singleton(X1)),X2)|identity_relation(X3)!=X2|~relation(X2)|~in(X1,X3)),inference(er,[status(thm)],[148,theory(equality)])).
% cnf(225,plain,(in(X1,X2)|~relation(identity_relation(X2))|~in(unordered_pair(unordered_pair(X1,X3),singleton(X1)),identity_relation(X2))),inference(er,[status(thm)],[145,theory(equality)])).
% cnf(228,plain,(in(X1,X2)|$false|~in(unordered_pair(unordered_pair(X1,X3),singleton(X1)),identity_relation(X2))),inference(rw,[status(thm)],[225,46,theory(equality)])).
% cnf(229,plain,(in(X1,X2)|~in(unordered_pair(unordered_pair(X1,X3),singleton(X1)),identity_relation(X2))),inference(cn,[status(thm)],[228,theory(equality)])).
% cnf(232,plain,(in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),relation_composition(X3,X4))|~relation(relation_composition(X3,X4))|~relation(X4)|~relation(X3)|~in(unordered_pair(unordered_pair(X5,X2),singleton(X5)),X4)|~in(unordered_pair(unordered_pair(X1,X5),singleton(X1)),X3)),inference(er,[status(thm)],[152,theory(equality)])).
% cnf(240,plain,(in(unordered_pair(singleton(X4),unordered_pair(X4,esk3_5(X1,X2,X3,X4,X5))),X1)|relation_composition(X1,X2)!=X3|~relation(X3)|~relation(X2)|~relation(X1)|~in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),X3)),inference(rw,[status(thm)],[150,117,theory(equality)])).
% cnf(241,plain,(in(unordered_pair(singleton(X1),unordered_pair(X1,esk3_5(X2,X3,relation_composition(X2,X3),X1,X4))),X2)|~relation(relation_composition(X2,X3))|~relation(X3)|~relation(X2)|~in(unordered_pair(unordered_pair(X1,X4),singleton(X1)),relation_composition(X2,X3))),inference(er,[status(thm)],[240,theory(equality)])).
% cnf(278,plain,(in(unordered_pair(unordered_pair(X5,esk3_5(X1,X2,X3,X4,X5)),singleton(esk3_5(X1,X2,X3,X4,X5))),X2)|relation_composition(X1,X2)!=X3|~relation(X3)|~relation(X2)|~relation(X1)|~in(unordered_pair(unordered_pair(X4,X5),singleton(X4)),X3)),inference(rw,[status(thm)],[151,117,theory(equality)])).
% cnf(279,plain,(in(unordered_pair(unordered_pair(X1,esk3_5(X2,X3,relation_composition(X2,X3),X4,X1)),singleton(esk3_5(X2,X3,relation_composition(X2,X3),X4,X1))),X3)|~relation(relation_composition(X2,X3))|~relation(X3)|~relation(X2)|~in(unordered_pair(unordered_pair(X4,X1),singleton(X4)),relation_composition(X2,X3))),inference(er,[status(thm)],[278,theory(equality)])).
% cnf(585,plain,(X1=X2|~in(unordered_pair(singleton(X1),unordered_pair(X1,X2)),identity_relation(X3))),inference(spm,[status(thm)],[221,117,theory(equality)])).
% cnf(661,plain,(in(X1,X2)|~in(unordered_pair(singleton(X1),unordered_pair(X1,X3)),identity_relation(X2))),inference(spm,[status(thm)],[229,117,theory(equality)])).
% cnf(1179,plain,(in(unordered_pair(unordered_pair(X1,X1),singleton(X1)),identity_relation(X2))|~relation(identity_relation(X2))|~in(X1,X2)),inference(er,[status(thm)],[224,theory(equality)])).
% cnf(1184,plain,(in(unordered_pair(unordered_pair(X1,X1),singleton(X1)),identity_relation(X2))|$false|~in(X1,X2)),inference(rw,[status(thm)],[1179,46,theory(equality)])).
% cnf(1185,plain,(in(unordered_pair(unordered_pair(X1,X1),singleton(X1)),identity_relation(X2))|~in(X1,X2)),inference(cn,[status(thm)],[1184,theory(equality)])).
% cnf(1579,plain,(in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),relation_composition(X3,X4))|~relation(X4)|~relation(X3)|~in(unordered_pair(unordered_pair(X5,X2),singleton(X5)),X4)|~in(unordered_pair(unordered_pair(X1,X5),singleton(X1)),X3)),inference(csr,[status(thm)],[232,44])).
% cnf(1677,plain,(in(unordered_pair(singleton(X1),unordered_pair(X1,esk3_5(X2,X3,relation_composition(X2,X3),X1,X4))),X2)|~relation(X3)|~relation(X2)|~in(unordered_pair(unordered_pair(X1,X4),singleton(X1)),relation_composition(X2,X3))),inference(csr,[status(thm)],[241,44])).
% cnf(1702,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(esk12_0,esk14_0)|~relation(esk15_0)|~relation(identity_relation(esk14_0))),inference(spm,[status(thm)],[1677,140,theory(equality)])).
% cnf(1703,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|~relation(esk15_0)|~relation(identity_relation(esk14_0))),inference(spm,[status(thm)],[1677,141,theory(equality)])).
% cnf(1704,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(esk12_0,esk14_0)|$false|~relation(identity_relation(esk14_0))),inference(rw,[status(thm)],[1702,139,theory(equality)])).
% cnf(1705,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(esk12_0,esk14_0)|$false|$false),inference(rw,[status(thm)],[1704,46,theory(equality)])).
% cnf(1706,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(esk12_0,esk14_0)),inference(cn,[status(thm)],[1705,theory(equality)])).
% cnf(1707,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|$false|~relation(identity_relation(esk14_0))),inference(rw,[status(thm)],[1703,139,theory(equality)])).
% cnf(1708,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|$false|$false),inference(rw,[status(thm)],[1707,46,theory(equality)])).
% cnf(1709,negated_conjecture,(in(unordered_pair(singleton(esk12_0),unordered_pair(esk12_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),identity_relation(esk14_0))|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)),inference(cn,[status(thm)],[1708,theory(equality)])).
% cnf(1710,negated_conjecture,(in(esk12_0,esk14_0)),inference(csr,[status(thm)],[1706,661])).
% cnf(1714,negated_conjecture,(in(unordered_pair(unordered_pair(esk12_0,esk12_0),singleton(esk12_0)),identity_relation(esk14_0))),inference(spm,[status(thm)],[1185,1710,theory(equality)])).
% cnf(1723,negated_conjecture,(~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))|~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|$false),inference(rw,[status(thm)],[155,1710,theory(equality)])).
% cnf(1724,negated_conjecture,(~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))|~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)),inference(cn,[status(thm)],[1723,theory(equality)])).
% cnf(1953,negated_conjecture,(esk12_0=esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)),inference(spm,[status(thm)],[585,1709,theory(equality)])).
% cnf(3515,plain,(in(unordered_pair(unordered_pair(X1,esk3_5(X2,X3,relation_composition(X2,X3),X4,X1)),singleton(esk3_5(X2,X3,relation_composition(X2,X3),X4,X1))),X3)|~relation(X3)|~relation(X2)|~in(unordered_pair(unordered_pair(X4,X1),singleton(X4)),relation_composition(X2,X3))),inference(csr,[status(thm)],[279,44])).
% cnf(3544,negated_conjecture,(in(unordered_pair(unordered_pair(esk13_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0)),singleton(esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),esk15_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|~relation(esk15_0)|~relation(identity_relation(esk14_0))),inference(spm,[status(thm)],[3515,141,theory(equality)])).
% cnf(3545,negated_conjecture,(in(unordered_pair(unordered_pair(esk13_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0)),singleton(esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),esk15_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|$false|~relation(identity_relation(esk14_0))),inference(rw,[status(thm)],[3544,139,theory(equality)])).
% cnf(3546,negated_conjecture,(in(unordered_pair(unordered_pair(esk13_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0)),singleton(esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),esk15_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|$false|$false),inference(rw,[status(thm)],[3545,46,theory(equality)])).
% cnf(3547,negated_conjecture,(in(unordered_pair(unordered_pair(esk13_0,esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0)),singleton(esk3_5(identity_relation(esk14_0),esk15_0,relation_composition(identity_relation(esk14_0),esk15_0),esk12_0,esk13_0))),esk15_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)),inference(cn,[status(thm)],[3546,theory(equality)])).
% cnf(3578,negated_conjecture,(in(unordered_pair(unordered_pair(esk13_0,esk12_0),singleton(esk12_0)),esk15_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)),inference(spm,[status(thm)],[3547,1953,theory(equality)])).
% cnf(3638,negated_conjecture,(in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)|in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)),inference(rw,[status(thm)],[3578,117,theory(equality)])).
% cnf(3639,negated_conjecture,(in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),esk15_0)),inference(cn,[status(thm)],[3638,theory(equality)])).
% cnf(3644,negated_conjecture,(in(unordered_pair(unordered_pair(X1,esk13_0),singleton(X1)),relation_composition(X2,esk15_0))|~relation(esk15_0)|~relation(X2)|~in(unordered_pair(unordered_pair(X1,esk12_0),singleton(X1)),X2)),inference(spm,[status(thm)],[1579,3639,theory(equality)])).
% cnf(3672,negated_conjecture,(~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))|$false),inference(rw,[status(thm)],[1724,3639,theory(equality)])).
% cnf(3673,negated_conjecture,(~in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))),inference(cn,[status(thm)],[3672,theory(equality)])).
% cnf(3677,negated_conjecture,(in(unordered_pair(unordered_pair(X1,esk13_0),singleton(X1)),relation_composition(X2,esk15_0))|$false|~relation(X2)|~in(unordered_pair(unordered_pair(X1,esk12_0),singleton(X1)),X2)),inference(rw,[status(thm)],[3644,139,theory(equality)])).
% cnf(3678,negated_conjecture,(in(unordered_pair(unordered_pair(X1,esk13_0),singleton(X1)),relation_composition(X2,esk15_0))|~relation(X2)|~in(unordered_pair(unordered_pair(X1,esk12_0),singleton(X1)),X2)),inference(cn,[status(thm)],[3677,theory(equality)])).
% cnf(5274,negated_conjecture,(in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))|~relation(identity_relation(esk14_0))),inference(spm,[status(thm)],[3678,1714,theory(equality)])).
% cnf(5275,negated_conjecture,(in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))|$false),inference(rw,[status(thm)],[5274,46,theory(equality)])).
% cnf(5276,negated_conjecture,(in(unordered_pair(unordered_pair(esk12_0,esk13_0),singleton(esk12_0)),relation_composition(identity_relation(esk14_0),esk15_0))),inference(cn,[status(thm)],[5275,theory(equality)])).
% cnf(5277,negated_conjecture,($false),inference(sr,[status(thm)],[5276,3673,theory(equality)])).
% cnf(5278,negated_conjecture,($false),5277,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1049
% # ...of these trivial : 2
% # ...subsumed : 873
% # ...remaining for further processing: 174
% # Other redundant clauses eliminated : 24
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 2
% # Backward-rewritten : 44
% # Generated clauses : 3956
% # ...of the previous two non-trivial : 3777
% # Contextual simplify-reflections : 542
% # Paramodulations : 3920
% # Factorizations : 0
% # Equation resolutions : 31
% # Current number of processed clauses: 125
% # Positive orientable unit clauses: 24
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 20
% # Non-unit-clauses : 80
% # Current number of unprocessed clauses: 2026
% # ...number of literals in the above : 10806
% # Clause-clause subsumption calls (NU) : 10958
% # Rec. Clause-clause subsumption calls : 7339
% # Unit Clause-clause subsumption calls : 177
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 19
% # Indexed BW rewrite successes : 12
% # Backwards rewriting index: 138 leaves, 2.00+/-2.496 terms/leaf
% # Paramod-from index: 33 leaves, 1.42+/-0.818 terms/leaf
% # Paramod-into index: 113 leaves, 1.58+/-1.195 terms/leaf
% # -------------------------------------------------
% # User time : 0.198 s
% # System time : 0.007 s
% # Total time : 0.205 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.36 CPU 0.44 WC
% FINAL PrfWatch: 0.36 CPU 0.44 WC
% SZS output end Solution for /tmp/SystemOnTPTP26685/SEU191+1.tptp
%
%------------------------------------------------------------------------------