Erin is white. Harry is not white. If someone is kind then they are round. If someone is smart and white then they are round. Smart people are quiet. If someone is white then they are blue. If someone is blue then they are kind. If Erin is not blue then Erin is not quiet.
Erin is white.
("Erin" "is" "white" "+")
Harry is not white.
("Harry" "is" "white" "-")
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If someone is smart and white then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Erin is not blue then Erin is not quiet.
((("Erin" "is" "blue" "~")) -> ("Erin" "is" "quiet" "-"))
Harry is not white.
True
1
proof
[(triple2)]
("Harry" "is" "white" "-")
triple2
Harry is white.
False
1
inv-proof
[(triple2)]
("Harry" "is" "white" "+")
triple2
Erin is blue.
True
2
proof
[(((triple1) -> rule4))]
("Erin" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple1) -> rule4))]
("Erin" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Erin" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not kind.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Erin" "is" "kind" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
True
4
proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule1))]
("Erin" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not round.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule1))]
("Erin" "is" "round" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is quiet.
Unknown
rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not kind.
Unknown
inv-rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is round.
Unknown
rconc
[@3: Harry is round.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule4 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Erin is white.[(triple1)] Harry is not white.[(triple2)] @1: Erin is blue.[(((triple1) -> rule4))] @2: Erin is kind.[(((((triple1) -> rule4)) -> rule5))] @3: Erin is round.[(((((((triple1) -> rule4)) -> rule5)) -> rule1))]
Erin is white.
("Erin" "is" "white" "+")
triple1
Harry is not white.
("Harry" "is" "white" "-")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3