The bald eagle is cold. The bear eats the tiger. The lion is round. The tiger needs the bald eagle. If someone needs the bald eagle then the bald eagle eats the lion. If someone eats the lion then the lion visits the tiger. If someone eats the lion and the lion needs the tiger then the tiger is cold. If someone needs the tiger and the tiger is nice then they eat the bear. If someone eats the tiger then the tiger eats the lion. If someone needs the bear and they are not blue then the bear needs the lion.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The lion is round.
("lion" "is" "round" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
If someone needs the bald eagle then the bald eagle eats the lion.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "eats" "lion" "+"))
If someone eats the lion then the lion visits the tiger.
((("someone" "eats" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
If someone eats the lion and the lion needs the tiger then the tiger is cold.
((("someone" "eats" "lion" "+") ("lion" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If someone needs the tiger and the tiger is nice then they eat the bear.
((("someone" "needs" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("someone" "eats" "bear" "+"))
If someone eats the tiger then the tiger eats the lion.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "lion" "+"))
If someone needs the bear and they are not blue then the bear needs the lion.
((("someone" "needs" "bear" "+") ("someone" "is" "blue" "~")) -> ("bear" "needs" "lion" "+"))
The lion is round.
True
1
proof
[(triple3)]
("lion" "is" "round" "+")
triple3
The tiger does not need the bald eagle.
False
1
inv-proof
[(triple4)]
("tiger" "needs" "bald eagle" "-")
triple4
The bald eagle eats the lion.
True
2
proof
[(((triple4) -> rule1))]
("bald eagle" "eats" "lion" "+")
((triple4) -> (rule1 % int1))
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int1
The tiger does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule5))]
("tiger" "eats" "lion" "-")
((triple2) -> (rule5 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion visits the tiger.
True
3
proof
[(((((triple2) -> rule5)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("lion" "visits" "tiger" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int2
The lion does not visit the tiger.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
("lion" "visits" "tiger" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int2
The lion does not eat the bear.
Unknown
inv-rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "bear" "-")
The bear needs the lion.
Unknown
rconc
[@1: The bear needs the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "lion" "+")
The tiger does not eat the bear.
Unknown
inv-rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "eats" "bear" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
@0: The bald eagle is cold.[(triple1)] The bear eats the tiger.[(triple2)] The lion is round.[(triple3)] The tiger needs the bald eagle.[(triple4)] @1: The bald eagle eats the lion.[(((triple4) -> rule1))] The tiger eats the lion.[(((triple2) -> rule5))] @2: The lion visits the tiger.[(((((triple2) -> rule5)) -> rule2) OR ((((triple4) -> rule1)) -> rule2))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple4
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
((triple4) -> (rule1 % int1))
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((triple2) -> (rule5 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The bald eagle eats the lion.
("bald eagle" "eats" "lion" "+")
int2