The dog is big. The dog is blue. The dog is not kind. The dog is nice. The dog is young. The dog needs the lion. The dog sees the lion. The dog visits the lion. The lion is big. The lion is blue. The lion is kind. The lion is nice. The lion is not young. The lion needs the dog. The lion sees the dog. The lion visits the dog. If someone needs the lion and the lion visits the dog then the dog sees the lion. If someone is big and they need the dog then the dog sees the lion. If someone needs the dog and the dog does not visit the lion then the lion does not need the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is not kind.
("dog" "is" "kind" "-")
The dog is nice.
("dog" "is" "nice" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone needs the lion and the lion visits the dog then the dog sees the lion.
((("someone" "needs" "lion" "+") ("lion" "visits" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If someone is big and they need the dog then the dog sees the lion.
((("someone" "is" "big" "+") ("someone" "needs" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If someone needs the dog and the dog does not visit the lion then the lion does not need the dog.
((("someone" "needs" "dog" "+") ("dog" "visits" "lion" "~")) -> ("lion" "needs" "dog" "-"))
The lion needs the dog.
True
1
proof
[(triple14)]
("lion" "needs" "dog" "+")
triple14
The dog is not young.
False
1
inv-proof
[(triple5)]
("dog" "is" "young" "-")
triple5
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The dog is big.[(triple1)] The dog is blue.[(triple2)] The dog is nice.[(triple4)] The dog is not kind.[(triple3)] The dog is young.[(triple5)] The dog needs the lion.[(triple6)] The dog sees the lion.[(triple7 OR ((triple6 triple16) -> rule1) OR ((triple9 triple14) -> rule2))] The dog visits the lion.[(triple8)] The lion is big.[(triple9)] The lion is blue.[(triple10)] The lion is kind.[(triple11)] The lion is nice.[(triple12)] The lion is not young.[(triple13)] The lion needs the dog.[(triple14)] The lion sees the dog.[(triple15)] The lion visits the dog.[(triple16)]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple4
The dog is not kind.
("dog" "is" "kind" "-")
triple3
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The dog sees the lion.
("dog" "sees" "lion" "+")
triple7
((triple6 triple16) -> (rule1 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
((triple9 triple14) -> (rule2 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple8
The lion is big.
("lion" "is" "big" "+")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion is kind.
("lion" "is" "kind" "+")
triple11
The lion is nice.
("lion" "is" "nice" "+")
triple12
The lion is not young.
("lion" "is" "young" "-")
triple13
The lion needs the dog.
("lion" "needs" "dog" "+")
triple14
The lion sees the dog.
("lion" "sees" "dog" "+")
triple15
The lion visits the dog.
("lion" "visits" "dog" "+")
triple16