The bear chases the cow. The bear needs the cow. The bear needs the mouse. The cow chases the mouse. The cow does not eat the mouse. The cow is not young. The mouse is not nice. If the cow eats the bear and the bear eats the cow then the bear does not chase the mouse. If something eats the cow then it chases the cow. If something chases the cow and the cow needs the mouse then the cow is red. If something chases the mouse then it needs the mouse. If something chases the cow and the cow does not chase the bear then the bear is big. If something needs the mouse and it does not need the bear then the bear chases the cow. If something eats the cow and the cow chases the mouse then the mouse eats the bear. If something is red then it does not eat the bear.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow does not eat the mouse.
("cow" "eats" "mouse" "-")
The cow is not young.
("cow" "is" "young" "-")
The mouse is not nice.
("mouse" "is" "nice" "-")
If the cow eats the bear and the bear eats the cow then the bear does not chase the mouse.
((("cow" "eats" "bear" "+") ("bear" "eats" "cow" "+")) -> ("bear" "chases" "mouse" "-"))
If something eats the cow then it chases the cow.
((("something" "eats" "cow" "+")) -> ("something" "chases" "cow" "+"))
If something chases the cow and the cow needs the mouse then the cow is red.
((("something" "chases" "cow" "+") ("cow" "needs" "mouse" "+")) -> ("cow" "is" "red" "+"))
If something chases the mouse then it needs the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
If something chases the cow and the cow does not chase the bear then the bear is big.
((("something" "chases" "cow" "+") ("cow" "chases" "bear" "~")) -> ("bear" "is" "big" "+"))
If something needs the mouse and it does not need the bear then the bear chases the cow.
((("something" "needs" "mouse" "+") ("something" "needs" "bear" "~")) -> ("bear" "chases" "cow" "+"))
If something eats the cow and the cow chases the mouse then the mouse eats the bear.
((("something" "eats" "cow" "+") ("cow" "chases" "mouse" "+")) -> ("mouse" "eats" "bear" "+"))
If something is red then it does not eat the bear.
((("something" "is" "red" "+")) -> ("something" "eats" "bear" "-"))
The bear needs the mouse.
True
1
proof
[(triple3)]
("bear" "needs" "mouse" "+")
triple3
The bear does not need the cow.
False
1
inv-proof
[(triple2)]
("bear" "needs" "cow" "-")
triple2
The cow needs the mouse.
True
2
proof
[(((triple4) -> rule4))]
("cow" "needs" "mouse" "+")
((triple4) -> (rule4 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow does not need the mouse.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "needs" "mouse" "-")
((triple4) -> (rule4 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow is red.
True
4
proof
[(((triple1 ((triple4) -> rule4)) -> rule3))]
("cow" "is" "red" "+")
((triple1 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow is not red.
False
4
inv-proof
[(((triple1 ((triple4) -> rule4)) -> rule3))]
("cow" "is" "red" "-")
((triple1 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow does not eat the bear.
True
5
proof
[(((((triple1 ((triple4) -> rule4)) -> rule3)) -> rule8))]
("cow" "eats" "bear" "-")
((((triple1 ((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow does not eat the bear.
("cow" "eats" "bear" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The cow eats the bear.
False
5
inv-proof
[(((((triple1 ((triple4) -> rule4)) -> rule3)) -> rule8))]
("cow" "eats" "bear" "+")
((((triple1 ((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow does not eat the bear.
("cow" "eats" "bear" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3
The mouse does not eat the bear.
Unknown
inv-rconc
[@1: The mouse eats the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "eats" "bear" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "big" "+")
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "cow" "-")
The mouse chases the cow.
Unknown
rconc
[@1: The mouse chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "chases" "cow" "+")
The bear does not eat the bear.
Unknown
inv-random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "-")
The bear eats the mouse.
Unknown
random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear chases the mouse.
Unknown
random
[@0: The bear chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "mouse" "+")
@0: The bear chases the cow.[(triple1)] The bear needs the cow.[(triple2)] The bear needs the mouse.[(triple3)] The cow chases the mouse.[(triple4)] The cow does not eat the mouse.[(triple5)] The cow is not young.[(triple6)] The mouse is not nice.[(triple7)] @1: The cow needs the mouse.[(((triple4) -> rule4))] @2: The cow is red.[(((triple1 ((triple4) -> rule4)) -> rule3))] @3: The cow does not eat the bear.[(((((triple1 ((triple4) -> rule4)) -> rule3)) -> rule8))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear needs the cow.
("bear" "needs" "cow" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple4
The cow does not eat the mouse.
("cow" "eats" "mouse" "-")
triple5
The cow is not young.
("cow" "is" "young" "-")
triple6
The mouse is not nice.
("mouse" "is" "nice" "-")
triple7
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple4) -> (rule4 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((triple1 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int2
The cow does not eat the bear.
("cow" "eats" "bear" "-")
((((triple1 ((triple4) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cow does not eat the bear.
("cow" "eats" "bear" "-")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int3