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