The bear chases the cat. The bear is rough. The bear does not need the cow. The cat chases the bear. The cat does not chase the mouse. The cat needs the cow. The cow does not chase the mouse. The cow does not need the cat. The cow sees the mouse. The mouse is big. The mouse does not need the cow. The mouse sees the cat. If something is red and green then it does not chase the bear. If something chases the bear then the bear does not see the mouse. If something chases the cow then the cow does not see the cat.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear does not need the cow.
("bear" "needs" "cow" "-")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
The cow does not need the cat.
("cow" "needs" "cat" "-")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If something is red and green then it does not chase the bear.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "chases" "bear" "-"))
If something chases the bear then the bear does not see the mouse.
((("something" "chases" "bear" "+")) -> ("bear" "sees" "mouse" "-"))
If something chases the cow then the cow does not see the cat.
((("something" "chases" "cow" "+")) -> ("cow" "sees" "cat" "-"))
The mouse sees the cat.
True
1
proof
[(triple12)]
("mouse" "sees" "cat" "+")
triple12
The cat does not chase the bear.
False
1
inv-proof
[(triple4)]
("cat" "chases" "bear" "-")
triple4
The bear does not see the mouse.
True
2
proof
[(((triple4) -> rule2))]
("bear" "sees" "mouse" "-")
((triple4) -> (rule2 % int1))
The bear does not see the mouse.
("bear" "sees" "mouse" "-")
int1
The bear sees the mouse.
False
2
inv-proof
[(((triple4) -> rule2))]
("bear" "sees" "mouse" "+")
((triple4) -> (rule2 % int1))
The bear does not see the mouse.
("bear" "sees" "mouse" "-")
int1
The bear does not chase the cow.
Unknown
inv-random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "-")
The cat sees the cow.
Unknown
random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cow sees the bear.
Unknown
random
[@0: The cow sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bear" "+")
@0: The bear chases the cat.[(triple1)] The bear does not need the cow.[(triple3)] The bear is rough.[(triple2)] The cat chases the bear.[(triple4)] The cat does not chase the mouse.[(triple5)] The cat needs the cow.[(triple6)] The cow does not chase the mouse.[(triple7)] The cow does not need the cat.[(triple8)] The cow sees the mouse.[(triple9)] The mouse does not need the cow.[(triple11)] The mouse is big.[(triple10)] The mouse sees the cat.[(triple12)] @1: The bear does not see the mouse.[(((triple4) -> rule2))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear does not need the cow.
("bear" "needs" "cow" "-")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple2
The cat chases the bear.
("cat" "chases" "bear" "+")
triple4
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple5
The cat needs the cow.
("cat" "needs" "cow" "+")
triple6
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
triple7
The cow does not need the cat.
("cow" "needs" "cat" "-")
triple8
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple9
The mouse does not need the cow.
("mouse" "needs" "cow" "-")
triple11
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple12
The bear does not see the mouse.
("bear" "sees" "mouse" "-")
((triple4) -> (rule2 % int1))
The bear does not see the mouse.
("bear" "sees" "mouse" "-")
int1