The mouse is blue. The mouse likes the rabbit. The rabbit eats the mouse. The rabbit likes the mouse. The tiger likes the mouse. The tiger sees the mouse. The tiger does not see the rabbit. If something likes the tiger then it eats the rabbit. If something eats the tiger and the tiger sees the mouse then the mouse is blue. If something sees the tiger and it is not round then it sees the mouse. If something likes the mouse then the mouse likes the tiger. If something is rough then it does not like the mouse. If the mouse eats the rabbit then the rabbit does not see the tiger.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
If something likes the tiger then it eats the rabbit.
((("something" "likes" "tiger" "+")) -> ("something" "eats" "rabbit" "+"))
If something eats the tiger and the tiger sees the mouse then the mouse is blue.
((("something" "eats" "tiger" "+") ("tiger" "sees" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If something sees the tiger and it is not round then it sees the mouse.
((("something" "sees" "tiger" "+") ("something" "is" "round" "~")) -> ("something" "sees" "mouse" "+"))
If something likes the mouse then the mouse likes the tiger.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If something is rough then it does not like the mouse.
((("something" "is" "rough" "+")) -> ("something" "likes" "mouse" "-"))
If the mouse eats the rabbit then the rabbit does not see the tiger.
((("mouse" "eats" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "-"))
The tiger sees the mouse.
True
1
proof
[(triple6)]
("tiger" "sees" "mouse" "+")
triple6
The rabbit does not eat the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "mouse" "-")
triple3
The mouse likes the tiger.
True
2
proof
[(((triple4) -> rule4) OR ((triple5) -> rule4))]
("mouse" "likes" "tiger" "+")
((triple4) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
((triple5) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse does not like the tiger.
False
2
inv-proof
[(((triple4) -> rule4) OR ((triple5) -> rule4))]
("mouse" "likes" "tiger" "-")
((triple4) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
((triple5) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse eats the rabbit.
True
3
proof
[(((((triple4) -> rule4)) -> rule1) OR ((((triple5) -> rule4)) -> rule1))]
("mouse" "eats" "rabbit" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse does not eat the rabbit.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule1) OR ((((triple5) -> rule4)) -> rule1))]
("mouse" "eats" "rabbit" "-")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The rabbit does not see the tiger.
True
4
proof
[(((((((triple4) -> rule4)) -> rule1)) -> rule6) OR ((((((triple5) -> rule4)) -> rule1)) -> rule6))]
("rabbit" "sees" "tiger" "-")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The rabbit sees the tiger.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule1)) -> rule6) OR ((((((triple5) -> rule4)) -> rule1)) -> rule6))]
("rabbit" "sees" "tiger" "+")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The rabbit does not see the mouse.
Unknown
inv-rconc
[@1: The rabbit sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The tiger eats the rabbit.
Unknown
rconc
[@1: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "eats" "rabbit" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The mouse is blue.[(triple1)] The mouse likes the rabbit.[(triple2)] The rabbit eats the mouse.[(triple3)] The rabbit likes the mouse.[(triple4)] The tiger does not see the rabbit.[(triple7)] The tiger likes the mouse.[(triple5)] The tiger sees the mouse.[(triple6)] @1: The mouse likes the tiger.[(((triple4) -> rule4) OR ((triple5) -> rule4))] @2: The mouse eats the rabbit.[(((((triple4) -> rule4)) -> rule1) OR ((((triple5) -> rule4)) -> rule1))] @3: The rabbit does not see the tiger.[(((((((triple4) -> rule4)) -> rule1)) -> rule6) OR ((((((triple5) -> rule4)) -> rule1)) -> rule6))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple3
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple4
The tiger does not see the rabbit.
("tiger" "sees" "rabbit" "-")
triple7
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple5
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple6
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple4) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
((triple5) -> (rule4 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
((((triple4) -> (rule4 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
((((((triple4) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
((((((triple5) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3