Dave is furry. Dave is kind. Dave is nice. Dave is smart. Dave is young. Gary is green. Gary is nice. Gary is rough. Gary is smart. Gary is young. If something is furry then it is rough. If something is kind then it is furry. If Dave is green then Dave is furry. All furry, young things are kind. All green, smart things are young. Kind, rough things are young. If Gary is kind then Gary is smart. Rough things are kind.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is furry then it is rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If Dave is green then Dave is furry.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "furry" "+"))
All furry, young things are kind.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All green, smart things are young.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
Kind, rough things are young.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If Gary is kind then Gary is smart.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "smart" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Dave is furry.
True
1
proof
[(triple1 OR ((triple2) -> rule2))]
("Dave" "is" "furry" "+")
triple1
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not young.
False
1
inv-proof
[(triple5 OR ((triple2 ((triple1) -> rule1)) -> rule6) OR ((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule6) OR ((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule6) OR ((((((triple1) -> rule1)) -> rule8) ((((triple2) -> rule2)) -> rule1)) -> rule6))]
("Dave" "is" "young" "-")
triple5
((triple2 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((((triple2) -> (rule2 % int2))) -> (rule1 % int4))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Gary is kind.
True
2
proof
[(((triple8) -> rule8))]
("Gary" "is" "kind" "+")
((triple8) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is furry.
True
3
proof
[(((((triple8) -> rule8)) -> rule2))]
("Gary" "is" "furry" "+")
((((triple8) -> (rule8 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple8) -> rule8)) -> rule2))]
("Gary" "is" "furry" "-")
((((triple8) -> (rule8 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
@0: Dave is furry.[(triple1 OR ((triple2) -> rule2))] Dave is kind.[(triple2 OR ((triple1 triple5) -> rule4) OR ((((triple1) -> rule1)) -> rule8))] Dave is nice.[(triple3)] Dave is smart.[(triple4)] Dave is young.[(triple5 OR ((triple2 ((triple1) -> rule1)) -> rule6) OR ((triple2 ((((triple2) -> rule2)) -> rule1)) -> rule6) OR ((((((triple1) -> rule1)) -> rule8) ((triple1) -> rule1)) -> rule6) OR ((((((triple1) -> rule1)) -> rule8) ((((triple2) -> rule2)) -> rule1)) -> rule6))] Gary is green.[(triple6)] Gary is nice.[(triple7)] Gary is rough.[(triple8)] Gary is smart.[(triple9 OR ((((triple8) -> rule8)) -> rule7))] Gary is young.[(triple10 OR ((triple6 triple9) -> rule5) OR ((((triple8) -> rule8) triple8) -> rule6) OR ((triple6 ((((triple8) -> rule8)) -> rule7)) -> rule5))] @1: Dave is rough.[(((triple1) -> rule1) OR ((((triple2) -> rule2)) -> rule1))] Gary is kind.[(((triple8) -> rule8))] @2: Gary is furry.[(((((triple8) -> rule8)) -> rule2))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
((triple1 triple5) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
((triple2 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) ((triple1) -> (rule1 % int3))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
((((((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((((triple2) -> (rule2 % int2))) -> (rule1 % int4))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is nice.
("Gary" "is" "nice" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((((triple8) -> (rule8 % int2))) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple6 triple9) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((((triple8) -> (rule8 % int2)) triple8) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple6 ((((triple8) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple8) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple8) -> (rule8 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2