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