Gary is kind. Gary is smart. Gary is young. Harry is green. Harry is kind. Harry is red. Harry is smart. If someone is white then they are blue. If someone is green then they are white. All smart people are red. If Gary is smart and Gary is red then Gary is green. Green people are blue. White, green people are young. If someone is smart then they are kind. If Harry is green and Harry is red then Harry is kind.
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If Gary is smart and Gary is red then Gary is green.
((("Gary" "is" "smart" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "green" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
White, green people are young.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If Harry is green and Harry is red then Harry is kind.
((("Harry" "is" "green" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple5 OR ((triple7) -> rule7) OR ((triple4 triple6) -> rule8) OR ((triple4 ((triple7) -> rule3)) -> rule8))]
("Harry" "is" "kind" "+")
triple5
((triple7) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple4 triple6) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple4 ((triple7) -> (rule3 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not red.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule3))]
("Harry" "is" "red" "-")
triple6
((triple7) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Gary is red.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "red" "+")
((triple2) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple4) -> rule5) OR ((((triple4) -> rule2)) -> rule1))]
("Harry" "is" "blue" "-")
((triple4) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
True
4
proof
[(((((triple4) -> rule2) triple4) -> rule6))]
("Harry" "is" "young" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is not green.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule4))]
("Gary" "is" "green" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is blue.
True
5
proof
[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule5) OR ((((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule2)) -> rule1))]
("Gary" "is" "blue" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple2 ((triple2) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is not white.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule2))]
("Gary" "is" "white" "-")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
@0: Gary is kind.[(triple1 OR ((triple2) -> rule7))] Gary is smart.[(triple2)] Gary is young.[(triple3 OR ((((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule2) ((triple2 ((triple2) -> rule3)) -> rule4)) -> rule6))] Harry is green.[(triple4)] Harry is kind.[(triple5 OR ((triple7) -> rule7) OR ((triple4 triple6) -> rule8) OR ((triple4 ((triple7) -> rule3)) -> rule8))] Harry is red.[(triple6 OR ((triple7) -> rule3))] Harry is smart.[(triple7)] @1: Gary is red.[(((triple2) -> rule3))] Harry is blue.[(((triple4) -> rule5) OR ((((triple4) -> rule2)) -> rule1))] Harry is white.[(((triple4) -> rule2))] @2: Gary is green.[(((triple2 ((triple2) -> rule3)) -> rule4))] Harry is young.[(((((triple4) -> rule2) triple4) -> rule6))] @3: Gary is blue.[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule5) OR ((((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule2)) -> rule1))] Gary is white.[(((((triple2 ((triple2) -> rule3)) -> rule4)) -> rule2))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
((triple2) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
((((((triple2 ((triple2) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2)) ((triple2 ((triple2) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule6 % 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" "+")
int4
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
((triple7) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple4 triple6) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple4 ((triple7) -> (rule3 % int2))) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple6
((triple7) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
((triple2) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
((((triple4) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple2 ((triple2) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((((triple2 ((triple2) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3