The mouse eats the rabbit. The mouse is cold. The mouse is kind. The mouse is red. The mouse is rough. The mouse is round. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit eats the mouse. The rabbit is kind. The rabbit is red. The rabbit is rough. The rabbit is round. The rabbit sees the mouse. The rabbit visits the mouse. If something visits the mouse and the mouse is kind then the mouse eats the rabbit. If something is round then it eats the mouse. If the rabbit sees the mouse and the mouse sees the rabbit then the mouse eats the rabbit. If something eats the mouse then the mouse visits the rabbit. If something sees the mouse then it visits the rabbit. If something sees the mouse then the mouse visits the rabbit. If something is kind then it eats the mouse. All round things are kind.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something visits the mouse and the mouse is kind then the mouse eats the rabbit.
((("something" "visits" "mouse" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "eats" "rabbit" "+"))
If something is round then it eats the mouse.
((("something" "is" "round" "+")) -> ("something" "eats" "mouse" "+"))
If the rabbit sees the mouse and the mouse sees the rabbit then the mouse eats the rabbit.
((("rabbit" "sees" "mouse" "+") ("mouse" "sees" "rabbit" "+")) -> ("mouse" "eats" "rabbit" "+"))
If something eats the mouse then the mouse visits the rabbit.
((("something" "eats" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If something sees the mouse then it visits the rabbit.
((("something" "sees" "mouse" "+")) -> ("something" "visits" "rabbit" "+"))
If something sees the mouse then the mouse visits the rabbit.
((("something" "sees" "mouse" "+")) -> ("mouse" "visits" "rabbit" "+"))
If something is kind then it eats the mouse.
((("something" "is" "kind" "+")) -> ("something" "eats" "mouse" "+"))
All round things are kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
The rabbit is rough.
True
1
proof
[(triple12)]
("rabbit" "is" "rough" "+")
triple12
The mouse does not eat the rabbit.
False
1
inv-proof
[(triple1 OR ((triple14 triple7) -> rule3) OR ((triple15 triple3) -> rule1) OR ((triple15 ((triple6) -> rule8)) -> rule1))]
("mouse" "eats" "rabbit" "-")
triple1
((triple14 triple7) -> (rule3 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
((triple15 triple3) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
((triple15 ((triple6) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse eats the rabbit.[(triple1 OR ((triple14 triple7) -> rule3) OR ((triple15 triple3) -> rule1) OR ((triple15 ((triple6) -> rule8)) -> rule1))] The mouse is cold.[(triple2)] The mouse is kind.[(triple3 OR ((triple6) -> rule8))] The mouse is red.[(triple4)] The mouse is rough.[(triple5)] The mouse is round.[(triple6)] The mouse sees the rabbit.[(triple7)] The mouse visits the rabbit.[(triple8 OR ((triple14) -> rule6) OR ((triple9) -> rule4) OR ((((triple10) -> rule7)) -> rule4) OR ((((triple13) -> rule2)) -> rule4) OR ((((triple3) -> rule7)) -> rule4) OR ((((triple6) -> rule2)) -> rule4) OR ((((((triple13) -> rule8)) -> rule7)) -> rule4) OR ((((((triple6) -> rule8)) -> rule7)) -> rule4))] The rabbit eats the mouse.[(triple9 OR ((triple10) -> rule7) OR ((triple13) -> rule2) OR ((((triple13) -> rule8)) -> rule7))] The rabbit is kind.[(triple10 OR ((triple13) -> rule8))] The rabbit is red.[(triple11)] The rabbit is rough.[(triple12)] The rabbit is round.[(triple13)] The rabbit sees the mouse.[(triple14)] The rabbit visits the mouse.[(triple15)] @1: The mouse eats the mouse.[(((triple3) -> rule7) OR ((triple6) -> rule2) OR ((((triple6) -> rule8)) -> rule7))] The rabbit visits the rabbit.[(((triple14) -> rule5))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
((triple14 triple7) -> (rule3 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
((triple15 triple3) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
((triple15 ((triple6) -> (rule8 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
((triple6) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple7
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple8
((triple14) -> (rule6 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
((triple9) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
((((triple13) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
((((triple6) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
((((((triple13) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
((((((triple6) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple9
((triple10) -> (rule7 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
((triple13) -> (rule2 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
((((triple13) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
((triple13) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit is round.
("rabbit" "is" "round" "+")
triple13
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple14
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple15
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple3) -> (rule7 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
((triple6) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule7 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple14) -> (rule5 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1