The bear is green. The cow sees the lion. The lion chases the bear. If someone chases the bear then the bear needs the lion. If the cow needs the bear and the bear needs the cow then the bear sees the cow. If someone chases the bear and the bear needs the lion then the bear is nice.
The bear is green.
("bear" "is" "green" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
If someone chases the bear then the bear needs the lion.
((("someone" "chases" "bear" "+")) -> ("bear" "needs" "lion" "+"))
If the cow needs the bear and the bear needs the cow then the bear sees the cow.
((("cow" "needs" "bear" "+") ("bear" "needs" "cow" "+")) -> ("bear" "sees" "cow" "+"))
If someone chases the bear and the bear needs the lion then the bear is nice.
((("someone" "chases" "bear" "+") ("bear" "needs" "lion" "+")) -> ("bear" "is" "nice" "+"))
The lion chases the bear.
True
1
proof
[(triple3)]
("lion" "chases" "bear" "+")
triple3
The cow does not see the lion.
False
1
inv-proof
[(triple2)]
("cow" "sees" "lion" "-")
triple2
The bear needs the lion.
True
2
proof
[(((triple3) -> rule1))]
("bear" "needs" "lion" "+")
((triple3) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear does not need the lion.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "needs" "lion" "-")
((triple3) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is nice.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("bear" "is" "nice" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is not nice.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule3))]
("bear" "is" "nice" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear does not see the cow.
Unknown
inv-rconc
[@1: The bear sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "cow" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The cow does not need the lion.
Unknown
inv-random
[@0: The cow needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "lion" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The bear is green.[(triple1)] The cow sees the lion.[(triple2)] The lion chases the bear.[(triple3)] @1: The bear needs the lion.[(((triple3) -> rule1))] @2: The bear is nice.[(((triple3 ((triple3) -> rule1)) -> rule3))]
The bear is green.
("bear" "is" "green" "+")
triple1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple2
The lion chases the bear.
("lion" "chases" "bear" "+")
triple3
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple3) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2