The lion sees the mouse. The mouse eats the lion. The mouse is big. If something visits the mouse then the mouse is young. If the lion eats the mouse and the lion is not young then the mouse eats the lion. If something is big then it visits the lion. If something sees the lion then the lion is big. If something eats the mouse and the mouse is green then it visits the mouse. If something visits the lion then the lion sees the mouse. If something eats the lion and it is big then it sees the lion. If something is young and it does not see the lion then it is kind.
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
If something visits the mouse then the mouse is young.
((("something" "visits" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If the lion eats the mouse and the lion is not young then the mouse eats the lion.
((("lion" "eats" "mouse" "+") ("lion" "is" "young" "~")) -> ("mouse" "eats" "lion" "+"))
If something is big then it visits the lion.
((("something" "is" "big" "+")) -> ("something" "visits" "lion" "+"))
If something sees the lion then the lion is big.
((("something" "sees" "lion" "+")) -> ("lion" "is" "big" "+"))
If something eats the mouse and the mouse is green then it visits the mouse.
((("something" "eats" "mouse" "+") ("mouse" "is" "green" "+")) -> ("something" "visits" "mouse" "+"))
If something visits the lion then the lion sees the mouse.
((("something" "visits" "lion" "+")) -> ("lion" "sees" "mouse" "+"))
If something eats the lion and it is big then it sees the lion.
((("something" "eats" "lion" "+") ("something" "is" "big" "+")) -> ("something" "sees" "lion" "+"))
If something is young and it does not see the lion then it is kind.
((("something" "is" "young" "+") ("something" "sees" "lion" "~")) -> ("something" "is" "kind" "+"))
The mouse is big.
True
1
proof
[(triple3)]
("mouse" "is" "big" "+")
triple3
The lion does not see the mouse.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule3)) -> rule6) OR ((((((((triple2 triple3) -> rule7)) -> rule4)) -> rule3)) -> rule6))]
("lion" "sees" "mouse" "-")
triple1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int2
((((((((triple2 triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int4
The mouse visits the lion.
True
2
proof
[(((triple3) -> rule3))]
("mouse" "visits" "lion" "+")
((triple3) -> (rule3 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse does not see the lion.
False
3
inv-proof
[(((triple2 triple3) -> rule7))]
("mouse" "sees" "lion" "-")
((triple2 triple3) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The lion is big.
True
4
proof
[(((((triple2 triple3) -> rule7)) -> rule4))]
("lion" "is" "big" "+")
((((triple2 triple3) -> (rule7 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion is not big.
False
4
inv-proof
[(((((triple2 triple3) -> rule7)) -> rule4))]
("lion" "is" "big" "-")
((((triple2 triple3) -> (rule7 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion visits the lion.
True
5
proof
[(((((((triple2 triple3) -> rule7)) -> rule4)) -> rule3))]
("lion" "visits" "lion" "+")
((((((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int3
The lion does not visit the lion.
False
5
inv-proof
[(((((((triple2 triple3) -> rule7)) -> rule4)) -> rule3))]
("lion" "visits" "lion" "-")
((((((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int3
The mouse is not young.
Unknown
inv-rconc
[@2: The mouse is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("mouse" "is" "young" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The lion is not kind.
Unknown
inv-rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "kind" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "lion" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion sees the mouse.[(triple1 OR ((((triple3) -> rule3)) -> rule6) OR ((((((((triple2 triple3) -> rule7)) -> rule4)) -> rule3)) -> rule6))] The mouse eats the lion.[(triple2)] The mouse is big.[(triple3)] @1: The mouse sees the lion.[(((triple2 triple3) -> rule7))] The mouse visits the lion.[(((triple3) -> rule3))] @2: The lion is big.[(((((triple2 triple3) -> rule7)) -> rule4))] @3: The lion visits the lion.[(((((((triple2 triple3) -> rule7)) -> rule4)) -> rule3))]
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int2
((((((((triple2 triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((triple2 triple3) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
((triple3) -> (rule3 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple2 triple3) -> (rule7 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((((triple2 triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int3