The bear likes the tiger. The cow chases the bear. The tiger likes the cow. If something chases the cow and it needs the cow then it is not big. If something chases the bear then the bear chases the tiger. If something is cold and not big then it does not like the tiger.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If something chases the cow and it needs the cow then it is not big.
((("something" "chases" "cow" "+") ("something" "needs" "cow" "+")) -> ("something" "is" "big" "-"))
If something chases the bear then the bear chases the tiger.
((("something" "chases" "bear" "+")) -> ("bear" "chases" "tiger" "+"))
If something is cold and not big then it does not like the tiger.
((("something" "is" "cold" "+") ("something" "is" "big" "~")) -> ("something" "likes" "tiger" "-"))
The cow chases the bear.
True
1
proof
[(triple2)]
("cow" "chases" "bear" "+")
triple2
The bear does not like the tiger.
False
1
inv-proof
[(triple1)]
("bear" "likes" "tiger" "-")
triple1
The bear chases the tiger.
True
2
proof
[(((triple2) -> rule2))]
("bear" "chases" "tiger" "+")
((triple2) -> (rule2 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear does not chase the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "chases" "tiger" "-")
((triple2) -> (rule2 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
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 tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The cow does not like the bear.
Unknown
inv-random
[@0: The cow likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "bear" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
@0: The bear likes the tiger.[(triple1)] The cow chases the bear.[(triple2)] The tiger likes the cow.[(triple3)] @1: The bear chases the tiger.[(((triple2) -> rule2))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The cow chases the bear.
("cow" "chases" "bear" "+")
triple2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple2) -> (rule2 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1