Gary is young. All young, smart things are furry. If Gary is young and Gary is smart then Gary is white. White, young things are nice. If Gary is young then Gary is smart. If Gary is smart and Gary is white then Gary is cold. Young things are cold. If something is young and furry then it is white. If something is furry and rough then it is nice.
Gary is young.
("Gary" "is" "young" "+")
All young, smart things are furry.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Gary is young and Gary is smart then Gary is white.
((("Gary" "is" "young" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "white" "+"))
White, young things are nice.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Gary is young then Gary is smart.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "smart" "+"))
If Gary is smart and Gary is white then Gary is cold.
((("Gary" "is" "smart" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "cold" "+"))
Young things are cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
If something is young and furry then it is white.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is furry and rough then it is nice.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Gary is young.
True
1
proof
[(triple1)]
("Gary" "is" "young" "+")
triple1
Gary is not young.
False
1
inv-proof
[(triple1)]
("Gary" "is" "young" "-")
triple1
Gary is cold.
True
2
proof
[(((triple1) -> rule6) OR ((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule2)) -> rule5) OR ((((triple1) -> rule4) ((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule7)) -> rule5))]
("Gary" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple1) -> (rule4 % int4)) ((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Gary" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("Gary" "is" "furry" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not furry.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("Gary" "is" "furry" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
True
6
proof
[(((((triple1 ((triple1) -> rule4)) -> rule2) triple1) -> rule3) OR ((((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule7) triple1) -> rule3))]
("Gary" "is" "nice" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not nice.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule2) triple1) -> rule3) OR ((((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule7) triple1) -> rule3))]
("Gary" "is" "nice" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
@0: Gary is young.[(triple1)] @1: Gary is cold.[(((triple1) -> rule6) OR ((((triple1) -> rule4) ((triple1 ((triple1) -> rule4)) -> rule2)) -> rule5) OR ((((triple1) -> rule4) ((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule7)) -> rule5))] Gary is smart.[(((triple1) -> rule4))] @2: Gary is furry.[(((triple1 ((triple1) -> rule4)) -> rule1))] Gary is white.[(((triple1 ((triple1) -> rule4)) -> rule2) OR ((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule7))] @3: Gary is nice.[(((((triple1 ((triple1) -> rule4)) -> rule2) triple1) -> rule3) OR ((((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule7) triple1) -> rule3))]
Gary is young.
("Gary" "is" "young" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple1) -> (rule4 % int3)) ((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple1) -> (rule4 % int4)) ((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((triple1 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple1 ((triple1 ((triple1) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule7 % int2)) triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4