%------------------------------------------------------------------------------ % File : Refute---2015 % Problem : NLP196+1 : TPTP v6.4.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_refute %d %s % Computer : n028.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 16091.75MB % OS : Linux 3.10.0-327.10.1.el7.x86_64 % CPULimit : 300s % DateTime : Thu Apr 14 01:28:25 EDT 2016 % Result : Timeout 300.36s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NLP196+1 : TPTP v6.4.0. Released v2.4.0. % 0.00/0.04 % Command : isabelle tptp_refute %d %s % 0.03/0.23 % Computer : n028.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 16091.75MB % 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Tue Apr 5 13:55:09 CDT 2016 % 0.03/0.23 % CPUTime : % 6.26/5.85 > val it = (): unit % 6.51/6.49 Trying to find a model that refutes: ~ ~ (((EX U. bnd_actual_world U & % 6.51/6.49 (EX V W X Y Z X1 X2 X3 X4 X5 X6. % 6.51/6.49 ((((((((((((((((((((((((((((((bnd_of U W V & bnd_man U V) & % 6.51/6.49 bnd_jules_forename U W) & % 6.51/6.49 bnd_forename U W) & % 6.51/6.49 bnd_frontseat U X) & % 6.51/6.49 bnd_chevy U Y) & % 6.51/6.49 bnd_white U Y) & % 6.51/6.49 bnd_dirty U Y) & % 6.51/6.49 bnd_old U Y) & % 6.51/6.49 bnd_of U Z X1) & % 6.51/6.49 bnd_city U X1) & % 6.51/6.49 bnd_hollywood_placename U Z) & % 6.51/6.49 bnd_placename U Z) & % 6.51/6.49 bnd_street U X1) & % 6.51/6.49 bnd_lonely U X1) & % 6.51/6.49 bnd_event U X2) & % 6.51/6.49 bnd_agent U X2 Y) & % 6.51/6.49 bnd_present U X2) & % 6.51/6.49 bnd_barrel U X2) & % 6.51/6.49 bnd_down U X2 X1) & % 6.51/6.49 bnd_in U X2 X1) & % 6.51/6.49 (ALL X7. % 6.51/6.49 bnd_member U X7 X3 --> % 6.51/6.49 (EX X8 X9. % 6.51/6.49 (bnd_state U X8 & bnd_be U X8 X7 X9) & % 6.51/6.49 bnd_in U X9 X))) & % 6.51/6.49 bnd_two U X3) & % 6.51/6.49 bnd_group U X3) & % 6.51/6.49 (ALL X10. % 6.51/6.49 bnd_member U X10 X3 --> % 6.51/6.49 bnd_fellow U X10 & bnd_young U X10)) & % 6.51/6.49 (ALL X11. % 6.51/6.49 bnd_member U X11 X4 --> % 6.51/6.49 (ALL X12. % 6.51/6.49 bnd_member U X12 X3 --> % 6.51/6.49 (EX X13. % 6.51/6.49 ((((bnd_event U X13 & % 6.51/6.49 bnd_agent U X13 X12) & % 6.51/6.49 bnd_patient U X13 X11) & % 6.51/6.49 bnd_present U X13) & % 6.51/6.49 bnd_nonreflexive U X13) & % 6.51/6.49 bnd_wear U X13)))) & % 6.51/6.49 bnd_group U X4) & % 6.51/6.49 (ALL X14. % 6.51/6.49 bnd_member U X14 X4 --> % 6.51/6.49 (bnd_coat U X14 & bnd_black U X14) & % 6.51/6.49 bnd_cheap U X14)) & % 6.51/6.49 bnd_wheel U X6) & % 6.51/6.49 bnd_state U X5) & % 6.51/6.49 bnd_be U X5 V X6) & % 6.51/6.49 bnd_behind U X6 X6)) --> % 6.51/6.49 (EX X15. % 6.51/6.49 bnd_actual_world X15 & % 6.51/6.49 (EX X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27. % 6.51/6.49 ((((((((((((((((((((((((((((((bnd_of X15 X17 X16 & % 6.51/6.49 bnd_man X15 X16) & % 6.51/6.49 bnd_jules_forename X15 X17) & % 6.51/6.49 bnd_forename X15 X17) & % 6.51/6.49 bnd_wheel X15 X18) & % 6.51/6.49 bnd_frontseat X15 X19) & % 6.51/6.49 bnd_chevy X15 X20) & % 6.51/6.49 bnd_white X15 X20) & % 6.51/6.49 bnd_dirty X15 X20) & % 6.51/6.49 bnd_old X15 X20) & % 6.51/6.49 bnd_of X15 X21 X22) & % 6.51/6.49 bnd_city X15 X22) & % 6.51/6.49 bnd_hollywood_placename X15 X21) & % 6.51/6.49 bnd_placename X15 X21) & % 6.51/6.49 bnd_street X15 X22) & % 6.51/6.49 bnd_lonely X15 X22) & % 6.51/6.49 bnd_event X15 X23) & % 6.51/6.49 bnd_agent X15 X23 X20) & % 6.51/6.49 bnd_present X15 X23) & % 6.51/6.49 bnd_barrel X15 X23) & % 6.51/6.49 bnd_down X15 X23 X22) & % 6.51/6.49 bnd_in X15 X23 X22) & % 6.51/6.49 (ALL X28. % 6.51/6.49 bnd_member X15 X28 X24 --> % 6.51/6.49 (EX X29 X30. % 6.51/6.49 (bnd_state X15 X29 & % 6.51/6.49 bnd_be X15 X29 X28 X30) & % 6.51/6.49 bnd_in X15 X30 X19))) & % 6.51/6.49 bnd_two X15 X24) & % 6.51/6.49 bnd_group X15 X24) & % 6.51/6.49 (ALL X31. % 6.51/6.49 bnd_member X15 X31 X24 --> % 6.51/6.49 bnd_fellow X15 X31 & bnd_young X15 X31)) & % 6.51/6.49 (ALL X32. % 6.51/6.49 bnd_member X15 X32 X25 --> % 6.51/6.49 (ALL X33. % 6.51/6.49 bnd_member X15 X33 X24 --> % 6.51/6.49 (EX X34. % 6.51/6.49 ((((bnd_event X15 X34 & % 6.51/6.49 bnd_agent X15 X34 X33) & % 6.51/6.49 bnd_patient X15 X34 X32) & % 6.51/6.49 bnd_present X15 X34) & % 6.51/6.49 bnd_nonreflexive X15 X34) & % 6.51/6.49 bnd_wear X15 X34)))) & % 6.51/6.49 bnd_group X15 X25) & % 6.51/6.49 (ALL X35. % 6.51/6.49 bnd_member X15 X35 X25 --> % 6.51/6.49 (bnd_coat X15 X35 & bnd_black X15 X35) & % 6.51/6.49 bnd_cheap X15 X35)) & % 6.51/6.49 bnd_state X15 X26) & % 6.51/6.49 bnd_be X15 X26 X16 X27) & % 6.51/6.49 bnd_behind X15 X27 X18))) & % 6.51/6.49 ((EX X15. % 6.51/6.49 bnd_actual_world X15 & % 6.51/6.49 (EX X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27. % 6.51/6.49 ((((((((((((((((((((((((((((((bnd_of X15 X17 X16 & % 6.51/6.49 bnd_man X15 X16) & % 6.51/6.49 bnd_jules_forename X15 X17) & % 6.51/6.49 bnd_forename X15 X17) & % 6.51/6.49 bnd_wheel X15 X18) & % 6.51/6.49 bnd_frontseat X15 X19) & % 6.51/6.49 bnd_chevy X15 X20) & % 6.51/6.49 bnd_white X15 X20) & % 6.51/6.49 bnd_dirty X15 X20) & % 6.51/6.49 bnd_old X15 X20) & % 6.51/6.49 bnd_of X15 X21 X22) & % 6.51/6.49 bnd_city X15 X22) & % 6.51/6.49 bnd_hollywood_placename X15 X21) & % 6.51/6.49 bnd_placename X15 X21) & % 6.51/6.49 bnd_street X15 X22) & % 6.51/6.49 bnd_lonely X15 X22) & % 6.51/6.49 bnd_event X15 X23) & % 6.51/6.49 bnd_agent X15 X23 X20) & % 6.51/6.49 bnd_present X15 X23) & % 6.51/6.49 bnd_barrel X15 X23) & % 6.51/6.49 bnd_down X15 X23 X22) & % 6.51/6.49 bnd_in X15 X23 X22) & % 6.51/6.49 (ALL X28. % 6.51/6.49 bnd_member X15 X28 X24 --> % 6.51/6.49 (EX X29 X30. % 6.51/6.49 (bnd_state X15 X29 & % 6.51/6.49 bnd_be X15 X29 X28 X30) & % 6.51/6.49 bnd_in X15 X30 X19))) & % 6.51/6.49 bnd_two X15 X24) & % 6.51/6.49 bnd_group X15 X24) & % 6.51/6.49 (ALL X31. % 6.51/6.49 bnd_member X15 X31 X24 --> % 6.51/6.49 bnd_fellow X15 X31 & bnd_young X15 X31)) & % 6.51/6.49 (ALL X32. % 6.51/6.49 bnd_member X15 X32 X25 --> % 6.51/6.49 (ALL X33. % 6.51/6.49 bnd_member X15 X33 X24 --> % 6.51/6.49 (EX X34. % 6.51/6.49 ((((bnd_event X15 X34 & % 6.51/6.49 bnd_agent X15 X34 X33) & % 6.51/6.49 bnd_patient X15 X34 X32) & % 6.51/6.49 bnd_present X15 X34) & % 6.51/6.49 bnd_nonreflexive X15 X34) & % 6.51/6.49 bnd_wear X15 X34)))) & % 6.51/6.49 bnd_group X15 X25) & % 6.51/6.49 (ALL X35. % 6.51/6.49 bnd_member X15 X35 X25 --> % 6.51/6.49 (bnd_coat X15 X35 & bnd_black X15 X35) & % 6.51/6.49 bnd_cheap X15 X35)) & % 6.51/6.49 bnd_state X15 X26) & % 6.51/6.49 bnd_be X15 X26 X16 X27) & % 6.51/6.49 bnd_behind X15 X27 X18)) --> % 6.51/6.49 (EX U. bnd_actual_world U & % 6.51/6.49 (EX V W X Y Z X1 X2 X3 X4 X5 X6. % 6.51/6.49 ((((((((((((((((((((((((((((((bnd_of U W V & bnd_man U V) & % 6.51/6.49 bnd_jules_forename U W) & % 6.51/6.49 bnd_forename U W) & % 6.51/6.49 bnd_frontseat U X) & % 6.51/6.49 bnd_chevy U Y) & % 6.51/6.49 bnd_white U Y) & % 6.51/6.49 bnd_dirty U Y) & % 6.51/6.49 bnd_old U Y) & % 6.51/6.49 bnd_of U Z X1) & % 6.51/6.49 bnd_city U X1) & % 6.51/6.49 bnd_hollywood_placename U Z) & % 6.51/6.49 bnd_placename U Z) & % 6.51/6.49 bnd_street U X1) & % 6.51/6.49 bnd_lonely U X1) & % 6.51/6.49 bnd_event U X2) & % 6.51/6.49 bnd_agent U X2 Y) & % 6.51/6.49 bnd_present U X2) & % 6.51/6.49 bnd_barrel U X2) & % 6.51/6.49 bnd_down U X2 X1) & % 6.51/6.49 bnd_in U X2 X1) & % 6.51/6.49 (ALL X7. % 6.51/6.49 bnd_member U X7 X3 --> % 6.51/6.49 (EX X8 X9. % 6.51/6.49 (bnd_state U X8 & bnd_be U X8 X7 X9) & % 6.51/6.49 bnd_in U X9 X))) & % 6.51/6.49 bnd_two U X3) & % 6.51/6.49 bnd_group U X3) & % 6.51/6.49 (ALL X10. % 6.51/6.49 bnd_member U X10 X3 --> % 6.51/6.49 bnd_fellow U X10 & bnd_young U X10)) & % 6.51/6.49 (ALL X11. % 6.51/6.49 bnd_member U X11 X4 --> % 6.51/6.49 (ALL X12. % 6.51/6.49 bnd_member U X12 X3 --> % 6.51/6.49 (EX X13. % 6.51/6.49 ((((bnd_event U X13 & % 6.51/6.49 bnd_agent U X13 X12) & % 6.51/6.49 bnd_patient U X13 X11) & % 6.51/6.49 bnd_present U X13) & % 6.51/6.49 bnd_nonreflexive U X13) & % 6.51/6.49 bnd_wear U X13)))) & % 6.51/6.50 bnd_group U X4) & % 6.51/6.50 (ALL X14. % 6.51/6.50 bnd_member U X14 X4 --> % 6.51/6.50 (bnd_coat U X14 & bnd_black U X14) & % 6.51/6.50 bnd_cheap U X14)) & % 6.51/6.50 bnd_wheel U X6) & % 6.51/6.50 bnd_state U X5) & % 6.51/6.50 bnd_be U X5 V X6) & % 6.51/6.50 bnd_behind U X6 X6)))) % 7.61/7.56 Unfolded term: ~ ~ (((EX U. bnd_actual_world U & % 7.61/7.56 (EX V W X Y Z X1 X2 X3 X4 X5 X6. % 7.61/7.56 ((((((((((((((((((((((((((((((bnd_of U W V & bnd_man U V) & % 7.61/7.56 bnd_jules_forename U W) & % 7.61/7.56 bnd_forename U W) & % 7.61/7.56 bnd_frontseat U X) & % 7.61/7.56 bnd_chevy U Y) & % 7.61/7.56 bnd_white U Y) & % 7.61/7.56 bnd_dirty U Y) & % 7.61/7.56 bnd_old U Y) & % 7.61/7.56 bnd_of U Z X1) & % 7.61/7.56 bnd_city U X1) & % 7.61/7.56 bnd_hollywood_placename U Z) & % 7.61/7.56 bnd_placename U Z) & % 7.61/7.56 bnd_street U X1) & % 7.61/7.56 bnd_lonely U X1) & % 7.61/7.56 bnd_event U X2) & % 7.61/7.56 bnd_agent U X2 Y) & % 7.61/7.56 bnd_present U X2) & % 7.61/7.56 bnd_barrel U X2) & % 7.61/7.56 bnd_down U X2 X1) & % 7.61/7.56 bnd_in U X2 X1) & % 7.61/7.56 (ALL X7. % 7.61/7.56 bnd_member U X7 X3 --> % 7.61/7.56 (EX X8 X9. % 7.61/7.56 (bnd_state U X8 & bnd_be U X8 X7 X9) & % 7.61/7.56 bnd_in U X9 X))) & % 7.61/7.56 bnd_two U X3) & % 7.61/7.56 bnd_group U X3) & % 7.61/7.56 (ALL X10. % 7.61/7.56 bnd_member U X10 X3 --> % 7.61/7.56 bnd_fellow U X10 & bnd_young U X10)) & % 7.61/7.56 (ALL X11. % 7.61/7.56 bnd_member U X11 X4 --> % 7.61/7.56 (ALL X12. % 7.61/7.56 bnd_member U X12 X3 --> % 7.61/7.56 (EX X13. % 7.61/7.56 ((((bnd_event U X13 & % 7.61/7.56 bnd_agent U X13 X12) & % 7.61/7.56 bnd_patient U X13 X11) & % 7.61/7.56 bnd_present U X13) & % 7.61/7.56 bnd_nonreflexive U X13) & % 7.61/7.56 bnd_wear U X13)))) & % 7.61/7.56 bnd_group U X4) & % 7.61/7.56 (ALL X14. % 7.61/7.56 bnd_member U X14 X4 --> % 7.61/7.56 (bnd_coat U X14 & bnd_black U X14) & % 7.61/7.56 bnd_cheap U X14)) & % 7.61/7.56 bnd_wheel U X6) & % 7.61/7.56 bnd_state U X5) & % 7.61/7.56 bnd_be U X5 V X6) & % 7.61/7.56 bnd_behind U X6 X6)) --> % 7.61/7.56 (EX X15. % 7.61/7.56 bnd_actual_world X15 & % 7.61/7.56 (EX X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27. % 7.61/7.56 ((((((((((((((((((((((((((((((bnd_of X15 X17 X16 & % 7.61/7.56 bnd_man X15 X16) & % 7.61/7.56 bnd_jules_forename X15 X17) & % 7.61/7.56 bnd_forename X15 X17) & % 7.61/7.56 bnd_wheel X15 X18) & % 7.61/7.56 bnd_frontseat X15 X19) & % 7.61/7.56 bnd_chevy X15 X20) & % 7.61/7.56 bnd_white X15 X20) & % 7.61/7.56 bnd_dirty X15 X20) & % 7.61/7.56 bnd_old X15 X20) & % 7.61/7.56 bnd_of X15 X21 X22) & % 7.61/7.56 bnd_city X15 X22) & % 7.61/7.56 bnd_hollywood_placename X15 X21) & % 7.61/7.56 bnd_placename X15 X21) & % 7.61/7.56 bnd_street X15 X22) & % 7.61/7.56 bnd_lonely X15 X22) & % 7.61/7.56 bnd_event X15 X23) & % 7.61/7.56 bnd_agent X15 X23 X20) & % 7.61/7.56 bnd_present X15 X23) & % 7.61/7.56 bnd_barrel X15 X23) & % 7.61/7.56 bnd_down X15 X23 X22) & % 7.61/7.56 bnd_in X15 X23 X22) & % 7.61/7.56 (ALL X28. % 7.61/7.56 bnd_member X15 X28 X24 --> % 7.61/7.56 (EX X29 X30. % 7.61/7.56 (bnd_state X15 X29 & % 7.61/7.56 bnd_be X15 X29 X28 X30) & % 7.61/7.56 bnd_in X15 X30 X19))) & % 7.61/7.56 bnd_two X15 X24) & % 7.61/7.56 bnd_group X15 X24) & % 7.61/7.56 (ALL X31. % 7.61/7.56 bnd_member X15 X31 X24 --> % 7.61/7.56 bnd_fellow X15 X31 & bnd_young X15 X31)) & % 7.61/7.56 (ALL X32. % 7.61/7.56 bnd_member X15 X32 X25 --> % 7.61/7.56 (ALL X33. % 7.61/7.56 bnd_member X15 X33 X24 --> % 7.61/7.56 (EX X34. % 7.61/7.56 ((((bnd_event X15 X34 & % 7.61/7.56 bnd_agent X15 X34 X33) & % 7.61/7.56 bnd_patient X15 X34 X32) & % 7.61/7.56 bnd_present X15 X34) & % 7.61/7.56 bnd_nonreflexive X15 X34) & % 7.61/7.56 bnd_wear X15 X34)))) & % 7.61/7.56 bnd_group X15 X25) & % 7.61/7.56 (ALL X35. % 7.61/7.56 bnd_member X15 X35 X25 --> % 7.61/7.56 (bnd_coat X15 X35 & bnd_black X15 X35) & % 7.61/7.56 bnd_cheap X15 X35)) & % 7.61/7.56 bnd_state X15 X26) & % 7.61/7.56 bnd_be X15 X26 X16 X27) & % 7.61/7.56 bnd_behind X15 X27 X18))) & % 7.61/7.56 ((EX X15. % 7.61/7.56 bnd_actual_world X15 & % 7.61/7.56 (EX X16 X17 X18 X19 X20 X21 X22 X23 X24 X25 X26 X27. % 7.61/7.56 ((((((((((((((((((((((((((((((bnd_of X15 X17 X16 & % 7.61/7.56 bnd_man X15 X16) & % 7.61/7.56 bnd_jules_forename X15 X17) & % 7.61/7.56 bnd_forename X15 X17) & % 7.61/7.56 bnd_wheel X15 X18) & % 7.61/7.56 bnd_frontseat X15 X19) & % 7.61/7.56 bnd_chevy X15 X20) & % 7.61/7.56 bnd_white X15 X20) & % 7.61/7.56 bnd_dirty X15 X20) & % 7.61/7.56 bnd_old X15 X20) & % 7.61/7.56 bnd_of X15 X21 X22) & % 7.61/7.56 bnd_city X15 X22) & % 7.61/7.56 bnd_hollywood_placename X15 X21) & % 7.61/7.56 bnd_placename X15 X21) & % 7.61/7.56 bnd_street X15 X22) & % 7.61/7.56 bnd_lonely X15 X22) & % 7.61/7.56 bnd_event X15 X23) & % 7.61/7.56 bnd_agent X15 X23 X20) & % 7.61/7.56 bnd_present X15 X23) & % 7.61/7.56 bnd_barrel X15 X23) & % 7.61/7.56 bnd_down X15 X23 X22) & % 7.61/7.56 bnd_in X15 X23 X22) & % 7.61/7.56 (ALL X28. % 7.61/7.56 bnd_member X15 X28 X24 --> % 7.61/7.56 (EX X29 X30. % 7.61/7.56 (bnd_state X15 X29 & % 7.61/7.56 bnd_be X15 X29 X28 X30) & % 7.61/7.56 bnd_in X15 X30 X19))) & % 7.61/7.56 bnd_two X15 X24) & % 7.61/7.56 bnd_group X15 X24) & % 7.61/7.56 (ALL X31. % 7.61/7.56 bnd_member X15 X31 X24 --> % 7.61/7.56 bnd_fellow X15 X31 & bnd_young X15 X31)) & % 7.61/7.56 (ALL X32. % 7.61/7.56 bnd_member X15 X32 X25 --> % 7.61/7.56 (ALL X33. % 7.61/7.56 bnd_member X15 X33 X24 --> % 7.61/7.56 (EX X34. % 7.61/7.56 ((((bnd_event X15 X34 & % 7.61/7.56 bnd_agent X15 X34 X33) & % 7.61/7.56 bnd_patient X15 X34 X32) & % 7.61/7.56 bnd_present X15 X34) & % 7.61/7.56 bnd_nonreflexive X15 X34) & % 7.61/7.56 bnd_wear X15 X34)))) & % 7.61/7.56 bnd_group X15 X25) & % 7.61/7.56 (ALL X35. % 7.61/7.56 bnd_member X15 X35 X25 --> % 7.61/7.56 (bnd_coat X15 X35 & bnd_black X15 X35) & % 7.61/7.56 bnd_cheap X15 X35)) & % 7.61/7.56 bnd_state X15 X26) & % 7.61/7.56 bnd_be X15 X26 X16 X27) & % 7.61/7.56 bnd_behind X15 X27 X18)) --> % 7.61/7.56 (EX U. bnd_actual_world U & % 7.61/7.56 (EX V W X Y Z X1 X2 X3 X4 X5 X6. % 7.61/7.56 ((((((((((((((((((((((((((((((bnd_of U W V & bnd_man U V) & % 7.61/7.56 bnd_jules_forename U W) & % 7.61/7.56 bnd_forename U W) & % 7.61/7.56 bnd_frontseat U X) & % 7.61/7.56 bnd_chevy U Y) & % 7.61/7.56 bnd_white U Y) & % 7.61/7.56 bnd_dirty U Y) & % 7.61/7.56 bnd_old U Y) & % 7.61/7.56 bnd_of U Z X1) & % 7.61/7.56 bnd_city U X1) & % 7.61/7.56 bnd_hollywood_placename U Z) & % 7.61/7.56 bnd_placename U Z) & % 7.61/7.56 bnd_street U X1) & % 7.61/7.56 bnd_lonely U X1) & % 7.61/7.56 bnd_event U X2) & % 7.61/7.56 bnd_agent U X2 Y) & % 7.61/7.56 bnd_present U X2) & % 7.61/7.56 bnd_barrel U X2) & % 7.61/7.56 bnd_down U X2 X1) & % 7.61/7.56 bnd_in U X2 X1) & % 7.61/7.56 (ALL X7. % 7.61/7.56 bnd_member U X7 X3 --> % 7.61/7.56 (EX X8 X9. % 7.61/7.56 (bnd_state U X8 & bnd_be U X8 X7 X9) & % 7.61/7.56 bnd_in U X9 X))) & % 7.61/7.56 bnd_two U X3) & % 7.61/7.56 bnd_group U X3) & % 7.61/7.56 (ALL X10. % 7.61/7.56 bnd_member U X10 X3 --> % 7.61/7.56 bnd_fellow U X10 & bnd_young U X10)) & % 7.61/7.56 (ALL X11. % 7.61/7.56 bnd_member U X11 X4 --> % 7.61/7.56 (ALL X12. % 7.61/7.56 bnd_member U X12 X3 --> % 7.61/7.56 (EX X13. % 7.61/7.56 ((((bnd_event U X13 & % 7.61/7.56 bnd_agent U X13 X12) & % 7.61/7.56 bnd_patient U X13 X11) & % 7.61/7.56 bnd_present U X13) & % 7.61/7.56 bnd_nonreflexive U X13) & % 7.61/7.56 bnd_wear U X13)))) & % 7.61/7.56 bnd_group U X4) & % 7.61/7.56 (ALL X14. % 7.61/7.56 bnd_member U X14 X4 --> % 7.61/7.56 (bnd_coat U X14 & bnd_black U X14) & % 7.61/7.56 bnd_cheap U X14)) & % 7.61/7.56 bnd_wheel U X6) & % 7.61/7.56 bnd_state U X5) & % 7.61/7.56 bnd_be U X5 V X6) & % 7.61/7.56 bnd_behind U X6 X6)))) % 7.61/7.56 Adding axioms... % 7.61/7.57 Typedef.type_definition_def % 13.52/13.46 ...done. % 13.52/13.47 Ground types: ?'b, TPTP_Interpret.ind % 13.52/13.47 Translating term (sizes: 1, 1) ... % 17.64/17.52 Invoking SAT solver... % 17.64/17.52 No model exists. % 17.64/17.52 Translating term (sizes: 2, 1) ... % 22.34/22.24 Invoking SAT solver... % 22.34/22.24 No model exists. % 22.34/22.24 Translating term (sizes: 1, 2) ... %------------------------------------------------------------------------------