Gary is nice. Gary is quiet. Gary is young. If someone is big then they are young. Green, young people are quiet. If Gary is quiet and Gary is young then Gary is cold. If someone is quiet then they are kind. If Gary is young and Gary is quiet then Gary is big. If someone is kind and big then they are cold. All kind, quiet people are green. If someone is big then they are kind.
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Green, young people are quiet.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is quiet and Gary is young then Gary is cold.
((("Gary" "is" "quiet" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "cold" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Gary is young and Gary is quiet then Gary is big.
((("Gary" "is" "young" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "big" "+"))
If someone is kind and big then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All kind, quiet people are green.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Gary is nice.
True
1
proof
[(triple1)]
("Gary" "is" "nice" "+")
triple1
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Gary is cold.
True
3
proof
[(((triple2 triple3) -> rule3) OR ((((triple2) -> rule4) ((triple3 triple2) -> rule5)) -> rule6) OR ((((((triple3 triple2) -> rule5)) -> rule8) ((triple3 triple2) -> rule5)) -> rule6))]
("Gary" "is" "cold" "+")
((triple2 triple3) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple2) -> (rule4 % int3)) ((triple3 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple3 triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple3 triple2) -> (rule5 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not kind.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple3 triple2) -> rule5)) -> rule8))]
("Gary" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple3 triple2) -> (rule5 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule7) OR ((((((triple3 triple2) -> rule5)) -> rule8) triple2) -> rule7))]
("Gary" "is" "green" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple3 triple2) -> (rule5 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not green.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule7) OR ((((((triple3 triple2) -> rule5)) -> rule8) triple2) -> rule7))]
("Gary" "is" "green" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple3 triple2) -> (rule5 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
@0: Gary is nice.[(triple1)] Gary is quiet.[(triple2)] Gary is young.[(triple3)] @1: Gary is big.[(((triple3 triple2) -> rule5))] Gary is cold.[(((triple2 triple3) -> rule3) OR ((((triple2) -> rule4) ((triple3 triple2) -> rule5)) -> rule6) OR ((((((triple3 triple2) -> rule5)) -> rule8) ((triple3 triple2) -> rule5)) -> rule6))] Gary is kind.[(((triple2) -> rule4) OR ((((triple3 triple2) -> rule5)) -> rule8))] @2: Gary is green.[(((((triple2) -> rule4) triple2) -> rule7) OR ((((((triple3 triple2) -> rule5)) -> rule8) triple2) -> rule7))]
Gary is nice.
("Gary" "is" "nice" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
((triple3 triple2) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((triple2 triple3) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple2) -> (rule4 % int3)) ((triple3 triple2) -> (rule5 % int2))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple3 triple2) -> (rule5 % int3))) -> (rule8 % int2)) ((triple3 triple2) -> (rule5 % int3))) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple3 triple2) -> (rule5 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple3 triple2) -> (rule5 % int3))) -> (rule8 % int2)) triple2) -> (rule7 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3