The dog is cold. The dog is kind. The dog likes the rabbit. The dog visits the rabbit. The rabbit is big. The rabbit is cold. The rabbit is rough. The rabbit likes the dog. The rabbit sees the tiger. The rabbit visits the dog. The rabbit visits the tiger. The tiger is cold. The tiger likes the dog. The tiger sees the dog. The tiger sees the rabbit. The tiger visits the dog. If something is cold and it sees the dog then the dog visits the rabbit. If something visits the dog then it is kind. If something sees the rabbit and the rabbit sees the tiger then it is cold. If the dog is big then the dog likes the rabbit. If the rabbit visits the tiger then the tiger visits the dog. If something likes the dog and it visits the rabbit then it visits the tiger.
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something is cold and it sees the dog then the dog visits the rabbit.
((("something" "is" "cold" "+") ("something" "sees" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If something visits the dog then it is kind.
((("something" "visits" "dog" "+")) -> ("something" "is" "kind" "+"))
If something sees the rabbit and the rabbit sees the tiger then it is cold.
((("something" "sees" "rabbit" "+") ("rabbit" "sees" "tiger" "+")) -> ("something" "is" "cold" "+"))
If the dog is big then the dog likes the rabbit.
((("dog" "is" "big" "+")) -> ("dog" "likes" "rabbit" "+"))
If the rabbit visits the tiger then the tiger visits the dog.
((("rabbit" "visits" "tiger" "+")) -> ("tiger" "visits" "dog" "+"))
If something likes the dog and it visits the rabbit then it visits the tiger.
((("something" "likes" "dog" "+") ("something" "visits" "rabbit" "+")) -> ("something" "visits" "tiger" "+"))
The rabbit visits the tiger.
True
1
proof
[(triple11)]
("rabbit" "visits" "tiger" "+")
triple11
The rabbit does not like the dog.
False
1
inv-proof
[(triple8)]
("rabbit" "likes" "dog" "-")
triple8
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "visits" "tiger" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is cold.[(triple1)] The dog is kind.[(triple2)] The dog likes the rabbit.[(triple3)] The dog visits the rabbit.[(triple4 OR ((triple12 triple14) -> rule1) OR ((((triple15 triple9) -> rule3) triple14) -> rule1))] The rabbit is big.[(triple5)] The rabbit is cold.[(triple6)] The rabbit is rough.[(triple7)] The rabbit likes the dog.[(triple8)] The rabbit sees the tiger.[(triple9)] The rabbit visits the dog.[(triple10)] The rabbit visits the tiger.[(triple11)] The tiger is cold.[(triple12 OR ((triple15 triple9) -> rule3))] The tiger likes the dog.[(triple13)] The tiger sees the dog.[(triple14)] The tiger sees the rabbit.[(triple15)] The tiger visits the dog.[(triple16 OR ((triple11) -> rule5))] @1: The rabbit is kind.[(((triple10) -> rule2))] The tiger is kind.[(((triple16) -> rule2) OR ((((triple11) -> rule5)) -> rule2))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
((triple12 triple14) -> (rule1 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
((((triple15 triple9) -> (rule3 % int2)) triple14) -> (rule1 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple7
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple8
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple9
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple10
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
((triple15 triple9) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple13
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple14
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple15
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple16
((triple11) -> (rule5 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple10) -> (rule2 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple16) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2