The dog chases the tiger. The dog is nice. The dog is round. The dog likes the tiger. The dog sees the tiger. The tiger does not chase the dog. The tiger is big. The tiger is round. The tiger is young. The tiger sees the dog. If someone chases the dog and the dog sees the tiger then the dog does not like the tiger. If someone likes the dog then they are round. If someone likes the dog and the dog is big then they like the tiger. If someone is young then they chase the tiger. If someone sees the dog and they are not big then the dog does not see the tiger. If someone chases the tiger then the tiger is not kind. If the tiger does not chase the dog then the tiger likes the dog. If someone likes the dog then they see the tiger.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is round.
("dog" "is" "round" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If someone chases the dog and the dog sees the tiger then the dog does not like the tiger.
((("someone" "chases" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("dog" "likes" "tiger" "-"))
If someone likes the dog then they are round.
((("someone" "likes" "dog" "+")) -> ("someone" "is" "round" "+"))
If someone likes the dog and the dog is big then they like the tiger.
((("someone" "likes" "dog" "+") ("dog" "is" "big" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is young then they chase the tiger.
((("someone" "is" "young" "+")) -> ("someone" "chases" "tiger" "+"))
If someone sees the dog and they are not big then the dog does not see the tiger.
((("someone" "sees" "dog" "+") ("someone" "is" "big" "~")) -> ("dog" "sees" "tiger" "-"))
If someone chases the tiger then the tiger is not kind.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "kind" "-"))
If the tiger does not chase the dog then the tiger likes the dog.
((("tiger" "chases" "dog" "~")) -> ("tiger" "likes" "dog" "+"))
If someone likes the dog then they see the tiger.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "tiger" "+"))
The dog sees the tiger.
True
1
proof
[(triple5)]
("dog" "sees" "tiger" "+")
triple5
The dog does not chase the tiger.
False
1
inv-proof
[(triple1)]
("dog" "chases" "tiger" "-")
triple1
The tiger likes the dog.
True
2
proof
[(((triple6) -> rule7))]
("tiger" "likes" "dog" "+")
((triple6) -> (rule7 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger is kind.
False
2
inv-proof
[(((triple1) -> rule6) OR ((((triple9) -> rule4)) -> rule6))]
("tiger" "is" "kind" "+")
((triple1) -> (rule6 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger sees the tiger.
True
3
proof
[(((((triple6) -> rule7)) -> rule8))]
("tiger" "sees" "tiger" "+")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule8))]
("tiger" "sees" "tiger" "-")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The dog chases the tiger.[(triple1)] The dog is nice.[(triple2)] The dog is round.[(triple3)] The dog likes the tiger.[(triple4)] The dog sees the tiger.[(triple5)] The tiger does not chase the dog.[(triple6)] The tiger is big.[(triple7)] The tiger is round.[(triple8 OR ((((triple6) -> rule7)) -> rule2))] The tiger is young.[(triple9)] The tiger sees the dog.[(triple10)] @1: The tiger chases the tiger.[(((triple9) -> rule4))] The tiger is not kind.[(((triple1) -> rule6) OR ((((triple9) -> rule4)) -> rule6))] The tiger likes the dog.[(((triple6) -> rule7))] @2: The tiger sees the tiger.[(((((triple6) -> rule7)) -> rule8))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is round.
("tiger" "is" "round" "+")
triple8
((((triple6) -> (rule7 % int2))) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple9) -> (rule4 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
((triple1) -> (rule6 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple6) -> (rule7 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2