The bear is round. The cat chases the bear. The lion is kind. Young, red people are round. If someone is round then they visit the lion. If someone visits the bear then the bear chases the cat. If the cat needs the bear then the bear is kind. If someone is blue then they visit the lion. If someone visits the lion then they are young. If someone needs the cat and the cat needs the lion then the cat chases the lion. If the bear needs the cat then the bear is blue.
The bear is round.
("bear" "is" "round" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The lion is kind.
("lion" "is" "kind" "+")
Young, red people are round.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they visit the lion.
((("someone" "is" "round" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the bear then the bear chases the cat.
((("someone" "visits" "bear" "+")) -> ("bear" "chases" "cat" "+"))
If the cat needs the bear then the bear is kind.
((("cat" "needs" "bear" "+")) -> ("bear" "is" "kind" "+"))
If someone is blue then they visit the lion.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the lion then they are young.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "young" "+"))
If someone needs the cat and the cat needs the lion then the cat chases the lion.
((("someone" "needs" "cat" "+") ("cat" "needs" "lion" "+")) -> ("cat" "chases" "lion" "+"))
If the bear needs the cat then the bear is blue.
((("bear" "needs" "cat" "+")) -> ("bear" "is" "blue" "+"))
The lion is kind.
True
1
proof
[(triple3)]
("lion" "is" "kind" "+")
triple3
The bear is not round.
False
1
inv-proof
[(triple1)]
("bear" "is" "round" "-")
triple1
The bear visits the lion.
True
2
proof
[(((triple1) -> rule2))]
("bear" "visits" "lion" "+")
((triple1) -> (rule2 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear does not visit the lion.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "visits" "lion" "-")
((triple1) -> (rule2 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("bear" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The bear is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("bear" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The cat is not young.
Unknown
inv-rconc
[@3: The cat is young.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule1 <- FAIL)]]
("cat" "is" "young" "-")
The bear chases the cat.
Unknown
rconc
[@1: The bear chases the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "cat" "+")
The cat does not visit the lion.
Unknown
inv-rconc
[@2: The cat visits the lion.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "visits" "lion" "-")
The lion needs the cat.
Unknown
random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The lion needs the bear.
Unknown
random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "+")
@0: The bear is round.[(triple1)] The cat chases the bear.[(triple2)] The lion is kind.[(triple3)] @1: The bear visits the lion.[(((triple1) -> rule2))] @2: The bear is young.[(((((triple1) -> rule2)) -> rule6))]
The bear is round.
("bear" "is" "round" "+")
triple1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The bear visits the lion.
("bear" "visits" "lion" "+")
((triple1) -> (rule2 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear is young.
("bear" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2