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