The cow is nice. The dog eats the cow. The tiger is young. If the tiger is young then the tiger needs the dog. If someone needs the dog then the dog is nice. If someone chases the cow then the cow is blue. If someone needs the tiger then the tiger chases the cow. If someone eats the dog then the dog chases the tiger. If someone needs the tiger then the tiger chases the dog.
The cow is nice.
("cow" "is" "nice" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The tiger is young.
("tiger" "is" "young" "+")
If the tiger is young then the tiger needs the dog.
((("tiger" "is" "young" "+")) -> ("tiger" "needs" "dog" "+"))
If someone needs the dog then the dog is nice.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "nice" "+"))
If someone chases the cow then the cow is blue.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "blue" "+"))
If someone needs the tiger then the tiger chases the cow.
((("someone" "needs" "tiger" "+")) -> ("tiger" "chases" "cow" "+"))
If someone eats the dog then the dog chases the tiger.
((("someone" "eats" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If someone needs the tiger then the tiger chases the dog.
((("someone" "needs" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
The dog eats the cow.
True
1
proof
[(triple2)]
("dog" "eats" "cow" "+")
triple2
The tiger is not young.
False
1
inv-proof
[(triple3)]
("tiger" "is" "young" "-")
triple3
The tiger needs the dog.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger does not need the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("tiger" "needs" "dog" "-")
((triple3) -> (rule1 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The dog is nice.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("dog" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The dog is not nice.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("dog" "is" "nice" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger does not chase the dog.
Unknown
inv-rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "dog" "-")
The cow is blue.
Unknown
rconc
[@2: The cow is blue.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("cow" "is" "blue" "+")
The tiger does not chase the cow.
Unknown
inv-rconc
[@1: The tiger chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "chases" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The dog does not chase the cow.
Unknown
inv-random
[@0: The dog chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cow" "-")
The dog eats the tiger.
Unknown
random
[@0: The dog eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "tiger" "+")
@0: The cow is nice.[(triple1)] The dog eats the cow.[(triple2)] The tiger is young.[(triple3)] @1: The tiger needs the dog.[(((triple3) -> rule1))] @2: The dog is nice.[(((((triple3) -> rule1)) -> rule2))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The dog eats the cow.
("dog" "eats" "cow" "+")
triple2
The tiger is young.
("tiger" "is" "young" "+")
triple3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((triple3) -> (rule1 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2