The bear chases the cow. The bear is big. The bear sees the mouse. The cow chases the bear. The cow is blue. The cow sees the lion. The cow visits the mouse. The lion is kind. The lion is red. The mouse chases the cow. The mouse is big. The mouse sees the cow. If the lion is kind and the lion is red then the lion chases the mouse.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear is big.
("bear" "is" "big" "+")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If the lion is kind and the lion is red then the lion chases the mouse.
((("lion" "is" "kind" "+") ("lion" "is" "red" "+")) -> ("lion" "chases" "mouse" "+"))
The cow chases the bear.
True
1
proof
[(triple4)]
("cow" "chases" "bear" "+")
triple4
The mouse does not chase the cow.
False
1
inv-proof
[(triple10)]
("mouse" "chases" "cow" "-")
triple10
The lion chases the mouse.
True
3
proof
[(((triple8 triple9) -> rule1))]
("lion" "chases" "mouse" "+")
((triple8 triple9) -> (rule1 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion does not chase the mouse.
False
3
inv-proof
[(((triple8 triple9) -> rule1))]
("lion" "chases" "mouse" "-")
((triple8 triple9) -> (rule1 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The mouse does not visit the lion.
Unknown
inv-random
[@0: The mouse visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "lion" "-")
The lion visits the cow.
Unknown
random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "+")
@0: The bear chases the cow.[(triple1)] The bear is big.[(triple2)] The bear sees the mouse.[(triple3)] The cow chases the bear.[(triple4)] The cow is blue.[(triple5)] The cow sees the lion.[(triple6)] The cow visits the mouse.[(triple7)] The lion is kind.[(triple8)] The lion is red.[(triple9)] The mouse chases the cow.[(triple10)] The mouse is big.[(triple11)] The mouse sees the cow.[(triple12)] @1: The lion chases the mouse.[(((triple8 triple9) -> rule1))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple3
The cow chases the bear.
("cow" "chases" "bear" "+")
triple4
The cow is blue.
("cow" "is" "blue" "+")
triple5
The cow sees the lion.
("cow" "sees" "lion" "+")
triple6
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple7
The lion is kind.
("lion" "is" "kind" "+")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple10
The mouse is big.
("mouse" "is" "big" "+")
triple11
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple12
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((triple8 triple9) -> (rule1 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1