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