Gary is furry. Gary is kind. Gary is rough. Gary is smart. Harry is furry. Harry is smart. Harry is young. If something is young and quiet then it is furry. All smart things are rough. If something is kind then it is quiet. Kind, quiet things are furry. All kind things are furry. All round, quiet things are smart. Quiet things are round. If something is furry then it is kind.
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young and quiet then it is furry.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All smart things are rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Kind, quiet things are furry.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All round, quiet things are smart.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Harry is smart.
True
1
proof
[(triple6 OR ((((((((triple5) -> rule8)) -> rule3)) -> rule7) ((((triple5) -> rule8)) -> rule3)) -> rule6))]
("Harry" "is" "smart" "+")
triple6
((((((((triple5) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple5) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is not young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "-")
triple7
@0: Gary is furry.[(triple1 OR ((triple2) -> rule5) OR ((triple2 ((triple2) -> rule3)) -> rule4))] Gary is kind.[(triple2 OR ((triple1) -> rule8))] Gary is rough.[(triple3 OR ((triple4) -> rule2) OR ((((((((triple2) -> rule3)) -> rule7) ((triple2) -> rule3)) -> rule6)) -> rule2) OR ((((((((triple2) -> rule3)) -> rule7) ((((triple1) -> rule8)) -> rule3)) -> rule6)) -> rule2) OR ((((((((((triple1) -> rule8)) -> rule3)) -> rule7) ((triple2) -> rule3)) -> rule6)) -> rule2) OR ((((((((((triple1) -> rule8)) -> rule3)) -> rule7) ((((triple1) -> rule8)) -> rule3)) -> rule6)) -> rule2))] Gary is smart.[(triple4 OR ((((((triple2) -> rule3)) -> rule7) ((triple2) -> rule3)) -> rule6) OR ((((((triple2) -> rule3)) -> rule7) ((((triple1) -> rule8)) -> rule3)) -> rule6) OR ((((((((triple1) -> rule8)) -> rule3)) -> rule7) ((triple2) -> rule3)) -> rule6) OR ((((((((triple1) -> rule8)) -> rule3)) -> rule7) ((((triple1) -> rule8)) -> rule3)) -> rule6))] Harry is furry.[(triple5)] Harry is smart.[(triple6 OR ((((((((triple5) -> rule8)) -> rule3)) -> rule7) ((((triple5) -> rule8)) -> rule3)) -> rule6))] Harry is young.[(triple7)] @1: Gary is quiet.[(((triple2) -> rule3) OR ((((triple1) -> rule8)) -> rule3))] Harry is kind.[(((triple5) -> rule8))] Harry is rough.[(((triple6) -> rule2) OR ((((((((((triple5) -> rule8)) -> rule3)) -> rule7) ((((triple5) -> rule8)) -> rule3)) -> rule6)) -> rule2))] @2: Gary is round.[(((((triple2) -> rule3)) -> rule7) OR ((((((triple1) -> rule8)) -> rule3)) -> rule7))] Harry is quiet.[(((((triple5) -> rule8)) -> rule3))] @3: Harry is round.[(((((((triple5) -> rule8)) -> rule3)) -> rule7))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
((triple2) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple2
((triple1) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple3
((triple4) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((((((((triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((triple2) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((((((triple2) -> (rule3 % int5))) -> (rule7 % int4)) ((((triple1) -> (rule8 % int3))) -> (rule3 % int5))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
int5
((((((((((triple1) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((triple2) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
((((((((((triple1) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
Gary is smart.
("Gary" "is" "smart" "+")
triple4
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule8 % int2))) -> (rule3 % int4))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
((((((((triple1) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((triple2) -> (rule3 % int3))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
((((((((triple1) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple1) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is smart.
("Harry" "is" "smart" "+")
triple6
((((((((triple5) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule7 % int2)) ((((triple5) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((triple5) -> (rule8 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple6) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((((((((triple5) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple5) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule6 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5
Gary is round.
("Gary" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple5) -> (rule8 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple5) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3