The lion eats the tiger. The lion is green. The lion likes the tiger. The rabbit chases the tiger. The rabbit is green. The tiger chases the rabbit. The tiger eats the lion. The tiger eats the rabbit. The tiger likes the lion. The tiger likes the rabbit. If something eats the tiger then the tiger likes the lion. If something eats the tiger and it is cold then it chases the rabbit. If something chases the lion then the lion eats the tiger. If something likes the tiger and it eats the rabbit then the rabbit chases the lion. If something eats the lion then the lion is round. If something likes the tiger then the tiger eats the lion.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If something eats the tiger then the tiger likes the lion.
((("something" "eats" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
If something eats the tiger and it is cold then it chases the rabbit.
((("something" "eats" "tiger" "+") ("something" "is" "cold" "+")) -> ("something" "chases" "rabbit" "+"))
If something chases the lion then the lion eats the tiger.
((("something" "chases" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
If something likes the tiger and it eats the rabbit then the rabbit chases the lion.
((("something" "likes" "tiger" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
If something eats the lion then the lion is round.
((("something" "eats" "lion" "+")) -> ("lion" "is" "round" "+"))
If something likes the tiger then the tiger eats the lion.
((("something" "likes" "tiger" "+")) -> ("tiger" "eats" "lion" "+"))
The tiger eats the lion.
True
1
proof
[(triple7 OR ((triple3) -> rule6))]
("tiger" "eats" "lion" "+")
triple7
((triple3) -> (rule6 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion does not eat the tiger.
False
1
inv-proof
[(triple1)]
("lion" "eats" "tiger" "-")
triple1
The lion is round.
True
2
proof
[(((triple7) -> rule5) OR ((((triple3) -> rule6)) -> rule5))]
("lion" "is" "round" "+")
((triple7) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion is not round.
False
2
inv-proof
[(((triple7) -> rule5) OR ((((triple3) -> rule6)) -> rule5))]
("lion" "is" "round" "-")
((triple7) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion does not chase the rabbit.
Unknown
inv-rconc
[@1: The lion chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "rabbit" "-")
The rabbit chases the lion.
Unknown
rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "lion" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The lion eats the tiger.[(triple1)] The lion is green.[(triple2)] The lion likes the tiger.[(triple3)] The rabbit chases the tiger.[(triple4)] The rabbit is green.[(triple5)] The tiger chases the rabbit.[(triple6)] The tiger eats the lion.[(triple7 OR ((triple3) -> rule6))] The tiger eats the rabbit.[(triple8)] The tiger likes the lion.[(triple9 OR ((triple1) -> rule1))] The tiger likes the rabbit.[(triple10)] @1: The lion is round.[(((triple7) -> rule5) OR ((((triple3) -> rule6)) -> rule5))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple3
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple4
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple6
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple7
((triple3) -> (rule6 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple8
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple9
((triple1) -> (rule1 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple10
The lion is round.
("lion" "is" "round" "+")
((triple7) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2