The cat chases the dog. The cat eats the rabbit. The cow eats the dog. The dog does not chase the cat. The dog eats the rabbit. The rabbit is nice. The rabbit sees the dog. If something is young then it chases the cow. If the rabbit does not chase the dog and the rabbit is not young then the rabbit does not eat the dog. If something is round then it eats the rabbit. If something eats the dog then it is not blue. If something sees the dog then it is round. If something is blue and it chases the cow then it eats the cat. If something sees the cow and it sees the rabbit then it is not green. If something chases the cow and it eats the dog then the dog sees the rabbit.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cow eats the dog.
("cow" "eats" "dog" "+")
The dog does not chase the cat.
("dog" "chases" "cat" "-")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something is young then it chases the cow.
((("something" "is" "young" "+")) -> ("something" "chases" "cow" "+"))
If the rabbit does not chase the dog and the rabbit is not young then the rabbit does not eat the dog.
((("rabbit" "chases" "dog" "~") ("rabbit" "is" "young" "~")) -> ("rabbit" "eats" "dog" "-"))
If something is round then it eats the rabbit.
((("something" "is" "round" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the dog then it is not blue.
((("something" "eats" "dog" "+")) -> ("something" "is" "blue" "-"))
If something sees the dog then it is round.
((("something" "sees" "dog" "+")) -> ("something" "is" "round" "+"))
If something is blue and it chases the cow then it eats the cat.
((("something" "is" "blue" "+") ("something" "chases" "cow" "+")) -> ("something" "eats" "cat" "+"))
If something sees the cow and it sees the rabbit then it is not green.
((("something" "sees" "cow" "+") ("something" "sees" "rabbit" "+")) -> ("something" "is" "green" "-"))
If something chases the cow and it eats the dog then the dog sees the rabbit.
((("something" "chases" "cow" "+") ("something" "eats" "dog" "+")) -> ("dog" "sees" "rabbit" "+"))
The cat chases the dog.
True
1
proof
[(triple1)]
("cat" "chases" "dog" "+")
triple1
The cat does not chase the dog.
False
1
inv-proof
[(triple1)]
("cat" "chases" "dog" "-")
triple1
The cow is not blue.
True
2
proof
[(((triple3) -> rule4))]
("cow" "is" "blue" "-")
((triple3) -> (rule4 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple7) -> rule5))]
("rabbit" "is" "round" "-")
((triple7) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit eats the rabbit.
True
3
proof
[(((((triple7) -> rule5)) -> rule3))]
("rabbit" "eats" "rabbit" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit does not eat the rabbit.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit does not chase the cow.
Unknown
inv-rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "cow" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "cow" "+")
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "round" "-")
The rabbit sees the cat.
Unknown
random
[@0: The rabbit sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cat" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cat chases the dog.[(triple1)] The cat eats the rabbit.[(triple2)] The cow eats the dog.[(triple3)] The dog does not chase the cat.[(triple4)] The dog eats the rabbit.[(triple5)] The rabbit is nice.[(triple6)] The rabbit sees the dog.[(triple7)] @1: The cow is not blue.[(((triple3) -> rule4))] The rabbit is round.[(((triple7) -> rule5))] @2: The rabbit eats the rabbit.[(((((triple7) -> rule5)) -> rule3))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The cow eats the dog.
("cow" "eats" "dog" "+")
triple3
The dog does not chase the cat.
("dog" "chases" "cat" "-")
triple4
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple5
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple6
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple7
The cow is not blue.
("cow" "is" "blue" "-")
((triple3) -> (rule4 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple7) -> (rule5 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((triple7) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2