The bear chases the rabbit. The bear is blue. The bear is cold. The bear is nice. The bear is red. The bear is young. The bear needs the rabbit. The bear visits the rabbit. The rabbit chases the bear. The rabbit is not cold. The rabbit needs the bear. The rabbit does not visit the bear. If someone is nice and not young then they do not visit the rabbit. If someone is blue then they chase the bear. If someone is nice then they chase the rabbit. If the bear chases the rabbit and the rabbit chases the bear then the rabbit is nice. If someone needs the rabbit and they do not visit the rabbit then they need the bear. If someone chases the bear and the bear does not chase the rabbit then the bear is not red.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
If someone is nice and not young then they do not visit the rabbit.
((("someone" "is" "nice" "+") ("someone" "is" "young" "~")) -> ("someone" "visits" "rabbit" "-"))
If someone is blue then they chase the bear.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "bear" "+"))
If someone is nice then they chase the rabbit.
((("someone" "is" "nice" "+")) -> ("someone" "chases" "rabbit" "+"))
If the bear chases the rabbit and the rabbit chases the bear then the rabbit is nice.
((("bear" "chases" "rabbit" "+") ("rabbit" "chases" "bear" "+")) -> ("rabbit" "is" "nice" "+"))
If someone needs the rabbit and they do not visit the rabbit then they need the bear.
((("someone" "needs" "rabbit" "+") ("someone" "visits" "rabbit" "~")) -> ("someone" "needs" "bear" "+"))
If someone chases the bear and the bear does not chase the rabbit then the bear is not red.
((("someone" "chases" "bear" "+") ("bear" "chases" "rabbit" "~")) -> ("bear" "is" "red" "-"))
The bear is cold.
True
1
proof
[(triple3)]
("bear" "is" "cold" "+")
triple3
The rabbit does not need the bear.
False
1
inv-proof
[(triple11)]
("rabbit" "needs" "bear" "-")
triple11
The bear chases the bear.
True
2
proof
[(((triple2) -> rule2))]
("bear" "chases" "bear" "+")
((triple2) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The rabbit is not nice.
False
3
inv-proof
[(((triple1 triple9) -> rule4) OR ((((triple4) -> rule3) triple9) -> rule4))]
("rabbit" "is" "nice" "-")
((triple1 triple9) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((((triple4) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
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 bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The bear chases the rabbit.[(triple1 OR ((triple4) -> rule3))] The bear is blue.[(triple2)] The bear is cold.[(triple3)] The bear is nice.[(triple4)] The bear is red.[(triple5)] The bear is young.[(triple6)] The bear needs the rabbit.[(triple7)] The bear visits the rabbit.[(triple8)] The rabbit chases the bear.[(triple9)] The rabbit does not visit the bear.[(triple12)] The rabbit is not cold.[(triple10)] The rabbit needs the bear.[(triple11)] @1: The bear chases the bear.[(((triple2) -> rule2))] The rabbit is nice.[(((triple1 triple9) -> rule4) OR ((((triple4) -> rule3) triple9) -> rule4))] @2: The rabbit chases the rabbit.[(((((triple1 triple9) -> rule4)) -> rule3) OR ((((((triple4) -> rule3) triple9) -> rule4)) -> rule3))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
((triple4) -> (rule3 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
triple5
The bear is young.
("bear" "is" "young" "+")
triple6
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple7
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple8
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple9
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
triple12
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple10
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple11
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple2) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple1 triple9) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((((triple4) -> (rule3 % int2)) triple9) -> (rule4 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple1 triple9) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
((((((triple4) -> (rule3 % int3)) triple9) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3