Anne is big. Anne is cold. Anne is kind. Anne is nice. Anne is rough. Anne is smart. Harry is big. Harry is cold. Harry is not kind. Harry is nice. Harry is rough. Harry is smart. If Anne is smart then Anne is red.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Anne is smart then Anne is red.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "red" "+"))
Anne is cold.
True
1
proof
[(triple2)]
("Anne" "is" "cold" "+")
triple2
Harry is kind.
False
1
inv-proof
[(triple9)]
("Harry" "is" "kind" "+")
triple9
Anne is red.
True
2
proof
[(((triple6) -> rule1))]
("Anne" "is" "red" "+")
((triple6) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple6) -> rule1))]
("Anne" "is" "red" "-")
((triple6) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4)] Anne is rough.[(triple5)] Anne is smart.[(triple6)] Harry is big.[(triple7)] Harry is cold.[(triple8)] Harry is nice.[(triple10)] Harry is not kind.[(triple9)] Harry is rough.[(triple11)] Harry is smart.[(triple12)] @1: Anne is red.[(((triple6) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Anne is red.
("Anne" "is" "red" "+")
((triple6) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1