The bear is green. The bear is young. The bear sees the cow. The bear sees the lion. The cow eats the lion. The cow is cold. The cow sees the bear. The cow sees the lion. The lion eats the bear. The lion likes the bear. The lion likes the cow. The lion sees the bear. If someone eats the lion and the lion is round then the lion sees the bear. If someone sees the lion and the lion eats the cow then they eat the cow. If someone is kind and they see the cow then they like the cow. If someone likes the bear then the bear is kind. If someone is young and cold then they eat the bear. If someone eats the bear then the bear sees the cow. If someone eats the cow then they see the cow. If someone sees the lion and they are young then the lion likes the cow.
The bear is green.
("bear" "is" "green" "+")
The bear is young.
("bear" "is" "young" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If someone eats the lion and the lion is round then the lion sees the bear.
((("someone" "eats" "lion" "+") ("lion" "is" "round" "+")) -> ("lion" "sees" "bear" "+"))
If someone sees the lion and the lion eats the cow then they eat the cow.
((("someone" "sees" "lion" "+") ("lion" "eats" "cow" "+")) -> ("someone" "eats" "cow" "+"))
If someone is kind and they see the cow then they like the cow.
((("someone" "is" "kind" "+") ("someone" "sees" "cow" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the bear then the bear is kind.
((("someone" "likes" "bear" "+")) -> ("bear" "is" "kind" "+"))
If someone is young and cold then they eat the bear.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the bear then the bear sees the cow.
((("someone" "eats" "bear" "+")) -> ("bear" "sees" "cow" "+"))
If someone eats the cow then they see the cow.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone sees the lion and they are young then the lion likes the cow.
((("someone" "sees" "lion" "+") ("someone" "is" "young" "+")) -> ("lion" "likes" "cow" "+"))
The lion sees the bear.
True
1
proof
[(triple12)]
("lion" "sees" "bear" "+")
triple12
The bear is not young.
False
1
inv-proof
[(triple2)]
("bear" "is" "young" "-")
triple2
The bear is kind.
True
2
proof
[(((triple10) -> rule4))]
("bear" "is" "kind" "+")
((triple10) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple10) -> rule4))]
("bear" "is" "kind" "-")
((triple10) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear likes the cow.
True
4
proof
[(((((triple10) -> rule4) triple3) -> rule3) OR ((((triple10) -> rule4) ((triple9) -> rule6)) -> rule3))]
("bear" "likes" "cow" "+")
((((triple10) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The bear does not like the cow.
False
4
inv-proof
[(((((triple10) -> rule4) triple3) -> rule3) OR ((((triple10) -> rule4) ((triple9) -> rule6)) -> rule3))]
("bear" "likes" "cow" "-")
((((triple10) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "bear" "-")
The cow sees the cow.
Unknown
rconc
[@2: The cow sees the cow.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("cow" "sees" "cow" "+")
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cow" "-")
The bear likes the lion.
Unknown
random
[@0: The bear likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "lion" "+")
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 cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The bear is green.[(triple1)] The bear is young.[(triple2)] The bear sees the cow.[(triple3 OR ((triple9) -> rule6))] The bear sees the lion.[(triple4)] The cow eats the lion.[(triple5)] The cow is cold.[(triple6)] The cow sees the bear.[(triple7)] The cow sees the lion.[(triple8)] The lion eats the bear.[(triple9)] The lion likes the bear.[(triple10)] The lion likes the cow.[(triple11 OR ((triple4 triple2) -> rule8))] The lion sees the bear.[(triple12)] @1: The bear is kind.[(((triple10) -> rule4))] @2: The bear likes the cow.[(((((triple10) -> rule4) triple3) -> rule3) OR ((((triple10) -> rule4) ((triple9) -> rule6)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear sees the cow.
("bear" "sees" "cow" "+")
triple3
((triple9) -> (rule6 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The bear sees the lion.
("bear" "sees" "lion" "+")
triple4
The cow eats the lion.
("cow" "eats" "lion" "+")
triple5
The cow is cold.
("cow" "is" "cold" "+")
triple6
The cow sees the bear.
("cow" "sees" "bear" "+")
triple7
The cow sees the lion.
("cow" "sees" "lion" "+")
triple8
The lion eats the bear.
("lion" "eats" "bear" "+")
triple9
The lion likes the bear.
("lion" "likes" "bear" "+")
triple10
The lion likes the cow.
("lion" "likes" "cow" "+")
triple11
((triple4 triple2) -> (rule8 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
triple12
The bear is kind.
("bear" "is" "kind" "+")
((triple10) -> (rule4 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear likes the cow.
("bear" "likes" "cow" "+")
((((triple10) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((triple10) -> (rule4 % int3)) ((triple9) -> (rule6 % int2))) -> (rule3 % int1))
The bear likes the cow.
("bear" "likes" "cow" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3