Erin is green. Erin is quiet. Erin is rough. All smart things are rough. If something is green then it is nice. Nice, quiet things are smart.
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Nice, quiet things are smart.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Erin is quiet.
True
1
proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Erin is not rough.
False
1
inv-proof
[(triple3 OR ((((((triple1) -> rule2) triple2) -> rule3)) -> rule1))]
("Erin" "is" "rough" "-")
triple3
((((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is nice.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
True
4
proof
[(((((triple1) -> rule2) triple2) -> rule3))]
("Erin" "is" "smart" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not smart.
False
4
inv-proof
[(((((triple1) -> rule2) triple2) -> rule3))]
("Erin" "is" "smart" "-")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Erin is green.[(triple1)] Erin is quiet.[(triple2)] Erin is rough.[(triple3 OR ((((((triple1) -> rule2) triple2) -> rule3)) -> rule1))] @1: Erin is nice.[(((triple1) -> rule2))] @2: Erin is smart.[(((((triple1) -> rule2) triple2) -> rule3))]
Erin is green.
("Erin" "is" "green" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
((((((triple1) -> (rule2 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple1) -> (rule2 % int2)) triple2) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2