The cat eats the mouse. The cat is big. The cat is blue. The cat is cold. The cat is kind. The cat likes the mouse. The cat visits the mouse. The mouse eats the cat. The mouse is big. The mouse is blue. The mouse is cold. The mouse is kind. The mouse is nice. The mouse does not like the cat. The mouse visits the cat. If someone likes the cat then the cat visits the mouse. If someone eats the cat and the cat eats the mouse then they visit the cat. If someone is blue then they eat the cat. If someone likes the cat and they like the mouse then they eat the cat. If someone visits the mouse and they are not blue then the mouse visits the cat. If someone likes the cat and the cat is cold then they like the mouse.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If someone likes the cat then the cat visits the mouse.
((("someone" "likes" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If someone eats the cat and the cat eats the mouse then they visit the cat.
((("someone" "eats" "cat" "+") ("cat" "eats" "mouse" "+")) -> ("someone" "visits" "cat" "+"))
If someone is blue then they eat the cat.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "cat" "+"))
If someone likes the cat and they like the mouse then they eat the cat.
((("someone" "likes" "cat" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "eats" "cat" "+"))
If someone visits the mouse and they are not blue then the mouse visits the cat.
((("someone" "visits" "mouse" "+") ("someone" "is" "blue" "~")) -> ("mouse" "visits" "cat" "+"))
If someone likes the cat and the cat is cold then they like the mouse.
((("someone" "likes" "cat" "+") ("cat" "is" "cold" "+")) -> ("someone" "likes" "mouse" "+"))
The cat likes the mouse.
True
1
proof
[(triple6)]
("cat" "likes" "mouse" "+")
triple6
The mouse is not blue.
False
1
inv-proof
[(triple10)]
("mouse" "is" "blue" "-")
triple10
The cat eats the cat.
True
2
proof
[(((triple3) -> rule3))]
("cat" "eats" "cat" "+")
((triple3) -> (rule3 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not eat the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("cat" "eats" "cat" "-")
((triple3) -> (rule3 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
True
4
proof
[(((((triple3) -> rule3) triple1) -> rule2))]
("cat" "visits" "cat" "+")
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat does not visit the cat.
False
4
inv-proof
[(((((triple3) -> rule3) triple1) -> rule2))]
("cat" "visits" "cat" "-")
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat eats the mouse.[(triple1)] The cat is big.[(triple2)] The cat is blue.[(triple3)] The cat is cold.[(triple4)] The cat is kind.[(triple5)] The cat likes the mouse.[(triple6)] The cat visits the mouse.[(triple7)] The mouse does not like the cat.[(triple14)] The mouse eats the cat.[(triple8 OR ((triple10) -> rule3))] The mouse is big.[(triple9)] The mouse is blue.[(triple10)] The mouse is cold.[(triple11)] The mouse is kind.[(triple12)] The mouse is nice.[(triple13)] The mouse visits the cat.[(triple15 OR ((triple8 triple1) -> rule2) OR ((((triple10) -> rule3) triple1) -> rule2))] @1: The cat eats the cat.[(((triple3) -> rule3))] @2: The cat visits the cat.[(((((triple3) -> rule3) triple1) -> rule2))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple6
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple7
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple14
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple8
((triple10) -> (rule3 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is cold.
("mouse" "is" "cold" "+")
triple11
The mouse is kind.
("mouse" "is" "kind" "+")
triple12
The mouse is nice.
("mouse" "is" "nice" "+")
triple13
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple15
((triple8 triple1) -> (rule2 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
((((triple10) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple3) -> (rule3 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple3) -> (rule3 % int2)) triple1) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2