Gary is blue. Gary is nice. Gary is quiet. If Gary is quiet and Gary is cold then Gary is nice. If Gary is kind and Gary is quiet then Gary is nice. If someone is quiet then they are not red. If someone is red then they are not nice. Kind people are cold. Nice people are kind. Cold people are white. If someone is red and not kind then they are white.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If Gary is quiet and Gary is cold then Gary is nice.
((("Gary" "is" "quiet" "+") ("Gary" "is" "cold" "+")) -> ("Gary" "is" "nice" "+"))
If Gary is kind and Gary is quiet then Gary is nice.
((("Gary" "is" "kind" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "nice" "+"))
If someone is quiet then they are not red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "-"))
If someone is red then they are not nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is red and not kind then they are white.
((("someone" "is" "red" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "white" "+"))
Gary is quiet.
True
1
proof
[(triple3)]
("Gary" "is" "quiet" "+")
triple3
Gary is not blue.
False
1
inv-proof
[(triple1)]
("Gary" "is" "blue" "-")
triple1
Gary is not red.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "red" "-")
((triple3) -> (rule3 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is not kind.
False
2
inv-proof
[(((triple2) -> rule6))]
("Gary" "is" "kind" "-")
((triple2) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is cold.
True
3
proof
[(((((triple2) -> rule6)) -> rule5))]
("Gary" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule5))]
("Gary" "is" "cold" "-")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
True
4
proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule7))]
("Gary" "is" "white" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule7))]
("Gary" "is" "white" "-")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
@0: Gary is blue.[(triple1)] Gary is nice.[(triple2)] Gary is quiet.[(triple3)] @1: Gary is kind.[(((triple2) -> rule6))] Gary is not red.[(((triple3) -> rule3))] @2: Gary is cold.[(((((triple2) -> rule6)) -> rule5))] @3: Gary is white.[(((((((triple2) -> rule6)) -> rule5)) -> rule7))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple2) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not red.
("Gary" "is" "red" "-")
((triple3) -> (rule3 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3