The dog is not blue. The lion is cold. The rabbit visits the dog. If someone chases the lion and the lion does not chase the rabbit then the lion does not visit the rabbit. If someone chases the rabbit then they visit the rabbit. If someone likes the dog and the dog likes the rabbit then the rabbit chases the dog. If someone chases the dog then the dog is not big. If the rabbit is not blue then the rabbit chases the lion. If someone is cold then they chase the dog.
The dog is not blue.
("dog" "is" "blue" "-")
The lion is cold.
("lion" "is" "cold" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone chases the lion and the lion does not chase the rabbit then the lion does not visit the rabbit.
((("someone" "chases" "lion" "+") ("lion" "chases" "rabbit" "~")) -> ("lion" "visits" "rabbit" "-"))
If someone chases the rabbit then they visit the rabbit.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone likes the dog and the dog likes the rabbit then the rabbit chases the dog.
((("someone" "likes" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("rabbit" "chases" "dog" "+"))
If someone chases the dog then the dog is not big.
((("someone" "chases" "dog" "+")) -> ("dog" "is" "big" "-"))
If the rabbit is not blue then the rabbit chases the lion.
((("rabbit" "is" "blue" "~")) -> ("rabbit" "chases" "lion" "+"))
If someone is cold then they chase the dog.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "dog" "+"))
The rabbit visits the dog.
True
1
proof
[(triple3)]
("rabbit" "visits" "dog" "+")
triple3
The lion is not cold.
False
1
inv-proof
[(triple2)]
("lion" "is" "cold" "-")
triple2
The lion chases the dog.
True
2
proof
[(((triple2) -> rule6))]
("lion" "chases" "dog" "+")
((triple2) -> (rule6 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion does not chase the dog.
False
2
inv-proof
[(((triple2) -> rule6))]
("lion" "chases" "dog" "-")
((triple2) -> (rule6 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "dog" "+")
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 dog likes the rabbit.
Unknown
random
[@0: The dog likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "rabbit" "+")
@0: The dog is not blue.[(triple1)] The lion is cold.[(triple2)] The rabbit visits the dog.[(triple3)] @1: The lion chases the dog.[(((triple2) -> rule6))] @2: The dog is not big.[(((((triple2) -> rule6)) -> rule4))]
The dog is not blue.
("dog" "is" "blue" "-")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple3
The lion chases the dog.
("lion" "chases" "dog" "+")
((triple2) -> (rule6 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The dog is not big.
("dog" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The dog is not big.
("dog" "is" "big" "-")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2