The dog chases the tiger. The dog eats the tiger. The dog is big. The dog is blue. The dog is nice. The dog is young. The dog visits the tiger. The tiger chases the dog. The tiger is blue. The tiger visits the dog. If someone eats the dog then they are young. If someone is nice and they eat the tiger then they chase the dog. If the tiger visits the dog then the tiger eats the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If someone eats the dog then they are young.
((("someone" "eats" "dog" "+")) -> ("someone" "is" "young" "+"))
If someone is nice and they eat the tiger then they chase the dog.
((("someone" "is" "nice" "+") ("someone" "eats" "tiger" "+")) -> ("someone" "chases" "dog" "+"))
If the tiger visits the dog then the tiger eats the dog.
((("tiger" "visits" "dog" "+")) -> ("tiger" "eats" "dog" "+"))
The tiger visits the dog.
True
1
proof
[(triple10)]
("tiger" "visits" "dog" "+")
triple10
The dog does not chase the tiger.
False
1
inv-proof
[(triple1)]
("dog" "chases" "tiger" "-")
triple1
The tiger eats the dog.
True
2
proof
[(((triple10) -> rule3))]
("tiger" "eats" "dog" "+")
((triple10) -> (rule3 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The dog does not chase the dog.
False
3
inv-proof
[(((triple5 triple2) -> rule2))]
("dog" "chases" "dog" "-")
((triple5 triple2) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The tiger is young.
True
3
proof
[(((((triple10) -> rule3)) -> rule1))]
("tiger" "is" "young" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The tiger is not young.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule1))]
("tiger" "is" "young" "-")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The dog chases the tiger.[(triple1)] The dog eats the tiger.[(triple2)] The dog is big.[(triple3)] The dog is blue.[(triple4)] The dog is nice.[(triple5)] The dog is young.[(triple6)] The dog visits the tiger.[(triple7)] The tiger chases the dog.[(triple8)] The tiger is blue.[(triple9)] The tiger visits the dog.[(triple10)] @1: The dog chases the dog.[(((triple5 triple2) -> rule2))] The tiger eats the dog.[(((triple10) -> rule3))] @2: The tiger is young.[(((((triple10) -> rule3)) -> rule1))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is blue.
("dog" "is" "blue" "+")
triple4
The dog is nice.
("dog" "is" "nice" "+")
triple5
The dog is young.
("dog" "is" "young" "+")
triple6
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple5 triple2) -> (rule2 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((triple10) -> (rule3 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2