%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU447+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.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 06:37:14 EST 2010
% Result : Theorem 7.71s
% Output : Solution 7.71s
% 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/SystemOnTPTP9659/SEU447+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP9659/SEU447+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP9659/SEU447+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 9755
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.93 CPU 2.02 WC
% PrfWatch: 3.92 CPU 4.03 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 5.91 CPU 6.03 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:(m1_subset_1(X2,k1_zfmisc_1(X1))=>m1_subset_1(k3_subset_1(X1,X2),k1_zfmisc_1(X1))),file('/tmp/SRASS.s.p', dt_k3_subset_1)).
% fof(2, axiom,![X1]:![X2]:![X3]:![X4]:((m1_subset_1(X3,k1_zfmisc_1(X1))&m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))=>m1_subset_1(k8_relset_2(X1,X2,X3,X4),k1_zfmisc_1(X2))),file('/tmp/SRASS.s.p', dt_k8_relset_2)).
% fof(3, axiom,![X1]:![X2]:![X3]:![X4]:![X5]:((m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))&m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X2,X3))))=>m2_relset_1(k9_relset_2(X1,X2,X3,X4,X5),X1,X3)),file('/tmp/SRASS.s.p', dt_k9_relset_2)).
% fof(4, axiom,![X1]:![X2]:![X3]:(m2_relset_1(X3,X1,X2)=>m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),file('/tmp/SRASS.s.p', dt_m2_relset_1)).
% fof(7, axiom,![X1]:![X2]:(m1_subset_1(X2,k1_zfmisc_1(X1))=>k3_subset_1(X1,k3_subset_1(X1,X2))=X2),file('/tmp/SRASS.s.p', involutiveness_k3_subset_1)).
% fof(8, axiom,![X1]:![X2]:![X3]:(m1_subset_1(X3,k1_zfmisc_1(X1))=>![X4]:(m2_relset_1(X4,X1,X2)=>k3_subset_1(X2,k10_relset_1(X1,X2,X4,X3))=k8_relset_2(X1,X2,X3,k3_subset_1(k2_zfmisc_1(X1,X2),X4)))),file('/tmp/SRASS.s.p', t50_relset_2)).
% fof(9, axiom,![X1]:![X2]:![X3]:(m1_subset_1(X3,k1_zfmisc_1(X1))=>![X4]:(m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))=>k3_subset_1(X2,k8_relset_2(X1,X2,X3,X4))=k9_relat_1(k3_subset_1(k2_zfmisc_1(X1,X2),X4),X3))),file('/tmp/SRASS.s.p', t49_relset_2)).
% fof(10, axiom,![X1]:![X2]:![X3]:![X4]:![X5]:((m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))&m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X2,X3))))=>k9_relset_2(X1,X2,X3,X4,X5)=k5_relat_1(X4,X5)),file('/tmp/SRASS.s.p', redefinition_k9_relset_2)).
% fof(12, axiom,![X1]:![X2]:![X3]:(m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))=>v1_relat_1(X3)),file('/tmp/SRASS.s.p', cc1_relset_1)).
% fof(13, axiom,![X1]:![X2]:![X3]:![X4]:(m1_relset_1(X3,X1,X2)=>m1_subset_1(k10_relset_1(X1,X2,X3,X4),k1_zfmisc_1(X2))),file('/tmp/SRASS.s.p', dt_k10_relset_1)).
% fof(28, axiom,![X1]:![X2]:![X3]:(m2_relset_1(X3,X1,X2)<=>m1_relset_1(X3,X1,X2)),file('/tmp/SRASS.s.p', redefinition_m2_relset_1)).
% fof(32, axiom,![X1]:![X2]:![X3]:![X4]:(m1_relset_1(X3,X1,X2)=>k10_relset_1(X1,X2,X3,X4)=k9_relat_1(X3,X4)),file('/tmp/SRASS.s.p', redefinition_k10_relset_1)).
% fof(45, axiom,![X1]:![X2]:(v1_relat_1(X2)=>![X3]:(v1_relat_1(X3)=>k9_relat_1(k5_relat_1(X2,X3),X1)=k9_relat_1(X3,k9_relat_1(X2,X1)))),file('/tmp/SRASS.s.p', t159_relat_1)).
% fof(60, conjecture,![X1]:![X2]:![X3]:![X4]:(m1_subset_1(X4,k1_zfmisc_1(X1))=>![X5]:(m2_relset_1(X5,X1,X2)=>![X6]:(m2_relset_1(X6,X2,X3)=>k8_relset_2(X2,X3,k10_relset_1(X1,X2,X5,X4),X6)=k8_relset_2(X1,X3,X4,k3_subset_1(k2_zfmisc_1(X1,X3),k9_relset_2(X1,X2,X3,X5,k3_subset_1(k2_zfmisc_1(X2,X3),X6))))))),file('/tmp/SRASS.s.p', t59_relset_2)).
% fof(61, negated_conjecture,~(![X1]:![X2]:![X3]:![X4]:(m1_subset_1(X4,k1_zfmisc_1(X1))=>![X5]:(m2_relset_1(X5,X1,X2)=>![X6]:(m2_relset_1(X6,X2,X3)=>k8_relset_2(X2,X3,k10_relset_1(X1,X2,X5,X4),X6)=k8_relset_2(X1,X3,X4,k3_subset_1(k2_zfmisc_1(X1,X3),k9_relset_2(X1,X2,X3,X5,k3_subset_1(k2_zfmisc_1(X2,X3),X6)))))))),inference(assume_negation,[status(cth)],[60])).
% fof(67, plain,![X1]:![X2]:(~(m1_subset_1(X2,k1_zfmisc_1(X1)))|m1_subset_1(k3_subset_1(X1,X2),k1_zfmisc_1(X1))),inference(fof_nnf,[status(thm)],[1])).
% fof(68, plain,![X3]:![X4]:(~(m1_subset_1(X4,k1_zfmisc_1(X3)))|m1_subset_1(k3_subset_1(X3,X4),k1_zfmisc_1(X3))),inference(variable_rename,[status(thm)],[67])).
% cnf(69,plain,(m1_subset_1(k3_subset_1(X1,X2),k1_zfmisc_1(X1))|~m1_subset_1(X2,k1_zfmisc_1(X1))),inference(split_conjunct,[status(thm)],[68])).
% fof(70, plain,![X1]:![X2]:![X3]:![X4]:((~(m1_subset_1(X3,k1_zfmisc_1(X1)))|~(m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))))|m1_subset_1(k8_relset_2(X1,X2,X3,X4),k1_zfmisc_1(X2))),inference(fof_nnf,[status(thm)],[2])).
% fof(71, plain,![X5]:![X6]:![X7]:![X8]:((~(m1_subset_1(X7,k1_zfmisc_1(X5)))|~(m1_subset_1(X8,k1_zfmisc_1(k2_zfmisc_1(X5,X6)))))|m1_subset_1(k8_relset_2(X5,X6,X7,X8),k1_zfmisc_1(X6))),inference(variable_rename,[status(thm)],[70])).
% cnf(72,plain,(m1_subset_1(k8_relset_2(X1,X2,X3,X4),k1_zfmisc_1(X2))|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|~m1_subset_1(X3,k1_zfmisc_1(X1))),inference(split_conjunct,[status(thm)],[71])).
% fof(73, plain,![X1]:![X2]:![X3]:![X4]:![X5]:((~(m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))|~(m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))))|m2_relset_1(k9_relset_2(X1,X2,X3,X4,X5),X1,X3)),inference(fof_nnf,[status(thm)],[3])).
% fof(74, plain,![X6]:![X7]:![X8]:![X9]:![X10]:((~(m1_subset_1(X9,k1_zfmisc_1(k2_zfmisc_1(X6,X7))))|~(m1_subset_1(X10,k1_zfmisc_1(k2_zfmisc_1(X7,X8)))))|m2_relset_1(k9_relset_2(X6,X7,X8,X9,X10),X6,X8)),inference(variable_rename,[status(thm)],[73])).
% cnf(75,plain,(m2_relset_1(k9_relset_2(X1,X2,X3,X4,X5),X1,X3)|~m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),inference(split_conjunct,[status(thm)],[74])).
% fof(76, plain,![X1]:![X2]:![X3]:(~(m2_relset_1(X3,X1,X2))|m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),inference(fof_nnf,[status(thm)],[4])).
% fof(77, plain,![X4]:![X5]:![X6]:(~(m2_relset_1(X6,X4,X5))|m1_subset_1(X6,k1_zfmisc_1(k2_zfmisc_1(X4,X5)))),inference(variable_rename,[status(thm)],[76])).
% cnf(78,plain,(m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))|~m2_relset_1(X1,X2,X3)),inference(split_conjunct,[status(thm)],[77])).
% fof(85, plain,![X1]:![X2]:(~(m1_subset_1(X2,k1_zfmisc_1(X1)))|k3_subset_1(X1,k3_subset_1(X1,X2))=X2),inference(fof_nnf,[status(thm)],[7])).
% fof(86, plain,![X3]:![X4]:(~(m1_subset_1(X4,k1_zfmisc_1(X3)))|k3_subset_1(X3,k3_subset_1(X3,X4))=X4),inference(variable_rename,[status(thm)],[85])).
% cnf(87,plain,(k3_subset_1(X1,k3_subset_1(X1,X2))=X2|~m1_subset_1(X2,k1_zfmisc_1(X1))),inference(split_conjunct,[status(thm)],[86])).
% fof(88, plain,![X1]:![X2]:![X3]:(~(m1_subset_1(X3,k1_zfmisc_1(X1)))|![X4]:(~(m2_relset_1(X4,X1,X2))|k3_subset_1(X2,k10_relset_1(X1,X2,X4,X3))=k8_relset_2(X1,X2,X3,k3_subset_1(k2_zfmisc_1(X1,X2),X4)))),inference(fof_nnf,[status(thm)],[8])).
% fof(89, plain,![X5]:![X6]:![X7]:(~(m1_subset_1(X7,k1_zfmisc_1(X5)))|![X8]:(~(m2_relset_1(X8,X5,X6))|k3_subset_1(X6,k10_relset_1(X5,X6,X8,X7))=k8_relset_2(X5,X6,X7,k3_subset_1(k2_zfmisc_1(X5,X6),X8)))),inference(variable_rename,[status(thm)],[88])).
% fof(90, plain,![X5]:![X6]:![X7]:![X8]:((~(m2_relset_1(X8,X5,X6))|k3_subset_1(X6,k10_relset_1(X5,X6,X8,X7))=k8_relset_2(X5,X6,X7,k3_subset_1(k2_zfmisc_1(X5,X6),X8)))|~(m1_subset_1(X7,k1_zfmisc_1(X5)))),inference(shift_quantors,[status(thm)],[89])).
% cnf(91,plain,(k3_subset_1(X3,k10_relset_1(X2,X3,X4,X1))=k8_relset_2(X2,X3,X1,k3_subset_1(k2_zfmisc_1(X2,X3),X4))|~m1_subset_1(X1,k1_zfmisc_1(X2))|~m2_relset_1(X4,X2,X3)),inference(split_conjunct,[status(thm)],[90])).
% fof(92, plain,![X1]:![X2]:![X3]:(~(m1_subset_1(X3,k1_zfmisc_1(X1)))|![X4]:(~(m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))|k3_subset_1(X2,k8_relset_2(X1,X2,X3,X4))=k9_relat_1(k3_subset_1(k2_zfmisc_1(X1,X2),X4),X3))),inference(fof_nnf,[status(thm)],[9])).
% fof(93, plain,![X5]:![X6]:![X7]:(~(m1_subset_1(X7,k1_zfmisc_1(X5)))|![X8]:(~(m1_subset_1(X8,k1_zfmisc_1(k2_zfmisc_1(X5,X6))))|k3_subset_1(X6,k8_relset_2(X5,X6,X7,X8))=k9_relat_1(k3_subset_1(k2_zfmisc_1(X5,X6),X8),X7))),inference(variable_rename,[status(thm)],[92])).
% fof(94, plain,![X5]:![X6]:![X7]:![X8]:((~(m1_subset_1(X8,k1_zfmisc_1(k2_zfmisc_1(X5,X6))))|k3_subset_1(X6,k8_relset_2(X5,X6,X7,X8))=k9_relat_1(k3_subset_1(k2_zfmisc_1(X5,X6),X8),X7))|~(m1_subset_1(X7,k1_zfmisc_1(X5)))),inference(shift_quantors,[status(thm)],[93])).
% cnf(95,plain,(k3_subset_1(X3,k8_relset_2(X2,X3,X1,X4))=k9_relat_1(k3_subset_1(k2_zfmisc_1(X2,X3),X4),X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))),inference(split_conjunct,[status(thm)],[94])).
% fof(96, plain,![X1]:![X2]:![X3]:![X4]:![X5]:((~(m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))|~(m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))))|k9_relset_2(X1,X2,X3,X4,X5)=k5_relat_1(X4,X5)),inference(fof_nnf,[status(thm)],[10])).
% fof(97, plain,![X6]:![X7]:![X8]:![X9]:![X10]:((~(m1_subset_1(X9,k1_zfmisc_1(k2_zfmisc_1(X6,X7))))|~(m1_subset_1(X10,k1_zfmisc_1(k2_zfmisc_1(X7,X8)))))|k9_relset_2(X6,X7,X8,X9,X10)=k5_relat_1(X9,X10)),inference(variable_rename,[status(thm)],[96])).
% cnf(98,plain,(k9_relset_2(X1,X2,X3,X4,X5)=k5_relat_1(X4,X5)|~m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),inference(split_conjunct,[status(thm)],[97])).
% fof(102, plain,![X1]:![X2]:![X3]:(~(m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))|v1_relat_1(X3)),inference(fof_nnf,[status(thm)],[12])).
% fof(103, plain,![X4]:![X5]:![X6]:(~(m1_subset_1(X6,k1_zfmisc_1(k2_zfmisc_1(X4,X5))))|v1_relat_1(X6)),inference(variable_rename,[status(thm)],[102])).
% cnf(104,plain,(v1_relat_1(X1)|~m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))),inference(split_conjunct,[status(thm)],[103])).
% fof(105, plain,![X1]:![X2]:![X3]:![X4]:(~(m1_relset_1(X3,X1,X2))|m1_subset_1(k10_relset_1(X1,X2,X3,X4),k1_zfmisc_1(X2))),inference(fof_nnf,[status(thm)],[13])).
% fof(106, plain,![X5]:![X6]:![X7]:![X8]:(~(m1_relset_1(X7,X5,X6))|m1_subset_1(k10_relset_1(X5,X6,X7,X8),k1_zfmisc_1(X6))),inference(variable_rename,[status(thm)],[105])).
% cnf(107,plain,(m1_subset_1(k10_relset_1(X1,X2,X3,X4),k1_zfmisc_1(X2))|~m1_relset_1(X3,X1,X2)),inference(split_conjunct,[status(thm)],[106])).
% fof(155, plain,![X1]:![X2]:![X3]:((~(m2_relset_1(X3,X1,X2))|m1_relset_1(X3,X1,X2))&(~(m1_relset_1(X3,X1,X2))|m2_relset_1(X3,X1,X2))),inference(fof_nnf,[status(thm)],[28])).
% fof(156, plain,![X4]:![X5]:![X6]:((~(m2_relset_1(X6,X4,X5))|m1_relset_1(X6,X4,X5))&(~(m1_relset_1(X6,X4,X5))|m2_relset_1(X6,X4,X5))),inference(variable_rename,[status(thm)],[155])).
% cnf(158,plain,(m1_relset_1(X1,X2,X3)|~m2_relset_1(X1,X2,X3)),inference(split_conjunct,[status(thm)],[156])).
% fof(169, plain,![X1]:![X2]:![X3]:![X4]:(~(m1_relset_1(X3,X1,X2))|k10_relset_1(X1,X2,X3,X4)=k9_relat_1(X3,X4)),inference(fof_nnf,[status(thm)],[32])).
% fof(170, plain,![X5]:![X6]:![X7]:![X8]:(~(m1_relset_1(X7,X5,X6))|k10_relset_1(X5,X6,X7,X8)=k9_relat_1(X7,X8)),inference(variable_rename,[status(thm)],[169])).
% cnf(171,plain,(k10_relset_1(X1,X2,X3,X4)=k9_relat_1(X3,X4)|~m1_relset_1(X3,X1,X2)),inference(split_conjunct,[status(thm)],[170])).
% fof(209, plain,![X1]:![X2]:(~(v1_relat_1(X2))|![X3]:(~(v1_relat_1(X3))|k9_relat_1(k5_relat_1(X2,X3),X1)=k9_relat_1(X3,k9_relat_1(X2,X1)))),inference(fof_nnf,[status(thm)],[45])).
% fof(210, plain,![X4]:![X5]:(~(v1_relat_1(X5))|![X6]:(~(v1_relat_1(X6))|k9_relat_1(k5_relat_1(X5,X6),X4)=k9_relat_1(X6,k9_relat_1(X5,X4)))),inference(variable_rename,[status(thm)],[209])).
% fof(211, plain,![X4]:![X5]:![X6]:((~(v1_relat_1(X6))|k9_relat_1(k5_relat_1(X5,X6),X4)=k9_relat_1(X6,k9_relat_1(X5,X4)))|~(v1_relat_1(X5))),inference(shift_quantors,[status(thm)],[210])).
% cnf(212,plain,(k9_relat_1(k5_relat_1(X1,X2),X3)=k9_relat_1(X2,k9_relat_1(X1,X3))|~v1_relat_1(X1)|~v1_relat_1(X2)),inference(split_conjunct,[status(thm)],[211])).
% fof(249, negated_conjecture,?[X1]:?[X2]:?[X3]:?[X4]:(m1_subset_1(X4,k1_zfmisc_1(X1))&?[X5]:(m2_relset_1(X5,X1,X2)&?[X6]:(m2_relset_1(X6,X2,X3)&~(k8_relset_2(X2,X3,k10_relset_1(X1,X2,X5,X4),X6)=k8_relset_2(X1,X3,X4,k3_subset_1(k2_zfmisc_1(X1,X3),k9_relset_2(X1,X2,X3,X5,k3_subset_1(k2_zfmisc_1(X2,X3),X6)))))))),inference(fof_nnf,[status(thm)],[61])).
% fof(250, negated_conjecture,?[X7]:?[X8]:?[X9]:?[X10]:(m1_subset_1(X10,k1_zfmisc_1(X7))&?[X11]:(m2_relset_1(X11,X7,X8)&?[X12]:(m2_relset_1(X12,X8,X9)&~(k8_relset_2(X8,X9,k10_relset_1(X7,X8,X11,X10),X12)=k8_relset_2(X7,X9,X10,k3_subset_1(k2_zfmisc_1(X7,X9),k9_relset_2(X7,X8,X9,X11,k3_subset_1(k2_zfmisc_1(X8,X9),X12)))))))),inference(variable_rename,[status(thm)],[249])).
% fof(251, negated_conjecture,(m1_subset_1(esk14_0,k1_zfmisc_1(esk11_0))&(m2_relset_1(esk15_0,esk11_0,esk12_0)&(m2_relset_1(esk16_0,esk12_0,esk13_0)&~(k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)=k8_relset_2(esk11_0,esk13_0,esk14_0,k3_subset_1(k2_zfmisc_1(esk11_0,esk13_0),k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)))))))),inference(skolemize,[status(esa)],[250])).
% cnf(252,negated_conjecture,(k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)!=k8_relset_2(esk11_0,esk13_0,esk14_0,k3_subset_1(k2_zfmisc_1(esk11_0,esk13_0),k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0))))),inference(split_conjunct,[status(thm)],[251])).
% cnf(253,negated_conjecture,(m2_relset_1(esk16_0,esk12_0,esk13_0)),inference(split_conjunct,[status(thm)],[251])).
% cnf(254,negated_conjecture,(m2_relset_1(esk15_0,esk11_0,esk12_0)),inference(split_conjunct,[status(thm)],[251])).
% cnf(255,negated_conjecture,(m1_subset_1(esk14_0,k1_zfmisc_1(esk11_0))),inference(split_conjunct,[status(thm)],[251])).
% cnf(269,plain,(v1_relat_1(k3_subset_1(k2_zfmisc_1(X1,X2),X3))|~m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),inference(spm,[status(thm)],[104,69,theory(equality)])).
% cnf(277,plain,(v1_relat_1(X1)|~m2_relset_1(X1,X2,X3)),inference(spm,[status(thm)],[104,78,theory(equality)])).
% cnf(312,plain,(m1_subset_1(k9_relat_1(X3,X4),k1_zfmisc_1(X2))|~m1_relset_1(X3,X1,X2)),inference(spm,[status(thm)],[107,171,theory(equality)])).
% cnf(316,plain,(k3_subset_1(X1,k9_relat_1(k3_subset_1(k2_zfmisc_1(X2,X1),X4),X3))=k8_relset_2(X2,X1,X3,X4)|~m1_subset_1(k8_relset_2(X2,X1,X3,X4),k1_zfmisc_1(X1))|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X2,X1)))|~m1_subset_1(X3,k1_zfmisc_1(X2))),inference(spm,[status(thm)],[87,95,theory(equality)])).
% cnf(322,plain,(m2_relset_1(k5_relat_1(X4,X5),X1,X3)|~m1_subset_1(X5,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),inference(spm,[status(thm)],[75,98,theory(equality)])).
% cnf(323,negated_conjecture,(k3_subset_1(esk13_0,k10_relset_1(esk11_0,esk13_0,k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk14_0))!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_subset_1(esk14_0,k1_zfmisc_1(esk11_0))),inference(spm,[status(thm)],[252,91,theory(equality)])).
% cnf(328,negated_conjecture,(k3_subset_1(esk13_0,k10_relset_1(esk11_0,esk13_0,k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk14_0))!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|$false),inference(rw,[status(thm)],[323,255,theory(equality)])).
% cnf(329,negated_conjecture,(k3_subset_1(esk13_0,k10_relset_1(esk11_0,esk13_0,k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk14_0))!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)),inference(cn,[status(thm)],[328,theory(equality)])).
% cnf(343,negated_conjecture,(k3_subset_1(esk13_0,k9_relat_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk14_0))!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_relset_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)),inference(spm,[status(thm)],[329,171,theory(equality)])).
% cnf(378,negated_conjecture,(v1_relat_1(esk15_0)),inference(spm,[status(thm)],[277,254,theory(equality)])).
% cnf(390,negated_conjecture,(k3_subset_1(esk13_0,k9_relat_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk14_0))!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k9_relset_2(esk11_0,esk12_0,esk13_0,esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)),inference(csr,[status(thm)],[343,158])).
% cnf(391,negated_conjecture,(k3_subset_1(esk13_0,k9_relat_1(k5_relat_1(esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk14_0))!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k5_relat_1(esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_subset_1(k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0),k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))),inference(spm,[status(thm)],[390,98,theory(equality)])).
% cnf(481,plain,(m1_subset_1(k9_relat_1(X1,X2),k1_zfmisc_1(X3))|~m2_relset_1(X1,X4,X3)),inference(spm,[status(thm)],[312,158,theory(equality)])).
% cnf(516,negated_conjecture,(m1_subset_1(k9_relat_1(esk15_0,X1),k1_zfmisc_1(esk12_0))),inference(spm,[status(thm)],[481,254,theory(equality)])).
% cnf(1522,plain,(k3_subset_1(X1,k9_relat_1(k3_subset_1(k2_zfmisc_1(X2,X1),X4),X3))=k8_relset_2(X2,X1,X3,X4)|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X2,X1)))|~m1_subset_1(X3,k1_zfmisc_1(X2))),inference(csr,[status(thm)],[316,72])).
% cnf(1535,plain,(k3_subset_1(X1,k9_relat_1(k5_relat_1(X4,k3_subset_1(k2_zfmisc_1(X2,X1),X3)),X5))=k8_relset_2(X2,X1,k9_relat_1(X4,X5),X3)|~m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X2,X1)))|~m1_subset_1(k9_relat_1(X4,X5),k1_zfmisc_1(X2))|~v1_relat_1(k3_subset_1(k2_zfmisc_1(X2,X1),X3))|~v1_relat_1(X4)),inference(spm,[status(thm)],[1522,212,theory(equality)])).
% cnf(2107,plain,(m2_relset_1(k5_relat_1(X1,k3_subset_1(k2_zfmisc_1(X2,X3),X4)),X5,X3)|~m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X5,X2)))|~m1_subset_1(X4,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))),inference(spm,[status(thm)],[322,69,theory(equality)])).
% cnf(33555,plain,(k3_subset_1(X1,k9_relat_1(k5_relat_1(X4,k3_subset_1(k2_zfmisc_1(X2,X1),X3)),X5))=k8_relset_2(X2,X1,k9_relat_1(X4,X5),X3)|~v1_relat_1(X4)|~m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X2,X1)))|~m1_subset_1(k9_relat_1(X4,X5),k1_zfmisc_1(X2))),inference(csr,[status(thm)],[1535,269])).
% cnf(33557,negated_conjecture,(k8_relset_2(esk12_0,esk13_0,k9_relat_1(esk15_0,esk14_0),esk16_0)!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k5_relat_1(esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_subset_1(k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0),k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~v1_relat_1(esk15_0)|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_subset_1(k9_relat_1(esk15_0,esk14_0),k1_zfmisc_1(esk12_0))),inference(spm,[status(thm)],[391,33555,theory(equality)])).
% cnf(33687,negated_conjecture,(k8_relset_2(esk12_0,esk13_0,k9_relat_1(esk15_0,esk14_0),esk16_0)!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k5_relat_1(esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_subset_1(k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0),k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|$false|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_subset_1(k9_relat_1(esk15_0,esk14_0),k1_zfmisc_1(esk12_0))),inference(rw,[status(thm)],[33557,378,theory(equality)])).
% cnf(33688,negated_conjecture,(k8_relset_2(esk12_0,esk13_0,k9_relat_1(esk15_0,esk14_0),esk16_0)!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k5_relat_1(esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_subset_1(k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0),k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|$false|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|$false),inference(rw,[status(thm)],[33687,516,theory(equality)])).
% cnf(33689,negated_conjecture,(k8_relset_2(esk12_0,esk13_0,k9_relat_1(esk15_0,esk14_0),esk16_0)!=k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)|~m2_relset_1(k5_relat_1(esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_subset_1(k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0),k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))),inference(cn,[status(thm)],[33688,theory(equality)])).
% cnf(33710,negated_conjecture,(k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)!=k8_relset_2(esk12_0,esk13_0,k9_relat_1(esk15_0,esk14_0),esk16_0)|~m2_relset_1(k5_relat_1(esk15_0,k3_subset_1(k2_zfmisc_1(esk12_0,esk13_0),esk16_0)),esk11_0,esk13_0)|~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))),inference(csr,[status(thm)],[33689,69])).
% cnf(102698,negated_conjecture,(k8_relset_2(esk12_0,esk13_0,k10_relset_1(esk11_0,esk12_0,esk15_0,esk14_0),esk16_0)!=k8_relset_2(esk12_0,esk13_0,k9_relat_1(esk15_0,esk14_0),esk16_0)|~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))),inference(spm,[status(thm)],[33710,2107,theory(equality)])).
% cnf(102804,negated_conjecture,(~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m1_relset_1(esk15_0,esk11_0,esk12_0)),inference(spm,[status(thm)],[102698,171,theory(equality)])).
% cnf(102805,negated_conjecture,(~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|~m2_relset_1(esk15_0,esk11_0,esk12_0)),inference(spm,[status(thm)],[102804,158,theory(equality)])).
% cnf(102806,negated_conjecture,(~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))|$false),inference(rw,[status(thm)],[102805,254,theory(equality)])).
% cnf(102807,negated_conjecture,(~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m1_subset_1(esk16_0,k1_zfmisc_1(k2_zfmisc_1(esk12_0,esk13_0)))),inference(cn,[status(thm)],[102806,theory(equality)])).
% cnf(102809,negated_conjecture,(~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|~m2_relset_1(esk16_0,esk12_0,esk13_0)),inference(spm,[status(thm)],[102807,78,theory(equality)])).
% cnf(102810,negated_conjecture,(~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))|$false),inference(rw,[status(thm)],[102809,253,theory(equality)])).
% cnf(102811,negated_conjecture,(~m1_subset_1(esk15_0,k1_zfmisc_1(k2_zfmisc_1(esk11_0,esk12_0)))),inference(cn,[status(thm)],[102810,theory(equality)])).
% cnf(102813,negated_conjecture,(~m2_relset_1(esk15_0,esk11_0,esk12_0)),inference(spm,[status(thm)],[102811,78,theory(equality)])).
% cnf(102814,negated_conjecture,($false),inference(rw,[status(thm)],[102813,254,theory(equality)])).
% cnf(102815,negated_conjecture,($false),inference(cn,[status(thm)],[102814,theory(equality)])).
% cnf(102816,negated_conjecture,($false),102815,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 6654
% # ...of these trivial : 5
% # ...subsumed : 4917
% # ...remaining for further processing: 1732
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 659
% # Backward-rewritten : 59
% # Generated clauses : 63873
% # ...of the previous two non-trivial : 61444
% # Contextual simplify-reflections : 5193
% # Paramodulations : 63864
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1011
% # Positive orientable unit clauses: 93
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 12
% # Non-unit-clauses : 906
% # Current number of unprocessed clauses: 48254
% # ...number of literals in the above : 352439
% # Clause-clause subsumption calls (NU) : 354871
% # Rec. Clause-clause subsumption calls : 105842
% # Unit Clause-clause subsumption calls : 2238
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 115
% # Indexed BW rewrite successes : 21
% # Backwards rewriting index: 825 leaves, 2.50+/-5.767 terms/leaf
% # Paramod-from index: 339 leaves, 1.63+/-2.348 terms/leaf
% # Paramod-into index: 734 leaves, 2.14+/-4.282 terms/leaf
% # -------------------------------------------------
% # User time : 4.410 s
% # System time : 0.118 s
% # Total time : 4.528 s
% # Maximum resident set size: 0 pages
% PrfWatch: 6.81 CPU 6.94 WC
% FINAL PrfWatch: 6.81 CPU 6.94 WC
% SZS output end Solution for /tmp/SystemOnTPTP9659/SEU447+1.tptp
%
%------------------------------------------------------------------------------