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