2010-01-21T12:06:44-05:00 greater(low,very_low) cnf(19,axiom, ( greater(low,very_low) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#19 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 $false cnf(139,plain, ( $false ), inference('backward demodulation, forward subsumption resolution',[status(thm)],[19,138,76])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#139 TPTP Formula 0 Inference rule: backward demodulation, forward subsumption resolution Unknown 2010-01-21T12:06:44-05:00 ~ greater(hazard_of_mortality(sk1,sk3),very_low) cnf(76,plain, ( ~ greater(hazard_of_mortality(sk1,sk3),very_low) ), inference('backward demodulation',[status(thm)],[75,25])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#76 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) cnf(25,negated_conjecture, ( ~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#25 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 hazard_of_mortality(sk1,sk2) = very_low cnf(75,plain, ( hazard_of_mortality(sk1,sk2) = very_low ), inference(resolution,[status(thm)],[51,23])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#75 TPTP Formula 0 2010-01-21T12:06:44-05:00 has_immunity(sk1,sk2) cnf(23,negated_conjecture, ( has_immunity(sk1,sk2) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#23 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 ~ has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = very_low cnf(51,plain, ( ~ has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = very_low ), inference('literal permutation',[status(thm)],[39])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#51 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ has_immunity(sk1,X0) | very_low = hazard_of_mortality(sk1,X0) cnf(39,plain, ( ~ has_immunity(sk1,X0) | very_low = hazard_of_mortality(sk1,X0) ), inference(resolution,[status(thm)],[22,31])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#39 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | ~ has_immunity(X0,X1) | very_low = hazard_of_mortality(X0,X1) cnf(31,plain, ( ~ organization(X0) | ~ has_immunity(X0,X1) | very_low = hazard_of_mortality(X0,X1) ), inference(normalize,[status(thm)],[12])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#31 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | ~ has_immunity(X0,X1) | hazard_of_mortality(X0,X1) = very_low cnf(12,axiom, ( ~ organization(X0) | ~ has_immunity(X0,X1) | hazard_of_mortality(X0,X1) = very_low ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#12 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 organization(sk1) cnf(22,negated_conjecture, ( organization(sk1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#22 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 hazard_of_mortality(sk1,sk3) = low cnf(138,plain, ( hazard_of_mortality(sk1,sk3) = low ), inference('backward superposition, forward subsumption resolution',[status(thm)],[114,76,137])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#138 TPTP Formula 0 Inference rule: backward superposition, forward subsumption resolution Inference rule: backward superposition, forward subsumption resolution Inference rule: backward superposition, forward subsumption resolution Unknown 2010-01-21T12:06:44-05:00 hazard_of_mortality(sk1,sk3) = mod1 | hazard_of_mortality(sk1,sk3) = low cnf(137,plain, ( hazard_of_mortality(sk1,sk3) = mod1 | hazard_of_mortality(sk1,sk3) = low ), inference('backward superposition, forward subsumption resolution',[status(thm)],[115,76,136])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#137 TPTP Formula 0 2010-01-21T12:06:44-05:00 hazard_of_mortality(sk1,sk3) = mod2 | hazard_of_mortality(sk1,sk3) = mod1 | hazard_of_mortality(sk1,sk3) = low cnf(136,plain, ( hazard_of_mortality(sk1,sk3) = mod2 | hazard_of_mortality(sk1,sk3) = mod1 | hazard_of_mortality(sk1,sk3) = low ), inference('backward superposition, forward subsumption resolution',[status(thm)],[113,76,135])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#136 TPTP Formula 0 2010-01-21T12:06:44-05:00 hazard_of_mortality(sk1,sk3) = high | hazard_of_mortality(sk1,sk3) = mod2 | hazard_of_mortality(sk1,sk3) = mod1 | hazard_of_mortality(sk1,sk3) = low cnf(135,plain, ( hazard_of_mortality(sk1,sk3) = high | hazard_of_mortality(sk1,sk3) = mod2 | hazard_of_mortality(sk1,sk3) = mod1 | hazard_of_mortality(sk1,sk3) = low ), inference(resolution,[status(thm)],[24,133])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#135 TPTP Formula 0 2010-01-21T12:06:44-05:00 has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod2 | hazard_of_mortality(sk1,X1) = mod1 | hazard_of_mortality(sk1,X1) = low cnf(133,plain, ( has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod2 | hazard_of_mortality(sk1,X1) = mod1 | hazard_of_mortality(sk1,X1) = low ), inference(resolution,[status(thm)],[105,106])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#133 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ positional_advantage(sk1,X1) | has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod1 | hazard_of_mortality(sk1,X1) = low cnf(106,plain, ( ~ positional_advantage(sk1,X1) | has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod1 | hazard_of_mortality(sk1,X1) = low ), inference(resolution,[status(thm)],[48,74])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#106 TPTP Formula 0 2010-01-21T12:06:44-05:00 is_aligned(sk1,X1) | has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod1 cnf(74,plain, ( is_aligned(sk1,X1) | has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod1 ), inference(resolution,[status(thm)],[49,52])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#74 TPTP Formula 0 2010-01-21T12:06:44-05:00 positional_advantage(sk1,X1) | has_immunity(sk1,X1) | is_aligned(sk1,X1) | hazard_of_mortality(sk1,X1) = high cnf(52,plain, ( positional_advantage(sk1,X1) | has_immunity(sk1,X1) | is_aligned(sk1,X1) | hazard_of_mortality(sk1,X1) = high ), inference('literal permutation',[status(thm)],[40])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#52 TPTP Formula 0 2010-01-21T12:06:44-05:00 high = hazard_of_mortality(sk1,X0) | positional_advantage(sk1,X0) | is_aligned(sk1,X0) | has_immunity(sk1,X0) cnf(40,plain, ( high = hazard_of_mortality(sk1,X0) | positional_advantage(sk1,X0) | is_aligned(sk1,X0) | has_immunity(sk1,X0) ), inference(resolution,[status(thm)],[22,35])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#40 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | high = hazard_of_mortality(X0,X1) | positional_advantage(X0,X1) | is_aligned(X0,X1) | has_immunity(X0,X1) cnf(35,plain, ( ~ organization(X0) | high = hazard_of_mortality(X0,X1) | positional_advantage(X0,X1) | is_aligned(X0,X1) | has_immunity(X0,X1) ), inference(normalize,[status(thm)],[16])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#35 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | has_immunity(X0,X1) | is_aligned(X0,X1) | positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = high cnf(16,axiom, ( ~ organization(X0) | has_immunity(X0,X1) | is_aligned(X0,X1) | positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = high ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#16 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 ~ positional_advantage(sk1,X1) | has_immunity(sk1,X1) | is_aligned(sk1,X1) | hazard_of_mortality(sk1,X1) = mod1 cnf(49,plain, ( ~ positional_advantage(sk1,X1) | has_immunity(sk1,X1) | is_aligned(sk1,X1) | hazard_of_mortality(sk1,X1) = mod1 ), inference('literal permutation',[status(thm)],[37])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#49 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ positional_advantage(sk1,X0) | mod1 = hazard_of_mortality(sk1,X0) | is_aligned(sk1,X0) | has_immunity(sk1,X0) cnf(37,plain, ( ~ positional_advantage(sk1,X0) | mod1 = hazard_of_mortality(sk1,X0) | is_aligned(sk1,X0) | has_immunity(sk1,X0) ), inference(resolution,[status(thm)],[22,33])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#37 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | ~ positional_advantage(X0,X1) | mod1 = hazard_of_mortality(X0,X1) | is_aligned(X0,X1) | has_immunity(X0,X1) cnf(33,plain, ( ~ organization(X0) | ~ positional_advantage(X0,X1) | mod1 = hazard_of_mortality(X0,X1) | is_aligned(X0,X1) | has_immunity(X0,X1) ), inference(normalize,[status(thm)],[14])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#33 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | has_immunity(X0,X1) | is_aligned(X0,X1) | ~ positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = mod1 cnf(14,axiom, ( ~ organization(X0) | has_immunity(X0,X1) | is_aligned(X0,X1) | ~ positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = mod1 ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#14 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 ~ is_aligned(sk1,X1) | has_immunity(sk1,X1) | ~ positional_advantage(sk1,X1) | hazard_of_mortality(sk1,X1) = low cnf(48,plain, ( ~ is_aligned(sk1,X1) | has_immunity(sk1,X1) | ~ positional_advantage(sk1,X1) | hazard_of_mortality(sk1,X1) = low ), inference('literal permutation',[status(thm)],[36])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#48 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ is_aligned(sk1,X0) | ~ positional_advantage(sk1,X0) | low = hazard_of_mortality(sk1,X0) | has_immunity(sk1,X0) cnf(36,plain, ( ~ is_aligned(sk1,X0) | ~ positional_advantage(sk1,X0) | low = hazard_of_mortality(sk1,X0) | has_immunity(sk1,X0) ), inference(resolution,[status(thm)],[22,32])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#36 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | ~ is_aligned(X0,X1) | ~ positional_advantage(X0,X1) | low = hazard_of_mortality(X0,X1) | has_immunity(X0,X1) cnf(32,plain, ( ~ organization(X0) | ~ is_aligned(X0,X1) | ~ positional_advantage(X0,X1) | low = hazard_of_mortality(X0,X1) | has_immunity(X0,X1) ), inference(normalize,[status(thm)],[13])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#32 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | has_immunity(X0,X1) | ~ is_aligned(X0,X1) | ~ positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = low cnf(13,axiom, ( ~ organization(X0) | has_immunity(X0,X1) | ~ is_aligned(X0,X1) | ~ positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = low ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#13 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 positional_advantage(sk1,X1) | has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod2 | hazard_of_mortality(sk1,X1) = mod1 cnf(105,plain, ( positional_advantage(sk1,X1) | has_immunity(sk1,X1) | hazard_of_mortality(sk1,X1) = high | hazard_of_mortality(sk1,X1) = mod2 | hazard_of_mortality(sk1,X1) = mod1 ), inference(resolution,[status(thm)],[50,74])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#105 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ is_aligned(sk1,X1) | has_immunity(sk1,X1) | positional_advantage(sk1,X1) | hazard_of_mortality(sk1,X1) = mod2 cnf(50,plain, ( ~ is_aligned(sk1,X1) | has_immunity(sk1,X1) | positional_advantage(sk1,X1) | hazard_of_mortality(sk1,X1) = mod2 ), inference('literal permutation',[status(thm)],[38])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#50 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ is_aligned(sk1,X0) | mod2 = hazard_of_mortality(sk1,X0) | positional_advantage(sk1,X0) | has_immunity(sk1,X0) cnf(38,plain, ( ~ is_aligned(sk1,X0) | mod2 = hazard_of_mortality(sk1,X0) | positional_advantage(sk1,X0) | has_immunity(sk1,X0) ), inference(resolution,[status(thm)],[22,34])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#38 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | ~ is_aligned(X0,X1) | mod2 = hazard_of_mortality(X0,X1) | positional_advantage(X0,X1) | has_immunity(X0,X1) cnf(34,plain, ( ~ organization(X0) | ~ is_aligned(X0,X1) | mod2 = hazard_of_mortality(X0,X1) | positional_advantage(X0,X1) | has_immunity(X0,X1) ), inference(normalize,[status(thm)],[15])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#34 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ organization(X0) | has_immunity(X0,X1) | ~ is_aligned(X0,X1) | positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = mod2 cnf(15,axiom, ( ~ organization(X0) | has_immunity(X0,X1) | ~ is_aligned(X0,X1) | positional_advantage(X0,X1) | hazard_of_mortality(X0,X1) = mod2 ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#15 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 ~ has_immunity(sk1,sk3) cnf(24,negated_conjecture, ( ~ has_immunity(sk1,sk3) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#24 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 greater(high,very_low) cnf(113,plain, ( greater(high,very_low) ), inference(resolution,[status(thm)],[107,95])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#113 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ greater(X1,low) | greater(X1,very_low) cnf(95,plain, ( ~ greater(X1,low) | greater(X1,very_low) ), inference(resolution,[status(thm)],[29,19])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#95 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ greater(X1,X2) | ~ greater(X0,X1) | greater(X0,X2) cnf(29,plain, ( ~ greater(X1,X2) | ~ greater(X0,X1) | greater(X0,X2) ), inference(normalize,[status(thm)],[10])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#29 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ greater(X0,X1) | ~ greater(X1,X2) | greater(X0,X2) cnf(10,axiom, ( ~ greater(X0,X1) | ~ greater(X1,X2) | greater(X0,X2) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#10 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 greater(high,low) cnf(107,plain, ( greater(high,low) ), inference(resolution,[status(thm)],[17,87])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#107 TPTP Formula 0 2010-01-21T12:06:44-05:00 ~ greater(X1,mod1) | greater(X1,low) cnf(87,plain, ( ~ greater(X1,mod1) | greater(X1,low) ), inference(resolution,[status(thm)],[29,18])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#87 TPTP Formula 0 2010-01-21T12:06:44-05:00 greater(mod1,low) cnf(18,axiom, ( greater(mod1,low) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#18 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 greater(high,mod1) cnf(17,axiom, ( greater(high,mod1) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#17 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 greater(mod2,very_low) cnf(115,plain, ( greater(mod2,very_low) ), inference(resolution,[status(thm)],[21,95])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#115 TPTP Formula 0 2010-01-21T12:06:44-05:00 greater(mod2,low) cnf(21,axiom, ( greater(mod2,low) ), file(input,unknown)). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#21 TPTP Formula 0 2010-01-21T12:06:44-05:00 file://input unknown 2010-01-21T12:06:44-05:00 greater(mod1,very_low) cnf(114,plain, ( greater(mod1,very_low) ), inference(resolution,[status(thm)],[18,95])). http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Solutions&Domain=MGT&File=MGT060-1&System=Vampire---11.0.UNS-Ref.s#114 TPTP Formula 0