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