The bald eagle chases the cat. The bald eagle needs the cat. The cat needs the bald eagle. If someone sees the cat then the cat does not see the bald eagle. If someone needs the cat then they are red. If someone needs the bald eagle then the bald eagle needs the cat. If someone chases the cat then the cat does not chase the bald eagle. If the bald eagle does not chase the cat then the cat is green. If someone is red then they see the cat. If the bald eagle chases the cat and the cat is green then the cat needs the bald eagle. If someone chases the bald eagle and they are not green then they are not rough.
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
If someone sees the cat then the cat does not see the bald eagle.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "bald eagle" "-"))
If someone needs the cat then they are red.
((("someone" "needs" "cat" "+")) -> ("someone" "is" "red" "+"))
If someone needs the bald eagle then the bald eagle needs the cat.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "needs" "cat" "+"))
If someone chases the cat then the cat does not chase the bald eagle.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "bald eagle" "-"))
If the bald eagle does not chase the cat then the cat is green.
((("bald eagle" "chases" "cat" "~")) -> ("cat" "is" "green" "+"))
If someone is red then they see the cat.
((("someone" "is" "red" "+")) -> ("someone" "sees" "cat" "+"))
If the bald eagle chases the cat and the cat is green then the cat needs the bald eagle.
((("bald eagle" "chases" "cat" "+") ("cat" "is" "green" "+")) -> ("cat" "needs" "bald eagle" "+"))
If someone chases the bald eagle and they are not green then they are not rough.
((("someone" "chases" "bald eagle" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "rough" "-"))
The bald eagle chases the cat.
True
1
proof
[(triple1)]
("bald eagle" "chases" "cat" "+")
triple1
The cat does not need the bald eagle.
False
1
inv-proof
[(triple3)]
("cat" "needs" "bald eagle" "-")
triple3
The cat does not chase the bald eagle.
True
2
proof
[(((triple1) -> rule4))]
("cat" "chases" "bald eagle" "-")
((triple1) -> (rule4 % int1))
The cat does not chase the bald eagle.
("cat" "chases" "bald eagle" "-")
int1
The cat chases the bald eagle.
False
2
inv-proof
[(((triple1) -> rule4))]
("cat" "chases" "bald eagle" "+")
((triple1) -> (rule4 % int1))
The cat does not chase the bald eagle.
("cat" "chases" "bald eagle" "-")
int1
The bald eagle sees the cat.
True
3
proof
[(((((triple2) -> rule2)) -> rule6) OR ((((((triple3) -> rule3)) -> rule2)) -> rule6))]
("bald eagle" "sees" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int3
The bald eagle does not see the cat.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule6) OR ((((((triple3) -> rule3)) -> rule2)) -> rule6))]
("bald eagle" "sees" "cat" "-")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int3
The cat does not see the bald eagle.
True
4
proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule1) OR ((((((((triple3) -> rule3)) -> rule2)) -> rule6)) -> rule1))]
("cat" "sees" "bald eagle" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not see the bald eagle.
("cat" "sees" "bald eagle" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not see the bald eagle.
("cat" "sees" "bald eagle" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int4
The cat sees the bald eagle.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule6)) -> rule1) OR ((((((((triple3) -> rule3)) -> rule2)) -> rule6)) -> rule1))]
("cat" "sees" "bald eagle" "+")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not see the bald eagle.
("cat" "sees" "bald eagle" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not see the bald eagle.
("cat" "sees" "bald eagle" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int4
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "green" "-")
The cat sees the cat.
Unknown
rconc
[@2: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "red" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat is not round.
Unknown
inv-random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "-")
The bald eagle is green.
Unknown
random
[@0: The bald eagle is green.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "green" "+")
The bald eagle does not need the bald eagle.
Unknown
inv-random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The bald eagle chases the cat.[(triple1)] The bald eagle needs the cat.[(triple2 OR ((triple3) -> rule3))] The cat needs the bald eagle.[(triple3)] @1: The bald eagle is red.[(((triple2) -> rule2) OR ((((triple3) -> rule3)) -> rule2))] The cat does not chase the bald eagle.[(((triple1) -> rule4))] @2: The bald eagle sees the cat.[(((((triple2) -> rule2)) -> rule6) OR ((((((triple3) -> rule3)) -> rule2)) -> rule6))] @3: The cat does not see the bald eagle.[(((((((triple2) -> rule2)) -> rule6)) -> rule1) OR ((((((((triple3) -> rule3)) -> rule2)) -> rule6)) -> rule1))]
The bald eagle chases the cat.
("bald eagle" "chases" "cat" "+")
triple1
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
triple2
((triple3) -> (rule3 % int1))
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple3
The bald eagle is red.
("bald eagle" "is" "red" "+")
((triple2) -> (rule2 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int2
The cat does not chase the bald eagle.
("cat" "chases" "bald eagle" "-")
((triple1) -> (rule4 % int1))
The cat does not chase the bald eagle.
("cat" "chases" "bald eagle" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int3
The cat does not see the bald eagle.
("cat" "sees" "bald eagle" "-")
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not see the bald eagle.
("cat" "sees" "bald eagle" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cat does not see the bald eagle.
("cat" "sees" "bald eagle" "-")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int4