%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : KRS149+1 : TPTP v5.0.0. Released v3.1.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 : Wed Dec 29 08:37:52 EST 2010
% Result : Theorem 1.55s
% Output : Solution 1.55s
% 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/SystemOnTPTP11306/KRS149+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP11306/KRS149+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP11306/KRS149+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 11402
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.034 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(cowlThing(X1)&~(cowlNothing(X1))),file('/tmp/SRASS.s.p', axiom_0)).
% fof(2, axiom,![X1]:(xsd_string(X1)<=>~(xsd_integer(X1))),file('/tmp/SRASS.s.p', axiom_1)).
% fof(3, axiom,![X1]:(cC30(X1)<=>(cC14(X1)&cC28(X1))),file('/tmp/SRASS.s.p', axiom_70)).
% fof(4, axiom,![X1]:(cC46(X1)<=>(cC30(X1)&cC44(X1))),file('/tmp/SRASS.s.p', axiom_78)).
% fof(6, axiom,![X1]:(cC216(X1)<=>(~(cC214(X1))&cC64(X1))),file('/tmp/SRASS.s.p', axiom_65)).
% fof(7, axiom,![X1]:(cTEST(X1)<=>(cC216(X1)&cC46(X1))),file('/tmp/SRASS.s.p', axiom_107)).
% fof(9, axiom,cTEST(iV3102),file('/tmp/SRASS.s.p', axiom_108)).
% fof(126, conjecture,(((((((((![X1]:(cowlThing(X1)&~(cowlNothing(X1)))&![X1]:(xsd_string(X1)<=>~(xsd_integer(X1))))&cC216(iV3102))&cC46(iV3102))&cC30(iV3102))&cC44(iV3102))&cC28(iV3102))&cC64(iV3102))&cC14(iV3102))&cowlThing(iV3102)),file('/tmp/SRASS.s.p', the_axiom)).
% fof(127, negated_conjecture,~((((((((((![X1]:(cowlThing(X1)&~(cowlNothing(X1)))&![X1]:(xsd_string(X1)<=>~(xsd_integer(X1))))&cC216(iV3102))&cC46(iV3102))&cC30(iV3102))&cC44(iV3102))&cC28(iV3102))&cC64(iV3102))&cC14(iV3102))&cowlThing(iV3102))),inference(assume_negation,[status(cth)],[126])).
% fof(128, plain,![X1]:(cowlThing(X1)&~(cowlNothing(X1))),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% fof(129, plain,![X1]:(xsd_string(X1)<=>~(xsd_integer(X1))),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% fof(130, plain,![X1]:(cC216(X1)<=>(~(cC214(X1))&cC64(X1))),inference(fof_simplification,[status(thm)],[6,theory(equality)])).
% fof(194, negated_conjecture,~((((((((((![X1]:(cowlThing(X1)&~(cowlNothing(X1)))&![X1]:(xsd_string(X1)<=>~(xsd_integer(X1))))&cC216(iV3102))&cC46(iV3102))&cC30(iV3102))&cC44(iV3102))&cC28(iV3102))&cC64(iV3102))&cC14(iV3102))&cowlThing(iV3102))),inference(fof_simplification,[status(thm)],[127,theory(equality)])).
% fof(195, plain,![X2]:(cowlThing(X2)&~(cowlNothing(X2))),inference(variable_rename,[status(thm)],[128])).
% cnf(196,plain,(~cowlNothing(X1)),inference(split_conjunct,[status(thm)],[195])).
% cnf(197,plain,(cowlThing(X1)),inference(split_conjunct,[status(thm)],[195])).
% fof(198, plain,![X1]:((~(xsd_string(X1))|~(xsd_integer(X1)))&(xsd_integer(X1)|xsd_string(X1))),inference(fof_nnf,[status(thm)],[129])).
% fof(199, plain,![X2]:((~(xsd_string(X2))|~(xsd_integer(X2)))&(xsd_integer(X2)|xsd_string(X2))),inference(variable_rename,[status(thm)],[198])).
% cnf(200,plain,(xsd_string(X1)|xsd_integer(X1)),inference(split_conjunct,[status(thm)],[199])).
% cnf(201,plain,(~xsd_integer(X1)|~xsd_string(X1)),inference(split_conjunct,[status(thm)],[199])).
% fof(202, plain,![X1]:((~(cC30(X1))|(cC14(X1)&cC28(X1)))&((~(cC14(X1))|~(cC28(X1)))|cC30(X1))),inference(fof_nnf,[status(thm)],[3])).
% fof(203, plain,![X2]:((~(cC30(X2))|(cC14(X2)&cC28(X2)))&((~(cC14(X2))|~(cC28(X2)))|cC30(X2))),inference(variable_rename,[status(thm)],[202])).
% fof(204, plain,![X2]:(((cC14(X2)|~(cC30(X2)))&(cC28(X2)|~(cC30(X2))))&((~(cC14(X2))|~(cC28(X2)))|cC30(X2))),inference(distribute,[status(thm)],[203])).
% cnf(206,plain,(cC28(X1)|~cC30(X1)),inference(split_conjunct,[status(thm)],[204])).
% cnf(207,plain,(cC14(X1)|~cC30(X1)),inference(split_conjunct,[status(thm)],[204])).
% fof(208, plain,![X1]:((~(cC46(X1))|(cC30(X1)&cC44(X1)))&((~(cC30(X1))|~(cC44(X1)))|cC46(X1))),inference(fof_nnf,[status(thm)],[4])).
% fof(209, plain,![X2]:((~(cC46(X2))|(cC30(X2)&cC44(X2)))&((~(cC30(X2))|~(cC44(X2)))|cC46(X2))),inference(variable_rename,[status(thm)],[208])).
% fof(210, plain,![X2]:(((cC30(X2)|~(cC46(X2)))&(cC44(X2)|~(cC46(X2))))&((~(cC30(X2))|~(cC44(X2)))|cC46(X2))),inference(distribute,[status(thm)],[209])).
% cnf(212,plain,(cC44(X1)|~cC46(X1)),inference(split_conjunct,[status(thm)],[210])).
% cnf(213,plain,(cC30(X1)|~cC46(X1)),inference(split_conjunct,[status(thm)],[210])).
% fof(215, plain,![X1]:((~(cC216(X1))|(~(cC214(X1))&cC64(X1)))&((cC214(X1)|~(cC64(X1)))|cC216(X1))),inference(fof_nnf,[status(thm)],[130])).
% fof(216, plain,![X2]:((~(cC216(X2))|(~(cC214(X2))&cC64(X2)))&((cC214(X2)|~(cC64(X2)))|cC216(X2))),inference(variable_rename,[status(thm)],[215])).
% fof(217, plain,![X2]:(((~(cC214(X2))|~(cC216(X2)))&(cC64(X2)|~(cC216(X2))))&((cC214(X2)|~(cC64(X2)))|cC216(X2))),inference(distribute,[status(thm)],[216])).
% cnf(219,plain,(cC64(X1)|~cC216(X1)),inference(split_conjunct,[status(thm)],[217])).
% fof(221, plain,![X1]:((~(cTEST(X1))|(cC216(X1)&cC46(X1)))&((~(cC216(X1))|~(cC46(X1)))|cTEST(X1))),inference(fof_nnf,[status(thm)],[7])).
% fof(222, plain,![X2]:((~(cTEST(X2))|(cC216(X2)&cC46(X2)))&((~(cC216(X2))|~(cC46(X2)))|cTEST(X2))),inference(variable_rename,[status(thm)],[221])).
% fof(223, plain,![X2]:(((cC216(X2)|~(cTEST(X2)))&(cC46(X2)|~(cTEST(X2))))&((~(cC216(X2))|~(cC46(X2)))|cTEST(X2))),inference(distribute,[status(thm)],[222])).
% cnf(225,plain,(cC46(X1)|~cTEST(X1)),inference(split_conjunct,[status(thm)],[223])).
% cnf(226,plain,(cC216(X1)|~cTEST(X1)),inference(split_conjunct,[status(thm)],[223])).
% cnf(228,plain,(cTEST(iV3102)),inference(split_conjunct,[status(thm)],[9])).
% fof(973, negated_conjecture,(((((((((?[X1]:(~(cowlThing(X1))|cowlNothing(X1))|?[X1]:((~(xsd_string(X1))|xsd_integer(X1))&(xsd_string(X1)|~(xsd_integer(X1)))))|~(cC216(iV3102)))|~(cC46(iV3102)))|~(cC30(iV3102)))|~(cC44(iV3102)))|~(cC28(iV3102)))|~(cC64(iV3102)))|~(cC14(iV3102)))|~(cowlThing(iV3102))),inference(fof_nnf,[status(thm)],[194])).
% fof(974, negated_conjecture,(((((((((?[X2]:(~(cowlThing(X2))|cowlNothing(X2))|?[X3]:((~(xsd_string(X3))|xsd_integer(X3))&(xsd_string(X3)|~(xsd_integer(X3)))))|~(cC216(iV3102)))|~(cC46(iV3102)))|~(cC30(iV3102)))|~(cC44(iV3102)))|~(cC28(iV3102)))|~(cC64(iV3102)))|~(cC14(iV3102)))|~(cowlThing(iV3102))),inference(variable_rename,[status(thm)],[973])).
% fof(975, negated_conjecture,((((((((((~(cowlThing(esk55_0))|cowlNothing(esk55_0))|((~(xsd_string(esk56_0))|xsd_integer(esk56_0))&(xsd_string(esk56_0)|~(xsd_integer(esk56_0)))))|~(cC216(iV3102)))|~(cC46(iV3102)))|~(cC30(iV3102)))|~(cC44(iV3102)))|~(cC28(iV3102)))|~(cC64(iV3102)))|~(cC14(iV3102)))|~(cowlThing(iV3102))),inference(skolemize,[status(esa)],[974])).
% fof(976, negated_conjecture,(((((((((((~(xsd_string(esk56_0))|xsd_integer(esk56_0))|(~(cowlThing(esk55_0))|cowlNothing(esk55_0)))|~(cC216(iV3102)))|~(cC46(iV3102)))|~(cC30(iV3102)))|~(cC44(iV3102)))|~(cC28(iV3102)))|~(cC64(iV3102)))|~(cC14(iV3102)))|~(cowlThing(iV3102)))&((((((((((xsd_string(esk56_0)|~(xsd_integer(esk56_0)))|(~(cowlThing(esk55_0))|cowlNothing(esk55_0)))|~(cC216(iV3102)))|~(cC46(iV3102)))|~(cC30(iV3102)))|~(cC44(iV3102)))|~(cC28(iV3102)))|~(cC64(iV3102)))|~(cC14(iV3102)))|~(cowlThing(iV3102)))),inference(distribute,[status(thm)],[975])).
% cnf(977,negated_conjecture,(cowlNothing(esk55_0)|xsd_string(esk56_0)|~cowlThing(iV3102)|~cC14(iV3102)|~cC64(iV3102)|~cC28(iV3102)|~cC44(iV3102)|~cC30(iV3102)|~cC46(iV3102)|~cC216(iV3102)|~cowlThing(esk55_0)|~xsd_integer(esk56_0)),inference(split_conjunct,[status(thm)],[976])).
% cnf(978,negated_conjecture,(cowlNothing(esk55_0)|xsd_integer(esk56_0)|~cowlThing(iV3102)|~cC14(iV3102)|~cC64(iV3102)|~cC28(iV3102)|~cC44(iV3102)|~cC30(iV3102)|~cC46(iV3102)|~cC216(iV3102)|~cowlThing(esk55_0)|~xsd_string(esk56_0)),inference(split_conjunct,[status(thm)],[976])).
% cnf(980,negated_conjecture,(cowlNothing(esk55_0)|xsd_string(esk56_0)|$false|$false|~xsd_integer(esk56_0)|~cC30(iV3102)|~cC14(iV3102)|~cC28(iV3102)|~cC46(iV3102)|~cC44(iV3102)|~cC216(iV3102)|~cC64(iV3102)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[977,197,theory(equality)]),197,theory(equality)]),['unfolding']).
% cnf(981,negated_conjecture,(cowlNothing(esk55_0)|xsd_integer(esk56_0)|$false|$false|~xsd_string(esk56_0)|~cC30(iV3102)|~cC14(iV3102)|~cC28(iV3102)|~cC46(iV3102)|~cC44(iV3102)|~cC216(iV3102)|~cC64(iV3102)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[978,197,theory(equality)]),197,theory(equality)]),['unfolding']).
% cnf(982,negated_conjecture,(xsd_string(esk56_0)|~xsd_integer(esk56_0)|~cC30(iV3102)|~cC14(iV3102)|~cC28(iV3102)|~cC46(iV3102)|~cC44(iV3102)|~cC216(iV3102)|~cC64(iV3102)),inference(sr,[status(thm)],[980,196,theory(equality)])).
% cnf(983,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)|~cC44(iV3102)|~cC46(iV3102)|~cC28(iV3102)|~cC14(iV3102)|~cC30(iV3102)|~xsd_integer(esk56_0)),inference(csr,[status(thm)],[982,219])).
% cnf(984,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~cC28(iV3102)|~cC14(iV3102)|~cC30(iV3102)|~xsd_integer(esk56_0)),inference(csr,[status(thm)],[983,212])).
% cnf(985,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~cC14(iV3102)|~cC30(iV3102)|~xsd_integer(esk56_0)),inference(csr,[status(thm)],[984,206])).
% cnf(986,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~cC30(iV3102)|~xsd_integer(esk56_0)),inference(csr,[status(thm)],[985,207])).
% cnf(987,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~xsd_integer(esk56_0)),inference(csr,[status(thm)],[986,213])).
% cnf(988,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)|~cC46(iV3102)),inference(csr,[status(thm)],[987,200])).
% cnf(989,negated_conjecture,(xsd_integer(esk56_0)|~xsd_string(esk56_0)|~cC30(iV3102)|~cC14(iV3102)|~cC28(iV3102)|~cC46(iV3102)|~cC44(iV3102)|~cC216(iV3102)|~cC64(iV3102)),inference(sr,[status(thm)],[981,196,theory(equality)])).
% cnf(990,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)|~cC44(iV3102)|~cC46(iV3102)|~cC28(iV3102)|~cC14(iV3102)|~cC30(iV3102)|~xsd_string(esk56_0)),inference(csr,[status(thm)],[989,219])).
% cnf(991,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~cC28(iV3102)|~cC14(iV3102)|~cC30(iV3102)|~xsd_string(esk56_0)),inference(csr,[status(thm)],[990,212])).
% cnf(992,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~cC14(iV3102)|~cC30(iV3102)|~xsd_string(esk56_0)),inference(csr,[status(thm)],[991,206])).
% cnf(993,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~cC30(iV3102)|~xsd_string(esk56_0)),inference(csr,[status(thm)],[992,207])).
% cnf(994,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)|~cC46(iV3102)|~xsd_string(esk56_0)),inference(csr,[status(thm)],[993,213])).
% cnf(995,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)|~cC46(iV3102)),inference(csr,[status(thm)],[994,988])).
% cnf(998,plain,(cC46(iV3102)),inference(spm,[status(thm)],[225,228,theory(equality)])).
% cnf(1003,plain,(cC216(iV3102)),inference(spm,[status(thm)],[226,228,theory(equality)])).
% cnf(4023,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)|$false),inference(rw,[status(thm)],[995,998,theory(equality)])).
% cnf(4024,negated_conjecture,(xsd_integer(esk56_0)|~cC216(iV3102)),inference(cn,[status(thm)],[4023,theory(equality)])).
% cnf(4025,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)|$false),inference(rw,[status(thm)],[988,998,theory(equality)])).
% cnf(4026,negated_conjecture,(xsd_string(esk56_0)|~cC216(iV3102)),inference(cn,[status(thm)],[4025,theory(equality)])).
% cnf(4028,negated_conjecture,(xsd_integer(esk56_0)|$false),inference(rw,[status(thm)],[4024,1003,theory(equality)])).
% cnf(4029,negated_conjecture,(xsd_integer(esk56_0)),inference(cn,[status(thm)],[4028,theory(equality)])).
% cnf(4030,negated_conjecture,(~xsd_string(esk56_0)),inference(spm,[status(thm)],[201,4029,theory(equality)])).
% cnf(4031,negated_conjecture,(xsd_string(esk56_0)|$false),inference(rw,[status(thm)],[4026,1003,theory(equality)])).
% cnf(4032,negated_conjecture,(xsd_string(esk56_0)),inference(cn,[status(thm)],[4031,theory(equality)])).
% cnf(4034,negated_conjecture,($false),inference(rw,[status(thm)],[4030,4032,theory(equality)])).
% cnf(4035,negated_conjecture,($false),inference(cn,[status(thm)],[4034,theory(equality)])).
% cnf(4036,negated_conjecture,($false),4035,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 687
% # ...of these trivial : 0
% # ...subsumed : 0
% # ...remaining for further processing: 687
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 2
% # Generated clauses : 3026
% # ...of the previous two non-trivial : 2915
% # Contextual simplify-reflections : 12
% # Paramodulations : 3026
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 345
% # Positive orientable unit clauses: 10
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 10
% # Non-unit-clauses : 325
% # Current number of unprocessed clauses: 2905
% # ...number of literals in the above : 8669
% # Clause-clause subsumption calls (NU) : 39628
% # Rec. Clause-clause subsumption calls : 36240
% # Unit Clause-clause subsumption calls : 501
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 299 leaves, 1.14+/-0.344 terms/leaf
% # Paramod-from index: 159 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 283 leaves, 1.00+/-0.059 terms/leaf
% # -------------------------------------------------
% # User time : 0.135 s
% # System time : 0.005 s
% # Total time : 0.140 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.27 CPU 0.36 WC
% FINAL PrfWatch: 0.27 CPU 0.36 WC
% SZS output end Solution for /tmp/SystemOnTPTP11306/KRS149+1.tptp
%
%------------------------------------------------------------------------------