Erin is nice. Erin is round. Erin is smart. Kind things are big. All nice things are rough. If something is smart and rough then it is big.
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is smart and rough then it is big.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Erin is round.
True
1
proof
[(triple2)]
("Erin" "is" "round" "+")
triple2
Erin is not round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "-")
triple2
Erin is rough.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
True
4
proof
[(((triple3 ((triple1) -> rule2)) -> rule3))]
("Erin" "is" "big" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not big.
False
4
inv-proof
[(((triple3 ((triple1) -> rule2)) -> rule3))]
("Erin" "is" "big" "-")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Erin is nice.[(triple1)] Erin is round.[(triple2)] Erin is smart.[(triple3)] @1: Erin is rough.[(((triple1) -> rule2))] @2: Erin is big.[(((triple3 ((triple1) -> rule2)) -> rule3))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2