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