The cat chases the lion. The cat is nice. The cat visits the lion. The dog chases the cat. The dog is cold. The dog is nice. The dog needs the cat. The dog visits the lion. The dog visits the rabbit. The lion chases the rabbit. The rabbit is cold. The rabbit is red. The rabbit needs the dog. The rabbit visits the cat. The rabbit visits the lion. If the dog visits the lion then the dog chases the lion.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The dog chases the cat.
("dog" "chases" "cat" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If the dog visits the lion then the dog chases the lion.
((("dog" "visits" "lion" "+")) -> ("dog" "chases" "lion" "+"))
The rabbit is cold.
True
1
proof
[(triple11)]
("rabbit" "is" "cold" "+")
triple11
The rabbit is not cold.
False
1
inv-proof
[(triple11)]
("rabbit" "is" "cold" "-")
triple11
The dog chases the lion.
True
2
proof
[(((triple8) -> rule1))]
("dog" "chases" "lion" "+")
((triple8) -> (rule1 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog does not chase the lion.
False
2
inv-proof
[(((triple8) -> rule1))]
("dog" "chases" "lion" "-")
((triple8) -> (rule1 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The cat chases the dog.
Unknown
random
[@0: The cat chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "dog" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The cat chases the lion.[(triple1)] The cat is nice.[(triple2)] The cat visits the lion.[(triple3)] The dog chases the cat.[(triple4)] The dog is cold.[(triple5)] The dog is nice.[(triple6)] The dog needs the cat.[(triple7)] The dog visits the lion.[(triple8)] The dog visits the rabbit.[(triple9)] The lion chases the rabbit.[(triple10)] The rabbit is cold.[(triple11)] The rabbit is red.[(triple12)] The rabbit needs the dog.[(triple13)] The rabbit visits the cat.[(triple14)] The rabbit visits the lion.[(triple15)] @1: The dog chases the lion.[(((triple8) -> rule1))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The dog chases the cat.
("dog" "chases" "cat" "+")
triple4
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is nice.
("dog" "is" "nice" "+")
triple6
The dog needs the cat.
("dog" "needs" "cat" "+")
triple7
The dog visits the lion.
("dog" "visits" "lion" "+")
triple8
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple9
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple10
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple11
The rabbit is red.
("rabbit" "is" "red" "+")
triple12
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple13
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple14
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15
The dog chases the lion.
("dog" "chases" "lion" "+")
((triple8) -> (rule1 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1