The dog chases the lion. The dog is blue. The dog is not kind. The dog is nice. The dog is round. The dog needs the lion. The dog visits the lion. The lion is not cold. The lion is kind. The lion is round. The lion needs the dog. The lion visits the dog. If someone needs the dog and they visit the dog then they visit the lion.
The dog chases the lion.
("dog" "chases" "lion" "+")
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 round.
("dog" "is" "round" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If someone needs the dog and they visit the dog then they visit the lion.
((("someone" "needs" "dog" "+") ("someone" "visits" "dog" "+")) -> ("someone" "visits" "lion" "+"))
The lion needs the dog.
True
1
proof
[(triple11)]
("lion" "needs" "dog" "+")
triple11
The dog is not round.
False
1
inv-proof
[(triple5)]
("dog" "is" "round" "-")
triple5
The lion visits the lion.
True
3
proof
[(((triple11 triple12) -> rule1))]
("lion" "visits" "lion" "+")
((triple11 triple12) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
3
inv-proof
[(((triple11 triple12) -> rule1))]
("lion" "visits" "lion" "-")
((triple11 triple12) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
The lion does not chase the dog.
Unknown
inv-random
[@0: The lion chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog chases the lion.[(triple1)] The dog is blue.[(triple2)] The dog is nice.[(triple4)] The dog is not kind.[(triple3)] The dog is round.[(triple5)] The dog needs the lion.[(triple6)] The dog visits the lion.[(triple7)] The lion is kind.[(triple9)] The lion is not cold.[(triple8)] The lion is round.[(triple10)] The lion needs the dog.[(triple11)] The lion visits the dog.[(triple12)] @1: The lion visits the lion.[(((triple11 triple12) -> rule1))]
The dog chases the lion.
("dog" "chases" "lion" "+")
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 round.
("dog" "is" "round" "+")
triple5
The dog needs the lion.
("dog" "needs" "lion" "+")
triple6
The dog visits the lion.
("dog" "visits" "lion" "+")
triple7
The lion is kind.
("lion" "is" "kind" "+")
triple9
The lion is not cold.
("lion" "is" "cold" "-")
triple8
The lion is round.
("lion" "is" "round" "+")
triple10
The lion needs the dog.
("lion" "needs" "dog" "+")
triple11
The lion visits the dog.
("lion" "visits" "dog" "+")
triple12
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple11 triple12) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1