The cat likes the dog. The cat needs the dog. The cat visits the lion. The cow likes the dog. The cow likes the lion. The cow does not need the dog. The cow does not need the lion. The dog is red. The lion is red. The lion visits the dog. If something likes the cat then it is big. If something is blue and not young then it is not big. If something is big then it likes the dog. If the lion likes the dog then the lion does not need the dog. If something is young then it does not visit the cow. If something visits the lion then the lion likes the cow. If something needs the dog and it does not visit the cow then the dog needs the cow. If the cow is not big then the cow is nice.
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow does not need the dog.
("cow" "needs" "dog" "-")
The cow does not need the lion.
("cow" "needs" "lion" "-")
The dog is red.
("dog" "is" "red" "+")
The lion is red.
("lion" "is" "red" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If something likes the cat then it is big.
((("something" "likes" "cat" "+")) -> ("something" "is" "big" "+"))
If something is blue and not young then it is not big.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "big" "-"))
If something is big then it likes the dog.
((("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
If the lion likes the dog then the lion does not need the dog.
((("lion" "likes" "dog" "+")) -> ("lion" "needs" "dog" "-"))
If something is young then it does not visit the cow.
((("something" "is" "young" "+")) -> ("something" "visits" "cow" "-"))
If something visits the lion then the lion likes the cow.
((("something" "visits" "lion" "+")) -> ("lion" "likes" "cow" "+"))
If something needs the dog and it does not visit the cow then the dog needs the cow.
((("something" "needs" "dog" "+") ("something" "visits" "cow" "~")) -> ("dog" "needs" "cow" "+"))
If the cow is not big then the cow is nice.
((("cow" "is" "big" "~")) -> ("cow" "is" "nice" "+"))
The cat likes the dog.
True
1
proof
[(triple1)]
("cat" "likes" "dog" "+")
triple1
The cat does not need the dog.
False
1
inv-proof
[(triple2)]
("cat" "needs" "dog" "-")
triple2
The lion likes the cow.
True
2
proof
[(((triple3) -> rule6))]
("lion" "likes" "cow" "+")
((triple3) -> (rule6 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The lion does not like the cow.
False
2
inv-proof
[(((triple3) -> rule6))]
("lion" "likes" "cow" "-")
((triple3) -> (rule6 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "nice" "-")
The dog likes the dog.
Unknown
rconc
[@2: The dog likes the dog.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("dog" "likes" "dog" "+")
The dog does not like the lion.
Unknown
inv-random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
@0: The cat likes the dog.[(triple1)] The cat needs the dog.[(triple2)] The cat visits the lion.[(triple3)] The cow does not need the dog.[(triple6)] The cow does not need the lion.[(triple7)] The cow likes the dog.[(triple4)] The cow likes the lion.[(triple5)] The dog is red.[(triple8)] The lion is red.[(triple9)] The lion visits the dog.[(triple10)] @1: The lion likes the cow.[(((triple3) -> rule6))]
The cat likes the dog.
("cat" "likes" "dog" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The cow does not need the dog.
("cow" "needs" "dog" "-")
triple6
The cow does not need the lion.
("cow" "needs" "lion" "-")
triple7
The cow likes the dog.
("cow" "likes" "dog" "+")
triple4
The cow likes the lion.
("cow" "likes" "lion" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple8
The lion is red.
("lion" "is" "red" "+")
triple9
The lion visits the dog.
("lion" "visits" "dog" "+")
triple10
The lion likes the cow.
("lion" "likes" "cow" "+")
((triple3) -> (rule6 % int1))
The lion likes the cow.
("lion" "likes" "cow" "+")
int1