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