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