The bald eagle sees the lion. The cat sees the bald eagle. The cow sees the bald eagle. The lion is round. If the bald eagle is kind then the bald eagle visits the cat. If something visits the cat then the cat eats the cow. If something visits the cat and it sees the cat then the cat is round. If something visits the lion then the lion visits the bald eagle. If something is rough and it visits the lion then the lion eats the cow. If something eats the bald eagle and the bald eagle is round then the bald eagle visits the lion. If something sees the bald eagle then the bald eagle is kind. If something visits the cat then the cat visits the bald eagle.
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The lion is round.
("lion" "is" "round" "+")
If the bald eagle is kind then the bald eagle visits the cat.
((("bald eagle" "is" "kind" "+")) -> ("bald eagle" "visits" "cat" "+"))
If something visits the cat then the cat eats the cow.
((("something" "visits" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If something visits the cat and it sees the cat then the cat is round.
((("something" "visits" "cat" "+") ("something" "sees" "cat" "+")) -> ("cat" "is" "round" "+"))
If something visits the lion then the lion visits the bald eagle.
((("something" "visits" "lion" "+")) -> ("lion" "visits" "bald eagle" "+"))
If something is rough and it visits the lion then the lion eats the cow.
((("something" "is" "rough" "+") ("something" "visits" "lion" "+")) -> ("lion" "eats" "cow" "+"))
If something eats the bald eagle and the bald eagle is round then the bald eagle visits the lion.
((("something" "eats" "bald eagle" "+") ("bald eagle" "is" "round" "+")) -> ("bald eagle" "visits" "lion" "+"))
If something sees the bald eagle then the bald eagle is kind.
((("something" "sees" "bald eagle" "+")) -> ("bald eagle" "is" "kind" "+"))
If something visits the cat then the cat visits the bald eagle.
((("something" "visits" "cat" "+")) -> ("cat" "visits" "bald eagle" "+"))
The cat sees the bald eagle.
True
1
proof
[(triple2)]
("cat" "sees" "bald eagle" "+")
triple2
The cat does not see the bald eagle.
False
1
inv-proof
[(triple2)]
("cat" "sees" "bald eagle" "-")
triple2
The bald eagle is kind.
True
2
proof
[(((triple2) -> rule7) OR ((triple3) -> rule7))]
("bald eagle" "is" "kind" "+")
((triple2) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
((triple3) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle is not kind.
False
2
inv-proof
[(((triple2) -> rule7) OR ((triple3) -> rule7))]
("bald eagle" "is" "kind" "-")
((triple2) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
((triple3) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle visits the cat.
True
3
proof
[(((((triple2) -> rule7)) -> rule1) OR ((((triple3) -> rule7)) -> rule1))]
("bald eagle" "visits" "cat" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The bald eagle does not visit the cat.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule1) OR ((((triple3) -> rule7)) -> rule1))]
("bald eagle" "visits" "cat" "-")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The cat visits the bald eagle.
True
4
proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule8) OR ((((((triple3) -> rule7)) -> rule1)) -> rule8))]
("cat" "visits" "bald eagle" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
The cat does not eat the cow.
False
4
inv-proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule2) OR ((((((triple3) -> rule7)) -> rule1)) -> rule2))]
("cat" "eats" "cow" "-")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
The lion does not eat the cow.
Unknown
inv-rconc
[@1: The lion eats the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "cow" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "round" "+")
The lion does not visit the bald eagle.
Unknown
inv-rconc
[@2: The lion visits the bald eagle.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("lion" "visits" "bald eagle" "-")
The bald eagle visits the lion.
Unknown
rconc
[@1: The bald eagle visits the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "visits" "lion" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The bald eagle eats the bald eagle.
Unknown
random
[@0: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The cow does not eat the lion.
Unknown
inv-random
[@0: The cow eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bald eagle sees the lion.[(triple1)] The cat sees the bald eagle.[(triple2)] The cow sees the bald eagle.[(triple3)] The lion is round.[(triple4)] @1: The bald eagle is kind.[(((triple2) -> rule7) OR ((triple3) -> rule7))] @2: The bald eagle visits the cat.[(((((triple2) -> rule7)) -> rule1) OR ((((triple3) -> rule7)) -> rule1))] @3: The cat eats the cow.[(((((((triple2) -> rule7)) -> rule1)) -> rule2) OR ((((((triple3) -> rule7)) -> rule1)) -> rule2))] The cat visits the bald eagle.[(((((((triple2) -> rule7)) -> rule1)) -> rule8) OR ((((((triple3) -> rule7)) -> rule1)) -> rule8))]
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple2
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
((triple2) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
((triple3) -> (rule7 % int1))
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
int3