The dog sees the rabbit. The rabbit chases the dog. The tiger is round. If the tiger likes the rabbit then the tiger chases the dog. If something is round then it sees the rabbit.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The tiger is round.
("tiger" "is" "round" "+")
If the tiger likes the rabbit then the tiger chases the dog.
((("tiger" "likes" "rabbit" "+")) -> ("tiger" "chases" "dog" "+"))
If something is round then it sees the rabbit.
((("something" "is" "round" "+")) -> ("something" "sees" "rabbit" "+"))
The rabbit chases the dog.
True
1
proof
[(triple2)]
("rabbit" "chases" "dog" "+")
triple2
The dog does not see the rabbit.
False
1
inv-proof
[(triple1)]
("dog" "sees" "rabbit" "-")
triple1
The tiger sees the rabbit.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "sees" "rabbit" "+")
((triple3) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The tiger does not see the rabbit.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "sees" "rabbit" "-")
((triple3) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The tiger chases the dog.
Unknown
rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "dog" "+")
The tiger does not like the dog.
Unknown
inv-random
[@0: The tiger likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "dog" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The dog sees the rabbit.[(triple1)] The rabbit chases the dog.[(triple2)] The tiger is round.[(triple3)] @1: The tiger sees the rabbit.[(((triple3) -> rule2))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
((triple3) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1