Erin is kind. Erin is not round. Erin is white. All kind people are green. If someone is round and not furry then they are red. If someone is green and not round then they are red. Kind people are white. All furry people are white. If Erin is kind and Erin is green then Erin is red. If someone is red then they are blue. If someone is red and not green then they are blue.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is white.
("Erin" "is" "white" "+")
All kind people are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is round and not furry then they are red.
((("someone" "is" "round" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "red" "+"))
If someone is green and not round then they are red.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "red" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If Erin is kind and Erin is green then Erin is red.
((("Erin" "is" "kind" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "red" "+"))
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and not green then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "blue" "+"))
Erin is white.
True
1
proof
[(triple3 OR ((triple1) -> rule4))]
("Erin" "is" "white" "+")
triple3
((triple1) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "+")
triple2
Erin is green.
True
2
proof
[(((triple1) -> rule1))]
("Erin" "is" "green" "+")
((triple1) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Erin" "is" "green" "-")
((triple1) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule1) triple2) -> rule3))]
("Erin" "is" "red" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule1) triple2) -> rule3))]
("Erin" "is" "red" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is blue.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule7) OR ((((((triple1) -> rule1) triple2) -> rule3)) -> rule7))]
("Erin" "is" "blue" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not blue.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule7) OR ((((((triple1) -> rule1) triple2) -> rule3)) -> rule7))]
("Erin" "is" "blue" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
@0: Erin is kind.[(triple1)] Erin is not round.[(triple2)] Erin is white.[(triple3 OR ((triple1) -> rule4))] @1: Erin is green.[(((triple1) -> rule1))] @2: Erin is red.[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule1) triple2) -> rule3))] @3: Erin is blue.[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule7) OR ((((((triple1) -> rule1) triple2) -> rule3)) -> rule7))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Erin is not round.
("Erin" "is" "round" "-")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
((triple1) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple1) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((((triple1) -> (rule1 % int3)) triple2) -> (rule3 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3