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