The mouse is young. If the mouse is rough then the mouse is not red. Green things are nice. If something is young then it is not red. If something is nice and green then it is not red. All nice things are green. If the mouse is young then the mouse is green. All green, nice things are not rough. If the mouse is red then the mouse is young.
The mouse is young.
("mouse" "is" "young" "+")
If the mouse is rough then the mouse is not red.
((("mouse" "is" "rough" "+")) -> ("mouse" "is" "red" "-"))
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is young then it is not red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "-"))
If something is nice and green then it is not red.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "-"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If the mouse is young then the mouse is green.
((("mouse" "is" "young" "+")) -> ("mouse" "is" "green" "+"))
All green, nice things are not rough.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "-"))
If the mouse is red then the mouse is young.
((("mouse" "is" "red" "+")) -> ("mouse" "is" "young" "+"))
The mouse is young.
True
1
proof
[(triple1)]
("mouse" "is" "young" "+")
triple1
The mouse is not young.
False
1
inv-proof
[(triple1)]
("mouse" "is" "young" "-")
triple1
The mouse is not red.
True
2
proof
[(((triple1) -> rule3) OR ((((((triple1) -> rule6)) -> rule2) ((triple1) -> rule6)) -> rule4))]
("mouse" "is" "red" "-")
((triple1) -> (rule3 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse is red.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((((triple1) -> rule6)) -> rule2) ((triple1) -> rule6)) -> rule4))]
("mouse" "is" "red" "+")
((triple1) -> (rule3 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse is nice.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("mouse" "is" "nice" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is not nice.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("mouse" "is" "nice" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is not rough.
True
6
proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule7))]
("mouse" "is" "rough" "-")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse is rough.
False
6
inv-proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule7))]
("mouse" "is" "rough" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
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 chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The mouse is young.[(triple1)] @1: The mouse is green.[(((triple1) -> rule6))] The mouse is not red.[(((triple1) -> rule3) OR ((((((triple1) -> rule6)) -> rule2) ((triple1) -> rule6)) -> rule4))] @2: The mouse is nice.[(((((triple1) -> rule6)) -> rule2))] @3: The mouse is not rough.[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule7))]
The mouse is young.
("mouse" "is" "young" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
((triple1) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not red.
("mouse" "is" "red" "-")
((triple1) -> (rule3 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
The mouse is not red.
("mouse" "is" "red" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is not rough.
("mouse" "is" "rough" "-")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The mouse is not rough.
("mouse" "is" "rough" "-")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3