The cat visits the mouse. The mouse chases the cat. If something visits the mouse and the mouse likes the cat then the cat is blue. If something chases the cat then it likes the cat. If something visits the mouse then it is big.
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
If something visits the mouse and the mouse likes the cat then the cat is blue.
((("something" "visits" "mouse" "+") ("mouse" "likes" "cat" "+")) -> ("cat" "is" "blue" "+"))
If something chases the cat then it likes the cat.
((("something" "chases" "cat" "+")) -> ("something" "likes" "cat" "+"))
If something visits the mouse then it is big.
((("something" "visits" "mouse" "+")) -> ("something" "is" "big" "+"))
The cat visits the mouse.
True
1
proof
[(triple1)]
("cat" "visits" "mouse" "+")
triple1
The mouse does not chase the cat.
False
1
inv-proof
[(triple2)]
("mouse" "chases" "cat" "-")
triple2
The mouse likes the cat.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "is" "big" "-")
((triple1) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
True
4
proof
[(((triple1 ((triple2) -> rule2)) -> rule1))]
("cat" "is" "blue" "+")
((triple1 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The cat is not blue.
False
4
inv-proof
[(((triple1 ((triple2) -> rule2)) -> rule1))]
("cat" "is" "blue" "-")
((triple1 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "big" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "cat" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat visits the mouse.[(triple1)] The mouse chases the cat.[(triple2)] @1: The cat is big.[(((triple1) -> rule3))] The mouse likes the cat.[(((triple2) -> rule2))] @2: The cat is blue.[(((triple1 ((triple2) -> rule2)) -> rule1))]
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
((triple1) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple2) -> (rule2 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple1 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int2