The bear is green. The bear likes the rabbit. The dog is not kind. The rabbit is cold. The rabbit likes the bear. The tiger is young. The tiger visits the dog. If something sees the tiger and it is not cold then the tiger visits the rabbit. If the tiger sees the dog then the dog is not young. If something is young and it does not visit the dog then it likes the tiger. If something likes the dog then the dog does not visit the rabbit. If something likes the rabbit and the rabbit likes the dog then it likes the bear. If something is green and not young then it does not see the bear. If something visits the dog then it sees the bear. If something is young and it does not like the bear then it is red.
The bear is green.
("bear" "is" "green" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The dog is not kind.
("dog" "is" "kind" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something sees the tiger and it is not cold then the tiger visits the rabbit.
((("something" "sees" "tiger" "+") ("something" "is" "cold" "~")) -> ("tiger" "visits" "rabbit" "+"))
If the tiger sees the dog then the dog is not young.
((("tiger" "sees" "dog" "+")) -> ("dog" "is" "young" "-"))
If something is young and it does not visit the dog then it likes the tiger.
((("something" "is" "young" "+") ("something" "visits" "dog" "~")) -> ("something" "likes" "tiger" "+"))
If something likes the dog then the dog does not visit the rabbit.
((("something" "likes" "dog" "+")) -> ("dog" "visits" "rabbit" "-"))
If something likes the rabbit and the rabbit likes the dog then it likes the bear.
((("something" "likes" "rabbit" "+") ("rabbit" "likes" "dog" "+")) -> ("something" "likes" "bear" "+"))
If something is green and not young then it does not see the bear.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "sees" "bear" "-"))
If something visits the dog then it sees the bear.
((("something" "visits" "dog" "+")) -> ("something" "sees" "bear" "+"))
If something is young and it does not like the bear then it is red.
((("something" "is" "young" "+") ("something" "likes" "bear" "~")) -> ("something" "is" "red" "+"))
The tiger visits the dog.
True
1
proof
[(triple7)]
("tiger" "visits" "dog" "+")
triple7
The tiger does not visit the dog.
False
1
inv-proof
[(triple7)]
("tiger" "visits" "dog" "-")
triple7
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "red" "-")
The tiger sees the dog.
Unknown
random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "+")
@0: The bear is green.[(triple1)] The bear likes the rabbit.[(triple2)] The dog is not kind.[(triple3)] The rabbit is cold.[(triple4)] The rabbit likes the bear.[(triple5)] The tiger is young.[(triple6)] The tiger visits the dog.[(triple7)] @1: The tiger sees the bear.[(((triple7) -> rule7))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple2
The dog is not kind.
("dog" "is" "kind" "-")
triple3
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple4
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple7
The tiger sees the bear.
("tiger" "sees" "bear" "+")
((triple7) -> (rule7 % int1))
The tiger sees the bear.
("tiger" "sees" "bear" "+")
int1