The lion is cold. The lion is kind. The lion sees the mouse. The lion sees the rabbit. The mouse eats the rabbit. The mouse is cold. The mouse is kind. The mouse is not rough. The mouse does not see the lion. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit eats the mouse. The rabbit is cold. The rabbit is rough. The rabbit is round. The rabbit visits the mouse. If the lion visits the mouse and the mouse sees the lion then the mouse does not eat the rabbit. If something visits the rabbit and the rabbit visits the mouse then it is round. If the rabbit is cold and the rabbit eats the lion then the rabbit does not see the lion. If something is round and not kind then it does not see the lion. If something is round then it visits the mouse. If something sees the rabbit then it is not big. If something eats the mouse and it is big then the mouse is big. If something eats the lion and it does not see the lion then it is not rough.
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
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 not rough.
("mouse" "is" "rough" "-")
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
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 cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If the lion visits the mouse and the mouse sees the lion then the mouse does not eat the rabbit.
((("lion" "visits" "mouse" "+") ("mouse" "sees" "lion" "+")) -> ("mouse" "eats" "rabbit" "-"))
If something visits the rabbit and the rabbit visits the mouse then it is round.
((("something" "visits" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("something" "is" "round" "+"))
If the rabbit is cold and the rabbit eats the lion then the rabbit does not see the lion.
((("rabbit" "is" "cold" "+") ("rabbit" "eats" "lion" "+")) -> ("rabbit" "sees" "lion" "-"))
If something is round and not kind then it does not see the lion.
((("something" "is" "round" "+") ("something" "is" "kind" "~")) -> ("something" "sees" "lion" "-"))
If something is round then it visits the mouse.
((("something" "is" "round" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the rabbit then it is not big.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "big" "-"))
If something eats the mouse and it is big then the mouse is big.
((("something" "eats" "mouse" "+") ("something" "is" "big" "+")) -> ("mouse" "is" "big" "+"))
If something eats the lion and it does not see the lion then it is not rough.
((("something" "eats" "lion" "+") ("something" "sees" "lion" "~")) -> ("something" "is" "rough" "-"))
The mouse does not see the lion.
True
1
proof
[(triple9)]
("mouse" "sees" "lion" "-")
triple9
The rabbit is not cold.
False
1
inv-proof
[(triple13)]
("rabbit" "is" "cold" "-")
triple13
The mouse is round.
True
3
proof
[(((triple11 triple16) -> rule2) OR ((triple11 ((triple15) -> rule5)) -> rule2))]
("mouse" "is" "round" "+")
((triple11 triple16) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple11 ((triple15) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The mouse is big.
False
2
inv-proof
[(((triple10) -> rule6))]
("mouse" "is" "big" "+")
((triple10) -> (rule6 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
The mouse visits the mouse.
True
4
proof
[(((((triple11 triple16) -> rule2)) -> rule5) OR ((((triple11 ((triple15) -> rule5)) -> rule2)) -> rule5))]
("mouse" "visits" "mouse" "+")
((((triple11 triple16) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((((triple11 ((triple15) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3
The mouse does not visit the mouse.
False
4
inv-proof
[(((((triple11 triple16) -> rule2)) -> rule5) OR ((((triple11 ((triple15) -> rule5)) -> rule2)) -> rule5))]
("mouse" "visits" "mouse" "-")
((((triple11 triple16) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((((triple11 ((triple15) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3
The lion does not visit the mouse.
Unknown
inv-rconc
[@2: The lion visits the mouse.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("lion" "visits" "mouse" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "round" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The mouse eats the lion.
Unknown
random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "+")
@0: The lion is cold.[(triple1)] The lion is kind.[(triple2)] The lion sees the mouse.[(triple3)] The lion sees the rabbit.[(triple4)] The mouse does not see the lion.[(triple9)] The mouse eats the rabbit.[(triple5)] The mouse is cold.[(triple6)] The mouse is kind.[(triple7)] The mouse is not rough.[(triple8)] The mouse sees the rabbit.[(triple10)] The mouse visits the rabbit.[(triple11)] The rabbit eats the mouse.[(triple12)] The rabbit is cold.[(triple13)] The rabbit is rough.[(triple14)] The rabbit is round.[(triple15)] The rabbit visits the mouse.[(triple16 OR ((triple15) -> rule5))] @1: The lion is not big.[(((triple4) -> rule6))] The mouse is not big.[(((triple10) -> rule6))] The mouse is round.[(((triple11 triple16) -> rule2) OR ((triple11 ((triple15) -> rule5)) -> rule2))] @2: The mouse visits the mouse.[(((((triple11 triple16) -> rule2)) -> rule5) OR ((((triple11 ((triple15) -> rule5)) -> rule2)) -> rule5))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple4
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
triple9
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple5
The mouse is cold.
("mouse" "is" "cold" "+")
triple6
The mouse is kind.
("mouse" "is" "kind" "+")
triple7
The mouse is not rough.
("mouse" "is" "rough" "-")
triple8
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple10
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple11
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple12
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple13
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple14
The rabbit is round.
("rabbit" "is" "round" "+")
triple15
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple16
((triple15) -> (rule5 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The lion is not big.
("lion" "is" "big" "-")
((triple4) -> (rule6 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The mouse is not big.
("mouse" "is" "big" "-")
((triple10) -> (rule6 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple11 triple16) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple11 ((triple15) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple11 triple16) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
((((triple11 ((triple15) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int3