Anne is blue. Anne is cold. Anne is kind. Anne is red. Anne is round. Anne is young. Erin is cold. Erin is red. Erin is round. Erin is white. All round people are blue. If Erin is blue and Erin is white then Erin is kind. If someone is round and cold then they are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
All round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Erin is blue and Erin is white then Erin is kind.
((("Erin" "is" "blue" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "kind" "+"))
If someone is round and cold then they are young.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Anne is blue.
True
1
proof
[(triple1 OR ((triple5) -> rule1))]
("Anne" "is" "blue" "+")
triple1
((triple5) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not blue.
False
1
inv-proof
[(triple1 OR ((triple5) -> rule1))]
("Anne" "is" "blue" "-")
triple1
((triple5) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Erin is young.
True
3
proof
[(((triple9 triple7) -> rule3))]
("Erin" "is" "young" "+")
((triple9 triple7) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
3
inv-proof
[(((triple9 triple7) -> rule3))]
("Erin" "is" "young" "-")
((triple9 triple7) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
True
4
proof
[(((((triple9) -> rule1) triple10) -> rule2))]
("Erin" "is" "kind" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not kind.
False
4
inv-proof
[(((((triple9) -> rule1) triple10) -> rule2))]
("Erin" "is" "kind" "-")
((((triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
@0: Anne is blue.[(triple1 OR ((triple5) -> rule1))] Anne is cold.[(triple2)] Anne is kind.[(triple3)] Anne is red.[(triple4)] Anne is round.[(triple5)] Anne is young.[(triple6 OR ((triple5 triple2) -> rule3))] Erin is cold.[(triple7)] Erin is red.[(triple8)] Erin is round.[(triple9)] Erin is white.[(triple10)] @1: Erin is blue.[(((triple9) -> rule1))] Erin is young.[(((triple9 triple7) -> rule3))] @2: Erin is kind.[(((((triple9) -> rule1) triple10) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple5) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple5 triple2) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is round.
("Erin" "is" "round" "+")
triple9
Erin is white.
("Erin" "is" "white" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
((triple9) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple9 triple7) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2