The bald eagle is round. The cat needs the mouse. The mouse visits the cat. If someone needs the mouse then they like the bald eagle. If someone needs the mouse then they are green. If someone likes the cat then they need the cat. If someone needs the bald eagle and they are blue then they are round. If someone visits the bald eagle and they are cold then the bald eagle likes the cat. If someone likes the bald eagle then the bald eagle needs the mouse. If someone is blue and green then they need the mouse. If someone needs the cat then they visit the cat.
The bald eagle is round.
("bald eagle" "is" "round" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If someone needs the mouse then they like the bald eagle.
((("someone" "needs" "mouse" "+")) -> ("someone" "likes" "bald eagle" "+"))
If someone needs the mouse then they are green.
((("someone" "needs" "mouse" "+")) -> ("someone" "is" "green" "+"))
If someone likes the cat then they need the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the bald eagle and they are blue then they are round.
((("someone" "needs" "bald eagle" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone visits the bald eagle and they are cold then the bald eagle likes the cat.
((("someone" "visits" "bald eagle" "+") ("someone" "is" "cold" "+")) -> ("bald eagle" "likes" "cat" "+"))
If someone likes the bald eagle then the bald eagle needs the mouse.
((("someone" "likes" "bald eagle" "+")) -> ("bald eagle" "needs" "mouse" "+"))
If someone is blue and green then they need the mouse.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the cat then they visit the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "visits" "cat" "+"))
The bald eagle is round.
True
1
proof
[(triple1)]
("bald eagle" "is" "round" "+")
triple1
The mouse does not visit the cat.
False
1
inv-proof
[(triple3)]
("mouse" "visits" "cat" "-")
triple3
The cat likes the bald eagle.
True
2
proof
[(((triple2) -> rule1))]
("cat" "likes" "bald eagle" "+")
((triple2) -> (rule1 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The cat does not like the bald eagle.
False
2
inv-proof
[(((triple2) -> rule1))]
("cat" "likes" "bald eagle" "-")
((triple2) -> (rule1 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The bald eagle needs the mouse.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("bald eagle" "needs" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The bald eagle does not need the mouse.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("bald eagle" "needs" "mouse" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The bald eagle is green.
True
4
proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule2))]
("bald eagle" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int3
The bald eagle is not green.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule6)) -> rule2))]
("bald eagle" "is" "green" "-")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int3
The cat does not visit the cat.
Unknown
inv-rconc
[@2: The cat visits the cat.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("cat" "visits" "cat" "-")
The bald eagle visits the cat.
Unknown
rconc
[@3: The bald eagle visits the cat.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule5 <- FAIL)]]
("bald eagle" "visits" "cat" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "round" "+")
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 mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The cat does not visit the bald eagle.
Unknown
inv-random
[@0: The cat visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "bald eagle" "-")
The bald eagle is blue.
Unknown
random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "+")
@0: The bald eagle is round.[(triple1)] The cat needs the mouse.[(triple2)] The mouse visits the cat.[(triple3)] @1: The cat is green.[(((triple2) -> rule2))] The cat likes the bald eagle.[(((triple2) -> rule1))] @2: The bald eagle needs the mouse.[(((((triple2) -> rule1)) -> rule6))] @3: The bald eagle is green.[(((((((triple2) -> rule1)) -> rule6)) -> rule2))] The bald eagle likes the bald eagle.[(((((((triple2) -> rule1)) -> rule6)) -> rule1))]
The bald eagle is round.
("bald eagle" "is" "round" "+")
triple1
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
((triple2) -> (rule2 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
((triple2) -> (rule1 % int1))
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int2
The bald eagle is green.
("bald eagle" "is" "green" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle is green.
("bald eagle" "is" "green" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int3
The bald eagle likes the bald eagle.
("bald eagle" "likes" "bald eagle" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bald eagle likes the bald eagle.
("bald eagle" "likes" "bald eagle" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The cat likes the bald eagle.
("cat" "likes" "bald eagle" "+")
int3