%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR045+2 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.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 : Tue Dec 28 23:21:17 EST 2010
% Result : Theorem 116.38s
% Output : Solution 116.38s
% 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/SystemOnTPTP20347/CSR045+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP20347/CSR045+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP20347/CSR045+2.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 20479
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.084 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 1.92 CPU 2.01 WC
% # SZS output start CNFRefutation.
% fof(5, axiom,applicationcontext(c_wamt_evalinitial_p14),file('/tmp/SRASS.s.p', ax1_83)).
% fof(12, axiom,![X7]:![X5]:(genls(X7,X5)=>collection(X7)),file('/tmp/SRASS.s.p', ax1_229)).
% fof(176, axiom,![X9]:(applicationcontext(X9)=>microtheory(X9)),file('/tmp/SRASS.s.p', ax1_171)).
% fof(178, axiom,![X9]:~((collection(X9)&individual(X9))),file('/tmp/SRASS.s.p', ax1_289)).
% fof(544, axiom,![X9]:(partiallyintangibleindividual(X9)=>individual(X9)),file('/tmp/SRASS.s.p', ax1_33)).
% fof(575, axiom,![X9]:(microtheory(X9)=>aspatialinformationstore(X9)),file('/tmp/SRASS.s.p', ax1_156)).
% fof(765, axiom,![X9]:(intangibleindividual(X9)=>partiallyintangibleindividual(X9)),file('/tmp/SRASS.s.p', ax1_320)).
% fof(767, axiom,![X9]:(aspatialinformationstore(X9)=>intangibleindividual(X9)),file('/tmp/SRASS.s.p', ax1_382)).
% fof(1132, conjecture,~(genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088)),file('/tmp/SRASS.s.p', query95)).
% fof(1133, negated_conjecture,~(~(genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088))),inference(assume_negation,[status(cth)],[1132])).
% fof(1137, negated_conjecture,genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),inference(fof_simplification,[status(thm)],[1133,theory(equality)])).
% cnf(1150,plain,(applicationcontext(c_wamt_evalinitial_p14)),inference(split_conjunct,[status(thm)],[5])).
% fof(1169, plain,![X7]:![X5]:(~(genls(X7,X5))|collection(X7)),inference(fof_nnf,[status(thm)],[12])).
% fof(1170, plain,![X8]:![X9]:(~(genls(X8,X9))|collection(X8)),inference(variable_rename,[status(thm)],[1169])).
% cnf(1171,plain,(collection(X1)|~genls(X1,X2)),inference(split_conjunct,[status(thm)],[1170])).
% fof(1375, plain,![X9]:(~(applicationcontext(X9))|microtheory(X9)),inference(fof_nnf,[status(thm)],[176])).
% fof(1376, plain,![X10]:(~(applicationcontext(X10))|microtheory(X10)),inference(variable_rename,[status(thm)],[1375])).
% cnf(1377,plain,(microtheory(X1)|~applicationcontext(X1)),inference(split_conjunct,[status(thm)],[1376])).
% fof(1381, plain,![X9]:(~(collection(X9))|~(individual(X9))),inference(fof_nnf,[status(thm)],[178])).
% fof(1382, plain,![X10]:(~(collection(X10))|~(individual(X10))),inference(variable_rename,[status(thm)],[1381])).
% cnf(1383,plain,(~individual(X1)|~collection(X1)),inference(split_conjunct,[status(thm)],[1382])).
% fof(2469, plain,![X9]:(~(partiallyintangibleindividual(X9))|individual(X9)),inference(fof_nnf,[status(thm)],[544])).
% fof(2470, plain,![X10]:(~(partiallyintangibleindividual(X10))|individual(X10)),inference(variable_rename,[status(thm)],[2469])).
% cnf(2471,plain,(individual(X1)|~partiallyintangibleindividual(X1)),inference(split_conjunct,[status(thm)],[2470])).
% fof(2554, plain,![X9]:(~(microtheory(X9))|aspatialinformationstore(X9)),inference(fof_nnf,[status(thm)],[575])).
% fof(2555, plain,![X10]:(~(microtheory(X10))|aspatialinformationstore(X10)),inference(variable_rename,[status(thm)],[2554])).
% cnf(2556,plain,(aspatialinformationstore(X1)|~microtheory(X1)),inference(split_conjunct,[status(thm)],[2555])).
% fof(3069, plain,![X9]:(~(intangibleindividual(X9))|partiallyintangibleindividual(X9)),inference(fof_nnf,[status(thm)],[765])).
% fof(3070, plain,![X10]:(~(intangibleindividual(X10))|partiallyintangibleindividual(X10)),inference(variable_rename,[status(thm)],[3069])).
% cnf(3071,plain,(partiallyintangibleindividual(X1)|~intangibleindividual(X1)),inference(split_conjunct,[status(thm)],[3070])).
% fof(3075, plain,![X9]:(~(aspatialinformationstore(X9))|intangibleindividual(X9)),inference(fof_nnf,[status(thm)],[767])).
% fof(3076, plain,![X10]:(~(aspatialinformationstore(X10))|intangibleindividual(X10)),inference(variable_rename,[status(thm)],[3075])).
% cnf(3077,plain,(intangibleindividual(X1)|~aspatialinformationstore(X1)),inference(split_conjunct,[status(thm)],[3076])).
% cnf(3865,negated_conjecture,(genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088)),inference(split_conjunct,[status(thm)],[1137])).
% cnf(4153,negated_conjecture,(collection(c_wamt_evalinitial_p14)),inference(spm,[status(thm)],[1171,3865,theory(equality)])).
% cnf(4181,plain,(microtheory(c_wamt_evalinitial_p14)),inference(spm,[status(thm)],[1377,1150,theory(equality)])).
% cnf(4367,plain,(partiallyintangibleindividual(X1)|~aspatialinformationstore(X1)),inference(spm,[status(thm)],[3071,3077,theory(equality)])).
% cnf(13072,plain,(individual(X1)|~aspatialinformationstore(X1)),inference(spm,[status(thm)],[2471,4367,theory(equality)])).
% cnf(34338,plain,(individual(X1)|~microtheory(X1)),inference(spm,[status(thm)],[13072,2556,theory(equality)])).
% cnf(34583,plain,(~collection(X1)|~microtheory(X1)),inference(spm,[status(thm)],[1383,34338,theory(equality)])).
% cnf(34654,plain,(~collection(c_wamt_evalinitial_p14)),inference(spm,[status(thm)],[34583,4181,theory(equality)])).
% cnf(34657,plain,($false),inference(rw,[status(thm)],[34654,4153,theory(equality)])).
% cnf(34658,plain,($false),inference(cn,[status(thm)],[34657,theory(equality)])).
% cnf(34659,plain,($false),34658,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 6461
% # ...of these trivial : 797
% # ...subsumed : 553
% # ...remaining for further processing: 5111
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 23689
% # ...of the previous two non-trivial : 15515
% # Contextual simplify-reflections : 0
% # Paramodulations : 23689
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 5111
% # Positive orientable unit clauses: 2645
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 645
% # Non-unit-clauses : 1821
% # Current number of unprocessed clauses: 10186
% # ...number of literals in the above : 20894
% # Clause-clause subsumption calls (NU) : 795553
% # Rec. Clause-clause subsumption calls : 771911
% # Unit Clause-clause subsumption calls : 282916
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 3
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 4764 leaves, 1.02+/-0.238 terms/leaf
% # Paramod-from index: 3229 leaves, 1.00+/-0.047 terms/leaf
% # Paramod-into index: 4535 leaves, 1.02+/-0.196 terms/leaf
% # -------------------------------------------------
% # User time : 1.730 s
% # System time : 0.044 s
% # Total time : 1.774 s
% # Maximum resident set size: 0 pages
% PrfWatch: 2.20 CPU 2.30 WC
% FINAL PrfWatch: 2.20 CPU 2.30 WC
% SZS output end Solution for /tmp/SystemOnTPTP20347/CSR045+2.tptp
%
%------------------------------------------------------------------------------