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