The cat chases the mouse. The cat eats the mouse. The cat is blue. The cat is cold. The cat is rough. The cat is young. The cat sees the mouse. The mouse chases the cat. The mouse does not eat the cat. The mouse is blue. The mouse is not cold. The mouse is not kind. The mouse is rough. The mouse is young. The mouse does not see the cat. If someone is cold and rough then they do not see the cat.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse is not kind.
("mouse" "is" "kind" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
If someone is cold and rough then they do not see the cat.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "sees" "cat" "-"))
The mouse is young.
True
1
proof
[(triple14)]
("mouse" "is" "young" "+")
triple14
The mouse eats the cat.
False
1
inv-proof
[(triple9)]
("mouse" "eats" "cat" "+")
triple9
The cat does not see the cat.
True
3
proof
[(((triple4 triple5) -> rule1))]
("cat" "sees" "cat" "-")
((triple4 triple5) -> (rule1 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat sees the cat.
False
3
inv-proof
[(((triple4 triple5) -> rule1))]
("cat" "sees" "cat" "+")
((triple4 triple5) -> (rule1 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The cat chases the mouse.[(triple1)] The cat eats the mouse.[(triple2)] The cat is blue.[(triple3)] The cat is cold.[(triple4)] The cat is rough.[(triple5)] The cat is young.[(triple6)] The cat sees the mouse.[(triple7)] The mouse chases the cat.[(triple8)] The mouse does not eat the cat.[(triple9)] The mouse does not see the cat.[(triple15)] The mouse is blue.[(triple10)] The mouse is not cold.[(triple11)] The mouse is not kind.[(triple12)] The mouse is rough.[(triple13)] The mouse is young.[(triple14)] @1: The cat does not see the cat.[(((triple4 triple5) -> rule1))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple4
The cat is rough.
("cat" "is" "rough" "+")
triple5
The cat is young.
("cat" "is" "young" "+")
triple6
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple7
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple8
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
triple9
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
triple15
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is not cold.
("mouse" "is" "cold" "-")
triple11
The mouse is not kind.
("mouse" "is" "kind" "-")
triple12
The mouse is rough.
("mouse" "is" "rough" "+")
triple13
The mouse is young.
("mouse" "is" "young" "+")
triple14
The cat does not see the cat.
("cat" "sees" "cat" "-")
((triple4 triple5) -> (rule1 % int1))
The cat does not see the cat.
("cat" "sees" "cat" "-")
int1