The cat eats the mouse. The cat is cold. The cat is round. The cat likes the mouse. The cat needs the mouse. The mouse eats the cat. The mouse is big. The mouse is cold. The mouse is rough. The mouse is round. The mouse likes the cat. The mouse needs the cat. If someone eats the mouse then they need the cat.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
If someone eats the mouse then they need the cat.
((("someone" "eats" "mouse" "+")) -> ("someone" "needs" "cat" "+"))
The mouse likes the cat.
True
1
proof
[(triple11)]
("mouse" "likes" "cat" "+")
triple11
The cat does not eat the mouse.
False
1
inv-proof
[(triple1)]
("cat" "eats" "mouse" "-")
triple1
The cat needs the cat.
True
2
proof
[(((triple1) -> rule1))]
("cat" "needs" "cat" "+")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat does not need the cat.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "needs" "cat" "-")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The mouse is not nice.
Unknown
inv-random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
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 cold.[(triple2)] The cat is round.[(triple3)] The cat likes the mouse.[(triple4)] The cat needs the mouse.[(triple5)] The mouse eats the cat.[(triple6)] The mouse is big.[(triple7)] The mouse is cold.[(triple8)] The mouse is rough.[(triple9)] The mouse is round.[(triple10)] The mouse likes the cat.[(triple11)] The mouse needs the cat.[(triple12)] @1: The cat needs the cat.[(((triple1) -> rule1))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple4
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple5
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple6
The mouse is big.
("mouse" "is" "big" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple11
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple12
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple1) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1