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