The mouse is big. The mouse is blue. The mouse is kind. The mouse is red. The mouse is rough. If the mouse is kind and the mouse is not big then the mouse is not red. If the mouse is blue and the mouse is not big then the mouse is not rough. If the mouse is red then the mouse is rough. If the mouse is kind then the mouse is blue. All kind, big things are blue. If something is blue and not big then it is rough. All kind, big things are red. If the mouse is rough then the mouse is kind.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If the mouse is kind and the mouse is not big then the mouse is not red.
((("mouse" "is" "kind" "+") ("mouse" "is" "big" "~")) -> ("mouse" "is" "red" "-"))
If the mouse is blue and the mouse is not big then the mouse is not rough.
((("mouse" "is" "blue" "+") ("mouse" "is" "big" "~")) -> ("mouse" "is" "rough" "-"))
If the mouse is red then the mouse is rough.
((("mouse" "is" "red" "+")) -> ("mouse" "is" "rough" "+"))
If the mouse is kind then the mouse is blue.
((("mouse" "is" "kind" "+")) -> ("mouse" "is" "blue" "+"))
All kind, big things are blue.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is blue and not big then it is rough.
((("something" "is" "blue" "+") ("something" "is" "big" "~")) -> ("something" "is" "rough" "+"))
All kind, big things are red.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If the mouse is rough then the mouse is kind.
((("mouse" "is" "rough" "+")) -> ("mouse" "is" "kind" "+"))
The mouse is kind.
True
1
proof
[(triple3 OR ((triple5) -> rule8) OR ((((triple4) -> rule3)) -> rule8))]
("mouse" "is" "kind" "+")
triple3
((triple5) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is not blue.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule4) OR ((triple3 triple1) -> rule5) OR ((((triple5) -> rule8)) -> rule4) OR ((((triple5) -> rule8) triple1) -> rule5) OR ((((((triple4) -> rule3)) -> rule8)) -> rule4) OR ((((((triple4) -> rule3)) -> rule8) triple1) -> rule5))]
("mouse" "is" "blue" "-")
triple2
((triple3) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple3 triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((triple5) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The mouse is big.[(triple1)] The mouse is blue.[(triple2 OR ((triple3) -> rule4) OR ((triple3 triple1) -> rule5) OR ((((triple5) -> rule8)) -> rule4) OR ((((triple5) -> rule8) triple1) -> rule5) OR ((((((triple4) -> rule3)) -> rule8)) -> rule4) OR ((((((triple4) -> rule3)) -> rule8) triple1) -> rule5))] The mouse is kind.[(triple3 OR ((triple5) -> rule8) OR ((((triple4) -> rule3)) -> rule8))] The mouse is red.[(triple4 OR ((triple3 triple1) -> rule7) OR ((((triple5) -> rule8) triple1) -> rule7))] The mouse is rough.[(triple5 OR ((triple4) -> rule3) OR ((((triple3 triple1) -> rule7)) -> rule3))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
((triple3) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple3 triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((triple5) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
((((((triple4) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
((triple5) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
triple4
((triple3 triple1) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
((((triple5) -> (rule8 % int2)) triple1) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
((triple4) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((((triple3 triple1) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2