The dog is red. The tiger is green. The tiger visits the dog. If someone visits the dog and they are red then the dog chases the tiger. If the tiger is red and the tiger does not visit the dog then the dog chases the tiger. If someone visits the tiger then the tiger does not like the dog. If someone visits the dog then the dog does not visit the tiger. If someone visits the dog and they do not chase the tiger then the tiger does not chase the dog. If someone chases the dog and they visit the tiger then they like the dog.
The dog is red.
("dog" "is" "red" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone visits the dog and they are red then the dog chases the tiger.
((("someone" "visits" "dog" "+") ("someone" "is" "red" "+")) -> ("dog" "chases" "tiger" "+"))
If the tiger is red and the tiger does not visit the dog then the dog chases the tiger.
((("tiger" "is" "red" "+") ("tiger" "visits" "dog" "~")) -> ("dog" "chases" "tiger" "+"))
If someone visits the tiger then the tiger does not like the dog.
((("someone" "visits" "tiger" "+")) -> ("tiger" "likes" "dog" "-"))
If someone visits the dog then the dog does not visit the tiger.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "tiger" "-"))
If someone visits the dog and they do not chase the tiger then the tiger does not chase the dog.
((("someone" "visits" "dog" "+") ("someone" "chases" "tiger" "~")) -> ("tiger" "chases" "dog" "-"))
If someone chases the dog and they visit the tiger then they like the dog.
((("someone" "chases" "dog" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "likes" "dog" "+"))
The dog is red.
True
1
proof
[(triple1)]
("dog" "is" "red" "+")
triple1
The tiger is not green.
False
1
inv-proof
[(triple2)]
("tiger" "is" "green" "-")
triple2
The dog does not visit the tiger.
True
2
proof
[(((triple3) -> rule4))]
("dog" "visits" "tiger" "-")
((triple3) -> (rule4 % int1))
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
int1
The dog visits the tiger.
False
2
inv-proof
[(((triple3) -> rule4))]
("dog" "visits" "tiger" "+")
((triple3) -> (rule4 % int1))
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
int1
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "dog" "-")
The dog chases the tiger.
Unknown
rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "tiger" "+")
The tiger is not red.
Unknown
inv-random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "-")
The tiger chases the dog.
Unknown
random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "+")
@0: The dog is red.[(triple1)] The tiger is green.[(triple2)] The tiger visits the dog.[(triple3)] @1: The dog does not visit the tiger.[(((triple3) -> rule4))]
The dog is red.
("dog" "is" "red" "+")
triple1
The tiger is green.
("tiger" "is" "green" "+")
triple2
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple3
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
((triple3) -> (rule4 % int1))
The dog does not visit the tiger.
("dog" "visits" "tiger" "-")
int1