Dave is big. Dave is furry. Dave is green. Dave is round. Dave is smart. Dave is white. Dave is young. White people are round. If someone is white then they are green. If someone is smart and big then they are furry. All round, smart people are big. All smart people are young. If Dave is white and Dave is furry then Dave is young.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
White people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and big then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
All round, smart people are big.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
If Dave is white and Dave is furry then Dave is young.
((("Dave" "is" "white" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "young" "+"))
Dave is green.
True
1
proof
[(triple3 OR ((triple6) -> rule2))]
("Dave" "is" "green" "+")
triple3
((triple6) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not smart.
False
1
inv-proof
[(triple5)]
("Dave" "is" "smart" "-")
triple5
@0: Dave is big.[(triple1 OR ((triple4 triple5) -> rule4) OR ((((triple6) -> rule1) triple5) -> rule4))] Dave is furry.[(triple2 OR ((triple5 triple1) -> rule3) OR ((triple5 ((triple4 triple5) -> rule4)) -> rule3) OR ((triple5 ((((triple6) -> rule1) triple5) -> rule4)) -> rule3))] Dave is green.[(triple3 OR ((triple6) -> rule2))] Dave is round.[(triple4 OR ((triple6) -> rule1))] Dave is smart.[(triple5)] Dave is white.[(triple6)] Dave is young.[(triple7 OR ((triple5) -> rule5) OR ((triple6 triple2) -> rule6) OR ((triple6 ((triple5 triple1) -> rule3)) -> rule6) OR ((triple6 ((triple5 ((triple4 triple5) -> rule4)) -> rule3)) -> rule6) OR ((triple6 ((triple5 ((((triple6) -> rule1) triple5) -> rule4)) -> rule3)) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple4 triple5) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple6) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple5 triple1) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple5 ((triple4 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple5 ((((triple6) -> (rule1 % int3)) triple5) -> (rule4 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is green.
("Dave" "is" "green" "+")
triple3
((triple6) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple6) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
((triple5) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple6 triple2) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple6 ((triple5 triple1) -> (rule3 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((triple6 ((triple5 ((triple4 triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((triple6 ((triple5 ((((triple6) -> (rule1 % int4)) triple5) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is round.
("Dave" "is" "round" "+")
int4