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