The bear chases the cat. The bear is round. The cat sees the mouse. The cow is nice. The mouse chases the bear. The mouse sees the cow. The mouse visits the cow. If something is rough then it sees the bear. If the mouse sees the bear and the mouse chases the cow then the bear chases the cat. If something chases the cat and it is round then it is nice.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is round.
("bear" "is" "round" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is nice.
("cow" "is" "nice" "+")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something is rough then it sees the bear.
((("something" "is" "rough" "+")) -> ("something" "sees" "bear" "+"))
If the mouse sees the bear and the mouse chases the cow then the bear chases the cat.
((("mouse" "sees" "bear" "+") ("mouse" "chases" "cow" "+")) -> ("bear" "chases" "cat" "+"))
If something chases the cat and it is round then it is nice.
((("something" "chases" "cat" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
The cow is nice.
True
1
proof
[(triple4)]
("cow" "is" "nice" "+")
triple4
The cow is not nice.
False
1
inv-proof
[(triple4)]
("cow" "is" "nice" "-")
triple4
The bear is nice.
True
3
proof
[(((triple1 triple2) -> rule3))]
("bear" "is" "nice" "+")
((triple1 triple2) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is not nice.
False
3
inv-proof
[(((triple1 triple2) -> rule3))]
("bear" "is" "nice" "-")
((triple1 triple2) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The cow does not see the bear.
Unknown
inv-rconc
[@1: The cow sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "bear" "-")
The bear sees the bear.
Unknown
rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "bear" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The bear chases the cow.
Unknown
random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "+")
@0: The bear chases the cat.[(triple1)] The bear is round.[(triple2)] The cat sees the mouse.[(triple3)] The cow is nice.[(triple4)] The mouse chases the bear.[(triple5)] The mouse sees the cow.[(triple6)] The mouse visits the cow.[(triple7)] @1: The bear is nice.[(((triple1 triple2) -> rule3))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple5
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple6
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple7
The bear is nice.
("bear" "is" "nice" "+")
((triple1 triple2) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1