The dog eats the tiger. The dog is blue. The tiger is big. The tiger is cold. The tiger is kind. The tiger likes the dog. The tiger needs the dog. If the dog eats the tiger and the tiger likes the dog then the tiger eats the dog. If someone likes the tiger then the tiger needs the dog. If the tiger is kind then the tiger likes the dog.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If the dog eats the tiger and the tiger likes the dog then the tiger eats the dog.
((("dog" "eats" "tiger" "+") ("tiger" "likes" "dog" "+")) -> ("tiger" "eats" "dog" "+"))
If someone likes the tiger then the tiger needs the dog.
((("someone" "likes" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
If the tiger is kind then the tiger likes the dog.
((("tiger" "is" "kind" "+")) -> ("tiger" "likes" "dog" "+"))
The dog eats the tiger.
True
1
proof
[(triple1)]
("dog" "eats" "tiger" "+")
triple1
The dog is not blue.
False
1
inv-proof
[(triple2)]
("dog" "is" "blue" "-")
triple2
The tiger eats the dog.
True
3
proof
[(((triple1 triple6) -> rule1) OR ((triple1 ((triple5) -> rule3)) -> rule1))]
("tiger" "eats" "dog" "+")
((triple1 triple6) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
((triple1 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger does not eat the dog.
False
3
inv-proof
[(((triple1 triple6) -> rule1) OR ((triple1 ((triple5) -> rule3)) -> rule1))]
("tiger" "eats" "dog" "-")
((triple1 triple6) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
((triple1 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
@0: The dog eats the tiger.[(triple1)] The dog is blue.[(triple2)] The tiger is big.[(triple3)] The tiger is cold.[(triple4)] The tiger is kind.[(triple5)] The tiger likes the dog.[(triple6 OR ((triple5) -> rule3))] The tiger needs the dog.[(triple7)] @1: The tiger eats the dog.[(((triple1 triple6) -> rule1) OR ((triple1 ((triple5) -> rule3)) -> rule1))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The tiger is big.
("tiger" "is" "big" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple4
The tiger is kind.
("tiger" "is" "kind" "+")
triple5
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple6
((triple5) -> (rule3 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((triple1 triple6) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
((triple1 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2