The cat is cold. The cat is nice. The cat needs the mouse. The mouse is cold. The mouse is nice. The mouse needs the tiger. The mouse sees the cat. The mouse sees the rabbit. The rabbit eats the cat. The rabbit is kind. The rabbit sees the tiger. The tiger eats the rabbit. The tiger is big. The tiger needs the mouse. The tiger sees the mouse. If something sees the tiger and the tiger is nice then the tiger needs the mouse. If something needs the cat then the cat sees the mouse. If something is kind and it sees the mouse then the mouse is nice. If something needs the rabbit then it eats the rabbit. If something eats the rabbit then the rabbit is big. If something needs the cat then the cat is cold. If something needs the tiger then it is kind. If something is kind then it needs the mouse.
The cat is cold.
("cat" "is" "cold" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something sees the tiger and the tiger is nice then the tiger needs the mouse.
((("something" "sees" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "needs" "mouse" "+"))
If something needs the cat then the cat sees the mouse.
((("something" "needs" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If something is kind and it sees the mouse then the mouse is nice.
((("something" "is" "kind" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
If something needs the rabbit then it eats the rabbit.
((("something" "needs" "rabbit" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the rabbit then the rabbit is big.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If something needs the cat then the cat is cold.
((("something" "needs" "cat" "+")) -> ("cat" "is" "cold" "+"))
If something needs the tiger then it is kind.
((("something" "needs" "tiger" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it needs the mouse.
((("something" "is" "kind" "+")) -> ("something" "needs" "mouse" "+"))
The mouse sees the cat.
True
1
proof
[(triple7)]
("mouse" "sees" "cat" "+")
triple7
The tiger is not big.
False
1
inv-proof
[(triple13)]
("tiger" "is" "big" "-")
triple13
The rabbit is big.
True
2
proof
[(((triple12) -> rule5))]
("rabbit" "is" "big" "+")
((triple12) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple6) -> rule7))]
("mouse" "is" "kind" "-")
((triple6) -> (rule7 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse needs the mouse.
True
3
proof
[(((((triple6) -> rule7)) -> rule8))]
("mouse" "needs" "mouse" "+")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule8))]
("mouse" "needs" "mouse" "-")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The cat is kind.
Unknown
rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "kind" "+")
The cat does not eat the rabbit.
Unknown
inv-rconc
[@1: The cat eats the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "rabbit" "-")
The tiger sees the rabbit.
Unknown
random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit sees the mouse.
Unknown
random
[@0: The rabbit sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "mouse" "+")
@0: The cat is cold.[(triple1)] The cat is nice.[(triple2)] The cat needs the mouse.[(triple3)] The mouse is cold.[(triple4)] The mouse is nice.[(triple5)] The mouse needs the tiger.[(triple6)] The mouse sees the cat.[(triple7)] The mouse sees the rabbit.[(triple8)] The rabbit eats the cat.[(triple9)] The rabbit is kind.[(triple10)] The rabbit sees the tiger.[(triple11)] The tiger eats the rabbit.[(triple12)] The tiger is big.[(triple13)] The tiger needs the mouse.[(triple14)] The tiger sees the mouse.[(triple15)] @1: The mouse is kind.[(((triple6) -> rule7))] The rabbit is big.[(((triple12) -> rule5))] The rabbit needs the mouse.[(((triple10) -> rule8))] @2: The mouse needs the mouse.[(((((triple6) -> rule7)) -> rule8))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The mouse is nice.
("mouse" "is" "nice" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple7
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple8
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple11
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is big.
("tiger" "is" "big" "+")
triple13
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The mouse is kind.
("mouse" "is" "kind" "+")
((triple6) -> (rule7 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple12) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
((triple10) -> (rule8 % int1))
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2