%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR020+1 : TPTP v5.0.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art02.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 22:45:58 EST 2010
% Result : Theorem 1.03s
% Output : Solution 1.03s
% 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/SystemOnTPTP9562/CSR020+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP9562/CSR020+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP9562/CSR020+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 9658
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.021 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(10, axiom,~(push=pull),file('/tmp/SRASS.s.p', push_not_pull)).
% fof(14, axiom,![X5]:![X1]:![X2]:(terminates(X5,X1,X2)<=>(((((((X5=push&X1=backwards)&~(happens(pull,X2)))|((X5=pull&X1=forwards)&~(happens(push,X2))))|((X5=pull&X1=forwards)&happens(push,X2)))|((X5=pull&X1=backwards)&happens(push,X2)))|((X5=push&X1=spinning)&~(happens(pull,X2))))|((X5=pull&X1=spinning)&~(happens(push,X2))))),file('/tmp/SRASS.s.p', terminates_all_defn)).
% fof(22, axiom,plus(n1,n1)=n2,file('/tmp/SRASS.s.p', plus1_1)).
% fof(26, axiom,![X5]:![X2]:(happens(X5,X2)<=>((((X5=push&X2=n0)|(X5=pull&X2=n1))|(X5=pull&X2=n2))|(X5=push&X2=n2))),file('/tmp/SRASS.s.p', happens_all_defn)).
% fof(28, axiom,![X3]:(less(X3,n2)<=>less_or_equal(X3,n1)),file('/tmp/SRASS.s.p', less2)).
% fof(31, axiom,![X3]:![X4]:(less(X3,X4)<=>(~(less(X4,X3))&~(X4=X3))),file('/tmp/SRASS.s.p', less_property)).
% fof(33, axiom,![X3]:(less(X3,n1)<=>less_or_equal(X3,n0)),file('/tmp/SRASS.s.p', less1)).
% fof(38, axiom,![X5]:![X2]:![X1]:((happens(X5,X2)&terminates(X5,X1,X2))=>~(holdsAt(X1,plus(X2,n1)))),file('/tmp/SRASS.s.p', happens_terminates_not_holds)).
% fof(39, axiom,![X3]:![X4]:(less_or_equal(X3,X4)<=>(less(X3,X4)|X3=X4)),file('/tmp/SRASS.s.p', less_or_equal)).
% fof(48, conjecture,~(holdsAt(spinning,n2)),file('/tmp/SRASS.s.p', not_spinning_2)).
% fof(49, negated_conjecture,~(~(holdsAt(spinning,n2))),inference(assume_negation,[status(cth)],[48])).
% fof(55, plain,![X5]:![X1]:![X2]:(terminates(X5,X1,X2)<=>(((((((X5=push&X1=backwards)&~(happens(pull,X2)))|((X5=pull&X1=forwards)&~(happens(push,X2))))|((X5=pull&X1=forwards)&happens(push,X2)))|((X5=pull&X1=backwards)&happens(push,X2)))|((X5=push&X1=spinning)&~(happens(pull,X2))))|((X5=pull&X1=spinning)&~(happens(push,X2))))),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% fof(63, plain,![X3]:![X4]:(less(X3,X4)<=>(~(less(X4,X3))&~(X4=X3))),inference(fof_simplification,[status(thm)],[31,theory(equality)])).
% fof(64, plain,![X5]:![X2]:![X1]:((happens(X5,X2)&terminates(X5,X1,X2))=>~(holdsAt(X1,plus(X2,n1)))),inference(fof_simplification,[status(thm)],[38,theory(equality)])).
% fof(65, negated_conjecture,holdsAt(spinning,n2),inference(fof_simplification,[status(thm)],[49,theory(equality)])).
% fof(67, plain,![X1]:![X5]:![X2]:(epred2_3(X2,X5,X1)<=>((((X5=push&X1=backwards)&~(happens(pull,X2)))|((X5=pull&X1=forwards)&~(happens(push,X2))))|((X5=pull&X1=forwards)&happens(push,X2)))),introduced(definition)).
% fof(68, plain,![X1]:![X5]:![X2]:(epred3_3(X2,X5,X1)<=>(((((((X5=push&X1=backwards)&~(happens(pull,X2)))|((X5=pull&X1=forwards)&~(happens(push,X2))))|((X5=pull&X1=forwards)&happens(push,X2)))|((X5=pull&X1=backwards)&happens(push,X2)))|((X5=push&X1=spinning)&~(happens(pull,X2))))|((X5=pull&X1=spinning)&~(happens(push,X2))))),introduced(definition)).
% fof(70, plain,![X5]:![X1]:![X2]:(terminates(X5,X1,X2)<=>epred3_3(X2,X5,X1)),inference(apply_def,[status(esa)],[55,68,theory(equality)])).
% fof(71, plain,![X1]:![X5]:![X2]:(epred3_3(X2,X5,X1)<=>(((epred2_3(X2,X5,X1)|((X5=pull&X1=backwards)&happens(push,X2)))|((X5=push&X1=spinning)&~(happens(pull,X2))))|((X5=pull&X1=spinning)&~(happens(push,X2))))),inference(apply_def,[status(esa)],[68,67,theory(equality)])).
% cnf(84,plain,(push!=pull),inference(split_conjunct,[status(thm)],[10])).
% fof(92, plain,![X5]:![X1]:![X2]:((~(terminates(X5,X1,X2))|epred3_3(X2,X5,X1))&(~(epred3_3(X2,X5,X1))|terminates(X5,X1,X2))),inference(fof_nnf,[status(thm)],[70])).
% fof(93, plain,![X6]:![X7]:![X8]:((~(terminates(X6,X7,X8))|epred3_3(X8,X6,X7))&(~(epred3_3(X8,X6,X7))|terminates(X6,X7,X8))),inference(variable_rename,[status(thm)],[92])).
% cnf(94,plain,(terminates(X1,X2,X3)|~epred3_3(X3,X1,X2)),inference(split_conjunct,[status(thm)],[93])).
% cnf(129,plain,(plus(n1,n1)=n2),inference(split_conjunct,[status(thm)],[22])).
% fof(134, plain,![X5]:![X2]:((~(happens(X5,X2))|((((X5=push&X2=n0)|(X5=pull&X2=n1))|(X5=pull&X2=n2))|(X5=push&X2=n2)))&(((((~(X5=push)|~(X2=n0))&(~(X5=pull)|~(X2=n1)))&(~(X5=pull)|~(X2=n2)))&(~(X5=push)|~(X2=n2)))|happens(X5,X2))),inference(fof_nnf,[status(thm)],[26])).
% fof(135, plain,![X6]:![X7]:((~(happens(X6,X7))|((((X6=push&X7=n0)|(X6=pull&X7=n1))|(X6=pull&X7=n2))|(X6=push&X7=n2)))&(((((~(X6=push)|~(X7=n0))&(~(X6=pull)|~(X7=n1)))&(~(X6=pull)|~(X7=n2)))&(~(X6=push)|~(X7=n2)))|happens(X6,X7))),inference(variable_rename,[status(thm)],[134])).
% fof(136, plain,![X6]:![X7]:(((((((X6=push|(X6=pull|(X6=pull|X6=push)))|~(happens(X6,X7)))&((X7=n2|(X6=pull|(X6=pull|X6=push)))|~(happens(X6,X7))))&(((X6=push|(X7=n2|(X6=pull|X6=push)))|~(happens(X6,X7)))&((X7=n2|(X7=n2|(X6=pull|X6=push)))|~(happens(X6,X7)))))&((((X6=push|(X6=pull|(X7=n1|X6=push)))|~(happens(X6,X7)))&((X7=n2|(X6=pull|(X7=n1|X6=push)))|~(happens(X6,X7))))&(((X6=push|(X7=n2|(X7=n1|X6=push)))|~(happens(X6,X7)))&((X7=n2|(X7=n2|(X7=n1|X6=push)))|~(happens(X6,X7))))))&(((((X6=push|(X6=pull|(X6=pull|X7=n0)))|~(happens(X6,X7)))&((X7=n2|(X6=pull|(X6=pull|X7=n0)))|~(happens(X6,X7))))&(((X6=push|(X7=n2|(X6=pull|X7=n0)))|~(happens(X6,X7)))&((X7=n2|(X7=n2|(X6=pull|X7=n0)))|~(happens(X6,X7)))))&((((X6=push|(X6=pull|(X7=n1|X7=n0)))|~(happens(X6,X7)))&((X7=n2|(X6=pull|(X7=n1|X7=n0)))|~(happens(X6,X7))))&(((X6=push|(X7=n2|(X7=n1|X7=n0)))|~(happens(X6,X7)))&((X7=n2|(X7=n2|(X7=n1|X7=n0)))|~(happens(X6,X7)))))))&(((((~(X6=push)|~(X7=n0))|happens(X6,X7))&((~(X6=pull)|~(X7=n1))|happens(X6,X7)))&((~(X6=pull)|~(X7=n2))|happens(X6,X7)))&((~(X6=push)|~(X7=n2))|happens(X6,X7)))),inference(distribute,[status(thm)],[135])).
% cnf(139,plain,(happens(X1,X2)|X2!=n1|X1!=pull),inference(split_conjunct,[status(thm)],[136])).
% cnf(145,plain,(X2=n0|X1=pull|X2=n2|X2=n2|~happens(X1,X2)),inference(split_conjunct,[status(thm)],[136])).
% fof(158, plain,![X3]:((~(less(X3,n2))|less_or_equal(X3,n1))&(~(less_or_equal(X3,n1))|less(X3,n2))),inference(fof_nnf,[status(thm)],[28])).
% fof(159, plain,![X4]:((~(less(X4,n2))|less_or_equal(X4,n1))&(~(less_or_equal(X4,n1))|less(X4,n2))),inference(variable_rename,[status(thm)],[158])).
% cnf(160,plain,(less(X1,n2)|~less_or_equal(X1,n1)),inference(split_conjunct,[status(thm)],[159])).
% fof(168, plain,![X3]:![X4]:((~(less(X3,X4))|(~(less(X4,X3))&~(X4=X3)))&((less(X4,X3)|X4=X3)|less(X3,X4))),inference(fof_nnf,[status(thm)],[63])).
% fof(169, plain,![X5]:![X6]:((~(less(X5,X6))|(~(less(X6,X5))&~(X6=X5)))&((less(X6,X5)|X6=X5)|less(X5,X6))),inference(variable_rename,[status(thm)],[168])).
% fof(170, plain,![X5]:![X6]:(((~(less(X6,X5))|~(less(X5,X6)))&(~(X6=X5)|~(less(X5,X6))))&((less(X6,X5)|X6=X5)|less(X5,X6))),inference(distribute,[status(thm)],[169])).
% cnf(172,plain,(~less(X1,X2)|X2!=X1),inference(split_conjunct,[status(thm)],[170])).
% fof(175, plain,![X3]:((~(less(X3,n1))|less_or_equal(X3,n0))&(~(less_or_equal(X3,n0))|less(X3,n1))),inference(fof_nnf,[status(thm)],[33])).
% fof(176, plain,![X4]:((~(less(X4,n1))|less_or_equal(X4,n0))&(~(less_or_equal(X4,n0))|less(X4,n1))),inference(variable_rename,[status(thm)],[175])).
% cnf(177,plain,(less(X1,n1)|~less_or_equal(X1,n0)),inference(split_conjunct,[status(thm)],[176])).
% fof(203, plain,![X5]:![X2]:![X1]:((~(happens(X5,X2))|~(terminates(X5,X1,X2)))|~(holdsAt(X1,plus(X2,n1)))),inference(fof_nnf,[status(thm)],[64])).
% fof(204, plain,![X6]:![X7]:![X8]:((~(happens(X6,X7))|~(terminates(X6,X8,X7)))|~(holdsAt(X8,plus(X7,n1)))),inference(variable_rename,[status(thm)],[203])).
% cnf(205,plain,(~holdsAt(X1,plus(X2,n1))|~terminates(X3,X1,X2)|~happens(X3,X2)),inference(split_conjunct,[status(thm)],[204])).
% fof(206, plain,![X3]:![X4]:((~(less_or_equal(X3,X4))|(less(X3,X4)|X3=X4))&((~(less(X3,X4))&~(X3=X4))|less_or_equal(X3,X4))),inference(fof_nnf,[status(thm)],[39])).
% fof(207, plain,![X5]:![X6]:((~(less_or_equal(X5,X6))|(less(X5,X6)|X5=X6))&((~(less(X5,X6))&~(X5=X6))|less_or_equal(X5,X6))),inference(variable_rename,[status(thm)],[206])).
% fof(208, plain,![X5]:![X6]:((~(less_or_equal(X5,X6))|(less(X5,X6)|X5=X6))&((~(less(X5,X6))|less_or_equal(X5,X6))&(~(X5=X6)|less_or_equal(X5,X6)))),inference(distribute,[status(thm)],[207])).
% cnf(209,plain,(less_or_equal(X1,X2)|X1!=X2),inference(split_conjunct,[status(thm)],[208])).
% cnf(241,negated_conjecture,(holdsAt(spinning,n2)),inference(split_conjunct,[status(thm)],[65])).
% fof(308, plain,![X1]:![X5]:![X2]:((~(epred3_3(X2,X5,X1))|(((epred2_3(X2,X5,X1)|((X5=pull&X1=backwards)&happens(push,X2)))|((X5=push&X1=spinning)&~(happens(pull,X2))))|((X5=pull&X1=spinning)&~(happens(push,X2)))))&((((~(epred2_3(X2,X5,X1))&((~(X5=pull)|~(X1=backwards))|~(happens(push,X2))))&((~(X5=push)|~(X1=spinning))|happens(pull,X2)))&((~(X5=pull)|~(X1=spinning))|happens(push,X2)))|epred3_3(X2,X5,X1))),inference(fof_nnf,[status(thm)],[71])).
% fof(309, plain,![X6]:![X7]:![X8]:((~(epred3_3(X8,X7,X6))|(((epred2_3(X8,X7,X6)|((X7=pull&X6=backwards)&happens(push,X8)))|((X7=push&X6=spinning)&~(happens(pull,X8))))|((X7=pull&X6=spinning)&~(happens(push,X8)))))&((((~(epred2_3(X8,X7,X6))&((~(X7=pull)|~(X6=backwards))|~(happens(push,X8))))&((~(X7=push)|~(X6=spinning))|happens(pull,X8)))&((~(X7=pull)|~(X6=spinning))|happens(push,X8)))|epred3_3(X8,X7,X6))),inference(variable_rename,[status(thm)],[308])).
% fof(310, plain,![X6]:![X7]:![X8]:(((((((((X7=pull|(X7=push|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(X7=push|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(X7=push|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((((X7=pull|(X6=spinning|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(X6=spinning|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(X6=spinning|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))))&((((X7=pull|(~(happens(pull,X8))|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(~(happens(pull,X8))|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(~(happens(pull,X8))|(X7=pull|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))))&((((((X7=pull|(X7=push|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(X7=push|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(X7=push|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((((X7=pull|(X6=spinning|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(X6=spinning|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(X6=spinning|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))))&((((X7=pull|(~(happens(pull,X8))|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(~(happens(pull,X8))|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(~(happens(pull,X8))|(X6=backwards|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))))&((((((X7=pull|(X7=push|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(X7=push|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(X7=push|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((((X7=pull|(X6=spinning|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(X6=spinning|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(X6=spinning|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))))&((((X7=pull|(~(happens(pull,X8))|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6)))&((X6=spinning|(~(happens(pull,X8))|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))&((~(happens(push,X8))|(~(happens(pull,X8))|(happens(push,X8)|epred2_3(X8,X7,X6))))|~(epred3_3(X8,X7,X6))))))&((((~(epred2_3(X8,X7,X6))|epred3_3(X8,X7,X6))&(((~(X7=pull)|~(X6=backwards))|~(happens(push,X8)))|epred3_3(X8,X7,X6)))&(((~(X7=push)|~(X6=spinning))|happens(pull,X8))|epred3_3(X8,X7,X6)))&(((~(X7=pull)|~(X6=spinning))|happens(push,X8))|epred3_3(X8,X7,X6)))),inference(distribute,[status(thm)],[309])).
% cnf(311,plain,(epred3_3(X1,X2,X3)|happens(push,X1)|X3!=spinning|X2!=pull),inference(split_conjunct,[status(thm)],[310])).
% cnf(342,plain,(less_or_equal(X1,X1)),inference(er,[status(thm)],[209,theory(equality)])).
% cnf(343,plain,(~less(X1,X1)),inference(er,[status(thm)],[172,theory(equality)])).
% cnf(365,plain,(happens(pull,X1)|n1!=X1),inference(er,[status(thm)],[139,theory(equality)])).
% cnf(410,plain,(epred3_3(X1,X2,spinning)|happens(push,X1)|pull!=X2),inference(er,[status(thm)],[311,theory(equality)])).
% cnf(423,plain,(~terminates(X1,X2,n1)|~happens(X1,n1)|~holdsAt(X2,n2)),inference(spm,[status(thm)],[205,129,theory(equality)])).
% cnf(504,plain,(less(n1,n2)),inference(spm,[status(thm)],[160,342,theory(equality)])).
% cnf(506,plain,(less(n0,n1)),inference(spm,[status(thm)],[177,342,theory(equality)])).
% cnf(630,plain,(happens(pull,n1)),inference(er,[status(thm)],[365,theory(equality)])).
% cnf(1209,plain,(epred3_3(X1,pull,spinning)|happens(push,X1)),inference(er,[status(thm)],[410,theory(equality)])).
% cnf(1230,plain,(~terminates(pull,X1,n1)|~holdsAt(X1,n2)),inference(spm,[status(thm)],[423,630,theory(equality)])).
% cnf(1231,plain,(terminates(pull,spinning,X1)|happens(push,X1)),inference(spm,[status(thm)],[94,1209,theory(equality)])).
% cnf(1252,negated_conjecture,(~terminates(pull,spinning,n1)),inference(spm,[status(thm)],[1230,241,theory(equality)])).
% cnf(1253,plain,(happens(push,n1)),inference(spm,[status(thm)],[1252,1231,theory(equality)])).
% cnf(1254,plain,(pull=push|n2=n1|n0=n1),inference(spm,[status(thm)],[145,1253,theory(equality)])).
% cnf(1261,plain,(n2=n1|n0=n1),inference(sr,[status(thm)],[1254,84,theory(equality)])).
% cnf(1282,plain,(less(n1,n1)|n2=n1),inference(spm,[status(thm)],[506,1261,theory(equality)])).
% cnf(1310,plain,(n2=n1),inference(sr,[status(thm)],[1282,343,theory(equality)])).
% cnf(1364,plain,(less(n1,n1)),inference(rw,[status(thm)],[504,1310,theory(equality)])).
% cnf(1365,plain,($false),inference(sr,[status(thm)],[1364,343,theory(equality)])).
% cnf(1366,plain,($false),1365,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 446
% # ...of these trivial : 2
% # ...subsumed : 113
% # ...remaining for further processing: 331
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 38
% # Backward-rewritten : 62
% # Generated clauses : 668
% # ...of the previous two non-trivial : 475
% # Contextual simplify-reflections : 68
% # Paramodulations : 641
% # Factorizations : 3
% # Equation resolutions : 24
% # Current number of processed clauses: 229
% # Positive orientable unit clauses: 85
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 40
% # Non-unit-clauses : 103
% # Current number of unprocessed clauses: 93
% # ...number of literals in the above : 311
% # Clause-clause subsumption calls (NU) : 729
% # Rec. Clause-clause subsumption calls : 672
% # Unit Clause-clause subsumption calls : 1218
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 48
% # Indexed BW rewrite successes : 38
% # Backwards rewriting index: 199 leaves, 1.22+/-0.801 terms/leaf
% # Paramod-from index: 101 leaves, 1.04+/-0.195 terms/leaf
% # Paramod-into index: 170 leaves, 1.12+/-0.450 terms/leaf
% # -------------------------------------------------
% # User time : 0.057 s
% # System time : 0.007 s
% # Total time : 0.064 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.16 CPU 0.25 WC
% FINAL PrfWatch: 0.16 CPU 0.25 WC
% SZS output end Solution for /tmp/SystemOnTPTP9562/CSR020+1.tptp
%
%------------------------------------------------------------------------------