The bald eagle does not need the tiger. The bear chases the squirrel. The squirrel sees the bear. The tiger sees the bear. If the squirrel needs the tiger then the squirrel chases the bear. If the bald eagle is cold and the bald eagle is blue then the bald eagle chases the tiger. If someone needs the bald eagle and the bald eagle sees the tiger then the tiger does not chase the bald eagle. If the bear chases the squirrel then the squirrel needs the tiger. If the squirrel is cold and the squirrel chases the bear then the bear is round. If the squirrel needs the tiger then the squirrel does not see the bald eagle. If someone chases the bear then the bear is big. If someone chases the bald eagle and the bald eagle sees the tiger then they chase the bear.
The bald eagle does not need the tiger.
("bald eagle" "needs" "tiger" "-")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If the squirrel needs the tiger then the squirrel chases the bear.
((("squirrel" "needs" "tiger" "+")) -> ("squirrel" "chases" "bear" "+"))
If the bald eagle is cold and the bald eagle is blue then the bald eagle chases the tiger.
((("bald eagle" "is" "cold" "+") ("bald eagle" "is" "blue" "+")) -> ("bald eagle" "chases" "tiger" "+"))
If someone needs the bald eagle and the bald eagle sees the tiger then the tiger does not chase the bald eagle.
((("someone" "needs" "bald eagle" "+") ("bald eagle" "sees" "tiger" "+")) -> ("tiger" "chases" "bald eagle" "-"))
If the bear chases the squirrel then the squirrel needs the tiger.
((("bear" "chases" "squirrel" "+")) -> ("squirrel" "needs" "tiger" "+"))
If the squirrel is cold and the squirrel chases the bear then the bear is round.
((("squirrel" "is" "cold" "+") ("squirrel" "chases" "bear" "+")) -> ("bear" "is" "round" "+"))
If the squirrel needs the tiger then the squirrel does not see the bald eagle.
((("squirrel" "needs" "tiger" "+")) -> ("squirrel" "sees" "bald eagle" "-"))
If someone chases the bear then the bear is big.
((("someone" "chases" "bear" "+")) -> ("bear" "is" "big" "+"))
If someone chases the bald eagle and the bald eagle sees the tiger then they chase the bear.
((("someone" "chases" "bald eagle" "+") ("bald eagle" "sees" "tiger" "+")) -> ("someone" "chases" "bear" "+"))
The tiger sees the bear.
True
1
proof
[(triple4)]
("tiger" "sees" "bear" "+")
triple4
The bald eagle needs the tiger.
False
1
inv-proof
[(triple1)]
("bald eagle" "needs" "tiger" "+")
triple1
The squirrel needs the tiger.
True
2
proof
[(((triple2) -> rule4))]
("squirrel" "needs" "tiger" "+")
((triple2) -> (rule4 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel does not need the tiger.
False
2
inv-proof
[(((triple2) -> rule4))]
("squirrel" "needs" "tiger" "-")
((triple2) -> (rule4 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel does not see the bald eagle.
True
3
proof
[(((((triple2) -> rule4)) -> rule6))]
("squirrel" "sees" "bald eagle" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel does not see the bald eagle.
("squirrel" "sees" "bald eagle" "-")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int2
The squirrel does not chase the bear.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("squirrel" "chases" "bear" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int2
The bear is big.
True
4
proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule7))]
("bear" "is" "big" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int3
The bear is not big.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule1)) -> rule7))]
("bear" "is" "big" "-")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int3
The tiger does not chase the bear.
Unknown
inv-rconc
[@1: The tiger chases the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "chases" "bear" "-")
The bald eagle chases the bear.
Unknown
rconc
[@1: The bald eagle chases the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "chases" "bear" "+")
The bald eagle does not chase the tiger.
Unknown
inv-rconc
[@1: The bald eagle chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "chases" "tiger" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "round" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The tiger needs the bear.
Unknown
random
[@0: The tiger needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bear" "+")
The squirrel does not see the tiger.
Unknown
inv-random
[@0: The squirrel sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "tiger" "-")
The bear sees the tiger.
Unknown
random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "+")
@0: The bald eagle does not need the tiger.[(triple1)] The bear chases the squirrel.[(triple2)] The squirrel sees the bear.[(triple3)] The tiger sees the bear.[(triple4)] @1: The squirrel needs the tiger.[(((triple2) -> rule4))] @2: The squirrel chases the bear.[(((((triple2) -> rule4)) -> rule1))] The squirrel does not see the bald eagle.[(((((triple2) -> rule4)) -> rule6))] @3: The bear is big.[(((((((triple2) -> rule4)) -> rule1)) -> rule7))]
The bald eagle does not need the tiger.
("bald eagle" "needs" "tiger" "-")
triple1
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple3
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple4
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
((triple2) -> (rule4 % int1))
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int2
The squirrel does not see the bald eagle.
("squirrel" "sees" "bald eagle" "-")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel does not see the bald eagle.
("squirrel" "sees" "bald eagle" "-")
int1
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int2
The bear is big.
("bear" "is" "big" "+")
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
int2
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
int3