Dave is cold. Dave is furry. Dave is not nice. Dave is rough. Dave is white. Dave is young. Harry is cold. Harry is green. Harry is rough. Harry is white. Cold people are white. All young people are furry. All nice people are furry. All green people are nice. If someone is young and rough then they are not green. If someone is young and not white then they are not rough.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All young people are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is young and rough then they are not green.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If someone is young and not white then they are not rough.
((("someone" "is" "young" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "-"))
Dave is cold.
True
1
proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "-")
triple1
Dave is not green.
True
3
proof
[(((triple6 triple4) -> rule5))]
("Dave" "is" "green" "-")
((triple6 triple4) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is green.
False
3
inv-proof
[(((triple6 triple4) -> rule5))]
("Dave" "is" "green" "+")
((triple6 triple4) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Harry is furry.
True
3
proof
[(((((triple8) -> rule4)) -> rule3))]
("Harry" "is" "furry" "+")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule3))]
("Harry" "is" "furry" "-")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
@0: Dave is cold.[(triple1)] Dave is furry.[(triple2 OR ((triple6) -> rule2))] Dave is not nice.[(triple3)] Dave is rough.[(triple4)] Dave is white.[(triple5 OR ((triple1) -> rule1))] Dave is young.[(triple6)] Harry is cold.[(triple7)] Harry is green.[(triple8)] Harry is rough.[(triple9)] Harry is white.[(triple10 OR ((triple7) -> rule1))] @1: Dave is not green.[(((triple6 triple4) -> rule5))] Harry is nice.[(((triple8) -> rule4))] @2: Harry is furry.[(((((triple8) -> rule4)) -> rule3))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple6) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not nice.
("Dave" "is" "nice" "-")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
((triple7) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is not green.
("Dave" "is" "green" "-")
((triple6 triple4) -> (rule5 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple8) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2