The bald eagle visits the cow. The cow visits the bald eagle. If something sees the bald eagle and the bald eagle sees the cow then it does not visit the bald eagle. If something is round then it is big. If something sees the cow and it sees the bald eagle then it is big. If the bald eagle chases the cow and the bald eagle is rough then the bald eagle does not see the cow. If something sees the bald eagle then the bald eagle sees the cow. All kind things are young. If something visits the cow then it is kind. If something is round and it does not see the cow then it does not visit the cow.
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
If something sees the bald eagle and the bald eagle sees the cow then it does not visit the bald eagle.
((("something" "sees" "bald eagle" "+") ("bald eagle" "sees" "cow" "+")) -> ("something" "visits" "bald eagle" "-"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something sees the cow and it sees the bald eagle then it is big.
((("something" "sees" "cow" "+") ("something" "sees" "bald eagle" "+")) -> ("something" "is" "big" "+"))
If the bald eagle chases the cow and the bald eagle is rough then the bald eagle does not see the cow.
((("bald eagle" "chases" "cow" "+") ("bald eagle" "is" "rough" "+")) -> ("bald eagle" "sees" "cow" "-"))
If something sees the bald eagle then the bald eagle sees the cow.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "sees" "cow" "+"))
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something visits the cow then it is kind.
((("something" "visits" "cow" "+")) -> ("something" "is" "kind" "+"))
If something is round and it does not see the cow then it does not visit the cow.
((("something" "is" "round" "+") ("something" "sees" "cow" "~")) -> ("something" "visits" "cow" "-"))
The cow visits the bald eagle.
True
1
proof
[(triple2)]
("cow" "visits" "bald eagle" "+")
triple2
The cow does not visit the bald eagle.
False
1
inv-proof
[(triple2)]
("cow" "visits" "bald eagle" "-")
triple2
The bald eagle is kind.
True
2
proof
[(((triple1) -> rule7))]
("bald eagle" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle is not kind.
False
2
inv-proof
[(((triple1) -> rule7))]
("bald eagle" "is" "kind" "-")
((triple1) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle is young.
True
3
proof
[(((((triple1) -> rule7)) -> rule6))]
("bald eagle" "is" "young" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The bald eagle is not young.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6))]
("bald eagle" "is" "young" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The cow is not young.
Unknown
inv-rconc
[@2: The cow is young.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("cow" "is" "young" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "kind" "+")
The bald eagle is not big.
Unknown
inv-rconc
[@1: The bald eagle is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "is" "big" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The bald eagle does not visit the bald eagle.
Unknown
inv-random
[@0: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bald eagle" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle visits the cow.[(triple1)] The cow visits the bald eagle.[(triple2)] @1: The bald eagle is kind.[(((triple1) -> rule7))] @2: The bald eagle is young.[(((((triple1) -> rule7)) -> rule6))]
The bald eagle visits the cow.
("bald eagle" "visits" "cow" "+")
triple1
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
triple2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2