Gary is big. Gary is furry. Gary is kind. Gary is young. Harry is big. Harry is furry. Harry is quiet. Harry is round. Harry is smart. Harry is young. If someone is young and quiet then they are round. If someone is furry then they are kind. If someone is young then they are smart. Smart people are quiet. If Gary is furry then Gary is kind. Young, furry people are kind.
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is young and quiet then they are round.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is furry then they are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is furry then Gary is kind.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "kind" "+"))
Young, furry people are kind.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Gary is young.
True
1
proof
[(triple4)]
("Gary" "is" "young" "+")
triple4
Harry is not round.
False
1
inv-proof
[(triple8 OR ((triple10 triple7) -> rule1) OR ((triple10 ((triple9) -> rule4)) -> rule1) OR ((triple10 ((((triple10) -> rule3)) -> rule4)) -> rule1))]
("Harry" "is" "round" "-")
triple8
((triple10 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple10 ((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple10 ((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Gary is smart.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple6) -> rule2) OR ((triple10 triple6) -> rule6))]
("Harry" "is" "kind" "-")
((triple6) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple10 triple6) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple4) -> rule3)) -> rule4))]
("Gary" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule4))]
("Gary" "is" "quiet" "-")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
True
5
proof
[(((triple4 ((((triple4) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "round" "+")
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not round.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule3)) -> rule4)) -> rule1))]
("Gary" "is" "round" "-")
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
@0: Gary is big.[(triple1)] Gary is furry.[(triple2)] Gary is kind.[(triple3 OR ((triple2) -> rule2) OR ((triple2) -> rule5) OR ((triple4 triple2) -> rule6))] Gary is young.[(triple4)] Harry is big.[(triple5)] Harry is furry.[(triple6)] Harry is quiet.[(triple7 OR ((triple9) -> rule4) OR ((((triple10) -> rule3)) -> rule4))] Harry is round.[(triple8 OR ((triple10 triple7) -> rule1) OR ((triple10 ((triple9) -> rule4)) -> rule1) OR ((triple10 ((((triple10) -> rule3)) -> rule4)) -> rule1))] Harry is smart.[(triple9 OR ((triple10) -> rule3))] Harry is young.[(triple10)] @1: Gary is smart.[(((triple4) -> rule3))] Harry is kind.[(((triple6) -> rule2) OR ((triple10 triple6) -> rule6))] @2: Gary is quiet.[(((((triple4) -> rule3)) -> rule4))] @3: Gary is round.[(((triple4 ((((triple4) -> rule3)) -> rule4)) -> rule1))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
((triple2) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple2) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple4 triple2) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
((triple9) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple8
((triple10 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple10 ((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((triple10 ((((triple10) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
triple9
((triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((triple10 triple6) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3