Anne is not big. Anne is blue. Anne is cold. Anne is nice. Anne is quiet. Anne is rough. Anne is smart. Gary is big. Gary is blue. Gary is not cold. Gary is nice. Gary is quiet. Gary is rough. Gary is smart. All blue things are smart. Cold things are smart. Blue things are smart. If something is quiet and not big then it is blue. If something is nice and not big then it is rough. If Gary is not cold then Gary is quiet. All rough things are nice. If Gary is not rough then Gary is not smart.
Anne is not big.
("Anne" "is" "big" "-")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
If something is quiet and not big then it is blue.
((("something" "is" "quiet" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "+"))
If something is nice and not big then it is rough.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "rough" "+"))
If Gary is not cold then Gary is quiet.
((("Gary" "is" "cold" "~")) -> ("Gary" "is" "quiet" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If Gary is not rough then Gary is not smart.
((("Gary" "is" "rough" "~")) -> ("Gary" "is" "smart" "-"))
Anne is blue.
True
1
proof
[(triple2 OR ((triple5 triple1) -> rule4))]
("Anne" "is" "blue" "+")
triple2
((triple5 triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not nice.
False
1
inv-proof
[(triple4 OR ((triple6) -> rule7))]
("Anne" "is" "nice" "-")
triple4
((triple6) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
@0: Anne is blue.[(triple2 OR ((triple5 triple1) -> rule4))] Anne is cold.[(triple3)] Anne is nice.[(triple4 OR ((triple6) -> rule7))] Anne is not big.[(triple1)] Anne is quiet.[(triple5)] Anne is rough.[(triple6 OR ((triple4 triple1) -> rule5))] Anne is smart.[(triple7 OR ((triple2) -> rule1) OR ((triple2) -> rule3) OR ((triple3) -> rule2) OR ((((triple5 triple1) -> rule4)) -> rule1) OR ((((triple5 triple1) -> rule4)) -> rule3))] Gary is big.[(triple8)] Gary is blue.[(triple9)] Gary is nice.[(triple11 OR ((triple13) -> rule7))] Gary is not cold.[(triple10)] Gary is quiet.[(triple12 OR ((triple10) -> rule6))] Gary is rough.[(triple13)] Gary is smart.[(triple14 OR ((triple9) -> rule1) OR ((triple9) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple5 triple1) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple6) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
((triple4 triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple3) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple5 triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple5 triple1) -> (rule4 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is nice.
("Gary" "is" "nice" "+")
triple11
((triple13) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
((triple10) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple13
Gary is smart.
("Gary" "is" "smart" "+")
triple14
((triple9) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple9) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1