%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP155-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art06.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:25:39 EST 2011 % Result : Satisfiable 48.16s % Output : Assurance 48.16s % 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/NLP155-1+eq_rstfp.tme % result written to : /tmp/NLP155-1+eq_rstfp-eqt.tme % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP155-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP155-1+eq_rstfp-eqt.tme % System...................: Linux art06.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...: [+(_72755)] % 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.................: 83 % # Commits................: 0 % # Unit extension steps...: 249 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 47.69 seconds. % Result...................: SATISFIABLE with model: % -(be(U_2501_72828, V_2502_72829, skc9, skc11)) % -(be(U_2479_72839, V_2480_72840, skc11, skc9)) % -(tpos(skc11, skc9)) % -(tpos(skc9, skc11)) % -(skc11(skc9)) % -(be(U_2501_72870, V_2502_72871, skc7, skc11)) % -(be(U_2479_72881, V_2480_72882, skc11, skc7)) % -(skc9(skc11)) % -(hollywood_placename(skc6, skc11)) % -(tpos(skc11, skc7)) % -(chevy(skc6, skc9)) % -(be(U_2501_72919, V_2502_72920, skc9, skc8)) % -(be(U_2479_72930, V_2480_72931, skc8, skc9)) % -(tpos(skc7, skc11)) % -(placename(skc6, skc11)) % -(two(skc6, skc11)) % -(skc11(skc7)) % -(tpos(skc8, skc9)) % -(frontseat(skc6, skc9)) % -(car(skc6, skc9)) % -(tpos(skc9, skc8)) % -(be(U_2501_72996, V_2502_72997, skc9, skc10)) % -(be(U_2479_73007, V_2480_73008, skc10, skc9)) % -(skc7(skc11)) % -(barrel(skc6, skc11)) % -(relname(skc6, skc11)) % -(group(skc6, skc11)) % -(chevy(skc6, skc7)) % -(tpos(skc10, skc9)) % -(skc8(skc9)) % -(seat(skc6, skc9)) % -(vehicle(skc6, skc9)) % -(be(U_2501_73079, V_2502_73080, skc7, skc8)) % -(be(U_2479_73090, V_2480_73091, skc8, skc7)) % -(skc9(skc8)) % -(hollywood_placename(skc6, skc8)) % -(tpos(skc9, skc10)) % -(event(skc6, skc11)) % -(state(skc6, skc11)) % -(relation(skc6, skc11)) % -(set(skc6, skc11)) % -(tpos(skc8, skc7)) % -(frontseat(skc6, skc7)) % -(car(skc6, skc7)) % -(be(U_2501_73170, V_2502_73171, skc7, skc9)) % -(be(U_2479_73181, V_2480_73182, skc9, skc7)) % -(skc10(skc9)) % -(street(skc6, skc9)) % -(furniture(skc6, skc9)) % -(transport(skc6, skc9)) % -(tpos(skc7, skc8)) % -(placename(skc6, skc8)) % -(two(skc6, skc8)) % -(be(U_2501_73240, V_2502_73241, skc7, skc10)) % -(be(U_2479_73251, V_2480_73252, skc10, skc7)) % -(skc9(skc10)) % -(hollywood_placename(skc6, skc10)) % -(fellow(skc6, skc11)) % -(eventuality(skc6, skc11)) % -(abstraction(skc6, skc11)) % -(multiple(skc6, skc11)) % -(tpos(skc10, skc7)) % -(skc8(skc7)) % -(seat(skc6, skc7)) % -(vehicle(skc6, skc7)) % -(tpos(skc9, skc7)) % -(tpos(skc7, skc9)) % -(city(skc6, skc9)) % -(way(skc6, skc9)) % -(instrumentality(skc6, skc9)) % -(two(skc6, skc9)) % -(skc7(skc8)) % -(barrel(skc6, skc8)) % -(relname(skc6, skc8)) % -(group(skc6, skc8)) % -(tpos(skc7, skc10)) % -(placename(skc6, skc10)) % -(two(skc6, skc10)) % -(man(skc6, skc11)) % -(human_person(skc6, skc11)) % -(organism(skc6, skc11)) % -(nonexistent(skc6, skc11)) % -(general(skc6, skc11)) % +(singleton(skc6, skc11)) % -(skc10(skc7)) % -(street(skc6, skc7)) % -(furniture(skc6, skc7)) % -(transport(skc6, skc7)) % -(skc9(skc7)) % -(hollywood_placename(skc6, skc7)) % -(skc7(skc9)) % -(barrel(skc6, skc9)) % -(location(skc6, skc9)) % -(artifact(skc6, skc9)) % -(group(skc6, skc9)) % -(event(skc6, skc8)) % -(state(skc6, skc8)) % -(relation(skc6, skc8)) % -(set(skc6, skc8)) % -(skc7(skc10)) % -(barrel(skc6, skc10)) % -(relname(skc6, skc10)) % -(group(skc6, skc10)) % -(male(skc6, skc11)) % -(animate(skc6, skc11)) % -(living(skc6, skc11)) % +(existent(skc6, skc11)) % +(specific(skc6, skc11)) % +(thing(skc6, skc11)) % -(city(skc6, skc7)) % -(way(skc6, skc7)) % -(instrumentality(skc6, skc7)) % -(placename(skc6, skc7)) % -(two(skc6, skc7)) % -(fellow(skc6, skc9)) % -(event(skc6, skc9)) % -(state(skc6, skc9)) % -(object(skc6, skc9)) % -(organism(skc6, skc9)) % -(set(skc6, skc9)) % -(fellow(skc6, skc8)) % -(eventuality(skc6, skc8)) % -(abstraction(skc6, skc8)) % -(multiple(skc6, skc8)) % -(event(skc6, skc10)) % -(state(skc6, skc10)) % -(relation(skc6, skc10)) % -(set(skc6, skc10)) % +(unisex(skc6, skc11)) % +(impartial(skc6, skc11)) % +(nonliving(skc6, skc11)) % +(entity(skc6, skc11)) % -(location(skc6, skc7)) % -(artifact(skc6, skc7)) % -(human_person(skc6, skc7)) % -(relname(skc6, skc7)) % -(group(skc6, skc7)) % -(man(skc6, skc9)) % -(eventuality(skc6, skc9)) % -(entity(skc6, skc9)) % -(human_person(skc6, skc9)) % -(multiple(skc6, skc9)) % -(man(skc6, skc8)) % -(human_person(skc6, skc8)) % -(organism(skc6, skc8)) % -(nonexistent(skc6, skc8)) % -(general(skc6, skc8)) % +(singleton(skc6, skc8)) % -(fellow(skc6, skc10)) % -(eventuality(skc6, skc10)) % -(abstraction(skc6, skc10)) % -(multiple(skc6, skc10)) % +(object(skc6, skc11)) % -(fellow(skc6, skc7)) % -(object(skc6, skc7)) % -(organism(skc6, skc7)) % -(relation(skc6, skc7)) % -(set(skc6, skc7)) % -(male(skc6, skc9)) % -(specific(skc6, skc9)) % -(human(skc6, skc9)) % +(singleton(skc6, skc9)) % -(male(skc6, skc8)) % -(animate(skc6, skc8)) % -(living(skc6, skc8)) % +(existent(skc6, skc8)) % +(specific(skc6, skc8)) % +(thing(skc6, skc8)) % -(man(skc6, skc10)) % -(human_person(skc6, skc10)) % -(organism(skc6, skc10)) % -(nonexistent(skc6, skc10)) % -(general(skc6, skc10)) % +(singleton(skc6, skc10)) % +(artifact(skc6, skc11)) % -(man(skc6, skc7)) % -(entity(skc6, skc7)) % -(abstraction(skc6, skc7)) % -(multiple(skc6, skc7)) % +(unisex(skc6, skc9)) % +(general(skc6, skc9)) % +(nonhuman(skc6, skc9)) % +(thing(skc6, skc9)) % +(unisex(skc6, skc8)) % +(impartial(skc6, skc8)) % +(nonliving(skc6, skc8)) % +(entity(skc6, skc8)) % -(male(skc6, skc10)) % -(animate(skc6, skc10)) % -(living(skc6, skc10)) % +(tpos(skc9, skc9)) % +(existent(skc6, skc10)) % +(specific(skc6, skc10)) % +(thing(skc6, skc10)) % +(instrumentality(skc6, skc11)) % -(male(skc6, skc7)) % -(existent(skc6, skc7)) % -(general(skc6, skc7)) % +(singleton(skc6, skc7)) % +(abstraction(skc6, skc9)) % +(object(skc6, skc8)) % +(unisex(skc6, skc10)) % +(impartial(skc6, skc10)) % +(nonliving(skc6, skc10)) % +(entity(skc6, skc10)) % +(transport(skc6, skc11)) % +(unisex(skc6, skc7)) % +(nonexistent(skc6, skc7)) % +(specific(skc6, skc7)) % +(thing(skc6, skc7)) % +(relation(skc6, skc9)) % +(artifact(skc6, skc8)) % +(object(skc6, skc10)) % +(vehicle(skc6, skc11)) % +(eventuality(skc6, skc7)) % +(relname(skc6, skc9)) % +(way(skc6, skc8)) % +(location(skc6, skc10)) % -(young(skc6, skc11)) % +(car(skc6, skc11)) % +(agent(skc6, skc7, skc11)) % +(down(skc6, skc7, skc8)) % +(in(skc6, skc7, skc10)) % +(barrel(skc6, skc7)) % +(present(skc6, skc7)) % +(event(skc6, skc7)) % +(of(skc6, skc9, skc10)) % +(hollywood_placename(skc6, skc9)) % +(placename(skc6, skc9)) % +(street(skc6, skc8)) % +(lonely(skc6, skc8)) % +(city(skc6, skc10)) % +(old(skc6, skc11)) % +(dirty(skc6, skc11)) % +(white(skc6, skc11)) % +(chevy(skc6, skc11)) % +(actual_world(skc6)) % -(member(U_2442_74531, V_2443_74532, V_2443_74532)) % +(skc7(skc7)) % +(skc9(skc9)) % +(skc8(skc8)) % +(skc10(skc10)) % +(skc11(skc11)) % +(skc6(skc6)) % +(skf8(_2423_74577, _2425_74578, skf8(_2423_74577, _2425_74578))) % +(skf5(_2423_74590, _2425_74591, skf5(_2423_74590, _2425_74591))) % +(skf13(_2433_74605, _2435_74606, _2437_74607, _2439_74608, skf13(_2433_74605, _2435_74606, _2437_74607, _2439_74608))) % +(skf12(_2423_74622, _2425_74623, skf12(_2423_74622, _2425_74623))) % +(skf10(_2423_74635, _2425_74636, skf10(_2423_74635, _2425_74636))) % +(_74643) % -(member(skc6, skc10, skc9)) % -(member(skc6, skc9, skc10)) % -(member(skc6, skc7, skc8)) % -(member(skc6, skc8, skc9)) % -(member(skc6, skc8, skc10)) % -(member(skc6, skc10, skc8)) % -(member(skc6, skc10, skc7)) % -(member(skc6, skc8, skc7)) % -(member(skc6, skc9, skc11)) % -(member(skc6, skc7, skc11)) % -(member(skc6, skc11, skc9)) % -(member(skc6, skc11, skc10)) % -(member(skc6, skc11, skc8)) % -(member(skc6, skc11, skc7)) % -(young(U_2510_75018, V_2511_75019)) % -(unisex(U_2510_75044, V_2511_75045)) % -(eventuality(U_2441_75070, V_2442_75071)) % -(state(U_2441_75096, V_2442_75097)) % -(event(U_2441_75122, V_2442_75123)) % -(barrel(U_2441_75148, V_2442_75149)) % -(object(U_2441_75174, V_2442_75175)) % -(artifact(U_2441_75200, V_2442_75201)) % -(instrumentality(U_2441_75226, V_2442_75227)) % -(transport(U_2441_75252, V_2442_75253)) % -(vehicle(U_2441_75278, V_2442_75279)) % -(car(U_2441_75304, V_2442_75305)) % -(chevy(U_2441_75330, V_2442_75331)) % -(way(U_2441_75356, V_2442_75357)) % -(street(U_2441_75382, V_2442_75383)) % -(abstraction(U_2441_75408, V_2442_75409)) % -(relation(U_2441_75434, V_2442_75435)) % -(relname(U_2441_75460, V_2442_75461)) % -(placename(U_2441_75486, V_2442_75487)) % -(hollywood_placename(U_2441_75512, V_2442_75513)) % -(location(U_2441_75538, V_2442_75539)) % -(city(U_2441_75564, V_2442_75565)) % -(furniture(U_2441_75590, V_2442_75591)) % -(seat(U_2441_75616, V_2442_75617)) % -(frontseat(U_2441_75642, V_2442_75643)) % -(specific(U_2510_75668, V_2511_75669)) % -(entity(U_2441_75694, V_2442_75695)) % -(organism(U_2441_75720, V_2442_75721)) % -(human_person(U_2441_75746, V_2442_75747)) % -(man(U_2441_75772, V_2442_75773)) % -(fellow(U_2441_75798, V_2442_75799)) % -(singleton(U_2510_75824, V_2511_75825)) % -(thing(U_2441_75850, V_2442_75851)) % -(nonliving(U_2510_75876, V_2511_75877)) % -(nonhuman(U_2510_75902, V_2511_75903)) % -(existent(U_2510_75928, V_2511_75929)) % -(two(U_2452_75954, _2501_75955)) % -(skc11(_2435_75979)) % -(skc6(_2433_76003)) % -(skc10(_2435_76027)) % -(skc8(_2435_76051)) % -(skc9(_2435_76075)) % -(skc7(_2435_76099)) % -(tpos(skc6, FX_2400_76124)) % -(be(U_2479_76151, V_2480_76152, W_2469_76153, skc6)) % -(be(U_2501_76180, V_2502_76181, skc6, X_2491_76182)) % -(tpos(skc11, FX_2400_76207)) % -(be(U_2479_76234, V_2480_76235, W_2469_76236, skc11)) % -(be(U_2501_76263, V_2502_76264, skc11, X_2491_76265)) % -(tpos(skc10, FX_2400_76290)) % -(be(U_2479_76317, V_2480_76318, W_2469_76319, skc10)) % -(be(U_2501_76346, V_2502_76347, skc10, X_2491_76348)) % -(tpos(skc8, FX_2400_76373)) % -(be(U_2479_76400, V_2480_76401, W_2469_76402, skc8)) % -(be(U_2501_76429, V_2502_76430, skc8, X_2491_76431)) % -(tpos(skc9, FX_2400_76456)) % -(be(U_2479_76483, V_2480_76484, W_2469_76485, skc9)) % -(be(U_2501_76512, V_2502_76513, skc9, X_2491_76514)) % -(tpos(skc7, FX_2399_76539)) % -(be(U_2479_76566, V_2480_76567, W_2469_76568, skc7)) % -(be(U_2501_76595, V_2502_76596, skc7, X_2491_76597)) % -(member(skc6, V_2727_76623, skc11)) % -(member(skc6, V_2727_76649, skc8)) % -(member(skc6, V_2727_76675, skc9)) % -(member(skc6, V_2727_76701, skc10)) % -(member(skc6, V_2727_76727, skc7)) % -(member(Y_2719_76753, skc9, Z_2720_76754)) % -(member(Y_2719_76780, skc7, Z_2720_76781)) % -(member(Y_2719_76807, V_2727_76808, Z_2720_76809)) % %------------------------------------------------------------------------------