The cat chases the dog. The cat is nice. The cat needs the tiger. The dog chases the lion. The dog is young. The dog needs the tiger. The lion chases the cat. The lion chases the dog. The lion is blue. The lion is green. The lion is round. The lion needs the cat. The lion needs the tiger. The lion sees the tiger. The tiger is young. The tiger sees the lion. If something needs the dog then it is green. If something sees the lion then it needs the cat. If something sees the dog and it needs the cat then it sees the lion. If the cat chases the lion and the lion is nice then the lion needs the dog. If something needs the lion and the lion is blue then it needs the dog. If something needs the tiger and the tiger sees the lion then it needs the lion. If something sees the tiger then the tiger needs the lion. If something sees the lion then the lion chases the tiger.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something needs the dog then it is green.
((("something" "needs" "dog" "+")) -> ("something" "is" "green" "+"))
If something sees the lion then it needs the cat.
((("something" "sees" "lion" "+")) -> ("something" "needs" "cat" "+"))
If something sees the dog and it needs the cat then it sees the lion.
((("something" "sees" "dog" "+") ("something" "needs" "cat" "+")) -> ("something" "sees" "lion" "+"))
If the cat chases the lion and the lion is nice then the lion needs the dog.
((("cat" "chases" "lion" "+") ("lion" "is" "nice" "+")) -> ("lion" "needs" "dog" "+"))
If something needs the lion and the lion is blue then it needs the dog.
((("something" "needs" "lion" "+") ("lion" "is" "blue" "+")) -> ("something" "needs" "dog" "+"))
If something needs the tiger and the tiger sees the lion then it needs the lion.
((("something" "needs" "tiger" "+") ("tiger" "sees" "lion" "+")) -> ("something" "needs" "lion" "+"))
If something sees the tiger then the tiger needs the lion.
((("something" "sees" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If something sees the lion then the lion chases the tiger.
((("something" "sees" "lion" "+")) -> ("lion" "chases" "tiger" "+"))
The cat chases the dog.
True
1
proof
[(triple1)]
("cat" "chases" "dog" "+")
triple1
The lion does not need the tiger.
False
1
inv-proof
[(triple13)]
("lion" "needs" "tiger" "-")
triple13
The tiger needs the cat.
True
2
proof
[(((triple16) -> rule2))]
("tiger" "needs" "cat" "+")
((triple16) -> (rule2 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The dog does not need the lion.
False
3
inv-proof
[(((triple6 triple16) -> rule6))]
("dog" "needs" "lion" "-")
((triple6 triple16) -> (rule6 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion needs the dog.
True
5
proof
[(((((triple13 triple16) -> rule6) triple9) -> rule5))]
("lion" "needs" "dog" "+")
((((triple13 triple16) -> (rule6 % int2)) triple9) -> (rule5 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The dog does not need the dog.
False
5
inv-proof
[(((((triple6 triple16) -> rule6) triple9) -> rule5))]
("dog" "needs" "dog" "-")
((((triple6 triple16) -> (rule6 % int2)) triple9) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The cat is green.
True
6
proof
[(((((((triple3 triple16) -> rule6) triple9) -> rule5)) -> rule1))]
("cat" "is" "green" "+")
((((((triple3 triple16) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The cat is not green.
False
6
inv-proof
[(((((((triple3 triple16) -> rule6) triple9) -> rule5)) -> rule1))]
("cat" "is" "green" "-")
((((((triple3 triple16) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The dog does not need the cat.
Unknown
inv-rconc
[@2: The dog needs the cat.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("dog" "needs" "cat" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "lion" "+")
The cat does not see the lion.
Unknown
inv-rconc
[@1: The cat sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "lion" "-")
The dog sees the lion.
Unknown
rconc
[@1: The dog sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "lion" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger chases the dog.
Unknown
random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "+")
The cat does not see the dog.
Unknown
inv-random
[@0: The cat sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "dog" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The cat chases the dog.[(triple1)] The cat is nice.[(triple2)] The cat needs the tiger.[(triple3)] The dog chases the lion.[(triple4)] The dog is young.[(triple5)] The dog needs the tiger.[(triple6)] The lion chases the cat.[(triple7)] The lion chases the dog.[(triple8)] The lion is blue.[(triple9)] The lion is green.[(triple10 OR ((((((triple13 triple16) -> rule6) triple9) -> rule5)) -> rule1))] The lion is round.[(triple11)] The lion needs the cat.[(triple12)] The lion needs the tiger.[(triple13)] The lion sees the tiger.[(triple14)] The tiger is young.[(triple15)] The tiger sees the lion.[(triple16)] @1: The cat needs the lion.[(((triple3 triple16) -> rule6))] The dog needs the lion.[(((triple6 triple16) -> rule6))] The lion chases the tiger.[(((triple16) -> rule8))] The lion needs the lion.[(((triple13 triple16) -> rule6))] The tiger needs the cat.[(((triple16) -> rule2))] The tiger needs the lion.[(((triple14) -> rule7))] @2: The cat needs the dog.[(((((triple3 triple16) -> rule6) triple9) -> rule5))] The dog needs the dog.[(((((triple6 triple16) -> rule6) triple9) -> rule5))] The lion needs the dog.[(((((triple13 triple16) -> rule6) triple9) -> rule5))] The tiger needs the dog.[(((((triple14) -> rule7) triple9) -> rule5))] @3: The cat is green.[(((((((triple3 triple16) -> rule6) triple9) -> rule5)) -> rule1))] The dog is green.[(((((((triple6 triple16) -> rule6) triple9) -> rule5)) -> rule1))] The tiger is green.[(((((((triple14) -> rule7) triple9) -> rule5)) -> rule1))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The dog chases the lion.
("dog" "chases" "lion" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple6
The lion chases the cat.
("lion" "chases" "cat" "+")
triple7
The lion chases the dog.
("lion" "chases" "dog" "+")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple9
The lion is green.
("lion" "is" "green" "+")
triple10
((((((triple13 triple16) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The lion is round.
("lion" "is" "round" "+")
triple11
The lion needs the cat.
("lion" "needs" "cat" "+")
triple12
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple13
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple14
The tiger is young.
("tiger" "is" "young" "+")
triple15
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple16
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple3 triple16) -> (rule6 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple6 triple16) -> (rule6 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple16) -> (rule8 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple13 triple16) -> (rule6 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
((triple16) -> (rule2 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((triple14) -> (rule7 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
((((triple3 triple16) -> (rule6 % int2)) triple9) -> (rule5 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple6 triple16) -> (rule6 % int2)) triple9) -> (rule5 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
((((triple13 triple16) -> (rule6 % int2)) triple9) -> (rule5 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((((triple14) -> (rule7 % int2)) triple9) -> (rule5 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((((((triple3 triple16) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule1 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The dog is green.
("dog" "is" "green" "+")
((((((triple6 triple16) -> (rule6 % int3)) triple9) -> (rule5 % int2))) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
((((((triple14) -> (rule7 % int3)) triple9) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3