The cat is green. The cat is red. The cat is rough. The cat is round. The cat is young. The cat likes the mouse. The cat sees the mouse. The cat visits the mouse. The mouse is green. The mouse is red. The mouse is rough. The mouse is young. The mouse likes the cat. The mouse sees the cat. The mouse visits the cat. If someone is round then they see the mouse. If the mouse sees the cat and the mouse visits the cat then the mouse is round.
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If someone is round then they see the mouse.
((("someone" "is" "round" "+")) -> ("someone" "sees" "mouse" "+"))
If the mouse sees the cat and the mouse visits the cat then the mouse is round.
((("mouse" "sees" "cat" "+") ("mouse" "visits" "cat" "+")) -> ("mouse" "is" "round" "+"))
The cat visits the mouse.
True
1
proof
[(triple8)]
("cat" "visits" "mouse" "+")
triple8
The cat does not see the mouse.
False
1
inv-proof
[(triple7 OR ((triple4) -> rule1))]
("cat" "sees" "mouse" "-")
triple7
((triple4) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The mouse is round.
True
3
proof
[(((triple14 triple15) -> rule2))]
("mouse" "is" "round" "+")
((triple14 triple15) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
3
inv-proof
[(((triple14 triple15) -> rule2))]
("mouse" "is" "round" "-")
((triple14 triple15) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse sees the mouse.
True
4
proof
[(((((triple14 triple15) -> rule2)) -> rule1))]
("mouse" "sees" "mouse" "+")
((((triple14 triple15) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The mouse does not see the mouse.
False
4
inv-proof
[(((((triple14 triple15) -> rule2)) -> rule1))]
("mouse" "sees" "mouse" "-")
((((triple14 triple15) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
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 mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
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 cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is green.[(triple1)] The cat is red.[(triple2)] The cat is rough.[(triple3)] The cat is round.[(triple4)] The cat is young.[(triple5)] The cat likes the mouse.[(triple6)] The cat sees the mouse.[(triple7 OR ((triple4) -> rule1))] The cat visits the mouse.[(triple8)] The mouse is green.[(triple9)] The mouse is red.[(triple10)] The mouse is rough.[(triple11)] The mouse is young.[(triple12)] The mouse likes the cat.[(triple13)] The mouse sees the cat.[(triple14)] The mouse visits the cat.[(triple15)] @1: The mouse is round.[(((triple14 triple15) -> rule2))] @2: The mouse sees the mouse.[(((((triple14 triple15) -> rule2)) -> rule1))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple6
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple7
((triple4) -> (rule1 % int1))
The cat sees the mouse.
("cat" "sees" "mouse" "+")
int1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple8
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse is red.
("mouse" "is" "red" "+")
triple10
The mouse is rough.
("mouse" "is" "rough" "+")
triple11
The mouse is young.
("mouse" "is" "young" "+")
triple12
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple13
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple14
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple15
The mouse is round.
("mouse" "is" "round" "+")
((triple14 triple15) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple14 triple15) -> (rule2 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2