The dog chases the tiger. The dog is big. The dog is red. The dog is rough. The dog is round. The dog needs the tiger. The dog sees the tiger. The tiger chases the dog. The tiger is big. The tiger is red. The tiger is rough. The tiger is round. The tiger is young. The tiger needs the dog. The tiger sees the dog. If something is red then it chases the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is round.
("dog" "is" "round" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
If something is red then it chases the dog.
((("something" "is" "red" "+")) -> ("something" "chases" "dog" "+"))
The dog is round.
True
1
proof
[(triple5)]
("dog" "is" "round" "+")
triple5
The tiger is not round.
False
1
inv-proof
[(triple12)]
("tiger" "is" "round" "-")
triple12
The dog chases the dog.
True
2
proof
[(((triple3) -> rule1))]
("dog" "chases" "dog" "+")
((triple3) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog does not chase the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("dog" "chases" "dog" "-")
((triple3) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
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 is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The dog chases the tiger.[(triple1)] The dog is big.[(triple2)] The dog is red.[(triple3)] The dog is rough.[(triple4)] The dog is round.[(triple5)] The dog needs the tiger.[(triple6)] The dog sees the tiger.[(triple7)] The tiger chases the dog.[(triple8 OR ((triple10) -> rule1))] The tiger is big.[(triple9)] The tiger is red.[(triple10)] The tiger is rough.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger needs the dog.[(triple14)] The tiger sees the dog.[(triple15)] @1: The dog chases the dog.[(((triple3) -> rule1))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple7
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple8
((triple10) -> (rule1 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple14
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple15
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple3) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1