The bear needs the cow. The cat needs the cow. The cow eats the bear. The lion does not eat the cow. If something needs the lion and it eats the cow then it eats the bear. If the bear is rough and the bear chases the lion then the bear eats the cow. If something is young and it needs the cow then the cow chases the bear. If something needs the cow then the cow does not chase the bear. If something eats the bear then it does not eat the cat. If something chases the lion then the lion eats the cow. If something is rough and young then it needs the cow. If something is green then it chases the bear.
The bear needs the cow.
("bear" "needs" "cow" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The lion does not eat the cow.
("lion" "eats" "cow" "-")
If something needs the lion and it eats the cow then it eats the bear.
((("something" "needs" "lion" "+") ("something" "eats" "cow" "+")) -> ("something" "eats" "bear" "+"))
If the bear is rough and the bear chases the lion then the bear eats the cow.
((("bear" "is" "rough" "+") ("bear" "chases" "lion" "+")) -> ("bear" "eats" "cow" "+"))
If something is young and it needs the cow then the cow chases the bear.
((("something" "is" "young" "+") ("something" "needs" "cow" "+")) -> ("cow" "chases" "bear" "+"))
If something needs the cow then the cow does not chase the bear.
((("something" "needs" "cow" "+")) -> ("cow" "chases" "bear" "-"))
If something eats the bear then it does not eat the cat.
((("something" "eats" "bear" "+")) -> ("something" "eats" "cat" "-"))
If something chases the lion then the lion eats the cow.
((("something" "chases" "lion" "+")) -> ("lion" "eats" "cow" "+"))
If something is rough and young then it needs the cow.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "needs" "cow" "+"))
If something is green then it chases the bear.
((("something" "is" "green" "+")) -> ("something" "chases" "bear" "+"))
The cat needs the cow.
True
1
proof
[(triple2)]
("cat" "needs" "cow" "+")
triple2
The cow does not eat the bear.
False
1
inv-proof
[(triple3)]
("cow" "eats" "bear" "-")
triple3
The cow does not eat the cat.
True
2
proof
[(((triple3) -> rule5))]
("cow" "eats" "cat" "-")
((triple3) -> (rule5 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The cow eats the cat.
False
2
inv-proof
[(((triple3) -> rule5))]
("cow" "eats" "cat" "+")
((triple3) -> (rule5 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1
The lion does not chase the bear.
Unknown
inv-rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "chases" "bear" "-")
The lion eats the bear.
Unknown
rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "bear" "+")
The bear does not need the lion.
Unknown
inv-random
[@0: The bear needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "lion" "-")
The bear needs the cat.
Unknown
random
[@0: The bear needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cat" "+")
@0: The bear needs the cow.[(triple1)] The cat needs the cow.[(triple2)] The cow eats the bear.[(triple3)] The lion does not eat the cow.[(triple4)] @1: The cow does not chase the bear.[(((triple1) -> rule4) OR ((triple2) -> rule4))] The cow does not eat the cat.[(((triple3) -> rule5))]
The bear needs the cow.
("bear" "needs" "cow" "+")
triple1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple2
The cow eats the bear.
("cow" "eats" "bear" "+")
triple3
The lion does not eat the cow.
("lion" "eats" "cow" "-")
triple4
The cow does not chase the bear.
("cow" "chases" "bear" "-")
((triple1) -> (rule4 % int1))
The cow does not chase the bear.
("cow" "chases" "bear" "-")
int1
((triple2) -> (rule4 % int1))
The cow does not chase the bear.
("cow" "chases" "bear" "-")
int1
The cow does not eat the cat.
("cow" "eats" "cat" "-")
((triple3) -> (rule5 % int1))
The cow does not eat the cat.
("cow" "eats" "cat" "-")
int1