The bear chases the cow. The bear eats the cow. The bear is nice. The bear needs the cow. The cow chases the bear. The cow is round. The cow needs the bear. If something is nice and it eats the cow then the cow chases the bear. If something eats the bear then it is red. If something eats the cow and it chases the bear then the cow needs the bear. If something chases the cow then it eats the bear. If something is round and it needs the bear then it eats the bear. If the bear eats the cow then the cow eats the bear.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
If something is nice and it eats the cow then the cow chases the bear.
((("something" "is" "nice" "+") ("something" "eats" "cow" "+")) -> ("cow" "chases" "bear" "+"))
If something eats the bear then it is red.
((("something" "eats" "bear" "+")) -> ("something" "is" "red" "+"))
If something eats the cow and it chases the bear then the cow needs the bear.
((("something" "eats" "cow" "+") ("something" "chases" "bear" "+")) -> ("cow" "needs" "bear" "+"))
If something chases the cow then it eats the bear.
((("something" "chases" "cow" "+")) -> ("something" "eats" "bear" "+"))
If something is round and it needs the bear then it eats the bear.
((("something" "is" "round" "+") ("something" "needs" "bear" "+")) -> ("something" "eats" "bear" "+"))
If the bear eats the cow then the cow eats the bear.
((("bear" "eats" "cow" "+")) -> ("cow" "eats" "bear" "+"))
The cow chases the bear.
True
1
proof
[(triple5 OR ((triple3 triple2) -> rule1))]
("cow" "chases" "bear" "+")
triple5
((triple3 triple2) -> (rule1 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The bear does not chase the cow.
False
1
inv-proof
[(triple1)]
("bear" "chases" "cow" "-")
triple1
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The bear chases the cow.[(triple1)] The bear eats the cow.[(triple2)] The bear is nice.[(triple3)] The bear needs the cow.[(triple4)] The cow chases the bear.[(triple5 OR ((triple3 triple2) -> rule1))] The cow is round.[(triple6)] The cow needs the bear.[(triple7)] @1: The bear eats the bear.[(((triple1) -> rule4))] The cow eats the bear.[(((triple2) -> rule6) OR ((triple6 triple7) -> rule5))] @2: The bear is red.[(((((triple1) -> rule4)) -> rule2))] The cow is red.[(((((triple2) -> rule6)) -> rule2) OR ((((triple6 triple7) -> rule5)) -> rule2))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear eats the cow.
("bear" "eats" "cow" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear needs the cow.
("bear" "needs" "cow" "+")
triple4
The cow chases the bear.
("cow" "chases" "bear" "+")
triple5
((triple3 triple2) -> (rule1 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is round.
("cow" "is" "round" "+")
triple6
The cow needs the bear.
("cow" "needs" "bear" "+")
triple7
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple1) -> (rule4 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
((triple2) -> (rule6 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
((triple6 triple7) -> (rule5 % int1))
The cow eats the bear.
("cow" "eats" "bear" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear eats the bear.
("bear" "eats" "bear" "+")
int2
The cow is red.
("cow" "is" "red" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2
((((triple6 triple7) -> (rule5 % int2))) -> (rule2 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow eats the bear.
("cow" "eats" "bear" "+")
int2