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