The dog chases the tiger. The dog is red. The dog likes the tiger. The dog needs the tiger. The tiger is red. The tiger likes the dog. The tiger needs the dog. Red people are blue. If the tiger is blue and the tiger likes the dog then the dog is young. If the dog is young then the dog is rough. If someone chases the tiger and the tiger chases the dog then the dog needs the tiger. If someone needs the dog then the dog needs the tiger. If the tiger is red then the tiger chases the dog.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If the tiger is blue and the tiger likes the dog then the dog is young.
((("tiger" "is" "blue" "+") ("tiger" "likes" "dog" "+")) -> ("dog" "is" "young" "+"))
If the dog is young then the dog is rough.
((("dog" "is" "young" "+")) -> ("dog" "is" "rough" "+"))
If someone chases the tiger and the tiger chases the dog then the dog needs the tiger.
((("someone" "chases" "tiger" "+") ("tiger" "chases" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If someone needs the dog then the dog needs the tiger.
((("someone" "needs" "dog" "+")) -> ("dog" "needs" "tiger" "+"))
If the tiger is red then the tiger chases the dog.
((("tiger" "is" "red" "+")) -> ("tiger" "chases" "dog" "+"))
The tiger likes the dog.
True
1
proof
[(triple6)]
("tiger" "likes" "dog" "+")
triple6
The tiger is not red.
False
1
inv-proof
[(triple5)]
("tiger" "is" "red" "-")
triple5
The tiger chases the dog.
True
2
proof
[(((triple5) -> rule6))]
("tiger" "chases" "dog" "+")
((triple5) -> (rule6 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple5) -> rule1))]
("tiger" "is" "blue" "-")
((triple5) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The dog is young.
True
4
proof
[(((((triple5) -> rule1) triple6) -> rule2))]
("dog" "is" "young" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog is not young.
False
4
inv-proof
[(((((triple5) -> rule1) triple6) -> rule2))]
("dog" "is" "young" "-")
((((triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog is rough.
True
5
proof
[(((((((triple5) -> rule1) triple6) -> rule2)) -> rule3))]
("dog" "is" "rough" "+")
((((((triple5) -> (rule1 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The dog is not rough.
False
5
inv-proof
[(((((((triple5) -> rule1) triple6) -> rule2)) -> rule3))]
("dog" "is" "rough" "-")
((((((triple5) -> (rule1 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
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 is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The dog chases the tiger.[(triple1)] The dog is red.[(triple2)] The dog likes the tiger.[(triple3)] The dog needs the tiger.[(triple4 OR ((triple7) -> rule5) OR ((triple1 ((triple5) -> rule6)) -> rule4))] The tiger is red.[(triple5)] The tiger likes the dog.[(triple6)] The tiger needs the dog.[(triple7)] @1: The dog is blue.[(((triple2) -> rule1))] The tiger chases the dog.[(((triple5) -> rule6))] The tiger is blue.[(((triple5) -> rule1))] @2: The dog is young.[(((((triple5) -> rule1) triple6) -> rule2))] @3: The dog is rough.[(((((((triple5) -> rule1) triple6) -> rule2)) -> rule3))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple3
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple4
((triple7) -> (rule5 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
((triple1 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The dog needs the tiger.
("dog" "needs" "tiger" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
triple5
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple6
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple7
The dog is blue.
("dog" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((triple5) -> (rule6 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple5) -> (rule1 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((((triple5) -> (rule1 % int3)) triple6) -> (rule2 % int2))) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3