Anne is not big. Anne is cold. Anne is furry. Anne is nice. Anne is rough. Anne is round. Anne is young. Gary is cold. Gary is not furry. Gary is nice. Gary is round. Gary is young. All young, furry things are round. All big things are not nice. All young things are nice. If something is furry and big then it is nice. If something is cold and not furry then it is rough. If Gary is cold and Gary is not furry then Gary is nice. If something is cold then it is young. If Gary is big and Gary is not nice then Gary is rough.
Anne is not big.
("Anne" "is" "big" "-")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
All young, furry things are round.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
All big things are not nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is furry and big then it is nice.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If something is cold and not furry then it is rough.
((("something" "is" "cold" "+") ("something" "is" "furry" "~")) -> ("something" "is" "rough" "+"))
If Gary is cold and Gary is not furry then Gary is nice.
((("Gary" "is" "cold" "+") ("Gary" "is" "furry" "~")) -> ("Gary" "is" "nice" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If Gary is big and Gary is not nice then Gary is rough.
((("Gary" "is" "big" "+") ("Gary" "is" "nice" "~")) -> ("Gary" "is" "rough" "+"))
Gary is round.
True
1
proof
[(triple11)]
("Gary" "is" "round" "+")
triple11
Anne is not cold.
False
1
inv-proof
[(triple2)]
("Anne" "is" "cold" "-")
triple2
Gary is rough.
True
3
proof
[(((triple8 triple9) -> rule5))]
("Gary" "is" "rough" "+")
((triple8 triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
3
inv-proof
[(((triple8 triple9) -> rule5))]
("Gary" "is" "rough" "-")
((triple8 triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
@0: Anne is cold.[(triple2)] Anne is furry.[(triple3)] Anne is nice.[(triple4 OR ((triple7) -> rule3) OR ((((triple2) -> rule7)) -> rule3))] Anne is not big.[(triple1)] Anne is rough.[(triple5)] Anne is round.[(triple6 OR ((triple7 triple3) -> rule1) OR ((((triple2) -> rule7) triple3) -> rule1))] Anne is young.[(triple7 OR ((triple2) -> rule7))] Gary is cold.[(triple8)] Gary is nice.[(triple10 OR ((triple12) -> rule3) OR ((triple8 triple9) -> rule6) OR ((((triple8) -> rule7)) -> rule3))] Gary is not furry.[(triple9)] Gary is round.[(triple11)] Gary is young.[(triple12 OR ((triple8) -> rule7))] @1: Gary is rough.[(((triple8 triple9) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple7) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple7 triple3) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple2) -> (rule7 % int2)) triple3) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple2) -> (rule7 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple10
((triple12) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple8 triple9) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple8) -> (rule7 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
((triple8) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple8 triple9) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1