The bald eagle is kind. The bald eagle is young. The bald eagle does not need the squirrel. The bald eagle sees the lion. The bald eagle sees the squirrel. The bald eagle visits the lion. The lion is round. The lion visits the bald eagle. The squirrel is rough. The squirrel does not need the bald eagle. The squirrel sees the lion. The squirrel visits the lion. If something is round and it visits the squirrel then it is rough. If the bald eagle is young and the bald eagle is kind then the bald eagle sees the squirrel. If something needs the bald eagle and the bald eagle visits the squirrel then the bald eagle sees the squirrel. If something is young and it sees the lion then the lion is kind. If something needs the squirrel then the squirrel needs the lion. Rough things are young. If something sees the squirrel then it needs the lion. If something needs the lion then the lion visits the squirrel.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle is young.
("bald eagle" "is" "young" "+")
The bald eagle does not need the squirrel.
("bald eagle" "needs" "squirrel" "-")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
The lion visits the bald eagle.
("lion" "visits" "bald eagle" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel does not need the bald eagle.
("squirrel" "needs" "bald eagle" "-")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something is round and it visits the squirrel then it is rough.
((("something" "is" "round" "+") ("something" "visits" "squirrel" "+")) -> ("something" "is" "rough" "+"))
If the bald eagle is young and the bald eagle is kind then the bald eagle sees the squirrel.
((("bald eagle" "is" "young" "+") ("bald eagle" "is" "kind" "+")) -> ("bald eagle" "sees" "squirrel" "+"))
If something needs the bald eagle and the bald eagle visits the squirrel then the bald eagle sees the squirrel.
((("something" "needs" "bald eagle" "+") ("bald eagle" "visits" "squirrel" "+")) -> ("bald eagle" "sees" "squirrel" "+"))
If something is young and it sees the lion then the lion is kind.
((("something" "is" "young" "+") ("something" "sees" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something needs the squirrel then the squirrel needs the lion.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "lion" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something sees the squirrel then it needs the lion.
((("something" "sees" "squirrel" "+")) -> ("something" "needs" "lion" "+"))
If something needs the lion then the lion visits the squirrel.
((("something" "needs" "lion" "+")) -> ("lion" "visits" "squirrel" "+"))
The lion is round.
True
1
proof
[(triple7)]
("lion" "is" "round" "+")
triple7
The squirrel does not see the lion.
False
1
inv-proof
[(triple11)]
("squirrel" "sees" "lion" "-")
triple11
The bald eagle needs the lion.
True
2
proof
[(((triple5) -> rule7) OR ((((triple2 triple1) -> rule2)) -> rule7))]
("bald eagle" "needs" "lion" "+")
((triple5) -> (rule7 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
((((triple2 triple1) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
The squirrel is not young.
False
2
inv-proof
[(((triple9) -> rule6))]
("squirrel" "is" "young" "-")
((triple9) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The lion visits the squirrel.
True
3
proof
[(((((triple5) -> rule7)) -> rule8) OR ((((((triple2 triple1) -> rule2)) -> rule7)) -> rule8))]
("lion" "visits" "squirrel" "+")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
((((((triple2 triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
The lion does not visit the squirrel.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule8) OR ((((((triple2 triple1) -> rule2)) -> rule7)) -> rule8))]
("lion" "visits" "squirrel" "-")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
((((((triple2 triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
The lion is rough.
True
5
proof
[(((triple7 ((((triple5) -> rule7)) -> rule8)) -> rule1) OR ((triple7 ((((((triple2 triple1) -> rule2)) -> rule7)) -> rule8)) -> rule1))]
("lion" "is" "rough" "+")
((triple7 ((((triple5) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
((triple7 ((((((triple2 triple1) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int4
The lion is not rough.
False
5
inv-proof
[(((triple7 ((((triple5) -> rule7)) -> rule8)) -> rule1) OR ((triple7 ((((((triple2 triple1) -> rule2)) -> rule7)) -> rule8)) -> rule1))]
("lion" "is" "rough" "-")
((triple7 ((((triple5) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
((triple7 ((((((triple2 triple1) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int4
The bald eagle is not rough.
Unknown
inv-rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "rough" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "needs" "lion" "+")
The squirrel does not need the lion.
Unknown
inv-rconc
[@1: The squirrel needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "lion" "-")
The squirrel sees the bald eagle.
Unknown
random
[@0: The squirrel sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bald eagle" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
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" "+")
The lion does not see the bald eagle.
Unknown
inv-random
[@0: The lion sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "bald eagle" "-")
The bald eagle is big.
Unknown
random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "+")
@0: The bald eagle does not need the squirrel.[(triple3)] The bald eagle is kind.[(triple1)] The bald eagle is young.[(triple2)] The bald eagle sees the lion.[(triple4)] The bald eagle sees the squirrel.[(triple5 OR ((triple2 triple1) -> rule2))] The bald eagle visits the lion.[(triple6)] The lion is round.[(triple7)] The lion visits the bald eagle.[(triple8)] The squirrel does not need the bald eagle.[(triple10)] The squirrel is rough.[(triple9)] The squirrel sees the lion.[(triple11)] The squirrel visits the lion.[(triple12)] @1: The bald eagle needs the lion.[(((triple5) -> rule7) OR ((((triple2 triple1) -> rule2)) -> rule7))] The lion is kind.[(((triple2 triple4) -> rule4) OR ((((triple9) -> rule6) triple11) -> rule4))] The squirrel is young.[(((triple9) -> rule6))] @2: The lion visits the squirrel.[(((((triple5) -> rule7)) -> rule8) OR ((((((triple2 triple1) -> rule2)) -> rule7)) -> rule8))] @3: The lion is rough.[(((triple7 ((((triple5) -> rule7)) -> rule8)) -> rule1) OR ((triple7 ((((((triple2 triple1) -> rule2)) -> rule7)) -> rule8)) -> rule1))] @4: The lion is young.[(((((triple7 ((((triple5) -> rule7)) -> rule8)) -> rule1)) -> rule6) OR ((((triple7 ((((((triple2 triple1) -> rule2)) -> rule7)) -> rule8)) -> rule1)) -> rule6))]
The bald eagle does not need the squirrel.
("bald eagle" "needs" "squirrel" "-")
triple3
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The bald eagle is young.
("bald eagle" "is" "young" "+")
triple2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple4
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
triple5
((triple2 triple1) -> (rule2 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
triple6
The lion is round.
("lion" "is" "round" "+")
triple7
The lion visits the bald eagle.
("lion" "visits" "bald eagle" "+")
triple8
The squirrel does not need the bald eagle.
("squirrel" "needs" "bald eagle" "-")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple11
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
((triple5) -> (rule7 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
((((triple2 triple1) -> (rule2 % int2))) -> (rule7 % int1))
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int1
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
((triple2 triple4) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple9) -> (rule6 % int2)) triple11) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((triple9) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
((((((triple2 triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
((triple7 ((((triple5) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
((triple7 ((((((triple2 triple1) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int4
The lion is young.
("lion" "is" "young" "+")
((((triple7 ((((triple5) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int4
((((triple7 ((((((triple2 triple1) -> (rule2 % int5))) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int3
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
int4
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int5