The dog is cold. The dog needs the lion. The lion chases the dog. The lion is cold. The lion is round. The lion is young. The lion likes the dog. If something needs the lion then it chases the dog. If something is big and cold then it likes the dog. If something needs the lion and the lion likes the dog then the dog needs the lion.
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
If something needs the lion then it chases the dog.
((("something" "needs" "lion" "+")) -> ("something" "chases" "dog" "+"))
If something is big and cold then it likes the dog.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "likes" "dog" "+"))
If something needs the lion and the lion likes the dog then the dog needs the lion.
((("something" "needs" "lion" "+") ("lion" "likes" "dog" "+")) -> ("dog" "needs" "lion" "+"))
The lion is round.
True
1
proof
[(triple5)]
("lion" "is" "round" "+")
triple5
The lion does not chase the dog.
False
1
inv-proof
[(triple3)]
("lion" "chases" "dog" "-")
triple3
The dog chases the dog.
True
2
proof
[(((triple2) -> rule1))]
("dog" "chases" "dog" "+")
((triple2) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("dog" "chases" "dog" "-")
((triple2) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "dog" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The dog is cold.[(triple1)] The dog needs the lion.[(triple2)] The lion chases the dog.[(triple3)] The lion is cold.[(triple4)] The lion is round.[(triple5)] The lion is young.[(triple6)] The lion likes the dog.[(triple7)] @1: The dog chases the dog.[(((triple2) -> rule1))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog needs the lion.
("dog" "needs" "lion" "+")
triple2
The lion chases the dog.
("lion" "chases" "dog" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion likes the dog.
("lion" "likes" "dog" "+")
triple7
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple2) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1