The bear is green. The cow likes the rabbit. The rabbit likes the cow. The squirrel sees the bear. If someone likes the bear then they like the cow. If the bear is green then the bear likes the rabbit. If someone likes the rabbit then they chase the rabbit. If someone sees the bear and the bear chases the squirrel then the squirrel is round. If the bear is cold then the bear sees the rabbit. If someone is green and they chase the rabbit then the rabbit chases the squirrel.
The bear is green.
("bear" "is" "green" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
If someone likes the bear then they like the cow.
((("someone" "likes" "bear" "+")) -> ("someone" "likes" "cow" "+"))
If the bear is green then the bear likes the rabbit.
((("bear" "is" "green" "+")) -> ("bear" "likes" "rabbit" "+"))
If someone likes the rabbit then they chase the rabbit.
((("someone" "likes" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone sees the bear and the bear chases the squirrel then the squirrel is round.
((("someone" "sees" "bear" "+") ("bear" "chases" "squirrel" "+")) -> ("squirrel" "is" "round" "+"))
If the bear is cold then the bear sees the rabbit.
((("bear" "is" "cold" "+")) -> ("bear" "sees" "rabbit" "+"))
If someone is green and they chase the rabbit then the rabbit chases the squirrel.
((("someone" "is" "green" "+") ("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "squirrel" "+"))
The cow likes the rabbit.
True
1
proof
[(triple2)]
("cow" "likes" "rabbit" "+")
triple2
The cow does not like the rabbit.
False
1
inv-proof
[(triple2)]
("cow" "likes" "rabbit" "-")
triple2
The cow chases the rabbit.
True
2
proof
[(((triple2) -> rule3))]
("cow" "chases" "rabbit" "+")
((triple2) -> (rule3 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow does not chase the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "chases" "rabbit" "-")
((triple2) -> (rule3 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The bear chases the rabbit.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("bear" "chases" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The bear does not chase the rabbit.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("bear" "chases" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The rabbit chases the squirrel.
True
5
proof
[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule6))]
("rabbit" "chases" "squirrel" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int3
The rabbit does not chase the squirrel.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule6))]
("rabbit" "chases" "squirrel" "-")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int3
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "-")
The bear sees the rabbit.
Unknown
rconc
[@1: The bear sees the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "sees" "rabbit" "+")
The bear does not like the cow.
Unknown
inv-rconc
[@1: The bear likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "cow" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The cow sees the rabbit.
Unknown
random
[@0: The cow sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "rabbit" "+")
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The bear sees the squirrel.
Unknown
random
[@0: The bear sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "squirrel" "+")
@0: The bear is green.[(triple1)] The cow likes the rabbit.[(triple2)] The rabbit likes the cow.[(triple3)] The squirrel sees the bear.[(triple4)] @1: The bear likes the rabbit.[(((triple1) -> rule2))] The cow chases the rabbit.[(((triple2) -> rule3))] @2: The bear chases the rabbit.[(((((triple1) -> rule2)) -> rule3))] @3: The rabbit chases the squirrel.[(((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule6))]
The bear is green.
("bear" "is" "green" "+")
triple1
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple2
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple3
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple4
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
((triple1) -> (rule2 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((triple2) -> (rule3 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int3