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