The cat eats the mouse. The cat is big. The cat is kind. The cat visits the mouse. The mouse eats the cat. The mouse is not red. The mouse likes the cat. If someone likes the cat and they are not red then they eat the cat. If the mouse likes the cat and the cat does not eat the mouse then the mouse visits the cat. If someone likes the cat then the cat is nice. If someone is nice then they like the mouse. If someone is kind and they eat the cat then they like the cat. If the mouse likes the cat and the cat likes the mouse then the mouse is not kind.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is not red.
("mouse" "is" "red" "-")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If someone likes the cat and they are not red then they eat the cat.
((("someone" "likes" "cat" "+") ("someone" "is" "red" "~")) -> ("someone" "eats" "cat" "+"))
If the mouse likes the cat and the cat does not eat the mouse then the mouse visits the cat.
((("mouse" "likes" "cat" "+") ("cat" "eats" "mouse" "~")) -> ("mouse" "visits" "cat" "+"))
If someone likes the cat then the cat is nice.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "nice" "+"))
If someone is nice then they like the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is kind and they eat the cat then they like the cat.
((("someone" "is" "kind" "+") ("someone" "eats" "cat" "+")) -> ("someone" "likes" "cat" "+"))
If the mouse likes the cat and the cat likes the mouse then the mouse is not kind.
((("mouse" "likes" "cat" "+") ("cat" "likes" "mouse" "+")) -> ("mouse" "is" "kind" "-"))
The mouse likes the cat.
True
1
proof
[(triple7)]
("mouse" "likes" "cat" "+")
triple7
The cat is not kind.
False
1
inv-proof
[(triple3)]
("cat" "is" "kind" "-")
triple3
The cat is nice.
True
2
proof
[(((triple7) -> rule3))]
("cat" "is" "nice" "+")
((triple7) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is not nice.
False
2
inv-proof
[(((triple7) -> rule3))]
("cat" "is" "nice" "-")
((triple7) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the mouse.
True
3
proof
[(((((triple7) -> rule3)) -> rule4))]
("cat" "likes" "mouse" "+")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat does not like the mouse.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule4))]
("cat" "likes" "mouse" "-")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The mouse is not kind.
True
5
proof
[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule6))]
("mouse" "is" "kind" "-")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse is not kind.
("mouse" "is" "kind" "-")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The mouse is kind.
False
5
inv-proof
[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule6))]
("mouse" "is" "kind" "+")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse is not kind.
("mouse" "is" "kind" "-")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "-")
The mouse visits the cat.
Unknown
rconc
[@1: The mouse visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "cat" "+")
The cat does not like the cat.
Unknown
inv-rconc
[@2: The cat likes the cat.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cat" "likes" "cat" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "mouse" "+")
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 rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat eats the mouse.[(triple1)] The cat is big.[(triple2)] The cat is kind.[(triple3)] The cat visits the mouse.[(triple4)] The mouse eats the cat.[(triple5 OR ((triple7 triple6) -> rule1))] The mouse is not red.[(triple6)] The mouse likes the cat.[(triple7)] @1: The cat is nice.[(((triple7) -> rule3))] @2: The cat likes the mouse.[(((((triple7) -> rule3)) -> rule4))] @3: The mouse is not kind.[(((triple7 ((((triple7) -> rule3)) -> rule4)) -> rule6))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple4
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple5
((triple7 triple6) -> (rule1 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse is not red.
("mouse" "is" "red" "-")
triple6
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple7
The cat is nice.
("cat" "is" "nice" "+")
((triple7) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The mouse is not kind.
("mouse" "is" "kind" "-")
((triple7 ((((triple7) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The mouse is not kind.
("mouse" "is" "kind" "-")
int1
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
int3