Anne is big. Anne is not cold. Anne is green. Anne is kind. Anne is nice. Anne is round. Anne is white. Gary is big. Gary is cold. Gary is green. Gary is kind. Harry is big. Harry is cold. Harry is green. Harry is kind. Harry is round. If Harry is not cold then Harry is not white. If Harry is kind then Harry is white. Kind, cold things are nice. If Anne is not big then Anne is round. If something is nice and not cold then it is white. If something is nice then it is round.
Anne is big.
("Anne" "is" "big" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is not cold then Harry is not white.
((("Harry" "is" "cold" "~")) -> ("Harry" "is" "white" "-"))
If Harry is kind then Harry is white.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
Kind, cold things are nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If Anne is not big then Anne is round.
((("Anne" "is" "big" "~")) -> ("Anne" "is" "round" "+"))
If something is nice and not cold then it is white.
((("something" "is" "nice" "+") ("something" "is" "cold" "~")) -> ("something" "is" "white" "+"))
If something is nice then it is round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Anne is white.
True
1
proof
[(triple7 OR ((triple5 triple2) -> rule5))]
("Anne" "is" "white" "+")
triple7
((triple5 triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Harry is not round.
False
1
inv-proof
[(triple16 OR ((((triple15 triple13) -> rule3)) -> rule6))]
("Harry" "is" "round" "-")
triple16
((((triple15 triple13) -> (rule3 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Gary is nice.
True
3
proof
[(((triple11 triple9) -> rule3))]
("Gary" "is" "nice" "+")
((triple11 triple9) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is not nice.
False
3
inv-proof
[(((triple15 triple13) -> rule3))]
("Harry" "is" "nice" "-")
((triple15 triple13) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Gary is round.
True
4
proof
[(((((triple11 triple9) -> rule3)) -> rule6))]
("Gary" "is" "round" "+")
((((triple11 triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not round.
False
4
inv-proof
[(((((triple11 triple9) -> rule3)) -> rule6))]
("Gary" "is" "round" "-")
((((triple11 triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
@0: Anne is big.[(triple1)] Anne is green.[(triple3)] Anne is kind.[(triple4)] Anne is nice.[(triple5)] Anne is not cold.[(triple2)] Anne is round.[(triple6 OR ((triple5) -> rule6))] Anne is white.[(triple7 OR ((triple5 triple2) -> rule5))] Gary is big.[(triple8)] Gary is cold.[(triple9)] Gary is green.[(triple10)] Gary is kind.[(triple11)] Harry is big.[(triple12)] Harry is cold.[(triple13)] Harry is green.[(triple14)] Harry is kind.[(triple15)] Harry is round.[(triple16 OR ((((triple15 triple13) -> rule3)) -> rule6))] @1: Gary is nice.[(((triple11 triple9) -> rule3))] Harry is nice.[(((triple15 triple13) -> rule3))] Harry is white.[(((triple15) -> rule2))] @2: Gary is round.[(((((triple11 triple9) -> rule3)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is not cold.
("Anne" "is" "cold" "-")
triple2
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple5) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple7
((triple5 triple2) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Harry is big.
("Harry" "is" "big" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is kind.
("Harry" "is" "kind" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16
((((triple15 triple13) -> (rule3 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple11 triple9) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple15 triple13) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple15) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple11 triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2