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