The mouse is red. Red people are nice. All big people are kind. If someone is red and green then they are big. Nice people are green. Big people are nice. If someone is kind then they are nice. Nice people are green. If the mouse is red and the mouse is kind then the mouse is nice.
The mouse is red.
("mouse" "is" "red" "+")
Red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is red and green then they are big.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If the mouse is red and the mouse is kind then the mouse is nice.
((("mouse" "is" "red" "+") ("mouse" "is" "kind" "+")) -> ("mouse" "is" "nice" "+"))
The mouse is red.
True
1
proof
[(triple1)]
("mouse" "is" "red" "+")
triple1
The mouse is not red.
False
1
inv-proof
[(triple1)]
("mouse" "is" "red" "-")
triple1
The mouse is nice.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "is" "nice" "-")
((triple1) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
True
3
proof
[(((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule7))]
("mouse" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is not green.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule7))]
("mouse" "is" "green" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is big.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule3) OR ((triple1 ((((triple1) -> rule1)) -> rule7)) -> rule3))]
("mouse" "is" "big" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse is not big.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule3) OR ((triple1 ((((triple1) -> rule1)) -> rule7)) -> rule3))]
("mouse" "is" "big" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse is red.[(triple1)] @1: The mouse is nice.[(((triple1) -> rule1))] @2: The mouse is green.[(((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule1)) -> rule7))] @3: The mouse is big.[(((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule3) OR ((triple1 ((((triple1) -> rule1)) -> rule7)) -> rule3))] @4: The mouse is kind.[(((((triple1 ((((triple1) -> rule1)) -> rule4)) -> rule3)) -> rule2) OR ((((triple1 ((((triple1) -> rule1)) -> rule7)) -> rule3)) -> rule2))]
The mouse is red.
("mouse" "is" "red" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
((triple1) -> (rule1 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is nice.
("mouse" "is" "nice" "+")
int3
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple1 ((((triple1) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
int4
((((triple1 ((((triple1) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
int3
The mouse is nice.
("mouse" "is" "nice" "+")
int4