The lion chases the tiger. The lion is not kind. The tiger chases the lion. If someone chases the tiger then they like the lion. If someone likes the lion then they eat the tiger.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
If someone chases the tiger then they like the lion.
((("someone" "chases" "tiger" "+")) -> ("someone" "likes" "lion" "+"))
If someone likes the lion then they eat the tiger.
((("someone" "likes" "lion" "+")) -> ("someone" "eats" "tiger" "+"))
The tiger chases the lion.
True
1
proof
[(triple3)]
("tiger" "chases" "lion" "+")
triple3
The lion is kind.
False
1
inv-proof
[(triple2)]
("lion" "is" "kind" "+")
triple2
The lion likes the lion.
True
2
proof
[(((triple1) -> rule1))]
("lion" "likes" "lion" "+")
((triple1) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion does not like the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "likes" "lion" "-")
((triple1) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion eats the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion does not eat the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "eats" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The tiger does not like the lion.
Unknown
inv-rconc
[@1: The tiger likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "lion" "-")
The tiger eats the tiger.
Unknown
rconc
[@2: The tiger eats the tiger.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion chases the tiger.[(triple1)] The lion is not kind.[(triple2)] The tiger chases the lion.[(triple3)] @1: The lion likes the lion.[(((triple1) -> rule1))] @2: The lion eats the tiger.[(((((triple1) -> rule1)) -> rule2))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The lion is not kind.
("lion" "is" "kind" "-")
triple2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple3
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple1) -> (rule1 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2