The bear eats the cow. The bear is blue. The bear needs the cat. The bear sees the lion. The cat needs the cow. The cat sees the bear. The cow eats the cat. The cow is round. The cow needs the bear. The cow sees the bear. The cow sees the cat. The lion eats the bear. The lion eats the cat. The lion is blue. The lion sees the cat. If the cow eats the cat and the cat is rough then the cow sees the cat. If something sees the bear and the bear eats the cow then it eats the cat. If something sees the cow and the cow eats the bear then the cow eats the lion. If something sees the bear then the bear needs the cow. If the lion is round then the lion sees the bear. If something is nice then it needs the cow. If something sees the bear and the bear eats the cat then it eats the cat. If something eats the bear and the bear needs the cow then it is nice.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If the cow eats the cat and the cat is rough then the cow sees the cat.
((("cow" "eats" "cat" "+") ("cat" "is" "rough" "+")) -> ("cow" "sees" "cat" "+"))
If something sees the bear and the bear eats the cow then it eats the cat.
((("something" "sees" "bear" "+") ("bear" "eats" "cow" "+")) -> ("something" "eats" "cat" "+"))
If something sees the cow and the cow eats the bear then the cow eats the lion.
((("something" "sees" "cow" "+") ("cow" "eats" "bear" "+")) -> ("cow" "eats" "lion" "+"))
If something sees the bear then the bear needs the cow.
((("something" "sees" "bear" "+")) -> ("bear" "needs" "cow" "+"))
If the lion is round then the lion sees the bear.
((("lion" "is" "round" "+")) -> ("lion" "sees" "bear" "+"))
If something is nice then it needs the cow.
((("something" "is" "nice" "+")) -> ("something" "needs" "cow" "+"))
If something sees the bear and the bear eats the cat then it eats the cat.
((("something" "sees" "bear" "+") ("bear" "eats" "cat" "+")) -> ("something" "eats" "cat" "+"))
If something eats the bear and the bear needs the cow then it is nice.
((("something" "eats" "bear" "+") ("bear" "needs" "cow" "+")) -> ("something" "is" "nice" "+"))
The lion eats the cat.
True
1
proof
[(triple13)]
("lion" "eats" "cat" "+")
triple13
The cow is not round.
False
1
inv-proof
[(triple8)]
("cow" "is" "round" "-")
triple8
The cat eats the cat.
True
3
proof
[(((triple6 triple1) -> rule2))]
("cat" "eats" "cat" "+")
((triple6 triple1) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The bear does not need the cow.
False
2
inv-proof
[(((triple10) -> rule4) OR ((triple6) -> rule4))]
("bear" "needs" "cow" "-")
((triple10) -> (rule4 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
((triple6) -> (rule4 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The lion is nice.
True
4
proof
[(((triple12 ((triple10) -> rule4)) -> rule8) OR ((triple12 ((triple6) -> rule4)) -> rule8))]
("lion" "is" "nice" "+")
((triple12 ((triple10) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
((triple12 ((triple6) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The lion is not nice.
False
4
inv-proof
[(((triple12 ((triple10) -> rule4)) -> rule8) OR ((triple12 ((triple6) -> rule4)) -> rule8))]
("lion" "is" "nice" "-")
((triple12 ((triple10) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
((triple12 ((triple6) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The lion needs the cow.
True
5
proof
[(((((triple12 ((triple10) -> rule4)) -> rule8)) -> rule6) OR ((((triple12 ((triple6) -> rule4)) -> rule8)) -> rule6))]
("lion" "needs" "cow" "+")
((((triple12 ((triple10) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
((((triple12 ((triple6) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The lion does not need the cow.
False
5
inv-proof
[(((((triple12 ((triple10) -> rule4)) -> rule8)) -> rule6) OR ((((triple12 ((triple6) -> rule4)) -> rule8)) -> rule6))]
("lion" "needs" "cow" "-")
((((triple12 ((triple10) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
((((triple12 ((triple6) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "nice" "-")
The bear eats the cat.
Unknown
rconc
[@1: The bear eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "cat" "+")
The cow does not eat the lion.
Unknown
inv-rconc
[@1: The cow eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "eats" "lion" "-")
The cat is nice.
Unknown
rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "nice" "+")
The bear does not need the lion.
Unknown
inv-random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "-")
The bear eats the lion.
Unknown
random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "+")
The lion does not need the cat.
Unknown
inv-random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The bear eats the cow.[(triple1)] The bear is blue.[(triple2)] The bear needs the cat.[(triple3)] The bear sees the lion.[(triple4)] The cat needs the cow.[(triple5)] The cat sees the bear.[(triple6)] The cow eats the cat.[(triple7 OR ((triple10 triple1) -> rule2))] The cow is round.[(triple8)] The cow needs the bear.[(triple9)] The cow sees the bear.[(triple10)] The cow sees the cat.[(triple11)] The lion eats the bear.[(triple12)] The lion eats the cat.[(triple13)] The lion is blue.[(triple14)] The lion sees the cat.[(triple15)] @1: The bear needs the cow.[(((triple10) -> rule4) OR ((triple6) -> rule4))] The cat eats the cat.[(((triple6 triple1) -> rule2))] @2: The lion is nice.[(((triple12 ((triple10) -> rule4)) -> rule8) OR ((triple12 ((triple6) -> rule4)) -> rule8))] @3: The lion needs the cow.[(((((triple12 ((triple10) -> rule4)) -> rule8)) -> rule6) OR ((((triple12 ((triple6) -> rule4)) -> rule8)) -> rule6))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear needs the cat.
("bear" "needs" "cat" "+")
triple3
The bear sees the lion.
("bear" "sees" "lion" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
The cat sees the bear.
("cat" "sees" "bear" "+")
triple6
The cow eats the cat.
("cow" "eats" "cat" "+")
triple7
((triple10 triple1) -> (rule2 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple8
The cow needs the bear.
("cow" "needs" "bear" "+")
triple9
The cow sees the bear.
("cow" "sees" "bear" "+")
triple10
The cow sees the cat.
("cow" "sees" "cat" "+")
triple11
The lion eats the bear.
("lion" "eats" "bear" "+")
triple12
The lion eats the cat.
("lion" "eats" "cat" "+")
triple13
The lion is blue.
("lion" "is" "blue" "+")
triple14
The lion sees the cat.
("lion" "sees" "cat" "+")
triple15
The bear needs the cow.
("bear" "needs" "cow" "+")
((triple10) -> (rule4 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
((triple6) -> (rule4 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple6 triple1) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((triple12 ((triple10) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
((triple12 ((triple6) -> (rule4 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
((((triple12 ((triple10) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3
((((triple12 ((triple6) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The bear needs the cow.
("bear" "needs" "cow" "+")
int3