The bear sees the cow. The cow sees the bear. The mouse is cold. If someone is rough then they eat the mouse. If someone eats the mouse and the mouse sees the bear then they see the cow. If someone eats the cow then they see the cow. If someone eats the mouse then the mouse is green. If someone needs the cow then the cow eats the mouse. If someone sees the bear then they eat the cow.
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
If someone is rough then they eat the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the mouse and the mouse sees the bear then they see the cow.
((("someone" "eats" "mouse" "+") ("mouse" "sees" "bear" "+")) -> ("someone" "sees" "cow" "+"))
If someone eats the cow then they see the cow.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone eats the mouse then the mouse is green.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If someone needs the cow then the cow eats the mouse.
((("someone" "needs" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
If someone sees the bear then they eat the cow.
((("someone" "sees" "bear" "+")) -> ("someone" "eats" "cow" "+"))
The mouse is cold.
True
1
proof
[(triple3)]
("mouse" "is" "cold" "+")
triple3
The bear does not see the cow.
False
1
inv-proof
[(triple1)]
("bear" "sees" "cow" "-")
triple1
The cow eats the cow.
True
2
proof
[(((triple2) -> rule6))]
("cow" "eats" "cow" "+")
((triple2) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow does not eat the cow.
False
2
inv-proof
[(((triple2) -> rule6))]
("cow" "eats" "cow" "-")
((triple2) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow sees the cow.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("cow" "sees" "cow" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow does not see the cow.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("cow" "sees" "cow" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The bear does not eat the cow.
Unknown
inv-rconc
[@1: The bear eats the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "cow" "-")
The mouse is green.
Unknown
rconc
[@2: The mouse is green.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("mouse" "is" "green" "+")
The mouse does not see the cow.
Unknown
inv-rconc
[@2: The mouse sees the cow.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("mouse" "sees" "cow" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
The mouse does not need the bear.
Unknown
inv-random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear sees the cow.[(triple1)] The cow sees the bear.[(triple2)] The mouse is cold.[(triple3)] @1: The cow eats the cow.[(((triple2) -> rule6))] @2: The cow sees the cow.[(((((triple2) -> rule6)) -> rule3))]
The bear sees the cow.
("bear" "sees" "cow" "+")
triple1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple2) -> (rule6 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2