The cat likes the mouse. The mouse eats the cat. If someone eats the cat and the cat likes the mouse then they eat the mouse. If someone eats the mouse then they like the cat. If someone likes the cat and the cat sees the mouse then they like the mouse. If someone likes the mouse and the mouse is green then they see the mouse. If someone is young then they eat the cat. If someone likes the mouse then they eat the cat. If the cat sees the mouse then the cat eats the mouse. If someone is cold then they like the mouse.
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
If someone eats the cat and the cat likes the mouse then they eat the mouse.
((("someone" "eats" "cat" "+") ("cat" "likes" "mouse" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the mouse then they like the cat.
((("someone" "eats" "mouse" "+")) -> ("someone" "likes" "cat" "+"))
If someone likes the cat and the cat sees the mouse then they like the mouse.
((("someone" "likes" "cat" "+") ("cat" "sees" "mouse" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse and the mouse is green then they see the mouse.
((("someone" "likes" "mouse" "+") ("mouse" "is" "green" "+")) -> ("someone" "sees" "mouse" "+"))
If someone is young then they eat the cat.
((("someone" "is" "young" "+")) -> ("someone" "eats" "cat" "+"))
If someone likes the mouse then they eat the cat.
((("someone" "likes" "mouse" "+")) -> ("someone" "eats" "cat" "+"))
If the cat sees the mouse then the cat eats the mouse.
((("cat" "sees" "mouse" "+")) -> ("cat" "eats" "mouse" "+"))
If someone is cold then they like the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "mouse" "+"))
The mouse eats the cat.
True
1
proof
[(triple2)]
("mouse" "eats" "cat" "+")
triple2
The mouse does not eat the cat.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "cat" "-")
triple2
The cat eats the cat.
True
2
proof
[(((triple1) -> rule6))]
("cat" "eats" "cat" "+")
((triple1) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not eat the cat.
False
2
inv-proof
[(((triple1) -> rule6))]
("cat" "eats" "cat" "-")
((triple1) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The mouse likes the cat.
True
4
proof
[(((((triple2 triple1) -> rule1)) -> rule2))]
("mouse" "likes" "cat" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse does not like the cat.
False
4
inv-proof
[(((((triple2 triple1) -> rule1)) -> rule2))]
("mouse" "likes" "cat" "-")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat likes the cat.
True
5
proof
[(((((((triple1) -> rule6) triple1) -> rule1)) -> rule2))]
("cat" "likes" "cat" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat does not like the cat.
False
5
inv-proof
[(((((((triple1) -> rule6) triple1) -> rule1)) -> rule2))]
("cat" "likes" "cat" "-")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The mouse does not like the mouse.
Unknown
inv-rconc
[@2: The mouse likes the mouse.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The cat sees the mouse.
Unknown
rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The cat likes the mouse.[(triple1)] The mouse eats the cat.[(triple2)] @1: The cat eats the cat.[(((triple1) -> rule6))] The mouse eats the mouse.[(((triple2 triple1) -> rule1))] @2: The cat eats the mouse.[(((((triple1) -> rule6) triple1) -> rule1))] The mouse likes the cat.[(((((triple2 triple1) -> rule1)) -> rule2))] @3: The cat likes the cat.[(((((((triple1) -> rule6) triple1) -> rule1)) -> rule2))]
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple2
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple1) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple2 triple1) -> (rule1 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule1 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((((triple2 triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3