The bald eagle chases the squirrel. The bald eagle chases the tiger. The bald eagle is blue. The bald eagle sees the tiger. The squirrel chases the bald eagle. The squirrel is green. The tiger sees the bald eagle. If something sees the bald eagle then it is big. If something is big then it is kind. If something is green then it chases the tiger. If something eats the squirrel then the squirrel is green. If something sees the bald eagle and it chases the bald eagle then it eats the bald eagle. If the tiger is kind then the tiger is blue.
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
If something sees the bald eagle then it is big.
((("something" "sees" "bald eagle" "+")) -> ("something" "is" "big" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is green then it chases the tiger.
((("something" "is" "green" "+")) -> ("something" "chases" "tiger" "+"))
If something eats the squirrel then the squirrel is green.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
If something sees the bald eagle and it chases the bald eagle then it eats the bald eagle.
((("something" "sees" "bald eagle" "+") ("something" "chases" "bald eagle" "+")) -> ("something" "eats" "bald eagle" "+"))
If the tiger is kind then the tiger is blue.
((("tiger" "is" "kind" "+")) -> ("tiger" "is" "blue" "+"))
The bald eagle is blue.
True
1
proof
[(triple3)]
("bald eagle" "is" "blue" "+")
triple3
The bald eagle is not blue.
False
1
inv-proof
[(triple3)]
("bald eagle" "is" "blue" "-")
triple3
The tiger is big.
True
2
proof
[(((triple7) -> rule1))]
("tiger" "is" "big" "+")
((triple7) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not big.
False
2
inv-proof
[(((triple7) -> rule1))]
("tiger" "is" "big" "-")
((triple7) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
True
3
proof
[(((((triple7) -> rule1)) -> rule2))]
("tiger" "is" "kind" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not kind.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule2))]
("tiger" "is" "kind" "-")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
True
4
proof
[(((((((triple7) -> rule1)) -> rule2)) -> rule6))]
("tiger" "is" "blue" "+")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is not blue.
False
4
inv-proof
[(((((((triple7) -> rule1)) -> rule2)) -> rule6))]
("tiger" "is" "blue" "-")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The squirrel is not big.
Unknown
inv-rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "big" "-")
The squirrel eats the bald eagle.
Unknown
rconc
[@1: The squirrel eats the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "eats" "bald eagle" "+")
The bald eagle is not big.
Unknown
inv-rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "big" "-")
The squirrel is kind.
Unknown
rconc
[@2: The squirrel is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("squirrel" "is" "kind" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The squirrel sees the tiger.
Unknown
random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "+")
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel eats the tiger.
Unknown
random
[@0: The squirrel eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "tiger" "+")
@0: The bald eagle chases the squirrel.[(triple1)] The bald eagle chases the tiger.[(triple2)] The bald eagle is blue.[(triple3)] The bald eagle sees the tiger.[(triple4)] The squirrel chases the bald eagle.[(triple5)] The squirrel is green.[(triple6)] The tiger sees the bald eagle.[(triple7)] @1: The squirrel chases the tiger.[(((triple6) -> rule3))] The tiger is big.[(((triple7) -> rule1))] @2: The tiger is kind.[(((((triple7) -> rule1)) -> rule2))] @3: The tiger is blue.[(((((((triple7) -> rule1)) -> rule2)) -> rule6))]
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
triple1
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
triple2
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple3
The bald eagle sees the tiger.
("bald eagle" "sees" "tiger" "+")
triple4
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple7
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
((triple6) -> (rule3 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple7) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
((((((triple7) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3