The cat is green. The cat is kind. The cat is nice. The cat needs the mouse. The cat sees the mouse. The cat sees the tiger. The mouse needs the cat. The mouse sees the cat. The mouse sees the tiger. The tiger sees the mouse. If something eats the mouse and the mouse sees the tiger then it is red. If something is kind and it eats the cat then it sees the mouse.
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something eats the mouse and the mouse sees the tiger then it is red.
((("something" "eats" "mouse" "+") ("mouse" "sees" "tiger" "+")) -> ("something" "is" "red" "+"))
If something is kind and it eats the cat then it sees the mouse.
((("something" "is" "kind" "+") ("something" "eats" "cat" "+")) -> ("something" "sees" "mouse" "+"))
The cat is kind.
True
1
proof
[(triple2)]
("cat" "is" "kind" "+")
triple2
The cat does not see the tiger.
False
1
inv-proof
[(triple6)]
("cat" "sees" "tiger" "-")
triple6
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is green.[(triple1)] The cat is kind.[(triple2)] The cat is nice.[(triple3)] The cat needs the mouse.[(triple4)] The cat sees the mouse.[(triple5)] The cat sees the tiger.[(triple6)] The mouse needs the cat.[(triple7)] The mouse sees the cat.[(triple8)] The mouse sees the tiger.[(triple9)] The tiger sees the mouse.[(triple10)]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple6
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple7
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple8
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple9
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple10