Charlie is cold. Charlie is furry. Charlie is kind. Charlie is red. Charlie is white. Charlie is young. Harry is cold. Harry is furry. Harry is green. Harry is kind. Harry is red. Harry is young. If Harry is furry then Harry is white. If Charlie is green and Charlie is young then Charlie is furry. All young things are green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is furry then Harry is white.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "white" "+"))
If Charlie is green and Charlie is young then Charlie is furry.
((("Charlie" "is" "green" "+") ("Charlie" "is" "young" "+")) -> ("Charlie" "is" "furry" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Harry is young.
True
1
proof
[(triple12)]
("Harry" "is" "young" "+")
triple12
Harry is not red.
False
1
inv-proof
[(triple11)]
("Harry" "is" "red" "-")
triple11
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2 OR ((((triple6) -> rule3) triple6) -> rule2))] Charlie is kind.[(triple3)] Charlie is red.[(triple4)] Charlie is white.[(triple5)] Charlie is young.[(triple6)] Harry is cold.[(triple7)] Harry is furry.[(triple8)] Harry is green.[(triple9 OR ((triple12) -> rule3))] Harry is kind.[(triple10)] Harry is red.[(triple11)] Harry is young.[(triple12)] @1: Charlie is green.[(((triple6) -> rule3))] Harry is white.[(((triple8) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((((triple6) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple12) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Charlie is green.
("Charlie" "is" "green" "+")
((triple6) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple8) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1