The dog chases the tiger. The dog is big. The dog is young. The dog likes the tiger. The dog sees the tiger. The tiger chases the dog. The tiger is cold. The tiger is nice. The tiger likes the dog. The tiger sees the dog. If someone is big then they chase the tiger. If someone sees the dog then the dog chases the tiger. If the dog likes the tiger then the tiger likes the dog. If someone sees the tiger and they chase the tiger then they are big. If someone likes the dog then they are big. If someone sees the tiger and they chase the dog then the dog sees the tiger.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If someone is big then they chase the tiger.
((("someone" "is" "big" "+")) -> ("someone" "chases" "tiger" "+"))
If someone sees the dog then the dog chases the tiger.
((("someone" "sees" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If the dog likes the tiger then the tiger likes the dog.
((("dog" "likes" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
If someone sees the tiger and they chase the tiger then they are big.
((("someone" "sees" "tiger" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "is" "big" "+"))
If someone likes the dog then they are big.
((("someone" "likes" "dog" "+")) -> ("someone" "is" "big" "+"))
If someone sees the tiger and they chase the dog then the dog sees the tiger.
((("someone" "sees" "tiger" "+") ("someone" "chases" "dog" "+")) -> ("dog" "sees" "tiger" "+"))
The dog sees the tiger.
True
1
proof
[(triple5)]
("dog" "sees" "tiger" "+")
triple5
The tiger does not chase the dog.
False
1
inv-proof
[(triple6)]
("tiger" "chases" "dog" "-")
triple6
The tiger is big.
True
2
proof
[(((triple9) -> rule5) OR ((((triple4) -> rule3)) -> rule5))]
("tiger" "is" "big" "+")
((triple9) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger is not big.
False
2
inv-proof
[(((triple9) -> rule5) OR ((((triple4) -> rule3)) -> rule5))]
("tiger" "is" "big" "-")
((triple9) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger chases the tiger.
True
3
proof
[(((((triple9) -> rule5)) -> rule1) OR ((((((triple4) -> rule3)) -> rule5)) -> rule1))]
("tiger" "chases" "tiger" "+")
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The tiger does not chase the tiger.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule1) OR ((((((triple4) -> rule3)) -> rule5)) -> rule1))]
("tiger" "chases" "tiger" "-")
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
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 likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog chases the tiger.[(triple1 OR ((triple10) -> rule2) OR ((triple2) -> rule1))] The dog is big.[(triple2 OR ((triple5 triple1) -> rule4) OR ((triple5 ((triple10) -> rule2)) -> rule4))] The dog is young.[(triple3)] The dog likes the tiger.[(triple4)] The dog sees the tiger.[(triple5)] The tiger chases the dog.[(triple6)] The tiger is cold.[(triple7)] The tiger is nice.[(triple8)] The tiger likes the dog.[(triple9 OR ((triple4) -> rule3))] The tiger sees the dog.[(triple10)] @1: The tiger is big.[(((triple9) -> rule5) OR ((((triple4) -> rule3)) -> rule5))] @2: The tiger chases the tiger.[(((((triple9) -> rule5)) -> rule1) OR ((((((triple4) -> rule3)) -> rule5)) -> rule1))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
((triple10) -> (rule2 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
((triple2) -> (rule1 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog is big.
("dog" "is" "big" "+")
triple2
((triple5 triple1) -> (rule4 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
((triple5 ((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog is young.
("dog" "is" "young" "+")
triple3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple9
((triple4) -> (rule3 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
((triple9) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int2
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple9) -> (rule5 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int3