Erin is blue. Erin is cold. Erin is furry. Erin is kind. Erin is nice. Gary is not blue. Gary is cold. Gary is furry. Gary is not kind. Gary is nice. Gary is round. Gary is smart. All round things are nice. All smart things are nice. If something is furry and nice then it is smart. All furry things are round. If Erin is not nice then Erin is not blue. If something is smart and not blue then it is cold.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is furry and nice then it is smart.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
All furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Erin is not nice then Erin is not blue.
((("Erin" "is" "nice" "~")) -> ("Erin" "is" "blue" "-"))
If something is smart and not blue then it is cold.
((("something" "is" "smart" "+") ("something" "is" "blue" "~")) -> ("something" "is" "cold" "+"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Gary is not furry.
False
1
inv-proof
[(triple8)]
("Gary" "is" "furry" "-")
triple8
Erin is round.
True
2
proof
[(((triple3) -> rule4))]
("Erin" "is" "round" "+")
((triple3) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple3 triple5) -> rule3) OR ((triple3 ((((triple3) -> rule4)) -> rule1)) -> rule3))]
("Erin" "is" "smart" "-")
((triple3 triple5) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
@0: Erin is blue.[(triple1)] Erin is cold.[(triple2)] Erin is furry.[(triple3)] Erin is kind.[(triple4)] Erin is nice.[(triple5 OR ((((triple3) -> rule4)) -> rule1))] Gary is cold.[(triple7 OR ((triple12 triple6) -> rule6) OR ((((triple8 triple10) -> rule3) triple6) -> rule6) OR ((((triple8 ((triple11) -> rule1)) -> rule3) triple6) -> rule6) OR ((((triple8 ((((triple8) -> rule4)) -> rule1)) -> rule3) triple6) -> rule6))] Gary is furry.[(triple8)] Gary is nice.[(triple10 OR ((triple11) -> rule1) OR ((triple12) -> rule2) OR ((((triple8) -> rule4)) -> rule1))] Gary is not blue.[(triple6)] Gary is not kind.[(triple9)] Gary is round.[(triple11 OR ((triple8) -> rule4))] Gary is smart.[(triple12 OR ((triple8 triple10) -> rule3) OR ((triple8 ((triple11) -> rule1)) -> rule3) OR ((triple8 ((((triple8) -> rule4)) -> rule1)) -> rule3))] @1: Erin is round.[(((triple3) -> rule4))] Erin is smart.[(((triple3 triple5) -> rule3) OR ((triple3 ((((triple3) -> rule4)) -> rule1)) -> rule3))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple7
((triple12 triple6) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple8 triple10) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((((triple8 ((triple11) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((triple8 ((((triple8) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple6) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple10
((triple11) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple12) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not blue.
("Gary" "is" "blue" "-")
triple6
Gary is not kind.
("Gary" "is" "kind" "-")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple11
((triple8) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple12
((triple8 triple10) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple8 ((triple11) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((triple8 ((((triple8) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule4 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3 triple5) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple3 ((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3