%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NLP204+1 : TPTP v5.0.0. Released v2.4.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 : Wed Dec 29 17:10:01 EST 2010
% Result : Theorem 1.07s
% Output : Solution 1.07s
% 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/SystemOnTPTP4939/NLP204+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP4939/NLP204+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP4939/NLP204+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 5035
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(17, axiom,![X1]:![X2]:![X3]:![X4]:(be(X1,X2,X3,X4)=>X3=X4),file('/tmp/SRASS.s.p', ax71)).
% fof(24, axiom,![X1]:![X2]:(man(X1,X2)=>male(X1,X2)),file('/tmp/SRASS.s.p', ax24)).
% fof(28, axiom,![X1]:![X2]:(wheel(X1,X2)=>device(X1,X2)),file('/tmp/SRASS.s.p', ax48)).
% fof(40, axiom,![X1]:![X2]:(device(X1,X2)=>instrumentality(X1,X2)),file('/tmp/SRASS.s.p', ax47)).
% fof(43, axiom,![X1]:![X2]:(unisex(X1,X2)=>~(male(X1,X2))),file('/tmp/SRASS.s.p', ax63)).
% fof(55, axiom,![X1]:![X2]:(object(X1,X2)=>unisex(X1,X2)),file('/tmp/SRASS.s.p', ax38)).
% fof(56, axiom,![X1]:![X2]:(artifact(X1,X2)=>object(X1,X2)),file('/tmp/SRASS.s.p', ax45)).
% fof(57, axiom,![X1]:![X2]:(instrumentality(X1,X2)=>artifact(X1,X2)),file('/tmp/SRASS.s.p', ax46)).
% fof(72, conjecture,~(?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:?[X10]:?[X11]:?[X12]:(((((((((((((((((((((((((((((((of(X1,X3,X2)&man(X1,X2))&jules_forename(X1,X3))&forename(X1,X3))&frontseat(X1,X4))&chevy(X1,X5))&white(X1,X5))&dirty(X1,X5))&old(X1,X5))&of(X1,X6,X7))&city(X1,X7))&hollywood_placename(X1,X6))&placename(X1,X6))&street(X1,X7))&lonely(X1,X7))&event(X1,X8))&agent(X1,X8,X5))&present(X1,X8))&barrel(X1,X8))&down(X1,X8,X7))&in(X1,X8,X7))&![X13]:(member(X1,X13,X9)=>?[X14]:?[X15]:((state(X1,X14)&be(X1,X14,X13,X15))&in(X1,X15,X4))))&two(X1,X9))&group(X1,X9))&![X16]:(member(X1,X16,X9)=>(fellow(X1,X16)&young(X1,X16))))&![X17]:(member(X1,X17,X10)=>![X18]:(member(X1,X18,X9)=>?[X19]:(((((event(X1,X19)&agent(X1,X19,X18))&patient(X1,X19,X17))&present(X1,X19))&nonreflexive(X1,X19))&wear(X1,X19)))))&group(X1,X10))&![X20]:(member(X1,X20,X10)=>((coat(X1,X20)&black(X1,X20))&cheap(X1,X20))))&wheel(X1,X12))&state(X1,X11))&be(X1,X11,X2,X12))&behind(X1,X12,X12)))),file('/tmp/SRASS.s.p', co1)).
% fof(73, negated_conjecture,~(~(?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:?[X10]:?[X11]:?[X12]:(((((((((((((((((((((((((((((((of(X1,X3,X2)&man(X1,X2))&jules_forename(X1,X3))&forename(X1,X3))&frontseat(X1,X4))&chevy(X1,X5))&white(X1,X5))&dirty(X1,X5))&old(X1,X5))&of(X1,X6,X7))&city(X1,X7))&hollywood_placename(X1,X6))&placename(X1,X6))&street(X1,X7))&lonely(X1,X7))&event(X1,X8))&agent(X1,X8,X5))&present(X1,X8))&barrel(X1,X8))&down(X1,X8,X7))&in(X1,X8,X7))&![X13]:(member(X1,X13,X9)=>?[X14]:?[X15]:((state(X1,X14)&be(X1,X14,X13,X15))&in(X1,X15,X4))))&two(X1,X9))&group(X1,X9))&![X16]:(member(X1,X16,X9)=>(fellow(X1,X16)&young(X1,X16))))&![X17]:(member(X1,X17,X10)=>![X18]:(member(X1,X18,X9)=>?[X19]:(((((event(X1,X19)&agent(X1,X19,X18))&patient(X1,X19,X17))&present(X1,X19))&nonreflexive(X1,X19))&wear(X1,X19)))))&group(X1,X10))&![X20]:(member(X1,X20,X10)=>((coat(X1,X20)&black(X1,X20))&cheap(X1,X20))))&wheel(X1,X12))&state(X1,X11))&be(X1,X11,X2,X12))&behind(X1,X12,X12))))),inference(assume_negation,[status(cth)],[72])).
% fof(76, plain,![X1]:![X2]:(unisex(X1,X2)=>~(male(X1,X2))),inference(fof_simplification,[status(thm)],[43,theory(equality)])).
% fof(142, plain,![X1]:![X2]:![X3]:![X4]:(~(be(X1,X2,X3,X4))|X3=X4),inference(fof_nnf,[status(thm)],[17])).
% fof(143, plain,![X5]:![X6]:![X7]:![X8]:(~(be(X5,X6,X7,X8))|X7=X8),inference(variable_rename,[status(thm)],[142])).
% cnf(144,plain,(X1=X2|~be(X3,X4,X1,X2)),inference(split_conjunct,[status(thm)],[143])).
% fof(163, plain,![X1]:![X2]:(~(man(X1,X2))|male(X1,X2)),inference(fof_nnf,[status(thm)],[24])).
% fof(164, plain,![X3]:![X4]:(~(man(X3,X4))|male(X3,X4)),inference(variable_rename,[status(thm)],[163])).
% cnf(165,plain,(male(X1,X2)|~man(X1,X2)),inference(split_conjunct,[status(thm)],[164])).
% fof(175, plain,![X1]:![X2]:(~(wheel(X1,X2))|device(X1,X2)),inference(fof_nnf,[status(thm)],[28])).
% fof(176, plain,![X3]:![X4]:(~(wheel(X3,X4))|device(X3,X4)),inference(variable_rename,[status(thm)],[175])).
% cnf(177,plain,(device(X1,X2)|~wheel(X1,X2)),inference(split_conjunct,[status(thm)],[176])).
% fof(211, plain,![X1]:![X2]:(~(device(X1,X2))|instrumentality(X1,X2)),inference(fof_nnf,[status(thm)],[40])).
% fof(212, plain,![X3]:![X4]:(~(device(X3,X4))|instrumentality(X3,X4)),inference(variable_rename,[status(thm)],[211])).
% cnf(213,plain,(instrumentality(X1,X2)|~device(X1,X2)),inference(split_conjunct,[status(thm)],[212])).
% fof(220, plain,![X1]:![X2]:(~(unisex(X1,X2))|~(male(X1,X2))),inference(fof_nnf,[status(thm)],[76])).
% fof(221, plain,![X3]:![X4]:(~(unisex(X3,X4))|~(male(X3,X4))),inference(variable_rename,[status(thm)],[220])).
% cnf(222,plain,(~male(X1,X2)|~unisex(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% fof(256, plain,![X1]:![X2]:(~(object(X1,X2))|unisex(X1,X2)),inference(fof_nnf,[status(thm)],[55])).
% fof(257, plain,![X3]:![X4]:(~(object(X3,X4))|unisex(X3,X4)),inference(variable_rename,[status(thm)],[256])).
% cnf(258,plain,(unisex(X1,X2)|~object(X1,X2)),inference(split_conjunct,[status(thm)],[257])).
% fof(259, plain,![X1]:![X2]:(~(artifact(X1,X2))|object(X1,X2)),inference(fof_nnf,[status(thm)],[56])).
% fof(260, plain,![X3]:![X4]:(~(artifact(X3,X4))|object(X3,X4)),inference(variable_rename,[status(thm)],[259])).
% cnf(261,plain,(object(X1,X2)|~artifact(X1,X2)),inference(split_conjunct,[status(thm)],[260])).
% fof(262, plain,![X1]:![X2]:(~(instrumentality(X1,X2))|artifact(X1,X2)),inference(fof_nnf,[status(thm)],[57])).
% fof(263, plain,![X3]:![X4]:(~(instrumentality(X3,X4))|artifact(X3,X4)),inference(variable_rename,[status(thm)],[262])).
% cnf(264,plain,(artifact(X1,X2)|~instrumentality(X1,X2)),inference(split_conjunct,[status(thm)],[263])).
% fof(307, negated_conjecture,?[X1]:(actual_world(X1)&?[X2]:?[X3]:?[X4]:?[X5]:?[X6]:?[X7]:?[X8]:?[X9]:?[X10]:?[X11]:?[X12]:(((((((((((((((((((((((((((((((of(X1,X3,X2)&man(X1,X2))&jules_forename(X1,X3))&forename(X1,X3))&frontseat(X1,X4))&chevy(X1,X5))&white(X1,X5))&dirty(X1,X5))&old(X1,X5))&of(X1,X6,X7))&city(X1,X7))&hollywood_placename(X1,X6))&placename(X1,X6))&street(X1,X7))&lonely(X1,X7))&event(X1,X8))&agent(X1,X8,X5))&present(X1,X8))&barrel(X1,X8))&down(X1,X8,X7))&in(X1,X8,X7))&![X13]:(~(member(X1,X13,X9))|?[X14]:?[X15]:((state(X1,X14)&be(X1,X14,X13,X15))&in(X1,X15,X4))))&two(X1,X9))&group(X1,X9))&![X16]:(~(member(X1,X16,X9))|(fellow(X1,X16)&young(X1,X16))))&![X17]:(~(member(X1,X17,X10))|![X18]:(~(member(X1,X18,X9))|?[X19]:(((((event(X1,X19)&agent(X1,X19,X18))&patient(X1,X19,X17))&present(X1,X19))&nonreflexive(X1,X19))&wear(X1,X19)))))&group(X1,X10))&![X20]:(~(member(X1,X20,X10))|((coat(X1,X20)&black(X1,X20))&cheap(X1,X20))))&wheel(X1,X12))&state(X1,X11))&be(X1,X11,X2,X12))&behind(X1,X12,X12))),inference(fof_nnf,[status(thm)],[73])).
% fof(308, negated_conjecture,?[X21]:(actual_world(X21)&?[X22]:?[X23]:?[X24]:?[X25]:?[X26]:?[X27]:?[X28]:?[X29]:?[X30]:?[X31]:?[X32]:(((((((((((((((((((((((((((((((of(X21,X23,X22)&man(X21,X22))&jules_forename(X21,X23))&forename(X21,X23))&frontseat(X21,X24))&chevy(X21,X25))&white(X21,X25))&dirty(X21,X25))&old(X21,X25))&of(X21,X26,X27))&city(X21,X27))&hollywood_placename(X21,X26))&placename(X21,X26))&street(X21,X27))&lonely(X21,X27))&event(X21,X28))&agent(X21,X28,X25))&present(X21,X28))&barrel(X21,X28))&down(X21,X28,X27))&in(X21,X28,X27))&![X33]:(~(member(X21,X33,X29))|?[X34]:?[X35]:((state(X21,X34)&be(X21,X34,X33,X35))&in(X21,X35,X24))))&two(X21,X29))&group(X21,X29))&![X36]:(~(member(X21,X36,X29))|(fellow(X21,X36)&young(X21,X36))))&![X37]:(~(member(X21,X37,X30))|![X38]:(~(member(X21,X38,X29))|?[X39]:(((((event(X21,X39)&agent(X21,X39,X38))&patient(X21,X39,X37))&present(X21,X39))&nonreflexive(X21,X39))&wear(X21,X39)))))&group(X21,X30))&![X40]:(~(member(X21,X40,X30))|((coat(X21,X40)&black(X21,X40))&cheap(X21,X40))))&wheel(X21,X32))&state(X21,X31))&be(X21,X31,X22,X32))&behind(X21,X32,X32))),inference(variable_rename,[status(thm)],[307])).
% fof(309, negated_conjecture,(actual_world(esk4_0)&(((((((((((((((((((((((((((((((of(esk4_0,esk6_0,esk5_0)&man(esk4_0,esk5_0))&jules_forename(esk4_0,esk6_0))&forename(esk4_0,esk6_0))&frontseat(esk4_0,esk7_0))&chevy(esk4_0,esk8_0))&white(esk4_0,esk8_0))&dirty(esk4_0,esk8_0))&old(esk4_0,esk8_0))&of(esk4_0,esk9_0,esk10_0))&city(esk4_0,esk10_0))&hollywood_placename(esk4_0,esk9_0))&placename(esk4_0,esk9_0))&street(esk4_0,esk10_0))&lonely(esk4_0,esk10_0))&event(esk4_0,esk11_0))&agent(esk4_0,esk11_0,esk8_0))&present(esk4_0,esk11_0))&barrel(esk4_0,esk11_0))&down(esk4_0,esk11_0,esk10_0))&in(esk4_0,esk11_0,esk10_0))&![X33]:(~(member(esk4_0,X33,esk12_0))|((state(esk4_0,esk16_1(X33))&be(esk4_0,esk16_1(X33),X33,esk17_1(X33)))&in(esk4_0,esk17_1(X33),esk7_0))))&two(esk4_0,esk12_0))&group(esk4_0,esk12_0))&![X36]:(~(member(esk4_0,X36,esk12_0))|(fellow(esk4_0,X36)&young(esk4_0,X36))))&![X37]:(~(member(esk4_0,X37,esk13_0))|![X38]:(~(member(esk4_0,X38,esk12_0))|(((((event(esk4_0,esk18_2(X37,X38))&agent(esk4_0,esk18_2(X37,X38),X38))&patient(esk4_0,esk18_2(X37,X38),X37))&present(esk4_0,esk18_2(X37,X38)))&nonreflexive(esk4_0,esk18_2(X37,X38)))&wear(esk4_0,esk18_2(X37,X38))))))&group(esk4_0,esk13_0))&![X40]:(~(member(esk4_0,X40,esk13_0))|((coat(esk4_0,X40)&black(esk4_0,X40))&cheap(esk4_0,X40))))&wheel(esk4_0,esk15_0))&state(esk4_0,esk14_0))&be(esk4_0,esk14_0,esk5_0,esk15_0))&behind(esk4_0,esk15_0,esk15_0))),inference(skolemize,[status(esa)],[308])).
% fof(310, negated_conjecture,![X33]:![X36]:![X37]:![X38]:![X40]:(((((((~(member(esk4_0,X40,esk13_0))|((coat(esk4_0,X40)&black(esk4_0,X40))&cheap(esk4_0,X40)))&((((~(member(esk4_0,X38,esk12_0))|(((((event(esk4_0,esk18_2(X37,X38))&agent(esk4_0,esk18_2(X37,X38),X38))&patient(esk4_0,esk18_2(X37,X38),X37))&present(esk4_0,esk18_2(X37,X38)))&nonreflexive(esk4_0,esk18_2(X37,X38)))&wear(esk4_0,esk18_2(X37,X38))))|~(member(esk4_0,X37,esk13_0)))&((~(member(esk4_0,X36,esk12_0))|(fellow(esk4_0,X36)&young(esk4_0,X36)))&((((~(member(esk4_0,X33,esk12_0))|((state(esk4_0,esk16_1(X33))&be(esk4_0,esk16_1(X33),X33,esk17_1(X33)))&in(esk4_0,esk17_1(X33),esk7_0)))&((((((((((((((((((((of(esk4_0,esk6_0,esk5_0)&man(esk4_0,esk5_0))&jules_forename(esk4_0,esk6_0))&forename(esk4_0,esk6_0))&frontseat(esk4_0,esk7_0))&chevy(esk4_0,esk8_0))&white(esk4_0,esk8_0))&dirty(esk4_0,esk8_0))&old(esk4_0,esk8_0))&of(esk4_0,esk9_0,esk10_0))&city(esk4_0,esk10_0))&hollywood_placename(esk4_0,esk9_0))&placename(esk4_0,esk9_0))&street(esk4_0,esk10_0))&lonely(esk4_0,esk10_0))&event(esk4_0,esk11_0))&agent(esk4_0,esk11_0,esk8_0))&present(esk4_0,esk11_0))&barrel(esk4_0,esk11_0))&down(esk4_0,esk11_0,esk10_0))&in(esk4_0,esk11_0,esk10_0)))&two(esk4_0,esk12_0))&group(esk4_0,esk12_0))))&group(esk4_0,esk13_0)))&wheel(esk4_0,esk15_0))&state(esk4_0,esk14_0))&be(esk4_0,esk14_0,esk5_0,esk15_0))&behind(esk4_0,esk15_0,esk15_0))&actual_world(esk4_0)),inference(shift_quantors,[status(thm)],[309])).
% fof(311, negated_conjecture,![X33]:![X36]:![X37]:![X38]:![X40]:(((((((((coat(esk4_0,X40)|~(member(esk4_0,X40,esk13_0)))&(black(esk4_0,X40)|~(member(esk4_0,X40,esk13_0))))&(cheap(esk4_0,X40)|~(member(esk4_0,X40,esk13_0))))&(((((((((event(esk4_0,esk18_2(X37,X38))|~(member(esk4_0,X38,esk12_0)))|~(member(esk4_0,X37,esk13_0)))&((agent(esk4_0,esk18_2(X37,X38),X38)|~(member(esk4_0,X38,esk12_0)))|~(member(esk4_0,X37,esk13_0))))&((patient(esk4_0,esk18_2(X37,X38),X37)|~(member(esk4_0,X38,esk12_0)))|~(member(esk4_0,X37,esk13_0))))&((present(esk4_0,esk18_2(X37,X38))|~(member(esk4_0,X38,esk12_0)))|~(member(esk4_0,X37,esk13_0))))&((nonreflexive(esk4_0,esk18_2(X37,X38))|~(member(esk4_0,X38,esk12_0)))|~(member(esk4_0,X37,esk13_0))))&((wear(esk4_0,esk18_2(X37,X38))|~(member(esk4_0,X38,esk12_0)))|~(member(esk4_0,X37,esk13_0))))&(((fellow(esk4_0,X36)|~(member(esk4_0,X36,esk12_0)))&(young(esk4_0,X36)|~(member(esk4_0,X36,esk12_0))))&((((((state(esk4_0,esk16_1(X33))|~(member(esk4_0,X33,esk12_0)))&(be(esk4_0,esk16_1(X33),X33,esk17_1(X33))|~(member(esk4_0,X33,esk12_0))))&(in(esk4_0,esk17_1(X33),esk7_0)|~(member(esk4_0,X33,esk12_0))))&((((((((((((((((((((of(esk4_0,esk6_0,esk5_0)&man(esk4_0,esk5_0))&jules_forename(esk4_0,esk6_0))&forename(esk4_0,esk6_0))&frontseat(esk4_0,esk7_0))&chevy(esk4_0,esk8_0))&white(esk4_0,esk8_0))&dirty(esk4_0,esk8_0))&old(esk4_0,esk8_0))&of(esk4_0,esk9_0,esk10_0))&city(esk4_0,esk10_0))&hollywood_placename(esk4_0,esk9_0))&placename(esk4_0,esk9_0))&street(esk4_0,esk10_0))&lonely(esk4_0,esk10_0))&event(esk4_0,esk11_0))&agent(esk4_0,esk11_0,esk8_0))&present(esk4_0,esk11_0))&barrel(esk4_0,esk11_0))&down(esk4_0,esk11_0,esk10_0))&in(esk4_0,esk11_0,esk10_0)))&two(esk4_0,esk12_0))&group(esk4_0,esk12_0))))&group(esk4_0,esk13_0)))&wheel(esk4_0,esk15_0))&state(esk4_0,esk14_0))&be(esk4_0,esk14_0,esk5_0,esk15_0))&behind(esk4_0,esk15_0,esk15_0))&actual_world(esk4_0)),inference(distribute,[status(thm)],[310])).
% cnf(314,negated_conjecture,(be(esk4_0,esk14_0,esk5_0,esk15_0)),inference(split_conjunct,[status(thm)],[311])).
% cnf(316,negated_conjecture,(wheel(esk4_0,esk15_0)),inference(split_conjunct,[status(thm)],[311])).
% cnf(339,negated_conjecture,(man(esk4_0,esk5_0)),inference(split_conjunct,[status(thm)],[311])).
% cnf(362,negated_conjecture,(esk5_0=esk15_0),inference(spm,[status(thm)],[144,314,theory(equality)])).
% cnf(370,plain,(~unisex(X1,X2)|~man(X1,X2)),inference(spm,[status(thm)],[222,165,theory(equality)])).
% cnf(376,plain,(instrumentality(X1,X2)|~wheel(X1,X2)),inference(spm,[status(thm)],[213,177,theory(equality)])).
% cnf(398,negated_conjecture,(man(esk4_0,esk15_0)),inference(rw,[status(thm)],[339,362,theory(equality)])).
% cnf(409,plain,(~man(X1,X2)|~object(X1,X2)),inference(spm,[status(thm)],[370,258,theory(equality)])).
% cnf(415,negated_conjecture,(~object(esk4_0,esk15_0)),inference(spm,[status(thm)],[409,398,theory(equality)])).
% cnf(434,negated_conjecture,(instrumentality(esk4_0,esk15_0)),inference(spm,[status(thm)],[376,316,theory(equality)])).
% cnf(435,negated_conjecture,(artifact(esk4_0,esk15_0)),inference(spm,[status(thm)],[264,434,theory(equality)])).
% cnf(437,negated_conjecture,(object(esk4_0,esk15_0)),inference(spm,[status(thm)],[261,435,theory(equality)])).
% cnf(438,negated_conjecture,($false),inference(sr,[status(thm)],[437,415,theory(equality)])).
% cnf(439,negated_conjecture,($false),438,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 163
% # ...of these trivial : 0
% # ...subsumed : 2
% # ...remaining for further processing: 161
% # Other redundant clauses eliminated : 1
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 3
% # Generated clauses : 70
% # ...of the previous two non-trivial : 67
% # Contextual simplify-reflections : 0
% # Paramodulations : 69
% # Factorizations : 0
% # Equation resolutions : 1
% # Current number of processed clauses: 157
% # Positive orientable unit clauses: 38
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 8
% # Non-unit-clauses : 111
% # Current number of unprocessed clauses: 22
% # ...number of literals in the above : 57
% # Clause-clause subsumption calls (NU) : 2719
% # Rec. Clause-clause subsumption calls : 2628
% # Unit Clause-clause subsumption calls : 79
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 153 leaves, 1.08+/-0.395 terms/leaf
% # Paramod-from index: 91 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 139 leaves, 1.01+/-0.119 terms/leaf
% # -------------------------------------------------
% # User time : 0.027 s
% # System time : 0.002 s
% # Total time : 0.029 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.12 CPU 0.21 WC
% FINAL PrfWatch: 0.12 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP4939/NLP204+1.tptp
%
%------------------------------------------------------------------------------