The mouse is big. The mouse is cold. The mouse is round. If someone is young and cold then they are rough. If the mouse is cold and the mouse is big then the mouse is young. If someone is round and young then they are big.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is round.
("mouse" "is" "round" "+")
If someone is young and cold then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If the mouse is cold and the mouse is big then the mouse is young.
((("mouse" "is" "cold" "+") ("mouse" "is" "big" "+")) -> ("mouse" "is" "young" "+"))
If someone is round and young then they are big.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
The mouse is cold.
True
1
proof
[(triple2)]
("mouse" "is" "cold" "+")
triple2
The mouse is not round.
False
1
inv-proof
[(triple3)]
("mouse" "is" "round" "-")
triple3
The mouse is young.
True
3
proof
[(((triple2 triple1) -> rule2))]
("mouse" "is" "young" "+")
((triple2 triple1) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("mouse" "is" "young" "-")
((triple2 triple1) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is rough.
True
5
proof
[(((((triple2 triple1) -> rule2) triple2) -> rule1))]
("mouse" "is" "rough" "+")
((((triple2 triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse is not rough.
False
5
inv-proof
[(((((triple2 triple1) -> rule2) triple2) -> rule1))]
("mouse" "is" "rough" "-")
((((triple2 triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
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 needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The mouse is big.[(triple1)] The mouse is cold.[(triple2)] The mouse is round.[(triple3)] @1: The mouse is young.[(((triple2 triple1) -> rule2))] @2: The mouse is rough.[(((((triple2 triple1) -> rule2) triple2) -> rule1))]
The mouse is big.
("mouse" "is" "big" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The mouse is young.
("mouse" "is" "young" "+")
((triple2 triple1) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple2 triple1) -> (rule2 % int2)) triple2) -> (rule1 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2