Anne is nice. Dave is green. Dave is kind. Dave is nice. Dave is white. Erin is kind. Erin is nice. All nice, smart people are white. White, cold people are kind. If someone is smart then they are cold. If someone is smart and quiet then they are nice. If someone is quiet then they are smart. All white people are quiet. All green, cold people are quiet. If Anne is smart then Anne is green.
Anne is nice.
("Anne" "is" "nice" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
All nice, smart people are white.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
White, cold people are kind.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and quiet then they are nice.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All green, cold people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is smart then Anne is green.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "green" "+"))
Erin is kind.
True
1
proof
[(triple6)]
("Erin" "is" "kind" "+")
triple6
Erin is not kind.
False
1
inv-proof
[(triple6)]
("Erin" "is" "kind" "-")
triple6
Dave is quiet.
True
2
proof
[(((triple5) -> rule6))]
("Dave" "is" "quiet" "+")
((triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple5) -> rule6))]
("Dave" "is" "quiet" "-")
((triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
True
3
proof
[(((((triple5) -> rule6)) -> rule5))]
("Dave" "is" "smart" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple5) -> rule6)) -> rule5))]
("Dave" "is" "smart" "-")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@4: Erin is cold.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule6 <- rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Anne is quiet.
Unknown
rconc
[@5: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule5 <- rule7 <- rule8 <- FAIL)]]
("Anne" "is" "quiet" "+")
Erin is not white.
Unknown
inv-rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule6 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
@0: Anne is nice.[(triple1)] Dave is green.[(triple2)] Dave is kind.[(triple3 OR ((triple5 ((((((triple5) -> rule6)) -> rule5)) -> rule3)) -> rule2))] Dave is nice.[(triple4 OR ((((((triple5) -> rule6)) -> rule5) ((triple5) -> rule6)) -> rule4))] Dave is white.[(triple5)] Erin is kind.[(triple6)] Erin is nice.[(triple7)] @1: Dave is quiet.[(((triple5) -> rule6))] @2: Dave is smart.[(((((triple5) -> rule6)) -> rule5))] @3: Dave is cold.[(((((((triple5) -> rule6)) -> rule5)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple5 ((((((triple5) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
triple4
((((((triple5) -> (rule6 % int3))) -> (rule5 % int2)) ((triple5) -> (rule6 % int3))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is nice.
("Erin" "is" "nice" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple5) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3