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