The bear does not eat the cat. The cat does not eat the mouse. The mouse chases the cat. The rabbit eats the cat. If something needs the mouse then the mouse needs the rabbit. If the rabbit is round and the mouse does not chase the rabbit then the rabbit eats the cat. If something eats the mouse and it is cold then the mouse does not eat the cat. If something chases the cat then it needs the mouse. If something needs the cat and the cat needs the bear then it needs the bear. If something eats the mouse then the mouse is kind. If the mouse is kind and the mouse chases the rabbit then the mouse is cold. If the bear chases the mouse and the bear needs the mouse then the bear chases the rabbit.
The bear does not eat the cat.
("bear" "eats" "cat" "-")
The cat does not eat the mouse.
("cat" "eats" "mouse" "-")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
If something needs the mouse then the mouse needs the rabbit.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If the rabbit is round and the mouse does not chase the rabbit then the rabbit eats the cat.
((("rabbit" "is" "round" "+") ("mouse" "chases" "rabbit" "~")) -> ("rabbit" "eats" "cat" "+"))
If something eats the mouse and it is cold then the mouse does not eat the cat.
((("something" "eats" "mouse" "+") ("something" "is" "cold" "+")) -> ("mouse" "eats" "cat" "-"))
If something chases the cat then it needs the mouse.
((("something" "chases" "cat" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the cat and the cat needs the bear then it needs the bear.
((("something" "needs" "cat" "+") ("cat" "needs" "bear" "+")) -> ("something" "needs" "bear" "+"))
If something eats the mouse then the mouse is kind.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If the mouse is kind and the mouse chases the rabbit then the mouse is cold.
((("mouse" "is" "kind" "+") ("mouse" "chases" "rabbit" "+")) -> ("mouse" "is" "cold" "+"))
If the bear chases the mouse and the bear needs the mouse then the bear chases the rabbit.
((("bear" "chases" "mouse" "+") ("bear" "needs" "mouse" "+")) -> ("bear" "chases" "rabbit" "+"))
The cat does not eat the mouse.
True
1
proof
[(triple2)]
("cat" "eats" "mouse" "-")
triple2
The rabbit does not eat the cat.
False
1
inv-proof
[(triple4)]
("rabbit" "eats" "cat" "-")
triple4
The mouse needs the mouse.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "needs" "mouse" "+")
((triple3) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse does not need the mouse.
False
2
inv-proof
[(((triple3) -> rule4))]
("mouse" "needs" "mouse" "-")
((triple3) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the rabbit.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("mouse" "needs" "rabbit" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse does not need the rabbit.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("mouse" "needs" "rabbit" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The cat does not need the bear.
Unknown
inv-rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "needs" "bear" "-")
The rabbit needs the bear.
Unknown
rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "needs" "bear" "+")
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "kind" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The bear does not eat the mouse.
Unknown
inv-random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The bear does not eat the cat.[(triple1)] The cat does not eat the mouse.[(triple2)] The mouse chases the cat.[(triple3)] The rabbit eats the cat.[(triple4)] @1: The mouse needs the mouse.[(((triple3) -> rule4))] @2: The mouse needs the rabbit.[(((((triple3) -> rule4)) -> rule1))]
The bear does not eat the cat.
("bear" "eats" "cat" "-")
triple1
The cat does not eat the mouse.
("cat" "eats" "mouse" "-")
triple2
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple3
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple4
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple3) -> (rule4 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2