The bear chases the cow. The bear is big. The bear is green. The bear is red. The bear is rough. The bear is round. The bear needs the cow. The bear visits the cow. The cow chases the bear. The cow is big. The cow is green. The cow is red. The cow is rough. The cow is round. The cow needs the bear. The cow visits the bear. If someone chases the cow then they are rough. If someone is big and they chase the cow then they are red. If someone is red then they chase the cow. If someone needs the cow then the cow needs the bear. If the bear needs the cow then the cow is round. If the cow needs the bear then the bear visits the cow.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
If someone chases the cow then they are rough.
((("someone" "chases" "cow" "+")) -> ("someone" "is" "rough" "+"))
If someone is big and they chase the cow then they are red.
((("someone" "is" "big" "+") ("someone" "chases" "cow" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they chase the cow.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cow" "+"))
If someone needs the cow then the cow needs the bear.
((("someone" "needs" "cow" "+")) -> ("cow" "needs" "bear" "+"))
If the bear needs the cow then the cow is round.
((("bear" "needs" "cow" "+")) -> ("cow" "is" "round" "+"))
If the cow needs the bear then the bear visits the cow.
((("cow" "needs" "bear" "+")) -> ("bear" "visits" "cow" "+"))
The cow needs the bear.
True
1
proof
[(triple15 OR ((triple7) -> rule4))]
("cow" "needs" "bear" "+")
triple15
((triple7) -> (rule4 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the bear.
False
1
inv-proof
[(triple15 OR ((triple7) -> rule4))]
("cow" "needs" "bear" "-")
triple15
((triple7) -> (rule4 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
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 cow.[(triple1 OR ((triple4) -> rule3))] The bear is big.[(triple2)] The bear is green.[(triple3)] The bear is red.[(triple4 OR ((triple2 triple1) -> rule2))] The bear is rough.[(triple5 OR ((triple1) -> rule1) OR ((((triple4) -> rule3)) -> rule1))] The bear is round.[(triple6)] The bear needs the cow.[(triple7)] The bear visits the cow.[(triple8 OR ((triple15) -> rule6) OR ((((triple7) -> rule4)) -> rule6))] The cow chases the bear.[(triple9)] The cow is big.[(triple10)] The cow is green.[(triple11)] The cow is red.[(triple12)] The cow is rough.[(triple13 OR ((((triple12) -> rule3)) -> rule1))] The cow is round.[(triple14 OR ((triple7) -> rule5))] The cow needs the bear.[(triple15 OR ((triple7) -> rule4))] The cow visits the bear.[(triple16)] @1: The cow chases the cow.[(((triple12) -> rule3))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
((triple4) -> (rule3 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear is red.
("bear" "is" "red" "+")
triple4
((triple2 triple1) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
triple5
((triple1) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear is round.
("bear" "is" "round" "+")
triple6
The bear needs the cow.
("bear" "needs" "cow" "+")
triple7
The bear visits the cow.
("bear" "visits" "cow" "+")
triple8
((triple15) -> (rule6 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
The bear visits the cow.
("bear" "visits" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow chases the bear.
("cow" "chases" "bear" "+")
triple9
The cow is big.
("cow" "is" "big" "+")
triple10
The cow is green.
("cow" "is" "green" "+")
triple11
The cow is red.
("cow" "is" "red" "+")
triple12
The cow is rough.
("cow" "is" "rough" "+")
triple13
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
triple14
((triple7) -> (rule5 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
triple15
((triple7) -> (rule4 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
triple16
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple12) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1