The bear chases the rabbit. The rabbit chases the bear. If the rabbit is green and the rabbit chases the bear then the rabbit visits the bear. If the rabbit chases the bear then the rabbit is green. If something is kind then it visits the bear. All red, nice things are green. If something chases the rabbit then the rabbit chases the bear. If the bear is red and the bear chases the rabbit then the rabbit is kind.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
If the rabbit is green and the rabbit chases the bear then the rabbit visits the bear.
((("rabbit" "is" "green" "+") ("rabbit" "chases" "bear" "+")) -> ("rabbit" "visits" "bear" "+"))
If the rabbit chases the bear then the rabbit is green.
((("rabbit" "chases" "bear" "+")) -> ("rabbit" "is" "green" "+"))
If something is kind then it visits the bear.
((("something" "is" "kind" "+")) -> ("something" "visits" "bear" "+"))
All red, nice things are green.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something chases the rabbit then the rabbit chases the bear.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "bear" "+"))
If the bear is red and the bear chases the rabbit then the rabbit is kind.
((("bear" "is" "red" "+") ("bear" "chases" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
The bear chases the rabbit.
True
1
proof
[(triple1)]
("bear" "chases" "rabbit" "+")
triple1
The bear does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "chases" "rabbit" "-")
triple1
The rabbit is green.
True
2
proof
[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))]
("rabbit" "is" "green" "+")
((triple2) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is not green.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))]
("rabbit" "is" "green" "-")
((triple2) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit visits the bear.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule1) OR ((((triple2) -> rule2) ((triple1) -> rule5)) -> rule1) OR ((((((triple1) -> rule5)) -> rule2) triple2) -> rule1) OR ((((((triple1) -> rule5)) -> rule2) ((triple1) -> rule5)) -> rule1))]
("rabbit" "visits" "bear" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) ((triple1) -> (rule5 % int3))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit does not visit the bear.
False
4
inv-proof
[(((((triple2) -> rule2) triple2) -> rule1) OR ((((triple2) -> rule2) ((triple1) -> rule5)) -> rule1) OR ((((((triple1) -> rule5)) -> rule2) triple2) -> rule1) OR ((((((triple1) -> rule5)) -> rule2) ((triple1) -> rule5)) -> rule1))]
("rabbit" "visits" "bear" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) ((triple1) -> (rule5 % int3))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "visits" "bear" "-")
The bear is green.
Unknown
rconc
[@1: The bear is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "green" "+")
The rabbit is not kind.
Unknown
inv-rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "kind" "-")
The bear visits the rabbit.
Unknown
random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "+")
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 bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear chases the rabbit.[(triple1)] The rabbit chases the bear.[(triple2 OR ((triple1) -> rule5))] @1: The rabbit is green.[(((triple2) -> rule2) OR ((((triple1) -> rule5)) -> rule2))] @2: The rabbit visits the bear.[(((((triple2) -> rule2) triple2) -> rule1) OR ((((triple2) -> rule2) ((triple1) -> rule5)) -> rule1) OR ((((((triple1) -> rule5)) -> rule2) triple2) -> rule1) OR ((((((triple1) -> rule5)) -> rule2) ((triple1) -> rule5)) -> rule1))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple2
((triple1) -> (rule5 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple2) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
((((triple2) -> (rule2 % int3)) ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2)) ((triple1) -> (rule5 % int3))) -> (rule1 % int1))
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3