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