The bear chases the cat. The bear needs the cat. The bear visits the cat. The cat chases the bear. The cat is young. The cat needs the bear. The cat visits the bear. If something needs the cat then it is red. If something is young then it chases the bear. If something chases the bear then the bear is kind. If the bear visits the cat and the cat visits the bear then the cat is big. If the bear needs the cat then the cat needs the bear. If something is blue and kind then it needs the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If something needs the cat then it is red.
((("something" "needs" "cat" "+")) -> ("something" "is" "red" "+"))
If something is young then it chases the bear.
((("something" "is" "young" "+")) -> ("something" "chases" "bear" "+"))
If something chases the bear then the bear is kind.
((("something" "chases" "bear" "+")) -> ("bear" "is" "kind" "+"))
If the bear visits the cat and the cat visits the bear then the cat is big.
((("bear" "visits" "cat" "+") ("cat" "visits" "bear" "+")) -> ("cat" "is" "big" "+"))
If the bear needs the cat then the cat needs the bear.
((("bear" "needs" "cat" "+")) -> ("cat" "needs" "bear" "+"))
If something is blue and kind then it needs the bear.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "needs" "bear" "+"))
The cat is young.
True
1
proof
[(triple5)]
("cat" "is" "young" "+")
triple5
The bear does not visit the cat.
False
1
inv-proof
[(triple3)]
("bear" "visits" "cat" "-")
triple3
The bear is red.
True
2
proof
[(((triple2) -> rule1))]
("bear" "is" "red" "+")
((triple2) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple4) -> rule3) OR ((((triple5) -> rule2)) -> rule3))]
("bear" "is" "kind" "-")
((triple4) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The bear does not need the bear.
Unknown
inv-rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "bear" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "bear" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
@0: The bear chases the cat.[(triple1)] The bear needs the cat.[(triple2)] The bear visits the cat.[(triple3)] The cat chases the bear.[(triple4 OR ((triple5) -> rule2))] The cat is young.[(triple5)] The cat needs the bear.[(triple6 OR ((triple2) -> rule5))] The cat visits the bear.[(triple7)] @1: The bear is kind.[(((triple4) -> rule3) OR ((((triple5) -> rule2)) -> rule3))] The bear is red.[(((triple2) -> rule1))] The cat is big.[(((triple3 triple7) -> rule4))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear needs the cat.
("bear" "needs" "cat" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The cat chases the bear.
("cat" "chases" "bear" "+")
triple4
((triple5) -> (rule2 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat is young.
("cat" "is" "young" "+")
triple5
The cat needs the bear.
("cat" "needs" "bear" "+")
triple6
((triple2) -> (rule5 % int1))
The cat needs the bear.
("cat" "needs" "bear" "+")
int1
The cat visits the bear.
("cat" "visits" "bear" "+")
triple7
The bear is kind.
("bear" "is" "kind" "+")
((triple4) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
int2
The bear is red.
("bear" "is" "red" "+")
((triple2) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((triple3 triple7) -> (rule4 % int1))
The cat is big.
("cat" "is" "big" "+")
int1