Anne is nice. Anne is round. Anne is white. If something is white then it is smart. If something is green then it is kind. If something is white then it is nice. If something is smart and nice then it is kind. All kind things are blue. If something is green and nice then it is kind.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
If something is white then it is smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If something is green then it is kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is smart and nice then it is kind.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is green and nice then it is kind.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Anne is white.
True
1
proof
[(triple3)]
("Anne" "is" "white" "+")
triple3
Anne is not white.
False
1
inv-proof
[(triple3)]
("Anne" "is" "white" "-")
triple3
Anne is smart.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
True
4
proof
[(((((triple3) -> rule1) triple1) -> rule4) OR ((((triple3) -> rule1) ((triple3) -> rule3)) -> rule4))]
("Anne" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not kind.
False
4
inv-proof
[(((((triple3) -> rule1) triple1) -> rule4) OR ((((triple3) -> rule1) ((triple3) -> rule3)) -> rule4))]
("Anne" "is" "kind" "-")
((((triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is blue.
True
5
proof
[(((((((triple3) -> rule1) triple1) -> rule4)) -> rule5) OR ((((((triple3) -> rule1) ((triple3) -> rule3)) -> rule4)) -> rule5))]
("Anne" "is" "blue" "+")
((((((triple3) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple3) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not blue.
False
5
inv-proof
[(((((((triple3) -> rule1) triple1) -> rule4)) -> rule5) OR ((((((triple3) -> rule1) ((triple3) -> rule3)) -> rule4)) -> rule5))]
("Anne" "is" "blue" "-")
((((((triple3) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple3) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
@0: Anne is nice.[(triple1 OR ((triple3) -> rule3))] Anne is round.[(triple2)] Anne is white.[(triple3)] @1: Anne is smart.[(((triple3) -> rule1))] @2: Anne is kind.[(((((triple3) -> rule1) triple1) -> rule4) OR ((((triple3) -> rule1) ((triple3) -> rule3)) -> rule4))] @3: Anne is blue.[(((((((triple3) -> rule1) triple1) -> rule4)) -> rule5) OR ((((((triple3) -> rule1) ((triple3) -> rule3)) -> rule4)) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
((triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple3) -> (rule1 % int2)) triple1) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple3) -> (rule1 % int3)) ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple3) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
((((((triple3) -> (rule1 % int4)) ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4