Anne is blue. Anne is green. Anne is red. Anne is smart. Bob is blue. Bob is green. Bob is red. Bob is white. Dave is blue. Dave is cold. Dave is green. Dave is red. Dave is smart. Dave is white. Dave is young. Cold people are white. All young, blue people are cold. If someone is green and young then they are red. If Dave is smart and Dave is red then Dave is young. Red people are young. If someone is white then they are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All young, blue people are cold.
((("someone" "is" "young" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and young then they are red.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If Dave is smart and Dave is red then Dave is young.
((("Dave" "is" "smart" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "young" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Dave is red.
True
1
proof
[(triple12 OR ((triple11 triple15) -> rule3))]
("Dave" "is" "red" "+")
triple12
((triple11 triple15) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Bob is not white.
False
1
inv-proof
[(triple8 OR ((((((triple7) -> rule5) triple5) -> rule2)) -> rule1))]
("Bob" "is" "white" "-")
triple8
((((((triple7) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Anne is young.
True
2
proof
[(((triple3) -> rule5))]
("Anne" "is" "young" "+")
((triple3) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple3) -> rule5))]
("Anne" "is" "young" "-")
((triple3) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is cold.
True
4
proof
[(((((triple3) -> rule5) triple1) -> rule2))]
("Anne" "is" "cold" "+")
((((triple3) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((((triple7) -> rule5) triple5) -> rule2) OR ((((triple7) -> rule5) ((triple8) -> rule6)) -> rule2))]
("Bob" "is" "cold" "-")
((((triple7) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple7) -> (rule5 % int3)) ((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Anne is white.
True
5
proof
[(((((((triple3) -> rule5) triple1) -> rule2)) -> rule1))]
("Anne" "is" "white" "+")
((((((triple3) -> (rule5 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not white.
False
5
inv-proof
[(((((((triple3) -> rule5) triple1) -> rule2)) -> rule1))]
("Anne" "is" "white" "-")
((((((triple3) -> (rule5 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is red.[(triple3)] Anne is smart.[(triple4)] Bob is blue.[(triple5 OR ((triple8) -> rule6))] Bob is green.[(triple6)] Bob is red.[(triple7)] Bob is white.[(triple8 OR ((((((triple7) -> rule5) triple5) -> rule2)) -> rule1))] Dave is blue.[(triple9 OR ((triple14) -> rule6) OR ((((triple10) -> rule1)) -> rule6))] Dave is cold.[(triple10 OR ((triple15 triple9) -> rule2) OR ((triple15 ((triple14) -> rule6)) -> rule2) OR ((((triple12) -> rule5) triple9) -> rule2) OR ((((triple13 triple12) -> rule4) triple9) -> rule2) OR ((((triple12) -> rule5) ((triple14) -> rule6)) -> rule2) OR ((((triple13 triple12) -> rule4) ((triple14) -> rule6)) -> rule2))] Dave is green.[(triple11)] Dave is red.[(triple12 OR ((triple11 triple15) -> rule3))] Dave is smart.[(triple13)] Dave is white.[(triple14 OR ((triple10) -> rule1) OR ((((triple15 triple9) -> rule2)) -> rule1) OR ((((((triple12) -> rule5) triple9) -> rule2)) -> rule1) OR ((((((triple13 triple12) -> rule4) triple9) -> rule2)) -> rule1))] Dave is young.[(triple15 OR ((triple12) -> rule5) OR ((triple13 triple12) -> rule4))] @1: Anne is young.[(((triple3) -> rule5))] Bob is young.[(((triple7) -> rule5))] @2: Anne is cold.[(((((triple3) -> rule5) triple1) -> rule2))] Bob is cold.[(((((triple7) -> rule5) triple5) -> rule2) OR ((((triple7) -> rule5) ((triple8) -> rule6)) -> rule2))] @3: Anne is white.[(((((((triple3) -> rule5) triple1) -> rule2)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Bob is blue.
("Bob" "is" "blue" "+")
triple5
((triple8) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is red.
("Bob" "is" "red" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
triple8
((((((triple7) -> (rule5 % int3)) triple5) -> (rule2 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
triple9
((triple14) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple10
((triple15 triple9) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple15 ((triple14) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((triple12) -> (rule5 % int2)) triple9) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple13 triple12) -> (rule4 % int2)) triple9) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple12) -> (rule5 % int3)) ((triple14) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((triple13 triple12) -> (rule4 % int3)) ((triple14) -> (rule6 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple11
Dave is red.
("Dave" "is" "red" "+")
triple12
((triple11 triple15) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple13
Dave is white.
("Dave" "is" "white" "+")
triple14
((triple10) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple15 triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
((((((triple12) -> (rule5 % int3)) triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((triple13 triple12) -> (rule4 % int3)) triple9) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple15
((triple12) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple13 triple12) -> (rule4 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple3) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple7) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple3) -> (rule5 % int2)) triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple7) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((((triple7) -> (rule5 % int3)) ((triple8) -> (rule6 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((((triple3) -> (rule5 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3