The cat is not green. The cat visits the mouse. The mouse chases the cat. The mouse eats the cat. The mouse is not cold. The mouse is red. The mouse visits the cat. If someone visits the mouse then the mouse visits the cat.
The cat is not green.
("cat" "is" "green" "-")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If someone visits the mouse then the mouse visits the cat.
((("someone" "visits" "mouse" "+")) -> ("mouse" "visits" "cat" "+"))
The mouse is red.
True
1
proof
[(triple6)]
("mouse" "is" "red" "+")
triple6
The mouse does not visit the cat.
False
1
inv-proof
[(triple7 OR ((triple2) -> rule1))]
("mouse" "visits" "cat" "-")
triple7
((triple2) -> (rule1 % int1))
The mouse visits the cat.
("mouse" "visits" "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 mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The cat is not green.[(triple1)] The cat visits the mouse.[(triple2)] The mouse chases the cat.[(triple3)] The mouse eats the cat.[(triple4)] The mouse is not cold.[(triple5)] The mouse is red.[(triple6)] The mouse visits the cat.[(triple7 OR ((triple2) -> rule1))]
The cat is not green.
("cat" "is" "green" "-")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple3
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple4
The mouse is not cold.
("mouse" "is" "cold" "-")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple7
((triple2) -> (rule1 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1