%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP017-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art09.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:01 EST 2011 % Result : Satisfiable 2.76s % Output : Assurance 2.76s % 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/NLP017-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/NLP017-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/NLP017-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP017-1+eq_rstfp-eqt.tme % System...................: Linux art09.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...: [+(_106096)] % 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...: 338 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 2.32 seconds. % Result...................: SATISFIABLE with model: % -(tpos(skc11, skc7)) % -(tpos(skc11, skc8)) % -(tpos(skc7, skc11)) % -(tpos(skc8, skc11)) % -(tpos(skc12, skc11)) % -(tpos(skf1(U_2416_106206, V_2417_106207), skc11)) % -(tpos(skc11, skc12)) % -(tpos(skc11, skf1(_2423_106225, _2425_106226))) % -(skc11(skc7)) % -(chevy(skc7)) % -(skc11(skc8)) % -(chevy(skc8)) % -(skc7(skc11)) % -(skc8(skc11)) % -(fellow(skc11)) % -(woman(skc11)) % -(skc12(skc11)) % -(skf1(U_2416_106289, V_2417_106290, skc11)) % -(skc11(skc12)) % -(chevy(skc12)) % -(skc11(skf1(_2423_106312, _2425_106313))) % -(chevy(skf1(_2423_106323, _2425_106324))) % -(car(skc7)) % -(car(skc8)) % -(tpos(skc13, skc11)) % -(man(skc11)) % -(male(skc11)) % -(female(skc11)) % -(event(skc11)) % -(car(skc12)) % -(tpos(skc11, skc13)) % -(car(skf1(_2423_106390, _2425_106391))) % -(tpos(skc7, skc10)) % -(tpos(skc8, skc10)) % -(tpos(skc12, skc10)) % -(tpos(skf1(U_2416_106423, V_2417_106424), skc10)) % -(tpos(skc10, skc7)) % -(seat(skc7)) % -(vehicle(skc7)) % -(tpos(skc13, skc7)) % -(tpos(skc12, skc7)) % -(tpos(skf1(U_2416_106468, V_2417_106469), skc7)) % -(tpos(skc10, skc8)) % -(seat(skc8)) % -(vehicle(skc8)) % -(tpos(skc13, skc8)) % -(tpos(skc12, skc8)) % -(tpos(skf1(U_2416_106513, V_2417_106514), skc8)) % -(skc13(skc11)) % -(hollywood(skc11)) % -(human(skc11)) % -(eventuality(skc11)) % -(abstraction(skc11)) % -(tpos(skc7, skc12)) % -(tpos(skc8, skc12)) % -(tpos(skc10, skc12)) % -(seat(skc12)) % -(vehicle(skc12)) % -(tpos(skc13, skc12)) % -(skc11(skc13)) % -(chevy(skc13)) % -(tpos(skc7, skc13)) % -(tpos(skc8, skc13)) % -(tpos(skc12, skc13)) % -(tpos(skf1(U_2416_106628, V_2417_106629), skc13)) % -(tpos(skc7, skf1(_2423_106640, _2425_106641))) % -(tpos(skc8, skf1(_2423_106652, _2425_106653))) % -(tpos(skc10, skf1(_2423_106664, _2425_106665))) % -(seat(skf1(_2423_106675, _2425_106676))) % -(vehicle(skf1(_2423_106686, _2425_106687))) % -(tpos(skc13, skf1(_2423_106698, _2425_106699))) % -(tpos(skc11, skc10)) % -(skc7(skc10)) % -(skc8(skc10)) % -(fellow(skc10)) % -(woman(skc10)) % -(skc12(skc10)) % -(skf1(U_2416_106745, V_2417_106746, skc10)) % -(skc10(skc7)) % -(street(skc7)) % -(furniture(skc7)) % -(transport(skc7)) % -(skc13(skc7)) % -(hollywood(skc7)) % -(skc12(skc7)) % -(skf1(U_2416_106797, V_2417_106798, skc7)) % -(skc10(skc8)) % -(street(skc8)) % -(furniture(skc8)) % -(transport(skc8)) % -(skc13(skc8)) % -(hollywood(skc8)) % -(skc12(skc8)) % -(skf1(U_2416_106849, V_2417_106850, skc8)) % -(tpos(skc12, skc9)) % -(tpos(skf1(U_2416_106868, V_2417_106869), skc9)) % -(tpos(skc13, skc9)) % -(tpos(skc10, skc11)) % -(city(skc11)) % -(organism(skc11)) % +(entity(skc11)) % -(skc7(skc12)) % -(skc8(skc12)) % -(fellow(skc12)) % -(woman(skc12)) % -(skc10(skc12)) % -(street(skc12)) % -(furniture(skc12)) % -(transport(skc12)) % -(skc13(skc12)) % -(hollywood(skc12)) % -(tpos(skc9, skc12)) % -(tpos(skc9, skc13)) % -(car(skc13)) % -(skc7(skc13)) % -(skc8(skc13)) % -(fellow(skc13)) % -(woman(skc13)) % -(skc12(skc13)) % -(skf1(U_2416_107020, V_2417_107021, skc13)) % -(skc7(skf1(_2423_107031, _2425_107032))) % -(skc8(skf1(_2423_107042, _2425_107043))) % -(fellow(skf1(_2423_107053, _2425_107054))) % -(woman(skf1(_2423_107064, _2425_107065))) % -(skc10(skf1(_2423_107075, _2425_107076))) % -(street(skf1(_2423_107086, _2425_107087))) % -(furniture(skf1(_2423_107097, _2425_107098))) % -(transport(skf1(_2423_107108, _2425_107109))) % -(skc13(skf1(_2423_107119, _2425_107120))) % -(hollywood(skf1(_2423_107130, _2425_107131))) % -(tpos(skc9, skf1(_2423_107142, _2425_107143))) % -(skc11(skc10)) % -(chevy(skc10)) % -(tpos(skc13, skc10)) % -(man(skc10)) % -(male(skc10)) % -(female(skc10)) % -(event(skc10)) % -(tpos(skc9, skc7)) % -(way(skc7)) % -(instrumentality(skc7)) % -(city(skc7)) % -(event(skc7)) % -(tpos(skc9, skc8)) % -(way(skc8)) % -(instrumentality(skc8)) % -(city(skc8)) % -(event(skc8)) % -(tpos(skc7, skc9)) % -(tpos(skc8, skc9)) % -(skc12(skc9)) % -(skf1(U_2416_107277, V_2417_107278, skc9)) % -(tpos(skc11, skc9)) % -(skc13(skc9)) % -(hollywood(skc9)) % -(tpos(skc9, skc11)) % -(skc10(skc11)) % -(street(skc11)) % -(location(skc11)) % +(object(skc11)) % -(man(skc12)) % -(male(skc12)) % -(female(skc12)) % -(way(skc12)) % -(instrumentality(skc12)) % -(city(skc12)) % -(skc9(skc12)) % -(tpos(skc10, skc13)) % -(skc9(skc13)) % -(seat(skc13)) % -(vehicle(skc13)) % -(man(skc13)) % -(male(skc13)) % -(female(skc13)) % -(event(skc13)) % -(man(skf1(_2423_107429, _2425_107430))) % -(male(skf1(_2423_107440, _2425_107441))) % -(female(skf1(_2423_107451, _2425_107452))) % -(way(skf1(_2423_107462, _2425_107463))) % -(instrumentality(skf1(_2423_107473, _2425_107474))) % -(city(skf1(_2423_107484, _2425_107485))) % -(skc9(skf1(_2423_107495, _2425_107496))) % -(tpos(skc9, skc10)) % -(car(skc10)) % -(skc13(skc10)) % -(hollywood(skc10)) % -(human(skc10)) % -(eventuality(skc10)) % -(abstraction(skc10)) % -(skc9(skc7)) % -(artifact(skc7)) % -(location(skc7)) % -(eventuality(skc7)) % -(abstraction(skc7)) % -(skc9(skc8)) % -(artifact(skc8)) % -(location(skc8)) % -(eventuality(skc8)) % -(abstraction(skc8)) % -(skc7(skc9)) % -(skc8(skc9)) % -(fellow(skc9)) % -(woman(skc9)) % -(event(skc9)) % -(skc11(skc9)) % -(chevy(skc9)) % -(tpos(skc10, skc9)) % -(city(skc9)) % -(organism(skc9)) % -(skc9(skc11)) % -(seat(skc11)) % -(way(skc11)) % +(artifact(skc11)) % -(human(skc12)) % -(artifact(skc12)) % -(location(skc12)) % -(front(skc12)) % -(skc10(skc13)) % -(street(skc13)) % -(furniture(skc13)) % -(transport(skc13)) % -(human(skc13)) % -(eventuality(skc13)) % -(abstraction(skc13)) % -(human(skf1(_2423_107760, _2425_107761))) % -(artifact(skf1(_2423_107771, _2425_107772))) % -(location(skf1(_2423_107782, _2425_107783))) % -(front(skf1(_2423_107793, _2425_107794))) % -(skc9(skc10)) % -(seat(skc10)) % -(vehicle(skc10)) % -(city(skc10)) % -(organism(skc10)) % +(entity(skc10)) % -(front(skc7)) % -(object(skc7)) % +(entity(skc7)) % -(front(skc8)) % -(object(skc8)) % +(entity(skc8)) % -(man(skc9)) % -(male(skc9)) % -(female(skc9)) % -(eventuality(skc9)) % -(abstraction(skc9)) % -(car(skc9)) % -(skc10(skc9)) % -(street(skc9)) % -(location(skc9)) % +(object(skc9)) % -(furniture(skc11)) % +(instrumentality(skc11)) % -(organism(skc12)) % -(object(skc12)) % -(nonhuman(skc12)) % -(way(skc13)) % -(instrumentality(skc13)) % -(organism(skc13)) % +(entity(skc13)) % -(organism(skf1(_2423_107990, _2425_107991))) % -(object(skf1(_2423_108001, _2425_108002))) % -(nonhuman(skf1(_2423_108012, _2425_108013))) % -(furniture(skc10)) % -(transport(skc10)) % -(location(skc10)) % +(object(skc10)) % -(nonhuman(skc7)) % +(organism(skc7)) % -(female(skc7)) % -(nonhuman(skc8)) % +(organism(skc8)) % -(female(skc8)) % -(human(skc9)) % +(entity(skc9)) % -(vehicle(skc9)) % -(way(skc9)) % +(artifact(skc9)) % +(transport(skc11)) % -(entity(skc12)) % -(abstraction(skc12)) % -(artifact(skc13)) % +(object(skc13)) % -(entity(skf1(_2423_108143, _2425_108144))) % -(abstraction(skf1(_2423_108154, _2425_108155))) % -(instrumentality(skc10)) % +(artifact(skc10)) % -(tpos(skc8, skc7)) % -(woman(skc7)) % +(human(skc7)) % +(male(skc7)) % -(tpos(skc7, skc8)) % -(woman(skc8)) % +(human(skc8)) % +(male(skc8)) % +(nonhuman(skc9)) % -(transport(skc9)) % +(instrumentality(skc9)) % -(new(skc11)) % +(vehicle(skc11)) % +(eventuality(skc12)) % +(location(skc13)) % +(eventuality(skf1(_2423_108269, _2425_108270))) % +(down(skc12, skc10)) % +(street(skc10)) % +(way(skc10)) % +(lonely(skc10)) % +(in(skc7, skc9)) % -(skc8(skc7)) % +(young(skc7)) % +(man(skc7)) % +(fellow(skc7)) % +(in(skc8, skc9)) % -(skc7(skc8)) % +(fellow(skc8)) % +(man(skc8)) % +(young(skc8)) % +(front(skc9)) % +(furniture(skc9)) % +(seat(skc9)) % +(barrel(skc12, skc11)) % +(old(skc11)) % +(dirty(skc11)) % +(white(skc11)) % +(car(skc11)) % +(chevy(skc11)) % +(in(skc12, skc13)) % +(event(skc12)) % +(city(skc13)) % +(hollywood(skc13)) % +(event(skf1(_2423_108447, _2425_108448))) % +(skc10(skc10)) % +(skc7(skc7)) % +(skc8(skc8)) % +(skc9(skc9)) % +(skc11(skc11)) % +(skc12(skc12)) % +(skc13(skc13)) % +(skf1(_2423_108499, _2425_108500, skf1(_2423_108499, _2425_108500))) % +(_108507) % %------------------------------------------------------------------------------