The mouse eats the rabbit. The mouse eats the tiger. The mouse is blue. The mouse is kind. The mouse sees the rabbit. The rabbit eats the tiger. The rabbit is big. The rabbit is kind. The rabbit likes the mouse. The rabbit sees the mouse. The tiger eats the mouse. The tiger eats the rabbit. The tiger is cold. The tiger likes the mouse. The tiger likes the rabbit. The tiger sees the mouse. If something likes the mouse then the mouse likes the tiger. If something likes the tiger and it eats the rabbit then it sees the tiger. If something sees the tiger then it is big. If something is blue and it likes the rabbit then the rabbit likes the mouse. If something sees the mouse then the mouse is red. If something is red then it eats the tiger.
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something likes the mouse then the mouse likes the tiger.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "tiger" "+"))
If something likes the tiger and it eats the rabbit then it sees the tiger.
((("something" "likes" "tiger" "+") ("something" "eats" "rabbit" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the tiger then it is big.
((("something" "sees" "tiger" "+")) -> ("something" "is" "big" "+"))
If something is blue and it likes the rabbit then the rabbit likes the mouse.
((("something" "is" "blue" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "mouse" "+"))
If something sees the mouse then the mouse is red.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If something is red then it eats the tiger.
((("something" "is" "red" "+")) -> ("something" "eats" "tiger" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple10)]
("rabbit" "sees" "mouse" "+")
triple10
The mouse does not eat the rabbit.
False
1
inv-proof
[(triple1)]
("mouse" "eats" "rabbit" "-")
triple1
The mouse is red.
True
2
proof
[(((triple10) -> rule5) OR ((triple16) -> rule5))]
("mouse" "is" "red" "+")
((triple10) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((triple16) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse does not like the tiger.
False
2
inv-proof
[(((triple14) -> rule1) OR ((triple9) -> rule1))]
("mouse" "likes" "tiger" "-")
((triple14) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
((triple9) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse sees the tiger.
True
4
proof
[(((((triple14) -> rule1) triple1) -> rule2) OR ((((triple9) -> rule1) triple1) -> rule2))]
("mouse" "sees" "tiger" "+")
((((triple14) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((triple9) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse does not see the tiger.
False
4
inv-proof
[(((((triple14) -> rule1) triple1) -> rule2) OR ((((triple9) -> rule1) triple1) -> rule2))]
("mouse" "sees" "tiger" "-")
((((triple14) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((triple9) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse is big.
True
5
proof
[(((((((triple14) -> rule1) triple1) -> rule2)) -> rule3) OR ((((((triple9) -> rule1) triple1) -> rule2)) -> rule3))]
("mouse" "is" "big" "+")
((((((triple14) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
((((((triple9) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The mouse is not big.
False
5
inv-proof
[(((((((triple14) -> rule1) triple1) -> rule2)) -> rule3) OR ((((((triple9) -> rule1) triple1) -> rule2)) -> rule3))]
("mouse" "is" "big" "-")
((((((triple14) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
((((((triple9) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The rabbit sees the tiger.
Unknown
rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "tiger" "+")
The tiger is not big.
Unknown
inv-rconc
[@2: The tiger is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("tiger" "is" "big" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The mouse eats the rabbit.[(triple1)] The mouse eats the tiger.[(triple2 OR ((((triple10) -> rule5)) -> rule6) OR ((((triple16) -> rule5)) -> rule6))] The mouse is blue.[(triple3)] The mouse is kind.[(triple4)] The mouse sees the rabbit.[(triple5)] The rabbit eats the tiger.[(triple6)] The rabbit is big.[(triple7)] The rabbit is kind.[(triple8)] The rabbit likes the mouse.[(triple9)] The rabbit sees the mouse.[(triple10)] The tiger eats the mouse.[(triple11)] The tiger eats the rabbit.[(triple12)] The tiger is cold.[(triple13)] The tiger likes the mouse.[(triple14)] The tiger likes the rabbit.[(triple15)] The tiger sees the mouse.[(triple16)] @1: The mouse is red.[(((triple10) -> rule5) OR ((triple16) -> rule5))] The mouse likes the tiger.[(((triple14) -> rule1) OR ((triple9) -> rule1))] @2: The mouse sees the tiger.[(((((triple14) -> rule1) triple1) -> rule2) OR ((((triple9) -> rule1) triple1) -> rule2))] @3: The mouse is big.[(((((((triple14) -> rule1) triple1) -> rule2)) -> rule3) OR ((((((triple9) -> rule1) triple1) -> rule2)) -> rule3))]
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
((((triple10) -> (rule5 % int2))) -> (rule6 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
((((triple16) -> (rule5 % int2))) -> (rule6 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple5
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple6
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple9
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple10
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple11
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is cold.
("tiger" "is" "cold" "+")
triple13
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple14
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple15
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple16
The mouse is red.
("mouse" "is" "red" "+")
((triple10) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((triple16) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
((triple14) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
((triple9) -> (rule1 % int1))
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((triple14) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
((((triple9) -> (rule1 % int2)) triple1) -> (rule2 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((((((triple14) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3
((((((triple9) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
int3