The dog likes the mouse. The dog needs the mouse. The dog needs the rabbit. The lion is cold. The lion needs the mouse. The lion needs the rabbit. The mouse eats the dog. The mouse eats the lion. The mouse is big. The mouse needs the rabbit. The rabbit is big. The rabbit likes the lion. If something likes the lion then the lion is young. If something is young then it likes the mouse. If the dog eats the rabbit then the dog likes the rabbit. All blue, young things are cold. If something needs the mouse then it eats the mouse. If the dog needs the mouse and the dog likes the lion then the mouse likes the lion. If something needs the rabbit and it likes the mouse then it likes the dog. If something likes the rabbit then the rabbit eats the mouse.
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If something likes the lion then the lion is young.
((("something" "likes" "lion" "+")) -> ("lion" "is" "young" "+"))
If something is young then it likes the mouse.
((("something" "is" "young" "+")) -> ("something" "likes" "mouse" "+"))
If the dog eats the rabbit then the dog likes the rabbit.
((("dog" "eats" "rabbit" "+")) -> ("dog" "likes" "rabbit" "+"))
All blue, young things are cold.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something needs the mouse then it eats the mouse.
((("something" "needs" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If the dog needs the mouse and the dog likes the lion then the mouse likes the lion.
((("dog" "needs" "mouse" "+") ("dog" "likes" "lion" "+")) -> ("mouse" "likes" "lion" "+"))
If something needs the rabbit and it likes the mouse then it likes the dog.
((("something" "needs" "rabbit" "+") ("something" "likes" "mouse" "+")) -> ("something" "likes" "dog" "+"))
If something likes the rabbit then the rabbit eats the mouse.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
The dog needs the rabbit.
True
1
proof
[(triple3)]
("dog" "needs" "rabbit" "+")
triple3
The dog does not like the mouse.
False
1
inv-proof
[(triple1)]
("dog" "likes" "mouse" "-")
triple1
The lion eats the mouse.
True
2
proof
[(((triple5) -> rule5))]
("lion" "eats" "mouse" "+")
((triple5) -> (rule5 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The dog does not eat the mouse.
False
2
inv-proof
[(((triple2) -> rule5))]
("dog" "eats" "mouse" "-")
((triple2) -> (rule5 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The lion likes the mouse.
True
3
proof
[(((((triple12) -> rule1)) -> rule2))]
("lion" "likes" "mouse" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not like the mouse.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule2))]
("lion" "likes" "mouse" "-")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "cold" "+")
The mouse does not like the lion.
Unknown
inv-rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "lion" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The dog likes the mouse.[(triple1)] The dog needs the mouse.[(triple2)] The dog needs the rabbit.[(triple3)] The lion is cold.[(triple4)] The lion needs the mouse.[(triple5)] The lion needs the rabbit.[(triple6)] The mouse eats the dog.[(triple7)] The mouse eats the lion.[(triple8)] The mouse is big.[(triple9)] The mouse needs the rabbit.[(triple10)] The rabbit is big.[(triple11)] The rabbit likes the lion.[(triple12)] @1: The dog eats the mouse.[(((triple2) -> rule5))] The dog likes the dog.[(((triple3 triple1) -> rule7))] The lion eats the mouse.[(((triple5) -> rule5))] The lion is young.[(((triple12) -> rule1))] @2: The lion likes the mouse.[(((((triple12) -> rule1)) -> rule2))] @3: The lion likes the dog.[(((triple6 ((((triple12) -> rule1)) -> rule2)) -> rule7))]
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple5
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple6
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple7
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple8
The mouse is big.
("mouse" "is" "big" "+")
triple9
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple10
The rabbit is big.
("rabbit" "is" "big" "+")
triple11
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple12
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((triple2) -> (rule5 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple3 triple1) -> (rule7 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((triple5) -> (rule5 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple12) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion likes the dog.
("lion" "likes" "dog" "+")
((triple6 ((((triple12) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3