The bear chases the cow. The bear eats the mouse. The bear is not blue. The bear sees the mouse. The cow eats the mouse. The cow is blue. The cow is green. The mouse chases the cow. The mouse eats the bear. The mouse eats the cow. The mouse sees the bear. The mouse sees the cow. If someone is big then they do not see the bear. If someone eats the cow then they see the bear. If someone sees the bear and they do not eat the cow then the bear does not chase the mouse. If the mouse does not eat the bear then the bear eats the mouse. If someone chases the cow and the cow is blue then the cow chases the mouse. If someone eats the mouse and they chase the mouse then they are big.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear is not blue.
("bear" "is" "blue" "-")
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If someone is big then they do not see the bear.
((("someone" "is" "big" "+")) -> ("someone" "sees" "bear" "-"))
If someone eats the cow then they see the bear.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "bear" "+"))
If someone sees the bear and they do not eat the cow then the bear does not chase the mouse.
((("someone" "sees" "bear" "+") ("someone" "eats" "cow" "~")) -> ("bear" "chases" "mouse" "-"))
If the mouse does not eat the bear then the bear eats the mouse.
((("mouse" "eats" "bear" "~")) -> ("bear" "eats" "mouse" "+"))
If someone chases the cow and the cow is blue then the cow chases the mouse.
((("someone" "chases" "cow" "+") ("cow" "is" "blue" "+")) -> ("cow" "chases" "mouse" "+"))
If someone eats the mouse and they chase the mouse then they are big.
((("someone" "eats" "mouse" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "is" "big" "+"))
The cow is green.
True
1
proof
[(triple7)]
("cow" "is" "green" "+")
triple7
The mouse does not chase the cow.
False
1
inv-proof
[(triple8)]
("mouse" "chases" "cow" "-")
triple8
The cow chases the mouse.
True
3
proof
[(((triple1 triple6) -> rule5) OR ((triple8 triple6) -> rule5))]
("cow" "chases" "mouse" "+")
((triple1 triple6) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
((triple8 triple6) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow does not chase the mouse.
False
3
inv-proof
[(((triple1 triple6) -> rule5) OR ((triple8 triple6) -> rule5))]
("cow" "chases" "mouse" "-")
((triple1 triple6) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
((triple8 triple6) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow is big.
True
5
proof
[(((triple5 ((triple1 triple6) -> rule5)) -> rule6) OR ((triple5 ((triple8 triple6) -> rule5)) -> rule6))]
("cow" "is" "big" "+")
((triple5 ((triple1 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
((triple5 ((triple8 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow is not big.
False
5
inv-proof
[(((triple5 ((triple1 triple6) -> rule5)) -> rule6) OR ((triple5 ((triple8 triple6) -> rule5)) -> rule6))]
("cow" "is" "big" "-")
((triple5 ((triple1 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
((triple5 ((triple8 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow does not see the bear.
True
6
proof
[(((((triple5 ((triple1 triple6) -> rule5)) -> rule6)) -> rule1) OR ((((triple5 ((triple8 triple6) -> rule5)) -> rule6)) -> rule1))]
("cow" "sees" "bear" "-")
((((triple5 ((triple1 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not see the bear.
("cow" "sees" "bear" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
((((triple5 ((triple8 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not see the bear.
("cow" "sees" "bear" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
The cow sees the bear.
False
6
inv-proof
[(((((triple5 ((triple1 triple6) -> rule5)) -> rule6)) -> rule1) OR ((((triple5 ((triple8 triple6) -> rule5)) -> rule6)) -> rule1))]
("cow" "sees" "bear" "+")
((((triple5 ((triple1 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not see the bear.
("cow" "sees" "bear" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
((((triple5 ((triple8 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not see the bear.
("cow" "sees" "bear" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
The bear does not see the bear.
Unknown
inv-rconc
[@1: The bear sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "sees" "bear" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "big" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "big" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
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 eats the mouse.[(triple2)] The bear is not blue.[(triple3)] The bear sees the mouse.[(triple4)] The cow eats the mouse.[(triple5)] The cow is blue.[(triple6)] The cow is green.[(triple7)] The mouse chases the cow.[(triple8)] The mouse eats the bear.[(triple9)] The mouse eats the cow.[(triple10)] The mouse sees the bear.[(triple11 OR ((triple10) -> rule2))] The mouse sees the cow.[(triple12)] @1: The cow chases the mouse.[(((triple1 triple6) -> rule5) OR ((triple8 triple6) -> rule5))] @2: The cow is big.[(((triple5 ((triple1 triple6) -> rule5)) -> rule6) OR ((triple5 ((triple8 triple6) -> rule5)) -> rule6))] @3: The cow does not see the bear.[(((((triple5 ((triple1 triple6) -> rule5)) -> rule6)) -> rule1) OR ((((triple5 ((triple8 triple6) -> rule5)) -> rule6)) -> rule1))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple2
The bear is not blue.
("bear" "is" "blue" "-")
triple3
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple4
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple5
The cow is blue.
("cow" "is" "blue" "+")
triple6
The cow is green.
("cow" "is" "green" "+")
triple7
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple8
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple9
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple10
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple11
((triple10) -> (rule2 % int1))
The mouse sees the bear.
("mouse" "sees" "bear" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple12
The cow chases the mouse.
("cow" "chases" "mouse" "+")
((triple1 triple6) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
((triple8 triple6) -> (rule5 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((triple5 ((triple1 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
((triple5 ((triple8 triple6) -> (rule5 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow does not see the bear.
("cow" "sees" "bear" "-")
((((triple5 ((triple1 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not see the bear.
("cow" "sees" "bear" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
((((triple5 ((triple8 triple6) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not see the bear.
("cow" "sees" "bear" "-")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3