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