The bald eagle is blue. The bald eagle is red. The bald eagle is rough. The bald eagle sees the cat. The cat is young. The cat needs the bald eagle. The cat needs the tiger. The cat sees the tiger. The cat visits the bald eagle. The tiger is cold. The tiger is red. The tiger needs the bald eagle. The tiger needs the cat. The tiger sees the bald eagle. The tiger visits the bald eagle. The tiger visits the cat. If someone needs the tiger then they are red. If the bald eagle is rough and the bald eagle sees the cat then the bald eagle needs the tiger. If someone visits the tiger then they visit the bald eagle. If someone is rough then they visit the tiger. If someone is red and they visit the tiger then they need the bald eagle. If someone visits the bald eagle then they need the cat.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If someone needs the tiger then they are red.
((("someone" "needs" "tiger" "+")) -> ("someone" "is" "red" "+"))
If the bald eagle is rough and the bald eagle sees the cat then the bald eagle needs the tiger.
((("bald eagle" "is" "rough" "+") ("bald eagle" "sees" "cat" "+")) -> ("bald eagle" "needs" "tiger" "+"))
If someone visits the tiger then they visit the bald eagle.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone is rough then they visit the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "visits" "tiger" "+"))
If someone is red and they visit the tiger then they need the bald eagle.
((("someone" "is" "red" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "needs" "bald eagle" "+"))
If someone visits the bald eagle then they need the cat.
((("someone" "visits" "bald eagle" "+")) -> ("someone" "needs" "cat" "+"))
The tiger sees the bald eagle.
True
1
proof
[(triple14)]
("tiger" "sees" "bald eagle" "+")
triple14
The tiger is not cold.
False
1
inv-proof
[(triple10)]
("tiger" "is" "cold" "-")
triple10
The cat is red.
True
2
proof
[(((triple7) -> rule1))]
("cat" "is" "red" "+")
((triple7) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple7) -> rule1))]
("cat" "is" "red" "-")
((triple7) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bald eagle visits the bald eagle.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("bald eagle" "visits" "bald eagle" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bald eagle does not need the bald eagle.
False
4
inv-proof
[(((triple2 ((triple3) -> rule4)) -> rule5) OR ((((((triple3 triple4) -> rule2)) -> rule1) ((triple3) -> rule4)) -> rule5))]
("bald eagle" "needs" "bald eagle" "-")
((triple2 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
((((((triple3 triple4) -> (rule2 % int4))) -> (rule1 % int3)) ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int4
The bald eagle needs the cat.
True
4
proof
[(((((((triple3) -> rule4)) -> rule3)) -> rule6))]
("bald eagle" "needs" "cat" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int3
The bald eagle does not need the cat.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule3)) -> rule6))]
("bald eagle" "needs" "cat" "-")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int3
The cat does not visit the tiger.
Unknown
inv-rconc
[@1: The cat visits the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The bald eagle is cold.
Unknown
random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger sees the cat.
Unknown
random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "+")
@0: The bald eagle is blue.[(triple1)] The bald eagle is red.[(triple2 OR ((((triple3 triple4) -> rule2)) -> rule1))] The bald eagle is rough.[(triple3)] The bald eagle sees the cat.[(triple4)] The cat is young.[(triple5)] The cat needs the bald eagle.[(triple6)] The cat needs the tiger.[(triple7)] The cat sees the tiger.[(triple8)] The cat visits the bald eagle.[(triple9)] The tiger is cold.[(triple10)] The tiger is red.[(triple11)] The tiger needs the bald eagle.[(triple12)] The tiger needs the cat.[(triple13 OR ((triple15) -> rule6))] The tiger sees the bald eagle.[(triple14)] The tiger visits the bald eagle.[(triple15)] The tiger visits the cat.[(triple16)] @1: The bald eagle needs the tiger.[(((triple3 triple4) -> rule2))] The bald eagle visits the tiger.[(((triple3) -> rule4))] The cat is red.[(((triple7) -> rule1))] The cat needs the cat.[(((triple9) -> rule6))] @2: The bald eagle needs the bald eagle.[(((triple2 ((triple3) -> rule4)) -> rule5) OR ((((((triple3 triple4) -> rule2)) -> rule1) ((triple3) -> rule4)) -> rule5))] The bald eagle visits the bald eagle.[(((((triple3) -> rule4)) -> rule3))] @3: The bald eagle needs the cat.[(((((((triple3) -> rule4)) -> rule3)) -> rule6))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple2
((((triple3 triple4) -> (rule2 % int2))) -> (rule1 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int2
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple3
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple4
The cat is young.
("cat" "is" "young" "+")
triple5
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple6
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple7
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple8
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple12
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple13
((triple15) -> (rule6 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
triple14
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
triple15
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple16
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
((triple3 triple4) -> (rule2 % int1))
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
((triple3) -> (rule4 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((triple7) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((triple9) -> (rule6 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
((triple2 ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
((((((triple3 triple4) -> (rule2 % int4))) -> (rule1 % int3)) ((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle needs the tiger.
("bald eagle" "needs" "tiger" "+")
int4
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int2
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
((((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int3