Bob is furry. Bob is green. Bob is nice. Bob is quiet. Bob is round. Bob is smart. Bob is young. Harry is furry. Harry is green. Harry is nice. Harry is quiet. Harry is round. Harry is smart. Harry is young. If someone is smart and round then they are young. If Bob is nice and Bob is round then Bob is furry. If someone is furry then they are smart. All young people are nice. If Bob is green and Bob is smart then Bob is nice. If someone is furry then they are round.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is smart and round then they are young.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If Bob is nice and Bob is round then Bob is furry.
((("Bob" "is" "nice" "+") ("Bob" "is" "round" "+")) -> ("Bob" "is" "furry" "+"))
If someone is furry then they are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If Bob is green and Bob is smart then Bob is nice.
((("Bob" "is" "green" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "nice" "+"))
If someone is furry then they are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Harry is round.
True
1
proof
[(triple12 OR ((triple8) -> rule6))]
("Harry" "is" "round" "+")
triple12
((triple8) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is not round.
False
1
inv-proof
[(triple5 OR ((triple1) -> rule6))]
("Bob" "is" "round" "-")
triple5
((triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
@0: Bob is furry.[(triple1 OR ((triple3 triple5) -> rule2) OR ((((triple7) -> rule4) triple5) -> rule2) OR ((((triple2 triple6) -> rule5) triple5) -> rule2) OR ((((((triple6 triple5) -> rule1)) -> rule4) triple5) -> rule2))] Bob is green.[(triple2)] Bob is nice.[(triple3 OR ((triple7) -> rule4) OR ((triple2 triple6) -> rule5) OR ((((triple6 triple5) -> rule1)) -> rule4) OR ((triple2 ((triple1) -> rule3)) -> rule5) OR ((((triple6 ((triple1) -> rule6)) -> rule1)) -> rule4) OR ((((((triple1) -> rule3) triple5) -> rule1)) -> rule4) OR ((((((triple1) -> rule3) ((triple1) -> rule6)) -> rule1)) -> rule4))] Bob is quiet.[(triple4)] Bob is round.[(triple5 OR ((triple1) -> rule6))] Bob is smart.[(triple6 OR ((triple1) -> rule3) OR ((((triple3 triple5) -> rule2)) -> rule3) OR ((((((triple7) -> rule4) triple5) -> rule2)) -> rule3))] Bob is young.[(triple7 OR ((triple6 triple5) -> rule1) OR ((triple6 ((triple1) -> rule6)) -> rule1) OR ((((triple1) -> rule3) triple5) -> rule1) OR ((((triple1) -> rule3) ((triple1) -> rule6)) -> rule1) OR ((((((triple3 triple5) -> rule2)) -> rule3) triple5) -> rule1) OR ((((((triple3 triple5) -> rule2)) -> rule3) ((triple1) -> rule6)) -> rule1))] Harry is furry.[(triple8)] Harry is green.[(triple9)] Harry is nice.[(triple10 OR ((triple14) -> rule4) OR ((((triple13 triple12) -> rule1)) -> rule4) OR ((((triple13 ((triple8) -> rule6)) -> rule1)) -> rule4) OR ((((((triple8) -> rule3) triple12) -> rule1)) -> rule4) OR ((((((triple8) -> rule3) ((triple8) -> rule6)) -> rule1)) -> rule4))] Harry is quiet.[(triple11)] Harry is round.[(triple12 OR ((triple8) -> rule6))] Harry is smart.[(triple13 OR ((triple8) -> rule3))] Harry is young.[(triple14 OR ((triple13 triple12) -> rule1) OR ((triple13 ((triple8) -> rule6)) -> rule1) OR ((((triple8) -> rule3) triple12) -> rule1) OR ((((triple8) -> rule3) ((triple8) -> rule6)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple3 triple5) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple7) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2 triple6) -> (rule5 % int2)) triple5) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple6 triple5) -> (rule1 % int3))) -> (rule4 % int2)) triple5) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple7) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 triple6) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple6 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
((triple2 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple6 ((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
((((((triple1) -> (rule3 % int3)) triple5) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple1) -> (rule3 % int4)) ((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
((triple1) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((((triple7) -> (rule4 % int3)) triple5) -> (rule2 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple6 triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple6 ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
((((triple1) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
((((((triple3 triple5) -> (rule2 % int3))) -> (rule3 % int2)) triple5) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
((((((triple3 triple5) -> (rule2 % int4))) -> (rule3 % int3)) ((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple14) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple13 triple12) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple13 ((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((((triple8) -> (rule3 % int3)) triple12) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple8) -> (rule3 % int4)) ((triple8) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
((triple8) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple13
((triple8) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple13 triple12) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple13 ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple8) -> (rule3 % int2)) triple12) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple8) -> (rule3 % int3)) ((triple8) -> (rule6 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3