The bear does not chase the cow. The bear is kind. The bear is nice. The bear visits the cow. The cow chases the mouse. The cow sees the bear. The cow does not visit the bear. The mouse chases the bear. The mouse chases the cow. The mouse sees the cow. If the mouse sees the bear and the mouse is nice then the mouse sees the cow. If someone sees the bear and the bear chases the mouse then the mouse is nice. If someone chases the bear and the bear is big then the bear does not chase the mouse. If someone sees the cow and the cow chases the mouse then the cow is blue. If someone is blue then they chase the bear. If someone chases the cow then the cow is nice.
The bear does not chase the cow.
("bear" "chases" "cow" "-")
The bear is kind.
("bear" "is" "kind" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow does not visit the bear.
("cow" "visits" "bear" "-")
The mouse chases the bear.
("mouse" "chases" "bear" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If the mouse sees the bear and the mouse is nice then the mouse sees the cow.
((("mouse" "sees" "bear" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "sees" "cow" "+"))
If someone sees the bear and the bear chases the mouse then the mouse is nice.
((("someone" "sees" "bear" "+") ("bear" "chases" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If someone chases the bear and the bear is big then the bear does not chase the mouse.
((("someone" "chases" "bear" "+") ("bear" "is" "big" "+")) -> ("bear" "chases" "mouse" "-"))
If someone sees the cow and the cow chases the mouse then the cow is blue.
((("someone" "sees" "cow" "+") ("cow" "chases" "mouse" "+")) -> ("cow" "is" "blue" "+"))
If someone is blue then they chase the bear.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the cow then the cow is nice.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "nice" "+"))
The mouse chases the bear.
True
1
proof
[(triple8)]
("mouse" "chases" "bear" "+")
triple8
The bear chases the cow.
False
1
inv-proof
[(triple1)]
("bear" "chases" "cow" "+")
triple1
The cow is nice.
True
2
proof
[(((triple9) -> rule6))]
("cow" "is" "nice" "+")
((triple9) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not blue.
False
3
inv-proof
[(((triple10 triple5) -> rule4))]
("cow" "is" "blue" "-")
((triple10 triple5) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow chases the bear.
True
4
proof
[(((((triple10 triple5) -> rule4)) -> rule5))]
("cow" "chases" "bear" "+")
((((triple10 triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow does not chase the bear.
False
4
inv-proof
[(((((triple10 triple5) -> rule4)) -> rule5))]
("cow" "chases" "bear" "-")
((((triple10 triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "nice" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "chases" "bear" "+")
The mouse does not visit the cow.
Unknown
inv-random
[@0: The mouse visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cow" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
@0: The bear does not chase the cow.[(triple1)] The bear is kind.[(triple2)] The bear is nice.[(triple3)] The bear visits the cow.[(triple4)] The cow chases the mouse.[(triple5)] The cow does not visit the bear.[(triple7)] The cow sees the bear.[(triple6)] The mouse chases the bear.[(triple8)] The mouse chases the cow.[(triple9)] The mouse sees the cow.[(triple10)] @1: The cow is blue.[(((triple10 triple5) -> rule4))] The cow is nice.[(((triple9) -> rule6))] @2: The cow chases the bear.[(((((triple10 triple5) -> rule4)) -> rule5))]
The bear does not chase the cow.
("bear" "chases" "cow" "-")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear visits the cow.
("bear" "visits" "cow" "+")
triple4
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple5
The cow does not visit the bear.
("cow" "visits" "bear" "-")
triple7
The cow sees the bear.
("cow" "sees" "bear" "+")
triple6
The mouse chases the bear.
("mouse" "chases" "bear" "+")
triple8
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple9
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
The cow is blue.
("cow" "is" "blue" "+")
((triple10 triple5) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
((triple9) -> (rule6 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow chases the bear.
("cow" "chases" "bear" "+")
((((triple10 triple5) -> (rule4 % int2))) -> (rule5 % int1))
The cow chases the bear.
("cow" "chases" "bear" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2