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