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