The cat is round. The cat likes the dog. The cat sees the dog. The cat visits the dog. The dog is big. The dog is round. The dog is young. The dog likes the cat. The dog sees the cat. The dog visits the cat. If something visits the cat then it visits the dog. If something visits the dog then the dog sees the cat.
The cat is round.
("cat" "is" "round" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If something visits the cat then it visits the dog.
((("something" "visits" "cat" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then the dog sees the cat.
((("something" "visits" "dog" "+")) -> ("dog" "sees" "cat" "+"))
The cat visits the dog.
True
1
proof
[(triple4)]
("cat" "visits" "dog" "+")
triple4
The dog does not see the cat.
False
1
inv-proof
[(triple9 OR ((triple4) -> rule2) OR ((((triple10) -> rule1)) -> rule2))]
("dog" "sees" "cat" "-")
triple9
((triple4) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the dog.
True
2
proof
[(((triple10) -> rule1))]
("dog" "visits" "dog" "+")
((triple10) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple10) -> rule1))]
("dog" "visits" "dog" "-")
((triple10) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The cat is round.[(triple1)] The cat likes the dog.[(triple2)] The cat sees the dog.[(triple3)] The cat visits the dog.[(triple4)] The dog is big.[(triple5)] The dog is round.[(triple6)] The dog is young.[(triple7)] The dog likes the cat.[(triple8)] The dog sees the cat.[(triple9 OR ((triple4) -> rule2) OR ((((triple10) -> rule1)) -> rule2))] The dog visits the cat.[(triple10)] @1: The dog visits the dog.[(((triple10) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat likes the dog.
("cat" "likes" "dog" "+")
triple2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The dog is big.
("dog" "is" "big" "+")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
The dog likes the cat.
("dog" "likes" "cat" "+")
triple8
The dog sees the cat.
("dog" "sees" "cat" "+")
triple9
((triple4) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
triple10
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple10) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1