%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP154-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art04.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:22 EST 2011 % Result : Satisfiable 47.44s % Output : Assurance 47.44s % 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/NLP154-1+eq_rstfp.tme % result written to : /tmp/NLP154-1+eq_rstfp-eqt.tme % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP154-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP154-1+eq_rstfp-eqt.tme % System...................: Linux art04.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...: [+(_72777)] % 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.....................: 46.98 seconds. % Result...................: SATISFIABLE with model: % -(be(U_2501_72850, V_2502_72851, skc9, skc11)) % -(be(U_2479_72861, V_2480_72862, skc11, skc9)) % -(tpos(skc11, skc9)) % -(tpos(skc9, skc11)) % -(skc11(skc9)) % -(be(U_2501_72892, V_2502_72893, skc7, skc11)) % -(be(U_2479_72903, V_2480_72904, skc11, skc7)) % -(skc9(skc11)) % -(hollywood_placename(skc6, skc11)) % -(tpos(skc11, skc7)) % -(chevy(skc6, skc9)) % -(be(U_2501_72941, V_2502_72942, skc9, skc8)) % -(be(U_2479_72952, V_2480_72953, 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_73018, V_2502_73019, skc9, skc10)) % -(be(U_2479_73029, V_2480_73030, 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_73101, V_2502_73102, skc7, skc8)) % -(be(U_2479_73112, V_2480_73113, 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_73192, V_2502_73193, skc7, skc9)) % -(be(U_2479_73203, V_2480_73204, 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_73262, V_2502_73263, skc7, skc10)) % -(be(U_2479_73273, V_2480_73274, 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_74553, V_2443_74554, V_2443_74554)) % +(skc7(skc7)) % +(skc9(skc9)) % +(skc8(skc8)) % +(skc10(skc10)) % +(skc11(skc11)) % +(skc6(skc6)) % +(skf8(_2423_74599, _2425_74600, skf8(_2423_74599, _2425_74600))) % +(skf5(_2423_74612, _2425_74613, skf5(_2423_74612, _2425_74613))) % +(skf13(_2433_74627, _2435_74628, _2437_74629, _2439_74630, skf13(_2433_74627, _2435_74628, _2437_74629, _2439_74630))) % +(skf12(_2423_74644, _2425_74645, skf12(_2423_74644, _2425_74645))) % +(skf10(_2423_74657, _2425_74658, skf10(_2423_74657, _2425_74658))) % +(_74665) % -(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_75040, V_2511_75041)) % -(unisex(U_2510_75066, V_2511_75067)) % -(eventuality(U_2441_75092, V_2442_75093)) % -(state(U_2441_75118, V_2442_75119)) % -(event(U_2441_75144, V_2442_75145)) % -(barrel(U_2441_75170, V_2442_75171)) % -(object(U_2441_75196, V_2442_75197)) % -(artifact(U_2441_75222, V_2442_75223)) % -(instrumentality(U_2441_75248, V_2442_75249)) % -(transport(U_2441_75274, V_2442_75275)) % -(vehicle(U_2441_75300, V_2442_75301)) % -(car(U_2441_75326, V_2442_75327)) % -(chevy(U_2441_75352, V_2442_75353)) % -(way(U_2441_75378, V_2442_75379)) % -(street(U_2441_75404, V_2442_75405)) % -(abstraction(U_2441_75430, V_2442_75431)) % -(relation(U_2441_75456, V_2442_75457)) % -(relname(U_2441_75482, V_2442_75483)) % -(placename(U_2441_75508, V_2442_75509)) % -(hollywood_placename(U_2441_75534, V_2442_75535)) % -(location(U_2441_75560, V_2442_75561)) % -(city(U_2441_75586, V_2442_75587)) % -(furniture(U_2441_75612, V_2442_75613)) % -(seat(U_2441_75638, V_2442_75639)) % -(frontseat(U_2441_75664, V_2442_75665)) % -(specific(U_2510_75690, V_2511_75691)) % -(entity(U_2441_75716, V_2442_75717)) % -(organism(U_2441_75742, V_2442_75743)) % -(human_person(U_2441_75768, V_2442_75769)) % -(man(U_2441_75794, V_2442_75795)) % -(fellow(U_2441_75820, V_2442_75821)) % -(singleton(U_2510_75846, V_2511_75847)) % -(thing(U_2441_75872, V_2442_75873)) % -(nonliving(U_2510_75898, V_2511_75899)) % -(nonhuman(U_2510_75924, V_2511_75925)) % -(existent(U_2510_75950, V_2511_75951)) % -(two(U_2452_75976, _2501_75977)) % -(skc11(_2435_76001)) % -(skc6(_2433_76025)) % -(skc10(_2435_76049)) % -(skc8(_2435_76073)) % -(skc9(_2435_76097)) % -(skc7(_2435_76121)) % -(tpos(skc6, FX_2400_76146)) % -(be(U_2479_76173, V_2480_76174, W_2469_76175, skc6)) % -(be(U_2501_76202, V_2502_76203, skc6, X_2491_76204)) % -(tpos(skc11, FX_2400_76229)) % -(be(U_2479_76256, V_2480_76257, W_2469_76258, skc11)) % -(be(U_2501_76285, V_2502_76286, skc11, X_2491_76287)) % -(tpos(skc10, FX_2400_76312)) % -(be(U_2479_76339, V_2480_76340, W_2469_76341, skc10)) % -(be(U_2501_76368, V_2502_76369, skc10, X_2491_76370)) % -(tpos(skc8, FX_2400_76395)) % -(be(U_2479_76422, V_2480_76423, W_2469_76424, skc8)) % -(be(U_2501_76451, V_2502_76452, skc8, X_2491_76453)) % -(tpos(skc9, FX_2400_76478)) % -(be(U_2479_76505, V_2480_76506, W_2469_76507, skc9)) % -(be(U_2501_76534, V_2502_76535, skc9, X_2491_76536)) % -(tpos(skc7, FX_2399_76561)) % -(be(U_2479_76588, V_2480_76589, W_2469_76590, skc7)) % -(be(U_2501_76617, V_2502_76618, skc7, X_2491_76619)) % -(member(skc6, X1_2728_76645, skc11)) % -(member(skc6, X1_2728_76671, skc8)) % -(member(skc6, X1_2728_76697, skc9)) % -(member(skc6, X1_2728_76723, skc10)) % -(member(skc6, X1_2728_76749, skc7)) % -(member(Y_2720_76775, skc9, Z_2721_76776)) % -(member(Y_2720_76802, skc7, Z_2721_76803)) % -(member(Y_2720_76829, X1_2728_76830, Z_2721_76831)) % %------------------------------------------------------------------------------