The mouse is nice. The mouse is red. The mouse is rough. The mouse is round. The mouse is young. If someone is red and round then they are nice. All nice people are young. If someone is round and young then they are rough.
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone is red and round then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is round and young then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
The mouse is young.
True
1
proof
[(triple5 OR ((triple1) -> rule2) OR ((((triple2 triple4) -> rule1)) -> rule2))]
("mouse" "is" "young" "+")
triple5
((triple1) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((triple2 triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is not rough.
False
1
inv-proof
[(triple3 OR ((triple4 triple5) -> rule3) OR ((triple4 ((triple1) -> rule2)) -> rule3) OR ((triple4 ((((triple2 triple4) -> rule1)) -> rule2)) -> rule3))]
("mouse" "is" "rough" "-")
triple3
((triple4 triple5) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple4 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((triple4 ((((triple2 triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "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 nice.[(triple1 OR ((triple2 triple4) -> rule1))] The mouse is red.[(triple2)] The mouse is rough.[(triple3 OR ((triple4 triple5) -> rule3) OR ((triple4 ((triple1) -> rule2)) -> rule3) OR ((triple4 ((((triple2 triple4) -> rule1)) -> rule2)) -> rule3))] The mouse is round.[(triple4)] The mouse is young.[(triple5 OR ((triple1) -> rule2) OR ((((triple2 triple4) -> rule1)) -> rule2))]
The mouse is nice.
("mouse" "is" "nice" "+")
triple1
((triple2 triple4) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
((triple4 triple5) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
((triple4 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((triple4 ((((triple2 triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
((triple1) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((((triple2 triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2