The bear chases the cat. The cat is not nice. The mouse chases the bear. If something needs the cat then it is nice. If something chases the cat then the cat does not need the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
If something needs the cat then it is nice.
((("something" "needs" "cat" "+")) -> ("something" "is" "nice" "+"))
If something chases the cat then the cat does not need the bear.
((("something" "chases" "cat" "+")) -> ("cat" "needs" "bear" "-"))
The mouse chases the bear.
True
1
proof
[(triple3)]
("mouse" "chases" "bear" "+")
triple3
The mouse does not chase the bear.
False
1
inv-proof
[(triple3)]
("mouse" "chases" "bear" "-")
triple3
The cat does not need the bear.
True
2
proof
[(((triple1) -> rule2))]
("cat" "needs" "bear" "-")
((triple1) -> (rule2 % int1))
The cat does not need the bear.
("cat" "needs" "bear" "-")
int1
The cat needs the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The cat does not need the bear.
("cat" "needs" "bear" "-")
int1
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "nice" "-")
The bear is nice.
Unknown
rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "nice" "+")
The cat is not big.
Unknown
inv-random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "-")
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 cat is not nice.[(triple2)] The mouse chases the bear.[(triple3)] @1: The cat does not need the bear.[(((triple1) -> rule2))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple3
The cat does not need the bear.
("cat" "needs" "bear" "-")
((triple1) -> (rule2 % int1))
The cat does not need the bear.
("cat" "needs" "bear" "-")
int1