Erin is red. If something is kind and not white then it is not cold. All nice, rough things are round. Nice things are rough. If something is kind then it is not rough. If Erin is red then Erin is nice. If Erin is not nice then Erin is cold.
Erin is red.
("Erin" "is" "red" "+")
If something is kind and not white then it is not cold.
((("something" "is" "kind" "+") ("something" "is" "white" "~")) -> ("something" "is" "cold" "-"))
All nice, rough things are round.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is not rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "-"))
If Erin is red then Erin is nice.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "nice" "+"))
If Erin is not nice then Erin is cold.
((("Erin" "is" "nice" "~")) -> ("Erin" "is" "cold" "+"))
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 nice.
True
2
proof
[(((triple1) -> rule5))]
("Erin" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple1) -> rule5))]
("Erin" "is" "nice" "-")
((triple1) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("Erin" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("Erin" "is" "rough" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
True
6
proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule2))]
("Erin" "is" "round" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not round.
False
6
inv-proof
[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule2))]
("Erin" "is" "round" "-")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Erin is red.[(triple1)] @1: Erin is nice.[(((triple1) -> rule5))] @2: Erin is rough.[(((((triple1) -> rule5)) -> rule3))] @3: Erin is round.[(((((triple1) -> rule5) ((((triple1) -> rule5)) -> rule3)) -> rule2))]
Erin is red.
("Erin" "is" "red" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple1) -> (rule5 % int3)) ((((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3