The bald eagle chases the squirrel. The bald eagle chases the tiger. The bald eagle is round. The squirrel does not chase the bald eagle. The squirrel is nice. The tiger chases the squirrel. The tiger is big. If the tiger is rough and the tiger needs the bald eagle then the bald eagle is rough. If someone sees the bald eagle and the bald eagle is nice then the bald eagle does not see the squirrel. If someone chases the squirrel then they see the squirrel. If someone sees the squirrel then the squirrel sees the bald eagle. If the squirrel chases the tiger then the tiger is not rough. If someone sees the bald eagle then they are big.
The bald eagle chases the squirrel.
("bald eagle" "chases" "squirrel" "+")
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
The bald eagle is round.
("bald eagle" "is" "round" "+")
The squirrel does not chase the bald eagle.
("squirrel" "chases" "bald eagle" "-")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
If the tiger is rough and the tiger needs the bald eagle then the bald eagle is rough.
((("tiger" "is" "rough" "+") ("tiger" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "rough" "+"))
If someone sees the bald eagle and the bald eagle is nice then the bald eagle does not see the squirrel.
((("someone" "sees" "bald eagle" "+") ("bald eagle" "is" "nice" "+")) -> ("bald eagle" "sees" "squirrel" "-"))
If someone chases the squirrel then they see the squirrel.
((("someone" "chases" "squirrel" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone sees the squirrel then the squirrel sees the bald eagle.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "bald eagle" "+"))
If the squirrel chases the tiger then the tiger is not rough.
((("squirrel" "chases" "tiger" "+")) -> ("tiger" "is" "rough" "-"))
If someone sees the bald eagle then they are big.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "is" "big" "+"))
The bald eagle chases the tiger.
True
1
proof
[(triple2)]
("bald eagle" "chases" "tiger" "+")
triple2
The bald eagle is not round.
False
1
inv-proof
[(triple3)]
("bald eagle" "is" "round" "-")
triple3
The tiger sees the squirrel.
True
2
proof
[(((triple6) -> rule3))]
("tiger" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger does not see the squirrel.
False
2
inv-proof
[(((triple6) -> rule3))]
("tiger" "sees" "squirrel" "-")
((triple6) -> (rule3 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
True
3
proof
[(((((triple1) -> rule3)) -> rule4) OR ((((triple6) -> rule3)) -> rule4))]
("squirrel" "sees" "bald eagle" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel does not see the bald eagle.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4) OR ((((triple6) -> rule3)) -> rule4))]
("squirrel" "sees" "bald eagle" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel is big.
True
4
proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule6) OR ((((((triple6) -> rule3)) -> rule4)) -> rule6))]
("squirrel" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int3
The squirrel is not big.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule6) OR ((((((triple6) -> rule3)) -> rule4)) -> rule6))]
("squirrel" "is" "big" "-")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int3
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The bald eagle is big.
Unknown
rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "big" "+")
The bald eagle is not rough.
Unknown
inv-rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "rough" "-")
The bald eagle is nice.
Unknown
random
[@0: The bald eagle is nice.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "nice" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel does not need the bald eagle.
Unknown
inv-random
[@0: The squirrel needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bald eagle" "-")
The tiger chases the bald eagle.
Unknown
random
[@0: The tiger chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bald eagle" "+")
@0: The bald eagle chases the squirrel.[(triple1)] The bald eagle chases the tiger.[(triple2)] The bald eagle is round.[(triple3)] The squirrel does not chase the bald eagle.[(triple4)] The squirrel is nice.[(triple5)] The tiger chases the squirrel.[(triple6)] The tiger is big.[(triple7)] @1: The bald eagle sees the squirrel.[(((triple1) -> rule3))] The tiger sees the squirrel.[(((triple6) -> rule3))] @2: The squirrel sees the bald eagle.[(((((triple1) -> rule3)) -> rule4) OR ((((triple6) -> rule3)) -> rule4))] @3: The squirrel is big.[(((((((triple1) -> rule3)) -> rule4)) -> rule6) OR ((((((triple6) -> rule3)) -> rule4)) -> 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 round.
("bald eagle" "is" "round" "+")
triple3
The squirrel does not chase the bald eagle.
("squirrel" "chases" "bald eagle" "-")
triple4
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple5
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
((triple1) -> (rule3 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
((triple6) -> (rule3 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int1
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
int2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int3