%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP150-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art01.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:24:41 EST 2011 % Result : Satisfiable 19.17s % Output : Assurance 19.17s % 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/NLP150-1+eq_rstfp.tme % result written to : /tmp/NLP150-1+eq_rstfp-eqt.tme % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP150-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP150-1+eq_rstfp-eqt.tme % System...................: Linux art01.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...: [+(_58892)] % 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.................: 71 % # Commits................: 0 % # Unit extension steps...: 205 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 18.68 seconds. % Result...................: SATISFIABLE with model: % -(be(U_2501_58965, V_2502_58966, skc8, skc9)) % -(be(U_2479_58976, V_2480_58977, skc9, skc8)) % -(tpos(skc9, skc8)) % -(tpos(skc8, skc9)) % -(skc9(skc8)) % -(be(U_2501_59007, V_2502_59008, skc6, skc9)) % -(be(U_2479_59018, V_2480_59019, skc9, skc6)) % -(skc8(skc9)) % -(hollywood_placename(skc5, skc9)) % -(tpos(skc9, skc6)) % -(chevy(skc5, skc8)) % -(tpos(skc6, skc9)) % -(placename(skc5, skc9)) % -(two(skc5, skc9)) % -(skc9(skc6)) % -(be(U_2501_59083, V_2502_59084, skc7, skc8)) % -(be(U_2479_59094, V_2480_59095, skc8, skc7)) % -(frontseat(skc5, skc8)) % -(car(skc5, skc8)) % -(skc6(skc9)) % -(barrel(skc5, skc9)) % -(relname(skc5, skc9)) % -(group(skc5, skc9)) % -(chevy(skc5, skc6)) % -(tpos(skc8, skc7)) % -(tpos(skc7, skc8)) % -(seat(skc5, skc8)) % -(vehicle(skc5, skc8)) % -(event(skc5, skc9)) % -(state(skc5, skc9)) % -(relation(skc5, skc9)) % -(set(skc5, skc9)) % -(frontseat(skc5, skc6)) % -(car(skc5, skc6)) % -(be(U_2501_59223, V_2502_59224, skc6, skc7)) % -(be(U_2479_59234, V_2480_59235, skc7, skc6)) % -(skc8(skc7)) % -(hollywood_placename(skc5, skc7)) % -(be(U_2501_59258, V_2502_59259, skc6, skc8)) % -(be(U_2479_59269, V_2480_59270, skc8, skc6)) % -(skc7(skc8)) % -(street(skc5, skc8)) % -(furniture(skc5, skc8)) % -(transport(skc5, skc8)) % -(fellow(skc5, skc9)) % -(eventuality(skc5, skc9)) % -(abstraction(skc5, skc9)) % -(multiple(skc5, skc9)) % -(tpos(skc7, skc6)) % -(seat(skc5, skc6)) % -(vehicle(skc5, skc6)) % -(tpos(skc8, skc6)) % -(tpos(skc6, skc7)) % -(placename(skc5, skc7)) % -(two(skc5, skc7)) % -(tpos(skc6, skc8)) % -(city(skc5, skc8)) % -(way(skc5, skc8)) % -(instrumentality(skc5, skc8)) % -(two(skc5, skc8)) % -(man(skc5, skc9)) % -(human_person(skc5, skc9)) % -(organism(skc5, skc9)) % -(nonexistent(skc5, skc9)) % -(general(skc5, skc9)) % +(singleton(skc5, skc9)) % -(skc7(skc6)) % -(street(skc5, skc6)) % -(furniture(skc5, skc6)) % -(transport(skc5, skc6)) % -(skc8(skc6)) % -(hollywood_placename(skc5, skc6)) % -(skc6(skc7)) % -(barrel(skc5, skc7)) % -(relname(skc5, skc7)) % -(group(skc5, skc7)) % -(skc6(skc8)) % -(barrel(skc5, skc8)) % -(location(skc5, skc8)) % -(artifact(skc5, skc8)) % -(group(skc5, skc8)) % -(male(skc5, skc9)) % -(animate(skc5, skc9)) % -(living(skc5, skc9)) % +(existent(skc5, skc9)) % +(specific(skc5, skc9)) % +(thing(skc5, skc9)) % -(city(skc5, skc6)) % -(way(skc5, skc6)) % -(instrumentality(skc5, skc6)) % -(placename(skc5, skc6)) % -(two(skc5, skc6)) % -(event(skc5, skc7)) % -(state(skc5, skc7)) % -(relation(skc5, skc7)) % -(set(skc5, skc7)) % -(fellow(skc5, skc8)) % -(event(skc5, skc8)) % -(state(skc5, skc8)) % -(object(skc5, skc8)) % -(organism(skc5, skc8)) % -(set(skc5, skc8)) % +(unisex(skc5, skc9)) % +(impartial(skc5, skc9)) % +(nonliving(skc5, skc9)) % +(entity(skc5, skc9)) % -(location(skc5, skc6)) % -(artifact(skc5, skc6)) % -(human_person(skc5, skc6)) % -(relname(skc5, skc6)) % -(group(skc5, skc6)) % -(fellow(skc5, skc7)) % -(eventuality(skc5, skc7)) % -(abstraction(skc5, skc7)) % -(multiple(skc5, skc7)) % -(man(skc5, skc8)) % -(eventuality(skc5, skc8)) % -(entity(skc5, skc8)) % -(human_person(skc5, skc8)) % -(multiple(skc5, skc8)) % +(object(skc5, skc9)) % -(fellow(skc5, skc6)) % -(object(skc5, skc6)) % -(organism(skc5, skc6)) % -(relation(skc5, skc6)) % -(set(skc5, skc6)) % -(man(skc5, skc7)) % -(human_person(skc5, skc7)) % -(organism(skc5, skc7)) % -(nonexistent(skc5, skc7)) % -(general(skc5, skc7)) % +(singleton(skc5, skc7)) % -(male(skc5, skc8)) % -(specific(skc5, skc8)) % -(human(skc5, skc8)) % +(singleton(skc5, skc8)) % +(artifact(skc5, skc9)) % -(man(skc5, skc6)) % -(entity(skc5, skc6)) % -(abstraction(skc5, skc6)) % -(multiple(skc5, skc6)) % -(male(skc5, skc7)) % -(animate(skc5, skc7)) % -(living(skc5, skc7)) % +(tpos(skc8, skc8)) % +(existent(skc5, skc7)) % +(specific(skc5, skc7)) % +(thing(skc5, skc7)) % +(unisex(skc5, skc8)) % +(general(skc5, skc8)) % +(nonhuman(skc5, skc8)) % +(thing(skc5, skc8)) % +(instrumentality(skc5, skc9)) % -(male(skc5, skc6)) % -(existent(skc5, skc6)) % -(general(skc5, skc6)) % +(singleton(skc5, skc6)) % +(unisex(skc5, skc7)) % +(impartial(skc5, skc7)) % +(nonliving(skc5, skc7)) % +(entity(skc5, skc7)) % +(abstraction(skc5, skc8)) % +(transport(skc5, skc9)) % +(unisex(skc5, skc6)) % +(nonexistent(skc5, skc6)) % +(specific(skc5, skc6)) % +(thing(skc5, skc6)) % +(artifact(skc5, skc7)) % +(object(skc5, skc7)) % +(relation(skc5, skc8)) % +(vehicle(skc5, skc9)) % +(eventuality(skc5, skc6)) % +(way(skc5, skc7)) % +(location(skc5, skc7)) % +(relname(skc5, skc8)) % -(young(skc5, skc9)) % +(car(skc5, skc9)) % +(agent(skc5, skc6, skc9)) % +(in(skc5, skc6, skc7)) % +(down(skc5, skc6, skc7)) % +(event(skc5, skc6)) % +(present(skc5, skc6)) % +(barrel(skc5, skc6)) % +(of(skc5, skc8, skc7)) % +(lonely(skc5, skc7)) % +(street(skc5, skc7)) % +(city(skc5, skc7)) % +(hollywood_placename(skc5, skc8)) % +(placename(skc5, skc8)) % +(old(skc5, skc9)) % +(dirty(skc5, skc9)) % +(white(skc5, skc9)) % +(chevy(skc5, skc9)) % +(actual_world(skc5)) % -(member(U_2442_60355, V_2443_60356, V_2443_60356)) % +(skc6(skc6)) % +(skc7(skc7)) % +(skc8(skc8)) % +(skc9(skc9)) % +(skc5(skc5)) % +(skf8(_2423_60395, _2425_60396, skf8(_2423_60395, _2425_60396))) % +(skf5(_2423_60408, _2425_60409, skf5(_2423_60408, _2425_60409))) % +(skf13(_2433_60423, _2435_60424, _2437_60425, _2439_60426, skf13(_2433_60423, _2435_60424, _2437_60425, _2439_60426))) % +(skf12(_2423_60440, _2425_60441, skf12(_2423_60440, _2425_60441))) % +(skf10(_2423_60453, _2425_60454, skf10(_2423_60453, _2425_60454))) % +(_60461) % -(member(skc5, skc8, skc7)) % -(member(skc5, skc7, skc8)) % -(member(skc5, skc8, skc6)) % -(member(skc5, skc7, skc9)) % -(member(skc5, skc6, skc9)) % -(member(skc5, skc9, skc7)) % -(member(skc5, skc9, skc8)) % -(young(U_2510_60661, V_2511_60662)) % -(unisex(U_2510_60687, V_2511_60688)) % -(eventuality(U_2441_60713, V_2442_60714)) % -(state(U_2441_60739, V_2442_60740)) % -(event(U_2441_60765, V_2442_60766)) % -(barrel(U_2441_60791, V_2442_60792)) % -(object(U_2441_60817, V_2442_60818)) % -(artifact(U_2441_60843, V_2442_60844)) % -(instrumentality(U_2441_60869, V_2442_60870)) % -(transport(U_2441_60895, V_2442_60896)) % -(vehicle(U_2441_60921, V_2442_60922)) % -(car(U_2441_60947, V_2442_60948)) % -(chevy(U_2441_60973, V_2442_60974)) % -(way(U_2441_60999, V_2442_61000)) % -(street(U_2441_61025, V_2442_61026)) % -(abstraction(U_2441_61051, V_2442_61052)) % -(relation(U_2441_61077, V_2442_61078)) % -(relname(U_2441_61103, V_2442_61104)) % -(placename(U_2441_61129, V_2442_61130)) % -(hollywood_placename(U_2441_61155, V_2442_61156)) % -(location(U_2441_61181, V_2442_61182)) % -(city(U_2441_61207, V_2442_61208)) % -(furniture(U_2441_61233, V_2442_61234)) % -(seat(U_2441_61259, V_2442_61260)) % -(frontseat(U_2441_61285, V_2442_61286)) % -(specific(U_2510_61311, V_2511_61312)) % -(entity(U_2441_61337, V_2442_61338)) % -(organism(U_2441_61363, V_2442_61364)) % -(human_person(U_2441_61389, V_2442_61390)) % -(man(U_2441_61415, V_2442_61416)) % -(fellow(U_2441_61441, V_2442_61442)) % -(singleton(U_2510_61467, V_2511_61468)) % -(thing(U_2441_61493, V_2442_61494)) % -(nonliving(U_2510_61519, V_2511_61520)) % -(nonhuman(U_2510_61545, V_2511_61546)) % -(existent(U_2510_61571, V_2511_61572)) % -(two(U_2452_61597, _2501_61598)) % -(skc9(_2435_61622)) % -(skc5(_2433_61646)) % -(skc8(_2435_61670)) % -(skc7(_2435_61694)) % -(skc6(_2435_61718)) % -(tpos(skc5, FX_2400_61743)) % -(be(U_2479_61770, V_2480_61771, W_2469_61772, skc5)) % -(be(U_2501_61799, V_2502_61800, skc5, X_2491_61801)) % -(tpos(skc9, FX_2400_61826)) % -(be(U_2479_61853, V_2480_61854, W_2469_61855, skc9)) % -(be(U_2501_61882, V_2502_61883, skc9, X_2491_61884)) % -(tpos(skc8, FX_2400_61909)) % -(be(U_2479_61936, V_2480_61937, W_2469_61938, skc8)) % -(be(U_2501_61965, V_2502_61966, skc8, X_2491_61967)) % -(tpos(skc7, FX_2400_61992)) % -(be(U_2479_62019, V_2480_62020, W_2469_62021, skc7)) % -(be(U_2501_62048, V_2502_62049, skc7, X_2491_62050)) % -(tpos(skc6, FX_2399_62075)) % -(be(U_2479_62102, V_2480_62103, W_2469_62104, skc6)) % -(be(U_2501_62131, V_2502_62132, skc6, X_2491_62133)) % -(member(skc5, X1_2728_62159, skc9)) % -(member(skc5, X1_2728_62185, skc7)) % -(member(skc5, X1_2728_62211, skc8)) % -(member(skc5, X1_2728_62237, skc6)) % -(member(Y_2720_62263, skc8, Z_2721_62264)) % -(member(Y_2720_62290, skc6, Z_2721_62291)) % -(member(Y_2720_62317, X1_2728_62318, Z_2721_62319)) % %------------------------------------------------------------------------------