The dog likes the rabbit. The lion visits the dog. The rabbit is green. If something sees the dog then it sees the lion. If the lion visits the rabbit then the lion visits the dog. If something is nice then it sees the dog. If the rabbit is nice then the rabbit sees the dog. If something visits the rabbit then the rabbit is nice. If something visits the dog then the dog is green. If something sees the lion then the lion is green. If something sees the rabbit and it is red then it sees the lion.
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
If something sees the dog then it sees the lion.
((("something" "sees" "dog" "+")) -> ("something" "sees" "lion" "+"))
If the lion visits the rabbit then the lion visits the dog.
((("lion" "visits" "rabbit" "+")) -> ("lion" "visits" "dog" "+"))
If something is nice then it sees the dog.
((("something" "is" "nice" "+")) -> ("something" "sees" "dog" "+"))
If the rabbit is nice then the rabbit sees the dog.
((("rabbit" "is" "nice" "+")) -> ("rabbit" "sees" "dog" "+"))
If something visits the rabbit then the rabbit is nice.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If something visits the dog then the dog is green.
((("something" "visits" "dog" "+")) -> ("dog" "is" "green" "+"))
If something sees the lion then the lion is green.
((("something" "sees" "lion" "+")) -> ("lion" "is" "green" "+"))
If something sees the rabbit and it is red then it sees the lion.
((("something" "sees" "rabbit" "+") ("something" "is" "red" "+")) -> ("something" "sees" "lion" "+"))
The lion visits the dog.
True
1
proof
[(triple2)]
("lion" "visits" "dog" "+")
triple2
The lion does not visit the dog.
False
1
inv-proof
[(triple2)]
("lion" "visits" "dog" "-")
triple2
The dog is green.
True
2
proof
[(((triple2) -> rule6))]
("dog" "is" "green" "+")
((triple2) -> (rule6 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog is not green.
False
2
inv-proof
[(((triple2) -> rule6))]
("dog" "is" "green" "-")
((triple2) -> (rule6 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The lion is not green.
Unknown
inv-rconc
[@4: The lion is green.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule3 <- rule5 <- FAIL)]]
("lion" "is" "green" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "dog" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The dog likes the rabbit.[(triple1)] The lion visits the dog.[(triple2)] The rabbit is green.[(triple3)] @1: The dog is green.[(((triple2) -> rule6))]
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple1
The lion visits the dog.
("lion" "visits" "dog" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The dog is green.
("dog" "is" "green" "+")
((triple2) -> (rule6 % int1))
The dog is green.
("dog" "is" "green" "+")
int1