Erin is blue. Erin is cold. Erin is kind. Erin is nice. Erin is not red. Gary is big. Gary is blue. Gary is cold. Gary is kind. Gary is nice. Gary is red. Gary is round. If Erin is nice and Erin is kind then Erin is cold. If someone is cold then they are round. If someone is cold and not big then they are round. If someone is round then they are blue. If someone is round then they are blue. If Gary is blue and Gary is kind then Gary is round. All nice, cold people are kind. Cold people are kind.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not red.
("Erin" "is" "red" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
If Erin is nice and Erin is kind then Erin is cold.
((("Erin" "is" "nice" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "cold" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is cold and not big then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If Gary is blue and Gary is kind then Gary is round.
((("Gary" "is" "blue" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "round" "+"))
All nice, cold people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Erin is cold.
True
1
proof
[(triple2 OR ((triple4 triple3) -> rule1))]
("Erin" "is" "cold" "+")
triple2
((triple4 triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not nice.
False
1
inv-proof
[(triple4)]
("Erin" "is" "nice" "-")
triple4
Erin is round.
True
2
proof
[(((triple2) -> rule2) OR ((((triple4 triple3) -> rule1)) -> rule2))]
("Erin" "is" "round" "+")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple4 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule2) OR ((((triple4 triple3) -> rule1)) -> rule2))]
("Erin" "is" "round" "-")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple4 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
@0: Erin is blue.[(triple1 OR ((((triple2) -> rule2)) -> rule4) OR ((((triple2) -> rule2)) -> rule5) OR ((((((triple4 triple3) -> rule1)) -> rule2)) -> rule4) OR ((((((triple4 triple3) -> rule1)) -> rule2)) -> rule5))] Erin is cold.[(triple2 OR ((triple4 triple3) -> rule1))] Erin is kind.[(triple3 OR ((triple2) -> rule8) OR ((triple4 triple2) -> rule7))] Erin is nice.[(triple4)] Erin is not red.[(triple5)] Gary is big.[(triple6)] Gary is blue.[(triple7 OR ((triple12) -> rule4) OR ((triple12) -> rule5) OR ((((triple8) -> rule2)) -> rule4) OR ((((triple8) -> rule2)) -> rule5))] Gary is cold.[(triple8)] Gary is kind.[(triple9 OR ((triple8) -> rule8) OR ((triple10 triple8) -> rule7))] Gary is nice.[(triple10)] Gary is red.[(triple11)] Gary is round.[(triple12 OR ((triple8) -> rule2) OR ((triple7 triple9) -> rule6) OR ((triple7 ((triple8) -> rule8)) -> rule6) OR ((triple7 ((triple10 triple8) -> rule7)) -> rule6))] @1: Erin is round.[(((triple2) -> rule2) OR ((((triple4 triple3) -> rule1)) -> rule2))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple4 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple4 triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple4 triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple3
((triple2) -> (rule8 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple4 triple2) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is not red.
("Erin" "is" "red" "-")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
((triple12) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple12) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
((triple8) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple10 triple8) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is round.
("Gary" "is" "round" "+")
triple12
((triple8) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7 triple9) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7 ((triple8) -> (rule8 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple7 ((triple10 triple8) -> (rule7 % int2))) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple4 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2