The cow sees the mouse. The lion is kind. The mouse sees the lion. The rabbit eats the lion. If something is kind then it does not eat the rabbit. If something likes the lion and it is nice then it is not kind. If something sees the mouse then it is not kind.
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
If something is kind then it does not eat the rabbit.
((("something" "is" "kind" "+")) -> ("something" "eats" "rabbit" "-"))
If something likes the lion and it is nice then it is not kind.
((("something" "likes" "lion" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "-"))
If something sees the mouse then it is not kind.
((("something" "sees" "mouse" "+")) -> ("something" "is" "kind" "-"))
The rabbit eats the lion.
True
1
proof
[(triple4)]
("rabbit" "eats" "lion" "+")
triple4
The rabbit does not eat the lion.
False
1
inv-proof
[(triple4)]
("rabbit" "eats" "lion" "-")
triple4
The cow is not kind.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The lion eats the rabbit.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "eats" "rabbit" "+")
((triple2) -> (rule1 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1
The cow does not eat the mouse.
Unknown
inv-random
[@0: The cow eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "mouse" "-")
The cow likes the lion.
Unknown
random
[@0: The cow likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "lion" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The cow sees the mouse.[(triple1)] The lion is kind.[(triple2)] The mouse sees the lion.[(triple3)] The rabbit eats the lion.[(triple4)] @1: The cow is not kind.[(((triple1) -> rule3))] The lion does not eat the rabbit.[(((triple2) -> rule1))]
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple3
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple4
The cow is not kind.
("cow" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The cow is not kind.
("cow" "is" "kind" "-")
int1
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
((triple2) -> (rule1 % int1))
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
int1