%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP020-1 : 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 22:02:32 EST 2011 % Result : Satisfiable 1.84s % Output : Assurance 1.84s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % WARNING: Unrecognized structure name in 'B of C' in module eclipse. % WARNING: Unrecognized structure name in 'A of C' in module eclipse. % WARNING: Unrecognized structure name in 'C of B' in module eclipse. % WARNING: Unrecognized structure name in 'C of A' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % WARNING: Unrecognized structure name in 'V of W' in module eclipse. % WARNING: Unrecognized structure name in 'U of W' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % WARNING: Unrecognized structure name in 'B of C' in module eclipse. % WARNING: Unrecognized structure name in 'A of C' in module eclipse. % WARNING: Unrecognized structure name in 'C of B' in module eclipse. % WARNING: Unrecognized structure name in 'C of A' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % WARNING: Unrecognized structure name in 'V of W' in module eclipse. % WARNING: Unrecognized structure name in 'U of W' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % o===================================o % | EQuality TRAnsFOrmation | % | bthomas@informatik.uni-koblenz.de | % o===================================o % $Revision: 1.14 $ % reading /tmp/NLP020-1+eq_rstfp.tme % WARNING: Unrecognized structure name in 'B of C' in module eclipse. % WARNING: Unrecognized structure name in 'A of C' in module eclipse. % WARNING: Unrecognized structure name in 'C of B' in module eclipse. % WARNING: Unrecognized structure name in 'C of A' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % WARNING: Unrecognized structure name in 'V of W' in module eclipse. % WARNING: Unrecognized structure name in 'U of W' in module eclipse. % WARNING: Unrecognized structure name in 'U of V' in module eclipse. % result written to : /tmp/NLP020-1+eq_rstfp-eqt.tme % WARNING: Unrecognized structure name in 'U_2513 of V_2527' in module eclipse. % WARNING: Unrecognized structure name in 'U_2506 of V_2507' in module eclipse. % WARNING: Unrecognized structure name in 'V_2529 of W_2530' in module eclipse. % WARNING: Unrecognized structure name in 'U_2529 of W_2530' in module eclipse. % WARNING: Unrecognized structure name in 'U_2531 of V_2532' in module eclipse. % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP020-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP020-1+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...: [+(_87680)] % Clause set type..........: 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.................: 0 % # Commits................: 0 % # Unit extension steps...: 280 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 1.41 seconds. % Result...................: SATISFIABLE with model: % -(tpos(skc6, skc8)) % -(tpos(skc10, skc8)) % -(tpos(skf1(U_2416_87769, V_2417_87770), skc8)) % -(tpos(skc8, skc6)) % -(tpos(skc8, skc10)) % -(tpos(skc8, skf1(_2423_87795, _2425_87796))) % -(skc6(skc8)) % -(fellow(skc8)) % -(woman(skc8)) % -(skc10(skc8)) % -(skf1(U_2416_87829, V_2417_87830, skc8)) % -(skc8(skc6)) % -(chevy(skc6)) % -(skc8(skc10)) % -(chevy(skc10)) % -(skc8(skf1(_2423_87864, _2425_87865))) % -(chevy(skf1(_2423_87875, _2425_87876))) % -(tpos(skc11, skc8)) % -(man(skc8)) % -(male(skc8)) % -(female(skc8)) % -(event(skc8)) % -(car(skc6)) % -(car(skc10)) % -(tpos(skc8, skc11)) % -(car(skf1(_2423_87936, _2425_87937))) % -(skc11(skc8)) % -(hollywood(skc8)) % -(human(skc8)) % -(eventuality(skc8)) % -(abstraction(skc8)) % -(tpos(skc9, skc6)) % -(seat(skc6)) % -(vehicle(skc6)) % -(tpos(skc11, skc6)) % -(tpos(skc10, skc6)) % -(tpos(skf1(U_2416_88011, V_2417_88012), skc6)) % -(tpos(skc6, skc9)) % -(tpos(skc10, skc9)) % -(tpos(skf1(U_2416_88037, V_2417_88038), skc9)) % -(tpos(skc6, skc10)) % -(tpos(skc9, skc10)) % -(seat(skc10)) % -(vehicle(skc10)) % -(tpos(skc11, skc10)) % -(skc8(skc11)) % -(chevy(skc11)) % -(tpos(skc6, skc11)) % -(tpos(skc10, skc11)) % -(tpos(skf1(U_2416_88108, V_2417_88109), skc11)) % -(tpos(skc6, skf1(_2423_88120, _2425_88121))) % -(tpos(skc9, skf1(_2423_88132, _2425_88133))) % -(seat(skf1(_2423_88143, _2425_88144))) % -(vehicle(skf1(_2423_88154, _2425_88155))) % -(tpos(skc11, skf1(_2423_88166, _2425_88167))) % -(tpos(skc9, skc8)) % -(city(skc8)) % -(organism(skc8)) % +(entity(skc8)) % -(skc9(skc6)) % -(street(skc6)) % -(furniture(skc6)) % -(transport(skc6)) % -(skc11(skc6)) % -(hollywood(skc6)) % -(skc10(skc6)) % -(skf1(U_2416_88243, V_2417_88244, skc6)) % -(tpos(skc10, skc7)) % -(tpos(skf1(U_2416_88262, V_2417_88263), skc7)) % -(tpos(skc11, skc7)) % -(tpos(skc8, skc9)) % -(skc6(skc9)) % -(fellow(skc9)) % -(woman(skc9)) % -(skc10(skc9)) % -(skf1(U_2416_88310, V_2417_88311, skc9)) % -(skc6(skc10)) % -(fellow(skc10)) % -(woman(skc10)) % -(skc9(skc10)) % -(street(skc10)) % -(furniture(skc10)) % -(transport(skc10)) % -(skc11(skc10)) % -(hollywood(skc10)) % -(tpos(skc7, skc10)) % -(tpos(skc7, skc11)) % -(car(skc11)) % -(skc6(skc11)) % -(fellow(skc11)) % -(woman(skc11)) % -(skc10(skc11)) % -(skf1(U_2416_88418, V_2417_88419, skc11)) % -(skc6(skf1(_2423_88429, _2425_88430))) % -(fellow(skf1(_2423_88440, _2425_88441))) % -(woman(skf1(_2423_88451, _2425_88452))) % -(skc9(skf1(_2423_88462, _2425_88463))) % -(street(skf1(_2423_88473, _2425_88474))) % -(furniture(skf1(_2423_88484, _2425_88485))) % -(transport(skf1(_2423_88495, _2425_88496))) % -(skc11(skf1(_2423_88506, _2425_88507))) % -(hollywood(skf1(_2423_88517, _2425_88518))) % -(tpos(skc7, skf1(_2423_88529, _2425_88530))) % -(tpos(skc7, skc8)) % -(skc9(skc8)) % -(street(skc8)) % -(location(skc8)) % +(object(skc8)) % -(tpos(skc7, skc6)) % -(way(skc6)) % -(instrumentality(skc6)) % -(city(skc6)) % -(event(skc6)) % -(tpos(skc6, skc7)) % -(skc10(skc7)) % -(skf1(U_2416_88614, V_2417_88615, skc7)) % -(tpos(skc8, skc7)) % -(skc11(skc7)) % -(hollywood(skc7)) % -(skc8(skc9)) % -(chevy(skc9)) % -(tpos(skc11, skc9)) % -(man(skc9)) % -(male(skc9)) % -(female(skc9)) % -(event(skc9)) % -(man(skc10)) % -(male(skc10)) % -(female(skc10)) % -(way(skc10)) % -(instrumentality(skc10)) % -(city(skc10)) % -(skc7(skc10)) % -(tpos(skc9, skc11)) % -(skc7(skc11)) % -(seat(skc11)) % -(vehicle(skc11)) % -(man(skc11)) % -(male(skc11)) % -(female(skc11)) % -(event(skc11)) % -(man(skf1(_2423_88778, _2425_88779))) % -(male(skf1(_2423_88789, _2425_88790))) % -(female(skf1(_2423_88800, _2425_88801))) % -(way(skf1(_2423_88811, _2425_88812))) % -(instrumentality(skf1(_2423_88822, _2425_88823))) % -(city(skf1(_2423_88833, _2425_88834))) % -(skc7(skf1(_2423_88844, _2425_88845))) % -(skc7(skc8)) % -(seat(skc8)) % -(way(skc8)) % +(artifact(skc8)) % -(skc7(skc6)) % -(artifact(skc6)) % -(location(skc6)) % -(eventuality(skc6)) % -(abstraction(skc6)) % -(skc6(skc7)) % -(fellow(skc7)) % -(woman(skc7)) % -(event(skc7)) % -(skc8(skc7)) % -(chevy(skc7)) % -(tpos(skc9, skc7)) % -(city(skc7)) % -(organism(skc7)) % -(tpos(skc7, skc9)) % -(car(skc9)) % -(skc11(skc9)) % -(hollywood(skc9)) % -(human(skc9)) % -(eventuality(skc9)) % -(abstraction(skc9)) % -(human(skc10)) % -(artifact(skc10)) % -(location(skc10)) % -(front(skc10)) % -(skc9(skc11)) % -(street(skc11)) % -(furniture(skc11)) % -(transport(skc11)) % -(human(skc11)) % -(eventuality(skc11)) % -(abstraction(skc11)) % -(human(skf1(_2423_89073, _2425_89074))) % -(artifact(skf1(_2423_89084, _2425_89085))) % -(location(skf1(_2423_89095, _2425_89096))) % -(front(skf1(_2423_89106, _2425_89107))) % -(furniture(skc8)) % +(instrumentality(skc8)) % -(front(skc6)) % -(object(skc6)) % +(entity(skc6)) % -(man(skc7)) % -(male(skc7)) % -(female(skc7)) % -(eventuality(skc7)) % -(abstraction(skc7)) % -(car(skc7)) % -(skc9(skc7)) % -(street(skc7)) % -(location(skc7)) % +(object(skc7)) % -(skc7(skc9)) % -(seat(skc9)) % -(vehicle(skc9)) % -(city(skc9)) % -(organism(skc9)) % +(entity(skc9)) % -(organism(skc10)) % -(object(skc10)) % -(nonhuman(skc10)) % -(way(skc11)) % -(instrumentality(skc11)) % -(organism(skc11)) % +(entity(skc11)) % -(organism(skf1(_2423_89285, _2425_89286))) % -(object(skf1(_2423_89296, _2425_89297))) % -(nonhuman(skf1(_2423_89307, _2425_89308))) % +(transport(skc8)) % -(nonhuman(skc6)) % +(organism(skc6)) % -(female(skc6)) % -(human(skc7)) % +(entity(skc7)) % -(vehicle(skc7)) % -(way(skc7)) % +(artifact(skc7)) % -(furniture(skc9)) % -(transport(skc9)) % -(location(skc9)) % +(object(skc9)) % -(entity(skc10)) % -(abstraction(skc10)) % -(artifact(skc11)) % +(object(skc11)) % -(entity(skf1(_2423_89420, _2425_89421))) % -(abstraction(skf1(_2423_89431, _2425_89432))) % -(new(skc8)) % +(vehicle(skc8)) % -(woman(skc6)) % +(human(skc6)) % +(male(skc6)) % +(nonhuman(skc7)) % -(transport(skc7)) % +(instrumentality(skc7)) % -(instrumentality(skc9)) % +(artifact(skc9)) % +(eventuality(skc10)) % +(location(skc11)) % +(eventuality(skf1(_2423_89514, _2425_89515))) % +(barrel(skc10, skc8)) % +(old(skc8)) % +(dirty(skc8)) % +(white(skc8)) % +(car(skc8)) % +(chevy(skc8)) % +(in(skc6, skc7)) % +(fellow(skc6)) % +(man(skc6)) % +(young(skc6)) % +(front(skc7)) % +(furniture(skc7)) % +(seat(skc7)) % +(down(skc10, skc9)) % +(street(skc9)) % +(way(skc9)) % +(lonely(skc9)) % +(in(skc10, skc11)) % +(event(skc10)) % +(hollywood(skc11)) % +(city(skc11)) % +(event(skf1(_2423_89655, _2425_89656))) % +(skc8(skc8)) % +(skc6(skc6)) % +(skc7(skc7)) % +(skc9(skc9)) % +(skc10(skc10)) % +(skc11(skc11)) % +(skf1(_2423_89701, _2425_89702, skf1(_2423_89701, _2425_89702))) % +(_89709) % %------------------------------------------------------------------------------