%------------------------------------------------------------------------------ % File : S-SETHEO---0.0 % Problem : PUZ019-1 : TPTP v5.1.0. Bugfixed v5.1.0. % Transfm : add_equality % Format : oldtptp % Command : scheme-setheo -norel -foldup -sgindex -indexfoldup -reg -mate -dynsgreord 0 %s % Computer : art01.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2800MHz % Memory : 2005MB % OS : Linux 2.6.32.26-175.fc12.i686.PAE % CPULimit : 300s % DateTime : Mon Jun 20 23:04:40 EDT 2011 % Result : Unsatisfiable 2.50s % Output : Assurance 2.50s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % /tmp/SystemOnTPTP4850/PUZ019-1.oldtptp: Trying to parse % Syntax: Number of clauses: 64 ( 4 non-Horn; 44 unit) % Number of literals: 105 ( 0 equality) % Maximal clause size: 8 % Number of predicates: 7 ( 0 propositional; 1-2 arity) % Number of functors: 12 ( 12 constant; 0-0 arity) % Number of variables: 40 ( 10 singleton) % all negated are conjectures % Lev. 1: inferences: succ match fail constr: 43 0 157 0 % Lev. 2: inferences: succ match fail constr: 212 10 1778 0 % Lev. 3: inferences: succ match fail constr: 1391 223 16641 43 % Lev. 4: inferences: succ match fail constr: 11226 1257 131165 1285 % Lev. 5: inferences: succ match fail constr: 176413 56388 1767503 56543 % Lev. 6: inferences: succ match fail constr: 579309 116601 5840590 99472 % ***** PROOF WITH 46 INFERENCES (8 RED.) (25 LEM.) FOUND ***** % Total successful/failed inferences: 768594 (RED: 117925) (LEM: 174479)/7757834 % %------------------------------------------------------------------------------