The cat is red. The cow is cold. The mouse sees the cow. If something sees the cat then it needs the cat. If the cat is rough and the cat is round then the cat needs the mouse.
The cat is red.
("cat" "is" "red" "+")
The cow is cold.
("cow" "is" "cold" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something sees the cat then it needs the cat.
((("something" "sees" "cat" "+")) -> ("something" "needs" "cat" "+"))
If the cat is rough and the cat is round then the cat needs the mouse.
((("cat" "is" "rough" "+") ("cat" "is" "round" "+")) -> ("cat" "needs" "mouse" "+"))
The mouse sees the cow.
True
1
proof
[(triple3)]
("mouse" "sees" "cow" "+")
triple3
The cow is not cold.
False
1
inv-proof
[(triple2)]
("cow" "is" "cold" "-")
triple2
The cat does not need the mouse.
Unknown
inv-rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "mouse" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cat is red.[(triple1)] The cow is cold.[(triple2)] The mouse sees the cow.[(triple3)]
The cat is red.
("cat" "is" "red" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple3