Gary is blue. Gary is cold. Gary is smart. Green, blue people are cold. All white people are quiet. All quiet people are smart. All white people are smart. If someone is red then they are white. All cold people are red.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Green, blue people are cold.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All white people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Gary is blue.
True
1
proof
[(triple1)]
("Gary" "is" "blue" "+")
triple1
Gary is not smart.
False
1
inv-proof
[(triple3 OR ((((((triple2) -> rule6)) -> rule5)) -> rule4) OR ((((((((triple2) -> rule6)) -> rule5)) -> rule2)) -> rule3))]
("Gary" "is" "smart" "-")
triple3
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is red.
True
2
proof
[(((triple2) -> rule6))]
("Gary" "is" "red" "+")
((triple2) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple2) -> rule6))]
("Gary" "is" "red" "-")
((triple2) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
True
3
proof
[(((((triple2) -> rule6)) -> rule5))]
("Gary" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not white.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule5))]
("Gary" "is" "white" "-")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
True
4
proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
("Gary" "is" "quiet" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not quiet.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
("Gary" "is" "quiet" "-")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
@0: Gary is blue.[(triple1)] Gary is cold.[(triple2)] Gary is smart.[(triple3 OR ((((((triple2) -> rule6)) -> rule5)) -> rule4) OR ((((((((triple2) -> rule6)) -> rule5)) -> rule2)) -> rule3))] @1: Gary is red.[(((triple2) -> rule6))] @2: Gary is white.[(((((triple2) -> rule6)) -> rule5))] @3: Gary is quiet.[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((((triple2) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
((triple2) -> (rule6 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3