Erin is red. If someone is furry then they are nice. Red, big people are furry. If Erin is red then Erin is big. If someone is big then they are red. If someone is furry and not red then they are not green. If Erin is green and Erin is red then Erin is not kind.
Erin is red.
("Erin" "is" "red" "+")
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Red, big people are furry.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Erin is red then Erin is big.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "big" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is furry and not red then they are not green.
((("someone" "is" "furry" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "green" "-"))
If Erin is green and Erin is red then Erin is not kind.
((("Erin" "is" "green" "+") ("Erin" "is" "red" "+")) -> ("Erin" "is" "kind" "-"))
Erin is red.
True
1
proof
[(triple1)]
("Erin" "is" "red" "+")
triple1
Erin is not red.
False
1
inv-proof
[(triple1)]
("Erin" "is" "red" "-")
triple1
Erin is big.
True
2
proof
[(((triple1) -> rule3))]
("Erin" "is" "big" "+")
((triple1) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Erin" "is" "big" "-")
((triple1) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Erin" "is" "furry" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("Erin" "is" "furry" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
True
5
proof
[(((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "nice" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not nice.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "nice" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Erin is red.[(triple1)] @1: Erin is big.[(((triple1) -> rule3))] @2: Erin is furry.[(((triple1 ((triple1) -> rule3)) -> rule2))] @3: Erin is nice.[(((((triple1 ((triple1) -> rule3)) -> rule2)) -> rule1))]
Erin is red.
("Erin" "is" "red" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
((triple1) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3