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