The lion eats the squirrel. The lion is cold. The lion is nice. The lion is rough. The lion is round. The lion needs the squirrel. The lion visits the squirrel. The squirrel does not eat the lion. The squirrel is nice. The squirrel is rough. The squirrel is young. The squirrel visits the lion. If someone is cold and they do not eat the lion then the lion is cold. If the squirrel does not eat the lion then the squirrel needs the lion. If someone visits the lion and the lion visits the squirrel then the lion eats the squirrel. If someone eats the squirrel and the squirrel is not cold then the squirrel visits the lion. If someone needs the squirrel and the squirrel is round then the squirrel visits the lion. If someone is nice then they visit the squirrel. If someone is rough then they need the lion. If someone visits the lion and the lion is round then the lion needs the squirrel.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel does not eat the lion.
("squirrel" "eats" "lion" "-")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If someone is cold and they do not eat the lion then the lion is cold.
((("someone" "is" "cold" "+") ("someone" "eats" "lion" "~")) -> ("lion" "is" "cold" "+"))
If the squirrel does not eat the lion then the squirrel needs the lion.
((("squirrel" "eats" "lion" "~")) -> ("squirrel" "needs" "lion" "+"))
If someone visits the lion and the lion visits the squirrel then the lion eats the squirrel.
((("someone" "visits" "lion" "+") ("lion" "visits" "squirrel" "+")) -> ("lion" "eats" "squirrel" "+"))
If someone eats the squirrel and the squirrel is not cold then the squirrel visits the lion.
((("someone" "eats" "squirrel" "+") ("squirrel" "is" "cold" "~")) -> ("squirrel" "visits" "lion" "+"))
If someone needs the squirrel and the squirrel is round then the squirrel visits the lion.
((("someone" "needs" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("squirrel" "visits" "lion" "+"))
If someone is nice then they visit the squirrel.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone is rough then they need the lion.
((("someone" "is" "rough" "+")) -> ("someone" "needs" "lion" "+"))
If someone visits the lion and the lion is round then the lion needs the squirrel.
((("someone" "visits" "lion" "+") ("lion" "is" "round" "+")) -> ("lion" "needs" "squirrel" "+"))
The lion is round.
True
1
proof
[(triple5)]
("lion" "is" "round" "+")
triple5
The lion does not eat the squirrel.
False
1
inv-proof
[(triple1 OR ((triple12 triple7) -> rule3) OR ((triple12 ((triple3) -> rule6)) -> rule3))]
("lion" "eats" "squirrel" "-")
triple1
((triple12 triple7) -> (rule3 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
((triple12 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The squirrel visits the squirrel.
True
2
proof
[(((triple9) -> rule6))]
("squirrel" "visits" "squirrel" "+")
((triple9) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple4) -> rule7))]
("lion" "needs" "lion" "-")
((triple4) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The lion eats the squirrel.[(triple1 OR ((triple12 triple7) -> rule3) OR ((triple12 ((triple3) -> rule6)) -> rule3))] The lion is cold.[(triple2)] The lion is nice.[(triple3)] The lion is rough.[(triple4)] The lion is round.[(triple5)] The lion needs the squirrel.[(triple6 OR ((triple12 triple5) -> rule8))] The lion visits the squirrel.[(triple7 OR ((triple3) -> rule6))] The squirrel does not eat the lion.[(triple8)] The squirrel is nice.[(triple9)] The squirrel is rough.[(triple10)] The squirrel is young.[(triple11)] The squirrel visits the lion.[(triple12)] @1: The lion needs the lion.[(((triple4) -> rule7))] The squirrel needs the lion.[(((triple10) -> rule7) OR ((triple8) -> rule2))] The squirrel visits the squirrel.[(((triple9) -> rule6))]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
((triple12 triple7) -> (rule3 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
((triple12 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple6
((triple12 triple5) -> (rule8 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple7
((triple3) -> (rule6 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The squirrel does not eat the lion.
("squirrel" "eats" "lion" "-")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
The squirrel is young.
("squirrel" "is" "young" "+")
triple11
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple4) -> (rule7 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((triple10) -> (rule7 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
((triple8) -> (rule2 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple9) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1