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