The dog chases the lion. The lion chases the dog. The lion chases the rabbit. The lion is nice. The rabbit eats the dog. The tiger chases the dog. The tiger likes the lion. If something is green then it likes the tiger. If something likes the tiger then it chases the lion. If something chases the rabbit then the rabbit likes the tiger.
The dog chases the lion.
("dog" "chases" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is nice.
("lion" "is" "nice" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
If something is green then it likes the tiger.
((("something" "is" "green" "+")) -> ("something" "likes" "tiger" "+"))
If something likes the tiger then it chases the lion.
((("something" "likes" "tiger" "+")) -> ("something" "chases" "lion" "+"))
If something chases the rabbit then the rabbit likes the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
The tiger chases the dog.
True
1
proof
[(triple6)]
("tiger" "chases" "dog" "+")
triple6
The dog does not chase the lion.
False
1
inv-proof
[(triple1)]
("dog" "chases" "lion" "-")
triple1
The rabbit likes the tiger.
True
2
proof
[(((triple3) -> rule3))]
("rabbit" "likes" "tiger" "+")
((triple3) -> (rule3 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit does not like the tiger.
False
2
inv-proof
[(((triple3) -> rule3))]
("rabbit" "likes" "tiger" "-")
((triple3) -> (rule3 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit chases the lion.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("rabbit" "chases" "lion" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The rabbit does not chase the lion.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("rabbit" "chases" "lion" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The lion does not like the tiger.
Unknown
inv-rconc
[@1: The lion likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "tiger" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The lion does not chase the lion.
Unknown
inv-rconc
[@2: The lion chases the lion.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("lion" "chases" "lion" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The lion eats the tiger.
Unknown
random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "+")
@0: The dog chases the lion.[(triple1)] The lion chases the dog.[(triple2)] The lion chases the rabbit.[(triple3)] The lion is nice.[(triple4)] The rabbit eats the dog.[(triple5)] The tiger chases the dog.[(triple6)] The tiger likes the lion.[(triple7)] @1: The rabbit likes the tiger.[(((triple3) -> rule3))] @2: The rabbit chases the lion.[(((((triple3) -> rule3)) -> rule2))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The lion chases the dog.
("lion" "chases" "dog" "+")
triple2
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple5
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple6
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple7
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
((triple3) -> (rule3 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2