The dog eats the tiger. The dog is rough. The dog sees the lion. The dog sees the mouse. The dog sees the tiger. The lion is rough. The lion sees the dog. The lion sees the mouse. The mouse eats the dog. The mouse eats the lion. The mouse is kind. The mouse needs the dog. The mouse needs the tiger. The mouse sees the dog. The mouse sees the tiger. The tiger needs the dog. If the lion is young then the lion eats the dog. If something needs the mouse then it needs the lion. If something sees the tiger then it is young. If the lion sees the dog then the dog eats the mouse. If something is blue and big then it needs the tiger. If the lion is young then the lion is big.
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If the lion is young then the lion eats the dog.
((("lion" "is" "young" "+")) -> ("lion" "eats" "dog" "+"))
If something needs the mouse then it needs the lion.
((("something" "needs" "mouse" "+")) -> ("something" "needs" "lion" "+"))
If something sees the tiger then it is young.
((("something" "sees" "tiger" "+")) -> ("something" "is" "young" "+"))
If the lion sees the dog then the dog eats the mouse.
((("lion" "sees" "dog" "+")) -> ("dog" "eats" "mouse" "+"))
If something is blue and big then it needs the tiger.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "needs" "tiger" "+"))
If the lion is young then the lion is big.
((("lion" "is" "young" "+")) -> ("lion" "is" "big" "+"))
The lion is rough.
True
1
proof
[(triple6)]
("lion" "is" "rough" "+")
triple6
The dog does not see the lion.
False
1
inv-proof
[(triple3)]
("dog" "sees" "lion" "-")
triple3
The mouse is young.
True
2
proof
[(((triple15) -> rule3))]
("mouse" "is" "young" "+")
((triple15) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The dog does not eat the mouse.
False
2
inv-proof
[(((triple7) -> rule4))]
("dog" "eats" "mouse" "-")
((triple7) -> (rule4 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "lion" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger does not see the lion.
Unknown
inv-random
[@0: The tiger sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "lion" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The dog eats the tiger.[(triple1)] The dog is rough.[(triple2)] The dog sees the lion.[(triple3)] The dog sees the mouse.[(triple4)] The dog sees the tiger.[(triple5)] The lion is rough.[(triple6)] The lion sees the dog.[(triple7)] The lion sees the mouse.[(triple8)] The mouse eats the dog.[(triple9)] The mouse eats the lion.[(triple10)] The mouse is kind.[(triple11)] The mouse needs the dog.[(triple12)] The mouse needs the tiger.[(triple13)] The mouse sees the dog.[(triple14)] The mouse sees the tiger.[(triple15)] The tiger needs the dog.[(triple16)] @1: The dog eats the mouse.[(((triple7) -> rule4))] The dog is young.[(((triple5) -> rule3))] The mouse is young.[(((triple15) -> rule3))]
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog sees the lion.
("dog" "sees" "lion" "+")
triple3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple4
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple5
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion sees the dog.
("lion" "sees" "dog" "+")
triple7
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple8
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple9
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple11
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple12
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple13
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple14
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple15
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple16
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((triple7) -> (rule4 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((triple5) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple15) -> (rule3 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1