The cat chases the tiger. The dog chases the tiger. The dog is red. The dog is rough. The dog needs the cat. The dog sees the lion. The lion chases the cat. The lion does not chase the tiger. The lion is rough. The tiger chases the cat. The tiger needs the dog. If someone needs the cat and the cat needs the lion then the cat is kind. If someone is rough then they are red. If someone is round then they do not need the lion. If someone sees the dog and they are red then the dog sees the cat. If someone sees the tiger then the tiger chases the dog. If someone needs the lion then they need the dog. If the lion is red and the lion chases the cat then the lion sees the tiger. If someone chases the dog then they are rough. If the cat sees the tiger then the tiger sees the cat.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
The lion is rough.
("lion" "is" "rough" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If someone needs the cat and the cat needs the lion then the cat is kind.
((("someone" "needs" "cat" "+") ("cat" "needs" "lion" "+")) -> ("cat" "is" "kind" "+"))
If someone is rough then they are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is round then they do not need the lion.
((("someone" "is" "round" "+")) -> ("someone" "needs" "lion" "-"))
If someone sees the dog and they are red then the dog sees the cat.
((("someone" "sees" "dog" "+") ("someone" "is" "red" "+")) -> ("dog" "sees" "cat" "+"))
If someone sees the tiger then the tiger chases the dog.
((("someone" "sees" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
If someone needs the lion then they need the dog.
((("someone" "needs" "lion" "+")) -> ("someone" "needs" "dog" "+"))
If the lion is red and the lion chases the cat then the lion sees the tiger.
((("lion" "is" "red" "+") ("lion" "chases" "cat" "+")) -> ("lion" "sees" "tiger" "+"))
If someone chases the dog then they are rough.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "rough" "+"))
If the cat sees the tiger then the tiger sees the cat.
((("cat" "sees" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
The tiger needs the dog.
True
1
proof
[(triple11)]
("tiger" "needs" "dog" "+")
triple11
The dog is not red.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule2))]
("dog" "is" "red" "-")
triple3
((triple4) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The lion is red.
True
2
proof
[(((triple9) -> rule2))]
("lion" "is" "red" "+")
((triple9) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is not red.
False
2
inv-proof
[(((triple9) -> rule2))]
("lion" "is" "red" "-")
((triple9) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion sees the tiger.
True
4
proof
[(((((triple9) -> rule2) triple7) -> rule7))]
("lion" "sees" "tiger" "+")
((((triple9) -> (rule2 % int2)) triple7) -> (rule7 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion does not see the tiger.
False
4
inv-proof
[(((((triple9) -> rule2) triple7) -> rule7))]
("lion" "sees" "tiger" "-")
((((triple9) -> (rule2 % int2)) triple7) -> (rule7 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger chases the dog.
True
5
proof
[(((((((triple9) -> rule2) triple7) -> rule7)) -> rule5))]
("tiger" "chases" "dog" "+")
((((((triple9) -> (rule2 % int3)) triple7) -> (rule7 % int2))) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger does not chase the dog.
False
5
inv-proof
[(((((((triple9) -> rule2) triple7) -> rule7)) -> rule5))]
("tiger" "chases" "dog" "-")
((((((triple9) -> (rule2 % int3)) triple7) -> (rule7 % int2))) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger is rough.
True
6
proof
[(((((((((triple9) -> rule2) triple7) -> rule7)) -> rule5)) -> rule8))]
("tiger" "is" "rough" "+")
((((((((triple9) -> (rule2 % int4)) triple7) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger is not rough.
False
6
inv-proof
[(((((((((triple9) -> rule2) triple7) -> rule7)) -> rule5)) -> rule8))]
("tiger" "is" "rough" "-")
((((((((triple9) -> (rule2 % int4)) triple7) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger is red.
True
7
proof
[(((((((((((triple9) -> rule2) triple7) -> rule7)) -> rule5)) -> rule8)) -> rule2))]
("tiger" "is" "red" "+")
((((((((((triple9) -> (rule2 % int5)) triple7) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The tiger is not red.
False
7
inv-proof
[(((((((((((triple9) -> rule2) triple7) -> rule7)) -> rule5)) -> rule8)) -> rule2))]
("tiger" "is" "red" "-")
((((((((((triple9) -> (rule2 % int5)) triple7) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "rough" "-")
The dog sees the cat.
Unknown
rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "sees" "cat" "+")
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "dog" "-")
The lion needs the dog.
Unknown
rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "needs" "dog" "+")
The cat is not red.
Unknown
inv-rconc
[@2: The cat is red.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("cat" "is" "red" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "kind" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion sees the cat.
Unknown
random
[@0: The lion sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "cat" "+")
@0: The cat chases the tiger.[(triple1)] The dog chases the tiger.[(triple2)] The dog is red.[(triple3 OR ((triple4) -> rule2))] The dog is rough.[(triple4)] The dog needs the cat.[(triple5)] The dog sees the lion.[(triple6)] The lion chases the cat.[(triple7)] The lion does not chase the tiger.[(triple8)] The lion is rough.[(triple9)] The tiger chases the cat.[(triple10)] The tiger needs the dog.[(triple11)] @1: The lion is red.[(((triple9) -> rule2))] @2: The lion sees the tiger.[(((((triple9) -> rule2) triple7) -> rule7))] @3: The tiger chases the dog.[(((((((triple9) -> rule2) triple7) -> rule7)) -> rule5))] @4: The tiger is rough.[(((((((((triple9) -> rule2) triple7) -> rule7)) -> rule5)) -> rule8))] @5: The tiger is red.[(((((((((((triple9) -> rule2) triple7) -> rule7)) -> rule5)) -> rule8)) -> rule2))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The dog is red.
("dog" "is" "red" "+")
triple3
((triple4) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog needs the cat.
("dog" "needs" "cat" "+")
triple5
The dog sees the lion.
("dog" "sees" "lion" "+")
triple6
The lion chases the cat.
("lion" "chases" "cat" "+")
triple7
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple10
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple11
The lion is red.
("lion" "is" "red" "+")
((triple9) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((triple9) -> (rule2 % int2)) triple7) -> (rule7 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((((((triple9) -> (rule2 % int3)) triple7) -> (rule7 % int2))) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
((((((((triple9) -> (rule2 % int4)) triple7) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
((((((((((triple9) -> (rule2 % int5)) triple7) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int3
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5