The lion is green. The lion is not red. The mouse is green. The mouse visits the lion. The tiger is red. The tiger sees the lion. The tiger visits the lion. If someone is red then they need the tiger. If someone is green then they visit the mouse. If someone needs the lion then the lion does not need the mouse. If someone visits the mouse then they visit the tiger. If someone visits the tiger then they need the mouse. If someone visits the tiger and they are big then they are nice. If someone is big and they need the mouse then they see the tiger. If someone sees the lion and they do not visit the mouse then the lion visits the tiger.
The lion is green.
("lion" "is" "green" "+")
The lion is not red.
("lion" "is" "red" "-")
The mouse is green.
("mouse" "is" "green" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone is red then they need the tiger.
((("someone" "is" "red" "+")) -> ("someone" "needs" "tiger" "+"))
If someone is green then they visit the mouse.
((("someone" "is" "green" "+")) -> ("someone" "visits" "mouse" "+"))
If someone needs the lion then the lion does not need the mouse.
((("someone" "needs" "lion" "+")) -> ("lion" "needs" "mouse" "-"))
If someone visits the mouse then they visit the tiger.
((("someone" "visits" "mouse" "+")) -> ("someone" "visits" "tiger" "+"))
If someone visits the tiger then they need the mouse.
((("someone" "visits" "tiger" "+")) -> ("someone" "needs" "mouse" "+"))
If someone visits the tiger and they are big then they are nice.
((("someone" "visits" "tiger" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is big and they need the mouse then they see the tiger.
((("someone" "is" "big" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "sees" "tiger" "+"))
If someone sees the lion and they do not visit the mouse then the lion visits the tiger.
((("someone" "sees" "lion" "+") ("someone" "visits" "mouse" "~")) -> ("lion" "visits" "tiger" "+"))
The mouse visits the lion.
True
1
proof
[(triple4)]
("mouse" "visits" "lion" "+")
triple4
The tiger is not red.
False
1
inv-proof
[(triple5)]
("tiger" "is" "red" "-")
triple5
The tiger needs the tiger.
True
2
proof
[(((triple5) -> rule1))]
("tiger" "needs" "tiger" "+")
((triple5) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "visits" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse visits the tiger.
True
3
proof
[(((((triple3) -> rule2)) -> rule4))]
("mouse" "visits" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The lion does not visit the tiger.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("lion" "visits" "tiger" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The lion needs the mouse.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("lion" "needs" "mouse" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int3
The lion does not need the mouse.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("lion" "needs" "mouse" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int3
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "-")
The mouse needs the tiger.
Unknown
rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-rconc
[@2: The tiger visits the tiger.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "nice" "+")
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 tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The mouse does not see the lion.
Unknown
inv-random
[@0: The mouse sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "lion" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The lion is green.[(triple1)] The lion is not red.[(triple2)] The mouse is green.[(triple3)] The mouse visits the lion.[(triple4)] The tiger is red.[(triple5)] The tiger sees the lion.[(triple6)] The tiger visits the lion.[(triple7)] @1: The lion visits the mouse.[(((triple1) -> rule2))] The mouse visits the mouse.[(((triple3) -> rule2))] The tiger needs the tiger.[(((triple5) -> rule1))] @2: The lion visits the tiger.[(((((triple1) -> rule2)) -> rule4))] The mouse visits the tiger.[(((((triple3) -> rule2)) -> rule4))] @3: The lion needs the mouse.[(((((((triple1) -> rule2)) -> rule4)) -> rule5))] The mouse needs the mouse.[(((((((triple3) -> rule2)) -> rule4)) -> rule5))]
The lion is green.
("lion" "is" "green" "+")
triple1
The lion is not red.
("lion" "is" "red" "-")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple4
The tiger is red.
("tiger" "is" "red" "+")
triple5
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple6
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple7
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((triple1) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple3) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple5) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int3
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
int2
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int3