The bear sees the dog. The dog likes the rabbit. The rabbit is big. If something sees the dog and the dog sees the bear then the bear likes the rabbit. If the bear visits the dog and the bear visits the rabbit then the dog sees the rabbit. If something sees the bear then it is kind. If something sees the dog and it sees the rabbit then the dog is blue. If something likes the rabbit then the rabbit sees the bear. If something is green and it sees the rabbit then it is nice. If something is kind then it visits the rabbit. If the rabbit visits the bear and the bear is nice then the rabbit likes the bear.
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
If something sees the dog and the dog sees the bear then the bear likes the rabbit.
((("something" "sees" "dog" "+") ("dog" "sees" "bear" "+")) -> ("bear" "likes" "rabbit" "+"))
If the bear visits the dog and the bear visits the rabbit then the dog sees the rabbit.
((("bear" "visits" "dog" "+") ("bear" "visits" "rabbit" "+")) -> ("dog" "sees" "rabbit" "+"))
If something sees the bear then it is kind.
((("something" "sees" "bear" "+")) -> ("something" "is" "kind" "+"))
If something sees the dog and it sees the rabbit then the dog is blue.
((("something" "sees" "dog" "+") ("something" "sees" "rabbit" "+")) -> ("dog" "is" "blue" "+"))
If something likes the rabbit then the rabbit sees the bear.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "sees" "bear" "+"))
If something is green and it sees the rabbit then it is nice.
((("something" "is" "green" "+") ("something" "sees" "rabbit" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it visits the rabbit.
((("something" "is" "kind" "+")) -> ("something" "visits" "rabbit" "+"))
If the rabbit visits the bear and the bear is nice then the rabbit likes the bear.
((("rabbit" "visits" "bear" "+") ("bear" "is" "nice" "+")) -> ("rabbit" "likes" "bear" "+"))
The dog likes the rabbit.
True
1
proof
[(triple2)]
("dog" "likes" "rabbit" "+")
triple2
The rabbit is not big.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "big" "-")
triple3
The rabbit sees the bear.
True
2
proof
[(((triple2) -> rule5))]
("rabbit" "sees" "bear" "+")
((triple2) -> (rule5 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The rabbit does not see the bear.
False
2
inv-proof
[(((triple2) -> rule5))]
("rabbit" "sees" "bear" "-")
((triple2) -> (rule5 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "nice" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear sees the dog.[(triple1)] The dog likes the rabbit.[(triple2)] The rabbit is big.[(triple3)] @1: The rabbit sees the bear.[(((triple2) -> rule5))] @2: The rabbit is kind.[(((((triple2) -> rule5)) -> rule3))] @3: The rabbit visits the rabbit.[(((((((triple2) -> rule5)) -> rule3)) -> rule7))]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
((triple2) -> (rule5 % int1))
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
int3