Anne is not green. Anne is nice. Anne is young. All nice people are smart. All nice, rough people are smart. All furry, white people are smart. If Anne is not young then Anne is green. If Anne is smart and Anne is nice then Anne is not furry. If Anne is white and Anne is rough then Anne is smart. Nice, young people are rough. If someone is white and not smart then they are green.
Anne is not green.
("Anne" "is" "green" "-")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is young.
("Anne" "is" "young" "+")
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
All nice, rough people are smart.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
All furry, white people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Anne is not young then Anne is green.
((("Anne" "is" "young" "~")) -> ("Anne" "is" "green" "+"))
If Anne is smart and Anne is nice then Anne is not furry.
((("Anne" "is" "smart" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "furry" "-"))
If Anne is white and Anne is rough then Anne is smart.
((("Anne" "is" "white" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "smart" "+"))
Nice, young people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is white and not smart then they are green.
((("someone" "is" "white" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "green" "+"))
Anne is young.
True
1
proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Anne is not young.
False
1
inv-proof
[(triple3)]
("Anne" "is" "young" "-")
triple3
Anne is rough.
True
3
proof
[(((triple2 triple3) -> rule7))]
("Anne" "is" "rough" "+")
((triple2 triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
3
inv-proof
[(((triple2 triple3) -> rule7))]
("Anne" "is" "rough" "-")
((triple2 triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not furry.
True
4
proof
[(((((triple2) -> rule1) triple2) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule7)) -> rule2) triple2) -> rule5))]
("Anne" "is" "furry" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is furry.
False
4
inv-proof
[(((((triple2) -> rule1) triple2) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule7)) -> rule2) triple2) -> rule5))]
("Anne" "is" "furry" "+")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
@0: Anne is nice.[(triple2)] Anne is not green.[(triple1)] Anne is young.[(triple3)] @1: Anne is rough.[(((triple2 triple3) -> rule7))] Anne is smart.[(((triple2) -> rule1) OR ((triple2 ((triple2 triple3) -> rule7)) -> rule2))] @2: Anne is not furry.[(((((triple2) -> rule1) triple2) -> rule5) OR ((((triple2 ((triple2 triple3) -> rule7)) -> rule2) triple2) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not green.
("Anne" "is" "green" "-")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 triple3) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple2 ((triple2 triple3) -> (rule7 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not furry.
("Anne" "is" "furry" "-")
((((triple2) -> (rule1 % int2)) triple2) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 ((triple2 triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3