The dog eats the mouse. The dog eats the tiger. The dog is big. The dog is cold. The dog needs the mouse. The dog visits the mouse. The dog visits the tiger. The mouse is big. The tiger eats the dog. The tiger is big. The tiger is young. The tiger needs the mouse. If someone is cold and they visit the dog then they are young. If someone needs the tiger and they are big then the tiger needs the mouse. If the mouse needs the tiger then the mouse eats the dog. If someone needs the dog then the dog is big. If someone is big and green then they need the tiger. If someone is green and nice then they need the mouse.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If someone is cold and they visit the dog then they are young.
((("someone" "is" "cold" "+") ("someone" "visits" "dog" "+")) -> ("someone" "is" "young" "+"))
If someone needs the tiger and they are big then the tiger needs the mouse.
((("someone" "needs" "tiger" "+") ("someone" "is" "big" "+")) -> ("tiger" "needs" "mouse" "+"))
If the mouse needs the tiger then the mouse eats the dog.
((("mouse" "needs" "tiger" "+")) -> ("mouse" "eats" "dog" "+"))
If someone needs the dog then the dog is big.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "big" "+"))
If someone is big and green then they need the tiger.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "needs" "tiger" "+"))
If someone is green and nice then they need the mouse.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "needs" "mouse" "+"))
The tiger is young.
True
1
proof
[(triple11)]
("tiger" "is" "young" "+")
triple11
The tiger does not need the mouse.
False
1
inv-proof
[(triple12)]
("tiger" "needs" "mouse" "-")
triple12
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "young" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog eats the mouse.[(triple1)] The dog eats the tiger.[(triple2)] The dog is big.[(triple3)] The dog is cold.[(triple4)] The dog needs the mouse.[(triple5)] The dog visits the mouse.[(triple6)] The dog visits the tiger.[(triple7)] The mouse is big.[(triple8)] The tiger eats the dog.[(triple9)] The tiger is big.[(triple10)] The tiger is young.[(triple11)] The tiger needs the mouse.[(triple12)]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog is big.
("dog" "is" "big" "+")
triple3
The dog is cold.
("dog" "is" "cold" "+")
triple4
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple5
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple6
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple8
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is young.
("tiger" "is" "young" "+")
triple11
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple12