Dave is big. Dave is furry. Gary is blue. If Dave is blue and Dave is furry then Dave is cold. All big people are quiet. If someone is quiet then they are white. Cold, white people are furry. Cold, furry people are big. Blue, furry people are big.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If Dave is blue and Dave is furry then Dave is cold.
((("Dave" "is" "blue" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "cold" "+"))
All big people are quiet.
((("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
Cold, white people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Cold, furry people are big.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Blue, furry people are big.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Gary is blue.
True
1
proof
[(triple3)]
("Gary" "is" "blue" "+")
triple3
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is quiet.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not white.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Dave" "is" "white" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is white.
Unknown
rconc
[@4: Gary is white.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule6 <- rule4 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Gary is blue.[(triple3)] @1: Dave is quiet.[(((triple1) -> rule2))] @2: Dave is white.[(((((triple1) -> rule2)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2