The lion is cold. The lion is nice. The lion is rough. The lion is round. The lion is young. The lion needs the squirrel. The lion sees the squirrel. The lion visits the squirrel. The squirrel is cold. The squirrel is nice. The squirrel is rough. The squirrel is round. The squirrel needs the lion. The squirrel sees the lion. The squirrel visits the lion. If something sees the lion and it needs the lion then the lion visits the squirrel. If the squirrel sees the lion then the squirrel is cold.
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 is young.
("lion" "is" "young" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something sees the lion and it needs the lion then the lion visits the squirrel.
((("something" "sees" "lion" "+") ("something" "needs" "lion" "+")) -> ("lion" "visits" "squirrel" "+"))
If the squirrel sees the lion then the squirrel is cold.
((("squirrel" "sees" "lion" "+")) -> ("squirrel" "is" "cold" "+"))
The squirrel is cold.
True
1
proof
[(triple9 OR ((triple14) -> rule2))]
("squirrel" "is" "cold" "+")
triple9
((triple14) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The lion does not visit the squirrel.
False
1
inv-proof
[(triple8 OR ((triple14 triple13) -> rule1))]
("lion" "visits" "squirrel" "-")
triple8
((triple14 triple13) -> (rule1 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
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 lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion is cold.[(triple1)] The lion is nice.[(triple2)] The lion is rough.[(triple3)] The lion is round.[(triple4)] The lion is young.[(triple5)] The lion needs the squirrel.[(triple6)] The lion sees the squirrel.[(triple7)] The lion visits the squirrel.[(triple8 OR ((triple14 triple13) -> rule1))] The squirrel is cold.[(triple9 OR ((triple14) -> rule2))] The squirrel is nice.[(triple10)] The squirrel is rough.[(triple11)] The squirrel is round.[(triple12)] The squirrel needs the lion.[(triple13)] The squirrel sees the lion.[(triple14)] The squirrel visits the lion.[(triple15)]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple6
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple7
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple8
((triple14 triple13) -> (rule1 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
((triple14) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel is round.
("squirrel" "is" "round" "+")
triple12
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple13
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple14
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple15