%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR022+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:46:08 EST 2010
% Result : Theorem 1.02s
% Output : Solution 1.02s
% 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/SystemOnTPTP9821/CSR022+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP9821/CSR022+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP9821/CSR022+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 9917
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.021 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(11, axiom,![X3]:![X4]:plus(X3,X4)=plus(X4,X3),file('/tmp/SRASS.s.p', symmetry_of_plus)).
% 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(25, 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(26, axiom,plus(n1,n2)=n3,file('/tmp/SRASS.s.p', plus1_2)).
% fof(39, 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(48, conjecture,~(holdsAt(forwards,n3)),file('/tmp/SRASS.s.p', not_forwards_3)).
% fof(49, negated_conjecture,~(~(holdsAt(forwards,n3))),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(64, plain,![X5]:![X2]:![X1]:((happens(X5,X2)&terminates(X5,X1,X2))=>~(holdsAt(X1,plus(X2,n1)))),inference(fof_simplification,[status(thm)],[39,theory(equality)])).
% fof(65, negated_conjecture,holdsAt(forwards,n3),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)])).
% fof(85, plain,![X5]:![X6]:plus(X5,X6)=plus(X6,X5),inference(variable_rename,[status(thm)],[11])).
% cnf(86,plain,(plus(X1,X2)=plus(X2,X1)),inference(split_conjunct,[status(thm)],[85])).
% 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])).
% fof(133, 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)],[25])).
% fof(134, 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)],[133])).
% fof(135, 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)],[134])).
% cnf(137,plain,(happens(X1,X2)|X2!=n2|X1!=pull),inference(split_conjunct,[status(thm)],[135])).
% cnf(156,plain,(plus(n1,n2)=n3),inference(split_conjunct,[status(thm)],[26])).
% fof(204, plain,![X5]:![X2]:![X1]:((~(happens(X5,X2))|~(terminates(X5,X1,X2)))|~(holdsAt(X1,plus(X2,n1)))),inference(fof_nnf,[status(thm)],[64])).
% fof(205, plain,![X6]:![X7]:![X8]:((~(happens(X6,X7))|~(terminates(X6,X8,X7)))|~(holdsAt(X8,plus(X7,n1)))),inference(variable_rename,[status(thm)],[204])).
% cnf(206,plain,(~holdsAt(X1,plus(X2,n1))|~terminates(X3,X1,X2)|~happens(X3,X2)),inference(split_conjunct,[status(thm)],[205])).
% cnf(241,negated_conjecture,(holdsAt(forwards,n3)),inference(split_conjunct,[status(thm)],[65])).
% fof(275, 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))))&(((((~(X5=push)|~(X1=backwards))|happens(pull,X2))&((~(X5=pull)|~(X1=forwards))|happens(push,X2)))&((~(X5=pull)|~(X1=forwards))|~(happens(push,X2))))|epred2_3(X2,X5,X1))),inference(fof_nnf,[status(thm)],[67])).
% fof(276, plain,![X6]:![X7]:![X8]:((~(epred2_3(X8,X7,X6))|((((X7=push&X6=backwards)&~(happens(pull,X8)))|((X7=pull&X6=forwards)&~(happens(push,X8))))|((X7=pull&X6=forwards)&happens(push,X8))))&(((((~(X7=push)|~(X6=backwards))|happens(pull,X8))&((~(X7=pull)|~(X6=forwards))|happens(push,X8)))&((~(X7=pull)|~(X6=forwards))|~(happens(push,X8))))|epred2_3(X8,X7,X6))),inference(variable_rename,[status(thm)],[275])).
% fof(277, plain,![X6]:![X7]:![X8]:(((((((((X7=pull|(X7=pull|X7=push))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(X7=pull|X7=push))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(X7=pull|X7=push))|~(epred2_3(X8,X7,X6))))&((((X7=pull|(X6=forwards|X7=push))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(X6=forwards|X7=push))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(X6=forwards|X7=push))|~(epred2_3(X8,X7,X6)))))&((((X7=pull|(~(happens(push,X8))|X7=push))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(~(happens(push,X8))|X7=push))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(~(happens(push,X8))|X7=push))|~(epred2_3(X8,X7,X6)))))&((((((X7=pull|(X7=pull|X6=backwards))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(X7=pull|X6=backwards))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(X7=pull|X6=backwards))|~(epred2_3(X8,X7,X6))))&((((X7=pull|(X6=forwards|X6=backwards))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(X6=forwards|X6=backwards))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(X6=forwards|X6=backwards))|~(epred2_3(X8,X7,X6)))))&((((X7=pull|(~(happens(push,X8))|X6=backwards))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(~(happens(push,X8))|X6=backwards))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(~(happens(push,X8))|X6=backwards))|~(epred2_3(X8,X7,X6))))))&((((((X7=pull|(X7=pull|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(X7=pull|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(X7=pull|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6))))&((((X7=pull|(X6=forwards|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(X6=forwards|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(X6=forwards|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6)))))&((((X7=pull|(~(happens(push,X8))|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6)))&((X6=forwards|(~(happens(push,X8))|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6))))&((happens(push,X8)|(~(happens(push,X8))|~(happens(pull,X8))))|~(epred2_3(X8,X7,X6))))))&(((((~(X7=push)|~(X6=backwards))|happens(pull,X8))|epred2_3(X8,X7,X6))&(((~(X7=pull)|~(X6=forwards))|happens(push,X8))|epred2_3(X8,X7,X6)))&(((~(X7=pull)|~(X6=forwards))|~(happens(push,X8)))|epred2_3(X8,X7,X6)))),inference(distribute,[status(thm)],[276])).
% cnf(278,plain,(epred2_3(X1,X2,X3)|~happens(push,X1)|X3!=forwards|X2!=pull),inference(split_conjunct,[status(thm)],[277])).
% cnf(279,plain,(epred2_3(X1,X2,X3)|happens(push,X1)|X3!=forwards|X2!=pull),inference(split_conjunct,[status(thm)],[277])).
% 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(314,plain,(epred3_3(X1,X2,X3)|~epred2_3(X1,X2,X3)),inference(split_conjunct,[status(thm)],[310])).
% cnf(365,plain,(happens(pull,X1)|n2!=X1),inference(er,[status(thm)],[137,theory(equality)])).
% cnf(411,plain,(epred2_3(X1,X2,X3)|forwards!=X3|pull!=X2),inference(csr,[status(thm)],[278,279])).
% cnf(412,plain,(epred2_3(X1,X2,forwards)|pull!=X2),inference(er,[status(thm)],[411,theory(equality)])).
% cnf(429,plain,(~terminates(X1,X2,X3)|~happens(X1,X3)|~holdsAt(X2,plus(n1,X3))),inference(spm,[status(thm)],[206,86,theory(equality)])).
% cnf(628,plain,(happens(pull,n2)),inference(er,[status(thm)],[365,theory(equality)])).
% cnf(1205,plain,(epred2_3(X1,pull,forwards)),inference(er,[status(thm)],[412,theory(equality)])).
% cnf(1206,plain,(epred3_3(X1,pull,forwards)),inference(spm,[status(thm)],[314,1205,theory(equality)])).
% cnf(1207,plain,(terminates(pull,forwards,X1)),inference(spm,[status(thm)],[94,1206,theory(equality)])).
% cnf(1316,plain,(~terminates(X1,X2,n2)|~happens(X1,n2)|~holdsAt(X2,n3)),inference(spm,[status(thm)],[429,156,theory(equality)])).
% cnf(1356,plain,(~terminates(pull,X1,n2)|~holdsAt(X1,n3)),inference(spm,[status(thm)],[1316,628,theory(equality)])).
% cnf(1359,negated_conjecture,(~terminates(pull,forwards,n2)),inference(spm,[status(thm)],[1356,241,theory(equality)])).
% cnf(1360,negated_conjecture,($false),inference(rw,[status(thm)],[1359,1207,theory(equality)])).
% cnf(1361,negated_conjecture,($false),inference(cn,[status(thm)],[1360,theory(equality)])).
% cnf(1362,negated_conjecture,($false),1361,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 469
% # ...of these trivial : 3
% # ...subsumed : 122
% # ...remaining for further processing: 344
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 42
% # Backward-rewritten : 2
% # Generated clauses : 696
% # ...of the previous two non-trivial : 475
% # Contextual simplify-reflections : 72
% # Paramodulations : 669
% # Factorizations : 3
% # Equation resolutions : 24
% # Current number of processed clauses: 298
% # Positive orientable unit clauses: 109
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 47
% # Non-unit-clauses : 141
% # Current number of unprocessed clauses: 95
% # ...number of literals in the above : 362
% # Clause-clause subsumption calls (NU) : 777
% # Rec. Clause-clause subsumption calls : 713
% # Unit Clause-clause subsumption calls : 1072
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 45
% # Indexed BW rewrite successes : 35
% # Backwards rewriting index: 261 leaves, 1.20+/-0.820 terms/leaf
% # Paramod-from index: 137 leaves, 1.03+/-0.168 terms/leaf
% # Paramod-into index: 229 leaves, 1.10+/-0.400 terms/leaf
% # -------------------------------------------------
% # User time : 0.059 s
% # System time : 0.006 s
% # Total time : 0.065 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.17 CPU 0.25 WC
% FINAL PrfWatch: 0.17 CPU 0.25 WC
% SZS output end Solution for /tmp/SystemOnTPTP9821/CSR022+1.tptp
%
%------------------------------------------------------------------------------