The bald eagle needs the squirrel. The lion needs the bald eagle. The squirrel is round. If someone needs the lion and the lion sees the squirrel then the squirrel does not like the bald eagle. All young people are red. If someone likes the lion and the lion is round then they see the lion. If someone is round then they see the lion. If someone likes the squirrel then they like the lion. If someone sees the squirrel then they like the lion. If someone is young then they like the bald eagle. If someone sees the lion and they are round then the lion sees the squirrel.
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone needs the lion and the lion sees the squirrel then the squirrel does not like the bald eagle.
((("someone" "needs" "lion" "+") ("lion" "sees" "squirrel" "+")) -> ("squirrel" "likes" "bald eagle" "-"))
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone likes the lion and the lion is round then they see the lion.
((("someone" "likes" "lion" "+") ("lion" "is" "round" "+")) -> ("someone" "sees" "lion" "+"))
If someone is round then they see the lion.
((("someone" "is" "round" "+")) -> ("someone" "sees" "lion" "+"))
If someone likes the squirrel then they like the lion.
((("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "lion" "+"))
If someone sees the squirrel then they like the lion.
((("someone" "sees" "squirrel" "+")) -> ("someone" "likes" "lion" "+"))
If someone is young then they like the bald eagle.
((("someone" "is" "young" "+")) -> ("someone" "likes" "bald eagle" "+"))
If someone sees the lion and they are round then the lion sees the squirrel.
((("someone" "sees" "lion" "+") ("someone" "is" "round" "+")) -> ("lion" "sees" "squirrel" "+"))
The squirrel is round.
True
1
proof
[(triple3)]
("squirrel" "is" "round" "+")
triple3
The bald eagle does not need the squirrel.
False
1
inv-proof
[(triple1)]
("bald eagle" "needs" "squirrel" "-")
triple1
The squirrel sees the lion.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "sees" "lion" "+")
((triple3) -> (rule4 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel does not see the lion.
False
2
inv-proof
[(((triple3) -> rule4))]
("squirrel" "sees" "lion" "-")
((triple3) -> (rule4 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The lion sees the squirrel.
True
4
proof
[(((((triple3) -> rule4) triple3) -> rule8))]
("lion" "sees" "squirrel" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule8 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion does not see the squirrel.
False
4
inv-proof
[(((((triple3) -> rule4) triple3) -> rule8))]
("lion" "sees" "squirrel" "-")
((((triple3) -> (rule4 % int2)) triple3) -> (rule8 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion likes the lion.
True
5
proof
[(((((((triple3) -> rule4) triple3) -> rule8)) -> rule6))]
("lion" "likes" "lion" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule8 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The lion does not like the lion.
False
5
inv-proof
[(((((((triple3) -> rule4) triple3) -> rule8)) -> rule6))]
("lion" "likes" "lion" "-")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule8 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The lion does not like the bald eagle.
Unknown
inv-rconc
[@1: The lion likes the bald eagle.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "likes" "bald eagle" "-")
The bald eagle sees the lion.
Unknown
rconc
[@1: The bald eagle sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "sees" "lion" "+")
The bald eagle does not like the lion.
Unknown
inv-rconc
[@1: The bald eagle likes the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "likes" "lion" "-")
The squirrel likes the lion.
Unknown
rconc
[@1: The squirrel likes the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "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 squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The bald eagle needs the squirrel.[(triple1)] The lion needs the bald eagle.[(triple2)] The squirrel is round.[(triple3)] @1: The squirrel sees the lion.[(((triple3) -> rule4))] @2: The lion sees the squirrel.[(((((triple3) -> rule4) triple3) -> rule8))] @3: The lion likes the lion.[(((((((triple3) -> rule4) triple3) -> rule8)) -> rule6))]
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
triple1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
triple2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple3) -> (rule4 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule8 % int1))
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule8 % int2))) -> (rule6 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3