The bear sees the rabbit. The dog sees the bear. The rabbit needs the dog. If someone eats the dog then the dog is not blue. If someone needs the rabbit then the rabbit does not need the dog. If someone eats the rabbit then the rabbit needs the dog. If someone eats the bear and the bear is blue then the bear eats the rabbit. If someone sees the dog then they need the bear. If someone sees the rabbit then they are nice. Cold people are not big. If someone is nice and they see the rabbit then the rabbit is big.
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If someone eats the dog then the dog is not blue.
((("someone" "eats" "dog" "+")) -> ("dog" "is" "blue" "-"))
If someone needs the rabbit then the rabbit does not need the dog.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "dog" "-"))
If someone eats the rabbit then the rabbit needs the dog.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If someone eats the bear and the bear is blue then the bear eats the rabbit.
((("someone" "eats" "bear" "+") ("bear" "is" "blue" "+")) -> ("bear" "eats" "rabbit" "+"))
If someone sees the dog then they need the bear.
((("someone" "sees" "dog" "+")) -> ("someone" "needs" "bear" "+"))
If someone sees the rabbit then they are nice.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "nice" "+"))
Cold people are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
If someone is nice and they see the rabbit then the rabbit is big.
((("someone" "is" "nice" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
The rabbit needs the dog.
True
1
proof
[(triple3)]
("rabbit" "needs" "dog" "+")
triple3
The dog does not see the bear.
False
1
inv-proof
[(triple2)]
("dog" "sees" "bear" "-")
triple2
The bear is nice.
True
2
proof
[(((triple1) -> rule6))]
("bear" "is" "nice" "+")
((triple1) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple1) -> rule6))]
("bear" "is" "nice" "-")
((triple1) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The rabbit is big.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule8))]
("rabbit" "is" "big" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The rabbit is not big.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule8))]
("rabbit" "is" "big" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "needs" "bear" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "nice" "+")
The dog does not need the bear.
Unknown
inv-rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "needs" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The bear does not see the dog.
Unknown
inv-random
[@0: The bear sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "dog" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear sees the rabbit.[(triple1)] The dog sees the bear.[(triple2)] The rabbit needs the dog.[(triple3)] @1: The bear is nice.[(((triple1) -> rule6))] @2: The rabbit is big.[(((((triple1) -> rule6) triple1) -> rule8))]
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple1
The dog sees the bear.
("dog" "sees" "bear" "+")
triple2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
((triple1) -> (rule6 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule8 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2