FDP---0.9.16.SAT-Ass.s

%------------------------------------------------------------------------------
% File     : FDP---0.9.16
% Problem  : ANA006-2 : TPTP v5.0.0. Released v2.5.0.
% Transfm  : add_equality
% Format   : protein
% Command  : fdp-casc %s %d

% Computer : art07.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 : Sat Jan  8 20:10:58 EST 2011

% Result   : Satisfiable 0.49s
% Output   : Assurance 0.49s
% Verified : 
% SZS Type : None (Parsing solution fails)
% Syntax   : Number of formulae    : 0

% Comments : 
%------------------------------------------------------------------------------
%----NO SOLUTION OUTPUT BY SYSTEM
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 		o===================================o
% 		|      EQuality TRAnsFOrmation      |
% 		| bthomas@informatik.uni-koblenz.de |
% 		o===================================o
% 		          $Revision: 1.14 $
% reading /tmp/ANA006-2+eq_rstfp.tme
% result written to : /tmp/ANA006-2+eq_rstfp-eqt.tme
% FDPLL - A First-Order Davis-Putnam Theorem Prover
% Version 0.9.16 (26/06/2002)
% Proving /tmp/ANA006-2+eq_rstfp-eqt ...
% Done.
% Input File...............: /tmp/ANA006-2+eq_rstfp-eqt.tme
% System...................: Linux art07.cs.miami.edu 2.6.26.8-57.fc8 #1 SMP Thu Dec 18 19:19:45 EST 2008 i686 i686 i386 GNU/Linux
% Automatic mode...........: on
% Time limit...............: 300 seconds
% Current restart interval.: 157 seconds
% Restart with =-axioms....: 225 seconds
% Initial interpretation...: [+(_88760)]
% Clause set type..........: Non-Horn, with equality
% Equality transformation..: on
% Non-constant functions...: yes
% Term depth settings......: 3/2 (Init/Increment)
% unit_extend..............: on
% splitting type...........: exact
% Final tree statistics:
% Tree for clause set......: with equality transformation applied
% # Restarts...............: 0
% Term depth limit.........: 3
% # Splits.................: 0
% # Commits................: 0
% # Unit extension steps...: 35
% # Unit back subsumptions.: 0
% # Branches closed........: 0
% # Level cuts.............: 0
% Time.....................: 0.07 seconds.
% Result...................: SATISFIABLE with model:
%   +(minimum(minimum(_2423_88835, _2423_88835), minimum(_2423_88835, _2423_88835), _2423_88835))
%   +(minimum(add(_2425_88850, _2423_88851), add(_2425_88850, _2423_88851), add(_2423_88851, _2425_88850)))
%   +(minimum(minimum(_2423_88869, _2423_88869), minimum(_2423_88869, _2425_88873), minimum(_2423_88869, _2425_88873)))
%   +(minimum(minimum(_2423_88888, _2425_88889), minimum(_2423_88888, _2423_88888), minimum(_2423_88888, _2425_88889)))
%   +(minimum(minimum(_2423_88907, _2423_88907), minimum(_2423_88911, _2423_88907), minimum(_2423_88911, _2423_88907)))
%   +(minimum(minimum(_2423_88926, _2423_88927), minimum(_2423_88927, _2423_88927), minimum(_2423_88926, _2423_88927)))
%   +(tpos(minimum(_2423_88944, _2423_88944), _2423_88944))
%   +(tpos(add(_2425_88955, _2423_88956), add(_2423_88956, _2425_88955)))
%   +(less_or_equal(minimum(_2423_88970, _2425_88971), minimum(_2423_88970, _2423_88970)))
%   +(less_or_equal(minimum(_2423_88985, _2423_88986), minimum(_2423_88986, _2423_88986)))
%   +(minimum(minimum(_2423_89001, _2423_89001), _2423_89001, _2423_89001))
%   +(minimum(_2423_89010, minimum(_2423_89010, _2423_89010), _2423_89010))
%   +(n0(minimum(n0, n0)))
%   +(add(half(_2423_89033), half(_2423_89033), minimum(_2423_89033, _2423_89033)))
%   +(minimum(_2425_89047, minimum(_2423_89051, _2425_89047), minimum(_2423_89051, _2425_89047)))
%   +(minimum(minimum(_2423_89066, _2425_89067), _2425_89067, minimum(_2423_89066, _2425_89067)))
%   +(minimum(_2423_89079, minimum(_2423_89079, _2425_89083), minimum(_2423_89079, _2425_89083)))
%   +(minimum(minimum(_2423_89098, _2425_89099), _2423_89098, minimum(_2423_89098, _2425_89099)))
%   +(minimum(add(_2425_89114, _2423_89115), add(_2423_89115, _2425_89114), add(_2423_89115, _2425_89114)))
%   +(minimum(add(_2423_89133, _2425_89134), add(_2425_89134, _2423_89133), add(_2423_89133, _2425_89134)))
%   +(tpos(X_2439_89148, X_2439_89148))
%   +(less_or_equal(_2423_89156, minimum(_2423_89156, _2423_89156)))
%   +(tpos(_2423_89167, minimum(_2423_89167, _2423_89167)))
%   +(less_or_equal(minimum(_2423_89181, _2425_89182), _2425_89182))
%   +(less_or_equal(minimum(_2423_89193, _2425_89194), _2423_89193))
%   +(add(half(_2418_89205), half(_2418_89205), _2418_89205))
%   +(less_or_equal(add(_2423_89218, _2425_89219), add(_2425_89219, _2423_89218)))
%   +(add(_2425_89231, _2423_89232, add(_2423_89232, _2425_89231)))
%   +(minimum(X_2439_89244, X_2439_89244, X_2439_89244))
%   +(n0(n0))
%   +(minimum(_2423_89259, _2425_89260, minimum(_2423_89259, _2425_89260)))
%   +(half(_2418_89271, half(_2418_89271)))
%   +(add(_2423_89282, _2425_89283, add(_2423_89282, _2425_89283)))
%   +(absolute(_2418_89294, absolute(_2418_89294)))
%   +(less_or_equal(X_2439_89304, X_2439_89304))
%   +(_89308)
% 
%------------------------------------------------------------------------------