The dog is big. The dog is young. The dog likes the lion. The dog likes the squirrel. The dog sees the lion. The dog visits the lion. The dog visits the squirrel. The lion is red. The lion is rough. The lion likes the squirrel. The lion sees the squirrel. The lion visits the dog. The squirrel is big. The squirrel likes the lion. The squirrel visits the dog. If something is green and it likes the lion then the lion visits the dog. If something sees the squirrel then the squirrel likes the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something is green and it likes the lion then the lion visits the dog.
((("something" "is" "green" "+") ("something" "likes" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If something sees the squirrel then the squirrel likes the dog.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "likes" "dog" "+"))
The dog is big.
True
1
proof
[(triple1)]
("dog" "is" "big" "+")
triple1
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The squirrel does not visit the lion.
Unknown
inv-random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The dog is big.[(triple1)] The dog is young.[(triple2)] The dog likes the lion.[(triple3)] The dog likes the squirrel.[(triple4)] The dog sees the lion.[(triple5)] The dog visits the lion.[(triple6)] The dog visits the squirrel.[(triple7)] The lion is red.[(triple8)] The lion is rough.[(triple9)] The lion likes the squirrel.[(triple10)] The lion sees the squirrel.[(triple11)] The lion visits the dog.[(triple12)] The squirrel is big.[(triple13)] The squirrel likes the lion.[(triple14)] The squirrel visits the dog.[(triple15)] @1: The squirrel likes the dog.[(((triple11) -> rule2))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is young.
("dog" "is" "young" "+")
triple2
The dog likes the lion.
("dog" "likes" "lion" "+")
triple3
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The dog visits the lion.
("dog" "visits" "lion" "+")
triple6
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple7
The lion is red.
("lion" "is" "red" "+")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple10
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple11
The lion visits the dog.
("lion" "visits" "dog" "+")
triple12
The squirrel is big.
("squirrel" "is" "big" "+")
triple13
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple14
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple15
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
((triple11) -> (rule2 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1