The bear is big. The cat is cold. The rabbit visits the cat. The tiger does not see the cat. If someone visits the cat then they do not chase the cat. If someone sees the tiger and they do not visit the bear then the bear does not visit the rabbit.
The bear is big.
("bear" "is" "big" "+")
The cat is cold.
("cat" "is" "cold" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
If someone visits the cat then they do not chase the cat.
((("someone" "visits" "cat" "+")) -> ("someone" "chases" "cat" "-"))
If someone sees the tiger and they do not visit the bear then the bear does not visit the rabbit.
((("someone" "sees" "tiger" "+") ("someone" "visits" "bear" "~")) -> ("bear" "visits" "rabbit" "-"))
The cat is cold.
True
1
proof
[(triple2)]
("cat" "is" "cold" "+")
triple2
The cat is not cold.
False
1
inv-proof
[(triple2)]
("cat" "is" "cold" "-")
triple2
The rabbit does not chase the cat.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "chases" "cat" "-")
((triple3) -> (rule1 % int1))
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
int1
The rabbit chases the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("rabbit" "chases" "cat" "+")
((triple3) -> (rule1 % int1))
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
int1
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The cat does not chase the bear.
Unknown
inv-random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "-")
The bear sees the rabbit.
Unknown
random
[@0: The bear sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "rabbit" "+")
@0: The bear is big.[(triple1)] The cat is cold.[(triple2)] The rabbit visits the cat.[(triple3)] The tiger does not see the cat.[(triple4)] @1: The rabbit does not chase the cat.[(((triple3) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple3
The tiger does not see the cat.
("tiger" "sees" "cat" "-")
triple4
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
((triple3) -> (rule1 % int1))
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
int1