The bear chases the dog. The bear likes the cat. The bear likes the dog. The cat is red. The cat likes the dog. The cat sees the dog. The dog likes the bear. The dog sees the cat. The tiger is blue. The tiger is red. The tiger is young. The tiger likes the dog. If someone chases the bear then the bear likes the cat. If the bear chases the dog then the bear chases the tiger. If someone is red then they see the dog. If someone likes the dog and the dog is young then the dog is red. If someone chases the cat and the cat likes the dog then the dog is young. If the tiger chases the bear then the tiger likes the dog. If the bear chases the tiger then the tiger chases the cat. If the cat chases the tiger then the tiger sees the dog.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If someone chases the bear then the bear likes the cat.
((("someone" "chases" "bear" "+")) -> ("bear" "likes" "cat" "+"))
If the bear chases the dog then the bear chases the tiger.
((("bear" "chases" "dog" "+")) -> ("bear" "chases" "tiger" "+"))
If someone is red then they see the dog.
((("someone" "is" "red" "+")) -> ("someone" "sees" "dog" "+"))
If someone likes the dog and the dog is young then the dog is red.
((("someone" "likes" "dog" "+") ("dog" "is" "young" "+")) -> ("dog" "is" "red" "+"))
If someone chases the cat and the cat likes the dog then the dog is young.
((("someone" "chases" "cat" "+") ("cat" "likes" "dog" "+")) -> ("dog" "is" "young" "+"))
If the tiger chases the bear then the tiger likes the dog.
((("tiger" "chases" "bear" "+")) -> ("tiger" "likes" "dog" "+"))
If the bear chases the tiger then the tiger chases the cat.
((("bear" "chases" "tiger" "+")) -> ("tiger" "chases" "cat" "+"))
If the cat chases the tiger then the tiger sees the dog.
((("cat" "chases" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
The tiger is blue.
True
1
proof
[(triple9)]
("tiger" "is" "blue" "+")
triple9
The tiger is not blue.
False
1
inv-proof
[(triple9)]
("tiger" "is" "blue" "-")
triple9
The bear chases the tiger.
True
2
proof
[(((triple1) -> rule2))]
("bear" "chases" "tiger" "+")
((triple1) -> (rule2 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The tiger does not see the dog.
False
2
inv-proof
[(((triple10) -> rule3))]
("tiger" "sees" "dog" "-")
((triple10) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger chases the cat.
True
3
proof
[(((((triple1) -> rule2)) -> rule7))]
("tiger" "chases" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger does not chase the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule7))]
("tiger" "chases" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The dog is young.
True
5
proof
[(((((((triple1) -> rule2)) -> rule7) triple5) -> rule5))]
("dog" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple5) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The dog is not young.
False
5
inv-proof
[(((((((triple1) -> rule2)) -> rule7) triple5) -> rule5))]
("dog" "is" "young" "-")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple5) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The dog is red.
True
7
proof
[(((triple12 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4) OR ((triple3 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4) OR ((triple5 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4))]
("dog" "is" "red" "+")
((triple12 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
((triple3 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
((triple5 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
The dog is not red.
False
7
inv-proof
[(((triple12 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4) OR ((triple3 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4) OR ((triple5 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4))]
("dog" "is" "red" "-")
((triple12 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
((triple3 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
((triple5 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
The dog sees the dog.
True
8
proof
[(((((triple12 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3) OR ((((triple3 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3) OR ((((triple5 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3))]
("dog" "sees" "dog" "+")
((((triple12 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
((((triple3 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
((((triple5 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
The dog does not see the dog.
False
8
inv-proof
[(((((triple12 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3) OR ((((triple3 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3) OR ((((triple5 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3))]
("dog" "sees" "dog" "-")
((((triple12 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
((((triple3 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
((((triple5 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
The bear does not see the dog.
Unknown
inv-rconc
[@1: The bear sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "sees" "dog" "-")
The cat chases the bear.
Unknown
random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The tiger chases the dog.
Unknown
random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The cat chases the tiger.
Unknown
random
[@0: The cat chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "tiger" "+")
The dog does not see the tiger.
Unknown
inv-random
[@0: The dog sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "tiger" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The tiger does not see the cat.
Unknown
inv-random
[@0: The tiger sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
The dog does not like the cat.
Unknown
inv-random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "-")
The dog chases the cat.
Unknown
random
[@0: The dog chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cat" "+")
@0: The bear chases the dog.[(triple1)] The bear likes the cat.[(triple2)] The bear likes the dog.[(triple3)] The cat is red.[(triple4)] The cat likes the dog.[(triple5)] The cat sees the dog.[(triple6 OR ((triple4) -> rule3))] The dog likes the bear.[(triple7)] The dog sees the cat.[(triple8)] The tiger is blue.[(triple9)] The tiger is red.[(triple10)] The tiger is young.[(triple11)] The tiger likes the dog.[(triple12)] @1: The bear chases the tiger.[(((triple1) -> rule2))] The tiger sees the dog.[(((triple10) -> rule3))] @2: The tiger chases the cat.[(((((triple1) -> rule2)) -> rule7))] @3: The dog is young.[(((((((triple1) -> rule2)) -> rule7) triple5) -> rule5))] @4: The dog is red.[(((triple12 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4) OR ((triple3 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4) OR ((triple5 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4))] @5: The dog sees the dog.[(((((triple12 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3) OR ((((triple3 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3) OR ((((triple5 ((((((triple1) -> rule2)) -> rule7) triple5) -> rule5)) -> rule4)) -> rule3))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear likes the cat.
("bear" "likes" "cat" "+")
triple2
The bear likes the dog.
("bear" "likes" "dog" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat likes the dog.
("cat" "likes" "dog" "+")
triple5
The cat sees the dog.
("cat" "sees" "dog" "+")
triple6
((triple4) -> (rule3 % int1))
The cat sees the dog.
("cat" "sees" "dog" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
triple7
The dog sees the cat.
("dog" "sees" "cat" "+")
triple8
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
triple11
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple12
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple1) -> (rule2 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple10) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule7 % int2)) triple5) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int2
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int3
The dog is red.
("dog" "is" "red" "+")
((triple12 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
((triple3 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
((triple5 ((((((triple1) -> (rule2 % int4))) -> (rule7 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int4
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple12 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
((((triple3 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5
((((triple5 ((((((triple1) -> (rule2 % int5))) -> (rule7 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int4
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int5