Erin is round. If Erin is smart then Erin is rough. If Erin is round then Erin is rough. All smart people are round. All red people are smart. Red, round people are not smart. All rough people are kind. If someone is kind then they are quiet. If someone is red and rough then they are not furry.
Erin is round.
("Erin" "is" "round" "+")
If Erin is smart then Erin is rough.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "rough" "+"))
If Erin is round then Erin is rough.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "rough" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
All red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Red, round people are not smart.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "-"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red and rough then they are not furry.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "-"))
Erin is round.
True
1
proof
[(triple1)]
("Erin" "is" "round" "+")
triple1
Erin is not round.
False
1
inv-proof
[(triple1)]
("Erin" "is" "round" "-")
triple1
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 kind.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Erin" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Erin" "is" "kind" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule7))]
("Erin" "is" "quiet" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule7))]
("Erin" "is" "quiet" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Erin is round.[(triple1)] @1: Erin is rough.[(((triple1) -> rule2))] @2: Erin is kind.[(((((triple1) -> rule2)) -> rule6))] @3: Erin is quiet.[(((((((triple1) -> rule2)) -> rule6)) -> rule7))]
Erin is round.
("Erin" "is" "round" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3