The dog eats the rabbit. The dog is kind. The dog is red. The dog is not young. The dog does not visit the rabbit. The rabbit eats the dog. The rabbit is kind. The rabbit is rough. The rabbit does not need the dog. The rabbit visits the dog. If something is kind then it does not visit the rabbit. If something visits the rabbit and the rabbit needs the dog then it is not rough. If something eats the dog and it does not need the rabbit then it does not need the dog. If the rabbit eats the dog and the rabbit does not need the dog then the rabbit visits the dog. If something needs the rabbit then the rabbit is young. If something visits the rabbit and it eats the rabbit then the rabbit is young. If the rabbit visits the dog then the dog eats the rabbit. If something visits the dog and it needs the rabbit then it is big.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is not young.
("dog" "is" "young" "-")
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something is kind then it does not visit the rabbit.
((("something" "is" "kind" "+")) -> ("something" "visits" "rabbit" "-"))
If something visits the rabbit and the rabbit needs the dog then it is not rough.
((("something" "visits" "rabbit" "+") ("rabbit" "needs" "dog" "+")) -> ("something" "is" "rough" "-"))
If something eats the dog and it does not need the rabbit then it does not need the dog.
((("something" "eats" "dog" "+") ("something" "needs" "rabbit" "~")) -> ("something" "needs" "dog" "-"))
If the rabbit eats the dog and the rabbit does not need the dog then the rabbit visits the dog.
((("rabbit" "eats" "dog" "+") ("rabbit" "needs" "dog" "~")) -> ("rabbit" "visits" "dog" "+"))
If something needs the rabbit then the rabbit is young.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If something visits the rabbit and it eats the rabbit then the rabbit is young.
((("something" "visits" "rabbit" "+") ("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If the rabbit visits the dog then the dog eats the rabbit.
((("rabbit" "visits" "dog" "+")) -> ("dog" "eats" "rabbit" "+"))
If something visits the dog and it needs the rabbit then it is big.
((("something" "visits" "dog" "+") ("something" "needs" "rabbit" "+")) -> ("something" "is" "big" "+"))
The rabbit does not need the dog.
True
1
proof
[(triple9)]
("rabbit" "needs" "dog" "-")
triple9
The dog does not eat the rabbit.
False
1
inv-proof
[(triple1 OR ((triple10) -> rule7) OR ((((triple6 triple9) -> rule4)) -> rule7))]
("dog" "eats" "rabbit" "-")
triple1
((triple10) -> (rule7 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
((((triple6 triple9) -> (rule4 % int2))) -> (rule7 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The rabbit does not visit the rabbit.
True
2
proof
[(((triple7) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((triple7) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The rabbit visits the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((triple7) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "big" "-")
The rabbit is young.
Unknown
rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "young" "+")
The dog does not need the rabbit.
Unknown
inv-random
[@0: The dog needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "rabbit" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog does not visit the rabbit.[(triple5 OR ((triple2) -> rule1))] The dog eats the rabbit.[(triple1 OR ((triple10) -> rule7) OR ((((triple6 triple9) -> rule4)) -> rule7))] The dog is kind.[(triple2)] The dog is not young.[(triple4)] The dog is red.[(triple3)] The rabbit does not need the dog.[(triple9)] The rabbit eats the dog.[(triple6)] The rabbit is kind.[(triple7)] The rabbit is rough.[(triple8)] The rabbit visits the dog.[(triple10 OR ((triple6 triple9) -> rule4))] @1: The rabbit does not visit the rabbit.[(((triple7) -> rule1))]
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
triple5
((triple2) -> (rule1 % int1))
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
((triple10) -> (rule7 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
((((triple6 triple9) -> (rule4 % int2))) -> (rule7 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is not young.
("dog" "is" "young" "-")
triple4
The dog is red.
("dog" "is" "red" "+")
triple3
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
triple9
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple10
((triple6 triple9) -> (rule4 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
((triple7) -> (rule1 % int1))
The rabbit does not visit the rabbit.
("rabbit" "visits" "rabbit" "-")
int1