The mouse is blue. All red things are cold. If the mouse is young and the mouse is rough then the mouse is blue. All rough things are blue. All young, blue things are cold. Red, blue things are cold. All blue things are young. Cold things are red. If something is young and red then it is rough.
The mouse is blue.
("mouse" "is" "blue" "+")
All red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If the mouse is young and the mouse is rough then the mouse is blue.
((("mouse" "is" "young" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "is" "blue" "+"))
All rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
All young, blue things are cold.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Red, blue things are cold.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is young and red then it is rough.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
The mouse is blue.
True
1
proof
[(triple1)]
("mouse" "is" "blue" "+")
triple1
The mouse is not blue.
False
1
inv-proof
[(triple1)]
("mouse" "is" "blue" "-")
triple1
The mouse is young.
True
2
proof
[(((triple1) -> rule6))]
("mouse" "is" "young" "+")
((triple1) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple1) -> rule6))]
("mouse" "is" "young" "-")
((triple1) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is cold.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule4))]
("mouse" "is" "cold" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is not cold.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule4))]
("mouse" "is" "cold" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is red.
True
5
proof
[(((((((triple1) -> rule6) triple1) -> rule4)) -> rule7))]
("mouse" "is" "red" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is not red.
False
5
inv-proof
[(((((((triple1) -> rule6) triple1) -> rule4)) -> rule7))]
("mouse" "is" "red" "-")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The mouse is blue.[(triple1)] @1: The mouse is young.[(((triple1) -> rule6))] @2: The mouse is cold.[(((((triple1) -> rule6) triple1) -> rule4))] @3: The mouse is red.[(((((((triple1) -> rule6) triple1) -> rule4)) -> rule7))] @4: The mouse is rough.[(((((triple1) -> rule6) ((((((triple1) -> rule6) triple1) -> rule4)) -> rule7)) -> rule8))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is young.
("mouse" "is" "young" "+")
((triple1) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4)) triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4