The cow eats the rabbit. The cow is green. The cow is red. The cow sees the mouse. The mouse eats the cow. The mouse is green. The mouse is nice. The mouse is round. The mouse sees the rabbit. The rabbit does not eat the cow. The rabbit eats the mouse. The rabbit is green. The rabbit is not round. The rabbit sees the cow. The rabbit sees the mouse. The rabbit visits the mouse. If someone is green and they eat the cow then they do not eat the mouse. If someone is round then they see the mouse. If someone eats the rabbit and the rabbit visits the mouse then they are nice. If someone sees the mouse then they are green. All round people are red. If someone eats the cow and the cow does not visit the mouse then the cow sees the rabbit.
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is red.
("cow" "is" "red" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If someone is green and they eat the cow then they do not eat the mouse.
((("someone" "is" "green" "+") ("someone" "eats" "cow" "+")) -> ("someone" "eats" "mouse" "-"))
If someone is round then they see the mouse.
((("someone" "is" "round" "+")) -> ("someone" "sees" "mouse" "+"))
If someone eats the rabbit and the rabbit visits the mouse then they are nice.
((("someone" "eats" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("someone" "is" "nice" "+"))
If someone sees the mouse then they are green.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "green" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone eats the cow and the cow does not visit the mouse then the cow sees the rabbit.
((("someone" "eats" "cow" "+") ("cow" "visits" "mouse" "~")) -> ("cow" "sees" "rabbit" "+"))
The cow sees the mouse.
True
1
proof
[(triple4)]
("cow" "sees" "mouse" "+")
triple4
The mouse is not nice.
False
1
inv-proof
[(triple7)]
("mouse" "is" "nice" "-")
triple7
The cow does not see the rabbit.
Unknown
inv-rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "rabbit" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The cow eats the rabbit.[(triple1)] The cow is green.[(triple2 OR ((triple4) -> rule4))] The cow is red.[(triple3)] The cow sees the mouse.[(triple4)] The mouse eats the cow.[(triple5)] The mouse is green.[(triple6 OR ((((triple8) -> rule2)) -> rule4))] The mouse is nice.[(triple7)] The mouse is round.[(triple8)] The mouse sees the rabbit.[(triple9)] The rabbit does not eat the cow.[(triple10)] The rabbit eats the mouse.[(triple11)] The rabbit is green.[(triple12 OR ((triple15) -> rule4))] The rabbit is not round.[(triple13)] The rabbit sees the cow.[(triple14)] The rabbit sees the mouse.[(triple15)] The rabbit visits the mouse.[(triple16)] @1: The cow is nice.[(((triple1 triple16) -> rule3))] The mouse does not eat the mouse.[(((triple6 triple5) -> rule1) OR ((((((triple8) -> rule2)) -> rule4) triple5) -> rule1))] The mouse is red.[(((triple8) -> rule5))] The mouse sees the mouse.[(((triple8) -> rule2))]
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
((triple4) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is red.
("cow" "is" "red" "+")
triple3
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
triple7
The mouse is round.
("mouse" "is" "round" "+")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple9
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
triple10
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple11
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
((triple15) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not round.
("rabbit" "is" "round" "-")
triple13
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple14
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple15
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple16
The cow is nice.
("cow" "is" "nice" "+")
((triple1 triple16) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
((triple6 triple5) -> (rule1 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2)) triple5) -> (rule1 % int1))
The mouse does not eat the mouse.
("mouse" "eats" "mouse" "-")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
((triple8) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((triple8) -> (rule2 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1