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