The bald eagle eats the mouse. The lion does not visit the mouse. The mouse needs the bald eagle. The tiger eats the lion. If something visits the lion then it eats the tiger. If something is young then it visits the lion. If something eats the tiger then the tiger eats the mouse. If something visits the mouse then it eats the bald eagle. If something eats the lion then it is young. If the mouse visits the bald eagle and the mouse does not eat the tiger then the tiger is red. If something visits the tiger then the tiger is nice. If something needs the lion and it is red then the lion visits the tiger.
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If something visits the lion then it eats the tiger.
((("something" "visits" "lion" "+")) -> ("something" "eats" "tiger" "+"))
If something is young then it visits the lion.
((("something" "is" "young" "+")) -> ("something" "visits" "lion" "+"))
If something eats the tiger then the tiger eats the mouse.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
If something visits the mouse then it eats the bald eagle.
((("something" "visits" "mouse" "+")) -> ("something" "eats" "bald eagle" "+"))
If something eats the lion then it is young.
((("something" "eats" "lion" "+")) -> ("something" "is" "young" "+"))
If the mouse visits the bald eagle and the mouse does not eat the tiger then the tiger is red.
((("mouse" "visits" "bald eagle" "+") ("mouse" "eats" "tiger" "~")) -> ("tiger" "is" "red" "+"))
If something visits the tiger then the tiger is nice.
((("something" "visits" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If something needs the lion and it is red then the lion visits the tiger.
((("something" "needs" "lion" "+") ("something" "is" "red" "+")) -> ("lion" "visits" "tiger" "+"))
The tiger eats the lion.
True
1
proof
[(triple4)]
("tiger" "eats" "lion" "+")
triple4
The tiger does not eat the lion.
False
1
inv-proof
[(triple4)]
("tiger" "eats" "lion" "-")
triple4
The tiger is young.
True
2
proof
[(((triple4) -> rule5))]
("tiger" "is" "young" "+")
((triple4) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is not young.
False
2
inv-proof
[(((triple4) -> rule5))]
("tiger" "is" "young" "-")
((triple4) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the lion.
True
3
proof
[(((((triple4) -> rule5)) -> rule2))]
("tiger" "visits" "lion" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger does not visit the lion.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule2))]
("tiger" "visits" "lion" "-")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger eats the tiger.
True
4
proof
[(((((((triple4) -> rule5)) -> rule2)) -> rule1))]
("tiger" "eats" "tiger" "+")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger does not eat the tiger.
False
4
inv-proof
[(((((((triple4) -> rule5)) -> rule2)) -> rule1))]
("tiger" "eats" "tiger" "-")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is not nice.
Unknown
inv-rconc
[@2: The tiger is nice.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("tiger" "is" "nice" "-")
The bald eagle is young.
Unknown
rconc
[@1: The bald eagle is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "is" "young" "+")
The bald eagle does not visit the lion.
Unknown
inv-rconc
[@2: The bald eagle visits the lion.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("bald eagle" "visits" "lion" "-")
The tiger eats the bald eagle.
Unknown
rconc
[@1: The tiger eats the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "eats" "bald eagle" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The bald eagle needs the tiger.
Unknown
random
[@0: The bald eagle needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "tiger" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The bald eagle eats the mouse.[(triple1)] The lion does not visit the mouse.[(triple2)] The mouse needs the bald eagle.[(triple3)] The tiger eats the lion.[(triple4)] @1: The tiger is young.[(((triple4) -> rule5))] @2: The tiger visits the lion.[(((((triple4) -> rule5)) -> rule2))] @3: The tiger eats the tiger.[(((((((triple4) -> rule5)) -> rule2)) -> rule1))] @4: The tiger eats the mouse.[(((((((((triple4) -> rule5)) -> rule2)) -> rule1)) -> rule3))]
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
triple1
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple2
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple3
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple4
The tiger is young.
("tiger" "is" "young" "+")
((triple4) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((((triple4) -> (rule5 % int2))) -> (rule2 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((((triple4) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((((((((triple4) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
int4