The cow sees the tiger. The rabbit sees the cow. The tiger eats the rabbit. If the cow sees the rabbit then the cow is kind.
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If the cow sees the rabbit then the cow is kind.
((("cow" "sees" "rabbit" "+")) -> ("cow" "is" "kind" "+"))
The rabbit sees the cow.
True
1
proof
[(triple2)]
("rabbit" "sees" "cow" "+")
triple2
The cow does not see the tiger.
False
1
inv-proof
[(triple1)]
("cow" "sees" "tiger" "-")
triple1
The cow is not kind.
Unknown
inv-rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "kind" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The cow sees the tiger.[(triple1)] The rabbit sees the cow.[(triple2)] The tiger eats the rabbit.[(triple3)]
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple3