The cat eats the mouse. The cat is green. The cat is kind. The cat is not red. The cat is not round. The cat is not young. The cat likes the mouse. The cat does not visit the mouse. The mouse eats the cat. The mouse is green. The mouse is kind. The mouse is red. The mouse is round. The mouse is not young. The mouse does not like the cat. The mouse visits the cat. If something eats the cat then it visits the mouse. If something visits the cat then the cat is not round. If the cat likes the mouse then the cat eats the mouse. If the cat likes the mouse and the mouse eats the cat then the cat eats the mouse. If something likes the cat and it visits the cat then the cat is green. If the mouse eats the cat and the mouse is not kind then the cat visits the mouse.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is not red.
("cat" "is" "red" "-")
The cat is not round.
("cat" "is" "round" "-")
The cat is not young.
("cat" "is" "young" "-")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If something eats the cat then it visits the mouse.
((("something" "eats" "cat" "+")) -> ("something" "visits" "mouse" "+"))
If something visits the cat then the cat is not round.
((("something" "visits" "cat" "+")) -> ("cat" "is" "round" "-"))
If the cat likes the mouse then the cat eats the mouse.
((("cat" "likes" "mouse" "+")) -> ("cat" "eats" "mouse" "+"))
If the cat likes the mouse and the mouse eats the cat then the cat eats the mouse.
((("cat" "likes" "mouse" "+") ("mouse" "eats" "cat" "+")) -> ("cat" "eats" "mouse" "+"))
If something likes the cat and it visits the cat then the cat is green.
((("something" "likes" "cat" "+") ("something" "visits" "cat" "+")) -> ("cat" "is" "green" "+"))
If the mouse eats the cat and the mouse is not kind then the cat visits the mouse.
((("mouse" "eats" "cat" "+") ("mouse" "is" "kind" "~")) -> ("cat" "visits" "mouse" "+"))
The mouse is red.
True
1
proof
[(triple12)]
("mouse" "is" "red" "+")
triple12
The cat visits the mouse.
False
1
inv-proof
[(triple8)]
("cat" "visits" "mouse" "+")
triple8
The mouse visits the mouse.
True
2
proof
[(((triple9) -> rule1))]
("mouse" "visits" "mouse" "+")
((triple9) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple9) -> rule1))]
("mouse" "visits" "mouse" "-")
((triple9) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
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" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The cat does not visit the mouse.[(triple8)] The cat eats the mouse.[(triple1 OR ((triple7) -> rule3) OR ((triple7 triple9) -> rule4))] The cat is green.[(triple2)] The cat is kind.[(triple3)] The cat is not red.[(triple4)] The cat is not round.[(triple5 OR ((triple16) -> rule2))] The cat is not young.[(triple6)] The cat likes the mouse.[(triple7)] The mouse does not like the cat.[(triple15)] The mouse eats the cat.[(triple9)] The mouse is green.[(triple10)] The mouse is kind.[(triple11)] The mouse is not young.[(triple14)] The mouse is red.[(triple12)] The mouse is round.[(triple13)] The mouse visits the cat.[(triple16)] @1: The mouse visits the mouse.[(((triple9) -> rule1))]
The cat does not visit the mouse.
("cat" "visits" "mouse" "-")
triple8
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
((triple7) -> (rule3 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
((triple7 triple9) -> (rule4 % int1))
The cat eats the mouse.
("cat" "eats" "mouse" "+")
int1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is not red.
("cat" "is" "red" "-")
triple4
The cat is not round.
("cat" "is" "round" "-")
triple5
((triple16) -> (rule2 % int1))
The cat is not round.
("cat" "is" "round" "-")
int1
The cat is not young.
("cat" "is" "young" "-")
triple6
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple7
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple15
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple9
The mouse is green.
("mouse" "is" "green" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse is not young.
("mouse" "is" "young" "-")
triple14
The mouse is red.
("mouse" "is" "red" "+")
triple12
The mouse is round.
("mouse" "is" "round" "+")
triple13
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple16
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple9) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1