The dog is cold. The dog is red. The dog is young. The dog needs the mouse. The dog visits the mouse. The mouse is round. The mouse likes the tiger. The mouse needs the rabbit. The mouse visits the dog. The rabbit visits the dog. The rabbit visits the mouse. The rabbit visits the tiger. The tiger is red. The tiger is round. The tiger likes the dog. The tiger visits the rabbit. If the tiger needs the rabbit then the tiger likes the mouse. If something needs the tiger and it needs the dog then it is red. If something is red and it needs the rabbit then it visits the mouse. If something is round then it needs the rabbit. If the rabbit likes the mouse then the mouse likes the dog. If something needs the tiger then it likes the rabbit.
The dog is cold.
("dog" "is" "cold" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
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 is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If the tiger needs the rabbit then the tiger likes the mouse.
((("tiger" "needs" "rabbit" "+")) -> ("tiger" "likes" "mouse" "+"))
If something needs the tiger and it needs the dog then it is red.
((("something" "needs" "tiger" "+") ("something" "needs" "dog" "+")) -> ("something" "is" "red" "+"))
If something is red and it needs the rabbit then it visits the mouse.
((("something" "is" "red" "+") ("something" "needs" "rabbit" "+")) -> ("something" "visits" "mouse" "+"))
If something is round then it needs the rabbit.
((("something" "is" "round" "+")) -> ("something" "needs" "rabbit" "+"))
If the rabbit likes the mouse then the mouse likes the dog.
((("rabbit" "likes" "mouse" "+")) -> ("mouse" "likes" "dog" "+"))
If something needs the tiger then it likes the rabbit.
((("something" "needs" "tiger" "+")) -> ("something" "likes" "rabbit" "+"))
The mouse visits the dog.
True
1
proof
[(triple9)]
("mouse" "visits" "dog" "+")
triple9
The mouse does not visit the dog.
False
1
inv-proof
[(triple9)]
("mouse" "visits" "dog" "-")
triple9
The tiger needs the rabbit.
True
2
proof
[(((triple14) -> rule4))]
("tiger" "needs" "rabbit" "+")
((triple14) -> (rule4 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger does not need the rabbit.
False
2
inv-proof
[(((triple14) -> rule4))]
("tiger" "needs" "rabbit" "-")
((triple14) -> (rule4 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger visits the mouse.
True
4
proof
[(((triple13 ((triple14) -> rule4)) -> rule3))]
("tiger" "visits" "mouse" "+")
((triple13 ((triple14) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The tiger does not like the mouse.
False
3
inv-proof
[(((((triple14) -> rule4)) -> rule1))]
("tiger" "likes" "mouse" "-")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The tiger does not like the rabbit.
Unknown
inv-rconc
[@1: The tiger likes the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "rabbit" "-")
The mouse is red.
Unknown
rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "red" "+")
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "red" "-")
The tiger visits the dog.
Unknown
random
[@0: The tiger visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "dog" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The mouse needs the tiger.
Unknown
random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "+")
@0: The dog is cold.[(triple1)] The dog is red.[(triple2)] The dog is young.[(triple3)] The dog needs the mouse.[(triple4)] The dog visits the mouse.[(triple5)] The mouse is round.[(triple6)] The mouse likes the tiger.[(triple7)] The mouse needs the rabbit.[(triple8 OR ((triple6) -> rule4))] The mouse visits the dog.[(triple9)] The rabbit visits the dog.[(triple10)] The rabbit visits the mouse.[(triple11)] The rabbit visits the tiger.[(triple12)] The tiger is red.[(triple13)] The tiger is round.[(triple14)] The tiger likes the dog.[(triple15)] The tiger visits the rabbit.[(triple16)] @1: The tiger needs the rabbit.[(((triple14) -> rule4))] @2: The tiger likes the mouse.[(((((triple14) -> rule4)) -> rule1))] The tiger visits the mouse.[(((triple13 ((triple14) -> rule4)) -> rule3))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple4
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple7
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple8
((triple6) -> (rule4 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
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 is red.
("tiger" "is" "red" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple15
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple16
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
((triple14) -> (rule4 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((((triple14) -> (rule4 % int2))) -> (rule1 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((triple13 ((triple14) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int2