The bear is blue. The bear needs the rabbit. The rabbit is nice. If the bear visits the rabbit then the rabbit visits the bear. If someone is cold then they need the bear. If the bear needs the rabbit then the rabbit is round. If the rabbit visits the bear then the bear visits the rabbit. If someone visits the bear and the bear needs the rabbit then the bear is round. If someone is round then they visit the bear.
The bear is blue.
("bear" "is" "blue" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
If the bear visits the rabbit then the rabbit visits the bear.
((("bear" "visits" "rabbit" "+")) -> ("rabbit" "visits" "bear" "+"))
If someone is cold then they need the bear.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "bear" "+"))
If the bear needs the rabbit then the rabbit is round.
((("bear" "needs" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If the rabbit visits the bear then the bear visits the rabbit.
((("rabbit" "visits" "bear" "+")) -> ("bear" "visits" "rabbit" "+"))
If someone visits the bear and the bear needs the rabbit then the bear is round.
((("someone" "visits" "bear" "+") ("bear" "needs" "rabbit" "+")) -> ("bear" "is" "round" "+"))
If someone is round then they visit the bear.
((("someone" "is" "round" "+")) -> ("someone" "visits" "bear" "+"))
The bear is blue.
True
1
proof
[(triple1)]
("bear" "is" "blue" "+")
triple1
The rabbit is not nice.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "nice" "-")
triple3
The rabbit is round.
True
2
proof
[(((triple2) -> rule3))]
("rabbit" "is" "round" "+")
((triple2) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "is" "round" "-")
((triple2) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit visits the bear.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("rabbit" "visits" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit does not visit the bear.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("rabbit" "visits" "bear" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The bear is round.
True
5
proof
[(((((((triple2) -> rule3)) -> rule6) triple2) -> rule5))]
("bear" "is" "round" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple2) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The bear does not visit the rabbit.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule4))]
("bear" "visits" "rabbit" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "bear" "-")
The rabbit needs the bear.
Unknown
rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear likes the rabbit.
Unknown
random
[@0: The bear likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "rabbit" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The rabbit likes the bear.
Unknown
random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The bear is blue.[(triple1)] The bear needs the rabbit.[(triple2)] The rabbit is nice.[(triple3)] @1: The rabbit is round.[(((triple2) -> rule3))] @2: The rabbit visits the bear.[(((((triple2) -> rule3)) -> rule6))] @3: The bear is round.[(((((((triple2) -> rule3)) -> rule6) triple2) -> rule5))] The bear visits the rabbit.[(((((((triple2) -> rule3)) -> rule6)) -> rule4))] @4: The bear visits the bear.[(((((((((triple2) -> rule3)) -> rule6) triple2) -> rule5)) -> rule6))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
((triple2) -> (rule3 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The bear is round.
("bear" "is" "round" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple2) -> (rule5 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
int1
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The bear visits the bear.
("bear" "visits" "bear" "+")
((((((((triple2) -> (rule3 % int4))) -> (rule6 % int3)) triple2) -> (rule5 % int2))) -> (rule6 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4