The cat chases the mouse. The cat visits the mouse. The dog visits the mouse. The mouse chases the tiger. The mouse is blue. The mouse is red. The mouse visits the dog. The mouse visits the tiger. The tiger is green. The tiger visits the cat. If someone visits the cat and the cat does not visit the tiger then they are green. If someone visits the mouse then they are green. If someone visits the tiger then they visit the mouse.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone visits the cat and the cat does not visit the tiger then they are green.
((("someone" "visits" "cat" "+") ("cat" "visits" "tiger" "~")) -> ("someone" "is" "green" "+"))
If someone visits the mouse then they are green.
((("someone" "visits" "mouse" "+")) -> ("someone" "is" "green" "+"))
If someone visits the tiger then they visit the mouse.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "mouse" "+"))
The cat visits the mouse.
True
1
proof
[(triple2)]
("cat" "visits" "mouse" "+")
triple2
The tiger is not green.
False
1
inv-proof
[(triple9)]
("tiger" "is" "green" "-")
triple9
The cat is green.
True
2
proof
[(((triple2) -> rule2))]
("cat" "is" "green" "+")
((triple2) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "is" "green" "-")
((triple3) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The mouse is green.
True
3
proof
[(((((triple8) -> rule3)) -> rule2))]
("mouse" "is" "green" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple8) -> rule3)) -> rule2))]
("mouse" "is" "green" "-")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The tiger does not visit the mouse.
Unknown
inv-rconc
[@1: The tiger visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "mouse" "-")
The cat likes the tiger.
Unknown
random
[@0: The cat likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "tiger" "+")
The cat does not chase the dog.
Unknown
inv-random
[@0: The cat chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "dog" "-")
The dog likes the cat.
Unknown
random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The mouse chases the cat.
Unknown
random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "+")
@0: The cat chases the mouse.[(triple1)] The cat visits the mouse.[(triple2)] The dog visits the mouse.[(triple3)] The mouse chases the tiger.[(triple4)] The mouse is blue.[(triple5)] The mouse is red.[(triple6)] The mouse visits the dog.[(triple7)] The mouse visits the tiger.[(triple8)] The tiger is green.[(triple9)] The tiger visits the cat.[(triple10)] @1: The cat is green.[(((triple2) -> rule2))] The dog is green.[(((triple3) -> rule2))] The mouse visits the mouse.[(((triple8) -> rule3))] @2: The mouse is green.[(((((triple8) -> rule3)) -> rule2))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple3
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple5
The mouse is red.
("mouse" "is" "red" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger is green.
("tiger" "is" "green" "+")
triple9
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple10
The cat is green.
("cat" "is" "green" "+")
((triple2) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((triple3) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple8) -> (rule3 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple8) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2