Charlie is blue. Charlie is cold. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is round. Charlie is white. Harry is blue. Harry is cold. Harry is green. Harry is kind. Harry is quiet. Harry is round. Harry is white. Round people are cold. If someone is white then they are quiet. If Harry is white then Harry is green. If Charlie is quiet and Charlie is round then Charlie is kind. If Harry is green and Harry is not cold then Harry is quiet. If someone is quiet and not cold then they are not green.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is white then Harry is green.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "green" "+"))
If Charlie is quiet and Charlie is round then Charlie is kind.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "kind" "+"))
If Harry is green and Harry is not cold then Harry is quiet.
((("Harry" "is" "green" "+") ("Harry" "is" "cold" "~")) -> ("Harry" "is" "quiet" "+"))
If someone is quiet and not cold then they are not green.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "green" "-"))
Harry is quiet.
True
1
proof
[(triple12 OR ((triple14) -> rule2))]
("Harry" "is" "quiet" "+")
triple12
((triple14) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is not cold.
False
1
inv-proof
[(triple2 OR ((triple6) -> rule1))]
("Charlie" "is" "cold" "-")
triple2
((triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2 OR ((triple6) -> rule1))] Charlie is green.[(triple3)] Charlie is kind.[(triple4 OR ((triple5 triple6) -> rule4) OR ((((triple7) -> rule2) triple6) -> rule4))] Charlie is quiet.[(triple5 OR ((triple7) -> rule2))] Charlie is round.[(triple6)] Charlie is white.[(triple7)] Harry is blue.[(triple8)] Harry is cold.[(triple9 OR ((triple13) -> rule1))] Harry is green.[(triple10 OR ((triple14) -> rule3))] Harry is kind.[(triple11)] Harry is quiet.[(triple12 OR ((triple14) -> rule2))] Harry is round.[(triple13)] Harry is white.[(triple14)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple6) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple5 triple6) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple7) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple7) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple13) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple10
((triple14) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
((triple14) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14