Dave is furry. Dave is green. Dave is smart. If something is furry then it is round. Green, nice things are round. All green things are kind. All nice, green things are round. Nice, smart things are rough. If Dave is round then Dave is green. Smart, rough things are green. If something is green and smart then it is nice.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If something is furry then it is round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
Green, nice things are round.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All nice, green things are round.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
Nice, smart things are rough.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If Dave is round then Dave is green.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "green" "+"))
Smart, rough things are green.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is green and smart then it is nice.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Dave is smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "+")
triple3
Dave is not smart.
False
1
inv-proof
[(triple3)]
("Dave" "is" "smart" "-")
triple3
@0: Dave is furry.[(triple1)] Dave is green.[(triple2 OR ((((triple1) -> rule1)) -> rule6))] Dave is smart.[(triple3)] @1: Dave is kind.[(((triple2) -> rule3) OR ((((((triple1) -> rule1)) -> rule6)) -> rule3))] Dave is nice.[(((triple2 triple3) -> rule8) OR ((((((triple1) -> rule1)) -> rule6) triple3) -> rule8))] Dave is round.[(((triple1) -> rule1) OR ((triple2 ((triple2 triple3) -> rule8)) -> rule2) OR ((((triple2 triple3) -> rule8) triple2) -> rule4))] @2: Dave is rough.[(((((triple2 triple3) -> rule8) triple3) -> rule5) OR ((((((((triple1) -> rule1)) -> rule6) triple3) -> rule8) triple3) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((triple2 triple3) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple3) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
((triple1) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple2 ((triple2 triple3) -> (rule8 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple2 triple3) -> (rule8 % int2)) triple2) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2 triple3) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3)) triple3) -> (rule8 % int2)) triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4