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