%------------------------------------------------------------------------------ % File : FDP---0.9.16 % Problem : NLP060-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:14:53 EST 2011 % Result : Satisfiable 1.03s % Output : Assurance 1.03s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % FDPLL - A First-Order Davis-Putnam Theorem Prover % Version 0.9.16 (26/06/2002) % Proving /tmp/NLP060-1+noeq ... % Done. % Input File...............: /tmp/NLP060-1+noeq.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.: 210 seconds % Restart with =-axioms....: off % Initial interpretation...: [+(_43966)] % Clause set type..........: Non-Horn, without equality % Equality transformation..: off % Non-constant functions...: yes % Term depth settings......: 3/2 (Init/Increment) % unit_extend..............: on % splitting type...........: exact % Final tree statistics: % Tree for clause set......: as initially given % # Restarts...............: 0 % Term depth limit.........: 5 % # Splits.................: 31 % # Commits................: 7 % # Unit extension steps...: 28 % # Unit back subsumptions.: 0 % # Branches closed........: 3 % # Level cuts.............: 0 % Time.....................: 0.8 seconds. % Result...................: SATISFIABLE with model: % +(actual_world(skc6)) % +(actual_world(skc61)) % +(_44044) % +(ssSkP1(skc63, skc62, skc61)) % +(male(skc61, skc63)) % +(group(skc61, skc62)) % +(six(skc61, skc62)) % -(ssSkC0) % +(of(skc61, skf20(skc61, skc63, skf14(skc62, skc61, X_44129), skf18(skc61, X_44134, Y_44135)), skc63)) % +(patient(skc61, skf19(skc61, skf18(skc61, W_44153, skc62), skf14(skc62, skc61, W_44153), X2_44158), skf14(skc62, skc61, W_44153))) % +(member(skc61, skf14(skc62, skc61, skc63), skc62)) % +(patient(skc61, skf19(skc61, skf18(skc61, skc63, skc62), skf14(skc62, skc61, skc63), X2_44196), skf14(skc62, skc61, skc63))) % -(from_loc(skc61, skf19(skc61, skf18(skc61, skc63, skc62), skf14(skc62, skc61, skc63), Z_44222), skf16(skc61, skc63, skc62))) % +(from_loc(skc61, skf19(skc61, skf18(skc61, X_44244, Y_44245), skf14(skc62, skc61, X_44250), skc63), skf20(skc61, skc63, skf14(skc62, skc61, X_44250), skf18(skc61, X_44244, Y_44245)))) % +(patient(skc61, skf19(skc61, skf18(skc61, X_44281, Y_44282), skf14(skc62, skc61, X_44287), Z_44288), skf14(skc62, skc61, X_44287))) % +(agent(skc61, skf19(skc61, skf18(skc61, skc63, skc62), Z_44310, X1_44311), skf18(skc61, skc63, skc62))) % +(agent(skc61, skf19(skc61, skf18(skc61, skc63, Y_44333), Z_44334, X1_44335), skf18(skc61, skc63, Y_44333))) % +(agent(skc61, skf19(skc61, skf18(skc61, X_44357, skc62), Z_44358, X1_44359), skf18(skc61, X_44357, skc62))) % +(agent(skc61, skf19(skc61, skf18(skc61, X_44381, Y_44382), Z_44383, X1_44384), skf18(skc61, X_44381, Y_44382))) % +(of(skc61, skf20(skc61, skc63, Z_44402, X1_44403), skc63)) % +(cannon(skc61, skf20(skc61, Z_44416, X1_44417, X2_44418))) % +(fire(skc61, skf19(skc61, Z_44431, X1_44432, X2_44433))) % +(nonreflexive(skc61, skf19(skc61, Z_44446, X1_44447, X2_44448))) % +(present(skc61, skf19(skc61, Z_44461, X1_44462, X2_44463))) % +(event(skc61, skf19(skc61, Z_44476, X1_44477, X2_44478))) % +(shot(skc61, skf14(skc62, skc61, X_44490))) % +(of(skc61, skf16(skc61, skc63, X_44503), skc63)) % +(member(skc61, skf14(skc62, skc61, X_44516), skc62)) % +(man(skc61, skf18(skc61, X_44528, Y_44529))) % +(cannon(skc61, skf16(skc61, X_44541, Y_44542))) % -(ssSkP0(skc62, skc63, skc61)) % -(male(skc61, X_44575)) % -(ssSkP0(V_44601, skc63, skc61)) % -(male(skc6, X_44626)) % -(actual_world(U_44650)) % -(agent(skc61, skf19(skc61, Z_44681, X1_44682, X2_44683), skf18(skc61, skc63, skc62))) % -(event(skc61, V_44712)) % -(ssSkP0(skc62, Y_44738, skc61)) % -(ssSkP0(W_44764, Y_44765, skc61)) % -(agent(skc61, skf19(skc61, Z_44796, X1_44797, X2_44798), skf18(skc61, skc63, X_44803))) % -(agent(skc61, skf19(skc61, Z_44834, X1_44835, X2_44836), skf18(skc61, W_44841, skc62))) % -(agent(skc61, skf19(skc61, Z_44872, X1_44873, X2_44874), skf18(skc61, W_44879, X_44880))) % -(patient(skc61, skf19(skc61, skf18(skc61, skc63, skc62), X1_44915, X2_44916), skf14(skc62, skc61, skc63))) % -(patient(skc61, skf19(skc61, skf18(skc61, skc63, X_44955), X1_44956, X2_44957), skf14(X_44955, skc61, skc63))) % -(member(skc61, skf14(X_44991, skc61, skc63), skc62)) % -(ssSkP1(Y_45017, W_45018, skc61)) % -(from_loc(skc61, skf19(skc61, skf18(skc61, W_45053, skc62), skf14(skc62, skc61, W_45053), X2_45058), skf16(skc61, W_45053, skc62))) % -(patient(skc61, skf19(skc61, skf18(skc61, W_45097, skc62), X1_45098, X2_45099), skf14(skc62, skc61, W_45097))) % -(patient(skc61, skf19(skc61, skf18(skc61, W_45138, X_45139), X1_45140, X2_45141), skf14(X_45139, skc61, W_45138))) % -(member(skc61, skf14(X_45175, skc61, W_45176), skc62)) % -(of(skc61, skf20(skc61, skc63, skf14(skc62, skc61, X_45211), skf18(skc61, X_45216, Y_45217)), X_45218)) % -(of(skc61, skf20(skc61, Z_45249, X1_45250, X2_45251), X_45252)) % +(of(skc61, skf16(skc61, X_45282, Y_45283), X_45284)) % -(from_loc(skc61, skf19(skc61, Z_45315, X1_45316, X2_45317), skf16(skc61, X_45322, Y_45323))) % -(of(skc61, Y_45349, X_45350)) % +(ssSkP1(skc63, W_45376, skc61)) % +(member(skc61, skf14(X_45406, skc61, skc63), W_45407)) % +(patient(skc61, skf19(skc61, skf18(skc61, skc63, X_45442), skf14(X_45442, skc61, skc63), Z_45447), skf14(X_45442, skc61, skc63))) % +(member(skc61, skf14(X_45481, skc61, W_45482), W_45483)) % +(patient(skc61, skf19(skc61, skf18(skc61, W_45518, X_45519), skf14(X_45519, skc61, W_45518), Z_45524), skf14(X_45519, skc61, W_45518))) % %------------------------------------------------------------------------------