The cat is nice. The cat likes the mouse. The cat likes the squirrel. The cat needs the mouse. The cat needs the squirrel. The cat visits the mouse. The mouse is cold. The mouse is nice. The mouse likes the cat. The mouse likes the squirrel. The mouse needs the cat. The squirrel is blue. If something visits the cat then it visits the mouse. If something likes the squirrel and it likes the cat then the squirrel visits the cat. If the cat visits the squirrel and the squirrel visits the mouse then the cat is red.
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If something visits the cat then it visits the mouse.
((("something" "visits" "cat" "+")) -> ("something" "visits" "mouse" "+"))
If something likes the squirrel and it likes the cat then the squirrel visits the cat.
((("something" "likes" "squirrel" "+") ("something" "likes" "cat" "+")) -> ("squirrel" "visits" "cat" "+"))
If the cat visits the squirrel and the squirrel visits the mouse then the cat is red.
((("cat" "visits" "squirrel" "+") ("squirrel" "visits" "mouse" "+")) -> ("cat" "is" "red" "+"))
The cat needs the mouse.
True
1
proof
[(triple4)]
("cat" "needs" "mouse" "+")
triple4
The cat does not need the squirrel.
False
1
inv-proof
[(triple5)]
("cat" "needs" "squirrel" "-")
triple5
The squirrel visits the cat.
True
3
proof
[(((triple10 triple9) -> rule2))]
("squirrel" "visits" "cat" "+")
((triple10 triple9) -> (rule2 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel does not visit the cat.
False
3
inv-proof
[(((triple10 triple9) -> rule2))]
("squirrel" "visits" "cat" "-")
((triple10 triple9) -> (rule2 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel visits the mouse.
True
4
proof
[(((((triple10 triple9) -> rule2)) -> rule1))]
("squirrel" "visits" "mouse" "+")
((((triple10 triple9) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The squirrel does not visit the mouse.
False
4
inv-proof
[(((((triple10 triple9) -> rule2)) -> rule1))]
("squirrel" "visits" "mouse" "-")
((((triple10 triple9) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "red" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse needs the squirrel.
Unknown
random
[@0: The mouse needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "squirrel" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The cat is nice.[(triple1)] The cat likes the mouse.[(triple2)] The cat likes the squirrel.[(triple3)] The cat needs the mouse.[(triple4)] The cat needs the squirrel.[(triple5)] The cat visits the mouse.[(triple6)] The mouse is cold.[(triple7)] The mouse is nice.[(triple8)] The mouse likes the cat.[(triple9)] The mouse likes the squirrel.[(triple10)] The mouse needs the cat.[(triple11)] The squirrel is blue.[(triple12)] @1: The squirrel visits the cat.[(((triple10 triple9) -> rule2))] @2: The squirrel visits the mouse.[(((((triple10 triple9) -> rule2)) -> rule1))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple5
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple9
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple10
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple11
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple12
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple10 triple9) -> (rule2 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((((triple10 triple9) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2