The dog sees the rabbit. The rabbit is round. If someone is rough and not red then they do not eat the rabbit. If someone eats the dog then they eat the rabbit. If someone visits the rabbit then the rabbit does not eat the dog. If someone sees the rabbit then the rabbit eats the dog. If someone eats the dog and they eat the rabbit then they are rough. If someone sees the rabbit and the rabbit is rough then they see the dog.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If someone is rough and not red then they do not eat the rabbit.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "eats" "rabbit" "-"))
If someone eats the dog then they eat the rabbit.
((("someone" "eats" "dog" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone visits the rabbit then the rabbit does not eat the dog.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "eats" "dog" "-"))
If someone sees the rabbit then the rabbit eats the dog.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "eats" "dog" "+"))
If someone eats the dog and they eat the rabbit then they are rough.
((("someone" "eats" "dog" "+") ("someone" "eats" "rabbit" "+")) -> ("someone" "is" "rough" "+"))
If someone sees the rabbit and the rabbit is rough then they see the dog.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("someone" "sees" "dog" "+"))
The rabbit is round.
True
1
proof
[(triple2)]
("rabbit" "is" "round" "+")
triple2
The rabbit is not round.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "round" "-")
triple2
The rabbit eats the dog.
True
2
proof
[(((triple1) -> rule4))]
("rabbit" "eats" "dog" "+")
((triple1) -> (rule4 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit does not eat the dog.
False
2
inv-proof
[(((triple1) -> rule4))]
("rabbit" "eats" "dog" "-")
((triple1) -> (rule4 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit eats the rabbit.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("rabbit" "eats" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("rabbit" "eats" "rabbit" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The rabbit is rough.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "is" "rough" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int3
The rabbit is not rough.
False
6
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "is" "rough" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int3
The rabbit does not see the dog.
Unknown
inv-rconc
[@1: The rabbit sees the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "dog" "-")
The dog is rough.
Unknown
rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "rough" "+")
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The rabbit does not visit the dog.
Unknown
inv-random
[@0: The rabbit visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The dog sees the rabbit.[(triple1)] The rabbit is round.[(triple2)] @1: The rabbit eats the dog.[(((triple1) -> rule4))] @2: The rabbit eats the rabbit.[(((((triple1) -> rule4)) -> rule2))] @3: The rabbit is rough.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule2)) -> rule5))] @4: The dog sees the dog.[(((triple1 ((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule2)) -> rule5)) -> rule6))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
triple2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
((triple1) -> (rule4 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int3
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple1 ((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int4