The mouse eats the tiger. The mouse is blue. The mouse is round. The mouse sees the tiger. The mouse visits the tiger. The tiger eats the mouse. The tiger is blue. The tiger is kind. The tiger sees the mouse. The tiger visits the mouse. If something visits the mouse and it eats the mouse then the mouse eats the tiger. If something is blue and green then it visits the mouse. If something sees the mouse and the mouse sees the tiger then it is blue. If something visits the mouse and it is blue then it is red. If something eats the mouse and the mouse sees the tiger then the tiger sees the mouse. If something is kind and it sees the tiger then it sees the mouse.
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something visits the mouse and it eats the mouse then the mouse eats the tiger.
((("something" "visits" "mouse" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If something is blue and green then it visits the mouse.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the mouse and the mouse sees the tiger then it is blue.
((("something" "sees" "mouse" "+") ("mouse" "sees" "tiger" "+")) -> ("something" "is" "blue" "+"))
If something visits the mouse and it is blue then it is red.
((("something" "visits" "mouse" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something eats the mouse and the mouse sees the tiger then the tiger sees the mouse.
((("something" "eats" "mouse" "+") ("mouse" "sees" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If something is kind and it sees the tiger then it sees the mouse.
((("something" "is" "kind" "+") ("something" "sees" "tiger" "+")) -> ("something" "sees" "mouse" "+"))
The mouse sees the tiger.
True
1
proof
[(triple4)]
("mouse" "sees" "tiger" "+")
triple4
The mouse does not see the tiger.
False
1
inv-proof
[(triple4)]
("mouse" "sees" "tiger" "-")
triple4
The tiger is red.
True
3
proof
[(((triple10 triple7) -> rule4) OR ((triple10 ((triple9 triple4) -> rule3)) -> rule4) OR ((triple10 ((((triple6 triple4) -> rule5) triple4) -> rule3)) -> rule4))]
("tiger" "is" "red" "+")
((triple10 triple7) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple10 ((triple9 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((triple10 ((((triple6 triple4) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The tiger is not red.
False
3
inv-proof
[(((triple10 triple7) -> rule4) OR ((triple10 ((triple9 triple4) -> rule3)) -> rule4) OR ((triple10 ((((triple6 triple4) -> rule5) triple4) -> rule3)) -> rule4))]
("tiger" "is" "red" "-")
((triple10 triple7) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple10 ((triple9 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((triple10 ((((triple6 triple4) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The mouse eats the tiger.[(triple1 OR ((triple10 triple6) -> rule1))] The mouse is blue.[(triple2)] The mouse is round.[(triple3)] The mouse sees the tiger.[(triple4)] The mouse visits the tiger.[(triple5)] The tiger eats the mouse.[(triple6)] The tiger is blue.[(triple7 OR ((triple9 triple4) -> rule3) OR ((((triple6 triple4) -> rule5) triple4) -> rule3))] The tiger is kind.[(triple8)] The tiger sees the mouse.[(triple9 OR ((triple6 triple4) -> rule5))] The tiger visits the mouse.[(triple10)] @1: The tiger is red.[(((triple10 triple7) -> rule4) OR ((triple10 ((triple9 triple4) -> rule3)) -> rule4) OR ((triple10 ((((triple6 triple4) -> rule5) triple4) -> rule3)) -> rule4))]
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple1
((triple10 triple6) -> (rule1 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple4
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple5
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
((triple9 triple4) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple6 triple4) -> (rule5 % int2)) triple4) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple9
((triple6 triple4) -> (rule5 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
((triple10 triple7) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple10 ((triple9 triple4) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((triple10 ((((triple6 triple4) -> (rule5 % int3)) triple4) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3