The cow chases the rabbit. The cow eats the mouse. The cow eats the rabbit. The cow is rough. The cow needs the tiger. The mouse chases the cow. The mouse eats the cow. The mouse eats the tiger. The mouse is kind. The mouse does not need the tiger. The rabbit chases the cow. The tiger chases the rabbit. The tiger eats the cow. The tiger is rough. The tiger needs the mouse. The tiger needs the rabbit. If the mouse eats the rabbit and the mouse is round then the mouse chases the cow. If someone chases the mouse and the mouse does not need the rabbit then the rabbit chases the tiger. If someone needs the rabbit then the rabbit needs the cow. If someone needs the tiger then the tiger is young. If someone is young and they chase the rabbit then the rabbit does not chase the mouse. If someone chases the cow and the cow eats the tiger then they eat the cow. If someone eats the tiger then the tiger does not eat the mouse. If someone eats the tiger and they are not red then they chase the rabbit.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse does not need the tiger.
("mouse" "needs" "tiger" "-")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If the mouse eats the rabbit and the mouse is round then the mouse chases the cow.
((("mouse" "eats" "rabbit" "+") ("mouse" "is" "round" "+")) -> ("mouse" "chases" "cow" "+"))
If someone chases the mouse and the mouse does not need the rabbit then the rabbit chases the tiger.
((("someone" "chases" "mouse" "+") ("mouse" "needs" "rabbit" "~")) -> ("rabbit" "chases" "tiger" "+"))
If someone needs the rabbit then the rabbit needs the cow.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "cow" "+"))
If someone needs the tiger then the tiger is young.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "young" "+"))
If someone is young and they chase the rabbit then the rabbit does not chase the mouse.
((("someone" "is" "young" "+") ("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "-"))
If someone chases the cow and the cow eats the tiger then they eat the cow.
((("someone" "chases" "cow" "+") ("cow" "eats" "tiger" "+")) -> ("someone" "eats" "cow" "+"))
If someone eats the tiger then the tiger does not eat the mouse.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "mouse" "-"))
If someone eats the tiger and they are not red then they chase the rabbit.
((("someone" "eats" "tiger" "+") ("someone" "is" "red" "~")) -> ("someone" "chases" "rabbit" "+"))
The cow eats the mouse.
True
1
proof
[(triple2)]
("cow" "eats" "mouse" "+")
triple2
The tiger does not chase the rabbit.
False
1
inv-proof
[(triple12)]
("tiger" "chases" "rabbit" "-")
triple12
The tiger is young.
True
2
proof
[(((triple5) -> rule4))]
("tiger" "is" "young" "+")
((triple5) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The rabbit does not need the cow.
False
2
inv-proof
[(((triple16) -> rule3))]
("rabbit" "needs" "cow" "-")
((triple16) -> (rule3 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit does not chase the tiger.
Unknown
inv-rconc
[@1: The rabbit chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "tiger" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow chases the rabbit.[(triple1)] The cow eats the mouse.[(triple2)] The cow eats the rabbit.[(triple3)] The cow is rough.[(triple4)] The cow needs the tiger.[(triple5)] The mouse chases the cow.[(triple6)] The mouse does not need the tiger.[(triple10)] The mouse eats the cow.[(triple7)] The mouse eats the tiger.[(triple8)] The mouse is kind.[(triple9)] The rabbit chases the cow.[(triple11)] The tiger chases the rabbit.[(triple12)] The tiger eats the cow.[(triple13)] The tiger is rough.[(triple14)] The tiger needs the mouse.[(triple15)] The tiger needs the rabbit.[(triple16)] @1: The rabbit needs the cow.[(((triple16) -> rule3))] The tiger does not eat the mouse.[(((triple8) -> rule7))] The tiger is young.[(((triple5) -> rule4))] @2: The rabbit does not chase the mouse.[(((((triple5) -> rule4) triple12) -> rule5))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple2
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple3
The cow is rough.
("cow" "is" "rough" "+")
triple4
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple5
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple6
The mouse does not need the tiger.
("mouse" "needs" "tiger" "-")
triple10
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple7
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple8
The mouse is kind.
("mouse" "is" "kind" "+")
triple9
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple11
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple12
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple13
The tiger is rough.
("tiger" "is" "rough" "+")
triple14
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple15
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple16
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((triple16) -> (rule3 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
((triple8) -> (rule7 % int1))
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple5) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
((((triple5) -> (rule4 % int2)) triple12) -> (rule5 % int1))
The rabbit does not chase the mouse.
("rabbit" "chases" "mouse" "-")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2