The mouse chases the tiger. The mouse eats the tiger. The mouse is kind. The mouse does not visit the rabbit. The mouse visits the tiger. The rabbit chases the tiger. The rabbit eats the mouse. The rabbit does not eat the tiger. The rabbit is rough. The rabbit does not visit the mouse. The rabbit does not visit the tiger. The tiger does not chase the mouse. The tiger does not chase the rabbit. The tiger is kind. The tiger visits the mouse. The tiger visits the rabbit. If something visits the tiger then the tiger visits the mouse. If the tiger is nice and the tiger does not chase the mouse then the tiger visits the mouse. If something is round and it does not eat the mouse then the mouse visits the rabbit. If something is rough then it chases the rabbit. If something visits the mouse and it chases the tiger then the mouse is round. If something eats the tiger and it eats the rabbit then the rabbit does not visit the tiger. If something eats the rabbit then it is round. If something visits the mouse and it does not chase the mouse then it eats the rabbit.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something visits the tiger then the tiger visits the mouse.
((("something" "visits" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If the tiger is nice and the tiger does not chase the mouse then the tiger visits the mouse.
((("tiger" "is" "nice" "+") ("tiger" "chases" "mouse" "~")) -> ("tiger" "visits" "mouse" "+"))
If something is round and it does not eat the mouse then the mouse visits the rabbit.
((("something" "is" "round" "+") ("something" "eats" "mouse" "~")) -> ("mouse" "visits" "rabbit" "+"))
If something is rough then it chases the rabbit.
((("something" "is" "rough" "+")) -> ("something" "chases" "rabbit" "+"))
If something visits the mouse and it chases the tiger then the mouse is round.
((("something" "visits" "mouse" "+") ("something" "chases" "tiger" "+")) -> ("mouse" "is" "round" "+"))
If something eats the tiger and it eats the rabbit then the rabbit does not visit the tiger.
((("something" "eats" "tiger" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "-"))
If something eats the rabbit then it is round.
((("something" "eats" "rabbit" "+")) -> ("something" "is" "round" "+"))
If something visits the mouse and it does not chase the mouse then it eats the rabbit.
((("something" "visits" "mouse" "+") ("something" "chases" "mouse" "~")) -> ("something" "eats" "rabbit" "+"))
The rabbit is rough.
True
1
proof
[(triple9)]
("rabbit" "is" "rough" "+")
triple9
The rabbit is not rough.
False
1
inv-proof
[(triple9)]
("rabbit" "is" "rough" "-")
triple9
The tiger eats the rabbit.
True
3
proof
[(((triple15 triple12) -> rule8) OR ((((triple5) -> rule1) triple12) -> rule8))]
("tiger" "eats" "rabbit" "+")
((triple15 triple12) -> (rule8 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
((((triple5) -> (rule1 % int2)) triple12) -> (rule8 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple9) -> rule4))]
("rabbit" "chases" "rabbit" "-")
((triple9) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The tiger is round.
True
4
proof
[(((((triple15 triple12) -> rule8)) -> rule7) OR ((((((triple5) -> rule1) triple12) -> rule8)) -> rule7))]
("tiger" "is" "round" "+")
((((triple15 triple12) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
((((((triple5) -> (rule1 % int3)) triple12) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3
The tiger is not round.
False
4
inv-proof
[(((((triple15 triple12) -> rule8)) -> rule7) OR ((((((triple5) -> rule1) triple12) -> rule8)) -> rule7))]
("tiger" "is" "round" "-")
((((triple15 triple12) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
((((((triple5) -> (rule1 % int3)) triple12) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The mouse chases the rabbit.
Unknown
rconc
[@1: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "rabbit" "+")
The mouse does not eat the rabbit.
Unknown
inv-rconc
[@1: The mouse eats the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "rabbit" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse does not visit the rabbit.[(triple4)] The mouse eats the tiger.[(triple2)] The mouse is kind.[(triple3)] The mouse visits the tiger.[(triple5)] The rabbit chases the tiger.[(triple6)] The rabbit does not eat the tiger.[(triple8)] The rabbit does not visit the mouse.[(triple10)] The rabbit does not visit the tiger.[(triple11)] The rabbit eats the mouse.[(triple7)] The rabbit is rough.[(triple9)] The tiger does not chase the mouse.[(triple12)] The tiger does not chase the rabbit.[(triple13)] The tiger is kind.[(triple14)] The tiger visits the mouse.[(triple15 OR ((triple5) -> rule1))] The tiger visits the rabbit.[(triple16)] @1: The rabbit chases the rabbit.[(((triple9) -> rule4))] The tiger eats the rabbit.[(((triple15 triple12) -> rule8) OR ((((triple5) -> rule1) triple12) -> rule8))] @2: The tiger is round.[(((((triple15 triple12) -> rule8)) -> rule7) OR ((((((triple5) -> rule1) triple12) -> rule8)) -> rule7))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse does not visit the rabbit.
("mouse" "visits" "rabbit" "-")
triple4
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple6
The rabbit does not eat the tiger.
("rabbit" "eats" "tiger" "-")
triple8
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple10
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
triple11
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple9
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
triple12
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
triple13
The tiger is kind.
("tiger" "is" "kind" "+")
triple14
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
((triple5) -> (rule1 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple16
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple9) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple15 triple12) -> (rule8 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
((((triple5) -> (rule1 % int2)) triple12) -> (rule8 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((((triple15 triple12) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
((((((triple5) -> (rule1 % int3)) triple12) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int3