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