The lion visits the mouse. The mouse visits the lion. The rabbit needs the lion. If someone needs the lion then the lion is young. All young people are big.
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If someone needs the lion then the lion is young.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "young" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
The lion visits the mouse.
True
1
proof
[(triple1)]
("lion" "visits" "mouse" "+")
triple1
The lion does not visit the mouse.
False
1
inv-proof
[(triple1)]
("lion" "visits" "mouse" "-")
triple1
The lion is young.
True
2
proof
[(((triple3) -> rule1))]
("lion" "is" "young" "+")
((triple3) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "is" "young" "-")
((triple3) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("lion" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("lion" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "big" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "big" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse sees the rabbit.
Unknown
random
[@0: The mouse sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "rabbit" "+")
@0: The lion visits the mouse.[(triple1)] The mouse visits the lion.[(triple2)] The rabbit needs the lion.[(triple3)] @1: The lion is young.[(((triple3) -> rule1))] @2: The lion is big.[(((((triple3) -> rule1)) -> rule2))]
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple2
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
((triple3) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2