The bald eagle is big. The bald eagle is green. The bald eagle is rough. The bald eagle needs the mouse. The bald eagle needs the rabbit. The cat likes the bald eagle. The cat visits the bald eagle. The mouse is green. The mouse is rough. The rabbit is rough. If something is young then it needs the rabbit. If something is green then it visits the cat. If the rabbit needs the cat and the rabbit needs the mouse then the cat visits the bald eagle. If something visits the cat then it is young. If something visits the mouse and the mouse likes the bald eagle then the bald eagle is cold. If something needs the bald eagle then it needs the cat. If something needs the mouse and it is big then it is cold. If something likes the bald eagle then it is rough.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The bald eagle is green.
("bald eagle" "is" "green" "+")
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If something is young then it needs the rabbit.
((("something" "is" "young" "+")) -> ("something" "needs" "rabbit" "+"))
If something is green then it visits the cat.
((("something" "is" "green" "+")) -> ("something" "visits" "cat" "+"))
If the rabbit needs the cat and the rabbit needs the mouse then the cat visits the bald eagle.
((("rabbit" "needs" "cat" "+") ("rabbit" "needs" "mouse" "+")) -> ("cat" "visits" "bald eagle" "+"))
If something visits the cat then it is young.
((("something" "visits" "cat" "+")) -> ("something" "is" "young" "+"))
If something visits the mouse and the mouse likes the bald eagle then the bald eagle is cold.
((("something" "visits" "mouse" "+") ("mouse" "likes" "bald eagle" "+")) -> ("bald eagle" "is" "cold" "+"))
If something needs the bald eagle then it needs the cat.
((("something" "needs" "bald eagle" "+")) -> ("something" "needs" "cat" "+"))
If something needs the mouse and it is big then it is cold.
((("something" "needs" "mouse" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something likes the bald eagle then it is rough.
((("something" "likes" "bald eagle" "+")) -> ("something" "is" "rough" "+"))
The bald eagle needs the mouse.
True
1
proof
[(triple4)]
("bald eagle" "needs" "mouse" "+")
triple4
The rabbit is not rough.
False
1
inv-proof
[(triple10)]
("rabbit" "is" "rough" "-")
triple10
The cat is rough.
True
2
proof
[(((triple6) -> rule8))]
("cat" "is" "rough" "+")
((triple6) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple6) -> rule8))]
("cat" "is" "rough" "-")
((triple6) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The bald eagle is young.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("bald eagle" "is" "young" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The mouse is not young.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule4))]
("mouse" "is" "young" "-")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The mouse needs the rabbit.
True
4
proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule1))]
("mouse" "needs" "rabbit" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The mouse does not need the rabbit.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule1))]
("mouse" "needs" "rabbit" "-")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "cold" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "cat" "+")
The rabbit is not cold.
Unknown
inv-rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "cold" "-")
The bald eagle needs the cat.
Unknown
rconc
[@1: The bald eagle needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "needs" "cat" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The bald eagle likes the cat.
Unknown
random
[@0: The bald eagle likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "cat" "+")
The mouse does not need the bald eagle.
Unknown
inv-random
[@0: The mouse needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bald eagle" "-")
The bald eagle visits the rabbit.
Unknown
random
[@0: The bald eagle visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "rabbit" "+")
@0: The bald eagle is big.[(triple1)] The bald eagle is green.[(triple2)] The bald eagle is rough.[(triple3)] The bald eagle needs the mouse.[(triple4)] The bald eagle needs the rabbit.[(triple5 OR ((((((triple2) -> rule2)) -> rule4)) -> rule1))] The cat likes the bald eagle.[(triple6)] The cat visits the bald eagle.[(triple7)] The mouse is green.[(triple8)] The mouse is rough.[(triple9)] The rabbit is rough.[(triple10)] @1: The bald eagle is cold.[(((triple4 triple1) -> rule7))] The bald eagle visits the cat.[(((triple2) -> rule2))] The cat is rough.[(((triple6) -> rule8))] The mouse visits the cat.[(((triple8) -> rule2))] @2: The bald eagle is young.[(((((triple2) -> rule2)) -> rule4))] The mouse is young.[(((((triple8) -> rule2)) -> rule4))] @3: The mouse needs the rabbit.[(((((((triple8) -> rule2)) -> rule4)) -> rule1))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple2
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple3
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple4
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple5
((((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int3
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
triple6
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((triple4 triple1) -> (rule7 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
((triple6) -> (rule8 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((triple8) -> (rule2 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int2
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int3