The cat is cold. The mouse is nice. The rabbit sees the mouse. The tiger is red. If something eats the cat and it is nice then it sees the rabbit. If something sees the mouse then the mouse eats the cat. If something is kind and it sees the mouse then it eats the tiger.
The cat is cold.
("cat" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The tiger is red.
("tiger" "is" "red" "+")
If something eats the cat and it is nice then it sees the rabbit.
((("something" "eats" "cat" "+") ("something" "is" "nice" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the mouse then the mouse eats the cat.
((("something" "sees" "mouse" "+")) -> ("mouse" "eats" "cat" "+"))
If something is kind and it sees the mouse then it eats the tiger.
((("something" "is" "kind" "+") ("something" "sees" "mouse" "+")) -> ("something" "eats" "tiger" "+"))
The tiger is red.
True
1
proof
[(triple4)]
("tiger" "is" "red" "+")
triple4
The mouse is not nice.
False
1
inv-proof
[(triple2)]
("mouse" "is" "nice" "-")
triple2
The mouse eats the cat.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "eats" "cat" "+")
((triple3) -> (rule2 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse does not eat the cat.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "eats" "cat" "-")
((triple3) -> (rule2 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the rabbit.
True
4
proof
[(((((triple3) -> rule2) triple2) -> rule1))]
("mouse" "sees" "rabbit" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The mouse does not see the rabbit.
False
4
inv-proof
[(((((triple3) -> rule2) triple2) -> rule1))]
("mouse" "sees" "rabbit" "-")
((((triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cat eats the tiger.
Unknown
rconc
[@1: The cat eats the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "tiger" "+")
The tiger does not see the rabbit.
Unknown
inv-rconc
[@1: The tiger sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "rabbit" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat is not nice.
Unknown
inv-random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cat is cold.[(triple1)] The mouse is nice.[(triple2)] The rabbit sees the mouse.[(triple3)] The tiger is red.[(triple4)] @1: The mouse eats the cat.[(((triple3) -> rule2))] @2: The mouse sees the rabbit.[(((((triple3) -> rule2) triple2) -> rule1))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
The mouse eats the cat.
("mouse" "eats" "cat" "+")
((triple3) -> (rule2 % int1))
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((((triple3) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
int2