Dave is big. Dave is furry. Dave is round. If Dave is round and Dave is furry then Dave is young. If someone is kind and furry then they are rough. If someone is round and kind then they are rough. If someone is round then they are kind. All furry people are kind. If someone is kind then they are rough.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
If Dave is round and Dave is furry then Dave is young.
((("Dave" "is" "round" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "young" "+"))
If someone is kind and furry then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is round and kind then they are rough.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
All furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not round.
False
1
inv-proof
[(triple3)]
("Dave" "is" "round" "-")
triple3
Dave is kind.
True
2
proof
[(((triple2) -> rule5) OR ((triple3) -> rule4))]
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple3) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple3) -> rule4))]
("Dave" "is" "kind" "-")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple3) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
True
3
proof
[(((((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((triple3 ((triple2) -> rule5)) -> rule3) OR ((triple3 ((triple3) -> rule4)) -> rule3) OR ((((triple2) -> rule5) triple2) -> rule2) OR ((((triple3) -> rule4) triple2) -> rule2))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple3 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((triple3 ((triple2) -> rule5)) -> rule3) OR ((triple3 ((triple3) -> rule4)) -> rule3) OR ((((triple2) -> rule5) triple2) -> rule2) OR ((((triple3) -> rule4) triple2) -> rule2))]
("Dave" "is" "rough" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple3 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is round.[(triple3)] @1: Dave is kind.[(((triple2) -> rule5) OR ((triple3) -> rule4))] Dave is young.[(((triple3 triple2) -> rule1))] @2: Dave is rough.[(((((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((triple3 ((triple2) -> rule5)) -> rule3) OR ((triple3 ((triple3) -> rule4)) -> rule3) OR ((((triple2) -> rule5) triple2) -> rule2) OR ((((triple3) -> rule4) triple2) -> rule2))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple3) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3 triple2) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple3 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((triple3 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple3) -> (rule4 % int2)) triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2