The bear needs the cat. The bear sees the cat. The cat chases the bear. If someone needs the cat then they are cold. If someone sees the cat and they chase the bear then the bear is kind. If someone sees the bear and they are red then they need the cat. If someone sees the cat then the cat sees the bear. If someone sees the bear then they need the bear. If someone sees the bear and the bear chases the cat then they need the cat.
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
If someone needs the cat then they are cold.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the cat and they chase the bear then the bear is kind.
((("someone" "sees" "cat" "+") ("someone" "chases" "bear" "+")) -> ("bear" "is" "kind" "+"))
If someone sees the bear and they are red then they need the cat.
((("someone" "sees" "bear" "+") ("someone" "is" "red" "+")) -> ("someone" "needs" "cat" "+"))
If someone sees the cat then the cat sees the bear.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "bear" "+"))
If someone sees the bear then they need the bear.
((("someone" "sees" "bear" "+")) -> ("someone" "needs" "bear" "+"))
If someone sees the bear and the bear chases the cat then they need the cat.
((("someone" "sees" "bear" "+") ("bear" "chases" "cat" "+")) -> ("someone" "needs" "cat" "+"))
The cat chases the bear.
True
1
proof
[(triple3)]
("cat" "chases" "bear" "+")
triple3
The cat does not chase the bear.
False
1
inv-proof
[(triple3)]
("cat" "chases" "bear" "-")
triple3
The cat sees the bear.
True
2
proof
[(((triple2) -> rule4))]
("cat" "sees" "bear" "+")
((triple2) -> (rule4 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The bear is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "cold" "-")
((triple1) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "kind" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "needs" "bear" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
@0: The bear needs the cat.[(triple1)] The bear sees the cat.[(triple2)] The cat chases the bear.[(triple3)] @1: The bear is cold.[(((triple1) -> rule1))] The cat sees the bear.[(((triple2) -> rule4))] @2: The cat needs the bear.[(((((triple2) -> rule4)) -> rule5))]
The bear needs the cat.
("bear" "needs" "cat" "+")
triple1
The bear sees the cat.
("bear" "sees" "cat" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple3
The bear is cold.
("bear" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
((triple2) -> (rule4 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat needs the bear.
("cat" "needs" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat sees the bear.
("cat" "sees" "bear" "+")
int2