The bear is nice. The bear sees the cat. The bear visits the cat. The cat does not chase the bear. The cat is big. The cat is blue. The cat is cold. The cat is rough. The cat sees the bear. The cat visits the bear. If someone visits the cat then they see the cat. If someone sees the cat and the cat visits the bear then they chase the cat. If someone visits the cat and they do not chase the bear then the bear is nice.
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat does not chase the bear.
("cat" "chases" "bear" "-")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If someone visits the cat then they see the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone sees the cat and the cat visits the bear then they chase the cat.
((("someone" "sees" "cat" "+") ("cat" "visits" "bear" "+")) -> ("someone" "chases" "cat" "+"))
If someone visits the cat and they do not chase the bear then the bear is nice.
((("someone" "visits" "cat" "+") ("someone" "chases" "bear" "~")) -> ("bear" "is" "nice" "+"))
The bear sees the cat.
True
1
proof
[(triple2 OR ((triple3) -> rule1))]
("bear" "sees" "cat" "+")
triple2
((triple3) -> (rule1 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The cat is not cold.
False
1
inv-proof
[(triple7)]
("cat" "is" "cold" "-")
triple7
The bear chases the cat.
True
3
proof
[(((triple2 triple10) -> rule2) OR ((((triple3) -> rule1) triple10) -> rule2))]
("bear" "chases" "cat" "+")
((triple2 triple10) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
((((triple3) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The bear does not chase the cat.
False
3
inv-proof
[(((triple2 triple10) -> rule2) OR ((((triple3) -> rule1) triple10) -> rule2))]
("bear" "chases" "cat" "-")
((triple2 triple10) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
((((triple3) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat chases the cat.
Unknown
rconc
[@2: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cat" "chases" "cat" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is nice.[(triple1)] The bear sees the cat.[(triple2 OR ((triple3) -> rule1))] The bear visits the cat.[(triple3)] The cat does not chase the bear.[(triple4)] The cat is big.[(triple5)] The cat is blue.[(triple6)] The cat is cold.[(triple7)] The cat is rough.[(triple8)] The cat sees the bear.[(triple9)] The cat visits the bear.[(triple10)] @1: The bear chases the cat.[(((triple2 triple10) -> rule2) OR ((((triple3) -> rule1) triple10) -> rule2))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear sees the cat.
("bear" "sees" "cat" "+")
triple2
((triple3) -> (rule1 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The cat does not chase the bear.
("cat" "chases" "bear" "-")
triple4
The cat is big.
("cat" "is" "big" "+")
triple5
The cat is blue.
("cat" "is" "blue" "+")
triple6
The cat is cold.
("cat" "is" "cold" "+")
triple7
The cat is rough.
("cat" "is" "rough" "+")
triple8
The cat sees the bear.
("cat" "sees" "bear" "+")
triple9
The cat visits the bear.
("cat" "visits" "bear" "+")
triple10
The bear chases the cat.
("bear" "chases" "cat" "+")
((triple2 triple10) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
((((triple3) -> (rule1 % int2)) triple10) -> (rule2 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2