The mouse is cold. The mouse is green. The mouse is nice. All nice people are blue. Cold, green people are nice. If the mouse is blue then the mouse is not round.
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Cold, green people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If the mouse is blue then the mouse is not round.
((("mouse" "is" "blue" "+")) -> ("mouse" "is" "round" "-"))
The mouse is green.
True
1
proof
[(triple2)]
("mouse" "is" "green" "+")
triple2
The mouse is not nice.
False
1
inv-proof
[(triple3 OR ((triple1 triple2) -> rule2))]
("mouse" "is" "nice" "-")
triple3
((triple1 triple2) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is blue.
True
2
proof
[(((triple3) -> rule1) OR ((((triple1 triple2) -> rule2)) -> rule1))]
("mouse" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is not blue.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple1 triple2) -> rule2)) -> rule1))]
("mouse" "is" "blue" "-")
((triple3) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is not round.
True
3
proof
[(((((triple3) -> rule1)) -> rule3) OR ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule3))]
("mouse" "is" "round" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse is round.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3) OR ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule3))]
("mouse" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
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 cold.[(triple1)] The mouse is green.[(triple2)] The mouse is nice.[(triple3 OR ((triple1 triple2) -> rule2))] @1: The mouse is blue.[(((triple3) -> rule1) OR ((((triple1 triple2) -> rule2)) -> rule1))] @2: The mouse is not round.[(((((triple3) -> rule1)) -> rule3) OR ((((((triple1 triple2) -> rule2)) -> rule1)) -> rule3))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple3) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is not round.
("mouse" "is" "round" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((((triple1 triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is not round.
("mouse" "is" "round" "-")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3