Anne is blue. Anne is rough. Anne is white. Anne is young. Bob is furry. Bob is white. Bob is young. All blue, white things are red. If something is young and furry then it is blue. Red, young things are furry. All furry things are white. Green, white things are red. All rough, red things are blue. Green things are red. All red, young things are green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
All blue, white things are red.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is young and furry then it is blue.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
Red, young things are furry.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Green, white things are red.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All rough, red things are blue.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Green things are red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
All red, young things are green.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
Anne is young.
True
1
proof
[(triple4)]
("Anne" "is" "young" "+")
triple4
Anne is not rough.
False
1
inv-proof
[(triple2)]
("Anne" "is" "rough" "-")
triple2
Bob is blue.
True
3
proof
[(((triple7 triple5) -> rule2))]
("Bob" "is" "blue" "+")
((triple7 triple5) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Anne is not red.
False
3
inv-proof
[(((triple1 triple3) -> rule1))]
("Anne" "is" "red" "-")
((triple1 triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is red.
True
5
proof
[(((((triple7 triple5) -> rule2) triple6) -> rule1) OR ((((triple7 triple5) -> rule2) ((triple5) -> rule4)) -> rule1))]
("Bob" "is" "red" "+")
((((triple7 triple5) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple7 triple5) -> (rule2 % int3)) ((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Anne is not furry.
False
5
inv-proof
[(((((triple1 triple3) -> rule1) triple4) -> rule3))]
("Anne" "is" "furry" "-")
((((triple1 triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is green.
True
7
proof
[(((((((triple7 triple5) -> rule2) triple6) -> rule1) triple7) -> rule8) OR ((((((triple7 triple5) -> rule2) ((triple5) -> rule4)) -> rule1) triple7) -> rule8))]
("Bob" "is" "green" "+")
((((((triple7 triple5) -> (rule2 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple7 triple5) -> (rule2 % int4)) ((triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is not green.
False
7
inv-proof
[(((((((triple7 triple5) -> rule2) triple6) -> rule1) triple7) -> rule8) OR ((((((triple7 triple5) -> rule2) ((triple5) -> rule4)) -> rule1) triple7) -> rule8))]
("Bob" "is" "green" "-")
((((((triple7 triple5) -> (rule2 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple7 triple5) -> (rule2 % int4)) ((triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
@0: Anne is blue.[(triple1)] Anne is rough.[(triple2)] Anne is white.[(triple3)] Anne is young.[(triple4)] Bob is furry.[(triple5)] Bob is white.[(triple6 OR ((triple5) -> rule4))] Bob is young.[(triple7)] @1: Anne is red.[(((triple1 triple3) -> rule1))] Bob is blue.[(((triple7 triple5) -> rule2))] @2: Anne is furry.[(((((triple1 triple3) -> rule1) triple4) -> rule3))] Anne is green.[(((((triple1 triple3) -> rule1) triple4) -> rule8))] Bob is red.[(((((triple7 triple5) -> rule2) triple6) -> rule1) OR ((((triple7 triple5) -> rule2) ((triple5) -> rule4)) -> rule1))] @3: Bob is green.[(((((((triple7 triple5) -> rule2) triple6) -> rule1) triple7) -> rule8) OR ((((((triple7 triple5) -> rule2) ((triple5) -> rule4)) -> rule1) triple7) -> rule8))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
Bob is furry.
("Bob" "is" "furry" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple5) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple1 triple3) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple7 triple5) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1 triple3) -> (rule1 % int2)) triple4) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((triple1 triple3) -> (rule1 % int2)) triple4) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((((triple7 triple5) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple7 triple5) -> (rule2 % int3)) ((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
((((((triple7 triple5) -> (rule2 % int3)) triple6) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
((((((triple7 triple5) -> (rule2 % int4)) ((triple5) -> (rule4 % int3))) -> (rule1 % int2)) triple7) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4