The lion chases the mouse. The lion eats the mouse. The mouse is nice. If someone eats the mouse and they chase the lion then they are young. If someone is nice then they need the mouse. If the lion eats the mouse and the lion chases the mouse then the mouse is nice. If someone chases the lion then they eat the mouse. If someone is nice and they need the mouse then they are red. Young people are round. If someone needs the mouse then the mouse is round. If the mouse eats the lion then the lion eats the mouse.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
If someone eats the mouse and they chase the lion then they are young.
((("someone" "eats" "mouse" "+") ("someone" "chases" "lion" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they need the mouse.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "mouse" "+"))
If the lion eats the mouse and the lion chases the mouse then the mouse is nice.
((("lion" "eats" "mouse" "+") ("lion" "chases" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If someone chases the lion then they eat the mouse.
((("someone" "chases" "lion" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is nice and they need the mouse then they are red.
((("someone" "is" "nice" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "is" "red" "+"))
Young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone needs the mouse then the mouse is round.
((("someone" "needs" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If the mouse eats the lion then the lion eats the mouse.
((("mouse" "eats" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
The lion eats the mouse.
True
1
proof
[(triple2)]
("lion" "eats" "mouse" "+")
triple2
The lion does not chase the mouse.
False
1
inv-proof
[(triple1)]
("lion" "chases" "mouse" "-")
triple1
The mouse needs the mouse.
True
2
proof
[(((triple3) -> rule2) OR ((((triple2 triple1) -> rule3)) -> rule2))]
("mouse" "needs" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule2) OR ((((triple2 triple1) -> rule3)) -> rule2))]
("mouse" "needs" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The lion is not red.
Unknown
inv-rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "red" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "young" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The lion chases the mouse.[(triple1)] The lion eats the mouse.[(triple2)] The mouse is nice.[(triple3 OR ((triple2 triple1) -> rule3))] @1: The mouse needs the mouse.[(((triple3) -> rule2) OR ((((triple2 triple1) -> rule3)) -> rule2))] @2: The mouse is red.[(((triple3 ((triple3) -> rule2)) -> rule5) OR ((((triple2 triple1) -> rule3) ((triple3) -> rule2)) -> rule5) OR ((triple3 ((((triple2 triple1) -> rule3)) -> rule2)) -> rule5) OR ((((triple2 triple1) -> rule3) ((((triple2 triple1) -> rule3)) -> rule2)) -> rule5))] The mouse is round.[(((((triple3) -> rule2)) -> rule7) OR ((((((triple2 triple1) -> rule3)) -> rule2)) -> rule7))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
((triple2 triple1) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
((((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((triple2 triple1) -> (rule3 % int3)) ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((triple3 ((((triple2 triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((((triple2 triple1) -> (rule3 % int3)) ((((triple2 triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
((((((triple2 triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3