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