The bear chases the cat. The bear chases the mouse. The bear likes the cat. The bear likes the mouse. The bear needs the cat. The cat is red. The cat is rough. The cat likes the bear. The cat likes the mouse. The cat needs the bear. The cat needs the mouse. The mouse needs the cat. If something is kind then it chases the cat. If something needs the mouse then it likes the mouse. Red things are kind. If something chases the mouse and the mouse chases the cat then the cat needs the mouse. If something likes the bear then it needs the bear. If the mouse is red and the mouse chases the cat then the mouse likes the cat. If something chases the mouse and the mouse is blue then the mouse needs the cat. If the mouse needs the cat then the mouse needs the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the mouse.
("bear" "chases" "mouse" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If something is kind then it chases the cat.
((("something" "is" "kind" "+")) -> ("something" "chases" "cat" "+"))
If something needs the mouse then it likes the mouse.
((("something" "needs" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If something chases the mouse and the mouse chases the cat then the cat needs the mouse.
((("something" "chases" "mouse" "+") ("mouse" "chases" "cat" "+")) -> ("cat" "needs" "mouse" "+"))
If something likes the bear then it needs the bear.
((("something" "likes" "bear" "+")) -> ("something" "needs" "bear" "+"))
If the mouse is red and the mouse chases the cat then the mouse likes the cat.
((("mouse" "is" "red" "+") ("mouse" "chases" "cat" "+")) -> ("mouse" "likes" "cat" "+"))
If something chases the mouse and the mouse is blue then the mouse needs the cat.
((("something" "chases" "mouse" "+") ("mouse" "is" "blue" "+")) -> ("mouse" "needs" "cat" "+"))
If the mouse needs the cat then the mouse needs the bear.
((("mouse" "needs" "cat" "+")) -> ("mouse" "needs" "bear" "+"))
The cat is rough.
True
1
proof
[(triple7)]
("cat" "is" "rough" "+")
triple7
The mouse does not need the cat.
False
1
inv-proof
[(triple12)]
("mouse" "needs" "cat" "-")
triple12
The cat is kind.
True
2
proof
[(((triple6) -> rule3))]
("cat" "is" "kind" "+")
((triple6) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple6) -> rule3))]
("cat" "is" "kind" "-")
((triple6) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse does not like the cat.
Unknown
inv-rconc
[@1: The mouse likes the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "cat" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "kind" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the mouse.[(triple2)] The bear likes the cat.[(triple3)] The bear likes the mouse.[(triple4)] The bear needs the cat.[(triple5)] The cat is red.[(triple6)] The cat is rough.[(triple7)] The cat likes the bear.[(triple8)] The cat likes the mouse.[(triple9 OR ((triple11) -> rule2))] The cat needs the bear.[(triple10 OR ((triple8) -> rule5))] The cat needs the mouse.[(triple11)] The mouse needs the cat.[(triple12)] @1: The cat is kind.[(((triple6) -> rule3))] The mouse needs the bear.[(((triple12) -> rule8))] @2: The cat chases the cat.[(((((triple6) -> rule3)) -> rule1))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the mouse.
("bear" "chases" "mouse" "+")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple3
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple4
The bear needs the cat.
("bear" "needs" "cat" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
The cat is rough.
("cat" "is" "rough" "+")
triple7
The cat likes the bear.
("cat" "likes" "bear" "+")
triple8
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple9
((triple11) -> (rule2 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
triple10
((triple8) -> (rule5 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple11
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple12
The cat is kind.
("cat" "is" "kind" "+")
((triple6) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple12) -> (rule8 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple6) -> (rule3 % int2))) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2