Anne is blue. Anne is red. Anne is white. Furry, blue people are young. If someone is blue and smart then they are furry. All blue people are furry. If someone is young then they are red. If Anne is young and Anne is blue then Anne is white. If Anne is smart then Anne is red. Young, white people are smart. All furry people are big.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Furry, blue people are young.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is blue and smart then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Anne is young and Anne is blue then Anne is white.
((("Anne" "is" "young" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "white" "+"))
If Anne is smart then Anne is red.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "red" "+"))
Young, white people are smart.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Anne is white.
True
1
proof
[(triple3 OR ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5))]
("Anne" "is" "white" "+")
triple3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Anne is furry.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not young.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule1))]
("Anne" "is" "young" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is smart.
True
6
proof
[(((((((triple1) -> rule3) triple1) -> rule1) triple3) -> rule7) OR ((((((triple1) -> rule3) triple1) -> rule1) ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5)) -> rule7))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((triple1) -> (rule3 % int4)) triple1) -> (rule1 % int3)) ((((((triple1) -> (rule3 % int4)) triple1) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is not smart.
False
6
inv-proof
[(((((((triple1) -> rule3) triple1) -> rule1) triple3) -> rule7) OR ((((((triple1) -> rule3) triple1) -> rule1) ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5)) -> rule7))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((triple1) -> (rule3 % int4)) triple1) -> (rule1 % int3)) ((((((triple1) -> (rule3 % int4)) triple1) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
@0: Anne is blue.[(triple1)] Anne is red.[(triple2 OR ((((((triple1) -> rule3) triple1) -> rule1)) -> rule4) OR ((((((((triple1) -> rule3) triple1) -> rule1) triple3) -> rule7)) -> rule6) OR ((((((((triple1) -> rule3) triple1) -> rule1) ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5)) -> rule7)) -> rule6))] Anne is white.[(triple3 OR ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5))] @1: Anne is furry.[(((triple1) -> rule3))] @2: Anne is big.[(((((triple1) -> rule3)) -> rule8))] Anne is young.[(((((triple1) -> rule3) triple1) -> rule1))] @3: Anne is smart.[(((((((triple1) -> rule3) triple1) -> rule1) triple3) -> rule7) OR ((((((triple1) -> rule3) triple1) -> rule1) ((((((triple1) -> rule3) triple1) -> rule1) triple1) -> rule5)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
((((((((triple1) -> (rule3 % int5)) triple1) -> (rule1 % int4)) ((((((triple1) -> (rule3 % int5)) triple1) -> (rule1 % int4)) triple1) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
int5
Anne is white.
("Anne" "is" "white" "+")
triple3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple3) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
((((((triple1) -> (rule3 % int4)) triple1) -> (rule1 % int3)) ((((((triple1) -> (rule3 % int4)) triple1) -> (rule1 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4