Erin is young. Quiet people are blue. Rough people are cold. If someone is young and quiet then they are rough. Young people are rough. All cold, young people are kind. If someone is blue then they are rough.
Erin is young.
("Erin" "is" "young" "+")
Quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is young and quiet then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All cold, young people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
Erin is young.
True
1
proof
[(triple1)]
("Erin" "is" "young" "+")
triple1
Erin is not young.
False
1
inv-proof
[(triple1)]
("Erin" "is" "young" "-")
triple1
Erin is rough.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Erin" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Erin" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
True
5
proof
[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule5))]
("Erin" "is" "kind" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not kind.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule5))]
("Erin" "is" "kind" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Erin is young.[(triple1)] @1: Erin is rough.[(((triple1) -> rule4))] @2: Erin is cold.[(((((triple1) -> rule4)) -> rule2))] @3: Erin is kind.[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule5))]
Erin is young.
("Erin" "is" "young" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3