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