Charlie is green. Charlie is rough. Erin is quiet. All rough, red things are quiet. Quiet, green things are white. If something is green then it is quiet. If Charlie is rough then Charlie is quiet. All white things are quiet. Green things are furry. All smart, furry things are quiet. Red things are green.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
All rough, red things are quiet.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Quiet, green things are white.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is rough then Charlie is quiet.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "quiet" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All smart, furry things are quiet.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
Erin is quiet.
True
1
proof
[(triple3)]
("Erin" "is" "quiet" "+")
triple3
Charlie is not rough.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "rough" "-")
triple2
Charlie is quiet.
True
2
proof
[(((triple1) -> rule3) OR ((triple2) -> rule4))]
("Charlie" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple2) -> rule4))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule2) OR ((((triple2) -> rule4) triple1) -> rule2))]
("Charlie" "is" "white" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule2) OR ((((triple2) -> rule4) triple1) -> rule2))]
("Charlie" "is" "white" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "green" "+")
Erin is not furry.
Unknown
inv-rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule6 <- rule8 <- FAIL)]]
("Erin" "is" "furry" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Charlie is green.[(triple1)] Charlie is rough.[(triple2)] Erin is quiet.[(triple3)] @1: Charlie is furry.[(((triple1) -> rule6))] Charlie is quiet.[(((triple1) -> rule3) OR ((triple2) -> rule4))] @2: Charlie is white.[(((((triple1) -> rule3) triple1) -> rule2) OR ((((triple2) -> rule4) triple1) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule4 % int2)) triple1) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2