Charlie is cold. Charlie is not furry. Charlie is not nice. Charlie is quiet. Charlie is not red. Charlie is white. Charlie is young. Harry is not cold. Harry is furry. Harry is not nice. Harry is quiet. Harry is not red. Harry is white. Harry is young. If someone is red then they are not furry. Young people are not nice. All nice people are young. White people are young. If someone is red and not cold then they are white. If Harry is nice and Harry is not cold then Harry is not red. If Harry is furry and Harry is white then Harry is not nice. If someone is nice and not furry then they are quiet.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is red then they are not furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "-"))
Young people are not nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "-"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
White people are young.
((("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
If someone is red and not cold then they are white.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "white" "+"))
If Harry is nice and Harry is not cold then Harry is not red.
((("Harry" "is" "nice" "+") ("Harry" "is" "cold" "~")) -> ("Harry" "is" "red" "-"))
If Harry is furry and Harry is white then Harry is not nice.
((("Harry" "is" "furry" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "nice" "-"))
If someone is nice and not furry then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "quiet" "+"))
Charlie is young.
True
1
proof
[(triple7 OR ((triple6) -> rule4))]
("Charlie" "is" "young" "+")
triple7
((triple6) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
@0: Charlie is cold.[(triple1)] Charlie is not furry.[(triple2)] Charlie is not nice.[(triple3 OR ((triple7) -> rule2) OR ((((triple6) -> rule4)) -> rule2))] Charlie is not red.[(triple5)] Charlie is quiet.[(triple4)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple6) -> rule4))] Harry is furry.[(triple9)] Harry is not cold.[(triple8)] Harry is not nice.[(triple10 OR ((triple14) -> rule2) OR ((triple9 triple13) -> rule7) OR ((((triple13) -> rule4)) -> rule2))] Harry is not red.[(triple12)] Harry is quiet.[(triple11)] Harry is white.[(triple13)] Harry is young.[(triple14 OR ((triple13) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple3
((triple7) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not red.
("Charlie" "is" "red" "-")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple6) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is not cold.
("Harry" "is" "cold" "-")
triple8
Harry is not nice.
("Harry" "is" "nice" "-")
triple10
((triple14) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
((triple9 triple13) -> (rule7 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not red.
("Harry" "is" "red" "-")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple13
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple13) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1