The dog likes the rabbit. The dog visits the rabbit. The rabbit is kind. The rabbit is round. The rabbit needs the dog. The tiger is big. The tiger likes the dog. The tiger likes the rabbit. The tiger needs the dog. The tiger does not visit the dog. If someone visits the dog and they are round then the dog is cold. If the tiger needs the rabbit and the rabbit likes the dog then the tiger likes the rabbit. If the dog is big and the dog likes the tiger then the dog needs the tiger. If someone is kind then they visit the dog. If someone needs the dog and they do not visit the dog then the dog is not rough. If someone visits the rabbit and they do not like the rabbit then the rabbit does not like the tiger.
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
If someone visits the dog and they are round then the dog is cold.
((("someone" "visits" "dog" "+") ("someone" "is" "round" "+")) -> ("dog" "is" "cold" "+"))
If the tiger needs the rabbit and the rabbit likes the dog then the tiger likes the rabbit.
((("tiger" "needs" "rabbit" "+") ("rabbit" "likes" "dog" "+")) -> ("tiger" "likes" "rabbit" "+"))
If the dog is big and the dog likes the tiger then the dog needs the tiger.
((("dog" "is" "big" "+") ("dog" "likes" "tiger" "+")) -> ("dog" "needs" "tiger" "+"))
If someone is kind then they visit the dog.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "dog" "+"))
If someone needs the dog and they do not visit the dog then the dog is not rough.
((("someone" "needs" "dog" "+") ("someone" "visits" "dog" "~")) -> ("dog" "is" "rough" "-"))
If someone visits the rabbit and they do not like the rabbit then the rabbit does not like the tiger.
((("someone" "visits" "rabbit" "+") ("someone" "likes" "rabbit" "~")) -> ("rabbit" "likes" "tiger" "-"))
The tiger likes the dog.
True
1
proof
[(triple7)]
("tiger" "likes" "dog" "+")
triple7
The tiger is not big.
False
1
inv-proof
[(triple6)]
("tiger" "is" "big" "-")
triple6
The dog is not rough.
True
3
proof
[(((triple9 triple10) -> rule5))]
("dog" "is" "rough" "-")
((triple9 triple10) -> (rule5 % int1))
The dog is not rough.
("dog" "is" "rough" "-")
int1
The rabbit does not visit the dog.
False
2
inv-proof
[(((triple3) -> rule4))]
("rabbit" "visits" "dog" "-")
((triple3) -> (rule4 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog is cold.
True
4
proof
[(((((triple3) -> rule4) triple4) -> rule1))]
("dog" "is" "cold" "+")
((((triple3) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The dog is not cold.
False
4
inv-proof
[(((((triple3) -> rule4) triple4) -> rule1))]
("dog" "is" "cold" "-")
((((triple3) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "dog" "-")
The dog needs the tiger.
Unknown
rconc
[@1: The dog needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "tiger" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The tiger does not visit the rabbit.
Unknown
inv-random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The dog likes the rabbit.[(triple1)] The dog visits the rabbit.[(triple2)] The rabbit is kind.[(triple3)] The rabbit is round.[(triple4)] The rabbit needs the dog.[(triple5)] The tiger does not visit the dog.[(triple10)] The tiger is big.[(triple6)] The tiger likes the dog.[(triple7)] The tiger likes the rabbit.[(triple8)] The tiger needs the dog.[(triple9)] @1: The dog is not rough.[(((triple9 triple10) -> rule5))] The rabbit visits the dog.[(((triple3) -> rule4))] @2: The dog is cold.[(((((triple3) -> rule4) triple4) -> rule1))]
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple5
The tiger does not visit the dog.
("tiger" "visits" "dog" "-")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple7
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple8
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple9
The dog is not rough.
("dog" "is" "rough" "-")
((triple9 triple10) -> (rule5 % int1))
The dog is not rough.
("dog" "is" "rough" "-")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple3) -> (rule4 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((((triple3) -> (rule4 % int2)) triple4) -> (rule1 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2