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