%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP002-1 : TPTP v5.0.0. Released v2.4.0. % Transfm : add_equality % Format : protein % Command : fdp-casc %s %d % Computer : art11.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz % Memory : 2006MB % OS : Linux 2.6.31.5-127.fc12.i686.PAE % CPULimit : 300s % DateTime : Sun Jan 9 22:03:34 EST 2011 % Result : Satisfiable 0.65s % Output : Assurance 0.65s % 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/NLP002-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/NLP002-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/NLP002-1+eq_rstfp-eqt ... % Done. % Input File...............: /tmp/NLP002-1+eq_rstfp-eqt.tme % System...................: Linux art11.cs.miami.edu 2.6.31.5-127.fc12.i686.PAE #1 SMP Sat Nov 7 21:25:57 EST 2009 i686 i686 i386 GNU/Linux % Automatic mode...........: on % Time limit...............: 300 seconds % Current restart interval.: 157 seconds % Restart with =-axioms....: 225 seconds % Initial interpretation...: [+(_41003)] % 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...: 131 % # Unit back subsumptions.: 0 % # Branches closed........: 0 % # Level cuts.............: 0 % Time.....................: 0.21 seconds. % Result...................: SATISFIABLE with model: % -(tpos(skc6, skc4)) % -(tpos(skf1(U_2416_41085, V_2417_41086), skc4)) % -(tpos(skc4, skc6)) % -(tpos(skc4, skf1(_2423_41104, _2425_41105))) % -(skc6(skc4)) % -(skf1(U_2416_41120, V_2417_41121, skc4)) % -(skc4(skc6)) % -(chevy(skc6)) % -(skc4(skf1(_2423_41143, _2425_41144))) % -(chevy(skf1(_2423_41154, _2425_41155))) % -(tpos(skc7, skc4)) % -(event(skc4)) % -(car(skc6)) % -(tpos(skc4, skc7)) % -(car(skf1(_2423_41191, _2425_41192))) % -(skc7(skc4)) % -(hollywood(skc4)) % -(eventuality(skc4)) % -(abstraction(skc4)) % -(tpos(skc6, skc5)) % -(tpos(skf1(U_2416_41234, V_2417_41235), skc5)) % -(vehicle(skc6)) % -(tpos(skc5, skc6)) % -(tpos(skc7, skc6)) % -(skc4(skc7)) % -(chevy(skc7)) % -(tpos(skc6, skc7)) % -(tpos(skf1(U_2416_41285, V_2417_41286), skc7)) % -(vehicle(skf1(_2423_41296, _2425_41297))) % -(tpos(skc5, skf1(_2423_41308, _2425_41309))) % -(tpos(skc7, skf1(_2423_41320, _2425_41321))) % -(tpos(skc5, skc4)) % -(city(skc4)) % +(entity(skc4)) % -(tpos(skc4, skc5)) % -(skc6(skc5)) % -(skf1(U_2416_41362, V_2417_41363, skc5)) % -(transport(skc6)) % -(skc5(skc6)) % -(street(skc6)) % -(skc7(skc6)) % -(hollywood(skc6)) % -(car(skc7)) % -(skc6(skc7)) % -(skf1(U_2416_41414, V_2417_41415, skc7)) % -(transport(skf1(_2423_41425, _2425_41426))) % -(skc5(skf1(_2423_41436, _2425_41437))) % -(street(skf1(_2423_41447, _2425_41448))) % -(skc7(skf1(_2423_41458, _2425_41459))) % -(hollywood(skf1(_2423_41469, _2425_41470))) % -(skc5(skc4)) % -(street(skc4)) % -(location(skc4)) % +(object(skc4)) % -(skc4(skc5)) % -(chevy(skc5)) % -(tpos(skc7, skc5)) % -(event(skc5)) % -(instrumentality(skc6)) % -(way(skc6)) % -(city(skc6)) % -(vehicle(skc7)) % -(tpos(skc5, skc7)) % -(event(skc7)) % -(instrumentality(skf1(_2423_41566, _2425_41567))) % -(way(skf1(_2423_41577, _2425_41578))) % -(city(skf1(_2423_41588, _2425_41589))) % -(way(skc4)) % +(artifact(skc4)) % -(car(skc5)) % -(skc7(skc5)) % -(hollywood(skc5)) % -(eventuality(skc5)) % -(abstraction(skc5)) % -(artifact(skc6)) % -(location(skc6)) % -(transport(skc7)) % -(skc5(skc7)) % -(street(skc7)) % -(eventuality(skc7)) % -(abstraction(skc7)) % -(artifact(skf1(_2423_41683, _2425_41684))) % -(location(skf1(_2423_41694, _2425_41695))) % +(instrumentality(skc4)) % -(vehicle(skc5)) % -(city(skc5)) % +(entity(skc5)) % -(object(skc6)) % -(nonhuman(skc6)) % -(instrumentality(skc7)) % -(way(skc7)) % +(entity(skc7)) % -(object(skf1(_2423_41759, _2425_41760))) % -(nonhuman(skf1(_2423_41770, _2425_41771))) % +(transport(skc4)) % -(transport(skc5)) % -(location(skc5)) % +(object(skc5)) % -(entity(skc6)) % -(abstraction(skc6)) % -(artifact(skc7)) % +(object(skc7)) % -(entity(skf1(_2423_41829, _2425_41830))) % -(abstraction(skf1(_2423_41840, _2425_41841))) % +(vehicle(skc4)) % -(new(skc4)) % -(instrumentality(skc5)) % +(artifact(skc5)) % +(eventuality(skc6)) % +(location(skc7)) % +(eventuality(skf1(_2423_41887, _2425_41888))) % +(barrel(skc6, skc4)) % +(chevy(skc4)) % +(car(skc4)) % +(white(skc4)) % +(dirty(skc4)) % +(old(skc4)) % +(down(skc6, skc5)) % +(lonely(skc5)) % +(way(skc5)) % +(street(skc5)) % +(in(skc6, skc7)) % +(event(skc6)) % +(city(skc7)) % +(hollywood(skc7)) % +(event(skf1(_2423_41985, _2425_41986))) % +(skc4(skc4)) % +(skc5(skc5)) % +(skc6(skc6)) % +(skc7(skc7)) % +(skf1(_2423_42019, _2425_42020, skf1(_2423_42019, _2425_42020))) % +(_42027) % %------------------------------------------------------------------------------