The cow is blue. The dog chases the tiger. The dog is blue. The dog needs the mouse. The mouse chases the tiger. The mouse is round. The tiger needs the cow. The tiger needs the mouse. The tiger visits the cow. The tiger visits the dog. If someone chases the tiger and the tiger needs the cow then they visit the tiger. If someone is cold and they visit the cow then they visit the dog. If the cow needs the mouse then the mouse needs the cow.
The cow is blue.
("cow" "is" "blue" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is round.
("mouse" "is" "round" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone chases the tiger and the tiger needs the cow then they visit the tiger.
((("someone" "chases" "tiger" "+") ("tiger" "needs" "cow" "+")) -> ("someone" "visits" "tiger" "+"))
If someone is cold and they visit the cow then they visit the dog.
((("someone" "is" "cold" "+") ("someone" "visits" "cow" "+")) -> ("someone" "visits" "dog" "+"))
If the cow needs the mouse then the mouse needs the cow.
((("cow" "needs" "mouse" "+")) -> ("mouse" "needs" "cow" "+"))
The tiger visits the cow.
True
1
proof
[(triple9)]
("tiger" "visits" "cow" "+")
triple9
The mouse is not round.
False
1
inv-proof
[(triple6)]
("mouse" "is" "round" "-")
triple6
The mouse visits the tiger.
True
3
proof
[(((triple5 triple7) -> rule1))]
("mouse" "visits" "tiger" "+")
((triple5 triple7) -> (rule1 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse does not visit the tiger.
False
3
inv-proof
[(((triple5 triple7) -> rule1))]
("mouse" "visits" "tiger" "-")
((triple5 triple7) -> (rule1 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The cow does not visit the tiger.
Unknown
inv-rconc
[@1: The cow visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "tiger" "-")
The cow visits the dog.
Unknown
rconc
[@1: The cow visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "dog" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The cow is blue.[(triple1)] The dog chases the tiger.[(triple2)] The dog is blue.[(triple3)] The dog needs the mouse.[(triple4)] The mouse chases the tiger.[(triple5)] The mouse is round.[(triple6)] The tiger needs the cow.[(triple7)] The tiger needs the mouse.[(triple8)] The tiger visits the cow.[(triple9)] The tiger visits the dog.[(triple10)] @1: The dog visits the tiger.[(((triple2 triple7) -> rule1))] The mouse visits the tiger.[(((triple5 triple7) -> rule1))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple7
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple8
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
The dog visits the tiger.
("dog" "visits" "tiger" "+")
((triple2 triple7) -> (rule1 % int1))
The dog visits the tiger.
("dog" "visits" "tiger" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((triple5 triple7) -> (rule1 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1