The dog chases the tiger. The dog does not eat the tiger. The dog is big. The dog is rough. The dog is round. The dog does not see the tiger. The tiger chases the dog. The tiger eats the dog. The tiger is big. The tiger is nice. The tiger is rough. The tiger sees the dog. If someone eats the dog then they do not eat the tiger. If someone chases the tiger then they do not eat the tiger. If someone is rough and they see the dog then the dog is nice. If someone eats the dog and they are kind then the dog is nice. If someone chases the dog and the dog chases the tiger then the tiger sees the dog. If someone eats the dog then the dog chases the tiger.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog does not eat the tiger.
("dog" "eats" "tiger" "-")
The dog is big.
("dog" "is" "big" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If someone eats the dog then they do not eat the tiger.
((("someone" "eats" "dog" "+")) -> ("someone" "eats" "tiger" "-"))
If someone chases the tiger then they do not eat the tiger.
((("someone" "chases" "tiger" "+")) -> ("someone" "eats" "tiger" "-"))
If someone is rough and they see the dog then the dog is nice.
((("someone" "is" "rough" "+") ("someone" "sees" "dog" "+")) -> ("dog" "is" "nice" "+"))
If someone eats the dog and they are kind then the dog is nice.
((("someone" "eats" "dog" "+") ("someone" "is" "kind" "+")) -> ("dog" "is" "nice" "+"))
If someone chases the dog and the dog chases the tiger then the tiger sees the dog.
((("someone" "chases" "dog" "+") ("dog" "chases" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If someone eats the dog then the dog chases the tiger.
((("someone" "eats" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
The tiger is rough.
True
1
proof
[(triple11)]
("tiger" "is" "rough" "+")
triple11
The dog does not chase the tiger.
False
1
inv-proof
[(triple1 OR ((triple8) -> rule6))]
("dog" "chases" "tiger" "-")
triple1
((triple8) -> (rule6 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The dog chases the tiger.[(triple1 OR ((triple8) -> rule6))] The dog does not eat the tiger.[(triple2 OR ((triple1) -> rule2) OR ((((triple8) -> rule6)) -> rule2))] The dog does not see the tiger.[(triple6)] The dog is big.[(triple3)] The dog is rough.[(triple4)] The dog is round.[(triple5)] The tiger chases the dog.[(triple7)] The tiger eats the dog.[(triple8)] The tiger is big.[(triple9)] The tiger is nice.[(triple10)] The tiger is rough.[(triple11)] The tiger sees the dog.[(triple12 OR ((triple7 triple1) -> rule5) OR ((triple7 ((triple8) -> rule6)) -> rule5))] @1: The dog is nice.[(((triple11 triple12) -> rule3) OR ((triple11 ((triple7 triple1) -> rule5)) -> rule3) OR ((triple11 ((triple7 ((triple8) -> rule6)) -> rule5)) -> rule3))] The tiger does not eat the tiger.[(((triple8) -> rule1))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
((triple8) -> (rule6 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog does not eat the tiger.
("dog" "eats" "tiger" "-")
triple2
((triple1) -> (rule2 % int1))
The dog does not eat the tiger.
("dog" "eats" "tiger" "-")
int1
((((triple8) -> (rule6 % int2))) -> (rule2 % int1))
The dog does not eat the tiger.
("dog" "eats" "tiger" "-")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog does not see the tiger.
("dog" "sees" "tiger" "-")
triple6
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple7
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple12
((triple7 triple1) -> (rule5 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
((triple7 ((triple8) -> (rule6 % int2))) -> (rule5 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
((triple11 triple12) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
((triple11 ((triple7 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((triple11 ((triple7 ((triple8) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
((triple8) -> (rule1 % int1))
The tiger does not eat the tiger.
("tiger" "eats" "tiger" "-")
int1