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