The cat likes the mouse. The mouse is blue. If someone likes the mouse and the mouse likes the cat then the cat chases the mouse. If someone needs the cat then the cat is blue. If someone needs the cat then they need the mouse. Kind people are blue. If someone likes the mouse then they need the cat. If the cat likes the mouse and the cat needs the mouse then the mouse is nice.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
If someone likes the mouse and the mouse likes the cat then the cat chases the mouse.
((("someone" "likes" "mouse" "+") ("mouse" "likes" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If someone needs the cat then the cat is blue.
((("someone" "needs" "cat" "+")) -> ("cat" "is" "blue" "+"))
If someone needs the cat then they need the mouse.
((("someone" "needs" "cat" "+")) -> ("someone" "needs" "mouse" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone likes the mouse then they need the cat.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "cat" "+"))
If the cat likes the mouse and the cat needs the mouse then the mouse is nice.
((("cat" "likes" "mouse" "+") ("cat" "needs" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
The cat likes the mouse.
True
1
proof
[(triple1)]
("cat" "likes" "mouse" "+")
triple1
The mouse is not blue.
False
1
inv-proof
[(triple2)]
("mouse" "is" "blue" "-")
triple2
The cat needs the cat.
True
2
proof
[(((triple1) -> rule5))]
("cat" "needs" "cat" "+")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "needs" "cat" "-")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is blue.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("cat" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat does not need the mouse.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("cat" "needs" "mouse" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The mouse is nice.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule6))]
("mouse" "is" "nice" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The mouse is not nice.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule6))]
("mouse" "is" "nice" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3
The mouse does not need the cat.
Unknown
inv-rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "needs" "cat" "-")
The cat chases the mouse.
Unknown
rconc
[@1: The cat chases the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
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 cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat likes the mouse.[(triple1)] The mouse is blue.[(triple2)] @1: The cat needs the cat.[(((triple1) -> rule5))] @2: The cat is blue.[(((((triple1) -> rule5)) -> rule2))] The cat needs the mouse.[(((((triple1) -> rule5)) -> rule3))] @3: The mouse is nice.[(((triple1 ((((triple1) -> rule5)) -> rule3)) -> rule6))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple1) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
int3