Charlie is quiet. Dave is kind. Erin is green. All rough, smart people are nice. If Charlie is furry then Charlie is smart. All rough, quiet people are nice. If Dave is smart then Dave is green. Green people are nice. Furry people are rough. All nice people are rough. All nice, furry people are quiet.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is green.
("Erin" "is" "green" "+")
All rough, smart people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is furry then Charlie is smart.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "smart" "+"))
All rough, quiet people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If Dave is smart then Dave is green.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All nice, furry people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Erin is green.
True
1
proof
[(triple3)]
("Erin" "is" "green" "+")
triple3
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Erin is nice.
True
2
proof
[(((triple3) -> rule5))]
("Erin" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("Erin" "is" "nice" "-")
((triple3) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
True
3
proof
[(((((triple3) -> rule5)) -> rule7))]
("Erin" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not rough.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule7))]
("Erin" "is" "rough" "-")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("Dave" "is" "nice" "-")
Charlie is smart.
Unknown
rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is quiet.[(triple1)] Dave is kind.[(triple2)] Erin is green.[(triple3)] @1: Erin is nice.[(((triple3) -> rule5))] @2: Erin is rough.[(((((triple3) -> rule5)) -> rule7))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2