The bear is red. The bear visits the rabbit. The rabbit needs the bear. If someone visits the rabbit then they are red. If someone eats the rabbit then the rabbit does not visit the bear. If someone needs the bear then the bear eats the rabbit. If the bear does not visit the rabbit then the bear does not eat the rabbit. If the bear visits the rabbit then the rabbit is young. If the rabbit does not visit the bear then the rabbit eats the bear.
The bear is red.
("bear" "is" "red" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
If someone visits the rabbit then they are red.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "red" "+"))
If someone eats the rabbit then the rabbit does not visit the bear.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "visits" "bear" "-"))
If someone needs the bear then the bear eats the rabbit.
((("someone" "needs" "bear" "+")) -> ("bear" "eats" "rabbit" "+"))
If the bear does not visit the rabbit then the bear does not eat the rabbit.
((("bear" "visits" "rabbit" "~")) -> ("bear" "eats" "rabbit" "-"))
If the bear visits the rabbit then the rabbit is young.
((("bear" "visits" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If the rabbit does not visit the bear then the rabbit eats the bear.
((("rabbit" "visits" "bear" "~")) -> ("rabbit" "eats" "bear" "+"))
The bear visits the rabbit.
True
1
proof
[(triple2)]
("bear" "visits" "rabbit" "+")
triple2
The rabbit does not need the bear.
False
1
inv-proof
[(triple3)]
("rabbit" "needs" "bear" "-")
triple3
The rabbit is young.
True
2
proof
[(((triple2) -> rule5))]
("rabbit" "is" "young" "+")
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The bear does not eat the rabbit.
False
2
inv-proof
[(((triple3) -> rule3))]
("bear" "eats" "rabbit" "-")
((triple3) -> (rule3 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The rabbit does not visit the bear.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("rabbit" "visits" "bear" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The rabbit visits the bear.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("rabbit" "visits" "bear" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The rabbit eats the bear.
True
4
proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule6))]
("rabbit" "eats" "bear" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
The rabbit does not eat the bear.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule6))]
("rabbit" "eats" "bear" "-")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3
The rabbit is not red.
Unknown
inv-rconc
[@1: The rabbit is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "red" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear is red.[(triple1 OR ((triple2) -> rule1))] The bear visits the rabbit.[(triple2)] The rabbit needs the bear.[(triple3)] @1: The bear eats the rabbit.[(((triple3) -> rule3))] The rabbit is young.[(((triple2) -> rule5))] @2: The rabbit does not visit the bear.[(((((triple3) -> rule3)) -> rule2))] @3: The rabbit eats the bear.[(((((((triple3) -> rule3)) -> rule2)) -> rule6))]
The bear is red.
("bear" "is" "red" "+")
triple1
((triple2) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple2
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple3
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
((triple3) -> (rule3 % int1))
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int2
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit does not visit the bear.
("rabbit" "visits" "bear" "-")
int2
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
int3