Dave is furry. Dave is nice. Dave is red. Dave is round. Dave is smart. Dave is young. Gary is big. Gary is nice. Gary is round. Gary is young. If someone is big then they are smart. If someone is round then they are nice. Smart, round people are red. All big, furry people are red. Smart people are young. Big, red people are smart. If Gary is red then Gary is round. If someone is young and big then they are furry.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is big then they are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is round then they are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Smart, round people are red.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All big, furry people are red.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Big, red people are smart.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If Gary is red then Gary is round.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "round" "+"))
If someone is young and big then they are furry.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Dave is red.
True
1
proof
[(triple3 OR ((triple5 triple4) -> rule3))]
("Dave" "is" "red" "+")
triple3
((triple5 triple4) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not furry.
False
1
inv-proof
[(triple1)]
("Dave" "is" "furry" "-")
triple1
Gary is furry.
True
3
proof
[(((triple10 triple7) -> rule8) OR ((((((triple7) -> rule1)) -> rule5) triple7) -> rule8))]
("Gary" "is" "furry" "+")
((triple10 triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((((triple7) -> (rule1 % int3))) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not furry.
False
3
inv-proof
[(((triple10 triple7) -> rule8) OR ((((((triple7) -> rule1)) -> rule5) triple7) -> rule8))]
("Gary" "is" "furry" "-")
((triple10 triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((((triple7) -> (rule1 % int3))) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
@0: Dave is furry.[(triple1)] Dave is nice.[(triple2 OR ((triple4) -> rule2))] Dave is red.[(triple3 OR ((triple5 triple4) -> rule3))] Dave is round.[(triple4)] Dave is smart.[(triple5)] Dave is young.[(triple6 OR ((triple5) -> rule5))] Gary is big.[(triple7)] Gary is nice.[(triple8 OR ((triple9) -> rule2) OR ((((((triple7 ((triple10 triple7) -> rule8)) -> rule4)) -> rule7)) -> rule2) OR ((((((triple7 ((((((triple7) -> rule1)) -> rule5) triple7) -> rule8)) -> rule4)) -> rule7)) -> rule2))] Gary is round.[(triple9 OR ((((triple7 ((triple10 triple7) -> rule8)) -> rule4)) -> rule7) OR ((((triple7 ((((((triple7) -> rule1)) -> rule5) triple7) -> rule8)) -> rule4)) -> rule7))] Gary is young.[(triple10 OR ((((triple7) -> rule1)) -> rule5))] @1: Gary is furry.[(((triple10 triple7) -> rule8) OR ((((((triple7) -> rule1)) -> rule5) triple7) -> rule8))] Gary is smart.[(((triple7) -> rule1) OR ((triple7 ((triple7 ((triple10 triple7) -> rule8)) -> rule4)) -> rule6))] @2: Gary is red.[(((triple7 ((triple10 triple7) -> rule8)) -> rule4) OR ((((triple7) -> rule1) triple9) -> rule3) OR ((triple7 ((((((triple7) -> rule1)) -> rule5) triple7) -> rule8)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple2
((triple4) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple3
((triple5 triple4) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
((triple5) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
((triple9) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((((triple7 ((triple10 triple7) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
((((((triple7 ((((((triple7) -> (rule1 % int6))) -> (rule5 % int5)) triple7) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
int5
Gary is smart.
("Gary" "is" "smart" "+")
int6
Gary is round.
("Gary" "is" "round" "+")
triple9
((((triple7 ((triple10 triple7) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
((((triple7 ((((((triple7) -> (rule1 % int5))) -> (rule5 % int4)) triple7) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is young.
("Gary" "is" "young" "+")
triple10
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple10 triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((((triple7) -> (rule1 % int3))) -> (rule5 % int2)) triple7) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
((triple7 ((triple7 ((triple10 triple7) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
((triple7 ((triple10 triple7) -> (rule8 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int2)) triple9) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((triple7 ((((((triple7) -> (rule1 % int4))) -> (rule5 % int3)) triple7) -> (rule8 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4