The bear eats the cow. The bear eats the rabbit. The bear is green. The bear is rough. The bear likes the rabbit. The bear does not see the cow. The cow eats the bear. The cow is kind. The cow is rough. The cow likes the bear. The cow sees the bear. The rabbit is rough. The rabbit likes the bear. The rabbit does not like the cow. The rabbit sees the cow. If someone eats the bear and the bear sees the rabbit then they eat the rabbit. If someone is kind then they see the bear. If someone sees the bear then the bear is kind.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear does not see the cow.
("bear" "sees" "cow" "-")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If someone eats the bear and the bear sees the rabbit then they eat the rabbit.
((("someone" "eats" "bear" "+") ("bear" "sees" "rabbit" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is kind then they see the bear.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the bear then the bear is kind.
((("someone" "sees" "bear" "+")) -> ("bear" "is" "kind" "+"))
The cow is kind.
True
1
proof
[(triple8)]
("cow" "is" "kind" "+")
triple8
The rabbit likes the cow.
False
1
inv-proof
[(triple14)]
("rabbit" "likes" "cow" "+")
triple14
The bear is kind.
True
2
proof
[(((triple11) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("bear" "is" "kind" "+")
((triple11) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
int2
The bear is not kind.
False
2
inv-proof
[(((triple11) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("bear" "is" "kind" "-")
((triple11) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
int2
The bear sees the bear.
True
3
proof
[(((((triple11) -> rule3)) -> rule2) OR ((((((triple8) -> rule2)) -> rule3)) -> rule2))]
("bear" "sees" "bear" "+")
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The cow sees the bear.
("cow" "sees" "bear" "+")
int3
The bear does not see the bear.
False
3
inv-proof
[(((((triple11) -> rule3)) -> rule2) OR ((((((triple8) -> rule2)) -> rule3)) -> rule2))]
("bear" "sees" "bear" "-")
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The cow sees the bear.
("cow" "sees" "bear" "+")
int3
The rabbit does not see the bear.
Unknown
inv-rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "bear" "-")
The rabbit eats the rabbit.
Unknown
rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "rabbit" "+")
The cow does not eat the rabbit.
Unknown
inv-rconc
[@1: The cow eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "eats" "rabbit" "-")
The cow likes the rabbit.
Unknown
random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The bear does not see the cow.[(triple6)] The bear eats the cow.[(triple1)] The bear eats the rabbit.[(triple2)] The bear is green.[(triple3)] The bear is rough.[(triple4)] The bear likes the rabbit.[(triple5)] The cow eats the bear.[(triple7)] The cow is kind.[(triple8)] The cow is rough.[(triple9)] The cow likes the bear.[(triple10)] The cow sees the bear.[(triple11 OR ((triple8) -> rule2))] The rabbit does not like the cow.[(triple14)] The rabbit is rough.[(triple12)] The rabbit likes the bear.[(triple13)] The rabbit sees the cow.[(triple15)] @1: The bear is kind.[(((triple11) -> rule3) OR ((((triple8) -> rule2)) -> rule3))] @2: The bear sees the bear.[(((((triple11) -> rule3)) -> rule2) OR ((((((triple8) -> rule2)) -> rule3)) -> rule2))]
The bear does not see the cow.
("bear" "sees" "cow" "-")
triple6
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple5
The cow eats the bear.
("cow" "eats" "bear" "+")
triple7
The cow is kind.
("cow" "is" "kind" "+")
triple8
The cow is rough.
("cow" "is" "rough" "+")
triple9
The cow likes the bear.
("cow" "likes" "bear" "+")
triple10
The cow sees the bear.
("cow" "sees" "bear" "+")
triple11
((triple8) -> (rule2 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The rabbit does not like the cow.
("rabbit" "likes" "cow" "-")
triple14
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple13
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple15
The bear is kind.
("bear" "is" "kind" "+")
((triple11) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
((((triple11) -> (rule3 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The cow sees the bear.
("cow" "sees" "bear" "+")
int3