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