Anne is furry. Anne is nice. Anne is smart. All nice, red things are young. All nice, young things are quiet. Furry things are quiet. If something is young then it is furry. If something is young then it is red. All furry, smart things are young. Nice, young things are red. If something is red and smart then it is young.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
All nice, red things are young.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All nice, young things are quiet.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is young then it is furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
All furry, smart things are young.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Nice, young things are red.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is red and smart then it is young.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple3)]
("Anne" "is" "smart" "-")
triple3
Anne is young.
True
3
proof
[(((triple1 triple3) -> rule6))]
("Anne" "is" "young" "+")
((triple1 triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple2 ((triple1 triple3) -> rule6)) -> rule2))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple2 ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
True
4
proof
[(((((triple1 triple3) -> rule6)) -> rule5) OR ((triple2 ((triple1 triple3) -> rule6)) -> rule7))]
("Anne" "is" "red" "+")
((((triple1 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple2 ((triple1 triple3) -> (rule6 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple1 triple3) -> rule6)) -> rule5) OR ((triple2 ((triple1 triple3) -> rule6)) -> rule7))]
("Anne" "is" "red" "-")
((((triple1 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple2 ((triple1 triple3) -> (rule6 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
@0: Anne is furry.[(triple1)] Anne is nice.[(triple2)] Anne is smart.[(triple3)] @1: Anne is quiet.[(((triple1) -> rule3) OR ((triple2 ((triple1 triple3) -> rule6)) -> rule2))] Anne is young.[(((triple1 triple3) -> rule6))] @2: Anne is red.[(((((triple1 triple3) -> rule6)) -> rule5) OR ((triple2 ((triple1 triple3) -> rule6)) -> rule7))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple2 ((triple1 triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple1 triple3) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1 triple3) -> (rule6 % int2))) -> (rule5 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple2 ((triple1 triple3) -> (rule6 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2