The bear chases the cow. The bear eats the cow. The bear is kind. The bear is round. The bear does not visit the cow. The cow eats the bear. The cow is big. If someone chases the cow then they chase the bear. If someone chases the bear then the bear does not visit the cow. If someone is big then they do not visit the cow.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is round.
("bear" "is" "round" "+")
The bear does not visit the cow.
("bear" "visits" "cow" "-")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is big.
("cow" "is" "big" "+")
If someone chases the cow then they chase the bear.
((("someone" "chases" "cow" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the bear then the bear does not visit the cow.
((("someone" "chases" "bear" "+")) -> ("bear" "visits" "cow" "-"))
If someone is big then they do not visit the cow.
((("someone" "is" "big" "+")) -> ("someone" "visits" "cow" "-"))
The bear eats the cow.
True
1
proof
[(triple2)]
("bear" "eats" "cow" "+")
triple2
The bear is not kind.
False
1
inv-proof
[(triple3)]
("bear" "is" "kind" "-")
triple3
The cow does not visit the cow.
True
2
proof
[(((triple7) -> rule3))]
("cow" "visits" "cow" "-")
((triple7) -> (rule3 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow visits the cow.
False
2
inv-proof
[(((triple7) -> rule3))]
("cow" "visits" "cow" "+")
((triple7) -> (rule3 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1
The cow does not chase the bear.
Unknown
inv-rconc
[@1: The cow chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "bear" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The bear chases the cow.[(triple1)] The bear does not visit the cow.[(triple5 OR ((((triple1) -> rule1)) -> rule2))] The bear eats the cow.[(triple2)] The bear is kind.[(triple3)] The bear is round.[(triple4)] The cow eats the bear.[(triple6)] The cow is big.[(triple7)] @1: The bear chases the bear.[(((triple1) -> rule1))] The cow does not visit the cow.[(((triple7) -> rule3))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear does not visit the cow.
("bear" "visits" "cow" "-")
triple5
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The bear does not visit the cow.
("bear" "visits" "cow" "-")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
triple2
The bear is kind.
("bear" "is" "kind" "+")
triple3
The bear is round.
("bear" "is" "round" "+")
triple4
The cow eats the bear.
("cow" "eats" "bear" "+")
triple6
The cow is big.
("cow" "is" "big" "+")
triple7
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple1) -> (rule1 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The cow does not visit the cow.
("cow" "visits" "cow" "-")
((triple7) -> (rule3 % int1))
The cow does not visit the cow.
("cow" "visits" "cow" "-")
int1