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