The dog is blue. The mouse is red. The mouse is young. The mouse likes the rabbit. The mouse visits the rabbit. The rabbit chases the tiger. The rabbit is round. The rabbit likes the dog. The rabbit likes the tiger. The rabbit visits the dog. The rabbit visits the mouse. The rabbit visits the tiger. The tiger chases the rabbit. The tiger is kind. The tiger likes the dog. The tiger likes the rabbit. If someone likes the tiger then they chase the rabbit. If someone chases the dog and they do not visit the dog then they chase the rabbit. If someone likes the mouse then they do not visit the tiger. If someone visits the tiger and the tiger visits the rabbit then they visit the mouse. If the tiger visits the mouse and the tiger does not like the mouse then the tiger visits the rabbit. If someone visits the mouse and they chase the tiger then the mouse likes the tiger.
The dog is blue.
("dog" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If someone likes the tiger then they chase the rabbit.
((("someone" "likes" "tiger" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the dog and they do not visit the dog then they chase the rabbit.
((("someone" "chases" "dog" "+") ("someone" "visits" "dog" "~")) -> ("someone" "chases" "rabbit" "+"))
If someone likes the mouse then they do not visit the tiger.
((("someone" "likes" "mouse" "+")) -> ("someone" "visits" "tiger" "-"))
If someone visits the tiger and the tiger visits the rabbit then they visit the mouse.
((("someone" "visits" "tiger" "+") ("tiger" "visits" "rabbit" "+")) -> ("someone" "visits" "mouse" "+"))
If the tiger visits the mouse and the tiger does not like the mouse then the tiger visits the rabbit.
((("tiger" "visits" "mouse" "+") ("tiger" "likes" "mouse" "~")) -> ("tiger" "visits" "rabbit" "+"))
If someone visits the mouse and they chase the tiger then the mouse likes the tiger.
((("someone" "visits" "mouse" "+") ("someone" "chases" "tiger" "+")) -> ("mouse" "likes" "tiger" "+"))
The mouse visits the rabbit.
True
1
proof
[(triple5)]
("mouse" "visits" "rabbit" "+")
triple5
The tiger does not like the dog.
False
1
inv-proof
[(triple15)]
("tiger" "likes" "dog" "-")
triple15
The mouse likes the tiger.
True
3
proof
[(((triple11 triple6) -> rule6))]
("mouse" "likes" "tiger" "+")
((triple11 triple6) -> (rule6 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse does not like the tiger.
False
3
inv-proof
[(((triple11 triple6) -> rule6))]
("mouse" "likes" "tiger" "-")
((triple11 triple6) -> (rule6 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse chases the rabbit.
True
4
proof
[(((((triple11 triple6) -> rule6)) -> rule1))]
("mouse" "chases" "rabbit" "+")
((((triple11 triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse does not chase the rabbit.
False
4
inv-proof
[(((((triple11 triple6) -> rule6)) -> rule1))]
("mouse" "chases" "rabbit" "-")
((((triple11 triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The tiger does not visit the mouse.
Unknown
inv-rconc
[@1: The tiger visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "visits" "mouse" "-")
The dog chases the rabbit.
Unknown
rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "rabbit" "+")
The tiger does not visit the rabbit.
Unknown
inv-rconc
[@1: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "visits" "rabbit" "-")
The tiger visits the dog.
Unknown
random
[@0: The tiger visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "dog" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The dog visits the tiger.
Unknown
random
[@0: The dog visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "tiger" "+")
@0: The dog is blue.[(triple1)] The mouse is red.[(triple2)] The mouse is young.[(triple3)] The mouse likes the rabbit.[(triple4)] The mouse visits the rabbit.[(triple5)] The rabbit chases the tiger.[(triple6)] The rabbit is round.[(triple7)] The rabbit likes the dog.[(triple8)] The rabbit likes the tiger.[(triple9)] The rabbit visits the dog.[(triple10)] The rabbit visits the mouse.[(triple11)] The rabbit visits the tiger.[(triple12)] The tiger chases the rabbit.[(triple13)] The tiger is kind.[(triple14)] The tiger likes the dog.[(triple15)] The tiger likes the rabbit.[(triple16)] @1: The mouse likes the tiger.[(((triple11 triple6) -> rule6))] The rabbit chases the rabbit.[(((triple9) -> rule1))] @2: The mouse chases the rabbit.[(((((triple11 triple6) -> rule6)) -> rule1))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse is young.
("mouse" "is" "young" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple4
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple5
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple6
The rabbit is round.
("rabbit" "is" "round" "+")
triple7
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple8
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple9
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple10
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple11
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple12
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple13
The tiger is kind.
("tiger" "is" "kind" "+")
triple14
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple15
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple16
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple11 triple6) -> (rule6 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple9) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((((triple11 triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2