The bald eagle visits the tiger. The tiger visits the bald eagle. If someone visits the bald eagle and they do not visit the tiger then the tiger visits the bald eagle. If someone visits the bald eagle then they are green. All young people are green. If someone visits the bald eagle then they see the bald eagle. If someone visits the tiger and they are nice then they do not eat the bald eagle. If the tiger sees the bald eagle then the tiger is big. If someone is big then they are blue. If someone sees the bald eagle then the bald eagle eats the tiger.
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
If someone visits the bald eagle and they do not visit the tiger then the tiger visits the bald eagle.
((("someone" "visits" "bald eagle" "+") ("someone" "visits" "tiger" "~")) -> ("tiger" "visits" "bald eagle" "+"))
If someone visits the bald eagle then they are green.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "is" "green" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone visits the bald eagle then they see the bald eagle.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "sees" "bald eagle" "+"))
If someone visits the tiger and they are nice then they do not eat the bald eagle.
((("someone" "visits" "tiger" "+") ("someone" "is" "nice" "+")) -> ("someone" "eats" "bald eagle" "-"))
If the tiger sees the bald eagle then the tiger is big.
((("tiger" "sees" "bald eagle" "+")) -> ("tiger" "is" "big" "+"))
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the bald eagle then the bald eagle eats the tiger.
((("someone" "sees" "bald eagle" "+")) -> ("bald eagle" "eats" "tiger" "+"))
The tiger visits the bald eagle.
True
1
proof
[(triple2)]
("tiger" "visits" "bald eagle" "+")
triple2
The bald eagle does not visit the tiger.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "tiger" "-")
triple1
The tiger is green.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "is" "green" "+")
((triple2) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "is" "green" "-")
((triple2) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is big.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("tiger" "is" "big" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The bald eagle does not eat the tiger.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule8))]
("bald eagle" "eats" "tiger" "-")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger is blue.
True
4
proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule7))]
("tiger" "is" "blue" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The tiger is not blue.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule6)) -> rule7))]
("tiger" "is" "blue" "-")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The bald eagle is not blue.
Unknown
inv-rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "is" "blue" "-")
The bald eagle sees the bald eagle.
Unknown
rconc
[@1: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
The bald eagle is not green.
Unknown
inv-rconc
[@1: The bald eagle is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "green" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The bald eagle is young.
Unknown
random
[@0: The bald eagle is young.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "young" "+")
The bald eagle does not visit the bald eagle.
Unknown
inv-random
[@0: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bald eagle" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The bald eagle visits the tiger.[(triple1)] The tiger visits the bald eagle.[(triple2)] @1: The tiger is green.[(((triple2) -> rule2))] The tiger sees the bald eagle.[(((triple2) -> rule4))] @2: The bald eagle eats the tiger.[(((((triple2) -> rule4)) -> rule8))] The tiger is big.[(((((triple2) -> rule4)) -> rule6))] @3: The tiger is blue.[(((((((triple2) -> rule4)) -> rule6)) -> rule7))]
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
triple1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
triple2
The tiger is green.
("tiger" "is" "green" "+")
((triple2) -> (rule2 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
((triple2) -> (rule4 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((((triple2) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3