Gary is kind. Gary is nice. Gary is white. All nice, young people are kind. All kind, nice people are white. If someone is cold and kind then they are nice. If someone is red then they are young. Cold people are white. All young people are cold. If someone is white then they are red. Kind people are nice.
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
All nice, young people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All kind, nice people are white.
((("someone" "is" "kind" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is cold and kind then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
All young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Gary is kind.
True
1
proof
[(triple1 OR ((triple2 ((((triple3) -> rule7)) -> rule4)) -> rule1))]
("Gary" "is" "kind" "+")
triple1
((triple2 ((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is not white.
False
1
inv-proof
[(triple3 OR ((triple1 triple2) -> rule2) OR ((triple1 ((triple1) -> rule8)) -> rule2))]
("Gary" "is" "white" "-")
triple3
((triple1 triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple1 ((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
True
2
proof
[(((triple3) -> rule7) OR ((((triple1 triple2) -> rule2)) -> rule7) OR ((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7))]
("Gary" "is" "red" "+")
((triple3) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not red.
False
2
inv-proof
[(((triple3) -> rule7) OR ((((triple1 triple2) -> rule2)) -> rule7) OR ((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7))]
("Gary" "is" "red" "-")
((triple3) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is young.
True
3
proof
[(((((triple3) -> rule7)) -> rule4) OR ((((((triple1 triple2) -> rule2)) -> rule7)) -> rule4) OR ((((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7)) -> rule4))]
("Gary" "is" "young" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple1 triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is not young.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule4) OR ((((((triple1 triple2) -> rule2)) -> rule7)) -> rule4) OR ((((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7)) -> rule4))]
("Gary" "is" "young" "-")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple1 triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is cold.
True
4
proof
[(((((((triple3) -> rule7)) -> rule4)) -> rule6) OR ((((((((triple1 triple2) -> rule2)) -> rule7)) -> rule4)) -> rule6) OR ((((((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7)) -> rule4)) -> rule6))]
("Gary" "is" "cold" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((((triple1 triple2) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((((triple1 ((triple1) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
int5
Gary is not cold.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule4)) -> rule6) OR ((((((((triple1 triple2) -> rule2)) -> rule7)) -> rule4)) -> rule6) OR ((((((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7)) -> rule4)) -> rule6))]
("Gary" "is" "cold" "-")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((((triple1 triple2) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((((triple1 ((triple1) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
int5
@0: Gary is kind.[(triple1 OR ((triple2 ((((triple3) -> rule7)) -> rule4)) -> rule1))] Gary is nice.[(triple2 OR ((triple1) -> rule8) OR ((((((((triple3) -> rule7)) -> rule4)) -> rule6) triple1) -> rule3))] Gary is white.[(triple3 OR ((triple1 triple2) -> rule2) OR ((triple1 ((triple1) -> rule8)) -> rule2))] @1: Gary is red.[(((triple3) -> rule7) OR ((((triple1 triple2) -> rule2)) -> rule7) OR ((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7))] @2: Gary is young.[(((((triple3) -> rule7)) -> rule4) OR ((((((triple1 triple2) -> rule2)) -> rule7)) -> rule4) OR ((((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7)) -> rule4))] @3: Gary is cold.[(((((((triple3) -> rule7)) -> rule4)) -> rule6) OR ((((((((triple1 triple2) -> rule2)) -> rule7)) -> rule4)) -> rule6) OR ((((((((triple1 ((triple1) -> rule8)) -> rule2)) -> rule7)) -> rule4)) -> rule6))]
Gary is kind.
("Gary" "is" "kind" "+")
triple1
((triple2 ((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple2
((triple1) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((((((triple3) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
((triple1 ((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((((triple1 triple2) -> (rule2 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((((triple1 triple2) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple3) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((((triple1 triple2) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
((((((((triple1 ((triple1) -> (rule8 % int5))) -> (rule2 % int4))) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
int5