The mouse is big. The mouse is green. The mouse is kind. The mouse is nice. The mouse is red. Kind, red people are big. If someone is nice and big then they are green. If the mouse is kind and the mouse is nice then the mouse is big. If someone is nice and big then they are kind. If someone is kind then they are big. If the mouse is kind then the mouse is red.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
Kind, red people are big.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and big then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If the mouse is kind and the mouse is nice then the mouse is big.
((("mouse" "is" "kind" "+") ("mouse" "is" "nice" "+")) -> ("mouse" "is" "big" "+"))
If someone is nice and big then they are kind.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If the mouse is kind then the mouse is red.
((("mouse" "is" "kind" "+")) -> ("mouse" "is" "red" "+"))
The mouse is nice.
True
1
proof
[(triple4)]
("mouse" "is" "nice" "+")
triple4
The mouse is not red.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule6) OR ((((triple4 triple1) -> rule4)) -> rule6))]
("mouse" "is" "red" "-")
triple5
((triple3) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((((triple4 triple1) -> (rule4 % int2))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is big.[(triple1 OR ((triple3) -> rule5) OR ((triple3 triple4) -> rule3) OR ((triple3 triple5) -> rule1) OR ((triple3 ((triple3) -> rule6)) -> rule1))] The mouse is green.[(triple2 OR ((triple4 triple1) -> rule2) OR ((triple4 ((triple3) -> rule5)) -> rule2) OR ((triple4 ((triple3 triple4) -> rule3)) -> rule2) OR ((triple4 ((triple3 triple5) -> rule1)) -> rule2) OR ((triple4 ((triple3 ((triple3) -> rule6)) -> rule1)) -> rule2))] The mouse is kind.[(triple3 OR ((triple4 triple1) -> rule4))] The mouse is nice.[(triple4)] The mouse is red.[(triple5 OR ((triple3) -> rule6) OR ((((triple4 triple1) -> rule4)) -> rule6))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
((triple3) -> (rule5 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple3 triple4) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple3 triple5) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple3 ((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
triple2
((triple4 triple1) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
((triple4 ((triple3) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
((triple4 ((triple3 triple4) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
((triple4 ((triple3 triple5) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
((triple4 ((triple3 ((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
((triple4 triple1) -> (rule4 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
((triple3) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((((triple4 triple1) -> (rule4 % int2))) -> (rule6 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2