The dog likes the tiger. The tiger eats the dog. If the dog likes the tiger then the tiger eats the dog. If someone likes the tiger and the tiger eats the dog then the tiger is red.
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
If the dog likes the tiger then the tiger eats the dog.
((("dog" "likes" "tiger" "+")) -> ("tiger" "eats" "dog" "+"))
If someone likes the tiger and the tiger eats the dog then the tiger is red.
((("someone" "likes" "tiger" "+") ("tiger" "eats" "dog" "+")) -> ("tiger" "is" "red" "+"))
The dog likes the tiger.
True
1
proof
[(triple1)]
("dog" "likes" "tiger" "+")
triple1
The dog does not like the tiger.
False
1
inv-proof
[(triple1)]
("dog" "likes" "tiger" "-")
triple1
The tiger is red.
True
3
proof
[(((triple1 triple2) -> rule2) OR ((triple1 ((triple1) -> rule1)) -> rule2))]
("tiger" "is" "red" "+")
((triple1 triple2) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The tiger is not red.
False
3
inv-proof
[(((triple1 triple2) -> rule2) OR ((triple1 ((triple1) -> rule1)) -> rule2))]
("tiger" "is" "red" "-")
((triple1 triple2) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The dog likes the tiger.[(triple1)] The tiger eats the dog.[(triple2 OR ((triple1) -> rule1))] @1: The tiger is red.[(((triple1 triple2) -> rule2) OR ((triple1 ((triple1) -> rule1)) -> rule2))]
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple2
((triple1) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple1 triple2) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2