The dog likes the tiger. The tiger is kind. The tiger visits the dog. If someone needs the tiger then they visit the tiger. If someone likes the tiger then they do not visit the dog. If someone likes the tiger and they do not visit the dog then the dog is round.
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone needs the tiger then they visit the tiger.
((("someone" "needs" "tiger" "+")) -> ("someone" "visits" "tiger" "+"))
If someone likes the tiger then they do not visit the dog.
((("someone" "likes" "tiger" "+")) -> ("someone" "visits" "dog" "-"))
If someone likes the tiger and they do not visit the dog then the dog is round.
((("someone" "likes" "tiger" "+") ("someone" "visits" "dog" "~")) -> ("dog" "is" "round" "+"))
The dog likes the tiger.
True
1
proof
[(triple1)]
("dog" "likes" "tiger" "+")
triple1
The tiger is not kind.
False
1
inv-proof
[(triple2)]
("tiger" "is" "kind" "-")
triple2
The dog does not visit the dog.
True
2
proof
[(((triple1) -> rule2))]
("dog" "visits" "dog" "-")
((triple1) -> (rule2 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The dog visits the dog.
False
2
inv-proof
[(((triple1) -> rule2))]
("dog" "visits" "dog" "+")
((triple1) -> (rule2 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The dog is round.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("dog" "is" "round" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int2
The dog is not round.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("dog" "is" "round" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int2
The dog does not visit the tiger.
Unknown
inv-rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "tiger" "-")
The tiger visits the tiger.
Unknown
rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "tiger" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The tiger likes the dog.
Unknown
random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The tiger needs the dog.
Unknown
random
[@0: The tiger needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "dog" "+")
@0: The dog likes the tiger.[(triple1)] The tiger is kind.[(triple2)] The tiger visits the dog.[(triple3)] @1: The dog does not visit the dog.[(((triple1) -> rule2))] @2: The dog is round.[(((triple1 ((triple1) -> rule2)) -> rule3))]
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple1
The tiger is kind.
("tiger" "is" "kind" "+")
triple2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple3
The dog does not visit the dog.
("dog" "visits" "dog" "-")
((triple1) -> (rule2 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The dog is round.
("dog" "is" "round" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int2