%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : MGT019-2 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % 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 : Sun Jan 9 21:42:02 EST 2011 % Result : Satisfiable 11.99s % Output : Assurance 11.99s % 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/MGT019-2+eq_rstfp.tme % result written to : /tmp/MGT019-2+eq_rstfp-eqt.tme % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/MGT019-2+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/MGT019-2+eq_rstfp-eqt.tme % System...................: Linux art02.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...: [+(_89608)] % 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.........: 5 % # Splits.................: 68 % # Commits................: 15 % # Unit extension steps...: 57 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 11.57 seconds. % Result...................: SATISFIABLE with model: % +(disbanding_rate(first_movers, sk5(sk3(sk4)), disbanding_rate(first_movers, sk5(sk3(sk4))))) % +(disbanding_rate(efficient_producers, sk5(sk3(sk4)), disbanding_rate(efficient_producers, sk5(sk3(sk4))))) % +(growth_rate(efficient_producers, sk5(sk3(sk4)), growth_rate(efficient_producers, sk5(sk3(sk4))))) % +(growth_rate(first_movers, sk5(sk3(sk4)), growth_rate(first_movers, sk5(sk3(sk4))))) % -(greater(disbanding_rate(first_movers, sk5(sk3(sk4))), disbanding_rate(efficient_producers, sk5(sk3(sk4))))) % +(greater_or_equal(founding_rate(efficient_producers, sk5(sk3(sk4))), founding_rate(first_movers, sk5(sk3(sk4))))) % -(greater(growth_rate(efficient_producers, sk5(sk3(sk4))), growth_rate(first_movers, sk5(sk3(sk4))))) % +(subpopulations(first_movers, efficient_producers, sk4, sk5(sk3(sk4)))) % +(greater_or_equal(sk5(sk3(sk4)), sk3(sk4))) % +(founding_rate(efficient_producers, A_2620_89845, founding_rate(efficient_producers, A_2620_89845))) % +(founding_rate(first_movers, A_2620_89857, founding_rate(first_movers, A_2620_89857))) % +(sk5(sk3(sk4), sk5(sk3(sk4)))) % +(disbanding_rate(first_movers, sk2, disbanding_rate(first_movers, sk2))) % +(sk5(growth_rate(first_movers, sk2), sk5(growth_rate(first_movers, sk2)))) % +(sk5(disbanding_rate(efficient_producers, sk2), sk5(disbanding_rate(efficient_producers, sk2)))) % +(sk5(founding_rate(first_movers, sk2), sk5(founding_rate(first_movers, sk2)))) % +(sk3(sk4, sk3(sk4))) % +(growth_rate(efficient_producers, sk2, growth_rate(efficient_producers, sk2))) % +(growth_rate(first_movers, sk2, growth_rate(first_movers, sk2))) % +(disbanding_rate(efficient_producers, sk2, disbanding_rate(efficient_producers, sk2))) % +(in_environment(sk4, sk3(sk4))) % +(stable(sk4)) % +(environment(sk4)) % -(greater(disbanding_rate(first_movers, sk2), disbanding_rate(efficient_producers, sk2))) % +(subpopulations(first_movers, efficient_producers, sk1, sk2)) % +(environment(sk1)) % +(sk4(sk4)) % +(sk2(sk2)) % +(efficient_producers(efficient_producers)) % +(first_movers(first_movers)) % +(sk1(sk1)) % +(sk5(_2418_90058, sk5(_2418_90058))) % +(sk3(_2418_90068, sk3(_2418_90068))) % +(growth_rate(_2423_90079, _2425_90080, growth_rate(_2423_90079, _2425_90080))) % +(founding_rate(_2423_90092, _2425_90093, founding_rate(_2423_90092, _2425_90093))) % +(disbanding_rate(_2423_90105, _2425_90106, disbanding_rate(_2423_90105, _2425_90106))) % +(_90113) % -(sk2(_2746_90137)) % -(tpos(sk2, FX_2400_90162)) % -(efficient_producers(_2744_90186)) % -(tpos(efficient_producers, FX_2400_90211)) % -(disbanding_rate(efficient_producers, sk2, _2495_90237)) % -(tpos(first_movers, efficient_producers)) % -(first_movers(efficient_producers)) % -(greater_or_equal(founding_rate(efficient_producers, sk2), founding_rate(first_movers, sk2))) % -(tpos(growth_rate(first_movers, sk2), disbanding_rate(efficient_producers, sk2))) % -(growth_rate(first_movers, sk2, disbanding_rate(efficient_producers, sk2))) % -(tpos(growth_rate(efficient_producers, sk2), disbanding_rate(first_movers, sk2))) % -(growth_rate(efficient_producers, sk2, disbanding_rate(first_movers, sk2))) % -(tpos(sk3(sk4), founding_rate(first_movers, sk2))) % -(sk3(sk4, founding_rate(first_movers, sk2))) % -(in_environment(sk4, founding_rate(first_movers, sk2))) % -(tpos(sk5(founding_rate(first_movers, sk2)), founding_rate(efficient_producers, sk2))) % -(sk5(founding_rate(first_movers, sk2), founding_rate(efficient_producers, sk2))) % -(tpos(sk5(sk3(sk4)), sk2)) % -(tpos(sk1, sk4)) % -(sk5(sk3(sk4), sk2)) % -(sk1(sk4)) % -(subpopulations(first_movers, efficient_producers, sk4, sk2)) % -(greater_or_equal(sk2, sk3(sk4))) % -(tpos(sk4, sk1)) % -(sk4(sk1)) % -(stable(sk1)) % -(tpos(disbanding_rate(efficient_producers, sk2), FX_2407_90622)) % -(greater_or_equal(disbanding_rate(first_movers, sk2), disbanding_rate(efficient_producers, sk2))) % -(tpos(sk3(sk4), disbanding_rate(efficient_producers, sk2))) % -(sk3(sk4, disbanding_rate(efficient_producers, sk2))) % -(in_environment(sk4, disbanding_rate(efficient_producers, sk2))) % -(tpos(sk5(disbanding_rate(efficient_producers, sk2)), disbanding_rate(first_movers, sk2))) % -(sk5(disbanding_rate(efficient_producers, sk2), disbanding_rate(first_movers, sk2))) % -(growth_rate(first_movers, sk2, X_2408_90772)) % -(growth_rate(efficient_producers, sk2, X_2408_90798)) % -(greater(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))) % -(tpos(growth_rate(first_movers, sk2), FX_2407_90856)) % -(greater_or_equal(growth_rate(efficient_producers, sk2), growth_rate(first_movers, sk2))) % -(tpos(sk3(sk4), growth_rate(first_movers, sk2))) % -(sk3(sk4, growth_rate(first_movers, sk2))) % -(in_environment(sk4, growth_rate(first_movers, sk2))) % -(tpos(sk5(growth_rate(first_movers, sk2)), growth_rate(efficient_producers, sk2))) % -(sk5(growth_rate(first_movers, sk2), growth_rate(efficient_producers, sk2))) % -(tpos(growth_rate(efficient_producers, sk2), FX_2407_91008)) % -(sk3(sk4, X_2405_91033)) % -(tpos(sk3(sk4), FX_2404_91060)) % -(tpos(X_2405_91085, sk2)) % -(sk5(founding_rate(first_movers, sk2), X_2405_91113)) % -(sk5(disbanding_rate(efficient_producers, sk2), X_2405_91141)) % -(sk5(growth_rate(first_movers, sk2), X_2405_91169)) % -(sk1(X_2401_91193)) % -(tpos(sk1, FX_2400_91218)) % -(first_movers(X_2401_91242)) % -(tpos(first_movers, FX_2400_91267)) % -(sk4(X_2400_91291)) % -(tpos(sk4, FX_2399_91316)) % -(disbanding_rate(first_movers, sk2, _2493_91342)) % -(tpos(disbanding_rate(first_movers, sk2), FX_2407_91370)) % -(in_environment(sk4, A_2454_91395)) % -(sk5(sk3(sk4), _2984_91422)) % -(stable(A_2680_91446)) % -(subpopulations(first_movers, efficient_producers, sk4, B_2670_91473)) % -(greater_or_equal(founding_rate(efficient_producers, A_2620_91501), founding_rate(first_movers, A_2620_91501))) % -(founding_rate(first_movers, A_2620_91530, _3284_91531)) % -(tpos(founding_rate(first_movers, _2414_91559), FX_2407_91560)) % -(founding_rate(efficient_producers, A_2620_91586, _3282_91587)) % -(tpos(founding_rate(efficient_producers, _2414_91615), FX_2407_91616)) % -(tpos(growth_rate(first_movers, sk5(sk3(sk4))), disbanding_rate(efficient_producers, sk2))) % -(growth_rate(first_movers, sk5(sk3(sk4)), disbanding_rate(efficient_producers, sk2))) % -(tpos(growth_rate(first_movers, sk5(sk3(sk4))), growth_rate(first_movers, sk2))) % -(growth_rate(first_movers, sk5(sk3(sk4)), growth_rate(first_movers, sk2))) % -(tpos(growth_rate(first_movers, sk5(sk3(sk4))), disbanding_rate(efficient_producers, sk5(sk3(sk4))))) % -(growth_rate(first_movers, sk5(sk3(sk4)), disbanding_rate(efficient_producers, sk5(sk3(sk4))))) % -(tpos(X_2408_91796, disbanding_rate(efficient_producers, sk2))) % -(tpos(X_2408_91824, growth_rate(first_movers, sk2))) % -(growth_rate(first_movers, sk5(sk3(sk4)), X_2408_91857)) % -(tpos(growth_rate(first_movers, sk5(sk3(sk4))), FX_2407_91889)) % -(greater_or_equal(growth_rate(efficient_producers, sk5(sk3(sk4))), growth_rate(first_movers, sk5(sk3(sk4))))) % -(tpos(sk5(founding_rate(first_movers, sk2)), FX_2404_91957)) % -(tpos(sk5(disbanding_rate(efficient_producers, sk2)), FX_2404_91987)) % -(tpos(sk5(growth_rate(first_movers, sk2)), FX_2404_92017)) % -(tpos(sk5(sk3(sk4)), FX_2404_92046)) % -(growth_rate(efficient_producers, sk5(sk3(sk4)), _2719_92076)) % -(tpos(growth_rate(efficient_producers, sk5(sk3(sk4))), FX_2407_92108)) % -(disbanding_rate(efficient_producers, sk5(sk3(sk4)), _2986_92138)) % -(tpos(disbanding_rate(efficient_producers, sk5(sk3(sk4))), FX_2407_92170)) % -(greater_or_equal(disbanding_rate(first_movers, sk5(sk3(sk4))), disbanding_rate(efficient_producers, sk5(sk3(sk4))))) % -(disbanding_rate(first_movers, sk5(sk3(sk4)), _2984_92238)) % -(tpos(disbanding_rate(first_movers, sk5(sk3(sk4))), FX_2407_92270)) % %------------------------------------------------------------------------------