The cow is red. The lion needs the cow. The mouse eats the cow. If something needs the cow and the cow likes the lion then the lion likes the cow. If something likes the lion and the lion is round then it needs the cow. If something is nice then it eats the cow. If something likes the cow then it is cold. If something is round and it likes the mouse then the mouse likes the cow. If something is cold then it needs the lion. If something needs the lion and it likes the cow then the cow likes the mouse. If something needs the cow then the cow eats the mouse.
The cow is red.
("cow" "is" "red" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
If something needs the cow and the cow likes the lion then the lion likes the cow.
((("something" "needs" "cow" "+") ("cow" "likes" "lion" "+")) -> ("lion" "likes" "cow" "+"))
If something likes the lion and the lion is round then it needs the cow.
((("something" "likes" "lion" "+") ("lion" "is" "round" "+")) -> ("something" "needs" "cow" "+"))
If something is nice then it eats the cow.
((("something" "is" "nice" "+")) -> ("something" "eats" "cow" "+"))
If something likes the cow then it is cold.
((("something" "likes" "cow" "+")) -> ("something" "is" "cold" "+"))
If something is round and it likes the mouse then the mouse likes the cow.
((("something" "is" "round" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "likes" "cow" "+"))
If something is cold then it needs the lion.
((("something" "is" "cold" "+")) -> ("something" "needs" "lion" "+"))
If something needs the lion and it likes the cow then the cow likes the mouse.
((("something" "needs" "lion" "+") ("something" "likes" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
If something needs the cow then the cow eats the mouse.
((("something" "needs" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
The lion needs the cow.
True
1
proof
[(triple2)]
("lion" "needs" "cow" "+")
triple2
The mouse does not eat the cow.
False
1
inv-proof
[(triple3)]
("mouse" "eats" "cow" "-")
triple3
The cow eats the mouse.
True
2
proof
[(((triple2) -> rule8))]
("cow" "eats" "mouse" "+")
((triple2) -> (rule8 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow does not eat the mouse.
False
2
inv-proof
[(((triple2) -> rule8))]
("cow" "eats" "mouse" "-")
((triple2) -> (rule8 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "cow" "-")
The cow likes the mouse.
Unknown
rconc
[@2: The cow likes the mouse.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("cow" "likes" "mouse" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The cow eats the lion.
Unknown
random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "+")
@0: The cow is red.[(triple1)] The lion needs the cow.[(triple2)] The mouse eats the cow.[(triple3)] @1: The cow eats the mouse.[(((triple2) -> rule8))]
The cow is red.
("cow" "is" "red" "+")
triple1
The lion needs the cow.
("lion" "needs" "cow" "+")
triple2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple3
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((triple2) -> (rule8 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1