Charlie is blue. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is smart. Charlie is white. Charlie is young. If Charlie is cold then Charlie is blue. If someone is kind and young then they are white. If someone is smart and young then they are furry.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If Charlie is cold then Charlie is blue.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "blue" "+"))
If someone is kind and young then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is smart and young then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Charlie is furry.
True
1
proof
[(triple3 OR ((triple5 triple7) -> rule3))]
("Charlie" "is" "furry" "+")
triple3
((triple5 triple7) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not white.
False
1
inv-proof
[(triple6 OR ((triple4 triple7) -> rule2))]
("Charlie" "is" "white" "-")
triple6
((triple4 triple7) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
@0: Charlie is blue.[(triple1 OR ((triple2) -> rule1))] Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple5 triple7) -> rule3))] Charlie is kind.[(triple4)] Charlie is smart.[(triple5)] Charlie is white.[(triple6 OR ((triple4 triple7) -> rule2))] Charlie is young.[(triple7)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple5 triple7) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple4 triple7) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple7