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