The bald eagle likes the tiger. The bald eagle sees the tiger. The tiger is rough. Blue things are cold. Green, rough things are blue. If something likes the bald eagle then it sees the tiger. If something sees the tiger then the tiger is green. If something likes the tiger then it eats the tiger. If the bald eagle sees the tiger then the tiger sees the bald eagle.
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Green, rough things are blue.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If something likes the bald eagle then it sees the tiger.
((("something" "likes" "bald eagle" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the tiger then the tiger is green.
((("something" "sees" "tiger" "+")) -> ("tiger" "is" "green" "+"))
If something likes the tiger then it eats the tiger.
((("something" "likes" "tiger" "+")) -> ("something" "eats" "tiger" "+"))
If the bald eagle sees the tiger then the tiger sees the bald eagle.
((("bald eagle" "sees" "tiger" "+")) -> ("tiger" "sees" "bald eagle" "+"))
The bald eagle sees the tiger.
True
1
proof
[(triple2)]
("bald eagle" "sees" "tiger" "+")
triple2
The bald eagle does not like the tiger.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "tiger" "-")
triple1
The tiger sees the bald eagle.
True
2
proof
[(((triple2) -> rule6))]
("tiger" "sees" "bald eagle" "+")
((triple2) -> (rule6 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple2) -> rule4))]
("tiger" "is" "green" "-")
((triple2) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is blue.
True
4
proof
[(((((triple2) -> rule4) triple3) -> rule2))]
("tiger" "is" "blue" "+")
((((triple2) -> (rule4 % int2)) triple3) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is not blue.
False
4
inv-proof
[(((((triple2) -> rule4) triple3) -> rule2))]
("tiger" "is" "blue" "-")
((((triple2) -> (rule4 % int2)) triple3) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is cold.
True
5
proof
[(((((((triple2) -> rule4) triple3) -> rule2)) -> rule1))]
("tiger" "is" "cold" "+")
((((((triple2) -> (rule4 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is not cold.
False
5
inv-proof
[(((((((triple2) -> rule4) triple3) -> rule2)) -> rule1))]
("tiger" "is" "cold" "-")
((((((triple2) -> (rule4 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The bald eagle is not blue.
Unknown
inv-rconc
[@1: The bald eagle is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "blue" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The bald eagle is cold.
Unknown
rconc
[@2: The bald eagle is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bald eagle" "is" "cold" "+")
The tiger does not like the bald eagle.
Unknown
inv-random
[@0: The tiger likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bald eagle" "-")
The bald eagle likes the bald eagle.
Unknown
random
[@0: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "bald eagle" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The bald eagle is green.
Unknown
random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "+")
@0: The bald eagle likes the tiger.[(triple1)] The bald eagle sees the tiger.[(triple2)] The tiger is rough.[(triple3)] @1: The bald eagle eats the tiger.[(((triple1) -> rule5))] The tiger is green.[(((triple2) -> rule4))] The tiger sees the bald eagle.[(((triple2) -> rule6))] @2: The tiger is blue.[(((((triple2) -> rule4) triple3) -> rule2))] @3: The tiger is cold.[(((((((triple2) -> rule4) triple3) -> rule2)) -> rule1))]
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
triple1
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple2
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
((triple1) -> (rule5 % int1))
The bald eagle eats the tiger.
("bald eagle" "eats" "tiger" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple2) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
((triple2) -> (rule6 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((((triple2) -> (rule4 % int2)) triple3) -> (rule2 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((((triple2) -> (rule4 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3