The cow chases the lion. The cow chases the tiger. The cow likes the tiger. The dog chases the cow. The dog chases the tiger. The dog is blue. The dog is rough. The dog likes the cow. The dog likes the tiger. The lion is blue. The lion likes the cow. The tiger chases the lion. The tiger eats the dog. The tiger is big. The tiger is green. The tiger likes the cow. If something likes the lion then the lion chases the cow. If something chases the dog then the dog likes the lion. If something is big and young then it likes the cow. If something chases the dog and it is green then it eats the cow. If something chases the lion then the lion chases the dog. If something is young then it chases the lion.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If something likes the lion then the lion chases the cow.
((("something" "likes" "lion" "+")) -> ("lion" "chases" "cow" "+"))
If something chases the dog then the dog likes the lion.
((("something" "chases" "dog" "+")) -> ("dog" "likes" "lion" "+"))
If something is big and young then it likes the cow.
((("something" "is" "big" "+") ("something" "is" "young" "+")) -> ("something" "likes" "cow" "+"))
If something chases the dog and it is green then it eats the cow.
((("something" "chases" "dog" "+") ("something" "is" "green" "+")) -> ("something" "eats" "cow" "+"))
If something chases the lion then the lion chases the dog.
((("something" "chases" "lion" "+")) -> ("lion" "chases" "dog" "+"))
If something is young then it chases the lion.
((("something" "is" "young" "+")) -> ("something" "chases" "lion" "+"))
The dog is rough.
True
1
proof
[(triple7)]
("dog" "is" "rough" "+")
triple7
The cow does not like the tiger.
False
1
inv-proof
[(triple3)]
("cow" "likes" "tiger" "-")
triple3
The lion chases the dog.
True
2
proof
[(((triple1) -> rule5) OR ((triple12) -> rule5))]
("lion" "chases" "dog" "+")
((triple1) -> (rule5 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
((triple12) -> (rule5 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The lion does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple12) -> rule5))]
("lion" "chases" "dog" "-")
((triple1) -> (rule5 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
((triple12) -> (rule5 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The dog likes the lion.
True
3
proof
[(((((triple1) -> rule5)) -> rule2) OR ((((triple12) -> rule5)) -> rule2))]
("dog" "likes" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The dog does not like the lion.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule2) OR ((((triple12) -> rule5)) -> rule2))]
("dog" "likes" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The lion chases the cow.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule1) OR ((((((triple12) -> rule5)) -> rule2)) -> rule1))]
("lion" "chases" "cow" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The lion does not chase the cow.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule1) OR ((((((triple12) -> rule5)) -> rule2)) -> rule1))]
("lion" "chases" "cow" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
The tiger does not eat the cow.
Unknown
inv-rconc
[@1: The tiger eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "eats" "cow" "-")
The lion eats the cow.
Unknown
rconc
[@1: The lion eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "eats" "cow" "+")
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "cow" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cow" "+")
The lion does not chase the tiger.
Unknown
inv-random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cow chases the lion.[(triple1)] The cow chases the tiger.[(triple2)] The cow likes the tiger.[(triple3)] The dog chases the cow.[(triple4)] The dog chases the tiger.[(triple5)] The dog is blue.[(triple6)] The dog is rough.[(triple7)] The dog likes the cow.[(triple8)] The dog likes the tiger.[(triple9)] The lion is blue.[(triple10)] The lion likes the cow.[(triple11)] The tiger chases the lion.[(triple12)] The tiger eats the dog.[(triple13)] The tiger is big.[(triple14)] The tiger is green.[(triple15)] The tiger likes the cow.[(triple16)] @1: The lion chases the dog.[(((triple1) -> rule5) OR ((triple12) -> rule5))] @2: The dog likes the lion.[(((((triple1) -> rule5)) -> rule2) OR ((((triple12) -> rule5)) -> rule2))] @3: The lion chases the cow.[(((((((triple1) -> rule5)) -> rule2)) -> rule1) OR ((((((triple12) -> rule5)) -> rule2)) -> rule1))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple3
The dog chases the cow.
("dog" "chases" "cow" "+")
triple4
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog is rough.
("dog" "is" "rough" "+")
triple7
The dog likes the cow.
("dog" "likes" "cow" "+")
triple8
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion likes the cow.
("lion" "likes" "cow" "+")
triple11
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple12
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple13
The tiger is big.
("tiger" "is" "big" "+")
triple14
The tiger is green.
("tiger" "is" "green" "+")
triple15
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple16
The lion chases the dog.
("lion" "chases" "dog" "+")
((triple1) -> (rule5 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
((triple12) -> (rule5 % int1))
The lion chases the dog.
("lion" "chases" "dog" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
((((triple12) -> (rule5 % int2))) -> (rule2 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion chases the dog.
("lion" "chases" "dog" "+")
int2
The lion chases the cow.
("lion" "chases" "cow" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3
((((((triple12) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The lion chases the cow.
("lion" "chases" "cow" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
The lion chases the dog.
("lion" "chases" "dog" "+")
int3